From 7a5a0eefc3cfbdf06a5fa5a42654f1922df31f70 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 31 Jan 2022 11:39:53 +0100
Subject: [PATCH] [WP] Review of the sequent decomposition
---
src/plugins/wp/Conditions.ml | 24 +++++++++++++++----
.../wp_acsl/oracle/base_offset.res.oracle | 3 ++-
.../tests/wp_acsl/oracle/bitwise.res.oracle | 7 +-----
.../wp_acsl/oracle_qualif/bitwise.res.oracle | 8 +++----
.../wp/tests/wp_bts/oracle/ex5.res.oracle | 2 +-
5 files changed, 28 insertions(+), 16 deletions(-)
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index f6bd2c4468f..fcf91379566 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -447,7 +447,10 @@ let rec exist_intro p =
let _,t = e_open ~pool ~exists:true
~forall:false ~lambda:false (e_prop p) in
exist_intro (F.p_bool t)
- | _ ->
+ | _ -> (* Note: Qed implement De Morgan rules
+ such that [p] cannot match the
+ decomposable representations:
+ Not Or, Not Imply, Not Forall *)
if Wp_parameters.Prenex.get ()
then prenex_intro p
else p
@@ -463,7 +466,11 @@ let rec exist_intros = function
let _,t = F.QED.e_open ~pool ~exists:true
~forall:false ~lambda:false (e_prop p) in
exist_intros ((F.p_bool t)::hs)
- | _ -> p::(exist_intros hs)
+ | _ -> (* Note: Qed implement De Morgan rules
+ such that [p] cannot match the
+ decomposable representations:
+ Not Or, Not Imply, Not Forall *)
+ p::(exist_intros hs)
end
(* -------------------------------------------------------------------------- *)
@@ -488,8 +495,17 @@ let rec forall_intro p =
(hp @ hs), (p::ps)) ([],[]) qs
in (* ORs qs <==> ORs (hps ==> ps)
<==> ((ANDs hps) ==> ORs ps) *)
- hps, (p_disj ps)
- | _ -> [] , p
+ let hps,ps = List.fold_left (fun (hs,ps) q ->
+ match F.repr (F.e_prop q) with
+ | Neq _ -> ((F.p_not q)::hs), ps
+ | _ -> hs, (q::ps)) (hps,[]) ps
+ in (* ORs qs <==> ((ANDs hps) ==> ORs ps)) *)
+ hps, (F.p_disj ps)
+ | _ -> (* Note: Qed implement De Morgan rules
+ such that [p] cannot match the
+ decomposable representations:
+ Not And, Not Exists *)
+ [] , p
(* -------------------------------------------------------------------------- *)
(* --- Constructors --- *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
index 951ae643d25..18e31ad1d27 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/base_offset.res.oracle
@@ -39,6 +39,7 @@ Prove: table_of_base(G_z_33) = table_of_base(G_x_31).
------------------------------------------------------------
Goal Check 'KO' (file base_offset.i, line 30):
-Prove: table_of_base(G_y_32) != table_of_base(G_x_31).
+Assume { (* Goal *) When: table_of_base(G_y_32) = table_of_base(G_x_31). }
+Prove: false.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
index 232b2653404..836623e5e0d 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/bitwise.res.oracle
@@ -153,12 +153,7 @@ Prove: (a = 0) /\ (b = 0).
------------------------------------------------------------
Goal Post-condition for 'true' (file bitwise.i, line 78) in 'bor_bool':
-Assume {
- Type: is_bool(a) /\ is_bool(b).
- (* Pre-condition for 'true' *)
- Have: (a = 1) \/ (b = 1).
-}
-Prove: (a != 0) \/ (b != 0).
+Prove: true.
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
index 413c2326caa..97ca9dc0b2e 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle
@@ -27,7 +27,7 @@
[wp] [Qed] Goal typed_lshift_shift2_ensures_lsl3 : Valid
[wp] [Qed] Goal typed_rshift_ensures : Valid
[wp] [Qed] Goal typed_rshift_shift1_ensures_lsr1 : Valid
-[wp] [Alt-Ergo] Goal typed_bor_bool_true_ensures : Valid
+[wp] [Qed] Goal typed_bor_bool_true_ensures : Valid
[wp] [Alt-Ergo] Goal typed_bor_bool_false_ensures : Valid
[wp] [Qed] Goal typed_band_bool_true_ensures : Valid
[wp] [Alt-Ergo] Goal typed_band_bool_false_ensures : Valid
@@ -42,8 +42,8 @@
[wp] [Qed] Goal typed_lemma_check_7 : Valid
[wp] [Qed] Goal typed_cast_uchar_ensures : Valid
[wp] Proved goals: 38 / 38
- Qed: 34
- Alt-Ergo: 4
+ Qed: 35
+ Alt-Ergo: 3
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
band 8 - 8 100%
@@ -52,7 +52,7 @@
bnot 1 - 1 100%
lshift 4 - 4 100%
rshift 2 - 2 100%
- bor_bool - 2 2 100%
+ bor_bool 1 1 2 100%
band_bool 1 1 2 100%
bxor_bool 1 1 2 100%
lemma 7 - 7 100%
diff --git a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
index 5e8dbbdb083..97a39bb3a67 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/ex5.res.oracle
@@ -174,7 +174,7 @@ Prove: (i + L_f(i)) != b.
------------------------------------------------------------
Goal Post-condition 'ko4' in 'forall':
-Prove: (L_f(i) != i_1) \/ P_P(i_1).
+Prove: P_P(L_f(i)).
------------------------------------------------------------
--
GitLab