Skip to content

Commit

Permalink
Update usage of HeapVar and IsHeapVar
Browse files Browse the repository at this point in the history
  • Loading branch information
mrstanb committed Sep 20, 2023
1 parent 9a06189 commit d8c5965
Show file tree
Hide file tree
Showing 3 changed files with 14 additions and 12 deletions.
20 changes: 11 additions & 9 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 (
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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));
Expand All @@ -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 *)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -2563,6 +2564,7 @@ struct
| MayBeThreadReturn
| PartAccess _
| IsHeapVar _
| IsDynamicallyAlloced _
| IsMultiple _
| CreatedThreads
| MustJoinedThreads ->
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/mallocFresh.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions src/analyses/memLeak.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit d8c5965

Please sign in to comment.