[Wp] improve Cint simplifier

src/plugins/wp/Cint.ml

@@ -1445,49 +1445,26 @@ let mask_simplifier =
       r
 
   end in
-  let unary_op e f rewrite a =
+  let unary_op e f rewrite a = (* requires [e==f a] *)
     (* reuse the previous term when not rewritten *)
     let a' = rewrite a in if a'==a then e else f a'
   in
-  let bin_op e f rewrite a b =
+  let bin_op e f rewrite a b = (* requires [e==f a b] *)
     (* reuse the previous term when there is no rewriting *)
     let a' = rewrite a and b' = rewrite b in
     if a'==a && b'==b then e else f a' b'
   in
-  let nary_op e es f rewrite xs =
+  let nary_op e es f rewrite xs = (* requires [e==f es] and [xs=map g es] *)
     (* reuse the previous term when there is no rewriting *)
     let modified = ref false in
     let xs = List.map2 (fun e x ->
         let x = rewrite x in
-        if x==e then modified := true;
+        if not (x==e) then modified := true;
         x) es xs
     in if !modified then f xs else e
   in
-  let rec rewrite ctx e = (* [r = rewrite ctx e] such that [ctx |- e = r] *)
+  let rewrite_cst ctx e = (* [r = rewrite ctx e] such that [ctx |- e = r] *)
     match F.repr e with
-    | Fun(f,xs) when f == f_land ->
-        let es = List.map (rewrite ctx) xs in
-        Wp_parameters.debug ~dkey "Rewrite AND %a@." Lang.F.pp_term e;
-        let reduce unset x = match F.repr x with
-          | Kint v -> F.e_zint (Integer.logand (Integer.lognot unset) v)
-          | _ -> x
-        and collect ctx unset_mask x = try
-            let open Masks in
-            let m = eval ctx x in
-            Integer.logor unset_mask m.unset
-          with Not_found -> unset_mask
-        in
-        let unset_mask = List.fold_left (collect ctx) Integer.zero es in
-        if Integer.is_zero unset_mask then e
-        else if Integer.equal unset_mask Integer.minus_one then e_zero
-        else nary_op e xs (F.e_fun f_land) (reduce unset_mask) es
-    | Fun(f,xs) when f == f_lor ->
-        nary_op e xs (F.e_fun f_lor) (rewrite ctx) xs
-    | Fun(f,[a]) when f == f_lnot ->
-        unary_op e (fun x -> F.e_fun f_lnot [x]) (rewrite ctx) a
-    | Not a -> unary_op e e_not (rewrite ctx) a
-    | Eq (a, b) -> bin_op e e_eq (rewrite ctx) a b
-    | Leq (a, b) -> bin_op e e_leq (rewrite ctx) a b
     | Kint _ -> e
     | _ when is_int e ->
         let open Masks in
@@ -1496,6 +1473,34 @@ let mask_simplifier =
           F.e_zint v.set
         else e
     | _ -> e
+  in
+  let rec rewrite ctx e = (* [r = rewrite ctx e] such that [ctx |- e = r] *)
+    let e =
+      match F.repr e with
+      | Fun(f,xs) when f == f_land ->
+          let es = List.map (rewrite ctx) xs in
+          Wp_parameters.debug ~dkey "Rewrite AND %a@." Lang.F.pp_term e;
+          let reduce unset x = match F.repr x with
+            | Kint v -> F.e_zint (Integer.logand (Integer.lognot unset) v)
+            | _ -> x
+          and collect ctx unset_mask x = try
+              let open Masks in
+              let m = eval ctx x in
+              Integer.logor unset_mask m.unset
+            with Not_found -> unset_mask
+          in
+          let unset_mask = List.fold_left (collect ctx) Integer.zero es in
+          if Integer.is_zero unset_mask then e
+          else if Integer.equal unset_mask Integer.minus_one then e_zero
+          else nary_op e xs (F.e_fun f_land) (reduce unset_mask) es
+      | Fun(f,xs) -> (try
+                        nary_op e xs (F.e_fun ~result:(F.typeof e) f) (rewrite ctx) xs
+                      with _ -> e)
+      | Not a -> unary_op e e_not (rewrite ctx) a
+      | Eq (a, b) -> bin_op e e_eq (rewrite ctx) a b
+      | Leq (a, b) -> bin_op e e_leq (rewrite ctx) a b
+      | _ -> e
+    in rewrite_cst ctx e
 
   in
   object
