From 884763609adc2e457727d089745c679a4d42a7be Mon Sep 17 00:00:00 2001 From: karoliineh Date: Fri, 9 Jun 2023 21:38:44 +0300 Subject: [PATCH 1/7] Add (function) Call to accessKind --- src/analyses/libraryFunctions.ml | 23 ++++++++++++----------- src/analyses/mutexAnalysis.ml | 1 + src/domains/accessKind.ml | 4 +++- 3 files changed, 16 insertions(+), 12 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 9b689b64ad..31ed3adb65 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -797,70 +797,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 @@ -1158,6 +1158,7 @@ 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 -> [] (* TODO: option *) | Spawn when get_bool "sem.unknown_function.spawn" -> args | Spawn -> [] in diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 9029c1b4a1..6d39be150c 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -254,6 +254,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/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 ( From d58c1ca6e0182b86daf083180d986aa52315654b Mon Sep 17 00:00:00 2001 From: karoliineh Date: Fri, 9 Jun 2023 22:17:30 +0300 Subject: [PATCH 2/7] Add tests for thread-unsafe function call --- .../04-mutex/77-thread-unsafe_fun_rc.c | 22 +++++++++++++++++++ .../04-mutex/78-thread-unsafe_fun_nr.c | 21 ++++++++++++++++++ 2 files changed, 43 insertions(+) create mode 100644 tests/regression/04-mutex/77-thread-unsafe_fun_rc.c create mode 100644 tests/regression/04-mutex/78-thread-unsafe_fun_nr.c diff --git a/tests/regression/04-mutex/77-thread-unsafe_fun_rc.c b/tests/regression/04-mutex/77-thread-unsafe_fun_rc.c new file mode 100644 index 0000000000..8f2f01fc6d --- /dev/null +++ b/tests/regression/04-mutex/77-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/78-thread-unsafe_fun_nr.c b/tests/regression/04-mutex/78-thread-unsafe_fun_nr.c new file mode 100644 index 0000000000..df02d23db9 --- /dev/null +++ b/tests/regression/04-mutex/78-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; +} From 874c1864bc2f4e4cdc14138de09c9a408c94f319 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Fri, 9 Jun 2023 22:18:38 +0300 Subject: [PATCH 3/7] Handle thread-unsafe function calls in raceAnalysis #723 Co-authored-by: Simmo Saan --- src/analyses/raceAnalysis.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 481ccbf60b..30cf03cfa7 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -153,6 +153,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 (`Type f.vtype) (Some (f, `NoOffset)) (conf, Call, loc, e, a); + ); + ctx.local + let finalize () = let total = !safe + !unsafe + !vulnerable in if total > 0 then ( From e11c982aac5925edc348389305ce1a48efb73aa0 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 14 Aug 2023 13:53:11 +0300 Subject: [PATCH 4/7] Make sem.unknown_function.call option --- src/analyses/libraryFunctions.ml | 3 ++- src/util/options.schema.json | 7 +++++++ 2 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 6495341c7a..7c31d69fb8 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -1165,7 +1165,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 -> [] (* TODO: option *) + | 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/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", From f150fdca489dfe76e1510c6a78ececddc0a0c60e Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 14 Aug 2023 14:37:09 +0300 Subject: [PATCH 5/7] Fix rand in libraryFunctions --- src/analyses/libraryFunctions.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 7c31d69fb8..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. From 379a7ff53d0f330e8fe92042c6cec9b37b369ccc Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 14 Aug 2023 14:37:36 +0300 Subject: [PATCH 6/7] Fix side_access call --- src/analyses/raceAnalysis.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index c09396bdd3..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 = @@ -202,7 +202,7 @@ struct 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) ((`Type f.vtype), `NoOffset) ; + side_access ctx (conf, Call, loc, e, a) ((`Var f), `NoOffset) ; ); ctx.local From 8465e0b2eb3a72230ec3c327faa47fc969aad211 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 14 Aug 2023 14:38:05 +0300 Subject: [PATCH 7/7] Rename tests to have unique numbers --- .../{77-thread-unsafe_fun_rc.c => 90-thread-unsafe_fun_rc.c} | 0 .../{78-thread-unsafe_fun_nr.c => 91-thread-unsafe_fun_nr.c} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/04-mutex/{77-thread-unsafe_fun_rc.c => 90-thread-unsafe_fun_rc.c} (100%) rename tests/regression/04-mutex/{78-thread-unsafe_fun_nr.c => 91-thread-unsafe_fun_nr.c} (100%) diff --git a/tests/regression/04-mutex/77-thread-unsafe_fun_rc.c b/tests/regression/04-mutex/90-thread-unsafe_fun_rc.c similarity index 100% rename from tests/regression/04-mutex/77-thread-unsafe_fun_rc.c rename to tests/regression/04-mutex/90-thread-unsafe_fun_rc.c diff --git a/tests/regression/04-mutex/78-thread-unsafe_fun_nr.c b/tests/regression/04-mutex/91-thread-unsafe_fun_nr.c similarity index 100% rename from tests/regression/04-mutex/78-thread-unsafe_fun_nr.c rename to tests/regression/04-mutex/91-thread-unsafe_fun_nr.c