--- layout: fc_discuss_archives title: Message 74 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] JessieIntegerModel question




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.


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