pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[racerd] replace quandary traces with explicit ones

Browse Source 
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
master
Nikos Gorogiannis 6 years ago committed by Facebook Github Bot
parent 9790eb5a78
commit 05f14391a6
8 changed files with 274 additions and 279 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/checkers/classLoadsDomain.ml
Unescape View File

@ -12,6 +12,8 @@ module ClassLoad = struct
include String include String
let pp_human = pp let pp_human = pp
let pp_call = ExplicitTrace.default_pp_call
end end
module Event = ExplicitTrace.MakeTraceElemModuloLocation (ClassLoad) module Event = ExplicitTrace.MakeTraceElemModuloLocation (ClassLoad)

21
infer/src/concurrency/ExplicitTrace.ml
Unescape View File

@ -8,6 +8,10 @@ open! IStd
module F = Format module F = Format
module MF = MarkupFormatter 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 module type FiniteSet = sig
include AbstractDomain.FiniteSetS include AbstractDomain.FiniteSetS
@ -18,6 +22,8 @@ module type Element = sig
include PrettyPrintable.PrintableOrderedType include PrettyPrintable.PrintableOrderedType
val pp_human : Format.formatter -> t -> unit val pp_human : Format.formatter -> t -> unit
val pp_call : Format.formatter -> CallSite.t -> unit
end end
type 'a comparator = 'a -> Location.t -> 'a -> Location.t -> int 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 make : elem_t -> Location.t -> t
val map : f:(elem_t -> elem_t) -> t -> t
val get_loc : t -> Location.t val get_loc : t -> Location.t
val make_loc_trace : ?nesting:int -> t -> Errlog.loc_trace 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 fmt {elem} = Elem.pp fmt elem
let pp_human fmt {elem} = Elem.pp_human fmt elem let pp_human fmt {elem} = Elem.pp_human fmt elem
let pp_call = Elem.pp_call
end end
include T include T
let make elem loc = {elem; loc; trace= []} 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 get_loc {loc; trace} = match trace with [] -> loc | hd :: _ -> CallSite.loc hd
let make_loc_trace ?(nesting = 0) e = let make_loc_trace ?(nesting = 0) e =
let call_trace, nesting = let call_trace, nesting =
List.fold e.trace ~init:([], nesting) ~f:(fun (tr, ns) callsite -> List.fold e.trace ~init:([], nesting) ~f:(fun (tr, ns) callsite ->
let descr = let descr = F.asprintf "%a" pp_call callsite in
F.asprintf "Method call: %a"
(MF.wrap_monospaced Typ.Procname.pp)
(CallSite.pname callsite)
in
let call = Errlog.make_trace_element ns (CallSite.loc callsite) descr [] in let call = Errlog.make_trace_element ns (CallSite.loc callsite) descr [] in
(call :: tr, ns + 1) ) (call :: tr, ns + 1) )
in in

6
infer/src/concurrency/ExplicitTrace.mli
Unescape View File

@ -7,6 +7,8 @@
open! IStd open! IStd
val default_pp_call : Format.formatter -> CallSite.t -> unit
(** A powerset domain of traces, with bottom = empty and join = union *) (** A powerset domain of traces, with bottom = empty and join = union *)
module type FiniteSet = sig module type FiniteSet = sig
include AbstractDomain.FiniteSetS include AbstractDomain.FiniteSetS
@ -20,6 +22,8 @@ module type Element = sig
val pp_human : Format.formatter -> t -> unit val pp_human : Format.formatter -> t -> unit
(** Pretty printer used for trace construction; [pp] is used for debug output. *) (** Pretty printer used for trace construction; [pp] is used for debug output. *)
val pp_call : Format.formatter -> CallSite.t -> unit
end end
module type TraceElem = sig module type TraceElem = sig
@ -33,6 +37,8 @@ module type TraceElem = sig
val make : elem_t -> Location.t -> t val make : elem_t -> Location.t -> t
val map : f:(elem_t -> elem_t) -> t -> t
val get_loc : t -> Location.t val get_loc : t -> Location.t
(** Starting location of the trace: this is either [loc] if [trace==[]], or the head of [trace]. *) (** Starting location of the trace: this is either [loc] if [trace==[]], or the head of [trace]. *)

159
infer/src/concurrency/RacerD.ml
Unescape View File

