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/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index d19bacb5bd4c9800a65005833298362e9fdc30fd..17a55fcf05e666baabab4a36fb712cdfedfea96a 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1198,34 +1198,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,14 +1219,48 @@ 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 ~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 call = Why3.Driver.prove_task_prepared ~command ~limit driver task in
+ call_prover_task ~timeout ~steps prover call
(* -------------------------------------------------------------------------- *)
(* --- Prove 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 ?timeout ?steplimit ~prover wpo () =
try
(* Always generate common task *)
@@ -1259,12 +1270,14 @@ 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
+ Cache.get_result
+ ~digest:(digest wpo drv)
+ ~runner:(batch pconf drv)
+ ~timeout ~steplimit prover task
with exn ->
if Wp_parameters.has_dkey dkey_api then
Wp_parameters.fatal "[Why3 Error] %a@\n%s"
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'
+
+(* -------------------------------------------------------------------------- *)