Replace exception handling with top checks

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) =

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) =

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 =

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.";