From 3525e494835566906a38c493c03ce5a57c2539dc Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 19 Jun 2023 15:14:09 +0300 Subject: [PATCH 01/28] Add more tests for covering different cases of access outer distribution Co-authored-by: Simmo Saan --- .../04-mutex/90-distribute-fields-type-1.c | 42 +++++++++++++++++ .../04-mutex/90-distribute-fields-type-1.t | 31 ++++++++++++ .../04-mutex/91-distribute-fields-type-2.c | 43 +++++++++++++++++ .../04-mutex/91-distribute-fields-type-2.t | 31 ++++++++++++ .../04-mutex/92-distribute-fields-type-deep.c | 47 +++++++++++++++++++ .../04-mutex/92-distribute-fields-type-deep.t | 33 +++++++++++++ .../93-distribute-fields-type-global.c | 26 ++++++++++ .../93-distribute-fields-type-global.t | 5 ++ 8 files changed, 258 insertions(+) create mode 100644 tests/regression/04-mutex/90-distribute-fields-type-1.c create mode 100644 tests/regression/04-mutex/90-distribute-fields-type-1.t create mode 100644 tests/regression/04-mutex/91-distribute-fields-type-2.c create mode 100644 tests/regression/04-mutex/91-distribute-fields-type-2.t create mode 100644 tests/regression/04-mutex/92-distribute-fields-type-deep.c create mode 100644 tests/regression/04-mutex/92-distribute-fields-type-deep.t create mode 100644 tests/regression/04-mutex/93-distribute-fields-type-global.c create mode 100644 tests/regression/04-mutex/93-distribute-fields-type-global.t diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.c b/tests/regression/04-mutex/90-distribute-fields-type-1.c new file mode 100644 index 0000000000..51f0e52426 --- /dev/null +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.c @@ -0,0 +1,42 @@ +//PARAM: --enable ana.race.direct-arithmetic +#include +#include + +// (int) (S) (T) (U) +// \ / \ / \ / +// >f< >s< t +// \ / \ / +// f s +// \ / +// f + +struct S { + int field; +}; + +struct T { + struct S s; +}; + +// struct S s; +// struct T t; + +extern struct S* getS(); +extern struct T* getT(); + +// getS could return the same struct as is contained in getT + +void *t_fun(void *arg) { + // should write to (struct T).s.field in addition to (struct S).field + // but easier to implement the other way around? + getS()->field = 1; // RACE! + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + struct S s1; + getT()->s = s1; // RACE! + return 0; +} diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t new file mode 100644 index 0000000000..dd862fa65a --- /dev/null +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t @@ -0,0 +1,31 @@ + $ goblint --enable allglobs 90-distribute-fields-type-1.c + [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:32:3-32:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:32:3-32:20) + [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:40:3-40:17) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Warning][Race] Memory location (struct T).s.field (race with conf. 100): + write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) + write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) + [Success][Race] Memory location (struct T).s (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 1 + total memory locations: 3 diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.c b/tests/regression/04-mutex/91-distribute-fields-type-2.c new file mode 100644 index 0000000000..12866105f6 --- /dev/null +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.c @@ -0,0 +1,43 @@ +//PARAM: --enable ana.race.direct-arithmetic +#include +#include + +// (int) >(S)< >(T)< (U) +// \ / \ / \ / +// f s t +// \ / \ / +// f s +// \ / +// f + +struct S { + int field; +}; + +struct T { + struct S s; +}; + +// struct S s; +// struct T t; + +extern struct S* getS(); +extern struct T* getT(); + +// getS could return the same struct as is contained in getT + +void *t_fun(void *arg) { + // should write to (struct T).s.field in addition to (struct S).field + // but easier to implement the other way around? + struct S s1; + *(getS()) = s1; // RACE! + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + struct T t1; + *(getT()) = t1; // RACE! + return 0; +} diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t new file mode 100644 index 0000000000..4cfb965e25 --- /dev/null +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t @@ -0,0 +1,31 @@ + $ goblint --enable allglobs 91-distribute-fields-type-2.c + [Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:33:3-33:17) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:33:3-33:17) + [Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:41:3-41:17) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Warning][Race] Memory location (struct T).s (race with conf. 100): + write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:33:3-33:17) + write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:41:3-41:17) + [Success][Race] Memory location (struct T) (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:41:3-41:17) + [Success][Race] Memory location (struct S) (safe): + write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 1 + total memory locations: 3 diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.c b/tests/regression/04-mutex/92-distribute-fields-type-deep.c new file mode 100644 index 0000000000..891f5fb51f --- /dev/null +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.c @@ -0,0 +1,47 @@ +//PARAM: --enable ana.race.direct-arithmetic +#include +#include + +// (int) (S) (T) (U) +// \ / \ / \ / +// >f< s >t< +// \ / \ / +// f s +// \ / +// f + +struct S { + int field; +}; + +struct T { + struct S s; +}; + +struct U { + struct T t; +}; + +// struct S s; +// struct T t; + +extern struct S* getS(); +extern struct T* getT(); +extern struct U* getU(); + +// getS could return the same struct as is contained in getT + +void *t_fun(void *arg) { + // should write to (struct U).t.s.field in addition to (struct T).s.field + // but easier to implement the other way around? + getS()->field = 1; // RACE! + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + struct T t1; + getU()->t = t1; // RACE! + return 0; +} diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t new file mode 100644 index 0000000000..12dc5e8f52 --- /dev/null +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -0,0 +1,33 @@ + $ goblint --enable allglobs 92-distribute-fields-type-deep.c + [Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:37:3-37:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:37:3-37:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:37:3-37:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:37:3-37:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:37:3-37:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:37:3-37:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:37:3-37:20) + [Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:45:3-45:17) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Success][Race] Memory location (struct T).s.field (safe): + write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) + [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): + write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) + write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) + [Success][Race] Memory location (struct U).t (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Race] Memory locations race summary: + safe: 3 + vulnerable: 0 + unsafe: 1 + total memory locations: 4 diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.c b/tests/regression/04-mutex/93-distribute-fields-type-global.c new file mode 100644 index 0000000000..e0065b7870 --- /dev/null +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.c @@ -0,0 +1,26 @@ +//PARAM: --enable ana.race.direct-arithmetic +#include +#include + +struct S { + int field; +}; + +struct S s; + +void *t_fun(void *arg) { + printf("%d",getS()->field); // RACE! + + return NULL; +} + +extern struct S* getS(); + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + struct S s1; + s = s1; // RACE! + return 0; +} + diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t new file mode 100644 index 0000000000..90baf61492 --- /dev/null +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t @@ -0,0 +1,5 @@ + $ goblint --enable allglobs 93-distribute-fields-type-global.c + 93-distribute-fields-type-global.c:12: Error: expecting a pointer to a struct + Error: There were parsing errors in .goblint/preprocessed/93-distribute-fields-type-global.i + Fatal error: exception Goblint_lib__Maingoblint.FrontendError("Errormsg.Error") + [2] From 2a003ab733b53c3e89eef205c6a152a9d71aadb7 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 19 Jun 2023 15:16:24 +0300 Subject: [PATCH 02/28] Add cram tests and ASCII art to existing tests that cover access outer distribution --- .../04-mutex/77-type-nested-fields.c | 8 +++++ .../04-mutex/77-type-nested-fields.t | 29 +++++++++++++++++ .../04-mutex/79-type-nested-fields-deep1.c | 8 +++++ .../04-mutex/79-type-nested-fields-deep1.t | 31 +++++++++++++++++++ .../04-mutex/80-type-nested-fields-deep2.c | 8 +++++ .../04-mutex/80-type-nested-fields-deep2.t | 29 +++++++++++++++++ tests/regression/06-symbeq/16-type_rc.c | 8 +++++ tests/regression/06-symbeq/16-type_rc.t | 30 +++++++++--------- 8 files changed, 136 insertions(+), 15 deletions(-) create mode 100644 tests/regression/04-mutex/77-type-nested-fields.t create mode 100644 tests/regression/04-mutex/79-type-nested-fields-deep1.t create mode 100644 tests/regression/04-mutex/80-type-nested-fields-deep2.t diff --git a/tests/regression/04-mutex/77-type-nested-fields.c b/tests/regression/04-mutex/77-type-nested-fields.c index 6f173d6fec..a526defb06 100644 --- a/tests/regression/04-mutex/77-type-nested-fields.c +++ b/tests/regression/04-mutex/77-type-nested-fields.c @@ -2,6 +2,14 @@ #include #include +// (int) (S) (T) (U) +// \ / \ / \ / +// >f< s t +// \ / \ / +// >f< s +// \ / +// f + struct S { int field; }; diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t new file mode 100644 index 0000000000..2cbd339dfa --- /dev/null +++ b/tests/regression/04-mutex/77-type-nested-fields.t @@ -0,0 +1,29 @@ + $ goblint --enable allglobs 77-type-nested-fields.c + [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:32:3-32:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:32:3-32:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:32:3-32:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:32:3-32:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:32:3-32:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:32:3-32:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:32:3-32:20) + [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:39:3-39:22) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:39:3-39:22) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:39:3-39:22) + [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:39:3-39:22) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:39:3-39:22) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:39:3-39:22) + [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:39:3-39:22) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Warning][Race] Memory location (struct T).s.field (race with conf. 100): + write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:32:3-32:20) + write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:39:3-39:22) + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:32:3-32:20) + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 1 + total memory locations: 2 diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.c b/tests/regression/04-mutex/79-type-nested-fields-deep1.c index ee99c40973..c38e700829 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.c +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.c @@ -2,6 +2,14 @@ #include #include +// (int) (S) (T) (U) +// \ / \ / \ / +// >f< s t +// \ / \ / +// f s +// \ / +// >f< + struct S { int field; }; diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t new file mode 100644 index 0000000000..6bb9b040fd --- /dev/null +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -0,0 +1,31 @@ + $ goblint --enable allglobs 79-type-nested-fields-deep1.c + [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:37:3-37:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:37:3-37:20) + [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:44:3-44:24) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Success][Race] Memory location (struct T).s.field (safe): + write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) + [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): + write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) + write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 1 + total memory locations: 3 diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.c b/tests/regression/04-mutex/80-type-nested-fields-deep2.c index 646acd9147..9a1e3028a3 100644 --- a/tests/regression/04-mutex/80-type-nested-fields-deep2.c +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.c @@ -2,6 +2,14 @@ #include #include +// (int) (S) (T) (U) +// \ / \ / \ / +// f s t +// \ / \ / +// >f< s +// \ / +// >f< + struct S { int field; }; diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t new file mode 100644 index 0000000000..f14a315de2 --- /dev/null +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t @@ -0,0 +1,29 @@ + $ goblint --enable allglobs 80-type-nested-fields-deep2.c + [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:37:3-37:22) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:37:3-37:22) + [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:44:3-44:24) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Success][Race] Memory location (struct T).s.field (safe): + write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:37:3-37:22) + [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): + write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:37:3-37:22) + write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Race] Memory locations race summary: + safe: 1 + vulnerable: 0 + unsafe: 1 + total memory locations: 2 diff --git a/tests/regression/06-symbeq/16-type_rc.c b/tests/regression/06-symbeq/16-type_rc.c index efeb6c768b..e9e7c7972b 100644 --- a/tests/regression/06-symbeq/16-type_rc.c +++ b/tests/regression/06-symbeq/16-type_rc.c @@ -1,6 +1,14 @@ // PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" #include +//>(int)< (S) (T) (U) +// \ / \ / \ / +// >f< s t +// \ / \ / +// f s +// \ / +// f + struct s { int datum; pthread_mutex_t mutex; diff --git a/tests/regression/06-symbeq/16-type_rc.t b/tests/regression/06-symbeq/16-type_rc.t index 78c293b7ef..06a3b314a4 100644 --- a/tests/regression/06-symbeq/16-type_rc.t +++ b/tests/regression/06-symbeq/16-type_rc.t @@ -1,22 +1,22 @@ Disable info messages because race summary contains (safe) memory location count, which is different on Linux and OSX. $ goblint --enable warn.deterministic --disable warn.info --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" 16-type_rc.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:13:3-13:15) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:24:3-24:16) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:25:3-25:16) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:28:3-28:9) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:21:3-21:15) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:32:3-32:16) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9) [Warning][Race] Memory location (struct s).datum (race with conf. 100): - write with [mhp:{tid=[main, t_fun@16-type_rc.c:27:3-27:37#top]}, thread:[main, t_fun@16-type_rc.c:27:3-27:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:13:3-13:15) - write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:27:3-27:37#top]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:28:3-28:9) - [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:12:12-12:24) - [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:23:3-23:14) + write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#top]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + write with [mhp:{tid=[main]; created={[main, t_fun@16-type_rc.c:35:3-35:37#top]}}, thread:[main]] (conf. 100) (exp: & *d) (16-type_rc.c:36:3-36:9) + [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24) + [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14) $ goblint --enable warn.deterministic --disable warn.info --disable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --set ana.activated[+] "'symb_locks'" --enable allglobs 16-type_rc.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:13:3-13:15) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:24:3-24:16) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:25:3-25:16) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:28:3-28:9) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:21:3-21:15) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:32:3-32:16) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:33:3-33:16) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (16-type_rc.c:36:3-36:9) [Success][Race] Memory location (struct s).datum (safe): - write with [mhp:{tid=[main, t_fun@16-type_rc.c:27:3-27:37#top]}, thread:[main, t_fun@16-type_rc.c:27:3-27:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:13:3-13:15) - [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:12:12-12:24) - [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:23:3-23:14) + write with [mhp:{tid=[main, t_fun@16-type_rc.c:35:3-35:37#top]}, thread:[main, t_fun@16-type_rc.c:35:3-35:37#top]] (conf. 100) (exp: & s->datum) (16-type_rc.c:21:3-21:15) + [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:20:12-20:24) + [Error][Imprecise][Unsound] Function definition missing for get_s (16-type_rc.c:31:3-31:14) From 91b64e827dbaeacac52497482c72cbf8a7ceadd6 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 19 Jun 2023 16:24:48 +0300 Subject: [PATCH 03/28] Fix test 04 93 --- .../93-distribute-fields-type-global.c | 4 +-- .../93-distribute-fields-type-global.t | 28 ++++++++++++++++--- 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.c b/tests/regression/04-mutex/93-distribute-fields-type-global.c index e0065b7870..ad7839d95f 100644 --- a/tests/regression/04-mutex/93-distribute-fields-type-global.c +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.c @@ -8,14 +8,14 @@ struct S { struct S s; +extern struct S* getS(); + void *t_fun(void *arg) { printf("%d",getS()->field); // RACE! return NULL; } -extern struct S* getS(); - int main(void) { pthread_t id; pthread_create(&id, NULL, t_fun, NULL); diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t index 90baf61492..30f61cb3cc 100644 --- a/tests/regression/04-mutex/93-distribute-fields-type-global.t +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t @@ -1,5 +1,25 @@ $ goblint --enable allglobs 93-distribute-fields-type-global.c - 93-distribute-fields-type-global.c:12: Error: expecting a pointer to a struct - Error: There were parsing errors in .goblint/preprocessed/93-distribute-fields-type-global.i - Fatal error: exception Goblint_lib__Maingoblint.FrontendError("Errormsg.Error") - [2] + [Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Unsound] Unknown address in {&tmp} has escaped. (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (93-distribute-fields-type-global.c:14:3-14:29) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Unsound] Write to unknown address: privatization is unsound. (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Warning][Race] Memory location s.field@93-distribute-fields-type-global.c:9:10-9:11 (race with conf. 110): + read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:14:3-14:29) + write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:23:3-23:9) + [Success][Race] Memory location s@93-distribute-fields-type-global.c:9:10-9:11 (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:23:3-23:9) + [Success][Race] Memory location (struct S).field (safe): + read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Race] Memory locations race summary: + safe: 2 + vulnerable: 0 + unsafe: 1 + total memory locations: 3 From 4ac338dbfa8813197663a250b742d71ed5b9bf51 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 19 Jun 2023 16:47:09 +0300 Subject: [PATCH 04/28] Move access outer distribute to raceAnalysis Co-authored-by: Simmo Saan --- src/analyses/raceAnalysis.ml | 41 ++++++++++++++++--- src/domains/access.ml | 23 +---------- .../04-mutex/79-type-nested-fields-deep1.t | 6 +-- .../04-mutex/84-distribute-fields-1.t | 4 +- .../04-mutex/85-distribute-fields-2.t | 4 +- .../04-mutex/86-distribute-fields-3.t | 4 +- 6 files changed, 44 insertions(+), 38 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 802c83dadc..f2d2554abc 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -54,6 +54,12 @@ struct struct include TrieDomain.Make (OneOffset) (Access.AS) + let rec find (offset : Offset.Unit.t) ((accs, children) : t) : value = + match offset with + | `NoOffset -> accs + | `Field (f, offset') -> find offset' (ChildMap.find (Field f) children) + | `Index ((), offset') -> find offset' (ChildMap.find Index children) + let rec singleton (offset : Offset.Unit.t) (value : value) : t = match offset with | `NoOffset -> (value, ChildMap.empty ()) @@ -99,6 +105,22 @@ struct ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (Access.AS.singleton (conf, w, loc, e, a)))); side_vars ctx memo + let outer_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option = + match offset with + | `NoOffset -> None + | `Field (f, offset') -> Some (`Type f.ftype, offset') + | `Index ((), offset') -> None (* TODO *) + + let rec distribute_outer ctx ((root, offset) : Access.Memo.t) : Access.AS.t = + let trie = G.access (ctx.global (V.access root)) in + let accs = OffsetTrie.find offset trie in + let outer_accs = + match outer_memo (root, offset) with + | Some outer_memo -> distribute_outer ctx outer_memo + | None -> Access.AS.empty () + in + Access.AS.union accs outer_accs + let query ctx (type a) (q: a Queries.t): a Queries.result = match q with | WarnGlobal g -> @@ -109,15 +131,22 @@ struct let trie = G.access (ctx.global g) in (** Distribute access to contained fields. *) let rec distribute_inner offset (accs, children) ancestor_accs = - let ancestor_accs' = Access.AS.union ancestor_accs accs in - OffsetTrie.ChildMap.iter (fun child_key child_trie -> - distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ancestor_accs' - ) children; + let outer_accs = + match outer_memo (g', offset) with + | Some outer_memo -> distribute_outer ctx outer_memo + | None -> Access.AS.empty () + in + M.trace "access" "outer accs = %a" Access.AS.pretty outer_accs; + let ancestor_accs' = Access.AS.union ancestor_accs outer_accs in if not (Access.AS.is_empty accs) then ( let memo = (g', offset) in let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in - Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs memo) accs - ) + Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs:ancestor_accs' memo) accs + ); + let ancestor_accs'' = Access.AS.union ancestor_accs' accs in + OffsetTrie.ChildMap.iter (fun child_key child_trie -> + distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ancestor_accs'' + ) children; in distribute_inner `NoOffset trie (Access.AS.empty ()) | `Right _ -> (* vars *) diff --git a/src/domains/access.ml b/src/domains/access.ml index 798a35ee9c..0e029ff128 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -211,27 +211,6 @@ let add_one side memo: unit = if not ignorable then side memo -(** Distribute type-based access to variables and containing fields. *) -let rec add_distribute_outer side (t: typ) (o: Offset.Unit.t) = - let memo = (`Type t, o) in - if M.tracing then M.tracei "access" "add_distribute_outer %a\n" Memo.pretty memo; - add_one side memo; - - (* distribute to variables of the type *) - let ts = typeSig t in - let vars = TSH.find_all typeVar ts in - List.iter (fun v -> - add_one side (`Var v, o) (* same offset, but on variable *) - ) vars; - - (* recursively distribute to fields containing the type *) - let fields = TSH.find_all typeIncl ts in - List.iter (fun f -> - (* prepend field and distribute to outer struct *) - add_distribute_outer side (TComp (f.fcomp, [])) (`Field (f, o)) - ) fields; - - if M.tracing then M.traceu "access" "add_distribute_outer\n" (** Add access to known variable with offsets or unknown variable from expression. *) let add side e voffs = @@ -249,7 +228,7 @@ let add side e voffs = in match o with | `NoOffset when not !collect_direct_arithmetic && isArithmeticType t -> () - | _ -> add_distribute_outer side t o (* distribute to variables and outer offsets *) + | _ -> add_one side (`Type t, o) (* add_distribute_outer side t o (* distribute to variables and outer offsets *)*) end; if M.tracing then M.traceu "access" "add\n" diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t index 6bb9b040fd..4075dab33b 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -17,15 +17,13 @@ live: 7 dead: 0 total lines: 7 - [Success][Race] Memory location (struct T).s.field (safe): - write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) [Success][Race] Memory location (struct S).field (safe): write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:44:3-44:24) [Info][Race] Memory locations race summary: - safe: 2 + safe: 1 vulnerable: 0 unsafe: 1 - total memory locations: 3 + total memory locations: 2 diff --git a/tests/regression/04-mutex/84-distribute-fields-1.t b/tests/regression/04-mutex/84-distribute-fields-1.t index eb2c43623f..27653d4759 100644 --- a/tests/regression/04-mutex/84-distribute-fields-1.t +++ b/tests/regression/04-mutex/84-distribute-fields-1.t @@ -3,11 +3,11 @@ live: 8 dead: 0 total lines: 8 + [Success][Race] Memory location s@84-distribute-fields-1.c:9:10-9:11 (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) [Warning][Race] Memory location s.data@84-distribute-fields-1.c:9:10-9:11 (race with conf. 110): write with [mhp:{tid=[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}, thread:[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]] (conf. 110) (exp: & s.data) (84-distribute-fields-1.c:12:3-12:13) write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) - [Success][Race] Memory location s@84-distribute-fields-1.c:9:10-9:11 (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@84-distribute-fields-1.c:18:3-18:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (84-distribute-fields-1.c:20:3-20:9) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 diff --git a/tests/regression/04-mutex/85-distribute-fields-2.t b/tests/regression/04-mutex/85-distribute-fields-2.t index 7039fc399c..19355f7bc9 100644 --- a/tests/regression/04-mutex/85-distribute-fields-2.t +++ b/tests/regression/04-mutex/85-distribute-fields-2.t @@ -3,11 +3,11 @@ live: 8 dead: 0 total lines: 8 + [Success][Race] Memory location t.s@85-distribute-fields-2.c:15:10-15:11 (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) [Warning][Race] Memory location t.s.data@85-distribute-fields-2.c:15:10-15:11 (race with conf. 110): write with [mhp:{tid=[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}, thread:[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]] (conf. 110) (exp: & t.s.data) (85-distribute-fields-2.c:18:3-18:15) write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) - [Success][Race] Memory location t.s@85-distribute-fields-2.c:15:10-15:11 (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@85-distribute-fields-2.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t.s) (85-distribute-fields-2.c:26:3-26:11) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 diff --git a/tests/regression/04-mutex/86-distribute-fields-3.t b/tests/regression/04-mutex/86-distribute-fields-3.t index 5557f3400a..9651a91923 100644 --- a/tests/regression/04-mutex/86-distribute-fields-3.t +++ b/tests/regression/04-mutex/86-distribute-fields-3.t @@ -3,11 +3,11 @@ live: 8 dead: 0 total lines: 8 + [Success][Race] Memory location t@86-distribute-fields-3.c:15:10-15:11 (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [Warning][Race] Memory location t.s.data@86-distribute-fields-3.c:15:10-15:11 (race with conf. 110): write with [mhp:{tid=[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}, thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) - [Success][Race] Memory location t@86-distribute-fields-3.c:15:10-15:11 (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 From bdf116d466db245f7021eaf312df9392e8629adb Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 20 Jun 2023 15:56:12 +0300 Subject: [PATCH 05/28] Handle global variables in outer_memo Co-authored-by: Simmo Saan --- src/analyses/raceAnalysis.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index f2d2554abc..18426ebc4f 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -106,10 +106,11 @@ struct side_vars ctx memo let outer_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option = - match offset with - | `NoOffset -> None - | `Field (f, offset') -> Some (`Type f.ftype, offset') - | `Index ((), offset') -> None (* TODO *) + match root, offset with + | `Var v, _ -> Some (`Type v.vtype, offset) (* TODO: Alloc variables void type *) + | _, `NoOffset -> None + | _, `Field (f, offset') -> Some (`Type f.ftype, offset') + | _, `Index ((), offset') -> None (* TODO *) let rec distribute_outer ctx ((root, offset) : Access.Memo.t) : Access.AS.t = let trie = G.access (ctx.global (V.access root)) in From 31ec579e2d7b3b51ee293db8b42d96290cfaccfd Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 20 Jun 2023 16:43:01 +0300 Subject: [PATCH 06/28] Split ancestor accs and outer ancestor accs Co-authored-by: Simmo Saan --- src/analyses/raceAnalysis.ml | 12 ++++++------ src/domains/access.ml | 21 +++++++++++++-------- 2 files changed, 19 insertions(+), 14 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 18426ebc4f..2e9a3d5b4b 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -131,25 +131,25 @@ struct (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *) let trie = G.access (ctx.global g) in (** Distribute access to contained fields. *) - let rec distribute_inner offset (accs, children) ancestor_accs = + let rec distribute_inner offset (accs, children) ~ancestor_accs ~ancestor_outer_accs = let outer_accs = match outer_memo (g', offset) with | Some outer_memo -> distribute_outer ctx outer_memo | None -> Access.AS.empty () in M.trace "access" "outer accs = %a" Access.AS.pretty outer_accs; - let ancestor_accs' = Access.AS.union ancestor_accs outer_accs in if not (Access.AS.is_empty accs) then ( let memo = (g', offset) in let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in - Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs:ancestor_accs' memo) accs + Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs ~ancestor_outer_accs ~outer_accs memo) accs ); - let ancestor_accs'' = Access.AS.union ancestor_accs' accs in + let ancestor_outer_accs' = Access.AS.union ancestor_outer_accs outer_accs in + let ancestor_accs' = Access.AS.union ancestor_accs accs in OffsetTrie.ChildMap.iter (fun child_key child_trie -> - distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ancestor_accs'' + distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ~ancestor_accs:ancestor_accs' ~ancestor_outer_accs:ancestor_outer_accs' ) children; in - distribute_inner `NoOffset trie (Access.AS.empty ()) + distribute_inner `NoOffset trie ~ancestor_accs:(Access.AS.empty ()) ~ancestor_outer_accs:(Access.AS.empty ()) | `Right _ -> (* vars *) () end diff --git a/src/domains/access.ml b/src/domains/access.ml index 0e029ff128..1dc6cbafce 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -357,9 +357,9 @@ let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),lo else true -let group_may_race ~ancestor_accs accs = +let group_may_race ~ancestor_accs ~ancestor_outer_accs ~outer_accs accs = (* BFS to traverse one component with may_race edges *) - let rec bfs' ~ancestor_accs ~accs ~todo ~visited = + let rec bfs' ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs ~todo ~visited = let may_race_accs ~accs ~todo = AS.fold (fun acc todo' -> AS.fold (fun acc' todo' -> @@ -372,16 +372,21 @@ let group_may_race ~ancestor_accs accs = in let accs' = AS.diff accs todo in let ancestor_accs' = AS.diff ancestor_accs todo in + let ancestor_outer_accs' = AS.diff ancestor_outer_accs todo in + let outer_accs' = AS.diff outer_accs todo in let todo_accs = may_race_accs ~accs:accs' ~todo in - let todo_ancestor_accs = may_race_accs ~accs:ancestor_accs' ~todo:(AS.diff todo ancestor_accs') in - let todo' = AS.union todo_accs todo_ancestor_accs in + let accs_todo = AS.inter todo accs in + let todo_ancestor_accs = may_race_accs ~accs:ancestor_accs' ~todo:accs_todo in + let todo_ancestor_outer_accs = may_race_accs ~accs:ancestor_outer_accs' ~todo:accs_todo in + let todo_outer_accs = may_race_accs ~accs:outer_accs' ~todo:accs_todo in + let todo' = AS.union (AS.union todo_accs todo_ancestor_accs) (AS.union todo_ancestor_outer_accs todo_outer_accs) in let visited' = AS.union visited todo in if AS.is_empty todo' then (accs', visited') else - (bfs' [@tailcall]) ~ancestor_accs:ancestor_accs' ~accs:accs' ~todo:todo' ~visited:visited' + (bfs' [@tailcall]) ~ancestor_accs:ancestor_accs' ~ancestor_outer_accs:ancestor_outer_accs' ~outer_accs:outer_accs' ~accs:accs' ~todo:todo' ~visited:visited' in - let bfs accs acc = bfs' ~ancestor_accs ~accs ~todo:(AS.singleton acc) ~visited:(AS.empty ()) in + let bfs accs acc = bfs' ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs ~todo:(AS.singleton acc) ~visited:(AS.empty ()) in (* repeat BFS to find all components *) let rec components comps accs = if AS.is_empty accs then @@ -457,7 +462,7 @@ let print_accesses memo grouped_accs = M.msg_group Success ~category:Race "Memory location %a (safe)" Memo.pretty memo (msgs safe_accs) ) -let warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs memo accs = - let grouped_accs = group_may_race ~ancestor_accs accs in (* do expensive component finding only once *) +let warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs ~ancestor_outer_accs ~outer_accs memo accs = + let grouped_accs = group_may_race ~ancestor_accs ~ancestor_outer_accs ~outer_accs accs in (* do expensive component finding only once *) incr_summary ~safe ~vulnerable ~unsafe memo grouped_accs; print_accesses memo grouped_accs From 936d7b04331ebeee920bc699a7dc64dbc217ead8 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Thu, 22 Jun 2023 12:22:45 +0300 Subject: [PATCH 07/28] Fix races between ancestor and outer accs Co-authored-by: Simmo Saan --- src/analyses/raceAnalysis.ml | 29 +++++++--- src/domains/access.ml | 58 +++++++++++++++---- .../04-mutex/79-type-nested-fields-deep1.t | 6 +- .../04-mutex/86-distribute-fields-3.t | 8 ++- .../04-mutex/90-distribute-fields-type-1.t | 4 +- .../04-mutex/91-distribute-fields-type-2.t | 4 +- .../04-mutex/92-distribute-fields-type-deep.t | 14 +++-- .../93-distribute-fields-type-global.t | 4 +- 8 files changed, 94 insertions(+), 33 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 2e9a3d5b4b..e0fbf96c2f 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -52,7 +52,7 @@ struct module OffsetTrie = struct - include TrieDomain.Make (OneOffset) (Access.AS) + include TrieDomain.Make (OneOffset) (Lattice.LiftBot (Access.AS)) let rec find (offset : Offset.Unit.t) ((accs, children) : t) : value = match offset with @@ -63,8 +63,8 @@ struct let rec singleton (offset : Offset.Unit.t) (value : value) : t = match offset with | `NoOffset -> (value, ChildMap.empty ()) - | `Field (f, offset') -> (Access.AS.empty (), ChildMap.singleton (Field f) (singleton offset' value)) - | `Index ((), offset') -> (Access.AS.empty (), ChildMap.singleton Index (singleton offset' value)) + | `Field (f, offset') -> (`Bot, ChildMap.singleton (Field f) (singleton offset' value)) + | `Index ((), offset') -> (`Bot, ChildMap.singleton Index (singleton offset' value)) end module G = @@ -102,7 +102,13 @@ struct let side_access ctx (conf, w, loc, e, a) ((memoroot, offset) as memo) = if !AnalysisState.should_warn then - ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (Access.AS.singleton (conf, w, loc, e, a)))); + ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton (conf, w, loc, e, a))))); + side_vars ctx memo + + let side_access0 ctx ((memoroot, offset) as memo) = + (* ignore (Pretty.printf "memo: %a\n" Access.Memo.pretty memo); *) + if !AnalysisState.should_warn then + ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.empty ())))); side_vars ctx memo let outer_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option = @@ -114,7 +120,11 @@ struct let rec distribute_outer ctx ((root, offset) : Access.Memo.t) : Access.AS.t = let trie = G.access (ctx.global (V.access root)) in - let accs = OffsetTrie.find offset trie in + let accs = + match OffsetTrie.find offset trie with + | `Lifted accs -> accs + | `Bot -> Access.AS.empty () + in let outer_accs = match outer_memo (root, offset) with | Some outer_memo -> distribute_outer ctx outer_memo @@ -132,13 +142,18 @@ struct let trie = G.access (ctx.global g) in (** Distribute access to contained fields. *) let rec distribute_inner offset (accs, children) ~ancestor_accs ~ancestor_outer_accs = + let accs = + match accs with + | `Lifted accs -> accs + | `Bot -> Access.AS.empty () + in let outer_accs = match outer_memo (g', offset) with | Some outer_memo -> distribute_outer ctx outer_memo | None -> Access.AS.empty () in M.trace "access" "outer accs = %a" Access.AS.pretty outer_accs; - if not (Access.AS.is_empty accs) then ( + if not (Access.AS.is_empty accs && Access.AS.is_empty ancestor_accs && Access.AS.is_empty outer_accs) then ( let memo = (g', offset) in let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs ~ancestor_outer_accs ~outer_accs memo) accs @@ -172,7 +187,7 @@ struct let loc = Option.get !Node.current_node in let add_access conf voffs = let a = part_access (Option.map fst voffs) in - Access.add (side_access octx (conf, kind, loc, e, a)) e voffs; + Access.add (side_access octx (conf, kind, loc, e, a)) (side_access0 octx) e voffs; in let add_access_struct conf ci = let a = part_access None in diff --git a/src/domains/access.ml b/src/domains/access.ml index 1dc6cbafce..40ebb289db 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -211,9 +211,30 @@ let add_one side memo: unit = if not ignorable then side memo +(** Distribute type-based access to variables and containing fields. *) +let rec add_distribute_outer side side0 (t: typ) (o: Offset.Unit.t) = + let memo = (`Type t, o) in + if M.tracing then M.tracei "access" "add_distribute_outer %a\n" Memo.pretty memo; + add_one side memo; + + (* distribute to variables of the type *) + let ts = typeSig t in + let vars = TSH.find_all typeVar ts in + List.iter (fun v -> + add_one side0 (`Var v, o) (* same offset, but on variable *) + ) vars; + + (* recursively distribute to fields containing the type *) + let fields = TSH.find_all typeIncl ts in + List.iter (fun f -> + (* prepend field and distribute to outer struct *) + add_distribute_outer side0 side0 (TComp (f.fcomp, [])) (`Field (f, o)) + ) fields; + + if M.tracing then M.traceu "access" "add_distribute_outer\n" (** Add access to known variable with offsets or unknown variable from expression. *) -let add side e voffs = +let add side side0 e voffs = begin match voffs with | Some (v, o) -> (* known variable *) if M.tracing then M.traceli "access" "add var %a%a\n" CilType.Varinfo.pretty v CilType.Offset.pretty o; @@ -228,7 +249,7 @@ let add side e voffs = in match o with | `NoOffset when not !collect_direct_arithmetic && isArithmeticType t -> () - | _ -> add_one side (`Type t, o) (* add_distribute_outer side t o (* distribute to variables and outer offsets *)*) + | _ -> add_distribute_outer side side0 t o (* distribute to variables and outer offsets *) end; if M.tracing then M.traceu "access" "add\n" @@ -379,26 +400,43 @@ let group_may_race ~ancestor_accs ~ancestor_outer_accs ~outer_accs accs = let todo_ancestor_accs = may_race_accs ~accs:ancestor_accs' ~todo:accs_todo in let todo_ancestor_outer_accs = may_race_accs ~accs:ancestor_outer_accs' ~todo:accs_todo in let todo_outer_accs = may_race_accs ~accs:outer_accs' ~todo:accs_todo in - let todo' = AS.union (AS.union todo_accs todo_ancestor_accs) (AS.union todo_ancestor_outer_accs todo_outer_accs) in + let todo_ancestor_accs_cross = may_race_accs ~accs:ancestor_accs' ~todo:(AS.inter todo outer_accs) in + let todo_outer_accs_cross = may_race_accs ~accs:outer_accs' ~todo:(AS.inter todo ancestor_accs) in + let todos = [todo_accs; todo_ancestor_accs; todo_ancestor_outer_accs; todo_outer_accs; todo_ancestor_accs_cross; todo_outer_accs_cross] in + let todo' = List.reduce AS.union todos in let visited' = AS.union visited todo in if AS.is_empty todo' then - (accs', visited') + (accs', ancestor_accs', ancestor_outer_accs', outer_accs', visited') else (bfs' [@tailcall]) ~ancestor_accs:ancestor_accs' ~ancestor_outer_accs:ancestor_outer_accs' ~outer_accs:outer_accs' ~accs:accs' ~todo:todo' ~visited:visited' in - let bfs accs acc = bfs' ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs ~todo:(AS.singleton acc) ~visited:(AS.empty ()) in + let bfs ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs acc = bfs' ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs ~todo:(AS.singleton acc) ~visited:(AS.empty ()) in (* repeat BFS to find all components *) - let rec components comps accs = + let rec components comps ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs = if AS.is_empty accs then - comps + (comps, ancestor_accs, outer_accs) else ( let acc = AS.choose accs in - let (accs', comp) = bfs accs acc in + let (accs', ancestor_accs', ancestor_outer_accs', outer_accs', comp) = bfs ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs acc in + let comps' = comp :: comps in + components comps' ~ancestor_accs:ancestor_accs' ~ancestor_outer_accs:ancestor_outer_accs' ~outer_accs:outer_accs' ~accs:accs' + ) + in + (* ignore (Pretty.printf "ancestors0: %a outer0: %a\n" AS.pretty ancestor_accs AS.pretty outer_accs); *) + let (comps, ancestor_accs, outer_accs) = components [] ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs in + (* ignore (Pretty.printf "ancestors: %a outer: %a\n" AS.pretty ancestor_accs AS.pretty outer_accs); *) + let rec components_cross comps ~ancestor_accs ~outer_accs = + if AS.is_empty ancestor_accs then + comps + else ( + let ancestor_acc = AS.choose ancestor_accs in + let (_, ancestor_accs', _, outer_accs', comp) = bfs ~ancestor_accs ~ancestor_outer_accs:(AS.empty ()) ~outer_accs ~accs:(AS.empty ()) ancestor_acc in + (* ignore (Pretty.printf "ancestor: %a comp: %a\n" A.pretty ancestor_acc AS.pretty comp); *) let comps' = comp :: comps in - components comps' accs' + components_cross comps' ~ancestor_accs:ancestor_accs' ~outer_accs:outer_accs' ) in - components [] accs + components_cross comps ~ancestor_accs ~outer_accs let race_conf accs = assert (not (AS.is_empty accs)); (* group_may_race should only construct non-empty components *) diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t index 4075dab33b..33bc8eede4 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -23,7 +23,9 @@ write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:44:3-44:24) [Info][Race] Memory locations race summary: - safe: 1 + safe: 2 vulnerable: 0 unsafe: 1 - total memory locations: 2 + total memory locations: 3 + +TODO: fix memory location numbers diff --git a/tests/regression/04-mutex/86-distribute-fields-3.t b/tests/regression/04-mutex/86-distribute-fields-3.t index 9651a91923..af17297db9 100644 --- a/tests/regression/04-mutex/86-distribute-fields-3.t +++ b/tests/regression/04-mutex/86-distribute-fields-3.t @@ -5,11 +5,15 @@ total lines: 8 [Success][Race] Memory location t@86-distribute-fields-3.c:15:10-15:11 (safe): write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) + [Success][Race] Memory location t.s@86-distribute-fields-3.c:15:10-15:11 (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [Warning][Race] Memory location t.s.data@86-distribute-fields-3.c:15:10-15:11 (race with conf. 110): write with [mhp:{tid=[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}, thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [Info][Race] Memory locations race summary: - safe: 1 + safe: 2 vulnerable: 0 unsafe: 1 - total memory locations: 2 + total memory locations: 3 + +TODO: fix memory location numbers diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t index dd862fa65a..65689ff4d4 100644 --- a/tests/regression/04-mutex/90-distribute-fields-type-1.t +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t @@ -17,11 +17,11 @@ live: 7 dead: 0 total lines: 7 + [Success][Race] Memory location (struct T).s (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) [Warning][Race] Memory location (struct T).s.field (race with conf. 100): write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) - [Success][Race] Memory location (struct T).s (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) [Success][Race] Memory location (struct S).field (safe): write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) [Info][Race] Memory locations race summary: diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t index 4cfb965e25..be365577f2 100644 --- a/tests/regression/04-mutex/91-distribute-fields-type-2.t +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t @@ -17,11 +17,11 @@ live: 7 dead: 0 total lines: 7 + [Success][Race] Memory location (struct T) (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:41:3-41:17) [Warning][Race] Memory location (struct T).s (race with conf. 100): write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:33:3-33:17) write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:41:3-41:17) - [Success][Race] Memory location (struct T) (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:41:3-41:17) [Success][Race] Memory location (struct S) (safe): write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:33:3-33:17) [Info][Race] Memory locations race summary: diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t index 12dc5e8f52..f605c4c4cf 100644 --- a/tests/regression/04-mutex/92-distribute-fields-type-deep.t +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -17,17 +17,19 @@ live: 7 dead: 0 total lines: 7 - [Success][Race] Memory location (struct T).s.field (safe): - write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) [Success][Race] Memory location (struct S).field (safe): write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) + [Success][Race] Memory location (struct U).t (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) + [Success][Race] Memory location (struct U).t.s (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) - [Success][Race] Memory location (struct U).t (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) [Info][Race] Memory locations race summary: - safe: 3 + safe: 4 vulnerable: 0 unsafe: 1 - total memory locations: 4 + total memory locations: 5 + +TODO: fix memory location numbers diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t index 30f61cb3cc..5a00f03dce 100644 --- a/tests/regression/04-mutex/93-distribute-fields-type-global.t +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t @@ -11,11 +11,11 @@ live: 7 dead: 0 total lines: 7 + [Success][Race] Memory location s@93-distribute-fields-type-global.c:9:10-9:11 (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:23:3-23:9) [Warning][Race] Memory location s.field@93-distribute-fields-type-global.c:9:10-9:11 (race with conf. 110): read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:14:3-14:29) write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:23:3-23:9) - [Success][Race] Memory location s@93-distribute-fields-type-global.c:9:10-9:11 (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:23:3-23:9) [Success][Race] Memory location (struct S).field (safe): read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:14:3-14:29) [Info][Race] Memory locations race summary: From edff1d3b94fdb84e26f3e98be6d0e3cf47548e2c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 22 Jun 2023 13:35:51 +0300 Subject: [PATCH 08/28] Fix memory location counts for cross races --- src/analyses/raceAnalysis.ml | 4 ++-- src/domains/access.ml | 7 ++++++- tests/regression/04-mutex/79-type-nested-fields-deep1.t | 6 ++---- tests/regression/04-mutex/86-distribute-fields-3.t | 8 ++------ .../regression/04-mutex/92-distribute-fields-type-deep.t | 8 ++------ 5 files changed, 14 insertions(+), 19 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index e0fbf96c2f..76b93892f6 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -153,10 +153,10 @@ struct | None -> Access.AS.empty () in M.trace "access" "outer accs = %a" Access.AS.pretty outer_accs; - if not (Access.AS.is_empty accs && Access.AS.is_empty ancestor_accs && Access.AS.is_empty outer_accs) then ( + if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty ancestor_accs) && not (Access.AS.is_empty outer_accs)) then ( let memo = (g', offset) in let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in - Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs ~ancestor_outer_accs ~outer_accs memo) accs + Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs ~ancestor_outer_accs ~outer_accs memo) accs ); let ancestor_outer_accs' = Access.AS.union ancestor_outer_accs outer_accs in let ancestor_accs' = Access.AS.union ancestor_accs accs in diff --git a/src/domains/access.ml b/src/domains/access.ml index 40ebb289db..9d5147f2b0 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -432,7 +432,12 @@ let group_may_race ~ancestor_accs ~ancestor_outer_accs ~outer_accs accs = let ancestor_acc = AS.choose ancestor_accs in let (_, ancestor_accs', _, outer_accs', comp) = bfs ~ancestor_accs ~ancestor_outer_accs:(AS.empty ()) ~outer_accs ~accs:(AS.empty ()) ancestor_acc in (* ignore (Pretty.printf "ancestor: %a comp: %a\n" A.pretty ancestor_acc AS.pretty comp); *) - let comps' = comp :: comps in + let comps' = + if AS.cardinal comp > 1 then + comp :: comps + else + comps (* ignore self-race ancestor_acc component, self-race checked at ancestor's level *) + in components_cross comps' ~ancestor_accs:ancestor_accs' ~outer_accs:outer_accs' ) in diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t index 33bc8eede4..4075dab33b 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -23,9 +23,7 @@ write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:44:3-44:24) [Info][Race] Memory locations race summary: - safe: 2 + safe: 1 vulnerable: 0 unsafe: 1 - total memory locations: 3 - -TODO: fix memory location numbers + total memory locations: 2 diff --git a/tests/regression/04-mutex/86-distribute-fields-3.t b/tests/regression/04-mutex/86-distribute-fields-3.t index af17297db9..9651a91923 100644 --- a/tests/regression/04-mutex/86-distribute-fields-3.t +++ b/tests/regression/04-mutex/86-distribute-fields-3.t @@ -5,15 +5,11 @@ total lines: 8 [Success][Race] Memory location t@86-distribute-fields-3.c:15:10-15:11 (safe): write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) - [Success][Race] Memory location t.s@86-distribute-fields-3.c:15:10-15:11 (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [Warning][Race] Memory location t.s.data@86-distribute-fields-3.c:15:10-15:11 (race with conf. 110): write with [mhp:{tid=[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}, thread:[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]] (conf. 110) (exp: & t.s.data) (86-distribute-fields-3.c:18:3-18:15) write with [mhp:{tid=[main]; created={[main, t_fun@86-distribute-fields-3.c:24:3-24:40#top]}}, thread:[main]] (conf. 110) (exp: & t) (86-distribute-fields-3.c:26:3-26:9) [Info][Race] Memory locations race summary: - safe: 2 + safe: 1 vulnerable: 0 unsafe: 1 - total memory locations: 3 - -TODO: fix memory location numbers + total memory locations: 2 diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t index f605c4c4cf..c0f3beae2c 100644 --- a/tests/regression/04-mutex/92-distribute-fields-type-deep.t +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -21,15 +21,11 @@ write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) [Success][Race] Memory location (struct U).t (safe): write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) - [Success][Race] Memory location (struct U).t.s (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) [Info][Race] Memory locations race summary: - safe: 4 + safe: 2 vulnerable: 0 unsafe: 1 - total memory locations: 5 - -TODO: fix memory location numbers + total memory locations: 3 From f419f50c0c26d35835235d6fb76084a7d8546fdb Mon Sep 17 00:00:00 2001 From: karoliineh Date: Thu, 22 Jun 2023 17:28:06 +0300 Subject: [PATCH 09/28] Replace print comments with tracing in group_may_race --- src/analyses/raceAnalysis.ml | 1 - src/domains/access.ml | 10 ++++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 76b93892f6..c004800db6 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -152,7 +152,6 @@ struct | Some outer_memo -> distribute_outer ctx outer_memo | None -> Access.AS.empty () in - M.trace "access" "outer accs = %a" Access.AS.pretty outer_accs; if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty ancestor_accs) && not (Access.AS.is_empty outer_accs)) then ( let memo = (g', offset) in let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in diff --git a/src/domains/access.ml b/src/domains/access.ml index 9d5147f2b0..b31d69baf6 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -379,6 +379,7 @@ let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),lo true let group_may_race ~ancestor_accs ~ancestor_outer_accs ~outer_accs accs = + if M.tracing then M.tracei "access" "group_may_race\n\tancestors_accs: %a\n\touter_accs: %a\n" AS.pretty ancestor_accs AS.pretty outer_accs; (* BFS to traverse one component with may_race edges *) let rec bfs' ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs ~todo ~visited = let may_race_accs ~accs ~todo = @@ -422,16 +423,15 @@ let group_may_race ~ancestor_accs ~ancestor_outer_accs ~outer_accs accs = components comps' ~ancestor_accs:ancestor_accs' ~ancestor_outer_accs:ancestor_outer_accs' ~outer_accs:outer_accs' ~accs:accs' ) in - (* ignore (Pretty.printf "ancestors0: %a outer0: %a\n" AS.pretty ancestor_accs AS.pretty outer_accs); *) let (comps, ancestor_accs, outer_accs) = components [] ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs in - (* ignore (Pretty.printf "ancestors: %a outer: %a\n" AS.pretty ancestor_accs AS.pretty outer_accs); *) + if M.tracing then M.trace "access" "components\n\tancestors_accs: %a\n\touter_accs: %a\n" AS.pretty ancestor_accs AS.pretty outer_accs; let rec components_cross comps ~ancestor_accs ~outer_accs = if AS.is_empty ancestor_accs then comps else ( let ancestor_acc = AS.choose ancestor_accs in let (_, ancestor_accs', _, outer_accs', comp) = bfs ~ancestor_accs ~ancestor_outer_accs:(AS.empty ()) ~outer_accs ~accs:(AS.empty ()) ancestor_acc in - (* ignore (Pretty.printf "ancestor: %a comp: %a\n" A.pretty ancestor_acc AS.pretty comp); *) + if M.tracing then M.trace "access" "components_cross\n\tancestors_accs: %a\n\touter_accs: %a\n" AS.pretty ancestor_accs' AS.pretty outer_accs'; let comps' = if AS.cardinal comp > 1 then comp :: comps @@ -441,7 +441,9 @@ let group_may_race ~ancestor_accs ~ancestor_outer_accs ~outer_accs accs = components_cross comps' ~ancestor_accs:ancestor_accs' ~outer_accs:outer_accs' ) in - components_cross comps ~ancestor_accs ~outer_accs + let components_cross = components_cross comps ~ancestor_accs ~outer_accs in + if M.tracing then M.traceu "access" "group_may_race\n"; + components_cross let race_conf accs = assert (not (AS.is_empty accs)); (* group_may_race should only construct non-empty components *) From 59feaf8beebfb16ec3e69bebe300ce781f4631bb Mon Sep 17 00:00:00 2001 From: karoliineh Date: Mon, 14 Aug 2023 18:05:18 +0300 Subject: [PATCH 10/28] Create warn_accs record and refactor Co-authored-by: Simmo Saan --- src/analyses/raceAnalysis.ml | 2 +- src/domains/access.ml | 83 +++++++++++++++++++----------------- 2 files changed, 45 insertions(+), 40 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index c004800db6..bc0709541d 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -155,7 +155,7 @@ struct if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty ancestor_accs) && not (Access.AS.is_empty outer_accs)) then ( let memo = (g', offset) in let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in - Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs ~ancestor_outer_accs ~outer_accs memo) accs + Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe {prefix=ancestor_accs; type_suffix_prefix=ancestor_outer_accs; type_suffix=outer_accs; node=accs}) memo ); let ancestor_outer_accs' = Access.AS.union ancestor_outer_accs outer_accs in let ancestor_accs' = Access.AS.union ancestor_accs accs in diff --git a/src/domains/access.ml b/src/domains/access.ml index b31d69baf6..918573835f 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -378,11 +378,18 @@ let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),lo else true -let group_may_race ~ancestor_accs ~ancestor_outer_accs ~outer_accs accs = - if M.tracing then M.tracei "access" "group_may_race\n\tancestors_accs: %a\n\touter_accs: %a\n" AS.pretty ancestor_accs AS.pretty outer_accs; +type warn_accs = { + node: AS.t; + prefix: AS.t; + type_suffix: AS.t; + type_suffix_prefix: AS.t; +} + +let group_may_race warn_accs = + if M.tracing then M.tracei "access" "group_may_race\n\tprefix: %a\n\ttype_suffix: %a\n" AS.pretty warn_accs.prefix AS.pretty warn_accs.type_suffix; (* BFS to traverse one component with may_race edges *) - let rec bfs' ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs ~todo ~visited = - let may_race_accs ~accs ~todo = + let rec bfs' {prefix; type_suffix_prefix; type_suffix; node} ~todo ~visited = + let may_race_accs ~accs ~todo = (* TODO: rename to from-to *) AS.fold (fun acc todo' -> AS.fold (fun acc' todo' -> if may_race acc acc' then @@ -392,56 +399,54 @@ let group_may_race ~ancestor_accs ~ancestor_outer_accs ~outer_accs accs = ) accs todo' ) todo (AS.empty ()) in - let accs' = AS.diff accs todo in - let ancestor_accs' = AS.diff ancestor_accs todo in - let ancestor_outer_accs' = AS.diff ancestor_outer_accs todo in - let outer_accs' = AS.diff outer_accs todo in - let todo_accs = may_race_accs ~accs:accs' ~todo in - let accs_todo = AS.inter todo accs in - let todo_ancestor_accs = may_race_accs ~accs:ancestor_accs' ~todo:accs_todo in - let todo_ancestor_outer_accs = may_race_accs ~accs:ancestor_outer_accs' ~todo:accs_todo in - let todo_outer_accs = may_race_accs ~accs:outer_accs' ~todo:accs_todo in - let todo_ancestor_accs_cross = may_race_accs ~accs:ancestor_accs' ~todo:(AS.inter todo outer_accs) in - let todo_outer_accs_cross = may_race_accs ~accs:outer_accs' ~todo:(AS.inter todo ancestor_accs) in - let todos = [todo_accs; todo_ancestor_accs; todo_ancestor_outer_accs; todo_outer_accs; todo_ancestor_accs_cross; todo_outer_accs_cross] in - let todo' = List.reduce AS.union todos in - let visited' = AS.union visited todo in + let node' = AS.diff node todo in + let prefix' = AS.diff prefix todo in + let type_suffix' = AS.diff type_suffix todo in + let type_suffix_prefix' = AS.diff type_suffix_prefix todo in + let todo_node = AS.inter todo node in + let todo_node' = may_race_accs ~accs:node' ~todo in + let todo_prefix' = may_race_accs ~accs:prefix' ~todo:(AS.union todo_node (AS.inter todo type_suffix)) in + let todo_type_suffix' = may_race_accs ~accs:type_suffix' ~todo:(AS.union todo_node (AS.inter todo prefix)) in + let todo_type_suffix_prefix' = may_race_accs ~accs:type_suffix_prefix' ~todo:todo_node in + let todo' = List.reduce AS.union [todo_node'; todo_prefix'; todo_type_suffix_prefix'; todo_type_suffix'] in + let visited' = AS.union visited todo in (* TODO: use warn_accs record for todo *) + let warn_accs' = {prefix=prefix'; type_suffix_prefix=type_suffix_prefix'; type_suffix=type_suffix'; node=node'} in if AS.is_empty todo' then - (accs', ancestor_accs', ancestor_outer_accs', outer_accs', visited') + (warn_accs', visited') else - (bfs' [@tailcall]) ~ancestor_accs:ancestor_accs' ~ancestor_outer_accs:ancestor_outer_accs' ~outer_accs:outer_accs' ~accs:accs' ~todo:todo' ~visited:visited' + (bfs' [@tailcall]) warn_accs' ~todo:todo' ~visited:visited' in - let bfs ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs acc = bfs' ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs ~todo:(AS.singleton acc) ~visited:(AS.empty ()) in + let bfs warn_accs acc = bfs' warn_accs ~todo:(AS.singleton acc) ~visited:(AS.empty ()) in (* repeat BFS to find all components *) - let rec components comps ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs = - if AS.is_empty accs then - (comps, ancestor_accs, outer_accs) + let rec components comps warn_accs = + if AS.is_empty warn_accs.node then + (comps, warn_accs) else ( - let acc = AS.choose accs in - let (accs', ancestor_accs', ancestor_outer_accs', outer_accs', comp) = bfs ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs acc in + let acc = AS.choose warn_accs.node in + let (warn_accs', comp) = bfs warn_accs acc in let comps' = comp :: comps in - components comps' ~ancestor_accs:ancestor_accs' ~ancestor_outer_accs:ancestor_outer_accs' ~outer_accs:outer_accs' ~accs:accs' + components comps' warn_accs' ) in - let (comps, ancestor_accs, outer_accs) = components [] ~ancestor_accs ~ancestor_outer_accs ~outer_accs ~accs in - if M.tracing then M.trace "access" "components\n\tancestors_accs: %a\n\touter_accs: %a\n" AS.pretty ancestor_accs AS.pretty outer_accs; - let rec components_cross comps ~ancestor_accs ~outer_accs = - if AS.is_empty ancestor_accs then + let (comps, warn_accs) = components [] warn_accs in + if M.tracing then M.trace "access" "components\n\tprefix: %a\n\ttype_suffix: %a\n" AS.pretty warn_accs.prefix AS.pretty warn_accs.type_suffix; + let rec components_cross comps ~prefix ~type_suffix = + if AS.is_empty prefix then comps else ( - let ancestor_acc = AS.choose ancestor_accs in - let (_, ancestor_accs', _, outer_accs', comp) = bfs ~ancestor_accs ~ancestor_outer_accs:(AS.empty ()) ~outer_accs ~accs:(AS.empty ()) ancestor_acc in - if M.tracing then M.trace "access" "components_cross\n\tancestors_accs: %a\n\touter_accs: %a\n" AS.pretty ancestor_accs' AS.pretty outer_accs'; + let prefix_acc = AS.choose prefix in + let (warn_accs', comp) = bfs {prefix; type_suffix_prefix=(AS.empty ()); type_suffix; node=(AS.empty ())} prefix_acc in + if M.tracing then M.trace "access" "components_cross\n\tprefix: %a\n\ttype_suffix: %a\n" AS.pretty warn_accs'.prefix AS.pretty warn_accs'.type_suffix; let comps' = if AS.cardinal comp > 1 then comp :: comps else - comps (* ignore self-race ancestor_acc component, self-race checked at ancestor's level *) + comps (* ignore self-race prefix_acc component, self-race checked at prefix's level *) in - components_cross comps' ~ancestor_accs:ancestor_accs' ~outer_accs:outer_accs' + components_cross comps' ~prefix:warn_accs'.prefix ~type_suffix:warn_accs'.type_suffix ) in - let components_cross = components_cross comps ~ancestor_accs ~outer_accs in + let components_cross = components_cross comps ~prefix:warn_accs.prefix ~type_suffix:warn_accs.type_suffix in if M.tracing then M.traceu "access" "group_may_race\n"; components_cross @@ -507,7 +512,7 @@ let print_accesses memo grouped_accs = M.msg_group Success ~category:Race "Memory location %a (safe)" Memo.pretty memo (msgs safe_accs) ) -let warn_global ~safe ~vulnerable ~unsafe ~ancestor_accs ~ancestor_outer_accs ~outer_accs memo accs = - let grouped_accs = group_may_race ~ancestor_accs ~ancestor_outer_accs ~outer_accs accs in (* do expensive component finding only once *) +let warn_global ~safe ~vulnerable ~unsafe warn_accs memo = + let grouped_accs = group_may_race warn_accs in (* do expensive component finding only once *) incr_summary ~safe ~vulnerable ~unsafe memo grouped_accs; print_accesses memo grouped_accs From 49e529f627e9fc1ae8fe9f4fbd6b31a065fc6cbf Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 15 Aug 2023 10:55:09 +0300 Subject: [PATCH 11/28] Refactor distribute_inner in raceAnalysis --- src/analyses/raceAnalysis.ml | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index bc0709541d..2cf97afffd 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -111,7 +111,7 @@ struct ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.empty ())))); side_vars ctx memo - let outer_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option = + let type_suffix_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option = match root, offset with | `Var v, _ -> Some (`Type v.vtype, offset) (* TODO: Alloc variables void type *) | _, `NoOffset -> None @@ -125,12 +125,12 @@ struct | `Lifted accs -> accs | `Bot -> Access.AS.empty () in - let outer_accs = - match outer_memo (root, offset) with - | Some outer_memo -> distribute_outer ctx outer_memo + let type_suffix = + match type_suffix_memo (root, offset) with + | Some type_suffix_memo -> distribute_outer ctx type_suffix_memo | None -> Access.AS.empty () in - Access.AS.union accs outer_accs + Access.AS.union accs type_suffix let query ctx (type a) (q: a Queries.t): a Queries.result = match q with @@ -141,29 +141,29 @@ struct (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *) let trie = G.access (ctx.global g) in (** Distribute access to contained fields. *) - let rec distribute_inner offset (accs, children) ~ancestor_accs ~ancestor_outer_accs = + let rec distribute_inner offset (accs, children) ~prefix ~type_suffix_prefix = let accs = match accs with | `Lifted accs -> accs | `Bot -> Access.AS.empty () in - let outer_accs = - match outer_memo (g', offset) with - | Some outer_memo -> distribute_outer ctx outer_memo + let type_suffix = + match type_suffix_memo (g', offset) with + | Some type_suffix_memo -> distribute_outer ctx type_suffix_memo | None -> Access.AS.empty () in - if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty ancestor_accs) && not (Access.AS.is_empty outer_accs)) then ( + if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty prefix) && not (Access.AS.is_empty type_suffix)) then ( let memo = (g', offset) in let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in - Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe {prefix=ancestor_accs; type_suffix_prefix=ancestor_outer_accs; type_suffix=outer_accs; node=accs}) memo + Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe {prefix; type_suffix_prefix; type_suffix; node=accs}) memo ); - let ancestor_outer_accs' = Access.AS.union ancestor_outer_accs outer_accs in - let ancestor_accs' = Access.AS.union ancestor_accs accs in + let prefix' = Access.AS.union prefix accs in + let type_suffix_prefix' = Access.AS.union type_suffix_prefix type_suffix in OffsetTrie.ChildMap.iter (fun child_key child_trie -> - distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ~ancestor_accs:ancestor_accs' ~ancestor_outer_accs:ancestor_outer_accs' + distribute_inner (Offset.Unit.add_offset offset (OneOffset.to_offset child_key)) child_trie ~prefix:prefix' ~type_suffix_prefix:type_suffix_prefix' ) children; in - distribute_inner `NoOffset trie ~ancestor_accs:(Access.AS.empty ()) ~ancestor_outer_accs:(Access.AS.empty ()) + distribute_inner `NoOffset trie ~prefix:(Access.AS.empty ()) ~type_suffix_prefix:(Access.AS.empty ()) | `Right _ -> (* vars *) () end From 64c761bee01954873ce85148d9cb1b818f0d238f Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 15 Aug 2023 11:29:24 +0300 Subject: [PATCH 12/28] Use warn_accs for todo Co-authored-by: Simmo Saan --- src/domains/access.ml | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/domains/access.ml b/src/domains/access.ml index 918573835f..85626c4463 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -399,31 +399,31 @@ let group_may_race warn_accs = ) accs todo' ) todo (AS.empty ()) in - let node' = AS.diff node todo in - let prefix' = AS.diff prefix todo in - let type_suffix' = AS.diff type_suffix todo in - let type_suffix_prefix' = AS.diff type_suffix_prefix todo in - let todo_node = AS.inter todo node in - let todo_node' = may_race_accs ~accs:node' ~todo in - let todo_prefix' = may_race_accs ~accs:prefix' ~todo:(AS.union todo_node (AS.inter todo type_suffix)) in - let todo_type_suffix' = may_race_accs ~accs:type_suffix' ~todo:(AS.union todo_node (AS.inter todo prefix)) in - let todo_type_suffix_prefix' = may_race_accs ~accs:type_suffix_prefix' ~todo:todo_node in - let todo' = List.reduce AS.union [todo_node'; todo_prefix'; todo_type_suffix_prefix'; todo_type_suffix'] in - let visited' = AS.union visited todo in (* TODO: use warn_accs record for todo *) + let node' = AS.diff node todo.node in + let prefix' = AS.diff prefix todo.prefix in + let type_suffix' = AS.diff type_suffix todo.type_suffix in + let type_suffix_prefix' = AS.diff type_suffix_prefix todo.type_suffix_prefix in + let todo_all = AS.union todo.node (AS.union (AS.union todo.prefix todo.type_suffix) todo.type_suffix_prefix) in + let todo_node' = may_race_accs ~accs:node' ~todo:todo_all in + let todo_prefix' = may_race_accs ~accs:prefix' ~todo:(AS.union todo.node todo.type_suffix) in + let todo_type_suffix' = may_race_accs ~accs:type_suffix' ~todo:(AS.union todo.node todo.prefix) in + let todo_type_suffix_prefix' = may_race_accs ~accs:type_suffix_prefix' ~todo:todo.node in + let todo' = {prefix=todo_prefix'; type_suffix=todo_type_suffix'; type_suffix_prefix=todo_type_suffix_prefix'; node=todo_node'} in + let visited' = AS.union visited todo_all in let warn_accs' = {prefix=prefix'; type_suffix_prefix=type_suffix_prefix'; type_suffix=type_suffix'; node=node'} in - if AS.is_empty todo' then + if AS.is_empty todo'.node && AS.is_empty todo'.prefix && AS.is_empty todo'.type_suffix && AS.is_empty todo'.type_suffix_prefix then (warn_accs', visited') else (bfs' [@tailcall]) warn_accs' ~todo:todo' ~visited:visited' in - let bfs warn_accs acc = bfs' warn_accs ~todo:(AS.singleton acc) ~visited:(AS.empty ()) in + let bfs warn_accs todo = bfs' warn_accs ~todo ~visited:(AS.empty ()) in (* repeat BFS to find all components *) let rec components comps warn_accs = if AS.is_empty warn_accs.node then (comps, warn_accs) else ( let acc = AS.choose warn_accs.node in - let (warn_accs', comp) = bfs warn_accs acc in + let (warn_accs', comp) = bfs warn_accs {node=AS.singleton acc; prefix=AS.empty (); type_suffix=AS.empty (); type_suffix_prefix=AS.empty ()} in let comps' = comp :: comps in components comps' warn_accs' ) @@ -435,7 +435,7 @@ let group_may_race warn_accs = comps else ( let prefix_acc = AS.choose prefix in - let (warn_accs', comp) = bfs {prefix; type_suffix_prefix=(AS.empty ()); type_suffix; node=(AS.empty ())} prefix_acc in + let (warn_accs', comp) = bfs {prefix; type_suffix_prefix=(AS.empty ()); type_suffix; node=(AS.empty ())} {node=AS.empty (); prefix=AS.singleton prefix_acc; type_suffix=AS.empty (); type_suffix_prefix=AS.empty ()} in if M.tracing then M.trace "access" "components_cross\n\tprefix: %a\n\ttype_suffix: %a\n" AS.pretty warn_accs'.prefix AS.pretty warn_accs'.type_suffix; let comps' = if AS.cardinal comp > 1 then From b06b3e342981f8dfda512b58c1e1049053332321 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 15 Aug 2023 11:48:23 +0300 Subject: [PATCH 13/28] Make warn_accs record to a module Co-authored-by: Simmo Saan --- src/domains/access.ml | 77 ++++++++++++++++++++++++++++--------------- 1 file changed, 50 insertions(+), 27 deletions(-) diff --git a/src/domains/access.ml b/src/domains/access.ml index 85626c4463..4c752096ac 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -378,17 +378,42 @@ let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),lo else true -type warn_accs = { - node: AS.t; - prefix: AS.t; - type_suffix: AS.t; - type_suffix_prefix: AS.t; -} - -let group_may_race warn_accs = - if M.tracing then M.tracei "access" "group_may_race\n\tprefix: %a\n\ttype_suffix: %a\n" AS.pretty warn_accs.prefix AS.pretty warn_accs.type_suffix; +module WarnAccs = +struct + type t = { + node: AS.t; + prefix: AS.t; + type_suffix: AS.t; + type_suffix_prefix: AS.t; + } + + let diff w1 w2 = { + node = AS.diff w1.node w2.node; + prefix = AS.diff w1.prefix w2.prefix; + type_suffix = AS.diff w1.type_suffix w2.type_suffix; + type_suffix_prefix = AS.diff w1.type_suffix_prefix w2.type_suffix_prefix; + } + + let union_all w = + AS.union + (AS.union w.node w.prefix) + (AS.union w.type_suffix w.type_suffix_prefix) + + let is_empty w = + AS.is_empty w.node && AS.is_empty w.prefix && AS.is_empty w.type_suffix && AS.is_empty w.type_suffix_prefix + + let empty () = + {node=AS.empty (); prefix=AS.empty (); type_suffix=AS.empty (); type_suffix_prefix=AS.empty ()} + + let pretty () w = + Pretty.dprintf "{node = %a; prefix = %a; type_suffix = %a; type_suffix_prefix = %a}" + AS.pretty w.node AS.pretty w.prefix AS.pretty w.type_suffix AS.pretty w.type_suffix_prefix +end + +let group_may_race (warn_accs:WarnAccs.t) = + if M.tracing then M.tracei "access" "group_may_race %a\n" WarnAccs.pretty warn_accs; (* BFS to traverse one component with may_race edges *) - let rec bfs' {prefix; type_suffix_prefix; type_suffix; node} ~todo ~visited = + let rec bfs' warn_accs ~todo ~visited = let may_race_accs ~accs ~todo = (* TODO: rename to from-to *) AS.fold (fun acc todo' -> AS.fold (fun acc' todo' -> @@ -399,44 +424,42 @@ let group_may_race warn_accs = ) accs todo' ) todo (AS.empty ()) in - let node' = AS.diff node todo.node in - let prefix' = AS.diff prefix todo.prefix in - let type_suffix' = AS.diff type_suffix todo.type_suffix in - let type_suffix_prefix' = AS.diff type_suffix_prefix todo.type_suffix_prefix in - let todo_all = AS.union todo.node (AS.union (AS.union todo.prefix todo.type_suffix) todo.type_suffix_prefix) in - let todo_node' = may_race_accs ~accs:node' ~todo:todo_all in - let todo_prefix' = may_race_accs ~accs:prefix' ~todo:(AS.union todo.node todo.type_suffix) in - let todo_type_suffix' = may_race_accs ~accs:type_suffix' ~todo:(AS.union todo.node todo.prefix) in - let todo_type_suffix_prefix' = may_race_accs ~accs:type_suffix_prefix' ~todo:todo.node in - let todo' = {prefix=todo_prefix'; type_suffix=todo_type_suffix'; type_suffix_prefix=todo_type_suffix_prefix'; node=todo_node'} in + let warn_accs' = WarnAccs.diff warn_accs todo in + let todo_all = WarnAccs.union_all todo in let visited' = AS.union visited todo_all in - let warn_accs' = {prefix=prefix'; type_suffix_prefix=type_suffix_prefix'; type_suffix=type_suffix'; node=node'} in - if AS.is_empty todo'.node && AS.is_empty todo'.prefix && AS.is_empty todo'.type_suffix && AS.is_empty todo'.type_suffix_prefix then + let todo' : WarnAccs.t = { + node = may_race_accs ~accs:warn_accs'.node ~todo:todo_all; + prefix = may_race_accs ~accs:warn_accs'.prefix ~todo:(AS.union todo.node todo.type_suffix); + type_suffix = may_race_accs ~accs:warn_accs'.type_suffix ~todo:(AS.union todo.node todo.prefix); + type_suffix_prefix = may_race_accs ~accs:warn_accs'.type_suffix_prefix ~todo:todo.node + } + in + if WarnAccs.is_empty todo' then (warn_accs', visited') else (bfs' [@tailcall]) warn_accs' ~todo:todo' ~visited:visited' in let bfs warn_accs todo = bfs' warn_accs ~todo ~visited:(AS.empty ()) in (* repeat BFS to find all components *) - let rec components comps warn_accs = + let rec components comps (warn_accs:WarnAccs.t) = if AS.is_empty warn_accs.node then (comps, warn_accs) else ( let acc = AS.choose warn_accs.node in - let (warn_accs', comp) = bfs warn_accs {node=AS.singleton acc; prefix=AS.empty (); type_suffix=AS.empty (); type_suffix_prefix=AS.empty ()} in + let (warn_accs', comp) = bfs warn_accs {(WarnAccs.empty ()) with node=AS.singleton acc} in let comps' = comp :: comps in components comps' warn_accs' ) in let (comps, warn_accs) = components [] warn_accs in - if M.tracing then M.trace "access" "components\n\tprefix: %a\n\ttype_suffix: %a\n" AS.pretty warn_accs.prefix AS.pretty warn_accs.type_suffix; + if M.tracing then M.trace "access" "components %a\n" WarnAccs.pretty warn_accs; let rec components_cross comps ~prefix ~type_suffix = if AS.is_empty prefix then comps else ( let prefix_acc = AS.choose prefix in - let (warn_accs', comp) = bfs {prefix; type_suffix_prefix=(AS.empty ()); type_suffix; node=(AS.empty ())} {node=AS.empty (); prefix=AS.singleton prefix_acc; type_suffix=AS.empty (); type_suffix_prefix=AS.empty ()} in - if M.tracing then M.trace "access" "components_cross\n\tprefix: %a\n\ttype_suffix: %a\n" AS.pretty warn_accs'.prefix AS.pretty warn_accs'.type_suffix; + let (warn_accs', comp) = bfs {(WarnAccs.empty ()) with prefix; type_suffix} {(WarnAccs.empty ()) with prefix=AS.singleton prefix_acc} in + if M.tracing then M.trace "access" "components_cross %a\n" WarnAccs.pretty warn_accs'; let comps' = if AS.cardinal comp > 1 then comp :: comps From 69ddfdffab00cf5c3699a9490d86d64800b990c3 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 15 Aug 2023 12:13:20 +0300 Subject: [PATCH 14/28] Refactor and document todo' computation Co-authored-by: Simmo Saan --- src/domains/access.ml | 32 ++++++++++++++++++++++++-------- 1 file changed, 24 insertions(+), 8 deletions(-) diff --git a/src/domains/access.ml b/src/domains/access.ml index 4c752096ac..6a802e5c14 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -414,7 +414,11 @@ let group_may_race (warn_accs:WarnAccs.t) = if M.tracing then M.tracei "access" "group_may_race %a\n" WarnAccs.pretty warn_accs; (* BFS to traverse one component with may_race edges *) let rec bfs' warn_accs ~todo ~visited = - let may_race_accs ~accs ~todo = (* TODO: rename to from-to *) + let warn_accs' = WarnAccs.diff warn_accs todo in + let todo_all = WarnAccs.union_all todo in + let visited' = AS.union visited todo_all in + + let step_may_race ~todo ~accs = (* step from todo to accs if may_race *) AS.fold (fun acc todo' -> AS.fold (fun acc' todo' -> if may_race acc acc' then @@ -424,16 +428,28 @@ let group_may_race (warn_accs:WarnAccs.t) = ) accs todo' ) todo (AS.empty ()) in - let warn_accs' = WarnAccs.diff warn_accs todo in - let todo_all = WarnAccs.union_all todo in - let visited' = AS.union visited todo_all in + (* Undirected graph of may_race checks: + + type_suffix_prefix + | + | + type_suffix --+-- prefix + \ | / + \ | / + node + / \ + \_/ + + Each undirected edge is handled by two opposite step_may_race-s. + All missing edges are checked at other nodes by other group_may_race calls. *) let todo' : WarnAccs.t = { - node = may_race_accs ~accs:warn_accs'.node ~todo:todo_all; - prefix = may_race_accs ~accs:warn_accs'.prefix ~todo:(AS.union todo.node todo.type_suffix); - type_suffix = may_race_accs ~accs:warn_accs'.type_suffix ~todo:(AS.union todo.node todo.prefix); - type_suffix_prefix = may_race_accs ~accs:warn_accs'.type_suffix_prefix ~todo:todo.node + node = step_may_race ~todo:todo_all ~accs:warn_accs'.node; + prefix = step_may_race ~todo:(AS.union todo.node todo.type_suffix) ~accs:warn_accs'.prefix; + type_suffix = step_may_race ~todo:(AS.union todo.node todo.prefix) ~accs:warn_accs'.type_suffix; + type_suffix_prefix = step_may_race ~todo:todo.node ~accs:warn_accs'.type_suffix_prefix } in + if WarnAccs.is_empty todo' then (warn_accs', visited') else From 857d1cbaa31673ced488acbf42b97f9e3c3413aa Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 15 Aug 2023 12:36:18 +0300 Subject: [PATCH 15/28] Use Typsig for Access MemoRoot Co-authored-by: Simmo Saan --- src/analyses/raceAnalysis.ml | 6 +++--- src/domains/access.ml | 29 +++++++++-------------------- 2 files changed, 12 insertions(+), 23 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 2cf97afffd..72d73f9de1 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -113,9 +113,9 @@ struct let type_suffix_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option = match root, offset with - | `Var v, _ -> Some (`Type v.vtype, offset) (* TODO: Alloc variables void type *) + | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* TODO: Alloc variables void type *) | _, `NoOffset -> None - | _, `Field (f, offset') -> Some (`Type f.ftype, offset') + | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') | _, `Index ((), offset') -> None (* TODO *) let rec distribute_outer ctx ((root, offset) : Access.Memo.t) : Access.AS.t = @@ -190,7 +190,7 @@ struct in let add_access_struct conf ci = let a = part_access None in - Access.add_one (side_access octx (conf, kind, loc, e, a)) (`Type (TComp (ci, [])), `NoOffset) + Access.add_one (side_access octx (conf, kind, loc, e, a)) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset) in let has_escaped g = octx.ask (Queries.MayEscape g) in (* The following function adds accesses to the lval-set ls diff --git a/src/domains/access.ml b/src/domains/access.ml index 6a802e5c14..ce71fcc98c 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -83,8 +83,7 @@ type acc_typ = [ `Type of CilType.Typ.t | `Struct of CilType.Compinfo.t * Offset module MemoRoot = struct include Printable.StdLeaf - type t = [`Var of CilType.Varinfo.t | `Type of CilType.Typ.t] [@@deriving eq, ord, hash] - (* Can't use typsig for `Type because there's no function to follow offsets on typsig. *) + type t = [`Var of CilType.Varinfo.t | `Type of CilType.Typsig.t] [@@deriving eq, ord, hash] let name () = "memoroot" @@ -92,8 +91,8 @@ struct (* Imitate old printing for now *) match vt with | `Var v -> Pretty.dprintf "%a@@%a" CilType.Varinfo.pretty v CilType.Location.pretty v.vdecl - | `Type (TComp (c, _)) -> Pretty.dprintf "(struct %s)" c.cname - | `Type t -> Pretty.dprintf "(%a)" CilType.Typ.pretty t + | `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)" name + | `Type t -> Pretty.dprintf "(%a)" CilType.Typsig.pretty t include Printable.SimplePretty ( struct @@ -108,7 +107,6 @@ module Memo = struct include Printable.StdLeaf type t = MemoRoot.t * Offset.Unit.t [@@deriving eq, ord, hash] - (* Can't use typsig for `Type because there's no function to follow offsets on typsig. *) let name () = "memo" @@ -116,8 +114,8 @@ struct (* Imitate old printing for now *) match vt with | `Var v -> Pretty.dprintf "%a%a@@%a" CilType.Varinfo.pretty v Offset.Unit.pretty o CilType.Location.pretty v.vdecl - | `Type (TComp (c, _)) -> Pretty.dprintf "(struct %s)%a" c.cname Offset.Unit.pretty o - | `Type t -> Pretty.dprintf "(%a)%a" CilType.Typ.pretty t Offset.Unit.pretty o + | `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)%a" name Offset.Unit.pretty o + | `Type t -> Pretty.dprintf "(%a)%a" CilType.Typsig.pretty t Offset.Unit.pretty o include Printable.SimplePretty ( struct @@ -128,23 +126,14 @@ struct let of_ty (ty: acc_typ): t = match ty with - | `Struct (c, o) -> (`Type (TComp (c, [])), o) - | `Type t -> (`Type t, `NoOffset) + | `Struct (c, o) -> (`Type (TSComp (c.cstruct, c.cname, [])), o) + | `Type t -> (`Type (Cil.typeSig t), `NoOffset) let to_mval: t -> Mval.Unit.t option = function | (`Var v, o) -> Some (v, o) | (`Type _, _) -> None let add_offset ((vt, o): t) o2: t = (vt, Offset.Unit.add_offset o o2) - - let type_of_base ((vt, _): t): typ = - match vt with - | `Var v -> v.vtype - | `Type t -> t - - (** @raise Offset.Type_of_error *) - let type_of ((vt, o) as memo: t): typ = - Offset.Unit.type_of ~base:(type_of_base memo) o end (* TODO: What is the logic for get_type? *) @@ -213,12 +202,12 @@ let add_one side memo: unit = (** Distribute type-based access to variables and containing fields. *) let rec add_distribute_outer side side0 (t: typ) (o: Offset.Unit.t) = - let memo = (`Type t, o) in + let ts = typeSig t in + let memo = (`Type ts, o) in if M.tracing then M.tracei "access" "add_distribute_outer %a\n" Memo.pretty memo; add_one side memo; (* distribute to variables of the type *) - let ts = typeSig t in let vars = TSH.find_all typeVar ts in List.iter (fun v -> add_one side0 (`Var v, o) (* same offset, but on variable *) From b28cbba1abb527b6d1768bbd1bd584348d49d2e3 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 15 Aug 2023 13:32:38 +0300 Subject: [PATCH 16/28] Fix index in type_suffix_memo Co-authored-by: Simmo Saan --- src/analyses/raceAnalysis.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 72d73f9de1..f8705613c8 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -116,7 +116,8 @@ struct | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* TODO: Alloc variables void type *) | _, `NoOffset -> None | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') - | _, `Index ((), offset') -> None (* TODO *) + | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') + | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *) let rec distribute_outer ctx ((root, offset) : Access.Memo.t) : Access.AS.t = let trie = G.access (ctx.global (V.access root)) in From d6c5bbac05531ec6f52b2f45d419f841a61793cb Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 15 Aug 2023 13:58:54 +0300 Subject: [PATCH 17/28] Make new cram tests deterministic Co-authored-by: Simmo Saan --- .../04-mutex/77-type-nested-fields.t | 38 ++++++++--------- .../04-mutex/79-type-nested-fields-deep1.t | 38 ++++++++--------- .../04-mutex/80-type-nested-fields-deep2.t | 38 ++++++++--------- .../04-mutex/90-distribute-fields-type-1.t | 42 +++++++++---------- .../04-mutex/91-distribute-fields-type-2.t | 42 +++++++++---------- .../04-mutex/92-distribute-fields-type-deep.t | 42 +++++++++---------- .../93-distribute-fields-type-global.t | 32 +++++++------- 7 files changed, 136 insertions(+), 136 deletions(-) diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t index 2cbd339dfa..dc87d0a85e 100644 --- a/tests/regression/04-mutex/77-type-nested-fields.t +++ b/tests/regression/04-mutex/77-type-nested-fields.t @@ -1,29 +1,29 @@ - $ goblint --enable allglobs 77-type-nested-fields.c - [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:32:3-32:20) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:32:3-32:20) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:32:3-32:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:32:3-32:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:32:3-32:20) + $ goblint --enable warn.deterministic --enable allglobs 77-type-nested-fields.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:32:3-32:20) - [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:32:3-32:20) - [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:39:3-39:22) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:39:3-39:22) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:39:3-39:22) - [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:39:3-39:22) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:39:3-39:22) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:39:3-39:22) - [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:39:3-39:22) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 7 - dead: 0 - total lines: 7 [Warning][Race] Memory location (struct T).s.field (race with conf. 100): write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:32:3-32:20) write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:39:3-39:22) - [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:32:3-32:20) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:32:3-32:20) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:32:3-32:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:32:3-32:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:32:3-32:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:39:3-39:22) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:39:3-39:22) + [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:39:3-39:22) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:32:3-32:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:32:3-32:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:39:3-39:22) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:39:3-39:22) + [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:32:3-32:20) + [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:39:3-39:22) diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t index 4075dab33b..5fc60223b9 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -1,24 +1,6 @@ - $ goblint --enable allglobs 79-type-nested-fields-deep1.c - [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:37:3-37:20) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:37:3-37:20) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:37:3-37:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:37:3-37:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:37:3-37:20) + $ goblint --enable warn.deterministic --enable allglobs 79-type-nested-fields-deep1.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:37:3-37:20) - [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:37:3-37:20) - [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:44:3-44:24) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:44:3-44:24) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:44:3-44:24) - [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:44:3-44:24) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:44:3-44:24) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:44:3-44:24) - [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:44:3-44:24) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 7 - dead: 0 - total lines: 7 - [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:44:3-44:24) @@ -27,3 +9,21 @@ vulnerable: 0 unsafe: 1 total memory locations: 2 + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:37:3-37:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:44:3-44:24) + [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:37:3-37:20) + [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:44:3-44:24) diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t index f14a315de2..a0541235ee 100644 --- a/tests/regression/04-mutex/80-type-nested-fields-deep2.t +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t @@ -1,24 +1,6 @@ - $ goblint --enable allglobs 80-type-nested-fields-deep2.c - [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:37:3-37:22) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:37:3-37:22) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:37:3-37:22) - [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:37:3-37:22) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:37:3-37:22) + $ goblint --enable warn.deterministic --enable allglobs 80-type-nested-fields-deep2.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:37:3-37:22) - [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:37:3-37:22) - [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:44:3-44:24) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:44:3-44:24) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:44:3-44:24) - [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:44:3-44:24) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:44:3-44:24) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:44:3-44:24) - [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:44:3-44:24) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 7 - dead: 0 - total lines: 7 - [Success][Race] Memory location (struct T).s.field (safe): - write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:37:3-37:22) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:37:3-37:22) write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:44:3-44:24) @@ -27,3 +9,21 @@ vulnerable: 0 unsafe: 1 total memory locations: 2 + [Success][Race] Memory location (struct T).s.field (safe): + write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:37:3-37:22) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:44:3-44:24) + [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:37:3-37:22) + [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:44:3-44:24) diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t index 65689ff4d4..fb6af7ceca 100644 --- a/tests/regression/04-mutex/90-distribute-fields-type-1.t +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t @@ -1,31 +1,31 @@ - $ goblint --enable allglobs 90-distribute-fields-type-1.c - [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:32:3-32:20) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:32:3-32:20) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:32:3-32:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:32:3-32:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:32:3-32:20) + $ goblint --enable warn.deterministic --enable allglobs 90-distribute-fields-type-1.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:32:3-32:20) - [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:32:3-32:20) - [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:40:3-40:17) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:40:3-40:17) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:40:3-40:17) - [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:40:3-40:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:40:3-40:17) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:40:3-40:17) - [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:40:3-40:17) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 7 - dead: 0 - total lines: 7 - [Success][Race] Memory location (struct T).s (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) [Warning][Race] Memory location (struct T).s.field (race with conf. 100): write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) - [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) + [Success][Race] Memory location (struct T).s (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:32:3-32:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:40:3-40:17) + [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:32:3-32:20) + [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:40:3-40:17) diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t index be365577f2..0b4ec982e8 100644 --- a/tests/regression/04-mutex/91-distribute-fields-type-2.t +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t @@ -1,31 +1,31 @@ - $ goblint --enable allglobs 91-distribute-fields-type-2.c - [Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:33:3-33:17) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:33:3-33:17) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:33:3-33:17) - [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:33:3-33:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:33:3-33:17) + $ goblint --enable warn.deterministic --enable allglobs 91-distribute-fields-type-2.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:33:3-33:17) - [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:33:3-33:17) - [Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:41:3-41:17) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:41:3-41:17) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:41:3-41:17) - [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:41:3-41:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:41:3-41:17) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:41:3-41:17) - [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:41:3-41:17) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 7 - dead: 0 - total lines: 7 - [Success][Race] Memory location (struct T) (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:41:3-41:17) [Warning][Race] Memory location (struct T).s (race with conf. 100): write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:33:3-33:17) write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:41:3-41:17) - [Success][Race] Memory location (struct S) (safe): - write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:33:3-33:17) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 + [Success][Race] Memory location (struct S) (safe): + write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:33:3-33:17) + [Success][Race] Memory location (struct T) (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:33:3-33:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:41:3-41:17) + [Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:33:3-33:17) + [Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:41:3-41:17) diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t index c0f3beae2c..aedc66f101 100644 --- a/tests/regression/04-mutex/92-distribute-fields-type-deep.t +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -1,26 +1,6 @@ - $ goblint --enable allglobs 92-distribute-fields-type-deep.c - [Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:37:3-37:20) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:37:3-37:20) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:37:3-37:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:37:3-37:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:37:3-37:20) + $ goblint --enable warn.deterministic --enable allglobs 92-distribute-fields-type-deep.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:37:3-37:20) - [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:37:3-37:20) - [Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:45:3-45:17) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:45:3-45:17) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:45:3-45:17) - [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:45:3-45:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:45:3-45:17) [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:45:3-45:17) - [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:45:3-45:17) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 7 - dead: 0 - total lines: 7 - [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) - [Success][Race] Memory location (struct U).t (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) @@ -29,3 +9,23 @@ vulnerable: 0 unsafe: 1 total memory locations: 3 + [Success][Race] Memory location (struct S).field (safe): + write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) + [Success][Race] Memory location (struct U).t (safe): + write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:37:3-37:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:37:3-37:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:37:3-37:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:37:3-37:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:37:3-37:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:45:3-45:17) + [Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:37:3-37:20) + [Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:45:3-45:17) diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t index 3761e9f7b4..fcc3e804c7 100644 --- a/tests/regression/04-mutex/93-distribute-fields-type-global.t +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t @@ -1,25 +1,25 @@ - $ goblint --enable allglobs 93-distribute-fields-type-global.c - [Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Unsound] Unknown address in {&tmp} has escaped. (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (93-distribute-fields-type-global.c:14:3-14:29) + $ goblint --enable warn.deterministic --enable allglobs 93-distribute-fields-type-global.c [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Unsound] Write to unknown address: privatization is unsound. (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 7 - dead: 0 - total lines: 7 - [Success][Race] Memory location s (safe): (93-distribute-fields-type-global.c:9:10-9:11) - write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:23:3-23:9) [Warning][Race] Memory location s.field (race with conf. 110): (93-distribute-fields-type-global.c:9:10-9:11) read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:14:3-14:29) write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:23:3-23:9) - [Success][Race] Memory location (struct S).field (safe): - read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:14:3-14:29) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 + [Success][Race] Memory location (struct S).field (safe): + read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:14:3-14:29) + [Success][Race] Memory location s (safe): (93-distribute-fields-type-global.c:9:10-9:11) + write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:23:3-23:9) + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 7 + dead: 0 + total lines: 7 + [Info][Unsound] Unknown address in {&tmp} has escaped. (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Unsound] Write to unknown address: privatization is unsound. (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (93-distribute-fields-type-global.c:14:3-14:29) + [Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:14:3-14:29) From 21332cc346d78e84f5b51d24800e005971db2a08 Mon Sep 17 00:00:00 2001 From: karoliineh Date: Tue, 15 Aug 2023 14:17:18 +0300 Subject: [PATCH 18/28] Refactor distribute_outer Co-authored-by: Simmo Saan --- src/analyses/raceAnalysis.ml | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 93c2f0994f..5f100c869a 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -119,20 +119,21 @@ struct | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *) - let rec distribute_outer ctx ((root, offset) : Access.Memo.t) : Access.AS.t = + let rec find_type_suffix' ctx ((root, offset) as memo : Access.Memo.t) : Access.AS.t = let trie = G.access (ctx.global (V.access root)) in let accs = match OffsetTrie.find offset trie with | `Lifted accs -> accs | `Bot -> Access.AS.empty () in - let type_suffix = - match type_suffix_memo (root, offset) with - | Some type_suffix_memo -> distribute_outer ctx type_suffix_memo - | None -> Access.AS.empty () - in + let type_suffix = find_type_suffix ctx memo in Access.AS.union accs type_suffix + and find_type_suffix ctx (memo : Access.Memo.t) : Access.AS.t = + match type_suffix_memo memo with + | Some type_suffix_memo -> find_type_suffix' ctx type_suffix_memo + | None -> Access.AS.empty () + let query ctx (type a) (q: a Queries.t): a Queries.result = match q with | WarnGlobal g -> @@ -148,11 +149,7 @@ struct | `Lifted accs -> accs | `Bot -> Access.AS.empty () in - let type_suffix = - match type_suffix_memo (g', offset) with - | Some type_suffix_memo -> distribute_outer ctx type_suffix_memo - | None -> Access.AS.empty () - in + let type_suffix = find_type_suffix ctx (g', offset) in if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty prefix) && not (Access.AS.is_empty type_suffix)) then ( let memo = (g', offset) in let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in From e3e322a7ee08a8ab8424329a746355b9d59f46dc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 15 Aug 2023 16:08:41 +0300 Subject: [PATCH 19/28] Clean up and comment lazy outer distribution changes --- src/analyses/raceAnalysis.ml | 27 ++++++++++++++--------- src/domains/access.ml | 42 ++++++++++++++++++++---------------- 2 files changed, 40 insertions(+), 29 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 5f100c869a..3265bc6979 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -12,7 +12,7 @@ struct let name () = "race" (* Two global invariants: - 1. memoroot -> (offset -> accesses) -- used for warnings + 1. memoroot -> (offset --trie--> accesses) -- used for warnings 2. varinfo -> set of memo -- used for IterSysVars Global *) module V = @@ -52,6 +52,9 @@ struct module OffsetTrie = struct + (* LiftBot such that add_distribute_outer can side-effect empty set to indicate + all offsets that exist for prefix-type_suffix race checking. + Otherwise, there are no trie nodes to traverse to where this check must happen. *) include TrieDomain.Make (OneOffset) (Lattice.LiftBot (Access.AS)) let rec find (offset : Offset.Unit.t) ((accs, children) : t) : value = @@ -105,18 +108,19 @@ struct ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.singleton (conf, w, loc, e, a))))); side_vars ctx memo - let side_access0 ctx ((memoroot, offset) as memo) = - (* ignore (Pretty.printf "memo: %a\n" Access.Memo.pretty memo); *) + (** Side-effect empty access set for prefix-type_suffix race checking. *) + let side_access_empty ctx ((memoroot, offset) as memo) = if !AnalysisState.should_warn then ctx.sideg (V.access memoroot) (G.create_access (OffsetTrie.singleton offset (`Lifted (Access.AS.empty ())))); side_vars ctx memo + (** Get immediate type_suffix memo. *) let type_suffix_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option = match root, offset with - | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* TODO: Alloc variables void type *) - | _, `NoOffset -> None - | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') - | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') + | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* global.foo.bar -> (struct S).foo.bar *) (* TODO: Alloc variables void type *) + | _, `NoOffset -> None (* primitive type *) + | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') (* (struct S).foo.bar -> (struct T).bar *) + | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') (* (int[])[*] -> int *) | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *) let rec find_type_suffix' ctx ((root, offset) as memo : Access.Memo.t) : Access.AS.t = @@ -129,6 +133,7 @@ struct let type_suffix = find_type_suffix ctx memo in Access.AS.union accs type_suffix + (** Find accesses from all type_suffixes transitively. *) and find_type_suffix ctx (memo : Access.Memo.t) : Access.AS.t = match type_suffix_memo memo with | Some type_suffix_memo -> find_type_suffix' ctx type_suffix_memo @@ -153,8 +158,10 @@ struct if not (Access.AS.is_empty accs) || (not (Access.AS.is_empty prefix) && not (Access.AS.is_empty type_suffix)) then ( let memo = (g', offset) in let mem_loc_str = GobPretty.sprint Access.Memo.pretty memo in - Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe {prefix; type_suffix_prefix; type_suffix; node=accs}) memo + Timing.wrap ~args:[("memory location", `String mem_loc_str)] "race" (Access.warn_global ~safe ~vulnerable ~unsafe {node=accs; prefix; type_suffix; type_suffix_prefix}) memo ); + + (* Recurse to children. *) let prefix' = Access.AS.union prefix accs in let type_suffix_prefix' = Access.AS.union type_suffix_prefix type_suffix in OffsetTrie.ChildMap.iter (fun child_key child_trie -> @@ -184,11 +191,11 @@ struct let loc = Option.get !Node.current_node in let add_access conf voffs = let a = part_access (Option.map fst voffs) in - Access.add (side_access octx (conf, kind, loc, e, a)) (side_access0 octx) e voffs; + Access.add ~side:(side_access octx (conf, kind, loc, e, a)) ~side_empty:(side_access_empty octx) e voffs; in let add_access_struct conf ci = let a = part_access None in - Access.add_one (side_access octx (conf, kind, loc, e, a)) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset) + Access.add_one ~side:(side_access octx (conf, kind, loc, e, a)) (`Type (TSComp (ci.cstruct, ci.cname, [])), `NoOffset) in let has_escaped g = octx.ask (Queries.MayEscape g) in (* The following function adds accesses to the lval-set ls diff --git a/src/domains/access.ml b/src/domains/access.ml index 457063950d..07d1632529 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -93,7 +93,7 @@ struct match vt with | `Var v -> CilType.Varinfo.pretty () v | `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)" name - | `Type t -> Pretty.dprintf "(%a)" CilType.Typsig.pretty t + | `Type t -> Pretty.dprintf "(%a)" CilType.Typsig.pretty t (* TODO: fix TSBase printing *) include Printable.SimplePretty ( struct @@ -116,7 +116,7 @@ struct match vt with | `Var v -> Pretty.dprintf "%a%a" CilType.Varinfo.pretty v Offset.Unit.pretty o | `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)%a" name Offset.Unit.pretty o - | `Type t -> Pretty.dprintf "(%a)%a" CilType.Typsig.pretty t Offset.Unit.pretty o + | `Type t -> Pretty.dprintf "(%a)%a" CilType.Typsig.pretty t Offset.Unit.pretty o (* TODO: fix TSBase printing *) include Printable.SimplePretty ( struct @@ -194,42 +194,44 @@ let get_val_type e: acc_typ = (** Add access to {!Memo} after distributing. *) -let add_one side memo: unit = +let add_one ~side memo: unit = let mv = Memo.to_mval memo in let ignorable = is_ignorable mv in if M.tracing then M.trace "access" "add_one %a (ignorable = %B)\n" Memo.pretty memo ignorable; if not ignorable then side memo -(** Distribute type-based access to variables and containing fields. *) -let rec add_distribute_outer side side0 (t: typ) (o: Offset.Unit.t) = +(** Distribute empty access set for type-based access to variables and containing fields. + Empty access sets are needed for prefix-type_suffix race checking. *) +let rec add_distribute_outer ~side ~side_empty (t: typ) (o: Offset.Unit.t) = let ts = typeSig t in let memo = (`Type ts, o) in if M.tracing then M.tracei "access" "add_distribute_outer %a\n" Memo.pretty memo; - add_one side memo; + add_one ~side memo; (* Add actual access for non-recursive call, or empty access for recursive call when side is side_empty. *) (* distribute to variables of the type *) let vars = TSH.find_all typeVar ts in List.iter (fun v -> - add_one side0 (`Var v, o) (* same offset, but on variable *) + (* same offset, but on variable *) + add_one ~side:side_empty (`Var v, o) (* Switch to side_empty. *) ) vars; (* recursively distribute to fields containing the type *) let fields = TSH.find_all typeIncl ts in List.iter (fun f -> (* prepend field and distribute to outer struct *) - add_distribute_outer side0 side0 (TComp (f.fcomp, [])) (`Field (f, o)) + add_distribute_outer ~side:side_empty ~side_empty (TComp (f.fcomp, [])) (`Field (f, o)) (* Switch to side_empty. *) ) fields; if M.tracing then M.traceu "access" "add_distribute_outer\n" (** Add access to known variable with offsets or unknown variable from expression. *) -let add side side0 e voffs = +let add ~side ~side_empty e voffs = begin match voffs with | Some (v, o) -> (* known variable *) if M.tracing then M.traceli "access" "add var %a%a\n" CilType.Varinfo.pretty v CilType.Offset.pretty o; let memo = (`Var v, Offset.Unit.of_cil o) in - add_one side memo + add_one ~side memo | None -> (* unknown variable *) if M.tracing then M.traceli "access" "add type %a\n" CilType.Exp.pretty e; let ty = get_val_type e in (* extract old acc_typ from expression *) @@ -239,7 +241,7 @@ let add side side0 e voffs = in match o with | `NoOffset when not !collect_direct_arithmetic && isArithmeticType t -> () - | _ -> add_distribute_outer side side0 t o (* distribute to variables and outer offsets *) + | _ -> add_distribute_outer ~side ~side_empty t o (* distribute to variables and outer offsets *) end; if M.tracing then M.traceu "access" "add\n" @@ -368,13 +370,14 @@ let may_race (conf,(kind: AccessKind.t),loc,e,a) (conf2,(kind2: AccessKind.t),lo else true +(** Access sets for race detection and warnings. *) module WarnAccs = struct type t = { - node: AS.t; - prefix: AS.t; - type_suffix: AS.t; - type_suffix_prefix: AS.t; + node: AS.t; (** Accesses for current memo. From accesses at trie node corresponding to memo offset. *) + prefix: AS.t; (** Accesses for all prefixes. From accesses to trie node ancestors. *) + type_suffix: AS.t; (** Accesses for all type suffixes. From offset suffixes in other tries. *) + type_suffix_prefix: AS.t; (** Accesses to all prefixes of all type suffixes. *) } let diff w1 w2 = { @@ -404,9 +407,9 @@ let group_may_race (warn_accs:WarnAccs.t) = if M.tracing then M.tracei "access" "group_may_race %a\n" WarnAccs.pretty warn_accs; (* BFS to traverse one component with may_race edges *) let rec bfs' warn_accs ~todo ~visited = - let warn_accs' = WarnAccs.diff warn_accs todo in let todo_all = WarnAccs.union_all todo in - let visited' = AS.union visited todo_all in + let visited' = AS.union visited todo_all in (* Add all todo accesses to component. *) + let warn_accs' = WarnAccs.diff warn_accs todo in (* Todo accesses don't need to be considered as step targets, because they're already in the component. *) let step_may_race ~todo ~accs = (* step from todo to accs if may_race *) AS.fold (fun acc todo' -> @@ -437,7 +440,7 @@ let group_may_race (warn_accs:WarnAccs.t) = prefix = step_may_race ~todo:(AS.union todo.node todo.type_suffix) ~accs:warn_accs'.prefix; type_suffix = step_may_race ~todo:(AS.union todo.node todo.prefix) ~accs:warn_accs'.type_suffix; type_suffix_prefix = step_may_race ~todo:todo.node ~accs:warn_accs'.type_suffix_prefix - } + } in if WarnAccs.is_empty todo' then @@ -446,7 +449,7 @@ let group_may_race (warn_accs:WarnAccs.t) = (bfs' [@tailcall]) warn_accs' ~todo:todo' ~visited:visited' in let bfs warn_accs todo = bfs' warn_accs ~todo ~visited:(AS.empty ()) in - (* repeat BFS to find all components *) + (* repeat BFS to find all components starting from node accesses *) let rec components comps (warn_accs:WarnAccs.t) = if AS.is_empty warn_accs.node then (comps, warn_accs) @@ -459,6 +462,7 @@ let group_may_race (warn_accs:WarnAccs.t) = in let (comps, warn_accs) = components [] warn_accs in if M.tracing then M.trace "access" "components %a\n" WarnAccs.pretty warn_accs; + (* repeat BFS to find all prefix-type_suffix-only components starting from prefix accesses (symmetric) *) let rec components_cross comps ~prefix ~type_suffix = if AS.is_empty prefix then comps From 81dac32fd56807e6695197c36e4c375eb073962a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 15 Aug 2023 16:58:39 +0300 Subject: [PATCH 20/28] Document new race analysis --- src/analyses/raceAnalysis.ml | 79 ++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 3265bc6979..f617df2048 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -3,6 +3,85 @@ open GoblintCil open Analyses +(** Data race analysis with tries and hookers. + + Accesses are to memory locations ({{!Access.Memo} memos}) which consist of a root and offset. + {{!Access.MemoRoot} Root} can be: + + variable, if access is to known global variable or alloc-variable; + + type, if access is to unknown pointer. + + Accesses are (now) collected to sets for each corresponding memo, + after points-to sets are resolved, during postsolving. + + Race checking is performed per-memo, + except must additionally account for accesses to other memos (see diagram below): + + access to [s.f] can race with access to a prefix like [s], which writes an entire struct at once; + + access to [s.f] can race with type-based access like [(struct S).f]; + + access to [(struct S).f] can race with type-based access to a suffix like [(int)]. + + access to [(struct T).s.f] can race with type-based access like [(struct S)], which is a combination of the above. + + These are accounted for lazily (unlike in the past). + + Prefixes (a.k.a. inner distribution) are handled using a trie data structure enriched with lattice properties. + Race checking starts at the root and passes accesses to ancestor nodes down to children. + + Type suffixes (a.k.a. outer distribution) are handled by computing successive immediate type suffixes transitively + and accessing corresponding offsets from corresponding root tries in the global invariant. + + Type suffix prefixes (for the combination of the two) are handled by passing type suffix accesses down when traversing the prefix trie. + + Race checking happens at each trie node with the above three access sets at hand using {!Access.group_may_race}. + All necessary combinations between the four classes are handled, but unnecessary repeated work is carefully avoided. + E.g. accesses which are pairwise checked at some prefix are not re-checked pairwise at a node. + Thus, races (with prefixes or type suffixes) are reported for most precise memos with actual accesses: + at the longest prefix and longest type suffix. + + Additionally, accesses between prefix and type suffix intersecting at a node are checked. + These races are reported at the unique memo at the intersection of the prefix and the type suffix. + This requires an implementation hack to still eagerly do outer distribution, but only of empty access sets. + It ensures that corresponding trie nodes exist for traversal later. *) + +(** Example structure of related memos for race checking: + {v + (int) (S) (T) + \ / \ / \ + f s t + \ / \ / + f s + \ / + f + v} + where: + - [(int)] is a type-based memo root for the primitive [int] type; + - [(S)] and [(T)] are short for [(struct S)] and [(struct T)], which are type-based memo roots; + - [f] is a field of [S] and [s] is a field of [T]; + - [t] is a global variable of type [T]. + - prefix relations are indicated by [/]; + - type suffix relations are indicated by [\ ]. + + Prefix races: + - Race between [t.s.f] and [t.s] is checked/reported at [t.s.f]. + - Race between [t.s.f] and [t] is checked/reported at [t.s.f]. + - Race between [t.s] and [t] is checked/reported at [t.s]. + - Race between [t] and [t] is checked/reported at [t]. + - Race between [(S).f] and [(S)] is checked/reported at [(S).f]. + + Type suffix races: + - Race between [t.s.f] and [(T).s.f] is checked/reported at [t.s.f]. + - Race between [t.s.f] and [(S).f] is checked/reported at [t.s.f]. + - Race between [t.s.f] and [(int)] is checked/reported at [t.s.f]. + - Race between [(S).f] and [(int)] is checked/reported at [(S).f]. + + Type suffix prefix races: + - Race between [t.s.f] and [(T).s] is checked/reported at [t.s.f]. + - Race between [t.s.f] and [(T)] is checked/reported at [t.s.f]. + - Race between [t.s.f] and [(S)] is checked/reported at [t.s.f]. + - Race between [(T).s.f] and [(S)] is checked/reported at [(T).s.f]. + + Prefix-type suffix races: + - Race between [(T).s] and [(S).f] is checked/reported at [(T).s.f]. + - Race between [t] and [(S).f] is checked/reported at [t.s.f]. *) + (** Data race analyzer without base --- this is the new standard *) module Spec = From 7297241f591bc1719011dda4fe0ef0906ec2cddd Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 15 Aug 2023 17:15:48 +0300 Subject: [PATCH 21/28] Remove --enable ana.race.direct-arithmetic from some tests Irrelevant because no (int) accesses. --- .../regression/04-mutex/49-type-invariants.c | 1 - .../regression/04-mutex/49-type-invariants.t | 48 +++++++++---------- .../04-mutex/77-type-nested-fields.c | 5 +- .../04-mutex/77-type-nested-fields.t | 34 ++++++------- tests/regression/04-mutex/78-type-array.c | 1 - .../04-mutex/79-type-nested-fields-deep1.c | 5 +- .../04-mutex/79-type-nested-fields-deep1.t | 34 ++++++------- .../04-mutex/80-type-nested-fields-deep2.c | 5 +- .../04-mutex/80-type-nested-fields-deep2.t | 34 ++++++------- .../04-mutex/90-distribute-fields-type-1.c | 5 +- .../04-mutex/90-distribute-fields-type-1.t | 36 +++++++------- .../04-mutex/91-distribute-fields-type-2.c | 5 +- .../04-mutex/91-distribute-fields-type-2.t | 36 +++++++------- .../04-mutex/92-distribute-fields-type-deep.c | 5 +- .../04-mutex/92-distribute-fields-type-deep.t | 36 +++++++------- .../93-distribute-fields-type-global.c | 1 - .../93-distribute-fields-type-global.t | 28 +++++------ 17 files changed, 155 insertions(+), 164 deletions(-) diff --git a/tests/regression/04-mutex/49-type-invariants.c b/tests/regression/04-mutex/49-type-invariants.c index 4f69986478..e6ac17dcd9 100644 --- a/tests/regression/04-mutex/49-type-invariants.c +++ b/tests/regression/04-mutex/49-type-invariants.c @@ -1,4 +1,3 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include diff --git a/tests/regression/04-mutex/49-type-invariants.t b/tests/regression/04-mutex/49-type-invariants.t index 3d3f7442ef..3ddd8f237d 100644 --- a/tests/regression/04-mutex/49-type-invariants.t +++ b/tests/regression/04-mutex/49-type-invariants.t @@ -1,47 +1,47 @@ $ goblint --enable warn.deterministic --enable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:22:3-22:21) - [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:9:10-9:11) - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:22:3-22:21) - read with [mhp:{tid=[main, t_fun@49-type-invariants.c:21:3-21:40#top]}, thread:[main, t_fun@49-type-invariants.c:21:3-21:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:12:3-12:23) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21) + [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11) + write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#top]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:22:3-22:21) + write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:22:3-22:21) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:22:3-22:21) - [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:22:3-22:21) - [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:22:3-22:21) + [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:21:3-21:21) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:21:3-21:21) + [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21) + [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21) $ goblint --enable warn.deterministic --disable ana.race.direct-arithmetic --enable allglobs 49-type-invariants.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:22:3-22:21) - [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:9:10-9:11) - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:22:3-22:21) - read with [mhp:{tid=[main, t_fun@49-type-invariants.c:21:3-21:40#top]}, thread:[main, t_fun@49-type-invariants.c:21:3-21:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:12:3-12:23) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (49-type-invariants.c:21:3-21:21) + [Warning][Race] Memory location s.field (race with conf. 110): (49-type-invariants.c:8:10-8:11) + write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) + read with [mhp:{tid=[main, t_fun@49-type-invariants.c:20:3-20:40#top]}, thread:[main, t_fun@49-type-invariants.c:20:3-20:40#top]] (conf. 110) (exp: & s.field) (49-type-invariants.c:11:3-11:23) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:21:3-21:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:22:3-22:21) + write with [mhp:{tid=[main]; created={[main, t_fun@49-type-invariants.c:20:3-20:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->field) (49-type-invariants.c:21:3-21:21) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:22:3-22:21) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:22:3-22:21) - [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:22:3-22:21) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:22:3-22:21) - [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:22:3-22:21) + [Info][Unsound] Unknown address in {&tmp} has escaped. (49-type-invariants.c:21:3-21:21) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (49-type-invariants.c:21:3-21:21) + [Info][Unsound] Write to unknown address: privatization is unsound. (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (49-type-invariants.c:21:3-21:21) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (49-type-invariants.c:21:3-21:21) + [Error][Imprecise][Unsound] Function definition missing for getS (49-type-invariants.c:21:3-21:21) diff --git a/tests/regression/04-mutex/77-type-nested-fields.c b/tests/regression/04-mutex/77-type-nested-fields.c index a526defb06..00b21e3fcf 100644 --- a/tests/regression/04-mutex/77-type-nested-fields.c +++ b/tests/regression/04-mutex/77-type-nested-fields.c @@ -1,11 +1,10 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include // (int) (S) (T) (U) -// \ / \ / \ / +// \ / \ / \ / // >f< s t -// \ / \ / +// \ / \ / // >f< s // \ / // f diff --git a/tests/regression/04-mutex/77-type-nested-fields.t b/tests/regression/04-mutex/77-type-nested-fields.t index dc87d0a85e..738784f5d5 100644 --- a/tests/regression/04-mutex/77-type-nested-fields.t +++ b/tests/regression/04-mutex/77-type-nested-fields.t @@ -1,29 +1,29 @@ $ goblint --enable warn.deterministic --enable allglobs 77-type-nested-fields.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:32:3-32:20) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:39:3-39:22) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:31:3-31:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (77-type-nested-fields.c:38:3-38:22) [Warning][Race] Memory location (struct T).s.field (race with conf. 100): - write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:32:3-32:20) - write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:39:3-39:22) + write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) + write with [mhp:{tid=[main]; created={[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s.field) (77-type-nested-fields.c:38:3-38:22) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:32:3-32:20) + write with [mhp:{tid=[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]}, thread:[main, t_fun@77-type-nested-fields.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (77-type-nested-fields.c:31:3-31:20) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:32:3-32:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:32:3-32:20) - [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:32:3-32:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:39:3-39:22) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:39:3-39:22) - [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:39:3-39:22) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:32:3-32:20) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:32:3-32:20) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:39:3-39:22) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:39:3-39:22) - [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:32:3-32:20) - [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:39:3-39:22) + [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:31:3-31:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:31:3-31:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:31:3-31:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (77-type-nested-fields.c:38:3-38:22) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (77-type-nested-fields.c:38:3-38:22) + [Info][Unsound] Write to unknown address: privatization is unsound. (77-type-nested-fields.c:38:3-38:22) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:31:3-31:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:31:3-31:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (77-type-nested-fields.c:38:3-38:22) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (77-type-nested-fields.c:38:3-38:22) + [Error][Imprecise][Unsound] Function definition missing for getS (77-type-nested-fields.c:31:3-31:20) + [Error][Imprecise][Unsound] Function definition missing for getT (77-type-nested-fields.c:38:3-38:22) diff --git a/tests/regression/04-mutex/78-type-array.c b/tests/regression/04-mutex/78-type-array.c index cdffe244b9..835f6163a3 100644 --- a/tests/regression/04-mutex/78-type-array.c +++ b/tests/regression/04-mutex/78-type-array.c @@ -1,4 +1,3 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.c b/tests/regression/04-mutex/79-type-nested-fields-deep1.c index c38e700829..e100404960 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.c +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.c @@ -1,11 +1,10 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include // (int) (S) (T) (U) -// \ / \ / \ / +// \ / \ / \ / // >f< s t -// \ / \ / +// \ / \ / // f s // \ / // >f< diff --git a/tests/regression/04-mutex/79-type-nested-fields-deep1.t b/tests/regression/04-mutex/79-type-nested-fields-deep1.t index 5fc60223b9..2e15f83c39 100644 --- a/tests/regression/04-mutex/79-type-nested-fields-deep1.t +++ b/tests/regression/04-mutex/79-type-nested-fields-deep1.t @@ -1,29 +1,29 @@ $ goblint --enable warn.deterministic --enable allglobs 79-type-nested-fields-deep1.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:37:3-37:20) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:44:3-44:24) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:36:3-36:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (79-type-nested-fields-deep1.c:43:3-43:24) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): - write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) - write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:44:3-44:24) + write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) + write with [mhp:{tid=[main]; created={[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (79-type-nested-fields-deep1.c:43:3-43:24) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:37:3-37:20) + write with [mhp:{tid=[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]}, thread:[main, t_fun@79-type-nested-fields-deep1.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (79-type-nested-fields-deep1.c:36:3-36:20) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:37:3-37:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:37:3-37:20) - [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:37:3-37:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:44:3-44:24) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:44:3-44:24) - [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:44:3-44:24) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:37:3-37:20) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:37:3-37:20) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:44:3-44:24) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:44:3-44:24) - [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:37:3-37:20) - [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:44:3-44:24) + [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (79-type-nested-fields-deep1.c:43:3-43:24) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (79-type-nested-fields-deep1.c:43:3-43:24) + [Info][Unsound] Write to unknown address: privatization is unsound. (79-type-nested-fields-deep1.c:43:3-43:24) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:36:3-36:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (79-type-nested-fields-deep1.c:43:3-43:24) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (79-type-nested-fields-deep1.c:43:3-43:24) + [Error][Imprecise][Unsound] Function definition missing for getS (79-type-nested-fields-deep1.c:36:3-36:20) + [Error][Imprecise][Unsound] Function definition missing for getU (79-type-nested-fields-deep1.c:43:3-43:24) diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.c b/tests/regression/04-mutex/80-type-nested-fields-deep2.c index 9a1e3028a3..4ddd4684f7 100644 --- a/tests/regression/04-mutex/80-type-nested-fields-deep2.c +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.c @@ -1,11 +1,10 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include // (int) (S) (T) (U) -// \ / \ / \ / +// \ / \ / \ / // f s t -// \ / \ / +// \ / \ / // >f< s // \ / // >f< diff --git a/tests/regression/04-mutex/80-type-nested-fields-deep2.t b/tests/regression/04-mutex/80-type-nested-fields-deep2.t index a0541235ee..48e726f623 100644 --- a/tests/regression/04-mutex/80-type-nested-fields-deep2.t +++ b/tests/regression/04-mutex/80-type-nested-fields-deep2.t @@ -1,29 +1,29 @@ $ goblint --enable warn.deterministic --enable allglobs 80-type-nested-fields-deep2.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:37:3-37:22) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:44:3-44:24) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:36:3-36:22) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (80-type-nested-fields-deep2.c:43:3-43:24) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): - write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:37:3-37:22) - write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:44:3-44:24) + write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) + write with [mhp:{tid=[main]; created={[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t.s.field) (80-type-nested-fields-deep2.c:43:3-43:24) [Info][Race] Memory locations race summary: safe: 1 vulnerable: 0 unsafe: 1 total memory locations: 2 [Success][Race] Memory location (struct T).s.field (safe): - write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:37:3-37:22) + write with [mhp:{tid=[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]}, thread:[main, t_fun@80-type-nested-fields-deep2.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->s.field) (80-type-nested-fields-deep2.c:36:3-36:22) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:37:3-37:22) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:37:3-37:22) - [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:37:3-37:22) - [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:44:3-44:24) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:44:3-44:24) - [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:44:3-44:24) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:37:3-37:22) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:37:3-37:22) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:44:3-44:24) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:44:3-44:24) - [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:37:3-37:22) - [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:44:3-44:24) + [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Unsound] Unknown address in {&tmp} has escaped. (80-type-nested-fields-deep2.c:43:3-43:24) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (80-type-nested-fields-deep2.c:43:3-43:24) + [Info][Unsound] Write to unknown address: privatization is unsound. (80-type-nested-fields-deep2.c:43:3-43:24) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:36:3-36:22) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (80-type-nested-fields-deep2.c:43:3-43:24) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (80-type-nested-fields-deep2.c:43:3-43:24) + [Error][Imprecise][Unsound] Function definition missing for getT (80-type-nested-fields-deep2.c:36:3-36:22) + [Error][Imprecise][Unsound] Function definition missing for getU (80-type-nested-fields-deep2.c:43:3-43:24) diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.c b/tests/regression/04-mutex/90-distribute-fields-type-1.c index 51f0e52426..062b7421e6 100644 --- a/tests/regression/04-mutex/90-distribute-fields-type-1.c +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.c @@ -1,11 +1,10 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include // (int) (S) (T) (U) -// \ / \ / \ / +// \ / \ / \ / // >f< >s< t -// \ / \ / +// \ / \ / // f s // \ / // f diff --git a/tests/regression/04-mutex/90-distribute-fields-type-1.t b/tests/regression/04-mutex/90-distribute-fields-type-1.t index fb6af7ceca..ba3e3da0ed 100644 --- a/tests/regression/04-mutex/90-distribute-fields-type-1.t +++ b/tests/regression/04-mutex/90-distribute-fields-type-1.t @@ -1,31 +1,31 @@ $ goblint --enable warn.deterministic --enable allglobs 90-distribute-fields-type-1.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:32:3-32:20) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:40:3-40:17) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:31:3-31:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (90-distribute-fields-type-1.c:39:3-39:17) [Warning][Race] Memory location (struct T).s.field (race with conf. 100): - write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) - write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) + write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) + write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:32:3-32:20) + write with [mhp:{tid=[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}, thread:[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]] (conf. 100) (exp: & tmp->field) (90-distribute-fields-type-1.c:31:3-31:20) [Success][Race] Memory location (struct T).s (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:40:3-40:17) + write with [mhp:{tid=[main]; created={[main, t_fun@90-distribute-fields-type-1.c:37:3-37:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->s) (90-distribute-fields-type-1.c:39:3-39:17) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:32:3-32:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:32:3-32:20) - [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:32:3-32:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:40:3-40:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:40:3-40:17) - [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:40:3-40:17) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:32:3-32:20) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:32:3-32:20) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:40:3-40:17) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:40:3-40:17) - [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:32:3-32:20) - [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:40:3-40:17) + [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:31:3-31:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:31:3-31:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:31:3-31:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (90-distribute-fields-type-1.c:39:3-39:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (90-distribute-fields-type-1.c:39:3-39:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (90-distribute-fields-type-1.c:39:3-39:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:31:3-31:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:31:3-31:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (90-distribute-fields-type-1.c:39:3-39:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (90-distribute-fields-type-1.c:39:3-39:17) + [Error][Imprecise][Unsound] Function definition missing for getS (90-distribute-fields-type-1.c:31:3-31:20) + [Error][Imprecise][Unsound] Function definition missing for getT (90-distribute-fields-type-1.c:39:3-39:17) diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.c b/tests/regression/04-mutex/91-distribute-fields-type-2.c index 12866105f6..01c945f730 100644 --- a/tests/regression/04-mutex/91-distribute-fields-type-2.c +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.c @@ -1,11 +1,10 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include // (int) >(S)< >(T)< (U) -// \ / \ / \ / +// \ / \ / \ / // f s t -// \ / \ / +// \ / \ / // f s // \ / // f diff --git a/tests/regression/04-mutex/91-distribute-fields-type-2.t b/tests/regression/04-mutex/91-distribute-fields-type-2.t index 0b4ec982e8..fd544b0b0b 100644 --- a/tests/regression/04-mutex/91-distribute-fields-type-2.t +++ b/tests/regression/04-mutex/91-distribute-fields-type-2.t @@ -1,31 +1,31 @@ $ goblint --enable warn.deterministic --enable allglobs 91-distribute-fields-type-2.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:33:3-33:17) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:41:3-41:17) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:32:3-32:17) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (91-distribute-fields-type-2.c:40:3-40:17) [Warning][Race] Memory location (struct T).s (race with conf. 100): - write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:33:3-33:17) - write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:41:3-41:17) + write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) + write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S) (safe): - write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:33:3-33:17) + write with [mhp:{tid=[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}, thread:[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:32:3-32:17) [Success][Race] Memory location (struct T) (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:39:3-39:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:41:3-41:17) + write with [mhp:{tid=[main]; created={[main, t_fun@91-distribute-fields-type-2.c:38:3-38:40#top]}}, thread:[main]] (conf. 100) (exp: & *tmp) (91-distribute-fields-type-2.c:40:3-40:17) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:33:3-33:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:33:3-33:17) - [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:33:3-33:17) - [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:41:3-41:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:41:3-41:17) - [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:41:3-41:17) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:33:3-33:17) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:33:3-33:17) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:41:3-41:17) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:41:3-41:17) - [Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:33:3-33:17) - [Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:41:3-41:17) + [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:32:3-32:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:32:3-32:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:32:3-32:17) + [Info][Unsound] Unknown address in {&tmp} has escaped. (91-distribute-fields-type-2.c:40:3-40:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (91-distribute-fields-type-2.c:40:3-40:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (91-distribute-fields-type-2.c:40:3-40:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:32:3-32:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:32:3-32:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (91-distribute-fields-type-2.c:40:3-40:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (91-distribute-fields-type-2.c:40:3-40:17) + [Error][Imprecise][Unsound] Function definition missing for getS (91-distribute-fields-type-2.c:32:3-32:17) + [Error][Imprecise][Unsound] Function definition missing for getT (91-distribute-fields-type-2.c:40:3-40:17) diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.c b/tests/regression/04-mutex/92-distribute-fields-type-deep.c index 891f5fb51f..59fb09a605 100644 --- a/tests/regression/04-mutex/92-distribute-fields-type-deep.c +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.c @@ -1,11 +1,10 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include // (int) (S) (T) (U) -// \ / \ / \ / +// \ / \ / \ / // >f< s >t< -// \ / \ / +// \ / \ / // f s // \ / // f diff --git a/tests/regression/04-mutex/92-distribute-fields-type-deep.t b/tests/regression/04-mutex/92-distribute-fields-type-deep.t index aedc66f101..aefc1520d1 100644 --- a/tests/regression/04-mutex/92-distribute-fields-type-deep.t +++ b/tests/regression/04-mutex/92-distribute-fields-type-deep.t @@ -1,31 +1,31 @@ $ goblint --enable warn.deterministic --enable allglobs 92-distribute-fields-type-deep.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:37:3-37:20) - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:45:3-45:17) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:36:3-36:20) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (92-distribute-fields-type-deep.c:44:3-44:17) [Warning][Race] Memory location (struct U).t.s.field (race with conf. 100): - write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) - write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) + write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) + write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S).field (safe): - write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:37:3-37:20) + write with [mhp:{tid=[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}, thread:[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]] (conf. 100) (exp: & tmp->field) (92-distribute-fields-type-deep.c:36:3-36:20) [Success][Race] Memory location (struct U).t (safe): - write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:43:3-43:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:45:3-45:17) + write with [mhp:{tid=[main]; created={[main, t_fun@92-distribute-fields-type-deep.c:42:3-42:40#top]}}, thread:[main]] (conf. 100) (exp: & tmp->t) (92-distribute-fields-type-deep.c:44:3-44:17) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:37:3-37:20) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:37:3-37:20) - [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:37:3-37:20) - [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:45:3-45:17) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:45:3-45:17) - [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:45:3-45:17) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:37:3-37:20) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:37:3-37:20) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:45:3-45:17) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:45:3-45:17) - [Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:37:3-37:20) - [Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:45:3-45:17) + [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:36:3-36:20) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:36:3-36:20) + [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:36:3-36:20) + [Info][Unsound] Unknown address in {&tmp} has escaped. (92-distribute-fields-type-deep.c:44:3-44:17) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (92-distribute-fields-type-deep.c:44:3-44:17) + [Info][Unsound] Write to unknown address: privatization is unsound. (92-distribute-fields-type-deep.c:44:3-44:17) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:36:3-36:20) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:36:3-36:20) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (92-distribute-fields-type-deep.c:44:3-44:17) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (92-distribute-fields-type-deep.c:44:3-44:17) + [Error][Imprecise][Unsound] Function definition missing for getS (92-distribute-fields-type-deep.c:36:3-36:20) + [Error][Imprecise][Unsound] Function definition missing for getU (92-distribute-fields-type-deep.c:44:3-44:17) diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.c b/tests/regression/04-mutex/93-distribute-fields-type-global.c index ad7839d95f..466d47e7fc 100644 --- a/tests/regression/04-mutex/93-distribute-fields-type-global.c +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.c @@ -1,4 +1,3 @@ -//PARAM: --enable ana.race.direct-arithmetic #include #include diff --git a/tests/regression/04-mutex/93-distribute-fields-type-global.t b/tests/regression/04-mutex/93-distribute-fields-type-global.t index fcc3e804c7..2199c689b1 100644 --- a/tests/regression/04-mutex/93-distribute-fields-type-global.t +++ b/tests/regression/04-mutex/93-distribute-fields-type-global.t @@ -1,25 +1,25 @@ $ goblint --enable warn.deterministic --enable allglobs 93-distribute-fields-type-global.c - [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (93-distribute-fields-type-global.c:14:3-14:29) - [Warning][Race] Memory location s.field (race with conf. 110): (93-distribute-fields-type-global.c:9:10-9:11) - read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:14:3-14:29) - write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:23:3-23:9) + [Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (93-distribute-fields-type-global.c:13:3-13:29) + [Warning][Race] Memory location s.field (race with conf. 110): (93-distribute-fields-type-global.c:8:10-8:11) + read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) [Info][Race] Memory locations race summary: safe: 2 vulnerable: 0 unsafe: 1 total memory locations: 3 [Success][Race] Memory location (struct S).field (safe): - read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:14:3-14:29) - [Success][Race] Memory location s (safe): (93-distribute-fields-type-global.c:9:10-9:11) - write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:21:3-21:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:23:3-23:9) + read with [mhp:{tid=[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}, thread:[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]] (conf. 100) (exp: & tmp->field) (93-distribute-fields-type-global.c:13:3-13:29) + [Success][Race] Memory location s (safe): (93-distribute-fields-type-global.c:8:10-8:11) + write with [mhp:{tid=[main]; created={[main, t_fun@93-distribute-fields-type-global.c:20:3-20:40#top]}}, thread:[main]] (conf. 110) (exp: & s) (93-distribute-fields-type-global.c:22:3-22:9) [Info][Deadcode] Logical lines of code (LLoC) summary: live: 7 dead: 0 total lines: 7 - [Info][Unsound] Unknown address in {&tmp} has escaped. (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Unsound] Write to unknown address: privatization is unsound. (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Imprecise] INVALIDATING ALL GLOBALS! (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:14:3-14:29) - [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (93-distribute-fields-type-global.c:14:3-14:29) - [Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:14:3-14:29) + [Info][Unsound] Unknown address in {&tmp} has escaped. (93-distribute-fields-type-global.c:13:3-13:29) + [Info][Unsound] Unknown value in {?} could be an escaped pointer address! (93-distribute-fields-type-global.c:13:3-13:29) + [Info][Unsound] Write to unknown address: privatization is unsound. (93-distribute-fields-type-global.c:13:3-13:29) + [Info][Imprecise] INVALIDATING ALL GLOBALS! (93-distribute-fields-type-global.c:13:3-13:29) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(s, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29) + [Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (93-distribute-fields-type-global.c:13:3-13:29) + [Error][Imprecise][Unsound] Function definition missing for getS (93-distribute-fields-type-global.c:13:3-13:29) From 48884b3a2a17474092fff20f5298e410ff7be239 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 15 Aug 2023 17:40:46 +0300 Subject: [PATCH 22/28] Fix non-struct typsig pretty in MemoRoot --- src/domains/access.ml | 4 +- src/util/cilfacade.ml | 95 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 97 insertions(+), 2 deletions(-) diff --git a/src/domains/access.ml b/src/domains/access.ml index 07d1632529..4069763b99 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -93,7 +93,7 @@ struct match vt with | `Var v -> CilType.Varinfo.pretty () v | `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)" name - | `Type t -> Pretty.dprintf "(%a)" CilType.Typsig.pretty t (* TODO: fix TSBase printing *) + | `Type t -> Pretty.dprintf "(%a)" Cilfacade.pretty_typsig_like_typ t include Printable.SimplePretty ( struct @@ -116,7 +116,7 @@ struct match vt with | `Var v -> Pretty.dprintf "%a%a" CilType.Varinfo.pretty v Offset.Unit.pretty o | `Type (TSComp (_, name, _)) -> Pretty.dprintf "(struct %s)%a" name Offset.Unit.pretty o - | `Type t -> Pretty.dprintf "(%a)%a" CilType.Typsig.pretty t Offset.Unit.pretty o (* TODO: fix TSBase printing *) + | `Type t -> Pretty.dprintf "(%a)%a" Cilfacade.pretty_typsig_like_typ t Offset.Unit.pretty o include Printable.SimplePretty ( struct diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml index d0dcc428ad..c77d2cd738 100644 --- a/src/util/cilfacade.ml +++ b/src/util/cilfacade.ml @@ -359,6 +359,101 @@ let split_anoncomp_name name = else invalid_arg "Cilfacade.split_anoncomp_name" +(** Pretty-print typsig like typ, because + {!d_typsig} prints with CIL constructors. *) +let rec pretty_typsig_like_typ (nameOpt: Pretty.doc option) () ts = + (* Copied & modified from Cil.defaultCilPrinterClass#pType. *) + let open Pretty in + let name = match nameOpt with None -> nil | Some d -> d in + let printAttributes (a: attributes) = + let pa = d_attrlist () a in + match nameOpt with + | None when not !print_CIL_Input -> + (* Cannot print the attributes in this case because gcc does not + like them here, except if we are printing for CIL. *) + if pa = nil then nil else + text "/*" ++ pa ++ text "*/" + | _ -> pa + in + match ts with + | TSBase t -> dn_type () t + | TSComp (cstruct, cname, a) -> + let su = if cstruct then "struct" else "union" in + text (su ^ " " ^ cname ^ " ") + ++ d_attrlist () a + ++ name + | TSEnum (ename, a) -> + text ("enum " ^ ename ^ " ") + ++ d_attrlist () a + ++ name + | TSPtr (bt, a) -> + (* Parenthesize the ( * attr name) if a pointer to a function or an + array. *) + let (paren: doc option), (bt': typsig) = + match bt with + | TSFun _ | TSArray _ -> Some (text "("), bt + | _ -> None, bt + in + let name' = text "*" ++ printAttributes a ++ name in + let name'' = (* Put the parenthesis *) + match paren with + Some p -> p ++ name' ++ text ")" + | _ -> name' + in + pretty_typsig_like_typ + (Some name'') + () + bt' + + | TSArray (elemt, lo, a) -> + (* ignore the const attribute for arrays *) + let a' = dropAttributes [ "pconst" ] a in + let name' = + if a' == [] then name else + if nameOpt == None then printAttributes a' else + text "(" ++ printAttributes a' ++ name ++ text ")" + in + pretty_typsig_like_typ + (Some (name' + ++ text "[" + ++ (match lo with None -> nil | Some e -> text (Z.to_string e)) + ++ text "]")) + () + elemt + + | TSFun (restyp, args, isvararg, a) -> + let name' = + if a == [] then name else + if nameOpt == None then printAttributes a else + text "(" ++ printAttributes a ++ name ++ text ")" + in + pretty_typsig_like_typ + (Some + (name' + ++ text "(" + ++ (align + ++ + (if args = Some [] && isvararg then + text "..." + else + (if args = None then nil + else if args = Some [] then text "void" + else + let pArg atype = + (pretty_typsig_like_typ None () atype) + in + (docList ~sep:(chr ',' ++ break) pArg) () + (match args with None -> [] | Some args -> args)) + ++ (if isvararg then break ++ text ", ..." else nil)) + ++ unalign) + ++ text ")")) + () + restyp + +(** Pretty-print typsig like typ, because + {!d_typsig} prints with CIL constructors. *) +let pretty_typsig_like_typ = pretty_typsig_like_typ None + (** HashSet of line numbers *) let locs = Hashtbl.create 200 From 789dd00022dfe69776c4e589b1d799c9120d433b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 15 Aug 2023 17:51:56 +0300 Subject: [PATCH 23/28] Use fewer Cil.typeSig calls for Access.add_distribute_outer --- src/domains/access.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/domains/access.ml b/src/domains/access.ml index 4069763b99..675d1c2e72 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -203,8 +203,7 @@ let add_one ~side memo: unit = (** Distribute empty access set for type-based access to variables and containing fields. Empty access sets are needed for prefix-type_suffix race checking. *) -let rec add_distribute_outer ~side ~side_empty (t: typ) (o: Offset.Unit.t) = - let ts = typeSig t in +let rec add_distribute_outer ~side ~side_empty (ts: typsig) (o: Offset.Unit.t) = let memo = (`Type ts, o) in if M.tracing then M.tracei "access" "add_distribute_outer %a\n" Memo.pretty memo; add_one ~side memo; (* Add actual access for non-recursive call, or empty access for recursive call when side is side_empty. *) @@ -220,7 +219,7 @@ let rec add_distribute_outer ~side ~side_empty (t: typ) (o: Offset.Unit.t) = let fields = TSH.find_all typeIncl ts in List.iter (fun f -> (* prepend field and distribute to outer struct *) - add_distribute_outer ~side:side_empty ~side_empty (TComp (f.fcomp, [])) (`Field (f, o)) (* Switch to side_empty. *) + add_distribute_outer ~side:side_empty ~side_empty (TSComp (f.fcomp.cstruct, f.fcomp.cname, [])) (`Field (f, o)) (* Switch to side_empty. *) ) fields; if M.tracing then M.traceu "access" "add_distribute_outer\n" @@ -241,7 +240,7 @@ let add ~side ~side_empty e voffs = in match o with | `NoOffset when not !collect_direct_arithmetic && isArithmeticType t -> () - | _ -> add_distribute_outer ~side ~side_empty t o (* distribute to variables and outer offsets *) + | _ -> add_distribute_outer ~side ~side_empty (Cil.typeSig t) o (* distribute to variables and outer offsets *) end; if M.tracing then M.traceu "access" "add\n" From fe1660e0e74d6934aec68d590ade46d29b171d0c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 21 Aug 2023 10:24:32 +0300 Subject: [PATCH 24/28] Remove RaceAnalysis joke --- src/analyses/raceAnalysis.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index f617df2048..462834e2f4 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -3,7 +3,7 @@ open GoblintCil open Analyses -(** Data race analysis with tries and hookers. +(** Data race analysis with tries for offsets and type-based memory locations for open code. Accesses are to memory locations ({{!Access.Memo} memos}) which consist of a root and offset. {{!Access.MemoRoot} Root} can be: From 00fb4964810643a998fb522cfc4e470b07a21ec8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 21 Aug 2023 10:30:09 +0300 Subject: [PATCH 25/28] Add C declarations to race analysis documentation --- src/analyses/raceAnalysis.ml | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 462834e2f4..d452b6b131 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -41,7 +41,20 @@ open Analyses This requires an implementation hack to still eagerly do outer distribution, but only of empty access sets. It ensures that corresponding trie nodes exist for traversal later. *) -(** Example structure of related memos for race checking: +(** Given C declarations: + {@c[ + struct S { + int f; + }; + + struct T { + struct S s; + }; + + struct T t; + ]} + + Example structure of related memos for race checking: {v (int) (S) (T) \ / \ / \ @@ -54,9 +67,7 @@ open Analyses where: - [(int)] is a type-based memo root for the primitive [int] type; - [(S)] and [(T)] are short for [(struct S)] and [(struct T)], which are type-based memo roots; - - [f] is a field of [S] and [s] is a field of [T]; - - [t] is a global variable of type [T]. - - prefix relations are indicated by [/]; + - prefix relations are indicated by [/], so access paths run diagonally from top-right to bottom-left; - type suffix relations are indicated by [\ ]. Prefix races: From 0329b30ad74cce93b55d4998f169faf108ec3eca Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 21 Aug 2023 10:44:05 +0300 Subject: [PATCH 26/28] Make race analysis documentation example races list complete --- src/analyses/raceAnalysis.ml | 46 ++++++++++++++++++++++++++++++------ 1 file changed, 39 insertions(+), 7 deletions(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index d452b6b131..4ca1094b4a 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -70,28 +70,60 @@ open Analyses - prefix relations are indicated by [/], so access paths run diagonally from top-right to bottom-left; - type suffix relations are indicated by [\ ]. - Prefix races: + All same-node races: + - Race between [t.s.f] and [t.s.f] is checked/reported at [t.s.f]. + - Race between [t.s] and [t.s] is checked/reported at [t.s]. + - Race between [t] and [t] is checked/reported at [t]. + - Race between [(T).s.f] and [(T).s.f] is checked/reported at [(T).s.f]. + - Race between [(T).s] and [(T).s] is checked/reported at [(T).s]. + - Race between [(T)] and [(T)] is checked/reported at [(T)]. + - Race between [(S).f] and [(S).f] is checked/reported at [(S).f]. + - Race between [(S)] and [(S)] is checked/reported at [(S)]. + - Race between [(int)] and [(int)] is checked/reported at [(int)]. + + All prefix races: - Race between [t.s.f] and [t.s] is checked/reported at [t.s.f]. - Race between [t.s.f] and [t] is checked/reported at [t.s.f]. - Race between [t.s] and [t] is checked/reported at [t.s]. - - Race between [t] and [t] is checked/reported at [t]. + - Race between [(T).s.f] and [(T).s] is checked/reported at [(T).s.f]. + - Race between [(T).s.f] and [(T)] is checked/reported at [(T).s.f]. + - Race between [(T).s] and [(T)] is checked/reported at [(T).s]. - Race between [(S).f] and [(S)] is checked/reported at [(S).f]. - Type suffix races: + All type suffix races: - Race between [t.s.f] and [(T).s.f] is checked/reported at [t.s.f]. - Race between [t.s.f] and [(S).f] is checked/reported at [t.s.f]. - Race between [t.s.f] and [(int)] is checked/reported at [t.s.f]. + - Race between [(T).s.f] and [(S).f] is checked/reported at [(T).s.f]. + - Race between [(T).s.f] and [(int)] is checked/reported at [(T).s.f]. - Race between [(S).f] and [(int)] is checked/reported at [(S).f]. + - Race between [t.s] and [(T).s] is checked/reported at [t.s]. + - Race between [t.s] and [(S)] is checked/reported at [t.s]. + - Race between [(T).s] and [(S)] is checked/reported at [(T).s]. + - Race between [t] and [(T)] is checked/reported at [t]. - Type suffix prefix races: + All type suffix prefix races: - Race between [t.s.f] and [(T).s] is checked/reported at [t.s.f]. - Race between [t.s.f] and [(T)] is checked/reported at [t.s.f]. - Race between [t.s.f] and [(S)] is checked/reported at [t.s.f]. - Race between [(T).s.f] and [(S)] is checked/reported at [(T).s.f]. - - Prefix-type suffix races: + - Race between [t.s] and [(T)] is checked/reported at [t.s]. + + All prefix-type suffix races: + - Race between [t.s] and [(T).s.f] is checked/reported at [t.s.f]. + - Race between [t.s] and [(S).f] is checked/reported at [t.s.f]. + - Race between [t.s] and [(int)] is checked/reported at [t.s.f]. + - Race between [t] and [(T).s.f] is checked/reported at [t.s.f]. + - Race between [t] and [(S).f] is checked/reported at [t.s.f]. + - Race between [t] and [(int)] is checked/reported at [t.s.f]. + - Race between [t] and [(T).s] is checked/reported at [t.s]. + - Race between [t] and [(S)] is checked/reported at [t.s]. - Race between [(T).s] and [(S).f] is checked/reported at [(T).s.f]. - - Race between [t] and [(S).f] is checked/reported at [t.s.f]. *) + - Race between [(T).s] and [(int)] is checked/reported at [(T).s.f]. + - Race between [(T)] and [(S).f] is checked/reported at [(T).s.f]. + - Race between [(T)] and [(int)] is checked/reported at [(T).s.f]. + - Race between [(T)] and [(S)] is checked/reported at [(T).s]. + - Race between [(S)] and [(int)] is checked/reported at [(S).f]. *) (** Data race analyzer without base --- this is the new standard *) From a8a8899d94f237cb76825b8a78f508fa50d3f450 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 21 Aug 2023 17:43:25 +0300 Subject: [PATCH 27/28] Add TODO for ana.race.direct-arithmetic in lazy outer distribution --- src/analyses/raceAnalysis.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index 4ca1094b4a..d6621154b7 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -241,6 +241,7 @@ struct match root, offset with | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* global.foo.bar -> (struct S).foo.bar *) (* TODO: Alloc variables void type *) | _, `NoOffset -> None (* primitive type *) + (* TODO: should handle ana.race.direct-arithmetic special case here? *) | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') (* (struct S).foo.bar -> (struct T).bar *) | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') (* (int[])[*] -> int *) | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *) From 4e1cf15f28143ec2e231e791f38f75e25ebd8efe Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 22 Aug 2023 15:10:16 +0300 Subject: [PATCH 28/28] Add comment about ana.race.direct-arithmetic --- src/analyses/raceAnalysis.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/analyses/raceAnalysis.ml b/src/analyses/raceAnalysis.ml index d6621154b7..74a98af6be 100644 --- a/src/analyses/raceAnalysis.ml +++ b/src/analyses/raceAnalysis.ml @@ -238,10 +238,11 @@ struct (** Get immediate type_suffix memo. *) let type_suffix_memo ((root, offset) : Access.Memo.t) : Access.Memo.t option = + (* No need to make ana.race.direct-arithmetic return None here, + because (int) is empty anyway since Access.add_distribute_outer isn't called. *) match root, offset with | `Var v, _ -> Some (`Type (Cil.typeSig v.vtype), offset) (* global.foo.bar -> (struct S).foo.bar *) (* TODO: Alloc variables void type *) | _, `NoOffset -> None (* primitive type *) - (* TODO: should handle ana.race.direct-arithmetic special case here? *) | _, `Field (f, offset') -> Some (`Type (Cil.typeSig f.ftype), offset') (* (struct S).foo.bar -> (struct T).bar *) | `Type (TSArray (ts, _, _)), `Index ((), offset') -> Some (`Type ts, offset') (* (int[])[*] -> int *) | _, `Index ((), offset') -> None (* TODO: why indexing on non-array? *)