diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index d179e9ce4fc46b632a7f76c2579300b0e5156033..3cad7ef4576845f79aea542c9a061d4360a4a94e 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/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"
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index ee87e6e60202bbcaba1410a9f3e0266774b9c298..c12c38ce188ba445a909d6179d8291f2285932fa 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/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
diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index 518a8bf3d49c305391b7b1d7788e5aacce6f6a79..c4c50da4b0eea223343f0fae79e8a77914cffe76 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/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
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index 1e6f33366a86b33af63958b9eb4f6da4527a84e5..454e2c0953ee3f215766687de9c8618fd7875bef 100644
--- a/src/plugins/from/callwise.ml
+++ b/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
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index d0e4af644e50c8cf81fa612dec1bd33d08c850d7..9cced9ee2b48f45c64890bc919e5f5d31be281f3 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/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
diff --git a/src/plugins/metrics/metrics_base.ml b/src/plugins/metrics/metrics_base.ml
index ca172c1db4a5526ba842ee1dbedcc1782d57307b..a29fdada1c39483d090761c6af07185d31df7d24 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 (!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))
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index fc8b622ad39830cb5a8912b7908f011d198ffb76..686e7ab24143eb3e8109230b809c2b36ef7955b8 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 f21513bf138ab55f4549da24607745400b5a7e68..5f571b6d2de43b264e2da334157e750bf5227ea9 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/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:
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index d4c8e217ac82dc4059ba3e4b32208fb4cf8972d5..353be4b52e81e4b3ef4ee8c9b868a391d0f7f2e8 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/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
(*
diff --git a/src/plugins/value/domains/cvalue/builtins_float.ml b/src/plugins/value/domains/cvalue/builtins_float.ml
index 8194285d1c601ae0bb9a120e7a87a233dbd7a427..f950c308568da01b587e7d9c0a39c9b333214cc5 100644
--- a/src/plugins/value/domains/cvalue/builtins_float.ml
+++ b/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
- | Cil_types.FDouble -> Eval_op.wrap_double r
- | _ -> assert false
-
let restrict_float ~assume_finite fkind value =
let truth = Cvalue_forward.assume_not_nan ~assume_finite fkind value in
match truth with
@@ -44,35 +39,30 @@ let remove_special_float fk value =
| "non-finite" -> restrict_float ~assume_finite:true fk value
| _ -> assert false
-let arity2 fk caml_fun state actuals =
+let arity2 fk caml_fun _state actuals =
match actuals with
- | [_, arg1, _; _, arg2, _] ->
- begin
- let r =
- try
- let i1 = Cvalue.V.project_ival arg1 in
- let f1 = Ival.project_float i1 in
- let i2 = Cvalue.V.project_ival arg2 in
- let f2 = Ival.project_float i2 in
- let f' = Cvalue.V.inject_float (caml_fun (Fval.kind fk) f1 f2) in
- remove_special_float fk f'
- with Cvalue.V.Not_based_on_null ->
- Cvalue.V.topify_arith_origin (V.join arg1 arg2)
- in
- { Value_types.c_values =
- if V.is_bottom r then []
- else [wrap_fk r fk, state ];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable; }
- end
+ | [_, arg1; _, arg2] ->
+ let r =
+ try
+ let i1 = Cvalue.V.project_ival arg1 in
+ let f1 = Ival.project_float i1 in
+ let i2 = Cvalue.V.project_ival arg2 in
+ let f2 = Ival.project_float i2 in
+ let f' = Cvalue.V.inject_float (caml_fun (Fval.kind fk) f1 f2) in
+ remove_special_float fk f'
+ with Cvalue.V.Not_based_on_null ->
+ Cvalue.V.topify_arith_origin (V.join arg1 arg2)
+ in
+ let result = if V.is_bottom r then [] else [r] in
+ Builtins.Result result
| _ -> raise (Builtins.Invalid_nb_of_args 2)
let register_arity2 c_name fk f =
let name = "Frama_C_" ^ c_name in
+ let replace = c_name in
let t = Cil_types.TFloat (fk, []) in
let typ () = t, [t; t] in
- Builtins.register_builtin name ~replace:c_name ~typ (arity2 fk f)
+ Builtins.register_builtin name ~replace ~typ Cacheable (arity2 fk f)
let () =
let open Fval in
@@ -83,39 +73,35 @@ let () =
register_arity2 "fmod" Cil_types.FDouble fmod;
register_arity2 "fmodf" Cil_types.FFloat fmod
-let arity1 name fk caml_fun state actuals =
+let arity1 name fk caml_fun _state actuals =
match actuals with
- | [_, arg, _] -> begin
- let r =
- try
- let i = Cvalue.V.project_ival arg in
- let f = Ival.project_float i in
- let f' = Cvalue.V.inject_float (caml_fun (Fval.kind fk) f) in
- remove_special_float fk f'
- with
- | Cvalue.V.Not_based_on_null ->
- if Cvalue.V.is_bottom arg then begin
- V.bottom
- end else begin
- Value_parameters.result ~once:true ~current:true
- "function %s applied to address" name;
- Cvalue.V.topify_arith_origin arg
- end
- in
- { Value_types.c_values =
- if V.is_bottom r then []
- else [wrap_fk r fk, state ];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable; }
- end
+ | [_, arg] ->
+ let r =
+ try
+ let i = Cvalue.V.project_ival arg in
+ let f = Ival.project_float i in
+ let f' = Cvalue.V.inject_float (caml_fun (Fval.kind fk) f) in
+ remove_special_float fk f'
+ with
+ | Cvalue.V.Not_based_on_null ->
+ if Cvalue.V.is_bottom arg then begin
+ V.bottom
+ end else begin
+ Value_parameters.result ~once:true ~current:true
+ "function %s applied to address" name;
+ Cvalue.V.topify_arith_origin arg
+ end
+ in
+ let result = if V.is_bottom r then [] else [r] in
+ Builtins.Result result
| _ -> raise (Builtins.Invalid_nb_of_args 1)
let register_arity1 c_name fk f =
let name = "Frama_C_" ^ c_name in
+ let replace = c_name in
let t = Cil_types.TFloat (fk, []) in
let typ () = t, [t] in
- Builtins.register_builtin name ~replace:c_name ~typ (arity1 name fk f)
+ Builtins.register_builtin name ~replace ~typ Cacheable (arity1 name fk f)
let () =
let open Fval in
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index 60a35cc4c72b208110f8a378f6f869508b15a22c..177c7f980d55a010df054ee50392ffaa2b057dd8 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -301,10 +301,10 @@ let add_zeroes = add_v (V_Or_Uninitialized.initialized Cvalue.V.singleton_zero)
let wrap_fallible_alloc ?returns_null ret orig_state state_after_alloc =
let default_returns_null = Value_parameters.AllocReturnsNull.get () in
let returns_null = Option.value ~default:default_returns_null returns_null in
- let success = Eval_op.wrap_ptr ret, state_after_alloc in
+ let success = Some ret, state_after_alloc in
if returns_null
then
- let failure = Eval_op.wrap_ptr Cvalue.V.singleton_zero, orig_state in
+ let failure = Some Cvalue.V.singleton_zero, orig_state in
[ success ; failure ]
else [ success ]
@@ -485,7 +485,7 @@ let choose_base_allocation () =
let register_malloc ?replace name ?returns_null prefix region =
let builtin state args =
let size = match args with
- | [ _, size, _ ] -> size
+ | [ _, size ] -> size
| _ -> raise (Builtins.Invalid_nb_of_args 1)
in
let allocate_base = choose_base_allocation () in
@@ -493,14 +493,12 @@ let register_malloc ?replace name ?returns_null prefix region =
let new_state = add_uninitialized state new_base max_alloc in
let ret = V.inject new_base Ival.zero in
let c_values = wrap_fallible_alloc ?returns_null ret state new_state in
- { Value_types.c_values = c_values ;
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.NoCacheCallers;
- c_from = None; }
+ let c_clobbered = Base.SetLattice.bottom in
+ Builtins.Full { c_values; c_clobbered; c_from = None; }
in
let name = "Frama_C_" ^ name in
let typ () = Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf] in
- Builtins.register_builtin ?replace name builtin ~typ
+ Builtins.register_builtin ?replace name NoCacheCallers builtin ~typ
let () =
register_malloc ~replace:"malloc" "malloc" "malloc" Base.Malloc;
@@ -526,7 +524,7 @@ let alloc_size_ok intended_size =
let calloc_builtin state args =
let nmemb, sizev =
match args with
- | [(_, nmemb, _); (_, size, _)] -> nmemb, size
+ | [(_, nmemb); (_, size)] -> nmemb, size
| _ -> raise (Builtins.Invalid_nb_of_args 2)
in
let size = Cvalue.V.mul nmemb sizev in
@@ -536,7 +534,7 @@ let calloc_builtin state args =
"calloc out of bounds: assert(nmemb * size <= SIZE_MAX)";
let c_values =
if size_ok = Alarmset.False (* size always overflows *)
- then [Eval_op.wrap_ptr Cvalue.V.singleton_zero, state]
+ then [Some Cvalue.V.singleton_zero, state]
else
let allocate_base = choose_base_allocation () in
let base, max_valid = allocate_base Base.Malloc "calloc" size state in
@@ -547,18 +545,17 @@ let calloc_builtin state args =
let ret = V.inject base Ival.zero in
wrap_fallible_alloc ?returns_null ret state new_state
in
- { Value_types.c_values;
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.NoCacheCallers;
- c_from = None; }
+ let c_clobbered = Base.SetLattice.bottom in
+ Builtins.Full { c_values; c_clobbered; c_from = None; }
let () =
let name = "Frama_C_calloc" in
+ let replace = "calloc" in
let typ () =
let sizeof_typ = Cil.theMachine.Cil.typeOfSizeOf in
Cil.voidPtrType, [ sizeof_typ; sizeof_typ ]
in
- Builtins.register_builtin ~replace:"calloc" name calloc_builtin ~typ
+ Builtins.register_builtin ~replace name NoCacheCallers calloc_builtin ~typ
(* ---------------------------------- Free ---------------------------------- *)
@@ -650,44 +647,37 @@ let free_aux state ~strong bases_to_remove =
(* Builtin for [free] function *)
let frama_c_free state actuals =
match actuals with
- | [ _, arg, _ ] ->
+ | [ _, arg ] ->
let bases_to_remove, card_to_remove, _null = resolve_bases_to_free arg in
+ let c_clobbered = Base.SetLattice.bottom in
if card_to_remove = 0 then
- { Value_types.c_values = [];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable; }
+ Builtins.Full { c_values = []; c_clobbered; c_from = None; }
else
let strong = card_to_remove <= 1 in
let state, changed = free_aux state ~strong bases_to_remove in
- { Value_types.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = Some changed;
- c_cacheable = Value_types.Cacheable;
- }
+ let c_values = [None, state] in
+ Builtins.Full { c_values; c_clobbered; c_from = Some changed; }
| _ -> raise (Builtins.Invalid_nb_of_args 1)
let () =
- Builtins.register_builtin ~replace:"free" "Frama_C_free" frama_c_free
- ~typ:(fun () -> (Cil.voidType, [Cil.voidPtrType]))
+ Builtins.register_builtin ~replace:"free" "Frama_C_free" Cacheable
+ frama_c_free ~typ:(fun () -> (Cil.voidType, [Cil.voidPtrType]))
(* built-in for [__fc_vla_free] function. By construction, VLA should always
be mapped to a single base. *)
let frama_c_vla_free state actuals =
match actuals with
- | [ _, arg, _] ->
+ | [ _, arg ] ->
let bases_to_remove, _card_to_remove, _null = resolve_bases_to_free arg in
let state, changed = free_aux state ~strong:true bases_to_remove in
- { Value_types.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = Some changed;
- c_cacheable = Value_types.Cacheable;
- }
+ let c_values = [None, state] in
+ let c_clobbered = Base.SetLattice.bottom in
+ Builtins.Full { c_values; c_clobbered; c_from = Some changed; }
| _ -> raise (Builtins.Invalid_nb_of_args 1)
let () =
Builtins.register_builtin
- ~replace:"__fc_vla_free" "Frama_C_vla_free" frama_c_vla_free
+ ~replace:"__fc_vla_free" "Frama_C_vla_free" Cacheable frama_c_vla_free
~typ:(fun () -> (Cil.voidType, [Cil.voidPtrType]))
let free_automatic_bases stack state =
@@ -830,7 +820,7 @@ let choose_bases_reallocation () =
let realloc_builtin state args =
let ptr, size =
match args with
- | [ (_, ptr, _); (_, size, _) ] -> ptr, size
+ | [ (_, ptr); (_, size) ] -> ptr, size
| _ -> raise (Builtins.Invalid_nb_of_args 2)
in
let bases, card_ok, null = resolve_bases_to_free ptr in
@@ -843,20 +833,17 @@ let realloc_builtin state args =
(* free old bases. *)
let new_state, changed = free_aux new_state ~strong bases in
let c_values = wrap_fallible_alloc ret state new_state in
- { Value_types.c_values;
- c_clobbered = Builtins.clobbered_set_from_ret new_state ret;
- c_cacheable = Value_types.NoCacheCallers;
- c_from = Some changed; }
+ let c_clobbered = Builtins.clobbered_set_from_ret new_state ret in
+ Builtins.Full { c_values; c_clobbered; c_from = Some changed; }
else (* Invalid call. *)
- { Value_types.c_values = [] ;
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.NoCacheCallers;
- c_from = None; }
+ let c_clobbered = Base.SetLattice.bottom in
+ Builtins.Full { c_values = []; c_clobbered; c_from = None; }
let () =
let name = "Frama_C_realloc" in
+ let replace = "realloc" in
let typ () = Cil.(voidPtrType, [voidPtrType; theMachine.typeOfSizeOf]) in
- Builtins.register_builtin ~replace:"realloc" name realloc_builtin ~typ
+ Builtins.register_builtin ~replace name NoCacheCallers realloc_builtin ~typ
(* ----------------------------- Leak detection ----------------------------- *)
@@ -892,14 +879,12 @@ let check_leaked_malloced_bases state _ =
Value_util.warning_once_current "memory leak detected for %a"
Base.pretty base)
alloced_bases;
- { Value_types.c_values = [None,state] ;
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.NoCacheCallers;
- c_from = None;
- }
+ let c_clobbered = Base.SetLattice.bottom in
+ Builtins.Full { c_values = [None,state]; c_clobbered; c_from = None; }
let () =
- Builtins.register_builtin "Frama_C_check_leak" check_leaked_malloced_bases
+ Builtins.register_builtin "Frama_C_check_leak" NoCacheCallers
+ check_leaked_malloced_bases
(*
diff --git a/src/plugins/value/domains/cvalue/builtins_memory.ml b/src/plugins/value/domains/cvalue/builtins_memory.ml
index 8aea7089f54d77dd6bccf7b5a0d5ac052bf7e3f5..394404c9d03745fcb67a82cca5bf3be5eaf4351e 100644
--- a/src/plugins/value/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/value/domains/cvalue/builtins_memory.ml
@@ -24,64 +24,38 @@ open Cil_types
open Cvalue
open Abstract_interp
open Locations
-open Value_util
-let register_builtin = Builtins.register_builtin
+let register_builtin name ?replace builtin =
+ Builtins.register_builtin name ?replace Cacheable builtin
let dkey = Value_parameters.register_category "imprecision"
-exception Found_misaligned_base
-
-let frama_C_is_base_aligned state actuals =
- try begin
- match actuals with
- | [_,x,_; _,y,_] ->
- let i = Cvalue.V.project_ival y in
- begin match Ival.project_small_set i with
- | Some si ->
- Location_Bytes.fold_i
- (fun b _o () ->
- List.iter
- (fun int ->
- if not (Base.is_aligned_by b int)
- then raise Found_misaligned_base)
- si)
+let frama_C_is_base_aligned _state = function
+ | [_, x; _, y] ->
+ let result =
+ match Ival.project_small_set (Cvalue.V.project_ival y) with
+ | Some si ->
+ let aligned =
+ Location_Bytes.for_all
+ (fun b _o -> List.for_all (Base.is_aligned_by b) si)
x
- ();
- { Value_types.c_values =
- [ Eval_op.wrap_int Cvalue.V.singleton_one, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable;
- }
- | None -> raise Found_misaligned_base
- end
- | _ -> raise (Builtins.Invalid_nb_of_args 2)
- end
- with
- | Found_misaligned_base
- | Not_found (* from project_ival *)
- | Abstract_interp.Error_Top (* from fold_i *) ->
- { Value_types.c_values = [Eval_op.wrap_int Cvalue.V.zero_or_one, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable;
- }
+ in
+ if aligned then Cvalue.V.singleton_one else Cvalue.V.zero_or_one
+ | None
+ | exception Cvalue.V.Not_based_on_null -> Cvalue.V.zero_or_one
+ in
+ Builtins.Result [result]
+ | _ -> raise (Builtins.Invalid_nb_of_args 2)
let () = register_builtin "Frama_C_is_base_aligned" frama_C_is_base_aligned
-let frama_c_offset state actuals =
- match actuals with
- | [_,x,_] ->
- let value =
+let frama_c_offset _state = function
+ | [_, x] ->
+ let result =
try
- let offsets =
- Location_Bytes.fold_i
- (fun _b o a -> Ival.join a o)
- x
- Ival.bottom
- in
+ let acc = Ival.bottom in
+ let offsets = Location_Bytes.fold_i (fun _b -> Ival.join) x acc in
Cvalue.V.inject_ival offsets
with Abstract_interp.Error_Top ->
Value_parameters.error ~current:true
@@ -89,11 +63,7 @@ let frama_c_offset state actuals =
guaranteed to be an address";
Cvalue.V.top_int
in
- { Value_types.c_values = [Eval_op.wrap_size_t value, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable;
- }
+ Builtins.Result [result]
| _ -> raise (Builtins.Invalid_nb_of_args 1)
let () = register_builtin "Frama_C_offset" frama_c_offset
@@ -130,7 +100,7 @@ let deps_nth_arg n =
let frama_c_memcpy state actuals =
- let compute (_exp_dst,dst_bytes,_) (_exp_src,src_bytes,_) (_exp_size,size,_) =
+ let compute (_exp_dst,dst_bytes) (_exp_src,src_bytes) (_exp_size,size) =
let plevel = Value_parameters.ArrayPrecisionLevel.get() in
let size =
try Cvalue.V.project_ival size
@@ -300,15 +270,15 @@ let frama_c_memcpy state actuals =
if Model.is_reachable new_state then
(* Copy at least partially succeeded (with perhaps an
alarm for some of the sizes *)
- { Value_types.c_values = [Eval_op.wrap_ptr dst_bytes, new_state];
- c_clobbered = Builtins.clobbered_set_from_ret new_state dst_bytes;
- c_from = Some(c_from, sure_zone);
- c_cacheable = Value_types.Cacheable }
+ Builtins.Full
+ { Builtins.c_values = [Some dst_bytes, new_state];
+ c_clobbered = Builtins.clobbered_set_from_ret new_state dst_bytes;
+ c_from = Some (c_from, sure_zone); }
else
- { Value_types.c_values = [ None, Cvalue.Model.bottom];
- c_clobbered = Base.SetLattice.bottom;
- c_from = Some(c_from, sure_zone);
- c_cacheable = Value_types.Cacheable }
+ Builtins.Full
+ { Builtins.c_values = [ None, Cvalue.Model.bottom];
+ c_clobbered = Base.SetLattice.bottom;
+ c_from = Some (c_from, sure_zone); }
in
match actuals with
| [dst; src; size] -> compute dst src size
@@ -385,11 +355,10 @@ let frama_c_memset_imprecise state dst v size =
let deps_return = deps_nth_arg 0 in
{ deps_table; deps_return }
in
- { Value_types.c_values = [Eval_op.wrap_ptr dst, new_state'];
- c_clobbered = Base.SetLattice.bottom;
- c_from = Some(c_from,sure_zone);
- c_cacheable = Value_types.Cacheable;
- }
+ Builtins.Full
+ { Builtins.c_values = [Some dst, new_state'];
+ c_clobbered = Base.SetLattice.bottom;
+ c_from = Some (c_from,sure_zone); }
(* let () = register_builtin "Frama_C_memset" frama_c_memset_imprecise *)
(* Type that describes why the 'precise memset' builtin may fail. *)
@@ -603,11 +572,10 @@ let frama_c_memset_precise state dst v (exp_size, size) =
Cvalue.Model.paste_offsetmap
~from:offsm ~dst_loc ~size:size_bits ~exact:true state
in
- { Value_types.c_values = [Eval_op.wrap_ptr dst, state'];
- c_clobbered = Base.SetLattice.bottom;
- c_from = Some (c_from,dst_zone);
- c_cacheable = Value_types.Cacheable;
- }
+ Builtins.Full
+ { Builtins.c_values = [Some dst, state'];
+ c_clobbered = Base.SetLattice.bottom;
+ c_from = Some (c_from,dst_zone); }
with
| Bit_utils.NoMatchingOffset -> raise (ImpreciseMemset SizeMismatch)
| Base.Not_a_C_variable -> raise (ImpreciseMemset NoTypeForDest)
@@ -619,7 +587,7 @@ let frama_c_memset_precise state dst v (exp_size, size) =
let frama_c_memset state actuals =
match actuals with
- | [(_exp_dst, dst, _); (_, v, _); (exp_size, size, _)] ->
+ | [(_exp_dst, dst); (_, v); (exp_size, size)] ->
begin
(* Remove read-only destinations *)
let dst = V.filter_base (fun b -> not (Base.is_read_only b)) dst in
@@ -634,7 +602,7 @@ let frama_c_memset state actuals =
with ImpreciseMemset reason ->
Value_parameters.debug ~dkey ~current:true
"Call to builtin precise_memset(%a) failed; %a%t"
- pretty_actuals actuals pretty_imprecise_memset_reason reason
+ Value_util.pretty_actuals actuals pretty_imprecise_memset_reason reason
Value_util.pp_callstack;
frama_c_memset_imprecise state dst v size
end
@@ -642,53 +610,40 @@ let frama_c_memset state actuals =
let () = register_builtin ~replace:"memset" "Frama_C_memset" frama_c_memset
-let frama_c_interval_split state actuals =
- try
- begin match actuals with
- | [_,lower,_; _,upper,_] ->
+let frama_c_interval_split _state actuals =
+ match actuals with
+ | [_,lower; _,upper] ->
+ begin
+ try
let upper = Ival.project_int (Cvalue.V.project_ival upper) in
let lower = Ival.project_int (Cvalue.V.project_ival lower) in
let i = ref lower in
let r = ref [] in
while (Int.le !i upper) do
- r := (Eval_op.wrap_int (Cvalue.V.inject_int !i), state) :: !r;
+ r := Cvalue.V.inject_int !i :: !r;
i := Int.succ !i;
done;
- { Value_types.c_values = !r;
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable;
- }
- | _ -> raise (Builtins.Invalid_nb_of_args 2)
+ Builtins.Result !r
+ with
+ | Cvalue.V.Not_based_on_null
+ | Ival.Not_Singleton_Int ->
+ Value_parameters.error
+ "Invalid call to Frama_C_interval_split%a"
+ Value_util.pretty_actuals actuals;
+ raise Db.Value.Aborted
end
- with
- | Cvalue.V.Not_based_on_null
- | Ival.Not_Singleton_Int ->
- Value_parameters.error
- "Invalid call to Frama_C_interval_split%a" pretty_actuals actuals;
- raise Db.Value.Aborted
+ | _ -> raise (Builtins.Invalid_nb_of_args 2)
let () = register_builtin "Frama_C_interval_split" frama_c_interval_split
(* Transforms a garbled mix into Top_int. Let other values unchanged.
Remark: this currently returns an int. Maybe we need multiple versions? *)
-let frama_c_ungarble state actuals =
- begin match actuals with
- | [_,i,_] ->
- let v =
- try
- ignore (V.project_ival i);
- i
- with V.Not_based_on_null ->
- V.inject_ival Ival.top
- in
- { Value_types.c_values = [ Eval_op.wrap_int v, state ];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable;
- }
- | _ -> raise (Builtins.Invalid_nb_of_args 1)
- end
+let frama_c_ungarble _state = function
+ | [_, i] ->
+ if Cvalue.V.is_imprecise i
+ then Builtins.Result [Cvalue.V.top_int]
+ else Builtins.Result [i]
+ | _ -> raise (Builtins.Invalid_nb_of_args 1)
let () = register_builtin "Frama_C_ungarble" frama_c_ungarble
diff --git a/src/plugins/value/domains/cvalue/builtins_misc.ml b/src/plugins/value/domains/cvalue/builtins_misc.ml
index 7b2e54d5fa9e1bf50b927908f683065923cb20fe..c4112b70f8b004939b2a5bf9e0aa890e5c36e15d 100644
--- a/src/plugins/value/domains/cvalue/builtins_misc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_misc.ml
@@ -29,28 +29,23 @@ let frama_C_assert state actuals =
Cvalue.Model.bottom
in
match actuals with
- | [arg_exp, arg, _arg_offsm] -> begin
- let state =
- if Cvalue.V.is_zero arg
- then do_bottom ()
- else if Cvalue.V.contains_zero arg
- then begin
- let state = !Db.Value.reduce_by_cond state arg_exp true in
- if Cvalue.Model.is_reachable state
- then (warning_once_current "Frama_C_assert: unknown"; state)
- else do_bottom ()
- end
- else begin
- warning_once_current "Frama_C_assert: true";
- state
- end
- in
- { Value_types.c_values = [ None, state ] ;
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.NoCache;
- }
- end
+ | [arg_exp, arg] ->
+ let state =
+ if Cvalue.V.is_zero arg
+ then do_bottom ()
+ else if Cvalue.V.contains_zero arg
+ then begin
+ let state = !Db.Value.reduce_by_cond state arg_exp true in
+ if Cvalue.Model.is_reachable state
+ then (warning_once_current "Frama_C_assert: unknown"; state)
+ else do_bottom ()
+ end
+ else begin
+ warning_once_current "Frama_C_assert: true";
+ state
+ end
+ in
+ Builtins.States [ state ]
| _ -> raise (Builtins.Invalid_nb_of_args 1)
-let () = Builtins.register_builtin "Frama_C_assert" frama_C_assert
+let () = Builtins.register_builtin "Frama_C_assert" NoCache frama_C_assert
diff --git a/src/plugins/value/domains/cvalue/builtins_print_c.ml b/src/plugins/value/domains/cvalue/builtins_print_c.ml
index 28c2180087e06c2dc1993768818a08933439bac1..88c3a58a4fa49b19efc2fdaf53c6c7b93bc92841 100644
--- a/src/plugins/value/domains/cvalue/builtins_print_c.ml
+++ b/src/plugins/value/domains/cvalue/builtins_print_c.ml
@@ -325,25 +325,17 @@ let pretty_state_as_c_assignments fmt state =
let frama_c_dump_assert state _actuals =
Value_parameters.result ~current:true "Frama_C_dump_assert_each called:@\n(%a)@\nEnd of Frama_C_dump_assert_each output"
pretty_state_as_c_assert state;
- { Value_types.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.NoCache;
- }
+ Builtins.States [state]
-let () = Builtins.register_builtin "Frama_C_dump_assert_each" frama_c_dump_assert
+let () = Builtins.register_builtin "Frama_C_dump_assert_each" NoCache frama_c_dump_assert
let frama_c_dump_assignments state _actuals =
Value_parameters.result ~current:true "Frama_C_dump_assignment_each called:@\n%a@\nEnd of Frama_C_dump_assignment_each output"
pretty_state_as_c_assignments state;
- { Value_types.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.NoCache;
- }
+ Builtins.States [state]
let () =
- Builtins.register_builtin "Frama_C_dump_assignments_each" frama_c_dump_assignments
+ Builtins.register_builtin "Frama_C_dump_assignments_each" NoCache frama_c_dump_assignments
(*
diff --git a/src/plugins/value/domains/cvalue/builtins_split.ml b/src/plugins/value/domains/cvalue/builtins_split.ml
index eabc8ced8ace46ec1af4b4055c39b35995f15e26..bcc7c2e5a68bc717203ed39264932f5ba88bdfd5 100644
--- a/src/plugins/value/domains/cvalue/builtins_split.ml
+++ b/src/plugins/value/domains/cvalue/builtins_split.ml
@@ -25,54 +25,41 @@ open Cil_types
open Abstract_interp
open Cvalue
+let register_builtin name builtin =
+ Builtins.register_builtin name Cacheable builtin
+
(** Enumeration *)
(** Cardinal of an abstract value (-1 if not enumerable). Beware this builtin
is not monotonic *)
-let frama_c_cardinal state actuals =
- match actuals with
- | [_, v, _] -> begin
- let nb = match Cvalue.V.cardinal v with
- | None -> Cvalue.V.inject_int Integer.minus_one
- | Some i -> Cvalue.V.inject_int i
- in
- { Value_types.c_values = [Eval_op.wrap_long_long nb, state];
- c_clobbered = Base.SetLattice.empty;
- c_cacheable = Value_types.Cacheable;
- c_from = None;
- }
- end
- | _ ->
- Kernel.abort ~current:true "Incorrect argument for Frama_C_cardinal"
+let frama_c_cardinal _state = function
+ | [_, v] ->
+ let nb = match Cvalue.V.cardinal v with
+ | None -> Cvalue.V.inject_int Integer.minus_one
+ | Some i -> Cvalue.V.inject_int i
+ in
+ Builtins.Result [nb]
+ | _ -> Kernel.abort ~current:true "Incorrect argument for Frama_C_cardinal"
-let () =
- !Db.Value.register_builtin "Frama_C_abstract_cardinal" frama_c_cardinal
+let () = register_builtin "Frama_C_abstract_cardinal" frama_c_cardinal
(** Minimum or maximum of an integer abstract value, Top_int otherwise.
Also not monotonic. *)
-let frama_c_min_max f state actuals =
- match actuals with
- | [_, v, _] -> begin
- let nb =
- try
- match f (Ival.min_and_max (V.project_ival v)) with
- | None -> Cvalue.V.top_int
- | Some i -> Cvalue.V.inject_int i
- with V.Not_based_on_null -> Cvalue.V.top_int
- in
- { Value_types.c_values = [Eval_op.wrap_long_long nb, state];
- c_clobbered = Base.SetLattice.empty;
- c_cacheable = Value_types.Cacheable;
- c_from = None;
- }
- end
- | _ ->
- Kernel.abort ~current:true "Incorrect argument for Frama_C_min/max"
+let frama_c_min_max f _state = function
+ | [_, v] ->
+ let nb =
+ try
+ match f (Ival.min_and_max (V.project_ival v)) with
+ | None -> Cvalue.V.top_int
+ | Some i -> Cvalue.V.inject_int i
+ with V.Not_based_on_null -> Cvalue.V.top_int
+ in
+ Builtins.Result [nb]
+ | _ -> Kernel.abort ~current:true "Incorrect argument for Frama_C_min/max"
let () =
- !Db.Value.register_builtin "Frama_C_abstract_min" (frama_c_min_max fst);
- !Db.Value.register_builtin "Frama_C_abstract_max" (frama_c_min_max snd);
-;;
+ register_builtin "Frama_C_abstract_min" (frama_c_min_max fst);
+ register_builtin "Frama_C_abstract_max" (frama_c_min_max snd)
(** Splitting values *)
@@ -186,44 +173,26 @@ let split_all ~warn lv state max_card =
(* Auxiliary function, used to register a 'Frama_C_split' variant. Only the
parsing and the error handling is shared; all the hard work is done by [f] *)
-let aux_split f state actuals =
- match actuals with
- | [({ enode = (Lval lv | CastE (_, {enode = Lval lv}))}, _, _);
- (_, card, _)] ->
- begin
+let aux_split f state = function
+ | [({ enode = (Lval lv | CastE (_, {enode = Lval lv}))}, _); (_, card)] ->
+ let states =
try
let max_card =
Integer.to_int (Ival.project_int (V.project_ival_bottom card))
in
- let states = f ~warn:true lv state max_card in
- (* Add empty return *)
- let states = List.map (fun state -> None, state) states in
- { Value_types.c_values = states;
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.Cacheable;
- c_from = None;
- }
+ f ~warn:true lv state max_card
with V.Not_based_on_null | Ival.Not_Singleton_Int ->
Value_parameters.warning ~current:true ~once:true
"Cannot use non-constant split level %a" V.pretty card;
- { Value_types.c_values = [(None, state)];
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.Cacheable;
- c_from = None;
- }
- end
+ [state]
+ in
+ Builtins.States states
| _ ->
Value_parameters.warning ~current:true ~once:true
"Cannot interpret split directive. Ignoring";
- { Value_types.c_values = [(None, state)];
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Value_types.Cacheable;
- c_from = None;
- }
+ Builtins.States [state]
let () =
- !Db.Value.register_builtin "Frama_C_builtin_split" (aux_split split_v)
-let () =
- !Db.Value.register_builtin "Frama_C_builtin_split_pointer" (aux_split split_pointer)
-let () =
- !Db.Value.register_builtin "Frama_C_builtin_split_all" (aux_split split_all)
+ register_builtin "Frama_C_builtin_split" (aux_split split_v);
+ register_builtin "Frama_C_builtin_split_pointer" (aux_split split_pointer);
+ register_builtin "Frama_C_builtin_split_all" (aux_split split_all)
diff --git a/src/plugins/value/domains/cvalue/builtins_string.ml b/src/plugins/value/domains/cvalue/builtins_string.ml
index d479ad1dca70ae6fde9c20075f2611ba92a99b79..97bae714d07b173d5a56aac6c858e699cef058da 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.ml
+++ b/src/plugins/value/domains/cvalue/builtins_string.ml
@@ -376,54 +376,44 @@ let do_search ~search ~stop_at_0 ~typ ~length ?limit = fun state args ->
let size = bits_size typ in
let signed = signed_char typ in
let str = List.nth args 0 in
- let result, alarm =
- try
- let str, valid = reduce_by_validity ~size str in
- let search =
- if Ival.is_bottom search
- then searched_char ~size ~signed (List.nth args 1)
- else search
- in
- (* When searching exactly 0, the search naturally stops at 0. *)
- let stop_at_0 = if Ival.is_zero search then false else stop_at_0 in
- let interpret_limit n =
- let cvalue = List.nth args n in
- let limit = Ival.scale size (Cvalue.V.project_ival cvalue) in
- Ival.(narrow positive_integers limit)
- in
- let limit = Option.map interpret_limit limit in
- let kind = { search; stop_at_0; size; signed; limit } in
- let result, alarm = search_char kind ~length state str in
- result, alarm || not valid
- with | Abstract_interp.Error_Top
- | Cvalue.V.Not_based_on_null -> return_top ~length str, true
- in
- let wrapper = if length then Eval_op.wrap_size_t else Eval_op.wrap_ptr in
- if Cvalue.V.is_bottom result then None, alarm else wrapper result, alarm
+ try
+ let str, valid = reduce_by_validity ~size str in
+ let search =
+ if Ival.is_bottom search
+ then searched_char ~size ~signed (List.nth args 1)
+ else search
+ in
+ (* When searching exactly 0, the search naturally stops at 0. *)
+ let stop_at_0 = if Ival.is_zero search then false else stop_at_0 in
+ let interpret_limit n =
+ let cvalue = List.nth args n in
+ let limit = Ival.scale size (Cvalue.V.project_ival cvalue) in
+ Ival.(narrow positive_integers limit)
+ in
+ let limit = Option.map interpret_limit limit in
+ let kind = { search; stop_at_0; size; signed; limit } in
+ let result, alarm = search_char kind ~length state str in
+ result, alarm || not valid
+ with | Abstract_interp.Error_Top
+ | Cvalue.V.Not_based_on_null -> return_top ~length str, true
(* Applies the [builtin] built by [do_search]. *)
let apply_builtin _name builtin = fun state args ->
- let args = List.map (fun (_, v, _) -> v) args in
+ let args = List.map snd args in
let result, _alarm = builtin state args in
- let res_cvalue = match result with
- | None -> None, Cvalue.Model.bottom
- | Some _ -> result, state
- in
- { Value_types.c_values = [ res_cvalue ];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable; }
+ let result = if Cvalue.V.is_bottom result then [] else [result] in
+ Builtins.Result result
(* Builds, registers and exports a builtin for the C function [c_name]. *)
let register_builtin c_name ~search ~stop_at_0 ~typ ~length ?limit =
let name = "Frama_C_" ^ c_name in
let f = do_search ~search ~stop_at_0 ~typ ~length ?limit in
let builtin = apply_builtin name f in
- Builtins.register_builtin name ~replace:c_name builtin;
+ Builtins.register_builtin name ~replace:c_name Cacheable builtin;
f
type str_builtin_sig =
- Cvalue.Model.t -> Cvalue.V.t list -> Cvalue.V_Offsetmap.t option * bool
+ Cvalue.Model.t -> Cvalue.V.t list -> Cvalue.V.t * bool
let frama_c_strlen_wrapper : str_builtin_sig =
register_builtin "strlen"
diff --git a/src/plugins/value/domains/cvalue/builtins_string.mli b/src/plugins/value/domains/cvalue/builtins_string.mli
index feea3c2719fbae80a462531a671a89bc02fe46da..8883ed2efeb68bbf3d6863a2b0fe90997e20d3ea 100644
--- a/src/plugins/value/domains/cvalue/builtins_string.mli
+++ b/src/plugins/value/domains/cvalue/builtins_string.mli
@@ -21,10 +21,10 @@
(**************************************************************************)
(** A builtin takes the state and a list of values for the arguments, and
- returns the offsetmap of the return value (None if bottom), and a boolean
- indicating the possibility of alarms. *)
+ returns the return value (which can be bottom), and a boolean indicating the
+ possibility of alarms. *)
type str_builtin_sig =
- Cvalue.Model.t -> Cvalue.V.t list -> Cvalue.V_Offsetmap.t option * bool
+ Cvalue.Model.t -> Cvalue.V.t list -> Cvalue.V.t * bool
val frama_c_strlen_wrapper: str_builtin_sig
val frama_c_wcslen_wrapper: str_builtin_sig
diff --git a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
index d7b0df933a864380c577ea0c1143bd2517255360..2ae3ce11c47ef2a8aaf2dcf3cc877a2fa7c8e34b 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -49,20 +49,20 @@ let new_watchpoint name_lv loc v n =
let add_watch make_watch state actuals =
match actuals with
- | [(dst_e, dst, _); (_, size, _); (_, target_value, _); (_, number, _)] ->
+ | [(dst_e, dst); (_, size); (_, target_value); (_, number)] ->
let size =
try
let size = Cvalue.V.project_ival size in
Int.mul Int.eight (Ival.project_int size)
with V.Not_based_on_null | Ival.Not_Singleton_Int ->
- raise Db.Value.Outside_builtin_possibilities
+ raise Builtins.Outside_builtin_possibilities
in
let number =
try
let number = Cvalue.V.project_ival number in
Ival.project_int number
with V.Not_based_on_null | Ival.Not_Singleton_Int ->
- raise Db.Value.Outside_builtin_possibilities
+ raise Builtins.Outside_builtin_possibilities
in
let loc_bits = Locations.loc_bytes_to_loc_bits dst in
let loc = Locations.make_loc loc_bits (Int_Base.inject size) in
@@ -76,10 +76,7 @@ let add_watch make_watch state actuals =
then
watch_table :=
(new_watchpoint dst_e loc target_w number) :: current;
- { Value_types.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable }
+ Builtins.States [state]
| _ -> raise (Builtins.Invalid_nb_of_args 4)
let make_watch_value target_value = Value target_value
@@ -90,13 +87,13 @@ let make_watch_cardinal target_value =
Cardinal (Integer.to_int (Ival.project_int target_value))
with V.Not_based_on_null | Ival.Not_Singleton_Int
| Z.Overflow (* from Integer.to_int *) ->
- raise Db.Value.Outside_builtin_possibilities
+ raise Builtins.Outside_builtin_possibilities
let () =
- Builtins.register_builtin "Frama_C_watch_value" (add_watch make_watch_value)
+ Builtins.register_builtin "Frama_C_watch_value" Cacheable
+ (add_watch make_watch_value)
let () =
- Builtins.register_builtin
- "Frama_C_watch_cardinal"
+ Builtins.register_builtin "Frama_C_watch_cardinal" Cacheable
(add_watch make_watch_cardinal)
let watch_hook (stmt, _callstack, states) =
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index b41b8cc4851e0eb6063887946f3b6d5dd4276c16..b622130d6e7c272654cfa450ebc47e2f5d7232d1 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -195,7 +195,7 @@ module Make (Abstract: Abstractions.Eva) = struct
if Cil.is_in_libc vi.vattr then
Library_functions.warn_unsupported_spec vi.vorig_name;
Spec.compute_using_specification ~warn:true call_kinstr call spec state,
- Value_types.Cacheable
+ Eval.Cacheable
| `Def _fundec ->
Db.Value.Call_Type_Value_Callbacks.apply (`Def, cvalue_state, call_stack);
Computer.compute kf call_kinstr state
@@ -221,7 +221,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let call_result = default () in
let () =
if not (!Db.Value.use_spec_instead_of_definition call.kf)
- && call_result.Transfer.cacheable = Value_types.Cacheable
+ && call_result.Transfer.cacheable = Eval.Cacheable
then
let final_states = call_result.Transfer.states in
MemExec.store_computed_call call.kf init_state args final_states
@@ -251,7 +251,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Db.Value.Record_Value_Callbacks_New.apply
(stack_with_call, Value_types.Reuse i);
(* call can be cached since it was cached once *)
- Transfer.{states; cacheable = Value_types.Cacheable; builtin=false}
+ Transfer.{states; cacheable = Cacheable; builtin=false}
else
default ()
@@ -275,7 +275,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute_call_or_builtin stmt call state =
match Builtins.find_builtin_override call.kf with
| None -> compute_and_cache_call stmt call state
- | Some (name, builtin, spec) ->
+ | Some (name, builtin, cacheable, spec) ->
Value_results.mark_kf_as_called call.kf;
let kinstr = Kstmt stmt in
let kf_name = Kernel_function.get_name call.kf in
@@ -296,12 +296,13 @@ module Make (Abstract: Abstractions.Eva) = struct
| `Bottom ->
let cs = Value_util.call_stack () in
Db.Value.Call_Type_Value_Callbacks.apply (`Spec spec, cvalue_state, cs);
- let cacheable = Value_types.Cacheable in
+ let cacheable = Eval.Cacheable in
Transfer.{states; cacheable; builtin=true}
| `Value final_state ->
let cvalue_call = get_cvalue_call call in
- let cvalue_states, cacheable =
- Builtins.apply_builtin builtin cvalue_call cvalue_state
+ let post = Abstract.Dom.get_cvalue_or_top final_state in
+ let cvalue_states =
+ Builtins.apply_builtin builtin cvalue_call ~pre:cvalue_state ~post
in
let insert cvalue_state =
Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 8de2b35637636c8fb659923ce0c9cb30b2a33084..930c01942de58d96d47e0845553c4b4e9e249415 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -66,7 +66,7 @@ module Make_Dataflow
let kf = AnalysisParam.kf
let fundec = Kernel_function.get_definition kf
- let cacheable = ref Value_types.Cacheable
+ let cacheable = ref Eval.Cacheable
(* --- Plugin parameters --- *)
@@ -273,9 +273,9 @@ module Make_Dataflow
let result, call_cacheable =
Transfer.call stmt dest callee args state
in
- if call_cacheable = Value_types.NoCacheCallers then
+ if call_cacheable = Eval.NoCacheCallers then
(* Propagate info that the current call cannot be cached either *)
- cacheable := Value_types.NoCacheCallers;
+ cacheable := Eval.NoCacheCallers;
Bottom.list_of_bot result
let transfer_instr (stmt : stmt) (instr : instr) : transfer_function =
diff --git a/src/plugins/value/engine/iterator.mli b/src/plugins/value/engine/iterator.mli
index d11bb54625270b285e09ce0e6fd051deb55caf7c..163796d15e9f89c74a07ebdc070d07dbd5e92352 100644
--- a/src/plugins/value/engine/iterator.mli
+++ b/src/plugins/value/engine/iterator.mli
@@ -46,7 +46,7 @@ module Computer
val compute:
kernel_function -> kinstr -> Abstract.Dom.t ->
- Abstract.Dom.t list or_bottom * Value_types.cacheable
+ Abstract.Dom.t list or_bottom * Eval.cacheable
end
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 34ea9d023571c31f42450e6c07ff4c34d3e85d2b..040629aa88699be86afd064e0775d464398b4e34 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -32,7 +32,7 @@ module type S = sig
val assume: state -> stmt -> exp -> bool -> state or_bottom
val call:
stmt -> lval option -> exp -> exp list -> state ->
- state list or_bottom * Value_types.cacheable
+ state list or_bottom * Eval.cacheable
val check_unspecified_sequence:
stmt ->
state -> (stmt * lval list * lval list * lval list * stmt ref list) list ->
@@ -40,7 +40,7 @@ module type S = sig
val enter_scope: kernel_function -> varinfo list -> state -> state
type call_result = {
states: state list or_bottom;
- cacheable: Value_types.cacheable;
+ cacheable: Eval.cacheable;
builtin: bool;
}
val compute_call_ref:
@@ -290,7 +290,7 @@ module Make (Abstract: Abstractions.Eva) = struct
type call_result = {
states: state list or_bottom;
- cacheable: Value_types.cacheable;
+ cacheable: cacheable;
builtin: bool;
}
@@ -317,7 +317,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Domain.Store.register_initial_state (Value_util.call_stack ()) state;
!compute_call_ref stmt call state
| `Bottom ->
- { states = `Bottom; cacheable = Value_types.Cacheable; builtin=false }
+ { states = `Bottom; cacheable = Cacheable; builtin=false }
in
cleanup ();
res
@@ -716,15 +716,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Domain.get_cvalue_or_top state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
Db.Value.merge_initial_state (Value_util.call_stack ()) cvalue_state;
- let result =
- { Value_types.c_values = [ None, cvalue_state] ;
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Value_types.Cacheable;
- }
- in
Db.Value.Call_Type_Value_Callbacks.apply
- (`Builtin result, cvalue_state, stack_with_call)
+ (`Builtin None, cvalue_state, stack_with_call)
(* --------------------- Process the call statement ---------------------- *)
@@ -737,7 +730,7 @@ module Make (Abstract: Abstractions.Eva) = struct
Eval.eval_function_exp ~subdivnb funcexp ~args state
in
Alarmset.emit ki_call alarms;
- let cacheable = ref Value_types.Cacheable in
+ let cacheable = ref Cacheable in
let eval =
functions >>- fun functions ->
let current_kf = Value_util.current_kf () in
@@ -757,8 +750,8 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Do the call. *)
let c, states = do_one_call valuation stmt lval_option call state in
(* If needed, propagate that callers cannot be cached. *)
- if c = Value_types.NoCacheCallers then
- cacheable := Value_types.NoCacheCallers;
+ if c = NoCacheCallers then
+ cacheable := NoCacheCallers;
states
in
(* Process each possible function apart, and append the result list. *)
diff --git a/src/plugins/value/engine/transfer_stmt.mli b/src/plugins/value/engine/transfer_stmt.mli
index c280d047b07afa5c60902dadb7b1de0880d81d02..af7e5fa3e7383125abfbb9101e64a23d5b8f9baf 100644
--- a/src/plugins/value/engine/transfer_stmt.mli
+++ b/src/plugins/value/engine/transfer_stmt.mli
@@ -37,7 +37,7 @@ module type S = sig
val call:
stmt -> lval option -> exp -> exp list -> state ->
- state list or_bottom * Value_types.cacheable
+ state list or_bottom * Eval.cacheable
val check_unspecified_sequence:
Cil_types.stmt ->
@@ -50,7 +50,7 @@ module type S = sig
type call_result = {
states: state list or_bottom;
- cacheable: Value_types.cacheable;
+ cacheable: Eval.cacheable;
builtin: bool;
}
diff --git a/src/plugins/value/eval.ml b/src/plugins/value/eval.ml
index 2702268a75fcfe979f8c8060fcf866574e88fc1c..35890fccc1ce014f27793899aa2029ee5cafe3ec 100644
--- a/src/plugins/value/eval.ml
+++ b/src/plugins/value/eval.ml
@@ -243,6 +243,8 @@ type ('loc, 'value) call = {
recursive: bool;
}
+type cacheable = Cacheable | NoCache | NoCacheCallers
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/value/eval.mli b/src/plugins/value/eval.mli
index 28301c46e79ddeb64d84603b5f97f584fc34ca63..31f6e332eca013eac6d003c7c202eb07c6038a6a 100644
--- a/src/plugins/value/eval.mli
+++ b/src/plugins/value/eval.mli
@@ -220,6 +220,15 @@ type ('loc, 'value) call = {
recursive: bool;
}
+(* 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:
compile-command: "make -C ../../.."
diff --git a/src/plugins/value/legacy/eval_op.ml b/src/plugins/value/legacy/eval_op.ml
index 1cc14743aa781c7880a58f42a98e8842b606f937..8c754c4a2696134bef381ff1320dbe5d4caeeeb2 100644
--- a/src/plugins/value/legacy/eval_op.ml
+++ b/src/plugins/value/legacy/eval_op.ml
@@ -39,14 +39,6 @@ let offsetmap_of_loc location state =
in
Precise_locs.fold aux location `Bottom
-let wrap_int i = Some (offsetmap_of_v ~typ:Cil.intType i)
-let wrap_ptr p = Some (offsetmap_of_v ~typ:Cil.intPtrType p)
-let wrap_double d = Some (offsetmap_of_v ~typ:Cil.doubleType d)
-let wrap_float d = Some (offsetmap_of_v ~typ:Cil.floatType d)
-let wrap_size_t i =
- Some (offsetmap_of_v ~typ:(Cil.theMachine.Cil.typeOfSizeOf) i)
-let wrap_long_long i = Some (offsetmap_of_v ~typ:Cil.longLongType i)
-
let v_uninit_of_offsetmap ~typ offsm =
let size = Eval_typ.sizeof_lval_typ typ in
match size with
diff --git a/src/plugins/value/legacy/eval_op.mli b/src/plugins/value/legacy/eval_op.mli
index 9e0e02ed42f34a5d75b917bae0189bfc1a0b6d28..ef8f6150c68314d7c18f5b8681755b651ac52d80 100644
--- a/src/plugins/value/legacy/eval_op.mli
+++ b/src/plugins/value/legacy/eval_op.mli
@@ -33,14 +33,6 @@ val offsetmap_of_v: typ:Cil_types.typ -> V.t -> V_Offsetmap.t
val offsetmap_of_loc:
Precise_locs.precise_location -> Model.t -> V_Offsetmap.t Eval.or_bottom
-(** Specialization of the function above for standard types *)
-val wrap_size_t: V.t -> V_Offsetmap.t option
-val wrap_int: V.t -> V_Offsetmap.t option
-val wrap_ptr: V.t -> V_Offsetmap.t option
-val wrap_double: V.t -> V_Offsetmap.t option
-val wrap_float: V.t -> V_Offsetmap.t option
-val wrap_long_long: V.t -> V_Offsetmap.t option
-
val backward_comp_left_from_type:
logic_type ->
(bool -> Abstract_interp.Comp.t -> Cvalue.V.t -> Cvalue.V.t -> Cvalue.V.t)
diff --git a/src/plugins/value/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 4a19ba063da93259551138260379081ece972574..5de658b98e54d52516fc62bf0f3e08d402e3bda4 100644
--- a/src/plugins/value/legacy/eval_terms.ml
+++ b/src/plugins/value/legacy/eval_terms.ml
@@ -568,28 +568,20 @@ let constraint_trange idx size_arr =
(* Applies a cvalue [builtin] to the list of arguments [args_list] in the
current state of [env]. Returns [v, alarms], where [v] is the resulting
- cvalue, or [None] if the builtin leads to [bottom]. *)
+ cvalue, which can be bottom. *)
let apply_logic_builtin builtin env args_list =
(* the call below could in theory return Builtins.Invalid_nb_of_args,
but logic typing constraints prevent that. *)
- let res, alarms = builtin (env_current_state env) args_list in
- match res with
- | None -> None
- | Some offsm ->
- let v = Option.get (Cvalue.V_Offsetmap.single_interval_value offsm) in
- let v = Cvalue.V_Or_Uninitialized.get_v v in
- Some (v, alarms)
+ builtin (env_current_state env) args_list
(* Never raises exceptions; instead, returns [-1,+oo] in case of alarms
(most imprecise result possible for the logic strlen/wcslen predicates). *)
let eval_logic_charlen wrapper env v ldeps =
let eover =
- match apply_logic_builtin wrapper env [v] with
- | None -> Cvalue.V.bottom
- | Some (v, alarms) ->
- if alarms
- then Cvalue.V.inject_ival (Ival.inject_range (Some Int.minus_one) None)
- else v
+ let v, alarms = apply_logic_builtin wrapper env [v] in
+ if alarms && not (Cvalue.V.is_bottom v)
+ then Cvalue.V.inject_ival (Ival.inject_range (Some Int.minus_one) None)
+ else v
in
let eunder = under_from_over eover in
(* the C strlen function has type size_t, but the logic strlen function has
@@ -600,19 +592,16 @@ let eval_logic_charlen wrapper env v ldeps =
(* Evaluates the logical predicates strchr/wcschr. *)
let eval_logic_charchr builtin env s c ldeps_s ldeps_c =
let eover =
- match apply_logic_builtin builtin env [s; c] with
- | None -> Cvalue.V.bottom
- | Some (r, alarms) ->
- if alarms
- then Cvalue.V.zero_or_one
- else
- let ctrue = Cvalue.V.contains_non_zero r
- and cfalse = Cvalue.V.contains_zero r in
- match ctrue, cfalse with
- | true, true -> Cvalue.V.zero_or_one
- | true, false -> Cvalue.V.singleton_one
- | false, true -> Cvalue.V.singleton_zero
- | false, false -> assert false (* a logic alarm would have been raised*)
+ let v, alarms = apply_logic_builtin builtin env [s; c] in
+ if Cvalue.V.is_bottom v then v else
+ if alarms then Cvalue.V.zero_or_one else
+ let ctrue = Cvalue.V.contains_non_zero v
+ and cfalse = Cvalue.V.contains_zero v in
+ match ctrue, cfalse with
+ | true, true -> Cvalue.V.zero_or_one
+ | true, false -> Cvalue.V.singleton_one
+ | false, true -> Cvalue.V.singleton_zero
+ | false, false -> assert false (* a logic alarm would have been raised*)
in
let eunder = under_from_over eover in
(* the C strchr function has type char*, but the logic strchr predicate has
@@ -629,11 +618,12 @@ let eval_logic_memchr_off builtin env s c n =
let n_pos = Cvalue.V.narrow positive pred_n in
let eover =
if Cvalue.V.is_bottom n_pos then minus_one else
- match apply_logic_builtin builtin env [s.eover; c.eover; n_pos] with
- | None -> pred_n
- | Some (v, alarms) ->
- if alarms then Cvalue.V.join pred_n v else
- if Cvalue.V.equal n_pos pred_n then v else Cvalue.V.join minus_one v
+ let args = [s.eover; c.eover; n_pos] in
+ let v, alarms = apply_logic_builtin builtin env args in
+ if Cvalue.V.is_bottom v then pred_n else
+ if alarms then Cvalue.V.join pred_n v else
+ if Cvalue.V.equal n_pos pred_n then v else
+ Cvalue.V.join minus_one v
in
let ldeps = join_logic_deps s.ldeps (join_logic_deps c.ldeps n.ldeps) in
{ (einteger eover) with ldeps }
@@ -1681,12 +1671,12 @@ let eval_valid_read_str ~wide env v =
if wide then Builtins_string.frama_c_wcslen_wrapper
else Builtins_string.frama_c_strlen_wrapper
in
- match apply_logic_builtin wrapper env [v] with
- | None -> (* bottom state => string always invalid *) False
- | Some (_res, alarms) ->
- if alarms
- then (* alarm => string possibly invalid *) Unknown
- else (* no alarm => string always valid for reading *) True
+ let v, alarms = apply_logic_builtin wrapper env [v] in
+ if Cvalue.V.is_bottom v
+ then False (* bottom state => string always invalid *)
+ else if alarms
+ then Unknown (* alarm => string possibly invalid *)
+ else True (* no alarm => string always valid for reading *)
(* Evaluates a [valid_string] or [valid_wstring] predicate.
First, we check the constness of the arguments.
diff --git a/src/plugins/value/utils/value_util.ml b/src/plugins/value/utils/value_util.ml
index b6826afb7ea3f80eabdabd2850acb5f8de10a757..00f2871518eca24188ce2f575e0bfdc71771c7c6 100644
--- a/src/plugins/value/utils/value_util.ml
+++ b/src/plugins/value/utils/value_util.ml
@@ -88,7 +88,7 @@ let get_subdivision stmt =
x
let pretty_actuals fmt actuals =
- let pp fmt (e,x,_) = Cvalue.V.pretty_typ (Some (Cil.typeOf e)) fmt x in
+ let pp fmt (e,x) = Cvalue.V.pretty_typ (Some (Cil.typeOf e)) fmt x in
Pretty_utils.pp_flowlist pp fmt actuals
let pretty_current_cfunction_name fmt =
diff --git a/src/plugins/value/utils/value_util.mli b/src/plugins/value/utils/value_util.mli
index 3ae37341f50d8a81d2ad457387c3cb93f789a6f3..61df6ce5331ea7d09ef8efb35e2e607bb5f3d0e5 100644
--- a/src/plugins/value/utils/value_util.mli
+++ b/src/plugins/value/utils/value_util.mli
@@ -48,7 +48,7 @@ val emitter : Emitter.t
val get_slevel : Kernel_function.t -> Value_parameters.SlevelFunction.value
val get_subdivision: stmt -> int
val pretty_actuals :
- Format.formatter -> (Cil_types.exp * Cvalue.V.t * 'b) list -> unit
+ Format.formatter -> (Cil_types.exp * Cvalue.V.t) list -> unit
val pretty_current_cfunction_name : Format.formatter -> unit
val warning_once_current : ('a, Format.formatter, unit) format -> 'a
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 7714801f87bdc613d7a694f723c721172a12bfbf..ec4e77fd3ed01fec6b323a0129a6a1f580db8bd0 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -885,6 +885,10 @@ let () = add_precision_dep ILevel.parameter
let () = ILevel.add_update_hook (fun _ i -> Int_set.set_small_cardinal i)
let () = ILevel.set_range 4 256
+let builtins = ref Datatype.String.Set.empty
+let register_builtin name = builtins := Datatype.String.Set.add name !builtins
+let mem_builtin name = Datatype.String.Set.mem name !builtins
+
let () = Parameter_customize.set_group precision_tuning
let () = Parameter_customize.argument_may_be_fundecl ()
module BuiltinsOverrides =
@@ -895,12 +899,12 @@ module BuiltinsOverrides =
let of_string ~key:kf ~prev:_ nameopt =
begin match nameopt with
| Some name ->
- if not (!Db.Value.mem_builtin name) then
+ if not (mem_builtin name) then
abort "option '-eva-builtin %a:%s': undeclared builtin '%s'@.\
declared builtins: @[%a@]"
Kernel_function.pretty kf name name
(Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string)
- (List.map fst (!Db.Value.registered_builtins ()))
+ (Datatype.String.Set.elements !builtins)
| _ -> abort
"option '-eva-builtin':@ \
no builtin associated to function '%a',@ use '%a:<builtin>'"
@@ -921,7 +925,7 @@ let () = add_correctness_dep BuiltinsOverrides.parameter
(* Exported in Eva.mli. *)
let use_builtin key name =
- if !Db.Value.mem_builtin name
+ if mem_builtin name
then BuiltinsOverrides.add (key, Some name)
else raise Not_found
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 0a294b1e8c116567bfb723b1843c173484228d91..3f50d6efaa7990c3c68289b0043e4259bab34ba0 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -218,6 +218,9 @@ val dkey_callbacks : category
(** Debug category used to print the usage of widenings. *)
val dkey_widening : category
+(** Registers available cvalue builtins for the -eva-builtin option. *)
+val register_builtin: string -> unit
+
(** Registers available domain names for the -eva-domains option. *)
val register_domain: name:string -> descr:string -> unit
diff --git a/src/plugins/value_types/value_types.ml b/src/plugins/value_types/value_types.ml
index 724f9d5b835abcaad649f350df881c8371fc8f52..b115bc2ce41b7ea3f80a549a13432a606852a64e 100644
--- a/src/plugins/value_types/value_types.ml
+++ b/src/plugins/value_types/value_types.ml
@@ -114,18 +114,7 @@ type 'a callback_result =
| NormalStore of 'a * int
| Reuse of int
-type cacheable =
- | Cacheable
- | NoCache
- | NoCacheCallers
-
-
-type call_result = {
- c_values: (Cvalue.V_Offsetmap.t option * Cvalue.Model.t) list;
- c_clobbered: Base.SetLattice.t;
- c_cacheable: cacheable;
- c_from: (Function_Froms.froms * Locations.Zone.t) option
-}
+type call_froms = (Function_Froms.froms * Locations.Zone.t) option
type logic_dependencies = Locations.Zone.t Cil_datatype.Logic_label.Map.t
diff --git a/src/plugins/value_types/value_types.mli b/src/plugins/value_types/value_types.mli
index f3226b1161b4a4a3d6dd83ec8e1de742b24188c8..6d5ebf1fa8704d196ec5cf2ab5f9156c590b01c2 100644
--- a/src/plugins/value_types/value_types.mli
+++ b/src/plugins/value_types/value_types.mli
@@ -63,37 +63,10 @@ type 'a callback_result =
| NormalStore of 'a * int
| Reuse of int
-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 *)
-
-
-(** Results of a a call to a function *)
-type call_result = {
- c_values: (** Memory states after the call *)
- (Cvalue.V_Offsetmap.t option
- (** the value returned (ie. what is after the 'return' C keyword). *)
- * Cvalue.Model.t
- (** the memory state after the function has been executed *))
- list;
-
- c_clobbered: Base.SetLattice.t
- (** An over-approximation of the bases in which addresses of local
- variables might have been written *);
-
- c_cacheable: cacheable
- (** Is it possible to cache the result of this call? *);
-
- 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 the dependencies
- of each zone written to. *)
-}
-
+type call_froms = (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 the dependencies
+ of each zone written to. *)
(** Dependencies for the evaluation of a term or a predicate: for each
program point involved, sets of zones that must be read *)
diff --git a/tests/builtins/oracle/memchr.res.oracle b/tests/builtins/oracle/memchr.res.oracle
index 4fbe20f941e39805a6270ea36816a8f5df791524..df4a1d526227438f0e5e72bc778aa514d5533a41 100644
--- a/tests/builtins/oracle/memchr.res.oracle
+++ b/tests/builtins/oracle/memchr.res.oracle
@@ -538,12 +538,12 @@
[eva] tests/builtins/memchr.c:376: assertion got status valid.
[eva] tests/builtins/memchr.c:377: assertion got status valid.
[eva] tests/builtins/memchr.c:379: Call to builtin memchr
-[eva:alarm] tests/builtins/memchr.c:379: Warning:
- function memchr: precondition 'valid' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:379: Warning:
- function memchr: precondition 'initialization' got status unknown.
-[eva:alarm] tests/builtins/memchr.c:379: Warning:
- function memchr: precondition 'danglingness' got status unknown.
+[eva] tests/builtins/memchr.c:379:
+ function memchr: precondition 'valid' got status valid.
+[eva] tests/builtins/memchr.c:379:
+ function memchr: precondition 'initialization' got status valid.
+[eva] tests/builtins/memchr.c:379:
+ function memchr: precondition 'danglingness' got status valid.
[eva] tests/builtins/memchr.c:379: Frama_C_show_each_mymemchr: {1}
[eva] tests/builtins/memchr.c:380: Call to builtin memchr
[eva:alarm] tests/builtins/memchr.c:380: Warning:
@@ -1308,9 +1308,15 @@
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function memchr_big_array:
c ∈ {0}
- u[0..199] ∈ {270729319} or UNINITIALIZED
- r[0..200] ∈ {270729319} or UNINITIALIZED
- t[0..999999] ∈ {270729319} or UNINITIALIZED
+ u[0][bits 0 to 15]# ∈ {270729319}%32, bits 0 to 15
+ [bits 16 to 6399]# ∈
+ {270729319} or UNINITIALIZED repeated %32, bits 16 to 6399
+ r[0][bits 0 to 15]# ∈ {270729319} or UNINITIALIZED%32, bits 0 to 15
+ [bits 16 to 6431]# ∈
+ {270729319} or UNINITIALIZED repeated %32, bits 16 to 6431
+ t[0][bits 0 to 15]# ∈ {270729319} or UNINITIALIZED%32, bits 0 to 15
+ [bits 16 to 31999999]# ∈
+ {270729319} or UNINITIALIZED repeated %32, bits 16 to 31999999
p ∈ {{ &t + [0..3999996],0%4 }}
len_u ∈ {1}
len_r ∈ {1}
@@ -1339,13 +1345,12 @@
z2 ∈ {0}
[eva:final-states] Values at end of function memchr_initialization:
c ∈ {0}
- empty_or_uninitialized[0] ∈ {0} or UNINITIALIZED
+ empty_or_uninitialized[0] ∈ {0}
z1 ∈ {0}
- s[0] ∈ {1} or UNINITIALIZED
+ s[0] ∈ {1}
[1] ∈ {0}
z2 ∈ {1}
- t[0..1] ∈ {10}
- [2] ∈ {10} or UNINITIALIZED
+ t[0..2] ∈ {10}
[3] ∈ {0}
z3 ∈ {3}
[eva:final-states] Values at end of function memchr_misc:
@@ -1381,7 +1386,7 @@
s1 ∈ {{ "mno\000pqr" ; "MNOP\000QRS" }}
sz5 ∈ {3; 4}
sz6 ∈ {3; 4}
- maybe_init[0] ∈ {65} or UNINITIALIZED
+ maybe_init[0] ∈ {65}
[1] ∈ {0}
sz8 ∈ {1}
[eva:final-states] Values at end of function memchr_misc_array: