Frama-C-discuss mailing list archives

dcok at grammatech.com (David Cok) · Thu, 07 Nov 2013 17:15:12 -0500

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?

- David

On 11/7/2013 4:54 PM, Pascal Cuoq wrote:
> On Thu, Nov 7, 2013 at 10:26 PM, John Regehr <regehr at cs.utah.edu 
> <mailto:regehr at cs.utah.edu>> wrote:
>
>
>     If I understand correctly, Jessie's three integer models are:
>
>     - math -- infinite range
>     - modulo -- both signed and unsigned behave as if two's complement
>     - strict -- no overflow permitted
>
>     The problem is that none of these is a match for C. In C, unsigned
>     integers follow the modulo rules and signed integers follow the
>     strict rules. Is there a way to get the C integer model in Jessie?
>      Otherwise it seems like I might be stuck with some strange tradeoffs.
>
>
> I second the wish for a C mode ---as a user. However, here is what I 
> think a hypothetical weakest precondition plug-in implementor might say:
>
> "math" is not sound for any serious definition of sound. Instead of 
> weakening the definition of "sound" to the point of ridiculousness 
> (http://soundiness.org/documents/InDefenseOfUnsoundness.pdf ---damn, 
> another blog post to write), we can choose the honorable path and 
> forget that "math" even exists.
>
> "modulo" inserts modulo operations everywhere, making proof 
> obligations impossibly hard for existing automatic provers. That it is 
> unusable in practice might actually be good news, as it too is ---as 
> you rightly point out--- unsound with respect to the C standard 
> (although it may be sound with respect to a specific compiler, perhaps 
> used with specific options).
>
> If a function happens to be verifiable with "strict", that is, if for 
> the inputs it expects, it never relies on the wrap-around behavior of 
> unsigned overflow, then it should be verified with "strict". With 
> respect to the "C" mode that regretfully does not exist, this only 
> adds additional proof obligations, which should individually be easy 
> to prove, instead of sprinkling existing proof obligations with modulo 
> operations that make them extremely difficult to tackle for existing 
> automatic provers. Any function verified with "strict" works when 
> executed in C. The only issue is that some functions that work 
> according to the C standard cannot be verified with "strict", because 
> they rely on unsigned overflow behavior.
>
> Something that would be better than "modulo", and better than the "C" 
> mode you request, is a mode similar to "strict" but that would let the 
> operator specify only the few unsigned operations that are supposed to 
> wrap around, and would only insert modulo operations for these ones. 
> The other overflows, that wouldn't harm according to the standard, 
> would still be assumed not to happen (no modulo inserted) and proved 
> not to happen (but as long as it is true that they do not happen, why 
> not prove it as a useful intermediate lemma?). This would likely work 
> quite well in practice.
>
> Perhaps real implementors of weakest precondition Frama-C plug-ins 
> will want to differ. This is only the opinion of a hypothetical character.
>
> 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/20131107/e4e9a088/attachment-0001.html>

Frama-C-discuss mailing list archives

[Frama-c-discuss] JessieIntegerModel question