[Eva] Exports builtin registration in Eva.mli. Fixes Aorai and Metrics plugins.

Comments the interface builtins.mli.

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 _) ->

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))

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

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 =

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.

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: