From d9df607e99ea78600b81f879955208ec00391bcb Mon Sep 17 00:00:00 2001 From: Stanimir Bozhilov Date: Thu, 21 Sep 2023 09:49:48 +0200 Subject: [PATCH] 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? *)