diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index cb2bad4c9639644f6e0f265e2afef45495f9b172..16c04fc09ca8b761c684cc157dcf6a14bea1870b 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -613,13 +613,24 @@ let smp_lnot = function
(* --- Comparision with L-AND / L-OR / L-NOT --- *)
(* -------------------------------------------------------------------------- *)
-let smp_leq_with_land a b =
- let es = match_fun f_land a in
- let a1,_ = match_list_head match_positive_or_null_integer es in
- if F.decide (F.e_leq (e_zint a1) b)
+let smp_leq_improved f a b =
+ ignore (match_fun f b) ; (* It must be an improved of [is_positive_or_null f(args)] *)
+ (* a <= 0 && 0 <= f(args) *)
+ if F.decide (F.e_leq a F.e_zero) && is_positive_or_null b
then e_true
else raise Not_found
+let smp_leq_with_land a b =
+ try
+ let es = match_fun f_land a in
+ let a1,_ = match_list_head match_positive_or_null_integer es in
+ if F.decide (F.e_leq (e_zint a1) b)
+ then e_true
+ else raise Not_found
+ with Not_found ->
+ (* a <= 0 && 0 <= (x&y) ==> a <= (x & y) *)
+ smp_leq_improved f_land a b
+
let smp_eq_with_land a b =
let es = match_fun f_land a in
try
@@ -777,7 +788,11 @@ let smp_eq_with_lsl a b =
try smp_eq_with_lsl_cst a b
with Not_found -> smp_cmp_with_lsl e_eq a b
-let smp_leq_with_lsl a0 b0 = smp_cmp_with_lsl e_leq a0 b0
+let smp_leq_with_lsl a b =
+ try smp_cmp_with_lsl e_leq a b
+ with Not_found ->
+ (* a <= 0 && 0 <= (x << y) ==> a <= (x << y) *)
+ smp_leq_improved f_lsl a b
let smp_eq_with_lsr a0 b0 =
try
@@ -820,6 +835,7 @@ let smp_leq_with_lsr x y =
let k = two_power_k p in
e_leq x (e_div a (e_zint k))
with Not_found ->
+ try
let a,p = match_fun f_lsr x |> match_positive_or_null_integer_arg2 in
(* (a >> p) <= y with p >= 0 *)
if y == e_zero then
@@ -829,6 +845,10 @@ let smp_leq_with_lsr x y =
(* p >= 0 ==> ( (a >> p) <= y <==> a/(2**p) <= y ) *)
let k = two_power_k p in
e_leq (e_div a (e_zint k)) y
+ with Not_found ->
+ (* x <= y && 0 <= (a&b) ==> x <= (a >> b) *)
+ smp_leq_improved f_lsr x y
+
(* Rewritting at export *)
let bitk_export k e = F.e_fun ~result:Logic.Bool f_bit_export [e;k]
@@ -858,10 +878,10 @@ 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 smp_lnot in
- let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
+ let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot smp_lnot ~leq:(smp_leq_improved f_lnot) in
+ let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor ~leq:(smp_leq_improved f_lxor)
(smp2 f_lxor Integer.logxor) in
- let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor
+ let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor ~leq:(smp_leq_improved f_lor)
(smp2 f_lor Integer.logor) in
let bi_land = mk_builtin "f_land" f_land ~eq:smp_eq_with_land ~leq:smp_leq_with_land
smp_land in
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
index 6c74a498337a8547eb0dacd1cf85f2c6177e638a..18231f2787cfacbce7f1fd426b27d0a7d6beaf6e 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle
@@ -10,8 +10,7 @@ Goal Preservation of Invariant 'RANGE' (file issue_751.i, line 7):
Let x = land(3840, R).
Let x_1 = x / 256.
Assume {
- Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(1 + j) /\
- is_sint32(lsr(x, 8)).
+ Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(1 + j).
(* Pre-condition *)
Have: (0 < x) /\ (x <= 2303).
(* Invariant 'RANGE' *)
@@ -36,18 +35,17 @@ Prove: true.
Goal Loop assigns (file issue_751.i, line 8) (2/2):
Effect at line 11
Let x = land(3840, R).
-Let x_1 = lsr(x, 8).
-Let x_2 = j - 1.
+Let x_1 = j - 1.
Assume {
- Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(x_2) /\ is_sint32(x_1).
+ Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(x_1).
(* Heap *)
Type: (region(Data_0.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: !invalid(Malloc_0, shift_sint32(Data_0, x_2), 1).
+ When: !invalid(Malloc_0, shift_sint32(Data_0, x_1), 1).
(* Pre-condition *)
Have: (0 < x) /\ (x <= 2303).
(* Invariant 'RANGE' *)
- Have: (0 < j) /\ (j <= (1 + x_1)).
+ Have: (0 < j) /\ (j <= (1 + lsr(x, 8))).
(* Then *)
Have: j <= (x / 256).
}
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
index 69f63c6e1c94ed8159119284c2bcf135b224b07b..c3ac6213cb42eb711a1f83d9ab1b354d146f655b 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle
@@ -3,10 +3,10 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 40 goals scheduled
-[wp] [Alt-Ergo] Goal typed_acquire_loop_invariant_RANGE_preserved : Valid
+[wp] [Alt-Ergo] Goal typed_acquire_loop_invariant_RANGE_preserved : Valid (Qed:3ms) (17ms) (39) (missing cache)
[wp] [Qed] Goal typed_acquire_loop_invariant_RANGE_established : Valid
[wp] [Qed] Goal typed_acquire_loop_assigns_part1 : Valid
-[wp] [Alt-Ergo] Goal typed_acquire_loop_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_acquire_loop_assigns_part2 : Valid (Qed:5ms) (18ms) (52) (missing cache)
[wp] [Qed] Goal typed_issue_751_check : Valid
[wp] [Qed] Goal typed_issue_751_check_2 : Valid
[wp] [Qed] Goal typed_issue_751_check_3 : Valid
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
index 558b45d9fdf74924a1face948576f5abfc6fa618..7454740a0f188b3058081228b4a2837ba6beeb9f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_bitwise.res.oracle
@@ -147,8 +147,7 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'ok' (file unit_bitwise.c, line 117):
-Let x = land(1, a). Assume { Type: is_uint8(a) /\ is_uint8(x). }
-Prove: 0 <= x.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -161,8 +160,7 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'ok' (file unit_bitwise.c, line 52):
-Let x = land(1, a). Assume { Type: is_uint32(a) /\ is_uint32(x). }
-Prove: 0 <= x.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -175,8 +173,7 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'ok' (file unit_bitwise.c, line 170):
-Let x = land(1, a). Assume { Type: is_uint64(a) /\ is_uint64(x). }
-Prove: 0 <= x.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
@@ -189,8 +186,7 @@ Prove: true.
------------------------------------------------------------
Goal Assertion 'ok' (file unit_bitwise.c, line 165):
-Let x = land(1, a). Assume { Type: is_uint16(a) /\ is_uint16(x). }
-Prove: 0 <= x.
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
index 5c838689f12914c9e16edb03cb53b10e8ec0312c..8c72c29788e6c5de7430921640c4ca0c5b4297fd 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_bitwise.0.res.oracle
@@ -29,7 +29,7 @@
[wp] [Qed] Goal typed_lshift_int_ensures_ok : Valid
[wp] [Qed] Goal typed_rshift_int_ensures_ok : Valid
[wp] [Qed] Goal typed_band1_uint_assert_ok : Valid
-[wp] [Alt-Ergo] Goal typed_band1_uint_assert_ok_2 : Valid
+[wp] [Qed] Goal typed_band1_uint_assert_ok_2 : Valid
[wp] [Qed] Goal typed_band_uint_ensures_ok : Valid
[wp] [Qed] Goal typed_bor_uint_ensures_ok : Valid
[wp] [Qed] Goal typed_bxor_uint_ensures_ok : Valid
@@ -44,7 +44,7 @@
[wp] [Qed] Goal typed_lshift_char_ensures_ok : Valid
[wp] [Qed] Goal typed_rshift_char_ensures_ok : Valid
[wp] [Qed] Goal typed_band1_uchar_assert_ok : Valid
-[wp] [Alt-Ergo] Goal typed_band1_uchar_assert_ok_2 : Valid
+[wp] [Qed] Goal typed_band1_uchar_assert_ok_2 : Valid
[wp] [Alt-Ergo] Goal typed_band_uchar_ensures_ok : Valid
[wp] [Qed] Goal typed_bor_uchar_ensures_ok : Valid
[wp] [Qed] Goal typed_bxor_uchar_ensures_ok : Valid
@@ -53,9 +53,9 @@
[wp] [Qed] Goal typed_lshift_uchar_ensures_ok : Valid
[wp] [Alt-Ergo] Goal typed_rshift_uchar_ensures_ok : Valid
[wp] [Qed] Goal typed_band1_ushort_assert_ok : Valid
-[wp] [Alt-Ergo] Goal typed_band1_ushort_assert_ok_2 : Valid
+[wp] [Qed] Goal typed_band1_ushort_assert_ok_2 : Valid
[wp] [Qed] Goal typed_band1_ulong_assert_ok : Valid
-[wp] [Alt-Ergo] Goal typed_band1_ulong_assert_ok_2 : Valid
+[wp] [Qed] Goal typed_band1_ulong_assert_ok_2 : Valid
[wp] [Qed] Goal typed_cast_ensures_ok : Valid
[wp] [Qed] Goal typed_cast_assert_ok : Valid
[wp] [Qed] Goal typed_cast_assert_ok_2 : Valid
@@ -65,8 +65,8 @@
[wp] [Qed] Goal typed_cast_assert_ok_6 : Valid
[wp] [Qed] Goal typed_cast_assert_ok_7 : Valid
[wp] Proved goals: 61 / 61
- Qed: 41
- Alt-Ergo: 20
+ Qed: 45
+ Alt-Ergo: 16
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Lemma 10 8 18 100%
@@ -78,7 +78,7 @@
bnot_int 1 - 1 100%
lshift_int 1 - 1 100%
rshift_int 1 - 1 100%
- band1_uint 1 1 2 100%
+ band1_uint 2 - 2 100%
band_uint 1 - 1 100%
bor_uint 1 - 1 100%
bxor_uint 1 1 2 100%
@@ -91,14 +91,14 @@
bnot_char - 1 1 100%
lshift_char 1 - 1 100%
rshift_char 1 - 1 100%
- band1_uchar 1 1 2 100%
+ band1_uchar 2 - 2 100%
band_uchar - 1 1 100%
bor_uchar 1 - 1 100%
bxor_uchar 1 1 2 100%
bnot_uchar 1 - 1 100%
lshift_uchar 1 - 1 100%
rshift_uchar - 1 1 100%
- band1_ushort 1 1 2 100%
- band1_ulong 1 1 2 100%
+ band1_ushort 2 - 2 100%
+ band1_ulong 2 - 2 100%
cast 8 - 8 100%
------------------------------------------------------------