@ -58,49 +58,41 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
add_field_accesses (base, []) acc accesses ) add_field_accesses (base, []) acc accesses )
let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc let make_container_access ret_base callee_pname ~is_write receiver_ap callee_loc tenv
(astate : Domain.t) = caller_pdesc (astate : Domain.t) =
(* create a dummy write that represents mutating the contents of the container *)
let open Domain in let open Domain in
let callee_accesses = let callee_access =
if RacerDModels.is_synchronized_container callee_pname receiver_ap tenv then if RacerDModels.is_synchronized_container callee_pname receiver_ap tenv then None
AccessDomain.empty
else else
let container_access = let container_access =
TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc
in in
let snapshot = let ownership_pre = OwnershipDomain.get_precondition receiver_ap astate.ownership in
AccessSnapshot.make container_access astate.locks astate.threads AccessSnapshot.make container_access astate.locks astate.threads ownership_pre caller_pdesc
(AccessSnapshot.OwnershipPrecondition.Conjunction (IntSet.singleton 0))
caller_pdesc
in
AccessDomain.add_opt snapshot AccessDomain.empty
in in
(* if a container c is owned in cpp, make c[i] owned for all i *) (* 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 match callee_pname with
| Typ.Procname.ObjC_Cpp _ | C _ -> | Typ.Procname.ObjC_Cpp _ | C _ ->
OwnershipAbstractValue.make_owned_if 0 OwnershipAbstractValue.make_owned_if 0
| _ -> | _ ->
OwnershipAbstractValue.unowned OwnershipAbstractValue.unowned
in 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 let open RacerDModels in
match get_container_access callee_pname tenv with Option.bind (get_container_access callee_pname tenv) ~f:(fun container_access ->
| None ->
Payload.read caller_pdesc callee_pname
| Some container_access -> (
match List.hd actuals with match List.hd actuals with
| Some (HilExp.AccessExpression receiver_expr) -> | Some (HilExp.AccessExpression receiver_expr) ->
let receiver_ap = HilExp.AccessExpression.to_access_path receiver_expr in let receiver_ap = HilExp.AccessExpression.to_access_path receiver_expr in
let is_write = let is_write =
match container_access with ContainerWrite -> true | ContainerRead -> false match container_access with ContainerWrite -> true | ContainerRead -> false
in in
make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc make_container_access ret_base callee_pname ~is_write receiver_ap loc tenv pdesc astate
astate
| _ -> | _ ->
L.internal_error "Call to %a is marked as a container write, but has no receiver" L.internal_error "Call to %a is marked as a container write, but has no receiver"
Typ.Procname.pp callee_pname ; Typ.Procname.pp callee_pname ;
@ -258,22 +250,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
else astate 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 Domain in
let open RacerDModels in let open RacerDModels in
let open ConcurrencyModels in let open ConcurrencyModels in
match instr with
| Call (ret_base, Direct procname, actuals, _, loc) when acquires_ownership procname tenv ->
let ret_access_path = (ret_base, []) in
let accesses =
add_reads actuals loc astate.accesses astate.locks astate.threads astate.ownership
proc_data
in
let ownership =
OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned astate.ownership
in
{astate with accesses; ownership}
| Call (ret_base, Direct callee_pname, actuals, call_flags, loc) ->
let ret_access_path = (ret_base, []) in let ret_access_path = (ret_base, []) in
let astate = let astate =
if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then if RacerDModels.should_flag_interface_call tenv actuals call_flags callee_pname then
@ -333,7 +314,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| GuardConstruct {acquire_now= false} -> | GuardConstruct {acquire_now= false} ->
astate astate
| NoEffect -> ( | NoEffect -> (
let summary_opt = get_summary pdesc callee_pname actuals loc tenv astate in let summary_opt = Payload.read pdesc callee_pname in
let callee_pdesc = Ondemand.get_proc_desc callee_pname in let callee_pdesc = Ondemand.get_proc_desc callee_pname in
match match
Option.map summary_opt ~f:(fun summary -> Option.map summary_opt ~f:(fun summary ->
@ -345,12 +326,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
with with
| Some {threads; locks; accesses; return_ownership; return_attributes} -> | Some {threads; locks; accesses; return_ownership; return_attributes} ->
let locks = let locks =
LocksDomain.integrate_summary ~caller_astate:astate.locks LocksDomain.integrate_summary ~caller_astate:astate.locks ~callee_astate:locks
~callee_astate:locks
in in
let accesses = let accesses =
add_callee_accesses astate accesses locks threads actuals callee_pname pdesc add_callee_accesses astate accesses locks threads actuals callee_pname pdesc loc
loc
in in
let ownership = let ownership =
OwnershipDomain.propagate_return ret_access_path return_ownership actuals OwnershipDomain.propagate_return ret_access_path return_ownership actuals
@ -372,20 +351,38 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
AttributeMapDomain.add_attribute ret_access_path attribute attribute_map AttributeMapDomain.add_attribute ret_access_path attribute attribute_map
else attribute_map else attribute_map
in in
let attribute_map = let attribute_map = add_if_annotated is_functional Functional astate_callee.attribute_map in
add_if_annotated is_functional Functional astate_callee.attribute_map
in
let ownership = let ownership =
if if
PatternMatch.override_exists PatternMatch.override_exists
(has_return_annot Annotations.ia_is_returns_ownership) (has_return_annot Annotations.ia_is_returns_ownership)
tenv callee_pname tenv callee_pname
then then OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned astate_callee.ownership
OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned
astate_callee.ownership
else astate_callee.ownership else astate_callee.ownership
in in
{astate_callee with ownership; attribute_map} {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
let accesses =
add_reads actuals loc astate.accesses astate.locks astate.threads astate.ownership
proc_data
in
let ownership =
OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned astate.ownership
in
{astate with accesses; ownership}
| Call (ret_base, Direct callee_pname, actuals, call_flags, loc) ->
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) -> | Assign (lhs_access_expr, rhs_exp, loc) ->
let lhs_access_path = HilExp.AccessExpression.to_access_path lhs_access_expr in let lhs_access_path = HilExp.AccessExpression.to_access_path lhs_access_expr in
let rhs_accesses = 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)) (MF.monospaced_to_string (Typ.Procname.get_method access_pname))
let pp_access fmt sink = let pp_access fmt (t : RacerDDomain.TraceElem.t) =
match RacerDDomain.PathDomain.Sink.kind sink with match t.elem with
| Read {path} | Write {path} -> | Read {path} | Write {path} ->
(MF.wrap_monospaced AccessPath.pp) fmt path (MF.wrap_monospaced AccessPath.pp) fmt path
| ContainerRead {path; pname} | ContainerWrite {path; pname} -> | ContainerRead {path; pname} | ContainerWrite {path; pname} ->
@ -697,9 +694,9 @@ let pp_access fmt sink =
RacerDDomain.Access.pp fmt access RacerDDomain.Access.pp fmt access
let desc_of_sink sink = (* let desc_of_sink sink =
let sink_pname = CallSite.pname (RacerDDomain.PathDomain.Sink.call_site sink) in let sink_pname = CallSite.pname (RacerDDomain.TraceElem.call_site sink) in
match RacerDDomain.PathDomain.Sink.kind sink with match RacerDDomain.TraceElem.kind sink with
| Read _ | Write _ -> | Read _ | Write _ ->
if Typ.Procname.equal sink_pname Typ.Procname.empty_block then if Typ.Procname.equal sink_pname Typ.Procname.empty_block then
F.asprintf "access to %a" pp_access sink F.asprintf "access to %a" pp_access sink
@ -715,41 +712,31 @@ let desc_of_sink sink =
| InterfaceCall _ as access -> | InterfaceCall _ as access ->
if Typ.Procname.equal sink_pname Typ.Procname.empty_block then if Typ.Procname.equal sink_pname Typ.Procname.empty_block then
F.asprintf "%a" RacerDDomain.Access.pp access 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 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 match Payload.read orig_pdesc callee_pname with
| Some {accesses} -> | Some {accesses} ->
AccessDomain.fold AccessDomain.fold
(fun snapshot acc -> (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 PathDomain.add_sink snapshot.access acc
else acc ) else acc )
accesses PathDomain.bottom 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 open RacerDDomain in
let loc_trace_of_path path = PathDomain.to_sink_loc_trace ~desc_of_sink path in let loc_trace_of_path path = TraceElem.make_loc_trace 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 original_trace = loc_trace_of_path original_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 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 original_end = get_end_loc original_trace in
let make_with_conflicts conflict_sink original_trace ~label1 ~label2 = 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 *) (* 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 let conflict_end = get_end_loc conflict_trace in
( Errlog.concat_traces [(label1, original_trace); (label2, conflict_trace)] ( Errlog.concat_traces [(label1, original_trace); (label2, conflict_trace)]
, original_end , original_end
@ -771,31 +758,23 @@ let log_issue current_pname ~loc ~ltr ~access issue_type error_message =
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 open RacerDDomain in
let pname = Procdesc.get_proc_name pdesc in let pname = Procdesc.get_proc_name pdesc in
let report_one_path ((_, sinks) as path) = let final_pname = List.last access.trace |> Option.value_map ~default:pname ~f:CallSite.pname in
let final_sink, _ = List.hd_exn sinks in let final_sink_site = CallSite.make final_pname access.loc in
let initial_sink, _ = List.last_exn sinks in let initial_sink_site = CallSite.make pname (TraceElem.get_loc access) 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 loc = CallSite.loc initial_sink_site in
let ltr, original_end, conflict_end = make_trace ~report_kind path pdesc in let ltr, original_end, conflict_end = make_trace ~report_kind access in
(* what the potential bug is *) (* what the potential bug is *)
let description = make_description pname final_sink_site initial_sink_site initial_sink in let description = make_description pname final_sink_site initial_sink_site access in
(* why we are reporting it *) (* why we are reporting it *)
let issue_type, explanation = get_reporting_explanation report_kind tenv pname thread in let issue_type, explanation = get_reporting_explanation report_kind tenv pname thread in
let error_message = F.sprintf "%s%s" description explanation 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 end_locs = Option.to_list original_end @ Option.to_list conflict_end in
let access = IssueAuxData.encode end_locs in let access = IssueAuxData.encode end_locs in
log_issue pname ~loc ~ltr ~access issue_type error_message 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 report_unannotated_interface_violation tenv pdesc access thread reported_pname = let report_unannotated_interface_violation tenv pdesc access thread reported_pname =
@ -930,7 +909,7 @@ end = struct
let empty = M.empty let empty = M.empty
let add (rep : reported_access) map = 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 if RacerDDomain.Access.get_access_path access |> should_filter_access then map
else else
let k = Key.of_access access in 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 open RacerDModels in
let is_duplicate_report access pname let is_duplicate_report access pname
{reported_sites; reported_writes; reported_reads; reported_unannotated_calls} = {reported_sites; reported_writes; reported_reads; reported_unannotated_calls} =
let call_site = CallSite.make pname (TraceElem.get_loc access) in
if Config.filtering then 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 _ -> | Access.Write _ | Access.ContainerWrite _ ->
Typ.Procname.Set.mem pname reported_writes Typ.Procname.Set.mem pname reported_writes
| Access.Read _ | Access.ContainerRead _ -> | Access.Read _ | Access.ContainerRead _ ->
@ -1018,8 +998,9 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) =
in in
let update_reported access pname reported = let update_reported access pname reported =
if Config.filtering then if Config.filtering then
let reported_sites = CallSite.Set.add (TraceElem.call_site access) reported.reported_sites in let call_site = CallSite.make pname (TraceElem.get_loc access) in
match TraceElem.kind access with let reported_sites = CallSite.Set.add call_site reported.reported_sites in
match access.TraceElem.elem with
| Access.Write _ | Access.ContainerWrite _ -> | Access.Write _ | Access.ContainerWrite _ ->
let reported_writes = Typ.Procname.Set.add pname reported.reported_writes in let reported_writes = Typ.Procname.Set.add pname reported.reported_writes in
{reported with reported_writes; reported_sites} {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 let pname = Procdesc.get_proc_name procdesc in
if is_duplicate_report snapshot.access pname reported_acc then reported_acc if is_duplicate_report snapshot.access pname reported_acc then reported_acc
else else
match TraceElem.kind snapshot.access with match snapshot.access.elem with
| Access.InterfaceCall unannoted_call_pname | Access.InterfaceCall unannoted_call_pname
when AccessSnapshot.is_unprotected snapshot when AccessSnapshot.is_unprotected snapshot
&& ThreadsDomain.is_any threads && ThreadsDomain.is_any threads

121
infer/src/concurrency/RacerDDomain.ml
Unescape View File

@ -7,6 +7,7 @@
open! IStd open! IStd
module F = Format module F = Format
module MF = MarkupFormatter
(** Master function for deciding whether RacerD should completely ignore a variable as the root (** 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 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 module Access = struct
type t = type t =
| Read of {path: AccessPath.t; original: AccessPath.t} | Read of {path: AccessPath.t; original: AccessPath.t [@compare.ignore]}
| Write of {path: AccessPath.t; original: AccessPath.t} | Write of {path: AccessPath.t; original: AccessPath.t [@compare.ignore]}
| ContainerRead of {path: AccessPath.t; original: AccessPath.t; pname: Typ.Procname.t} | ContainerRead of
| ContainerWrite of {path: AccessPath.t; original: AccessPath.t; pname: Typ.Procname.t} { 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 | InterfaceCall of Typ.Procname.t
[@@deriving compare] [@@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 = let make_field_access path ~is_write =
if is_write then Write {path; original= path} else Read {path; original= path} 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 F.fprintf fmt "Write to container %a via %a" AccessPath.pp path Typ.Procname.pp pname
| InterfaceCall pname -> | InterfaceCall pname ->
F.fprintf fmt "Call to un-annotated interface method %a" Typ.Procname.pp 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 module TraceElem = struct
end) (* 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 let map ~f trace_elem = map ~f:(Access.map ~f) trace_elem
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 make_container_access access_path pname ~is_write loc = 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) loc
make (Access.make_container_access access_path pname ~is_write) site
let make_field_access access_path ~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) loc
make (Access.make_field_access access_path ~is_write) site
let make_unannotated_call_access pname loc = let make_unannotated_call_access pname loc = make (Access.InterfaceCall pname) loc
let site = make_dummy_site loc in
make (Access.InterfaceCall pname) site
end end
module PathDomain = SinkTrace.Make (TraceElem)
module LockCount = AbstractDomain.CountDomain (struct module LockCount = AbstractDomain.CountDomain (struct
let max = 5 let max = 5
@ -282,7 +262,7 @@ module AccessSnapshot = struct
end end
type t = type t =
{ access: PathDomain.Sink.t { access: TraceElem.t
; thread: ThreadsDomain.t ; thread: ThreadsDomain.t
; lock: bool ; lock: bool
; ownership_precondition: OwnershipPrecondition.t } ; ownership_precondition: OwnershipPrecondition.t }
@ -310,16 +290,17 @@ module AccessSnapshot = struct
let pp fmt {access; thread; lock; ownership_precondition} = let pp fmt {access; thread; lock; ownership_precondition} =
F.fprintf fmt "Access: %a Thread: %a Lock: %b Pre: %a" TraceElem.pp access ThreadsDomain.pp F.fprintf fmt "Loc: %a Access: %a Thread: %a Lock: %b Pre: %a" Location.pp
thread lock OwnershipPrecondition.pp ownership_precondition (TraceElem.get_loc access) TraceElem.pp access ThreadsDomain.pp thread lock
OwnershipPrecondition.pp ownership_precondition
end end
module AccessDomain = struct module AccessDomain = struct
include AbstractDomain.FiniteSet (AccessSnapshot) include AbstractDomain.FiniteSet (AccessSnapshot)
let add ({AccessSnapshot.access= {kind}} as s) astate = let add ({AccessSnapshot.access= {elem}} as s) astate =
let skip = 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 in
if skip then astate else add s astate if skip then astate else add s astate
@ -431,6 +412,16 @@ module OwnershipDomain = struct
IntSet.fold get_ownership formal_indexes OwnershipAbstractValue.owned IntSet.fold get_ownership formal_indexes OwnershipAbstractValue.owned
in in
add ret_access_path ret_ownership_wrt_actuals ownership 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 end
module Choice = struct module Choice = struct

19
infer/src/concurrency/RacerDDomain.mli
Unescape View File

@ -22,13 +22,13 @@ module Access : sig
(** Call to method of interface not annotated with @ThreadSafe *) (** Call to method of interface not annotated with @ThreadSafe *)
[@@deriving compare] [@@deriving compare]
include TraceElem.Kind with type t := t include ExplicitTrace.Element with type t := t
val get_access_path : t -> AccessPath.t option val get_access_path : t -> AccessPath.t option
end end
module TraceElem : sig module TraceElem : sig
include TraceElem.S with module Kind = Access include ExplicitTrace.TraceElem with type elem_t = Access.t
val is_write : t -> bool val is_write : t -> bool
@ -36,18 +36,11 @@ module TraceElem : sig
val map : f:(AccessPath.t -> AccessPath.t) -> t -> t 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_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 val make_field_access : AccessPath.t -> is_write:bool -> Location.t -> t
end 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 *) (** Overapproximation of number of locks that are currently held *)
module LocksDomain : sig module LocksDomain : sig
type t type t
@ -103,7 +96,7 @@ module AccessSnapshot : sig
end end
type t = private type t = private
{ access: PathDomain.Sink.t { access: TraceElem.t
; thread: ThreadsDomain.t ; thread: ThreadsDomain.t
; lock: bool ; lock: bool
; ownership_precondition: OwnershipPrecondition.t } ; ownership_precondition: OwnershipPrecondition.t }
@ -111,14 +104,14 @@ module AccessSnapshot : sig
include PrettyPrintable.PrintableOrderedType with type t := t include PrettyPrintable.PrintableOrderedType with type t := t
val make : val make :
PathDomain.Sink.t TraceElem.t
-> LocksDomain.t -> LocksDomain.t
-> ThreadsDomain.t -> ThreadsDomain.t
-> OwnershipPrecondition.t -> OwnershipPrecondition.t
-> Procdesc.t -> Procdesc.t
-> t option -> 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 val is_unprotected : t -> bool
(** return true if not protected by lock, thread, or ownership *) (** 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_assignment : AccessPath.t -> HilExp.t -> t -> t
val propagate_return : AccessPath.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t val propagate_return : AccessPath.t -> OwnershipAbstractValue.t -> HilExp.t list -> t -> t
val get_precondition : AccessPath.t -> t -> AccessSnapshot.OwnershipPrecondition.t
end end
(** attribute attached to a boolean variable specifying what it means when the boolean is true *) (** attribute attached to a boolean variable specifying what it means when the boolean is true *)

9
infer/src/concurrency/starvationDomain.ml
Unescape View File

@ -57,6 +57,8 @@ module Lock = struct
F.fprintf fmt "%a%a" (MF.wrap_monospaced pp) lock pp_owner lock 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 let pp_locks fmt lock = F.fprintf fmt " locks %a" pp_human lock
end end
@ -94,6 +96,9 @@ module Event = struct
F.pp_print_string fmt msg F.pp_print_string fmt msg
| StrictModeCall msg -> | StrictModeCall msg ->
F.pp_print_string fmt msg F.pp_print_string fmt msg
let pp_call = ExplicitTrace.default_pp_call
end end
include ExplicitTrace.MakeTraceElem (EventElement) include ExplicitTrace.MakeTraceElem (EventElement)
@ -135,6 +140,8 @@ module Order = struct
let pp_human fmt {first} = Lock.pp_locks fmt first let pp_human fmt {first} = Lock.pp_locks fmt first
let pp_call = ExplicitTrace.default_pp_call
end end
include ExplicitTrace.MakeTraceElem (OrderElement) include ExplicitTrace.MakeTraceElem (OrderElement)
@ -200,6 +207,8 @@ module UIThreadExplanationDomain = struct
include String include String
let pp_human = pp let pp_human = pp
let pp_call = ExplicitTrace.default_pp_call
end end
include ExplicitTrace.MakeTraceElem (StringElement) include ExplicitTrace.MakeTraceElem (StringElement)

2
infer/tests/build_systems/racerd_dedup/issues.exp
Unescape View File

@ -1,6 +1,6 @@
DeDup.java, build_systems.threadsafety.DeDup.colocated_read_write():void, 63, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to void DeDup.read_and_write(),access to `this.colocated_read`,<Write trace>,access to `this.colocated_read`] DeDup.java, build_systems.threadsafety.DeDup.colocated_read_write():void, 63, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to void DeDup.read_and_write(),access to `this.colocated_read`,<Write trace>,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.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_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, [<Read trace>,access to `this.field`,<Write trace>,access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.two_reads():void, 38, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.field`,<Write trace>,access to `this.field`]
DeDup.java, build_systems.threadsafety.DeDup.two_writes():void, 31, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.two_writes():void, 31, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`]

Write Preview
Loading…
Cancel
Save