From dc0c3e30391d2b202e7b678708d99de9aa0d0a04 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 13 May 2024 12:45:20 +0200 Subject: [PATCH 1/3] Add problematic examples for #1457 --- .../13-privatized/80-treachery-and-lies.c | 54 ++++++++++++++++++ .../81-how-could-we-have-been-so-blind.c | 55 ++++++++++++++++++ .../13-privatized/82-well-laid-out-plans.c | 56 +++++++++++++++++++ .../83-treachery-and-lies-write.c | 54 ++++++++++++++++++ ...84-how-could-we-have-been-so-blind-write.c | 55 ++++++++++++++++++ .../85-well-laid-out-plans-write.c | 56 +++++++++++++++++++ .../86-treachery-and-lies-lock.c | 54 ++++++++++++++++++ .../87-how-could-we-have-been-so-blind-lock.c | 55 ++++++++++++++++++ .../88-well-laid-out-plans-lock.c | 56 +++++++++++++++++++ 9 files changed, 495 insertions(+) create mode 100644 tests/regression/13-privatized/80-treachery-and-lies.c create mode 100644 tests/regression/13-privatized/81-how-could-we-have-been-so-blind.c create mode 100644 tests/regression/13-privatized/82-well-laid-out-plans.c create mode 100644 tests/regression/13-privatized/83-treachery-and-lies-write.c create mode 100644 tests/regression/13-privatized/84-how-could-we-have-been-so-blind-write.c create mode 100644 tests/regression/13-privatized/85-well-laid-out-plans-write.c create mode 100644 tests/regression/13-privatized/86-treachery-and-lies-lock.c create mode 100644 tests/regression/13-privatized/87-how-could-we-have-been-so-blind-lock.c create mode 100644 tests/regression/13-privatized/88-well-laid-out-plans-lock.c diff --git a/tests/regression/13-privatized/80-treachery-and-lies.c b/tests/regression/13-privatized/80-treachery-and-lies.c new file mode 100644 index 0000000000..7670bad8f8 --- /dev/null +++ b/tests/regression/13-privatized/80-treachery-and-lies.c @@ -0,0 +1,54 @@ +// PARAM: --set ana.base.privatization protection --enable ana.int.enums +#include +#include +struct a { + int b; +}; + +struct a *ptr; +struct a *straightandnarrow; + +pthread_mutex_t m; + +void doit() { + void *newa = malloc(sizeof(struct a)); + + pthread_mutex_lock(&m); + ptr->b = 5; + + int fear = straightandnarrow->b; + __goblint_check(fear == 5); //UNKNOWN! + + ptr = newa; + pthread_mutex_unlock(&m); + + pthread_mutex_lock(&m); + int hope = straightandnarrow->b; + __goblint_check(hope == 5); //UNKNOWN! + pthread_mutex_unlock(&m); + +} + +void* k(void *arg) { + doit(); + return NULL; +} + +int main() { + int top; + struct a other = { 0 }; + struct a other2 = { 42 }; + if(top) { + ptr = &other; + } else { + ptr = &other2; + } + + straightandnarrow = &other; + + pthread_t t1; + pthread_create(&t1, 0, k, 0); + + doit(); + return 0; +} diff --git a/tests/regression/13-privatized/81-how-could-we-have-been-so-blind.c b/tests/regression/13-privatized/81-how-could-we-have-been-so-blind.c new file mode 100644 index 0000000000..d6a33dece4 --- /dev/null +++ b/tests/regression/13-privatized/81-how-could-we-have-been-so-blind.c @@ -0,0 +1,55 @@ +// PARAM: --set ana.base.privatization protection --enable ana.int.enums +// Like 80-treachery-and-lies.c, but somewhat simplified to not use structs and malloc etc +#include +#include +struct a { + int b; +}; + +int *ptr; +int *immer_da_oane; + +pthread_mutex_t m; + +void doit() { + pthread_mutex_lock(&m); + *ptr = 5; + + // Should be either 5 or 0, depending on which one the pointer points to + int fear = *immer_da_oane; + __goblint_check(fear == 5); //UNKNOWN! + + pthread_mutex_unlock(&m); + + pthread_mutex_lock(&m); + int hope = *immer_da_oane; + __goblint_check(hope == 5); //UNKNOWN! + pthread_mutex_unlock(&m); + +} + +void* k(void *arg) { + // Force MT + return NULL; +} + +int main() { + int top; + + int da_oane = 0; + int de_andre = 42; + + if(top) { + ptr = &da_oane; + } else { + ptr = &de_andre; + } + + immer_da_oane = &da_oane; + + pthread_t t1; + pthread_create(&t1, 0, k, 0); + + doit(); + return 0; +} diff --git a/tests/regression/13-privatized/82-well-laid-out-plans.c b/tests/regression/13-privatized/82-well-laid-out-plans.c new file mode 100644 index 0000000000..8eb1cc11e1 --- /dev/null +++ b/tests/regression/13-privatized/82-well-laid-out-plans.c @@ -0,0 +1,56 @@ +// PARAM: --set ana.base.privatization protection --enable ana.int.enums +// Like 81-how-could-we-have-been-so-blind.c, but with syntactic globals instead of escaping ones. +#include +#include +struct a { + int b; +}; + +int *ptr; +int *immer_da_oane; + +int da_oane = 0; +int de_andre = 42; + +pthread_mutex_t m; + +void doit() { + pthread_mutex_lock(&m); + *ptr = 5; + + // Should be either 0 or 5, depending on which one ptr points to + int fear = *immer_da_oane; + __goblint_check(fear == 5); //UNKNOWN! + + pthread_mutex_unlock(&m); + + pthread_mutex_lock(&m); + // This works + int hope = *immer_da_oane; + __goblint_check(hope == 5); //UNKNOWN! + pthread_mutex_unlock(&m); + +} + +void* k(void *arg) { + // Force MT + return NULL; +} + +int main() { + int top; + + if(top) { + ptr = &da_oane; + } else { + ptr = &de_andre; + } + + immer_da_oane = &da_oane; + + pthread_t t1; + pthread_create(&t1, 0, k, 0); + + doit(); + return 0; +} diff --git a/tests/regression/13-privatized/83-treachery-and-lies-write.c b/tests/regression/13-privatized/83-treachery-and-lies-write.c new file mode 100644 index 0000000000..f317100825 --- /dev/null +++ b/tests/regression/13-privatized/83-treachery-and-lies-write.c @@ -0,0 +1,54 @@ +// PARAM: --set ana.base.privatization write --enable ana.int.enums +#include +#include +struct a { + int b; +}; + +struct a *ptr; +struct a *straightandnarrow; + +pthread_mutex_t m; + +void doit() { + void *newa = malloc(sizeof(struct a)); + + pthread_mutex_lock(&m); + ptr->b = 5; + + int fear = straightandnarrow->b; + __goblint_check(fear == 5); //UNKNOWN! + + ptr = newa; + pthread_mutex_unlock(&m); + + pthread_mutex_lock(&m); + int hope = straightandnarrow->b; + __goblint_check(hope == 5); //UNKNOWN! + pthread_mutex_unlock(&m); + +} + +void* k(void *arg) { + doit(); + return NULL; +} + +int main() { + int top; + struct a other = { 0 }; + struct a other2 = { 42 }; + if(top) { + ptr = &other; + } else { + ptr = &other2; + } + + straightandnarrow = &other; + + pthread_t t1; + pthread_create(&t1, 0, k, 0); + + doit(); + return 0; +} diff --git a/tests/regression/13-privatized/84-how-could-we-have-been-so-blind-write.c b/tests/regression/13-privatized/84-how-could-we-have-been-so-blind-write.c new file mode 100644 index 0000000000..c62e49ba69 --- /dev/null +++ b/tests/regression/13-privatized/84-how-could-we-have-been-so-blind-write.c @@ -0,0 +1,55 @@ +// PARAM: --set ana.base.privatization write --enable ana.int.enums +// Like 80-treachery-and-lies.c, but somewhat simplified to not use structs and malloc etc +#include +#include +struct a { + int b; +}; + +int *ptr; +int *immer_da_oane; + +pthread_mutex_t m; + +void doit() { + pthread_mutex_lock(&m); + *ptr = 5; + + // Should be either 5 or 0, depending on which one the pointer points to + int fear = *immer_da_oane; + __goblint_check(fear == 5); //UNKNOWN! + + pthread_mutex_unlock(&m); + + pthread_mutex_lock(&m); + int hope = *immer_da_oane; + __goblint_check(hope == 5); //UNKNOWN! + pthread_mutex_unlock(&m); + +} + +void* k(void *arg) { + // Force MT + return NULL; +} + +int main() { + int top; + + int da_oane = 0; + int de_andre = 42; + + if(top) { + ptr = &da_oane; + } else { + ptr = &de_andre; + } + + immer_da_oane = &da_oane; + + pthread_t t1; + pthread_create(&t1, 0, k, 0); + + doit(); + return 0; +} diff --git a/tests/regression/13-privatized/85-well-laid-out-plans-write.c b/tests/regression/13-privatized/85-well-laid-out-plans-write.c new file mode 100644 index 0000000000..246804f82e --- /dev/null +++ b/tests/regression/13-privatized/85-well-laid-out-plans-write.c @@ -0,0 +1,56 @@ +// PARAM: --set ana.base.privatization write --enable ana.int.enums +// Like 81-how-could-we-have-been-so-blind.c, but with syntactic globals instead of escaping ones. +#include +#include +struct a { + int b; +}; + +int *ptr; +int *immer_da_oane; + +int da_oane = 0; +int de_andre = 42; + +pthread_mutex_t m; + +void doit() { + pthread_mutex_lock(&m); + *ptr = 5; + + // Should be either 0 or 5, depending on which one ptr points to + int fear = *immer_da_oane; + __goblint_check(fear == 5); //UNKNOWN! + + pthread_mutex_unlock(&m); + + pthread_mutex_lock(&m); + // This works + int hope = *immer_da_oane; + __goblint_check(hope == 5); //UNKNOWN! + pthread_mutex_unlock(&m); + +} + +void* k(void *arg) { + // Force MT + return NULL; +} + +int main() { + int top; + + if(top) { + ptr = &da_oane; + } else { + ptr = &de_andre; + } + + immer_da_oane = &da_oane; + + pthread_t t1; + pthread_create(&t1, 0, k, 0); + + doit(); + return 0; +} diff --git a/tests/regression/13-privatized/86-treachery-and-lies-lock.c b/tests/regression/13-privatized/86-treachery-and-lies-lock.c new file mode 100644 index 0000000000..aa21f89ea7 --- /dev/null +++ b/tests/regression/13-privatized/86-treachery-and-lies-lock.c @@ -0,0 +1,54 @@ +// PARAM: --set ana.base.privatization lock --enable ana.int.enums +#include +#include +struct a { + int b; +}; + +struct a *ptr; +struct a *straightandnarrow; + +pthread_mutex_t m; + +void doit() { + void *newa = malloc(sizeof(struct a)); + + pthread_mutex_lock(&m); + ptr->b = 5; + + int fear = straightandnarrow->b; + __goblint_check(fear == 5); //UNKNOWN! + + ptr = newa; + pthread_mutex_unlock(&m); + + pthread_mutex_lock(&m); + int hope = straightandnarrow->b; + __goblint_check(hope == 5); //UNKNOWN! + pthread_mutex_unlock(&m); + +} + +void* k(void *arg) { + doit(); + return NULL; +} + +int main() { + int top; + struct a other = { 0 }; + struct a other2 = { 42 }; + if(top) { + ptr = &other; + } else { + ptr = &other2; + } + + straightandnarrow = &other; + + pthread_t t1; + pthread_create(&t1, 0, k, 0); + + doit(); + return 0; +} diff --git a/tests/regression/13-privatized/87-how-could-we-have-been-so-blind-lock.c b/tests/regression/13-privatized/87-how-could-we-have-been-so-blind-lock.c new file mode 100644 index 0000000000..02f5b721ba --- /dev/null +++ b/tests/regression/13-privatized/87-how-could-we-have-been-so-blind-lock.c @@ -0,0 +1,55 @@ +// PARAM: --set ana.base.privatization lock --enable ana.int.enums +// Like 80-treachery-and-lies.c, but somewhat simplified to not use structs and malloc etc +#include +#include +struct a { + int b; +}; + +int *ptr; +int *immer_da_oane; + +pthread_mutex_t m; + +void doit() { + pthread_mutex_lock(&m); + *ptr = 5; + + // Should be either 5 or 0, depending on which one the pointer points to + int fear = *immer_da_oane; + __goblint_check(fear == 5); //UNKNOWN! + + pthread_mutex_unlock(&m); + + pthread_mutex_lock(&m); + int hope = *immer_da_oane; + __goblint_check(hope == 5); //UNKNOWN! + pthread_mutex_unlock(&m); + +} + +void* k(void *arg) { + // Force MT + return NULL; +} + +int main() { + int top; + + int da_oane = 0; + int de_andre = 42; + + if(top) { + ptr = &da_oane; + } else { + ptr = &de_andre; + } + + immer_da_oane = &da_oane; + + pthread_t t1; + pthread_create(&t1, 0, k, 0); + + doit(); + return 0; +} diff --git a/tests/regression/13-privatized/88-well-laid-out-plans-lock.c b/tests/regression/13-privatized/88-well-laid-out-plans-lock.c new file mode 100644 index 0000000000..9caae2daf1 --- /dev/null +++ b/tests/regression/13-privatized/88-well-laid-out-plans-lock.c @@ -0,0 +1,56 @@ +// PARAM: --set ana.base.privatization lock --enable ana.int.enums +// Like 81-how-could-we-have-been-so-blind.c, but with syntactic globals instead of escaping ones. +#include +#include +struct a { + int b; +}; + +int *ptr; +int *immer_da_oane; + +int da_oane = 0; +int de_andre = 42; + +pthread_mutex_t m; + +void doit() { + pthread_mutex_lock(&m); + *ptr = 5; + + // Should be either 0 or 5, depending on which one ptr points to + int fear = *immer_da_oane; + __goblint_check(fear == 5); //UNKNOWN! + + pthread_mutex_unlock(&m); + + pthread_mutex_lock(&m); + // This works + int hope = *immer_da_oane; + __goblint_check(hope == 5); //UNKNOWN! + pthread_mutex_unlock(&m); + +} + +void* k(void *arg) { + // Force MT + return NULL; +} + +int main() { + int top; + + if(top) { + ptr = &da_oane; + } else { + ptr = &de_andre; + } + + immer_da_oane = &da_oane; + + pthread_t t1; + pthread_create(&t1, 0, k, 0); + + doit(); + return 0; +} From cd795646e190294c6e945f056a98567e57c8a5db Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 13 May 2024 13:21:27 +0200 Subject: [PATCH 2/3] `set`: For non-definite AD, join over **all** components not just `cpa` Earlier `priv` was not joined over, which lead to unsound results #1457. On top, this also considers `dep` and `weak`. While not strictly necessary to pass tests, this also seems to be the right thing here. --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index eb6b9154bb..4385f1fca8 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1738,7 +1738,7 @@ struct (* if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *) (* If the address was definite, then we just return it. If the address * was ambiguous, we have to join it with the initial state. *) - let nst = if AD.cardinal lval > 1 then { nst with cpa = CPA.join st.cpa nst.cpa } else nst in + let nst = if AD.cardinal lval > 1 then D.join st nst else nst in (* if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *) nst with From d1ed12ce404fb98e2d2ee4622ae512830a1469ab Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 15 May 2024 10:08:41 +0200 Subject: [PATCH 3/3] Rename tests to more speaking (arguably less fun) names --- .../{80-treachery-and-lies.c => 80-nondet-struct-ptr.c} | 0 ...-could-we-have-been-so-blind.c => 81-nondet-local-pointer.c} | 2 +- .../{82-well-laid-out-plans.c => 82-nondet-global-pointer.c} | 2 +- ...-treachery-and-lies-write.c => 83-nondet-struct-ptr-write.c} | 0 ...ve-been-so-blind-write.c => 84-nondet-local-pointer-write.c} | 1 - ...-laid-out-plans-write.c => 85-nondet-global-pointer-write.c} | 1 - ...86-treachery-and-lies-lock.c => 86-nondet-struct-ptr-lock.c} | 0 ...have-been-so-blind-lock.c => 87-nondet-local-pointer-lock.c} | 1 - ...ll-laid-out-plans-lock.c => 88-nondet-global-pointer-lock.c} | 1 - 9 files changed, 2 insertions(+), 6 deletions(-) rename tests/regression/13-privatized/{80-treachery-and-lies.c => 80-nondet-struct-ptr.c} (100%) rename tests/regression/13-privatized/{81-how-could-we-have-been-so-blind.c => 81-nondet-local-pointer.c} (90%) rename tests/regression/13-privatized/{82-well-laid-out-plans.c => 82-nondet-global-pointer.c} (89%) rename tests/regression/13-privatized/{83-treachery-and-lies-write.c => 83-nondet-struct-ptr-write.c} (100%) rename tests/regression/13-privatized/{84-how-could-we-have-been-so-blind-write.c => 84-nondet-local-pointer-write.c} (90%) rename tests/regression/13-privatized/{85-well-laid-out-plans-write.c => 85-nondet-global-pointer-write.c} (89%) rename tests/regression/13-privatized/{86-treachery-and-lies-lock.c => 86-nondet-struct-ptr-lock.c} (100%) rename tests/regression/13-privatized/{87-how-could-we-have-been-so-blind-lock.c => 87-nondet-local-pointer-lock.c} (90%) rename tests/regression/13-privatized/{88-well-laid-out-plans-lock.c => 88-nondet-global-pointer-lock.c} (89%) diff --git a/tests/regression/13-privatized/80-treachery-and-lies.c b/tests/regression/13-privatized/80-nondet-struct-ptr.c similarity index 100% rename from tests/regression/13-privatized/80-treachery-and-lies.c rename to tests/regression/13-privatized/80-nondet-struct-ptr.c diff --git a/tests/regression/13-privatized/81-how-could-we-have-been-so-blind.c b/tests/regression/13-privatized/81-nondet-local-pointer.c similarity index 90% rename from tests/regression/13-privatized/81-how-could-we-have-been-so-blind.c rename to tests/regression/13-privatized/81-nondet-local-pointer.c index d6a33dece4..caa256ef73 100644 --- a/tests/regression/13-privatized/81-how-could-we-have-been-so-blind.c +++ b/tests/regression/13-privatized/81-nondet-local-pointer.c @@ -1,5 +1,5 @@ // PARAM: --set ana.base.privatization protection --enable ana.int.enums -// Like 80-treachery-and-lies.c, but somewhat simplified to not use structs and malloc etc +// Like 80-nondet-struct-ptr.c, but somewhat simplified to not use structs and malloc etc #include #include struct a { diff --git a/tests/regression/13-privatized/82-well-laid-out-plans.c b/tests/regression/13-privatized/82-nondet-global-pointer.c similarity index 89% rename from tests/regression/13-privatized/82-well-laid-out-plans.c rename to tests/regression/13-privatized/82-nondet-global-pointer.c index 8eb1cc11e1..50b4e267cb 100644 --- a/tests/regression/13-privatized/82-well-laid-out-plans.c +++ b/tests/regression/13-privatized/82-nondet-global-pointer.c @@ -1,5 +1,5 @@ // PARAM: --set ana.base.privatization protection --enable ana.int.enums -// Like 81-how-could-we-have-been-so-blind.c, but with syntactic globals instead of escaping ones. +// Like 81-nondet-struct-ptr.c, but with syntactic globals instead of escaping ones. #include #include struct a { diff --git a/tests/regression/13-privatized/83-treachery-and-lies-write.c b/tests/regression/13-privatized/83-nondet-struct-ptr-write.c similarity index 100% rename from tests/regression/13-privatized/83-treachery-and-lies-write.c rename to tests/regression/13-privatized/83-nondet-struct-ptr-write.c diff --git a/tests/regression/13-privatized/84-how-could-we-have-been-so-blind-write.c b/tests/regression/13-privatized/84-nondet-local-pointer-write.c similarity index 90% rename from tests/regression/13-privatized/84-how-could-we-have-been-so-blind-write.c rename to tests/regression/13-privatized/84-nondet-local-pointer-write.c index c62e49ba69..86337cea43 100644 --- a/tests/regression/13-privatized/84-how-could-we-have-been-so-blind-write.c +++ b/tests/regression/13-privatized/84-nondet-local-pointer-write.c @@ -1,5 +1,4 @@ // PARAM: --set ana.base.privatization write --enable ana.int.enums -// Like 80-treachery-and-lies.c, but somewhat simplified to not use structs and malloc etc #include #include struct a { diff --git a/tests/regression/13-privatized/85-well-laid-out-plans-write.c b/tests/regression/13-privatized/85-nondet-global-pointer-write.c similarity index 89% rename from tests/regression/13-privatized/85-well-laid-out-plans-write.c rename to tests/regression/13-privatized/85-nondet-global-pointer-write.c index 246804f82e..e8e3aa13d5 100644 --- a/tests/regression/13-privatized/85-well-laid-out-plans-write.c +++ b/tests/regression/13-privatized/85-nondet-global-pointer-write.c @@ -1,5 +1,4 @@ // PARAM: --set ana.base.privatization write --enable ana.int.enums -// Like 81-how-could-we-have-been-so-blind.c, but with syntactic globals instead of escaping ones. #include #include struct a { diff --git a/tests/regression/13-privatized/86-treachery-and-lies-lock.c b/tests/regression/13-privatized/86-nondet-struct-ptr-lock.c similarity index 100% rename from tests/regression/13-privatized/86-treachery-and-lies-lock.c rename to tests/regression/13-privatized/86-nondet-struct-ptr-lock.c diff --git a/tests/regression/13-privatized/87-how-could-we-have-been-so-blind-lock.c b/tests/regression/13-privatized/87-nondet-local-pointer-lock.c similarity index 90% rename from tests/regression/13-privatized/87-how-could-we-have-been-so-blind-lock.c rename to tests/regression/13-privatized/87-nondet-local-pointer-lock.c index 02f5b721ba..21390b19dd 100644 --- a/tests/regression/13-privatized/87-how-could-we-have-been-so-blind-lock.c +++ b/tests/regression/13-privatized/87-nondet-local-pointer-lock.c @@ -1,5 +1,4 @@ // PARAM: --set ana.base.privatization lock --enable ana.int.enums -// Like 80-treachery-and-lies.c, but somewhat simplified to not use structs and malloc etc #include #include struct a { diff --git a/tests/regression/13-privatized/88-well-laid-out-plans-lock.c b/tests/regression/13-privatized/88-nondet-global-pointer-lock.c similarity index 89% rename from tests/regression/13-privatized/88-well-laid-out-plans-lock.c rename to tests/regression/13-privatized/88-nondet-global-pointer-lock.c index 9caae2daf1..daeb5df03a 100644 --- a/tests/regression/13-privatized/88-well-laid-out-plans-lock.c +++ b/tests/regression/13-privatized/88-nondet-global-pointer-lock.c @@ -1,5 +1,4 @@ // PARAM: --set ana.base.privatization lock --enable ana.int.enums -// Like 81-how-could-we-have-been-so-blind.c, but with syntactic globals instead of escaping ones. #include #include struct a {