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

On Tue, Nov 12, 2013 at 1:21 AM, Claude Marche <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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131112/e7627e57/attachment.html>