From ba396747badffe0a703136d1687cbaa420dcbe50 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 16 Dec 2024 17:40:49 +0200 Subject: [PATCH 1/4] Add mine-W-noinit test for resetting W in threadenter --- .../13-privatized/96-mine-W-threadenter.c | 32 +++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 tests/regression/13-privatized/96-mine-W-threadenter.c diff --git a/tests/regression/13-privatized/96-mine-W-threadenter.c b/tests/regression/13-privatized/96-mine-W-threadenter.c new file mode 100644 index 0000000000..424d45c52b --- /dev/null +++ b/tests/regression/13-privatized/96-mine-W-threadenter.c @@ -0,0 +1,32 @@ +// PARAM: --set ana.base.privatization mine-W-noinit --enable ana.int.enums +#include +#include + +int g; +pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + return NULL; +} + +void *t_fun2(void *arg) { + pthread_mutex_lock(&A); + pthread_mutex_unlock(&A); // spuriously publishes g = 8 + return NULL; +} + +int main() { + pthread_t id, id2; + pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded + + pthread_mutex_lock(&A); + g = 8; + pthread_create(&id2, NULL, t_fun2, NULL); // passes g = 8 and W: A -> {g} to t_fun2 + g = 0; + pthread_mutex_unlock(&A); + + pthread_mutex_lock(&A); + __goblint_check(g == 0); // TODO + pthread_mutex_unlock(&A); + return 0; +} From be4d3de02fba0cc16bfc8cc3072893b0d3516d6e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 16 Dec 2024 17:42:49 +0200 Subject: [PATCH 2/4] Fix mine-W-noinit threadenter to reset W --- src/analyses/basePriv.ml | 6 +++--- tests/regression/13-privatized/96-mine-W-threadenter.c | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 3afd758daa..792f084e05 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -1255,11 +1255,11 @@ struct else st - let threadenter = + let threadenter ask st = if Param.side_effect_global_init then - startstate_threadenter startstate + startstate_threadenter startstate ask st else - old_threadenter + {(old_threadenter ask st) with priv = W.empty ()} end module LockCenteredD = diff --git a/tests/regression/13-privatized/96-mine-W-threadenter.c b/tests/regression/13-privatized/96-mine-W-threadenter.c index 424d45c52b..ec9903b653 100644 --- a/tests/regression/13-privatized/96-mine-W-threadenter.c +++ b/tests/regression/13-privatized/96-mine-W-threadenter.c @@ -11,7 +11,7 @@ void *t_fun(void *arg) { void *t_fun2(void *arg) { pthread_mutex_lock(&A); - pthread_mutex_unlock(&A); // spuriously publishes g = 8 + pthread_mutex_unlock(&A); // used to spuriously publish g = 8 return NULL; } @@ -21,12 +21,12 @@ int main() { pthread_mutex_lock(&A); g = 8; - pthread_create(&id2, NULL, t_fun2, NULL); // passes g = 8 and W: A -> {g} to t_fun2 + pthread_create(&id2, NULL, t_fun2, NULL); // used to pass g = 8 and W: A -> {g} to t_fun2 g = 0; pthread_mutex_unlock(&A); pthread_mutex_lock(&A); - __goblint_check(g == 0); // TODO + __goblint_check(g == 0); pthread_mutex_unlock(&A); return 0; } From 5dba343249ef5abdc0cca2650176c5b81111896b Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Thu, 19 Dec 2024 11:07:46 +0100 Subject: [PATCH 3/4] forgot to wrap speculative mode around bounds computation --- src/cdomains/apron/sharedFunctions.apron.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 112e327530..c277999b14 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -170,6 +170,7 @@ struct | exception Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) | true -> texpr1 e | false -> (* Cast is not injective - we now try to establish suitable ranges manually *) + GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> (* try to evaluate e by EvalInt Query *) let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) in (* convert response to a constant *) From 7410da727afb82d30a194f780feba300a5ba719d Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Thu, 19 Dec 2024 16:36:43 +0100 Subject: [PATCH 4/4] better test --- src/cdomains/apron/sharedFunctions.apron.ml | 11 +++++---- .../77-lin2vareq/36-relations-overflow.c | 24 +++++++++++++++++++ 2 files changed, 30 insertions(+), 5 deletions(-) create mode 100644 tests/regression/77-lin2vareq/36-relations-overflow.c diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index c277999b14..fd6c578e60 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -170,11 +170,12 @@ struct | exception Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) | true -> texpr1 e | false -> (* Cast is not injective - we now try to establish suitable ranges manually *) - GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> - (* try to evaluate e by EvalInt Query *) - let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) in - (* convert response to a constant *) - let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res in + (* retrieving a valuerange for a non-injective cast works by a query to the value-domain with subsequent value extraction from domtuple - which should be speculative, since it is not program code *) + let const,res = GobRef.wrap AnalysisState.executing_speculative_computations true @@ fun () -> + (* try to evaluate e by EvalInt Query *) + let res = try (query e @@ Cilfacade.get_ikind_exp e) with Invalid_argument _ -> raise (Unsupported_CilExp Exp_not_supported) in + (* convert response to a constant *) + IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res, res in match const with | Some c -> Cst (Coeff.s_of_z c) (* Got a constant value -> use it straight away *) (* I gotten top, we can not guarantee injectivity *) diff --git a/tests/regression/77-lin2vareq/36-relations-overflow.c b/tests/regression/77-lin2vareq/36-relations-overflow.c new file mode 100644 index 0000000000..12997a5a3f --- /dev/null +++ b/tests/regression/77-lin2vareq/36-relations-overflow.c @@ -0,0 +1,24 @@ +//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none --set ana.activated[+] lin2vareq + +#include + +int nondet() { + int x; + return x; +} +int SIZE = 1; +int rand; + +int main() { + unsigned int n=2,i=8; + n = i%(SIZE+2); //NOWARN + + rand=nondet(); + + if (rand>5 && rand<10) { + n= i%(rand+2); //NOWARN + } + + return 0; +} +