From e32b12227c8674588f28f18b97bdc8d3e2f54700 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 24 Jan 2022 15:02:46 +0100
Subject: [PATCH] [wp] TacClear in conjunctions
---
src/plugins/wp/TacClear.ml | 35 ++++-
src/plugins/wp/tests/wp_tip/clear.i | 7 +-
.../wp/tests/wp_tip/oracle/clear.res.oracle | 146 +++++++++++++++++-
.../script/clear_in_step_check.json | 20 +++
4 files changed, 202 insertions(+), 6 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_in_step_check.json
diff --git a/src/plugins/wp/TacClear.ml b/src/plugins/wp/TacClear.ml
index 62492909112..a16fa3aa2f7 100644
--- a/src/plugins/wp/TacClear.ml
+++ b/src/plugins/wp/TacClear.ml
@@ -21,6 +21,7 @@
(**************************************************************************)
open Tactical
+open Conditions
class clear =
object(_)
@@ -34,8 +35,38 @@ class clear =
| Clause(Step step) ->
let removed = [ "Cleared hypothesis", Conditions.Have Lang.F.p_true] in
Applicable (Tactical.replace ~at:step.id removed)
- | _ ->
- Not_applicable
+ | Inside(Step step, remove) ->
+ let cond p = (* keep original kind of step *)
+ match step.condition with
+ | Type _ -> Type p
+ | Have _ -> Have p
+ | When _ -> When p
+ | Core _ -> Core p
+ | Init _ -> Init p
+ | _ -> assert false (* see above pattern matching *)
+ in
+ let rec collect p =
+ match Lang.F.p_expr p with
+ | And ps -> collect_list ps
+ | _ -> [ p ]
+ and collect_list = function
+ | [] -> []
+ | p :: l -> List.rev_append (List.rev @@ collect p) (collect_list l)
+ in
+ begin match step.condition with
+ | Type p | Have p | When p | Core p | Init p ->
+ let ps = Lang.F.e_props @@ collect p in
+ if List.mem remove ps then
+ let ps = List.filter (fun x -> x <> remove) ps in
+ let cond = cond @@ Lang.F.p_bool @@ Lang.F.e_and ps in
+ let filtered = [ "Filtered", cond ] in
+ Applicable (Tactical.replace ~at:step.id filtered)
+ else
+ Not_applicable
+
+ | _ -> Not_applicable
+ end
+ | _ -> Not_applicable
end
let tactical = Tactical.export (new clear)
diff --git a/src/plugins/wp/tests/wp_tip/clear.i b/src/plugins/wp/tests/wp_tip/clear.i
index 6abddf24da8..38bb4997fe9 100644
--- a/src/plugins/wp/tests/wp_tip/clear.i
+++ b/src/plugins/wp/tests/wp_tip/clear.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_DIR@/oracle/@PTEST_NAME@.session
+ OPT: -wp-par 1 -wp-no-print -wp-prover qed,tip -wp-msg-key script -wp-session @PTEST_SUITE_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.session
*/
/* run.config_qualif
DONTRUN:
@@ -26,3 +26,8 @@ void clear(void) {
b--;
}
}
+
+void clear_in_step(void){
+ //@ admit P && Q && R ;
+ //@ check S(42) ;
+}
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
index 72226ceb96e..85363bf27b5 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -2,7 +2,147 @@
[kernel] Parsing clear.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] 1 goal scheduled
-[wp] [Failed] Goal typed_clear_ensures
-[wp] Proved goals: 0 / 1
+[wp] 2 goals scheduled
+[wp:script:allgoals]
+ Goal Post-condition (file clear.i, line 21) in 'clear':
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+ is_sint32(b_1) /\ is_sint32(b_2).
+ (* Pre-condition *)
+ Have: P_P.
+ (* Pre-condition *)
+ Have: P_Q.
+ (* Pre-condition *)
+ Have: P_R.
+ If a_2 < b_2
+ Then { Have: (a_2 = a_1) /\ (b_2 = b). Have: (1 + a_1) = a. }
+ Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+ }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ Goal Check (file clear.i, line 32):
+ Assume { (* Admit *) Have: P_P /\ P_Q /\ P_R. }
+ Prove: P_S(42).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-0 (generated):
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+ is_sint32(b_1) /\ is_sint32(b_2).
+ (* Pre-condition *)
+ Have: P_P.
+ (* Pre-condition *)
+ Have: P_Q.
+ (* Pre-condition *)
+ Have: P_R.
+ If a_2 < b_2
+ Then { Have: (a_2 = a_1) /\ (b_2 = b). }
+ Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+ }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_in_step_check subgoal:
+
+ Goal Wp.Tactical.typed_clear_in_step_check-0 (generated):
+ Assume { (* Filtered *) Have: P_Q /\ P_R. }
+ Prove: P_S(42).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-1 (generated):
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+ is_sint32(b_1) /\ is_sint32(b_2).
+ (* Pre-condition *)
+ Have: P_P.
+ (* Pre-condition *)
+ Have: P_Q.
+ If a_2 < b_2
+ Then { Have: (a_2 = a_1) /\ (b_2 = b). }
+ Else { Have: (a_2 = a) /\ (b_2 = b_1). Have: (1 + b) = b_1. }
+ }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_in_step_check subgoal:
+
+ Goal Wp.Tactical.typed_clear_in_step_check-1 (generated):
+ Assume { (* Filtered *) Have: P_R. }
+ Prove: P_S(42).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-2 (generated):
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(a_1) /\ is_sint32(a_2) /\ is_sint32(b) /\
+ is_sint32(b_1).
+ (* Pre-condition *)
+ Have: P_P.
+ (* Pre-condition *)
+ Have: P_Q.
+ If a_2 < b_1
+ Then { Have: (a_2 = a_1) /\ (b_1 = b). }
+ }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_in_step_check subgoal:
+
+ Goal Wp.Tactical.typed_clear_in_step_check-2 (generated):
+ Prove: P_S(42).
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_clear_in_step_check : Unsuccess
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-3 (generated):
+ Assume {
+ Type: is_sint32(a) /\ is_sint32(b).
+ (* Pre-condition *)
+ Have: P_P.
+ (* Pre-condition *)
+ Have: P_Q.
+ }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-4 (generated):
+ Assume { Type: is_sint32(a) /\ is_sint32(b). (* Pre-condition *) Have: P_P. }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-5 (generated):
+ Assume { (* Pre-condition *) Have: P_P. }
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp:script:allgoals]
+ typed_clear_ensures subgoal:
+
+ Goal Wp.Tactical.typed_clear_ensures-6 (generated):
+ Prove: P_S(a + b).
+
+ ------------------------------------------------------------
+[wp] [Script] Goal typed_clear_ensures : Unsuccess
+[wp] Proved goals: 0 / 2
[wp] No updated script.
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_in_step_check.json b/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_in_step_check.json
new file mode 100644
index 00000000000..231674bdd87
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_in_step_check.json
@@ -0,0 +1,20 @@
+[ { "header": "Clear", "tactic": "Wp.clear", "params": {},
+ "select": { "select": "inside-step", "at": 2, "kind": "have", "occur": 0,
+ "target": "P_P", "pattern": "P_P" },
+ "children": { "Filtered": [ { "header": "Clear", "tactic": "Wp.clear",
+ "params": {},
+ "select": { "select": "inside-step",
+ "at": 2, "kind": "have",
+ "occur": 0, "target": "P_Q",
+ "pattern": "P_Q" },
+ "children": { "Filtered": [ { "header": "Clear",
+ "tactic": "Wp.clear",
+ "params": {},
+ "select":
+ { "select": "clause-step",
+ "at": 2,
+ "kind": "have",
+ "target": "P_R",
+ "pattern": "P_R" },
+ "children":
+ { "Cleared hypothesis": [] } } ] } } ] } } ]
--
GitLab