Support stack-allocating functions when allocating heap vars

src/analyses/base.ml

@@ -150,8 +150,8 @@ struct
 
   let longjmp_return = ref dummyFunDec.svar
 
-  let heap_var ctx =
-    let info = match (ctx.ask Q.HeapVar) with
+  let heap_var on_stack ctx =
+    let info = match (ctx.ask (Q.HeapVar {on_stack = on_stack})) with
       | `Lifted vinfo -> vinfo
       | _ -> failwith("Ran without a malloc analysis.") in
     info
@@ -1254,7 +1254,7 @@ struct
         | Address a ->
           (* If there's a non-heap var or an offset in the lval set, we answer with bottom *)
           if AD.exists (function
-              | Addr (v,o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset
+              | Addr (v,o) -> (not @@ ctx.ask (Queries.IsHeapVar v)) || (ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsDynamicallyAlloced v)) || o <> `NoOffset
               | _ -> false) a then
             Queries.Result.bot q
           else (
@@ -1995,7 +1995,7 @@ struct
 
   let check_invalid_mem_dealloc ctx special_fn ptr =
     let has_non_heap_var = AD.exists (function
-        | Addr (v,_) -> not (ctx.ask (Q.IsHeapVar v))
+        | Addr (v,_) -> not (ctx.ask (Q.IsHeapVar v)) || (ctx.ask (Q.IsHeapVar v) && not @@ ctx.ask (Q.IsDynamicallyAlloced v))
         | _ -> false)
     in
     let has_non_zero_offset = AD.exists (function
@@ -2263,13 +2263,14 @@ struct
     | Unknown, "__goblint_assume_join" ->
       let id = List.hd args in
       Priv.thread_join ~force:true (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st
-    | Malloc size, _ -> begin
+    | Malloc size, fname -> begin
         match lv with
         | Some lv ->
+          let is_stack_alloc = fname = "alloc" || fname = "__builtin_alloca" in
           let heap_var =
             if (get_bool "sem.malloc.fail")
-            then AD.join (AD.of_var (heap_var ctx)) AD.null_ptr
-            else AD.of_var (heap_var ctx)
+            then AD.join (AD.of_var (heap_var is_stack_alloc ctx)) AD.null_ptr
+            else AD.of_var (heap_var is_stack_alloc ctx)
           in
           (* ignore @@ printf "malloc will allocate %a bytes\n" ID.pretty (eval_int ctx.ask gs st size); *)
           set_many ~ctx (Analyses.ask_of_ctx ctx) gs st [(heap_var, TVoid [], Blob (VD.bot (), eval_int (Analyses.ask_of_ctx ctx) gs st size, true));
@@ -2279,7 +2280,7 @@ 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 ctx in
+          let heap_var = heap_var false ctx in
           let add_null addr =
             if get_bool "sem.malloc.fail"
             then AD.join addr AD.null_ptr (* calloc can fail and return NULL *)
@@ -2322,7 +2323,7 @@ struct
           let p_addr_get = get ask gs st p_addr' None in (* implicitly includes join of malloc value (VD.bot) *)
           let size_int = eval_int ask gs st size in
           let heap_val:value = Blob (p_addr_get, size_int, true) in (* copy old contents with new size *)
-          let heap_addr = AD.of_var (heap_var ctx) in
+          let heap_addr = AD.of_var (heap_var false ctx) in
           let heap_addr' =
             if get_bool "sem.malloc.fail" then
               AD.join heap_addr AD.null_ptr
@@ -2563,6 +2564,7 @@ struct
                 | MayBeThreadReturn
                 | PartAccess _
                 | IsHeapVar _
+                | IsDynamicallyAlloced _
                 | IsMultiple _
                 | CreatedThreads
                 | MustJoinedThreads ->

src/analyses/libraryFunctions.ml

@@ -64,6 +64,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__builtin_strcmp", special [__ "s1" [r]; __ "s2" [r]] @@ fun s1 s2 -> Strcmp { s1; s2; n = None; });
     ("strncmp", special [__ "s1" [r]; __ "s2" [r]; __ "n" []] @@ fun s1 s2 n -> Strcmp { s1; s2; n = Some n; });
     ("malloc", special [__ "size" []] @@ fun size -> Malloc size);
+    ("alloca", special [__ "size" []] @@ fun size -> Malloc size); (* TODO: Maybe define a new special type [Alloca], just like [Malloc]? *)
     ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size });
     ("free", special [__ "ptr" [f]] @@ fun ptr -> Free ptr);
     ("abort", special [] Abort);

src/analyses/mallocFresh.ml

@@ -43,7 +43,7 @@ struct
     | Malloc _
     | Calloc _
     | Realloc _ ->
-      begin match ctx.ask HeapVar with
+      begin match ctx.ask (HeapVar {on_stack = false}) with
         | `Lifted var -> D.add var ctx.local
         | _ -> ctx.local
       end

src/analyses/memLeak.ml

@@ -44,7 +44,7 @@ struct
     | Realloc _ ->
       (* Warn about multi-threaded programs as soon as we encounter a dynamic memory allocation function *)
       warn_for_multi_threaded ctx;
-      begin match ctx.ask Queries.HeapVar with
+      begin match ctx.ask (Queries.HeapVar {on_stack = false}) with
         | `Lifted var -> D.add var state
         | _ -> state
       end
@@ -53,7 +53,7 @@ struct
         | ad when not (Queries.AD.is_top ad) && Queries.AD.cardinal ad = 1 ->
           (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
           begin match Queries.AD.choose ad with
-            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state (* Unique pointed to heap vars *)
+            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) && ctx.ask (Queries.IsDynamicallyAlloced v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state (* Unique pointed to heap vars *)
             | _ -> state
           end
         | _ -> state

src/analyses/wrapperFunctionAnalysis.ml

@@ -133,17 +133,20 @@ module MallocWrapper : MCPSpec = struct
   let query (ctx: (D.t, G.t, C.t, V.t) ctx) (type a) (q: a Q.t): a Q.result =
     let wrapper_node, counter = ctx.local in
     match q with
-    | Q.HeapVar ->
+    | Q.HeapVar {on_stack = on_stack} ->
       let node = match wrapper_node with
         | `Lifted wrapper_node -> wrapper_node
         | _ -> node_for_ctx ctx
       in
       let count = UniqueCallCounter.find (`Lifted node) counter in
       let var = NodeVarinfoMap.to_varinfo (ctx.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 *)
       `Lifted var
     | Q.IsHeapVar v ->
       NodeVarinfoMap.mem_varinfo v
+    | Q.IsDynamicallyAlloced v ->
+      NodeVarinfoMap.mem_varinfo v && not @@ hasAttribute "stack_alloca" v.vattr
     | Q.IsMultiple v ->
       begin match NodeVarinfoMap.from_varinfo v with
         | Some (_, _, c) -> UniqueCount.is_top c || not (ctx.ask Q.MustBeUniqueThread)

src/domains/queries.ml

@@ -99,8 +99,9 @@ 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]. *)
-  | HeapVar: VI.t t
+  | HeapVar: {on_stack: bool} -> VI.t t (* If on_stack is [true], then alloca() or a similar function was called *)
   | IsHeapVar: varinfo -> MayBool.t t (* TODO: is may or must? *)
+  | IsDynamicallyAlloced: varinfo -> MayBool.t t (* [true] if heap var represents dynamically alloced memory, [false] if it represents the result of an alloca() call *)
   | IsMultiple: varinfo -> MustBool.t t
   (* For locals: Is another copy of this local variable reachable via pointers? *)
   (* For dynamically allocated memory: Does this abstract variable corrrespond to a unique heap location? *)
@@ -152,6 +153,7 @@ struct
     | MayBePublicWithout _ -> (module MayBool)
     | MayBeThreadReturn -> (module MayBool)
     | IsHeapVar _ -> (module MayBool)
+    | IsDynamicallyAlloced _ -> (module MayBool)
     | MustBeProtectedBy _ -> (module MustBool)
     | MustBeAtomic -> (module MustBool)
     | MustBeSingleThreaded _ -> (module MustBool)
@@ -163,7 +165,7 @@ struct
     | BlobSize _ -> (module ID)
     | CurrentThreadId -> (module ThreadIdDomain.ThreadLifted)
     | ThreadCreateIndexedNode -> (module ThreadNodeLattice)
-    | HeapVar -> (module VI)
+    | HeapVar _ -> (module VI)
     | EvalStr _ -> (module SD)
     | IterPrevVars _ -> (module Unit)
     | IterVars _ -> (module Unit)
@@ -216,6 +218,7 @@ struct
     | MayBePublicWithout _ -> MayBool.top ()
     | MayBeThreadReturn -> MayBool.top ()
     | IsHeapVar _ -> MayBool.top ()
+    | IsDynamicallyAlloced _ -> MayBool.top ()
     | MutexType _ -> MutexAttrDomain.top ()
     | MustBeProtectedBy _ -> MustBool.top ()
     | MustBeAtomic -> MustBool.top ()
@@ -228,7 +231,7 @@ struct
     | BlobSize _ -> ID.top ()
     | CurrentThreadId -> ThreadIdDomain.ThreadLifted.top ()
     | ThreadCreateIndexedNode -> ThreadNodeLattice.top ()
-    | HeapVar -> VI.top ()
+    | HeapVar _ -> VI.top ()
     | EvalStr _ -> SD.top ()
     | IterPrevVars _ -> Unit.top ()
     | IterVars _ -> Unit.top ()
@@ -288,7 +291,7 @@ struct
     | Any (PartAccess _) -> 23
     | Any (IterPrevVars _) -> 24
     | Any (IterVars _) -> 25
-    | Any HeapVar -> 29
+    | Any (HeapVar _) -> 29
     | Any (IsHeapVar _) -> 30
     | Any (IsMultiple _) -> 31
     | Any (EvalThread _) -> 32
@@ -313,6 +316,7 @@ struct
     | Any ThreadCreateIndexedNode -> 51
     | Any ThreadsJoinedCleanly -> 52
     | Any (TmpSpecial _) -> 53
+    | Any (IsDynamicallyAlloced _) -> 54
 
   let rec compare a b =
     let r = Stdlib.compare (order a) (order b) in
@@ -347,6 +351,7 @@ struct
         else
           compare (Any q1) (Any q2)
       | Any (IsHeapVar v1), Any (IsHeapVar v2) -> CilType.Varinfo.compare v1 v2
+      | Any (IsDynamicallyAlloced v1), Any (IsDynamicallyAlloced v2) -> CilType.Varinfo.compare v1 v2
       | Any (IsMultiple v1), Any (IsMultiple v2) -> CilType.Varinfo.compare v1 v2
       | Any (EvalThread e1), Any (EvalThread e2) -> CilType.Exp.compare e1 e2
       | Any (EvalJumpBuf e1), Any (EvalJumpBuf e2) -> CilType.Exp.compare e1 e2
@@ -387,6 +392,7 @@ struct
     | Any (IterVars i) -> 0
     | Any (PathQuery (i, q)) -> 31 * i + hash (Any q)
     | Any (IsHeapVar v) -> CilType.Varinfo.hash v
+    | Any (IsDynamicallyAlloced v) -> CilType.Varinfo.hash v
     | Any (IsMultiple v) -> CilType.Varinfo.hash v
     | Any (EvalThread e) -> CilType.Exp.hash e
     | Any (EvalJumpBuf e) -> CilType.Exp.hash e
@@ -434,8 +440,9 @@ 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 HeapVar -> Pretty.dprintf "HeapVar"
+    | Any (HeapVar {on_stack = on_stack}) -> Pretty.dprintf "HeapVar %b" on_stack
     | Any (IsHeapVar v) -> Pretty.dprintf "IsHeapVar %a" CilType.Varinfo.pretty v
+    | Any (IsDynamicallyAlloced v) -> Pretty.dprintf "IsDynamicallyAlloced %a" CilType.Varinfo.pretty v
     | Any (IsMultiple v) -> Pretty.dprintf "IsMultiple %a" CilType.Varinfo.pretty v
     | Any (EvalThread e) -> Pretty.dprintf "EvalThread %a" CilType.Exp.pretty e
     | Any (EvalJumpBuf e) -> Pretty.dprintf "EvalJumpBuf %a" CilType.Exp.pretty e