diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index b386af162b..3adfa272bb 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -1011,17 +1011,17 @@ struct ) ) else ( - match ConcDomain.ThreadSet.elements tids with - | [tid] -> - let lmust',l' = G.thread (getg (V.thread tid)) in - {st with priv = (w, LMust.union lmust' lmust, L.join l l')} - | _ -> - (* To match the paper more closely, one would have to join in the non-definite case too *) - (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) - st - | exception SetDomain.Unsupported _ -> - (* elements throws if the thread set is top *) - st + if ConcDomain.ThreadSet.is_top tids + then st + else + match ConcDomain.ThreadSet.elements tids with + | [tid] -> + let lmust',l' = G.thread (getg (V.thread tid)) in + {st with priv = (w, LMust.union lmust' lmust, L.join l l')} + | _ -> + (* To match the paper more closely, one would have to join in the non-definite case too *) + (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) + st ) let thread_return ask getg sideg tid (st: relation_components_t) = diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 0154924a1c..ed6439a847 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -544,17 +544,17 @@ struct ) ) else ( - match ConcDomain.ThreadSet.elements tids with - | [tid] -> - let lmust',l' = G.thread (getg (V.thread tid)) in - {st with priv = (w, LMust.union lmust' lmust, L.join l l')} - | _ -> - (* To match the paper more closely, one would have to join in the non-definite case too *) - (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) - st - | exception SetDomain.Unsupported _ -> - (* elements throws if the thread set is top *) - st + if (ConcDomain.ThreadSet.is_top tids) + then st + else + match ConcDomain.ThreadSet.elements tids with + | [tid] -> + let lmust',l' = G.thread (getg (V.thread tid)) in + {st with priv = (w, LMust.union lmust' lmust, L.join l l')} + | _ -> + (* To match the paper more closely, one would have to join in the non-definite case too *) + (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) + st ) let thread_return ask getg sideg tid (st: BaseComponents (D).t) = diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml index 1e679a4707..acc53d9dee 100644 --- a/src/analyses/threadAnalysis.ml +++ b/src/analyses/threadAnalysis.ml @@ -54,15 +54,16 @@ struct | ThreadJoin { thread = id; ret_var } -> (* TODO: generalize ThreadJoin like ThreadCreate *) (let has_clean_exit tid = not (BatTuple.Tuple3.third (ctx.global tid)) in + let tids = ctx.ask (Queries.EvalThread id) in let join_thread s tid = if has_clean_exit tid && not (is_not_unique ctx tid) then D.remove tid s else s in - match TS.elements (ctx.ask (Queries.EvalThread id)) with - | threads -> List.fold_left join_thread ctx.local threads - | exception SetDomain.Unsupported _ -> ctx.local) + if TS.is_top tids + then ctx.local + else List.fold_left join_thread ctx.local (TS.elements tids)) | _ -> ctx.local let query ctx (type a) (q: a Queries.t): a Queries.result = diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml index f2cd36619f..2977ed9082 100644 --- a/src/analyses/threadJoins.ml +++ b/src/analyses/threadJoins.ml @@ -52,7 +52,7 @@ struct if TIDs.is_top threads then ctx.local else ( - (* elements throws if the thread set is top *) + (* all elements are known *) let threads = TIDs.elements threads in match threads with | [tid] when TID.is_unique tid-> @@ -70,7 +70,7 @@ struct (MustTIDs.bot(), true) (* consider everything joined, MustTIDs is reversed so bot is All threads *) ) else ( - (* elements throws if the thread set is top *) + (* all elements are known *) let threads = TIDs.elements threads in if List.compare_length_with threads 1 > 0 then M.info ~category:Unsound "Ambiguous thread ID assume-joined, assuming all of those threads must-joined.";