From 7e6a27b76671c8981a1889f2aa58cd9736906a66 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 10:46:54 +0100 Subject: [PATCH 01/13] Add `__builtin_popcount{,l,ll}` --- src/analyses/libraryFunctions.ml | 3 +++ tests/regression/41-stdlib/04-more.c | 14 ++++++++++++++ 2 files changed, 17 insertions(+) create mode 100644 tests/regression/41-stdlib/04-more.c diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 103753fac9..11ab345a8e 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -111,6 +111,9 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_add_overflow_p", unknown [drop "a" []; drop "b" []; drop "c" []]); ("__builtin_sub_overflow_p", unknown [drop "a" []; drop "b" []; drop "c" []]); ("__builtin_mul_overflow_p", unknown [drop "a" []; drop "b" []; drop "c" []]); + ("__builtin_popcount", unknown [drop "x" []]); + ("__builtin_popcountl", unknown [drop "x" []]); + ("__builtin_popcountll", unknown [drop "x" []]); ] let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ diff --git a/tests/regression/41-stdlib/04-more.c b/tests/regression/41-stdlib/04-more.c new file mode 100644 index 0000000000..8ab39fc404 --- /dev/null +++ b/tests/regression/41-stdlib/04-more.c @@ -0,0 +1,14 @@ +// PARAM: --set pre.cppflags[+] -DGOBLINT_NO_QSORT +#include + +int g = 8; + +int main() { + + int r = __builtin_popcount(5u); + int r = __builtin_popcountl(5ul); + int r = __builtin_popcountll(5ul); + + // Should not be invalidated + __goblint_check(g == 8); +} From b47b985789e0c812f0e73b1d0ea438d3dcbcfef8 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 10:58:56 +0100 Subject: [PATCH 02/13] Add `__bad_*` --- src/analyses/libraryFunctions.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 11ab345a8e..9632791abe 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -131,6 +131,12 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__overflow", unknown [drop "f" [r]; drop "ch" []]); ("__ctype_get_mb_cur_max", unknown []); ("__xmknod", unknown [drop "ver" []; drop "path" [r]; drop "mode" []; drop "dev" [r; w]]); + ("__bad_percpu_size", special' [] @@ fun () -> Abort); (* these do not have defintions so the linker will fail if they are actually called *) + ("__bad_size_call_parameter", special' [] @@ fun () -> Abort); + ("__xchg_wrong_size", special' [] @@ fun () -> Abort); + ("__cmpxchg_wrong_size", special' [] @@ fun () -> Abort); + ("__xadd_wrong_size", special' [] @@ fun () -> Abort); + ("__put_user_bad", special' [] @@ fun () -> Abort); ] let big_kernel_lock = AddrOf (Cil.var (Goblintutil.create_var (makeGlobalVar "[big kernel lock]" intType))) From a19d2dd9236efe8c5bedba756df609441d67a759 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 11:13:07 +0100 Subject: [PATCH 03/13] Add `pthread_attr_destroy` --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 9632791abe..94e02464c1 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -75,6 +75,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_cond_broadcast", special [__ "cond" []] @@ fun cond -> Broadcast cond); ("pthread_cond_wait", special [__ "cond" []; __ "mutex" []] @@ fun cond mutex -> Wait {cond; mutex}); ("pthread_cond_timedwait", special [__ "cond" []; __ "mutex" []; __ "abstime" [r]] @@ fun cond mutex abstime -> TimedWait {cond; mutex; abstime}); + ("pthread_attr_destroy", unknown [drop "attr" [f]]) ] (** GCC builtin functions. From a1bd0cfa2e63df36e845dc3c4d3b1a4b627b0474 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 11:16:13 +0100 Subject: [PATCH 04/13] Add `puts` --- src/analyses/libraryFunctions.ml | 1 + tests/regression/41-stdlib/04-more.c | 1 + 2 files changed, 2 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 94e02464c1..e13475c89d 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -29,6 +29,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("iswalnum", unknown [drop "wc" []]); ("iswprint", unknown [drop "wc" []]); ("rename" , unknown [drop "oldpath" [r]; drop "newpath" [r];]); + ("puts", unknown [drop "s" [r]]); ] (** C POSIX library functions. diff --git a/tests/regression/41-stdlib/04-more.c b/tests/regression/41-stdlib/04-more.c index 8ab39fc404..8c8d86e1c4 100644 --- a/tests/regression/41-stdlib/04-more.c +++ b/tests/regression/41-stdlib/04-more.c @@ -8,6 +8,7 @@ int main() { int r = __builtin_popcount(5u); int r = __builtin_popcountl(5ul); int r = __builtin_popcountll(5ul); + puts("blarg"); // Should not be invalidated __goblint_check(g == 8); From 8e8ed76757737021cba353250d985a2779cfefac Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 11:21:50 +0100 Subject: [PATCH 05/13] Add `str[c]spn` --- src/analyses/libraryFunctions.ml | 2 ++ tests/regression/41-stdlib/04-more.c | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index e13475c89d..6756c95312 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -30,6 +30,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("iswprint", unknown [drop "wc" []]); ("rename" , unknown [drop "oldpath" [r]; drop "newpath" [r];]); ("puts", unknown [drop "s" [r]]); + ("strspn", unknown [drop "s" [r]; drop "accept" [r]]); + ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]); ] (** C POSIX library functions. diff --git a/tests/regression/41-stdlib/04-more.c b/tests/regression/41-stdlib/04-more.c index 8c8d86e1c4..e96398e567 100644 --- a/tests/regression/41-stdlib/04-more.c +++ b/tests/regression/41-stdlib/04-more.c @@ -10,6 +10,9 @@ int main() { int r = __builtin_popcountll(5ul); puts("blarg"); + int a = strspn("bla","blu"); + a = strcspn("bla","blu"); + // Should not be invalidated __goblint_check(g == 8); } From ddc0a66d9453bcd0ab5a067981150d3ff5befe44 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 11:30:23 +0100 Subject: [PATCH 06/13] Add various `strto...` --- src/analyses/libraryFunctions.ml | 6 +++++- tests/regression/41-stdlib/04-more.c | 2 ++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 6756c95312..eb206960b4 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -32,6 +32,11 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("puts", unknown [drop "s" [r]]); ("strspn", unknown [drop "s" [r]; drop "accept" [r]]); ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]); + ("strtod", unknown [drop "nptr" [r]; drop "endptr" [w_deep]]); + ("strtol", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); + ("strtoll", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); + ("strtoul", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); + ("strtoull", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); ] (** C POSIX library functions. @@ -547,7 +552,6 @@ let invalidate_actions = [ "getopt_long", writesAllButFirst 2 readsAll;(*drop 2*) "__strdup", readsAll;(*safe*) "strtoul__extinline", readsAll;(*safe*) - "strtol", writes [2]; "geteuid", readsAll;(*safe*) "opendir", readsAll; (*safe*) "readdir_r", writesAll;(*unsafe*) diff --git a/tests/regression/41-stdlib/04-more.c b/tests/regression/41-stdlib/04-more.c index e96398e567..ad27ea1d7b 100644 --- a/tests/regression/41-stdlib/04-more.c +++ b/tests/regression/41-stdlib/04-more.c @@ -13,6 +13,8 @@ int main() { int a = strspn("bla","blu"); a = strcspn("bla","blu"); + long r = strtol("bla", 0, 8); + // Should not be invalidated __goblint_check(g == 8); } From 8227170c8072eb7c88d28f6bb2d56b67ffcfc959 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 11:35:37 +0100 Subject: [PATCH 07/13] Add time related library functions --- src/analyses/libraryFunctions.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index eb206960b4..31ccf90c66 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -37,6 +37,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strtoll", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); ("strtoul", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); ("strtoull", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); + ("mktime", unknown [drop "tm" [r;w]]); + ("ctime", unknown [drop "rm" [r]]) ] (** C POSIX library functions. From 91000d4e30ac0dffaf371a03660d5379e7995d2b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 11:37:23 +0100 Subject: [PATCH 08/13] Add `clearerr` --- 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 31ccf90c66..6401f533cd 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -38,7 +38,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strtoul", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); ("strtoull", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); ("mktime", unknown [drop "tm" [r;w]]); - ("ctime", unknown [drop "rm" [r]]) + ("ctime", unknown [drop "rm" [r]]); + ("clearerr", unknown [drop "stream" [w]]); ] (** C POSIX library functions. From ed2b3ea601951386a5ee93a9421508e4c240c6aa Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 11:38:54 +0100 Subject: [PATCH 09/13] Add `setbuf` --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 6401f533cd..dd1fed9bc9 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -40,6 +40,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("mktime", unknown [drop "tm" [r;w]]); ("ctime", unknown [drop "rm" [r]]); ("clearerr", unknown [drop "stream" [w]]); + ("setbuf", unknown [drop "stream" [w]; drop "buf" [w]]); ] (** C POSIX library functions. From 046e15399a0243a802ad069605098432b743a8b7 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 11:40:03 +0100 Subject: [PATCH 10/13] Add `ntohs` --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index dd1fed9bc9..7d644f058f 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -77,6 +77,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("symlink" , unknown [drop "oldpath" [r]; drop "newpath" [r];]); ("ftruncate", unknown [drop "fd" []; drop "length" []]); ("mkfifo", unknown [drop "pathname" [r]; drop "mode" []]); + ("ntohs", unknown [drop "netshort" []]); ] (** Pthread functions. *) From 9d3566a8671474851bc319903581b1af1eb20bff Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 1 Nov 2022 11:43:28 +0100 Subject: [PATCH 11/13] Add `swprintf` --- src/analyses/libraryFunctions.ml | 1 + tests/regression/41-stdlib/04-more.c | 8 ++++++++ 2 files changed, 9 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 7d644f058f..6f05caf527 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -41,6 +41,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("ctime", unknown [drop "rm" [r]]); ("clearerr", unknown [drop "stream" [w]]); ("setbuf", unknown [drop "stream" [w]; drop "buf" [w]]); + ("swprintf", unknown (drop "wcs" [w] :: drop "maxlen" [] :: drop "fmt" [r] :: VarArgs (drop' []))); ] (** C POSIX library functions. diff --git a/tests/regression/41-stdlib/04-more.c b/tests/regression/41-stdlib/04-more.c index ad27ea1d7b..019eb84110 100644 --- a/tests/regression/41-stdlib/04-more.c +++ b/tests/regression/41-stdlib/04-more.c @@ -1,5 +1,7 @@ // PARAM: --set pre.cppflags[+] -DGOBLINT_NO_QSORT #include +#include +#include int g = 8; @@ -15,6 +17,12 @@ int main() { long r = strtol("bla", 0, 8); + wchar_t wcsbuf[100]; + wchar_t wstring[] = L"ABCDE"; + int num; + + num = swprintf(wcsbuf, 100, L"%s", "xyz"); + // Should not be invalidated __goblint_check(g == 8); } From 31be10fb70362ad07d2836852822058e6d8da056 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 2 Nov 2022 10:32:31 +0100 Subject: [PATCH 12/13] Remove `wdeep` from strto.... --- src/analyses/libraryFunctions.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 6f05caf527..9ddbe2decb 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -32,11 +32,11 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("puts", unknown [drop "s" [r]]); ("strspn", unknown [drop "s" [r]; drop "accept" [r]]); ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]); - ("strtod", unknown [drop "nptr" [r]; drop "endptr" [w_deep]]); - ("strtol", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); - ("strtoll", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); - ("strtoul", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); - ("strtoull", unknown [drop "nptr" [r]; drop "endptr" [w_deep]; drop "base" []]); + ("strtod", unknown [drop "nptr" [r]; drop "endptr" [w]]); + ("strtol", unknown [drop "nptr" [r]; drop "endptr" [w]; drop "base" []]); + ("strtoll", unknown [drop "nptr" [r]; drop "endptr" [w]; drop "base" []]); + ("strtoul", unknown [drop "nptr" [r]; drop "endptr" [w]; drop "base" []]); + ("strtoull", unknown [drop "nptr" [r]; drop "endptr" [w]; drop "base" []]); ("mktime", unknown [drop "tm" [r;w]]); ("ctime", unknown [drop "rm" [r]]); ("clearerr", unknown [drop "stream" [w]]); From 442d8cd7b3073a51e2494c7bffbef046a2bdf046 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 2 Nov 2022 10:35:22 +0100 Subject: [PATCH 13/13] Move `__bad_*` to `linux_desc_list` --- src/analyses/libraryFunctions.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 9ddbe2decb..f789a75a42 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -146,12 +146,6 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__overflow", unknown [drop "f" [r]; drop "ch" []]); ("__ctype_get_mb_cur_max", unknown []); ("__xmknod", unknown [drop "ver" []; drop "path" [r]; drop "mode" []; drop "dev" [r; w]]); - ("__bad_percpu_size", special' [] @@ fun () -> Abort); (* these do not have defintions so the linker will fail if they are actually called *) - ("__bad_size_call_parameter", special' [] @@ fun () -> Abort); - ("__xchg_wrong_size", special' [] @@ fun () -> Abort); - ("__cmpxchg_wrong_size", special' [] @@ fun () -> Abort); - ("__xadd_wrong_size", special' [] @@ fun () -> Abort); - ("__put_user_bad", special' [] @@ fun () -> Abort); ] let big_kernel_lock = AddrOf (Cil.var (Goblintutil.create_var (makeGlobalVar "[big kernel lock]" intType))) @@ -169,6 +163,12 @@ let linux_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("acquire_console_sem", special [] @@ Lock { lock = console_sem; try_ = false; write = true; return_on_success = true }); ("release_console_sem", special [] @@ Unlock console_sem); ("misc_deregister", unknown [drop "misc" [r_deep]]); + ("__bad_percpu_size", special [] Abort); (* these do not have definitions so the linker will fail if they are actually called *) + ("__bad_size_call_parameter", special [] Abort); + ("__xchg_wrong_size", special [] Abort); + ("__cmpxchg_wrong_size", special [] Abort); + ("__xadd_wrong_size", special [] Abort); + ("__put_user_bad", special [] Abort); ] (** Goblint functions. *)