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] math vs. bits

Hi,

CEA have done some works in WP to deals with ACSL bitwise operator:
- internal simplification during WP calculus,
- axiomatic for Alt-Ergo (to be extracted soon from a why3 axiomatic and 
proofs with Coq of the lemmas given to the external provers).

There is a "good" specification of your rotate example for WP and also 
for the developer for my point of view:

#define BIT_TEST(x,n) (((x)&(1<<(n)))!=0)
/*@ ensures bit_zero: BIT_TEST(\result,0) <==> BIT_TEST(x,31);
   @ ensures other_bits: \forall integer k ; 0 <= k && k < 31 ==> ( 
BIT_TEST(\result,1+k) <==> BIT_TEST(x,k) );
  */
unsigned rotate_left (unsigned x) {
   return (x << 1) | (x >> 31);
}

Once you guess what means this BIT_TEST macro inside an ACSL annotation, 
this specification become easy to understand:
the bitwise operators (here: &, <<) apply to any mathematical integer  
(infinite 2-complement binary representation) (see page 22 of ASCL manual).
The macro BIT_TEST(x,n) allow to specify the n-th bit (n=0 for the first 
bit) of x (and nothing is specified for negative value of n).

Unfortunately, only parts of this work is inside Fluorine.
With the development version, these two properties are proved, the first 
one by the internal simplifier Qed, the second one needs an external 
prover as Alt-Ergo:
 > frama-c -pp-annot rotate.c -wp
[kernel] preprocessing with "gcc -C -E -I.  -dD rotate.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[wp] warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Qed] Goal typed_rotate_left_post_bit_zero : Valid (10ms)
[wp] [Alt-Ergo] Goal typed_rotate_left_post_other_bits : Valid (2.6s) (1193)
[wp] Proved goals:    2 / 2
      Qed:             1  (10ms-10ms)
      Alt-Ergo:        1  (2.6s-2.6s) (1193)

-- Patrick

Le 12/11/2013 01:17, Claude Marche a ?crit :
> Hi,
>
> The main reason is that the support of bitwise operators in Jessie in
> very shallow, if any.
>
> I'm surprised that the first function could be proved.
>
> To succeed in proving such kind of code with Jessie, you should probably
> provide properties on bitwise operators, under the form of lemmas.
>
> I'm not sure Jessie is the right tool for that, The Value plugin or the
> WP plugin might do better.
>
> - Claude
>