Consider option that malloc(0) may return NULL

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

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

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

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

src/analyses/wrapperFunctionAnalysis.ml

@@ -155,15 +155,15 @@ 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
       in
       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

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": "either"
             }
           },
           "additionalProperties": false

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

tests/regression/11-heap/19-malloc-zero.c

@@ -0,0 +1,12 @@
+// PARAM: --set sem.malloc.zero either
+#include<pthread.h>
+#include<goblint.h>
+
+int main(void){
+  int* ptr = malloc(0);
+
+  if(ptr == 0) {
+    // Reachable
+    __goblint_check(1);
+  }
+}