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


  • Subject: [Frama-c-discuss] JessieIntegerModel question
  • From: dcok at grammatech.com (David Cok)
  • Date: Thu, 07 Nov 2013 17:15:12 -0500
  • In-reply-to: <CAOH62Jg5UyBhM6T3Fke9+gXaruBoQvRd5WB-m7=qGq-W0ue1Jw@mail.gmail.com>
  • References: <527C0595.5040000@cs.utah.edu> <CAOH62Jg5UyBhM6T3Fke9+gXaruBoQvRd5WB-m7=qGq-W0ue1Jw@mail.gmail.com>

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>