Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix BlobSize for calloc #1262

Merged
merged 3 commits into from
Nov 22, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 11 additions & 2 deletions src/analyses/base.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1139,6 +1139,9 @@ struct

(* interpreter end *)

let is_not_alloc_var ctx v =
not (ctx.ask (Queries.IsAllocVar v))

let is_not_heap_alloc_var ctx v =
let is_alloc = ctx.ask (Queries.IsAllocVar v) in
not is_alloc || (is_alloc && not (ctx.ask (Queries.IsHeapVar v)))
Expand Down Expand Up @@ -1277,7 +1280,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) -> is_not_heap_alloc_var ctx v || (if not from_base_addr then o <> `NoOffset else false)
| Addr (v,o) -> is_not_alloc_var ctx v || (if not from_base_addr then o <> `NoOffset else false)
| _ -> false) a then
Queries.Result.bot q
else (
Expand All @@ -1289,9 +1292,15 @@ struct
else
a
in
let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a None in
let r = get ~full:true (Analyses.ask_of_ctx ctx) ctx.global ctx.local a None in
(* ignore @@ printf "BlobSize %a = %a\n" d_plainexp e VD.pretty r; *)
(match r with
| Array a ->
(* unroll into array for Calloc calls *)
(match ValueDomain.CArrays.get (Queries.to_value_domain_ask (Analyses.ask_of_ctx ctx)) a (None, (IdxDom.of_int (Cilfacade.ptrdiff_ikind ()) BI.zero)) with
| Blob (_,s,_) -> `Lifted s
| _ -> Queries.Result.top q
)
| Blob (_,s,_) -> `Lifted s
| _ -> Queries.Result.top q)
)
Expand Down
6 changes: 3 additions & 3 deletions src/analyses/memOutOfBounds.ml
Original file line number Diff line number Diff line change
Expand Up @@ -69,17 +69,17 @@ struct
in
host_contains_a_ptr host || offset_contains_a_ptr offset

let points_to_heap_only ctx ptr =
let points_to_alloc_only ctx ptr =
match ctx.ask (Queries.MayPointTo ptr) with
| a when not (Queries.AD.is_top a)->
Queries.AD.for_all (function
| Addr (v, o) -> ctx.ask (Queries.IsHeapVar v)
| Addr (v, o) -> ctx.ask (Queries.IsAllocVar v)
| _ -> false
) a
| _ -> false

let get_size_of_ptr_target ctx ptr =
if points_to_heap_only ctx ptr then
if points_to_alloc_only ctx ptr then
(* Ask for BlobSize from the base address (the second component being set to true) in order to avoid BlobSize giving us bot *)
ctx.ask (Queries.BlobSize {exp = ptr; base_address = true})
else
Expand Down
9 changes: 9 additions & 0 deletions tests/regression/74-invalid_deref/30-calloc.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
//PARAM: --set ana.activated[+] useAfterFree --set ana.activated[+] threadJoins --set ana.activated[+] memOutOfBounds --enable ana.int.interval --set ana.base.arrays.domain partitioned
#include <pthread.h>
#include <goblint.h>

int main(int argc, char **argv)
{
int* ptrCalloc = calloc(100UL,8UL);
*ptrCalloc = 8; //NOWARN
}
Loading