From e1f4a9314ef97415b8ee1b37f65edf329bdd23b5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 3 Apr 2020 19:18:58 +0200
Subject: [PATCH] [Eva] Allocation builtins: renames some functions.
---
.../value/domains/cvalue/builtins_malloc.ml | 42 +++++++++----------
1 file changed, 21 insertions(+), 21 deletions(-)
diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index 5b396ffa99a..6af07c51781 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -315,7 +315,7 @@ let pp_validity fmt (v1, v2) =
Returns the new base, and its maximum validity.
Note that [_state] is not used, but it is present to ensure a compatible
signature with [alloc_by_stack]. *)
-let alloc_abstract weak deallocation prefix sizev _state =
+let alloc_fresh weak deallocation prefix sizev _state =
let stack = call_stack_no_wrappers () in
let tsize = guess_intended_malloc_type stack sizev (weak = Strong) in
let type_base = type_from_nb_elems tsize in
@@ -373,7 +373,7 @@ let string_of_region = function
| Base.Alloca -> "via alloca"
(* Only called when the 'weakest base' needs to be allocated. *)
-let alloc_imprecise_weakest_alloc region =
+let create_weakest_base region =
let stack = [ fst (Globals.entry_point ()), Kglobal ] in
let type_base =
TArray (Cil.charType, None, Cil.empty_size_cache (), [])
@@ -393,14 +393,14 @@ let alloc_imprecise_weakest_alloc region =
new_base, max_alloc
(* used by calloc_abstract *)
-let alloc_imprecise_weakest_abstract region =
+let alloc_weakest_base region =
let memo =
match region with
| Base.Malloc -> MallocedSingleMalloc.memo
| Base.VLA -> MallocedSingleVLA.memo
| Base.Alloca -> MallocedSingleAlloca.memo
in
- memo (fun () -> alloc_imprecise_weakest_alloc region)
+ memo (fun () -> create_weakest_base region)
(* Variables that have been returned by a call to an allocation function
at this callstack. The first allocated variable is at the top of the
@@ -444,7 +444,7 @@ let update_variable_validity ?(make_weak=false) base sizev =
base, max_valid_bits
| _ -> Value_parameters.fatal "base is not Allocated: %a" Base.pretty base
-let alloc_by_stack_aux region prefix sizev state =
+let alloc_by_stack region prefix sizev state =
let stack = call_stack_no_wrappers () in
let max_level = Value_parameters.MallocLevel.get () in
let all_vars =
@@ -454,7 +454,7 @@ let alloc_by_stack_aux region prefix sizev state =
let rec aux nb vars =
match vars with
| [] -> (* must allocate a new variable *)
- let b, _ as r = alloc_abstract Strong region prefix sizev state in
+ let b, _ as r = alloc_fresh Strong region prefix sizev state in
MallocedByStack.replace stack (all_vars @ [b]);
r
| b :: q ->
@@ -490,21 +490,21 @@ let register_malloc ?replace name ?returns_null allocate_base =
let () =
register_malloc "malloc_fresh"
- (alloc_abstract Strong Base.Malloc "malloc");
+ (alloc_fresh Strong Base.Malloc "malloc");
register_malloc "malloc_fresh_weak"
- (alloc_abstract Weak Base.Malloc "malloc");
+ (alloc_fresh Weak Base.Malloc "malloc");
register_malloc ~replace:"malloc" "malloc_by_stack"
- (alloc_by_stack_aux Base.Malloc "malloc");
+ (alloc_by_stack Base.Malloc "malloc");
register_malloc ~replace:"__fc_vla_alloc" "vla_alloc_by_stack"
- (alloc_by_stack_aux Base.VLA "malloc") ~returns_null:false;
+ (alloc_by_stack Base.VLA "malloc") ~returns_null:false;
register_malloc ~replace:"alloca" "alloca"
- (alloc_by_stack_aux Base.Alloca "alloca") ~returns_null:false;
+ (alloc_by_stack Base.Alloca "alloca") ~returns_null:false;
register_malloc "malloc_imprecise"
- (fun _ _ -> alloc_imprecise_weakest_abstract Base.Malloc);
+ (fun _ _ -> alloc_weakest_base Base.Malloc);
register_malloc "vla_alloc_imprecise"
- (fun _ _ -> alloc_imprecise_weakest_abstract Base.VLA);
+ (fun _ _ -> alloc_weakest_base Base.VLA);
register_malloc "alloca_imprecise"
- (fun _ _ -> alloc_imprecise_weakest_abstract Base.Alloca)
+ (fun _ _ -> alloc_weakest_base Base.Alloca)
(* --------------------------------- Calloc --------------------------------- *)
@@ -559,12 +559,12 @@ let register_calloc ?replace name allocate_base =
Builtins.register_builtin ?replace name builtin ~typ
let () =
- register_calloc "calloc_fresh" (alloc_abstract Strong Base.Malloc);
- register_calloc "calloc_fresh_weak" (alloc_abstract Weak Base.Malloc);
+ register_calloc "calloc_fresh" (alloc_fresh Strong Base.Malloc);
+ register_calloc "calloc_fresh_weak" (alloc_fresh Weak Base.Malloc);
register_calloc ~replace:"calloc" "calloc_by_stack"
- (alloc_by_stack_aux Base.Malloc);
+ (alloc_by_stack Base.Malloc);
register_calloc "calloc_imprecise"
- (fun _ _ _ -> alloc_imprecise_weakest_abstract Base.Malloc)
+ (fun _ _ _ -> alloc_weakest_base Base.Malloc)
(* ---------------------------------- Free ---------------------------------- *)
@@ -761,8 +761,8 @@ let realloc_alloc_copy weak bases_to_realloc null_in_arg sizev state =
let base, max_valid =
let prefix = "realloc" in
match weak with
- | Strong -> alloc_abstract Strong Base.Malloc prefix sizev state
- | Weak -> alloc_by_stack_aux Base.Malloc prefix sizev state
+ | Strong -> alloc_fresh Strong Base.Malloc prefix sizev state
+ | Weak -> alloc_by_stack Base.Malloc prefix sizev state
in
(* Make sure that [ret] will be present in the result: we bind it at least
to bottom everywhere *)
@@ -821,7 +821,7 @@ let realloc_multiple bases null size state =
else res
let realloc_imprecise_weakest _bases _null _size state =
- let new_base, max_alloc = alloc_imprecise_weakest_abstract Base.Malloc in
+ let new_base, max_alloc = alloc_weakest_base Base.Malloc in
let state = add_uninitialized state new_base max_alloc in
let ret = V.inject new_base Ival.zero in
ret, state
--
GitLab