[WP] adds trivial simplifications for LNOT

src/plugins/wp/Cint.ml

@@ -590,6 +590,15 @@ let smp_shift zf = (* f(e1,0)~>e1, c2>0==>f(c1,c2)~>zf(c1,c2), c2>0==>f(0,c2)~>0
     end
   | _ -> raise Not_found
 
+let smp_lnot = function
+  | ([e] as args) -> begin match F.repr e with
+      | Logic.Fun( f , [e] ) when Fun.equal f f_lnot ->
+          (* ~~e ~> e *)
+          e
+      | _ -> smp1 Integer.lognot args
+    end
+  | _ -> raise Not_found
+
 (* -------------------------------------------------------------------------- *)
 (* --- Comparision with L-AND / L-OR / L-NOT                              --- *)
 (* -------------------------------------------------------------------------- *)
@@ -647,11 +656,15 @@ let smp_eq_with_lxor a b = (* b1==(a2^e) <==> (b1^a2)==e *)
           | e1::((_::_) as e22) -> e_eq e1 (e_fun f_lnot [e_fun f_lxor e22])
           | _ -> raise Not_found)
 
-let smp_eq_with_lnot a b = (* b1==~e <==> ~b1==e *)
-  let b1 = match_integer b in
+let smp_eq_with_lnot a b =
   let e = match_ufun f_lnot a in
-  let k1 = Integer.lognot b1 in
-  e_eq (e_zint k1) e
+  try (* b1==~e <==> ~b1==e *)
+    let b1 = match_integer b in
+    let k1 = Integer.lognot b1 in
+    e_eq (e_zint k1) e
+  with Not_found ->(* ~b==~e <==> b==e *)
+    let b = match_ufun f_lnot b in
+    e_eq e b
 
 (* -------------------------------------------------------------------------- *)
 (* --- Comparision with LSL / LSR                                         --- *)
@@ -807,8 +820,7 @@ let () =
            no creation of [e_fun f_bit_stdlib args] *)
         let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
         let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
-        let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot
-            (smp1 Integer.lognot) in
+        let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot smp_lnot in
         let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
             (smp2 f_lxor Integer.logxor) in
         let bi_lor  = mk_builtin "f_lor" f_lor  ~eq:smp_eq_with_lor

src/plugins/wp/tests/wp_acsl/bitwise.i

@@ -48,7 +48,7 @@ int bor(int a,int b, int c) { return a | b | c ; }
   @   ensures \result == 0;
   @ behavior bit3:
   @   assumes a == ~b;
-  @   ensures zbit: \result == -1;
+  @   ensures \result == -1;
  */ 
 int bxor(int a,int b) { return a ^ b ; }
 
@@ -100,3 +100,14 @@ _Bool band_bool(_Bool a, _Bool b) { return (_Bool)(((int)a & (int)b) != 0); }
   @   ensures \result == 0;
  */
 _Bool bxor_bool(_Bool a, _Bool b) { return (_Bool)(((int)a ^ (int)b) != 0); }
+
+void lemma(unsigned a, unsigned b) {
+  //@ check zbit: a1: ~(a + ~a)  == 0;
+  //@ check zbit: a2: ~(a | ~a)  == 0;
+  //@ check zbit: a3:  (a & ~a)  == 0;
+  //@ check           ~(a ^ ~a)  == 0;
+  //@ check            (a ^  a)  == 0;
+  //@ check           (~a --> a) == a;
+  //@ check           (a --> ~a) == ~a;
+  //@ check           (~a == ~b) ==> (a == b);
+}

src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle

@@ -189,10 +189,8 @@ Prove: true.
   Function bxor with behavior bit3
 ------------------------------------------------------------
 
-Goal Post-condition for 'bit3' 'zbit' in 'bxor':
-Let x = lnot(b).
-Assume { Type: is_sint32(b) /\ is_sint32(x) /\ is_sint32(lxor(b, x)). }
-Prove: lnot(x) = b.
+Goal Post-condition for 'bit3' (file tests/wp_acsl/bitwise.i, line 51) in 'bxor':
+Prove: true.
 
 ------------------------------------------------------------
 ------------------------------------------------------------
@@ -220,6 +218,52 @@ Assume {
 }
 Prove: b != a.
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function lemma
+------------------------------------------------------------
+
+Goal Check 'zbit,a1' (file tests/wp_acsl/bitwise.i, line 105):
+Assume { Type: is_uint32(a). }
+Prove: (a + lnot(a)) = (-1).
+
+------------------------------------------------------------
+
+Goal Check 'zbit,a2' (file tests/wp_acsl/bitwise.i, line 106):
+Assume { Type: is_uint32(a). }
+Prove: lor(a, lnot(a)) = (-1).
+
+------------------------------------------------------------
+
+Goal Check 'zbit,a3' (file tests/wp_acsl/bitwise.i, line 107):
+Assume { Type: is_uint32(a). }
+Prove: land(a, lnot(a)) = 0.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/bitwise.i, line 108):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/bitwise.i, line 109):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/bitwise.i, line 110):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/bitwise.i, line 111):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_acsl/bitwise.i, line 112):
+Prove: true.
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function lshift

src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle

@@ -2,7 +2,7 @@
 [kernel] Parsing tests/wp_acsl/bitwise.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 29 goals scheduled
+[wp] 35 goals scheduled
 [wp] [Qed] Goal typed_band_ensures : Valid
 [wp] [Qed] Goal typed_band_ensures_band0 : Valid
 [wp] [Qed] Goal typed_band_bit0_ensures_band1 : Valid
@@ -19,6 +19,7 @@
 [wp] [Qed] Goal typed_bxor_ensures : Valid
 [wp] [Qed] Goal typed_bxor_bit1_ensures : Valid
 [wp] [Qed] Goal typed_bxor_bit2_ensures : Valid
+[wp] [Qed] Goal typed_bxor_bit3_ensures : Valid
 [wp] [Qed] Goal typed_bnot_ensures : Valid
 [wp] [Qed] Goal typed_lshift_ensures : Valid
 [wp] [Qed] Goal typed_lshift_shift1_ensures_lsl1 : Valid
@@ -32,18 +33,24 @@
 [wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Valid
 [wp] [Qed] Goal typed_bxor_bool_true_ensures : Valid
 [wp] [Alt-Ergo] Goal typed_bxor_bool_false_ensures : Valid
-[wp] Proved goals:   29 / 29
-  Qed:            25 
+[wp] [Qed] Goal typed_lemma_check : Valid
+[wp] [Qed] Goal typed_lemma_check_2 : Valid
+[wp] [Qed] Goal typed_lemma_check_3 : Valid
+[wp] [Qed] Goal typed_lemma_check_4 : Valid
+[wp] [Qed] Goal typed_lemma_check_5 : Valid
+[wp] Proved goals:   35 / 35
+  Qed:            31 
   Alt-Ergo:        4
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   band                      8        -        8       100%
   bor                       5        -        5       100%
-  bxor                      3        -        3       100%
+  bxor                      4        -        4       100%
   bnot                      1        -        1       100%
   lshift                    4        -        4       100%
   rshift                    2        -        2       100%
   bor_bool                  -        2        2       100%
   band_bool                 1        1        2       100%
   bxor_bool                 1        1        2       100%
+  lemma                     5        -        5       100%
 ------------------------------------------------------------