[thread-safety] don't use Map.choose or Set.choose

Summary:
Read the documentation and it doesn't seem like these functions are guaranteed to choose the same value in different runs.
I hypothesize that these may be the source of flakiness in the thread-safety tests/smoke tests.

Reviewed By: jvillard

Differential Revision: D5794384

fbshipit-source-id: 02b7a96

infer/src/absint/Scheduler.ml

@@ -94,7 +94,7 @@ module ReversePostorder (CFG : ProcCfg.S) = struct
      quick popping, and do a linear search only when this list is empty *)
   let pop t =
     try
-      let init_id, init_work = M.choose t.worklist in
+      let init_id, init_work = M.min_binding t.worklist in
       let init_priority = WorkUnit.priority init_work in
       let max_priority_id, _ =
         M.fold

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -332,13 +332,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             if Ident.is_none id then mem
             else
               let mem = Dom.Mem.add_stack (Loc.of_var (Var.of_id id)) v mem in
-              if PowLoc.is_singleton locs then Dom.Mem.load_alias id (PowLoc.choose locs) mem
+              if PowLoc.is_singleton locs then Dom.Mem.load_alias id (PowLoc.min_elt locs) mem
               else mem
         | Store (exp1, _, exp2, loc)
          -> let locs = Sem.eval exp1 mem loc |> Dom.Val.get_all_locs in
             let v = Sem.eval exp2 mem loc |> Dom.Val.add_trace_elem (Trace.Assign loc) in
             let mem = Dom.Mem.update_mem locs v mem in
-            if PowLoc.is_singleton locs then Dom.Mem.store_alias (PowLoc.choose locs) exp2 mem
+            if PowLoc.is_singleton locs then Dom.Mem.store_alias (PowLoc.min_elt locs) exp2 mem
             else mem
         | Prune (exp, loc, _, _)
          -> Sem.prune exp loc mem
@@ -483,7 +483,7 @@ module Report = struct
     (* check that we are the last instruction in the current node
      * and that the current node is followed by a unique successor
      * with no instructions.
-     * 
+     *
      * this is our proxy for being the last statement in a procedure.
      * The tests pass, but it's kind of a hack and depends on an internal
      * detail of SIL that could change in the future. *)

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -434,8 +434,8 @@ module Make (CFG : ProcCfg.S) = struct
         match callee_ret_alias with
         | Some ret_loc
          -> if PowLoc.is_singleton v1 && PowLoc.is_singleton v2
-               && Loc.equal (PowLoc.choose v1) ret_loc
-            then ret_alias := Some (PowLoc.choose v2)
+               && Loc.equal (PowLoc.min_elt v1) ret_loc
+            then ret_alias := Some (PowLoc.min_elt v2)
         | None
          -> ()
       in
@@ -488,7 +488,7 @@ module Make (CFG : ProcCfg.S) = struct
         | Itv.Bound.Linear (_, se1) when Itv.SymLinear.is_zero se1
          -> (bound_map, trace_map)
         | Itv.Bound.Linear (0, se1) when Itv.SymLinear.cardinal se1 > 0
-         -> let symbol, coeff = Itv.SymLinear.choose se1 in
+         -> let symbol, coeff = Itv.SymLinear.min_binding se1 in
             if Int.equal coeff 1 then
               (Itv.SubstMap.add symbol actual bound_map, Itv.SubstMap.add symbol traces trace_map)
             else assert false

infer/src/bufferoverrun/itv.ml

@@ -50,7 +50,7 @@ module SymLinear = struct
 
   let cardinal : t -> int = M.cardinal
 
-  let choose : t -> Symbol.t * int = M.choose
+  let min_binding : t -> Symbol.t * int = M.min_binding
 
   let fold : (Symbol.t -> int -> 'b -> 'b) -> t -> 'b -> 'b = M.fold
 
@@ -138,7 +138,7 @@ module SymLinear = struct
     fun x ->
       let x = M.filter (fun _ v -> v <> 0) x in
       if Int.equal (M.cardinal x) 1 then
-        let k, v = M.choose x in
+        let k, v = M.min_binding x in
         if Int.equal v 1 then Some k else None
       else None
 

infer/src/checkers/ThreadSafety.ml

@@ -1228,7 +1228,7 @@ let make_read_write_race_description conflicts tenv pname final_sink_site initia
   in
   let pp_conflicts fmt conflicts =
     if Int.equal (Typ.Procname.Set.cardinal conflicts) 1 then
-      Typ.Procname.pp fmt (Typ.Procname.Set.choose conflicts)
+      Typ.Procname.pp fmt (Typ.Procname.Set.min_elt conflicts)
     else Typ.Procname.Set.pp fmt conflicts
   in
   let conflicts_description =
@@ -1529,7 +1529,7 @@ let quotient_access_map acc_map =
   let rec aux acc m =
     if AccessListMap.is_empty m then acc
     else
-      let k, vals = AccessListMap.choose m in
+      let k, vals = AccessListMap.min_binding m in
       let _, _, _, tenv, _ =
         List.find_exn vals ~f:(fun (elem, _, _, _, _) ->
             ThreadSafetyDomain.Access.equal (ThreadSafetyDomain.TraceElem.kind elem) k )

infer/src/checkers/annotationReachability.ml

@@ -196,7 +196,7 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site si
         AnnotReachabilityDomain.SinkMap.fold
           (fun _ call_sites (unseen, visited as accu) ->
             try
-              let call_site = AnnotReachabilityDomain.CallSites.choose call_sites in
+              let call_site = AnnotReachabilityDomain.CallSites.min_elt call_sites in
               let p = CallSite.pname call_site in
               let loc = CallSite.loc call_site in
               if Typ.Procname.Set.mem p visited then accu
@@ -209,7 +209,7 @@ let report_call_stack summary end_of_stack lookup_next_calls report call_site si
   AnnotReachabilityDomain.SinkMap.iter
     (fun _ call_sites ->
       try
-        let fst_call_site = AnnotReachabilityDomain.CallSites.choose call_sites in
+        let fst_call_site = AnnotReachabilityDomain.CallSites.min_elt call_sites in
         let fst_callee_pname = CallSite.pname fst_call_site in
         let fst_call_loc = CallSite.loc fst_call_site in
         let start_trace = update_trace (CallSite.loc call_site) [] in