diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index f4a9ac803d..5dc311a587 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -84,7 +84,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("getchar", unknown []); ("putchar", unknown [drop "ch" []]); ("puts", unknown [drop "s" [r]]); - ("rand", unknown ~attrs:[ThreadUnsafe] []); + ("rand", special ~attrs:[ThreadUnsafe] [] Rand); ("strerror", unknown ~attrs:[ThreadUnsafe] [drop "errnum" []]); ("strspn", unknown [drop "s" [r]; drop "accept" [r]]); ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]); @@ -118,7 +118,6 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *) ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value }); - ("rand", special [] Rand); ] (** C POSIX library functions. @@ -890,70 +889,70 @@ struct let writesAllButFirst n f a x = match a with - | Write | Spawn -> f a x @ drop n x + | Write | Call | Spawn -> f a x @ drop n x | Read -> f a x | Free -> [] let readsAllButFirst n f a x = match a with - | Write | Spawn -> f a x + | Write | Call | Spawn -> f a x | Read -> f a x @ drop n x | Free -> [] let reads ns a x = let i, o = partition ns x in match a with - | Write | Spawn -> o + | Write | Call | Spawn -> o | Read -> i | Free -> [] let writes ns a x = let i, o = partition ns x in match a with - | Write | Spawn -> i + | Write | Call | Spawn -> i | Read -> o | Free -> [] let frees ns a x = let i, o = partition ns x in match a with - | Write | Spawn -> [] + | Write | Call | Spawn -> [] | Read -> o | Free -> i let readsFrees rs fs a x = match a with - | Write | Spawn -> [] + | Write | Call | Spawn -> [] | Read -> keep rs x | Free -> keep fs x let onlyReads ns a x = match a with - | Write | Spawn -> [] + | Write | Call | Spawn -> [] | Read -> keep ns x | Free -> [] let onlyWrites ns a x = match a with - | Write | Spawn -> keep ns x + | Write | Call | Spawn -> keep ns x | Read -> [] | Free -> [] let readsWrites rs ws a x = match a with - | Write | Spawn -> keep ws x + | Write | Call | Spawn -> keep ws x | Read -> keep rs x | Free -> [] let readsAll a x = match a with - | Write | Spawn -> [] + | Write | Call | Spawn -> [] | Read -> x | Free -> [] let writesAll a x = match a with - | Write | Spawn -> x + | Write | Call | Spawn -> x | Read -> [] | Free -> [] end @@ -1165,6 +1164,8 @@ let unknown_desc ~f name = (* TODO: remove name argument, unknown function shoul | Read when GobConfig.get_bool "sem.unknown_function.read.args" -> args | Read -> [] | Free -> [] + | Call when get_bool "sem.unknown_function.call.args" -> args + | Call -> [] | Spawn when get_bool "sem.unknown_function.spawn" -> args | Spawn -> [] in diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index d9cdef9286..5a3aeb55ce 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -306,6 +306,7 @@ struct let write = match kind with | Write | Free -> true | Read -> false + | Call | Spawn -> false (* TODO: nonsense? *) in let s = GProtecting.make ~write ~recovered:is_recovered_to_st locks in diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 3ed5a5acbe..970895e971 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -105,7 +105,7 @@ struct let g: V.t = Obj.obj g in begin match g with | `Left g' -> (* accesses *) - (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *) + (* ignore (Pretty.printf "WarnGlobal %a\n" Access.MemoRoot.pretty g'); *) let trie = G.access (ctx.global g) in (** Distribute access to contained fields. *) let rec distribute_inner offset (accs, children) ancestor_accs = @@ -193,6 +193,19 @@ struct | _ -> ctx.local + let special ctx (lvalOpt: lval option) (f:varinfo) (arglist:exp list) : D.t = + (* perform shallow and deep invalidate according to Library descriptors *) + let desc = LibraryFunctions.find f in + if List.mem LibraryDesc.ThreadUnsafe desc.attrs then ( + let e = Lval (Var f, NoOffset) in + let conf = 110 in + let loc = Option.get !Node.current_node in + let vo = Some f in + let a = Obj.obj (ctx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind=Call}))) in + side_access ctx (conf, Call, loc, e, a) ((`Var f), `NoOffset) ; + ); + ctx.local + let finalize () = let total = !safe + !unsafe + !vulnerable in if total > 0 then ( diff --git a/src/domains/accessKind.ml b/src/domains/accessKind.ml index 576581af02..b36e8f3eca 100644 --- a/src/domains/accessKind.ml +++ b/src/domains/accessKind.ml @@ -1,9 +1,10 @@ (** Kinds of memory accesses. *) type t = - | Write (** argument may be read or written to *) + | Write (** argument may be written to *) | Read (** argument may be read *) | Free (** argument may be freed *) + | Call (** argument may be called *) | Spawn (** argument may be spawned *) [@@deriving eq, ord, hash] (** Specifies what is known about an argument. *) @@ -12,6 +13,7 @@ let show: t -> string = function | Write -> "write" | Read -> "read" | Free -> "free" + | Call -> "call" | Spawn -> "spawn" include Printable.SimpleShow ( diff --git a/src/util/options.schema.json b/src/util/options.schema.json index efa1dfabb8..0e89ede0b5 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -1317,6 +1317,13 @@ "type": "boolean", "default": true }, + "call": { + "title": "sem.unknown_function.call", + "description": + "Unknown function call calls reachable functions", + "type": "boolean", + "default": true + }, "invalidate": { "title": "sem.unknown_function.invalidate", "type": "object", diff --git a/tests/regression/04-mutex/90-thread-unsafe_fun_rc.c b/tests/regression/04-mutex/90-thread-unsafe_fun_rc.c new file mode 100644 index 0000000000..8f2f01fc6d --- /dev/null +++ b/tests/regression/04-mutex/90-thread-unsafe_fun_rc.c @@ -0,0 +1,22 @@ +#include +#include + +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); + rand(); // RACE! + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + pthread_mutex_lock(&mutex2); + rand(); // RACE! + pthread_mutex_unlock(&mutex2); + pthread_join (id, NULL); + return 0; +} diff --git a/tests/regression/04-mutex/91-thread-unsafe_fun_nr.c b/tests/regression/04-mutex/91-thread-unsafe_fun_nr.c new file mode 100644 index 0000000000..df02d23db9 --- /dev/null +++ b/tests/regression/04-mutex/91-thread-unsafe_fun_nr.c @@ -0,0 +1,21 @@ +#include +#include + +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); + rand(); // NORACE + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + pthread_mutex_lock(&mutex1); + rand(); // NORACE + pthread_mutex_unlock(&mutex1); + pthread_join (id, NULL); + return 0; +}