Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>