From d5584ba06c517ec4fe2704398ae373c941032e4b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 8 Nov 2023 11:11:58 +0100 Subject: [PATCH 01/10] Add `__VERIFIER_nondet_size_t` --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index f84fe1d4e3..7c376fe426 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -972,6 +972,7 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__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 *) + ("__VERIFIER_nondet_size_t ", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *) ] let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ From 9a06289988dc949f3b49a672678d0f059b966490 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 8 Nov 2023 11:15:49 +0100 Subject: [PATCH 02/10] Add `__builtin_memcmp` --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 7c376fe426..448b621fe4 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" []]); + ("__builtin_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]]); From 67c8d9b395e8a263f1b8a0461602d66921ddb0c4 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 8 Nov 2023 11:17:10 +0100 Subject: [PATCH 03/10] Add `__builtin_strlen` --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 448b621fe4..c3726f6d95 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -63,6 +63,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("localeconv", unknown ~attrs:[ThreadUnsafe] []); ("localtime", unknown ~attrs:[ThreadUnsafe] [drop "time" [r]]); ("strlen", special [__ "s" [r]] @@ fun s -> Strlen s); + ("__builtin_strlen", special [__ "s" [r]] @@ fun s -> Strlen s); ("strstr", special [__ "haystack" [r]; __ "needle" [r]] @@ fun haystack needle -> Strstr { haystack; needle; }); ("strcmp", special [__ "s1" [r]; __ "s2" [r]] @@ fun s1 s2 -> Strcmp { s1; s2; n = None; }); ("strtok", unknown ~attrs:[ThreadUnsafe] [drop "str" [r; w]; drop "delim" [r]]); From 24aca6767df3e2f0cf4296009d761ae56749231e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 8 Nov 2023 11:42:31 +0100 Subject: [PATCH 04/10] Add `__fread_unlocked_*` --- src/analyses/libraryFunctions.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index c3726f6d95..75392c2243 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -52,6 +52,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("putc", unknown [drop "ch" []; drop "stream" [r_deep; w_deep]]); ("fputs", unknown [drop "str" [r]; drop "stream" [r_deep; w_deep]]); ("fread", unknown [drop "buffer" [w]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); + ("fread_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "buffer" [w]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); ("fseek", unknown [drop "stream" [r_deep; w_deep]; drop "offset" []; drop "origin" []]); ("ftell", unknown [drop "stream" [r_deep]]); ("fwrite", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); @@ -578,6 +579,9 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__fgets_chk", unknown [drop "__s" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); ("__fread_alias", unknown [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); ("__fread_chk", unknown [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("__fread_unlocked_alias", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("__fread_unlocked_chk", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("__fread_unlocked_chk_warn", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); ("__read_chk", unknown [drop "__fd" []; drop "__buf" [w]; drop "__nbytes" []; drop "__buflen" []]); ("__read_alias", unknown [drop "__fd" []; drop "__buf" [w]; drop "__nbytes" []]); ("__readlink_chk", unknown [drop "path" [r]; drop "buf" [w]; drop "len" []; drop "buflen" []]); From 8972bd853f3bb5b11b1c659147a34b6697d7e2cf Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 8 Nov 2023 12:41:12 +0100 Subject: [PATCH 05/10] Fix typo Co-authored-by: Simmo Saan --- 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 75392c2243..93c1cbaabe 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -978,7 +978,7 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__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 *) - ("__VERIFIER_nondet_size_t ", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *) + ("__VERIFIER_nondet_size_t", unknown []); (* cannot give it in sv-comp.c without including stdlib or similar *) ] let ncurses_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ From b3ef0621077e46441516f91b73cd9f23ce56492e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 8 Nov 2023 14:01:25 +0100 Subject: [PATCH 06/10] _Exit / _exit --- src/analyses/libraryFunctions.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 93c1cbaabe..c71c7a7f7e 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -149,6 +149,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("atomic_flag_test_and_set_explicit", unknown [drop "obj" [r; w]; drop "order" []]); ("atomic_load", unknown [drop "obj" [r]]); ("atomic_store", unknown [drop "obj" [w]; drop "desired" []]); + ("_Exit", special [drop "status" []] @@ Abort); + ("_exit", special [drop "status" []] @@ Abort); ] (** C POSIX library functions. From 2fc622067b2a7a2754f6d67a4990ed4b05008d32 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 8 Nov 2023 14:12:18 +0100 Subject: [PATCH 07/10] `__assert` --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index c71c7a7f7e..eeddfbb218 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -510,6 +510,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_unreachable", special' [] @@ fun () -> if get_bool "sem.builtin_unreachable.dead_code" then Abort else Unknown); (* https://github.com/sosy-lab/sv-benchmarks/issues/1296 *) ("__assert_rtn", special [drop "func" [r]; drop "file" [r]; drop "line" []; drop "exp" [r]] @@ Abort); (* MacOS's built-in assert *) ("__assert_fail", special [drop "assertion" [r]; drop "file" [r]; drop "line" []; drop "function" [r]] @@ Abort); (* gcc's built-in assert *) + ("__assert", special [drop "assertion" [r]; drop "file" [r]; drop "line" []] @@ Abort); (* header says: The following is not at all used here but needed for standard compliance. *) ("__builtin_return_address", unknown [drop "level" []]); ("__builtin___sprintf_chk", unknown (drop "s" [w] :: drop "flag" [] :: drop "os" [] :: drop "fmt" [r] :: VarArgs (drop' [r]))); ("__builtin_add_overflow", unknown [drop "a" []; drop "b" []; drop "c" [w]]); From c4353f9f2c46e1f9b6b6d0e9d3d7168ccdc8a577 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 8 Nov 2023 14:15:02 +0100 Subject: [PATCH 08/10] Move `_exit` to C, as C usually takes precedence over posix for us --- src/analyses/libraryFunctions.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index eeddfbb218..7774e37ee2 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -340,7 +340,6 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("regexec", unknown [drop "preg" [r_deep]; drop "string" [r]; drop "nmatch" []; drop "pmatch" [w_deep]; drop "eflags" []]); ("regfree", unknown [drop "preg" [f_deep]]); ("ffs", unknown [drop "i" []]); - ("_exit", special [drop "status" []] Abort); ("execvp", unknown [drop "file" [r]; drop "argv" [r_deep]]); ("execl", unknown (drop "path" [r] :: drop "arg" [r] :: VarArgs (drop' [r]))); ("statvfs", unknown [drop "path" [r]; drop "buf" [w]]); From dd3de9e01ef9bce8d04369c7e698f973f25d00ea Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 9 Nov 2023 10:16:11 +0100 Subject: [PATCH 09/10] Move `_exit` back --- 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 7774e37ee2..df3217e380 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -150,7 +150,6 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("atomic_load", unknown [drop "obj" [r]]); ("atomic_store", unknown [drop "obj" [w]; drop "desired" []]); ("_Exit", special [drop "status" []] @@ Abort); - ("_exit", special [drop "status" []] @@ Abort); ] (** C POSIX library functions. @@ -340,6 +339,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("regexec", unknown [drop "preg" [r_deep]; drop "string" [r]; drop "nmatch" []; drop "pmatch" [w_deep]; drop "eflags" []]); ("regfree", unknown [drop "preg" [f_deep]]); ("ffs", unknown [drop "i" []]); + ("_exit", special [drop "status" []] @@ Abort); ("execvp", unknown [drop "file" [r]; drop "argv" [r_deep]]); ("execl", unknown (drop "path" [r] :: drop "arg" [r] :: VarArgs (drop' [r]))); ("statvfs", unknown [drop "path" [r]; drop "buf" [w]]); From 39a942752434625e0044f59158484d203752fb58 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 9 Nov 2023 10:18:15 +0100 Subject: [PATCH 10/10] Move `fread_unlocked` 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 df3217e380..117dcbd236 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -52,7 +52,6 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("putc", unknown [drop "ch" []; drop "stream" [r_deep; w_deep]]); ("fputs", unknown [drop "str" [r]; drop "stream" [r_deep; w_deep]]); ("fread", unknown [drop "buffer" [w]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); - ("fread_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "buffer" [w]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); ("fseek", unknown [drop "stream" [r_deep; w_deep]; drop "offset" []; drop "origin" []]); ("ftell", unknown [drop "stream" [r_deep]]); ("fwrite", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); @@ -581,6 +580,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__fgets_chk", unknown [drop "__s" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); ("__fread_alias", unknown [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); ("__fread_chk", unknown [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("fread_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "buffer" [w]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); ("__fread_unlocked_alias", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); ("__fread_unlocked_chk", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); ("__fread_unlocked_chk_warn", unknown ~attrs:[ThreadUnsafe] [drop "__ptr" [w]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]);