Commit 46ad0e65 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch '740-wp-redefinition-of-logic-warning' into 'master'

Resolve "[WP] Multiple definition of drivers"

Closes #740

See merge request frama-c/frama-c!2443
parents 9c21b773 c9f86431
......@@ -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
(* -------------------------------------------------------------------------- *)
......@@ -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 *)
......
......@@ -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
......
......@@ -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 *)
......
......@@ -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)
......
......@@ -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 :
......
......@@ -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
(* -------------------------------------------------------------------------- *)
......@@ -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
......
......@@ -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
......
......@@ -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 =
......
......@@ -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 =
......
......@@ -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
......
......@@ -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) =