From d838ad2e827c98312aefdbc76b45af4fec8608a7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 16 Oct 2020 17:41:42 +0200
Subject: [PATCH] [wp] induction tactic
---
headers/header_spec.txt | 2 +
src/plugins/wp/Conditions.mli | 2 +-
src/plugins/wp/Makefile.in | 2 +-
src/plugins/wp/TacInduction.ml | 115 ++++++++++++++++++
src/plugins/wp/TacInduction.mli | 29 +++++
src/plugins/wp/tests/wp_tip/induction.i | 28 +++++
.../oracle_qualif/induction.0.res.oracle | 12 ++
.../script/lemma_ByInd.json | 14 +++
.../oracle_qualif/induction.1.res.oracle | 10 ++
.../script/lemma_ByInd.json | 11 ++
.../oracle_qualif/induction.2.res.oracle | 10 ++
.../script/lemma_ByInd.json | 11 ++
.../wp_tip/oracle_qualif/induction.res.oracle | 10 ++
.../script/lemma_ByInd.json | 13 ++
14 files changed, 267 insertions(+), 2 deletions(-)
create mode 100644 src/plugins/wp/TacInduction.ml
create mode 100644 src/plugins/wp/TacInduction.mli
create mode 100644 src/plugins/wp/tests/wp_tip/induction.i
create mode 100644 src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
create mode 100644 src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
create mode 100644 src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
create mode 100644 src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json
create mode 100644 src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
create mode 100644 src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json
create mode 100644 src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle
create mode 100644 src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index c77fc0d433b..a86fbfb6d25 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1629,6 +1629,8 @@ src/plugins/wp/TacFilter.ml: CEA_WP
src/plugins/wp/TacFilter.mli: CEA_WP
src/plugins/wp/TacHavoc.ml: CEA_WP
src/plugins/wp/TacHavoc.mli: CEA_WP
+src/plugins/wp/TacInduction.ml: CEA_WP
+src/plugins/wp/TacInduction.mli: CEA_WP
src/plugins/wp/TacInstance.ml: CEA_WP
src/plugins/wp/TacInstance.mli: CEA_WP
src/plugins/wp/TacLemma.ml: CEA_WP
diff --git a/src/plugins/wp/Conditions.mli b/src/plugins/wp/Conditions.mli
index 878a73afc76..3e6aa0e00a2 100644
--- a/src/plugins/wp/Conditions.mli
+++ b/src/plugins/wp/Conditions.mli
@@ -142,7 +142,7 @@ val map_sequence : (pred -> pred) -> sequence -> sequence
(** Rewrite all root predicates in sequence *)
val map_sequent : (pred -> pred) -> sequent -> sequent
-(** Rewrite all root predocates in hypotheses and goal *)
+(** Rewrite all root predicates in hypotheses and goal *)
val insert : ?at:int -> step -> sequent -> sequent
(** Insert a step in the sequent immediately [at] the specified position.
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 5264a1b2cfd..2d81efcad32 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -85,7 +85,7 @@ PLUGIN_CMO:= \
CfgCompiler StmtSemantics \
VCS script proof wpo wpReport \
Footprint Tactical Strategy \
- TacSplit TacChoice TacRange \
+ TacSplit TacChoice TacRange TacInduction \
TacArray TacCompound TacUnfold \
TacHavoc TacInstance TacLemma \
TacFilter TacCut WpTac TacNormalForm \
diff --git a/src/plugins/wp/TacInduction.ml b/src/plugins/wp/TacInduction.ml
new file mode 100644
index 00000000000..7a5a4185418
--- /dev/null
+++ b/src/plugins/wp/TacInduction.ml
@@ -0,0 +1,115 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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 Lang
+
+type env = {
+ n : F.var ;
+ sigma : F.sigma ;
+ mutable hind : F.pred list ;
+}
+
+let rec strip env p =
+ match F.p_expr p with
+ | And ps -> F.p_all (strip env) ps
+ | _ ->
+ let p = F.p_subst env.sigma p in
+ if F.occursp env.n p then
+ ( env.hind <- p :: env.hind ; F.p_true )
+ else p
+
+let process value n0 ~inf ~sup seq =
+
+ (* Transfrom seq into: hyps => (forall n, goal) *)
+ let n = Lang.freshvar ~basename:"n" Qed.Logic.Int in
+ let i = Lang.freshvar ~basename:"i" Qed.Logic.Int in
+ let vn = F.e_var n in
+ let vi = F.e_var i in
+ let v0 = F.e_int n0 in
+ let sigma = Lang.sigma () in
+ F.Subst.add sigma value vn ;
+ let env = { n ; sigma ; hind = [] } in
+ let hyps = Conditions.map_sequence (strip env) (fst seq) in
+ let goal_n = F.p_hyps env.hind @@ F.p_subst sigma (snd seq) in
+ let goal_i = F.p_subst_var n vi goal_n in
+
+ (* Base: n = n0 *)
+ let goal_base = F.p_imply (F.p_equal vn v0) goal_n in
+
+ (* Hind: n0 <= i < n *)
+ let goal_sup =
+ if sup
+ then
+ let hsup = [ F.p_leq v0 vi ; F.p_lt vi vn ] in
+ let hind = F.p_forall [i] (F.p_hyps hsup goal_i) in
+ F.p_hyps [F.p_lt v0 vn; hind] goal_n
+ else F.p_leq value v0 in
+
+ (* Hind: n < i <= n0 *)
+ let goal_inf =
+ if inf
+ then
+ let hinf = [ F.p_lt vn vi ; F.p_leq vi v0 ] in
+ let hind = F.p_forall [i] (F.p_hyps hinf goal_i) in
+ F.p_hyps [F.p_lt vn v0; hind] goal_n
+ else F.p_leq v0 value in
+
+ (* All Cases *)
+ List.map (fun (name,goal) -> name , (hyps,goal)) [
+ "Base" , goal_base ;
+ "Induction (sup)" , goal_sup ;
+ "Induction (inf)" , goal_inf ;
+ ]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Induction Tactical --- *)
+(* -------------------------------------------------------------------------- *)
+
+let vbase,pbase = Tactical.spinner ~id:"base"
+ ~title:"Base" ~descr:"Value of base case" ()
+let vsup,psup = Tactical.checkbox ~id:"hsup"
+ ~title:"Sup" ~descr:"Induction over base <= n" ~default:true ()
+let vinf,pinf = Tactical.checkbox ~id:"hinf"
+ ~title:"Inf" ~descr:"Induction over n <= base" ~default:true ()
+
+class induction =
+ object(self)
+ inherit Tactical.make
+ ~id:"Wp.induction"
+ ~title:"Induction"
+ ~descr:"Proof by integer induction"
+ ~params:[pbase;psup;pinf]
+
+ method select _feedback (s : Tactical.selection) =
+ let value = Tactical.selected s in
+ if F.is_int value then
+ let base = self#get_field vbase in
+ let inf = self#get_field vinf in
+ let sup = self#get_field vsup in
+ Applicable(process value base ~inf ~sup)
+ else Not_applicable
+
+ end
+
+let tactical = Tactical.export (new induction)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/TacInduction.mli b/src/plugins/wp/TacInduction.mli
new file mode 100644
index 00000000000..21c817a0b33
--- /dev/null
+++ b/src/plugins/wp/TacInduction.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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
+
+(**************************************************************************)
diff --git a/src/plugins/wp/tests/wp_tip/induction.i b/src/plugins/wp/tests/wp_tip/induction.i
new file mode 100644
index 00000000000..5ff948c0f86
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/induction.i
@@ -0,0 +1,28 @@
+/* run.config
+ DONTRUN:
+*/
+
+/* run.config_qualif
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1
+ OPT: -wp-prover script,alt-ergo -wp-timeout 1
+*/
+
+// Script 0: induction on f(x) => success
+// Script 1: induction on x => unsuccess
+// Script 2: induction on y => unsuccess
+
+/*@
+ axiomatic Inductive {
+
+ logic integer f(integer x);
+ predicate P(integer x, integer y);
+
+ axiom Hbse: \forall integer y; P(0,y);
+ axiom Hsup: \forall integer i,y; 0 <= i ==> P(i,y) ==> P(i+1,y);
+ axiom Hinf: \forall integer i,y; i <= 0 ==> P(i,y) ==> P(i-1,y);
+
+ lemma ByInd: \forall integer x,y; P(f(x),y);
+
+ }
+*/
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
new file mode 100644
index 00000000000..6a84303d1b4
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
@@ -0,0 +1,12 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_ByInd : Valid
+[wp] Proved goals: 1 / 1
+ Qed: 0
+ Script: 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Axiomatic Inductive - - 1 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
new file mode 100644
index 00000000000..c70ff7e2d9c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
@@ -0,0 +1,14 @@
+[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
+ { "prover": "script", "verdict": "valid" },
+ { "header": "Induction", "tactic": "Wp.induction",
+ "params": { "base": 0, "hsup": true, "hinf": true },
+ "select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
+ "pattern": "L_f$x" },
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0", "verdict": "valid",
+ "time": 0.0075, "steps": 6 } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0113,
+ "steps": 21 } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.009,
+ "steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
new file mode 100644
index 00000000000..68fc7293ba5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
@@ -0,0 +1,10 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_ByInd : Unsuccess
+[wp] Proved goals: 0 / 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Axiomatic Inductive - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json
new file mode 100644
index 00000000000..5a250b7fa27
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json
@@ -0,0 +1,11 @@
+[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
+ { "header": "Induction", "tactic": "Wp.induction",
+ "params": { "base": 0, "hsup": true, "hinf": true },
+ "select": { "select": "inside-goal", "occur": 0, "target": "x_0",
+ "pattern": "$x" },
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "unknown" } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "unknown" } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "timeout", "time": 1. } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
new file mode 100644
index 00000000000..68fc7293ba5
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
@@ -0,0 +1,10 @@
+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_ByInd : Unsuccess
+[wp] Proved goals: 0 / 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Axiomatic Inductive - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json
new file mode 100644
index 00000000000..c3224ca1dac
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json
@@ -0,0 +1,11 @@
+[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
+ { "header": "Induction", "tactic": "Wp.induction",
+ "params": { "base": 0, "hsup": true, "hinf": true },
+ "select": { "select": "inside-goal", "occur": 0, "target": "y_0",
+ "pattern": "$y" },
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "unknown" } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "unknown" } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "timeout", "time": 1. } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle
new file mode 100644
index 00000000000..1524fcd67af
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle
@@ -0,0 +1,10 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_Simple : Unsuccess
+[wp] Proved goals: 0 / 1
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Axiomatic Inductive - - 1 0.0%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json
new file mode 100644
index 00000000000..5a434573223
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json
@@ -0,0 +1,13 @@
+[ { "prover": "script", "verdict": "valid", "time": 0.0549, "steps": 117 },
+ { "header": "Induction", "tactic": "Wp.induction",
+ "params": { "base": 0, "hsup": true, "hinf": true },
+ "select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
+ "pattern": "L_f$x" },
+ "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0", "verdict": "valid",
+ "time": 0.0083, "steps": 6 } ],
+ "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0549,
+ "steps": 117 } ],
+ "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+ "verdict": "valid", "time": 0.0274,
+ "steps": 86 } ] } } ]
--
GitLab