diff --git a/src/plugins/value/domains/cvalue/builtins_malloc.ml b/src/plugins/value/domains/cvalue/builtins_malloc.ml
index 727ef69ca5040a887949e0e02cbe633d4238e380..dee1382281c94136b19e06645315db71d93de60e 100644
--- a/src/plugins/value/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/value/domains/cvalue/builtins_malloc.ml
@@ -30,6 +30,9 @@ let dkey = Value_parameters.register_category "malloc"
let wkey_weak_alloc = Value_parameters.register_warn_category "malloc:weak"
let () = Value_parameters.set_warn_status wkey_weak_alloc Log.Winactive
+let wkey_imprecise_alloc = Value_parameters.register_warn_category
+ "malloc:imprecise"
+
(** {1 Dynamically allocated bases} *)
module Base_hptmap = Hptmap.Make
@@ -363,12 +366,99 @@ let () =
(alloc_fresh Weak Base.Malloc)
~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
+module Base_with_Size = Datatype.Pair (Base.Base) (Datatype.Integer)
+
+(* Extremely aggressive and imprecise allocation: a single weak base for each
+ region. *)
+module MallocedSingleMalloc =
+ State_builder.Option_ref (Base_with_Size)
+ (struct
+ let name = "Value.Builtins_malloc.MallocedSingleMalloc"
+ let dependencies = [Ast.self]
+ end)
+let () = Ast.add_monotonic_state MallocedSingleMalloc.self
+
+module MallocedSingleVLA =
+ State_builder.Option_ref (Base_with_Size)
+ (struct
+ let name = "Value.Builtins_malloc.MallocedSingleVLA"
+ let dependencies = [Ast.self]
+ end)
+let () = Ast.add_monotonic_state MallocedSingleVLA.self
+
+module MallocedSingleAlloca =
+ State_builder.Option_ref (Base_with_Size)
+ (struct
+ let name = "Value.Builtins_malloc.MallocedSingleAlloca"
+ let dependencies = [Ast.self]
+ end)
+let () = Ast.add_monotonic_state MallocedSingleAlloca.self
+
+let string_of_region = function
+ | Base.Malloc -> "via malloc/calloc/realloc"
+ | Base.VLA -> "related to variable-length arrays"
+ | Base.Alloca -> "via alloca"
+
+(* Only called when the 'weakest base' needs to be allocated. *)
+let alloc_imprecise_weakest_alloc region =
+ let stack = [ fst (Globals.entry_point ()), Kglobal ] in
+ let type_base =
+ TArray (Cil.charType, None, Cil.empty_size_cache (), [])
+ in
+ let var = create_new_var stack "alloc" type_base Weak in
+ Value_parameters.warning ~wkey:wkey_imprecise_alloc ~current:true ~once:true
+ "allocating a single weak variable for ALL dynamic allocations %s: %a"
+ (string_of_region region) Printer.pp_varinfo var;
+ let min_alloc = Int.minus_one in
+ let max_alloc = Bit_utils.max_bit_address () in
+ let variable_v =
+ Base.create_variable_validity ~weak:true ~min_alloc ~max_alloc
+ in
+ let new_base = Base.register_allocated_var var region (Base.Variable variable_v) in
+ register_malloced_base ~stack new_base;
+ new_base, max_alloc
+
+(* used by calloc_abstract *)
+let alloc_imprecise_weakest_abstract 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)
+
+let alloc_imprecise_weakest_aux region _stack _prefix _sizev state =
+ let new_base, max_alloc = alloc_imprecise_weakest_abstract region in
+ let new_state = add_uninitialized state new_base max_alloc in
+ let ret = V.inject new_base Ival.zero in
+ ret, new_state
+
+let alloc_imprecise_weakest ?returns_null region state actuals =
+ match actuals with
+ | [_, _size, _] ->
+ begin
+ let ret, new_state = alloc_imprecise_weakest_aux region [] "" _size state 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;
+ }
+ end
+ | _ -> raise (Builtins.Invalid_nb_of_args 1)
+
+let () = Builtins.register_builtin
+ "Frama_C_malloc_imprecise" (alloc_imprecise_weakest Base.Malloc)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
+
+let zero_to_max_bytes () = Ival.inject_range
+ (Some Integer.zero) (Some (Bit_utils.max_byte_size ()))
+
let alloc_size_ok intended_size =
try
let size = Cvalue.V.project_ival intended_size in
- let ok_size =
- Ival.inject_range (Some Integer.zero) (Some (Bit_utils.max_byte_size ()))
- in
+ let ok_size = zero_to_max_bytes () in
if Ival.is_included size ok_size then Alarmset.True
else if Ival.intersects size ok_size then Alarmset.Unknown
else Alarmset.False
@@ -422,7 +512,7 @@ let () =
(* 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
stack. Currently, the callstacks are truncated according to
- [-val-malloc-functions]. *)
+ [-eva-alloc-functions]. *)
module MallocedByStack = (* varinfo list Callstack.hashtbl *)
State_builder.Hashtbl(Value_types.Callstack.Hashtbl)
(Datatype.List(Base))
@@ -510,10 +600,18 @@ let () = Builtins.register_builtin
~replace:"__fc_vla_alloc" "Frama_C_vla_alloc_by_stack"
(alloc_by_stack Base.VLA ~returns_null:false)
~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
+let () = Builtins.register_builtin
+ "Frama_C_vla_alloc_imprecise"
+ (alloc_imprecise_weakest Base.VLA ~returns_null:false)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
let () = Builtins.register_builtin
~replace:"alloca" "Frama_C_alloca"
(alloc_by_stack ~prefix:"alloca" Base.Alloca ~returns_null:false)
~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
+let () = Builtins.register_builtin
+ "Frama_C_alloca_imprecise"
+ (alloc_imprecise_weakest Base.Alloca ~returns_null:false)
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf]))
(* Equivalent to [alloc_by_stack], but for [calloc]. *)
let calloc_by_stack : Db.Value.builtin = fun state actuals ->
@@ -524,6 +622,18 @@ let () = Builtins.register_builtin
~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
Cil.theMachine.Cil.typeOfSizeOf]))
+(* Equivalent to [malloc_imprecise_weakest], but for [calloc]. *)
+let calloc_imprecise_weakest : Db.Value.builtin = fun state actuals ->
+ let calloc_f _stack _prefix _sizev _state =
+ alloc_imprecise_weakest_abstract Base.Malloc
+ in
+ calloc_abstract calloc_f state actuals
+
+let () = Builtins.register_builtin
+ "Frama_C_calloc_imprecise" calloc_imprecise_weakest
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf;
+ Cil.theMachine.Cil.typeOfSizeOf]))
+
(** {1 Free} *)
(* Change all references to bases into ESCAPINGADDR into the given state,
@@ -819,6 +929,33 @@ let () = Builtins.register_builtin
~typ:(fun () -> (Cil.voidPtrType, [Cil.voidPtrType;
Cil.theMachine.Cil.typeOfSizeOf]))
+let realloc_imprecise_weakest state args = match args with
+ | [ (_,ptr,_); (_,_size,_) ] ->
+ let (bases, card_ok, _null) = resolve_bases_to_free ptr in
+ if card_ok > 0 then
+ let orig_state = state in
+ let ret, state = alloc_imprecise_weakest_aux Base.Malloc [] "" _size state in
+ (* free old bases. *)
+ let state, changed = free_aux state ~strong:false bases in
+ let c_values = wrap_fallible_alloc ret orig_state state in
+ { Value_types.c_values;
+ c_clobbered = Builtins.clobbered_set_from_ret state ret;
+ c_cacheable = Value_types.NoCacheCallers;
+ c_from = Some changed;
+ }
+ else (* Invalid call. *)
+ { Value_types.c_values = [] ;
+ c_clobbered = Base.SetLattice.bottom;
+ c_cacheable = Value_types.NoCacheCallers;
+ c_from = None;
+ }
+ | _ -> raise (Builtins.Invalid_nb_of_args 2)
+
+let () = Builtins.register_builtin
+ "Frama_C_realloc_imprecise" realloc_imprecise_weakest
+ ~typ:(fun () -> (Cil.voidPtrType, [Cil.voidPtrType;
+ Cil.theMachine.Cil.typeOfSizeOf]))
+
(** {1 Leak detection} *)
(* Experimental, not to be released, leak detection built-in. *)
diff --git a/tests/builtins/calloc.c b/tests/builtins/calloc.c
index 648a4b4af03809048ffa6542498385caab9ecdbc..391526efc854f48c1a227508470978787b60aa80 100644
--- a/tests/builtins/calloc.c
+++ b/tests/builtins/calloc.c
@@ -4,8 +4,8 @@
STDOPT: #"-eva-no-builtins-auto -eva-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_by_stack"
STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_fresh"
STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_by_stack"
+ STDOPT: #"-eva-no-builtins-auto -eva-no-alloc-returns-null -eva-builtin calloc:Frama_C_calloc_imprecise"
*/
-
#include <stdlib.h>
#include <stdint.h>
diff --git a/tests/builtins/malloc.c b/tests/builtins/malloc.c
index c62203fa9ddc252a00f91fa13647a74520e169bf..af2dbc58d5b2eff3d0a49890a02bf98bbfc295c7 100644
--- a/tests/builtins/malloc.c
+++ b/tests/builtins/malloc.c
@@ -4,7 +4,7 @@
#include <stddef.h>
void *Frama_C_malloc_by_stack(size_t i);
void *Frama_C_malloc_fresh(size_t i);
-
+void *Frama_C_malloc_imprecise(size_t i);
void main(int c) {
int x;
int *s;
@@ -30,5 +30,10 @@ void main(int c) {
*r = 1;
*(r+2) = 3;
+ int *mw = Frama_C_malloc_imprecise(42);
+ *mw = 1;
+ int *mw2 = Frama_C_malloc_imprecise(42);
+ *mw2 = 2;
+
// *s = 1;
}
diff --git a/tests/builtins/oracle/calloc.5.res.oracle b/tests/builtins/oracle/calloc.5.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..679c1f964b2efcdc39a9b52a8af80ba2a8d09bd6
--- /dev/null
+++ b/tests/builtins/oracle/calloc.5.res.oracle
@@ -0,0 +1,57 @@
+[kernel] Parsing tests/builtins/calloc.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ nondet ∈ [--..--]
+[eva] tests/builtins/calloc.c:14:
+ Call to builtin Frama_C_calloc_imprecise for function calloc
+[eva:malloc:imprecise] tests/builtins/calloc.c:14: Warning:
+ allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main
+[eva] tests/builtins/calloc.c:17:
+ Call to builtin Frama_C_calloc_imprecise for function calloc
+[eva] tests/builtins/calloc.c:20:
+ Call to builtin Frama_C_calloc_imprecise for function calloc
+[eva] tests/builtins/calloc.c:23:
+ Call to builtin Frama_C_calloc_imprecise for function calloc
+[eva:alarm] tests/builtins/calloc.c:26: Warning: assertion got status unknown.
+[eva:alarm] tests/builtins/calloc.c:27: Warning: assertion got status unknown.
+[eva] tests/builtins/calloc.c:30:
+ Call to builtin Frama_C_calloc_imprecise for function calloc
+[eva:alarm] tests/builtins/calloc.c:33: Warning: assertion got status unknown.
+[eva:alarm] tests/builtins/calloc.c:34: Warning: assertion got status unknown.
+[eva:alarm] tests/builtins/calloc.c:35: Warning: assertion got status unknown.
+[eva] tests/builtins/calloc.c:38:
+ Call to builtin Frama_C_calloc_imprecise for function calloc
+[eva] tests/builtins/calloc.c:38: Warning:
+ calloc out of bounds: assert(nmemb * size <= SIZE_MAX)
+[eva] tests/builtins/calloc.c:40: assertion got status valid.
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
+ p1 ∈ {{ &__alloc_w_main[0] }}
+ p2 ∈ {{ &__alloc_w_main[0] }}
+ p3 ∈ {{ &__alloc_w_main[0] }}
+ p4 ∈ {{ &__alloc_w_main[0] }}
+ p5 ∈ {{ (int *)&__alloc_w_main }}
+ p9001 ∈ {0}
+ __retres ∈ {0}
+[from] Computing for function main
+[from] Computing for function calloc <-main
+[from] Done for function calloc
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function calloc:
+ __fc_heap_status FROM __fc_heap_status; nmemb; size (and SELF)
+ \result FROM __fc_heap_status; nmemb; size
+[from] Function main:
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+ \result FROM __fc_heap_status
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+ __fc_heap_status; p1; p2; p3; p4; p5; p9001; __retres
+[inout] Inputs for function main:
+ __fc_heap_status; nondet
diff --git a/tests/builtins/oracle/malloc.res.oracle b/tests/builtins/oracle/malloc.res.oracle
index ba9de96ef129ce0b44f01becf1eab69d204e5abb..6bfbf908188b5a5853ee19749c30e75bcd07d56f 100644
--- a/tests/builtins/oracle/malloc.res.oracle
+++ b/tests/builtins/oracle/malloc.res.oracle
@@ -3,6 +3,8 @@
Neither code nor specification for function Frama_C_malloc_fresh, generating default assigns from the prototype
[kernel:annot:missing-spec] tests/builtins/malloc.c:8: Warning:
Neither code nor specification for function Frama_C_malloc_by_stack, generating default assigns from the prototype
+[kernel:annot:missing-spec] tests/builtins/malloc.c:8: Warning:
+ Neither code nor specification for function Frama_C_malloc_imprecise, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
@@ -32,6 +34,16 @@
Frama_C_show_each: {{ &__malloc_main_l20 + {8} }}
[eva] tests/builtins/malloc.c:27:
Frama_C_show_each: {{ &__malloc_main_l20 + {8} }}
+[eva] tests/builtins/malloc.c:33: Call to builtin Frama_C_malloc_imprecise
+[eva:malloc:imprecise] tests/builtins/malloc.c:33: Warning:
+ allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main
+[eva] tests/builtins/malloc.c:33: Call to builtin Frama_C_malloc_imprecise
+[eva:alarm] tests/builtins/malloc.c:34: Warning:
+ out of bounds write. assert \valid(mw);
+[eva] tests/builtins/malloc.c:35: Call to builtin Frama_C_malloc_imprecise
+[eva] tests/builtins/malloc.c:35: Call to builtin Frama_C_malloc_imprecise
+[eva:alarm] tests/builtins/malloc.c:36: Warning:
+ out of bounds write. assert \valid(mw2);
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -41,6 +53,8 @@
p ∈ {{ (int *)&__malloc_main_l19 }}
q ∈ {{ &__malloc_main_l20[0] }}
r ∈ {{ &__malloc_main_l21[0] ; &__malloc_main_l21_0[0] }}
+ mw ∈ {{ (int *)&__alloc_w_main }}
+ mw2 ∈ {{ (int *)&__alloc_w_main }}
__malloc_main_l19[bits 0 to 31] ∈ {1}
[4..7] ∈ UNINITIALIZED
[bits 64 to 95] ∈ {3}
@@ -58,3 +72,5 @@
[1] ∈ UNINITIALIZED
[2] ∈ {3}
[3..24] ∈ UNINITIALIZED
+ __alloc_w_main[bits 0 to 31] ∈ {1; 2} or UNINITIALIZED
+ [4..4294967295] ∈ UNINITIALIZED
diff --git a/tests/builtins/oracle/realloc_imprecise.res.oracle b/tests/builtins/oracle/realloc_imprecise.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..346a55355c0f64cf362f127e98845f8691bee8b6
--- /dev/null
+++ b/tests/builtins/oracle/realloc_imprecise.res.oracle
@@ -0,0 +1,65 @@
+[kernel] Parsing tests/builtins/realloc_imprecise.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ v ∈ [--..--]
+[eva] tests/builtins/realloc_imprecise.c:10:
+ Call to builtin Frama_C_malloc_imprecise for function malloc
+[eva:malloc:imprecise] tests/builtins/realloc_imprecise.c:10: Warning:
+ allocating a single weak variable for ALL dynamic allocations via malloc/calloc/realloc: __alloc_w_main
+[eva:alarm] tests/builtins/realloc_imprecise.c:11: Warning:
+ out of bounds write. assert \valid(p);
+[eva] tests/builtins/realloc_imprecise.c:13:
+ Call to builtin Frama_C_realloc_imprecise for function realloc
+[eva] tests/builtins/realloc_imprecise.c:13:
+ function realloc: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/realloc_imprecise.c:13:
+ weak free on bases: {__alloc_w_main}
+[eva] tests/builtins/realloc_imprecise.c:15:
+ Call to builtin Frama_C_realloc_imprecise for function realloc
+[eva] tests/builtins/realloc_imprecise.c:15:
+ function realloc: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/realloc_imprecise.c:15:
+ weak free on bases: {__alloc_w_main}
+[eva] tests/builtins/realloc_imprecise.c:16: Call to builtin free
+[eva] tests/builtins/realloc_imprecise.c:16:
+ function free: precondition 'freeable' got status valid.
+[eva:malloc] tests/builtins/realloc_imprecise.c:16:
+ weak free on bases: {__alloc_w_main}
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __fc_heap_status ∈ [--..--]
+ p ∈ {{ (int *)&__alloc_w_main }} or ESCAPINGADDR
+ pp ∈ {{ (int *)&__alloc_w_main }} or ESCAPINGADDR
+ q ∈ {{ (int *)&__alloc_w_main }} or ESCAPINGADDR
+ __alloc_w_main[bits 0 to 31] ∈ {17} or UNINITIALIZED
+ [4..4294967295] ∈ UNINITIALIZED
+[from] Computing for function main
+[from] Computing for function malloc <-main
+[from] Done for function malloc
+[from] Computing for function realloc <-main
+[from] Done for function realloc
+[from] Computing for function free <-main
+[from] Done for function free
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[from] Function free:
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+[from] Function malloc:
+ __fc_heap_status FROM __fc_heap_status; size (and SELF)
+ \result FROM __fc_heap_status; size
+[from] Function realloc:
+ __fc_heap_status FROM __fc_heap_status (and SELF)
+ \result FROM __fc_heap_status; ptr; size
+[from] Function main:
+ __fc_heap_status FROM __fc_heap_status; v (and SELF)
+ __alloc_w_main[0..3] FROM __fc_heap_status (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main:
+ __fc_heap_status; p; pp; q; r; __alloc_w_main[0..3]
+[inout] Inputs for function main:
+ __fc_heap_status; v
diff --git a/tests/builtins/realloc_imprecise.c b/tests/builtins/realloc_imprecise.c
new file mode 100644
index 0000000000000000000000000000000000000000..bd9e002b64b2fc82554c3578f90877ee93a1fa45
--- /dev/null
+++ b/tests/builtins/realloc_imprecise.c
@@ -0,0 +1,18 @@
+/* run.config*
+ STDOPT: +"-eva-builtin malloc:Frama_C_malloc_imprecise,realloc:Frama_C_realloc_imprecise"
+*/
+
+#include <stdlib.h>
+
+volatile int v;
+
+void main() {
+ int *p = malloc(sizeof(int));
+ *p = 17;
+ int *pp = p;
+ int *q = realloc(p, 2 * sizeof(int));
+ if (v) {
+ int *r = realloc(q, sizeof(int));
+ free(r);
+ }
+}