diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 65da7ca4b528daae67654b0f7d37fdcc9eb24103..74e6c3b7ea8a2dfa30c8537266425371c8b77926 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -141,22 +141,6 @@ let is_updating () =
| NoCache | Replay | Offline -> false
| Update | Rebuild | Cleanup -> true
-let task_hash wpo drv prover task =
- lazy
- begin
- let file = Wpo.DISK.file_goal
- ~pid:wpo.Wpo.po_pid
- ~model:wpo.Wpo.po_model
- ~prover:(VCS.Why3 prover) in
- let _ = Command.print_file file
- begin fun fmt ->
- Format.fprintf fmt "(* WP Task for Prover %s *)@\n"
- (Why3Provers.print_why3 prover) ;
- Why3.Driver.print_task_prepared drv fmt task ;
- end
- in Digest.file file |> Digest.to_hex
- end
-
let time_fits time = function
| None | Some 0 -> true
| Some limit -> time <= float limit
@@ -256,23 +240,24 @@ let cleanup_cache () =
Wp_parameters.warning ~current:false
"Cannot cleanup cache"
-type runner =
- timeout:int option -> steplimit:int option ->
- Why3.Driver.driver -> Why3Provers.t -> Why3.Task.task ->
+type 'a digest =
+ Why3Provers.t -> 'a -> string
+
+type 'a runner =
+ timeout:int option -> steplimit:int option -> Why3Provers.t -> 'a ->
VCS.result Task.task
-let get_result wpo runner ~timeout ~steplimit drv prover task =
+let get_result ~digest ~runner ~timeout ~steplimit prover goal =
let mode = get_mode () in
match mode with
- | NoCache ->
- runner ~timeout ~steplimit drv prover task
+ | NoCache -> runner ~timeout ~steplimit prover goal
| Offline ->
- let hash = task_hash wpo drv prover task in
+ let hash = lazy (digest prover goal) in
let result = get_cache_result ~mode hash |> VCS.cached in
if VCS.is_verdict result then incr hits else incr miss ;
Task.return result
| Update | Replay | Rebuild | Cleanup ->
- let hash = task_hash wpo drv prover task in
+ let hash = lazy (digest prover goal) in
let result =
get_cache_result ~mode hash
|> promote ~timeout ~steplimit |> VCS.cached in
@@ -284,10 +269,12 @@ let get_result wpo runner ~timeout ~steplimit drv prover task =
end
else
Task.finally
- (runner ~timeout ~steplimit drv prover task)
+ (runner ~timeout ~steplimit prover goal)
begin function
| Task.Result result when VCS.is_verdict result ->
incr miss ;
set_cache_result ~mode hash prover result
| _ -> ()
end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cache.mli b/src/plugins/wp/Cache.mli
index 85130ef5bbf06c648b9bd4bd09b4dd50ed1735c9..7197a8dc22207aa1aec096a1a61735d3e43b4bc8 100644
--- a/src/plugins/wp/Cache.mli
+++ b/src/plugins/wp/Cache.mli
@@ -34,9 +34,12 @@ val is_updating : unit -> bool
val cleanup_cache : unit -> unit
-type runner =
- timeout:int option -> steplimit:int option ->
- Why3.Driver.driver -> Why3Provers.t -> Why3.Task.task ->
+type 'a digest = Why3Provers.t -> 'a -> string
+
+type 'a runner =
+ timeout:int option -> steplimit:int option -> Why3Provers.t -> 'a ->
VCS.result Task.task
-val get_result: Wpo.t -> runner -> runner
+val get_result: digest:('a digest) -> runner:('a runner) -> 'a runner
+
+(**************************************************************************)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 389007c7c917ae9519016a256dd51c427af755ff..51c3938458848eda30cd366caa3eb5ef6a144261 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,9 @@
Plugin WP <next-release>
#########################
+- WP [2020-09-21] Added support for Why3 Coq interactive prover
+- WP [2020-09-21] New option -wp-interactive <mode>
+- WP [2020-09-21] New option -wp-interactive-timeout <seconds>
- WP [2020-09-17] New experimental option: -wp-check-model-hypotheses
Generates requires in contracts for model hypotheses
- WP [2020-09-17] Hypotheses: assigned memory locations
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index a6bfe8c5311134b3378d4ff6fe49ca9145052b34..48b88111f836a747b202dd51c871d2e29484da20 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -263,7 +263,7 @@ class behavior
| Some m , _ -> m
| None , VCS.NativeCoq -> VCS.EditMode
| None , VCS.NativeAltErgo -> VCS.FixMode
- | _ -> VCS.BatchMode in
+ | _ -> if VCS.is_auto prover then VCS.BatchMode else VCS.FixMode in
schedule (Prover.prove w ~mode ~result prover) ;
refresh w
end
@@ -291,7 +291,8 @@ class behavior
val popup_tip = new Widget.popup ()
val popup_ergo = new Widget.popup ()
val popup_coq = new Widget.popup ()
- val popup_why3 = new Widget.popup ()
+ val popup_why3_auto = new Widget.popup ()
+ val popup_why3_inter = new Widget.popup ()
val mutable popup_target = None
method private popup_delete () =
@@ -327,8 +328,10 @@ class behavior
popup_tip#add_item ~label:"Run Script" ~callback:(self#popup_run BatchMode) ;
popup_tip#add_item ~label:"Edit Proof" ~callback:(self#popup_run EditMode) ;
popup_tip#add_item ~label:"Delete Script" ~callback:(self#popup_delete_script) ;
- self#add_popup_proofmodes popup_why3
- [ "Run",BatchMode ] ;
+ popup_why3_auto#add_item ~label:"Run Prover" ~callback:(self#popup_run VCS.BatchMode) ;
+ popup_why3_inter#add_item ~label:"Check Script" ~callback:(self#popup_run VCS.BatchMode) ;
+ popup_why3_inter#add_item ~label:"Edit Script" ~callback:(self#popup_run VCS.EditMode) ;
+ popup_why3_inter#add_item ~label:"Fixup Script" ~callback:(self#popup_run VCS.FixMode) ;
self#add_popup_proofmodes popup_ergo
[ "Run",BatchMode ; "Open Altgr-Ergo on Fail",EditMode ; "Open Altgr-Ergo",EditMode ] ;
self#add_popup_proofmodes popup_coq
@@ -344,7 +347,10 @@ class behavior
| Some Qed -> popup_qed#run ()
| Some NativeCoq -> popup_coq#run ()
| Some NativeAltErgo -> popup_ergo#run ()
- | Some (Why3 _) -> popup_why3#run ()
+ | Some (Why3 _ as p) ->
+ if VCS.is_auto p
+ then popup_why3_auto#run ()
+ else popup_why3_inter#run ()
end
method private action w p =
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index 73c77b5b71d37ffa4fbb17639893672e2e17a7e6..4ad9bd70305c577c20e833482bf6419f7a3cb5b3 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -342,7 +342,7 @@ let json_of_result (p : VCS.prover) (r : VCS.result) =
`Assoc (name :: verdict :: (time @ steps))
let prover_of_json js =
- try VCS.prover_of_name (js >? "prover" |> Json.string)
+ try VCS.parse_prover (js >? "prover" |> Json.string)
with Not_found -> None
let result_of_json js =
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index d19bacb5bd4c9800a65005833298362e9fdc30fd..a4e27a63283ac7f3ed795a1ffe75325fdaf953bd 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1153,18 +1153,21 @@ let ping_prover_call p =
match Why3.Call_provers.query_call p.call with
| NoUpdates
| ProverStarted ->
- let () = match p.timeover with
- | None ->
- let started = Unix.time () in
- p.timeover <- Some (started +. 2.0 +. float p.timeout)
- | Some timeout ->
- let time = Unix.time () in
- if time > timeout then
- begin
- Wp_parameters.debug ~dkey "Hard Kill (late why3server timeout)" ;
- p.interrupted <- true ;
- Why3.Call_provers.interrupt_call p.call ;
- end
+ let () =
+ if p.timeout > 0 then
+ match p.timeover with
+ | None ->
+ let started = Unix.time () in
+ p.timeover <- Some (started +. 2.0 +. float p.timeout)
+ | Some timeout ->
+ let time = Unix.time () in
+ if time > timeout then
+ begin
+ Wp_parameters.debug ~dkey
+ "Hard Kill (late why3server timeout)" ;
+ p.interrupted <- true ;
+ Why3.Call_provers.interrupt_call p.call ;
+ end
in Task.Wait 100
| InternalFailure exn ->
let msg = Format.asprintf "@[<hov 2>%a@]"
@@ -1198,34 +1201,11 @@ let ping_prover_call p =
VCS.pp_result r;
Task.Return (Task.Result r)
-let call_prover prover_config ~timeout ~steplimit drv prover task =
- let steps = match steplimit with Some 0 -> None | _ -> steplimit in
- let limit =
- let def = Why3.Call_provers.empty_limit in
- { def with
- Why3.Call_provers.limit_time = Why3.Opt.get_def def.limit_time timeout;
- Why3.Call_provers.limit_steps = Why3.Opt.get_def def.limit_time steps;
- } in
- let with_steps = match steps, prover_config.Why3.Whyconf.command_steps with
- | None, _ -> false
- | Some _, Some _ -> true
- | Some _, None ->
- Wp_parameters.warning ~once:true ~current:false
- "%a does not support steps limit (ignored option)"
- Why3.Whyconf.print_prover prover ;
- false
- in
- let command = Why3.Whyconf.get_complete_command prover_config ~with_steps in
- let call =
- Why3.Driver.prove_task_prepared ~command ~limit drv task in
- let pp_steps fmt s =
- if with_steps then Format.fprintf fmt "%i steps" (Why3.Opt.get_def (-1) s)
- else Format.fprintf fmt ""
- in
- Wp_parameters.debug ~dkey "Why3 run prover %a with %i timeout %a@."
+let call_prover_task ~timeout ~steps prover call =
+ Wp_parameters.debug ~dkey "Why3 run prover %a with timeout %d, steps %d@."
Why3.Whyconf.print_prover prover
(Why3.Opt.get_def (-1) timeout)
- pp_steps steps ;
+ (Why3.Opt.get_def (-1) steps) ;
let timeout = match timeout with None -> 0 | Some tlimit -> tlimit in
let pcall = {
call ; prover ;
@@ -1242,15 +1222,110 @@ let call_prover prover_config ~timeout ~steplimit drv prover task =
in
Task.async ping
-let is_trivial (t : Why3.Task.task) =
- let goal = Why3.Task.task_goal_fmla t in
- Why3.Term.t_equal goal Why3.Term.t_true
+(* -------------------------------------------------------------------------- *)
+(* --- Batch Prover --- *)
+(* -------------------------------------------------------------------------- *)
+
+let digest wpo drv prover task =
+ let file = Wpo.DISK.file_goal
+ ~pid:wpo.Wpo.po_pid
+ ~model:wpo.Wpo.po_model
+ ~prover:(VCS.Why3 prover) in
+ let _ = Command.print_file file
+ begin fun fmt ->
+ Format.fprintf fmt "(* WP Task for Prover %s *)@\n"
+ (Why3Provers.print_why3 prover) ;
+ Why3.Driver.print_task_prepared drv fmt task ;
+ end
+ in Digest.file file |> Digest.to_hex
+
+let batch pconf driver ?script ~timeout ~steplimit prover task =
+ let steps = match steplimit with Some 0 -> None | _ -> steplimit in
+ let limit =
+ let def = Why3.Call_provers.empty_limit in
+ { def with
+ Why3.Call_provers.limit_time = Why3.Opt.get_def def.limit_time timeout;
+ Why3.Call_provers.limit_steps = Why3.Opt.get_def def.limit_time steps;
+ } in
+ let with_steps = match steps, pconf.Why3.Whyconf.command_steps with
+ | None, _ -> false
+ | Some _, Some _ -> true
+ | Some _, None -> false
+ in
+ let command = Why3.Whyconf.get_complete_command pconf ~with_steps in
+ let inplace = if script <> None then Some true else None in
+ let call = Why3.Driver.prove_task_prepared ?old:script ?inplace
+ ~command ~limit driver task in
+ call_prover_task ~timeout ~steps prover call
+
+(* -------------------------------------------------------------------------- *)
+(* --- Interactive Prover (Coq) --- *)
+(* -------------------------------------------------------------------------- *)
+
+let editor pconf =
+ let config = Why3Provers.config () in
+ try
+ let ed = Why3.Whyconf.editor_by_id config pconf.Why3.Whyconf.editor in
+ String.concat " " (ed.editor_command :: ed.editor_options)
+ with Not_found ->
+ Why3.Whyconf.(default_editor (get_main config))
+
+let scriptfile ~force ~ext wpo =
+ let dir = Wp_parameters.get_session_dir ~force "interactive" in
+ Format.sprintf "%s/%s%s" (dir :> string) wpo.Wpo.po_sid ext
+
+let call_editor ~script pconf =
+ Wp_parameters.feedback ~ontty:`Transient "Editing %S..." script ;
+ let call = Why3.Call_provers.call_editor ~command:(editor pconf) script in
+ call_prover_task ~timeout:None ~steps:None pconf.prover call
+
+let compile ~script ~timeout pconf driver prover task =
+ let digest _prover _task = Digest.file script |> Digest.to_hex in
+ let runner = batch pconf driver ~script in
+ Cache.get_result ~digest ~runner ~timeout ~steplimit:None prover task
+
+let prepare ~mode wpo driver task =
+ let force = match mode with VCS.BatchMode -> false | _ -> true in
+ let ext = Filename.extension (Why3.Driver.file_of_task driver "S" "T" task) in
+ let script = scriptfile ~force wpo ~ext in
+ if Sys.file_exists script then Some script
+ else if force then
+ begin
+ Command.pp_to_file script (fun fmt ->
+ ignore (Why3.Driver.print_task_prepared driver fmt task)
+ ) ; Some script
+ end
+ else None
+
+let interactive ~mode wpo pconf driver prover task =
+ let time = Wp_parameters.InteractiveTimeout.get () in
+ let timeout = if time <= 0 then None else Some time in
+ match prepare ~mode wpo driver task with
+ | None -> Task.return VCS.unknown
+ | Some script ->
+ match mode with
+ | VCS.BatchMode ->
+ compile ~script ~timeout pconf driver prover task
+ | VCS.EditMode ->
+ let open Task in
+ call_editor ~script pconf >>= fun _ ->
+ compile ~script ~timeout pconf driver prover task
+ | VCS.FixMode ->
+ let open Task in
+ compile ~script ~timeout pconf driver prover task >>= fun r ->
+ if VCS.is_valid r then return r else
+ call_editor ~script pconf >>= fun _ ->
+ compile ~script ~timeout pconf driver prover task
(* -------------------------------------------------------------------------- *)
(* --- Prove WPO --- *)
(* -------------------------------------------------------------------------- *)
-let build_proof_task ?timeout ?steplimit ~prover wpo () =
+let is_trivial (t : Why3.Task.task) =
+ let goal = Why3.Task.task_goal_fmla t in
+ Why3.Term.t_equal goal Why3.Term.t_true
+
+let build_proof_task ?(mode=VCS.BatchMode) ?timeout ?steplimit ~prover wpo () =
try
(* Always generate common task *)
let context = Wpo.get_context wpo in
@@ -1259,12 +1334,17 @@ let build_proof_task ?timeout ?steplimit ~prover wpo () =
then Task.return VCS.no_result (* Only generate *)
else
let env = WpContext.on_context context get_why3_env () in
- let drv , config , task = prover_task env prover task in
+ let drv , pconf , task = prover_task env prover task in
if is_trivial task then
Task.return VCS.valid
else
- Cache.get_result wpo (call_prover config)
- ~timeout ~steplimit drv prover task
+ if pconf.interactive then
+ interactive ~mode wpo pconf drv prover task
+ else
+ Cache.get_result
+ ~digest:(digest wpo drv)
+ ~runner:(batch pconf drv ?script:None)
+ ~timeout ~steplimit prover task
with exn ->
if Wp_parameters.has_dkey dkey_api then
Wp_parameters.fatal "[Why3 Error] %a@\n%s"
@@ -1273,7 +1353,7 @@ let build_proof_task ?timeout ?steplimit ~prover wpo () =
else
Task.failed "[Why3 Error] %a" Why3.Exn_printer.exn_printer exn
-let prove ?timeout ?steplimit ~prover wpo =
- Task.later (build_proof_task ?timeout ?steplimit ~prover wpo) ()
+let prove ?mode ?timeout ?steplimit ~prover wpo =
+ Task.later (build_proof_task ?mode ?timeout ?steplimit ~prover wpo) ()
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index ea029e0804bc7aba4a8f25d66b18a043dd0804ea..e29b681ff4412f662db152da2af6b14bb9a9d19a 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -26,8 +26,8 @@ val add_specific_equality:
unit
(** Equality used in the goal, simpler to prove than polymorphic equality *)
-val prove : ?timeout:int -> ?steplimit:int -> prover:Why3Provers.t ->
- Wpo.t -> VCS.result Task.task
+val prove : ?mode:VCS.mode -> ?timeout:int -> ?steplimit:int ->
+ prover:Why3Provers.t -> Wpo.t -> VCS.result Task.task
(** Return NoResult if it is already proved by Qed *)
(**************************************************************************)
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 50507c33c3974e967750caf41b168e317e152ccb..2b7862a000d14da1f3699f8021af17af9babe1c9 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -38,7 +38,7 @@ type mode =
| EditMode (* Edit then check scripts *)
| FixMode (* Try check script, then edit script on non-success *)
-let prover_of_name = function
+let parse_prover = function
| "" | "none" -> None
| "qed" | "Qed" -> Some Qed
| "native-alt-ergo" (* for wp-reports *)
@@ -70,13 +70,19 @@ let prover_of_name = function
(String.concat ":" prv) (Why3Provers.print_wp p) ;
Some (Why3 p)
| NotFound ->
- Wp_parameters.error "Prover '%s' not found in why3.conf" name ;
+ Wp_parameters.error ~once:true
+ "Prover '%s' not found in why3.conf" name ;
None
-let mode_of_prover_name = function
- | "native:coqedit" -> EditMode
- | "native:coqide" | "native:altgr-ergo" -> FixMode
- | _ -> BatchMode
+let parse_mode m =
+ match String.lowercase_ascii m with
+ | "fix" -> FixMode
+ | "edit" -> EditMode
+ | "batch" -> BatchMode
+ | _ ->
+ Wp_parameters.error ~once:true
+ "Unrecognized mode %S (use 'batch' instead)" m ;
+ BatchMode
let name_of_prover = function
| Why3 s -> Why3Provers.print_wp s
@@ -122,8 +128,18 @@ let filename_for_prover = function
| Tactical -> "Tactical"
let is_auto = function
- | Qed | NativeAltErgo | Why3 _ -> true
+ | Qed | NativeAltErgo -> true
| Tactical | NativeCoq -> false
+ | Why3 p ->
+ match p.prover_name with
+ | "Alt-Ergo" | "CVC4" | "Z3" -> true
+ | "Coq" -> false
+ | _ ->
+ let config = Why3Provers.config () in
+ try
+ let prover_config = Why3.Whyconf.get_prover_config config p in
+ not prover_config.interactive
+ with Not_found -> true
let cmp_prover p q =
match p,q with
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 54b34f23ef850f4e974c4a2e18034c035d510ec4..e43bb52617772920bbe7fb93760c1a79ed832273 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -44,10 +44,11 @@ module Pmap : Map.S with type key = prover
val name_of_prover : prover -> string
val title_of_prover : prover -> string
val filename_for_prover : prover -> string
-val prover_of_name : string -> prover option
-val mode_of_prover_name : string -> mode
val title_of_mode : mode -> string
+val parse_mode : string -> mode
+val parse_prover : string -> prover option
+
val pp_prover : Format.formatter -> prover -> unit
val pp_mode : Format.formatter -> mode -> unit
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
index ab50c9858b2de0a3fec9d8adc147994a3e0db981..46a1f714ab5902d7b9356ede7a3a0f879af75a54 100644
--- a/src/plugins/wp/Why3Provers.ml
+++ b/src/plugins/wp/Why3Provers.ml
@@ -109,3 +109,5 @@ let has_shortcut p s =
(Why3.Whyconf.get_prover_shortcuts (config ())) with
| None -> false
| Some p' -> Why3.Whyconf.Prover.equal p p'
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/doc/manual/wp.bib b/src/plugins/wp/doc/manual/wp.bib
index bcc4524f29d0569c6fa30a52b475ee1966715b73..cbe190e5609458dda0b3b93767fafdf007fdd7c8 100644
--- a/src/plugins/wp/doc/manual/wp.bib
+++ b/src/plugins/wp/doc/manual/wp.bib
@@ -98,6 +98,39 @@
url = {http://ergo.lri.fr/papers/ergo.ps}
}
+@inproceedings{CVC4,
+ url = "http://www.cs.stanford.edu/~barrett/pubs/BCD+11.pdf",
+ author = "Clark Barrett and Christopher L. Conway and Morgan Deters and
+ Liana Hadarean and Dejan Jovanovi{'{c}} and Tim King and
+ Andrew Reynolds and Cesare Tinelli",
+ title = "{CVC4}",
+ booktitle = "Proceedings of the 23rd International Conference on Computer Aided Verification (CAV '11)",
+ series = "Lecture Notes in Computer Science",
+ volume = 6806,
+ publisher = "Springer",
+ editor = "Ganesh Gopalakrishnan and Shaz Qadeer",
+ pages = "171--177",
+ month = jul,
+ year = 2011,
+ note = "Snowbird, Utah",
+ category = "Conference Publications"
+}
+
+@InProceedings{Z3,
+author="de Moura, Leonardo
+and Bj{\o}rner, Nikolaj",
+editor="Ramakrishnan, C. R.
+and Rehof, Jakob",
+title="Z3: An Efficient SMT Solver",
+booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
+year="2008",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="337--340",
+abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.",
+isbn="978-3-540-78800-3"
+}
+
@inproceedings{qed,
author = {Lo{\"{\i}}c Correnson},
title = {Qed. Computing What Remains to Be Proved},
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 3e343ef02f74e318d518694174ef46d0af68f881..a690b944e0e6c4bcf93cee5cb064bdff5e15494c 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -10,51 +10,13 @@ This plug-in computes proof obligations of programs annotated with
\textsf{ACSL} annotations by \emph{weakest precondition calculus},
using a parametrized memory model to represent pointers and heap
values. The proof obligations may then be discharged by external
-decision procedures, which range over automated theorem provers such
-as \textsf{Alt-Ergo}~\cite{AltErgo2006}, interactive proof assistants
-like \textsf{Coq}~\cite{Coq84} and the interactive proof manager
-\textsf{Why3}~\cite{Why3}.
-
-This chapter describes how to use the plug-in, from the
-\textsf{Frama-C} graphical user interface (section~\ref{wp-gui}), from
-the command line (section~\ref{wp-cmdline}), or from another plug-in
-(section~\ref{wp-api}). Additionally, the combination of the \textsf{WP}
-plug-in with the load and save commands of \textsf{Frama-C} and/or the
-\texttt{-then} command-line option is explained in section~\ref{wp-persistent}.
-
-\clearpage
-%-----------------------------------------------------------------------------
-\section{Installing Provers}
-\label{wp-install-provers}
-%-----------------------------------------------------------------------------
-
-The \textsf{WP} plug-in requires external provers to work.
-The recommended versions for external provers are:
-\begin{center}
- \begin{tabular}{crlc}
- Prover & Versions & Download &\\
- \hline
- \textsf{Why3} & \verb|1.3.1| &
- \url{http://why3.lri.fr} & \cite{Why3}\\
- \textsf{Alt-Ergo} & \verb|2.0.0| &
- \url{http://alt-ergo.ocamlpro.com} & \cite{AltErgo2006}\\
- % \textsf{Coq} & \verb|8.9.0| &
- % \url{http://coq.inria.fr} & \cite{Coq84}\\
- \end{tabular}
-\end{center}
-
-Recent \textsf{OPAM}-provided versions should work smoothly.
-Other versions might be supported as well, typically, as far as we know:
-\begin{itemize}
-\item \textsf{Alt-Ergo} \verb+2.2.0+ and \verb+2.3.0+, although distributed under a non-commercial licence.
-% \item \textsf{Coq} \verb+8.7.2+ and \verb+8.8.2+, although proof scripts compatibility can be an issue.
-\item \textsf{Why3} \verb+1.3.1+.
-\end{itemize}
-
-Other provers, like \textsf{Coq}, \textsf{Gappa}, \textsf{Z3}, \textsf{CVC3},
-\textsf{CVC4}, \textsf{PVS}, and many others, are accessible from
-\textsf{WP} through \textsf{Why3}. We refer the user to the manual of
-\textsf{Why3} to handle specific configuration tasks.
+automated theorem provers such as
+\textsf{Alt-Ergo}~\cite{AltErgo2006},
+\textsf{CVC4}~\cite{CVC4} and
+\textsf{Z3}~\cite{Z3}
+or by interactive proof assistants
+like \textsf{Coq}~\cite{Coq84} and more generally, any automated or interactive
+prover supported by \textsf{Why3}~\cite{Why3}.
\clearpage
%-----------------------------------------------------------------------------
@@ -1018,6 +980,10 @@ all unproved proof obligations are sent to external decision procedures.
Support for \textsf{Why-3 IDE} is no longer provided.
+Since \textsf{Frama-C 22.0} (Titanium) support for Coq interactive prover has
+been added and might also work with other interactive provers.
+See \texttt{-wp-interactive <mode>} option for details.
+
\begin{description}
\item[\tt -wp-prover <dp,...>] selects the decision procedures used to
discharge proof obligations. See below for supported provers. By
@@ -1028,6 +994,13 @@ Support for \textsf{Why-3 IDE} is no longer provided.
It is possible to ask for several decision procedures to be tried.
For each goal, the first decision procedure that succeeds cancels the
other attempts.
+\item[\tt -wp-interactive <mode>] selects the interaction mode with
+ interactive provers such as Coq. Three modes are available:
+ \texttt{"batch"} mode only check existing scripts (the default);
+ \texttt{"edit"} mode opens the default prover editor on each generated goal;
+ \texttt{"fix"} mode only opens
+ editor for non-proved goals. New scripts are created in the \texttt{interactive}
+ directory of \textsf{WP} session (see option \texttt{-wp-session <dir>}).
\item[\tt -wp-detect] lists the provers available for \textsf{Why-3}.
This command can only work if \textsf{why3} API was installed before building and
installing \textsf{Frama-C}.
@@ -1053,6 +1026,8 @@ Support for \textsf{Why-3 IDE} is no longer provided.
to the decision prover (defaults to 10 seconds).
\item[\tt -wp-smoke-timeout <n>] sets the timeout (in seconds) for smoke tests
(see \verb+-wp-smoke-tests+, defaults to 5 seconds).
+\item[\tt -wp-interactive-timeout <n>] sets the timeout (in seconds) for checking
+ edited scripts with interactive provers (defaults to 30 seconds).
\item[\tt -wp-time-extra <n>] additional time allocated to provers when
replaying a script. This is used to cope with variable machine load.
Default is \verb+5s+.
diff --git a/src/plugins/wp/doc/manual/wp_simplifier.tex b/src/plugins/wp/doc/manual/wp_simplifier.tex
index 4dda147545e9ef5766ef6d3e8696a953e6d3443a..2e3e82551aa4e94a1ab36ac54e667b9e3ff97d0c 100644
--- a/src/plugins/wp/doc/manual/wp_simplifier.tex
+++ b/src/plugins/wp/doc/manual/wp_simplifier.tex
@@ -344,13 +344,3 @@ following heuristic:
Inside the same level of priority, alternatives are kept in their original
order.
-
-
-
-
-
-
-
-
-
-
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index 08291e8aeea9ec4e9fc2fe1b7f5f2b9be9945853..83b432ac6c284ec2826c9f5c99420d525a7bbcc4 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -40,7 +40,7 @@ let dispatch ?(config=VCS.default) mode prover wpo =
ProverWhy3.prove
~timeout:(VCS.get_timeout ~smoke config)
~steplimit:(VCS.get_stepout config)
- ~prover wpo
+ ~mode ~prover wpo
end
let started ?start wpo =
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index ed3a27c63af70ad7d6bc876c6d3adbb5c88fd0f9..74a692cf28f452a7040299b9129aa4fca50b15f3 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -551,7 +551,7 @@ let do_list_scheduled_result () =
(* --- Proving --- *)
(* ------------------------------------------------------------------------ *)
-type mode = {
+type script = {
mutable tactical : bool ;
mutable update : bool ;
mutable depth : int ;
@@ -561,24 +561,24 @@ type mode = {
mutable provers : (VCS.mode * VCS.prover) list ;
}
-let spawn_wp_proofs ~mode goals =
- if mode.tactical || mode.provers<>[] then
+let spawn_wp_proofs ~script goals =
+ if script.tactical || script.provers<>[] then
begin
let server = ProverTask.server () in
ignore (Wp_parameters.Share.get_dir "."); (* To prevent further errors *)
Bag.iter
(fun goal ->
- if mode.tactical
+ if script.tactical
&& not (Wpo.is_trivial goal)
- && (mode.auto <> [] || ProofSession.exists goal)
+ && (script.auto <> [] || ProofSession.exists goal)
then
ProverScript.spawn
~failed:false
- ~auto:mode.auto
- ~depth:mode.depth
- ~width:mode.width
- ~backtrack:mode.backtrack
- ~provers:(List.map snd mode.provers)
+ ~auto:script.auto
+ ~depth:script.depth
+ ~width:script.width
+ ~backtrack:script.backtrack
+ ~provers:(List.map snd script.provers)
~start:do_wpo_start
~progress:do_progress
~result:do_wpo_result
@@ -591,7 +591,7 @@ let spawn_wp_proofs ~mode goals =
~progress:do_progress
~result:do_wpo_result
~success:do_wpo_success
- mode.provers
+ script.provers
) goals ;
Task.on_server_wait server do_wpo_wait ;
Task.launch server
@@ -604,19 +604,20 @@ 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 ->
- match VCS.prover_of_name pname with
- | None -> prvs
- | Some VCS.Tactical ->
- mode.tactical <- true ;
- if pname = "tip" || env_script_update () then
- mode.update <- true ;
- prvs
- | Some prover ->
- (VCS.mode_of_prover_name pname , prover) :: prvs)
- (get_prover_names ()) []
+let compute_provers ~mode ~script =
+ script.provers <- List.fold_right
+ begin fun pname prvs ->
+ match VCS.parse_prover pname with
+ | None -> prvs
+ | Some VCS.Tactical ->
+ script.tactical <- true ;
+ if pname = "tip" || env_script_update () then
+ script.update <- true ;
+ prvs
+ | Some prover ->
+ let pmode = if VCS.is_auto prover then VCS.BatchMode else mode in
+ (pmode , prover) :: prvs
+ end (get_prover_names ()) []
let dump_strategies =
let once = ref true in
@@ -629,18 +630,18 @@ let dump_strategies =
Format.fprintf fmt "@\n '%s': %s" h#id h#title
)))
-let default_mode () = {
+let default_script_mode () = {
tactical = false ; update=false ; provers = [] ;
depth=0 ; width = 0 ; auto=[] ; backtrack = 0 ;
}
-let compute_auto ~mode =
- mode.auto <- [] ;
- mode.width <- Wp_parameters.AutoWidth.get () ;
- mode.depth <- Wp_parameters.AutoDepth.get () ;
- mode.backtrack <- max 0 (Wp_parameters.BackTrack.get ()) ;
+let compute_auto ~script =
+ script.auto <- [] ;
+ script.width <- Wp_parameters.AutoWidth.get () ;
+ script.depth <- Wp_parameters.AutoDepth.get () ;
+ script.backtrack <- max 0 (Wp_parameters.BackTrack.get ()) ;
let auto = Wp_parameters.Auto.get () in
- if mode.depth <= 0 || mode.width <= 0 then
+ if script.depth <= 0 || script.width <= 0 then
( if auto <> [] then
Wp_parameters.feedback
"Auto-search deactivated because of 0-depth or 0-width" )
@@ -650,17 +651,17 @@ let compute_auto ~mode =
(fun id ->
if id = "?" then dump_strategies ()
else
- try mode.auto <- Strategy.lookup ~id :: mode.auto
+ try script.auto <- Strategy.lookup ~id :: script.auto
with Not_found ->
Wp_parameters.error ~current:false
"Strategy -wp-auto '%s' unknown (ignored)." id
) auto ;
- mode.auto <- List.rev mode.auto ;
- if mode.auto <> [] then mode.tactical <- true ;
+ script.auto <- List.rev script.auto ;
+ if script.auto <> [] then script.tactical <- true ;
end
-let do_update_session mode goals =
- if mode.update then
+let do_update_session ~script goals =
+ if script.update then
begin
let removed = ref 0 in
let updated = ref 0 in
@@ -714,24 +715,25 @@ let do_update_session mode goals =
end
let do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) =
- let mode = default_mode () in
- compute_provers ~mode ;
- compute_auto ~mode ;
+ let script = default_script_mode () in
+ let mode = VCS.parse_mode (Wp_parameters.Interactive.get ()) in
+ compute_provers ~mode ~script ;
+ compute_auto ~script ;
begin match provers with None -> () | Some prvs ->
- mode.provers <- List.map (fun dp -> VCS.BatchMode , VCS.Why3 dp) prvs
+ script.provers <- List.map (fun dp -> VCS.BatchMode , VCS.Why3 dp) prvs
end ;
begin match tip with None -> () | Some tip ->
- mode.tactical <- tip ;
- mode.update <- tip ;
+ script.tactical <- tip ;
+ script.update <- tip ;
end ;
- let spawned = mode.tactical || mode.provers <> [] in
+ let spawned = script.tactical || script.provers <> [] in
begin
if spawned then do_list_scheduled goals ;
- spawn_wp_proofs ~mode goals ;
+ spawn_wp_proofs ~script goals ;
if spawned then
begin
do_list_scheduled_result () ;
- do_update_session mode goals ;
+ do_update_session ~script goals ;
end
else if not (Wp_parameters.Print.get ()) then
Bag.iter do_wpo_display goals
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index 07e77bf23093eb5c0ec694eecf32ac30f6317f15..ab8fd28f71adf5fe5a631056ae2ad39533d5a421 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
@@ -19,10 +19,10 @@ let run () =
let provers =
List.fold_right
- (fun pname prvs -> match VCS.prover_of_name pname with
+ (fun pname prvs -> match VCS.parse_prover pname with
| None -> prvs
| Some VCS.Tactical -> prvs
- | Some prv -> (VCS.mode_of_prover_name pname, prv) :: prvs)
+ | Some prv -> (VCS.BatchMode, prv) :: prvs)
["qed"] []
in
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index f38450c4501df76ed0fdbe6cbebbee247a3431d8..ee5548356cc7a0037c3bc2f56dd2c86f7b62b228 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -18,10 +18,10 @@ let run () =
let provers =
List.fold_right
- (fun pname prvs -> match VCS.prover_of_name pname with
+ (fun pname prvs -> match VCS.parse_prover pname with
| None -> prvs
| Some VCS.Tactical -> prvs
- | Some prv -> (VCS.mode_of_prover_name pname, prv) :: prvs)
+ | Some prv -> (VCS.BatchMode, prv) :: prvs)
["alt-ergo"] []
in
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
index 0aeeeccf367612ea83cffeda8d96603923e5c18f..ce12f14d75e508eb5d7d3aaf23c54f7322e71554 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/no_step_limit.res.oracle
@@ -2,7 +2,6 @@
[kernel] Parsing tests/wp_plugin/no_step_limit.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] Warning: no-steps does not support steps limit (ignored option)
[wp] [no-steps] Goal typed_lemma_truc : Unsuccess
[wp] Proved goals: 0 / 1
no-steps: 0 (unsuccess: 1)
diff --git a/src/plugins/wp/wpReport.ml b/src/plugins/wp/wpReport.ml
index be5b8151c1363541716bd1ebf093eb147be42926..6bdd9397a04e55018e96370fa42afd2ce900c248 100644
--- a/src/plugins/wp/wpReport.ml
+++ b/src/plugins/wp/wpReport.ml
@@ -609,7 +609,7 @@ let pstats ~config fmt s cmd arg =
| "wp" | "qed" -> stat ~config fmt (get_prover s VCS.Qed) arg
| cmd when is_stat_name cmd -> stat ~config fmt s.main cmd
| prover ->
- match (VCS.prover_of_name prover) with
+ match (VCS.parse_prover prover) with
| None -> Wp_parameters.error ~once:true "Unknown prover name %s" prover
| Some prover -> stat ~config fmt (get_prover s prover) arg
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 3fd6bd1b7487f96a33e342eca0758866d53a484c..85a91ef237393229e0aefb1a077ff92e76f8fe13 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -621,6 +621,20 @@ module Provers = String_list
"
end)
+let () = Parameter_customize.set_group wp_prover
+module Interactive = String
+ (struct
+ let option_name = "-wp-interactive"
+ let arg_name = "mode"
+ let default = "batch"
+ let help =
+ "WP mode for interactive provers:\n\
+ - 'batch': use script only (default)\n\
+ - 'edit': run editor on every goal\n\
+ - 'fix': run editor for unproved goal\n\
+ "
+ end)
+
let () = Parameter_customize.set_group wp_prover
module RunAllProvers =
False(struct
@@ -732,6 +746,18 @@ module SmokeTimeout =
"Set the timeout (in seconds) for provers (default: %d)." default
end)
+let () = Parameter_customize.set_group wp_prover
+module InteractiveTimeout =
+ Int(struct
+ let option_name = "-wp-interactive-timeout"
+ let default = 30
+ let arg_name = "n"
+ let help =
+ Printf.sprintf
+ "Set the timeout (in seconds) for checking scripts\n\
+ of interactive provers (default: %d)." default
+ end)
+
let () = Parameter_customize.set_group wp_prover
module TimeExtra =
Int(struct
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 5723c87072a18a4d4a738af17b749727147fb94a..236c418e01883ea1690ca1a4961af637dd808464 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -108,6 +108,7 @@ module PrecondWeakening : Parameter_sig.Bool
module Detect: Parameter_sig.Bool
module Generate:Parameter_sig.Bool
module Provers: Parameter_sig.String_list
+module Interactive: Parameter_sig.String
module RunAllProvers: Parameter_sig.Bool
module Cache: Parameter_sig.String
module CacheEnv: Parameter_sig.Bool
@@ -118,6 +119,7 @@ module Script: Parameter_sig.String
module UpdateScript: Parameter_sig.Bool
module Timeout: Parameter_sig.Int
module SmokeTimeout: Parameter_sig.Int
+module InteractiveTimeout: Parameter_sig.Int
module TimeExtra: Parameter_sig.Int
module TimeMargin: Parameter_sig.Int
module CoqTimeout: Parameter_sig.Int
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 252264a5f932e20b76b203fb541fc3d744c2b170..a36b16398193812618864a7ab292f6d1d012b751 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -954,7 +954,7 @@ let goals_of_property =
let prover_of_name =
Dynamic.register ~plugin:"Wp" "Wpo.prover_of_name" ~journalize:false
(Datatype.func Datatype.string (Datatype.option ProverType.ty))
- VCS.prover_of_name
+ VCS.parse_prover
(* -------------------------------------------------------------------------- *)
(* --- Prover and Files --- *)