Skip to content

Commit

Permalink
Merge branch 'master' into svcomp24-dev
Browse files Browse the repository at this point in the history
  • Loading branch information
@sim642
sim642 committed Nov 22, 2023
2 parents 9c65057 + 3414f4f commit af1ddef
Show file tree
Hide file tree
Showing 5 changed files with 43 additions and 8 deletions.
13 changes: 11 additions & 2 deletions src/analyses/base.ml
View file
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
19 changes: 18 additions & 1 deletion src/analyses/libraryFunctions.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("iswspace", unknown [drop "wc" []]);
("iswalnum", unknown [drop "wc" []]);
("iswprint", unknown [drop "wc" []]);
("iswxdigit", unknown [drop "ch" []]);
("rename" , unknown [drop "oldpath" [r]; drop "newpath" [r];]);
("perror", unknown [drop "s" [r]]);
("getchar", unknown []);
Expand Down Expand Up @@ -118,8 +119,10 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *)
("mktime", unknown [drop "tm" [r;w]]);
("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]);
("clearerr", unknown [drop "stream" [w]]);
("clearerr", unknown [drop "stream" [w]]); (* TODO: why only w? *)
("setbuf", unknown [drop "stream" [w]; drop "buf" [w]]);
("wprintf", unknown (drop "fmt" [r] :: VarArgs (drop' [r])));
("fwprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "fmt" [r] :: VarArgs (drop' [r])));
("swprintf", unknown (drop "wcs" [w] :: drop "maxlen" [] :: drop "fmt" [r] :: VarArgs (drop' [r])));
("assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" }); (* only used if assert is used without include, e.g. in transformed files *)
("difftime", unknown [drop "time1" []; drop "time2" []]);
Expand All @@ -133,6 +136,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (IInt, j)) });
("labs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) });
("llabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILongLong, j)) });
("imaxabs", unknown [drop "j" []]);
("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]);
("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]);
("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
Expand All @@ -151,6 +155,10 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("atomic_load", unknown [drop "obj" [r]]);
("atomic_store", unknown [drop "obj" [w]; drop "desired" []]);
("_Exit", special [drop "status" []] @@ Abort);
("strcoll", unknown [drop "lhs" [r]; drop "rhs" [r]]);
("wscanf", unknown (drop "fmt" [r] :: VarArgs (drop' [w])));
("fwscanf", unknown (drop "stream" [r_deep; w_deep] :: drop "fmt" [r] :: VarArgs (drop' [w])));
("swscanf", unknown (drop "buffer" [r] :: drop "fmt" [r] :: VarArgs (drop' [w])));
]

(** C POSIX library functions.
Expand Down Expand Up @@ -300,6 +308,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("sendto", unknown [drop "sockfd" []; drop "buf" [r]; drop "len" []; drop "flags" []; drop "dest_addr" [r_deep]; drop "addrlen" []]);
("strdup", unknown [drop "s" [r]]);
("strndup", unknown [drop "s" [r]; drop "n" []]);
("__strndup", unknown [drop "s" [r]; drop "n" []]);
("syscall", unknown (drop "number" [] :: VarArgs (drop' [r; w])));
("sysconf", unknown [drop "name" []]);
("syslog", unknown (drop "priority" [] :: drop "format" [r] :: VarArgs (drop' [r]))); (* TODO: is the VarArgs correct here? *)
Expand Down Expand Up @@ -408,6 +417,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("srandom", unknown [drop "seed" []]);
("random", special [] Rand);
("posix_memalign", unknown [drop "memptr" [w]; drop "alignment" []; drop "size" []]); (* TODO: Malloc *)
("stpcpy", unknown [drop "dest" [w]; drop "src" [r]]);
]

(** Pthread functions. *)
Expand Down Expand Up @@ -571,6 +581,10 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[

let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
("fputs_unlocked", unknown [drop "s" [r]; drop "stream" [w]]);
("feof_unlocked", unknown [drop "stream" [r_deep; w_deep]]);
("ferror_unlocked", unknown [drop "stream" [r_deep; w_deep]]);
("fwrite_unlocked", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
("clearerr_unlocked", unknown [drop "stream" [w]]); (* TODO: why only w? *)
("futimesat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "times" [r]]);
("error", unknown ((drop "status" []) :: (drop "errnum" []) :: (drop "format" [r]) :: (VarArgs (drop' [r]))));
("warn", unknown (drop "format" [r] :: VarArgs (drop' [r])));
Expand All @@ -582,6 +596,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[
("__fgets_chk", unknown [drop "__s" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
("__fread_alias", unknown [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
("__fread_chk", unknown [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
("__fread_chk_warn", unknown [drop "buffer" [w]; drop "os" []; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
("fread_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "buffer" [w]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]);
("__fread_unlocked_alias", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
("__fread_unlocked_chk", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);
Expand Down Expand Up @@ -654,6 +669,8 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
("fstatfs", unknown [drop "fd" []; drop "buf" [w]]);
("cfmakeraw", unknown [drop "termios" [r; w]]);
("process_vm_readv", unknown [drop "pid" []; drop "local_iov" [w_deep]; drop "liovcnt" []; drop "remote_iov" []; drop "riovcnt" []; drop "flags" []]);
("__libc_current_sigrtmax", unknown []);
("__libc_current_sigrtmin", unknown []);
]

let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType)))
Expand Down
6 changes: 3 additions & 3 deletions src/analyses/memOutOfBounds.ml
View file
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
4 changes: 2 additions & 2 deletions tests/regression/29-svcomp/32-no-ov.t
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
$ goblint --enable ana.int.interval --enable ana.sv-comp.enabled --enable ana.sv-comp.functions --set ana.specification "CHECK( init(main()), LTL(G ! overflow) )" 32-no-ov.c
SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (32-no-ov.c:5:6-5:159)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (32-no-ov.c:5:6-5:159)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (32-no-ov.c:5:6-5:159)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (32-no-ov.c:5:6-5:159)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (32-no-ov.c:5:6-5:159)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (32-no-ov.c:5:6-5:159)
[Info][Deadcode] Logical lines of code (LLoC) summary:
Expand Down
9 changes: 9 additions & 0 deletions tests/regression/74-invalid_deref/30-calloc.c
View file
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
}

0 comments on commit af1ddef

Please sign in to comment.