Merge branch 'feature/eva/builtins' into 'master'

[Eva] Changes the type and registration of builtins

See merge request frama-c/frama-c!3077

src/kernel_services/plugin_entry_points/db.ml

@@ -448,7 +448,7 @@ module Value = struct
 
   module Call_Type_Value_Callbacks =
     Hook.Build(struct
-      type t = [`Builtin of Value_types.call_result | `Spec of funspec
+      type t = [`Builtin of Value_types.call_froms | `Spec of funspec
                | `Def | `Memexec]
         * state * (kernel_function * kinstr) list end)
   ;;
@@ -628,19 +628,6 @@ module Value = struct
   let access =  mk_fun "Value.access"
   let access_expr =  mk_fun "Value.access_expr"
 
-  (** Type for a Value builtin function *)
-
-  type builtin_type = unit -> typ * typ list
-  type builtin =
-      state ->
-      (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
-      Value_types.call_result
-
-  exception Outside_builtin_possibilities
-  let register_builtin = mk_fun "Value.register_builtin"
-  let registered_builtins = mk_fun "Value.registered_builtins"
-  let mem_builtin = mk_fun "Value.mem_builtin"
-
   let use_spec_instead_of_definition =
     mk_fun "Value.use_spec_instead_of_definition"
 

src/kernel_services/plugin_entry_points/db.mli

@@ -175,40 +175,6 @@ module Value : sig
 
   (** {3 Parameterization} *)
 
-  exception Outside_builtin_possibilities
-
-  (* Type of a C function interpreted by a builtin:
-     return type and list of argument types. *)
-  type builtin_type = unit -> 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 -> ?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) list) ref
-  (** Returns a list of the pairs (name, builtin) registered via
-      [register_builtin].
-      @since Aluminium-20160501 *)
-
-  val mem_builtin: (string -> bool) ref
-  (** returns whether there is an abstract function registered by
-      {!register_builtin} with the given name. *)
-
   val use_spec_instead_of_definition: (kernel_function -> bool) ref
   (** To be called by derived analyses to determine if they must use
       the body of the function (if available), or only its spec. Used for
@@ -500,7 +466,7 @@ module Value : sig
       @since Aluminium-20160501  *)
   module Call_Type_Value_Callbacks:
     Hook.Iter_hook with type param =
-    [`Builtin of Value_types.call_result | `Spec of funspec | `Def | `Memexec]
+    [`Builtin of Value_types.call_froms | `Spec of funspec | `Def | `Memexec]
     * state * callstack
 
 

src/plugins/aorai/aorai_eva_analysis.enabled.ml

@@ -34,7 +34,7 @@ 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
@@ -56,19 +56,14 @@ 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 () =
-  !Db.Value.register_builtin show_aorai_state builtin_show_aorai_state
+  Eva.Builtins.register_builtin show_aorai_state Cacheable builtin_show_aorai_state
 
 let add_slevel_annotation vi kind =
   match kind with

src/plugins/from/callwise.ml

@@ -90,9 +90,9 @@ let call_for_individual_froms (call_type, value_initial_state, call_stack) =
       call_froms_stack :=
         { current_function; value_initial_state; table_for_calls } ::
         !call_froms_stack
-    | `Builtin { Value_types.c_from = Some (result,_) } ->
+    | `Builtin (Some (result,_)) ->
        register_from result
-    | `Builtin { Value_types.c_from = None } ->
+    | `Builtin None ->
         let behaviors =
           !Db.Value.valid_behaviors current_function value_initial_state
         in

src/plugins/inout/operational_inputs.ml

@@ -606,7 +606,7 @@ module Callwise = struct
         merge_call_in_local_table call_site table inout
     in
     match call_type with
