diff --git a/src/plugins/wp/Cfloat.ml b/src/plugins/wp/Cfloat.ml
index 460b93f8db9c6b8c13154c5d6e4ec98c455d4322..92e87357c4e43c2c67adbd85fdf72b232e04760b 100644
--- a/src/plugins/wp/Cfloat.ml
+++ b/src/plugins/wp/Cfloat.ml
@@ -71,6 +71,14 @@ let tau_of_float f =
| Real -> Logic.Real
| Float -> ftau f
+let float_name = function
+ | Float32 -> "float"
+ | Float64 -> "double"
+
+let model_name = function
+ | Float -> "Float"
+ | Real -> "Real"
+
(* -------------------------------------------------------------------------- *)
(* --- Operators --- *)
(* -------------------------------------------------------------------------- *)
@@ -90,17 +98,17 @@ type op =
[@@@ warning "-32"]
let op_name = function
- | LT -> "flt"
- | EQ -> "feq"
- | LE -> "fle"
- | NE -> "fne"
- | NEG -> "fneg"
- | ADD -> "fadd"
- | MUL -> "fmul"
- | DIV -> "fdiv"
- | REAL -> "freal"
- | ROUND -> "fround"
- | EXACT -> "fexact"
+ | LT -> "lt"
+ | EQ -> "eq"
+ | LE -> "le"
+ | NE -> "ne"
+ | NEG -> "neg"
+ | ADD -> "add"
+ | MUL -> "mul"
+ | DIV -> "div"
+ | REAL -> "of"
+ | ROUND -> "to"
+ | EXACT -> "exact"
[@@@ warning "+32"]
(* -------------------------------------------------------------------------- *)
@@ -115,6 +123,7 @@ module REGISTRY = WpContext.Static
include Lang.Fun
end)
+
let find = REGISTRY.find
let () = Context.register
@@ -288,71 +297,84 @@ let compute_real op xs =
| NE , [ x ; y ] -> F.e_neq x y
| _ -> raise Not_found
-let compute op ulp xs =
- match Context.get model with
- | Real -> compute_real op xs
- | Float -> compute_float op ulp xs
+let return_type ft = function
+ | REAL -> Logic.Real
+ | _ -> ftau ft
+
+module Compute = WpContext.StaticGenerator
+ (struct
+ type t = model * c_float * op
+
+ let compare = Pervasives.compare
+
+ let pretty fmt (m, ft, op) =
+ Format.fprintf fmt "%s_%a_%s" (model_name m) pp_suffix ft (op_name op)
+ end)
+ (struct
+ let name = "Wp.Cfloat.Compute"
+ type key = model * c_float * op
+ type data = lfun * (term list -> term)
+
+ let compile (m, ft, op) =
+ let impl = match m with
+ | Real -> compute_real op
+ | Float -> compute_float op ft
+ in
+ let name = op_name op in
+ let phi = match op with
+ | LT | EQ | LE | NE ->
+ let prop = Pretty_utils.sfprintf "%s_%a" name pp_suffix ft in
+ let bool = Pretty_utils.sfprintf "%s_%ab" name pp_suffix ft in
+ extern_p ~library ~bool ~prop ()
+ | _ ->
+ let result = return_type ft op in
+ extern_f ~library ~result "%s_%a" name pp_suffix ft
+ in
+ Lang.F.set_builtin phi impl ;
+ REGISTRY.define phi (op, ft) ;
+ (phi, impl)
+ end)
(* -------------------------------------------------------------------------- *)
(* --- Operations --- *)
(* -------------------------------------------------------------------------- *)
-let make_fun_float ?result name op ft =
- let result = match result with None -> ftau ft | Some r -> r in
- let phi = extern_f ~library ~result "%s_%a" name pp_suffix ft in
- Lang.F.set_builtin phi (compute op ft) ;
- REGISTRY.define phi (op,ft) ; phi
-
-let make_pred_float name op ft =
- let prop = Pretty_utils.sfprintf "%s_%a" name pp_suffix ft in
- let bool = Pretty_utils.sfprintf "%s_%ab" name pp_suffix ft in
- let phi = extern_p ~library ~bool ~prop () in
- Lang.F.set_builtin phi (compute op ft) ;
- REGISTRY.define phi (op,ft) ; phi
-
-let f_memo = Ctypes.f_memo
-
-let real_of_flt = f_memo (make_fun_float ~result:Logic.Real "of" REAL)
-let flt_of_real = f_memo (make_fun_float "to" ROUND)
-let flt_add = f_memo (make_fun_float "add" ADD)
-let flt_mul = f_memo (make_fun_float "mul" MUL)
-let flt_div = f_memo (make_fun_float "div" DIV)
-let flt_neg = f_memo (make_fun_float "neg" NEG)
-
-let flt_lt = f_memo (make_pred_float "lt" LT)
-let flt_eq = f_memo (make_pred_float "eq" EQ)
-let flt_le = f_memo (make_pred_float "le" LE)
-let flt_neq = f_memo (make_pred_float "ne" NE)
+let flt_eq ft = Compute.get (Context.get model, ft, EQ) |> fst
+let flt_neq ft = Compute.get (Context.get model, ft, NE) |> fst
+let flt_le ft = Compute.get (Context.get model, ft, LE) |> fst
+let flt_lt ft = Compute.get (Context.get model, ft, LT) |> fst
+let flt_neg ft = Compute.get (Context.get model, ft, NEG) |> fst
+let flt_add ft = Compute.get (Context.get model, ft, ADD) |> fst
+let flt_mul ft = Compute.get (Context.get model, ft, MUL) |> fst
+let flt_div ft = Compute.get (Context.get model, ft, DIV) |> fst
+let flt_of_real ft = Compute.get (Context.get model, ft, ROUND) |> fst
+let real_of_flt ft = Compute.get (Context.get model, ft, REAL) |> fst
+
(* -------------------------------------------------------------------------- *)
(* --- Builtins --- *)
(* -------------------------------------------------------------------------- *)
-let register_builtin_comparison suffix ft =
+let make_hack ?(converse=false) ft op xs =
+ let phi, impl = Compute.get ((Context.get model), ft, op) in
+ let xs = (if converse then List.rev xs else xs) in
+ try impl xs with Not_found -> F.e_fun phi xs
+
+let register_builtin ft =
begin
- let open Qed.Logic in
- let params = [Sdata;Sdata] in
- let sort = Sprop in
- let gt = generated_f ~params ~sort "\\gt_%s" suffix in
- let ge = generated_f ~params ~sort "\\ge_%s" suffix in
- let open LogicBuiltins in
- let signature = [F ft;F ft] in
- add_builtin ("\\eq_" ^ suffix) signature (flt_eq ft) ;
- add_builtin ("\\ne_" ^ suffix) signature (flt_neq ft) ;
- add_builtin ("\\lt_" ^ suffix) signature (flt_lt ft) ;
- add_builtin ("\\le_" ^ suffix) signature (flt_le ft) ;
- add_builtin ("\\gt_" ^ suffix) signature gt ;
- add_builtin ("\\ge_" ^ suffix) signature ge ;
- let converse phi x y = e_fun phi [y;x] in
- Lang.F.set_builtin_2 gt (converse (flt_lt ft)) ;
- Lang.F.set_builtin_2 ge (converse (flt_le ft)) ;
+ let suffix = float_name ft in
+ LogicBuiltins.hack ("\\eq_" ^ suffix) (make_hack ft EQ) ;
+ LogicBuiltins.hack ("\\ne_" ^ suffix) (make_hack ft NE) ;
+ LogicBuiltins.hack ("\\lt_" ^ suffix) (make_hack ~converse:false ft LT) ;
+ LogicBuiltins.hack ("\\gt_" ^ suffix) (make_hack ~converse:true ft LT) ;
+ LogicBuiltins.hack ("\\le_" ^ suffix) (make_hack ~converse:false ft LE) ;
+ LogicBuiltins.hack ("\\ge_" ^ suffix) (make_hack ~converse:true ft LE)
end
-let () =
- Context.register
+let () = Context.register
begin fun () ->
- register_builtin_comparison "float" Float32 ;
- register_builtin_comparison "double" Float64 ;
+ register_builtin Float32 ;
+ register_builtin Float64 ;
end
(* -------------------------------------------------------------------------- *)
@@ -360,17 +382,14 @@ let () =
(* -------------------------------------------------------------------------- *)
let () =
- Context.register
- begin fun () ->
- let open LogicBuiltins in
- let register_builtin ft =
- add_builtin "\\model" [F ft] (f_model ft) ;
- add_builtin "\\delta" [F ft] (f_delta ft) ;
- add_builtin "\\epsilon" [F ft] (f_epsilon ft) ;
- in
- register_builtin Float32 ;
- register_builtin Float64 ;
- end
+ let open LogicBuiltins in
+ let register_builtin ft =
+ add_builtin "\\model" [F ft] (f_model ft) ;
+ add_builtin "\\delta" [F ft] (f_delta ft) ;
+ add_builtin "\\epsilon" [F ft] (f_epsilon ft) ;
+ in
+ register_builtin Float32 ;
+ register_builtin Float64
(* -------------------------------------------------------------------------- *)
(* --- Conversion Symbols --- *)
@@ -424,8 +443,13 @@ let fneq = fcmp p_neq flt_neq
let configure m =
begin
- Context.set model m ;
- Context.set Lang.floats tau_of_float ;
+ let orig_model = Context.push model m in
+ let orig_floats = Context.push Lang.floats tau_of_float in
+ let rollback () =
+ Context.pop model orig_model ;
+ Context.pop Lang.floats orig_floats
+ in
+ rollback
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cfloat.mli b/src/plugins/wp/Cfloat.mli
index debed76a027159ea32212882699c09fae9de164d..0af6b9e436ae038e73c34e0cbc2b3bbc7c606855 100644
--- a/src/plugins/wp/Cfloat.mli
+++ b/src/plugins/wp/Cfloat.mli
@@ -35,7 +35,7 @@ val t32 : tau
val t64 : tau
type model = Real | Float
-val configure : model -> unit
+val configure : model -> WpContext.rollback
val ftau : c_float -> tau (** model independant *)
val tau_of_float : c_float -> tau (** with respect to model *)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 0e95b83d5e45c7ab5a0920eff8dcec20485c150a..4329cdf81c5fce669fa0ec6703086734b6b890f4 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -408,7 +408,9 @@ let () =
let model = Context.create "Cint.model"
let current () = Context.get model
-let configure = Context.set model
+let configure m =
+ let orig_model = Context.push model m in
+ (fun () -> Context.pop model orig_model)
let to_integer a = a
let of_integer i a = convert i a
diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli
index 2b830151f316fe3a125aa8db73c3f1e4aae93416..258f3f32cd7f5c13c84486a7d3812517057b188b 100644
--- a/src/plugins/wp/Cint.mli
+++ b/src/plugins/wp/Cint.mli
@@ -38,7 +38,7 @@ val to_cint : lfun -> c_int (** Raises [Not_found] if not. *)
val is_cint : lfun -> c_int (** Raises [Not_found] if not. *)
type model = Natural | Machine
-val configure : model -> unit
+val configure : model -> WpContext.rollback
val current : unit -> model
val range : c_int -> term -> pred (** Dependent on model *)
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index f0c8ce79b900acaa5eeca69ce0fc64a75fb0bbb8..5b9e54a4366c72f7bb67221e95d61d953d510e98 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -274,15 +274,27 @@ let configure_mheap = function
| Hoare -> MemEmpty.configure ()
| ZeroAlias -> MemZeroAlias.configure ()
| Region -> MemRegion.configure ()
- | Typed p -> MemTyped.configure () ; Context.set MemTyped.pointer p
-
-let configure (s:setup) (d:driver) () =
- begin
- configure_mheap s.mheap ;
- Cint.configure s.cint ;
- Cfloat.configure s.cfloat ;
- Context.set LogicBuiltins.driver d ;
- end
+ | Typed p ->
+ let rollback_memtyped = MemTyped.configure () in
+ let orig_memtyped_pointer = Context.push MemTyped.pointer p in
+ let rollback () =
+ rollback_memtyped () ;
+ Context.pop MemTyped.pointer orig_memtyped_pointer
+ in
+ rollback
+
+let configure_driver setup driver () =
+ let rollback_mheap = configure_mheap setup.mheap in
+ let rollback_cint = Cint.configure setup.cint in
+ let rollback_cfloat = Cfloat.configure setup.cfloat in
+ let old_driver = Context.push LogicBuiltins.driver driver in
+ let rollback () =
+ Context.pop LogicBuiltins.driver old_driver ;
+ rollback_cfloat () ;
+ rollback_cint () ;
+ rollback_mheap ()
+ in
+ rollback
(* -------------------------------------------------------------------------- *)
(* --- Access --- *)
@@ -298,21 +310,21 @@ module COMPILERS = FCMap.Make
let instances = ref (COMPILERS.empty : WpContext.model COMPILERS.t)
-let instance (s:setup) (d:driver) =
- try COMPILERS.find (s,d) !instances
+let instance setup driver =
+ try COMPILERS.find (setup,driver) !instances
with Not_found ->
- let id,descr = describe s in
- let module CC = (val compiler s.mheap s.mvar) in
- let tuning = [configure s d] in
+ let id,descr = describe setup in
+ let module CC = (val compiler setup.mheap setup.mvar) in
+ let configure = configure_driver setup driver in
let hypotheses = CC.M.hypotheses in
let id,descr =
- if LogicBuiltins.is_default d then id,descr
+ if LogicBuiltins.is_default driver then id,descr
else
- ( id ^ "_" ^ LogicBuiltins.id d ,
- descr ^ " (Driver " ^ LogicBuiltins.descr d ^ ")" )
+ ( id ^ "_" ^ LogicBuiltins.id driver ,
+ descr ^ " (Driver " ^ LogicBuiltins.descr driver ^ ")" )
in
- let model = WpContext.register ~id ~descr ~tuning ~hypotheses () in
- instances := COMPILERS.add (s,d) model !instances ; model
+ let model = WpContext.register ~id ~descr ~configure ~hypotheses () in
+ instances := COMPILERS.add (setup,driver) model !instances ; model
let ident s = fst (describe s)
let descr s = snd (describe s)
diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index 973daad343f83e449867c99592f1d3719573a678..2505e3567eebdb6d1f37966026b069b6bed6b233 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -39,7 +39,7 @@ type driver = LogicBuiltins.driver
val ident : setup -> string
val descr : setup -> string
val compiler : mheap -> mvar -> (module Sigs.Compiler)
-val configure : setup -> driver -> WpContext.tuning
+val configure_driver : setup -> driver -> unit -> WpContext.rollback
val instance : setup -> driver -> WpContext.model
val default : setup (** ["Var,Typed,Nat,Real"] memory model. *)
val parse :
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index 8b72dbbf23638161d1ef492574243ce79d5b1a1e..f199e117bfbd5c6798256a6861fe57f91b220c01 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/src/plugins/wp/LogicBuiltins.ml
@@ -109,20 +109,28 @@ type driver = {
hdeps : (string, string list) Hashtbl.t;
hoptions :
(string (* library *) * string (* group *) * string (* name *), string list)
- Hashtbl.t
+ Hashtbl.t;
+ mutable locked: bool
}
+let lock driver = driver.locked <- true
+
let id d = d.driverid
let descr d = d.description
let is_default d = (d.driverid = "")
let compare d d' = String.compare d.driverid d'.driverid
let driver = Context.create "driver"
-let cdriver () = Context.get driver
+let cdriver_ro () = Context.get driver
+let cdriver_rw () =
+ let driver = Context.get driver in
+ if driver.locked then
+ Wp_parameters.failure "Attempt to modify locked: %s" driver.driverid ;
+ driver
let lookup_driver name kinds =
try
- let sigs = Hashtbl.find (cdriver ()).hlogic name in
+ let sigs = Hashtbl.find (cdriver_ro ()).hlogic name in
try List.assoc kinds sigs
with Not_found ->
Wp_parameters.feedback ~once:true
@@ -152,25 +160,26 @@ let lookup name kinds =
with Not_found -> lookup_driver name kinds
let register ?source name kinds link =
- let sigs = try Hashtbl.find (cdriver ()).hlogic name with Not_found -> [] in
+ let driver = cdriver_rw () in
+ let sigs = try Hashtbl.find driver.hlogic name with Not_found -> [] in
if List.exists (fun (s,_) -> s = kinds) sigs then
Wp_parameters.warning ?source "Redefinition of logic %s%a"
name pp_kinds kinds ;
let entry = (kinds,link) in
- Hashtbl.add (cdriver ()).hlogic name (entry::sigs)
+ Hashtbl.add driver.hlogic name (entry::sigs)
let iter_table f =
let items = ref [] in
Hashtbl.iter
(fun a sigs -> List.iter (fun (ks,lnk) -> items := (a,ks,lnk)::!items) sigs)
- (cdriver ()).hlogic ;
+ (cdriver_ro ()).hlogic ;
List.iter f (List.sort Transitioning.Stdlib.compare !items)
let iter_libs f =
let items = ref [] in
Hashtbl.iter
(fun a libs -> items := (a,libs) :: !items)
- (cdriver ()).hdeps ;
+ (cdriver_ro ()).hdeps ;
List.iter f (List.sort Transitioning.Stdlib.compare !items)
let dump () =
@@ -204,11 +213,11 @@ let constant name =
(* -------------------------------------------------------------------------- *)
let dependencies lib =
- Hashtbl.find (cdriver ()).hdeps lib
+ Hashtbl.find (cdriver_ro ()).hdeps lib
let add_library lib deps =
let others = try dependencies lib with Not_found -> [] in
- Hashtbl.add (cdriver ()).hdeps lib (others @ deps)
+ Hashtbl.add (cdriver_rw ()).hdeps lib (others @ deps)
let add_alias ~source name kinds ~alias () =
register ~source name kinds (lookup alias kinds)
@@ -255,17 +264,17 @@ let create_option ~sanitizer group name =
option
let get_option (group,name) ~library =
- try Hashtbl.find (cdriver ()).hoptions (library,group,name)
+ try Hashtbl.find (cdriver_ro ()).hoptions (library,group,name)
with Not_found -> []
let set_option ~driver_dir group name ~library value =
let value = sanitize ~driver_dir group name value in
- Hashtbl.replace (cdriver ()).hoptions (library,group,name) [value]
+ Hashtbl.replace (cdriver_rw ()).hoptions (library,group,name) [value]
let add_option ~driver_dir group name ~library value =
let value = sanitize ~driver_dir group name value in
let l = get_option (group,name) ~library in
- Hashtbl.replace (cdriver ()).hoptions (library,group,name) (l @ [value])
+ Hashtbl.replace (cdriver_rw ()).hoptions (library,group,name) (l @ [value])
(** Includes *)
@@ -278,7 +287,7 @@ let find_lib file =
let path = Printf.sprintf "%s/%s" dir file in
if Sys.file_exists path then path else lookup file dirs
in
- lookup file (cdriver ()).includes
+ lookup file (cdriver_ro ()).includes
(* -------------------------------------------------------------------------- *)
(* --- Implemented Builtins --- *)
@@ -291,6 +300,7 @@ let builtin_driver = {
hlogic = Hashtbl.create 131;
hdeps = Hashtbl.create 31;
hoptions = Hashtbl.create 131;
+ locked = false
}
let add_builtin name kinds lfun =
@@ -300,17 +310,21 @@ let add_builtin name kinds lfun =
else
Context.bind driver builtin_driver (register name kinds) phi
-let create ~id ?(descr=id) ?(includes=[]) () =
- {
+let new_driver ~id ?(base=builtin_driver)
+ ?(descr=id) ?(includes=[]) ?(configure=fun () -> ()) () =
+ lock base ;
+ let new_driver = {
driverid = id ;
description = descr ;
- includes = includes @ builtin_driver.includes ;
- hlogic = Hashtbl.copy builtin_driver.hlogic ;
- hdeps = Hashtbl.copy builtin_driver.hdeps ;
- hoptions = Hashtbl.copy builtin_driver.hoptions ;
- }
-
-let init ~id ?descr ?includes () =
- Context.set driver (create ~id ?descr ?includes ())
+ includes = includes @ base.includes ;
+ hlogic = Hashtbl.copy base.hlogic ;
+ hdeps = Hashtbl.copy base.hdeps ;
+ hoptions = Hashtbl.copy base.hoptions ;
+ locked = false
+ } in
+ let old = Context.push driver new_driver in
+ configure () ;
+ Context.pop driver old ;
+ new_driver
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/LogicBuiltins.mli b/src/plugins/wp/LogicBuiltins.mli
index f54c67fd51308b702dc208aa412e2c63797a4eaa..be33a15e43653386a1f1606f62664e17123cc722 100644
--- a/src/plugins/wp/LogicBuiltins.mli
+++ b/src/plugins/wp/LogicBuiltins.mli
@@ -44,11 +44,22 @@ val add_builtin : string -> kind list -> lfun -> unit
type driver
val driver: driver Context.value
-val create: id:string -> ?descr:string -> ?includes:string list -> unit -> driver
-(** Create a new driver. leave the context empty. *)
-
-val init: id:string -> ?descr:string -> ?includes:string list -> unit -> unit
-(** Reset the context to a newly created driver *)
+val new_driver:
+ id:string ->
+ ?base:driver ->
+ ?descr:string ->
+ ?includes:string list ->
+ ?configure:(unit -> unit) -> unit ->
+ driver
+(** Creates a configured driver from an existing one.
+ Default:
+ - base: builtin WP driver
+ - descr: id
+ - includes: []
+ - configure: No-Op
+ The configure is the only operation allowed to modify the content of the
+ newly created driver. Except during static initialization of builtin driver.
+*)
val id : driver -> string
val descr : driver -> string
diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index cf7d3dc174069393407c5a60dcbca667178d9fb0..3690798ab1bb2424a68a9dd7935a7be04d60f702 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -32,8 +32,13 @@ module Logic = Qed.Logic
let datatype = "MemEmpty"
let configure () =
begin
- Context.set Lang.pointer (fun _typ -> Logic.Int) ;
- Context.set Cvalues.null (p_equal e_zero) ;
+ let orig_pointer = Context.push Lang.pointer (fun _typ -> Logic.Int) in
+ let orig_null = Context.push Cvalues.null (p_equal e_zero) in
+ let rollback () =
+ Context.pop Lang.pointer orig_pointer ;
+ Context.pop Cvalues.null orig_null ;
+ in
+ rollback
end
let no_binder = { bind = fun _ f v -> f v }
let configure_ia _ = no_binder
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 14660db121ee6b83878b883344b8d5a1abbd7a4f..4e90766687443e8f45be82f7727d4b4804ffe93b 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -428,8 +428,13 @@ let datatype = "MemRegion"
let configure () =
begin
- Context.set Lang.pointer (fun _ -> t_index) ;
- Context.set Cvalues.null p_inull ;
+ let orig_pointer = Context.push Lang.pointer (fun _ -> t_index) in
+ let orig_null = Context.push Cvalues.null p_inull in
+ let rollback () =
+ Context.pop Lang.pointer orig_pointer ;
+ Context.pop Cvalues.null orig_null
+ in
+ rollback
end
let configure_ia =
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 3836f09578188ba6491eabebc2083514a7bab9d5..dbe87223516f4ef8abc44357443dcb5a77206b6f 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -45,8 +45,13 @@ let datatype = "MemTyped"
let hypotheses () = []
let configure () =
begin
- Context.set Lang.pointer (fun _ -> t_addr) ;
- Context.set Cvalues.null (p_equal a_null) ;
+ let orig_pointer = Context.push Lang.pointer (fun _ -> t_addr) in
+ let orig_null = Context.push Cvalues.null (p_equal a_null) in
+ let rollback () =
+ Context.pop Lang.pointer orig_pointer ;
+ Context.pop Cvalues.null orig_null ;
+ in
+ rollback
end
let configure_ia =
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index c88f4531a438160afc5b4b7377c13978f189b43e..db4853dd6212da21c37c5cad37c19174936fe7f9 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -36,8 +36,13 @@ let datatype = "MemZeroAlias"
let configure () =
begin
- Context.set Lang.pointer (fun _typ -> Logic.Int) ;
- Context.set Cvalues.null F.(p_equal e_zero) ;
+ let orig_pointer = Context.push Lang.pointer (fun _typ -> Logic.Int) in
+ let orig_null = Context.push Cvalues.null (p_equal e_zero) in
+ let rollback () =
+ Context.pop Lang.pointer orig_pointer ;
+ Context.pop Cvalues.null orig_null ;
+ in
+ rollback
end
let no_binder = { bind = fun _ f v -> f v }
let configure_ia _ = no_binder
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 1284425bd9855e200a6e4541ffd78759b50e8e25..fb61c74912305f205fde7bab54ac2f4a6d9f9521 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1012,8 +1012,7 @@ let task_of_wpo wpo =
(* --- Prover Task --- *)
(* -------------------------------------------------------------------------- *)
-let prover_task prover task =
- let env = get_why3_env () in
+let prover_task env prover task =
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)
@@ -1315,50 +1314,49 @@ let is_trivial (t : Why3.Task.task) =
let build_proof_task ?timeout ?steplimit ~prover wpo () =
try
- WpContext.on_context (Wpo.get_context wpo)
- begin fun () ->
- (* Always generate common task *)
- let task = task_of_wpo wpo in
- if Wp_parameters.Check.get ()
- then Task.return VCS.checked (* Why3 tasks are type-checked *)
- else
- if Wp_parameters.Generate.get ()
- then Task.return VCS.no_result (* Only generate *)
- else
- let drv , config , task = prover_task prover task in
- if is_trivial task then
- Task.return VCS.valid
- else
- let mode = get_mode () in
- match mode with
- | NoCache ->
- call_prover ~timeout ~steplimit drv prover config task
- | Offline ->
- let hash = task_hash wpo drv prover task in
- let result = get_cache_result ~mode hash |> VCS.cached in
- if VCS.is_verdict result then incr hits else incr miss ;
+ (* Always generate common task *)
+ let context = Wpo.get_context wpo in
+ let task = WpContext.on_context context task_of_wpo wpo in
+ if Wp_parameters.Check.get ()
+ then Task.return VCS.checked (* Why3 tasks are type-checked *)
+ else
+ if Wp_parameters.Generate.get ()
+ 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
+ if is_trivial task then
+ Task.return VCS.valid
+ else
+ let mode = get_mode () in
+ match mode with
+ | NoCache ->
+ call_prover ~timeout ~steplimit drv prover config task
+ | Offline ->
+ let hash = task_hash wpo drv prover task 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 result =
+ get_cache_result ~mode hash
+ |> promote ~timeout ~steplimit |> VCS.cached in
+ if VCS.is_verdict result
+ then
+ begin
+ incr hits ;
Task.return result
- | Update | Replay | Rebuild | Cleanup ->
- let hash = task_hash wpo drv prover task in
- let result =
- get_cache_result ~mode hash
- |> promote ~timeout ~steplimit |> VCS.cached in
- if VCS.is_verdict result
- then
- begin
- incr hits ;
- Task.return result
- end
- else
- Task.finally
- (call_prover ~timeout ~steplimit drv prover config task)
- begin function
- | Task.Result result when VCS.is_verdict result ->
- incr miss ;
- set_cache_result ~mode hash prover result
- | _ -> ()
- end
- end ()
+ end
+ else
+ Task.finally
+ (call_prover ~timeout ~steplimit drv prover config task)
+ begin function
+ | Task.Result result when VCS.is_verdict result ->
+ incr miss ;
+ set_cache_result ~mode hash prover result
+ | _ -> ()
+ end
with exn ->
if Wp_parameters.has_dkey dkey_api then
Wp_parameters.fatal "[Why3 Error] %a@\n%s"
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 43db54a110aea9a9706f602940bc2a49e035b56d..a4a3bf6cd92eea3ab0cbd1d2ee5370e31746a4e8 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -277,9 +277,9 @@ sig
(** {2 Model Definition} *)
- val configure : WpContext.tuning
+ val configure : unit -> WpContext.rollback
(** Initializers to be run before using the model.
- Typically sets {!Context} values. *)
+ Typically push {!Context} values and returns a function to rollback. *)
val configure_ia: automaton -> vertex binder
(** Given an automaton, return a vertex's binder.
diff --git a/src/plugins/wp/driver.mll b/src/plugins/wp/driver.mll
index b3b2b170b395aae98e54e08948b86fee35f03ffd..4db36e6113c93c4edffa184c3e6574d1c147c546 100644
--- a/src/plugins/wp/driver.mll
+++ b/src/plugins/wp/driver.mll
@@ -339,7 +339,7 @@ and bal = parse
| ACSLDEF -> failwith (Printf.sprintf "Symbol '%s' not found" op)
| HACK _ -> failwith (Printf.sprintf "Symbol '%s' hacked" op)
| LFUN lfun -> E_fun(lfun,[])
-
+
let rec op_link op input =
match token input with
| LINK _ | RECLINK _ ->
@@ -490,16 +490,15 @@ and bal = parse
let load_driver () =
let drivers = Wp_parameters.Drivers.get () in
begin try
- let driver = Hashtbl.find loaded drivers in
- Context.set LogicBuiltins.driver driver
+ Hashtbl.find loaded drivers
with Not_found ->
- let driver_basename file =
- let base = Filename.basename file in
- try Filename.chop_extension base
- with Invalid_argument _ -> base in
- let drvs = List.map driver_basename drivers in
+ let driver_basename file =
+ let base = Filename.basename file in
+ try Filename.chop_extension base
+ with Invalid_argument _ -> base in
+ let drvs = List.map driver_basename drivers in
let id = String.concat "_" drvs in
- let descr = String.concat "," drvs in
+ let descr = String.concat "," drvs in
let includes =
let directories =
try [Wp_parameters.Share.dir ~error:false ()]
@@ -513,20 +512,23 @@ and bal = parse
);
directories
in
- LogicBuiltins.init ~id ~descr ~includes () ;
- let drivers =
- List.map (fun file ->
- if Sys.file_exists file
- then Filepath.normalize file
- else LogicBuiltins.find_lib file)
- drivers in
- let default = Wp_parameters.Share.file ~error:true "wp.driver" in
- let feedback = Wp_parameters.Share.Dir_name.is_set () in
- let ontty = if feedback then `Message else `Transient in
- load_file ~ontty default;
- List.iter load_file drivers;
- Hashtbl.add loaded drivers (Context.get LogicBuiltins.driver);
- if Wp_parameters.has_dkey dkey_driver then LogicBuiltins.dump ()
- end ; Context.get LogicBuiltins.driver
+ let configure ()=
+ let drivers =
+ List.map (fun file ->
+ if Sys.file_exists file
+ then Filepath.normalize file
+ else LogicBuiltins.find_lib file)
+ drivers in
+ let default = Wp_parameters.Share.file ~error:true "wp.driver" in
+ let feedback = Wp_parameters.Share.Dir_name.is_set () in
+ let ontty = if feedback then `Message else `Transient in
+ load_file ~ontty default;
+ List.iter load_file drivers
+ in
+ let driver = LogicBuiltins.new_driver ~id ~descr ~includes ~configure () in
+ Hashtbl.add loaded drivers driver;
+ if Wp_parameters.has_dkey dkey_driver then LogicBuiltins.dump () ;
+ driver
+ end
}
diff --git a/src/plugins/wp/wpContext.ml b/src/plugins/wp/wpContext.ml
index c6459a5af4949559d41c32a9dcfc7b16ffc0f42e..fda8f5d01b34d395e7466ab48ec739bcbe1241ba 100644
--- a/src/plugins/wp/wpContext.ml
+++ b/src/plugins/wp/wpContext.ml
@@ -29,10 +29,10 @@ type model = {
descr : string ; (* Title of the Model (for pretty) *)
emitter : Emitter.t ;
hypotheses : hypotheses ;
- tuning : tuning list ;
+ configure : (unit -> rollback) ;
}
-and tuning = unit -> unit
+and rollback = (unit -> unit)
and scope = Global | Kf of Kernel_function.t
and hypotheses = unit -> MemoryContext.clause list
and context = model * scope
@@ -51,7 +51,7 @@ struct
let repr = {
id = "?model" ; descr = "?model" ;
emitter = Emitter.kernel ;
- tuning = [ fun () -> () ] ;
+ configure = (fun () -> (fun () -> ())) ;
hypotheses = nohyp ;
}
end
@@ -69,7 +69,8 @@ struct
end
-let register ~id ?(descr=id) ?(tuning=[]) ?(hypotheses=nohyp) () =
+let register ~id ?(descr=id) ~configure
+ ?(hypotheses=nohyp) () =
if MODELS.mem id then
Wp_parameters.fatal "Duplicate model '%s'" id ;
let emitter =
@@ -82,7 +83,7 @@ let register ~id ?(descr=id) ?(tuning=[]) ?(hypotheses=nohyp) () =
id = id ;
descr ;
emitter ;
- tuning ;
+ configure ;
hypotheses ;
} in
MODELS.add model ; model
@@ -124,21 +125,23 @@ end
let context : (string * context) Context.value = Context.create "WpContext"
-let configure (model,_) = List.iter (fun f -> f()) model.tuning
-let rollback = function None -> () | Some (_,ctxt) -> configure ctxt
+let configure (model,_) = model.configure ()
let on_context gamma f x =
let id = S.id gamma in
let current = Context.push context (id,gamma) in
+ let rollback = try configure gamma
+ with _ -> Kernel.fatal "Model configuration failed" in
+ Context.configure () ;
try
- Context.configure () ;
- configure gamma ;
let result = f x in
Context.pop context current ;
- rollback current ; result
+ rollback () ;
+ result
with err ->
Context.pop context current ;
- rollback current ; raise err
+ rollback () ;
+ raise err
let is_defined () = Context.defined context
let get_ident () = Context.get context |> fst
diff --git a/src/plugins/wp/wpContext.mli b/src/plugins/wp/wpContext.mli
index d118296a75ccfb444359add87addc6ba812cb83d..89859439533992c7d72b80f202373ea49fd05476 100644
--- a/src/plugins/wp/wpContext.mli
+++ b/src/plugins/wp/wpContext.mli
@@ -24,15 +24,22 @@
type model
type scope = Global | Kf of Kernel_function.t
-type tuning = (unit -> unit)
+type rollback = unit -> unit
type hypotheses = unit -> MemoryContext.clause list
val register :
id:string ->
?descr:string ->
- ?tuning:tuning list ->
+ configure:(unit -> rollback) ->
?hypotheses:hypotheses ->
unit -> model
+(** Model registration. The model is identified by [id] and described by
+ [descr] (that defaults to [id]). The [configure] function is called on
+ [WpContext.on_context] call, it must prepare and set the different
+ [Context.values] related to the model. It must return the function that
+ allows to rollback on the original state. The [hypotheses] function must
+ return the hypotheses made by the model.
+*)
val get_descr : model -> string
val get_emitter : model -> Emitter.t