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] WP and unsigned int

Hi,

A follow-up question. I’m now using the TIP mode and saving my work in sessions (thanks again).

I’m wondering what the recommended way is to maintain a session using version control. I don’t expect multiple developers to be working on the proof concurrently (and hence am not concerned about merges) — rather, there is one developer working on the proof and the rest may wish to replay it. Is it necessary or recommended to distribute the entire session directory with the program source in order to reproduce the proof? Or do I just need <session-dir>/script, for example?

Thanks,
Alexander 

> On Nov 22, 2019, at 8:46 AM, Alexander Bakst <abakst at galois.com> wrote:
> 
> Hi Loïc,
> 
> OK, thank you very much for the suggestions & pointers!
> 
> —Alexander
> 
>> On Nov 22, 2019, at 12:49 AM, Loïc Correnson <loic.correnson at cea.fr <mailto:loic.correnson at cea.fr>> wrote:
>> 
>> Hi Alexander,
>> 
>> Unfortunately, we won’t have time to fix this issue for Calcium. As a matter of fact, we did a lot of effort to simplify bitwise simplifications to handle programs with a lot of shifting/masking operations to access bit fields. This is why the current simplifications made by Qed are likely to transform shifting into masking, like in your example.
>> 
>> The workaround for now is to hide such comparisons by using `\min` and `\max` to avoid such automated transformations. You can also use the following trick:
>> //@ logic integer id(integer x) = x ;
>> and use `id( a >> b) <= M` instead of `(a >> b) <= M` in your logical specifications.
>> 
>> However, proving programs with bitwise operations are still difficult and generally require interactions with WP through the Frama-C/Gui.
>> 
>> You shall have a look at the TIP (WP user manual, section § 2.3) ; relevant tactics are :
>>  - bitwise ranges (by selecting formula e <= K, where terme e contains bitwise operations at head)
>>  - bitwise equalities (by selecting formula a == b, where a and b contains bitwise operations)
>>  - bitwise shifts (to transform logical shifts into multiplications and divisions)
>> 
>> You can also apply « strategies » which (recursively) tries to apply tactics to solve your goal, and you can select which kind of tactics to try.
>> Strategies can be applied like tactics from the TIP, or from the command line (WP user manual, sections § 2.3.5 and § 2.3.7) :
>> 
>> $ frama-c -wp -wp-session <dir> -wp-prover tip,alt-ergo -wp-strategies <strategies> *.c
>> 
>> This will save under your local session <dir> some scripts, that you later on replay with the same command line, or with (for only replay) :
>> 
>> $ frama-c -wp -wp-session <dir> -wp-prover script,alt-ergo *.c
>> 
>> Best regards,
>> 	L.
>> 
>>> Le 21 nov. 2019 à 18:29, Alexander Bakst <abakst at galois.com <mailto:abakst at galois.com>> a écrit :
>>> 
>>>> 
>>>> Thanks for your mail. It allowed us to spot an issue in the way Qed, the internal formula simplifier of WP, is handling inequalities between the result of a bitwise operation and a constant, resulting in an unprovable simplified formula.
>>> 
>>> Interesting! I’m currently using the preview of frama-c 20.0. Will a fix make its way into the final release? Also, once the issue is understood better, would it be possible to describe a workaround, if one exists? I arrived at this example from a more complicated program (hence some of the curious issues you identified below), so it would be helpful if I could generalize your advice to the full program. For example, to add a bit more complexity back i (note the change from `MAX` to `MASK`: `FOO` fails, and `BAR` succeeds. I believe the axiom MASK is needed to prove the contract of MASK.
>>> 
>>> Also interesting to note is that if I uncomment the second ensures clause in MASK, then neither FOO nor BAR are proven. If the issue is QED simplification of bitwise operations with constants, then this does strike me as probably related.
>>> 
>>> /*@ axiomatic Bits {
>>>   @   axiom MASK: \forall Xuint32 x, y; (x & y) <= y;
>>>   @ }
>>> */
>>> 
>>> /*@ ensures 0 <= \result <= y;
>>>   @ //ensures \result == (x & y);
>>>   @ assigns \nothing;
>>> */
>>> Xuint32 MASK(Xuint32 x, Xuint32 y)
>>> {
>>>     return (x & y);
>>> }
>>> 
>>> void foo(Xuint32 input) {
>>>     Xuint32 foo = input;
>>> 
>>>     if (MASK(foo >> 8, 0xFFFF) + MASK(foo, 0xFF) < 128) {
>>>         //@ assert FOO: (foo & 0xFF) < 128;
>>>     }
>>> }
>>> 
>>> void bar(Xuint32 input) {
>>>     Xuint32 foo = input;
>>> 
>>>     Xuint32 x1 = MASK(foo >> 8, 0xFFFF);
>>>     Xuint32 x2 = MASK(foo, 0xFF);
>>> 
>>>     if (x1 + x2 < 128) {
>>>         //@ assert BAR: x2 < 128;
>>>     }
>>> }
>>> 
>>> 
>>>> 
>>>> Note that in the particular case of your program, a slight reformulation of the contract for MAX (by the way, it might be better to call it MIN, as it returns the smaller argument. 
>>> 
>>> Haha, quite right :).
>>> 
>>>> Finally, please note that your contract for MAX is lacking an assigns \nothing; clause. It does not really matter here as there's no global variable or pointer MAX could be messing with to modify the program state, but when using WP it is a good practice to always put assigns clause to all contracts
>>>> 
>>> 
>>> Indeed, I’ve burned myself enough times to have learned that lesson :).
>>> 
>>> Thanks again!
>>> 
>>> —Alexander
>>> 
>>>> #include <stdint.h>
>>>> 
>>>> typedef uint32_t Xuint32;
>>>> 
>>>> /*@ ensures x < y ==> \result == x;
>>>>     ensures x >= y ==> \result == y;
>>>> */
>>>> Xuint32 MAX(Xuint32 x, Xuint32 y)
>>>> {
>>>>     if (x < y) {
>>>>         return x;
>>>>     }
>>>>     return y;
>>>> }
>>>> 
>>>> void bar(Xuint32 input) {
>>>>     Xuint32 foo = input;
>>>> 
>>>>     Xuint32 x1 = MAX(foo >> 8, 0xFFFF);
>>>>     Xuint32 x2 = MAX(foo, 0xFF);
>>>> 
>>>>     if (x1 + x2 < 128) {
>>>>         //@ assert BAR: x2 < 128;
>>>>     }
>>>> }
>>>> 
>>>>  Best regards,
>>>> -- 
>>>> E tutto per oggi, a la prossima volta
>>>> Virgile
>>>> _______________________________________________
>>>> Frama-c-discuss mailing list
>>>> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>>>> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
>>> _______________________________________________
>>> Frama-c-discuss mailing list
>>> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>>> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
>> _______________________________________________
>> Frama-c-discuss mailing list
>> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
>> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191127/0b744bd0/attachment-0001.html>