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 Thu, Nov 7, 2013 at 10:26 PM, John Regehr <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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131107/59f06733/attachment.html>