--- layout: fc_discuss_archives title: Message 88 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] JessieIntegerModel question



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>