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

Hello Alexander,

Le jeu. 21 nov. 2019 à 00:58, Alexander Bakst <abakst at galois.com> a écrit :

> Hi all,
>
> I’m having some trouble proving assertion BAR below. The culprit seems to
> be the shift right operation — if I replace foo >> 8 with foo, then BAR is
> proven. Any pointers for making progress with minimal changes?
>
>
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.

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. As hinted to by Tomas, if it were really
returning MAX, there would be no guarantee that the C operation x1+x2 stays
within the bounds of uint32_t, so that we couldn't conclude that x2<128
from the fact that x1+x2<128). If you use

/*@ ensures \result == x || \result == y;
       ensures \result <= x && \result <= y;
*/

Then somehow the problematic Qed rule isn't triggered and the resulting
goal can be discharged by Alt-Ergo without issue. The lemma below can be
proved as well, showing that both contracts are equivalent:

/*@ lemma max: \forall integer x,y,z;
  ((x < y ==> z == x) && (x>=y ==> z == y)) <==>
  (z == x || z == y) && z <= x && z<=y;
*/

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

#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
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20191121/623b204d/attachment.html>