From 587b39f6e9aaf67cfcc572e2a686286c93fa1a70 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 13:44:20 +0200 Subject: [PATCH 01/50] `atoi` and friends --- src/analyses/libraryFunctions.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 034fd6bb97..90d13a00a1 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -127,6 +127,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value }); ("atexit", unknown [drop "function" [s]]); + ("atoi", unknown [drop "nptr" [r]]); + ("atol", unknown [drop "nptr" [r]]); + ("atoll", unknown [drop "nptr" [r]]); ] (** C POSIX library functions. @@ -486,6 +489,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("memmem", unknown [drop "haystack" [r]; drop "haystacklen" []; drop "needle" [r]; drop "needlelen" [r]]); ("getifaddrs", unknown [drop "ifap" [w]]); ("freeifaddrs", unknown [drop "ifa" [f_deep]]); + ("atoq", unknown [drop "nptr" [r]]); ] let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -1019,7 +1023,6 @@ open Invalidate * 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 = [ - "atoi", readsAll; (*safe*) "connect", readsAll; (*safe*) "__printf_chk", readsAll;(*safe*) "printk", readsAll;(*safe*) From d9418ce3d54161b49de2b49cc26ea10403d95a2f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 13:48:52 +0200 Subject: [PATCH 02/50] `htonl` and friends --- src/analyses/libraryFunctions.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 90d13a00a1..456443d7ff 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -319,6 +319,10 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("posix_fadvise", unknown [drop "fd" []; drop "offset" []; drop "len" []; drop "advice" []]); ("getppid", unknown []); ("lockf", unknown [drop "fd" []; drop "cmd" []; drop "len" []]); + ("htonl", unknown [drop "hostlong" []]); + ("htons", unknown [drop "hostshort" []]); + ("ntohl", unknown [drop "netlong" []]); + ("ntohs", unknown [drop "netshort" []]); ] (** Pthread functions. *) @@ -1151,9 +1155,6 @@ let invalidate_actions = [ "sem_post", readsAll; (*safe*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) - "htonl", readsAll; (*safe*) - "htons", readsAll; (*safe*) - "ntohl", readsAll; (*safe*) "munmap", readsAll;(*safe*) "mmap", readsAll;(*safe*) "clock", readsAll; From f41d2946a065ffa8e32c4ca2b49a10614b9406cd Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 13:54:19 +0200 Subject: [PATCH 03/50] `sleep` an friends --- src/analyses/libraryFunctions.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 456443d7ff..66327275bf 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -323,6 +323,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("htons", unknown [drop "hostshort" []]); ("ntohl", unknown [drop "netlong" []]); ("ntohs", unknown [drop "netshort" []]); + ("sleep", unknown [drop "seconds" []]); + ("usleep", unknown [drop "usec" []]); + ("nanosleep", unknown [drop "req" [r]; drop "rem" [w]]) ] (** Pthread functions. *) @@ -1107,8 +1110,6 @@ let invalidate_actions = [ "bind", readsAll;(*safe*) "svcudp_create", readsAll;(*safe*) "svc_register", writesAll;(*unsafe*) - "sleep", readsAll;(*safe*) - "usleep", readsAll; "svc_run", writesAll;(*unsafe*) "dup", readsAll; (*safe*) "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) From 6489d8cda1b5577a45220810d03fb71295cf01b5 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:01:37 +0200 Subject: [PATCH 04/50] `strchr` and friends --- src/analyses/libraryFunctions.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 66327275bf..54132ff8eb 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -64,6 +64,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strtok", unknown ~attrs:[ThreadUnsafe] [drop "str" [r; w]; drop "delim" [r]]); ("__builtin_strcmp", special [__ "s1" [r]; __ "s2" [r]] @@ fun s1 s2 -> Strcmp { s1; s2; n = None; }); ("strncmp", special [__ "s1" [r]; __ "s2" [r]; __ "n" []] @@ fun s1 s2 n -> Strcmp { s1; s2; n = Some n; }); + ("strchr", unknown [drop "s" [r]; drop "c" []]); + ("strrchr", unknown [drop "s" [r]; drop "c" []]); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); ("calloc", special [__ "n" []; __ "size" []] @@ fun n size -> Calloc {count = n; size}); ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size }); @@ -497,6 +499,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getifaddrs", unknown [drop "ifap" [w]]); ("freeifaddrs", unknown [drop "ifa" [f_deep]]); ("atoq", unknown [drop "nptr" [r]]); + ("strchrnul", unknown [drop "s" [r]; drop "c" []]); ] let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -1078,7 +1081,6 @@ let invalidate_actions = [ "ioctl", writesAll;(*unsafe*) "fstat__extinline", writesAll;(*unsafe*) "umount", readsAll;(*safe*) - "strrchr", readsAll;(*safe*) "scandir", writes [1;3;4];(*keep [1;3;4]*) "unlink", readsAll;(*safe*) "sched_yield", readsAll;(*safe*) @@ -1115,7 +1117,6 @@ let invalidate_actions = [ "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) "strcasecmp", readsAll; (*safe*) - "strchr", readsAll; (*safe*) "__error", readsAll; (*safe*) "__maskrune", writesAll; (*unsafe*) "inet_addr", readsAll; (*safe*) From 53a8aae43962db4b31ee9007398f48eb5d0c44ef Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:06:44 +0200 Subject: [PATCH 05/50] `strcasecmp` and friend --- src/analyses/libraryFunctions.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 54132ff8eb..ccae382abc 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -66,6 +66,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strncmp", special [__ "s1" [r]; __ "s2" [r]; __ "n" []] @@ fun s1 s2 n -> Strcmp { s1; s2; n = Some n; }); ("strchr", unknown [drop "s" [r]; drop "c" []]); ("strrchr", unknown [drop "s" [r]; drop "c" []]); + ("strcasecmp", unknown [drop "s1" [r]; drop "s2" [r]]); + ("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); ("calloc", special [__ "n" []; __ "size" []] @@ fun n size -> Calloc {count = n; size}); ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size }); @@ -1116,7 +1118,6 @@ let invalidate_actions = [ "dup", readsAll; (*safe*) "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) - "strcasecmp", readsAll; (*safe*) "__error", readsAll; (*safe*) "__maskrune", writesAll; (*unsafe*) "inet_addr", readsAll; (*safe*) From 10fd2f0084a14f7a3e67571cfd0325b1098e5978 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:08:56 +0200 Subject: [PATCH 06/50] `__builtin_strchr` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index ccae382abc..19bdba383a 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -65,6 +65,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_strcmp", special [__ "s1" [r]; __ "s2" [r]] @@ fun s1 s2 -> Strcmp { s1; s2; n = None; }); ("strncmp", special [__ "s1" [r]; __ "s2" [r]; __ "n" []] @@ fun s1 s2 n -> Strcmp { s1; s2; n = Some n; }); ("strchr", unknown [drop "s" [r]; drop "c" []]); + ("__builtin_strchr", unknown [drop "s" [r]; drop "c" []]); ("strrchr", unknown [drop "s" [r]; drop "c" []]); ("strcasecmp", unknown [drop "s1" [r]; drop "s2" [r]]); ("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); @@ -1071,7 +1072,6 @@ let invalidate_actions = [ "dlclose", readsAll;(*safe*) "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) - "__builtin_strchr", readsAll;(*safe*) "getpgrp", readsAll;(*safe*) "umount2", readsAll;(*safe*) "memchr", readsAll;(*safe*) From 220adb813d2f0eb5f09bb1c89ac93d0bdf570d77 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:09:31 +0200 Subject: [PATCH 07/50] Rm duplicate `nanosleep` --- src/analyses/libraryFunctions.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 19bdba383a..1ab22f56cd 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -1086,7 +1086,6 @@ let invalidate_actions = [ "scandir", writes [1;3;4];(*keep [1;3;4]*) "unlink", readsAll;(*safe*) "sched_yield", readsAll;(*safe*) - "nanosleep", writesAllButFirst 1 readsAll;(*drop 1*) "sigdelset", readsAll;(*safe*) "sigwait", writesAllButFirst 1 readsAll;(*drop 1*) "setlocale", readsAll;(*safe*) From 6453c18a3d4ef429235720af2638110516cef462 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:12:40 +0200 Subject: [PATCH 08/50] `memcmp` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 1ab22f56cd..d185e0deb0 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -31,6 +31,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strncat", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; }); ("__builtin_strncat", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; }); ("__builtin___strncat_chk", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; }); + ("memcmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); ("asctime", unknown ~attrs:[ThreadUnsafe] [drop "time_ptr" [r_deep]]); ("fclose", unknown [drop "stream" [r_deep; w_deep; f_deep]]); ("feof", unknown [drop "stream" [r_deep; w_deep]]); @@ -1143,7 +1144,6 @@ let invalidate_actions = [ "compress2", writes [3]; (*keep [3]*) "__toupper", readsAll; (*safe*) "BF_set_key", writes [3]; (*keep [3]*) - "memcmp", readsAll; (*safe*) "sendto", writes [2;4]; (*keep [2;4]*) "recvfrom", writes [4;5]; (*keep [4;5]*) "srand", readsAll; (*safe*) From 23491d842f33a63f9cb8514459bb65444b507244 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:14:22 +0200 Subject: [PATCH 09/50] `memchr` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index d185e0deb0..7d8828cbb7 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -32,6 +32,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_strncat", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; }); ("__builtin___strncat_chk", special [__ "dest" [r; w]; __ "src" [r]; __ "n" []; drop "os" []] @@ fun dest src n -> Strcat { dest; src; n = Some n; }); ("memcmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); + ("memchr", unknown [drop "s" [r]; drop "c" []; drop "n" []]); ("asctime", unknown ~attrs:[ThreadUnsafe] [drop "time_ptr" [r_deep]]); ("fclose", unknown [drop "stream" [r_deep; w_deep; f_deep]]); ("feof", unknown [drop "stream" [r_deep; w_deep]]); @@ -1075,7 +1076,6 @@ let invalidate_actions = [ "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "getpgrp", readsAll;(*safe*) "umount2", readsAll;(*safe*) - "memchr", readsAll;(*safe*) "waitpid", readsAll;(*safe*) "statfs", writes [1;3;4];(*keep [1;3;4]*) "mount", readsAll;(*safe*) From 3a4daa6e2e4636c67603b76589ff85ca676226ab Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:24:46 +0200 Subject: [PATCH 10/50] `{set,get}priority` --- src/analyses/libraryFunctions.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 7d8828cbb7..82b5814c80 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -137,6 +137,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("atoi", unknown [drop "nptr" [r]]); ("atol", unknown [drop "nptr" [r]]); ("atoll", unknown [drop "nptr" [r]]); + ("setlocale", unknown [drop "category" []; drop "locale" [r]]); ] (** C POSIX library functions. @@ -332,7 +333,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("ntohs", unknown [drop "netshort" []]); ("sleep", unknown [drop "seconds" []]); ("usleep", unknown [drop "usec" []]); - ("nanosleep", unknown [drop "req" [r]; drop "rem" [w]]) + ("nanosleep", unknown [drop "req" [r]; drop "rem" [w]]); + ("setpriority", unknown [drop "which" []; drop "who" []; drop "prio" []]); + ("getpriority", unknown [drop "which" []; drop "who" []]); ] (** Pthread functions. *) @@ -1089,7 +1092,6 @@ let invalidate_actions = [ "sched_yield", readsAll;(*safe*) "sigdelset", readsAll;(*safe*) "sigwait", writesAllButFirst 1 readsAll;(*drop 1*) - "setlocale", readsAll;(*safe*) "bindtextdomain", readsAll;(*safe*) "textdomain", readsAll;(*safe*) "dcgettext", readsAll;(*safe*) @@ -1171,8 +1173,6 @@ let invalidate_actions = [ "__VERIFIER_nondet_int", readsAll; (* no args, declare invalidate actions to prevent invalidating globals when extern in regression tests *) (* no args, declare invalidate actions to prevent invalidating globals *) "isatty", readsAll; - "setpriority", readsAll; - "getpriority", readsAll; (* ddverify *) "sema_init", readsAll; "__goblint_assume_join", readsAll; From b8f24dd240075f5bdc37942667abf08cd37a3ef8 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:28:44 +0200 Subject: [PATCH 11/50] `execl` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 82b5814c80..2b4e61ee73 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -319,6 +319,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("ffs", unknown [drop "i" []]); ("_exit", special [drop "status" []] Abort); ("execvp", unknown [drop "file" [r]; drop "argv" [r_deep]]); + ("execl", unknown (drop "path" [r] :: VarArgs (drop' [r]))); ("statvfs", unknown [drop "path" [r]; drop "buf" [w]]); ("readlink", unknown [drop "path" [r]; drop "buf" [w]; drop "bufsz" []]); ("wcswidth", unknown [drop "s" [r]; drop "n" []]); @@ -1126,7 +1127,6 @@ let invalidate_actions = [ "setsockopt", readsAll; (*safe*) "listen", readsAll; (*safe*) "getsockname", writes [1;3]; (*keep [1;3]*) - "execl", readsAll; (*safe*) "select", writes [1;5]; (*keep [1;5]*) "accept", writesAll; (*keep [1]*) "getpeername", writes [1]; (*keep [1]*) From b9160486b07750fe492d3e9b0639d622a7bccdd1 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:30:07 +0200 Subject: [PATCH 12/50] `clock` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 2b4e61ee73..294952b4d8 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -138,6 +138,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("atol", unknown [drop "nptr" [r]]); ("atoll", unknown [drop "nptr" [r]]); ("setlocale", unknown [drop "category" []; drop "locale" [r]]); + ("clock", unknown []); ] (** C POSIX library functions. @@ -1161,7 +1162,6 @@ let invalidate_actions = [ "assert_failed", readsAll; (*safe*) "munmap", readsAll;(*safe*) "mmap", readsAll;(*safe*) - "clock", readsAll; "__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 04896736e97113005600995b2cb7144977203318 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:37:54 +0200 Subject: [PATCH 13/50] `sem_init` --- src/analyses/libraryDesc.ml | 1 + src/analyses/libraryFunctions.ml | 3 +-- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 5f9f6f90f9..597c08f72f 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -57,6 +57,7 @@ type special = | Broadcast of Cil.exp | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; } | MutexInit of { mutex:Cil.exp; attr: Cil.exp; } + | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; } | Wait of { cond: Cil.exp; mutex: Cil.exp; } | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) } | Math of { fun_args: math; } diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 294952b4d8..f3c00f9b48 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -407,6 +407,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sem_timedwait", unknown [drop "sem" [r]; drop "abs_timeout" [r]]); (* no write accesses to sem because sync primitive itself has no race *) ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]); ("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]); + ("sem_init", special [__ "sem" [w]; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value}); ] (** GCC builtin functions. @@ -1154,7 +1155,6 @@ let invalidate_actions = [ "fork", readsAll; (*safe*) "setrlimit", readsAll; (*safe*) "getrlimit", writes [2]; (*keep [2]*) - "sem_init", readsAll; (*safe*) "sem_destroy", readsAll; (*safe*) "sem_wait", readsAll; (*safe*) "sem_post", readsAll; (*safe*) @@ -1174,7 +1174,6 @@ let invalidate_actions = [ (* no args, declare invalidate actions to prevent invalidating globals *) "isatty", readsAll; (* ddverify *) - "sema_init", readsAll; "__goblint_assume_join", readsAll; ] From aed4697887c2b2f3838265c39100d724328d7a9e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:42:46 +0200 Subject: [PATCH 14/50] `sem_wait` and `sem_trywait` --- src/analyses/libraryDesc.ml | 1 + src/analyses/libraryFunctions.ml | 4 +++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 597c08f72f..fde24ac77e 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -58,6 +58,7 @@ type special = | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; } | MutexInit of { mutex:Cil.exp; attr: Cil.exp; } | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; } + | SemWait of { sem: Cil.exp; try_:bool} | Wait of { cond: Cil.exp; mutex: Cil.exp; } | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) } | Math of { fun_args: math; } diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index f3c00f9b48..08ec2e2b3e 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -407,7 +407,10 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sem_timedwait", unknown [drop "sem" [r]; drop "abs_timeout" [r]]); (* no write accesses to sem because sync primitive itself has no race *) ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]); ("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]); + (* TODO: Remove w as soon as we have proper support for semaphores *) ("sem_init", special [__ "sem" [w]; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value}); + ("sem_wait", special [__ "sem" [w]] @@ fun sem -> SemWait {sem; try_ = false}); + ("sem_trywait", special [__ "sem" [w]] @@ fun sem -> SemWait {sem; try_ = true}); ] (** GCC builtin functions. @@ -1156,7 +1159,6 @@ let invalidate_actions = [ "setrlimit", readsAll; (*safe*) "getrlimit", writes [2]; (*keep [2]*) "sem_destroy", readsAll; (*safe*) - "sem_wait", readsAll; (*safe*) "sem_post", readsAll; (*safe*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) From e0e11b119f38a318df88128865366254356dd09b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:46:13 +0200 Subject: [PATCH 15/50] Make `sem_wait*` consistent --- src/analyses/libraryDesc.ml | 2 +- src/analyses/libraryFunctions.ml | 9 ++++----- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index fde24ac77e..a0cf133eb8 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -58,7 +58,7 @@ type special = | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; } | MutexInit of { mutex:Cil.exp; attr: Cil.exp; } | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; } - | SemWait of { sem: Cil.exp; try_:bool} + | SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;} | Wait of { cond: Cil.exp; mutex: Cil.exp; } | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) } | Math of { fun_args: math; } diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 08ec2e2b3e..fa87810b74 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -404,13 +404,12 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_condattr_setclock", unknown [drop "attr" [w]; drop "clock_id" []]); ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]); ("pthread_attr_setschedparam", unknown [drop "attr" [r; w]; drop "param" [r]]); - ("sem_timedwait", unknown [drop "sem" [r]; drop "abs_timeout" [r]]); (* no write accesses to sem because sync primitive itself has no race *) ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]); ("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]); - (* TODO: Remove w as soon as we have proper support for semaphores *) - ("sem_init", special [__ "sem" [w]; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value}); - ("sem_wait", special [__ "sem" [w]] @@ fun sem -> SemWait {sem; try_ = false}); - ("sem_trywait", special [__ "sem" [w]] @@ fun sem -> SemWait {sem; try_ = true}); + ("sem_init", special [__ "sem" [r]; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value}); + ("sem_wait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = false; timeout = None}); + ("sem_trywait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = true; timeout = None}); + ("sem_timedwait", special [__ "sem" [r]; __ "abs_timeout" [r]] @@ fun sem abs_timeout-> SemWait {sem; try_ = true; timeout = Some abs_timeout}); (* no write accesses to sem because sync primitive itself has no race *) ] (** GCC builtin functions. From 9fae0dc7e76ca2f842b4f7e2d83fded33cbc1c2b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:49:11 +0200 Subject: [PATCH 16/50] `sem_post` --- src/analyses/libraryDesc.ml | 1 + src/analyses/libraryFunctions.ml | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index a0cf133eb8..ad666bf1ee 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -59,6 +59,7 @@ type special = | MutexInit of { mutex:Cil.exp; attr: Cil.exp; } | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; } | SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;} + | SemPost of Cil.exp | Wait of { cond: Cil.exp; mutex: Cil.exp; } | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) } | Math of { fun_args: math; } diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index fa87810b74..3309a31d09 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -410,6 +410,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sem_wait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = false; timeout = None}); ("sem_trywait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = true; timeout = None}); ("sem_timedwait", special [__ "sem" [r]; __ "abs_timeout" [r]] @@ fun sem abs_timeout-> SemWait {sem; try_ = true; timeout = Some abs_timeout}); (* no write accesses to sem because sync primitive itself has no race *) + ("sem_post", special [__ "sem" [r]] @@ fun sem -> SemPost sem); ] (** GCC builtin functions. @@ -1158,7 +1159,6 @@ let invalidate_actions = [ "setrlimit", readsAll; (*safe*) "getrlimit", writes [2]; (*keep [2]*) "sem_destroy", readsAll; (*safe*) - "sem_post", readsAll; (*safe*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) "munmap", readsAll;(*safe*) From 92528b1ba0367e3b48cf04013f2f096654340b1b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 14:51:18 +0200 Subject: [PATCH 17/50] `sem_destroy` --- src/analyses/libraryDesc.ml | 1 + src/analyses/libraryFunctions.ml | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index ad666bf1ee..06a9b7e55b 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -60,6 +60,7 @@ type special = | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; } | SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;} | SemPost of Cil.exp + | SemDestroy of Cil.exp | Wait of { cond: Cil.exp; mutex: Cil.exp; } | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) } | Math of { fun_args: math; } diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 3309a31d09..16221b7de1 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -411,6 +411,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sem_trywait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = true; timeout = None}); ("sem_timedwait", special [__ "sem" [r]; __ "abs_timeout" [r]] @@ fun sem abs_timeout-> SemWait {sem; try_ = true; timeout = Some abs_timeout}); (* no write accesses to sem because sync primitive itself has no race *) ("sem_post", special [__ "sem" [r]] @@ fun sem -> SemPost sem); + ("sem_destroy", special [__ "sem" [r]] @@ fun sem -> SemDestroy sem); ] (** GCC builtin functions. @@ -1158,7 +1159,6 @@ let invalidate_actions = [ "fork", readsAll; (*safe*) "setrlimit", readsAll; (*safe*) "getrlimit", writes [2]; (*keep [2]*) - "sem_destroy", readsAll; (*safe*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) "munmap", readsAll;(*safe*) From 68f7ff8f0bf52cc5ad1de1b4df4a0ad02ed84cfd Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:20:25 +0200 Subject: [PATCH 18/50] `sched_yield` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 16221b7de1..1331c11475 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -338,6 +338,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("nanosleep", unknown [drop "req" [r]; drop "rem" [w]]); ("setpriority", unknown [drop "which" []; drop "who" []; drop "prio" []]); ("getpriority", unknown [drop "which" []; drop "who" []]); + ("sched_yield", unknown []); ] (** Pthread functions. *) @@ -1096,7 +1097,6 @@ let invalidate_actions = [ "umount", readsAll;(*safe*) "scandir", writes [1;3;4];(*keep [1;3;4]*) "unlink", readsAll;(*safe*) - "sched_yield", readsAll;(*safe*) "sigdelset", readsAll;(*safe*) "sigwait", writesAllButFirst 1 readsAll;(*drop 1*) "bindtextdomain", readsAll;(*safe*) From d2fa5b10a513d96cfc33fc15764fa3ea2c58311d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:22:21 +0200 Subject: [PATCH 19/50] `srand` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 1331c11475..039b1eb459 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -93,6 +93,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getchar", unknown []); ("putchar", unknown [drop "ch" []]); ("puts", unknown [drop "s" [r]]); + ("srand", unknown [drop "seed" []]); ("rand", special ~attrs:[ThreadUnsafe] [] Rand); ("strerror", unknown ~attrs:[ThreadUnsafe] [drop "errnum" []]); ("strspn", unknown [drop "s" [r]; drop "accept" [r]]); @@ -1154,7 +1155,6 @@ let invalidate_actions = [ "BF_set_key", writes [3]; (*keep [3]*) "sendto", writes [2;4]; (*keep [2;4]*) "recvfrom", writes [4;5]; (*keep [4;5]*) - "srand", readsAll; (*safe*) "gethostname", writesAll; (*unsafe*) "fork", readsAll; (*safe*) "setrlimit", readsAll; (*safe*) From de0dbca93dabbe92674f29c66096423a22907090 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:25:12 +0200 Subject: [PATCH 20/50] `getpid` --- src/analyses/libraryFunctions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 039b1eb459..1a8af90122 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -328,7 +328,6 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("link", unknown [drop "oldpath" [r]; drop "newpath" [r]]); ("renameat", unknown [drop "olddirfd" []; drop "oldpath" [r]; drop "newdirfd" []; drop "newpath" [r]]); ("posix_fadvise", unknown [drop "fd" []; drop "offset" []; drop "len" []; drop "advice" []]); - ("getppid", unknown []); ("lockf", unknown [drop "fd" []; drop "cmd" []; drop "len" []]); ("htonl", unknown [drop "hostlong" []]); ("htons", unknown [drop "hostshort" []]); @@ -340,6 +339,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("setpriority", unknown [drop "which" []; drop "who" []; drop "prio" []]); ("getpriority", unknown [drop "which" []; drop "who" []]); ("sched_yield", unknown []); + ("getpid", unknown []); + ("getppid", unknown []); ] (** Pthread functions. *) @@ -1071,7 +1072,6 @@ let invalidate_actions = [ "geteuid", readsAll;(*safe*) "readdir_r", writesAll;(*unsafe*) "atoi__extinline", readsAll;(*safe*) - "getpid", readsAll;(*safe*) "_IO_getc", writesAll;(*unsafe*) "pipe", writesAll;(*unsafe*) "close", writesAll;(*unsafe*) From 978f6b294a59dacfbee84147cd6c3ebb9ba6c716 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:26:36 +0200 Subject: [PATCH 21/50] `getuid`, `geteuid` --- src/analyses/libraryFunctions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 1a8af90122..3e5f7d1887 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -341,6 +341,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sched_yield", unknown []); ("getpid", unknown []); ("getppid", unknown []); + ("getuid", unknown []); + ("geteuid", unknown []); ] (** Pthread functions. *) @@ -1069,7 +1071,6 @@ let invalidate_actions = [ "getopt_long", writesAllButFirst 2 readsAll;(*drop 2*) "__strdup", readsAll;(*safe*) "strtoul__extinline", readsAll;(*safe*) - "geteuid", readsAll;(*safe*) "readdir_r", writesAll;(*unsafe*) "atoi__extinline", readsAll;(*safe*) "_IO_getc", writesAll;(*unsafe*) @@ -1108,7 +1109,6 @@ let invalidate_actions = [ "gethostbyname_r", readsAll;(*safe*) "__h_errno_location", readsAll;(*safe*) "__fxstat", readsAll;(*safe*) - "getuid", readsAll;(*safe*) "openlog", readsAll;(*safe*) "getdtablesize", readsAll;(*safe*) "umask", readsAll;(*safe*) From 96ea9819af21d88e551fe2068927edff3ac0c702 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:28:07 +0200 Subject: [PATCH 22/50] `getpgrp` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 3e5f7d1887..5e32686f96 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -343,6 +343,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getppid", unknown []); ("getuid", unknown []); ("geteuid", unknown []); + ("getpgrp", unknown []); ] (** Pthread functions. *) @@ -1087,7 +1088,6 @@ let invalidate_actions = [ "dlclose", readsAll;(*safe*) "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) - "getpgrp", readsAll;(*safe*) "umount2", readsAll;(*safe*) "waitpid", readsAll;(*safe*) "statfs", writes [1;3;4];(*keep [1;3;4]*) From 9f80b1c48dce2664bd1d2dd71eb8c765fc381ac3 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:31:56 +0200 Subject: [PATCH 23/50] `{set,get}rlimit` --- src/analyses/libraryFunctions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 5e32686f96..26619d8b83 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -344,6 +344,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getuid", unknown []); ("geteuid", unknown []); ("getpgrp", unknown []); + ("setrlimit", unknown [drop "resource" []; drop "rlim" [r]]); + ("getrlimit", unknown [drop "resource" []; drop "rlim" [w]]); ] (** Pthread functions. *) @@ -1157,8 +1159,6 @@ let invalidate_actions = [ "recvfrom", writes [4;5]; (*keep [4;5]*) "gethostname", writesAll; (*unsafe*) "fork", readsAll; (*safe*) - "setrlimit", readsAll; (*safe*) - "getrlimit", writes [2]; (*keep [2]*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) "munmap", readsAll;(*safe*) From 62f96fb70e45b47ca66aec11d84d7969b08d7500 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:33:05 +0200 Subject: [PATCH 24/50] `setsid` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 26619d8b83..3087ea5440 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -346,6 +346,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getpgrp", unknown []); ("setrlimit", unknown [drop "resource" []; drop "rlim" [r]]); ("getrlimit", unknown [drop "resource" []; drop "rlim" [w]]); + ("setsid", unknown []); ] (** Pthread functions. *) @@ -1079,7 +1080,6 @@ let invalidate_actions = [ "_IO_getc", writesAll;(*unsafe*) "pipe", writesAll;(*unsafe*) "close", writesAll;(*unsafe*) - "setsid", readsAll;(*safe*) "strerror_r", writesAll;(*unsafe*) "sigemptyset", writesAll;(*unsafe*) "sigaddset", writesAll;(*unsafe*) From a50a177a94475dee3b1260b776833071c4ea568c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:35:05 +0200 Subject: [PATCH 25/50] `getdtablesize` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 3087ea5440..1acbbc1ab2 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -546,6 +546,7 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fts_open", unknown [drop "path_argv" [r_deep]; drop "options" []; drop "compar" [s]]); (* TODO: use Call instead of Spawn *) ("fts_read", unknown [drop "ftsp" [r_deep; w_deep]]); ("fts_close", unknown [drop "ftsp" [f_deep]]); + ("getdtablesize", unknown []); ] let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType))) @@ -1112,7 +1113,6 @@ let invalidate_actions = [ "__h_errno_location", readsAll;(*safe*) "__fxstat", readsAll;(*safe*) "openlog", readsAll;(*safe*) - "getdtablesize", readsAll;(*safe*) "umask", readsAll;(*safe*) "socket", readsAll;(*safe*) "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*) From fdd2758c7c5fe83fda6b611f2aca185909155298 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:36:58 +0200 Subject: [PATCH 26/50] `isatty` --- src/analyses/libraryFunctions.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 1acbbc1ab2..5ee8f1ce16 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -347,6 +347,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("setrlimit", unknown [drop "resource" []; drop "rlim" [r]]); ("getrlimit", unknown [drop "resource" []; drop "rlim" [w]]); ("setsid", unknown []); + ("isatty", unknown [drop "fd" []]); ] (** Pthread functions. *) @@ -1172,8 +1173,6 @@ let invalidate_actions = [ "idr_pre_get", readsAll; "zil_replay", writes [1;2;3;5]; "__VERIFIER_nondet_int", readsAll; (* no args, declare invalidate actions to prevent invalidating globals when extern in regression tests *) - (* no args, declare invalidate actions to prevent invalidating globals *) - "isatty", readsAll; (* ddverify *) "__goblint_assume_join", readsAll; ] From 255035f616e9fd2dc7bd3a89163e7bf98733de25 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:38:38 +0200 Subject: [PATCH 27/50] `__VERIFIER_nondet_int` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 5ee8f1ce16..8db04e21a9 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -875,6 +875,7 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__VERIFIER_atomic_begin", special [] @@ Lock { lock = verifier_atomic; try_ = false; write = true; return_on_success = true }); ("__VERIFIER_atomic_end", special [] @@ Unlock verifier_atomic); ("__VERIFIER_nondet_loff_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *) + ("__VERIFIER_nondet_int", unknown []); (* declare invalidate actions to prevent invalidating globals when extern in regression tests *) ] let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -1172,7 +1173,6 @@ let invalidate_actions = [ "kmem_cache_create", readsAll; "idr_pre_get", readsAll; "zil_replay", writes [1;2;3;5]; - "__VERIFIER_nondet_int", readsAll; (* no args, declare invalidate actions to prevent invalidating globals when extern in regression tests *) (* ddverify *) "__goblint_assume_join", readsAll; ] From 13bc14ce62973f025484b005301a19deff236bbe Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:44:01 +0200 Subject: [PATCH 28/50] `sigemptyset` and friends --- src/analyses/libraryFunctions.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 8db04e21a9..89f31d8ffe 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -348,6 +348,11 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getrlimit", unknown [drop "resource" []; drop "rlim" [w]]); ("setsid", unknown []); ("isatty", unknown [drop "fd" []]); + ("sigemptyset", unknown [drop "set" [w]]); + ("sigfillset", unknown [drop "set" [w]]); + ("sigaddset", unknown [drop "set" [w]; drop "signum" []]); + ("sigdelset", unknown [drop "set" [w]; drop "signum" []]); + ("sigismember", unknown [drop "set" [r]; drop "signum" []]); ] (** Pthread functions. *) @@ -1072,7 +1077,6 @@ let invalidate_actions = [ "__ctype_b_loc", readsAll;(*safe*) "__errno", readsAll;(*safe*) "__errno_location", readsAll;(*safe*) - "sigfillset", writesAll; (*unsafe*) "sigprocmask", writesAll; (*unsafe*) "uname", writesAll;(*unsafe*) "getopt_long", writesAllButFirst 2 readsAll;(*drop 2*) @@ -1084,8 +1088,6 @@ let invalidate_actions = [ "pipe", writesAll;(*unsafe*) "close", writesAll;(*unsafe*) "strerror_r", writesAll;(*unsafe*) - "sigemptyset", writesAll;(*unsafe*) - "sigaddset", writesAll;(*unsafe*) "raise", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) "dlopen", readsAll;(*safe*) @@ -1104,7 +1106,6 @@ let invalidate_actions = [ "umount", readsAll;(*safe*) "scandir", writes [1;3;4];(*keep [1;3;4]*) "unlink", readsAll;(*safe*) - "sigdelset", readsAll;(*safe*) "sigwait", writesAllButFirst 1 readsAll;(*drop 1*) "bindtextdomain", readsAll;(*safe*) "textdomain", readsAll;(*safe*) From c439e2e5b20f08336896de7845136854db241a7e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:46:46 +0200 Subject: [PATCH 29/50] `sigprocmask` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 89f31d8ffe..f31cec9be6 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -353,6 +353,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sigaddset", unknown [drop "set" [w]; drop "signum" []]); ("sigdelset", unknown [drop "set" [w]; drop "signum" []]); ("sigismember", unknown [drop "set" [r]; drop "signum" []]); + ("sigprocmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]); ] (** Pthread functions. *) @@ -1077,7 +1078,6 @@ let invalidate_actions = [ "__ctype_b_loc", readsAll;(*safe*) "__errno", readsAll;(*safe*) "__errno_location", readsAll;(*safe*) - "sigprocmask", writesAll; (*unsafe*) "uname", writesAll;(*unsafe*) "getopt_long", writesAllButFirst 2 readsAll;(*drop 2*) "__strdup", readsAll;(*safe*) From fa8de7d30ca4c61b33e731b269aafdaf8501bdf4 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:48:16 +0200 Subject: [PATCH 30/50] `fork` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index f31cec9be6..a1ccbeba47 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -354,6 +354,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sigdelset", unknown [drop "set" [w]; drop "signum" []]); ("sigismember", unknown [drop "set" [r]; drop "signum" []]); ("sigprocmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]); + ("fork", unknown []); ] (** Pthread functions. *) @@ -1161,7 +1162,6 @@ let invalidate_actions = [ "sendto", writes [2;4]; (*keep [2;4]*) "recvfrom", writes [4;5]; (*keep [4;5]*) "gethostname", writesAll; (*unsafe*) - "fork", readsAll; (*safe*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) "munmap", readsAll;(*safe*) From 8c7a633bc4cc155981b8d2d4a2eb5aefa7517c8a Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:54:45 +0200 Subject: [PATCH 31/50] dynamic linking --- src/analyses/libraryFunctions.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index a1ccbeba47..1f557005a3 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -161,7 +161,6 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("dbm_nextkey", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep]]); ("dbm_open", unknown ~attrs:[ThreadUnsafe] [drop "file" [r; w]; drop "open_flags" []; drop "file_mode" []]); ("dbm_store", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep; w_deep]; drop "key" []; drop "content" []; drop "store_mode" []]); - ("dlerror", unknown ~attrs:[ThreadUnsafe] []); ("drand48", unknown ~attrs:[ThreadUnsafe] []); ("encrypt", unknown ~attrs:[ThreadUnsafe] [drop "block" [r; w]; drop "edflag" []]); ("setkey", unknown ~attrs:[ThreadUnsafe] [drop "key" [r]]); @@ -355,6 +354,10 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sigismember", unknown [drop "set" [r]; drop "signum" []]); ("sigprocmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]); ("fork", unknown []); + ("dlopen", unknown [drop "filename" [r]; drop "flag" []]); + ("dlerror", unknown ~attrs:[ThreadUnsafe] []); (* TODO: Why thread-unsafe? https://linux.die.net/man/3/dlopen *) + ("dlsym", unknown [drop "handle" [r]; drop "symbol" [r]]); + ("dlclose", unknown [drop "handle" [r]]); ] (** Pthread functions. *) @@ -1091,9 +1094,6 @@ let invalidate_actions = [ "strerror_r", writesAll;(*unsafe*) "raise", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) - "dlopen", readsAll;(*safe*) - "dlsym", readsAll;(*safe*) - "dlclose", readsAll;(*safe*) "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "umount2", readsAll;(*safe*) From 9b3b38f09e0420896cc4e9f20ce99d26d9e8a575 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 15:58:04 +0200 Subject: [PATCH 32/50] `inet_addr` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 1f557005a3..88ef3638b8 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -358,6 +358,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("dlerror", unknown ~attrs:[ThreadUnsafe] []); (* TODO: Why thread-unsafe? https://linux.die.net/man/3/dlopen *) ("dlsym", unknown [drop "handle" [r]; drop "symbol" [r]]); ("dlclose", unknown [drop "handle" [r]]); + ("inet_addr", unknown [drop "cp" [r]]) ] (** Pthread functions. *) @@ -1136,7 +1137,6 @@ let invalidate_actions = [ "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) "__error", readsAll; (*safe*) "__maskrune", writesAll; (*unsafe*) - "inet_addr", readsAll; (*safe*) "setsockopt", readsAll; (*safe*) "listen", readsAll; (*safe*) "getsockname", writes [1;3]; (*keep [1;3]*) From d4d170bcfd383c6c5c7a91560119054b3432d9da Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 16:00:11 +0200 Subject: [PATCH 33/50] `setsockopt` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 88ef3638b8..c1b3a61291 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -245,6 +245,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("hstrerror", unknown [drop "err" []]); ("inet_ntoa", unknown ~attrs:[ThreadUnsafe] [drop "in" []]); ("getsockopt", unknown [drop "sockfd" []; drop "level" []; drop "optname" []; drop "optval" [w]; drop "optlen" [w]]); + ("setsockopt", unknown [drop "sockfd" []; drop "level" []; drop "optname" []; drop "optval" [r]; drop "optlen" []]); ("gethostbyaddr", unknown ~attrs:[ThreadUnsafe] [drop "addr" [r_deep]; drop "len" []; drop "type" []]); ("gethostbyaddr_r", unknown [drop "addr" [r_deep]; drop "len" []; drop "type" []; drop "ret" [w_deep]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); ("gethostbyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); @@ -1137,7 +1138,6 @@ let invalidate_actions = [ "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) "__error", readsAll; (*safe*) "__maskrune", writesAll; (*unsafe*) - "setsockopt", readsAll; (*safe*) "listen", readsAll; (*safe*) "getsockname", writes [1;3]; (*keep [1;3]*) "select", writes [1;5]; (*keep [1;5]*) From ba4b4367b8de6135298b0420fe8449b875305bc0 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 16:02:19 +0200 Subject: [PATCH 34/50] `getsockname` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index c1b3a61291..a4624c1715 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -246,6 +246,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("inet_ntoa", unknown ~attrs:[ThreadUnsafe] [drop "in" []]); ("getsockopt", unknown [drop "sockfd" []; drop "level" []; drop "optname" []; drop "optval" [w]; drop "optlen" [w]]); ("setsockopt", unknown [drop "sockfd" []; drop "level" []; drop "optname" []; drop "optval" [r]; drop "optlen" []]); + ("getsockname", unknown [drop "sockfd" [r]; drop "addr" [w]; drop "addrlen" [r]]); ("gethostbyaddr", unknown ~attrs:[ThreadUnsafe] [drop "addr" [r_deep]; drop "len" []; drop "type" []]); ("gethostbyaddr_r", unknown [drop "addr" [r_deep]; drop "len" []; drop "type" []; drop "ret" [w_deep]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); ("gethostbyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); @@ -1139,7 +1140,6 @@ let invalidate_actions = [ "__error", readsAll; (*safe*) "__maskrune", writesAll; (*unsafe*) "listen", readsAll; (*safe*) - "getsockname", writes [1;3]; (*keep [1;3]*) "select", writes [1;5]; (*keep [1;5]*) "accept", writesAll; (*keep [1]*) "getpeername", writes [1]; (*keep [1]*) From 7742c6527a6cae28c017f664b41ea81f062bad48 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 16:04:37 +0200 Subject: [PATCH 35/50] `socket` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index a4624c1715..ef15ca0823 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -250,6 +250,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("gethostbyaddr", unknown ~attrs:[ThreadUnsafe] [drop "addr" [r_deep]; drop "len" []; drop "type" []]); ("gethostbyaddr_r", unknown [drop "addr" [r_deep]; drop "len" []; drop "type" []; drop "ret" [w_deep]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); ("gethostbyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); + ("socket", unknown [drop "domain" []; drop "type" []; drop "protocol" []]); ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); ("tcgetattr", unknown [drop "fd" []; drop "termios_p" [w_deep]]); ("tcsetattr", unknown [drop "fd" []; drop "optional_actions" []; drop "termios_p" [r_deep]]); @@ -1121,7 +1122,6 @@ let invalidate_actions = [ "__fxstat", readsAll;(*safe*) "openlog", readsAll;(*safe*) "umask", readsAll;(*safe*) - "socket", readsAll;(*safe*) "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*) "svctcp_create", readsAll;(*safe*) "clntudp_bufcreate", writesAll;(*unsafe*) From 57bc1ba203d764fd1b63b89634ecfc312b0dff0c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 16:08:48 +0200 Subject: [PATCH 36/50] `gethostbyname_r` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index ef15ca0823..eb5c07f793 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -250,6 +250,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("gethostbyaddr", unknown ~attrs:[ThreadUnsafe] [drop "addr" [r_deep]; drop "len" []; drop "type" []]); ("gethostbyaddr_r", unknown [drop "addr" [r_deep]; drop "len" []; drop "type" []; drop "ret" [w_deep]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); ("gethostbyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); + ("gethostbyname_r", unknown [drop "name" [r]; drop "result_buf" [w]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]) ("socket", unknown [drop "domain" []; drop "type" []; drop "protocol" []]); ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); ("tcgetattr", unknown [drop "fd" []; drop "termios_p" [w_deep]]); @@ -1117,7 +1118,6 @@ let invalidate_actions = [ "dcgettext", readsAll;(*safe*) "putw", readsAll;(*safe*) "__getdelim", writes [3];(*keep [3]*) - "gethostbyname_r", readsAll;(*safe*) "__h_errno_location", readsAll;(*safe*) "__fxstat", readsAll;(*safe*) "openlog", readsAll;(*safe*) From d535a47cae1ddf251e884d71633a6fde859fd674 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 16:11:21 +0200 Subject: [PATCH 37/50] `gethostname` --- src/analyses/libraryFunctions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index eb5c07f793..8a84d87457 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -250,7 +250,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("gethostbyaddr", unknown ~attrs:[ThreadUnsafe] [drop "addr" [r_deep]; drop "len" []; drop "type" []]); ("gethostbyaddr_r", unknown [drop "addr" [r_deep]; drop "len" []; drop "type" []; drop "ret" [w_deep]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); ("gethostbyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); - ("gethostbyname_r", unknown [drop "name" [r]; drop "result_buf" [w]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]) + ("gethostbyname_r", unknown [drop "name" [r]; drop "result_buf" [w]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); + ("gethostname", unknown [drop "name" [w]; drop "len" []]); ("socket", unknown [drop "domain" []; drop "type" []; drop "protocol" []]); ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); ("tcgetattr", unknown [drop "fd" []; drop "termios_p" [w_deep]]); @@ -1161,7 +1162,6 @@ let invalidate_actions = [ "BF_set_key", writes [3]; (*keep [3]*) "sendto", writes [2;4]; (*keep [2;4]*) "recvfrom", writes [4;5]; (*keep [4;5]*) - "gethostname", writesAll; (*unsafe*) "PL_NewHashTable", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) "munmap", readsAll;(*safe*) From f5ffd12ea42f5a8504f10f89f23989c441c924ef Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 16:13:57 +0200 Subject: [PATCH 38/50] `getpeername` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 8a84d87457..78fe678ba0 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -252,6 +252,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("gethostbyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); ("gethostbyname_r", unknown [drop "name" [r]; drop "result_buf" [w]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); ("gethostname", unknown [drop "name" [w]; drop "len" []]); + ("getpeername", unknown [drop "sockfd" []; drop "addr" [w]; drop "addrlen" [r]]); ("socket", unknown [drop "domain" []; drop "type" []; drop "protocol" []]); ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); ("tcgetattr", unknown [drop "fd" []; drop "termios_p" [w_deep]]); @@ -1143,7 +1144,6 @@ let invalidate_actions = [ "listen", readsAll; (*safe*) "select", writes [1;5]; (*keep [1;5]*) "accept", writesAll; (*keep [1]*) - "getpeername", writes [1]; (*keep [1]*) "times", writesAll; (*unsafe*) "timespec_get", writes [1]; "__tolower", readsAll; (*safe*) From a085287c6fcb5d4685d07398ee39d3ec02fc973c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 16:15:51 +0200 Subject: [PATCH 39/50] `uname` --- src/analyses/libraryFunctions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 78fe678ba0..d186c15c64 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -364,7 +364,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("dlerror", unknown ~attrs:[ThreadUnsafe] []); (* TODO: Why thread-unsafe? https://linux.die.net/man/3/dlopen *) ("dlsym", unknown [drop "handle" [r]; drop "symbol" [r]]); ("dlclose", unknown [drop "handle" [r]]); - ("inet_addr", unknown [drop "cp" [r]]) + ("inet_addr", unknown [drop "cp" [r]]); + ("uname", unknown [drop "buf" [w]]); ] (** Pthread functions. *) @@ -1089,7 +1090,6 @@ let invalidate_actions = [ "__ctype_b_loc", readsAll;(*safe*) "__errno", readsAll;(*safe*) "__errno_location", readsAll;(*safe*) - "uname", writesAll;(*unsafe*) "getopt_long", writesAllButFirst 2 readsAll;(*drop 2*) "__strdup", readsAll;(*safe*) "strtoul__extinline", readsAll;(*safe*) From 9fb68d4faaa38aacd00b0fc872c6c714ecb25be9 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 16:19:33 +0200 Subject: [PATCH 40/50] `getopt_long` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index d186c15c64..e0e8a20707 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -219,6 +219,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fileno", unknown [drop "stream" [r_deep; w_deep]]); ("fdopen", unknown [drop "fd" []; drop "mode" [r]]); ("getopt", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r_deep]; drop "optstring" [r]]); + ("getopt_long", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r_deep]; drop "optstring" [r]; drop "longopts" [r]; drop "longindex" [w]]); ("iconv_open", unknown [drop "tocode" [r]; drop "fromcode" [r]]); ("iconv", unknown [drop "cd" [r]; drop "inbuf" [r]; drop "inbytesleft" [r;w]; drop "outbuf" [w]; drop "outbytesleft" [r;w]]); ("iconv_close", unknown [drop "cd" [f]]); @@ -1090,7 +1091,6 @@ let invalidate_actions = [ "__ctype_b_loc", readsAll;(*safe*) "__errno", readsAll;(*safe*) "__errno_location", readsAll;(*safe*) - "getopt_long", writesAllButFirst 2 readsAll;(*drop 2*) "__strdup", readsAll;(*safe*) "strtoul__extinline", readsAll;(*safe*) "readdir_r", writesAll;(*unsafe*) From c8ed7e283683204e5b93c6ae57cea8011d2ab09c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 17:02:35 +0200 Subject: [PATCH 41/50] Enable `svcomp` library functions where `racemacros.h` is included --- tests/regression/28-race_reach/01-simple_racing.c | 3 ++- tests/regression/28-race_reach/02-simple_racefree.c | 3 ++- tests/regression/28-race_reach/03-munge_racing.c | 3 ++- tests/regression/28-race_reach/04-munge_racefree.c | 3 ++- tests/regression/28-race_reach/05-lockfuns_racefree.c | 3 ++- tests/regression/28-race_reach/06-cond_racing1.c | 5 +---- tests/regression/28-race_reach/07-cond_racing2.c | 1 + tests/regression/28-race_reach/08-cond_racefree.c | 1 + tests/regression/28-race_reach/09-ptrmunge_racing.c | 3 ++- tests/regression/28-race_reach/10-ptrmunge_racefree.c | 3 ++- tests/regression/28-race_reach/11-ptr_racing.c | 3 ++- tests/regression/28-race_reach/12-ptr_racefree.c | 5 +++-- tests/regression/28-race_reach/19-callback_racing.c | 1 + tests/regression/28-race_reach/20-callback_racefree.c | 1 + tests/regression/28-race_reach/21-deref_read_racing.c | 1 + tests/regression/28-race_reach/22-deref_read_racefree.c | 1 + tests/regression/28-race_reach/23-sound_unlock_racing.c | 1 + tests/regression/28-race_reach/24-sound_lock_racing.c | 1 + tests/regression/28-race_reach/27-funptr_racing.c | 7 ++++--- tests/regression/28-race_reach/28-funptr_racefree.c | 9 +++++---- tests/regression/28-race_reach/36-indirect_racefree.c | 1 + tests/regression/28-race_reach/37-indirect_racing.c | 1 + tests/regression/28-race_reach/40-trylock_racing.c | 3 ++- tests/regression/28-race_reach/41-trylock_racefree.c | 3 ++- tests/regression/28-race_reach/42-trylock2_racefree.c | 3 ++- tests/regression/28-race_reach/45-escape_racing.c | 1 + tests/regression/28-race_reach/46-escape_racefree.c | 1 + tests/regression/28-race_reach/51-mutexptr_racefree.c | 1 + tests/regression/28-race_reach/60-invariant_racefree.c | 1 + tests/regression/28-race_reach/61-invariant_racing.c | 1 + tests/regression/28-race_reach/70-funloop_racefree.c | 2 +- tests/regression/28-race_reach/71-funloop_racing.c | 2 +- tests/regression/28-race_reach/72-funloop_hard_racing.c | 2 +- .../regression/28-race_reach/73-funloop_hard_racefree.c | 2 +- .../28-race_reach/74-tricky_address1_racefree.c | 2 +- .../28-race_reach/75-tricky_address2_racefree.c | 2 +- .../28-race_reach/76-tricky_address3_racefree.c | 2 +- .../regression/28-race_reach/77-tricky_address4_racing.c | 2 +- tests/regression/28-race_reach/78-equ_racing.c | 2 +- tests/regression/28-race_reach/79-equ_racefree.c | 2 +- tests/regression/28-race_reach/81-list_racing.c | 2 +- tests/regression/28-race_reach/82-list_racefree.c | 2 +- tests/regression/28-race_reach/83-list2_racing1.c | 2 +- tests/regression/28-race_reach/84-list2_racing2.c | 2 +- tests/regression/28-race_reach/85-list2_racefree.c | 2 +- tests/regression/28-race_reach/86-lists_racing.c | 2 +- tests/regression/28-race_reach/87-lists_racefree.c | 2 +- tests/regression/28-race_reach/90-arrayloop2_racing.c | 2 +- tests/regression/28-race_reach/91-arrayloop2_racefree.c | 2 +- tests/regression/28-race_reach/92-evilcollapse_racing.c | 2 +- .../regression/28-race_reach/93-evilcollapse_racefree.c | 2 +- tests/regression/28-race_reach/94-alloc_region_racing.c | 2 +- 52 files changed, 72 insertions(+), 46 deletions(-) diff --git a/tests/regression/28-race_reach/01-simple_racing.c b/tests/regression/28-race_reach/01-simple_racing.c index 16a0fb28c9..f444228690 100644 --- a/tests/regression/28-race_reach/01-simple_racing.c +++ b/tests/regression/28-race_reach/01-simple_racing.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -19,4 +20,4 @@ int main(void) { pthread_mutex_unlock(&mutex2); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/02-simple_racefree.c b/tests/regression/28-race_reach/02-simple_racefree.c index 4713ccd48d..0e35f8da67 100644 --- a/tests/regression/28-race_reach/02-simple_racefree.c +++ b/tests/regression/28-race_reach/02-simple_racefree.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -19,4 +20,4 @@ int main(void) { pthread_mutex_unlock(&mutex1); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/03-munge_racing.c b/tests/regression/28-race_reach/03-munge_racing.c index 3c279d597a..9b8536e540 100644 --- a/tests/regression/28-race_reach/03-munge_racing.c +++ b/tests/regression/28-race_reach/03-munge_racing.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -26,4 +27,4 @@ int main(void) { create_threads(t1); create_threads(t2); join_threads(t1); join_threads(t2); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/04-munge_racefree.c b/tests/regression/28-race_reach/04-munge_racefree.c index 799477e6ae..86637da91f 100644 --- a/tests/regression/28-race_reach/04-munge_racefree.c +++ b/tests/regression/28-race_reach/04-munge_racefree.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -26,4 +27,4 @@ int main(void) { create_threads(t1); create_threads(t2); join_threads(t1); join_threads(t2); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/05-lockfuns_racefree.c b/tests/regression/28-race_reach/05-lockfuns_racefree.c index 0faecd0217..0a904005f8 100644 --- a/tests/regression/28-race_reach/05-lockfuns_racefree.c +++ b/tests/regression/28-race_reach/05-lockfuns_racefree.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -26,4 +27,4 @@ int main(void) { unlock(); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/06-cond_racing1.c b/tests/regression/28-race_reach/06-cond_racing1.c index c3e87507d5..931b68f81f 100644 --- a/tests/regression/28-race_reach/06-cond_racing1.c +++ b/tests/regression/28-race_reach/06-cond_racing1.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include @@ -31,7 +32,3 @@ int main() { join_threads(t); return 0; } - - - - diff --git a/tests/regression/28-race_reach/07-cond_racing2.c b/tests/regression/28-race_reach/07-cond_racing2.c index b13b52dd1c..5e0d3f77f5 100644 --- a/tests/regression/28-race_reach/07-cond_racing2.c +++ b/tests/regression/28-race_reach/07-cond_racing2.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/08-cond_racefree.c b/tests/regression/28-race_reach/08-cond_racefree.c index ce18620121..8d86e89cf5 100644 --- a/tests/regression/28-race_reach/08-cond_racefree.c +++ b/tests/regression/28-race_reach/08-cond_racefree.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/09-ptrmunge_racing.c b/tests/regression/28-race_reach/09-ptrmunge_racing.c index 3191ca3ead..eb6a098800 100644 --- a/tests/regression/28-race_reach/09-ptrmunge_racing.c +++ b/tests/regression/28-race_reach/09-ptrmunge_racing.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -27,4 +28,4 @@ int main(void) { create_threads(t1); create_threads(t2); join_threads(t1); join_threads(t2); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/10-ptrmunge_racefree.c b/tests/regression/28-race_reach/10-ptrmunge_racefree.c index d4e2144971..b21a1e9480 100644 --- a/tests/regression/28-race_reach/10-ptrmunge_racefree.c +++ b/tests/regression/28-race_reach/10-ptrmunge_racefree.c @@ -1,3 +1,4 @@ +//PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -27,4 +28,4 @@ int main(void) { create_threads(t1); create_threads(t2); join_threads(t1); join_threads(t2); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/11-ptr_racing.c b/tests/regression/28-race_reach/11-ptr_racing.c index dc3f3c1a21..d6851afa82 100644 --- a/tests/regression/28-race_reach/11-ptr_racing.c +++ b/tests/regression/28-race_reach/11-ptr_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -20,4 +21,4 @@ int main(void) { pthread_mutex_unlock(&mutex2); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/12-ptr_racefree.c b/tests/regression/28-race_reach/12-ptr_racefree.c index bb7bcffa3d..b22a942eda 100644 --- a/tests/regression/28-race_reach/12-ptr_racefree.c +++ b/tests/regression/28-race_reach/12-ptr_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -16,8 +17,8 @@ void *t_fun(void *arg) { int main(void) { create_threads(t); pthread_mutex_lock(&mutex1); - assert_racefree(global); + assert_racefree(global); pthread_mutex_unlock(&mutex1); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/19-callback_racing.c b/tests/regression/28-race_reach/19-callback_racing.c index 798d1e2783..04eaaeef4f 100644 --- a/tests/regression/28-race_reach/19-callback_racing.c +++ b/tests/regression/28-race_reach/19-callback_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp extern int __VERIFIER_nondet_int(); #include diff --git a/tests/regression/28-race_reach/20-callback_racefree.c b/tests/regression/28-race_reach/20-callback_racefree.c index 6f30ef492d..e41896f31a 100644 --- a/tests/regression/28-race_reach/20-callback_racefree.c +++ b/tests/regression/28-race_reach/20-callback_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp extern int __VERIFIER_nondet_int(); #include diff --git a/tests/regression/28-race_reach/21-deref_read_racing.c b/tests/regression/28-race_reach/21-deref_read_racing.c index 93166f8125..880a8a4d38 100644 --- a/tests/regression/28-race_reach/21-deref_read_racing.c +++ b/tests/regression/28-race_reach/21-deref_read_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/22-deref_read_racefree.c b/tests/regression/28-race_reach/22-deref_read_racefree.c index 2e4c5ebbb6..9ed4fb03cf 100644 --- a/tests/regression/28-race_reach/22-deref_read_racefree.c +++ b/tests/regression/28-race_reach/22-deref_read_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/23-sound_unlock_racing.c b/tests/regression/28-race_reach/23-sound_unlock_racing.c index da8db888db..c3ed280fbd 100644 --- a/tests/regression/28-race_reach/23-sound_unlock_racing.c +++ b/tests/regression/28-race_reach/23-sound_unlock_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/24-sound_lock_racing.c b/tests/regression/28-race_reach/24-sound_lock_racing.c index 89ed5103dc..597bea716c 100644 --- a/tests/regression/28-race_reach/24-sound_lock_racing.c +++ b/tests/regression/28-race_reach/24-sound_lock_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/27-funptr_racing.c b/tests/regression/28-race_reach/27-funptr_racing.c index 2c970deaf3..7210d0d56c 100644 --- a/tests/regression/28-race_reach/27-funptr_racing.c +++ b/tests/regression/28-race_reach/27-funptr_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include #include "racemacros.h" @@ -5,11 +6,11 @@ int global; pthread_mutex_t gm = PTHREAD_MUTEX_INITIALIZER; -void bad() { +void bad() { access(global); } -void good() { +void good() { pthread_mutex_lock(&gm); access(global); pthread_mutex_unlock(&gm); @@ -42,4 +43,4 @@ int main() { join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/28-funptr_racefree.c b/tests/regression/28-race_reach/28-funptr_racefree.c index 4e39156ecf..f36168aaaa 100644 --- a/tests/regression/28-race_reach/28-funptr_racefree.c +++ b/tests/regression/28-race_reach/28-funptr_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include #include "racemacros.h" @@ -5,10 +6,10 @@ int global = 0; pthread_mutex_t gm = PTHREAD_MUTEX_INITIALIZER; -void bad() { +void bad() { access(global); -} -void good() { +} +void good() { pthread_mutex_lock(&gm); access(global); pthread_mutex_unlock(&gm); @@ -41,4 +42,4 @@ int main() { join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/36-indirect_racefree.c b/tests/regression/28-race_reach/36-indirect_racefree.c index 97dd10fc85..a2733f9df3 100644 --- a/tests/regression/28-race_reach/36-indirect_racefree.c +++ b/tests/regression/28-race_reach/36-indirect_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/37-indirect_racing.c b/tests/regression/28-race_reach/37-indirect_racing.c index e769a24836..6bf5757991 100644 --- a/tests/regression/28-race_reach/37-indirect_racing.c +++ b/tests/regression/28-race_reach/37-indirect_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/40-trylock_racing.c b/tests/regression/28-race_reach/40-trylock_racing.c index 4d9c4acb98..94694bc1eb 100644 --- a/tests/regression/28-race_reach/40-trylock_racing.c +++ b/tests/regression/28-race_reach/40-trylock_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -25,4 +26,4 @@ int main(void) { pthread_mutex_unlock(&mutex); // no UB because ERRORCHECK join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/41-trylock_racefree.c b/tests/regression/28-race_reach/41-trylock_racefree.c index 0e521474c5..ce68d3abe2 100644 --- a/tests/regression/28-race_reach/41-trylock_racefree.c +++ b/tests/regression/28-race_reach/41-trylock_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -22,4 +23,4 @@ int main(void) { pthread_mutex_unlock(&mutex); join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/42-trylock2_racefree.c b/tests/regression/28-race_reach/42-trylock2_racefree.c index 5f50097355..8b73328281 100644 --- a/tests/regression/28-race_reach/42-trylock2_racefree.c +++ b/tests/regression/28-race_reach/42-trylock2_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" @@ -35,4 +36,4 @@ int main(void) { join_threads(t); return 0; -} \ No newline at end of file +} diff --git a/tests/regression/28-race_reach/45-escape_racing.c b/tests/regression/28-race_reach/45-escape_racing.c index a27db9a9df..31cb5fcacc 100644 --- a/tests/regression/28-race_reach/45-escape_racing.c +++ b/tests/regression/28-race_reach/45-escape_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/46-escape_racefree.c b/tests/regression/28-race_reach/46-escape_racefree.c index af4874534e..731a61483e 100644 --- a/tests/regression/28-race_reach/46-escape_racefree.c +++ b/tests/regression/28-race_reach/46-escape_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/51-mutexptr_racefree.c b/tests/regression/28-race_reach/51-mutexptr_racefree.c index 972cd6e667..c57b58eb61 100644 --- a/tests/regression/28-race_reach/51-mutexptr_racefree.c +++ b/tests/regression/28-race_reach/51-mutexptr_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/60-invariant_racefree.c b/tests/regression/28-race_reach/60-invariant_racefree.c index d396e349bc..b8b86a86ca 100644 --- a/tests/regression/28-race_reach/60-invariant_racefree.c +++ b/tests/regression/28-race_reach/60-invariant_racefree.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/61-invariant_racing.c b/tests/regression/28-race_reach/61-invariant_racing.c index 22277557f9..b61f34ba25 100644 --- a/tests/regression/28-race_reach/61-invariant_racing.c +++ b/tests/regression/28-race_reach/61-invariant_racing.c @@ -1,3 +1,4 @@ +// PARAM: --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/70-funloop_racefree.c b/tests/regression/28-race_reach/70-funloop_racefree.c index 11f44100cd..2ff0cdf9e5 100644 --- a/tests/regression/28-race_reach/70-funloop_racefree.c +++ b/tests/regression/28-race_reach/70-funloop_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/71-funloop_racing.c b/tests/regression/28-race_reach/71-funloop_racing.c index d34be23175..ac20711401 100644 --- a/tests/regression/28-race_reach/71-funloop_racing.c +++ b/tests/regression/28-race_reach/71-funloop_racing.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/72-funloop_hard_racing.c b/tests/regression/28-race_reach/72-funloop_hard_racing.c index d913bb16a6..78e24279f9 100644 --- a/tests/regression/28-race_reach/72-funloop_hard_racing.c +++ b/tests/regression/28-race_reach/72-funloop_hard_racing.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/73-funloop_hard_racefree.c b/tests/regression/28-race_reach/73-funloop_hard_racefree.c index 33571b8c4d..cc48865d24 100644 --- a/tests/regression/28-race_reach/73-funloop_hard_racefree.c +++ b/tests/regression/28-race_reach/73-funloop_hard_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/74-tricky_address1_racefree.c b/tests/regression/28-race_reach/74-tricky_address1_racefree.c index 0fdacd23c2..f9ce5d8b4d 100644 --- a/tests/regression/28-race_reach/74-tricky_address1_racefree.c +++ b/tests/regression/28-race_reach/74-tricky_address1_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/75-tricky_address2_racefree.c b/tests/regression/28-race_reach/75-tricky_address2_racefree.c index 76b3b3752a..162eb8d13a 100644 --- a/tests/regression/28-race_reach/75-tricky_address2_racefree.c +++ b/tests/regression/28-race_reach/75-tricky_address2_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/76-tricky_address3_racefree.c b/tests/regression/28-race_reach/76-tricky_address3_racefree.c index 1a782b670e..70c3d033b2 100644 --- a/tests/regression/28-race_reach/76-tricky_address3_racefree.c +++ b/tests/regression/28-race_reach/76-tricky_address3_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/77-tricky_address4_racing.c b/tests/regression/28-race_reach/77-tricky_address4_racing.c index 5b189aa221..5fea171553 100644 --- a/tests/regression/28-race_reach/77-tricky_address4_racing.c +++ b/tests/regression/28-race_reach/77-tricky_address4_racing.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/78-equ_racing.c b/tests/regression/28-race_reach/78-equ_racing.c index 32e10d5a02..b21d76b889 100644 --- a/tests/regression/28-race_reach/78-equ_racing.c +++ b/tests/regression/28-race_reach/78-equ_racing.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/79-equ_racefree.c b/tests/regression/28-race_reach/79-equ_racefree.c index ba9affb71f..5b8744c322 100644 --- a/tests/regression/28-race_reach/79-equ_racefree.c +++ b/tests/regression/28-race_reach/79-equ_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/81-list_racing.c b/tests/regression/28-race_reach/81-list_racing.c index c131e5c2a1..8b231f843c 100644 --- a/tests/regression/28-race_reach/81-list_racing.c +++ b/tests/regression/28-race_reach/81-list_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/82-list_racefree.c b/tests/regression/28-race_reach/82-list_racefree.c index 67470cf8e0..5bab3c5c31 100644 --- a/tests/regression/28-race_reach/82-list_racefree.c +++ b/tests/regression/28-race_reach/82-list_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/83-list2_racing1.c b/tests/regression/28-race_reach/83-list2_racing1.c index 6002bc73d4..f0d9f9744b 100644 --- a/tests/regression/28-race_reach/83-list2_racing1.c +++ b/tests/regression/28-race_reach/83-list2_racing1.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/84-list2_racing2.c b/tests/regression/28-race_reach/84-list2_racing2.c index d807e2d0ac..ce15b2ddf5 100644 --- a/tests/regression/28-race_reach/84-list2_racing2.c +++ b/tests/regression/28-race_reach/84-list2_racing2.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/85-list2_racefree.c b/tests/regression/28-race_reach/85-list2_racefree.c index b0fb1baa83..cef0e1cb08 100644 --- a/tests/regression/28-race_reach/85-list2_racefree.c +++ b/tests/regression/28-race_reach/85-list2_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/86-lists_racing.c b/tests/regression/28-race_reach/86-lists_racing.c index 0548dcab37..e90b699212 100644 --- a/tests/regression/28-race_reach/86-lists_racing.c +++ b/tests/regression/28-race_reach/86-lists_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/87-lists_racefree.c b/tests/regression/28-race_reach/87-lists_racefree.c index 0d05e5b2c2..8e51670b61 100644 --- a/tests/regression/28-race_reach/87-lists_racefree.c +++ b/tests/regression/28-race_reach/87-lists_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" +// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/90-arrayloop2_racing.c b/tests/regression/28-race_reach/90-arrayloop2_racing.c index 4859ed5a95..184d79af89 100644 --- a/tests/regression/28-race_reach/90-arrayloop2_racing.c +++ b/tests/regression/28-race_reach/90-arrayloop2_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true +// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/91-arrayloop2_racefree.c b/tests/regression/28-race_reach/91-arrayloop2_racefree.c index 30ffa83e78..4461e78459 100644 --- a/tests/regression/28-race_reach/91-arrayloop2_racefree.c +++ b/tests/regression/28-race_reach/91-arrayloop2_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true +// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/92-evilcollapse_racing.c b/tests/regression/28-race_reach/92-evilcollapse_racing.c index af5bae0830..a33eb630f5 100644 --- a/tests/regression/28-race_reach/92-evilcollapse_racing.c +++ b/tests/regression/28-race_reach/92-evilcollapse_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true +// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/93-evilcollapse_racefree.c b/tests/regression/28-race_reach/93-evilcollapse_racefree.c index e4ca831199..dee7d67659 100644 --- a/tests/regression/28-race_reach/93-evilcollapse_racefree.c +++ b/tests/regression/28-race_reach/93-evilcollapse_racefree.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true +// PARAM: --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --set ana.activated[+] "'region'" --set exp.region-offsets true --set lib.activated[+] sv-comp #include #include #include "racemacros.h" diff --git a/tests/regression/28-race_reach/94-alloc_region_racing.c b/tests/regression/28-race_reach/94-alloc_region_racing.c index 74333bcab4..f985a9d91e 100644 --- a/tests/regression/28-race_reach/94-alloc_region_racing.c +++ b/tests/regression/28-race_reach/94-alloc_region_racing.c @@ -1,4 +1,4 @@ -// PARAM: --set ana.activated[+] "'region'" --set exp.region-offsets true +// PARAM: --set ana.activated[+] "'region'" --set exp.region-offsets true --set lib.activated[+] sv-comp #include #include #include From c53f193557855bcc5d135640b0faf7e742eb2a71 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 1 Oct 2023 17:21:22 +0200 Subject: [PATCH 42/50] 36/15 activate sv-comp libraries --- tests/regression/36-apron/15-globals-st.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/36-apron/15-globals-st.c b/tests/regression/36-apron/15-globals-st.c index 692d66f299..4c167ad742 100644 --- a/tests/regression/36-apron/15-globals-st.c +++ b/tests/regression/36-apron/15-globals-st.c @@ -1,4 +1,4 @@ -// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --disable ana.int.interval +// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --disable ana.int.interval --set lib.activated[+] sv-comp extern int __VERIFIER_nondet_int(); #include From 8f1bd75c307bb7a426c2d6447cf278e89f80a20d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 3 Oct 2023 12:37:46 +0200 Subject: [PATCH 43/50] Comment on `Sem*` specials that they are unused --- src/analyses/libraryDesc.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 06a9b7e55b..c93e56f4d0 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -57,6 +57,7 @@ type special = | Broadcast of Cil.exp | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; } | MutexInit of { mutex:Cil.exp; attr: Cil.exp; } + (* All Sem specials are not used yet-*) | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; } | SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;} | SemPost of Cil.exp From 0e77bc21c2b398ecebffc658d79a5302e92f02a6 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 3 Oct 2023 12:39:16 +0200 Subject: [PATCH 44/50] Move `str[n]casecmp` to Posix group --- src/analyses/libraryFunctions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index e0e8a20707..c94e90216e 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -69,8 +69,6 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strchr", unknown [drop "s" [r]; drop "c" []]); ("__builtin_strchr", unknown [drop "s" [r]; drop "c" []]); ("strrchr", unknown [drop "s" [r]; drop "c" []]); - ("strcasecmp", unknown [drop "s1" [r]; drop "s2" [r]]); - ("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); ("calloc", special [__ "n" []; __ "size" []] @@ fun n size -> Calloc {count = n; size}); ("realloc", special [__ "ptr" [r; f]; __ "size" []] @@ fun ptr size -> Realloc { ptr; size }); @@ -367,6 +365,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("dlclose", unknown [drop "handle" [r]]); ("inet_addr", unknown [drop "cp" [r]]); ("uname", unknown [drop "buf" [w]]); + ("strcasecmp", unknown [drop "s1" [r]; drop "s2" [r]]); + ("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); ] (** Pthread functions. *) From 960b0239b28a112619e1037586ac3c3cb74c45ef Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 3 Oct 2023 12:40:50 +0200 Subject: [PATCH 45/50] Punctuation --- src/analyses/libraryDesc.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index c93e56f4d0..7862b2d6bd 100644 --- a/src/analyses/libraryDesc.ml +++ b/src/analyses/libraryDesc.ml @@ -57,7 +57,7 @@ type special = | Broadcast of Cil.exp | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; } | MutexInit of { mutex:Cil.exp; attr: Cil.exp; } - (* All Sem specials are not used yet-*) + (* All Sem specials are not used yet. *) | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; } | SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;} | SemPost of Cil.exp From d855613e895f56ca2ccc1638b8c06a8736eac82c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 3 Oct 2023 12:42:47 +0200 Subject: [PATCH 46/50] Apply suggestions from code review Co-authored-by: Karoliine Holter <44437975+karoliineh@users.noreply.github.com> Co-authored-by: Simmo Saan --- src/analyses/libraryFunctions.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index c94e90216e..f8b8b6cd89 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -217,7 +217,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fileno", unknown [drop "stream" [r_deep; w_deep]]); ("fdopen", unknown [drop "fd" []; drop "mode" [r]]); ("getopt", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r_deep]; drop "optstring" [r]]); - ("getopt_long", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r_deep]; drop "optstring" [r]; drop "longopts" [r]; drop "longindex" [w]]); + ("getopt_long", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r_deep]; drop "optstring" [r_deep]; drop "longopts" [r]; drop "longindex" [w]]); ("iconv_open", unknown [drop "tocode" [r]; drop "fromcode" [r]]); ("iconv", unknown [drop "cd" [r]; drop "inbuf" [r]; drop "inbytesleft" [r;w]; drop "outbuf" [w]; drop "outbytesleft" [r;w]]); ("iconv_close", unknown [drop "cd" [f]]); @@ -245,13 +245,13 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("inet_ntoa", unknown ~attrs:[ThreadUnsafe] [drop "in" []]); ("getsockopt", unknown [drop "sockfd" []; drop "level" []; drop "optname" []; drop "optval" [w]; drop "optlen" [w]]); ("setsockopt", unknown [drop "sockfd" []; drop "level" []; drop "optname" []; drop "optval" [r]; drop "optlen" []]); - ("getsockname", unknown [drop "sockfd" [r]; drop "addr" [w]; drop "addrlen" [r]]); + ("getsockname", unknown [drop "sockfd" []; drop "addr" [w_deep]; drop "addrlen" [w]]); ("gethostbyaddr", unknown ~attrs:[ThreadUnsafe] [drop "addr" [r_deep]; drop "len" []; drop "type" []]); ("gethostbyaddr_r", unknown [drop "addr" [r_deep]; drop "len" []; drop "type" []; drop "ret" [w_deep]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); ("gethostbyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); - ("gethostbyname_r", unknown [drop "name" [r]; drop "result_buf" [w]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); + ("gethostbyname_r", unknown [drop "name" [r]; drop "result_buf" [w_deep]; drop "buf" [w]; drop "buflen" []; drop "result" [w]; drop "h_errnop" [w]]); ("gethostname", unknown [drop "name" [w]; drop "len" []]); - ("getpeername", unknown [drop "sockfd" []; drop "addr" [w]; drop "addrlen" [r]]); + ("getpeername", unknown [drop "sockfd" []; drop "addr" [w_deep]; drop "addrlen" [r; w]]); ("socket", unknown [drop "domain" []; drop "type" []; drop "protocol" []]); ("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); ("tcgetattr", unknown [drop "fd" []; drop "termios_p" [w_deep]]); @@ -325,7 +325,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("ffs", unknown [drop "i" []]); ("_exit", special [drop "status" []] Abort); ("execvp", unknown [drop "file" [r]; drop "argv" [r_deep]]); - ("execl", unknown (drop "path" [r] :: VarArgs (drop' [r]))); + ("execl", unknown (drop "path" [r] :: drop "arg" [r] :: VarArgs (drop' [r]))); ("statvfs", unknown [drop "path" [r]; drop "buf" [w]]); ("readlink", unknown [drop "path" [r]; drop "buf" [w]; drop "bufsz" []]); ("wcswidth", unknown [drop "s" [r]; drop "n" []]); @@ -354,8 +354,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("isatty", unknown [drop "fd" []]); ("sigemptyset", unknown [drop "set" [w]]); ("sigfillset", unknown [drop "set" [w]]); - ("sigaddset", unknown [drop "set" [w]; drop "signum" []]); - ("sigdelset", unknown [drop "set" [w]; drop "signum" []]); + ("sigaddset", unknown [drop "set" [r; w]; drop "signum" []]); + ("sigdelset", unknown [drop "set" [r; w]; drop "signum" []]); ("sigismember", unknown [drop "set" [r]; drop "signum" []]); ("sigprocmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]); ("fork", unknown []); @@ -364,7 +364,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("dlsym", unknown [drop "handle" [r]; drop "symbol" [r]]); ("dlclose", unknown [drop "handle" [r]]); ("inet_addr", unknown [drop "cp" [r]]); - ("uname", unknown [drop "buf" [w]]); + ("uname", unknown [drop "buf" [w_deep]]); ("strcasecmp", unknown [drop "s1" [r]; drop "s2" [r]]); ("strncasecmp", unknown [drop "s1" [r]; drop "s2" [r]; drop "n" []]); ] From 79d71b881b4eb83f973d77cf94a5f8ff326e209c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 3 Oct 2023 12:45:46 +0200 Subject: [PATCH 47/50] Do not record accesses to `sem` --- src/analyses/libraryFunctions.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index f8b8b6cd89..15343a4149 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -435,12 +435,13 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_attr_setschedparam", unknown [drop "attr" [r; w]; drop "param" [r]]); ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]); ("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]); - ("sem_init", special [__ "sem" [r]; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value}); - ("sem_wait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = false; timeout = None}); - ("sem_trywait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = true; timeout = None}); - ("sem_timedwait", special [__ "sem" [r]; __ "abs_timeout" [r]] @@ fun sem abs_timeout-> SemWait {sem; try_ = true; timeout = Some abs_timeout}); (* no write accesses to sem because sync primitive itself has no race *) - ("sem_post", special [__ "sem" [r]] @@ fun sem -> SemPost sem); - ("sem_destroy", special [__ "sem" [r]] @@ fun sem -> SemDestroy sem); + (* Not recording read accesses to sem as these are thread-safe anyway not to clutter messages (as for mutexes) **) + ("sem_init", special [__ "sem" []; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value}); + ("sem_wait", special [__ "sem" []] @@ fun sem -> SemWait {sem; try_ = false; timeout = None}); + ("sem_trywait", special [__ "sem" []] @@ fun sem -> SemWait {sem; try_ = true; timeout = None}); + ("sem_timedwait", special [__ "sem" []; __ "abs_timeout" [r]] @@ fun sem abs_timeout-> SemWait {sem; try_ = true; timeout = Some abs_timeout}); (* no write accesses to sem because sync primitive itself has no race *) + ("sem_post", special [__ "sem" []] @@ fun sem -> SemPost sem); + ("sem_destroy", special [__ "sem" []] @@ fun sem -> SemDestroy sem); ] (** GCC builtin functions. From 8cdd6da6da323684ad2590f9485db342dc536da4 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 3 Oct 2023 12:46:59 +0200 Subject: [PATCH 48/50] Move `getdtablesize` to `glibc` --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 15343a4149..09acd4d678 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -545,6 +545,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("freeifaddrs", unknown [drop "ifa" [f_deep]]); ("atoq", unknown [drop "nptr" [r]]); ("strchrnul", unknown [drop "s" [r]; drop "c" []]); + ("getdtablesize", unknown []); ] let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -567,7 +568,6 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fts_open", unknown [drop "path_argv" [r_deep]; drop "options" []; drop "compar" [s]]); (* TODO: use Call instead of Spawn *) ("fts_read", unknown [drop "ftsp" [r_deep; w_deep]]); ("fts_close", unknown [drop "ftsp" [f_deep]]); - ("getdtablesize", unknown []); ] let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType))) From 820312cee8c891c72b6a692956413c427f2b17e7 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 3 Oct 2023 12:48:19 +0200 Subject: [PATCH 49/50] Add `sema_init` back --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 09acd4d678..e125c3bba3 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -1176,6 +1176,7 @@ let invalidate_actions = [ "idr_pre_get", readsAll; "zil_replay", writes [1;2;3;5]; (* ddverify *) + "sema_init", readsAll; "__goblint_assume_join", readsAll; ] From da997a3a21b298bbcbfd3023fd68b7d626522829 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 3 Oct 2023 13:12:01 +0200 Subject: [PATCH 50/50] Remove TODO --- src/analyses/libraryFunctions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index e125c3bba3..59f63e04c0 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -360,7 +360,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sigprocmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]); ("fork", unknown []); ("dlopen", unknown [drop "filename" [r]; drop "flag" []]); - ("dlerror", unknown ~attrs:[ThreadUnsafe] []); (* TODO: Why thread-unsafe? https://linux.die.net/man/3/dlopen *) + ("dlerror", unknown ~attrs:[ThreadUnsafe] []); ("dlsym", unknown [drop "handle" [r]; drop "symbol" [r]]); ("dlclose", unknown [drop "handle" [r]]); ("inet_addr", unknown [drop "cp" [r]]);