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`]