Skip to content

Commit

Permalink
Simplify and generalize malloc fix in relational mutex-meet
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Jul 30, 2024
1 parent 896f236 commit 2a714b8
Showing 1 changed file with 7 additions and 13 deletions.
20 changes: 7 additions & 13 deletions src/analyses/apron/relationPriv.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 2a714b8

Please sign in to comment.