From 57a074190a470ff3f2c85e1f1669555c4a58a3f6 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 23 May 2024 11:22:52 +0200 Subject: [PATCH 1/2] Add example for unsoundness due to escape --- .../46-apron2/86-escape-cluster12.c | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tests/regression/46-apron2/86-escape-cluster12.c diff --git a/tests/regression/46-apron2/86-escape-cluster12.c b/tests/regression/46-apron2/86-escape-cluster12.c new file mode 100644 index 0000000000..283e45b728 --- /dev/null +++ b/tests/regression/46-apron2/86-escape-cluster12.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 +#include +#include +void *a; + +void* nothing(void* arg) { + // Go multithreaded! +} + +void main() { + pthread_t t; + pthread_create(&t, 0, nothing, 0); + + int d = 5; + a = &d; + + if (0) + ; + + __goblint_check(1); // Should be reachable! +} From 7c6a86eae97ac4f376bf32053538f4b565c1ef2e Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 23 May 2024 17:40:38 +0200 Subject: [PATCH 2/2] Fix gloabl_init for escaped globals in cluster configuration --- src/analyses/apron/relationPriv.apron.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index dd4b65bab8..61da6ddc42 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -813,7 +813,9 @@ struct let g_var = V.global g in (* normal (strong) mapping: contains only still fully protected *) let g' = VS.singleton g in - let oct = LRD.find g' octs in + (* If there is no map entry yet which contains the global, default to top rather than bot *) + (* Happens e.g. in 46/86 because of escape *) + let oct = Option.default (RD.top ()) (LRD.find_opt g' octs) in LRD.singleton g' (RD.keep_vars oct [g_var]) let lock_get_m oct local_m get_m =