From 4fa70bd813e40e6621e252e4adfdf0b77cedb8c5 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Wed, 22 Nov 2023 13:11:06 +0200 Subject: [PATCH 1/4] Add missing fun defs from sv-benchmarks #1239 --- src/analyses/libraryFunctions.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 12eda8f728..1a032c84b3 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -37,7 +37,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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]]); + ("feof_unlocked", unknown [drop "stream" [r_deep; w_deep]]); ("ferror", unknown [drop "stream" [r_deep; w_deep]]); + ("ferror_unlocked", unknown [drop "stream" [r_deep; w_deep]]); ("fflush", unknown [drop "stream" [r_deep; w_deep]]); ("fgetc", unknown [drop "stream" [r_deep; w_deep]]); ("getc", unknown [drop "stream" [r_deep; w_deep]]); @@ -52,9 +54,11 @@ 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_chk_warn", unknown [drop "buffer" [w]; drop "os" []; 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]]); + ("fwrite_unlocked", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); ("rewind", unknown [drop "stream" [r_deep; w_deep]]); ("setvbuf", unknown [drop "stream" [r_deep; w_deep]; drop "buffer" [r; w]; drop "mode" []; drop "size" []]); (* TODO: if this is used to set an input buffer, the buffer (second argument) would need to remain TOP, *) @@ -119,6 +123,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("mktime", unknown [drop "tm" [r;w]]); ("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]); ("clearerr", unknown [drop "stream" [w]]); + ("clearerr_unlocked", unknown [drop "stream" [w]]); ("setbuf", unknown [drop "stream" [w]; drop "buf" [w]]); ("swprintf", unknown (drop "wcs" [w] :: drop "maxlen" [] :: drop "fmt" [r] :: VarArgs (drop' [r]))); ("assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" }); (* only used if assert is used without include, e.g. in transformed files *) @@ -133,6 +138,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("abs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (IInt, j)) }); ("labs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILong, j)) }); ("llabs", special [__ "j" []] @@ fun j -> Math { fun_args = (Abs (ILongLong, j)) }); + ("imaxabs", unknown [drop "j" []]); ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]); ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]); ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *) @@ -151,6 +157,7 @@ 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); + ("strcoll", unknown [drop "lhs" [r]; drop "rhs" [r]]); ] (** C POSIX library functions. @@ -300,6 +307,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("sendto", unknown [drop "sockfd" []; drop "buf" [r]; drop "len" []; drop "flags" []; drop "dest_addr" [r_deep]; drop "addrlen" []]); ("strdup", unknown [drop "s" [r]]); ("strndup", unknown [drop "s" [r]; drop "n" []]); + ("__strndup", unknown [drop "s" [r]; drop "n" []]); ("syscall", unknown (drop "number" [] :: VarArgs (drop' [r; w]))); ("sysconf", unknown [drop "name" []]); ("syslog", unknown (drop "priority" [] :: drop "format" [r] :: VarArgs (drop' [r]))); (* TODO: is the VarArgs correct here? *) @@ -408,6 +416,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("srandom", unknown [drop "seed" []]); ("random", special [] Rand); ("posix_memalign", unknown [drop "memptr" [w]; drop "alignment" []; drop "size" []]); (* TODO: Malloc *) + ("stpcpy", unknown [drop "dest" [w]; drop "src" [r]]); ] (** Pthread functions. *) @@ -654,6 +663,8 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fstatfs", unknown [drop "fd" []; drop "buf" [w]]); ("cfmakeraw", unknown [drop "termios" [r; w]]); ("process_vm_readv", unknown [drop "pid" []; drop "local_iov" [w_deep]; drop "liovcnt" []; drop "remote_iov" []; drop "riovcnt" []; drop "flags" []]); + ("__libc_current_sigrtmax", unknown []); + ("__libc_current_sigrtmin", unknown []); ] let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType))) From 7159875257d594d248b3b3b7b0560e4c37e91f09 Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Wed, 22 Nov 2023 13:47:15 +0200 Subject: [PATCH 2/4] Add fun defs for wprintf, iswxdigit and .*wscanf #1239 --- src/analyses/libraryFunctions.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 1a032c84b3..20995e2f09 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -125,6 +125,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("clearerr", unknown [drop "stream" [w]]); ("clearerr_unlocked", unknown [drop "stream" [w]]); ("setbuf", unknown [drop "stream" [w]; drop "buf" [w]]); + ("wprintf", unknown (drop "fmt" [r] :: VarArgs (drop' [r]))); + ("fwprintf", unknown (drop "stream" [w] :: drop "fmt" [r] :: VarArgs (drop' [r]))); ("swprintf", unknown (drop "wcs" [w] :: drop "maxlen" [] :: drop "fmt" [r] :: VarArgs (drop' [r]))); ("assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" }); (* only used if assert is used without include, e.g. in transformed files *) ("difftime", unknown [drop "time1" []; drop "time2" []]); @@ -158,6 +160,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("atomic_store", unknown [drop "obj" [w]; drop "desired" []]); ("_Exit", special [drop "status" []] @@ Abort); ("strcoll", unknown [drop "lhs" [r]; drop "rhs" [r]]); + ("wscanf", unknown (drop "fmt" [r] :: VarArgs (drop' [r]))); + ("fwscanf", unknown (drop "stream" [r] :: drop "fmt" [r] :: VarArgs (drop' [r]))); + ("swscanf", unknown (drop "buffer" [r] :: drop "fmt" [r] :: VarArgs (drop' [r]))); ] (** C POSIX library functions. From 949432b389c53939c08693ef1febe14f5c27e09b Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Wed, 22 Nov 2023 13:54:07 +0200 Subject: [PATCH 3/4] Add fun def for iswxdigit #1239 --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 20995e2f09..a9cce50b60 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -93,6 +93,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("iswspace", unknown [drop "wc" []]); ("iswalnum", unknown [drop "wc" []]); ("iswprint", unknown [drop "wc" []]); + ("iswxdigit", unknown [drop "ch" []]); ("rename" , unknown [drop "oldpath" [r]; drop "newpath" [r];]); ("perror", unknown [drop "s" [r]]); ("getchar", unknown []); From c98025cc96870659b7deff213bd7820c897d9a75 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 22 Nov 2023 14:09:50 +0200 Subject: [PATCH 4/4] Move *_unlocked functions to glibc group, fix *wscanf varargs --- src/analyses/libraryFunctions.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index a9cce50b60..8152e5b886 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -37,9 +37,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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]]); - ("feof_unlocked", unknown [drop "stream" [r_deep; w_deep]]); ("ferror", unknown [drop "stream" [r_deep; w_deep]]); - ("ferror_unlocked", unknown [drop "stream" [r_deep; w_deep]]); ("fflush", unknown [drop "stream" [r_deep; w_deep]]); ("fgetc", unknown [drop "stream" [r_deep; w_deep]]); ("getc", unknown [drop "stream" [r_deep; w_deep]]); @@ -54,11 +52,9 @@ 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_chk_warn", unknown [drop "buffer" [w]; drop "os" []; 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]]); - ("fwrite_unlocked", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); ("rewind", unknown [drop "stream" [r_deep; w_deep]]); ("setvbuf", unknown [drop "stream" [r_deep; w_deep]; drop "buffer" [r; w]; drop "mode" []; drop "size" []]); (* TODO: if this is used to set an input buffer, the buffer (second argument) would need to remain TOP, *) @@ -123,11 +119,10 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("vsnprintf", unknown [drop "str" [w]; drop "size" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("mktime", unknown [drop "tm" [r;w]]); ("ctime", unknown ~attrs:[ThreadUnsafe] [drop "rm" [r]]); - ("clearerr", unknown [drop "stream" [w]]); - ("clearerr_unlocked", unknown [drop "stream" [w]]); + ("clearerr", unknown [drop "stream" [w]]); (* TODO: why only w? *) ("setbuf", unknown [drop "stream" [w]; drop "buf" [w]]); ("wprintf", unknown (drop "fmt" [r] :: VarArgs (drop' [r]))); - ("fwprintf", unknown (drop "stream" [w] :: drop "fmt" [r] :: VarArgs (drop' [r]))); + ("fwprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "fmt" [r] :: VarArgs (drop' [r]))); ("swprintf", unknown (drop "wcs" [w] :: drop "maxlen" [] :: drop "fmt" [r] :: VarArgs (drop' [r]))); ("assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" }); (* only used if assert is used without include, e.g. in transformed files *) ("difftime", unknown [drop "time1" []; drop "time2" []]); @@ -161,9 +156,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("atomic_store", unknown [drop "obj" [w]; drop "desired" []]); ("_Exit", special [drop "status" []] @@ Abort); ("strcoll", unknown [drop "lhs" [r]; drop "rhs" [r]]); - ("wscanf", unknown (drop "fmt" [r] :: VarArgs (drop' [r]))); - ("fwscanf", unknown (drop "stream" [r] :: drop "fmt" [r] :: VarArgs (drop' [r]))); - ("swscanf", unknown (drop "buffer" [r] :: drop "fmt" [r] :: VarArgs (drop' [r]))); + ("wscanf", unknown (drop "fmt" [r] :: VarArgs (drop' [w]))); + ("fwscanf", unknown (drop "stream" [r_deep; w_deep] :: drop "fmt" [r] :: VarArgs (drop' [w]))); + ("swscanf", unknown (drop "buffer" [r] :: drop "fmt" [r] :: VarArgs (drop' [w]))); ] (** C POSIX library functions. @@ -586,6 +581,10 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fputs_unlocked", unknown [drop "s" [r]; drop "stream" [w]]); + ("feof_unlocked", unknown [drop "stream" [r_deep; w_deep]]); + ("ferror_unlocked", unknown [drop "stream" [r_deep; w_deep]]); + ("fwrite_unlocked", unknown [drop "buffer" [r]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); + ("clearerr_unlocked", unknown [drop "stream" [w]]); (* TODO: why only w? *) ("futimesat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "times" [r]]); ("error", unknown ((drop "status" []) :: (drop "errnum" []) :: (drop "format" [r]) :: (VarArgs (drop' [r])))); ("warn", unknown (drop "format" [r] :: VarArgs (drop' [r]))); @@ -597,6 +596,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_chk_warn", unknown [drop "buffer" [w]; drop "os" []; 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]]); ("__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]]);