From 5739ee1322f0c6912283303f834c159afceed1a0 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 7 May 2024 13:50:27 +0300 Subject: [PATCH 01/11] Convert all remaining libfuns to new format --- src/util/library/libraryFunctions.ml | 163 +++++++++++++++------------ 1 file changed, 94 insertions(+), 69 deletions(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 53bf804b1d..edf647c006 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -63,6 +63,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("localeconv", unknown ~attrs:[ThreadUnsafe] []); ("localtime", unknown ~attrs:[ThreadUnsafe] [drop "time" [r]]); ("strlen", special [__ "s" [r]] @@ fun s -> Strlen s); + ("_strlen", special [__ "s" [r]] @@ fun s -> Strlen s); ("__builtin_strlen", special [__ "s" [r]] @@ fun s -> Strlen s); ("strstr", special [__ "haystack" [r]; __ "needle" [r]] @@ fun haystack needle -> Strstr { haystack; needle; }); ("strcmp", special [__ "s1" [r]; __ "s2" [r]] @@ fun s1 s2 -> Strcmp { s1; s2; n = None; }); @@ -108,7 +109,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strtoul", unknown [drop "nptr" [r]; drop "endptr" [w]; drop "base" []]); ("strtoull", unknown [drop "nptr" [r]; drop "endptr" [w]; drop "base" []]); ("tolower", unknown [drop "ch" []]); + ("__tolower", unknown [drop "ch" []]); ("toupper", unknown [drop "ch" []]); + ("__toupper", unknown [drop "ch" []]); ("time", unknown [drop "arg" [w]]); ("tmpnam", unknown ~attrs:[ThreadUnsafe] [drop "filename" [w]]); ("vprintf", unknown [drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) @@ -117,6 +120,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("asprintf", unknown (drop "strp" [w] :: drop "format" [r] :: VarArgs (drop' [r_deep]))); (* TODO: glibc section? *) ("vasprintf", unknown [drop "strp" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("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? *) + ("__builtin_vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); + ("__builtin___vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: does this actually exist?! *) ("mktime", unknown [drop "tm" [r;w]]); ("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]); ("clearerr", unknown [drop "stream" [w]]); (* TODO: why only w? *) @@ -163,6 +168,13 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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]]); + ("va_arg", unknown [drop "ap" [r_deep]; drop "T" []]); + ("__builtin_va_arg", unknown [drop "ap" [r_deep]; drop "T" []]); + ("va_start", unknown [drop "ap" [r_deep]; drop "parmN" []]); + ("__builtin_va_start", unknown [drop "ap" [r_deep]; drop "parmN" []]); + ("va_end", unknown [drop "ap" [r_deep]]); + ("__builtin_va_end", unknown [drop "ap" [r_deep]]); + ("__builtin_va_arg_pack_len", unknown []); ] [@@coverage off] @@ -312,6 +324,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("send", unknown [drop "sockfd" []; drop "buf" [r]; drop "len" []; drop "flags" []]); ("sendto", unknown [drop "sockfd" []; drop "buf" [r]; drop "len" []; drop "flags" []; drop "dest_addr" [r_deep]; drop "addrlen" []]); ("strdup", unknown [drop "s" [r]]); + ("__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]))); @@ -433,6 +446,11 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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" []]); + ("getline", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r]; drop "stream" [r_deep; w_deep]]); + ("getwline", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r]; drop "stream" [r_deep; w_deep]]); + ("getdelim", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r]; drop "delimiter" [];drop "stream" [r_deep; w_deep]]); + ("__getdelim", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r]; drop "delimiter" [];drop "stream" [r_deep; w_deep]]); + ("getwdelim", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r]; drop "delimiter" [];drop "stream" [r_deep; w_deep]]); ] [@@coverage off] @@ -540,6 +558,13 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__assert", special [drop "assertion" [r]; drop "file" [r]; drop "line" []] @@ Abort); (* header says: The following is not at all used here but needed for standard compliance. *) ("__builtin_return_address", unknown [drop "level" []]); ("__builtin___sprintf_chk", unknown (drop "s" [w] :: drop "flag" [] :: drop "os" [] :: drop "fmt" [r] :: VarArgs (drop' [r]))); + ("__builtin___snprintf_chk", unknown [drop "s" [w]; drop "maxlen" []; drop "flag" []; drop "os" []]); + ("__builtin___vsprintf_chk", unknown [drop "s" [w]; drop "flag" []; drop "os" []; drop "fmt" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) + ("__builtin___vsnprintf_chk", unknown [drop "s" [w]; drop "maxlen" []; drop "flag" []; drop "os" []; drop "fmt" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) + ("__builtin___printf_chk", unknown (drop "flag" [] :: drop "format" [r] :: VarArgs (drop' [r]))); + ("__builtin___vprintf_chk", unknown [drop "flag" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) + ("__builtin___fprintf_chk", unknown (drop "stream" [r_deep; w_deep] :: drop "flag" [] :: drop "format" [r] :: VarArgs (drop' [r]))); + ("__builtin___vfprintf_chk", unknown [drop "stream" [r_deep; w_deep]; drop "flag" []; drop "format" [r]; drop "ap" [r_deep]]); ("__builtin_add_overflow", unknown [drop "a" []; drop "b" []; drop "c" [w]]); ("__builtin_sadd_overflow", unknown [drop "a" []; drop "b" []; drop "c" [w]]); ("__builtin_saddl_overflow", unknown [drop "a" []; drop "b" []; drop "c" [w]]); @@ -624,7 +649,9 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__readlink_chk", unknown [drop "path" [r]; drop "buf" [w]; drop "len" []; drop "buflen" []]); ("__readlink_alias", unknown [drop "path" [r]; drop "buf" [w]; drop "len" []]); ("__overflow", unknown [drop "f" [r]; drop "ch" []]); + ("__ctype_b_loc", unknown []); ("__ctype_get_mb_cur_max", unknown []); + ("__maskrune", unknown [drop "c" [w]; drop "f" []]); ("__xmknod", unknown [drop "ver" []; drop "path" [r]; drop "mode" []; drop "dev" [r; w]]); ("yp_get_default_domain", unknown [drop "outdomain" [w]]); ("__nss_configure_lookup", unknown [drop "db" [r]; drop "service_line" [r]]); @@ -657,6 +684,19 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getdtablesize", unknown []); ("daemon", unknown [drop "nochdir" []; drop "noclose" []]); ("putw", unknown [drop "w" []; drop "stream" [r_deep; w_deep]]); + (* RPC library start *) + ("clntudp_create", unknown [drop "addr" [r]; drop "prognum" []; drop "versnum" []; drop "wait" [r]; drop "sockp" [w]]); + ("clntudp_bufcreate", unknown [drop "addr" [r]; drop "prognum" []; drop "versnum" []; drop "wait" [r]; drop "sockp" [w]; drop "sendsize" []; drop "recosize" []]); + ("svctcp_create", unknown [drop "sock" []; drop "send_buf_size" []; drop "recv_buf_size" []]); + ("authunix_create_default", unknown []); + ("clnt_broadcast", unknown [drop "prognum" []; drop "versnum" []; drop "procnum" []; drop "inproc" [r]; drop "in" [w]; drop "outproc" [r]; drop "out" [w]; drop "eachresult" []]); + ("clnt_sperrno", unknown [drop "stat" []]); + ("pmap_unset", unknown [drop "prognum" []; drop "versnum" []]); + ("svcudp_create", unknown [drop "sock" []]); + ("svc_register", unknown [drop "xprt" [r;w]; drop "prognum" []; drop "versnum" []; drop "dispatch" [r;w]; drop "protocol" []]); + ("svc_run", unknown []); + (* RPC library end *) + ("scandir", unknown [drop "dirp" [r]; drop "namelist" [w_deep]; drop "filter" [r]; drop "compar" [r]]); ] [@@coverage off] @@ -669,7 +709,14 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("epoll_create", unknown [drop "size" []]); ("epoll_ctl", unknown [drop "epfd" []; drop "op" []; drop "fd" []; drop "event" [w]]); ("epoll_wait", unknown [drop "epfd" []; drop "events" [w]; drop "maxevents" []; drop "timeout" []]); + ("__error", unknown []); + ("__errno", unknown []); + ("__errno_location", unknown []); + ("__h_errno_location", unknown []); + ("printk", unknown (drop "fmt" [r] :: VarArgs (drop' [r]))); + ("__printf_chk", unknown [drop "flag" []; drop "format" [r]]); ("__fprintf_chk", unknown (drop "stream" [r_deep; w_deep] :: drop "flag" [] :: drop "format" [r] :: VarArgs (drop' [r]))); + ("__vfprintf_chk", unknown [drop "stream" [r_deep; w_deep]; drop "flag" []; drop "format" [r]; drop "ap" [r_deep]]); ("sysinfo", unknown [drop "info" [w_deep]]); ("__xpg_basename", unknown [drop "path" [r]]); ("ptrace", unknown (drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); (* man page has 4 arguments, but header has varargs and real-world programs may call with <4 *) @@ -691,6 +738,11 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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 []); + ("__xstat", unknown [drop "ver" []; drop "path" [r]; drop "stat_buf" [w]]); + ("__lxstat", unknown [drop "ver" []; drop "path" [r]; drop "stat_buf" [w]]); + ("__fxstat", unknown [drop "ver" []; drop "fildes" []; drop "stat_buf" [w]]); + ("kmem_cache_create", unknown [drop "name" [r]; drop "size" []; drop "align" []; drop "flags" []; drop "ctor" [r]]); + ("usb_submit_urb", unknown [drop "urb" [r]; drop "mem_flags" []]); (* first argument is written to but according to specification must not be read from anymore *) ] [@@coverage off] @@ -706,11 +758,13 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("up_read", special [__ "sem" []] @@ fun sem -> Unlock sem); ("up_write", special [__ "sem" []] @@ fun sem -> Unlock sem); ("mutex_init", unknown [drop "mutex" []]); + ("__mutex_init", unknown [drop "lock" [r]; drop "name" [r]; drop "key" [r]]); ("mutex_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); ("mutex_trylock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = true; write = true; return_on_success = true }); ("mutex_lock_interruptible", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); ("mutex_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); ("spin_lock_init", unknown [drop "lock" []]); + ("__spin_lock_init", unknown [drop "lock" []]); ("spin_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); ("_spin_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); ("_spin_lock_bh", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); @@ -770,6 +824,7 @@ let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__goblint_split_begin", unknown [drop "exp" []]); ("__goblint_split_end", unknown [drop "exp" []]); ("__goblint_bounded", special [__ "exp"[]] @@ fun exp -> Bounded { exp }); + ("__goblint_assume_join", unknown [drop "tid" []]); ] [@@coverage off] @@ -1045,6 +1100,11 @@ let klever_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("rtnl_lock", special [] @@ Lock { lock = rtnl_lock; try_ = false; write = true; return_on_success = true }); ("rtnl_unlock", special [] @@ Unlock rtnl_lock); ("__rtnl_unlock", special [] @@ Unlock rtnl_lock); + (* ldv-benchmarks *) + (* ddverify *) + ("sema_init", unknown [drop "sem" [r]; drop "val" []]); + ("idr_pre_get", unknown [drop "idp" [r]; drop "gfp_mask" []]); + ("dev_driver_string", unknown [drop "dev" [r]]); ] [@@coverage off] @@ -1127,6 +1187,38 @@ let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ] [@@coverage off] +let legacy_libs_misc_list: (string * LibraryDesc.t) list = LibraryDsl.[ + (* TODO: was "zil_replay", writes [1;2;3;5]; but couldn't find anything with 5/6 arguments, also not in bench *) + ("zil_replay", unknown [drop "os" [w]; drop "arg" [w]; drop "replay_func" [r]]); + ("_IO_getc", unknown [drop "f" [r_deep; w_deep]]); + ("__open_alias", unknown (drop "path" [r] :: drop "oflag" [] :: VarArgs (drop' [r]))); + ("__open_2", unknown [drop "file" [r]; drop "oflag" []]); + ("__open_too_many_args", unknown []); + (* bzlib *) + ("BZ2_bzBuffToBuffCompress", unknown [drop "dest" []; drop "destLen" []; drop "source" [w]; drop "sourceLen" []; drop "blockSize100k" []; drop "verbosity" []; drop "workFactor" []]); + ("BZ2_bzBuffToBuffDecompress", unknown [drop "dest" []; drop "destLen" []; drop "source" [w]; drop "sourceLen" []; drop "small" []; drop "verbosity" []]); + (* zlib (Zebedee) *) + ("uncompress", unknown [drop "dest" [w]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []]); + ("compress2", unknown [drop "dest" [r]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []; drop "level" []]); + (* opensssl blowfish *) + ("BF_cfb64_encrypt", unknown [drop "in" [r]; drop "out" [w]; drop "length" []; drop "schedule" [r]; drop "ivec" [w]; drop "num" [w]; drop "enc" [r]]); + ("BF_set_key", unknown [drop "key" [w]; drop "len" []; drop "data" [r]]); + (* libintl *) + ("textdomain", unknown [drop "domainname" [r]]); + ("bindtextdomain", unknown [drop "domainname" [r]; drop "dirname" [r]]); + ("dcgettext", unknown [drop "domainname" [r]; drop "msgid" [r]; drop "category" []]); + (* TODO: the __extinline suffix was added by CIL in the old times in some cases, but is now switched off for like 10 years *) + ("strtoul__extinline", unknown [drop "nptr" [r]; drop "endptr" [w]; drop "base" []]); + ("atoi__extinline", unknown [drop "nptr" [r]]); + ("stat__extinline", unknown [drop "pathname" [r]; drop "statbuf" [w]]); + ("lstat__extinline", unknown [drop "pathname" [r]; drop "statbuf" [w]]); + ("fstat__extinline", unknown [drop "fd" []; drop "buf" [w]]); + (* only in knot *) + ("PL_NewHashTable", unknown [drop "n" []; drop "keyHash" [r]; drop "keyCompare" [r]; drop "valueCompare" [r]; drop "allocOps" [r]; drop "allocPriv" [r]]); (* TODO: should have call instead of read *) + ("assert_failed", unknown [drop "file" [r]; drop "line" []; drop "func" [r]; drop "exp" [r]]); + ] +[@@coverage off] + let libraries = Hashtbl.of_list [ ("c", c_descs_list @ math_descs_list); ("posix", posix_descs_list); @@ -1143,6 +1235,7 @@ let libraries = Hashtbl.of_list [ ("pcre", pcre_descs_list); ("zlib", zlib_descs_list); ("liblzma", liblzma_descs_list); + ("legacy", legacy_libs_misc_list); ] let libraries = @@ -1282,75 +1375,7 @@ open Invalidate (* Data races: which arguments are read/written? * We assume that no known functions that are reachable are executed/spawned. For that we use ThreadCreate above. *) (* WTF: why are argument numbers 1-indexed (in partition)? *) -let invalidate_actions = [ - "__printf_chk", readsAll;(*safe*) - "printk", readsAll;(*safe*) - "__mutex_init", readsAll;(*safe*) - "__builtin___snprintf_chk", writes [1];(*keep [1]*) - "__vfprintf_chk", writes [1];(*keep [1]*) - "__builtin_va_arg", readsAll;(*safe*) - "__builtin_va_end", readsAll;(*safe*) - "__builtin_va_start", readsAll;(*safe*) - "__ctype_b_loc", readsAll;(*safe*) - "__errno", readsAll;(*safe*) - "__errno_location", readsAll;(*safe*) - "__strdup", readsAll;(*safe*) - "strtoul__extinline", readsAll;(*safe*) - "atoi__extinline", readsAll;(*safe*) - "_IO_getc", 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*) - "fstat__extinline", writesAll;(*unsafe*) - "scandir", writes [1;3;4];(*keep [1;3;4]*) - "bindtextdomain", readsAll;(*safe*) - "textdomain", readsAll;(*safe*) - "dcgettext", readsAll;(*safe*) - "__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*) - "authunix_create_default", readsAll;(*safe*) - "clnt_broadcast", writesAll;(*unsafe*) - "clnt_sperrno", readsAll;(*safe*) - "pmap_unset", writesAll;(*unsafe*) - "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*) - "__tolower", readsAll; (*safe*) - "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]*) - "__xstat", writes [3]; (*keep [1]*) - "__lxstat", writes [3]; (*keep [1]*) - "BZ2_bzBuffToBuffCompress", writes [3;4]; (*keep [3;4]*) - "compress2", writes [3]; (*keep [3]*) - "__toupper", readsAll; (*safe*) - "BF_set_key", writes [3]; (*keep [3]*) - "PL_NewHashTable", readsAll; (*safe*) - "assert_failed", 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 *) - "dev_driver_string", readsAll; - "__spin_lock_init", writes [1]; - "kmem_cache_create", readsAll; - "idr_pre_get", readsAll; - "zil_replay", writes [1;2;3;5]; - (* ddverify *) - "sema_init", readsAll; - "__goblint_assume_join", readsAll; -] +let invalidate_actions = [] let invalidate_actions = let tbl = Hashtbl.create 113 in From 05da8b83ee33422f1deb7ed22466fb8b0e1a4adc Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Wed, 8 May 2024 12:08:54 +0300 Subject: [PATCH 02/11] Fix `va_arg` and `va_start` libfun defs according to CIL special cases --- src/util/library/libraryFunctions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 14a04d9518..4db6c32abb 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -169,9 +169,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("timespec_get", unknown [drop "ts" [w]; drop "base" []]); ("signal", unknown [drop "signum" []; drop "handler" [s]]); ("va_arg", unknown [drop "ap" [r_deep]; drop "T" []]); - ("__builtin_va_arg", unknown [drop "ap" [r_deep]; drop "T" []]); + ("__builtin_va_arg", unknown [drop "ap" [r_deep]; drop "T" []; drop "lhs" []]); (* cil: "__builtin_va_arg is special: in CIL, the left hand side is stored as the last argument" *) ("va_start", unknown [drop "ap" [r_deep]; drop "parmN" []]); - ("__builtin_va_start", unknown [drop "ap" [r_deep]; drop "parmN" []]); + ("__builtin_va_start", unknown [drop "ap" [r_deep]]); (* cil: "When we parse builtin_{va,stdarg}_start, we drop the second argument" *) ("va_end", unknown [drop "ap" [r_deep]]); ("__builtin_va_end", unknown [drop "ap" [r_deep]]); ("__builtin_va_arg_pack_len", unknown []); From f4504b6ebd7823619cbccedadd4cf95f043f5e04 Mon Sep 17 00:00:00 2001 From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com> Date: Wed, 15 May 2024 12:03:55 +0300 Subject: [PATCH 03/11] `w` for `lhs` in `__builtin_va_arg` Co-authored-by: Simmo Saan --- 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 4db6c32abb..772cc07707 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -169,7 +169,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("timespec_get", unknown [drop "ts" [w]; drop "base" []]); ("signal", unknown [drop "signum" []; drop "handler" [s]]); ("va_arg", unknown [drop "ap" [r_deep]; drop "T" []]); - ("__builtin_va_arg", unknown [drop "ap" [r_deep]; drop "T" []; drop "lhs" []]); (* cil: "__builtin_va_arg is special: in CIL, the left hand side is stored as the last argument" *) + ("__builtin_va_arg", unknown [drop "ap" [r_deep]; drop "T" []; drop "lhs" [w]]); (* cil: "__builtin_va_arg is special: in CIL, the left hand side is stored as the last argument" *) ("va_start", unknown [drop "ap" [r_deep]; drop "parmN" []]); ("__builtin_va_start", unknown [drop "ap" [r_deep]]); (* cil: "When we parse builtin_{va,stdarg}_start, we drop the second argument" *) ("va_end", unknown [drop "ap" [r_deep]]); From ab35510e231d2bbf214b522b048d603ca1976a83 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Wed, 15 May 2024 12:07:16 +0300 Subject: [PATCH 04/11] Move `__builtin_` prefixed functions from c standard lib to GCC builtins --- 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 772cc07707..82da0fa69f 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -120,8 +120,6 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("asprintf", unknown (drop "strp" [w] :: drop "format" [r] :: VarArgs (drop' [r_deep]))); (* TODO: glibc section? *) ("vasprintf", unknown [drop "strp" [w]; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("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? *) - ("__builtin_vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); - ("__builtin___vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: does this actually exist?! *) ("mktime", unknown [drop "tm" [r;w]]); ("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]); ("clearerr", unknown [drop "stream" [w]]); (* TODO: why only w? *) @@ -169,12 +167,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("timespec_get", unknown [drop "ts" [w]; drop "base" []]); ("signal", unknown [drop "signum" []; drop "handler" [s]]); ("va_arg", unknown [drop "ap" [r_deep]; drop "T" []]); - ("__builtin_va_arg", unknown [drop "ap" [r_deep]; drop "T" []; drop "lhs" [w]]); (* cil: "__builtin_va_arg is special: in CIL, the left hand side is stored as the last argument" *) ("va_start", unknown [drop "ap" [r_deep]; drop "parmN" []]); - ("__builtin_va_start", unknown [drop "ap" [r_deep]]); (* cil: "When we parse builtin_{va,stdarg}_start, we drop the second argument" *) ("va_end", unknown [drop "ap" [r_deep]]); - ("__builtin_va_end", unknown [drop "ap" [r_deep]]); - ("__builtin_va_arg_pack_len", unknown []); ] [@@coverage off] @@ -619,6 +613,12 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]); ("alloca", special [__ "size" []] @@ fun size -> Alloca size); ("__builtin_alloca", special [__ "size" []] @@ fun size -> Alloca size); + ("__builtin_vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); + ("__builtin___vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: does this actually exist?! *) + ("__builtin_va_arg", unknown [drop "ap" [r_deep]; drop "T" []; drop "lhs" [w]]); (* cil: "__builtin_va_arg is special: in CIL, the left hand side is stored as the last argument" *) + ("__builtin_va_start", unknown [drop "ap" [r_deep]]); (* cil: "When we parse builtin_{va,stdarg}_start, we drop the second argument" *) + ("__builtin_va_end", unknown [drop "ap" [r_deep]]); + ("__builtin_va_arg_pack_len", unknown []); ] [@@coverage off] From 6c93ce61e979c57ac55633412204b95136e2588d Mon Sep 17 00:00:00 2001 From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com> Date: Wed, 15 May 2024 12:12:59 +0300 Subject: [PATCH 05/11] :: for VarArgs instead ; Co-authored-by: Simmo Saan --- 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 82da0fa69f..a83b917501 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -552,7 +552,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__assert", special [drop "assertion" [r]; drop "file" [r]; drop "line" []] @@ Abort); (* header says: The following is not at all used here but needed for standard compliance. *) ("__builtin_return_address", unknown [drop "level" []]); ("__builtin___sprintf_chk", unknown (drop "s" [w] :: drop "flag" [] :: drop "os" [] :: drop "fmt" [r] :: VarArgs (drop' [r]))); - ("__builtin___snprintf_chk", unknown [drop "s" [w]; drop "maxlen" []; drop "flag" []; drop "os" []]); + ("__builtin___snprintf_chk", unknown (drop "s" [w] :: drop "maxlen" [] :: drop "flag" [] :: drop "os" [] :: drop "fmt" [r] :: VarArgs (drop' [r]))); ("__builtin___vsprintf_chk", unknown [drop "s" [w]; drop "flag" []; drop "os" []; drop "fmt" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("__builtin___vsnprintf_chk", unknown [drop "s" [w]; drop "maxlen" []; drop "flag" []; drop "os" []; drop "fmt" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("__builtin___printf_chk", unknown (drop "flag" [] :: drop "format" [r] :: VarArgs (drop' [r]))); From ef726e985cc47ae9f92022a5ad19c15bbf25da3c Mon Sep 17 00:00:00 2001 From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com> Date: Wed, 15 May 2024 12:13:45 +0300 Subject: [PATCH 06/11] Add `w` for `n` in `getline` and `getdelim` Co-authored-by: Simmo Saan --- 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 a83b917501..e941ddf165 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -440,11 +440,11 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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" []]); - ("getline", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r]; drop "stream" [r_deep; w_deep]]); - ("getwline", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r]; drop "stream" [r_deep; w_deep]]); - ("getdelim", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r]; drop "delimiter" [];drop "stream" [r_deep; w_deep]]); - ("__getdelim", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r]; drop "delimiter" [];drop "stream" [r_deep; w_deep]]); - ("getwdelim", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r]; drop "delimiter" [];drop "stream" [r_deep; w_deep]]); + ("getline", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r; w]; drop "stream" [r_deep; w_deep]]); + ("getwline", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r; w]; drop "stream" [r_deep; w_deep]]); + ("getdelim", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r; w]; drop "delimiter" []; drop "stream" [r_deep; w_deep]]); + ("__getdelim", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r; w]; drop "delimiter" []; drop "stream" [r_deep; w_deep]]); + ("getwdelim", unknown [drop "lineptr" [r_deep; w_deep]; drop "n" [r; w]; drop "delimiter" []; drop "stream" [r_deep; w_deep]]); ] [@@coverage off] From 32791111c8569f25b0b543ce6be3254f8163c14e Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Wed, 15 May 2024 12:59:25 +0300 Subject: [PATCH 07/11] Apply suggested changes Co-authored-by: Simmo Saan --- src/config/options.schema.json | 6 ++++-- src/util/library/libraryFunctions.ml | 27 ++++++++++++--------------- 2 files changed, 16 insertions(+), 17 deletions(-) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 99c887ca53..37e62ebdda 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1344,7 +1344,8 @@ "zstd", "pcre", "zlib", - "liblzma" + "liblzma", + "legacy" ] }, "default": [ @@ -1355,7 +1356,8 @@ "glibc", "linux-userspace", "goblint", - "ncurses" + "ncurses", + "legacy" ] } }, diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index e941ddf165..cdde23fece 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -432,6 +432,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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]]); + ("scandir", unknown [drop "dirp" [r]; drop "namelist" [w]; drop "filter" [r]; drop "compar" [r]]); ("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" []]); @@ -649,7 +650,6 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__readlink_chk", unknown [drop "path" [r]; drop "buf" [w]; drop "len" []; drop "buflen" []]); ("__readlink_alias", unknown [drop "path" [r]; drop "buf" [w]; drop "len" []]); ("__overflow", unknown [drop "f" [r]; drop "ch" []]); - ("__ctype_b_loc", unknown []); ("__ctype_get_mb_cur_max", unknown []); ("__maskrune", unknown [drop "c" [w]; drop "f" []]); ("__xmknod", unknown [drop "ver" []; drop "path" [r]; drop "mode" []; drop "dev" [r; w]]); @@ -693,10 +693,9 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("clnt_sperrno", unknown [drop "stat" []]); ("pmap_unset", unknown [drop "prognum" []; drop "versnum" []]); ("svcudp_create", unknown [drop "sock" []]); - ("svc_register", unknown [drop "xprt" [r;w]; drop "prognum" []; drop "versnum" []; drop "dispatch" [r;w]; drop "protocol" []]); + ("svc_register", unknown [drop "xprt" [r_deep; w_deep]; drop "prognum" []; drop "versnum" []; drop "dispatch" [r; w]; drop "protocol" []]); ("svc_run", unknown []); (* RPC library end *) - ("scandir", unknown [drop "dirp" [r]; drop "namelist" [w_deep]; drop "filter" [r]; drop "compar" [r]]); ] [@@coverage off] @@ -713,7 +712,6 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__errno", unknown []); ("__errno_location", unknown []); ("__h_errno_location", unknown []); - ("printk", unknown (drop "fmt" [r] :: VarArgs (drop' [r]))); ("__printf_chk", unknown [drop "flag" []; drop "format" [r]]); ("__fprintf_chk", unknown (drop "stream" [r_deep; w_deep] :: drop "flag" [] :: drop "format" [r] :: VarArgs (drop' [r]))); ("__vfprintf_chk", unknown [drop "stream" [r_deep; w_deep]; drop "flag" []; drop "format" [r]; drop "ap" [r_deep]]); @@ -741,8 +739,8 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__xstat", unknown [drop "ver" []; drop "path" [r]; drop "stat_buf" [w]]); ("__lxstat", unknown [drop "ver" []; drop "path" [r]; drop "stat_buf" [w]]); ("__fxstat", unknown [drop "ver" []; drop "fildes" []; drop "stat_buf" [w]]); - ("kmem_cache_create", unknown [drop "name" [r]; drop "size" []; drop "align" []; drop "flags" []; drop "ctor" [r]]); - ("usb_submit_urb", unknown [drop "urb" [r]; drop "mem_flags" []]); (* first argument is written to but according to specification must not be read from anymore *) + ("__ctype_b_loc", unknown []); + ("_IO_getc", unknown [drop "f" [r_deep; w_deep]]); ] [@@coverage off] @@ -758,7 +756,7 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("up_read", special [__ "sem" []] @@ fun sem -> Unlock sem); ("up_write", special [__ "sem" []] @@ fun sem -> Unlock sem); ("mutex_init", unknown [drop "mutex" []]); - ("__mutex_init", unknown [drop "lock" [r]; drop "name" [r]; drop "key" [r]]); + ("__mutex_init", unknown [drop "lock" []; drop "name" [r]; drop "key" [r]]); ("mutex_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); ("mutex_trylock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = true; write = true; return_on_success = true }); ("mutex_lock_interruptible", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); @@ -810,7 +808,12 @@ 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); + ("usb_submit_urb", unknown [drop "urb" [r_deep; w_deep]; drop "mem_flags" []]); (* old comment: first argument is written to but according to specification must not be read from anymore *) + ("dev_driver_string", unknown [drop "dev" [r_deep]]); ("ioctl", unknown (drop "fd" [] :: drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); + ("idr_pre_get", unknown [drop "idp" [r_deep]; drop "gfp_mask" []]); + ("printk", unknown (drop "fmt" [r] :: VarArgs (drop' [r]))); + ("kmem_cache_create", unknown [drop "name" [r]; drop "size" []; drop "align" []; drop "flags" []; drop "ctor" [r]]); ] [@@coverage off] @@ -1100,11 +1103,8 @@ let klever_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("rtnl_lock", special [] @@ Lock { lock = rtnl_lock; try_ = false; write = true; return_on_success = true }); ("rtnl_unlock", special [] @@ Unlock rtnl_lock); ("__rtnl_unlock", special [] @@ Unlock rtnl_lock); - (* ldv-benchmarks *) (* ddverify *) - ("sema_init", unknown [drop "sem" [r]; drop "val" []]); - ("idr_pre_get", unknown [drop "idp" [r]; drop "gfp_mask" []]); - ("dev_driver_string", unknown [drop "dev" [r]]); + ("sema_init", unknown [drop "sem" []; drop "val" []]); ] [@@coverage off] @@ -1188,9 +1188,6 @@ let liblzma_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ [@@coverage off] let legacy_libs_misc_list: (string * LibraryDesc.t) list = LibraryDsl.[ - (* TODO: was "zil_replay", writes [1;2;3;5]; but couldn't find anything with 5/6 arguments, also not in bench *) - ("zil_replay", unknown [drop "os" [w]; drop "arg" [w]; drop "replay_func" [r]]); - ("_IO_getc", unknown [drop "f" [r_deep; w_deep]]); ("__open_alias", unknown (drop "path" [r] :: drop "oflag" [] :: VarArgs (drop' [r]))); ("__open_2", unknown [drop "file" [r]; drop "oflag" []]); ("__open_too_many_args", unknown []); @@ -1201,7 +1198,7 @@ let legacy_libs_misc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("uncompress", unknown [drop "dest" [w]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []]); ("compress2", unknown [drop "dest" [r]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []; drop "level" []]); (* opensssl blowfish *) - ("BF_cfb64_encrypt", unknown [drop "in" [r]; drop "out" [w]; drop "length" []; drop "schedule" [r]; drop "ivec" [w]; drop "num" [w]; drop "enc" [r]]); + ("BF_cfb64_encrypt", unknown [drop "in" [r]; drop "out" [w]; drop "length" []; drop "schedule" [r]; drop "ivec" [r; w]; drop "num" [r; w]; drop "enc" []]); ("BF_set_key", unknown [drop "key" [w]; drop "len" []; drop "data" [r]]); (* libintl *) ("textdomain", unknown [drop "domainname" [r]]); From 96f2cf2a8bd45ba4dcf993351ad1f931eda3fc0c Mon Sep 17 00:00:00 2001 From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com> Date: Wed, 15 May 2024 13:09:08 +0300 Subject: [PATCH 08/11] Apply suggestions from code review Co-authored-by: Simmo Saan --- src/util/library/libraryFunctions.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index cdde23fece..26c3b0a032 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -1192,11 +1192,11 @@ let legacy_libs_misc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__open_2", unknown [drop "file" [r]; drop "oflag" []]); ("__open_too_many_args", unknown []); (* bzlib *) - ("BZ2_bzBuffToBuffCompress", unknown [drop "dest" []; drop "destLen" []; drop "source" [w]; drop "sourceLen" []; drop "blockSize100k" []; drop "verbosity" []; drop "workFactor" []]); - ("BZ2_bzBuffToBuffDecompress", unknown [drop "dest" []; drop "destLen" []; drop "source" [w]; drop "sourceLen" []; drop "small" []; drop "verbosity" []]); + ("BZ2_bzBuffToBuffCompress", unknown [drop "dest" [w]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []; drop "blockSize100k" []; drop "verbosity" []; drop "workFactor" []]); + ("BZ2_bzBuffToBuffDecompress", unknown [drop "dest" [w]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []; drop "small" []; drop "verbosity" []]); (* zlib (Zebedee) *) ("uncompress", unknown [drop "dest" [w]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []]); - ("compress2", unknown [drop "dest" [r]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []; drop "level" []]); + ("compress2", unknown [drop "dest" [w]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []; drop "level" []]); (* opensssl blowfish *) ("BF_cfb64_encrypt", unknown [drop "in" [r]; drop "out" [w]; drop "length" []; drop "schedule" [r]; drop "ivec" [r; w]; drop "num" [r; w]; drop "enc" []]); ("BF_set_key", unknown [drop "key" [w]; drop "len" []; drop "data" [r]]); From bedfb35f020372b1fb23d5adbf374037b0e3f340 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 16 May 2024 12:38:43 +0300 Subject: [PATCH 09/11] Make arguments of function pointer type spawn --- src/util/library/libraryDsl.ml | 2 ++ src/util/library/libraryDsl.mli | 6 ++++++ src/util/library/libraryFunctions.ml | 19 +++++++++---------- 3 files changed, 17 insertions(+), 10 deletions(-) diff --git a/src/util/library/libraryDsl.ml b/src/util/library/libraryDsl.ml index 49aac8ce9b..64684fb1ce 100644 --- a/src/util/library/libraryDsl.ml +++ b/src/util/library/libraryDsl.ml @@ -102,3 +102,5 @@ let f = Access.{ kind = Free; deep = false; } let f_deep = Access.{ kind = Free; deep = true; } let s = Access.{ kind = Spawn; deep = false; } let s_deep = Access.{ kind = Spawn; deep = true; } +let c = Access.{ kind = Spawn; deep = false; } (* TODO: Sound, but very imprecise hack for calls to function pointers given as arguments. *) +let c_deep = Access.{ kind = Spawn; deep = true; } diff --git a/src/util/library/libraryDsl.mli b/src/util/library/libraryDsl.mli index fd0bc45c26..052f92c593 100644 --- a/src/util/library/libraryDsl.mli +++ b/src/util/library/libraryDsl.mli @@ -71,3 +71,9 @@ val s: LibraryDesc.Access.t (** Deep {!AccessKind.Spawn} access. Rarely needed. *) val s_deep: LibraryDesc.Access.t + +(** Shallow {!AccessKind.Spawn} access, substituting function pointer calls for now (TODO). *) +val c: LibraryDesc.Access.t + +(** Deep {!AccessKind.Spawn} access, substituting deep function pointer calls for now (TODO) *) +val c_deep: LibraryDesc.Access.t \ No newline at end of file diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index cdde23fece..71d34ead88 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -166,7 +166,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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]]); - ("va_arg", unknown [drop "ap" [r_deep]; drop "T" []]); + ("va_arg", unknown [drop "ap" [r]; drop "T" []]); ("va_start", unknown [drop "ap" [r_deep]; drop "parmN" []]); ("va_end", unknown [drop "ap" [r_deep]]); ] @@ -432,7 +432,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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]]); - ("scandir", unknown [drop "dirp" [r]; drop "namelist" [w]; drop "filter" [r]; drop "compar" [r]]); + ("scandir", unknown [drop "dirp" [r]; drop "namelist" [w]; drop "filter" [r; c]; drop "compar" [r; c]]); ("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" []]); @@ -689,12 +689,12 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("clntudp_bufcreate", unknown [drop "addr" [r]; drop "prognum" []; drop "versnum" []; drop "wait" [r]; drop "sockp" [w]; drop "sendsize" []; drop "recosize" []]); ("svctcp_create", unknown [drop "sock" []; drop "send_buf_size" []; drop "recv_buf_size" []]); ("authunix_create_default", unknown []); - ("clnt_broadcast", unknown [drop "prognum" []; drop "versnum" []; drop "procnum" []; drop "inproc" [r]; drop "in" [w]; drop "outproc" [r]; drop "out" [w]; drop "eachresult" []]); + ("clnt_broadcast", unknown [drop "prognum" []; drop "versnum" []; drop "procnum" []; drop "inproc" [r; c]; drop "in" [w]; drop "outproc" [r; c]; drop "out" [w]; drop "eachresult" [c]]); ("clnt_sperrno", unknown [drop "stat" []]); ("pmap_unset", unknown [drop "prognum" []; drop "versnum" []]); ("svcudp_create", unknown [drop "sock" []]); - ("svc_register", unknown [drop "xprt" [r_deep; w_deep]; drop "prognum" []; drop "versnum" []; drop "dispatch" [r; w]; drop "protocol" []]); - ("svc_run", unknown []); + ("svc_register", unknown [drop "xprt" [r_deep; w_deep]; drop "prognum" []; drop "versnum" []; drop "dispatch" [r; w; c]; drop "protocol" []]); + ("svc_run", special [] Abort); (* RPC library end *) ] [@@coverage off] @@ -808,12 +808,12 @@ 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); - ("usb_submit_urb", unknown [drop "urb" [r_deep; w_deep]; drop "mem_flags" []]); (* old comment: first argument is written to but according to specification must not be read from anymore *) + ("usb_submit_urb", unknown [drop "urb" [r_deep; w_deep; c_deep]; drop "mem_flags" []]); (* old comment: first argument is written to but according to specification must not be read from anymore *) ("dev_driver_string", unknown [drop "dev" [r_deep]]); ("ioctl", unknown (drop "fd" [] :: drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); ("idr_pre_get", unknown [drop "idp" [r_deep]; drop "gfp_mask" []]); ("printk", unknown (drop "fmt" [r] :: VarArgs (drop' [r]))); - ("kmem_cache_create", unknown [drop "name" [r]; drop "size" []; drop "align" []; drop "flags" []; drop "ctor" [r]]); + ("kmem_cache_create", unknown [drop "name" [r]; drop "size" []; drop "align" []; drop "flags" []; drop "ctor" [r; c]]); ] [@@coverage off] @@ -1171,6 +1171,8 @@ let zlib_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("gzdopen", unknown [drop "fd" []; drop "mode" [r]]); ("gzread", unknown [drop "file" [r_deep; w_deep]; drop "buf" [w]; drop "len" []]); ("gzclose", unknown [drop "file" [f_deep]]); + ("uncompress", unknown [drop "dest" [w]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []]); + ("compress2", unknown [drop "dest" [r]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []; drop "level" []]); ] [@@coverage off] @@ -1194,9 +1196,6 @@ let legacy_libs_misc_list: (string * LibraryDesc.t) list = LibraryDsl.[ (* bzlib *) ("BZ2_bzBuffToBuffCompress", unknown [drop "dest" []; drop "destLen" []; drop "source" [w]; drop "sourceLen" []; drop "blockSize100k" []; drop "verbosity" []; drop "workFactor" []]); ("BZ2_bzBuffToBuffDecompress", unknown [drop "dest" []; drop "destLen" []; drop "source" [w]; drop "sourceLen" []; drop "small" []; drop "verbosity" []]); - (* zlib (Zebedee) *) - ("uncompress", unknown [drop "dest" [w]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []]); - ("compress2", unknown [drop "dest" [r]; drop "destLen" [r; w]; drop "source" [r]; drop "sourceLen" []; drop "level" []]); (* opensssl blowfish *) ("BF_cfb64_encrypt", unknown [drop "in" [r]; drop "out" [w]; drop "length" []; drop "schedule" [r]; drop "ivec" [r; w]; drop "num" [r; w]; drop "enc" []]); ("BF_set_key", unknown [drop "key" [w]; drop "len" []; drop "data" [r]]); From 91216653bf5661c73d8b1a3e409c659391ad3ea4 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 21 May 2024 12:49:52 +0300 Subject: [PATCH 10/11] Convert svc_run back to unknown and add comment --- 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 0e67dc4c09..caf1dad784 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -694,7 +694,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pmap_unset", unknown [drop "prognum" []; drop "versnum" []]); ("svcudp_create", unknown [drop "sock" []]); ("svc_register", unknown [drop "xprt" [r_deep; w_deep]; drop "prognum" []; drop "versnum" []; drop "dispatch" [r; w; c]; drop "protocol" []]); - ("svc_run", special [] Abort); + ("svc_run", unknown []); (* TODO: make new special kind "NoReturn" for this: the following node will be dead (like Abort), but the program doesn't exit (so it shouldn't be Abort) *) (* RPC library end *) ] [@@coverage off] From 91eca5a639c3bd2654f882a596699e1f1a628dfe Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Tue, 21 May 2024 12:50:36 +0300 Subject: [PATCH 11/11] Apply suggested changes --- 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 caf1dad784..d0ed2fd820 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -651,7 +651,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__readlink_alias", unknown [drop "path" [r]; drop "buf" [w]; drop "len" []]); ("__overflow", unknown [drop "f" [r]; drop "ch" []]); ("__ctype_get_mb_cur_max", unknown []); - ("__maskrune", unknown [drop "c" [w]; drop "f" []]); + ("__maskrune", unknown [drop "c" []; drop "f" []]); ("__xmknod", unknown [drop "ver" []; drop "path" [r]; drop "mode" []; drop "dev" [r; w]]); ("yp_get_default_domain", unknown [drop "outdomain" [w]]); ("__nss_configure_lookup", unknown [drop "db" [r]; drop "service_line" [r]]);