From a432e47951b2c54660e23e6356917ef259d965e9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 8 Dec 2023 19:46:59 +0100 Subject: [PATCH 1/5] Port 6 specs --- src/util/library/libraryFunctions.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 2c65f7ae61..d91ee61d12 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -159,6 +159,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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]))); + ("remove", unknown [drop "pathname" [r]]); + ("raise", unknown [drop "sig" []]); (* safe-ish, we don't handle signal handlers for now *) ] (** C POSIX library functions. @@ -418,6 +420,10 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("random", special [] Rand); ("posix_memalign", unknown [drop "memptr" [w]; drop "alignment" []; drop "size" []]); (* TODO: Malloc *) ("stpcpy", unknown [drop "dest" [w]; drop "src" [r]]); + ("dup", unknown [drop "oldfd" []]); + ("readdir_r", unknown [drop "dirp" [r_deep]; drop "entry" [r_deep]; drop "result" [w]]); + ("pipe", unknown [drop "pipefd" [w_deep]]); + ("waitpid", unknown [drop "pid" []; drop "wstatus" [w]; drop "options" []]); ] (** Pthread functions. *) @@ -1246,16 +1252,12 @@ let invalidate_actions = [ "__errno_location", readsAll;(*safe*) "__strdup", readsAll;(*safe*) "strtoul__extinline", readsAll;(*safe*) - "readdir_r", writesAll;(*unsafe*) "atoi__extinline", readsAll;(*safe*) "_IO_getc", writesAll;(*unsafe*) - "pipe", writesAll;(*unsafe*) "strerror_r", writesAll;(*unsafe*) - "raise", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) - "waitpid", readsAll;(*safe*) "__open_alias", readsAll;(*safe*) "__open_2", readsAll;(*safe*) "ioctl", writesAll;(*unsafe*) @@ -1280,7 +1282,6 @@ let invalidate_actions = [ "svcudp_create", readsAll;(*safe*) "svc_register", writesAll;(*unsafe*) "svc_run", writesAll;(*unsafe*) - "dup", readsAll; (*safe*) "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) "__error", readsAll; (*safe*) @@ -1294,7 +1295,6 @@ let invalidate_actions = [ "uncompress", writes [3;4]; (*keep [3;4]*) "__xstat", writes [3]; (*keep [1]*) "__lxstat", writes [3]; (*keep [1]*) - "remove", readsAll; "BZ2_bzBuffToBuffCompress", writes [3;4]; (*keep [3;4]*) "compress2", writes [3]; (*keep [3]*) "__toupper", readsAll; (*safe*) From 1823684fa70be0993a62363f7285840e6396c552 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 8 Dec 2023 20:12:48 +0100 Subject: [PATCH 2/5] Port 5 specs --- src/util/library/libraryFunctions.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index d91ee61d12..4866f2aa17 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -424,6 +424,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("readdir_r", unknown [drop "dirp" [r_deep]; drop "entry" [r_deep]; drop "result" [w]]); ("pipe", unknown [drop "pipefd" [w_deep]]); ("waitpid", unknown [drop "pid" []; drop "wstatus" [w]; drop "options" []]); + ("strerror_r", unknown [drop "errnum" []; drop "buff" [w]; drop "buflen" []]); + ("umask", unknown [drop "mask" []]); + ("openlog", unknown [drop "ident" [r]; drop "option" []; drop "facility" []]); ] (** Pthread functions. *) @@ -644,6 +647,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strchrnul", unknown [drop "s" [r]; drop "c" []]); ("getdtablesize", unknown []); ("daemon", unknown [drop "nochdir" []; drop "noclose" []]); + ("putw", unknown [drop "w" []; drop "stream" [r_deep; w_deep]]); ] let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -741,6 +745,7 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__kmalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Malloc size); ("kzalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Calloc {count = Cil.one; size}); ("usb_alloc_urb", special [__ "iso_packets" []; drop "mem_flags" []] @@ fun iso_packets -> Malloc MyCFG.unknown_exp); + ("ioctl", unknown (drop "fd" [] :: drop "request" [] :: VarArgs (drop' [r]))); ] (** Goblint functions. *) @@ -1254,24 +1259,19 @@ let invalidate_actions = [ "strtoul__extinline", readsAll;(*safe*) "atoi__extinline", readsAll;(*safe*) "_IO_getc", writesAll;(*unsafe*) - "strerror_r", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "__open_alias", readsAll;(*safe*) "__open_2", readsAll;(*safe*) - "ioctl", writesAll;(*unsafe*) "fstat__extinline", writesAll;(*unsafe*) "scandir", writes [1;3;4];(*keep [1;3;4]*) "bindtextdomain", readsAll;(*safe*) "textdomain", readsAll;(*safe*) "dcgettext", readsAll;(*safe*) - "putw", readsAll;(*safe*) "__getdelim", writes [3];(*keep [3]*) "__h_errno_location", readsAll;(*safe*) "__fxstat", readsAll;(*safe*) - "openlog", readsAll;(*safe*) - "umask", readsAll;(*safe*) "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*) "svctcp_create", readsAll;(*safe*) "clntudp_bufcreate", writesAll;(*unsafe*) From 7d50626caa4883cbcb625a41016cbca7cf166941 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 8 Dec 2023 20:20:07 +0100 Subject: [PATCH 3/5] Port 2 more specs --- src/util/library/libraryFunctions.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 4866f2aa17..bb2b89c364 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -161,6 +161,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("swscanf", unknown (drop "buffer" [r] :: drop "fmt" [r] :: VarArgs (drop' [w]))); ("remove", unknown [drop "pathname" [r]]); ("raise", unknown [drop "sig" []]); (* safe-ish, we don't handle signal handlers for now *) + ("timespec_get", unknown [drop "ts" [w]; drop "base" []]); ] (** C POSIX library functions. @@ -427,6 +428,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strerror_r", unknown [drop "errnum" []; drop "buff" [w]; drop "buflen" []]); ("umask", unknown [drop "mask" []]); ("openlog", unknown [drop "ident" [r]; drop "option" []; drop "facility" []]); + ("times", unknown [drop "buf" [w]]) ] (** Pthread functions. *) @@ -1272,6 +1274,7 @@ let invalidate_actions = [ "__getdelim", writes [3];(*keep [3]*) "__h_errno_location", readsAll;(*safe*) "__fxstat", readsAll;(*safe*) + (* RPC library start *) "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*) "svctcp_create", readsAll;(*safe*) "clntudp_bufcreate", writesAll;(*unsafe*) @@ -1282,12 +1285,11 @@ let invalidate_actions = [ "svcudp_create", readsAll;(*safe*) "svc_register", writesAll;(*unsafe*) "svc_run", writesAll;(*unsafe*) + (* RPC library end *) "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) "__error", readsAll; (*safe*) "__maskrune", writesAll; (*unsafe*) - "times", writesAll; (*unsafe*) - "timespec_get", writes [1]; "__tolower", readsAll; (*safe*) "signal", writesAll; (*unsafe*) "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*) From 80b4f825d00cca340ebe8fb44784a76ca67c276e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 8 Dec 2023 20:27:07 +0100 Subject: [PATCH 4/5] Port 3 more specs --- src/util/library/libraryFunctions.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index bb2b89c364..ee8d58d886 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -162,6 +162,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("remove", unknown [drop "pathname" [r]]); ("raise", unknown [drop "sig" []]); (* safe-ish, we don't handle signal handlers for now *) ("timespec_get", unknown [drop "ts" [w]; drop "base" []]); + ("signal", unknown [drop "signum" []; drop "handler" [s]]); ] (** C POSIX library functions. @@ -428,7 +429,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strerror_r", unknown [drop "errnum" []; drop "buff" [w]; drop "buflen" []]); ("umask", unknown [drop "mask" []]); ("openlog", unknown [drop "ident" [r]; drop "option" []; drop "facility" []]); - ("times", unknown [drop "buf" [w]]) + ("times", unknown [drop "buf" [w]]); + ("mmap", unknown [drop "addr" []; drop "length" []; drop "prot" []; drop "flags" []; drop "fd" []; drop "offset" []]); + ("munmap", unknown [drop "addr" []; drop "length" []]); ] (** Pthread functions. *) @@ -1291,7 +1294,6 @@ let invalidate_actions = [ "__error", readsAll; (*safe*) "__maskrune", writesAll; (*unsafe*) "__tolower", readsAll; (*safe*) - "signal", writesAll; (*unsafe*) "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*) "BZ2_bzBuffToBuffDecompress", writes [3;4]; (*keep [3;4]*) "uncompress", writes [3;4]; (*keep [3;4]*) @@ -1303,8 +1305,6 @@ let invalidate_actions = [ "BF_set_key", writes [3]; (*keep [3]*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) - "munmap", readsAll;(*safe*) - "mmap", readsAll;(*safe*) "__builtin_va_arg_pack_len", readsAll; "__open_too_many_args", readsAll; "usb_submit_urb", readsAll; (* first argument is written to but according to specification must not be read from anymore *) From ea83c30f1db59c6f0cd7922a25e225ef1e4c4475 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 13 Dec 2023 16:11:38 +0100 Subject: [PATCH 5/5] Be more conservative for `ioctl` --- src/util/library/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index ee8d58d886..d260ebb070 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -750,7 +750,7 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__kmalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Malloc size); ("kzalloc", special [__ "size" []; drop "flags" []] @@ fun size -> Calloc {count = Cil.one; size}); ("usb_alloc_urb", special [__ "iso_packets" []; drop "mem_flags" []] @@ fun iso_packets -> Malloc MyCFG.unknown_exp); - ("ioctl", unknown (drop "fd" [] :: drop "request" [] :: VarArgs (drop' [r]))); + ("ioctl", unknown (drop "fd" [] :: drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); ] (** Goblint functions. *)