-    | `Builtin {Value_types.c_from = Some (froms,sure_out) } ->
+    | `Builtin (Some (froms,sure_out)) ->
       let in_, out_ = extract_inout_from_froms froms in
       let inout = {
         over_inputs_if_termination = in_;
@@ -624,7 +624,7 @@ module Callwise = struct
     | `Spec spec ->
       let inout =compute_using_given_spec_state state spec current_function in
       merge_inout inout
-    | `Builtin { Value_types.c_from = None } ->
+    | `Builtin None ->
       let inout = compute_using_prototype_state state current_function in
       merge_inout inout
 

src/plugins/metrics/metrics_base.ml

@@ -365,7 +365,7 @@ let get_filename fdef =
 ;;
 
 let consider_function ~libc vinfo =
-  not (!Db.Value.mem_builtin vinfo.vname
+  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

@@ -21,14 +21,25 @@
 (**************************************************************************)
 
 open Cil_types
-open Cvalue
 
 exception Invalid_nb_of_args of int
+exception Outside_builtin_possibilities
 
-(* 'Always' means the builtin will always be used to replace a function
-   with its name. 'OnAuto' means that the function will be replaced only
-   if -eva-builtins-auto is set. *)
-type use_builtin = Always | OnAuto
+type builtin_type = unit -> typ * typ list
+type cacheable = Eval.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
 
 (* Table of all registered builtins; filled by [register_builtin] calls.  *)
 let table = Hashtbl.create 17
@@ -44,33 +55,28 @@ end
 (** Set of functions overridden by a builtin. *)
 module BuiltinsOverride = State_builder.Set_ref (Kernel_function.Set) (Info)
 
-let register_builtin name ?replace ?typ f =
-  Hashtbl.replace table name (f, typ, None, Always);
+let register_builtin name ?replace ?typ cacheable f =
+  Value_parameters.register_builtin name;
+  let builtin = (name, f, cacheable, typ) in
+  Hashtbl.replace table name builtin;
   match replace with
   | None -> ()
-  | Some fname -> Hashtbl.replace table fname (f, typ, Some name, OnAuto)
-
-let () = Db.Value.register_builtin := register_builtin
-
-(* The functions in _builtin must only return the 'Always' builtins *)
-
-let registered_builtins () =
-  let l =
-    Hashtbl.fold
-      (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
+  | Some fname -> Hashtbl.replace table fname builtin
 
-let () = Db.Value.registered_builtins := registered_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 =
-    Hashtbl.fold (fun name (_, _, replaced_by, _) (acc1, acc2) ->
-        match replaced_by with
-        | None -> name :: acc1, acc2
-        | Some rep_by -> acc1, (name, rep_by) :: acc2
-      ) table ([], [])
+    Hashtbl.fold
+      (fun name (builtin_name, _, _, _) (acc1, acc2) ->
+         if name = builtin_name
+         then name :: acc1, acc2
+         else acc1, (name, builtin_name) :: acc2)
+      table ([], [])
   in
   List.sort String.compare stand_alone,
   List.sort (fun (name1, _) (name2, _) -> String.compare name1 name2) replacements
@@ -104,13 +110,9 @@ let () =
          raise Cmdline.Exit
        end)
 
-let mem_builtin name =
-  try
-    let _, _, _, u = Hashtbl.find table name in
-    u = Always
-  with Not_found -> false
-
-let () = Db.Value.mem_builtin := mem_builtin
+(* -------------------------------------------------------------------------- *)
+(* --- Prepare builtins for an analysis                                   --- *)
+(* -------------------------------------------------------------------------- *)
 
 (* Returns the specification of a builtin, used to evaluate preconditions
    and to transfer the states of other domains. *)
@@ -155,7 +157,7 @@ let warn_builtin_override kf source bname =
       "function %s: definition will be overridden by %s"
       fname (if fname = bname then "its builtin" else "builtin " ^ bname)
 
-let prepare_builtin kf builtin_name builtin expected_typ =
+let prepare_builtin kf (name, builtin, cacheable, expected_typ) =
   let source = fst (Kernel_function.get_location kf) in
   if inconsistent_builtin_typ kf expected_typ
   then
@@ -163,7 +165,7 @@ let prepare_builtin kf builtin_name builtin expected_typ =
       ~wkey:Value_parameters.wkey_builtins_override
       "The builtin %s will not be used for function %a of incompatible type.@ \
        (got: %a)."
-      builtin_name Kernel_function.pretty kf
+      name Kernel_function.pretty kf
       Printer.pp_typ (Kernel_function.get_type kf)
   else
     match find_builtin_specification kf with
@@ -174,9 +176,9 @@ let prepare_builtin kf builtin_name builtin expected_typ =
          specification is not available."
         Kernel_function.pretty kf
     | Some spec ->
-      warn_builtin_override kf source builtin_name;
+      warn_builtin_override kf source name;
       BuiltinsOverride.add kf;
-      Hashtbl.replace builtins_table kf (builtin_name, builtin, spec)
+      Hashtbl.replace builtins_table kf (name, builtin, cacheable, spec)
 
 let prepare_builtins () =
   BuiltinsOverride.clear ();
@@ -184,35 +186,33 @@ let prepare_builtins () =
   let autobuiltins = Value_parameters.BuiltinsAuto.get () in
   (* Links kernel functions to the registered builtins. *)
   Hashtbl.iter
-    (fun name (f, typ, _bname, u) ->
-       if autobuiltins || u = Always
+    (fun name (bname, f, cacheable, typ) ->
+       if autobuiltins || name = bname
        then
          try
            let kf = Globals.Functions.find_by_name name in
-           prepare_builtin kf name f typ
+           prepare_builtin kf (name, f, cacheable, typ)
          with Not_found -> ())
     table;
   (* Overrides builtins attribution according to the -eva-builtin option. *)
   Value_parameters.BuiltinsOverrides.iter
     (fun (kf, name) ->
-       let builtin_name = Option.get name in
-       let f, typ, _, _ = Hashtbl.find table builtin_name in
-       prepare_builtin kf builtin_name f typ)
+       prepare_builtin kf (Hashtbl.find table (Option.get name)))
 
 let find_builtin_override = Hashtbl.find_opt builtins_table
 
-let is_builtin_overridden =
+let is_builtin_overridden name =
   if not (BuiltinsOverride.is_computed ())
   then prepare_builtins ();
-  BuiltinsOverride.mem
+  BuiltinsOverride.mem name
 
 (* -------------------------------------------------------------------------- *)
-(* --- Returning a clobbered set                                          --- *)
+(* --- Applying a builtin                                                 --- *)
 (* -------------------------------------------------------------------------- *)
 
 let clobbered_set_from_ret state ret =
   let aux b _ acc =
-    match Model.find_base_or_default b state with
+    match Cvalue.Model.find_base_or_default b state with
     | `Top -> Base.SetLattice.top
     | `Bottom -> acc
     | `Value m ->
@@ -220,71 +220,70 @@ let clobbered_set_from_ret state ret =
         Base.SetLattice.(join (inject_singleton b) acc)
       else acc
   in
-  try V.fold_topset_ok aux ret Base.SetLattice.bottom
+  try Cvalue.V.fold_topset_ok aux ret Base.SetLattice.bottom
   with Abstract_interp.Error_Top -> Base.SetLattice.top
 
-(* -------------------------------------------------------------------------- *)
-(* --- Applying a builtin                                                 --- *)
-(* -------------------------------------------------------------------------- *)
-
 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
 
 open Eval
 
-let unbottomize = function
-  | `Bottom -> Cvalue.V.bottom
-  | `Value v -> v
-
-let offsetmap_of_formals state arguments rest =
-  let compute expr assigned =
-    let offsm = Cvalue_offsetmap.offsetmap_of_assignment state expr assigned in
-    let value = unbottomize (Eval.value_assigned assigned) in
-    expr, value, offsm
+let compute_arguments arguments rest =
+  let compute assigned =
+    match Eval.value_assigned assigned with
+    | `Bottom -> Cvalue.V.bottom
+    | `Value v -> v
   in
-  let treat_one_formal arg = compute arg.concrete arg.avalue in
-  let treat_one_rest (exp, v) = compute exp v in
-  let list = List.map treat_one_formal arguments in
-  let rest = List.map treat_one_rest rest in
+  let list = List.map (fun arg -> arg.concrete, compute arg.avalue) arguments in
+  let rest = List.map (fun (exp, v) -> exp, compute v) rest in
   list @ rest
 
-let compute_builtin name builtin state actuals =
-  try builtin state actuals
+let process_result call state call_result =
+  let clob = Locals_scoping.bottom () in
+  let bind_result state return =
+    match return, call.return with
+    | Some value, Some vi_ret ->
+      let b_ret = Base.of_varinfo vi_ret in
+      let offsm = Eval_op.offsetmap_of_v ~typ:vi_ret.vtype value in
+      Cvalue.Model.add_base b_ret offsm state, clob
+    | _, _ -> state, clob (* TODO: error? *)
+  in
+  match call_result with
+  | States states -> List.rev_map (fun s -> s, clob) states
+  | Result values -> List.rev_map (fun v -> bind_result state (Some v)) values
+  | Full result ->
+    Locals_scoping.remember_bases_with_locals clob result.c_clobbered;
+    let process_one_return acc (return, state) =
+      if Cvalue.Model.is_reachable state
+      then bind_result state return :: acc
+      else acc
+    in
+    List.fold_left process_one_return [] result.c_values
+
+let apply_builtin (builtin:builtin) call ~pre ~post =
+  let arguments = compute_arguments call.arguments call.rest in
+  try
+    let call_result = builtin pre arguments in
+    let call_stack = Value_util.call_stack () in
+    let froms =
+      match call_result with
+      | Full result -> `Builtin result.c_from
+      | States _ -> `Builtin None
+      | Result _ -> `Spec (Annotations.funspec call.kf)
+    in
+    Db.Value.Call_Type_Value_Callbacks.apply (froms, pre, call_stack);
+    process_result call post call_result
   with
   | Invalid_nb_of_args n ->
     Value_parameters.error ~current:true
-      "Invalid number of arguments for builtin %s: %d expected, %d found"
-      name n (List.length actuals);
+      "Invalid number of arguments for builtin %a: %d expected, %d found"
+      Kernel_function.pretty call.kf n (List.length arguments);
     raise Db.Value.Aborted
-  | Db.Value.Outside_builtin_possibilities ->
+  | Outside_builtin_possibilities ->
     Value_parameters.warning ~once:true ~current:true
-      "Call to builtin %s failed, aborting." name;
+      "Call to builtin %a failed, aborting." Kernel_function.pretty call.kf;
     raise Db.Value.Aborted
 
-let apply_builtin builtin call state =
-  let name = Kernel_function.get_name call.kf in
-  let actuals = offsetmap_of_formals state call.arguments call.rest in
-  let res = compute_builtin name builtin state actuals in
-  let call_stack = Value_util.call_stack () in
-  Db.Value.Call_Type_Value_Callbacks.apply (`Builtin res, state, call_stack);
-  let clob = Locals_scoping.bottom () in
-  Locals_scoping.remember_bases_with_locals clob res.Value_types.c_clobbered;
-  let process_one_return acc (ret, post_state) =
-    if Cvalue.Model.is_reachable post_state then
-      let state =
-        match ret, call.return with
-        | Some offsm_ret, Some vi_ret ->
-          let b_ret = Base.of_varinfo vi_ret in
-          Cvalue.Model.add_base b_ret offsm_ret post_state
-        | _, _ -> post_state
-      in
-      (state, clob) :: acc
-    else
-      acc
-  in
-  let list = List.fold_left process_one_return [] res.Value_types.c_values in
-  list, res.Value_types.c_cacheable
 
 (*
 Local Variables:

src/plugins/value/domains/cvalue/builtins.mli

@@ -20,20 +20,64 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Value analysis builtin shipped with Frama-C, more efficient than their
-    equivalent in C *)
+(** Eva analysis builtins for the cvalue domain, more efficient than their
+    equivalent in C. *)
+
+open Cil_types
 
 exception Invalid_nb_of_args of int
