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

> 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>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191121/ba64be65/attachment-0001.html>