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 diff --git a/tests/regression/13-privatized/80-nondet-struct-ptr.c b/tests/regression/13-privatized/80-nondet-struct-ptr.c new file mode 100644 index 0000000000..7670bad8f8 --- /dev/null +++ b/tests/regression/13-privatized/80-nondet-struct-ptr.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-nondet-local-pointer.c b/tests/regression/13-privatized/81-nondet-local-pointer.c new file mode 100644 index 0000000000..caa256ef73 --- /dev/null +++ b/tests/regression/13-privatized/81-nondet-local-pointer.c @@ -0,0 +1,55 @@ +// PARAM: --set ana.base.privatization protection --enable ana.int.enums +// Like 80-nondet-struct-ptr.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-nondet-global-pointer.c b/tests/regression/13-privatized/82-nondet-global-pointer.c new file mode 100644 index 0000000000..50b4e267cb --- /dev/null +++ b/tests/regression/13-privatized/82-nondet-global-pointer.c @@ -0,0 +1,56 @@ +// PARAM: --set ana.base.privatization protection --enable ana.int.enums +// Like 81-nondet-struct-ptr.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-nondet-struct-ptr-write.c b/tests/regression/13-privatized/83-nondet-struct-ptr-write.c new file mode 100644 index 0000000000..f317100825 --- /dev/null +++ b/tests/regression/13-privatized/83-nondet-struct-ptr-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-nondet-local-pointer-write.c b/tests/regression/13-privatized/84-nondet-local-pointer-write.c new file mode 100644 index 0000000000..86337cea43 --- /dev/null +++ b/tests/regression/13-privatized/84-nondet-local-pointer-write.c @@ -0,0 +1,54 @@ +// PARAM: --set ana.base.privatization write --enable ana.int.enums +#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-nondet-global-pointer-write.c b/tests/regression/13-privatized/85-nondet-global-pointer-write.c new file mode 100644 index 0000000000..e8e3aa13d5 --- /dev/null +++ b/tests/regression/13-privatized/85-nondet-global-pointer-write.c @@ -0,0 +1,55 @@ +// PARAM: --set ana.base.privatization write --enable ana.int.enums +#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-nondet-struct-ptr-lock.c b/tests/regression/13-privatized/86-nondet-struct-ptr-lock.c new file mode 100644 index 0000000000..aa21f89ea7 --- /dev/null +++ b/tests/regression/13-privatized/86-nondet-struct-ptr-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-nondet-local-pointer-lock.c b/tests/regression/13-privatized/87-nondet-local-pointer-lock.c new file mode 100644 index 0000000000..21390b19dd --- /dev/null +++ b/tests/regression/13-privatized/87-nondet-local-pointer-lock.c @@ -0,0 +1,54 @@ +// PARAM: --set ana.base.privatization lock --enable ana.int.enums +#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-nondet-global-pointer-lock.c b/tests/regression/13-privatized/88-nondet-global-pointer-lock.c new file mode 100644 index 0000000000..daeb5df03a --- /dev/null +++ b/tests/regression/13-privatized/88-nondet-global-pointer-lock.c @@ -0,0 +1,55 @@ +// PARAM: --set ana.base.privatization lock --enable ana.int.enums +#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; +}