+exception Outside_builtin_possibilities
+
+(* Signature of a builtin: type of the result, and type of the arguments. *)
+type builtin_type = unit -> typ * typ list
+
+(** 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:Db.Value.builtin_type -> Db.Value.builtin -> unit
+  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,
@@ -41,28 +85,27 @@ val register_builtin:
     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. *)
 val clobbered_set_from_ret: Cvalue.Model.t -> Cvalue.V.t -> Base.SetLattice.t
 
-type builtin
 type call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
-type result = Cvalue.Model.t * Locals_scoping.clobbered_set
-
-(** Is a given function replaced by a builtin? *)
-val is_builtin_overridden: Cil_types.kernel_function -> bool
+type result = Cvalue_domain.State.t
 
 (** 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.
     [prepare_builtins] should have been called before using this function. *)
 val find_builtin_override:
-  Cil_types.kernel_function -> (string * builtin * Cil_types.funspec) option
+  kernel_function -> (string * builtin * cacheable * funspec) option
 
 (* Applies a cvalue builtin for the given call, in the given cvalue state. *)
 val apply_builtin:
-  builtin -> call -> Cvalue.Model.t -> result list * Value_types.cacheable
+  builtin -> call -> pre:Cvalue.Model.t -> post:Cvalue.Model.t -> result list
 
 
 (*

src/plugins/value/domains/cvalue/builtins_float.ml

@@ -22,11 +22,6 @@
 
 open Cvalue
 
-let wrap_fk r = function
-  | Cil_types.FFloat -> Eval_op.wrap_float r