Commit 57f17599 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] more robust script session

Share scripts among models.
More robust against script errors.
parent c635c818
......@@ -20,12 +20,17 @@
# <Prover>: prover
###############################################################################
- WP [2020/02/10] Specify cache mode with FRAMAC_WP_CACHE=<mode> (-wp-cache-env)
- WP [2020/02/10] Update scripts with FRAMAC_WP_SCRIPT=update and -wp-prover script
- WP [2020/02/10] Move frame conditions to Type section for better filtering
- WP [2020/02/10] Extended frame conditions to pointers inside compound
- WP [2020/02/10] Extended frame conditions with global C-types
- WP [2019/17/04] Control splitting with -wp-max-split <n>
- WP [2019/12/04] Added option -wp-run-all-provers
- WP [2019/01/29] Emit a warning when no goal is generated
- TIP [2018/04/03] Create session directory only on demand
- TIP [2018/03/19] Specification of JSON script format
- TIP [2018/03/18] Refactor structure of session directory (remove models)
##########################
Plugin WP 20.0 (Calcium)
......
......@@ -493,18 +493,12 @@ class pane (gprovers : GuiConfig.provers) =
self#update_tactics None ;
| Proof proof ->
let wpo = ProofEngine.head proof in
if Wpo.is_proved wpo then
begin
self#update_provers None ;
self#update_tactics None ;
end
else
begin
self#update_provers (Some wpo) ;
let sequent = printer#sequent in
let select = printer#selection in
self#update_tactics (Some(proof,sequent,select)) ;
end
begin
self#update_provers (Some wpo) ;
let sequent = printer#sequent in
let select = printer#selection in
self#update_tactics (Some(proof,sequent,select)) ;
end
| Composer _ | Browser _ -> ()
method private update_proofview =
......@@ -626,9 +620,12 @@ class pane (gprovers : GuiConfig.provers) =
Wutil.later
begin fun () ->
let title = tactic#title in
let tactic = ProofScript.jtactic ~title tactic selection in
let anchor = ProofEngine.anchor proof () in
self#fork proof (ProofEngine.fork proof ~anchor tactic process)
try
let tactic = ProofScript.jtactic ~title tactic selection in
let anchor = ProofEngine.anchor proof () in
self#fork proof (ProofEngine.fork proof ~anchor tactic process)
with Exit | Not_found | Invalid_argument _ ->
text#printf "Application of tactic '%s' failed." title
end
method private search proof = function
......
......@@ -181,10 +181,10 @@ class printer (text : Wtext.text) =
| `Proof ->
text#printf "@{<it>Existing Script (navigate to explore)@}@."
| `Script ->
text#printf "[%a]@." ProofSession.pp_goal wpo ;
text#printf "[%a]@." ProofSession.pp_script_for wpo ;
text#printf "@{<it>Existing Script (replay to explore)@}@."
| `Saved ->
text#printf "[%a]@." ProofSession.pp_goal wpo ;
text#printf "[%a]@." ProofSession.pp_script_for wpo ;
text#printf "@{<it>Saved Script (replay to load)@}@."
| `None ->
text#printf "@{<it>No Script@}@."
......
......@@ -365,7 +365,7 @@ class tactic
initializer
begin
form#add_row ~xpadding:4 ~ypadding:2 ~field:`Compact descr#coerce ;
self#set_action ~tooltip:"Apply Tactic" ~icon:`MEDIA_PLAY () ;
self#set_action () ;
wfields <- List.map (wfield tac form pp) tac#params ;
List.iter (fun fd -> fd#connect self#updated) wfields ;
List.iter (fun fd -> fd#compose_with self#compose) wfields ;
......
......@@ -462,7 +462,7 @@ class console ~pool ~title =
= fun msg ->
Pretty_utils.ksfprintf
(fun s -> errors <- true ;
Wp_parameters.error "[%s] %s" title s)
Wp_parameters.warning "[%s] %s" title s)
msg
end
......
......@@ -22,59 +22,63 @@
open Wpo
type status =
type script =
| NoScript
| Script of string
| Deprecated of string
let files : (string,status) Hashtbl.t = Hashtbl.create 32
let files : (string,script) Hashtbl.t = Hashtbl.create 32
let jsonfile = Printf.sprintf "%s/%s.json"
let filename ~force wpo =
let d = Wp_parameters.get_session_dir ~force "script" in
Printf.sprintf "%s/%s.json" d wpo.po_gid
let dscript = Wp_parameters.get_session_dir ~force "script" in
jsonfile dscript wpo.po_sid (* no model in name *)
let legacies wpo =
let m = WpContext.MODEL.id wpo.po_model in
let d = Wp_parameters.get_session_dir ~force:false m in
List.map (Printf.sprintf "%s/%s.json" d) [
wpo.po_gid ;
wpo.po_leg ;
let mid = WpContext.MODEL.id wpo.po_model in
let dscript = Wp_parameters.get_session_dir ~force:false "script" in
let dmodel = Wp_parameters.get_session_dir ~force:false mid in
[
jsonfile dscript wpo.po_gid ;
jsonfile dmodel wpo.po_gid ;
jsonfile dmodel wpo.po_leg ;
]
let status wpo =
let get wpo =
let f = filename ~force:false wpo in
try Hashtbl.find files f
with Not_found ->
let status =
let script =
if Sys.file_exists f then Script f else
try
let f' = List.find Sys.file_exists (legacies wpo) in
Wp_parameters.warning ~current:false
"Deprecated script for '%s' (use prover tip to upgrade)" wpo.po_sid ;
"Deprecated script for '%s'" wpo.po_sid ;
Deprecated f'
with Not_found -> NoScript
in Hashtbl.add files f status ; status
in Hashtbl.add files f script ; script
let pp_file fmt s = Filepath.Normalized.(pretty fmt (of_string s))
let pp_status fmt = function
let pp_script fmt = function
| NoScript -> Format.pp_print_string fmt "no script file"
| Script f -> Format.fprintf fmt "script '%a'" pp_file f
| Deprecated f -> Format.fprintf fmt "script '%a' (deprecated)" pp_file f
let pp_goal fmt wpo = pp_status fmt (status wpo)
let pp_script_for fmt wpo = pp_script fmt (get wpo)
let exists wpo =
match status wpo with NoScript -> false | Script _ | Deprecated _ -> true
match get wpo with NoScript -> false | Script _ | Deprecated _ -> true
let load wpo =
match status wpo with
match get wpo with
| NoScript -> `Null
| Script f | Deprecated f ->
if Sys.file_exists f then Json.load_file f else `Null
let remove wpo =
match status wpo with
match get wpo with
| NoScript -> ()
| Script f ->
begin
......@@ -86,7 +90,8 @@ let remove wpo =
Wp_parameters.feedback
"Removed deprecated script for '%s'" wpo.po_sid ;
Extlib.safe_remove f0 ;
Hashtbl.replace files (filename ~force:true wpo) NoScript ;
let f = filename ~force:false wpo in
Hashtbl.replace files f NoScript ;
end
let save wpo js =
......@@ -95,8 +100,9 @@ let save wpo js =
| `Null | `List [] | `Assoc [] -> true
| _ -> false in
if empty then remove wpo else
match status wpo with
| Script f -> Json.save_file f js
match get wpo with
| Script f ->
Json.save_file f js
| NoScript ->
begin
let f = filename ~force:true wpo in
......
......@@ -20,16 +20,15 @@
(* *)
(**************************************************************************)
type status =
type script =
| NoScript
| Script of string
| Deprecated of string
val pp_status : Format.formatter -> status -> unit
val pp_goal : Format.formatter -> Wpo.t -> unit
val status : Wpo.t -> status
val pp_script : Format.formatter -> script -> unit
val pp_script_for : Format.formatter -> Wpo.t -> unit
val get : Wpo.t -> script
val exists : Wpo.t -> bool
val save : Wpo.t -> Json.t -> unit
val load : Wpo.t -> Json.t
......
......@@ -90,7 +90,7 @@ let jfork tree ?node jtactic =
| Some (script,process) ->
Some (ProofEngine.fork tree ~anchor script process)
with
| Not_found ->
| Exit | Not_found | Invalid_argument _ ->
console#set_error "Can not configure tactic" ; None
| e ->
console#set_error "Exception <%s>" (Printexc.to_string e) ;
......@@ -323,7 +323,8 @@ let rec crawl env on_child node = function
Task.return ()
| Error(msg,json) :: alternative ->
Wp_parameters.error "@[<hov 2>Script Error %S: %a@]@." msg Json.pp json ;
Wp_parameters.warning "@[<hov 2>Script Error %S: %a@]@."
msg Json.pp json ;
crawl env on_child node alternative
| Prover( prv , res ) :: alternative ->
......
......@@ -50,7 +50,7 @@ let fork tree anchor strategy =
| Some (script,process) ->
Some (ProofEngine.fork tree ~anchor script process)
with
| Not_found ->
| Exit | Not_found | Invalid_argument _ ->
console#set_error "Can not configure strategy" ; None
| e ->
console#set_error "Exception <%s>" (Printexc.to_string e) ;
......
......@@ -164,3 +164,193 @@ conditional is:
This form actually factorizes the common postcondition to $A$ and $B$,
which makes the \emph{weakest precondition} calculus linear in the
number of program statements.
\section{Structure of JSON Scripts}
The proof scripts generated by using the Interactive Proof Editor (Section~\ref{wp-proof-editor})
are saved in the \textsf{Frama-C/WP} session as \textsf{JSON} files. This section defines
the format of session scripts precisely.
\textsf{JSON} scripts files are located in the \texttt{<session>/wp/scripts} sub-directory
of the \textsf{Frama-C} session directory (set with command line option \texttt{-session})
or in the \texttt{<wpsession>/scripts} sub-directory of the \textsf{Frama-C/WP} session
directory (set with command line option \texttt{-wp-session}).
The proof scripts for goal named \texttt{<goal>} is stored in a single file \texttt{<goal>.json} ; the
format of the \texttt{<goal>} name is identical to the one used by the \textsf{Frama-C/Report} plug-in
for its \textsf{JSON} output.
The content of each script file is an array ofs alternatives, each alternative being a record with
two possible structures, that might represent a \textit{prover} attempt or the application of a
\textit{tactic}:
\begin{align*}
\mathit{wp.script} &::= \mathtt{[} \mathit{wp.alternative} , \ldots \mathtt{]} \\
\mathit{wp.alternative} &::= \mathit{wp.prover} \;|\; \mathit{wp.tactic}
\end{align*}
\paragraph{Prover Attempts} The proof script records previous attempts to discharge a proof obligation
with external provers (also called decision procedures).
Each attempt is represented by a \textsf{JSON} record with the following fields:
\begin{align*}
\mathit{wp.prover} &::=
\left\{
\begin{array}{rl}
\mathtt{"prover"} :& \mathit{string}, \\
\mathtt{"verdict"} :& \mathit{wp.verdict}, \\
\mathtt{"time"} :& \mathit{number}? \\
\mathtt{"steps"} :& \mathit{number}? \\
\mathtt{"depth"} :& \mathit{number}? \\
\end{array}
\right\} \\
\mathit{wp.verdict} &::=
\begin{array}[t]{l}
\mathtt{"none"} ~|~
\mathtt{"valid"} ~|~
\mathtt{"unknown"} ~|~ \\
\mathtt{"timeout"} ~|~
\mathtt{"stepout"} ~|~
\mathtt{"invalid"} ~|~
\mathtt{"failed"}
\end{array}
\end{align*}
Remark that, since the proof scripts do not record the proof obligation that was exercised, there is no
guarantee that replying the script on a (potentially new) proof obligation would issue the same result.
Hence, prover attempts \emph{must} not be used as a cache, but can serve as a hint for choosing among
several alternatives.
\paragraph{Proof Tactic} Applying a tactic is represented by a \textsf{JSON} record with the following
fields:
\begin{align*}
\mathit{wp.tactic} &::=
\left\{
\begin{array}{rl}
\mathtt{"tactic"} :& \mathit{string}, \\
\mathtt{"header"} :& \mathit{string} ? \\
\mathtt{"select"} :& \mathit{wp.selection}, \\
\mathtt{"params"} :& \mathtt{\{}\; \mathit{string}:\mathit{wp.param} ,\ldots \;\mathtt{\}} ? \\
\mathtt{"children"} :& \mathtt{\{}\; \mathit{string}:\mathit{wp.script}, \ldots \;\mathtt{\}} ? \\
\end{array}
\right\}
\end{align*}
The \verb"header" field is just a descriptive title and has no special meaning. The \verb"tactic"
identifies the tactic, as it has been registered in the \textsf{Frama-C/WP} internal API.
The \verb"selection" is an opaque encoding of the target of the tactic inside the proof obligation
structure. The \verb"params" array stores the value of tactic parameters, if any.
The \verb"children" stores the proof scripts associated with each sub-goal generated by applying
the specified tactic on a proof obligation.
\paragraph{Tactic Parameters} Values of tactical parameters are encoded with the
following \textsf{JSON} format, depending on the internal type of the parameter
value:
\begin{align*}
\mathit{wp.param} ::=\;&
\mathit{bool} ~|~ \mathit{number} ~|~ \mathit{string} \\
|\;&\mathit{wp.named} ~|~ \mathit{wp.selection} \\
\mathit{wp.named} ::= &\mathtt{null} ~|~
\left\{
\begin{array}{rl}
\mathtt{"id"} :& \mathit{string}, \\
\mathtt{"title"} :& \mathit{string}? \\
\mathtt{"description"} :& \mathit{string}?
\end{array}
\right\}
\end{align*}
Named items (\textit{wp.named}) corresponds, for instance, to searched lemmas.
Selections corresponds to terms or expressions selected by the user \emph{via}
the graphical user interface, like the target of the tactic, as described below.
\paragraph{Tactic Selection} The target of the tactic
is identified by a complex structure
encoding on which part of the proof obligation it shall be applied. Since the
exact structure of the proof obligation may vary from time to time, this structure
allows for searching in the proof obligation a \emph{pattern} that ressemble the
original target that was originally selected by the user during an interactive
session with the \textsf{Frama-C/WP} graphical user interface.
Such \emph{patterns} are encoded as follows:
\newcommand{\dash}{\rule[0.5ex]{1ex}{1pt}}
\begin{align*}
\mathit{wp.selection}
::=\;& \mathtt{null} \\
|\;\;& \mathtt{\{}\; \mathtt{"select":"clause\dash{}goal"},\;
\mathit{wp.pattern} \;\mathtt{\}} \\
|\;\;& \mathtt{\{}\; \mathtt{"select":"inside\dash{}goal"},\;
\mathit{wp.occur},\; \mathit{wp.pattern} \;\mathtt{\}} \\
|\;\;& \mathtt{\{}\; \mathtt{"select":"clause\dash{}step"},\;
\mathit{wp.at},\; \mathit{wp.kind},\;
\mathit{wp.pattern} \;\mathtt{\}} \\
|\;\;& \mathtt{\{}\; \mathtt{"select":"inside\dash{}step"},\;
\mathit{wp.at},\; \mathit{wp.kind},\;
\mathit{wp.occur},\; \mathit{wp.pattern} \;\mathtt{\}} \\
|\;\;& \mathtt{\{}\; \mathtt{"select":"range"},\;
\mathtt{"min"}:\mathit{number},\;
\mathtt{"max"}:\mathit{number} \;\mathtt{\}} \\
|\;\;& \mathtt{\{}\; \mathtt{"select":"kint"},\;
\mathtt{"val"}:\mathit{number} \;\mathtt{\}} \\
|\;\;& \mathtt{\{}\; \mathtt{"select":"compose"},\;
\mathtt{"id"}:\mathit{string},\;
\mathtt{"args"}:[\mathit{wp.selection},\ldots]
\;\mathtt{\}} \\
% --
\mathit{wp.pattern} ::=\;& \mathtt{"pattern"} : \mathit{string} \\
\mathit{wp.occur} ::=\;& \mathtt{"occur"} : \mathit{number} \\
\mathit{wp.at} ::=\;& \mathtt{"at"} : \mathit{number} \\
\mathit{wp.kind} ::=\;& \mathtt{"kind"} : \mathtt{"have"|"type"|"init"|"branch"|"either"|"state"} \\
\end{align*}
The various components of selection patterns have the following meaning: \textit{wp.pattern} encodes
a term or predicate pattern; \textit{wp.occur} designates which occurrence of the pattern to select,
in case of there is many of them inside the selected goal or hypothesis; \textit{wp.at} designates the
order of the selected hypothesis inside the proof obligation (the pattern is searched around this value),
and \textit{wp.kind} its kind.
The \textit{wp.pattern} is an simple string that encodes the head of the structure of the
selected term or formulæ inside the designated goal or hypothesis. It is the concatenation of
the first 32 head nodes of width-first traversal of the selected term, each node being represented by
the following string:
\begin{itemize}
\item constant are represented by their value,
\item free variables by their base-name prefixed with \verb'$',
\item bound variables by their de-Bruijn index prefixed with \verb'#',
\item true and false by \verb"T" and \verb"F", and quantifiers by \verb"\F" and \verb"\E",
\item operators by \verb"&,|,!,~,+,-,*,/,%<,>,=,>=,/,?"
\item array operations by \verb"[]", \verb"[.]" and \verb"[=]"
\item record operations by \verb".fd" and \verb"{fd,...}"
\item function calls by their name
\end{itemize}
For instance, the term $(x_1 \leq x_2+1)$ will be represented by the pattern \verb|"<=$x+$x1"|.
\paragraph{Alternative Ordering} When several alternatives are available for
discharging a proof obligation, the \texttt{script} and \texttt{tip} provers
of \textsf{Frama-C/WP} choose which one to apply first according to the
following heuristic:
\begin{enumerate}
\item try internal prover \texttt{"Qed"} with a \texttt{"valid"} verdict;
\item try any SMT prover with a \texttt{"valid"} verdict;
\item try the \texttt{"Coq"} proof assistant with a \texttt{"valid"} verdict;
\item try any Tactic alternative;
\item finally try the remaining Prover alternatives.
\end{enumerate}
Inside the same level of priority, alternatives are kept in their original
order.
......@@ -563,6 +563,10 @@ let spawn_wp_proofs_iter ~mode iter_on_goals =
let get_prover_names () =
match Wp_parameters.Provers.get () with [] -> [ "alt-ergo" ] | pnames -> pnames
let env_script_update () =
try Sys.getenv "FRAMAC_WP_SCRIPT" = "update"
with Not_found -> false
let compute_provers ~mode =
mode.provers <- List.fold_right
(fun pname prvs ->
......@@ -570,7 +574,8 @@ let compute_provers ~mode =
| None -> prvs
| Some VCS.Tactical ->
mode.tactical <- true ;
if pname = "tip" then mode.update <- true ;
if pname = "tip" || env_script_update () then
mode.update <- true ;
prvs
| Some prover ->
(VCS.mode_of_prover_name pname , prover) :: prvs)
......
......@@ -10,7 +10,7 @@
"pattern": "&<=<=<=0$x0land$x42949672954294967295" },
"children": { "Goal 1/3": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid",
"time": 0.0103,
"time": 0.0149,
"steps": 10 } ],
"Goal 2/3": [ { "header": "Bit Range",
"tactic": "Wp.bitrange",
......@@ -27,6 +27,6 @@
"verdict": "valid" } ] } } ],
"Goal 3/3": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid",
"time": 0.0105,
"time": 0.0153,
"steps": 10 } ] } } ],
"bitwise": [ { "prover": "qed", "verdict": "valid" } ] } } ]
......@@ -3,6 +3,5 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 0 goal scheduled
[wp] Proved goals: 0 / 0
[wp] Warning: No goal generated
------------------------------------------------------------
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