From 647c2821c0ad3b4ec3bcd3f7ca310323a25824d5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 15 May 2023 18:25:31 +0200
Subject: [PATCH] [wp] normalizing tip,script and mode
---
src/plugins/wp/Cache.ml | 10 +----
src/plugins/wp/ProofSession.ml | 52 +++++++++++++++++++++++++
src/plugins/wp/ProofSession.mli | 12 ++++++
src/plugins/wp/ProverScript.ml | 21 ++++++----
src/plugins/wp/ProverScript.mli | 1 +
src/plugins/wp/doc/manual/wp_plugin.tex | 17 +++++++-
src/plugins/wp/register.ml | 50 ++++++++++--------------
src/plugins/wp/wpContext.ml | 9 ++++-
src/plugins/wp/wpContext.mli | 5 ++-
src/plugins/wp/wp_parameters.ml | 39 ++++++++++---------
10 files changed, 146 insertions(+), 70 deletions(-)
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 76ff4b37443..247f0324a9f 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -105,14 +105,6 @@ let parse_mode ~origin ~fallback = function
"Unknown %s mode %S (use %s instead)" origin m fallback ;
raise Not_found
-let mode_name = function
- | NoCache -> "none"
- | Update -> "update"
- | Replay -> "replay"
- | Rebuild -> "rebuild"
- | Offline -> "offline"
- | Cleanup -> "cleanup"
-
module MODE = WpContext.StaticGenerator(Datatype.Unit)
(struct
type key = unit
@@ -134,7 +126,7 @@ module MODE = WpContext.StaticGenerator(Datatype.Unit)
end)
let get_mode = MODE.get
-let set_mode m = MODE.clear () ; Wp_parameters.Cache.set (mode_name m)
+let set_mode m = MODE.set () m
let is_active = function
| NoCache -> false
diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml
index 4e3e2eeaf3a..678d280f552 100644
--- a/src/plugins/wp/ProofSession.ml
+++ b/src/plugins/wp/ProofSession.ml
@@ -27,6 +27,58 @@ type script =
| Script of string
| Deprecated of string
+type mode =
+ | Batch
+ | Update
+ | Dry
+ | Init
+
+let parse_mode ~origin ~fallback = function
+ | "batch" -> Batch
+ | "update" -> Update
+ | "dry" -> Dry
+ | "init" -> Init
+ | "" -> raise Not_found
+ | m ->
+ Wp_parameters.warning ~current:false
+ "Unknown %s mode %S (use %s instead)" origin m fallback ;
+ raise Not_found
+
+module MODE = WpContext.StaticGenerator(Datatype.Unit)
+ (struct
+ type key = unit
+ type data = mode
+ let name = "Wp.Script.mode"
+ let compile () =
+ try
+ if not (Wp_parameters.CacheEnv.get()) then
+ raise Not_found ;
+ let origin = "FRAMAC_WP_SCRIPT" in
+ parse_mode ~origin ~fallback:"-wp-script" (Sys.getenv origin)
+ with Not_found ->
+ try
+ let mode = Wp_parameters.ScriptMode.get() in
+ parse_mode ~origin:"-wp-script" ~fallback:"batch" mode
+ with Not_found ->
+ let provers = Wp_parameters.Provers.get () in
+ if List.mem "tip" provers then Update else
+ if List.mem "script" provers then Batch else
+ Dry
+ end)
+
+let get_mode = MODE.get
+let set_mode m = MODE.set () m
+
+let scratch_mode () =
+ match MODE.get () with
+ | Batch | Update -> false
+ | Dry | Init -> true
+
+let saving_mode () =
+ match MODE.get () with
+ | Update | Init -> true
+ | Batch | Dry -> false
+
let files : (string,script) Hashtbl.t = Hashtbl.create 32
let jsonfile (dir:Datatype.Filepath.t) =
diff --git a/src/plugins/wp/ProofSession.mli b/src/plugins/wp/ProofSession.mli
index a7dd99a46ca..833cfea1038 100644
--- a/src/plugins/wp/ProofSession.mli
+++ b/src/plugins/wp/ProofSession.mli
@@ -25,6 +25,18 @@ type script =
| Script of string
| Deprecated of string
+type mode =
+ | Batch
+ | Update
+ | Dry
+ | Init
+
+val get_mode : unit -> mode
+val set_mode : mode -> unit
+
+val scratch_mode : unit -> bool
+val saving_mode : unit -> bool
+
val pp_file : Format.formatter -> string -> unit
val pp_script_for : Format.formatter -> Wpo.t -> unit
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index e74b8f423fe..feb73306307 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -118,6 +118,7 @@ struct
depth : int ;
width : int ;
auto : Strategy.heuristic list ; (* DEPRECATED *)
+ strategies : bool ;
mutable signaled : bool ;
backtrack : int ;
mutable backtracking : backtracking option ;
@@ -219,11 +220,11 @@ struct
let provers env = env.provers
let make tree
- ~valid ~failed ~provers
+ ~valid ~failed ~provers ~strategies
~depth ~width ~backtrack ~auto
~progress ~result ~success =
{ tree ; valid ; failed ; provers ;
- depth ; width ; backtrack ; auto ;
+ depth ; width ; backtrack ; auto ; strategies ;
progress ; result ; success ;
backtracking = None ;
signaled = false }
@@ -404,7 +405,7 @@ let explore_hints env process =
(* -------------------------------------------------------------------------- *)
let automated env process : solver =
- auto env +>> explore_hints env process
+ auto env +>> if env.Env.strategies then explore_hints env process else unknown
(* -------------------------------------------------------------------------- *)
(* --- Apply Script Tactic --- *)
@@ -504,7 +505,7 @@ let rec process env node =
let task
~valid ~failed ~provers
- ~depth ~width ~backtrack ~auto ~scratch
+ ~depth ~width ~backtrack ~auto ~scratch ~strategies
~start ~progress ~result ~success wpo =
begin fun () ->
Wp_parameters.debug ~dkey:dkey_pp_allgoals "%a" Wpo.pp_goal_flow wpo ;
@@ -520,7 +521,7 @@ let task
let tree = ProofEngine.proof ~main:wpo in
let env = Env.make tree
~valid ~failed ~provers
- ~depth ~width ~backtrack ~auto
+ ~depth ~width ~backtrack ~auto ~strategies
~progress ~result ~success in
crawl env (process env) None script >>?
(fun _ -> ProofEngine.forward tree) ;
@@ -534,6 +535,7 @@ type 'a process =
?valid:bool -> ?failed:bool -> ?scratch:bool -> ?provers:VCS.prover list ->
?depth:int -> ?width:int -> ?backtrack:int ->
?auto:Strategy.heuristic list ->
+ ?strategies:bool ->
?start:(Wpo.t -> unit) ->
?progress:(Wpo.t -> string -> unit) ->
?result:(Wpo.t -> VCS.prover -> VCS.result -> unit) ->
@@ -547,21 +549,23 @@ let skip3 _ _ _ = ()
let prove
?(valid = true) ?(failed = true) ?(scratch = false) ?(provers = [])
?(depth = 0) ?(width = 0) ?(backtrack = 0) ?(auto = [])
+ ?(strategies = false)
?(start = skip1) ?(progress = skip2) ?(result = skip3) ?(success = skip2)
wpo =
Task.todo (task
~valid ~failed ~provers
- ~depth ~width ~backtrack ~auto ~scratch
+ ~depth ~width ~backtrack ~auto ~scratch ~strategies
~start ~progress ~result ~success wpo)
let spawn
?(valid = true) ?(failed = true) ?(scratch = false) ?(provers = [])
?(depth = 0) ?(width = 0) ?(backtrack = 0) ?(auto = [])
+ ?(strategies = false)
?(start = skip1) ?(progress = skip2) ?(result = skip3) ?(success = skip2)
wpo =
schedule (task
~valid ~failed ~provers
- ~depth ~width ~backtrack ~auto ~scratch
+ ~depth ~width ~backtrack ~auto ~scratch ~strategies
~start ~progress ~result ~success wpo)
let search
@@ -571,7 +575,7 @@ let search
begin
let env = Env.make tree
~valid:false ~failed:false ~provers
- ~depth ~width ~backtrack ~auto
+ ~depth ~width ~backtrack ~auto ~strategies:false
~progress ~result ~success in
schedule
begin fun () ->
@@ -589,6 +593,7 @@ let explore ?(depth=0) ?(strategy)
let depth = ProofEngine.depth node + depth in
let env : Env.t =
Env.make tree ~valid:false ~failed:false
+ ~strategies:(strategy <> None)
~provers:[] ~depth ~width:0 ~backtrack:0 ~auto:[]
~progress ~result ~success in
schedule
diff --git a/src/plugins/wp/ProverScript.mli b/src/plugins/wp/ProverScript.mli
index e83c5e83dc8..022ffd6b573 100644
--- a/src/plugins/wp/ProverScript.mli
+++ b/src/plugins/wp/ProverScript.mli
@@ -40,6 +40,7 @@ type 'a process =
?width:int ->
?backtrack:int ->
?auto:Strategy.heuristic list ->
+ ?strategies:bool ->
?start:(Wpo.t -> unit) ->
?progress:(Wpo.t -> string -> unit) ->
?result:(Wpo.t -> prover -> result -> unit) ->
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index af659c6e712..d21f7f78f99 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -1314,6 +1314,21 @@ See \texttt{-wp-interactive <mode>} option for details.
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.
+
+ You may also select provers \verb|"tip"| to use proof strategies and \verb|"script"| to use
+ proof scripts (without applying new proof strategies),
+ see option \verb|"-wp-script"| below for more details.
+\item[\tt -wp-script <mode>] selects how to manage proof strategies and proof
+ scripts session. Several modes are available:
+ \begin{itemize}
+ \item \texttt{"batch"} use existing scripts, but do not store new scripts.
+ This is the default mode for prover \verb|"script"|.
+ \item \texttt{"update"} use existing scripts and store new or updated scripts in proof session.
+ This is the default mode for prover \verb|tip|.
+ \item \texttt{"init"} don't use existing scripts and store the newly generated
+ scripts in proof session.
+ \item \texttt{"dry"} don't use existing script and don't store any new scripts in proof session.
+ \end{itemize}
\item[\tt -wp-interactive <mode>] selects the interaction mode with
interactive provers such as Coq (while it could work for other interactive
provers, it has not been tested so far). Five modes are available:
@@ -1334,7 +1349,7 @@ See \texttt{-wp-interactive <mode>} option for details.
\item[\tt -wp-(no)-run-all-provers] Run all specified provers on each goal not
proved by Qed. When a prover succeeds in proving the goal, the others are not
stopped. (default is: no).
-\item[\tt -wp-strategy s,...] acticate proof strategies and specifies the default
+\item[\tt -wp-strategy s,...] specifies the default
ones to be used, see Section~\ref{wp-proof-strategies} for details.
\item[\tt -wp-gen] only generates proof obligations, does not run provers.
See option \texttt{-wp-out} to obtain the generated proof obligations.
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 4bfafe892e9..597d31342dd 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -481,7 +481,8 @@ let do_list_scheduled_result () =
(* ------------------------------------------------------------------------ *)
type script = {
- mutable tactical : bool ;
+ mutable proverscript : bool ;
+ mutable strategies : bool ;
mutable scratch : bool ;
mutable update : bool ;
mutable stdout : bool ;
@@ -493,7 +494,7 @@ type script = {
}
let spawn_wp_proofs ~script goals =
- if script.tactical || script.provers<>[] then
+ if script.proverscript || script.provers<>[] then
begin
let server = ProverTask.server () in
ignore (Wp_parameters.Share.get_dir "."); (* To prevent further errors *)
@@ -501,9 +502,10 @@ let spawn_wp_proofs ~script goals =
let cache = Cache.get_mode () in
Bag.iter
(fun goal ->
- if script.tactical
+ if script.proverscript
&& not (Wpo.is_trivial goal)
&& (script.auto <> [] ||
+ script.strategies ||
ProofSession.exists goal ||
Wp_parameters.DefaultStrategies.get () <> [] ||
ProofStrategy.hints goal <> [])
@@ -511,6 +513,7 @@ let spawn_wp_proofs ~script goals =
ProverScript.spawn
~failed:false
~scratch:script.scratch
+ ~strategies:script.strategies
~auto:script.auto
~depth:script.depth
~width:script.width
@@ -535,11 +538,8 @@ let spawn_wp_proofs ~script goals =
end
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
+ match Wp_parameters.Provers.get () with
+ | [] -> [ "alt-ergo" ] | pnames -> pnames
let compute_provers ~mode ~script =
script.provers <- List.fold_right
@@ -547,9 +547,8 @@ let compute_provers ~mode ~script =
match VCS.parse_prover pname with
| None -> prvs
| Some VCS.Tactical ->
- script.tactical <- true ;
- if pname = "tip" || env_script_update () then
- script.update <- true ;
+ script.proverscript <- true ;
+ if pname = "tip" then script.strategies <- true ;
prvs
| Some prover ->
let pmode = if VCS.is_auto prover then VCS.Batch else mode in
@@ -569,8 +568,12 @@ let dump_strategies =
let default_script_mode () = {
provers = [] ;
- tactical = false ; update = false ; scratch = false ; stdout = false ;
- depth=0 ; width = 0 ; auto=[] ; backtrack = 0 ;
+ proverscript = false ;
+ strategies = false ;
+ update = ProofSession.saving_mode () ;
+ scratch = ProofSession.scratch_mode () ;
+ stdout = Wp_parameters.ScriptOnStdout.get ();
+ depth=0 ; width = 0 ; backtrack = 0 ; auto=[] ;
}
let compute_auto ~script =
@@ -595,7 +598,7 @@ let compute_auto ~script =
"Strategy -wp-auto '%s' unknown (ignored)." id
) auto ;
script.auto <- List.rev script.auto ;
- if script.auto <> [] then script.tactical <- true ;
+ if script.auto <> [] then script.proverscript <- true ;
end
type session_scripts = {
@@ -732,22 +735,11 @@ let do_wp_proofs ?provers ?tip (goals : Wpo.t Bag.t) =
begin match provers with None -> () | Some prvs ->
script.provers <- List.map (fun dp -> VCS.Batch , VCS.Why3 dp) prvs
end ;
- begin match tip with None -> () | Some tip ->
- script.tactical <- tip ;
- script.update <- tip ;
- end ;
- begin match Wp_parameters.ScriptMode.get () with
- | "default" -> ()
- | "batch" -> script.update <- false
- | "update" -> script.update <- true
- | "init" -> script.scratch <- true
- | "dry" -> script.scratch <- true ; script.update <- false
- | opt -> Wp_parameters.error "Invalid -wp-script '%s' option" opt
- end ;
- begin
- script.stdout <- Wp_parameters.ScriptOnStdout.get ();
+ begin match tip with None -> () | Some strategies ->
+ script.proverscript <- true ;
+ script.strategies <- strategies ;
end ;
- let spawned = script.tactical || script.provers <> [] in
+ let spawned = script.proverscript || script.provers <> [] in
begin
if spawned then do_list_scheduled goals ;
spawn_wp_proofs ~script goals ;
diff --git a/src/plugins/wp/wpContext.ml b/src/plugins/wp/wpContext.ml
index 1adc3cfd70d..1f62b573e51 100644
--- a/src/plugins/wp/wpContext.ml
+++ b/src/plugins/wp/wpContext.ml
@@ -490,10 +490,11 @@ module type Generator =
sig
type key
type data
- val get : key -> data
val mem : key -> bool
- val clear : unit -> unit
+ val get : key -> data
+ val set : key -> data -> unit
val remove : key -> unit
+ val clear : unit -> unit
end
module StaticGenerator(K : Key)(D : Data with type key = K.t) =
@@ -508,6 +509,7 @@ struct
type key = D.key
type data = D.data
let get = G.memoize D.compile
+ let set = G.define
let mem = G.mem
let clear = G.clear
let remove = G.remove
@@ -525,6 +527,7 @@ struct
type key = D.key
type data = D.data
let get = G.memoize D.compile
+ let set = G.define
let mem = G.mem
let clear = G.clear
let remove = G.remove
@@ -542,6 +545,7 @@ struct
type key = D.key
type data = D.data
let get = G.memoize (fun k -> D.compile k (G.id ~basename:(D.basename k) k))
+ let set = G.define
let mem = G.mem
let clear = G.clear
let remove = G.remove
@@ -559,6 +563,7 @@ struct
type key = D.key
type data = D.data
let get = G.memoize (fun k -> D.compile k (G.id ~basename:(D.basename k) k))
+ let set = G.define
let mem = G.mem
let clear = G.clear
let remove = G.remove
diff --git a/src/plugins/wp/wpContext.mli b/src/plugins/wp/wpContext.mli
index 17a3273679d..f466f40d00d 100644
--- a/src/plugins/wp/wpContext.mli
+++ b/src/plugins/wp/wpContext.mli
@@ -163,10 +163,11 @@ module type Generator =
sig
type key
type data
- val get : key -> data
val mem : key -> bool
- val clear : unit -> unit
+ val get : key -> data
+ val set : key -> data -> unit
val remove : key -> unit
+ val clear : unit -> unit
end
(** projectified, depend on the model, not serialized *)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 4d6a6a21edc..7a37701948b 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -720,14 +720,14 @@ module ScriptMode = String
(struct
let option_name = "-wp-script"
let arg_name = "mode"
- let default = "default"
+ let default = ""
let help =
"WP mode for managing scripts and proof strategies:\n\
- - 'batch': replay from existing scripts (default for script prover)\n\
- - 'update': replay and update scripts (default for tip prover)\n\
- - 'init': replay from scratch and save scripts\n\
- - 'dry': replay from scratch, no script update\n\
- "
+ - 'batch': proof scripts are reused but not updated (default for script prover)\n\
+ - 'update': proof scripts are reused and updated (default for tip prover)\n\
+ - 'init': proof scripts are generated from scratch and saved\n\
+ - 'dry': proof scripts are explored from scratch and not saved\n\
+ See also option -wp-cache-env."
end)
let () = Parameter_customize.set_group wp_prover
@@ -767,18 +767,7 @@ module Cache = String
- 'replay': update mode with no cache update\n\
- 'rebuild': always run provers and update cache\n\
- 'offline': use cache but never run provers\n\
- You can also use the environment variable FRAMAC_WP_CACHE instead."
- end)
-
-let () = Parameter_customize.set_group wp_prover
-module CacheEnv = False
- (struct
- let option_name = "-wp-cache-env"
- let help = "Gives environment variables precedence over command line\n\
- for cache management:\n\
- - FRAMAC_WP_CACHE overrides -wp-cache\n\
- - FRAMAC_WP_CACHEDIR overrides -wp-cache-dir\n\
- Disabled by default."
+ See also option -wp-cache-env."
end)
let () = Parameter_customize.set_group wp_prover
@@ -790,7 +779,19 @@ module CacheDir = String
let help =
"Specify global cache directory (no cleanup mode).\n\
By default, cache entries are stored in the WP session directory.\n\
- You can also use the environment variable FRAMAC_WP_CACHEDIR instead."
+ See also option -wp-cache-env."
+ end)
+
+let () = Parameter_customize.set_group wp_prover
+module CacheEnv = False
+ (struct
+ let option_name = "-wp-cache-env"
+ let help = "Gives environment variables precedence over command line\n\
+ for cache management:\n\
+ - FRAMAC_WP_SCRIPT overrides -wp-script\n\
+ - FRAMAC_WP_CACHE overrides -wp-cache\n\
+ - FRAMAC_WP_CACHEDIR overrides -wp-cache-dir\n\
+ Disabled by default."
end)
let () = Parameter_customize.set_group wp_prover
--
GitLab