From 2a714b81804eb1bb4c06ba36aee34aa18bc9de10 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 30 Jul 2024 15:53:17 +0300 Subject: [PATCH] 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