From d3ab2cde1467124512c0af0763c951fbbcf4d19a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 16 Feb 2021 08:57:35 +0100
Subject: [PATCH] [Eva] Exports builtin registration in Eva.mli. Fixes Aorai
and Metrics plugins.
Comments the interface builtins.mli.
---
.../aorai/aorai_eva_analysis.enabled.ml | 14 +++----
src/plugins/metrics/metrics_base.ml | 2 +-
src/plugins/value/Eva.mli | 31 ++++++++++++++++
src/plugins/value/domains/cvalue/builtins.ml | 8 +++-
src/plugins/value/domains/cvalue/builtins.mli | 37 ++++++++++++++++---
src/plugins/value/eval.mli | 9 ++++-
6 files changed, 82 insertions(+), 19 deletions(-)
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index bc84db8cf54..d08d57fe36e 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -34,14 +34,13 @@ let show_aorai_variable state fmt var_name =
Z.Overflow | Not_found ->
Format.fprintf fmt "?"
-let show_val fmt (expr, v, _) =
+let show_val fmt (expr, v) =
Format.fprintf fmt "%a in %a"
Printer.pp_exp expr
(Cvalue.V.pretty_typ (Some (Cil.typeOf expr))) v
let show_aorai_state = "Frama_C_show_aorai_state"
-(*
let builtin_show_aorai_state state args =
if not (Aorai_option.Deterministic.get()) then begin
Aorai_option.warning
@@ -57,18 +56,15 @@ let builtin_show_aorai_state state args =
end;
end;
(* Return value : returns nothing, changes nothing *)
- {
- Value_types.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable;
- }
-*)
+ Eva.Builtins.States [state]
let () =
Cil_builtins.add_custom_builtin
(fun () -> (show_aorai_state,Cil.voidType,[],true))
+let () =
+ Eva.Builtins.register_builtin show_aorai_state Cacheable builtin_show_aorai_state
+
let add_slevel_annotation vi kind =
match kind with
| Aorai_visitors.Aux_funcs.(Pre _ | Post _) ->
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index 36624ef260b..2db4e1ba466 100644
--- a/src/plugins/metrics/metrics_base.ml
+++ b/src/plugins/metrics/metrics_base.ml
@@ -365,7 +365,7 @@ let get_filename fdef =
;;
let consider_function ~libc vinfo =
- not (false
+ not (Eva.Builtins.is_builtin vinfo.vname
|| Ast_info.is_frama_c_builtin vinfo.vname
|| Cil_builtins.is_unused_builtin vinfo
) && (libc || not (Cil.is_in_libc vinfo.vattr))
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index d71fa98faca..99ab8a6d81c 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -101,3 +101,34 @@ module Eva_annotations: sig
val add_subdivision_annot : emitter:Emitter.t -> loc:Cil_types.location ->
Cil_types.stmt -> int -> unit
end
+
+(** Analysis builtins for the cvalue domain, more efficient than the analysis
+ of the C functions. See {builtins.mli} for more details. *)
+module Builtins: sig
+ open Cil_types
+
+ exception Invalid_nb_of_args of int
+ exception Outside_builtin_possibilities
+
+ type builtin_type = unit -> typ * typ list
+ type cacheable = Cacheable | NoCache | NoCacheCallers
+
+ type full_result = {
+ c_values: (Cvalue.V.t option * Cvalue.Model.t) list;
+ c_clobbered: Base.SetLattice.t;
+ c_from: (Function_Froms.froms * Locations.Zone.t) option;
+ }
+
+ type call_result =
+ | States of Cvalue.Model.t list
+ | Result of Cvalue.V.t list
+ | Full of full_result
+
+ type builtin = Cvalue.Model.t -> (exp * Cvalue.V.t) list -> call_result
+
+ val register_builtin:
+ string -> ?replace:string -> ?typ:builtin_type -> cacheable ->
+ builtin -> unit
+
+ val is_builtin: string -> bool
+end
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 5ef2abd57a4..cb344b56e4a 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -26,7 +26,7 @@ exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
type builtin_type = unit -> typ * typ list
-type cacheable = Eval.cacheable
+type cacheable = Eval.cacheable = Cacheable | NoCache | NoCacheCallers
type full_result = {
c_values: (Cvalue.V.t option * Cvalue.Model.t) list;
@@ -63,7 +63,11 @@ let register_builtin name ?replace ?typ cacheable f =
| None -> ()
| Some fname -> Hashtbl.replace table fname builtin
-(* The functions in _builtin must only return the 'Always' builtins *)
+let is_builtin name =
+ try
+ let bname, _, _, _ = Hashtbl.find table name in
+ name = bname
+ with Not_found -> false
let builtin_names_and_replacements () =
let stand_alone, replacements =
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index 812503988ba..8ef7a279330 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -30,36 +30,64 @@ exception Outside_builtin_possibilities
(* Signature of a builtin: type of the result, and type of the arguments. *)
type builtin_type = unit -> typ * typ list
-type cacheable = Eval.cacheable
+
+(** Can the results of a builtin be cached? See {eval.mli} for more details.*)
+type cacheable = Eval.cacheable = Cacheable | NoCache | NoCacheCallers
type full_result = {
c_values: (Cvalue.V.t option * Cvalue.Model.t) list;
+ (** A list of results, consisting of:
+ - the value returned (ie. what is after the 'return' C keyword)
+ - the memory state after the function has been executed. *)
c_clobbered: Base.SetLattice.t;
+ (** An over-approximation of the bases in which addresses of local variables
+ might have been written *)
c_from: (Function_Froms.froms * Locations.Zone.t) option;
+ (** If not None, the froms of the function, and its sure outputs;
+ i.e. the dependencies of the result and of each zone written to. *)
}
+(** The result of a builtin can be given in different forms. *)
type call_result =
| States of Cvalue.Model.t list
+ (** A disjunctive list of post-states at the end of the C function.
+ Can only be used if the C function does not write the address of local
+ variables, does not read other locations than the call arguments, and
+ does not write other locations than the result. *)
| Result of Cvalue.V.t list
+ (** A disjunctive list of resulting values. The specification is used to
+ compute the post-state, in which the result is replaced by the values
+ computed by the builtin. *)
| Full of full_result
+ (** See [full_result] type. *)
+(** Type of a cvalue builtin, whose arguments are:
+ - the memory state at the beginning of the function call;
+ - the list of arguments of the function call. *)
type builtin = Cvalue.Model.t -> (exp * Cvalue.V.t) list -> call_result
-(** [register_builtin name ?replace ?typ f] registers the ocaml function [f]
+(** [register_builtin name ?replace ?typ cacheable f] registers the 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. *)
+ the C function is checked before using the builtin.
+ The results of the builtin are cached according to [cacheable]. *)
val register_builtin:
string -> ?replace:string -> ?typ:builtin_type -> cacheable -> builtin -> unit
+(** Has a builtin been registered with the given name? *)
+val is_builtin: string -> bool
+
(** 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
+(** Is a given function replaced by a builtin? *)
+val is_builtin_overridden: kernel_function -> bool
+
(** [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. *)
@@ -68,9 +96,6 @@ val clobbered_set_from_ret: Cvalue.Model.t -> Cvalue.V.t -> Base.SetLattice.t
type call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
type result = Cvalue_domain.State.t
-(** Is a given function replaced by a builtin? *)
-val is_builtin_overridden: kernel_function -> bool
-
(** Returns the cvalue builtin for a function, if any. Also returns the name of
the builtin and the specification of the function; the preconditions must be
evaluated along with the builtin.
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index 2610008ef2f..0ff92bbf2e3 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -220,7 +220,14 @@ type ('loc, 'value) call = {
recursive: bool;
}
-type cacheable = Cacheable | NoCache | NoCacheCallers
+(* Can the results of a function call be cached with memexec? *)
+type cacheable =
+ | Cacheable (** Functions whose result can be safely cached *)
+ | NoCache (** Functions whose result should not be cached, but for
+ which the caller can still be cached. Typically,
+ functions printing something during the analysis. *)
+ | NoCacheCallers (** Functions for which neither the call, neither the
+ callers, can be cached *)
(*
Local Variables:
--
GitLab