From fd105802db6bf2a695042912cec58f0038083bed Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Fri, 8 Sep 2017 15:22:07 -0700 Subject: [PATCH] [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 | 2 +- infer/src/bufferoverrun/bufferOverrunChecker.ml | 6 +++--- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 6 +++--- infer/src/bufferoverrun/itv.ml | 4 ++-- infer/src/checkers/ThreadSafety.ml | 4 ++-- infer/src/checkers/annotationReachability.ml | 4 ++-- 6 files changed, 13 insertions(+), 13 deletions(-) diff --git a/infer/src/absint/Scheduler.ml b/infer/src/absint/Scheduler.ml index baa3aa4bf..12b3dc7fc 100644 --- a/infer/src/absint/Scheduler.ml +++ b/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 diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index c99d2a9f7..64482afe5 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/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. *) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index 0efc7a649..af71646f2 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/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 diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 191825c37..5a03da61b 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/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 diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index df853de46..9e6e92fec 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/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 ) diff --git a/infer/src/checkers/annotationReachability.ml b/infer/src/checkers/annotationReachability.ml index e4dda1518..6936fd263 100644 --- a/infer/src/checkers/annotationReachability.ml +++ b/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