From 9b4b255f29f887b5cffb38280e7ebf86ed7cdd4c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 27 May 2024 17:45:58 +0200 Subject: [PATCH 1/3] Fix `mutex-meet` for malloc after thread creation --- src/analyses/apron/relationPriv.apron.ml | 9 +++++++-- tests/regression/46-apron2/89-malloc.c | 21 +++++++++++++++++++++ tests/regression/46-apron2/90-malloc2.c | 21 +++++++++++++++++++++ 3 files changed, 49 insertions(+), 2 deletions(-) create mode 100644 tests/regression/46-apron2/89-malloc.c create mode 100644 tests/regression/46-apron2/90-malloc2.c diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 61da6ddc42..046e1230d7 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -479,7 +479,7 @@ struct let get_mutex_inits' = keep_only_protected_globals ask m get_mutex_inits in RD.join get_m get_mutex_inits' - let get_mutex_global_g_with_mutex_inits ask getg g = + let get_mutex_global_g_with_mutex_inits (ask:Q.ask) getg g = let g_var = AV.global g in let get_mutex_global_g = if Param.handle_atomic then ( @@ -487,7 +487,12 @@ struct RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var] ) else - getg (V.global g) + let r = getg (V.global g) in + if RD.is_bot r && (ask.f (Queries.IsAllocVar g)) then + (* malloc'ed blobs may not have a value here yet *) + RD.top () + else + r in let get_mutex_inits = getg V.mutex_inits in let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in diff --git a/tests/regression/46-apron2/89-malloc.c b/tests/regression/46-apron2/89-malloc.c new file mode 100644 index 0000000000..8780568748 --- /dev/null +++ b/tests/regression/46-apron2/89-malloc.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set ana.apron.domain interval --set sem.int.signed_overflow assume_none +// Checks that assinging to malloc'ed memory does not cause both branches to be dead +#include +#include +void nop(void* arg) { +} + +void main() { + pthread_t thread; + pthread_create(&thread, 0, &nop, 0); + + long *k = malloc(sizeof(long)); + *k = 5; + if (1) + ; + + __goblint_check(*k >= 5); // Reachable and true + + *k = *k+1; + __goblint_check(*k >= 5); // Reachable and true +} diff --git a/tests/regression/46-apron2/90-malloc2.c b/tests/regression/46-apron2/90-malloc2.c new file mode 100644 index 0000000000..36696956e7 --- /dev/null +++ b/tests/regression/46-apron2/90-malloc2.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid --set ana.apron.domain interval --set sem.int.signed_overflow assume_none +// Checks that assinging to malloc'ed memory does not cause both branches to be dead +#include +#include +void nop(void* arg) { +} + +void main() { + pthread_t thread; + pthread_create(&thread, 0, &nop, 0); + + long *k = malloc(sizeof(long)); + *k = 5; + if (1) + ; + + __goblint_check(*k >= 5); // Reachable and true + + *k = *k+1; + __goblint_check(*k >= 5); // Reachable and true +} From 896f236c98ba829aee25e5f02cb08d4bb2bba9b1 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 27 May 2024 17:55:00 +0200 Subject: [PATCH 2/3] Also fix atomic --- src/analyses/apron/relationPriv.apron.ml | 21 ++++++++++--------- tests/regression/46-apron2/91-malloc-atomic.c | 21 +++++++++++++++++++ 2 files changed, 32 insertions(+), 10 deletions(-) create mode 100644 tests/regression/46-apron2/91-malloc-atomic.c diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 046e1230d7..78a06dc227 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -482,17 +482,18 @@ struct let get_mutex_global_g_with_mutex_inits (ask:Q.ask) getg g = let g_var = AV.global g in let get_mutex_global_g = - if Param.handle_atomic then ( - (* Unprotected invariant is one big relation. *) - RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var] - ) - else - let r = getg (V.global g) in - if RD.is_bot r && (ask.f (Queries.IsAllocVar g)) then - (* malloc'ed blobs may not have a value here yet *) - RD.top () + let r = + if Param.handle_atomic then + (* Unprotected invariant is one big relation. *) + RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var] else - r + getg (V.global g) + in + if RD.is_bot r && (ask.f (Queries.IsAllocVar g)) then + (* malloc'ed blobs may not have a value here yet *) + RD.top () + else + r in let get_mutex_inits = getg V.mutex_inits in let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in diff --git a/tests/regression/46-apron2/91-malloc-atomic.c b/tests/regression/46-apron2/91-malloc-atomic.c new file mode 100644 index 0000000000..b2f057f6a4 --- /dev/null +++ b/tests/regression/46-apron2/91-malloc-atomic.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.apron.domain interval --set sem.int.signed_overflow assume_none +// Checks that assinging to malloc'ed memory does not cause both branches to be dead +#include +#include +void nop(void* arg) { +} + +void main() { + pthread_t thread; + pthread_create(&thread, 0, &nop, 0); + + long *k = malloc(sizeof(long)); + *k = 5; + if (1) + ; + + __goblint_check(*k >= 5); // Reachable and true + + *k = *k+1; + __goblint_check(*k >= 5); // Reachable and true +} From 2a714b81804eb1bb4c06ba36aee34aa18bc9de10 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 30 Jul 2024 15:53:17 +0300 Subject: [PATCH 3/3] Simplify and generalize malloc fix in relational mutex-meet --- src/analyses/apron/relationPriv.apron.ml | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 78a06dc227..ad4d26dfbf 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -479,25 +479,19 @@ struct let get_mutex_inits' = keep_only_protected_globals ask m get_mutex_inits in RD.join get_m get_mutex_inits' - let get_mutex_global_g_with_mutex_inits (ask:Q.ask) getg g = + let get_mutex_global_g_with_mutex_inits ask getg g = let g_var = AV.global g in let get_mutex_global_g = - let r = - if Param.handle_atomic then - (* Unprotected invariant is one big relation. *) - RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var] - else - getg (V.global g) - in - if RD.is_bot r && (ask.f (Queries.IsAllocVar g)) then - (* malloc'ed blobs may not have a value here yet *) - RD.top () + if Param.handle_atomic then ( + (* Unprotected invariant is one big relation. *) + RD.keep_vars (getg (V.mutex atomic_mutex)) [g_var] + ) else - r + getg (V.global g) in let get_mutex_inits = getg V.mutex_inits in let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in - if not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *) + if RD.mem_var get_mutex_global_g g_var && not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *) (* This is an escaped variable whose value was never side-effected to get_mutex_inits' *) get_mutex_global_g else