Merge pull request #1777 from goblint/issue_1418

Consider option that `malloc(0)` may return `NULL`

Author: michael-schwarz

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,31 @@ struct
           | _ ->
             set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ))
         end
-    in 
+    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 =
+        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 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 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; 
+    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 *)
@@ -2720,53 +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 = AD.of_var (heap_var true man) 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 =
-            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
-          (* 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 = 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, 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 [
-              (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)))
-            ]
-          )
-          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 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 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 [
-              (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)))))
-            ]
-          )
+            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 }, _ ->
@@ -2787,18 +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 = 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_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

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

@@ -1644,9 +1644,16 @@
             "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
+            },
+            "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 *)
@@ -388,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
@@ -441,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
@@ -497,7 +503,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,14 @@
+// PARAM: --set sem.malloc.zero either --set ana.activated[+] memOutOfBounds 
+#include<pthread.h>
+#include<goblint.h>
+
+int main(void){
+  int* ptr = malloc(0);
+
+  if(ptr == 0) {
+    // Reachable
+    __goblint_check(1);
+  } else {
+    *ptr = 1; //WARN
+  }
+}