From 80f3d4d78082c64a5e87ce88313823eea75416dd Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Jul 2025 14:48:14 +0200 Subject: [PATCH 01/10] Add option to configure behavior upon allocating 0 bytes --- src/analyses/base.ml | 64 ++++++++++++++----------- src/analyses/mallocFresh.ml | 8 ++-- src/analyses/memLeak.ml | 2 +- src/analyses/useAfterFree.ml | 2 +- src/analyses/wrapperFunctionAnalysis.ml | 4 +- src/config/options.schema.json | 7 +++ src/domains/queries.ml | 8 +++- 7 files changed, 56 insertions(+), 39 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 63a790e852..75f500fdde 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -143,8 +143,8 @@ struct * Initializing my variables **************************************************************************) - let heap_var on_stack man = - let info = match (man.ask (Q.AllocVar {on_stack})) with + let alloced_var location man = + let info = match (man.ask (Q.AllocVar location)) with | `Lifted vinfo -> vinfo | _ -> failwith("Ran without a malloc analysis.") in info @@ -2501,9 +2501,27 @@ struct | _ -> set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ)) end - in + in + let alloc ?(offset=`NoOffset) loc size = + let bytes = eval_int ~man st size in + let is_zero = ID.equal_to Z.zero bytes in + let heap_var = + let include_null = get_bool "sem.malloc.fail" || (is_zero <> `Neq && get_string "sem.malloc.zero" <> "pointer") in + let include_pointer = (is_zero <> `Eq || get_string "sem.malloc.zero" <> "null") in + let res = if include_pointer then + AD.of_mval (alloced_var loc man, offset) + else + AD.bot () + in + if include_null then + AD.join res AD.null_ptr + else + res + in + heap_var + in (* Evaluate each functions arguments. `eval_rv` is only called for its side effects, we ignore the result. *) - List.iter (fun arg -> eval_rv ~man st arg |> ignore) args; + List.iter (fun arg -> eval_rv ~man st arg |> ignore) args; let st = match desc.special args, f.vname with | Memset { dest; ch; count; }, _ -> (* TODO: check count *) @@ -2723,7 +2741,7 @@ struct | Alloca size, _ -> begin match lv with | Some lv -> - let heap_var = AD.of_var (heap_var true man) in + let heap_var = alloc Queries.AllocationLocation.Stack size in (* ignore @@ printf "alloca will allocate %a bytes\n" ID.pretty (eval_int ~man size); *) set_many ~man st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~man st size, ZeroInit.malloc)); (eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address heap_var)] @@ -2732,11 +2750,7 @@ struct | Malloc size, _ -> begin match lv with | Some lv -> - let heap_var = - if (get_bool "sem.malloc.fail") - then AD.join (AD.of_var (heap_var false man)) AD.null_ptr - else AD.of_var (heap_var false man) - in + let heap_var = alloc Queries.AllocationLocation.Heap size in (* ignore @@ printf "malloc will allocate %a bytes\n" ID.pretty (eval_int ~man size); *) set_many ~man st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~man st size, ZeroInit.malloc)); (eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address heap_var)] @@ -2745,26 +2759,24 @@ struct | Calloc { count = n; size }, _ -> begin match lv with | Some lv -> (* array length is set to one, as num*size is done when turning into `Calloc *) - let heap_var = heap_var false man in - let add_null addr = - if get_bool "sem.malloc.fail" - then AD.join addr AD.null_ptr (* calloc can fail and return NULL *) - else addr in + let heap_var = alloc Queries.AllocationLocation.Heap size in let ik = Cilfacade.ptrdiff_ikind () in let sizeval = eval_int ~man st size in let countval = eval_int ~man st n in if ID.to_int countval = Some Z.one then ( - set_many ~man st [ - (add_null (AD.of_var heap_var), TVoid [], Blob (VD.bot (), sizeval, ZeroInit.calloc)); - (eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_var heap_var))) - ] + set_many ~man st [(heap_var, TVoid [], Blob (VD.bot (), sizeval, ZeroInit.calloc)); + (eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address heap_var)] ) else ( let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in + let heap_var = alloc Queries.AllocationLocation.Heap size in + let offset = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in + (* the heap_var is the base address of the allocated memory, but we need to keep track of the offset for the blob *) + let heap_var_offset = AD.map (fun a -> Addr.add_offset a offset) heap_var in (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *) set_many ~man st [ - (add_null (AD.of_var heap_var), TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, ZeroInit.calloc)))); - (eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address (add_null (AD.of_mval (heap_var, `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset))))) + (heap_var, TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, ZeroInit.calloc)))); + (eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address (heap_var_offset)) ] ) | _ -> st @@ -2787,17 +2799,11 @@ struct let p_addr_get = get ~man st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *) let size_int = eval_int ~man st size in let heap_val:value = Blob (p_addr_get, size_int, ZeroInit.malloc) in (* copy old contents with new size *) - let heap_addr = AD.of_var (heap_var false man) in - let heap_addr' = - if get_bool "sem.malloc.fail" then - AD.join heap_addr AD.null_ptr - else - heap_addr - in + let heap_addr = alloc Queries.AllocationLocation.Heap size in let lv_addr = eval_lv ~man st lv in set_many ~man st [ (heap_addr, TVoid [], heap_val); - (lv_addr, Cilfacade.typeOfLval lv, Address heap_addr'); + (lv_addr, Cilfacade.typeOfLval lv, Address heap_addr); ] (* TODO: free (i.e. invalidate) old blob if successful? *) | None -> st diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml index c226d7e6ce..102fcd2bf3 100644 --- a/src/analyses/mallocFresh.ml +++ b/src/analyses/mallocFresh.ml @@ -39,16 +39,16 @@ struct let special man lval f args = let desc = LibraryFunctions.find f in - let alloc_var on_stack = - match man.ask (AllocVar {on_stack = on_stack}) with + let alloc_var location = + match man.ask (AllocVar location) with | `Lifted var -> D.add var man.local | _ -> man.local in match desc.special args with | Malloc _ | Calloc _ - | Realloc _ -> alloc_var false - | Alloca _ -> alloc_var true + | Realloc _ -> alloc_var Heap + | Alloca _ -> alloc_var Stack | _ -> match lval with | None -> man.local diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index e3ce9e4967..7a8acb849d 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -206,7 +206,7 @@ struct | Calloc _ | Realloc _ -> man.sideg () true; - begin match man.ask (Queries.AllocVar {on_stack = false}) with + begin match man.ask (Queries.AllocVar Heap) with | `Lifted var -> ToppedVarInfoSet.add var state | _ -> state diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 32a095a13c..fab76f177b 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -230,7 +230,7 @@ struct end | Alloca _ -> (* Create fresh heap var for the alloca() call *) - begin match man.ask (Queries.AllocVar {on_stack = true}) with + begin match man.ask (Queries.AllocVar Stack) with | `Lifted v -> (AllocaVars.add v (fst state), snd state) | _ -> state end diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml index 929d9e2b0b..ea8572d867 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/src/analyses/wrapperFunctionAnalysis.ml @@ -155,7 +155,7 @@ module MallocWrapper : MCPSpec = struct let query (man: (D.t, G.t, C.t, V.t) man) (type a) (q: a Q.t): a Q.result = let wrapper_node, counter = man.local in match q with - | Q.AllocVar {on_stack = on_stack} -> + | Q.AllocVar location -> let node = match wrapper_node with | `Lifted wrapper_node -> wrapper_node | _ -> node_for_man man @@ -163,7 +163,7 @@ module MallocWrapper : MCPSpec = struct let count = UniqueCallCounter.find (`Lifted node) counter in let var = NodeVarinfoMap.to_varinfo (man.ask Q.CurrentThreadId, node, count) in var.vdecl <- UpdateCil.getLoc node; (* TODO: does this do anything bad for incremental? *) - if on_stack then var.vattr <- addAttribute (Attr ("stack_alloca", [])) var.vattr; (* If the call was for stack allocation, add an attr to mark the heap var *) + if location = Stack then var.vattr <- addAttribute (Attr ("stack_alloca", [])) var.vattr; (* If the call was for stack allocation, add an attr to mark the heap var *) `Lifted var | Q.IsHeapVar v -> NodeVarinfoMap.mem_varinfo v && not @@ hasAttribute "stack_alloca" v.vattr diff --git a/src/config/options.schema.json b/src/config/options.schema.json index ae26553ec0..e8543e2bf8 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1647,6 +1647,13 @@ "Consider the case where malloc or calloc fails.", "type": "boolean", "default": false + }, + "zero": { + "title": "sem.malloc.zero", + "description": "What happens when allocating zero bytes? null: Return null pointer, pointer: Return a pointer to valid memory of size 0, either: Consider both cases.", + "type": "string", + "enum": ["null", "pointer","either"], + "default": "pointer" } }, "additionalProperties": false diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 01f02f9fde..b31f19b955 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -50,6 +50,10 @@ module Protection = struct type t = Strong | Weak [@@deriving ord, hash] end +module AllocationLocation = struct + type t = Stack | Heap [@@deriving ord, hash] +end + (* Helper definitions for deriving complex parts of Any.compare below. *) type maybepublic = {global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash] type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: LockDomain.MustLock.t; protection: Protection.t} [@@deriving ord, hash] @@ -101,7 +105,7 @@ type _ t = | IterVars: itervar -> Unit.t t | PathQuery: int * 'a t -> 'a t (** Query only one path under witness lifter. *) | DYojson: FlatYojson.t t (** Get local state Yojson of one path under [PathQuery]. *) - | AllocVar: {on_stack: bool} -> VI.t t + | AllocVar: AllocationLocation.t -> VI.t t (* Create a variable representing a dynamic allocation-site *) (* If on_stack is [true], then the dynamic allocation is on the stack (i.e., alloca() or a similar function was called). Otherwise, allocation is on the heap *) | IsAllocVar: varinfo -> MayBool.t t (* [true] if variable represents dynamically allocated memory *) @@ -497,7 +501,7 @@ struct | Any (IterPrevVars i) -> Pretty.dprintf "IterPrevVars _" | Any (IterVars i) -> Pretty.dprintf "IterVars _" | Any (PathQuery (i, q)) -> Pretty.dprintf "PathQuery (%d, %a)" i pretty (Any q) - | Any (AllocVar {on_stack = on_stack}) -> Pretty.dprintf "AllocVar %b" on_stack + | Any (AllocVar location) -> Pretty.dprintf "AllocVar _" | Any (IsHeapVar v) -> Pretty.dprintf "IsHeapVar %a" CilType.Varinfo.pretty v | Any (IsAllocVar v) -> Pretty.dprintf "IsAllocVar %a" CilType.Varinfo.pretty v | Any (IsMultiple v) -> Pretty.dprintf "IsMultiple %a" CilType.Varinfo.pretty v From 5dd1f55edd023242f83acec7c070795343d58528 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Jul 2025 14:50:36 +0200 Subject: [PATCH 02/10] Add test case for considering returning zero --- tests/regression/11-heap/19-malloc-zero.c | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 tests/regression/11-heap/19-malloc-zero.c diff --git a/tests/regression/11-heap/19-malloc-zero.c b/tests/regression/11-heap/19-malloc-zero.c new file mode 100644 index 0000000000..cb0b9af0fb --- /dev/null +++ b/tests/regression/11-heap/19-malloc-zero.c @@ -0,0 +1,12 @@ +// PARAM: --set sem.malloc.zero either +#include +#include + +int main(void){ + int* ptr = malloc(0); + + if(ptr == 0) { + // Reachable + __goblint_check(1); + } +} From 6ad23e0c3c00f853e6d5cd278d668fc91c324928 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 3 Jul 2025 14:55:28 +0200 Subject: [PATCH 03/10] `sem.malloc.zero`: Sound default --- src/config/options.schema.json | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index e8543e2bf8..7901f2ccc3 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1650,10 +1650,10 @@ }, "zero": { "title": "sem.malloc.zero", - "description": "What happens when allocating zero bytes? null: Return null pointer, pointer: Return a pointer to valid memory of size 0, either: Consider both cases.", + "description": "What happens when allocating zero bytes? 'null': Return null pointer, 'pointer': Return a pointer to valid memory of size 0, 'either': Consider both cases.", "type": "string", "enum": ["null", "pointer","either"], - "default": "pointer" + "default": "either" } }, "additionalProperties": false From 8187a1cbffb68f91dfec863d1c38dfea666dcf97 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 4 Jul 2025 09:13:13 +0200 Subject: [PATCH 04/10] Queries: `AllocVar` handle `equal` and `hash` specifically --- src/domains/queries.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index b31f19b955..c32f78a769 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -392,6 +392,7 @@ struct | Any (CondVars e1), Any (CondVars e2) -> CilType.Exp.compare e1 e2 | Any (PartAccess p1), Any (PartAccess p2) -> compare_access p1 p2 | Any (IterPrevVars ip1), Any (IterPrevVars ip2) -> compare_iterprevvar ip1 ip2 + | Any (AllocVar location), Any (AllocVar location2) -> AllocationLocation.compare location location2 | Any (IterVars i1), Any (IterVars i2) -> compare_itervar i1 i2 | Any (PathQuery (i1, q1)), Any (PathQuery (i2, q2)) -> let r = Stdlib.compare i1 i2 in @@ -445,6 +446,7 @@ struct | Any (PartAccess p) -> hash_access p | Any (IterPrevVars i) -> 0 | Any (IterVars i) -> 0 + | Any (AllocVar location) -> AllocationLocation.hash location | Any (PathQuery (i, q)) -> 31 * i + hash (Any q) | Any (IsHeapVar v) -> CilType.Varinfo.hash v | Any (MustTermLoop s) -> CilType.Stmt.hash s From 541a827114c56b1ae1b10707185fb8d72ca2bce2 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 4 Jul 2025 09:15:12 +0200 Subject: [PATCH 05/10] base: Simplify `alloc` --- src/analyses/base.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 75f500fdde..94c04343f3 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2502,17 +2502,13 @@ struct set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ)) end in - let alloc ?(offset=`NoOffset) loc size = + let alloc loc size = let bytes = eval_int ~man st size in let is_zero = ID.equal_to Z.zero bytes in let heap_var = let include_null = get_bool "sem.malloc.fail" || (is_zero <> `Neq && get_string "sem.malloc.zero" <> "pointer") in let include_pointer = (is_zero <> `Eq || get_string "sem.malloc.zero" <> "null") in - let res = if include_pointer then - AD.of_mval (alloced_var loc man, offset) - else - AD.bot () - in + let res = if include_pointer then AD.of_var (alloced_var loc man) else AD.bot () in if include_null then AD.join res AD.null_ptr else From 2bb4ac2601a0ef5787a67543ac6aa07097577ec3 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 4 Jul 2025 09:37:03 +0200 Subject: [PATCH 06/10] Base: Simplify logic in `alloc`? --- src/analyses/base.ml | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 94c04343f3..3a3a7633d9 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2503,11 +2503,21 @@ struct end in let alloc loc size = + (* Whether malloc(0) is assumed to return the null pointer, a valid pointer, or both cases need to be considered. *) + let malloc_zero_null, malloc_zero_pointer = + match get_string "sem.malloc.zero" with + | "null" -> true, false + | "pointer" -> false, true + | "either" -> true, true + | _ -> failwith "Invalid value for sem.malloc.zero." + in let bytes = eval_int ~man st size in - let is_zero = ID.equal_to Z.zero bytes in + let cmp_bytes_with_zero = ID.equal_to Z.zero bytes in + let bytes_may_be_zero = cmp_bytes_with_zero <> `Neq in + let bytes_may_be_nonzero = cmp_bytes_with_zero <> `Eq in let heap_var = - let include_null = get_bool "sem.malloc.fail" || (is_zero <> `Neq && get_string "sem.malloc.zero" <> "pointer") in - let include_pointer = (is_zero <> `Eq || get_string "sem.malloc.zero" <> "null") in + let include_null = get_bool "sem.malloc.fail" || (bytes_may_be_zero && malloc_zero_null) in + let include_pointer = bytes_may_be_nonzero || malloc_zero_pointer in let res = if include_pointer then AD.of_var (alloced_var loc man) else AD.bot () in if include_null then AD.join res AD.null_ptr From 9f5738a064920e47d81a4550ee433e9f12eb1e7e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 7 Jul 2025 10:06:42 +0200 Subject: [PATCH 07/10] Separate options --- src/analyses/base.ml | 2 +- src/config/options.schema.json | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 3a3a7633d9..5a6cb1252d 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2516,7 +2516,7 @@ struct let bytes_may_be_zero = cmp_bytes_with_zero <> `Neq in let bytes_may_be_nonzero = cmp_bytes_with_zero <> `Eq in let heap_var = - let include_null = get_bool "sem.malloc.fail" || (bytes_may_be_zero && malloc_zero_null) in + let include_null = (bytes_may_be_nonzero && get_bool "sem.malloc.fail") || (bytes_may_be_zero && malloc_zero_null) in let include_pointer = bytes_may_be_nonzero || malloc_zero_pointer in let res = if include_pointer then AD.of_var (alloced_var loc man) else AD.bot () in if include_null then diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 7901f2ccc3..23a85e7045 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1644,7 +1644,7 @@ "fail": { "title": "sem.malloc.fail", "description": - "Consider the case where malloc or calloc fails.", + "Consider the case where malloc or calloc fails when called with an argument other than zero. For the case of zero, see `sem.malloc.zero`.", "type": "boolean", "default": false }, From 1014dcda13a8254dc1e01d51bc6a4a0f50b246e0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 7 Jul 2025 10:28:03 +0200 Subject: [PATCH 08/10] 11/19: Add out of bounds access Co-Authored-By: Simmo Saan --- tests/regression/11-heap/19-malloc-zero.c | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tests/regression/11-heap/19-malloc-zero.c b/tests/regression/11-heap/19-malloc-zero.c index cb0b9af0fb..6d00aeb599 100644 --- a/tests/regression/11-heap/19-malloc-zero.c +++ b/tests/regression/11-heap/19-malloc-zero.c @@ -1,4 +1,4 @@ -// PARAM: --set sem.malloc.zero either +// PARAM: --set sem.malloc.zero either --set ana.activated[+] memOutOfBounds #include #include @@ -8,5 +8,7 @@ int main(void){ if(ptr == 0) { // Reachable __goblint_check(1); + } else { + *ptr = 1; //WARN } } From ffe30b9eda935eb2bae2330dd02dc190b8043e3c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 8 Jul 2025 11:12:48 +0200 Subject: [PATCH 09/10] Add comment on `alloca` --- src/analyses/base.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 5a6cb1252d..f6f4a29761 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2745,6 +2745,7 @@ struct st end | Alloca size, _ -> begin + (* The behavior for alloc(0) is implementation defined. Here, we rely on the options specified for the malloc also applying to alloca. *) match lv with | Some lv -> let heap_var = alloc Queries.AllocationLocation.Stack size in From 558e44527cbcb075e339ae26d098fb9a78d04063 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 8 Jul 2025 12:58:39 +0200 Subject: [PATCH 10/10] Unify handling and avoiding writing to null pointer --- src/analyses/base.ml | 70 ++++++++++++++++++-------------------------- 1 file changed, 29 insertions(+), 41 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index f6f4a29761..221ac08073 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2502,6 +2502,7 @@ struct set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ)) end in + (* Returns a tuple, the first is the address of the blob if one was allocated, the second is the returned address (may contain null pointer or be only null-pointer) *) let alloc loc size = (* Whether malloc(0) is assumed to return the null pointer, a valid pointer, or both cases need to be considered. *) let malloc_zero_null, malloc_zero_pointer = @@ -2515,16 +2516,13 @@ struct let cmp_bytes_with_zero = ID.equal_to Z.zero bytes in let bytes_may_be_zero = cmp_bytes_with_zero <> `Neq in let bytes_may_be_nonzero = cmp_bytes_with_zero <> `Eq in - let heap_var = - let include_null = (bytes_may_be_nonzero && get_bool "sem.malloc.fail") || (bytes_may_be_zero && malloc_zero_null) in - let include_pointer = bytes_may_be_nonzero || malloc_zero_pointer in - let res = if include_pointer then AD.of_var (alloced_var loc man) else AD.bot () in - if include_null then - AD.join res AD.null_ptr - else - res - in - heap_var + let include_null = (bytes_may_be_nonzero && get_bool "sem.malloc.fail") || (bytes_may_be_zero && malloc_zero_null) in + let include_pointer = bytes_may_be_nonzero || malloc_zero_pointer in + if not include_pointer then + (None, AD.null_ptr) + else + let var = AD.of_var (alloced_var loc man) in + (Some var, if include_null then AD.join var AD.null_ptr else var) in (* Evaluate each functions arguments. `eval_rv` is only called for its side effects, we ignore the result. *) List.iter (fun arg -> eval_rv ~man st arg |> ignore) args; @@ -2744,48 +2742,39 @@ struct | None, _ -> st end - | Alloca size, _ -> begin + | ((Alloca size) as op), _ + | ((Malloc size) as op), _ -> + let open Queries.AllocationLocation in + begin (* The behavior for alloc(0) is implementation defined. Here, we rely on the options specified for the malloc also applying to alloca. *) match lv with | Some lv -> - let heap_var = alloc Queries.AllocationLocation.Stack size in + let loc = match op with | Alloca _ -> Stack | Malloc _ -> Heap | _ -> assert false in + let (heap_var, addr) = alloc loc size in (* ignore @@ printf "alloca will allocate %a bytes\n" ID.pretty (eval_int ~man size); *) - set_many ~man st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~man st size, ZeroInit.malloc)); - (eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address heap_var)] - | _ -> st - end - | Malloc size, _ -> begin - match lv with - | Some lv -> - let heap_var = alloc Queries.AllocationLocation.Heap size in - (* ignore @@ printf "malloc will allocate %a bytes\n" ID.pretty (eval_int ~man size); *) - set_many ~man st [(heap_var, TVoid [], Blob (VD.bot (), eval_int ~man st size, ZeroInit.malloc)); - (eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address heap_var)] + let blob_set = Option.map_default (fun heap_var -> [(heap_var, TVoid [], VD.Blob (VD.bot (), eval_int ~man st size, ZeroInit.malloc))]) [] heap_var in + set_many ~man st ((eval_lv ~man st lv, (Cilfacade.typeOfLval lv), VD.Address addr) :: blob_set) | _ -> st end | Calloc { count = n; size }, _ -> + let open Queries.AllocationLocation in begin match lv with | Some lv -> (* array length is set to one, as num*size is done when turning into `Calloc *) - let heap_var = alloc Queries.AllocationLocation.Heap size in + let (heap_var, addr) = alloc Queries.AllocationLocation.Heap size in let ik = Cilfacade.ptrdiff_ikind () in let sizeval = eval_int ~man st size in let countval = eval_int ~man st n in - if ID.to_int countval = Some Z.one then ( - set_many ~man st [(heap_var, TVoid [], Blob (VD.bot (), sizeval, ZeroInit.calloc)); - (eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address heap_var)] - ) - else ( + if ID.to_int countval = Some Z.one then + let blob_set = Option.map_default (fun heap_var -> [heap_var, TVoid [], VD.Blob (VD.bot (), sizeval, ZeroInit.calloc)]) [] heap_var in + set_many ~man st ((eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address addr):: blob_set) + else let blobsize = ID.mul (ID.cast_to ik @@ sizeval) (ID.cast_to ik @@ countval) in - let heap_var = alloc Queries.AllocationLocation.Heap size in let offset = `Index (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.zero, `NoOffset) in (* the heap_var is the base address of the allocated memory, but we need to keep track of the offset for the blob *) - let heap_var_offset = AD.map (fun a -> Addr.add_offset a offset) heap_var in + let addr_offset = AD.map (fun a -> Addr.add_offset a offset) addr in (* the memory that was allocated by calloc is set to bottom, but we keep track that it originated from calloc, so when bottom is read from memory allocated by calloc it is turned to zero *) - set_many ~man st [ - (heap_var, TVoid [], Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, ZeroInit.calloc)))); - (eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address (heap_var_offset)) - ] - ) + let blob_set = Option.map_default (fun heap_var -> [heap_var, TVoid [], VD.Array (CArrays.make (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) Z.one) (Blob (VD.bot (), blobsize, ZeroInit.calloc)))]) [] heap_var in + set_many ~man st ((eval_lv ~man st lv, (Cilfacade.typeOfLval lv), Address addr_offset) :: blob_set) | _ -> st end | Realloc { ptr = p; size }, _ -> @@ -2806,12 +2795,11 @@ struct let p_addr_get = get ~man st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *) let size_int = eval_int ~man st size in let heap_val:value = Blob (p_addr_get, size_int, ZeroInit.malloc) in (* copy old contents with new size *) - let heap_addr = alloc Queries.AllocationLocation.Heap size in + let (heap_var,addr) = alloc Queries.AllocationLocation.Heap size in let lv_addr = eval_lv ~man st lv in - set_many ~man st [ - (heap_addr, TVoid [], heap_val); - (lv_addr, Cilfacade.typeOfLval lv, Address heap_addr); - ] (* TODO: free (i.e. invalidate) old blob if successful? *) + let blob_set = Option.map_default (fun heap_addr -> [heap_addr, TVoid [], heap_val]) [] heap_var in + (* TODO: free (i.e. invalidate) old blob if successful? *) + set_many ~man st ((lv_addr, Cilfacade.typeOfLval lv, Address addr) :: blob_set) | None -> st end