Commit 1e68b681 authored by Allan Blanchard's avatar Allan Blanchard

Merge branch 'feature/wp/repeat-tactic' into 'master'

[wp] new tactic for sequence repeat

See merge request frama-c/frama-c!2932
parents 7d242b80 1e527557
...@@ -1643,6 +1643,8 @@ src/plugins/wp/TacRange.ml: CEA_WP ...@@ -1643,6 +1643,8 @@ src/plugins/wp/TacRange.ml: CEA_WP
src/plugins/wp/TacRange.mli: CEA_WP src/plugins/wp/TacRange.mli: CEA_WP
src/plugins/wp/TacRewrite.ml: CEA_WP src/plugins/wp/TacRewrite.ml: CEA_WP
src/plugins/wp/TacRewrite.mli: 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.ml: CEA_WP
src/plugins/wp/TacShift.mli: CEA_WP src/plugins/wp/TacShift.mli: CEA_WP
src/plugins/wp/TacSplit.ml: CEA_WP src/plugins/wp/TacSplit.ml: CEA_WP
......
...@@ -90,6 +90,7 @@ PLUGIN_CMO:= \ ...@@ -90,6 +90,7 @@ PLUGIN_CMO:= \
TacHavoc TacInstance TacLemma \ TacHavoc TacInstance TacLemma \
TacFilter TacCut WpTac TacNormalForm \ TacFilter TacCut WpTac TacNormalForm \
TacRewrite TacBitwised TacBitrange TacBittest TacShift \ TacRewrite TacBitwised TacBitrange TacBittest TacShift \
TacSequence \
TacCongruence TacOverflow Auto \ TacCongruence TacOverflow Auto \
ProofSession ProofScript ProofEngine \ ProofSession ProofScript ProofEngine \
ProverTask ProverErgo ProverCoq \ ProverTask ProverErgo ProverCoq \
......
(**************************************************************************)
(* *)
(* 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)
(* -------------------------------------------------------------------------- *)
(**************************************************************************)
(* *)
(* 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
(**************************************************************************)
...@@ -372,6 +372,9 @@ let rewrite ?at patterns sequent = ...@@ -372,6 +372,9 @@ let rewrite ?at patterns sequent =
descr , Conditions.insert ?at step sequent descr , Conditions.insert ?at step sequent
) patterns ) patterns
let condition name guard process seq =
( name , (fst seq , guard) ) :: process seq
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(* --- Tactical Engines --- *) (* --- Tactical Engines --- *)
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
......
...@@ -184,6 +184,9 @@ val rewrite : ?at:int -> (string * pred * term * term) list -> process ...@@ -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] (** For each pattern [(descr,guard,src,tgt)] replace [src] with [tgt]
under condition [guard], inserted in position [at]. *) 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} *) (** {2 Tactical Plug-in} *)
class type tactical = class type tactical =
......
...@@ -532,6 +532,53 @@ This is a variant of the \texttt{Lemma} tactic dedicated to \texttt{Havoc} predi ...@@ -532,6 +532,53 @@ This is a variant of the \texttt{Lemma} tactic dedicated to \texttt{Havoc} predi
\paragraph{Separated} Expand Separation Cases\\ \paragraph{Separated} Expand Separation Cases\\
This tactic decompose a \texttt{separated}$(a,n,b,m)$ predicate into its four base cases: $a$ and $b$ have different bases, $a+n \leq b$, $b+m \leq a$, and $a[0..n-1]$ and $b[0..m-1]$ overlaps. The regions are separated in the first three cases, and not separated in the overlapping case. This is kind of normal disjunctive form of the separation clause. This tactic decompose a \texttt{separated}$(a,n,b,m)$ predicate into its four base cases: $a$ and $b$ have different bases, $a+n \leq b$, $b+m \leq a$, and $a[0..n-1]$ and $b[0..m-1]$ overlaps. The regions are separated in the first three cases, and not separated in the overlapping case. This is kind of normal disjunctive form of the separation clause.
\paragraph{Sequence} Unroll repeat-sequence operator\\
In this section, let us use $A^n$ for the ACSL notation \lstinline{A *^ n},
the repeat list operation, and $A \oplus l$ for the list concatenation.
This tactics is used to transform $A^n$ sequences. Threes behaviors
can be selected:
unroll left that rewrites the list $A^n$ into $A \oplus A^{n-1}$,
unroll right that rewrites the list $A^n$ into $A^{n-1} \oplus A$
and unroll sum that rewrites the list $A ^{n_1 + ... + n_k}$
into $A^{n_1} \oplus ... \oplus A^{n_k}$. For unroll left and right,
a negative value leads to an empty list. For unroll sum, one must prove that all
$nI$ are positive.
Rule for unroll left:
\[
\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{lll}
\Delta[A^n\leftarrow A \oplus A^{n-1}],& n > 0 & \models G[A^n\leftarrow A \oplus A^{n-1}]\\
\Delta[A^n\leftarrow []],& n \leq 0 & \models G[A^n\leftarrow []]
\end{array}
}\]
Rule for unroll right:
\[
\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{lll}
\Delta[A^n\leftarrow A^{n-1} \oplus A],& n > 0 & \models G[A^n\leftarrow A^{n-1} \oplus A]\\
\Delta[A^n\leftarrow []],& n \leq 0 & \models G[A^n\leftarrow []]
\end{array}
}\]
Rule for unroll sum:
\[
\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
\Delta & \models\bigwedge_{i=1}^{k} 0 \leq n_i\\
&\\
\Delta[A^{\sum_{i=1}^{k}n_i}\leftarrow \bigoplus_{i=1}^{k} A^{n_i}] &
\models G[A^{\sum_{i=1}^{k}n_i}\leftarrow \bigoplus_{i=1}^{k} A^{n_i}]
\end{array}
}\]
\subsection{Custom Tactics and Strategies} \subsection{Custom Tactics and Strategies}
\label{wp-custom-tactics} \label{wp-custom-tactics}
......
[ { "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" } ] } } ]
[ { "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" } ] } } ]
[ { "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" } ] } } ]
# 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%
------------------------------------------------------------
/* 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))) ;
*/
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment