From 2b72e5f86712df35076d989b204838bf86444e93 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 15 Feb 2021 19:31:04 +0100
Subject: [PATCH] [Eva] Changes the type of cvalue builtins.
- [cacheable] is given at the registration of a builtin, and not separately
for each result of the builtin.
- Removes the offsetmap for the arguments: no builtin were using it anyway.
- Returns a Cvalue.V.t for the result instead of an offsetmap.
- Builtins can also return:
+ only the value of the result, in which case the post-state from the
interpretation of the specification is used with the resulting value
computed by the builtin.
+ only the post-states for functions with no froms dependency (other than the
result and arguments) and no write of local variable addresses.
Simplifies some builtins accordingly.
---
src/plugins/value/domains/cvalue/builtins.ml | 157 ++++++++--------
src/plugins/value/domains/cvalue/builtins.mli | 40 ++--
.../value/domains/cvalue/builtins_float.ml | 92 ++++------
.../value/domains/cvalue/builtins_malloc.ml | 85 ++++-----
.../value/domains/cvalue/builtins_memory.ml | 171 +++++++-----------
.../value/domains/cvalue/builtins_misc.ml | 41 ++---
.../value/domains/cvalue/builtins_print_c.ml | 16 +-
.../value/domains/cvalue/builtins_split.ml | 103 ++++-------
.../value/domains/cvalue/builtins_string.ml | 60 +++---
.../value/domains/cvalue/builtins_string.mli | 6 +-
.../domains/cvalue/builtins_watchpoint.ml | 13 +-
src/plugins/value/engine/compute_functions.ml | 7 +-
src/plugins/value/legacy/eval_terms.ml | 66 +++----
src/plugins/value/utils/value_util.ml | 2 +-
src/plugins/value/utils/value_util.mli | 2 +-
15 files changed, 362 insertions(+), 499 deletions(-)
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index 4791f793d20..5ef2abd57a4 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -21,7 +21,6 @@
(**************************************************************************)
open Cil_types
-open Cvalue
exception Invalid_nb_of_args of int
exception Outside_builtin_possibilities
@@ -29,20 +28,18 @@ exception Outside_builtin_possibilities
type builtin_type = unit -> typ * typ list
type cacheable = Eval.cacheable
-type call_result = {
- c_values:
- (Cvalue.V_Offsetmap.t option
- * Cvalue.Model.t)
- list;
+type full_result = {
+ c_values: (Cvalue.V.t option * Cvalue.Model.t) list;
c_clobbered: Base.SetLattice.t;
- c_cacheable: cacheable;
- c_from: (Function_Froms.froms * Locations.Zone.t) option
+ c_from: (Function_Froms.froms * Locations.Zone.t) option;
}
-type builtin =
- Cvalue.Model.t ->
- (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
- call_result
+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
@@ -58,22 +55,24 @@ 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 =
+let register_builtin name ?replace ?typ cacheable f =
Value_parameters.register_builtin name;
- Hashtbl.replace table name (f, typ, 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, name)
+ | Some fname -> Hashtbl.replace table fname builtin
(* The functions in _builtin must only return the 'Always' builtins *)
let builtin_names_and_replacements () =
let stand_alone, replacements =
- Hashtbl.fold (fun name (_, _, builtin_name) (acc1, acc2) ->
- if name = builtin_name
- then name :: acc1, acc2
- else acc1, (name, builtin_name) :: 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
@@ -107,6 +106,10 @@ let () =
raise Cmdline.Exit
end)
+(* -------------------------------------------------------------------------- *)
+(* --- Prepare builtins for an analysis --- *)
+(* -------------------------------------------------------------------------- *)
+
(* Returns the specification of a builtin, used to evaluate preconditions
and to transfer the states of other domains. *)
let find_builtin_specification kf =
@@ -150,7 +153,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
@@ -158,7 +161,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
@@ -169,9 +172,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 ();
@@ -179,35 +182,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) ->
+ (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 ->
@@ -215,68 +216,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
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
| 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 clob = Locals_scoping.bottom () in
- Locals_scoping.remember_bases_with_locals clob res.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.c_values in
- list, res.c_cacheable
(*
Local Variables:
diff --git a/src/plugins/value/domains/cvalue/builtins.mli b/src/plugins/value/domains/cvalue/builtins.mli
index ec4920b758b..812503988ba 100644
--- a/src/plugins/value/domains/cvalue/builtins.mli
+++ b/src/plugins/value/domains/cvalue/builtins.mli
@@ -20,29 +20,30 @@
(* *)
(**************************************************************************)
-(** 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
-type builtin_type = unit -> Cil_types.typ * Cil_types.typ list
+(* Signature of a builtin: type of the result, and type of the arguments. *)
+type builtin_type = unit -> typ * typ list
type cacheable = Eval.cacheable
-type call_result = {
- c_values:
- (Cvalue.V_Offsetmap.t option
- * Cvalue.Model.t)
- list;
+type full_result = {
+ c_values: (Cvalue.V.t option * Cvalue.Model.t) list;
c_clobbered: Base.SetLattice.t;
- c_cacheable: cacheable;
- c_from: (Function_Froms.froms * Locations.Zone.t) option
+ c_from: (Function_Froms.froms * Locations.Zone.t) option;
}
-type builtin =
- Cvalue.Model.t ->
- (Cil_types.exp * Cvalue.V.t * Cvalue.V_Offsetmap.t) list ->
- call_result
+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
(** [register_builtin name ?replace ?typ f] registers the ocaml function [f]
as a builtin to be used instead of the C function of name [name].
@@ -51,8 +52,7 @@ type builtin =
If [typ] is provided, consistency between the expected [typ] and the type of
the C function is checked before using the builtin. *)
val register_builtin:
- string -> ?replace:string ->
- ?typ:builtin_type -> builtin -> unit
+ string -> ?replace:string -> ?typ:builtin_type -> cacheable -> builtin -> unit
(** Prepares the builtins to be used for an analysis. Must be called at the
beginning of each Eva analysis. Warns about builtins of incompatible types,
@@ -66,21 +66,21 @@ val prepare_builtins: unit -> unit
val clobbered_set_from_ret: Cvalue.Model.t -> Cvalue.V.t -> Base.SetLattice.t
type call = (Precise_locs.precise_location, Cvalue.V.t) Eval.call
-type result = Cvalue.Model.t * Locals_scoping.clobbered_set
+type result = Cvalue_domain.State.t
(** Is a given function replaced by a builtin? *)
-val is_builtin_overridden: Cil_types.kernel_function -> bool
+val is_builtin_overridden: kernel_function -> bool
(** Returns the cvalue builtin for a function, if any. Also returns the name of
the builtin and the specification of the function; the preconditions must be
evaluated along with the builtin.
[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 * 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 888c25c53f0..d7d43b2281f 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
- { Builtins.c_values =
- if V.is_bottom r then []
- else [wrap_fk r fk, state ];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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
- { Builtins.c_values =
- if V.is_bottom r then []
- else [wrap_fk r fk, state ];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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 363f33aa4c0..b71595f745f 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
- { Builtins.c_values = c_values ;
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Eval.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
- { Builtins.c_values;
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Eval.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
- { Builtins.c_values = [];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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
- { Builtins.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = Some changed;
- c_cacheable = Eval.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
- { Builtins.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = Some changed;
- c_cacheable = Eval.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
- { Builtins.c_values;
- c_clobbered = Builtins.clobbered_set_from_ret new_state ret;
- c_cacheable = Eval.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. *)
- { Builtins.c_values = [] ;
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Eval.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;
- { Builtins.c_values = [None,state] ;
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Eval.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 037cca4f7cf..b4ca1334dda 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
- ();
- { Builtins.c_values =
- [ Eval_op.wrap_int Cvalue.V.singleton_one, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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 *) ->
- { Builtins.c_values = [Eval_op.wrap_int Cvalue.V.zero_or_one, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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
- { Builtins.c_values = [Eval_op.wrap_size_t value, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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 *)
- { Builtins.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 = Eval.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
- { Builtins.c_values = [ None, Cvalue.Model.bottom];
- c_clobbered = Base.SetLattice.bottom;
- c_from = Some(c_from, sure_zone);
- c_cacheable = Eval.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
- { Builtins.c_values = [Eval_op.wrap_ptr dst, new_state'];
- c_clobbered = Base.SetLattice.bottom;
- c_from = Some(c_from,sure_zone);
- c_cacheable = Eval.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
- { Builtins.c_values = [Eval_op.wrap_ptr dst, state'];
- c_clobbered = Base.SetLattice.bottom;
- c_from = Some (c_from,dst_zone);
- c_cacheable = Eval.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;
- { Builtins.c_values = !r;
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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
- { Builtins.c_values = [ Eval_op.wrap_int v, state ];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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 678df158bcf..6d1fdba911a 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
- { Builtins.c_values = [ None, state ] ;
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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 0a9ed1a950e..e7eb5094ef0 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;
- { Builtins.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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;
- { Builtins.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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 026c9c1aba5..2f349b60456 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
- { Builtins.c_values = [Eval_op.wrap_long_long nb, state];
- c_clobbered = Base.SetLattice.empty;
- c_cacheable = Eval.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 () =
- Builtins.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
- { Builtins.c_values = [Eval_op.wrap_long_long nb, state];
- c_clobbered = Base.SetLattice.empty;
- c_cacheable = Eval.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 () =
- Builtins.register_builtin "Frama_C_abstract_min" (frama_c_min_max fst);
- Builtins.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
- { Builtins.c_values = states;
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Eval.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;
- { Builtins.c_values = [(None, state)];
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Eval.Cacheable;
- c_from = None;
- }
- end
+ [state]
+ in
+ Builtins.States states
| _ ->
Value_parameters.warning ~current:true ~once:true
"Cannot interpret split directive. Ignoring";
- { Builtins.c_values = [(None, state)];
- c_clobbered = Base.SetLattice.bottom;
- c_cacheable = Eval.Cacheable;
- c_from = None;
- }
+ Builtins.States [state]
let () =
- Builtins.register_builtin "Frama_C_builtin_split" (aux_split split_v)
-let () =
- Builtins.register_builtin "Frama_C_builtin_split_pointer" (aux_split split_pointer)
-let () =
- Builtins.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 2bdf3bc24c4..29c8d6f6bbb 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
- { Builtins.c_values = [ res_cvalue ];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.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 632d0f94b39..b590cc56d0e 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 6eb8f97c252..f91e4314be7 100644
--- a/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
+++ b/src/plugins/value/domains/cvalue/builtins_watchpoint.ml
@@ -49,7 +49,7 @@ 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
@@ -76,10 +76,7 @@ let add_watch make_watch state actuals =
then
watch_table :=
(new_watchpoint dst_e loc target_w number) :: current;
- { Builtins.c_values = [None, state];
- c_clobbered = Base.SetLattice.bottom;
- c_from = None;
- c_cacheable = Eval.Cacheable }
+ Builtins.States [state]
| _ -> raise (Builtins.Invalid_nb_of_args 4)
let make_watch_value target_value = Value target_value
@@ -93,10 +90,10 @@ let make_watch_cardinal target_value =
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 aa0db0be304..000e3980103 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -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
@@ -300,8 +300,9 @@ module Make (Abstract: Abstractions.Eva) = struct
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/legacy/eval_terms.ml b/src/plugins/value/legacy/eval_terms.ml
index 462e57405d3..66d7c864869 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 436f349721f..1e92201d815 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 dc1e6de459c..644fa87438d 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
--
GitLab