[wp] New "Clear" tactic (hyp removal)

headers/header_spec.txt

@@ -1736,6 +1736,8 @@ src/plugins/wp/TacBittest.ml: CEA_WP
 src/plugins/wp/TacBittest.mli: CEA_WP
 src/plugins/wp/TacChoice.ml: CEA_WP
 src/plugins/wp/TacChoice.mli: CEA_WP
+src/plugins/wp/TacClear.ml: CEA_WP
+src/plugins/wp/TacClear.mli: CEA_WP
 src/plugins/wp/TacCongruence.ml: CEA_WP
 src/plugins/wp/TacCongruence.mli: CEA_WP
 src/plugins/wp/TacCompound.ml: CEA_WP

src/plugins/wp/Makefile.in

@@ -86,7 +86,7 @@ PLUGIN_CMO:= \
 	CfgCompiler StmtSemantics \
 	VCS script proof wpo wpReport \
 	Footprint Tactical Strategy \
-	TacSplit TacChoice TacRange TacInduction \
+	TacClear TacSplit TacChoice TacRange TacInduction \
 	TacArray TacCompound TacUnfold \
 	TacHavoc TacInstance TacLemma \
 	TacFilter TacCut WpTac TacNormalForm \

src/plugins/wp/TacClear.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2021                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Tactical
+
+class clear =
+  object(_)
+    inherit Tactical.make ~id:"Wp.clear"
+        ~title:"Clear"
+        ~descr:"Erase Hypothese"
+        ~params:[]
+
+    method select _feedback sel =
+      match sel with
+      | Clause(Step step) ->
+          let removed = [ "Cleared hypothesis", Conditions.Have Lang.F.p_true] in
+          Applicable (Tactical.replace ~at:step.id removed)
+      | _ ->
+          Not_applicable
+  end
+
+let tactical = Tactical.export (new clear)

src/plugins/wp/TacClear.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2021                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Built-in Range Tactical (auto-registered) *)
+
+open Tactical
+
+val tactical : tactical
+
+(**************************************************************************)

src/plugins/wp/tests/wp_tip/clear.i

+/* 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
+*/
+/* run.config_qualif
+   DONT_RUN:
+*/
+
+/*@ axiomatic X {
+      predicate P ;
+      predicate Q ;
+      predicate R ;
+      predicate S(integer i) ;
+    }
+*/
+
+int a = 42, b;
+
+/*@ requires P;
+  @ requires Q;
+  @ requires R;
+  @ ensures S(a+b); */
+void clear(void) {
+  if (a < b) {
+    a++;
+  } else {
+    b--;
+  }
+}

src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_tip/clear.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp:script:allgoals] 
+  Goal Post-condition (file tests/wp_tip/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] 
+  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_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_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_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 / 1
+[wp] No updated script.

src/plugins/wp/tests/wp_tip/oracle/clear.session/script/clear_ensures.json

+[ { "header": "Clear", "tactic": "Wp.clear", "params": {},
+    "select": { "select": "clause-step", "at": 9, "kind": "have",
+                "target": "(1+a_1)=a_0", "pattern": "=+$a1$a" },
+    "children": { "Cleared hypothesis": [ { "header": "Clear",
+                                            "tactic": "Wp.clear",
+                                            "params": {},
+                                            "select": { "select": "clause-step",
+                                                        "at": 4,
+                                                        "kind": "have",
+                                                        "target": "P_R",
+                                                        "pattern": "P_R" },
+                                            "children": { "Cleared hypothesis": 
+                                                            [ { "header": "Clear",
+                                                                "tactic": "Wp.clear",
+                                                                "params": {},
+                                                                "select": 
+                                                                  { "select": "clause-step",
+                                                                    "at": 9,
+                                                                    "kind": "have",
+                                                                    "target": "(a_2=a_0) /\\ (b_2=b_1)",
+                                                                    "pattern": "&==$a$a$b$b" },
+                                                                "children": 
+                                                                  { "Cleared hypothesis": 
+                                                                    [ { "header": "Clear",
+                                                                    "tactic": "Wp.clear",
+                                                                    "params": {},
+                                                                    "select": 
+                                                                    { "select": "clause-step",
+                                                                    "at": 5,
+                                                                    "kind": "branch",
+                                                                    "target": "a_2<b_2",
+                                                                    "pattern": "<$a$b" },
+                                                                    "children": 
+                                                                    { "Cleared hypothesis": 
+                                                                    [ { "header": "Clear",
+                                                                    "tactic": "Wp.clear",
+                                                                    "params": {},
+                                                                    "select": 
+                                                                    { "select": "clause-step",
+                                                                    "at": 3,
+                                                                    "kind": "have",
+                                                                    "target": "P_Q",
+                                                                    "pattern": "P_Q" },
+                                                                    "children": 
+                                                                    { "Cleared hypothesis": 
+                                                                    [ { "header": "Clear",
+                                                                    "tactic": "Wp.clear",
+                                                                    "params": {},
+                                                                    "select": 
+                                                                    { "select": "clause-step",
+                                                                    "at": 0,
+                                                                    "kind": "type",
+                                                                    "target": "(is_sint32 a_0) /\\ (is_sint32 b_0)",
+                                                                    "pattern": "&is_sint32is_sint32$a$b" },
+                                                                    "children": 
+                                                                    { "Cleared hypothesis": 
+                                                                    [ { "header": "Clear",
+                                                                    "tactic": "Wp.clear",
+                                                                    "params": {},
+                                                                    "select": 
+                                                                    { "select": "clause-step",
+                                                                    "at": 1,
+                                                                    "kind": "have",
+                                                                    "target": "P_P",
+                                                                    "pattern": "P_P" },
+                                                                    "children": 
+                                                                    { "Cleared hypothesis": [] } } ] } } ] } } ] } } ] } } ] } } ] } } ]