From 05f14391a64113333d2b2f405614bb97e71e4bdc Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 14 Mar 2019 02:42:32 -0700 Subject: [PATCH] [racerd] replace quandary traces with explicit ones Summary: Context: "quandary" traces optimise for space by only storing a call site (plus analysis element) in a summary, as opposed to a list of call sites plus the element (i.e., a trace). When forming a report, the trace is expanded to a full one by reading the summary of the called function, and then matching up the current element with one from the summary, iterating until the trace cannot be expanded any more. In the best case, this can give a quadratic saving, as a real trace gets longer the higher one goes in the call stack, and therefore the total cost of saving that trace in each summary is quadratic in the length of the trace. Quandary traces give a linear cost. HOWEVER, these have been a source of many subtle bugs. 1. The trace expansion strategy is very arbitrary and cannot distinguish between expanded traces that are invalid (i.e., end with a call and not an originating point, such as a field access in RacerD). Plus the strategy does not explore all expansions, just the left-most one, meaning the left most may be invalid in the above sense, but another (not left-most) isn't even though it's not discovered by the expansion. This is fixable with major surgery. 2. All real traces that lead to the same endpoint are conflated -- this is to save space because there may be exponentially many such traces. That's OK, but these traces may have different locking contexts -- one may take the lock along the way, and another may not. The expansion cannot make sure that if we are reporting a trace we have recorded as taking the lock, will actually do so. This has resulted in very confusing race reports that are superficially false positives (even though they point to the existence of a real race). 3. Expansion completely breaks down in the java/buck integration when the trace goes through f -> g -> h and f,g,h are all in distinct buck targets F,G,H and F does not depend directly on H. In that case, the summary of h is simply not available when reporting/expanding in f, so the expanded trace comes out as truncated and invalid. These are filtered out, but the filtering is buggy and kills real races too. This diff completely replaces quandary traces in RacerD with plain explicit traces. - This will incur the quadratic space/time cost previously saved. See test plan: there is indeed a 30% increase in summary size, but there is no slowdown. In fact, on openssl there is a 10-20% perf increase. - For each endpoint, up to a single trace is used, as before, so no exponential explosion. However, because there is no such thing as expansion, we cannot get it wrong and change the locking context of a trace. - This diff is emulating the previous reporting format as much as possible to allow good signal from the CI. Further diffs up this stack will remove quandary-trace specific things, and simplify further the code. - 2 is not fully addressed -- it will require pushing the `AccessSnapshot` structure inside `TraceElem`. Further diffs. Reviewed By: jberdine Differential Revision: D14405600 fbshipit-source-id: d239117aa --- infer/src/checkers/classLoadsDomain.ml | 2 + infer/src/concurrency/ExplicitTrace.ml | 21 +- infer/src/concurrency/ExplicitTrace.mli | 6 + infer/src/concurrency/RacerD.ml | 373 +++++++++--------- infer/src/concurrency/RacerDDomain.ml | 121 +++--- infer/src/concurrency/RacerDDomain.mli | 19 +- infer/src/concurrency/starvationDomain.ml | 9 + .../build_systems/racerd_dedup/issues.exp | 2 +- 8 files changed, 274 insertions(+), 279 deletions(-) diff --git a/infer/src/checkers/classLoadsDomain.ml b/infer/src/checkers/classLoadsDomain.ml index 6aeff6404..85608f930 100644 --- a/infer/src/checkers/classLoadsDomain.ml +++ b/infer/src/checkers/classLoadsDomain.ml @@ -12,6 +12,8 @@ module ClassLoad = struct include String let pp_human = pp + + let pp_call = ExplicitTrace.default_pp_call end module Event = ExplicitTrace.MakeTraceElemModuloLocation (ClassLoad) diff --git a/infer/src/concurrency/ExplicitTrace.ml b/infer/src/concurrency/ExplicitTrace.ml index a3ddc5ff6..a4f075950 100644 --- a/infer/src/concurrency/ExplicitTrace.ml +++ b/infer/src/concurrency/ExplicitTrace.ml @@ -8,6 +8,10 @@ open! IStd module F = Format module MF = MarkupFormatter +let default_pp_call fmt callsite = + F.fprintf fmt "Method call: %a" (MF.wrap_monospaced Typ.Procname.pp) (CallSite.pname callsite) + + module type FiniteSet = sig include AbstractDomain.FiniteSetS @@ -18,6 +22,8 @@ module type Element = sig include PrettyPrintable.PrintableOrderedType val pp_human : Format.formatter -> t -> unit + + val pp_call : Format.formatter -> CallSite.t -> unit end type 'a comparator = 'a -> Location.t -> 'a -> Location.t -> int @@ -37,6 +43,8 @@ module type TraceElem = sig val make : elem_t -> Location.t -> t + val map : f:(elem_t -> elem_t) -> t -> t + val get_loc : t -> Location.t val make_loc_trace : ?nesting:int -> t -> Errlog.loc_trace @@ -58,22 +66,25 @@ module MakeTraceElemWithComparator (Elem : Element) (Comp : Comparator with type let pp fmt {elem} = Elem.pp fmt elem let pp_human fmt {elem} = Elem.pp_human fmt elem + + let pp_call = Elem.pp_call end include T let make elem loc = {elem; loc; trace= []} + let map ~f (trace_elem : t) = + let elem' = f trace_elem.elem in + if phys_equal trace_elem.elem elem' then trace_elem else {trace_elem with elem= elem'} + + let get_loc {loc; trace} = match trace with [] -> loc | hd :: _ -> CallSite.loc hd let make_loc_trace ?(nesting = 0) e = let call_trace, nesting = List.fold e.trace ~init:([], nesting) ~f:(fun (tr, ns) callsite -> - let descr = - F.asprintf "Method call: %a" - (MF.wrap_monospaced Typ.Procname.pp) - (CallSite.pname callsite) - in + let descr = F.asprintf "%a" pp_call callsite in let call = Errlog.make_trace_element ns (CallSite.loc callsite) descr [] in (call :: tr, ns + 1) ) in diff --git a/infer/src/concurrency/ExplicitTrace.mli b/infer/src/concurrency/ExplicitTrace.mli index e8d8edff2..ee68e2655 100644 --- a/infer/src/concurrency/ExplicitTrace.mli +++ b/infer/src/concurrency/ExplicitTrace.mli @@ -7,6 +7,8 @@ open! IStd +val default_pp_call : Format.formatter -> CallSite.t -> unit + (** A powerset domain of traces, with bottom = empty and join = union *) module type FiniteSet = sig include AbstractDomain.FiniteSetS @@ -20,6 +22,8 @@ module type Element = sig val pp_human : Format.formatter -> t -> unit (** Pretty printer used for trace construction; [pp] is used for debug output. *) + + val pp_call : Format.formatter -> CallSite.t -> unit end module type TraceElem = sig @@ -33,6 +37,8 @@ module type TraceElem = sig val make : elem_t -> Location.t -> t + val map : f:(elem_t -> elem_t) -> t -> t + val get_loc : t -> Location.t (** Starting location of the trace: this is either [loc] if [trace==[]], or the head of [trace]. *) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 8b36b9fa7..a412390a0 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -58,53 +58,45 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_field_accesses (base, []) acc accesses ) - let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc - (astate : Domain.t) = - (* create a dummy write that represents mutating the contents of the container *) + let make_container_access ret_base callee_pname ~is_write receiver_ap callee_loc tenv + caller_pdesc (astate : Domain.t) = let open Domain in - let callee_accesses = - if RacerDModels.is_synchronized_container callee_pname receiver_ap tenv then - AccessDomain.empty + let callee_access = + if RacerDModels.is_synchronized_container callee_pname receiver_ap tenv then None else let container_access = TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc in - let snapshot = - AccessSnapshot.make container_access astate.locks astate.threads - (AccessSnapshot.OwnershipPrecondition.Conjunction (IntSet.singleton 0)) - caller_pdesc - in - AccessDomain.add_opt snapshot AccessDomain.empty + let ownership_pre = OwnershipDomain.get_precondition receiver_ap astate.ownership in + AccessSnapshot.make container_access astate.locks astate.threads ownership_pre caller_pdesc in (* if a container c is owned in cpp, make c[i] owned for all i *) - let return_ownership = + let ownership_value = match callee_pname with | Typ.Procname.ObjC_Cpp _ | C _ -> OwnershipAbstractValue.make_owned_if 0 | _ -> OwnershipAbstractValue.unowned in - Some {empty_summary with accesses= callee_accesses; return_ownership} + let ownership = OwnershipDomain.add (ret_base, []) ownership_value astate.ownership in + let accesses = AccessDomain.add_opt callee_access astate.accesses in + Some {astate with accesses; ownership} - let get_summary caller_pdesc callee_pname actuals callee_loc tenv (astate : Domain.t) = + let do_container_access ret_base callee_pname actuals loc {ProcData.tenv; pdesc} astate = let open RacerDModels in - match get_container_access callee_pname tenv with - | None -> - Payload.read caller_pdesc callee_pname - | Some container_access -> ( - match List.hd actuals with - | Some (HilExp.AccessExpression receiver_expr) -> - let receiver_ap = HilExp.AccessExpression.to_access_path receiver_expr in - let is_write = - match container_access with ContainerWrite -> true | ContainerRead -> false - in - make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc - astate - | _ -> - L.internal_error "Call to %a is marked as a container write, but has no receiver" - Typ.Procname.pp callee_pname ; - None ) + Option.bind (get_container_access callee_pname tenv) ~f:(fun container_access -> + match List.hd actuals with + | Some (HilExp.AccessExpression receiver_expr) -> + let receiver_ap = HilExp.AccessExpression.to_access_path receiver_expr in + let is_write = + match container_access with ContainerWrite -> true | ContainerRead -> false + in + make_container_access ret_base callee_pname ~is_write receiver_ap loc tenv pdesc astate + | _ -> + L.internal_error "Call to %a is marked as a container write, but has no receiver" + Typ.Procname.pp callee_pname ; + None ) let add_reads exps loc accesses locks threads ownership proc_data = @@ -258,10 +250,124 @@ module TransferFunctions (CFG : ProcCfg.S) = struct else astate - let exec_instr (astate : Domain.t) ({ProcData.tenv; pdesc} as proc_data) _ (instr : HilInstr.t) = + let do_call ret_base callee_pname actuals call_flags loc ({ProcData.tenv; pdesc} as proc_data) + (astate : Domain.t) = let open Domain in let open RacerDModels in let open ConcurrencyModels in + let ret_access_path = (ret_base, []) in + let astate = + if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then + Domain.add_unannotated_call_access callee_pname loc pdesc astate + else astate + in + let accesses_with_unannotated_calls = astate.accesses in + let accesses = + add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads + astate.ownership proc_data + in + let astate = {astate with accesses} in + let astate = + match get_thread callee_pname with + | BackgroundThread -> + {astate with threads= ThreadsDomain.AnyThread} + | MainThread -> + {astate with threads= ThreadsDomain.AnyThreadButSelf} + | MainThreadIfTrue -> + let attribute_map = + AttributeMapDomain.add_attribute ret_access_path (Choice Choice.OnMainThread) + astate.attribute_map + in + {astate with attribute_map} + | UnknownThread -> + astate + in + let astate_callee = + (* assuming that modeled procedures do not have useful summaries *) + if is_thread_utils_method "assertMainThread" callee_pname then + {astate with threads= ThreadsDomain.AnyThreadButSelf} + else + (* if we don't have any evidence about whether the current function can run in parallel + with other threads or not, start assuming that it can. why use a lock if the function + can't run in a multithreaded context? *) + let update_for_lock_use = function + | ThreadsDomain.AnyThreadButSelf -> + ThreadsDomain.AnyThreadButSelf + | _ -> + ThreadsDomain.AnyThread + in + match get_lock_effect callee_pname actuals with + | Lock _ | GuardLock _ | GuardConstruct {acquire_now= true} -> + { astate with + locks= LocksDomain.acquire_lock astate.locks + ; threads= update_for_lock_use astate.threads } + | Unlock _ | GuardDestroy _ | GuardUnlock _ -> + { astate with + locks= LocksDomain.release_lock astate.locks + ; threads= update_for_lock_use astate.threads } + | LockedIfTrue _ | GuardLockedIfTrue _ -> + let attribute_map = + AttributeMapDomain.add_attribute ret_access_path (Choice Choice.LockHeld) + astate.attribute_map + in + {astate with attribute_map; threads= update_for_lock_use astate.threads} + | GuardConstruct {acquire_now= false} -> + astate + | NoEffect -> ( + let summary_opt = Payload.read pdesc callee_pname in + let callee_pdesc = Ondemand.get_proc_desc callee_pname in + match + Option.map summary_opt ~f:(fun summary -> + let rebased_accesses = + Option.value_map callee_pdesc ~default:summary.accesses + ~f:(expand_actuals actuals summary.accesses) + in + {summary with accesses= rebased_accesses} ) + with + | Some {threads; locks; accesses; return_ownership; return_attributes} -> + let locks = + LocksDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks + in + let accesses = + add_callee_accesses astate accesses locks threads actuals callee_pname pdesc loc + in + let ownership = + OwnershipDomain.propagate_return ret_access_path return_ownership actuals + astate.ownership + in + let attribute_map = + AttributeMapDomain.add ret_access_path return_attributes astate.attribute_map + in + let threads = + ThreadsDomain.integrate_summary ~caller_astate:astate.threads + ~callee_astate:threads + in + {locks; threads; accesses; ownership; attribute_map} + | None -> + call_without_summary callee_pname ret_access_path call_flags actuals astate ) + in + let add_if_annotated predicate attribute attribute_map = + if PatternMatch.override_exists predicate tenv callee_pname then + AttributeMapDomain.add_attribute ret_access_path attribute attribute_map + else attribute_map + in + let attribute_map = add_if_annotated is_functional Functional astate_callee.attribute_map in + let ownership = + if + PatternMatch.override_exists + (has_return_annot Annotations.ia_is_returns_ownership) + tenv callee_pname + then OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned astate_callee.ownership + else astate_callee.ownership + in + {astate_callee with ownership; attribute_map} + + + let if_none_then = IOption.value_default_f + + let exec_instr (astate : Domain.t) ({ProcData.tenv; pdesc} as proc_data) _ (instr : HilInstr.t) = + let open Domain in + let open RacerDModels in match instr with | Call (ret_base, Direct procname, actuals, _, loc) when acquires_ownership procname tenv -> let ret_access_path = (ret_base, []) in @@ -274,118 +380,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in {astate with accesses; ownership} | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) -> - let ret_access_path = (ret_base, []) in - let astate = - if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then - Domain.add_unannotated_call_access callee_pname loc pdesc astate - else astate - in - let accesses_with_unannotated_calls = astate.accesses in - let accesses = - add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads - astate.ownership proc_data - in - let astate = {astate with accesses} in - let astate = - match get_thread callee_pname with - | BackgroundThread -> - {astate with threads= ThreadsDomain.AnyThread} - | MainThread -> - {astate with threads= ThreadsDomain.AnyThreadButSelf} - | MainThreadIfTrue -> - let attribute_map = - AttributeMapDomain.add_attribute ret_access_path (Choice Choice.OnMainThread) - astate.attribute_map - in - {astate with attribute_map} - | UnknownThread -> - astate - in - let astate_callee = - (* assuming that modeled procedures do not have useful summaries *) - if is_thread_utils_method "assertMainThread" callee_pname then - {astate with threads= ThreadsDomain.AnyThreadButSelf} - else - (* if we don't have any evidence about whether the current function can run in parallel - with other threads or not, start assuming that it can. why use a lock if the function - can't run in a multithreaded context? *) - let update_for_lock_use = function - | ThreadsDomain.AnyThreadButSelf -> - ThreadsDomain.AnyThreadButSelf - | _ -> - ThreadsDomain.AnyThread - in - match get_lock_effect callee_pname actuals with - | Lock _ | GuardLock _ | GuardConstruct {acquire_now= true} -> - { astate with - locks= LocksDomain.acquire_lock astate.locks - ; threads= update_for_lock_use astate.threads } - | Unlock _ | GuardDestroy _ | GuardUnlock _ -> - { astate with - locks= LocksDomain.release_lock astate.locks - ; threads= update_for_lock_use astate.threads } - | LockedIfTrue _ | GuardLockedIfTrue _ -> - let attribute_map = - AttributeMapDomain.add_attribute ret_access_path (Choice Choice.LockHeld) - astate.attribute_map - in - {astate with attribute_map; threads= update_for_lock_use astate.threads} - | GuardConstruct {acquire_now= false} -> - astate - | NoEffect -> ( - let summary_opt = get_summary pdesc callee_pname actuals loc tenv astate in - let callee_pdesc = Ondemand.get_proc_desc callee_pname in - match - Option.map summary_opt ~f:(fun summary -> - let rebased_accesses = - Option.value_map callee_pdesc ~default:summary.accesses - ~f:(expand_actuals actuals summary.accesses) - in - {summary with accesses= rebased_accesses} ) - with - | Some {threads; locks; accesses; return_ownership; return_attributes} -> - let locks = - LocksDomain.integrate_summary ~caller_astate:astate.locks - ~callee_astate:locks - in - let accesses = - add_callee_accesses astate accesses locks threads actuals callee_pname pdesc - loc - in - let ownership = - OwnershipDomain.propagate_return ret_access_path return_ownership actuals - astate.ownership - in - let attribute_map = - AttributeMapDomain.add ret_access_path return_attributes astate.attribute_map - in - let threads = - ThreadsDomain.integrate_summary ~caller_astate:astate.threads - ~callee_astate:threads - in - {locks; threads; accesses; ownership; attribute_map} - | None -> - call_without_summary callee_pname ret_access_path call_flags actuals astate ) - in - let add_if_annotated predicate attribute attribute_map = - if PatternMatch.override_exists predicate tenv callee_pname then - AttributeMapDomain.add_attribute ret_access_path attribute attribute_map - else attribute_map - in - let attribute_map = - add_if_annotated is_functional Functional astate_callee.attribute_map - in - let ownership = - if - PatternMatch.override_exists - (has_return_annot Annotations.ia_is_returns_ownership) - tenv callee_pname - then - OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned - astate_callee.ownership - else astate_callee.ownership - in - {astate_callee with ownership; attribute_map} + do_container_access ret_base callee_pname actuals loc proc_data astate + |> if_none_then ~f:(fun () -> + do_call ret_base callee_pname actuals call_flags loc proc_data astate ) | Assign (lhs_access_expr, rhs_exp, loc) -> let lhs_access_path = HilExp.AccessExpression.to_access_path lhs_access_expr in let rhs_accesses = @@ -687,8 +684,8 @@ let pp_container_access fmt (access_path, access_pname) = (MF.monospaced_to_string (Typ.Procname.get_method access_pname)) -let pp_access fmt sink = - match RacerDDomain.PathDomain.Sink.kind sink with +let pp_access fmt (t : RacerDDomain.TraceElem.t) = + match t.elem with | Read {path} | Write {path} -> (MF.wrap_monospaced AccessPath.pp) fmt path | ContainerRead {path; pname} | ContainerWrite {path; pname} -> @@ -697,9 +694,9 @@ let pp_access fmt sink = RacerDDomain.Access.pp fmt access -let desc_of_sink sink = - let sink_pname = CallSite.pname (RacerDDomain.PathDomain.Sink.call_site sink) in - match RacerDDomain.PathDomain.Sink.kind sink with +(* let desc_of_sink sink = + let sink_pname = CallSite.pname (RacerDDomain.TraceElem.call_site sink) in + match RacerDDomain.TraceElem.kind sink with | Read _ | Write _ -> if Typ.Procname.equal sink_pname Typ.Procname.empty_block then F.asprintf "access to %a" pp_access sink @@ -715,41 +712,31 @@ let desc_of_sink sink = | InterfaceCall _ as access -> if Typ.Procname.equal sink_pname Typ.Procname.empty_block then F.asprintf "%a" RacerDDomain.Access.pp access - else F.asprintf "call to %a" Typ.Procname.pp sink_pname - + else F.asprintf "call to %a" Typ.Procname.pp sink_pname *) -let trace_of_pname orig_sink orig_pdesc callee_pname = +(* let trace_of_pname orig_sink orig_pdesc callee_pname = let open RacerDDomain in - let orig_access = PathDomain.Sink.kind orig_sink in + let orig_access = TraceElem.kind orig_sink in match Payload.read orig_pdesc callee_pname with | Some {accesses} -> AccessDomain.fold (fun snapshot acc -> - if Access.matches ~caller:orig_access ~callee:(PathDomain.Sink.kind snapshot.access) then + if Access.matches ~caller:orig_access ~callee:(TraceElem.kind snapshot.access) then PathDomain.add_sink snapshot.access acc else acc ) accesses PathDomain.bottom | _ -> - PathDomain.bottom + PathDomain.bottom *) - -let make_trace ~report_kind original_path pdesc = +let make_trace ~report_kind original_path = let open RacerDDomain in - let loc_trace_of_path path = PathDomain.to_sink_loc_trace ~desc_of_sink path in - let make_trace_for_sink sink = - let trace_of_pname = trace_of_pname sink pdesc in - match PathDomain.get_reportable_sink_path sink ~trace_of_pname with - | Some path -> - loc_trace_of_path path - | None -> - [] - in + let loc_trace_of_path path = TraceElem.make_loc_trace path in let original_trace = loc_trace_of_path original_path in let get_end_loc trace = Option.map (List.last trace) ~f:(function {Errlog.lt_loc} -> lt_loc) in let original_end = get_end_loc original_trace in let make_with_conflicts conflict_sink original_trace ~label1 ~label2 = (* create a trace for one of the conflicts and append it to the trace for the original sink *) - let conflict_trace = make_trace_for_sink conflict_sink in + let conflict_trace = loc_trace_of_path conflict_sink in let conflict_end = get_end_loc conflict_trace in ( Errlog.concat_traces [(label1, original_trace); (label2, conflict_trace)] , original_end @@ -771,31 +758,23 @@ let log_issue current_pname ~loc ~ltr ~access issue_type error_message = error_message -let report_thread_safety_violation tenv pdesc ~make_description ~report_kind access thread = +let report_thread_safety_violation tenv pdesc ~make_description ~report_kind + (access : RacerDDomain.TraceElem.t) thread = let open RacerDDomain in let pname = Procdesc.get_proc_name pdesc in - let report_one_path ((_, sinks) as path) = - let final_sink, _ = List.hd_exn sinks in - let initial_sink, _ = List.last_exn sinks in - let is_full_trace = TraceElem.is_direct final_sink in - (* Traces can be truncated due to limitations of our Buck integration. If we have a truncated - trace, it's probably going to be too confusing to be actionable. Skip it. *) - if (not Config.filtering) || (not (Typ.Procname.is_java pname)) || is_full_trace then - let final_sink_site = PathDomain.Sink.call_site final_sink in - let initial_sink_site = PathDomain.Sink.call_site initial_sink in - let loc = CallSite.loc initial_sink_site in - let ltr, original_end, conflict_end = make_trace ~report_kind path pdesc in - (* what the potential bug is *) - let description = make_description pname final_sink_site initial_sink_site initial_sink in - (* why we are reporting it *) - let issue_type, explanation = get_reporting_explanation report_kind tenv pname thread in - let error_message = F.sprintf "%s%s" description explanation in - let end_locs = Option.to_list original_end @ Option.to_list conflict_end in - let access = IssueAuxData.encode end_locs in - log_issue pname ~loc ~ltr ~access issue_type error_message - in - let trace_of_pname = trace_of_pname access pdesc in - Option.iter ~f:report_one_path (PathDomain.get_reportable_sink_path access ~trace_of_pname) + let final_pname = List.last access.trace |> Option.value_map ~default:pname ~f:CallSite.pname in + let final_sink_site = CallSite.make final_pname access.loc in + let initial_sink_site = CallSite.make pname (TraceElem.get_loc access) in + let loc = CallSite.loc initial_sink_site in + let ltr, original_end, conflict_end = make_trace ~report_kind access in + (* what the potential bug is *) + let description = make_description pname final_sink_site initial_sink_site access in + (* why we are reporting it *) + let issue_type, explanation = get_reporting_explanation report_kind tenv pname thread in + let error_message = F.sprintf "%s%s" description explanation in + let end_locs = Option.to_list original_end @ Option.to_list conflict_end in + let access = IssueAuxData.encode end_locs in + log_issue pname ~loc ~ltr ~access issue_type error_message let report_unannotated_interface_violation tenv pdesc access thread reported_pname = @@ -930,7 +909,7 @@ end = struct let empty = M.empty let add (rep : reported_access) map = - let access = RacerDDomain.TraceElem.kind rep.snapshot.access in + let access = rep.snapshot.access.elem in if RacerDDomain.Access.get_access_path access |> should_filter_access then map else let k = Key.of_access access in @@ -1004,10 +983,11 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) = let open RacerDModels in let is_duplicate_report access pname {reported_sites; reported_writes; reported_reads; reported_unannotated_calls} = + let call_site = CallSite.make pname (TraceElem.get_loc access) in if Config.filtering then - CallSite.Set.mem (TraceElem.call_site access) reported_sites + CallSite.Set.mem call_site reported_sites || - match TraceElem.kind access with + match access.TraceElem.elem with | Access.Write _ | Access.ContainerWrite _ -> Typ.Procname.Set.mem pname reported_writes | Access.Read _ | Access.ContainerRead _ -> @@ -1018,8 +998,9 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) = in let update_reported access pname reported = if Config.filtering then - let reported_sites = CallSite.Set.add (TraceElem.call_site access) reported.reported_sites in - match TraceElem.kind access with + let call_site = CallSite.make pname (TraceElem.get_loc access) in + let reported_sites = CallSite.Set.add call_site reported.reported_sites in + match access.TraceElem.elem with | Access.Write _ | Access.ContainerWrite _ -> let reported_writes = Typ.Procname.Set.add pname reported.reported_writes in {reported with reported_writes; reported_sites} @@ -1037,7 +1018,7 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) = let pname = Procdesc.get_proc_name procdesc in if is_duplicate_report snapshot.access pname reported_acc then reported_acc else - match TraceElem.kind snapshot.access with + match snapshot.access.elem with | Access.InterfaceCall unannoted_call_pname when AccessSnapshot.is_unprotected snapshot && ThreadsDomain.is_any threads diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 93f91c73c..eecc03688 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -7,6 +7,7 @@ open! IStd module F = Format +module MF = MarkupFormatter (** Master function for deciding whether RacerD should completely ignore a variable as the root of an access path. Currently fires on *static locals* and any variable which does not @@ -21,27 +22,19 @@ let should_skip_var v = module Access = struct type t = - | Read of {path: AccessPath.t; original: AccessPath.t} - | Write of {path: AccessPath.t; original: AccessPath.t} - | ContainerRead of {path: AccessPath.t; original: AccessPath.t; pname: Typ.Procname.t} - | ContainerWrite of {path: AccessPath.t; original: AccessPath.t; pname: Typ.Procname.t} + | Read of {path: AccessPath.t; original: AccessPath.t [@compare.ignore]} + | Write of {path: AccessPath.t; original: AccessPath.t [@compare.ignore]} + | ContainerRead of + { path: AccessPath.t + ; original: AccessPath.t [@compare.ignore] + ; pname: Typ.Procname.t } + | ContainerWrite of + { path: AccessPath.t + ; original: AccessPath.t [@compare.ignore] + ; pname: Typ.Procname.t } | InterfaceCall of Typ.Procname.t [@@deriving compare] - let matches ~caller ~callee = - match (caller, callee) with - | Read {original= ap1}, Read {original= ap2} | Write {original= ap1}, Write {original= ap2} -> - AccessPath.equal ap1 ap2 - | ContainerRead {original= ap1; pname= pname1}, ContainerRead {original= ap2; pname= pname2} - | ContainerWrite {original= ap1; pname= pname1}, ContainerWrite {original= ap2; pname= pname2} - -> - Typ.Procname.equal pname1 pname2 && AccessPath.equal ap1 ap2 - | InterfaceCall pname1, InterfaceCall pname2 -> - Typ.Procname.equal pname1 pname2 - | _ -> - false - - let make_field_access path ~is_write = if is_write then Write {path; original= path} else Read {path; original= path} @@ -101,65 +94,52 @@ module Access = struct F.fprintf fmt "Write to container %a via %a" AccessPath.pp path Typ.Procname.pp pname | InterfaceCall pname -> F.fprintf fmt "Call to un-annotated interface method %a" Typ.Procname.pp pname -end - -module TraceElem = struct - module Kind = Access - - type t = {site: CallSite.t; kind: Kind.t} [@@deriving compare] - - let is_write {kind} = Access.is_write kind - - let is_container_write {kind} = Access.is_container_write kind - - let call_site {site} = site - - let kind {kind} = kind - let make ?indexes:_ kind site = {kind; site} - - let with_callsite t site = {t with site} - - let pp fmt {site; kind} = F.fprintf fmt "%a at %a" Access.pp kind CallSite.pp site - - let map ~f ({kind} as elem) = - let kind' = Access.map ~f kind in - if phys_equal kind kind' then elem else {elem with kind= kind'} + (* FIXME: changed to make tests pass *) + let pp_human fmt = function + | Read {original} -> + F.fprintf fmt "access to `%a`" AccessPath.pp original + | Write {original} -> + F.fprintf fmt "access to `%a`" AccessPath.pp original + | ContainerRead {original; pname} -> + F.fprintf fmt "Read of container %a via call to %s" + (MF.wrap_monospaced AccessPath.pp) + original + (MF.monospaced_to_string (Typ.Procname.get_method pname)) + | ContainerWrite {original; pname} -> + F.fprintf fmt "Write to container %a via call to %s" + (MF.wrap_monospaced AccessPath.pp) + original + (MF.monospaced_to_string (Typ.Procname.get_method pname)) + | InterfaceCall pname -> + F.fprintf fmt "Call to un-annotated interface method %a" Typ.Procname.pp pname - module Set = PrettyPrintable.MakePPSet (struct - type nonrec t = t - let compare = compare + let pp_call fmt cs = F.fprintf fmt "call to %a" Typ.Procname.pp (CallSite.pname cs) +end - let pp = pp - end) +module TraceElem = struct + (* FIXME evaluate modulo location functor *) + include ExplicitTrace.MakeTraceElem (Access) - let dummy_pname = Typ.Procname.empty_block + let is_write {elem} = Access.is_write elem - let make_dummy_site loc = CallSite.make dummy_pname loc + let is_container_write {elem} = Access.is_container_write elem - (* all trace elems are created with a dummy call site. any trace elem without a dummy call site - represents a call that leads to an access rather than a direct access *) - let is_direct {site} = Typ.Procname.equal (CallSite.pname site) dummy_pname + let map ~f trace_elem = map ~f:(Access.map ~f) trace_elem let make_container_access access_path pname ~is_write loc = - let site = make_dummy_site loc in - make (Access.make_container_access access_path pname ~is_write) site + make (Access.make_container_access access_path pname ~is_write) loc let make_field_access access_path ~is_write loc = - let site = make_dummy_site loc in - make (Access.make_field_access access_path ~is_write) site + make (Access.make_field_access access_path ~is_write) loc - let make_unannotated_call_access pname loc = - let site = make_dummy_site loc in - make (Access.InterfaceCall pname) site + let make_unannotated_call_access pname loc = make (Access.InterfaceCall pname) loc end -module PathDomain = SinkTrace.Make (TraceElem) - module LockCount = AbstractDomain.CountDomain (struct let max = 5 @@ -282,7 +262,7 @@ module AccessSnapshot = struct end type t = - { access: PathDomain.Sink.t + { access: TraceElem.t ; thread: ThreadsDomain.t ; lock: bool ; ownership_precondition: OwnershipPrecondition.t } @@ -310,16 +290,17 @@ module AccessSnapshot = struct let pp fmt {access; thread; lock; ownership_precondition} = - F.fprintf fmt "Access: %a Thread: %a Lock: %b Pre: %a" TraceElem.pp access ThreadsDomain.pp - thread lock OwnershipPrecondition.pp ownership_precondition + F.fprintf fmt "Loc: %a Access: %a Thread: %a Lock: %b Pre: %a" Location.pp + (TraceElem.get_loc access) TraceElem.pp access ThreadsDomain.pp thread lock + OwnershipPrecondition.pp ownership_precondition end module AccessDomain = struct include AbstractDomain.FiniteSet (AccessSnapshot) - let add ({AccessSnapshot.access= {kind}} as s) astate = + let add ({AccessSnapshot.access= {elem}} as s) astate = let skip = - Access.get_access_path kind |> Option.exists ~f:(fun ((v, _), _) -> should_skip_var v) + Access.get_access_path elem |> Option.exists ~f:(fun ((v, _), _) -> should_skip_var v) in if skip then astate else add s astate @@ -431,6 +412,16 @@ module OwnershipDomain = struct IntSet.fold get_ownership formal_indexes OwnershipAbstractValue.owned in add ret_access_path ret_ownership_wrt_actuals ownership + + + let get_precondition path t = + match get_owned path t with + | OwnedIf formal_indexes -> + (* access path conditionally owned if [formal_indexes] are owned *) + AccessSnapshot.OwnershipPrecondition.Conjunction formal_indexes + | Unowned -> + (* access path not rooted in a formal and not conditionally owned *) + AccessSnapshot.OwnershipPrecondition.False end module Choice = struct diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index 2559b0790..50b33c91d 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -22,13 +22,13 @@ module Access : sig (** Call to method of interface not annotated with @ThreadSafe *) [@@deriving compare] - include TraceElem.Kind with type t := t + include ExplicitTrace.Element with type t := t val get_access_path : t -> AccessPath.t option end module TraceElem : sig - include TraceElem.S with module Kind = Access + include ExplicitTrace.TraceElem with type elem_t = Access.t val is_write : t -> bool @@ -36,18 +36,11 @@ module TraceElem : sig val map : f:(AccessPath.t -> AccessPath.t) -> t -> t - val is_direct : t -> bool - (** return true if the given trace elem represents a direct access, not a call that eventually - leads to an access *) - val make_container_access : AccessPath.t -> Typ.Procname.t -> is_write:bool -> Location.t -> t val make_field_access : AccessPath.t -> is_write:bool -> Location.t -> t end -module PathDomain : - SinkTrace.S with module Source = Source.Dummy and module Sink = SinkTrace.MakeSink(TraceElem) - (** Overapproximation of number of locks that are currently held *) module LocksDomain : sig type t @@ -103,7 +96,7 @@ module AccessSnapshot : sig end type t = private - { access: PathDomain.Sink.t + { access: TraceElem.t ; thread: ThreadsDomain.t ; lock: bool ; ownership_precondition: OwnershipPrecondition.t } @@ -111,14 +104,14 @@ module AccessSnapshot : sig include PrettyPrintable.PrintableOrderedType with type t := t val make : - PathDomain.Sink.t + TraceElem.t -> LocksDomain.t -> ThreadsDomain.t -> OwnershipPrecondition.t -> Procdesc.t -> t option - val make_from_snapshot : PathDomain.Sink.t -> t -> t option + val make_from_snapshot : TraceElem.t -> t -> t option val is_unprotected : t -> bool (** return true if not protected by lock, thread, or ownership *) @@ -159,6 +152,8 @@ module OwnershipDomain : sig val propagate_assignment : AccessPath.t -> HilExp.t -> t -> t val propagate_return : AccessPath.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t + + val get_precondition : AccessPath.t -> t -> AccessSnapshot.OwnershipPrecondition.t end (** attribute attached to a boolean variable specifying what it means when the boolean is true *) diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 59fbfbea3..1ece879c5 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -57,6 +57,8 @@ module Lock = struct F.fprintf fmt "%a%a" (MF.wrap_monospaced pp) lock pp_owner lock + let pp_call = ExplicitTrace.default_pp_call + let pp_locks fmt lock = F.fprintf fmt " locks %a" pp_human lock end @@ -94,6 +96,9 @@ module Event = struct F.pp_print_string fmt msg | StrictModeCall msg -> F.pp_print_string fmt msg + + + let pp_call = ExplicitTrace.default_pp_call end include ExplicitTrace.MakeTraceElem (EventElement) @@ -135,6 +140,8 @@ module Order = struct let pp_human fmt {first} = Lock.pp_locks fmt first + + let pp_call = ExplicitTrace.default_pp_call end include ExplicitTrace.MakeTraceElem (OrderElement) @@ -200,6 +207,8 @@ module UIThreadExplanationDomain = struct include String let pp_human = pp + + let pp_call = ExplicitTrace.default_pp_call end include ExplicitTrace.MakeTraceElem (StringElement) diff --git a/infer/tests/build_systems/racerd_dedup/issues.exp b/infer/tests/build_systems/racerd_dedup/issues.exp index df35509f2..181092728 100644 --- a/infer/tests/build_systems/racerd_dedup/issues.exp +++ b/infer/tests/build_systems/racerd_dedup/issues.exp @@ -1,6 +1,6 @@ DeDup.java, build_systems.threadsafety.DeDup.colocated_read_write():void, 63, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,call to void DeDup.read_and_write(),access to `this.colocated_read`,,access to `this.colocated_read`] DeDup.java, build_systems.threadsafety.DeDup.separate_write_to_colocated_read():void, 68, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.colocated_read`] -DeDup.java, build_systems.threadsafety.DeDup.twoWritesOneInCaller():void, 51, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`] +DeDup.java, build_systems.threadsafety.DeDup.twoWritesOneInCaller():void, 50, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void DeDup.writeToField(),access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.two_fields():void, 20, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void DeDup.foo(),access to `this.fielda`] DeDup.java, build_systems.threadsafety.DeDup.two_reads():void, 38, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.field`,,access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.two_writes():void, 31, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`]