diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index e88014be4f9ba107cf6e08cecf77bbd531802be6..6d7e0a97be49d98241f37be69baf4bc27c6355c0 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -618,7 +618,8 @@ module Value = struct
(** Type for a Value builtin function *)
- type builtin_sig =
+ type builtin_type = typ * typ list
+ type builtin =
state ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index fe390a2c327da09e22208efe9dafb753b104b519..df8e76225528cc8d6f61c8f76e41f1a2012d10d3 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -177,26 +177,31 @@ module Value : sig
exception Outside_builtin_possibilities
- (** Type for a Value builtin function *)
- type builtin_sig =
- (** Memory state at the beginning of the function *)
- state ->
- (** Args for the function: the expressions corresponding to the formals
- of the functions at the call site, the actual value of those formals,
- and a more precise view of those formals using offsetmaps (for eg.
- structs) *)
- (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
+ (* Type of a C function interpreted by a builtin:
+ return type and list of argument types. *)
+ type builtin_type = typ * typ list
+
+ (** Type for an Eva builtin function *)
+ type builtin =
+ (** Memory state at the beginning of the function *)
+ state ->
+ (** Args for the function: the expressions corresponding to the formals
+ of the functions at the call site, the actual value of those formals,
+ and a more precise view of those formals using offsetmaps (for eg.
+ structs) *)
+ (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
Value_types.call_result
- val register_builtin: (string -> ?replace:string -> builtin_sig -> unit) ref
- (** [!register_builtin name ?replace f] registers an abstract function [f]
- to use everytime a C function named [name] is called in the program.
- If [replace] is supplied and option [-val-builtins-auto] is active,
- calls to [replace] will also be substituted by the builtin.
- See also option [-val-builtin] *)
+ val register_builtin:
+ (string -> ?replace:string -> ?typ:builtin_type -> builtin -> unit) ref
+ (** [!register_builtin name ?replace ?typ f] registers an abstract function
+ [f] to use everytime a C function named [name] of type [typ] is called in
+ the program. If [replace] is supplied and option [-eva-builtins-auto] is
+ active, calls to [replace] will also be substituted by the builtin. See
+ also option [-eva-builtin] *)
- val registered_builtins: (unit -> (string * builtin_sig) list) ref
- (** Returns a list of the pairs (name, builtin_sig) registered via
+ val registered_builtins: (unit -> (string * builtin) list) ref
+ (** Returns a list of the pairs (name, builtin) registered via
[register_builtin].
@since Aluminium-20160501 *)
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index fb2479c5e3c896d33ad478cb4d07bd459e6354d1..55f7f29e6d3546c8ff5f8b4c5ea1083aef6ebf19 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -32,11 +32,11 @@ type use_builtin = Always | OnAuto
let table = Hashtbl.create 17
-let register_builtin name ?replace f =
- Hashtbl.replace table name (f, None, Always);
+let register_builtin name ?replace ?typ f =
+ Hashtbl.replace table name (f, typ, None, Always);
match replace with
| None -> ()
- | Some fname -> Hashtbl.replace table fname (f, Some name, OnAuto)
+ | Some fname -> Hashtbl.replace table fname (f, typ, Some name, OnAuto)
let () = Db.Value.register_builtin := register_builtin
@@ -45,7 +45,7 @@ let () = Db.Value.register_builtin := register_builtin
let registered_builtins () =
let l =
Hashtbl.fold
- (fun name (f, _, u) acc -> if u = Always then (name, f) :: acc else acc)
+ (fun name (f, _, _, u) acc -> if u = Always then (name, f) :: acc else acc)
table []
in
List.sort (fun (name1, _) (name2, _) -> String.compare name1 name2) l
@@ -54,7 +54,7 @@ let () = Db.Value.registered_builtins := registered_builtins
let builtin_names_and_replacements () =
let stand_alone, replacements =
- Hashtbl.fold (fun name (_, replaced_by, _) (acc1, acc2) ->
+ Hashtbl.fold (fun name (_, _, replaced_by, _) (acc1, acc2) ->
match replaced_by with
| None -> name :: acc1, acc2
| Some rep_by -> acc1, (name, rep_by) :: acc2
@@ -94,7 +94,7 @@ let () =
let mem_builtin name =
try
- let _, _, u = Hashtbl.find table name in
+ let _, _, _, u = Hashtbl.find table name in
u = Always
with Not_found -> false
@@ -109,20 +109,41 @@ let find_builtin_specification kf =
TODO: check that the specification is the frama-c libc specification? *)
if spec.spec_behavior <> [] then Some spec else None
+(* Returns [true] if the function [kf] is incompatible with the expected type
+ for a given builtin, which therefore cannot be applied. *)
+let inconsistent_builtin_typ kf = function
+ | None -> false (* No expected type provided with the builtin, no check. *)
+ | Some (expected_result, expected_args) ->
+ match Kernel_function.get_type kf with
+ | TFun (result, args, _, _) ->
+ let args = Cil.argsToList args in
+ Cil.need_cast result expected_result
+ || List.length args <> List.length expected_args
+ || List.exists2 (fun (_, t, _) u -> Cil.need_cast t u) args expected_args
+ | _ -> assert false
+
let find_builtin_override kf =
let name =
try Value_parameters.BuiltinsOverrides.find kf
with Not_found -> Kernel_function.get_name kf
in
try
- let f, _, u = Hashtbl.find table name in
- if u = Always || Value_parameters.BuiltinsAuto.get ()
+ let f, typ, _, u = Hashtbl.find table name in
+ if (u = Always || Value_parameters.BuiltinsAuto.get ())
+ && not (inconsistent_builtin_typ kf typ)
then Extlib.opt_map (fun s -> name, f, s) (find_builtin_specification kf)
else None
with Not_found -> None
-let warn_builtin_override bname kf =
+let warn_builtin_override bname kf expected_typ =
let source = fst (Kernel_function.get_location kf) in
+ if inconsistent_builtin_typ kf expected_typ
+ then
+ Value_parameters.warning ~source ~once:true
+ ~wkey:Value_parameters.wkey_builtins_override
+ "The builtin %s will not be used for function %a of incompatible type."
+ bname Kernel_function.pretty kf
+ else
if find_builtin_specification kf = None
then
Value_parameters.warning ~source ~once:true
@@ -147,15 +168,18 @@ let warn_builtin_override bname kf =
let warn_definitions_overridden_by_builtins () =
Value_parameters.BuiltinsOverrides.iter
- (fun (kf, name) -> warn_builtin_override (Extlib.the name) kf);
+ (fun (kf, name) ->
+ let name = Extlib.the name in
+ let (_, typ, _ , _) = Hashtbl.find table name in
+ warn_builtin_override name kf typ);
let autobuiltins = Value_parameters.BuiltinsAuto.get () in
Hashtbl.iter
- (fun name (_, _, u) ->
+ (fun name (_, typ, _, u) ->
if autobuiltins || u = Always
then
try
let kf = Globals.Functions.find_by_name name in
- warn_builtin_override name kf
+ warn_builtin_override name kf typ
with Not_found -> ())
table
@@ -182,7 +206,7 @@ let clobbered_set_from_ret state ret =
type call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
type result = Cvalue.Model.t * Locals_scoping.clobbered_set
-type builtin = Db.Value.builtin_sig
+type builtin = Db.Value.builtin
open Eval
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index 351bf9a11ddd32c6df1c74fbba77bbe45f1ecf6e..ebf302fd0d534aa60c398de0623406087182a8e4 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -25,9 +25,15 @@
exception Invalid_nb_of_args of int
-(** Register the given OCaml function as a builtin, that will be used
- instead of the Cil C function of the same name *)
-val register_builtin: string -> ?replace:string -> Db.Value.builtin_sig -> unit
+(** [register_builtin name ?replace ?typ f] registers the ocaml function [f]
+ as a builtin to be used instead of the C function of name [name].
+ If [replace] is provided, the builtin is also used instead of the C function
+ of name [replace], unless option -eva-builtin-auto is disabled.
+ If [typ] is provided, consistency between the expected [typ] and the type of
+ the C function is checked before using the builtin. *)
+val register_builtin:
+ string -> ?replace:string ->
+ ?typ:Db.Value.builtin_type -> Db.Value.builtin -> unit
(** [clobbered_set_from_ret state ret] can be used for functions that return
a pointer to where they have written some data. It returns all the bases
diff --git a/src/plugins/value/domains/cvalue/builtins_float.ml b/src/plugins/value/domains/cvalue/builtins_float.ml
index 458470bfbd5d68f8ad26fab04d9ce4939cdc3369..e636114ac354bbbc3cb8a27ab973fb38ecf73049 100644
--- a/src/plugins/value/domains/cvalue/builtins_float.ml
+++ b/src/plugins/value/domains/cvalue/builtins_float.ml
@@ -70,8 +70,9 @@ let arity2 fk caml_fun state actuals =
let register_arity2 c_name fk f =
let name = "Frama_C_" ^ c_name in
- Builtins.register_builtin name ~replace:c_name (arity2 fk f);
-;;
+ let t = Cil_types.TFloat (fk, []) in
+ let typ = t, [t; t] in
+ Builtins.register_builtin name ~replace:c_name ~typ (arity2 fk f)
let () =
let open Fval in
@@ -80,9 +81,7 @@ let () =
register_arity2 "pow" Cil_types.FDouble pow;
register_arity2 "powf" Cil_types.FFloat pow;
register_arity2 "fmod" Cil_types.FDouble fmod;
- register_arity2 "fmodf" Cil_types.FFloat fmod;
-;;
-
+ register_arity2 "fmodf" Cil_types.FFloat fmod
let arity1 name fk caml_fun state actuals =
match actuals with
@@ -114,8 +113,9 @@ let arity1 name fk caml_fun state actuals =
let register_arity1 c_name fk f =
let name = "Frama_C_" ^ c_name in
- Builtins.register_builtin name ~replace:c_name (arity1 name fk f);
-;;
+ let t = Cil_types.TFloat (fk, []) in
+ let typ = t, [t] in
+ Builtins.register_builtin name ~replace:c_name ~typ (arity1 name fk f)
let () =
let open Fval in
@@ -139,5 +139,4 @@ let () =
register_arity1 "floorf" Cil_types.FFloat floor;
register_arity1 "ceilf" Cil_types.FFloat ceil;
register_arity1 "truncf" Cil_types.FFloat trunc;
- register_arity1 "roundf" Cil_types.FFloat fround;
-;;
+ register_arity1 "roundf" Cil_types.FFloat fround
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index f85c0c466ee462a48d0fb8bbd14878a4890e4a62..7c83a1be556453e8c96e124ec7b3b6c12413ac7e 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -476,7 +476,7 @@ let alloc_by_stack_aux region stack prefix sizev state =
(* For each callstack, the first MallocPrecision.get() are precise fresh
distinct locations. The following allocations all return the same
base, first strong, then weak, and which is extended as needed. *)
-let alloc_by_stack ?(prefix="malloc") region ?returns_null : Db.Value.builtin_sig = fun state actuals->
+let alloc_by_stack ?(prefix="malloc") region ?returns_null : Db.Value.builtin = fun state actuals->
let stack = call_stack_no_wrappers () in
let sizev = match actuals with
| [_,size,_] -> size
@@ -501,7 +501,7 @@ let () = Builtins.register_builtin
(alloc_by_stack ~prefix:"alloca" Base.Alloca ~returns_null:false)
(* Equivalent to [alloc_by_stack], but for [calloc]. *)
-let calloc_by_stack : Db.Value.builtin_sig = fun state actuals ->
+let calloc_by_stack : Db.Value.builtin = fun state actuals ->
calloc_abstract (alloc_by_stack_aux Base.Malloc) state actuals
let () = Builtins.register_builtin