--- layout: fc_discuss_archives title: Message 88 from Frama-C-discuss on November 2013 ---
Regarding Pascal's question at the end of his note about which tool has the responsibility for choices about integer vs. bit-vector representations. In my question, Pascal, I was presuming that Frama-C created a logical model that is a translation of the program + specification semantics. If that model is, say in SMTLIB, the modeler needs to choose whether to model 'int i = 1' as a mathematical integer or as a bit-vector (which is the fixed-width integer logic) and choose the corresponding SMT logic to represent it. So that is why I asked whether Frama-C developers have considered mapping C's fixed-width integer types into a BitVector logic. Essentially, if you really want precision, if the programming language uses fixed-width integers (as C does), they should be modeled as bit-vectors (which includes normal integer operations); if the programming language uses infinite-precision integers (as it could), then model them as mathematical integers. Part of the problem is that people often think of integers as infinite precision when reading a program. - David On 11/12/2013 5:36 AM, Pascal Cuoq wrote: > On Tue, Nov 12, 2013 at 1:21 AM, Claude Marche <Claude.Marche at inria.fr > <mailto:Claude.Marche at inria.fr>> wrote: > > > On 11/07/2013 11:15 PM, David Cok wrote: > > Using a bit-vector logic avoids the modulo operations, but also, I > > suspect, introduces difficulties in mapping to and from integer > > variables. Has that been tried in practice in Frama-C? > > "in Frama-C" is not precise enough. Surely Value plugin supports > mixing > bitwise and arithmetic operators. For the Jessie plugin the answer > is no. > > > The value analysis plugin's abstract domain can sometimes do a good > job on code that mixes bit and arithmetic operations because it > represents small sets of integers as sets (without loss of > information) and large sets as intervals with congruence information > (that may allow to capture some information about the highest- and > lowest-weight bits), but it is no panacea. > > Sven Mattsen studied a representation of sets of integers as Binary > Decision Diagrams during a personal student project. The initial goal > was to represent all integer sets without loss of information, so > that program variables for which bitwise information was known would > be represented very compactly, variables for which bounds were known > (and perhaps congruence information) would also be represented very > compactly, and both arithmetic and bit operations would give optimal > results (for a nonrelational abstract interpreter). > One conclusion of this study was that the original goal may have been > slightly quixotic in presence of integer multiplications in the target > program. > > Keeping the discussion about the deductive Frama-C plugins it also is > about, I have a question: why shouldn't it be the responsibility of > the automated theorem prover (and thus outside the realm of Frama-C > and its plugins) to interpret some integers as vectors of bits and > others as mathematical integers? It is not as if Frama-C plugins are > voluntarily mixing bit and arithmetic operations: they end up being > mixed up in the proof obligation because the language allows to mix > them up in programs. > > It seems to me that any pre-analysis to identify integer variables > worth representing as a vector of bits should be implemented, for > maximum usefulness, as initial phase of an automated prover working on > the SMT formulas generated by a weakest precondition generator > oblivious to the issue. > > So, to sum up, why should this "[have] been tried in practice in > Frama-C?". Shouldn't it be tried in practice in an automated prover > that Frama-C and other verification tools could blissfully use? > > Pascal > > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131112/c7859bb2/attachment.html>