From 232282e67a20b23f943220f68630532799d4e07f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 10 Jul 2023 17:31:47 +0200
Subject: [PATCH] [Eva] The allocation builtins use the new callstack type.
---
.../eva/domains/cvalue/builtins_malloc.ml | 73 +++++++++----------
.../eva/domains/cvalue/builtins_malloc.mli | 8 +-
.../eva/domains/cvalue/builtins_memory.ml | 2 +-
.../eva/domains/cvalue/cvalue_transfer.ml | 5 +-
4 files changed, 39 insertions(+), 49 deletions(-)
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index a0072d14ed6..7700235e157 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -38,7 +38,7 @@ let wkey_imprecise_alloc = Self.register_warn_category
module Base_hptmap = Hptmap.Make
(Base.Base)
- (Value_types.Callstack)
+ (Callstack)
(Hptmap.Comp_unused)
(struct let v = [ [ ] ] end)
(struct let l = [ Ast.self ] end)
@@ -57,9 +57,8 @@ let () = Ast.add_monotonic_state Dynamic_Alloc_Bases.self
(* -------------------------- Auxiliary functions -------------------------- *)
let current_call_site () =
- match Eva_utils.legacy_call_stack () with
- | (_kf, Kstmt stmt) :: _ -> stmt
- | _ -> Cil.dummyStmt
+ let callsite = Callstack.top_callsite (Eva_utils.current_call_stack ()) in
+ Option.value ~default:Cil.dummyStmt callsite
(* Remove some parts of the callstack:
- Remove the bottom of the call tree until we get to the call site
@@ -67,29 +66,26 @@ let current_call_site () =
these call site correspond to a different use of a malloc function,
so it is interesting to keep their bases separated. *)
let call_stack_no_wrappers () =
- let stack = Eva_utils.legacy_call_stack () in
- assert (stack != []);
- let wrappers = Parameters.AllocFunctions.get() in
+ let cs = Eva_utils.current_call_stack () in
+ let wrappers = Parameters.AllocFunctions.get () in
let rec bottom_filter = function
- | [] -> assert false
- | [_] as stack -> stack (* Do not empty the stack completely *)
+ | [] | [_] as stack -> stack
| (kf,_)::((kf', _):: _ as rest) as stack ->
- if Datatype.String.Set.mem (Kernel_function.get_name kf) wrappers then
- if Datatype.String.Set.mem (Kernel_function.get_name kf') wrappers then
- bottom_filter rest
- else
- stack
- else
- stack
+ if Datatype.String.Set.mem (Kernel_function.get_name kf) wrappers
+ && Datatype.String.Set.mem (Kernel_function.get_name kf') wrappers
+ then bottom_filter rest
+ else stack
in
- bottom_filter stack
+ { cs with stack = bottom_filter cs.stack }
-let register_malloced_base ?(stack=call_stack_no_wrappers ()) b =
- let stack_without_top = List.tl stack in
+let register_malloced_base ~stack b =
+ let stack_without_top =
+ Option.value ~default:stack (Callstack.pop stack)
+ in
Dynamic_Alloc_Bases.set
(Base_hptmap.add b stack_without_top (Dynamic_Alloc_Bases.get ()))
-let fold_dynamic_bases (f: Base.t -> Value_types.Callstack.t -> 'a -> 'a) init =
+let fold_dynamic_bases (f: Base.t -> Callstack.t -> 'a -> 'a) init =
Base_hptmap.fold f (Dynamic_Alloc_Bases.get ()) init
let is_automatically_deallocated base =
@@ -120,20 +116,17 @@ let extract_size sizev_bytes =
(* Name of the base that will be given to a malloced variable, determined
using the callstack. *)
-let base_name prefix stack =
+let base_name prefix cs =
let stmt_line stmt = (fst (Cil_datatype.Stmt.loc stmt)).Filepath.pos_lnum in
- match stack with
- | [] -> assert false
- | [kf, Kglobal] -> (* Degenerate case *)
- Format.asprintf "__%s_%a" prefix Kernel_function.pretty kf
- | (_, Kglobal) :: _ :: _ -> assert false
- | (_, Kstmt callsite) :: qstack ->
+ match cs.Callstack.stack with
+ | [] ->
+ (* Degenerate case *)
+ Format.asprintf "__%s_%a" prefix Kernel_function.pretty cs.entry_point
+ | (_, callsite) :: qstack ->
(* Use the whole call-stack to generate the name *)
let rec loop_full = function
- | [_, Kglobal] -> Format.sprintf "_%s" (Kernel.MainFunction.get ())
- | (_, Kglobal) :: _ :: _ -> assert false
- | [] -> assert false (* impossible, we should have seen a Kglobal *)
- | (kf, Kstmt line)::b ->
+ | [] -> Format.sprintf "_%s" (Kernel_function.get_name cs.entry_point)
+ | (kf, line) :: b ->
let line = stmt_line line in
let node_str = Format.asprintf "_l%d__%a"
line Kernel_function.pretty kf
@@ -141,14 +134,14 @@ let base_name prefix stack =
(loop_full b) ^ node_str
in
(* Use only the name of the caller to malloc for the name *)
- let caller = function
- | [] -> assert false (* caught above *)
- | (kf, _) :: _ -> Format.asprintf "_%a" Kernel_function.pretty kf
+ let caller =
+ let kf = Callstack.top_kf { cs with stack = qstack } in
+ Format.asprintf "_%a" Kernel_function.pretty kf
in
let full_name = false in
Format.asprintf "__%s%s_l%d"
prefix
- (if full_name then loop_full qstack else caller qstack)
+ (if full_name then loop_full qstack else caller)
(stmt_line callsite)
type var = Weak | Strong
@@ -217,7 +210,7 @@ let guess_intended_malloc_type stack sizev constant_size =
| _ -> raise Exit
in
try
- match snd (List.hd stack) with
+ match snd (Callstack.top_call stack) with
| Kstmt {skind = Instr (Call (Some lv, _, _, _))} ->
mk_typed_size (Cil.typeOfLval lv)
| Kstmt {skind = Instr(Local_init(vi, _, _))} -> mk_typed_size vi.vtype
@@ -380,7 +373,7 @@ let string_of_region = function
(* Only called when the 'weakest base' needs to be allocated. *)
let create_weakest_base region =
- let stack = [ fst (Globals.entry_point ()), Kglobal ] in
+ let stack = { (Eva_utils.current_call_stack ()) with stack = [] } in
let type_base =
TArray (Cil.charType, None, [])
in
@@ -413,8 +406,8 @@ let alloc_weakest_base region =
stack. Currently, the callstacks are truncated according to
[-eva-alloc-functions]. *)
module MallocedByStack = (* varinfo list Callstack.hashtbl *)
- State_builder.Hashtbl(Value_types.Callstack.Hashtbl)
- (Datatype.List(Base))
+ State_builder.Hashtbl (Callstack.Hashtbl)
+ (Datatype.List (Base))
(struct
let name = "Value.Builtins_malloc.MallocedByStack"
let size = 17
@@ -686,7 +679,7 @@ let free_automatic_bases stack state =
let bases_to_free =
Base_hptmap.fold (fun base stack' acc ->
if is_automatically_deallocated base &&
- Value_types.Callstack.equal stack stack'
+ Callstack.equal stack stack'
then Base.Hptset.add base acc
else acc
) (Dynamic_Alloc_Bases.get ()) Base.Hptset.empty
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.mli b/src/plugins/eva/domains/cvalue/builtins_malloc.mli
index 8cd4f9ddabf..399b01a97c6 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.mli
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.mli
@@ -23,7 +23,7 @@
(** Dynamic allocation related builtins.
Most functionality is exported as builtins. *)
-val fold_dynamic_bases: (Base.t -> Value_types.Callstack.t -> 'a -> 'a) -> 'a -> 'a
+val fold_dynamic_bases: (Base.t -> Callstack.t -> 'a -> 'a) -> 'a -> 'a
(** [fold_dynamic_bases f init] folds [f] to each dynamically allocated base,
with initial accumulator [init].
Note that this also includes bases created by [alloca] and [VLAs]. *)
@@ -34,7 +34,7 @@ val alloc_size_ok: Cvalue.V.t -> Alarmset.status
small enough, [False] that the allocation is guaranteed to fail (because
the size is always greater than SIZE_MAX). *)
-val free_automatic_bases: Value_types.Callstack.t -> Cvalue.Model.t -> Cvalue.Model.t
+val free_automatic_bases: Callstack.t -> Cvalue.Model.t -> Cvalue.Model.t
(** Performs the equivalent of [free] for each location that was allocated via
[alloca()] in the current function (as per [Eva_utils.call_stack ()]).
This function must be called during finalization of a function call. *)
@@ -44,7 +44,3 @@ val freeable: Cvalue.V.t -> Abstract_interp.truth
value points to an allocated memory block that can be safely released using
the C function free. Note that \freeable(\null) does not hold, despite NULL
being a valid argument to the C function free. *)
-
-(**/**)
-val register_malloced_base: ?stack:Value_types.Callstack.t -> Base.t -> unit
-(* Should not be used by casual users. *)
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index fae795db083..4a34203eed4 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -92,7 +92,7 @@ let memcpy_check_indeterminate_offsetmap offsm =
currently called function. *)
let deps_nth_arg n =
let open Function_Froms in
- let (kf,_) = List.hd (Eva_utils.legacy_call_stack()) in
+ let kf = Callstack.top_kf (Eva_utils.current_call_stack ()) in
try
let vi = List.nth (Kernel_function.get_formals kf) n in
Deps.add_data_dep Deps.bottom (Locations.zone_of_varinfo vi)
diff --git a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
index 52fb6f70d14..222f8bbe683 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
+++ b/src/plugins/eva/domains/cvalue/cvalue_transfer.ml
@@ -214,8 +214,9 @@ let finalize_call stmt call _recursion ~pre:_ ~post:state =
To minimize computations, only do it for function definitions. *)
let state' =
if Kernel_function.is_definition call.kf then
- let stack = (call.kf, Kstmt stmt) :: (Eva_utils.legacy_call_stack ()) in
- Builtins_malloc.free_automatic_bases stack state
+ let callstack = Eva_utils.current_call_stack () in
+ let callstack = Callstack.push call.kf stmt callstack in
+ Builtins_malloc.free_automatic_bases callstack state
else state
in
`Value state'
--
GitLab