@@ -1517,23 +1522,23 @@ let mask_simplifier =
     method equivalent_exp e =
       if Tmap.is_empty masks then e else
         (Wp_parameters.debug ~dkey "Rewrite Exp: %a@." Lang.F.pp_term e;
-         Lang.e_subst (rewrite masks) e)
+         rewrite masks e)
 
     method weaker_hyp p =
       if Tmap.is_empty masks then p else
         (Wp_parameters.debug ~dkey "Rewrite Hyp: %a@." Lang.F.pp_pred p;
-         Lang.p_subst (rewrite masks) p)
+         F.p_bool (rewrite masks (F.e_prop p)))
 
     method equivalent_branch p =
       if Tmap.is_empty masks then p else
         (Wp_parameters.debug ~dkey "Rewrite Branch: %a@." Lang.F.pp_pred p;
-         Lang.p_subst (rewrite masks) p
+         F.p_bool (rewrite masks (F.e_prop p))
         )
 
     method stronger_goal p =
       if Tmap.is_empty masks then p else
         (Wp_parameters.debug ~dkey "Rewrite Goal: %a@." Lang.F.pp_pred p;
-         Lang.p_subst (rewrite masks) p)
+         F.p_bool (rewrite masks (F.e_prop p)))
 
   end
 

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

@@ -125,11 +125,18 @@ void lemma(unsigned a, unsigned b, unsigned k) {
 
 }
 
+//@ axiomatic Def { predicate P(integer x); }
+
+
 //@ ensures \result == (x & 0xFF) ;
 unsigned char cast_uchar(int x) {
   unsigned char c = x;
-  //@ check bit_test: ok: (c & (1 << 1)) == 0  ==> (c & 5) == (c & 7);
+  //@ check bit_test: ok:  (c & (1 << 1)) == 0  ==> (c & 5) == (c & 7);
+  //@ check bit_test1: ok: (c & (1 << 1)) == 0  ==> (P(c & 5) <==> P(c & 7));
   //@ check bit_unset: ok: (c & 0x77) == 0x66 ==> (x & 1) == 0 ;
-  //@ check bit_set_unset: ok: (c & 0x77) == 0x66 && (x & 5) == (x & 7) ==> (x & 4) == (x & 6) ;
+  //@ check bit_set_unset: ok:  (c & 0x77) == 0x66 && (x & 5) == (x & 7) ==> (x & 4) == (x & 6) ;
+  //@ check bit_set_unset2: ok: (c & 0x77) == 0x66 && (x & 5) == (x & 7) ==> (P(x & 4) <==> P(x & 6)) ;
+  //@ check bit_defined: ok:  (c & 0x77) == 0x66 && (x & ~0x77) == (~0x77 & 0xFFF0) ==> (P(c)<==>P(0xE6));
+  //@ check bit_defined2: ok: (c & 0x77) == 0x66 && (x & ~0x77) == (~0x77 & 0xFFF0) ==> (P(x)<==>P(0xFFE6));
   return c;
 }

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

@@ -217,22 +217,42 @@ Prove: b != a.
   Function cast_uchar
 ------------------------------------------------------------
 
-Goal Post-condition (file bitwise.i, line 128) in 'cast_uchar':
+Goal Post-condition (file bitwise.i, line 131) in 'cast_uchar':
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_test,ok' (file bitwise.i, line 131):
+Goal Check 'bit_test,ok' (file bitwise.i, line 134):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_unset,ok' (file bitwise.i, line 132):
+Goal Check 'bit_test1,ok' (file bitwise.i, line 135):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'bit_set_unset,ok' (file bitwise.i, line 133):
+Goal Check 'bit_unset,ok' (file bitwise.i, line 136):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'bit_set_unset,ok' (file bitwise.i, line 137):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'bit_set_unset2,ok' (file bitwise.i, line 138):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'bit_defined,ok' (file bitwise.i, line 139):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'bit_defined2,ok' (file bitwise.i, line 140):
 Prove: true.
 
 ------------------------------------------------------------

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

@@ -2,7 +2,7 @@
 [kernel] Parsing bitwise.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 41 goals scheduled
+[wp] 45 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
@@ -42,10 +42,14 @@
 [wp] [Qed] Goal typed_lemma_check_7 : Valid
 [wp] [Qed] Goal typed_cast_uchar_ensures : Valid
 [wp] [Qed] Goal typed_cast_uchar_check_bit_test_ok : Valid
+[wp] [Qed] Goal typed_cast_uchar_check_bit_test1_ok : Valid
 [wp] [Qed] Goal typed_cast_uchar_check_bit_unset_ok : Valid
 [wp] [Qed] Goal typed_cast_uchar_check_bit_set_unset_ok : Valid
-[wp] Proved goals:   41 / 41
-  Qed:            38 
+[wp] [Qed] Goal typed_cast_uchar_check_bit_set_unset2_ok : Valid
+[wp] [Qed] Goal typed_cast_uchar_check_bit_defined_ok : Valid
+[wp] [Qed] Goal typed_cast_uchar_check_bit_defined2_ok : Valid
+[wp] Proved goals:   45 / 45
+  Qed:            42 
   Alt-Ergo:        3
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
@@ -59,5 +63,5 @@
   band_bool                 1        1        2       100%
   bxor_bool                 1        1        2       100%
   lemma                     7        -        7       100%
-  cast_uchar                4        -        4       100%
+  cast_uchar                8        -        8       100%
 ------------------------------------------------------------