From 89e007478b4d2d5b96181f42e946fff6f68d7a1f Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 20 Sep 2023 18:39:39 +0200 Subject: [PATCH 01/20] Make HeapVar support stack allocation, update IsHeapVar and add IsDynamicallyAlloced --- src/domains/queries.ml | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 0388ce2995..5ddf417699 100644 --- a/src/domains/queries.ml +++ b/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 From 9a06189b7cb843aeb9d645f59c3d08b86d2c8f6c Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 20 Sep 2023 18:41:08 +0200 Subject: [PATCH 02/20] Implement answer for IsDynamicallyAlloced --- src/analyses/wrapperFunctionAnalysis.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml index d9bbdb6197..99fac46d6c 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/src/analyses/wrapperFunctionAnalysis.ml @@ -133,7 +133,7 @@ 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 @@ -141,9 +141,12 @@ module MallocWrapper : MCPSpec = struct 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) From d8c59651549d3689a675579c1d9851aeeaa5cf56 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 20 Sep 2023 18:41:29 +0200 Subject: [PATCH 03/20] Update usage of HeapVar and IsHeapVar --- src/analyses/base.ml | 20 +++++++++++--------- src/analyses/mallocFresh.ml | 2 +- src/analyses/memLeak.ml | 4 ++-- 3 files changed, 14 insertions(+), 12 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 71e2661997..1212ceb9f4 100644 --- a/src/analyses/base.ml +++ b/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 -> diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml index 2c2b99a075..2eed772527 100644 --- a/src/analyses/mallocFresh.ml +++ b/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 diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 1bff7611a4..5b38ab79eb 100644 --- a/src/analyses/memLeak.ml +++ b/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 From 954be03ad32fcb685d2e04f50849df537b6c38f9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Wed, 20 Sep 2023 18:55:54 +0200 Subject: [PATCH 04/20] Add "alloca" as a library function --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 137a3103a5..326dedf434 100644 --- a/src/analyses/libraryFunctions.ml +++ b/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); From aa97af86c23911bd05822149a7d9c9fc4f819ae2 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 21 Sep 2023 09:38:24 +0200 Subject: [PATCH 05/20] Add Alloca special function type --- src/analyses/base.ml | 16 ++++++++++++---- src/analyses/libraryDesc.ml | 1 + src/analyses/libraryFunctions.ml | 3 ++- 3 files changed, 15 insertions(+), 5 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 1212ceb9f4..2138a51d41 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2263,14 +2263,22 @@ 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, fname -> begin + | Alloca size, _ -> begin + match lv with + | Some lv -> + let heap_var = AD.of_var (heap_var true ctx) in + (* ignore @@ printf "alloca 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)); + (eval_lv (Analyses.ask_of_ctx ctx) gs st lv, (Cilfacade.typeOfLval lv), Address heap_var)] + | _ -> st + end + | Malloc size, _ -> 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 is_stack_alloc ctx)) AD.null_ptr - else AD.of_var (heap_var is_stack_alloc ctx) + then AD.join (AD.of_var (heap_var false ctx)) AD.null_ptr + else AD.of_var (heap_var false 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)); diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 94de4fbf82..7cf68aa561 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -43,6 +43,7 @@ type math = (** Type of special function, or {!Unknown}. *) (* Use inline record if not single {!Cil.exp} argument. *) type special = + | Alloca of Cil.exp | Malloc of Cil.exp | Calloc of { count: Cil.exp; size: Cil.exp; } | Realloc of { ptr: Cil.exp; size: Cil.exp; } diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 326dedf434..0cc27f3523 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -63,8 +63,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strtok", unknown ~attrs:[ThreadUnsafe] [drop "str" [r; w]; drop "delim" [r]]); ("__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; }); + ("alloca", special [__ "size" []] @@ fun size -> Alloca size); ("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); @@ -1037,6 +1037,7 @@ let invalidate_actions = [ "sigaddset", writesAll;(*unsafe*) "raise", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) + "alloca", readsAll;(*safe*) "__builtin_alloca", readsAll;(*safe*) "dlopen", readsAll;(*safe*) "dlsym", readsAll;(*safe*) From 6e9bb2f121114a9c91bf1bb19557bbcfd0d3ffca Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 21 Sep 2023 09:39:42 +0200 Subject: [PATCH 06/20] Classify __builtin_alloca as Alloca and not as Malloc --- src/analyses/libraryFunctions.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 0cc27f3523..224b54907f 100644 --- a/src/analyses/libraryFunctions.ml +++ b/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; }); ("alloca", special [__ "size" []] @@ fun size -> Alloca size); + ("__builtin_alloca", special [__ "size" []] @@ fun size -> Alloca size); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size }); ("free", special [__ "ptr" [f]] @@ fun ptr -> Free ptr); @@ -891,7 +892,7 @@ let classify fn exps: categories = | [id; ret_var] -> `ThreadJoin (id, ret_var) | _ -> strange_arguments () end - | "kmalloc" | "__kmalloc" | "usb_alloc_urb" | "__builtin_alloca" -> + | "kmalloc" | "__kmalloc" | "usb_alloc_urb" -> begin match exps with | size::_ -> `Malloc size | _ -> strange_arguments () From d9df607e99ea78600b81f879955208ec00391bcb Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 21 Sep 2023 09:49:48 +0200 Subject: [PATCH 07/20] Implement and use IsHeapVar and IsDynamicallyAlloced right --- src/analyses/base.ml | 8 ++++---- src/analyses/memLeak.ml | 2 +- src/analyses/useAfterFree.ml | 4 ++-- src/analyses/wrapperFunctionAnalysis.ml | 4 ++-- src/domains/queries.ml | 2 +- 5 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 2138a51d41..7ee49603e9 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -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)) || (ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsDynamicallyAlloced v)) || o <> `NoOffset + | Addr (v,o) -> (not @@ ctx.ask (Queries.IsDynamicallyAlloced v)) || (ctx.ask (Queries.IsDynamicallyAlloced v) && not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset | _ -> false) a then Queries.Result.bot q else ( @@ -1383,7 +1383,7 @@ struct let t = match t_override with | Some t -> t | None -> - if a.f (Q.IsHeapVar x) then + if a.f (Q.IsDynamicallyAlloced x) then (* the vtype of heap vars will be TVoid, so we need to trust the pointer we got to this to be of the right type *) (* i.e. use the static type of the pointer here *) lval_type @@ -1429,7 +1429,7 @@ struct (* Optimization to avoid evaluating integer values when setting them. The case when invariant = true requires the old_value to be sound for the meet. Allocated blocks are representend by Blobs with additional information, so they need to be looked-up. *) - let old_value = if not invariant && Cil.isIntegralType x.vtype && not (a.f (IsHeapVar x)) && offs = `NoOffset then begin + let old_value = if not invariant && Cil.isIntegralType x.vtype && not (a.f (IsDynamicallyAlloced x)) && offs = `NoOffset then begin VD.bot_value ~varAttr:x.vattr lval_type end else Priv.read_global a priv_getg st x @@ -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)) || (ctx.ask (Q.IsHeapVar v) && not @@ ctx.ask (Q.IsDynamicallyAlloced v)) + | Addr (v,_) -> not (ctx.ask (Q.IsDynamicallyAlloced v)) || (ctx.ask (Q.IsDynamicallyAlloced v) && not @@ ctx.ask (Q.IsHeapVar v)) | _ -> false) in let has_non_zero_offset = AD.exists (function diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 5b38ab79eb..abf0deb954 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -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) && ctx.ask (Queries.IsDynamicallyAlloced 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.IsDynamicallyAlloced v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state (* Unique pointed to heap vars *) | _ -> state end | _ -> state diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 0aafbd1ad4..8c70322553 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -91,7 +91,7 @@ struct let pointed_to_heap_vars = Queries.AD.fold (fun addr vars -> match addr with - | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) -> v :: vars + | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsDynamicallyAlloced v) -> v :: vars | _ -> vars ) ad [] in @@ -185,7 +185,7 @@ struct let pointed_to_heap_vars = Queries.AD.fold (fun addr state -> match addr with - | Queries.AD.Addr.Addr (var,_) when ctx.ask (Queries.IsHeapVar var) -> D.add var state + | Queries.AD.Addr.Addr (var,_) when ctx.ask (Queries.IsDynamicallyAlloced var) -> D.add var state | _ -> state ) ad (D.empty ()) in diff --git a/src/analyses/wrapperFunctionAnalysis.ml b/src/analyses/wrapperFunctionAnalysis.ml index 99fac46d6c..43d472d0e3 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/src/analyses/wrapperFunctionAnalysis.ml @@ -144,9 +144,9 @@ module MallocWrapper : MCPSpec = struct 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.IsDynamicallyAlloced v -> + NodeVarinfoMap.mem_varinfo v | Q.IsMultiple v -> begin match NodeVarinfoMap.from_varinfo v with | Some (_, _, c) -> UniqueCount.is_top c || not (ctx.ask Q.MustBeUniqueThread) diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 5ddf417699..a5d1c727ab 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -101,7 +101,7 @@ type _ t = | DYojson: FlatYojson.t t (** Get local state Yojson of one path under [PathQuery]. *) | 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 *) + | IsDynamicallyAlloced: varinfo -> MayBool.t t (* [true] if heap var represents dynamically alloced memory *) | 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? *) From 4c84a102c2093066b28032cd0dc0cd4a653034c9 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 21 Sep 2023 12:50:44 +0200 Subject: [PATCH 08/20] CI run fix: remove alloca from invalidate_actions --- src/analyses/libraryFunctions.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 224b54907f..800d3e4902 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -1038,7 +1038,6 @@ let invalidate_actions = [ "sigaddset", writesAll;(*unsafe*) "raise", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) - "alloca", readsAll;(*safe*) "__builtin_alloca", readsAll;(*safe*) "dlopen", readsAll;(*safe*) "dlsym", readsAll;(*safe*) From 55a8f1e34a81c899bf5cff57a101139c2c240830 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 28 Sep 2023 15:41:58 +0200 Subject: [PATCH 09/20] Remove __builtin_alloca from invalidate_actions --- src/analyses/libraryFunctions.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 800d3e4902..e4f42cfaf2 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -1038,7 +1038,6 @@ let invalidate_actions = [ "sigaddset", writesAll;(*unsafe*) "raise", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) - "__builtin_alloca", readsAll;(*safe*) "dlopen", readsAll;(*safe*) "dlsym", readsAll;(*safe*) "dlclose", readsAll;(*safe*) From 21584eec15a258f47f5f9cb47b5daeef13ba0865 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 09:43:40 +0200 Subject: [PATCH 10/20] Extend UAF analysis to support alloca() --- src/analyses/useAfterFree.ml | 41 +++++++++++++++++++++++++----------- 1 file changed, 29 insertions(+), 12 deletions(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 8c70322553..c313c0a90b 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -4,7 +4,12 @@ open GoblintCil open Analyses open MessageCategory -module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) +module AllocaVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All alloca() Variables" end) +module HeapVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) + +(* Heap vars created by alloca() and deallocated at function exit * Heap vars deallocated by free() *) +module StackAndHeapVars = Lattice.Prod(AllocaVars)(HeapVars) + module ThreadIdSet = SetDomain.Make(ThreadIdDomain.ThreadLifted) module Spec : Analyses.MCPSpec = @@ -13,7 +18,7 @@ struct let name () = "useAfterFree" - module D = ToppedVarInfoSet + module D = StackAndHeapVars module C = Lattice.Unit module G = ThreadIdSet module V = VarinfoV @@ -57,7 +62,7 @@ struct let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in if not current_is_unique && any_equal_current freeing_threads then M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var - else if D.mem heap_var ctx.local then + else if HeapVars.mem heap_var (snd ctx.local) then M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Use-After-Free might occur in current unique thread %a for heap variable %a" ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var end | `Top -> @@ -85,7 +90,7 @@ struct match ctx.ask (Queries.MayPointTo lval_to_query) with | ad when not (Queries.AD.is_top ad) -> let warn_for_heap_var v = - if D.mem v state then + if HeapVars.mem v (snd state) then M.warn ~category:(Behavior undefined_behavior) ~tags:[CWE cwe_number] "lval (%s) in \"%s\" points to a maybe freed memory region" v.vname transfer_fn_name in let pointed_to_heap_vars = @@ -129,7 +134,7 @@ struct let side_effect_mem_free ctx freed_heap_vars threadid = let threadid = G.singleton threadid in - D.iter (fun var -> ctx.sideg var threadid) freed_heap_vars + HeapVars.iter (fun var -> ctx.sideg var threadid) freed_heap_vars (* TRANSFER FUNCTIONS *) @@ -153,7 +158,7 @@ struct let enter ctx (lval:lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = let caller_state = ctx.local in List.iter (fun arg -> warn_exp_might_contain_freed "enter" ctx arg) args; - if D.is_empty caller_state then + if AllocaVars.is_empty (fst caller_state) && HeapVars.is_empty (snd caller_state) then [caller_state, caller_state] else ( let reachable_from_args = List.fold_left (fun ad arg -> Queries.AD.join ad (ctx.ask (ReachableFrom arg))) (Queries.AD.empty ()) args in @@ -161,13 +166,18 @@ struct [caller_state, caller_state] else let reachable_vars = Queries.AD.to_var_may reachable_from_args in - let callee_state = D.filter (fun var -> List.mem var reachable_vars) caller_state in (* TODO: use AD.mem directly *) + let callee_state = (AllocaVars.empty (), HeapVars.filter (fun var -> List.mem var reachable_vars) (snd caller_state)) in (* TODO: use AD.mem directly *) [caller_state, callee_state] ) let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask:Queries.ask) : D.t = - let caller_state = ctx.local in - D.join caller_state callee_local + let (caller_stack_state, caller_heap_state) = ctx.local in + let callee_stack_state = fst callee_local in + let callee_heap_state = snd callee_local in + (* Put all alloca()-vars together with all freed() vars in the caller's second component *) + (* Don't change caller's first component => caller hasn't exited yet *) + let callee_combined_state = HeapVars.join callee_stack_state callee_heap_state in + (caller_stack_state, HeapVars.join caller_heap_state callee_combined_state) let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (callee_local:D.t) (f_ask: Queries.ask): D.t = Option.iter (fun x -> warn_lval_might_contain_freed "enter" ctx x) lval; @@ -185,13 +195,20 @@ struct let pointed_to_heap_vars = Queries.AD.fold (fun addr state -> match addr with - | Queries.AD.Addr.Addr (var,_) when ctx.ask (Queries.IsDynamicallyAlloced var) -> D.add var state + | Queries.AD.Addr.Addr (var,_) when ctx.ask (Queries.IsDynamicallyAlloced var) && ctx.ask (Queries.IsHeapVar var) -> HeapVars.add var state | _ -> state - ) ad (D.empty ()) + ) ad (HeapVars.empty ()) in (* Side-effect the tid that's freeing all the heap vars collected here *) side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx); - D.join state (pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *) + (* Add all heap vars, which ptr points to, to the state *) + (fst state, HeapVars.join (snd state) pointed_to_heap_vars) + | _ -> state + end + | Alloca _ -> + (* Create fresh heap var for the alloca() call *) + begin match ctx.ask (Queries.HeapVar {on_stack = true}) with + | `Lifted v -> (AllocaVars.add v (fst state), snd state) | _ -> state end | _ -> state From 05a3b98ea27b42994d275e14e43fb372c8337a2c Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 09:44:02 +0200 Subject: [PATCH 11/20] Add alloca() UAF test case --- .../regression/74-use_after_free/13-alloca-uaf.c | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 tests/regression/74-use_after_free/13-alloca-uaf.c diff --git a/tests/regression/74-use_after_free/13-alloca-uaf.c b/tests/regression/74-use_after_free/13-alloca-uaf.c new file mode 100644 index 0000000000..bb052b010c --- /dev/null +++ b/tests/regression/74-use_after_free/13-alloca-uaf.c @@ -0,0 +1,16 @@ +//PARAM: --set ana.activated[+] useAfterFree +#include +#include + +int *f() { + int *c = alloca(sizeof(int)); + return c; +} + +int main(int argc, char const *argv[]) { + int *ps = alloca(sizeof(int)); + int *c = f(); + int a = *ps; + int b = *c; //WARN + return 0; +} From 2fbcdb8d19e8e84998d2d709fb47bd949d743549 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 09:44:22 +0200 Subject: [PATCH 12/20] Add alloca() invalid dealloc test case --- .../09-juliet-invalid-dealloc-alloca.c | 75 +++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 tests/regression/75-invalid_dealloc/09-juliet-invalid-dealloc-alloca.c diff --git a/tests/regression/75-invalid_dealloc/09-juliet-invalid-dealloc-alloca.c b/tests/regression/75-invalid_dealloc/09-juliet-invalid-dealloc-alloca.c new file mode 100644 index 0000000000..9a84d1e49a --- /dev/null +++ b/tests/regression/75-invalid_dealloc/09-juliet-invalid-dealloc-alloca.c @@ -0,0 +1,75 @@ +#include +#include + +typedef struct twoIntsStruct { + int intOne ; + int intTwo ; +} twoIntsStruct; + +void CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54_bad(void) { + twoIntsStruct *data; + data = (twoIntsStruct *)0; + { + twoIntsStruct *dataBuffer = __builtin_alloca(800UL); + { + size_t i; + i = 0UL; + + goto ldv_3204; + ldv_3203: + ; + + (dataBuffer + i)->intOne = 1; + (dataBuffer + i)->intTwo = 1; + + i += 1UL; + ldv_3204: + ; + + if (i <= 99UL) + goto ldv_3203; + else + goto ldv_3205; + ldv_3205: + ; + } + + data = dataBuffer; + } + + CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54b_badSink(data); + return; +} + +void CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54b_badSink(twoIntsStruct *data) { + CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54c_badSink(data); + return; +} + +void CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54c_badSink(twoIntsStruct *data) { + CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54d_badSink(data); + return; +} + +void CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54d_badSink(twoIntsStruct *data) { + CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54e_badSink(data); + return; +} + +void CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54e_badSink(twoIntsStruct *data) { + free((void *)data); //WARN + return; +} + +int main(int argc, char **argv) { + int __retres; + { + CWE590_Free_Memory_Not_on_Heap__free_struct_alloca_54_bad(); + __retres = 0; + goto return_label; + } + + __retres = 0; + return_label: + return __retres; +} From 5cca543065efea0562294392a4dec1d6833b4b58 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 10:17:57 +0200 Subject: [PATCH 13/20] Add forgotton base_address check in BlobSize after master merge --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index b825bafab0..21513cc175 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1249,7 +1249,7 @@ struct (* If there's a non-heap var or an offset in the lval set, we answer with bottom *) (* If we're asking for the BlobSize from the base address, then don't check for offsets => we want to avoid getting bot *) if AD.exists (function - | Addr (v,o) -> (not @@ ctx.ask (Queries.IsDynamicallyAlloced v)) || (ctx.ask (Queries.IsDynamicallyAlloced v) && not @@ ctx.ask (Queries.IsHeapVar v)) || o <> `NoOffset + | Addr (v,o) -> (not @@ ctx.ask (Queries.IsDynamicallyAlloced v)) || (ctx.ask (Queries.IsDynamicallyAlloced v) && not @@ ctx.ask (Queries.IsHeapVar v)) || (if not from_base_addr then o <> `NoOffset else false) | _ -> false) a then Queries.Result.bot q else ( From 4090e7498b43093c2fd1a8a3250194b03c72043c Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 10:20:36 +0200 Subject: [PATCH 14/20] Fix __builtin_alloca classification --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 2388bff586..c8c9a25ec1 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -440,7 +440,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__sync_fetch_and_add", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' []))); ("__sync_fetch_and_sub", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' []))); ("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]); - ("__builtin_alloca", special [__ "size" []] @@ fun size -> Malloc size); + ("__builtin_alloca", special [__ "size" []] @@ fun size -> Alloca size); ] let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ From 35513d09c2ed2a0fb6f00a1e0dd1854f9dd79329 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 11:27:35 +0200 Subject: [PATCH 15/20] Move all *alloca() functions to gcc_descs_list --- src/analyses/libraryFunctions.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index c8c9a25ec1..87f7ef0572 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -64,8 +64,6 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strtok", unknown ~attrs:[ThreadUnsafe] [drop "str" [r; w]; drop "delim" [r]]); ("__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; }); - ("alloca", special [__ "size" []] @@ fun size -> Alloca size); - ("__builtin_alloca", special [__ "size" []] @@ fun size -> Alloca size); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); ("calloc", special [__ "n" []; __ "size" []] @@ fun n size -> Calloc {count = n; size}); ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size }); @@ -440,6 +438,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__sync_fetch_and_add", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' []))); ("__sync_fetch_and_sub", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' []))); ("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]); + ("alloca", special [__ "size" []] @@ fun size -> Alloca size); ("__builtin_alloca", special [__ "size" []] @@ fun size -> Alloca size); ] From 432a4e3259bea4ac597de6bf78db30f86ba101ae Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 13:31:31 +0300 Subject: [PATCH 16/20] Simply HeapVar ask in heap_var Co-authored-by: Simmo Saan --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 21513cc175..f2c4c4ed65 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -151,7 +151,7 @@ struct let longjmp_return = ref dummyFunDec.svar let heap_var on_stack ctx = - let info = match (ctx.ask (Q.HeapVar {on_stack = on_stack})) with + let info = match (ctx.ask (Q.HeapVar {on_stack})) with | `Lifted vinfo -> vinfo | _ -> failwith("Ran without a malloc analysis.") in info From 3bdc92d7c6e58520f6ed552cb687fa158adcf429 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 12:41:48 +0200 Subject: [PATCH 17/20] Extract long query ask into own function --- src/analyses/base.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index f2c4c4ed65..1c21da3327 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1122,6 +1122,9 @@ struct (* interpreter end *) + let is_not_heap_alloc_var ctx v = + (not (ctx.ask (Queries.IsDynamicallyAlloced v))) || (ctx.ask (Queries.IsDynamicallyAlloced v) && not (ctx.ask (Queries.IsHeapVar v))) + let query_invariant ctx context = let cpa = ctx.local.BaseDomain.cpa in let ask = Analyses.ask_of_ctx ctx in @@ -1249,7 +1252,7 @@ struct (* If there's a non-heap var or an offset in the lval set, we answer with bottom *) (* If we're asking for the BlobSize from the base address, then don't check for offsets => we want to avoid getting bot *) if AD.exists (function - | Addr (v,o) -> (not @@ ctx.ask (Queries.IsDynamicallyAlloced v)) || (ctx.ask (Queries.IsDynamicallyAlloced v) && not @@ ctx.ask (Queries.IsHeapVar v)) || (if not from_base_addr then o <> `NoOffset else false) + | Addr (v,o) -> is_not_heap_alloc_var ctx v || (if not from_base_addr then o <> `NoOffset else false) | _ -> false) a then Queries.Result.bot q else ( @@ -2009,7 +2012,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.IsDynamicallyAlloced v)) || (ctx.ask (Q.IsDynamicallyAlloced v) && not @@ ctx.ask (Q.IsHeapVar v)) + | Addr (v,_) -> is_not_heap_alloc_var ctx v | _ -> false) in let has_non_zero_offset = AD.exists (function From 7b1d29850036fb1287b10c8aeb962a162b7fac11 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 12:50:34 +0200 Subject: [PATCH 18/20] Rename queries: * HeapVar -> AllocVar * IsDynamicallyAlloced -> IsAllocVar --- src/analyses/base.ml | 10 +++++----- src/analyses/mallocFresh.ml | 2 +- src/analyses/memLeak.ml | 4 ++-- src/analyses/useAfterFree.ml | 6 +++--- src/analyses/wrapperFunctionAnalysis.ml | 4 ++-- src/domains/queries.ml | 26 +++++++++++++------------ 6 files changed, 27 insertions(+), 25 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 1c21da3327..dacd412072 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -151,7 +151,7 @@ struct let longjmp_return = ref dummyFunDec.svar let heap_var on_stack ctx = - let info = match (ctx.ask (Q.HeapVar {on_stack})) with + let info = match (ctx.ask (Q.AllocVar {on_stack})) with | `Lifted vinfo -> vinfo | _ -> failwith("Ran without a malloc analysis.") in info @@ -1123,7 +1123,7 @@ struct (* interpreter end *) let is_not_heap_alloc_var ctx v = - (not (ctx.ask (Queries.IsDynamicallyAlloced v))) || (ctx.ask (Queries.IsDynamicallyAlloced v) && not (ctx.ask (Queries.IsHeapVar v))) + (not (ctx.ask (Queries.IsAllocVar v))) || (ctx.ask (Queries.IsAllocVar v) && not (ctx.ask (Queries.IsHeapVar v))) let query_invariant ctx context = let cpa = ctx.local.BaseDomain.cpa in @@ -1400,7 +1400,7 @@ struct let t = match t_override with | Some t -> t | None -> - if a.f (Q.IsDynamicallyAlloced x) then + if a.f (Q.IsAllocVar x) then (* the vtype of heap vars will be TVoid, so we need to trust the pointer we got to this to be of the right type *) (* i.e. use the static type of the pointer here *) lval_type @@ -1446,7 +1446,7 @@ struct (* Optimization to avoid evaluating integer values when setting them. The case when invariant = true requires the old_value to be sound for the meet. Allocated blocks are representend by Blobs with additional information, so they need to be looked-up. *) - let old_value = if not invariant && Cil.isIntegralType x.vtype && not (a.f (IsDynamicallyAlloced x)) && offs = `NoOffset then begin + let old_value = if not invariant && Cil.isIntegralType x.vtype && not (a.f (IsAllocVar x)) && offs = `NoOffset then begin VD.bot_value ~varAttr:x.vattr lval_type end else Priv.read_global a priv_getg st x @@ -2596,7 +2596,7 @@ struct | MayBeThreadReturn | PartAccess _ | IsHeapVar _ - | IsDynamicallyAlloced _ + | IsAllocVar _ | IsMultiple _ | CreatedThreads | MustJoinedThreads -> diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml index 2eed772527..3a501fc72f 100644 --- a/src/analyses/mallocFresh.ml +++ b/src/analyses/mallocFresh.ml @@ -43,7 +43,7 @@ struct | Malloc _ | Calloc _ | Realloc _ -> - begin match ctx.ask (HeapVar {on_stack = false}) with + begin match ctx.ask (AllocVar {on_stack = false}) with | `Lifted var -> D.add var ctx.local | _ -> ctx.local end diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index abf0deb954..8576096dfe 100644 --- a/src/analyses/memLeak.ml +++ b/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 {on_stack = false}) with + begin match ctx.ask (Queries.AllocVar {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.IsDynamicallyAlloced v) && 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.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> D.remove v state (* Unique pointed to heap vars *) | _ -> state end | _ -> state diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index c313c0a90b..7e89dddb69 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -96,7 +96,7 @@ struct let pointed_to_heap_vars = Queries.AD.fold (fun addr vars -> match addr with - | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsDynamicallyAlloced v) -> v :: vars + | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) -> v :: vars | _ -> vars ) ad [] in @@ -195,7 +195,7 @@ struct let pointed_to_heap_vars = Queries.AD.fold (fun addr state -> match addr with - | Queries.AD.Addr.Addr (var,_) when ctx.ask (Queries.IsDynamicallyAlloced var) && ctx.ask (Queries.IsHeapVar var) -> HeapVars.add var state + | Queries.AD.Addr.Addr (var,_) when ctx.ask (Queries.IsAllocVar var) && ctx.ask (Queries.IsHeapVar var) -> HeapVars.add var state | _ -> state ) ad (HeapVars.empty ()) in @@ -207,7 +207,7 @@ struct end | Alloca _ -> (* Create fresh heap var for the alloca() call *) - begin match ctx.ask (Queries.HeapVar {on_stack = true}) with + begin match ctx.ask (Queries.AllocVar {on_stack = true}) 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 43d472d0e3..5c0176df48 100644 --- a/src/analyses/wrapperFunctionAnalysis.ml +++ b/src/analyses/wrapperFunctionAnalysis.ml @@ -133,7 +133,7 @@ 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 {on_stack = on_stack} -> + | Q.AllocVar {on_stack = on_stack} -> let node = match wrapper_node with | `Lifted wrapper_node -> wrapper_node | _ -> node_for_ctx ctx @@ -145,7 +145,7 @@ module MallocWrapper : MCPSpec = struct `Lifted var | Q.IsHeapVar v -> NodeVarinfoMap.mem_varinfo v && not @@ hasAttribute "stack_alloca" v.vattr - | Q.IsDynamicallyAlloced v -> + | Q.IsAllocVar v -> NodeVarinfoMap.mem_varinfo v | Q.IsMultiple v -> begin match NodeVarinfoMap.from_varinfo v with diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 07e239bee5..c706339bf2 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -101,9 +101,11 @@ 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: {on_stack: bool} -> VI.t t (* If on_stack is [true], then alloca() or a similar function was called *) + | AllocVar: {on_stack: bool} -> 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 *) | IsHeapVar: varinfo -> MayBool.t t (* TODO: is may or must? *) - | IsDynamicallyAlloced: varinfo -> MayBool.t t (* [true] if heap var represents dynamically alloced memory *) | 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? *) @@ -155,7 +157,7 @@ struct | MayBePublicWithout _ -> (module MayBool) | MayBeThreadReturn -> (module MayBool) | IsHeapVar _ -> (module MayBool) - | IsDynamicallyAlloced _ -> (module MayBool) + | IsAllocVar _ -> (module MayBool) | MustBeProtectedBy _ -> (module MustBool) | MustBeAtomic -> (module MustBool) | MustBeSingleThreaded _ -> (module MustBool) @@ -167,7 +169,7 @@ struct | BlobSize _ -> (module ID) | CurrentThreadId -> (module ThreadIdDomain.ThreadLifted) | ThreadCreateIndexedNode -> (module ThreadNodeLattice) - | HeapVar _ -> (module VI) + | AllocVar _ -> (module VI) | EvalStr _ -> (module SD) | IterPrevVars _ -> (module Unit) | IterVars _ -> (module Unit) @@ -220,7 +222,7 @@ struct | MayBePublicWithout _ -> MayBool.top () | MayBeThreadReturn -> MayBool.top () | IsHeapVar _ -> MayBool.top () - | IsDynamicallyAlloced _ -> MayBool.top () + | IsAllocVar _ -> MayBool.top () | MutexType _ -> MutexAttrDomain.top () | MustBeProtectedBy _ -> MustBool.top () | MustBeAtomic -> MustBool.top () @@ -233,7 +235,7 @@ struct | BlobSize _ -> ID.top () | CurrentThreadId -> ThreadIdDomain.ThreadLifted.top () | ThreadCreateIndexedNode -> ThreadNodeLattice.top () - | HeapVar _ -> VI.top () + | AllocVar _ -> VI.top () | EvalStr _ -> SD.top () | IterPrevVars _ -> Unit.top () | IterVars _ -> Unit.top () @@ -293,7 +295,7 @@ struct | Any (PartAccess _) -> 23 | Any (IterPrevVars _) -> 24 | Any (IterVars _) -> 25 - | Any (HeapVar _) -> 29 + | Any (AllocVar _) -> 29 | Any (IsHeapVar _) -> 30 | Any (IsMultiple _) -> 31 | Any (EvalThread _) -> 32 @@ -318,7 +320,7 @@ struct | Any ThreadCreateIndexedNode -> 51 | Any ThreadsJoinedCleanly -> 52 | Any (TmpSpecial _) -> 53 - | Any (IsDynamicallyAlloced _) -> 54 + | Any (IsAllocVar _) -> 54 let rec compare a b = let r = Stdlib.compare (order a) (order b) in @@ -358,7 +360,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 (IsAllocVar v1), Any (IsAllocVar 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 @@ -399,7 +401,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 (IsAllocVar 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 @@ -447,9 +449,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 {on_stack = on_stack}) -> Pretty.dprintf "HeapVar %b" on_stack + | Any (AllocVar {on_stack = on_stack}) -> Pretty.dprintf "AllocVar %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 (IsAllocVar v) -> Pretty.dprintf "IsAllocVar %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 From 5f162216927f10cf42a9b1b5ad50ddea0bd4868d Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 13:13:46 +0200 Subject: [PATCH 19/20] Fix wrong query usage in UAF --- src/analyses/useAfterFree.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index f3dbecacc2..02231336c0 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -121,7 +121,7 @@ struct let pointed_to_heap_vars = Queries.AD.fold (fun addr vars -> match addr with - | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsHeapVar v) -> v :: vars + | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) -> v :: vars | _ -> vars ) ad [] in From b1f2f2d9a5f3a665bdd63445f1d4796338b59401 Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Fri, 29 Sep 2023 13:14:04 +0200 Subject: [PATCH 20/20] Fix test numbering --- .../74-use_after_free/{13-alloca-uaf.c => 14-alloca-uaf.c} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename tests/regression/74-use_after_free/{13-alloca-uaf.c => 14-alloca-uaf.c} (91%) diff --git a/tests/regression/74-use_after_free/13-alloca-uaf.c b/tests/regression/74-use_after_free/14-alloca-uaf.c similarity index 91% rename from tests/regression/74-use_after_free/13-alloca-uaf.c rename to tests/regression/74-use_after_free/14-alloca-uaf.c index bb052b010c..3dc494cb09 100644 --- a/tests/regression/74-use_after_free/13-alloca-uaf.c +++ b/tests/regression/74-use_after_free/14-alloca-uaf.c @@ -10,7 +10,7 @@ int *f() { int main(int argc, char const *argv[]) { int *ps = alloca(sizeof(int)); int *c = f(); - int a = *ps; + int a = *ps; //NOWARN int b = *c; //WARN return 0; }