Skip to content

Commit

Permalink
Check in TheadAnalysis.return whether the return is actually a thread…
Browse files Browse the repository at this point in the history
…return before side-effecting.
  • Loading branch information
jerhard committed Nov 22, 2023
1 parent be9171b commit 585a65d
Showing 1 changed file with 8 additions and 4 deletions.
12 changes: 8 additions & 4 deletions src/analyses/threadAnalysis.ml
Original file line number Diff line number Diff line change
Expand Up @@ -22,12 +22,15 @@ struct
module P = IdentityP (D)

(* transfer functions *)
let return ctx (exp:exp option) _ : D.t =
let handle_thread_return ctx (exp: exp option) =
let tid = ThreadId.get_current (Analyses.ask_of_ctx ctx) in
begin match tid with
match tid with
| `Lifted tid -> ctx.sideg tid (false, TS.bot (), not (D.is_empty ctx.local))
| _ -> ()
end;

let return ctx (exp:exp option) _ : D.t =
if ctx.ask Queries.MayBeThreadReturn then
handle_thread_return ctx exp;
ctx.local

let rec is_not_unique ctx tid =
Expand Down Expand Up @@ -65,7 +68,8 @@ struct
| _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *)
| exception SetDomain.Unsupported _ -> ctx.local)
| ThreadExit { ret_val } ->
return ctx (Some ret_val) ()
handle_thread_return ctx (Some ret_val);
ctx.local
| _ -> ctx.local

let query ctx (type a) (q: a Queries.t): a Queries.result =
Expand Down

0 comments on commit 585a65d

Please sign in to comment.