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 125df89
Showing 1 changed file with 5 additions and 12 deletions.
17 changes: 5 additions & 12 deletions src/analyses/apron/relationPriv.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -482,22 +482,15 @@ 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 =
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 125df89

Please sign in to comment.