From 7460e1103d4d1756d35b7598d6ee3103c2c0944f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 17 Jan 2020 11:27:09 +0100
Subject: [PATCH] [Eva] Builtins: new function prepare_builtins called at the
start of the analysis.
This function links the kernel functions to their builtins for a given analysis.
Checks that the builtin replacing a function has a compatible type and a
specification. These requirements are not checked each time a builtin is used.
The type of a builtin is now a function "unit -> typ" applied when the analysis
starts, allowing builtins to use types defined from the machdep, such as size_t.
---
src/kernel_services/plugin_entry_points/db.ml | 2 +-
.../plugin_entry_points/db.mli | 2 +-
src/plugins/value/domains/cvalue/builtins.ml | 90 ++++++++++---------
src/plugins/value/domains/cvalue/builtins.mli | 12 +--
.../value/domains/cvalue/builtins_float.ml | 4 +-
src/plugins/value/engine/compute_functions.ml | 3 +-
6 files changed, 57 insertions(+), 56 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 6d7e0a97be4..699745967d9 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -618,7 +618,7 @@ module Value = struct
(** Type for a Value builtin function *)
- type builtin_type = typ * typ list
+ type builtin_type = unit -> typ * typ list
type builtin =
state ->
(Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index df8e7622552..b37707a8ae7 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -179,7 +179,7 @@ module Value : sig
(* Type of a C function interpreted by a builtin:
return type and list of argument types. *)
- type builtin_type = typ * typ list
+ type builtin_type = unit -> typ * typ list
(** Type for an Eva builtin function *)
type builtin =
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 55f7f29e6d3..2465cf27635 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -30,8 +30,13 @@ exception Invalid_nb_of_args of int
if -val-builtins-auto is set. *)
type use_builtin = Always | OnAuto
+(* Table of all registered builtins; filled by [register_builtin] calls. *)
let table = Hashtbl.create 17
+(* Table binding each kernel function to their builtin for a given analysis.
+ Filled at the beginning of each analysis by [prepare_builtins]. *)
+let builtins_table = Hashtbl.create 17
+
let register_builtin name ?replace ?typ f =
Hashtbl.replace table name (f, typ, None, Always);
match replace with
@@ -100,7 +105,7 @@ let mem_builtin name =
let () = Db.Value.mem_builtin := mem_builtin
-(* Returns the builtin with its specification, used to evaluate preconditions
+(* Returns the specification of a builtin, used to evaluate preconditions
and to transfer the states of other domains. *)
let find_builtin_specification kf =
let spec = Annotations.funspec kf in
@@ -113,7 +118,8 @@ let find_builtin_specification kf =
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) ->
+ | Some typ ->
+ let expected_result, expected_args = typ () in
match Kernel_function.get_type kf with
| TFun (result, args, _, _) ->
let args = Cil.argsToList args in
@@ -122,66 +128,62 @@ let inconsistent_builtin_typ kf = function
|| 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
+(* Warns if the builtin [bname] overrides the function definition [kf]. *)
+let warn_builtin_override kf source bname =
+ let internal =
+ (* TODO: treat this 'internal' *)
+ let file = source.Filepath.pos_path in
+ Filepath.is_relative ~base_name:Config.datadir (file :> string)
in
- try
- 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
+ if Kernel_function.is_definition kf && not internal
+ then
+ let fname = Kernel_function.get_name kf in
+ Value_parameters.warning ~source ~once:true
+ ~wkey:Value_parameters.wkey_builtins_override
+ "function %s: definition will be overridden by %s"
+ fname (if fname = bname then "its builtin" else "builtin " ^ bname)
-let warn_builtin_override bname kf expected_typ =
+let prepare_builtin kf builtin_name builtin 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
+ builtin_name Kernel_function.pretty kf
else
- if find_builtin_specification kf = None
- then
- Value_parameters.warning ~source ~once:true
- ~wkey:Value_parameters.wkey_builtins_missing_spec
- "The builtin for function %a will not be used, as its frama-c libc \
- specification is not available."
- Kernel_function.pretty kf
- else
- let internal =
- let pos = fst (Kernel_function.get_location kf) in
- (*TODO: treat this 'internal'*)
- let file = pos.Filepath.pos_path in
- Filepath.is_relative ~base_name:Config.datadir (file :> string)
- in
- if Kernel_function.is_definition kf && not internal
- then
- let fname = Kernel_function.get_name kf in
+ match find_builtin_specification kf with
+ | None ->
Value_parameters.warning ~source ~once:true
- ~wkey:Value_parameters.wkey_builtins_override
- "function %s: definition will be overridden by %s"
- fname (if fname = bname then "its builtin" else "builtin " ^ bname)
+ ~wkey:Value_parameters.wkey_builtins_missing_spec
+ "The builtin for function %a will not be used, as its frama-c libc \
+ specification is not available."
+ Kernel_function.pretty kf
+ | Some spec ->
+ warn_builtin_override kf source builtin_name;
+ Hashtbl.replace builtins_table kf (builtin_name, builtin, spec)
-let warn_definitions_overridden_by_builtins () =
- Value_parameters.BuiltinsOverrides.iter
- (fun (kf, name) ->
- let name = Extlib.the name in
- let (_, typ, _ , _) = Hashtbl.find table name in
- warn_builtin_override name kf typ);
+let prepare_builtins () =
+ Hashtbl.clear builtins_table;
let autobuiltins = Value_parameters.BuiltinsAuto.get () in
+ (* Links kernel functions to the registered builtins. *)
Hashtbl.iter
- (fun name (_, typ, _, u) ->
+ (fun name (f, typ, _bname, u) ->
if autobuiltins || u = Always
then
try
let kf = Globals.Functions.find_by_name name in
- warn_builtin_override name kf typ
+ prepare_builtin kf name f typ
with Not_found -> ())
- table
+ table;
+ (* Overrides builtins attribution according to the -eva-builtin option. *)
+ Value_parameters.BuiltinsOverrides.iter
+ (fun (kf, name) ->
+ let builtin_name = Extlib.the name in
+ let f, typ, _, _ = Hashtbl.find table builtin_name in
+ prepare_builtin kf builtin_name f typ)
+
+let find_builtin_override = Hashtbl.find_opt builtins_table
(* -------------------------------------------------------------------------- *)
(* --- Returning a clobbered set --- *)
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index ebf302fd0d5..561a04c266d 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -35,17 +35,17 @@ val register_builtin:
string -> ?replace:string ->
?typ:Db.Value.builtin_type -> Db.Value.builtin -> unit
+(** Prepares the builtins to be used for an analysis. Must be called at the
+ beginning of each Eva analysis. Warns about builtins of incompatible types,
+ builtins without an available specification and builtins overriding function
+ definitions. *)
+val prepare_builtins: unit -> 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
of [ret] whose contents may contain local variables. *)
val clobbered_set_from_ret: Cvalue.Model.t -> Cvalue.V.t -> Base.SetLattice.t
-(** Emits warnings for each function definition that will be overridden by an
- Eva built-in.
- Does not include definitions in the Frama-C stdlib.
- @since Phosphorus-20170501-beta1 *)
-val warn_definitions_overridden_by_builtins: unit -> unit
-
type builtin
type call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
type result = Cvalue.Model.t * Locals_scoping.clobbered_set
diff --git a/src/plugins/value/domains/cvalue/builtins_float.ml b/src/plugins/value/domains/cvalue/builtins_float.ml
index e636114ac35..3c28988d37d 100644
--- a/src/plugins/value/domains/cvalue/builtins_float.ml
+++ b/src/plugins/value/domains/cvalue/builtins_float.ml
@@ -71,7 +71,7 @@ let arity2 fk caml_fun state actuals =
let register_arity2 c_name fk f =
let name = "Frama_C_" ^ c_name in
let t = Cil_types.TFloat (fk, []) in
- let typ = t, [t; t] in
+ let typ () = t, [t; t] in
Builtins.register_builtin name ~replace:c_name ~typ (arity2 fk f)
let () =
@@ -114,7 +114,7 @@ let arity1 name fk caml_fun state actuals =
let register_arity1 c_name fk f =
let name = "Frama_C_" ^ c_name in
let t = Cil_types.TFloat (fk, []) in
- let typ = t, [t] in
+ let typ () = t, [t] in
Builtins.register_builtin name ~replace:c_name ~typ (arity1 name fk f)
let () =
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 21a9876322a..d5dabe47293 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -76,8 +76,7 @@ let pre_analysis () =
Split_return.pretty_strategies ();
generate_specs ();
Widen.precompute_widen_hints ();
- if Value_parameters.WarnBuiltinOverride.get () then
- Builtins.warn_definitions_overridden_by_builtins ();
+ Builtins.prepare_builtins ();
Value_perf.reset ();
(* We may be resuming Value from a previously crashed analysis. Clear
degeneration states *)
--
GitLab