From 856dccb47d6fd05498a9e01d541da00ccdfe2301 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Wed, 7 Jun 2023 18:58:53 +0300 Subject: [PATCH 01/22] Add fopencookie to libraryFunctions --- src/analyses/libraryFunctions.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 3eacf9013a..93eb75c09b 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -257,6 +257,7 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strsep", unknown [drop "stringp" [r_deep; w]; drop "delim" [r]]); ("strcasestr", unknown [drop "haystack" [r]; drop "needle" [r]]); ("inet_aton", unknown [drop "cp" [r]; drop "inp" [w]]); + ("fopencookie", unknown [drop "cookie" []; drop "mode" [r]; drop "io_funcs" [s_deep]]); (* doesn't access cookie but passes it to io_funcs *) ] let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ From 8753565a893c93e399fc233dd3f0234a86e0cf62 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Wed, 7 Jun 2023 19:04:03 +0300 Subject: [PATCH 02/22] Remove functions already defined in libraries from invalidate_actions --- src/analyses/libraryFunctions.ml | 48 -------------------------------- 1 file changed, 48 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 93eb75c09b..5a16c9edcf 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -671,10 +671,7 @@ let invalidate_actions = [ "_spin_lock", readsAll;(*safe*) "_spin_unlock", readsAll;(*safe*) "_spin_lock_irqsave", readsAll;(*safe*) - "_spin_unlock_irqrestore", readsAll;(*safe*) - "pthread_mutex_init", readsAll;(*safe*) "pthread_mutex_destroy", readsAll;(*safe*) - "pthread_mutexattr_settype", readsAll;(*safe*) "pthread_mutexattr_init", readsAll;(*safe*) "pthread_spin_init", readsAll;(*safe*) "pthread_spin_destroy", readsAll;(*safe*) @@ -718,7 +715,6 @@ let invalidate_actions = [ "getc", writesAll;(*unsafe*) "_IO_getc", writesAll;(*unsafe*) "closedir", writesAll;(*unsafe*) - "setrlimit", readsAll;(*safe*) "chdir", readsAll;(*safe*) "pipe", writesAll;(*unsafe*) "close", writesAll;(*unsafe*) @@ -732,9 +728,6 @@ let invalidate_actions = [ "pthread_attr_getstacksize", readsAll;(*safe*) "pthread_attr_getscope", readsAll;(*safe*) "pthread_cond_init", readsAll; (*safe*) - "pthread_cond_wait", readsAll; (*safe*) - "pthread_cond_signal", readsAll;(*safe*) - "pthread_cond_broadcast", readsAll;(*safe*) "pthread_cond_destroy", readsAll;(*safe*) "__pthread_cond_init", readsAll; (*safe*) "__pthread_cond_wait", readsAll; (*safe*) @@ -747,7 +740,6 @@ let invalidate_actions = [ "pthread_sigmask", writesAllButFirst 2 readsAll;(*unsafe*) "raise", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) - "__builtin_object_size", readsAll;(*safe*) "__builtin_alloca", readsAll;(*safe*) "dlopen", readsAll;(*safe*) "dlsym", readsAll;(*safe*) @@ -827,7 +819,6 @@ let invalidate_actions = [ "usleep", readsAll; "svc_run", writesAll;(*unsafe*) "dup", readsAll; (*safe*) - "__builtin_expect", readsAll; (*safe*) "vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) @@ -852,7 +843,6 @@ let invalidate_actions = [ "fgets", writes [1;3]; (*keep [3]*) "__fgets_alias", writes [1;3]; (*keep [3]*) "__fgets_chk", writes [1;3]; (*keep [3]*) - "strtoul", readsAll; (*safe*) "__tolower", readsAll; (*safe*) "signal", writesAll; (*unsafe*) "strsignal", readsAll; @@ -882,12 +872,10 @@ let invalidate_actions = [ "sem_wait", readsAll; (*safe*) "sem_post", readsAll; (*safe*) "PL_NewHashTable", readsAll; (*safe*) - "__assert_fail", readsAll; (*safe*) "assert_failed", readsAll; (*safe*) "htonl", readsAll; (*safe*) "htons", readsAll; (*safe*) "ntohl", readsAll; (*safe*) - "htons", readsAll; (*safe*) "munmap", readsAll;(*safe*) "mmap", readsAll;(*safe*) "clock", readsAll; @@ -908,15 +896,12 @@ let invalidate_actions = [ "__open_too_many_args", readsAll; "usb_submit_urb", readsAll; (* first argument is written to but according to specification must not be read from anymore *) "dev_driver_string", readsAll; - "dev_driver_string", readsAll; "__spin_lock_init", writes [1]; "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 *) (* no args, declare invalidate actions to prevent invalidating globals *) - "__VERIFIER_atomic_begin", readsAll; - "__VERIFIER_atomic_end", readsAll; "isatty", readsAll; "setpriority", readsAll; "getpriority", readsAll; @@ -927,42 +912,24 @@ let invalidate_actions = [ "sema_init", readsAll; "down_trylock", readsAll; "up", readsAll; - "acos", readsAll; - "acosf", readsAll; "acosh", readsAll; "acoshf", readsAll; "acoshl", readsAll; - "acosl", readsAll; - "asin", readsAll; - "asinf", readsAll; "asinh", readsAll; "asinhf", readsAll; "asinhl", readsAll; - "asinl", readsAll; - "atan", readsAll; - "atan2", readsAll; - "atan2f", readsAll; - "atan2l", readsAll; - "atanf", readsAll; "atanh", readsAll; "atanhf", readsAll; "atanhl", readsAll; - "atanl", readsAll; "cbrt", readsAll; "cbrtf", readsAll; "cbrtl", readsAll; - "ceil", readsAll; - "ceilf", readsAll; - "ceill", readsAll; "copysign", readsAll; "copysignf", readsAll; "copysignl", readsAll; - "cos", readsAll; - "cosf", readsAll; "cosh", readsAll; "coshf", readsAll; "coshl", readsAll; - "cosl", readsAll; "erf", readsAll; "erfc", readsAll; "erfcf", readsAll; @@ -984,12 +951,6 @@ let invalidate_actions = [ "fma", readsAll; "fmaf", readsAll; "fmal", readsAll; - "fmax", readsAll; - "fmaxf", readsAll; - "fmaxl", readsAll; - "fmin", readsAll; - "fminf", readsAll; - "fminl", readsAll; "fmod", readsAll; "fmodf", readsAll; "fmodl", readsAll; @@ -1041,9 +1002,6 @@ let invalidate_actions = [ "modf", readsAll; "modff", readsAll; "modfl", readsAll; - "nan", readsAll; - "nanf", readsAll; - "nanl", readsAll; "nearbyint", readsAll; "nearbyintf", readsAll; "nearbyintl", readsAll; @@ -1074,21 +1032,15 @@ let invalidate_actions = [ "scalbn", readsAll; "scalbnf", readsAll; "scalbnl", readsAll; - "sin", readsAll; - "sinf", readsAll; "sinh", readsAll; "sinhf", readsAll; "sinhl", readsAll; - "sinl", readsAll; "sqrt", readsAll; "sqrtf", readsAll; "sqrtl", readsAll; - "tan", readsAll; - "tanf", readsAll; "tanh", readsAll; "tanhf", readsAll; "tanhl", readsAll; - "tanl", readsAll; "tgamma", readsAll; "tgammaf", readsAll; "tgammal", readsAll; From a0b390930b895640301e73d75486e9ba919983ba Mon Sep 17 00:00:00 2001 From: karoliineh Date: Wed, 7 Jun 2023 19:05:17 +0300 Subject: [PATCH 03/22] Add failwith to prevent goblint devs from adding functions already in libraries to invalidate_actions --- src/analyses/libraryFunctions.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 5a16c9edcf..7940c03045 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -1053,6 +1053,10 @@ let invalidate_actions = [ "__goblint_assume_join", readsAll; ] +let () = List.iter (fun (x, _) -> + if Hashtbl.exists (fun _ b -> List.mem_assoc x b) libraries then + failwith ("You have added a function to invalidate_actions that already exists in libraries. Please undo this for function: " ^ x); + ) invalidate_actions (* used by get_invalidate_action to make sure * that hash of invalidates is built only once From 81db59318819a89cea0757dd4082f4bb26acfb75 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Thu, 8 Jun 2023 17:54:12 +0300 Subject: [PATCH 04/22] Convert all math.h functions to new specifications --- src/analyses/libraryFunctions.ml | 276 +++++++++++++++---------------- 1 file changed, 138 insertions(+), 138 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 7940c03045..0d432e0efa 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -398,6 +398,144 @@ let math_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("tan", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FDouble, x)) }); ("tanf", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FFloat, x)) }); ("tanl", special [__ "x" []] @@ fun x -> Math { fun_args = (Tan (FLongDouble, x)) }); + ("acosh", unknown [drop "x" []]); + ("acoshf", unknown [drop "x" []]); + ("acoshl", unknown [drop "x" []]); + ("asinh", unknown [drop "x" []]); + ("asinhf", unknown [drop "x" []]); + ("asinhl", unknown [drop "x" []]); + ("atanh", unknown [drop "x" []]); + ("atanhf", unknown [drop "x" []]); + ("atanhl", unknown [drop "x" []]); + ("cosh", unknown [drop "x" []]); + ("coshf", unknown [drop "x" []]); + ("coshl", unknown [drop "x" []]); + ("sinh", unknown [drop "x" []]); + ("sinhf", unknown [drop "x" []]); + ("sinhl", unknown [drop "x" []]); + ("tanh", unknown [drop "x" []]); + ("tanhf", unknown [drop "x" []]); + ("tanhl", unknown [drop "x" []]); + ("cbrt", unknown [drop "x" []]); + ("cbrtf", unknown [drop "x" []]); + ("cbrtl", unknown [drop "x" []]); + ("copysign", unknown [drop "x" []; drop "y" []]); + ("copysignf", unknown [drop "x" []; drop "y" []]); + ("copysignl", unknown [drop "x" []; drop "y" []]); + ("erf", unknown [drop "x" []]); + ("erff", unknown [drop "x" []]); + ("erfl", unknown [drop "x" []]); + ("erfc", unknown [drop "x" []]); + ("erfcf", unknown [drop "x" []]); + ("erfcl", unknown [drop "x" []]); + ("exp", unknown [drop "x" []]); + ("expf", unknown [drop "x" []]); + ("expl", unknown [drop "x" []]); + ("exp2", unknown [drop "x" []]); + ("exp2f", unknown [drop "x" []]); + ("exp2l", unknown [drop "x" []]); + ("expm1", unknown [drop "x" []]); + ("expm1f", unknown [drop "x" []]); + ("expm1l", unknown [drop "x" []]); + ("fdim", unknown [drop "x" []; drop "y" []]); + ("fdimf", unknown [drop "x" []; drop "y" []]); + ("fdiml", unknown [drop "x" []; drop "y" []]); + ("fma", unknown [drop "x" []; drop "y" []; drop "z" []]); + ("fmaf", unknown [drop "x" []; drop "y" []; drop "z" []]); + ("fmal", unknown [drop "x" []; drop "y" []; drop "z" []]); + ("fmod", unknown [drop "x" []; drop "y" []]); + ("fmodf", unknown [drop "x" []; drop "y" []]); + ("fmodl", unknown [drop "x" []; drop "y" []]); + ("frexp", unknown [drop "arg" []; drop "exp" [w]]); + ("frexpf", unknown [drop "arg" []; drop "exp" [w]]); + ("frexpl", unknown [drop "arg" []; drop "exp" [w]]); + ("hypot", unknown [drop "x" []; drop "y" []]); + ("hypotf", unknown [drop "x" []; drop "y" []]); + ("hypotl", unknown [drop "x" []; drop "y" []]); + ("ilogb", unknown [drop "x" []]); + ("ilogbf", unknown [drop "x" []]); + ("ilogbl", unknown [drop "x" []]); + ("ldexp", unknown [drop "arg" []; drop "exp" []]); + ("ldexpf", unknown [drop "arg" []; drop "exp" []]); + ("ldexpl", unknown [drop "arg" []; drop "exp" []]); + ("lgamma", unknown [drop "x" []]); + ("lgammaf", unknown [drop "x" []]); + ("lgammal", unknown [drop "x" []]); + ("log", unknown [drop "x" []]); + ("logf", unknown [drop "x" []]); + ("logl", unknown [drop "x" []]); + ("log10", unknown [drop "x" []]); + ("log10f", unknown [drop "x" []]); + ("log10l", unknown [drop "x" []]); + ("log1p", unknown [drop "x" []]); + ("log1pf", unknown [drop "x" []]); + ("log1pl", unknown [drop "x" []]); + ("log2", unknown [drop "x" []]); + ("log2f", unknown [drop "x" []]); + ("log2l", unknown [drop "x" []]); + ("logb", unknown [drop "x" []]); + ("logbf", unknown [drop "x" []]); + ("logbl", unknown [drop "x" []]); + ("rint", unknown [drop "x" []]); + ("rintf", unknown [drop "x" []]); + ("rintl", unknown [drop "x" []]); + ("lrint", unknown [drop "x" []]); + ("lrintf", unknown [drop "x" []]); + ("lrintl", unknown [drop "x" []]); + ("llrint", unknown [drop "x" []]); + ("llrintf", unknown [drop "x" []]); + ("llrintl", unknown [drop "x" []]); + ("round", unknown [drop "x" []]); + ("roundf", unknown [drop "x" []]); + ("roundl", unknown [drop "x" []]); + ("lround", unknown [drop "x" []]); + ("lroundf", unknown [drop "x" []]); + ("lroundl", unknown [drop "x" []]); + ("llround", unknown [drop "x" []]); + ("llroundf", unknown [drop "x" []]); + ("llroundl", unknown [drop "x" []]); + ("modf", unknown [drop "arg" []; drop "iptr" [w]]); + ("modff", unknown [drop "arg" []; drop "iptr" [w]]); + ("modfl", unknown [drop "arg" []; drop "iptr" [w]]); + ("nearbyint", unknown [drop "x" []]); + ("nearbyintf", unknown [drop "x" []]); + ("nearbyintl", unknown [drop "x" []]); + ("nextafter", unknown [drop "from" []; drop "to" []]); + ("nextafterf", unknown [drop "from" []; drop "to" []]); + ("nextafterl", unknown [drop "from" []; drop "to" []]); + ("nexttoward", unknown [drop "from" []; drop "to" []]); + ("nexttowardf", unknown [drop "from" []; drop "to" []]); + ("nexttowardl", unknown [drop "from" []; drop "to" []]); + ("pow", unknown [drop "base" []; drop "exponent" []]); + ("powf", unknown [drop "base" []; drop "exponent" []]); + ("powl", unknown [drop "base" []; drop "exponent" []]); + ("remainder", unknown [drop "x" []; drop "y" []]); + ("remainderf", unknown [drop "x" []; drop "y" []]); + ("remainderl", unknown [drop "x" []; drop "y" []]); + ("remquo", unknown [drop "x" []; drop "y" []; drop "quo" [w]]); + ("remquof", unknown [drop "x" []; drop "y" []; drop "quo" [w]]); + ("remquol", unknown [drop "x" []; drop "y" []; drop "quo" [w]]); + ("scalbn", unknown [drop "arg" []; drop "exp" []]); + ("scalbnf", unknown [drop "arg" []; drop "exp" []]); + ("scalbnl", unknown [drop "arg" []; drop "exp" []]); + ("scalbln", unknown [drop "arg" []; drop "exp" []]); + ("scalblnf", unknown [drop "arg" []; drop "exp" []]); + ("scalblnl", unknown [drop "arg" []; drop "exp" []]); + ("sqrt", unknown [drop "x" []]); + ("sqrtf", unknown [drop "x" []]); + ("sqrtl", unknown [drop "x" []]); + ("tgamma", unknown [drop "x" []]); + ("tgammaf", unknown [drop "x" []]); + ("tgammal", unknown [drop "x" []]); + ("trunc", unknown [drop "x" []]); + ("truncf", unknown [drop "x" []]); + ("truncl", unknown [drop "x" []]); + ("j0", unknown [drop "x" []]); (* GNU C Library special function *) + ("j1", unknown [drop "x" []]); (* GNU C Library special function *) + ("jn", unknown [drop "n" []; drop "x" []]); (* GNU C Library special function *) + ("y0", unknown [drop "x" []]); (* GNU C Library special function *) + ("y1", unknown [drop "x" []]); (* GNU C Library special function *) + ("yn", unknown [drop "n" []; drop "x" []]); (* GNU C Library special function *) ("fegetround", unknown []); ("fesetround", unknown [drop "round" []]); (* Our float domain is rounding agnostic *) ("__builtin_fpclassify", unknown [drop "nan" []; drop "infinite" []; drop "normal" []; drop "subnormal" []; drop "zero" []; drop "x" []]); (* TODO: We could do better here *) @@ -912,144 +1050,6 @@ let invalidate_actions = [ "sema_init", readsAll; "down_trylock", readsAll; "up", readsAll; - "acosh", readsAll; - "acoshf", readsAll; - "acoshl", readsAll; - "asinh", readsAll; - "asinhf", readsAll; - "asinhl", readsAll; - "atanh", readsAll; - "atanhf", readsAll; - "atanhl", readsAll; - "cbrt", readsAll; - "cbrtf", readsAll; - "cbrtl", readsAll; - "copysign", readsAll; - "copysignf", readsAll; - "copysignl", readsAll; - "cosh", readsAll; - "coshf", readsAll; - "coshl", readsAll; - "erf", readsAll; - "erfc", readsAll; - "erfcf", readsAll; - "erfcl", readsAll; - "erff", readsAll; - "erfl", readsAll; - "exp", readsAll; - "exp2", readsAll; - "exp2f", readsAll; - "exp2l", readsAll; - "expf", readsAll; - "expl", readsAll; - "expm1", readsAll; - "expm1f", readsAll; - "expm1l", readsAll; - "fdim", readsAll; - "fdimf", readsAll; - "fdiml", readsAll; - "fma", readsAll; - "fmaf", readsAll; - "fmal", readsAll; - "fmod", readsAll; - "fmodf", readsAll; - "fmodl", readsAll; - "frexp", readsAll; - "frexpf", readsAll; - "frexpl", readsAll; - "hypot", readsAll; - "hypotf", readsAll; - "hypotl", readsAll; - "ilogb", readsAll; - "ilogbf", readsAll; - "ilogbl", readsAll; - "j0", readsAll; - "j1", readsAll; - "jn", readsAll; - "ldexp", readsAll; - "ldexpf", readsAll; - "ldexpl", readsAll; - "lgamma", readsAll; - "lgammaf", readsAll; - "lgammal", readsAll; - "llrint", readsAll; - "llrintf", readsAll; - "llrintl", readsAll; - "llround", readsAll; - "llroundf", readsAll; - "llroundl", readsAll; - "log", readsAll; - "log10", readsAll; - "log10f", readsAll; - "log10l", readsAll; - "log1p", readsAll; - "log1pf", readsAll; - "log1pl", readsAll; - "log2", readsAll; - "log2f", readsAll; - "log2l", readsAll; - "logb", readsAll; - "logbf", readsAll; - "logbl", readsAll; - "logf", readsAll; - "logl", readsAll; - "lrint", readsAll; - "lrintf", readsAll; - "lrintl", readsAll; - "lround", readsAll; - "lroundf", readsAll; - "lroundl", readsAll; - "modf", readsAll; - "modff", readsAll; - "modfl", readsAll; - "nearbyint", readsAll; - "nearbyintf", readsAll; - "nearbyintl", readsAll; - "nextafter", readsAll; - "nextafterf", readsAll; - "nextafterl", readsAll; - "nexttoward", readsAll; - "nexttowardf", readsAll; - "nexttowardl", readsAll; - "pow", readsAll; - "powf", readsAll; - "powl", readsAll; - "remainder", readsAll; - "remainderf", readsAll; - "remainderl", readsAll; - "remquo", readsAll; - "remquof", readsAll; - "remquol", readsAll; - "rint", readsAll; - "rintf", readsAll; - "rintl", readsAll; - "round", readsAll; - "roundf", readsAll; - "roundl", readsAll; - "scalbln", readsAll; - "scalblnf", readsAll; - "scalblnl", readsAll; - "scalbn", readsAll; - "scalbnf", readsAll; - "scalbnl", readsAll; - "sinh", readsAll; - "sinhf", readsAll; - "sinhl", readsAll; - "sqrt", readsAll; - "sqrtf", readsAll; - "sqrtl", readsAll; - "tanh", readsAll; - "tanhf", readsAll; - "tanhl", readsAll; - "tgamma", readsAll; - "tgammaf", readsAll; - "tgammal", readsAll; - "trunc", readsAll; - "truncf", readsAll; - "truncl", readsAll; - "y0", readsAll; - "y1", readsAll; - "yn", readsAll; "__goblint_assume_join", readsAll; ] From e94f1c41c5f1b4b4068adc976efd6bf567a90cd6 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Thu, 8 Jun 2023 18:21:10 +0300 Subject: [PATCH 05/22] Convert some __builtin functions to new specifications --- 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 0d432e0efa..5ea4fdf3fa 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -182,6 +182,14 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ (** GCC builtin functions. These are not builtin versions of functions from other lists. *) let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ + ("__builtin_bswap16", unknown [drop "x" []]); + ("__builtin_bswap32", unknown [drop "x" []]); + ("__builtin_bswap64", unknown [drop "x" []]); + ("__builtin_bswap128", unknown [drop "x" []]); + ("__builtin_ctz", unknown [drop "x" []]); + ("__builtin_ctzl", unknown [drop "x" []]); + ("__builtin_ctzll", unknown [drop "x" []]); + ("__builtin_clz", unknown [drop "x" []]); ("__builtin_object_size", unknown [drop "ptr" [r]; drop' []]); ("__builtin_prefetch", unknown (drop "addr" [] :: VarArgs (drop' []))); ("__builtin_expect", special [__ "exp" []; drop' []] @@ fun exp -> Identity exp); (* Identity, because just compiler optimization annotation. *) @@ -765,10 +773,6 @@ open Invalidate (* WTF: why are argument numbers 1-indexed (in partition)? *) let invalidate_actions = [ "atoi", readsAll; (*safe*) - "__builtin_ctz", readsAll; - "__builtin_ctzl", readsAll; - "__builtin_ctzll", readsAll; - "__builtin_clz", readsAll; "connect", readsAll; (*safe*) "fclose", readsAll; (*safe*) "fflush", writesAll; (*unsafe*) @@ -1026,10 +1030,6 @@ let invalidate_actions = [ "pthread_rwlock_destroy", readsAll; "pthread_rwlock_init", readsAll; "pthread_rwlock_unlock", readsAll; - "__builtin_bswap16", readsAll; - "__builtin_bswap32", readsAll; - "__builtin_bswap64", readsAll; - "__builtin_bswap128", 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 96a59cbaadb917ed2f5665fce6df4e6c73a84299 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Fri, 9 Jun 2023 16:24:22 +0300 Subject: [PATCH 06/22] Convert most file-related functions to new specifications --- src/analyses/libraryFunctions.ml | 67 ++++++++++++++++---------------- 1 file changed, 34 insertions(+), 33 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 5ea4fdf3fa..8fdc867834 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -15,6 +15,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); ("__builtin_memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); ("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); + ("mempcpy", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []]); + ("__builtin___mempcpy_chk", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []; drop "os" []]); ("strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin_strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin___strcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "os" []] @@ fun dest src -> Strcpy { dest; src; n = None; }); @@ -27,6 +29,27 @@ 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; }); + ("free", unknown [drop "ptr" [f]]); + ("fclose", unknown [drop "stream" [r_deep; w_deep; f_deep]]); + ("feof", unknown [drop "stream" [r_deep; w_deep]]); + ("ferror", 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]]); + ("fgets", unknown [drop "str" [r; w]; drop "count" []; drop "stream" [r_deep; w_deep]]); + ("fopen", unknown [drop "pathname" [r]; drop "mode" [r]]); + ("fdopen", unknown [drop "fd" []; drop "mode" [r]]); + ("fprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]]); + ("fputc", 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_deep]; 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_deep]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); + ("setvbuf", unknown [drop "stream" [r_deep; w_deep]; drop "buffer" [r_deep; w_deep]; drop "mode" []; drop "size" []]); + (* TODO: if this is used to set an input buffer, the buffer (second argument) would need to remain TOP, *) + (* as any future write (or flush) of the stream could result in a write to the buffer *) + ("localtime", unknown [drop "time" [r]]); ("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; }); @@ -85,7 +108,10 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("putc_unlocked", unknown [drop "c" []; drop "stream" [w]]); ("putchar_unlocked", unknown [drop "c" []]); ("lseek", unknown [drop "fd" []; drop "offset" []; drop "whence" []]); - ("fseeko", unknown [drop "stream" [w]; drop "offset" []; drop "whence" []]); + ("fcntl", unknown (drop "fd" [] :: drop "cmd" [] :: VarArgs (drop' [r; w]))); + ("fseeko", unknown [drop "stream" [r_deep; w_deep]; drop "offset" []; drop "whence" []]); + ("fileno", unknown [drop "stream" [r_deep; w_deep]]); + ("getopt", unknown [drop "argc" []; drop "argv" [r]; drop "optstring" [r]]); ("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]]); @@ -98,6 +124,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("gettimeofday", unknown [drop "tv" [w]; drop "tz" [w]]); ("futimens", unknown [drop "fd" []; drop "times" [r]]); ("utimes", unknown [drop "filename" [r]; drop "times" [r]]); + ("utimensat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "times" [r]; drop "flags" []]); ("linkat", unknown [drop "olddirfd" []; drop "oldpath" [r]; drop "newdirfd" []; drop "newpath" [r]; drop "flags" []]); ("dirfd", unknown [drop "dirp" [r]]); ("fdopendir", unknown [drop "fd" []]); @@ -234,12 +261,16 @@ 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]]); - ("futimesat", unknown [drop "dirfd" [w]; drop "pathname" [r]; drop "times" [r]]); + ("futimesat", unknown [drop "dirfd" []; drop "pathname" [r]; drop "times" [r]]); ("error", unknown ((drop "status" []):: (drop "errnum" []) :: (drop "format" [r]) :: (VarArgs (drop' [r])))); ("gettext", unknown [drop "msgid" [r]]); ("euidaccess", unknown [drop "pathname" [r]; drop "mode" []]); ("rpmatch", unknown [drop "response" [r]]); ("getpagesize", unknown []); + ("__fgets_alias", unknown [drop "__s" [r; w]; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("__fgets_chk", unknown [drop "__s" [r; w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("__fread_alias", unknown [drop "__ptr" [w_deep]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("__fread_chk", unknown [drop "__ptr" [w_deep]; 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" []]); @@ -276,6 +307,7 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("epoll_create", unknown [drop "size" []]); ("epoll_ctl", unknown [drop "epfd" []; drop "op" []; drop "fd" []; drop "event" [w]]); ("epoll_wait", unknown [drop "epfd" []; drop "events" [w]; drop "maxevents" []; drop "timeout" []]); + ("__fprintf_chk", unknown [drop "stream" [r_deep; w_deep]; drop "flag" []; drop "format" [r]]); ("sysinfo", unknown [drop "info" [w_deep]]); ("__xpg_basename", unknown [drop "path" [r]]); ("ptrace", unknown (drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); (* man page has 4 arguments, but header has varargs and real-world programs may call with <4 *) @@ -774,24 +806,6 @@ open Invalidate let invalidate_actions = [ "atoi", readsAll; (*safe*) "connect", readsAll; (*safe*) - "fclose", readsAll; (*safe*) - "fflush", writesAll; (*unsafe*) - "fopen", readsAll; (*safe*) - "fdopen", readsAll; (*safe*) - "setvbuf", writes[1;2]; (* TODO: if this is used to set an input buffer, the buffer (second argument) would need to remain TOP, *) - (* as any future write (or flush) of the stream could result in a write to the buffer *) - "fprintf", writes [1]; (*keep [1]*) - "__fprintf_chk", writes [1]; (*keep [1]*) - "fread", writes [1;4]; - "__fread_alias", writes [1;4]; - "__fread_chk", writes [1;4]; - "utimensat", readsAll; - "free", frees [1]; (*unsafe*) - "fwrite", readsAll;(*safe*) - "getopt", writes [2];(*keep [2]*) - "localtime", readsAll;(*safe*) - "mempcpy", writes [1];(*keep [1]*) - "__builtin___mempcpy_chk", writes [1]; "printf", readsAll;(*safe*) "__printf_chk", readsAll;(*safe*) "printk", readsAll;(*safe*) @@ -853,8 +867,6 @@ let invalidate_actions = [ "readdir_r", writesAll;(*unsafe*) "atoi__extinline", readsAll;(*safe*) "getpid", readsAll;(*safe*) - "fgetc", writesAll;(*unsafe*) - "getc", writesAll;(*unsafe*) "_IO_getc", writesAll;(*unsafe*) "closedir", writesAll;(*unsafe*) "chdir", readsAll;(*safe*) @@ -904,7 +916,6 @@ let invalidate_actions = [ "open", readsAll;(*safe*) "__open_alias", readsAll;(*safe*) "__open_2", readsAll;(*safe*) - "fcntl", readsAll;(*safe*) "ioctl", writesAll;(*unsafe*) "fstat__extinline", writesAll;(*unsafe*) "umount", readsAll;(*safe*) @@ -922,18 +933,11 @@ let invalidate_actions = [ "dcgettext", readsAll;(*safe*) "syscall", writesAllButFirst 1 readsAll;(*drop 1*) "sysconf", readsAll; - "fputs", readsAll;(*safe*) - "fputc", readsAll;(*safe*) - "fseek", writes[1]; "rewind", writesAll; - "fileno", readsAll; - "ferror", readsAll; - "ftell", readsAll; "putc", readsAll;(*safe*) "putw", readsAll;(*safe*) "putchar", readsAll;(*safe*) "getchar", readsAll;(*safe*) - "feof", readsAll;(*safe*) "__getdelim", writes [3];(*keep [3]*) "vsyslog", readsAll;(*safe*) "gethostbyname_r", readsAll;(*safe*) @@ -982,9 +986,6 @@ let invalidate_actions = [ "getpeername", writes [1]; (*keep [1]*) "times", writesAll; (*unsafe*) "timespec_get", writes [1]; - "fgets", writes [1;3]; (*keep [3]*) - "__fgets_alias", writes [1;3]; (*keep [3]*) - "__fgets_chk", writes [1;3]; (*keep [3]*) "__tolower", readsAll; (*safe*) "signal", writesAll; (*unsafe*) "strsignal", readsAll; From ce50eb4eb88693f98316f5f2a2db1cfac4e2b02a Mon Sep 17 00:00:00 2001 From: karoliineh Date: Fri, 9 Jun 2023 19:11:02 +0300 Subject: [PATCH 07/22] Fix fprintf: add VarArgs --- 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 8fdc867834..ac60ec2643 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -39,7 +39,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fgets", unknown [drop "str" [r; w]; drop "count" []; drop "stream" [r_deep; w_deep]]); ("fopen", unknown [drop "pathname" [r]; drop "mode" [r]]); ("fdopen", unknown [drop "fd" []; drop "mode" [r]]); - ("fprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]]); + ("fprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) ("fputc", 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_deep]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); From c272f14e6a530829666841fd53786201176bb906 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Fri, 9 Jun 2023 19:11:49 +0300 Subject: [PATCH 08/22] Mark and add thread-unsafe functions in libraryFunctions, relates to #723 --- src/analyses/libraryFunctions.ml | 110 +++++++++++++++++++++++-------- 1 file changed, 84 insertions(+), 26 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index ac60ec2643..9b689b64ad 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -29,6 +29,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; }); + ("asctime", unknown ~attrs:[ThreadUnsafe] [drop "time_ptr" [r_deep]]); ("free", unknown [drop "ptr" [f]]); ("fclose", unknown [drop "stream" [r_deep; w_deep; f_deep]]); ("feof", unknown [drop "stream" [r_deep; w_deep]]); @@ -49,10 +50,13 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("setvbuf", unknown [drop "stream" [r_deep; w_deep]; drop "buffer" [r_deep; w_deep]; drop "mode" []; drop "size" []]); (* TODO: if this is used to set an input buffer, the buffer (second argument) would need to remain TOP, *) (* as any future write (or flush) of the stream could result in a write to the buffer *) - ("localtime", unknown [drop "time" [r]]); + ("gmtime", unknown ~attrs:[ThreadUnsafe] [drop "timer" [r_deep]]); + ("localeconv", unknown ~attrs:[ThreadUnsafe] []); + ("localtime", unknown ~attrs:[ThreadUnsafe] [drop "time" [r]]); ("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]; 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; }); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); @@ -69,6 +73,7 @@ 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]]); + ("rand", unknown ~attrs:[ThreadUnsafe] []); ("strspn", unknown [drop "s" [r]; drop "accept" [r]]); ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]); ("strtod", unknown [drop "nptr" [r]; drop "endptr" [w]]); @@ -77,15 +82,17 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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" []]); + ("tmpnam", unknown ~attrs:[ThreadUnsafe] [drop "filename" [r]]); ("mktime", unknown [drop "tm" [r;w]]); - ("ctime", unknown [drop "rm" [r]]); + ("ctime", unknown ~attrs:[ThreadUnsafe] [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' []))); ("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" []]); - ("system", unknown [drop "command" [r]]); + ("system", unknown ~attrs:[ThreadUnsafe] [drop "command" [r]]); ("wcscat", unknown [drop "dest" [r; w]; drop "src" [r]]); + ("wcrtomb", unknown ~attrs:[ThreadUnsafe] [drop "s" [r]; drop "wc" []; drop "ps" [w_deep]]); ("abs", unknown [drop "j" []]); ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]); ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]); @@ -101,17 +108,74 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_bzero", special [__ "dest" [w]; __ "count" []] @@ fun dest count -> Bzero { dest; count; }); ("explicit_bzero", special [__ "dest" [w]; __ "count" []] @@ fun dest count -> Bzero { dest; count; }); ("__explicit_bzero_chk", special [__ "dest" [w]; __ "count" []; drop "os" []] @@ fun dest count -> Bzero { dest; count; }); - ("nl_langinfo", unknown [drop "item" []]); + ("catgets", unknown ~attrs:[ThreadUnsafe] [drop "catalog" [r_deep]; drop "set_number" []; drop "message_number" []; drop "message" [r_deep]]); + ("crypt", unknown ~attrs:[ThreadUnsafe] [drop "key" [r]; drop "salt" [r]]); + ("ctermid", unknown ~attrs:[ThreadUnsafe] [drop "s" [r]]); + ("dbm_clearerr", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep; w_deep]]); + ("dbm_close", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep; w_deep; f_deep]]); + ("dbm_delete", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep; w_deep]; drop "key" []]); + ("dbm_error", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep]]); + ("dbm_fetch", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep]; drop "key" []]); + ("dbm_firstkey", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep]]); + ("dbm_nextkey", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep]]); + ("dbm_open", unknown ~attrs:[ThreadUnsafe] [drop "file" [r_deep; w_deep]; 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" []; drop "edflag" []]); + ("endgrent", unknown ~attrs:[ThreadUnsafe] []); + ("endpwent", unknown ~attrs:[ThreadUnsafe] []); + ("fcvt", unknown ~attrs:[ThreadUnsafe] [drop "number" []; drop "ndigits" []; drop "decpt" [w]; drop "sign" [w]]); + ("gcvt", unknown ~attrs:[ThreadUnsafe] [drop "number" []; drop "ndigit" []; drop "buf" [w]]); + ("getdate", unknown ~attrs:[ThreadUnsafe] [drop "string" [r]]); + ("getenv", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); + ("getgrent", unknown ~attrs:[ThreadUnsafe] []); + ("getgrgid", unknown ~attrs:[ThreadUnsafe] [drop "gid" []]); + ("getgrnam", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); + ("getlogin", unknown ~attrs:[ThreadUnsafe] []); + ("getnetbyaddr", unknown ~attrs:[ThreadUnsafe] [drop "net" []; drop "type" []]); + ("getnetbyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); + ("getnetent", unknown ~attrs:[ThreadUnsafe] []); + ("getprotobyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); + ("getprotobynumber", unknown ~attrs:[ThreadUnsafe] [drop "proto" []]); + ("getprotoent", unknown ~attrs:[ThreadUnsafe] []); + ("getpwent", unknown ~attrs:[ThreadUnsafe] []); + ("getpwnam", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); + ("getpwuid", unknown ~attrs:[ThreadUnsafe] [drop "uid" []]); + ("getservbyname", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]; drop "proto" [r]]); + ("getservbyport", unknown ~attrs:[ThreadUnsafe] [drop "port" []; drop "proto" [r]]); + ("getservent", unknown ~attrs:[ThreadUnsafe] []); + ("getutxent", unknown ~attrs:[ThreadUnsafe] []); + ("getutxid", unknown ~attrs:[ThreadUnsafe] [drop "utmpx" [r_deep]]); + ("getutxline", unknown ~attrs:[ThreadUnsafe] [drop "utmpx" [r_deep]]); + ("pututxline", unknown ~attrs:[ThreadUnsafe] [drop "utmpx" [r_deep]]); + ("hcreate", unknown ~attrs:[ThreadUnsafe] [drop "nel" []]); + ("hdestroy", unknown ~attrs:[ThreadUnsafe] []); + ("hsearch", unknown ~attrs:[ThreadUnsafe] [drop "item" [r_deep]; drop "action" [r_deep]]); + ("l64a", unknown ~attrs:[ThreadUnsafe] [drop "value" []]); + ("lrand48", unknown ~attrs:[ThreadUnsafe] []); + ("mrand48", unknown ~attrs:[ThreadUnsafe] []); + ("nl_langinfo", unknown ~attrs:[ThreadUnsafe] [drop "item" []]); ("nl_langinfo_l", unknown [drop "item" []; drop "locale" [r_deep]]); - ("getc_unlocked", unknown [drop "stream" [w]]); - ("getchar_unlocked", unknown []); - ("putc_unlocked", unknown [drop "c" []; drop "stream" [w]]); - ("putchar_unlocked", unknown [drop "c" []]); + ("getc_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "stream" [r_deep; w_deep]]); + ("getchar_unlocked", unknown ~attrs:[ThreadUnsafe] []); + ("ptsname", unknown ~attrs:[ThreadUnsafe] [drop "fd" []]); + ("putc_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "c" []; drop "stream" [w]]); + ("putchar_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "c" []]); + ("putenv", unknown ~attrs:[ThreadUnsafe] [drop "string" [r; w]]); + ("readdir", unknown ~attrs:[ThreadUnsafe] [drop "dirp" [r_deep]]); + ("setenv", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]; drop "name" [r]; drop "overwrite" []]); + ("setgrent", unknown ~attrs:[ThreadUnsafe] []); + ("setpwent", unknown ~attrs:[ThreadUnsafe] []); + ("setutxent", unknown ~attrs:[ThreadUnsafe] []); + ("strerror", unknown ~attrs:[ThreadUnsafe] [drop "errnum" []]); + ("strsignal", unknown ~attrs:[ThreadUnsafe] [drop "sig" []]); + ("unsetenv", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); ("lseek", unknown [drop "fd" []; drop "offset" []; drop "whence" []]); ("fcntl", unknown (drop "fd" [] :: drop "cmd" [] :: VarArgs (drop' [r; w]))); ("fseeko", unknown [drop "stream" [r_deep; w_deep]; drop "offset" []; drop "whence" []]); ("fileno", unknown [drop "stream" [r_deep; w_deep]]); - ("getopt", unknown [drop "argc" []; drop "argv" [r]; drop "optstring" [r]]); + ("getopt", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r]; drop "optstring" [r]]); ("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]]); @@ -136,15 +200,16 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("alarm", unknown [drop "seconds" []]); ("pwrite", unknown [drop "fd" []; drop "buf" [r]; drop "count" []; drop "offset" []]); ("hstrerror", unknown [drop "err" []]); - ("inet_ntoa", unknown [drop "in" []]); + ("inet_ntoa", unknown ~attrs:[ThreadUnsafe] [drop "in" []]); ("getsockopt", unknown [drop "sockfd" []; drop "level" []; drop "optname" []; drop "optval" [w]; drop "optlen" [w]]); - ("gethostbyaddr", unknown [drop "addr" [r_deep]; drop "len" []; drop "type" []]); + ("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]]); ("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]]); ("access", unknown [drop "pathname" [r]; drop "mode" []]); - ("ttyname", unknown [drop "fd" []]); + ("ttyname", unknown ~attrs:[ThreadUnsafe] [drop "fd" []]); ("shm_open", unknown [drop "name" [r]; drop "oflag" []; drop "mode" []]); ("sched_get_priority_max", unknown [drop "policy" []]); ("mprotect", unknown [drop "addr" []; drop "len" []; drop "prot" []]); @@ -164,14 +229,15 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strtok_r", unknown [drop "str" [r; w]; drop "delim" [r]; drop "saveptr" [r_deep; w_deep]]); (* deep accesses through saveptr if str is NULL: https://github.com/lattera/glibc/blob/895ef79e04a953cac1493863bcae29ad85657ee1/string/strtok_r.c#L31-L40 *) ("kill", unknown [drop "pid" []; drop "sig" []]); ("closelog", unknown []); - ("dirname", unknown [drop "path" [r]]); + ("dirname", unknown ~attrs:[ThreadUnsafe] [drop "path" [r]]); + ("basename", unknown ~attrs:[ThreadUnsafe] [drop "path" [r]]); ("setpgid", unknown [drop "pid" []; drop "pgid" []]); ("dup2", unknown [drop "oldfd" []; drop "newfd" []]); ("pclose", unknown [drop "stream" [w; f]]); ("getcwd", unknown [drop "buf" [w]; drop "size" []]); ("inet_pton", unknown [drop "af" []; drop "src" [r]; drop "dst" [w]]); ("inet_ntop", unknown [drop "af" []; drop "src" [r]; drop "dst" [w]; drop "size" []]); - ("gethostent", unknown []); + ("gethostent", unknown ~attrs:[ThreadUnsafe] []); ("poll", unknown [drop "fds" [r]; drop "nfds" []; drop "timeout" []]); ("semget", unknown [drop "key" []; drop "nsems" []; drop "semflg" []]); ("semctl", unknown (drop "semid" [] :: drop "semnum" [] :: drop "cmd" [] :: VarArgs (drop "semun" [r_deep]))); @@ -304,6 +370,7 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("prctl", unknown (drop "option" [] :: VarArgs (drop' []))); (* man page has 5 arguments, but header has varargs and real-world programs may call with <5 *) ("__ctype_tolower_loc", unknown []); ("__ctype_toupper_loc", unknown []); + ("endutxent", unknown ~attrs:[ThreadUnsafe] []); ("epoll_create", unknown [drop "size" []]); ("epoll_ctl", unknown [drop "epfd" []; drop "op" []; drop "fd" []; drop "event" [w]]); ("epoll_wait", unknown [drop "epfd" []; drop "events" [w]; drop "maxevents" []; drop "timeout" []]); @@ -498,9 +565,9 @@ let math_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("ldexp", unknown [drop "arg" []; drop "exp" []]); ("ldexpf", unknown [drop "arg" []; drop "exp" []]); ("ldexpl", unknown [drop "arg" []; drop "exp" []]); - ("lgamma", unknown [drop "x" []]); - ("lgammaf", unknown [drop "x" []]); - ("lgammal", unknown [drop "x" []]); + ("lgamma", unknown ~attrs:[ThreadUnsafe] [drop "x" []]); + ("lgammaf", unknown ~attrs:[ThreadUnsafe] [drop "x" []]); + ("lgammal", unknown ~attrs:[ThreadUnsafe] [drop "x" []]); ("log", unknown [drop "x" []]); ("logf", unknown [drop "x" []]); ("logl", unknown [drop "x" []]); @@ -898,11 +965,9 @@ let invalidate_actions = [ "dlopen", readsAll;(*safe*) "dlsym", readsAll;(*safe*) "dlclose", readsAll;(*safe*) - "dlerror", readsAll;(*safe*) "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) "__builtin_strchr", readsAll;(*safe*) - "strtok", readsAll;(*safe*) "getpgrp", readsAll;(*safe*) "umount2", readsAll;(*safe*) "memchr", readsAll;(*safe*) @@ -944,8 +1009,6 @@ let invalidate_actions = [ "__h_errno_location", readsAll;(*safe*) "__fxstat", readsAll;(*safe*) "getuid", readsAll;(*safe*) - "strerror", readsAll;(*safe*) - "readdir", readsAll;(*safe*) "openlog", readsAll;(*safe*) "getdtablesize", readsAll;(*safe*) "umask", readsAll;(*safe*) @@ -971,15 +1034,12 @@ let invalidate_actions = [ "syslog", readsAll; (*safe*) "strcasecmp", readsAll; (*safe*) "strchr", readsAll; (*safe*) - "getservbyname", readsAll; (*safe*) "__error", readsAll; (*safe*) "__maskrune", writesAll; (*unsafe*) "inet_addr", readsAll; (*safe*) - "gethostbyname", readsAll; (*safe*) "setsockopt", readsAll; (*safe*) "listen", readsAll; (*safe*) "getsockname", writes [1;3]; (*keep [1;3]*) - "getenv", readsAll; (*safe*) "execl", readsAll; (*safe*) "select", writes [1;5]; (*keep [1;5]*) "accept", writesAll; (*keep [1]*) @@ -988,7 +1048,6 @@ let invalidate_actions = [ "timespec_get", writes [1]; "__tolower", readsAll; (*safe*) "signal", writesAll; (*unsafe*) - "strsignal", readsAll; "popen", readsAll; (*safe*) "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*) "BZ2_bzBuffToBuffDecompress", writes [3;4]; (*keep [3;4]*) @@ -1005,7 +1064,6 @@ let invalidate_actions = [ "sendto", writes [2;4]; (*keep [2;4]*) "recvfrom", writes [4;5]; (*keep [4;5]*) "srand", readsAll; (*safe*) - "rand", readsAll; (*safe*) "gethostname", writesAll; (*unsafe*) "fork", readsAll; (*safe*) "setrlimit", readsAll; (*safe*) From a42b9645785acc38d7aa93fb9757230368c627c0 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 13 Jun 2023 14:03:04 +0300 Subject: [PATCH 09/22] Convert all pthread functions to new specifications --- src/analyses/libraryFunctions.ml | 78 ++++++++++++++++---------------- 1 file changed, 38 insertions(+), 40 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 9b689b64ad..a9b1fafa40 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -251,15 +251,47 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *) ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *) + ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [w]]); ("pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond); ("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_cond_destroy", unknown [drop "cond" [f]]); ("pthread_mutexattr_settype", special [__ "attr" []; __ "type" []] @@ fun attr typ -> MutexAttrSetType {attr; typ}); ("pthread_mutex_init", special [__ "mutex" []; __ "attr" []] @@ fun mutex attr -> MutexInit {mutex; attr}); + ("pthread_mutex_destroy", unknown [drop "mutex" [f]]); + ("pthread_mutex_lock", special [__ "mutex" []] @@ fun mutex -> Lock {lock = mutex; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false}); + ("pthread_mutex_trylock", special [__ "mutex" []] @@ fun mutex -> Lock {lock = mutex; try_ = true; write = true; return_on_success = false}); + ("pthread_mutex_unlock", special [__ "mutex" []] @@ fun mutex -> Unlock mutex); + ("pthread_mutexattr_init", unknown [drop "attr" [w]]); + ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]); + ("pthread_rwlock_init", unknown [drop "rwlock" [w]; drop "attr" [w]]); + ("pthread_rwlock_destroy", unknown [drop "rwlock" [f]]); + ("pthread_rwlock_rdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true}); + ("pthread_rwlock_tryrdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true}); + ("pthread_rwlock_wrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true}); + ("pthread_rwlock_trywrlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = true; write = true; return_on_success = false}); + ("pthread_rwlock_unlock", special [__ "rwlock" []] @@ fun rwlock -> Unlock rwlock); + ("pthread_rwlockattr_init", unknown [drop "attr" [w]]); + ("pthread_rwlockattr_destroy", unknown [drop "attr" [f]]); + ("pthread_spin_init", unknown [drop "lock" []; drop "pshared" []]); + ("pthread_spin_destroy", unknown [drop "lock" [f]]); + ("pthread_spin_lock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true}); + ("pthread_spin_trylock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = true; write = true; return_on_success = false}); + ("pthread_spin_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); + ("pthread_attr_init", unknown [drop "attr" [w]]); ("pthread_attr_destroy", unknown [drop "attr" [f]]); + ("pthread_attr_getdetachstate", unknown [drop "attr" [r]; drop "detachstate" [r]]); + ("pthread_attr_setdetachstate", unknown [drop "attr" [w]; drop "detachstate" []]); + ("pthread_attr_getstacksize", unknown [drop "attr" [r]; drop "stacksize" [r]]); + ("pthread_attr_setstacksize", unknown [drop "attr" [w]; drop "stacksize" []]); + ("pthread_attr_getscope", unknown [drop "attr" [r]; drop "scope" [r]]); + ("pthread_attr_setscope", unknown [drop "attr" [w]; drop "scope" []]); + ("pthread_self", unknown []); + ("pthread_sigmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]); ("pthread_setspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []; drop "value" [w_deep]]); ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]); + ("pthread_key_create", unknown [drop "key" [w]; drop "destructor" [s]]); ("pthread_key_delete", unknown [drop "key" [f]]); ("pthread_cancel", unknown [drop "thread" []]); ("pthread_setcanceltype", unknown [drop "type" []; drop "oldtype" [w]]); @@ -753,24 +785,21 @@ let classify fn exps: categories = | "_spin_trylock" | "spin_trylock" | "mutex_trylock" | "_spin_trylock_irqsave" | "down_trylock" -> `Lock(true, true, true) - | "pthread_mutex_trylock" | "pthread_rwlock_trywrlock" | "pthread_spin_trylock" - -> `Lock (true, true, false) | "_spin_lock" | "_spin_lock_irqsave" | "_spin_lock_bh" | "down_write" | "mutex_lock" | "mutex_lock_interruptible" | "_write_lock" | "_raw_write_lock" - | "pthread_rwlock_wrlock" | "GetResource" | "_raw_spin_lock" + | "GetResource" | "_raw_spin_lock" | "_raw_spin_lock_flags" | "_raw_spin_lock_irqsave" | "_raw_spin_lock_irq" | "_raw_spin_lock_bh" - | "spin_lock" | "pthread_spin_lock" + | "spin_lock" -> `Lock (get_bool "sem.lock.fail", true, true) - | "pthread_mutex_lock" | "__pthread_mutex_lock" + | "__pthread_mutex_lock" -> `Lock (get_bool "sem.lock.fail", true, false) - | "pthread_rwlock_tryrdlock" | "pthread_rwlock_rdlock" | "_read_lock" | "_raw_read_lock" - | "down_read" + | "_read_lock" | "_raw_read_lock" | "down_read" -> `Lock (get_bool "sem.lock.fail", false, true) | "__raw_read_unlock" | "__raw_write_unlock" | "raw_spin_unlock" | "_spin_unlock" | "spin_unlock" | "_spin_unlock_irqrestore" | "_spin_unlock_bh" | "_raw_spin_unlock_bh" | "mutex_unlock" | "_write_unlock" | "_read_unlock" - | "pthread_mutex_unlock" | "__pthread_mutex_unlock" | "up_read" | "up_write" - | "up" | "pthread_spin_unlock" + | "__pthread_mutex_unlock" | "up_read" | "up_write" + | "up" -> `Unlock | x -> `Unknown x @@ -877,12 +906,6 @@ let invalidate_actions = [ "__printf_chk", readsAll;(*safe*) "printk", readsAll;(*safe*) "perror", readsAll;(*safe*) - "pthread_mutex_lock", readsAll;(*safe*) - "pthread_mutex_trylock", readsAll; - "pthread_mutex_unlock", readsAll;(*safe*) - "pthread_spin_lock", readsAll;(*safe*) - "pthread_spin_trylock", readsAll; - "pthread_spin_unlock", readsAll;(*safe*) "__pthread_mutex_lock", readsAll;(*safe*) "__pthread_mutex_trylock", readsAll; "__pthread_mutex_unlock", readsAll;(*safe*) @@ -894,11 +917,6 @@ let invalidate_actions = [ "_spin_lock", readsAll;(*safe*) "_spin_unlock", readsAll;(*safe*) "_spin_lock_irqsave", readsAll;(*safe*) - "pthread_mutex_destroy", readsAll;(*safe*) - "pthread_mutexattr_init", readsAll;(*safe*) - "pthread_spin_init", readsAll;(*safe*) - "pthread_spin_destroy", readsAll;(*safe*) - "pthread_self", readsAll;(*safe*) "read", writes [2];(*keep [2]*) "recv", writes [2];(*keep [2]*) "scanf", writesAllButFirst 1 readsAll;(*drop 1*) @@ -941,24 +959,13 @@ let invalidate_actions = [ "close", writesAll;(*unsafe*) "setsid", readsAll;(*safe*) "strerror_r", writesAll;(*unsafe*) - "pthread_attr_init", writesAll; (*unsafe*) - "pthread_attr_setdetachstate", writesAll;(*unsafe*) - "pthread_attr_setstacksize", writesAll;(*unsafe*) - "pthread_attr_setscope", writesAll;(*unsafe*) - "pthread_attr_getdetachstate", readsAll;(*safe*) - "pthread_attr_getstacksize", readsAll;(*safe*) - "pthread_attr_getscope", readsAll;(*safe*) - "pthread_cond_init", readsAll; (*safe*) - "pthread_cond_destroy", readsAll;(*safe*) "__pthread_cond_init", readsAll; (*safe*) "__pthread_cond_wait", readsAll; (*safe*) "__pthread_cond_signal", readsAll;(*safe*) "__pthread_cond_broadcast", readsAll;(*safe*) "__pthread_cond_destroy", readsAll;(*safe*) - "pthread_key_create", writesAll;(*unsafe*) "sigemptyset", writesAll;(*unsafe*) "sigaddset", writesAll;(*unsafe*) - "pthread_sigmask", writesAllButFirst 2 readsAll;(*unsafe*) "raise", writesAll;(*unsafe*) "_strlen", readsAll;(*safe*) "__builtin_alloca", readsAll;(*safe*) @@ -1080,15 +1087,6 @@ let invalidate_actions = [ "munmap", readsAll;(*safe*) "mmap", readsAll;(*safe*) "clock", readsAll; - "pthread_rwlock_wrlock", readsAll; - "pthread_rwlock_trywrlock", readsAll; - "pthread_rwlock_rdlock", readsAll; - "pthread_rwlock_tryrdlock", readsAll; - "pthread_rwlockattr_destroy", writesAll; - "pthread_rwlockattr_init", writesAll; - "pthread_rwlock_destroy", readsAll; - "pthread_rwlock_init", readsAll; - "pthread_rwlock_unlock", 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 8c44ac7d68850372dfe8ffa9693e5a381e1fca5a Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 13 Jun 2023 14:49:40 +0300 Subject: [PATCH 10/22] Convert linux kernel functions from classify to new specifications --- src/analyses/libraryFunctions.ml | 44 +++++++++++++++++--------------- 1 file changed, 23 insertions(+), 21 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index a9b1fafa40..3b3af35399 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -417,8 +417,24 @@ let console_sem = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[console (** Linux kernel functions. *) let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ + ("down_trylock", special [__ "sem" []] @@ fun sem -> Lock { lock = sem; try_ = true; write = true; return_on_success = true }); + ("down_read", special [__ "sem" []] @@ fun sem -> Lock { lock = sem; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true }); + ("down_write", special [__ "sem" []] @@ fun sem -> Lock { lock = sem; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("up", special [__ "sem" []] @@ fun sem -> Unlock sem); + ("up_read", special [__ "sem" []] @@ fun sem -> Unlock sem); + ("up_write", special [__ "sem" []] @@ fun sem -> Unlock sem); + ("mutex_init", unknown [drop "mutex" []]); + ("mutex_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("mutex_trylock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = true; write = true; return_on_success = true }); + ("mutex_lock_interruptible", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("mutex_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); + ("spin_lock_init", unknown [drop "lock" []]); + ("spin_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("spin_trylock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = true; write = true; return_on_success = true }); + ("spin_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); ("spin_lock_irqsave", special [__ "lock" []; drop "flags" []] @@ fun lock -> Lock { lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); ("spin_unlock_irqrestore", special [__ "lock" []; drop "flags" []] @@ fun lock -> Unlock lock); + ("raw_spin_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); ("_raw_spin_unlock_irqrestore", special [__ "lock" []; drop "flags" []] @@ fun lock -> Unlock lock); ("spinlock_check", special [__ "lock" []] @@ fun lock -> Identity lock); (* Identity, because we don't want lock internals. *) ("_lock_kernel", special [drop "func" [r]; drop "file" [r]; drop "line" []] @@ Lock { lock = big_kernel_lock; try_ = false; write = true; return_on_success = true }); @@ -782,24 +798,19 @@ let classify fn exps: categories = | n::size::_ -> `Calloc (n, size) | _ -> strange_arguments () end - | "_spin_trylock" | "spin_trylock" | "mutex_trylock" | "_spin_trylock_irqsave" - | "down_trylock" + | "_spin_trylock" | "_spin_trylock_irqsave" -> `Lock(true, true, true) - | "_spin_lock" | "_spin_lock_irqsave" | "_spin_lock_bh" | "down_write" - | "mutex_lock" | "mutex_lock_interruptible" | "_write_lock" | "_raw_write_lock" - | "GetResource" | "_raw_spin_lock" + | "_spin_lock" | "_spin_lock_irqsave" | "_spin_lock_bh" + | "_write_lock" | "_raw_write_lock" | "GetResource" | "_raw_spin_lock" | "_raw_spin_lock_flags" | "_raw_spin_lock_irqsave" | "_raw_spin_lock_irq" | "_raw_spin_lock_bh" - | "spin_lock" -> `Lock (get_bool "sem.lock.fail", true, true) | "__pthread_mutex_lock" -> `Lock (get_bool "sem.lock.fail", true, false) - | "_read_lock" | "_raw_read_lock" | "down_read" + | "_read_lock" | "_raw_read_lock" -> `Lock (get_bool "sem.lock.fail", false, true) - | "__raw_read_unlock" | "__raw_write_unlock" | "raw_spin_unlock" - | "_spin_unlock" | "spin_unlock" | "_spin_unlock_irqrestore" | "_spin_unlock_bh" | "_raw_spin_unlock_bh" - | "mutex_unlock" | "_write_unlock" | "_read_unlock" - | "__pthread_mutex_unlock" | "up_read" | "up_write" - | "up" + | "__raw_read_unlock" | "__raw_write_unlock" + | "_spin_unlock" | "_spin_unlock_irqrestore" | "_spin_unlock_bh" | "_raw_spin_unlock_bh" + | "_write_unlock" | "_read_unlock" | "__pthread_mutex_unlock" -> `Unlock | x -> `Unknown x @@ -910,10 +921,6 @@ let invalidate_actions = [ "__pthread_mutex_trylock", readsAll; "__pthread_mutex_unlock", readsAll;(*safe*) "__mutex_init", readsAll;(*safe*) - "mutex_init", readsAll;(*safe*) - "mutex_lock", readsAll;(*safe*) - "mutex_lock_interruptible", readsAll;(*safe*) - "mutex_unlock", readsAll;(*safe*) "_spin_lock", readsAll;(*safe*) "_spin_unlock", readsAll;(*safe*) "_spin_lock_irqsave", readsAll;(*safe*) @@ -1101,12 +1108,7 @@ let invalidate_actions = [ "setpriority", readsAll; "getpriority", readsAll; (* ddverify *) - "spin_lock_init", readsAll; - "spin_lock", readsAll; - "spin_unlock", readsAll; "sema_init", readsAll; - "down_trylock", readsAll; - "up", readsAll; "__goblint_assume_join", readsAll; ] From 2ef2e7f4cb2311c76e135435cccacfb61c9a00de Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 13 Jun 2023 14:51:27 +0300 Subject: [PATCH 11/22] Remove GetResource from libraryFunctions --- 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 3b3af35399..d0bb1edf53 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -801,7 +801,7 @@ let classify fn exps: categories = | "_spin_trylock" | "_spin_trylock_irqsave" -> `Lock(true, true, true) | "_spin_lock" | "_spin_lock_irqsave" | "_spin_lock_bh" - | "_write_lock" | "_raw_write_lock" | "GetResource" | "_raw_spin_lock" + | "_write_lock" | "_raw_write_lock" | "_raw_spin_lock" | "_raw_spin_lock_flags" | "_raw_spin_lock_irqsave" | "_raw_spin_lock_irq" | "_raw_spin_lock_bh" -> `Lock (get_bool "sem.lock.fail", true, true) | "__pthread_mutex_lock" From 30d5aea6ed99832d8b6cafac19ac9e924561adb5 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 13 Jun 2023 15:31:24 +0300 Subject: [PATCH 12/22] Convert most functions from classify to new specifications --- src/analyses/libraryFunctions.ml | 43 ++++++++++++++++++-------------- 1 file changed, 24 insertions(+), 19 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index d0bb1edf53..31ee8bc497 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -261,8 +261,10 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_mutex_init", special [__ "mutex" []; __ "attr" []] @@ fun mutex attr -> MutexInit {mutex; attr}); ("pthread_mutex_destroy", unknown [drop "mutex" [f]]); ("pthread_mutex_lock", special [__ "mutex" []] @@ fun mutex -> Lock {lock = mutex; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false}); + ("__pthread_mutex_lock", special [__ "mutex" []] @@ fun mutex -> Lock {lock = mutex; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false}); ("pthread_mutex_trylock", special [__ "mutex" []] @@ fun mutex -> Lock {lock = mutex; try_ = true; write = true; return_on_success = false}); ("pthread_mutex_unlock", special [__ "mutex" []] @@ fun mutex -> Unlock mutex); + ("__pthread_mutex_unlock", special [__ "mutex" []] @@ fun mutex -> Unlock mutex); ("pthread_mutexattr_init", unknown [drop "attr" [w]]); ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]); ("pthread_rwlock_init", unknown [drop "rwlock" [w]; drop "attr" [w]]); @@ -430,12 +432,34 @@ let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("mutex_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); ("spin_lock_init", unknown [drop "lock" []]); ("spin_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("_spin_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("_spin_lock_bh", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); ("spin_trylock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = true; write = true; return_on_success = true }); + ("_spin_trylock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = true; write = true; return_on_success = true }); ("spin_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); + ("_spin_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); + ("_spin_unlock_bh", special [__ "lock" []] @@ fun lock -> Unlock lock); ("spin_lock_irqsave", special [__ "lock" []; drop "flags" []] @@ fun lock -> Lock { lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("_spin_lock_irqsave", special [__ "lock" []] @@ fun lock -> Lock { lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("_spin_trylock_irqsave", special [__ "lock" []; drop "flags" []] @@ fun lock -> Lock { lock; try_ = true; write = true; return_on_success = true }); ("spin_unlock_irqrestore", special [__ "lock" []; drop "flags" []] @@ fun lock -> Unlock lock); + ("_spin_unlock_irqrestore", special [__ "lock" []; drop "flags" []] @@ fun lock -> Unlock lock); ("raw_spin_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); ("_raw_spin_unlock_irqrestore", special [__ "lock" []; drop "flags" []] @@ fun lock -> Unlock lock); + ("_raw_spin_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("_raw_spin_lock_flags", special [__ "lock" []; drop "flags" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("_raw_spin_lock_irqsave", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("_raw_spin_lock_irq", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("_raw_spin_lock_bh", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("_raw_spin_unlock_bh", special [__ "lock" []] @@ fun lock -> Unlock lock); + ("_read_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true }); + ("_read_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); + ("_raw_read_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true }); + ("__raw_read_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); + ("_write_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("_write_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); + ("_raw_write_lock", special [__ "lock" []] @@ fun lock -> Lock { lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true }); + ("__raw_write_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); ("spinlock_check", special [__ "lock" []] @@ fun lock -> Identity lock); (* Identity, because we don't want lock internals. *) ("_lock_kernel", special [drop "func" [r]; drop "file" [r]; drop "line" []] @@ Lock { lock = big_kernel_lock; try_ = false; write = true; return_on_success = true }); ("_unlock_kernel", special [drop "func" [r]; drop "file" [r]; drop "line" []] @@ Unlock big_kernel_lock); @@ -798,20 +822,6 @@ let classify fn exps: categories = | n::size::_ -> `Calloc (n, size) | _ -> strange_arguments () end - | "_spin_trylock" | "_spin_trylock_irqsave" - -> `Lock(true, true, true) - | "_spin_lock" | "_spin_lock_irqsave" | "_spin_lock_bh" - | "_write_lock" | "_raw_write_lock" | "_raw_spin_lock" - | "_raw_spin_lock_flags" | "_raw_spin_lock_irqsave" | "_raw_spin_lock_irq" | "_raw_spin_lock_bh" - -> `Lock (get_bool "sem.lock.fail", true, true) - | "__pthread_mutex_lock" - -> `Lock (get_bool "sem.lock.fail", true, false) - | "_read_lock" | "_raw_read_lock" - -> `Lock (get_bool "sem.lock.fail", false, true) - | "__raw_read_unlock" | "__raw_write_unlock" - | "_spin_unlock" | "_spin_unlock_irqrestore" | "_spin_unlock_bh" | "_raw_spin_unlock_bh" - | "_write_unlock" | "_read_unlock" | "__pthread_mutex_unlock" - -> `Unlock | x -> `Unknown x @@ -917,13 +927,8 @@ let invalidate_actions = [ "__printf_chk", readsAll;(*safe*) "printk", readsAll;(*safe*) "perror", readsAll;(*safe*) - "__pthread_mutex_lock", readsAll;(*safe*) "__pthread_mutex_trylock", readsAll; - "__pthread_mutex_unlock", readsAll;(*safe*) "__mutex_init", readsAll;(*safe*) - "_spin_lock", readsAll;(*safe*) - "_spin_unlock", readsAll;(*safe*) - "_spin_lock_irqsave", readsAll;(*safe*) "read", writes [2];(*keep [2]*) "recv", writes [2];(*keep [2]*) "scanf", writesAllButFirst 1 readsAll;(*drop 1*) From 01ce50483be81bf863e5284280a73bcebe49e389 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 13 Jun 2023 16:10:44 +0300 Subject: [PATCH 13/22] Convert all __pthread functions to new specifications --- 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 31ee8bc497..f2fd7e0d41 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -252,17 +252,23 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *) ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *) ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [w]]); + ("__pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [w]]); ("pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond); + ("__pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond); ("pthread_cond_broadcast", special [__ "cond" []] @@ fun cond -> Broadcast cond); + ("__pthread_cond_broadcast", special [__ "cond" []] @@ fun cond -> Broadcast cond); ("pthread_cond_wait", special [__ "cond" []; __ "mutex" []] @@ fun cond mutex -> Wait {cond; mutex}); + ("__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_cond_destroy", unknown [drop "cond" [f]]); + ("__pthread_cond_destroy", unknown [drop "cond" [f]]); ("pthread_mutexattr_settype", special [__ "attr" []; __ "type" []] @@ fun attr typ -> MutexAttrSetType {attr; typ}); ("pthread_mutex_init", special [__ "mutex" []; __ "attr" []] @@ fun mutex attr -> MutexInit {mutex; attr}); ("pthread_mutex_destroy", unknown [drop "mutex" [f]]); ("pthread_mutex_lock", special [__ "mutex" []] @@ fun mutex -> Lock {lock = mutex; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false}); ("__pthread_mutex_lock", special [__ "mutex" []] @@ fun mutex -> Lock {lock = mutex; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = false}); ("pthread_mutex_trylock", special [__ "mutex" []] @@ fun mutex -> Lock {lock = mutex; try_ = true; write = true; return_on_success = false}); + ("__pthread_mutex_trylock", special [__ "mutex" []] @@ fun mutex -> Lock {lock = mutex; try_ = true; write = true; return_on_success = false}); ("pthread_mutex_unlock", special [__ "mutex" []] @@ fun mutex -> Unlock mutex); ("__pthread_mutex_unlock", special [__ "mutex" []] @@ fun mutex -> Unlock mutex); ("pthread_mutexattr_init", unknown [drop "attr" [w]]); @@ -927,7 +933,6 @@ let invalidate_actions = [ "__printf_chk", readsAll;(*safe*) "printk", readsAll;(*safe*) "perror", readsAll;(*safe*) - "__pthread_mutex_trylock", readsAll; "__mutex_init", readsAll;(*safe*) "read", writes [2];(*keep [2]*) "recv", writes [2];(*keep [2]*) @@ -971,11 +976,6 @@ let invalidate_actions = [ "close", writesAll;(*unsafe*) "setsid", readsAll;(*safe*) "strerror_r", writesAll;(*unsafe*) - "__pthread_cond_init", readsAll; (*safe*) - "__pthread_cond_wait", readsAll; (*safe*) - "__pthread_cond_signal", readsAll;(*safe*) - "__pthread_cond_broadcast", readsAll;(*safe*) - "__pthread_cond_destroy", readsAll;(*safe*) "sigemptyset", writesAll;(*unsafe*) "sigaddset", writesAll;(*unsafe*) "raise", writesAll;(*unsafe*) From 6a1445ac56ddf7235ab74768067cd08a47e163a2 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Fri, 16 Jun 2023 19:06:43 +0300 Subject: [PATCH 14/22] Convert some more lib-funs to new specifications --- src/analyses/libraryFunctions.ml | 70 ++++++++++++++++---------------- 1 file changed, 35 insertions(+), 35 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index f2fd7e0d41..e3fce8718a 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -40,13 +40,18 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fgets", unknown [drop "str" [r; w]; drop "count" []; drop "stream" [r_deep; w_deep]]); ("fopen", unknown [drop "pathname" [r]; drop "mode" [r]]); ("fdopen", unknown [drop "fd" []; drop "mode" [r]]); + ("printf", unknown (drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) ("fprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) - ("fputc", unknown [drop "ch" []; drop "stream" [r_deep; w_deep];]); - ("fputs", unknown [drop "str" [r]; drop "stream" [r_deep; w_deep];]); + ("sprintf", unknown (drop "buffer" [r_deep; w_deep] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) + ("snprintf", unknown (drop "buffer" [r_deep; w_deep] :: drop "bufsz" [] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) + ("fputc", unknown [drop "ch" []; drop "stream" [r_deep; w_deep]]); + ("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_deep]; 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_deep]; 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_deep; w_deep]; drop "mode" []; drop "size" []]); (* TODO: if this is used to set an input buffer, the buffer (second argument) would need to remain TOP, *) (* as any future write (or flush) of the stream could result in a write to the buffer *) @@ -64,7 +69,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("abort", special [] Abort); ("exit", special [drop "exit_code" []] Abort); ("ungetc", unknown [drop "c" []; drop "stream" [r; w]]); - ("fscanf", unknown ((drop "stream" [r; w]) :: (drop "format" [r]) :: (VarArgs (drop' [w])))); + ("scanf", unknown ((drop "format" [r]) :: (VarArgs (drop' [w])))); + ("fscanf", unknown ((drop "stream" [r; w]) :: (drop "format" [r]) :: (VarArgs (drop' [w])))); (* TODO: why stream not r_deep; w_deep? *) + ("sscanf", unknown ((drop "buffer" [r]) :: (drop "format" [r]) :: (VarArgs (drop' [w])))); ("__freading", unknown [drop "stream" [r]]); ("mbsinit", unknown [drop "ps" [r]]); ("mbrtowc", unknown [drop "pwc" [w]; drop "s" [r]; drop "n" []; drop "ps" [r; w]]); @@ -72,17 +79,27 @@ 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];]); + ("perror", unknown [drop "s" [r]]); + ("getchar", unknown []); + ("putchar", unknown [drop "ch" []]); ("puts", unknown [drop "s" [r]]); ("rand", unknown ~attrs:[ThreadUnsafe] []); ("strspn", unknown [drop "s" [r]; drop "accept" [r]]); ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]); + ("strftime", unknown [drop "str" [w]; drop "count" []; drop "format" [r]; drop "tp" [r]]); ("strtod", unknown [drop "nptr" [r]; drop "endptr" [w]]); ("strtol", unknown [drop "nptr" [r]; drop "endptr" [w]; drop "base" []]); ("__strtol_internal", unknown [drop "nptr" [r]; drop "endptr" [w]; drop "base" []; drop "group" []]); ("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" []]); + ("tolower", unknown [drop "ch" []]); + ("toupper", unknown [drop "ch" []]); + ("time", unknown [drop "arg" [w]]); ("tmpnam", unknown ~attrs:[ThreadUnsafe] [drop "filename" [r]]); + ("vprintf", unknown [drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) + ("vfprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) + ("vsprintf", unknown [drop "buffer" [w]; drop "format" [r]; drop "vlist" [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]]); @@ -220,7 +237,22 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("timer_getoverrun", unknown [drop "timerid" []]); ("lstat", unknown [drop "pathname" [r]; drop "statbuf" [w]]); ("getpwnam", unknown [drop "name" [r]]); + ("chdir", unknown [drop "path" [r]]); + ("closedir", unknown [drop "dirp" [w]]); + ("mkdir", unknown [drop "pathname" [r]; drop "mode" []]); + ("opendir", unknown [drop "name" [r]]); + ("rmdir", unknown [drop "path" [r]]); + ("open", unknown (drop "pathname" [r] :: drop "flags" [] :: VarArgs (drop "mode" []))); + ("read", unknown [drop "fd" []; drop "buf" [w]; drop "count" []]); + ("write", unknown [drop "fd" []; drop "buf" [r]; drop "count" []]); + ("recv", unknown [drop "sockfd" []; drop "buf" [w]; drop "len" []; drop "flags" []]); + ("send", unknown [drop "sockfd" []; drop "buf" [r]; drop "len" []; drop "flags" []]); + ("strdup", unknown [drop "s" [r]]); ("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? *) + ("vsyslog", unknown [drop "priority" []; drop "format" [r]; drop "ap" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("freeaddrinfo", unknown [drop "res" [f_deep]]); ("getgid", unknown []); ("pselect", unknown [drop "nfds" []; drop "readdfs" [r]; drop "writedfs" [r]; drop "exceptfds" [r]; drop "timeout" [r]; drop "sigmask" [r]]); @@ -929,29 +961,11 @@ open Invalidate let invalidate_actions = [ "atoi", readsAll; (*safe*) "connect", readsAll; (*safe*) - "printf", readsAll;(*safe*) "__printf_chk", readsAll;(*safe*) "printk", readsAll;(*safe*) - "perror", readsAll;(*safe*) "__mutex_init", readsAll;(*safe*) - "read", writes [2];(*keep [2]*) - "recv", writes [2];(*keep [2]*) - "scanf", writesAllButFirst 1 readsAll;(*drop 1*) - "send", readsAll;(*safe*) - "snprintf", writes [1];(*keep [1]*) "__builtin___snprintf_chk", writes [1];(*keep [1]*) - "sprintf", writes [1];(*keep [1]*) - "sscanf", writesAllButFirst 2 readsAll;(*drop 2*) - "strftime", writes [1];(*keep [1]*) - "strdup", readsAll;(*safe*) - "toupper", readsAll;(*safe*) - "tolower", readsAll;(*safe*) - "time", writesAll;(*unsafe*) - "vfprintf", writes [1];(*keep [1]*) "__vfprintf_chk", writes [1];(*keep [1]*) - "vprintf", readsAll;(*safe*) - "vsprintf", writes [1];(*keep [1]*) - "write", readsAll;(*safe*) "__builtin_va_arg", readsAll;(*safe*) "__builtin_va_end", readsAll;(*safe*) "__builtin_va_start", readsAll;(*safe*) @@ -965,13 +979,10 @@ let invalidate_actions = [ "__strdup", readsAll;(*safe*) "strtoul__extinline", readsAll;(*safe*) "geteuid", readsAll;(*safe*) - "opendir", readsAll; (*safe*) "readdir_r", writesAll;(*unsafe*) "atoi__extinline", readsAll;(*safe*) "getpid", readsAll;(*safe*) "_IO_getc", writesAll;(*unsafe*) - "closedir", writesAll;(*unsafe*) - "chdir", readsAll;(*safe*) "pipe", writesAll;(*unsafe*) "close", writesAll;(*unsafe*) "setsid", readsAll;(*safe*) @@ -995,15 +1006,12 @@ let invalidate_actions = [ "__builtin___memmove_chk", writes [2;3];(*keep [2;3]*) "waitpid", readsAll;(*safe*) "statfs", writes [1;3;4];(*keep [1;3;4]*) - "mkdir", readsAll;(*safe*) "mount", readsAll;(*safe*) - "open", readsAll;(*safe*) "__open_alias", readsAll;(*safe*) "__open_2", readsAll;(*safe*) "ioctl", writesAll;(*unsafe*) "fstat__extinline", writesAll;(*unsafe*) "umount", readsAll;(*safe*) - "rmdir", readsAll;(*safe*) "strrchr", readsAll;(*safe*) "scandir", writes [1;3;4];(*keep [1;3;4]*) "unlink", readsAll;(*safe*) @@ -1015,15 +1023,8 @@ let invalidate_actions = [ "bindtextdomain", readsAll;(*safe*) "textdomain", readsAll;(*safe*) "dcgettext", readsAll;(*safe*) - "syscall", writesAllButFirst 1 readsAll;(*drop 1*) - "sysconf", readsAll; - "rewind", writesAll; - "putc", readsAll;(*safe*) "putw", readsAll;(*safe*) - "putchar", readsAll;(*safe*) - "getchar", readsAll;(*safe*) "__getdelim", writes [3];(*keep [3]*) - "vsyslog", readsAll;(*safe*) "gethostbyname_r", readsAll;(*safe*) "__h_errno_location", readsAll;(*safe*) "__fxstat", readsAll;(*safe*) @@ -1050,7 +1051,6 @@ let invalidate_actions = [ "vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) - "syslog", readsAll; (*safe*) "strcasecmp", readsAll; (*safe*) "strchr", readsAll; (*safe*) "__error", readsAll; (*safe*) From 2d5604657c5d3e48a3827ae56fca3c5c0d02b10f Mon Sep 17 00:00:00 2001 From: karoliineh Date: Fri, 28 Jul 2023 15:57:25 +0300 Subject: [PATCH 15/22] Convert memmove library functions. fixes #1121 --- src/analyses/libraryFunctions.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index e3fce8718a..3cd3b308cd 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -17,6 +17,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); ("mempcpy", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []]); ("__builtin___mempcpy_chk", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []; drop "os" []]); + ("memmove", unknown [drop "dest" [w]; drop "src" [r]; drop "count" []]); + ("__builtin_memmove", unknown [drop "dest" [w]; drop "src" [r]; drop "count" []]); + ("__builtin___memmove_chk", unknown [drop "dest" [w]; drop "src" [r]; drop "count" []]); ("strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin_strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin___strcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "os" []] @@ fun dest src -> Strcpy { dest; src; n = None; }); @@ -1001,9 +1004,6 @@ let invalidate_actions = [ "getpgrp", readsAll;(*safe*) "umount2", readsAll;(*safe*) "memchr", readsAll;(*safe*) - "memmove", writes [2;3];(*keep [2;3]*) - "__builtin_memmove", writes [2;3];(*keep [2;3]*) - "__builtin___memmove_chk", writes [2;3];(*keep [2;3]*) "waitpid", readsAll;(*safe*) "statfs", writes [1;3;4];(*keep [1;3;4]*) "mount", readsAll;(*safe*) From fe2cdffb4849be983ebce91a81d48bbd224868c0 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 1 Aug 2023 14:47:19 +0300 Subject: [PATCH 16/22] Add missing argument to __builtin___memmove_chk --- 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 3cd3b308cd..8d809ba46a 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -19,7 +19,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin___mempcpy_chk", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []; drop "os" []]); ("memmove", unknown [drop "dest" [w]; drop "src" [r]; drop "count" []]); ("__builtin_memmove", unknown [drop "dest" [w]; drop "src" [r]; drop "count" []]); - ("__builtin___memmove_chk", unknown [drop "dest" [w]; drop "src" [r]; drop "count" []]); + ("__builtin___memmove_chk", unknown [drop "dest" [w]; drop "src" [r]; drop "count" []; drop "os" []]); ("strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin_strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin___strcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "os" []] @@ fun dest src -> Strcpy { dest; src; n = None; }); From 1f53318999d3d1d425ed68fdf680dd68151e2d9c Mon Sep 17 00:00:00 2001 From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com> Date: Wed, 2 Aug 2023 15:03:26 +0300 Subject: [PATCH 17/22] Apply suggestions from code review Co-authored-by: Simmo Saan --- src/analyses/libraryFunctions.ml | 54 ++++++++++++++++---------------- 1 file changed, 27 insertions(+), 27 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 8d809ba46a..242c3f37fd 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -40,22 +40,22 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fflush", unknown [drop "stream" [r_deep; w_deep]]); ("fgetc", unknown [drop "stream" [r_deep; w_deep]]); ("getc", unknown [drop "stream" [r_deep; w_deep]]); - ("fgets", unknown [drop "str" [r; w]; drop "count" []; drop "stream" [r_deep; w_deep]]); + ("fgets", unknown [drop "str" [w]; drop "count" []; drop "stream" [r_deep; w_deep]]); ("fopen", unknown [drop "pathname" [r]; drop "mode" [r]]); ("fdopen", unknown [drop "fd" []; drop "mode" [r]]); ("printf", unknown (drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) ("fprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) - ("sprintf", unknown (drop "buffer" [r_deep; w_deep] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) - ("snprintf", unknown (drop "buffer" [r_deep; w_deep] :: drop "bufsz" [] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) + ("sprintf", unknown (drop "buffer" [w] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) + ("snprintf", unknown (drop "buffer" [w] :: drop "bufsz" [] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) ("fputc", unknown [drop "ch" []; drop "stream" [r_deep; w_deep]]); ("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_deep]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); + ("fread", unknown [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_deep]; drop "size" []; drop "count" []; drop "stream" [r_deep; w_deep]]); + ("fwrite", 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_deep; w_deep]; drop "mode" []; drop "size" []]); + ("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, *) (* as any future write (or flush) of the stream could result in a write to the buffer *) ("gmtime", unknown ~attrs:[ThreadUnsafe] [drop "timer" [r_deep]]); @@ -64,7 +64,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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]; drop "delim" [r]]); + ("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; }); ("malloc", special [__ "size" []] @@ fun size -> Malloc size); @@ -73,7 +73,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("exit", special [drop "exit_code" []] Abort); ("ungetc", unknown [drop "c" []; drop "stream" [r; w]]); ("scanf", unknown ((drop "format" [r]) :: (VarArgs (drop' [w])))); - ("fscanf", unknown ((drop "stream" [r; w]) :: (drop "format" [r]) :: (VarArgs (drop' [w])))); (* TODO: why stream not r_deep; w_deep? *) + ("fscanf", unknown ((drop "stream" [r_deep; w_deep]) :: (drop "format" [r]) :: (VarArgs (drop' [w])))); ("sscanf", unknown ((drop "buffer" [r]) :: (drop "format" [r]) :: (VarArgs (drop' [w])))); ("__freading", unknown [drop "stream" [r]]); ("mbsinit", unknown [drop "ps" [r]]); @@ -99,7 +99,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("tolower", unknown [drop "ch" []]); ("toupper", unknown [drop "ch" []]); ("time", unknown [drop "arg" [w]]); - ("tmpnam", unknown ~attrs:[ThreadUnsafe] [drop "filename" [r]]); + ("tmpnam", unknown ~attrs:[ThreadUnsafe] [drop "filename" [w]]); ("vprintf", unknown [drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("vfprintf", unknown [drop "stream" [r_deep; w_deep]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) ("vsprintf", unknown [drop "buffer" [w]; drop "format" [r]; drop "vlist" [r_deep]]); (* TODO: what to do with a va_list type? is r_deep correct? *) @@ -112,7 +112,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("difftime", unknown [drop "time1" []; drop "time2" []]); ("system", unknown ~attrs:[ThreadUnsafe] [drop "command" [r]]); ("wcscat", unknown [drop "dest" [r; w]; drop "src" [r]]); - ("wcrtomb", unknown ~attrs:[ThreadUnsafe] [drop "s" [r]; drop "wc" []; drop "ps" [w_deep]]); + ("wcrtomb", unknown ~attrs:[ThreadUnsafe] [drop "s" [w]; drop "wc" []; drop "ps" [r_deep; w_deep]]); ("abs", unknown [drop "j" []]); ("localtime_r", unknown [drop "timep" [r]; drop "result" [w]]); ("strpbrk", unknown [drop "s" [r]; drop "accept" [r]]); @@ -128,9 +128,9 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__builtin_bzero", special [__ "dest" [w]; __ "count" []] @@ fun dest count -> Bzero { dest; count; }); ("explicit_bzero", special [__ "dest" [w]; __ "count" []] @@ fun dest count -> Bzero { dest; count; }); ("__explicit_bzero_chk", special [__ "dest" [w]; __ "count" []; drop "os" []] @@ fun dest count -> Bzero { dest; count; }); - ("catgets", unknown ~attrs:[ThreadUnsafe] [drop "catalog" [r_deep]; drop "set_number" []; drop "message_number" []; drop "message" [r_deep]]); + ("catgets", unknown ~attrs:[ThreadUnsafe] [drop "catalog" [r_deep]; drop "set_number" []; drop "message_number" []; drop "message" [r]]); ("crypt", unknown ~attrs:[ThreadUnsafe] [drop "key" [r]; drop "salt" [r]]); - ("ctermid", unknown ~attrs:[ThreadUnsafe] [drop "s" [r]]); + ("ctermid", unknown ~attrs:[ThreadUnsafe] [drop "s" [w]]); ("dbm_clearerr", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep; w_deep]]); ("dbm_close", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep; w_deep; f_deep]]); ("dbm_delete", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep; w_deep]; drop "key" []]); @@ -138,7 +138,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("dbm_fetch", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep]; drop "key" []]); ("dbm_firstkey", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep]]); ("dbm_nextkey", unknown ~attrs:[ThreadUnsafe] [drop "db" [r_deep]]); - ("dbm_open", unknown ~attrs:[ThreadUnsafe] [drop "file" [r_deep; w_deep]; drop "open_flags" []; drop "file_mode" []]); + ("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] []); @@ -180,7 +180,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getc_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "stream" [r_deep; w_deep]]); ("getchar_unlocked", unknown ~attrs:[ThreadUnsafe] []); ("ptsname", unknown ~attrs:[ThreadUnsafe] [drop "fd" []]); - ("putc_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "c" []; drop "stream" [w]]); + ("putc_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "c" []; drop "stream" [r_deep; w_deep]]); ("putchar_unlocked", unknown ~attrs:[ThreadUnsafe] [drop "c" []]); ("putenv", unknown ~attrs:[ThreadUnsafe] [drop "string" [r; w]]); ("readdir", unknown ~attrs:[ThreadUnsafe] [drop "dirp" [r_deep]]); @@ -195,7 +195,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("fcntl", unknown (drop "fd" [] :: drop "cmd" [] :: VarArgs (drop' [r; w]))); ("fseeko", unknown [drop "stream" [r_deep; w_deep]; drop "offset" []; drop "whence" []]); ("fileno", unknown [drop "stream" [r_deep; w_deep]]); - ("getopt", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r]; drop "optstring" [r]]); + ("getopt", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r_deep]; drop "optstring" [r]]); ("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]]); @@ -241,7 +241,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("lstat", unknown [drop "pathname" [r]; drop "statbuf" [w]]); ("getpwnam", unknown [drop "name" [r]]); ("chdir", unknown [drop "path" [r]]); - ("closedir", unknown [drop "dirp" [w]]); + ("closedir", unknown [drop "dirp" [r]]); ("mkdir", unknown [drop "pathname" [r]; drop "mode" []]); ("opendir", unknown [drop "name" [r]]); ("rmdir", unknown [drop "path" [r]]); @@ -286,8 +286,8 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_create", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* For precision purposes arg is not considered accessed here. Instead all accesses (if any) come from actually analyzing start_routine. *) ("pthread_exit", special [__ "retval" []] @@ fun retval -> ThreadExit { ret_val = retval }); (* Doesn't dereference the void* itself, but just passes to pthread_join. *) - ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [w]]); - ("__pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [w]]); + ("pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]); + ("__pthread_cond_init", unknown [drop "cond" [w]; drop "attr" [r]]); ("pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond); ("__pthread_cond_signal", special [__ "cond" []] @@ fun cond -> Signal cond); ("pthread_cond_broadcast", special [__ "cond" []] @@ fun cond -> Broadcast cond); @@ -308,7 +308,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__pthread_mutex_unlock", special [__ "mutex" []] @@ fun mutex -> Unlock mutex); ("pthread_mutexattr_init", unknown [drop "attr" [w]]); ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]); - ("pthread_rwlock_init", unknown [drop "rwlock" [w]; drop "attr" [w]]); + ("pthread_rwlock_init", unknown [drop "rwlock" [w]; drop "attr" [r]]); ("pthread_rwlock_destroy", unknown [drop "rwlock" [f]]); ("pthread_rwlock_rdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true}); ("pthread_rwlock_tryrdlock", special [__ "rwlock" []] @@ fun rwlock -> Lock {lock = rwlock; try_ = get_bool "sem.lock.fail"; write = false; return_on_success = true}); @@ -317,18 +317,18 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_rwlock_unlock", special [__ "rwlock" []] @@ fun rwlock -> Unlock rwlock); ("pthread_rwlockattr_init", unknown [drop "attr" [w]]); ("pthread_rwlockattr_destroy", unknown [drop "attr" [f]]); - ("pthread_spin_init", unknown [drop "lock" []; drop "pshared" []]); + ("pthread_spin_init", unknown [drop "lock" [w]; drop "pshared" []]); ("pthread_spin_destroy", unknown [drop "lock" [f]]); ("pthread_spin_lock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true}); ("pthread_spin_trylock", special [__ "lock" []] @@ fun lock -> Lock {lock = lock; try_ = true; write = true; return_on_success = false}); ("pthread_spin_unlock", special [__ "lock" []] @@ fun lock -> Unlock lock); ("pthread_attr_init", unknown [drop "attr" [w]]); ("pthread_attr_destroy", unknown [drop "attr" [f]]); - ("pthread_attr_getdetachstate", unknown [drop "attr" [r]; drop "detachstate" [r]]); + ("pthread_attr_getdetachstate", unknown [drop "attr" [r]; drop "detachstate" [w]]); ("pthread_attr_setdetachstate", unknown [drop "attr" [w]; drop "detachstate" []]); - ("pthread_attr_getstacksize", unknown [drop "attr" [r]; drop "stacksize" [r]]); + ("pthread_attr_getstacksize", unknown [drop "attr" [r]; drop "stacksize" [w]]); ("pthread_attr_setstacksize", unknown [drop "attr" [w]; drop "stacksize" []]); - ("pthread_attr_getscope", unknown [drop "attr" [r]; drop "scope" [r]]); + ("pthread_attr_getscope", unknown [drop "attr" [r]; drop "scope" [w]]); ("pthread_attr_setscope", unknown [drop "attr" [w]; drop "scope" []]); ("pthread_self", unknown []); ("pthread_sigmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]); @@ -408,10 +408,10 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("euidaccess", unknown [drop "pathname" [r]; drop "mode" []]); ("rpmatch", unknown [drop "response" [r]]); ("getpagesize", unknown []); - ("__fgets_alias", unknown [drop "__s" [r; w]; drop "__n" []; drop "__stream" [r_deep; w_deep]]); - ("__fgets_chk", unknown [drop "__s" [r; w]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); - ("__fread_alias", unknown [drop "__ptr" [w_deep]; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); - ("__fread_chk", unknown [drop "__ptr" [w_deep]; drop "__ptrlen" []; drop "__size" []; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("__fgets_alias", unknown [drop "__s" [w]; drop "__n" []; drop "__stream" [r_deep; w_deep]]); + ("__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]]); ("__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 5c8bcfbf2b270acca278db4cd8b2094b6a3693d3 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Wed, 2 Aug 2023 15:20:46 +0300 Subject: [PATCH 18/22] Implement comments from code review --- src/analyses/libraryFunctions.ml | 39 ++++++++++++++++---------------- 1 file changed, 19 insertions(+), 20 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 242c3f37fd..2de54f9660 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -15,11 +15,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); ("__builtin_memcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); ("__builtin___memcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); - ("mempcpy", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []]); - ("__builtin___mempcpy_chk", unknown [drop "dest" [w]; drop "src" [r]; drop "n" []; drop "os" []]); - ("memmove", unknown [drop "dest" [w]; drop "src" [r]; drop "count" []]); - ("__builtin_memmove", unknown [drop "dest" [w]; drop "src" [r]; drop "count" []]); - ("__builtin___memmove_chk", unknown [drop "dest" [w]; drop "src" [r]; drop "count" []; drop "os" []]); + ("memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src }); + ("__builtin_memmove", special [__ "dest" [w]; __ "src" [r]; drop "count" []] @@ fun dest src -> Memcpy { dest; src }); + ("__builtin___memmove_chk", special [__ "dest" [w]; __ "src" [r]; drop "count" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); ("strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin_strcpy", special [__ "dest" [w]; __ "src" [r]] @@ fun dest src -> Strcpy { dest; src; n = None; }); ("__builtin___strcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "os" []] @@ fun dest src -> Strcpy { dest; src; n = None; }); @@ -33,20 +31,15 @@ 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; }); ("asctime", unknown ~attrs:[ThreadUnsafe] [drop "time_ptr" [r_deep]]); - ("free", unknown [drop "ptr" [f]]); ("fclose", unknown [drop "stream" [r_deep; w_deep; f_deep]]); ("feof", unknown [drop "stream" [r_deep; w_deep]]); ("ferror", 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]]); - ("fgets", unknown [drop "str" [w]; drop "count" []; drop "stream" [r_deep; w_deep]]); - ("fopen", unknown [drop "pathname" [r]; drop "mode" [r]]); - ("fdopen", unknown [drop "fd" []; drop "mode" [r]]); - ("printf", unknown (drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) - ("fprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) - ("sprintf", unknown (drop "buffer" [w] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) - ("snprintf", unknown (drop "buffer" [w] :: drop "bufsz" [] :: drop "format" [r] :: VarArgs (drop' []))); (* TODO: why not r for VarArgs?*) + ("printf", unknown (drop "format" [r] :: VarArgs (drop' [r]))); + ("fprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "format" [r] :: VarArgs (drop' [r]))); + ("sprintf", unknown (drop "buffer" [w] :: drop "format" [r] :: VarArgs (drop' [r]))); + ("snprintf", unknown (drop "buffer" [w] :: drop "bufsz" [] :: drop "format" [r] :: VarArgs (drop' [r]))); ("fputc", unknown [drop "ch" []; drop "stream" [r_deep; w_deep]]); ("putc", unknown [drop "ch" []; drop "stream" [r_deep; w_deep]]); ("fputs", unknown [drop "str" [r]; drop "stream" [r_deep; w_deep]]); @@ -87,6 +80,10 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("putchar", unknown [drop "ch" []]); ("puts", unknown [drop "s" [r]]); ("rand", unknown ~attrs:[ThreadUnsafe] []); + ("setgrent", unknown ~attrs:[ThreadUnsafe] []); + ("setpwent", unknown ~attrs:[ThreadUnsafe] []); + ("setutxent", unknown ~attrs:[ThreadUnsafe] []); + ("strerror", unknown ~attrs:[ThreadUnsafe] [drop "errnum" []]); ("strspn", unknown [drop "s" [r]; drop "accept" [r]]); ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]); ("strftime", unknown [drop "str" [w]; drop "count" []; drop "format" [r]; drop "tp" [r]]); @@ -107,7 +104,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("ctime", unknown ~attrs:[ThreadUnsafe] [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' []))); + ("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" []]); ("system", unknown ~attrs:[ThreadUnsafe] [drop "command" [r]]); @@ -185,16 +182,16 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("putenv", unknown ~attrs:[ThreadUnsafe] [drop "string" [r; w]]); ("readdir", unknown ~attrs:[ThreadUnsafe] [drop "dirp" [r_deep]]); ("setenv", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]; drop "name" [r]; drop "overwrite" []]); - ("setgrent", unknown ~attrs:[ThreadUnsafe] []); - ("setpwent", unknown ~attrs:[ThreadUnsafe] []); - ("setutxent", unknown ~attrs:[ThreadUnsafe] []); - ("strerror", unknown ~attrs:[ThreadUnsafe] [drop "errnum" []]); ("strsignal", unknown ~attrs:[ThreadUnsafe] [drop "sig" []]); ("unsetenv", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); ("lseek", unknown [drop "fd" []; drop "offset" []; drop "whence" []]); ("fcntl", unknown (drop "fd" [] :: drop "cmd" [] :: VarArgs (drop' [r; w]))); ("fseeko", unknown [drop "stream" [r_deep; w_deep]; drop "offset" []; drop "whence" []]); ("fileno", unknown [drop "stream" [r_deep; w_deep]]); + ("fgets", unknown [drop "str" [w]; drop "count" []; drop "stream" [r_deep; w_deep]]); + ("fopen", unknown [drop "pathname" [r]; drop "mode" [r]]); + ("fdopen", unknown [drop "fd" []; drop "mode" [r]]); + ("getc", unknown [drop "stream" [r_deep; w_deep]]); ("getopt", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r_deep]; drop "optstring" [r]]); ("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]]); @@ -438,6 +435,8 @@ let glibc_desc_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("strcasestr", unknown [drop "haystack" [r]; drop "needle" [r]]); ("inet_aton", unknown [drop "cp" [r]; drop "inp" [w]]); ("fopencookie", unknown [drop "cookie" []; drop "mode" [r]; drop "io_funcs" [s_deep]]); (* doesn't access cookie but passes it to io_funcs *) + ("mempcpy", special [__ "dest" [w]; __ "src" [r]; drop "n" []] @@ fun dest src -> Memcpy { dest; src }); + ("__builtin___mempcpy_chk", special [__ "dest" [w]; __ "src" [r]; drop "n" []; drop "os" []] @@ fun dest src -> Memcpy { dest; src }); ] let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ @@ -449,7 +448,7 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("epoll_create", unknown [drop "size" []]); ("epoll_ctl", unknown [drop "epfd" []; drop "op" []; drop "fd" []; drop "event" [w]]); ("epoll_wait", unknown [drop "epfd" []; drop "events" [w]; drop "maxevents" []; drop "timeout" []]); - ("__fprintf_chk", unknown [drop "stream" [r_deep; w_deep]; drop "flag" []; drop "format" [r]]); + ("__fprintf_chk", unknown (drop "stream" [r_deep; w_deep] :: drop "flag" [] :: drop "format" [r] :: VarArgs (drop' [r]))); ("sysinfo", unknown [drop "info" [w_deep]]); ("__xpg_basename", unknown [drop "path" [r]]); ("ptrace", unknown (drop "request" [] :: VarArgs (drop' [r_deep; w_deep]))); (* man page has 4 arguments, but header has varargs and real-world programs may call with <4 *) From f2fd9b5e5bdebc92631088c22e6b43401903b85f Mon Sep 17 00:00:00 2001 From: Karoliine Holter <44437975+karoliineh@users.noreply.github.com> Date: Wed, 2 Aug 2023 22:32:05 +0300 Subject: [PATCH 19/22] Update src/analyses/libraryFunctions.ml 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 3accc6d2e8..d49800f33a 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -141,7 +141,7 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("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" []; drop "edflag" []]); + ("encrypt", unknown ~attrs:[ThreadUnsafe] [drop "block" [r; w]; drop "edflag" []]); ("endgrent", unknown ~attrs:[ThreadUnsafe] []); ("endpwent", unknown ~attrs:[ThreadUnsafe] []); ("fcvt", unknown ~attrs:[ThreadUnsafe] [drop "number" []; drop "ndigits" []; drop "decpt" [w]; drop "sign" [w]]); From ab339c5e5fdaf68cd4e7a836adfc1ff720e79bd6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 3 Aug 2023 11:26:40 +0300 Subject: [PATCH 20/22] Move back accidentally moved library functions --- 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 d49800f33a..bb3517a755 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -36,6 +36,9 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("ferror", 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]]); + ("fgets", unknown [drop "str" [w]; drop "count" []; drop "stream" [r_deep; w_deep]]); + ("fopen", unknown [drop "pathname" [r]; drop "mode" [r]]); ("printf", unknown (drop "format" [r] :: VarArgs (drop' [r]))); ("fprintf", unknown (drop "stream" [r_deep; w_deep] :: drop "format" [r] :: VarArgs (drop' [r]))); ("sprintf", unknown (drop "buffer" [w] :: drop "format" [r] :: VarArgs (drop' [r]))); @@ -81,9 +84,6 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("putchar", unknown [drop "ch" []]); ("puts", unknown [drop "s" [r]]); ("rand", unknown ~attrs:[ThreadUnsafe] []); - ("setgrent", unknown ~attrs:[ThreadUnsafe] []); - ("setpwent", unknown ~attrs:[ThreadUnsafe] []); - ("setutxent", unknown ~attrs:[ThreadUnsafe] []); ("strerror", unknown ~attrs:[ThreadUnsafe] [drop "errnum" []]); ("strspn", unknown [drop "s" [r]; drop "accept" [r]]); ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]); @@ -184,16 +184,16 @@ let posix_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("putenv", unknown ~attrs:[ThreadUnsafe] [drop "string" [r; w]]); ("readdir", unknown ~attrs:[ThreadUnsafe] [drop "dirp" [r_deep]]); ("setenv", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]; drop "name" [r]; drop "overwrite" []]); + ("setgrent", unknown ~attrs:[ThreadUnsafe] []); + ("setpwent", unknown ~attrs:[ThreadUnsafe] []); + ("setutxent", unknown ~attrs:[ThreadUnsafe] []); ("strsignal", unknown ~attrs:[ThreadUnsafe] [drop "sig" []]); ("unsetenv", unknown ~attrs:[ThreadUnsafe] [drop "name" [r]]); ("lseek", unknown [drop "fd" []; drop "offset" []; drop "whence" []]); ("fcntl", unknown (drop "fd" [] :: drop "cmd" [] :: VarArgs (drop' [r; w]))); ("fseeko", unknown [drop "stream" [r_deep; w_deep]; drop "offset" []; drop "whence" []]); ("fileno", unknown [drop "stream" [r_deep; w_deep]]); - ("fgets", unknown [drop "str" [w]; drop "count" []; drop "stream" [r_deep; w_deep]]); - ("fopen", unknown [drop "pathname" [r]; drop "mode" [r]]); ("fdopen", unknown [drop "fd" []; drop "mode" [r]]); - ("getc", unknown [drop "stream" [r_deep; w_deep]]); ("getopt", unknown ~attrs:[ThreadUnsafe] [drop "argc" []; drop "argv" [r_deep]; drop "optstring" [r]]); ("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]]); From 2267095562e397f4ee9400e5f45dd639cfae8933 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 3 Aug 2023 11:27:12 +0300 Subject: [PATCH 21/22] Remove LibraryFunctions trailing whitespace, fix one VarArgs --- src/analyses/libraryFunctions.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index bb3517a755..447263b3ef 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -51,7 +51,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("ftell", unknown [drop "stream" [r_deep]]); ("fwrite", 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" []]); + ("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, *) (* as any future write (or flush) of the stream could result in a write to the buffer *) ("gmtime", unknown ~attrs:[ThreadUnsafe] [drop "timer" [r_deep]]); @@ -364,7 +364,7 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("__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 *) ("__builtin_return_address", unknown [drop "level" []]); - ("__builtin___sprintf_chk", unknown (drop "s" [w] :: drop "flag" [] :: drop "os" [] :: drop "fmt" [r] :: VarArgs (drop' []))); + ("__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]]); ("__builtin_sadd_overflow", unknown [drop "a" []; drop "b" []; drop "c" [w]]); ("__builtin_saddl_overflow", unknown [drop "a" []; drop "b" []; drop "c" [w]]); @@ -1119,7 +1119,7 @@ let invalidate_actions = [ ] let () = List.iter (fun (x, _) -> - if Hashtbl.exists (fun _ b -> List.mem_assoc x b) libraries then + if Hashtbl.exists (fun _ b -> List.mem_assoc x b) libraries then failwith ("You have added a function to invalidate_actions that already exists in libraries. Please undo this for function: " ^ x); ) invalidate_actions From ed231fa346bb8c4abbfd17c4c31cdbb77b4e316a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 3 Aug 2023 11:46:31 +0300 Subject: [PATCH 22/22] Fix access analysis to not dereference non-pointer types --- src/analyses/accessAnalysis.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index 5245e4adfe..bc5330726c 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -44,7 +44,7 @@ struct let access_one_top ?(force=false) ?(deref=false) ctx (kind: AccessKind.t) reach exp = if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)\n" CilType.Exp.pretty exp AccessKind.pretty kind reach deref; if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) then ( - if deref then + if deref && Cil.isPointerType (Cilfacade.typeOf exp) then (* avoid dereferencing integers to unknown pointers, which cause many spurious type-based accesses *) do_access ctx kind reach exp; if M.tracing then M.tracei "access" "distribute_access_exp\n"; Access.distribute_access_exp (do_access ctx Read false) exp;