diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 6bd4c09e5beff8bddfe10223d583621181e647ea..49b3adf9b90b65dbe542d7b4b9e58ca91bb59925 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1543,6 +1543,8 @@ src/plugins/wp/Vset.ml: CEA_WP
src/plugins/wp/Vset.mli: CEA_WP
src/plugins/wp/Warning.ml: CEA_WP
src/plugins/wp/Warning.mli: CEA_WP
+src/plugins/wp/Why3Provers.ml: CEA_WP
+src/plugins/wp/Why3Provers.mli: CEA_WP
src/plugins/wp/Wp.mli: .ignore
src/plugins/wp/WpTac.ml: CEA_WP
src/plugins/wp/WpTac.mli: CEA_WP
diff --git a/src/plugins/wp/GuiConfig.ml b/src/plugins/wp/GuiConfig.ml
index 349477b535176e375105087936f23b1e3a5e1aa0..7974c19d95c5687637e2efec6d721f0dde723458 100644
--- a/src/plugins/wp/GuiConfig.ml
+++ b/src/plugins/wp/GuiConfig.ml
@@ -62,7 +62,7 @@ class enabled key =
let cmdline = Wp_parameters.Provers.get () in
let selection = List.fold_left
(fun acc e ->
- match VCS.Why3_prover.find_opt e with
+ match Why3Provers.find_opt e with
| None-> acc
| Some p -> Why3.Whyconf.Sprover.add p acc)
settings cmdline
@@ -97,7 +97,7 @@ class dp_chooser
Why3.Whyconf.Mprover.find dp selected
method private entry dp =
- let text = VCS.Why3_prover.title dp in
+ let text = Why3Provers.title dp in
let sw = new Widget.switch () in
let lb = new Widget.label ~align:`Left ~text () in
sw#set (self#lookup dp) ;
@@ -119,7 +119,7 @@ class dp_chooser
method private detect () =
begin
- self#configure (VCS.Why3_prover.provers_set ());
+ self#configure (Why3Provers.provers_set ());
end
method private apply () =
@@ -131,7 +131,7 @@ class dp_chooser
selected)
method run () =
- let dps = VCS.Why3_prover.provers_set () in
+ let dps = Why3Provers.provers_set () in
let sel = enabled#get in
selected <- Why3.Whyconf.Mprover.merge
(fun _ avail enab ->
@@ -163,16 +163,16 @@ type mprover =
| NONE
| ERGO
| COQ
- | WHY of VCS.Why3_prover.t
+ | WHY of Why3Provers.t
class dp_button () =
let render = function
| NONE -> "(none)"
| ERGO -> "Alt-Ergo (native)"
| COQ -> "Coq (native)"
- | WHY p when VCS.Why3_prover.has_shortcut p "alt-ergo" ->
+ | WHY p when Why3Provers.has_shortcut p "alt-ergo" ->
"Alt-Ergo (why3)"
- | WHY dp -> VCS.Why3_prover.title dp in
+ | WHY dp -> Why3Provers.title dp in
let select = function
| ERGO -> VCS.NativeAltErgo
| COQ -> VCS.NativeCoq
@@ -186,7 +186,7 @@ class dp_button () =
| Some (VCS.NativeAltErgo|VCS.Tactical) -> ERGO
| Some VCS.NativeCoq -> COQ
| Some (VCS.Why3 p) ->
- if Why3.Whyconf.Sprover.mem p (VCS.Why3_prover.provers_set ())
+ if Why3.Whyconf.Sprover.mem p (Why3Provers.provers_set ())
then WHY p
else import others
in
@@ -202,7 +202,7 @@ class dp_button () =
method update () =
(* called in polling mode *)
begin
- let avl = VCS.Why3_prover.provers_set () in
+ let avl = Why3Provers.provers_set () in
if Why3.Whyconf.Sprover.equal avl dps then
begin
dps <- avl ;
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index e44b38377560709a5fc5c40d21ddbe01c7b34970..700675e62b85cd73ce33bf43d4dad80af0525a23 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -62,6 +62,7 @@ PLUGIN_CMO:= \
rformat wprop \
wp_parameters wp_error \
dyncall ctypes clabels \
+ Why3Provers \
Context Warning MemoryContext wpContext \
LogicUsage RefUsage \
cil2cfg normAtLabels wpPropId mcfg \
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 076226d70929e4206bc32dfcfd0eb3b254b1fcae..f9fb84507f5285bd8024f254723954a6a62597e3 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -33,8 +33,6 @@ let option_import = LogicBuiltins.create_option
(fun ~driver_dir:_ x -> x)
"why3" "import"
-let config = VCS.why3_config
-
module Env = WpContext.Index(struct
include Datatype.Unit
type key = unit
@@ -43,7 +41,7 @@ module Env = WpContext.Index(struct
let get_why3_env = Env.memoize
begin fun () ->
- let config = Lazy.force config in
+ let config = Why3Provers.config () in
let main = Why3.Whyconf.get_main config in
let ld =
(WpContext.directory ())::
@@ -71,6 +69,9 @@ type convert = {
let specific_equalities: Lang.For_export.specific_equality list ref =
ref [Vlist.specialize_eq_list]
+let add_specific_equality ~for_tau ~mk_new_eq =
+ specific_equalities := { for_tau; mk_new_eq }::!specific_equalities
+
(** get symbols *)
let get_ls ~cnv ~f ~l ~p =
@@ -937,10 +938,13 @@ class visitor (ctx:context) c =
end
+(* -------------------------------------------------------------------------- *)
+(* --- Goal Compilation --- *)
+(* -------------------------------------------------------------------------- *)
let goal_id = (Why3.Decl.create_prsymbol (Why3.Ident.id_fresh "wp_goal"))
-let why3_of_qed ~id ~title ~name ?axioms t =
+let prove_goal ~id ~title ~name ?axioms t =
(* Format.printf "why3_of_qed start@."; *)
let goal = Definitions.cluster ~id ~title () in
let ctx = empty_context name in
@@ -961,17 +965,16 @@ let why3_of_qed ~id ~title ~name ?axioms t =
if Wp_parameters.has_print_generated () then begin
let th_uc_tmp = Why3.Theory.add_decl ~warn:false ctx.th decl in
let th_tmp = Why3.Theory.close_theory th_uc_tmp in
- Wp_parameters.debug ~dkey:Wp_parameters.cat_print_generated "%a" Why3.Pretty.print_theory th_tmp
+ Wp_parameters.debug ~dkey:Wp_parameters.cat_print_generated "%a"
+ Why3.Pretty.print_theory th_tmp
end;
th, decl
-(** Prover call *)
-
let prove_prop ?axioms ~pid ~prop =
let id = WpPropId.get_propid pid in
let title = Pretty_utils.to_string WpPropId.pretty pid in
let name = "WP" in
- let th, decl = why3_of_qed ?axioms ~id ~title ~name prop in
+ let th, decl = prove_goal ?axioms ~id ~title ~name prop in
let t = None in
let t = Why3.Task.use_export t th in
Why3.Task.add_decl t decl
@@ -992,21 +995,17 @@ let task_of_wpo wpo =
let axioms = Some(lemma.l_cluster,depends) in
prove_prop ~pid ~prop ?axioms
-let altergo_step_limit = Str.regexp "^Steps limit reached:"
+(* -------------------------------------------------------------------------- *)
+(* --- Prover Task --- *)
+(* -------------------------------------------------------------------------- *)
-let call_prover ~timeout ~steplimit prover wpo =
+let prover_task prover wpo =
let env = get_why3_env () in
let task = task_of_wpo wpo in
- let config = Lazy.force config in
+ let config = Why3Provers.config () in
let prover_config = Why3.Whyconf.get_prover_config config prover in
let drv = Why3.Whyconf.load_driver (Why3.Whyconf.get_main config)
env prover_config.driver prover_config.extra_drivers 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 steplimit;
- } in
let remove_for_prover =
if prover.prover_name = "Alt-Ergo"
then Filter_axioms.remove_for_altergo
@@ -1020,100 +1019,103 @@ let call_prover ~timeout ~steplimit prover wpo =
let task =
if prover.prover_name = "Coq"
then task
- else Why3.Trans.apply trans task in
- let task = Why3.Driver.prepare_task drv task in
- let file = Wpo.DISK.file_goal
- ~pid:wpo.Wpo.po_pid
- ~model:wpo.Wpo.po_model
- ~prover:(VCS.Why3 prover) in
- (* This printing is currently just for debugging *)
- let _ = Command.print_file file (fun fmt ->
- Why3.Driver.print_task_prepared drv fmt task
- ) in
- if Wp_parameters.Check.get ()
- then (** Why3 typed checked the task during its build *)
- Task.return VCS.checked
- else
- let steplimit = match steplimit with Some 0 -> None | _ -> steplimit in
- let command = Why3.Whyconf.get_complete_command prover_config
- ~with_steps:(steplimit<>None) in
- let call =
- Why3.Driver.prove_task_prepared ~command ~limit drv task in
- Wp_parameters.debug ~dkey
- "@[@[Why3 run prover %a with %i timeout %i steplimit@]@]@."
- Why3.Whyconf.print_prover prover
- (Why3.Opt.get_def (-1) timeout)
- (Why3.Opt.get_def (-1) steplimit);
- let ping _ (* why3 seems not to be able to kill a started prover *) =
- match Why3.Call_provers.query_call call with
- | NoUpdates
- | ProverStarted -> Task.Yield
- | InternalFailure exn ->
- let msg = Format.asprintf "%a" Why3.Exn_printer.exn_printer exn in
- Task.Return (Task.Result (VCS.failed msg))
- | ProverInterrupted ->
- Task.Return (Task.Result (VCS.failed "interrupted"))
- | ProverFinished pr ->
- let r = match pr.pr_answer with
- | Timeout -> VCS.timeout (int_of_float pr.pr_time)
- | Valid -> VCS.result ~time:pr.pr_time ~steps:pr.pr_steps VCS.Valid
- | Invalid -> VCS.result ~time:pr.pr_time ~steps:pr.pr_steps VCS.Invalid
- | OutOfMemory -> VCS.failed "out of memory"
- | StepLimitExceeded -> VCS.stepout
- | Unknown _ -> VCS.unknown
- | Failure s -> VCS.failed s
- | HighFailure ->
- let alt_ergo_hack =
- prover.prover_name = "Alt-Ergo" &&
- Str.string_match altergo_step_limit pr.pr_output 0
- in
- if alt_ergo_hack then VCS.stepout
- else VCS.failed "Unknown error"
- in
- Wp_parameters.debug ~dkey
- "@[@[Why3 result for %a:@] @[%a@] and @[%a@]@."
- Why3.Whyconf.print_prover prover
- (* why3 1.3 (Why3.Call_provers.print_prover_result ~json_model:false) pr *)
- (Why3.Call_provers.print_prover_result) pr
- VCS.pp_result r;
- Task.Return (Task.Result r)
- in
- Task.async ping
+ else Why3.Trans.apply trans task
+ in
+ drv , prover_config , Why3.Driver.prepare_task drv task
-let add_specific_equality ~for_tau ~mk_new_eq =
- specific_equalities := { for_tau; mk_new_eq }::!specific_equalities
+(* -------------------------------------------------------------------------- *)
+(* --- Prover Call --- *)
+(* -------------------------------------------------------------------------- *)
-let version = Why3.Config.version
+let altergo_step_limit = Str.regexp "^Steps limit reached:"
+
+let call_prover ~timeout ~steplimit drv prover prover_config 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 command = Why3.Whyconf.get_complete_command prover_config
+ ~with_steps:(steps<>None) in
+ let call =
+ Why3.Driver.prove_task_prepared ~command ~limit drv task in
+ Wp_parameters.debug ~dkey "Why3 run prover %a with %i timeout %i steps@."
+ Why3.Whyconf.print_prover prover
+ (Why3.Opt.get_def (-1) timeout)
+ (Why3.Opt.get_def (-1) steps);
+ let ping _ (* why3 seems not to be able to kill a started prover *) =
+ match Why3.Call_provers.query_call call with
+ | NoUpdates
+ | ProverStarted -> Task.Yield
+ | InternalFailure exn ->
+ let msg = Format.asprintf "%a" Why3.Exn_printer.exn_printer exn in
+ Task.Return (Task.Result (VCS.failed msg))
+ | ProverInterrupted ->
+ Task.Return (Task.Result (VCS.failed "interrupted"))
+ | ProverFinished pr ->
+ let r = match pr.pr_answer with
+ | Timeout -> VCS.timeout (int_of_float pr.pr_time)
+ | Valid -> VCS.result ~time:pr.pr_time ~steps:pr.pr_steps VCS.Valid
+ | Invalid -> VCS.result ~time:pr.pr_time ~steps:pr.pr_steps VCS.Invalid
+ | OutOfMemory -> VCS.failed "out of memory"
+ | StepLimitExceeded -> VCS.stepout
+ | Unknown _ -> VCS.unknown
+ | Failure s -> VCS.failed s
+ | HighFailure ->
+ let alt_ergo_hack =
+ prover.prover_name = "Alt-Ergo" &&
+ Str.string_match altergo_step_limit pr.pr_output 0
+ in
+ if alt_ergo_hack then VCS.stepout
+ else VCS.failed "Unknown error"
+ in
+ Wp_parameters.debug ~dkey
+ "@[@[Why3 result for %a:@] @[%a@] and @[%a@]@."
+ Why3.Whyconf.print_prover prover
+ (* why3 1.3 (Why3.Call_provers.print_prover_result ~json_model:false) pr *)
+ (Why3.Call_provers.print_prover_result) pr
+ VCS.pp_result r;
+ Task.Return (Task.Result r)
+ in
+ Task.async ping
+
+(* -------------------------------------------------------------------------- *)
+(* --- Prove WPO --- *)
+(* -------------------------------------------------------------------------- *)
let prove ?timeout ?steplimit ~prover wpo =
try
- let do_ () =
- if Wp_parameters.Generate.get ()
- then if Wp_parameters.Check.get ()
- then Task.return VCS.checked
- else Task.return VCS.no_result
- else call_prover ~timeout ~steplimit prover wpo
- in
- WpContext.on_context (Wpo.get_context wpo) do_ ()
+ WpContext.on_context (Wpo.get_context wpo)
+ begin fun () ->
+ if Wp_parameters.Generate.get ()
+ then if Wp_parameters.Check.get ()
+ then Task.return VCS.checked
+ else Task.return VCS.no_result
+ else
+ let drv , prover_config , task = prover_task prover wpo in
+ if Wp_parameters.Check.get ()
+ then
+ (* Why3 typed checked the task during its build *)
+ Task.return VCS.checked
+ else
+ let file = Wpo.DISK.file_goal
+ ~pid:wpo.Wpo.po_pid
+ ~model:wpo.Wpo.po_model
+ ~prover:(VCS.Why3 prover) in
+ (* This printing is currently just for debugging *)
+ let _ = Command.print_file file (fun fmt ->
+ Why3.Driver.print_task_prepared drv fmt task
+ ) in
+ let hash = Digest.file file |> Digest.to_hex in
+ Format.eprintf "[HASH] %s@." hash ;
+ call_prover ~timeout ~steplimit drv prover prover_config task
+ end ()
with exn ->
let bt = Printexc.get_raw_backtrace () in
Wp_parameters.fatal "Error in why3:%a@.%s@."
Why3.Exn_printer.exn_printer exn
(Printexc.raw_backtrace_to_string bt)
-let parse_why3_options =
- let todo = ref true in
- fun () ->
- if !todo then begin
- let args = Array.of_list ("why3"::Wp_parameters.WhyFlags.get ()) in
- begin try
- Arg.parse_argv ~current:(ref 0) args
- (Why3.Debug.Args.[desc_debug;desc_debug_all;desc_debug_list])
- (fun _ -> raise (Arg.Help "Unknown why3 option"))
- "Why3 options"
- with Arg.Bad s -> Wp_parameters.abort "%s" s
- end;
- ignore (Why3.Debug.Args.option_list ());
- Why3.Debug.Args.set_flags_selected ();
- todo := false
- end
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index 4325d11117e6c5920d61c9ebebf4bb594afa14f9..f2f10c93d0cd9de2519548f458ba64fd4c626b82 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -24,11 +24,8 @@ val add_specific_equality:
for_tau:(Lang.tau -> bool) ->
mk_new_eq:Lang.F.binop ->
unit
-(** equality used in the goal, simpler to prove than polymorphic equality *)
+(** Equality used in the goal, simpler to prove than polymorphic equality *)
-val version : string
-
-val prove : ?timeout:int -> ?steplimit:int -> prover:VCS.Why3_prover.t -> Wpo.t -> VCS.result Task.task
+val prove : ?timeout:int -> ?steplimit:int -> prover:Why3Provers.t ->
+ Wpo.t -> VCS.result Task.task
(** Return NoResult if it is already proved by Qed *)
-
-val parse_why3_options : unit -> unit
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 5118efccbcfd128a4172e3a9bd1cf7e1000d09b5..4f2bf8e0c4229dc6c183b016106126059b01b81b 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -21,7 +21,7 @@
(**************************************************************************)
(* -------------------------------------------------------------------------- *)
-(* --- Provers --- *)
+(* --- Prover Results --- *)
(* -------------------------------------------------------------------------- *)
let dkey_no_time_info = Wp_parameters.register_category "no-time-info"
@@ -29,72 +29,8 @@ let dkey_no_step_info = Wp_parameters.register_category "no-step-info"
let dkey_no_goals_info = Wp_parameters.register_category "no-goals-info"
let dkey_success_only = Wp_parameters.register_category "success-only"
-let why3_config =
- lazy begin
- try
- Why3.Whyconf.read_config None
- with exn ->
- Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn
- end
-
-module Why3_prover = struct
- type t = Why3.Whyconf.prover
-
- let find_opt : string -> t option = fun s ->
- try
- let config = Lazy.force why3_config in
- let filter = Why3.Whyconf.parse_filter_prover s in
- let filter = Why3.Whyconf.filter_prover_with_shortcut config filter in
- Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover)
- with
- | (Why3.Whyconf.ProverNotFound _ | Why3.Whyconf.ParseFilterProver _ | Why3.Whyconf.ProverAmbiguity _ ) ->
- None
-
- let find : ?donotfail:unit -> string -> t = fun ?donotfail s ->
- try
- try
- let config = Lazy.force why3_config in
- let filter = Why3.Whyconf.parse_filter_prover s in
- let filter = Why3.Whyconf.filter_prover_with_shortcut config filter in
- (Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover
- with
- | Why3.Whyconf.ProverNotFound _ as exn when donotfail <> None ->
- Wp_parameters.warning ~once:true "%a" Why3.Exn_printer.exn_printer exn;
- (** from Why3.Whyconf.parse_filter_prover *)
- let sl = Why3.Strings.rev_split ',' s in
- (* reverse order *)
- let prover_name, prover_version, prover_altern =
- match sl with
- | [name] -> name,"",""
- | [version;name] -> name,version,""
- | [altern;version;name] -> name,version,altern
- | _ -> raise (Why3.Whyconf.ParseFilterProver s) in
- { Why3.Whyconf.prover_name; Why3.Whyconf.prover_version; Why3.Whyconf.prover_altern }
- with
- | (Why3.Whyconf.ProverNotFound _ | Why3.Whyconf.ParseFilterProver _ | Why3.Whyconf.ProverAmbiguity _ ) as exn ->
- Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn
-
- let print : t -> string = Why3.Whyconf.prover_parseable_format
- let title : t -> string = fun p -> Pretty_utils.sfprintf "%a" Why3.Whyconf.print_prover p
- let compare : t -> t -> int = Why3.Whyconf.Prover.compare
- let get_config () : Why3.Whyconf.config = (Lazy.force why3_config)
- let provers () : t list =
- Why3.Whyconf.Mprover.keys (Why3.Whyconf.get_provers (get_config ()))
- let provers_set () : Why3.Whyconf.Sprover.t =
- Why3.Whyconf.Mprover.domain (Why3.Whyconf.get_provers (get_config ()))
- let is_available p =
- Why3.Whyconf.Mprover.mem p (Why3.Whyconf.get_provers (get_config ()))
-
- let has_shortcut p s =
- match Why3.Wstdlib.Mstr.find_opt s
- (Why3.Whyconf.get_prover_shortcuts (get_config ())) with
- | None -> false
- | Some p' -> Why3.Whyconf.Prover.equal p p'
-
-end
-
type prover =
- | Why3 of Why3_prover.t (* Prover via WHY *)
+ | Why3 of Why3Provers.t (* Prover via WHY *)
| NativeAltErgo (* Direct Alt-Ergo *)
| NativeCoq (* Direct Coq and Coqide *)
| Qed (* Qed Solver *)
@@ -114,7 +50,7 @@ let prover_of_name = function
| "" | "none" -> None
| "qed" | "Qed" -> Some Qed
| "coq" | "coqide" -> Some NativeCoq
- | "alt-ergo" | "altgr-ergo" -> Some (Why3 (Why3_prover.find "alt-ergo"))
+ | "alt-ergo" | "altgr-ergo" -> Some (Why3 (Why3Provers.find "alt-ergo"))
| "native:alt-ergo" | "native:altgr-ergo" -> Some NativeAltErgo
| "native:coq" | "native:coqide" -> Some NativeCoq
| "script" -> Some Tactical
@@ -125,18 +61,18 @@ let prover_of_name = function
| s ->
match Extlib.string_del_prefix "why3:" s with
| Some "" -> None
- | Some s' -> Some (Why3 (Why3_prover.find s'))
- | None -> Some (Why3 (Why3_prover.find s))
+ | Some s' -> Some (Why3 (Why3Provers.find s'))
+ | None -> Some (Why3 (Why3Provers.find s))
let name_of_prover = function
- | Why3 s -> "why3:" ^ (Why3_prover.print s)
+ | Why3 s -> "why3:" ^ (Why3Provers.print s)
| NativeAltErgo -> "alt-ergo"
| NativeCoq -> "coq"
| Qed -> "qed"
| Tactical -> "script"
let title_of_prover = function
- | Why3 s -> (Why3_prover.title s)
+ | Why3 s -> (Why3Provers.title s)
| NativeAltErgo -> "Alt-Ergo"
| NativeCoq -> "Coq"
| Qed -> "Qed"
@@ -162,7 +98,7 @@ let sanitize_why3 s =
Buffer.contents buffer
let filename_for_prover = function
- | Why3 s -> sanitize_why3 (Why3_prover.print s)
+ | Why3 s -> sanitize_why3 (Why3Provers.print s)
| NativeAltErgo -> "Alt-Ergo"
| NativeCoq -> "Coq"
| Qed -> "Qed"
@@ -203,16 +139,16 @@ let cmp_prover p q =
| NativeCoq , NativeCoq -> 0
| NativeCoq , _ -> (-1)
| _ , NativeCoq -> 1
- | Why3 p , Why3 q -> Why3_prover.compare p q
+ | Why3 p , Why3 q -> Why3Provers.compare p q
let pp_prover fmt = function
| NativeAltErgo -> Format.pp_print_string fmt "Alt-Ergo (Native)"
| NativeCoq -> Format.pp_print_string fmt "Coq (Native)"
| Why3 smt ->
if Wp_parameters.debug_atleast 1 then
- Format.fprintf fmt "Why:%s" (Why3_prover.print smt)
+ Format.fprintf fmt "Why:%s" (Why3Provers.print smt)
else
- Format.pp_print_string fmt (Why3_prover.title smt)
+ Format.pp_print_string fmt (Why3Provers.title smt)
| Qed -> Format.fprintf fmt "Qed"
| Tactical -> Format.pp_print_string fmt "Tactical"
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 2b696a3a725c937a51b9a766415c0ee08e580d2b..eaffd1a90b69d89de70440374d0332e9fb229f4a 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -26,37 +26,8 @@
(** {2 Prover} *)
-module Why3_prover: sig
- type t = Why3.Whyconf.prover
-
- val find: ?donotfail:unit -> string -> t
- (** Find the why3 prover with the given name.
- If it can't be found and donotfail is chosen, a
- prover with the given name and version is used instead
- Raises exception when the string doesn't corresponds to a prover filter
- *)
-
- val find_opt: string -> t option
- (** Try to find the why3 prover with the given name. *)
-
- val provers : unit -> t list
- val provers_set: unit -> Why3.Whyconf.Sprover.t
-
- val print : t -> string
- val title : t -> string
-
- val compare : t -> t -> int
-
- val has_shortcut : t -> string -> bool
- (** check if a prover has a given shortcut *)
-
- val get_config: unit -> Why3.Whyconf.config
-
- val is_available : t -> bool
-end
-
type prover =
- | Why3 of Why3_prover.t (* Prover via WHY *)
+ | Why3 of Why3Provers.t (* Prover via WHY *)
| NativeAltErgo (* Direct Alt-Ergo *)
| NativeCoq (* Direct Coq and Coqide *)
| Qed (* Qed Solver *)
@@ -103,7 +74,6 @@ type config = {
depth : int option ;
}
-
val current : unit -> config (** Current parameters *)
val default : config (** all None *)
@@ -164,7 +134,3 @@ val dkey_no_time_info: Wp_parameters.category
val dkey_no_step_info: Wp_parameters.category
val dkey_no_goals_info: Wp_parameters.category
val dkey_success_only: Wp_parameters.category
-
-(** {2 Why3} *)
-
-val why3_config: Why3.Whyconf.config Lazy.t
diff --git a/src/plugins/wp/Why3Provers.ml b/src/plugins/wp/Why3Provers.ml
new file mode 100644
index 0000000000000000000000000000000000000000..a5bd9951923d418610fcd6930d55295d13dd2b1f
--- /dev/null
+++ b/src/plugins/wp/Why3Provers.ml
@@ -0,0 +1,114 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Why3 Config & Provers --- *)
+(* -------------------------------------------------------------------------- *)
+
+let cfg = lazy
+ begin
+ try
+ Why3.Whyconf.read_config None
+ with exn ->
+ Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn
+ end
+
+let version = Why3.Config.version
+let config () = Lazy.force cfg
+
+let configure =
+ let todo = ref true in
+ begin fun () ->
+ if !todo then
+ begin
+ let args = Array.of_list ("why3"::Wp_parameters.WhyFlags.get ()) in
+ begin try
+ Arg.parse_argv ~current:(ref 0) args
+ (Why3.Debug.Args.[desc_debug;desc_debug_all;desc_debug_list])
+ (fun _ -> raise (Arg.Help "Unknown why3 option"))
+ "Why3 options"
+ with Arg.Bad s -> Wp_parameters.abort "%s" s
+ end;
+ ignore (Why3.Debug.Args.option_list ());
+ Why3.Debug.Args.set_flags_selected ();
+ todo := false
+ end
+ end
+
+type t = Why3.Whyconf.prover
+
+let find_opt s =
+ try
+ let config = Lazy.force cfg in
+ let filter = Why3.Whyconf.parse_filter_prover s in
+ let filter = Why3.Whyconf.filter_prover_with_shortcut config filter in
+ Some ((Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover)
+ with
+ | Why3.Whyconf.ProverNotFound _
+ | Why3.Whyconf.ParseFilterProver _
+ | Why3.Whyconf.ProverAmbiguity _ ->
+ None
+
+let find ?donotfail s =
+ try
+ try
+ let config = Lazy.force cfg in
+ let filter = Why3.Whyconf.parse_filter_prover s in
+ let filter = Why3.Whyconf.filter_prover_with_shortcut config filter in
+ (Why3.Whyconf.filter_one_prover config filter).Why3.Whyconf.prover
+ with
+ | Why3.Whyconf.ProverNotFound _ as exn when donotfail <> None ->
+ Wp_parameters.warning ~once:true "%a" Why3.Exn_printer.exn_printer exn;
+ (** from Why3.Whyconf.parse_filter_prover *)
+ let sl = Why3.Strings.rev_split ',' s in
+ (* reverse order *)
+ let prover_name, prover_version, prover_altern =
+ match sl with
+ | [name] -> name,"",""
+ | [version;name] -> name,version,""
+ | [altern;version;name] -> name,version,altern
+ | _ -> raise (Why3.Whyconf.ParseFilterProver s) in
+ { Why3.Whyconf.prover_name; Why3.Whyconf.prover_version; Why3.Whyconf.prover_altern }
+ with
+ | ( Why3.Whyconf.ProverNotFound _
+ | Why3.Whyconf.ParseFilterProver _
+ | Why3.Whyconf.ProverAmbiguity _ ) as exn ->
+ Wp_parameters.abort "%a" Why3.Exn_printer.exn_printer exn
+
+let print = Why3.Whyconf.prover_parseable_format
+let title p = Pretty_utils.sfprintf "%a" Why3.Whyconf.print_prover p
+let compare = Why3.Whyconf.Prover.compare
+
+let provers () =
+ Why3.Whyconf.Mprover.keys (Why3.Whyconf.get_provers (config ()))
+
+let provers_set () : Why3.Whyconf.Sprover.t =
+ Why3.Whyconf.Mprover.domain (Why3.Whyconf.get_provers (config ()))
+
+let is_available p =
+ Why3.Whyconf.Mprover.mem p (Why3.Whyconf.get_provers (config ()))
+
+let has_shortcut p s =
+ match Why3.Wstdlib.Mstr.find_opt s
+ (Why3.Whyconf.get_prover_shortcuts (config ())) with
+ | None -> false
+ | Some p' -> Why3.Whyconf.Prover.equal p p'
diff --git a/src/plugins/wp/Why3Provers.mli b/src/plugins/wp/Why3Provers.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a68eeb567d8caab7089bd8d82af71bfbfb7c1a25
--- /dev/null
+++ b/src/plugins/wp/Why3Provers.mli
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val version : string
+val config : unit -> Why3.Whyconf.config
+val configure : unit -> unit
+
+type t = Why3.Whyconf.prover
+
+val find_opt : string -> t option
+val find : ?donotfail:unit -> string -> t
+
+val print : t -> string
+val title : t -> string
+val compare : t -> t -> int
+
+val provers : unit -> t list
+val provers_set : unit -> Why3.Whyconf.Sprover.t
+val is_available : t -> bool
+val has_shortcut : t -> string -> bool
+
+(**************************************************************************)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 8babaed7338b4a43534c9bec6e54fdb475af7b5b..5e271cc24eeffad6ba140cb194f5645cb083667c 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -836,16 +836,16 @@ let () = Cmdline.run_after_setting_files
if Wp_parameters.has_dkey dkey_shell then
Log.print_on_output pp_wp_parameters)
-let () = Cmdline.run_after_configuring_stage ProverWhy3.parse_why3_options
+let () = Cmdline.run_after_configuring_stage Why3Provers.configure
let do_prover_detect () =
if not !Config.is_gui && Wp_parameters.Detect.get () then
- let provers = VCS.Why3_prover.provers () in
+ let provers = Why3Provers.provers () in
if provers = [] then
Wp_parameters.result "No Why3 provers detected."
else
let open Why3.Whyconf in
- let shortcuts = get_prover_shortcuts (VCS.Why3_prover.get_config ()) in
+ let shortcuts = get_prover_shortcuts (Why3Provers.config ()) in
List.iter
(fun p ->
Wp_parameters.result "Prover %10s %-10s %s [%t%a]"