[wp] new tactic for sequence repeat

headers/header_spec.txt

@@ -1641,6 +1641,8 @@ src/plugins/wp/TacRange.ml: CEA_WP
 src/plugins/wp/TacRange.mli: CEA_WP
 src/plugins/wp/TacRewrite.ml: CEA_WP
 src/plugins/wp/TacRewrite.mli: CEA_WP
+src/plugins/wp/TacSequence.ml: CEA_WP
+src/plugins/wp/TacSequence.mli: CEA_WP
 src/plugins/wp/TacShift.ml: CEA_WP
 src/plugins/wp/TacShift.mli: CEA_WP
 src/plugins/wp/TacSplit.ml: CEA_WP

src/plugins/wp/Makefile.in

@@ -90,6 +90,7 @@ PLUGIN_CMO:= \
 	TacHavoc TacInstance TacLemma \
 	TacFilter TacCut WpTac TacNormalForm \
 	TacRewrite TacBitwised TacBitrange TacBittest TacShift \
+	TacSequence \
 	TacCongruence TacOverflow Auto \
 	ProofSession ProofScript ProofEngine \
 	ProverTask ProverErgo ProverCoq \

src/plugins/wp/TacSequence.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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
+
+let negative n = F.p_leq n F.e_zero
+let positive n = F.p_leq F.e_zero n
+let concat ~result es = F.e_fun ~result Vlist.f_concat es
+let repeat ~result a n = F.e_fun ~result Vlist.f_repeat [a;n]
+let sum n = match F.repr n with
+  | Add ns -> ns
+  | _ -> [n]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Induction Tactical                                                 --- *)
+(* -------------------------------------------------------------------------- *)
+
+let vmode,pmode =
+  Tactical.selector ~id:"seq.side" ~title:"Mode" ~descr:"Unrolling mode"
+    ~options:[
+      { vid = "left" ; title = "Unroll left" ;
+        descr = "Transform (A^n) into (A.A^n-1)" ; value = `Left } ;
+      { vid = "right" ; title = "Unroll right" ;
+        descr = "Transform (A^n) into (A^n-1.A)" ; value = `Right } ;
+      { vid = "sum" ; title = "Concat sum" ;
+        descr = "Transform A^(p+q) into (A^p.A^q)" ; value = `Sum }
+    ] ()
+
+class sequence =
+  object(self)
+    inherit Tactical.make
+        ~id:"Wp.sequence"
+        ~title:"Sequence"
+        ~descr:"Unroll repeat-sequence operator"
+        ~params:[pmode]
+
+    method select _feedback (s : Tactical.selection) =
+      let value = Tactical.selected s in
+      match F.repr value with
+      | Fun(f,[a;n]) when f == Vlist.f_repeat ->
+          let result = F.typeof value in
+          let at = Tactical.at s in
+          Applicable
+            begin
+              match self#get_field vmode with
+              | `Sum ->
+                  let ns = sum n in
+                  let pos = F.p_all positive ns in
+                  let cat = concat ~result (List.map (repeat ~result a) ns) in
+                  Tactical.condition "Positive" pos @@
+                  Tactical.rewrite ?at [ "Unroll" , pos , value , cat ]
+              | `Left ->
+                  let p = F.e_add n F.e_minus_one in
+                  let unroll = concat ~result [a ; repeat ~result a p] in
+                  Tactical.rewrite ?at [
+                    "Nil", negative n , value , concat ~result [] ;
+                    "Unroll", positive p , value , unroll ;
+                  ]
+              | `Right ->
+                  let p = F.e_add n F.e_minus_one in
+                  let unroll = concat ~result [repeat ~result a p ; a] in
+                  Tactical.rewrite ?at [
+                    "Nil", negative n , value , concat ~result [] ;
+                    "Unroll", positive p , value , unroll ;
+                  ]
+            end
+      | _ -> Not_applicable
+
+  end
+
+let tactical = Tactical.export (new sequence)
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/TacSequence.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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 Sequence Tactical (auto-registered) *)
+
+open Tactical
+
+val tactical : tactical
+
+(**************************************************************************)

src/plugins/wp/Tactical.ml

@@ -372,6 +372,9 @@ let rewrite ?at patterns sequent =
        descr , Conditions.insert ?at step sequent
     ) patterns
 
+let condition name guard process seq =
+  ( name , (fst seq , guard) ) :: process seq
+
 (* -------------------------------------------------------------------------- *)
 (* --- Tactical Engines                                                   --- *)
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/Tactical.mli

@@ -184,6 +184,9 @@ val rewrite : ?at:int -> (string * pred * term * term) list -> process
 (** For each pattern [(descr,guard,src,tgt)] replace [src] with [tgt]
     under condition [guard], inserted in position [at]. *)
 
+val condition : string -> pred -> process -> process
+(** Apply process, but only after proving some condition *)
+
 (** {2 Tactical Plug-in} *)
 
 class type tactical =

src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json

+[ { "prover": "script", "verdict": "valid" },
+  { "header": "Sequence", "tactic": "Wp.sequence",
+    "params": { "seq.side": "left" },
+    "select": { "select": "inside-goal", "occur": 0,
+                "target": "(repeat a_0 n_0)", "pattern": "repeat$a$n" },
+    "children": { "Nil": [ { "prover": "qed", "verdict": "valid" } ],
+                  "Unroll": [ { "prover": "qed", "verdict": "valid" } ] } } ]

src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json

+[ { "prover": "script", "verdict": "valid" },
+  { "header": "Sequence", "tactic": "Wp.sequence",
+    "params": { "seq.side": "right" },
+    "select": { "select": "inside-goal", "occur": 0,
+                "target": "(repeat a_0 n_0)", "pattern": "repeat$a$n" },
+    "children": { "Nil": [ { "prover": "qed", "verdict": "valid" } ],
+                  "Unroll": [ { "prover": "qed", "verdict": "valid" } ] } } ]

src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json

+[ { "prover": "script", "verdict": "valid" },
+  { "header": "Sequence", "tactic": "Wp.sequence",
+    "params": { "seq.side": "sum" },
+    "select": { "select": "inside-goal", "occur": 0,
+                "target": "(repeat a_0 (p_0+q_0))",
+                "pattern": "repeat$a+$p$q" },
+    "children": { "Positive": [ { "prover": "qed", "verdict": "valid" } ],
+                  "Unroll": [ { "prover": "qed", "verdict": "valid" } ] } } ]

src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_tip/unroll.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 3 goals scheduled
+[wp] [Script] Goal typed_lemma_LEFT : Valid
+[wp] [Script] Goal typed_lemma_RIGHT : Valid
+[wp] [Script] Goal typed_lemma_SUM : Valid
+[wp] Proved goals:    3 / 3
+  Qed:             0 
+  Script:          3
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Lemma                     -        -        3       100%
+------------------------------------------------------------

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

+/* run.config
+   DONTRUN:
+*/
+
+/* run.config_qualif
+   OPT: -wp-prover script,none
+ */
+
+/*@
+  lemma SUM:
+    \forall \list<integer> a;
+    \forall integer p,q;
+    0 <= p ==> 0 <= q ==>
+    (a *^ (p+q)) == ((a *^ p) ^ (a *^ q)) ;
+*/
+
+/*@
+  lemma RIGHT:
+    \forall \list<integer> a;
+    \forall integer n;
+    0 < n ==>
+    (a *^ n) == ((a *^ (n-1)) ^ a) ;
+*/
+
+/*@
+  lemma LEFT:
+    \forall \list<integer> a;
+    \forall integer n;
+    0 < n ==>
+    (a *^ n) == (a ^ (a *^ (n-1))) ;
+*/