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

[racerd] gate stability

Browse Source 
Summary:
Do no computation of stability abstract state if not explicitly requested via the command line flag.
Also, simplify the reporting.

Reviewed By: jeremydubreil

Differential Revision: D8614885

fbshipit-source-id: 25dd9de
master
Nikos Gorogiannis 7 years ago committed by Facebook Github Bot
parent a6a7b7f467
commit d4a9c6f81a
3 changed files with 65 additions and 75 deletions
Show Stats Download Patch File Download Diff File

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

@ -347,20 +347,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(instr: HilInstr.t) = (instr: HilInstr.t) =
let open Domain in let open Domain in
let open RacerDConfig in let open RacerDConfig in
let add_base ret_base wps = StabilityDomain.add_path (ret_base, []) wps in
match instr with match instr with
| Call (ret_base, Direct procname, actuals, _, loc) | Call (ret_base, Direct procname, actuals, _, loc)
when Models.acquires_ownership procname tenv -> when Models.acquires_ownership procname tenv ->
let ret_access_path = (ret_base, []) in
let accesses = let accesses =
add_reads actuals loc astate.accesses astate.locks astate.threads astate.ownership add_reads actuals loc astate.accesses astate.locks astate.threads astate.ownership
proc_data proc_data
in in
let ownership = let ownership =
OwnershipDomain.add (ret_base, []) OwnershipAbstractValue.owned astate.ownership OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned astate.ownership
in in
let wobbly_paths = add_base ret_base astate.wobbly_paths in let wobbly_paths = StabilityDomain.add_path ret_access_path astate.wobbly_paths in
{astate with accesses; ownership; wobbly_paths} {astate with accesses; ownership; wobbly_paths}
| Call (ret_access_path, Direct callee_pname, actuals, call_flags, loc) -> | Call (ret_base, Direct callee_pname, actuals, call_flags, loc) ->
let ret_access_path = (ret_base, []) in
let accesses_with_unannotated_calls = let accesses_with_unannotated_calls =
add_unannotated_call_access callee_pname actuals call_flags loc tenv ~locks:astate.locks add_unannotated_call_access callee_pname actuals call_flags loc tenv ~locks:astate.locks
~threads:astate.threads astate.accesses proc_data ~threads:astate.threads astate.accesses proc_data
@ -369,7 +370,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads
astate.ownership proc_data astate.ownership proc_data
in in
let wobbly_paths = add_base ret_access_path astate.wobbly_paths in let wobbly_paths = StabilityDomain.add_path ret_access_path astate.wobbly_paths in
let astate = {astate with accesses; wobbly_paths} in let astate = {astate with accesses; wobbly_paths} in
let astate = let astate =
match Models.get_thread callee_pname with match Models.get_thread callee_pname with
@ -379,7 +380,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{astate with threads= ThreadsDomain.AnyThreadButSelf} {astate with threads= ThreadsDomain.AnyThreadButSelf}
| MainThreadIfTrue -> | MainThreadIfTrue ->
let attribute_map = let attribute_map =
AttributeMapDomain.add_attribute (ret_access_path, []) (Choice Choice.OnMainThread) AttributeMapDomain.add_attribute ret_access_path (Choice Choice.OnMainThread)
astate.attribute_map astate.attribute_map
in in
{astate with attribute_map} {astate with attribute_map}
@ -411,7 +412,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
; threads= update_for_lock_use astate.threads } ; threads= update_for_lock_use astate.threads }
| LockedIfTrue -> | LockedIfTrue ->
let attribute_map = let attribute_map =
AttributeMapDomain.add_attribute (ret_access_path, []) (Choice Choice.LockHeld) AttributeMapDomain.add_attribute ret_access_path (Choice Choice.LockHeld)
astate.attribute_map astate.attribute_map
in in
{astate with attribute_map; threads= update_for_lock_use astate.threads} {astate with attribute_map; threads= update_for_lock_use astate.threads}
@ -442,8 +443,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
loc loc
in in
let ownership, attribute_map = let ownership, attribute_map =
propagate_return ret_access_path return_ownership return_attributes actuals propagate_return ret_base return_ownership return_attributes actuals astate
astate
in in
let wobbly_paths = let wobbly_paths =
StabilityDomain.integrate_summary actuals callee_pdesc ~callee:callee_wps StabilityDomain.integrate_summary actuals callee_pdesc ~callee:callee_wps
@ -470,7 +470,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
then then
(* TODO: check for constants, which are functional? *) (* TODO: check for constants, which are functional? *)
let attribute_map = let attribute_map =
AttributeMapDomain.add_attribute (ret_access_path, []) Functional AttributeMapDomain.add_attribute ret_access_path Functional
astate.attribute_map astate.attribute_map
in in
{astate with attribute_map} {astate with attribute_map}
@ -479,7 +479,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
astate astate
else if should_assume_returns_ownership call_flags actuals then else if should_assume_returns_ownership call_flags actuals then
let ownership = let ownership =
OwnershipDomain.add (ret_access_path, []) OwnershipAbstractValue.owned OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned
astate.ownership astate.ownership
in in
{astate with ownership} {astate with ownership}
@ -487,7 +487,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in in
let add_if_annotated predicate attribute attribute_map = let add_if_annotated predicate attribute attribute_map =
if PatternMatch.override_exists predicate tenv callee_pname then if PatternMatch.override_exists predicate tenv callee_pname then
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 =
@ -499,7 +499,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(Models.has_return_annot Annotations.ia_is_returns_ownership) (Models.has_return_annot Annotations.ia_is_returns_ownership)
tenv callee_pname tenv callee_pname
then then
OwnershipDomain.add (ret_access_path, []) OwnershipAbstractValue.owned OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned
astate_callee.ownership astate_callee.ownership
else astate_callee.ownership else astate_callee.ownership
in in
@ -903,20 +903,19 @@ let make_trace ~report_kind original_path pdesc =
(original_trace, original_end, None) (original_trace, original_end, None)
let ignore_var v = Var.is_global v || Var.is_return v
(* Checking for a wobbly path *) (* Checking for a wobbly path *)
let get_contaminated_race_message access wobbly_paths = let is_contaminated access wobbly_paths =
let ignore_var ((v, _), _) = Var.is_global v || Var.is_return v in
let open RacerDDomain in let open RacerDDomain in
match TraceElem.kind access with match TraceElem.kind access with
| TraceElem.Kind.Read access_path | TraceElem.Kind.Read access_path
| Write access_path | Write access_path
(* Access paths rooted in static variables are always race-prone, (* Access paths rooted in static variables are always race-prone,
hence do not complain about contamination. *) hence do not complain about contamination. *)
when not (access_path |> fst |> fst |> ignore_var) -> when not (ignore_var access_path) ->
if StabilityDomain.exists_proper_prefix access_path wobbly_paths then Some " [wob]" else None StabilityDomain.exists_proper_prefix access_path wobbly_paths
| _ -> | _ ->
None false
let log_issue current_pname ~loc ~ltr ~access exn = let log_issue current_pname ~loc ~ltr ~access exn =
@ -931,42 +930,23 @@ let report_thread_safety_violation tenv pdesc ~make_description ~report_kind acc
let final_sink, _ = List.hd_exn sinks in let final_sink, _ = List.hd_exn sinks in
let initial_sink, _ = List.last_exn sinks in let initial_sink, _ = List.last_exn sinks in
let is_full_trace = TraceElem.is_direct final_sink in let is_full_trace = TraceElem.is_direct final_sink in
let is_pvar_base initial_sink =
let access_path = Access.get_access_path (PathDomain.Sink.kind initial_sink) in
Option.value_map ~default:true access_path ~f:(fun ((var, _), _) ->
Var.appears_in_source_code var )
in
(* Traces can be truncated due to limitations of our Buck integration. If we have a truncated (* 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. trace, it's probably going to be too confusing to be actionable. Skip it. *)
It is difficult to ensure that a report on an access path starting with a logical if not Config.filtering || not (Typ.Procname.is_java pname) || is_full_trace then
variable or a temporary variable, is a race. We want to skip the reports, at least for now.*) if not Config.racerd_use_path_stability || not (is_contaminated access wobbly_paths) then
if let final_sink_site = PathDomain.Sink.call_site final_sink in
not Config.filtering let initial_sink_site = PathDomain.Sink.call_site initial_sink in
|| (is_pvar_base initial_sink && (not (Typ.Procname.is_java pname) || is_full_trace)) let loc = CallSite.loc initial_sink_site in
then let ltr, original_end, conflict_end = make_trace ~report_kind path pdesc in
let final_sink_site = PathDomain.Sink.call_site final_sink in (* what the potential bug is *)
let initial_sink_site = PathDomain.Sink.call_site initial_sink in let description = make_description pname final_sink_site initial_sink_site initial_sink in
let loc = CallSite.loc initial_sink_site in (* why we are reporting it *)
let ltr, original_end, conflict_end = make_trace ~report_kind path pdesc in let issue_type, explanation = get_reporting_explanation report_kind tenv pname thread in
(* what the potential bug is *) let error_message = F.sprintf "%s%s" description explanation in
let description = make_description pname final_sink_site initial_sink_site initial_sink in let exn = Exceptions.Checkers (issue_type, Localise.verbatim_desc error_message) in
(* why we are reporting it *) let end_locs = Option.to_list original_end @ Option.to_list conflict_end in
let issue_type, explanation = get_reporting_explanation report_kind tenv pname thread in let access = IssueAuxData.encode (pname, access, end_locs) in
let error_message = F.sprintf "%s%s" description explanation in log_issue pname ~loc ~ltr ~access exn
match get_contaminated_race_message access wobbly_paths with
| Some _ when Config.racerd_use_path_stability ->
(* don't report races on unstable paths when use_path_stability is on *)
()
| contaminated_message_opt ->
let exn =
Exceptions.Checkers
( issue_type
, Localise.verbatim_desc
(error_message ^ Option.value contaminated_message_opt ~default:"") )
in
let end_locs = Option.to_list original_end @ Option.to_list conflict_end in
let access = IssueAuxData.encode (pname, access, end_locs) in
log_issue pname ~loc ~ltr ~access exn
in in
let trace_of_pname = trace_of_pname access pdesc 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) Option.iter ~f:report_one_path (PathDomain.get_reportable_sink_path access ~trace_of_pname)

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

@ -533,16 +533,24 @@ module StabilityDomain = struct
let add_path path_to_add t = let add_path path_to_add t =
if should_skip_var (fst path_to_add |> fst) || exists_prefix path_to_add t then t if
not Config.racerd_use_path_stability || should_skip_var (fst path_to_add |> fst)
|| exists_prefix path_to_add t
then t
else filter (fun path -> is_prefix path_to_add path |> not) t |> add path_to_add else filter (fun path -> is_prefix path_to_add path |> not) t |> add path_to_add
let add_exp exp paths = let add_exp exp paths =
AccessExpression.to_access_paths (HilExp.get_access_exprs exp) if not Config.racerd_use_path_stability then paths
|> List.fold ~f:(fun acc p -> add_path p acc) ~init:paths else
AccessExpression.to_access_paths (HilExp.get_access_exprs exp)
|> List.fold ~f:(fun acc p -> add_path p acc) ~init:paths
let add_assign lhs_path rhs_exp paths =
if not Config.racerd_use_path_stability then paths
else add_path lhs_path paths |> add_exp rhs_exp
let add_assign lhs_path rhs_exp paths = add_path lhs_path paths |> add_exp rhs_exp
let actual_to_access_path actual_exp = let actual_to_access_path actual_exp =
match HilExp.get_access_exprs actual_exp with match HilExp.get_access_exprs actual_exp with
@ -566,21 +574,23 @@ module StabilityDomain = struct
let integrate_summary actuals pdesc_opt ~callee ~caller = let integrate_summary actuals pdesc_opt ~callee ~caller =
let rebased = if not Config.racerd_use_path_stability then caller
Option.value_map pdesc_opt ~default:callee ~f:(fun pdesc -> rebase actuals pdesc callee) else
in let rebased =
let joined = join rebased caller in Option.value_map pdesc_opt ~default:callee ~f:(fun pdesc -> rebase actuals pdesc callee)
let actual_aps = List.filter_map actuals ~f:actual_to_access_path in in
let rec aux acc left right = let joined = join rebased caller in
match right with let actual_aps = List.filter_map actuals ~f:actual_to_access_path in
| [] -> let rec aux acc left right =
acc match right with
| ap :: aps -> | [] ->
let all = List.rev_append left aps in acc
let acc' = if List.exists all ~f:(is_prefix ap) then add_path ap acc else acc in | ap :: aps ->
aux acc' (ap :: left) aps let all = List.rev_append left aps in
in let acc' = if List.exists all ~f:(is_prefix ap) then add_path ap acc else acc in
aux joined [] actual_aps aux acc' (ap :: left) aps
in
aux joined [] actual_aps
end end
type astate = type astate =

4
infer/tests/codetoanalyze/cpp/racerd/issues.exp
Unescape View File

@ -2,9 +2,9 @@ codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get2, 36, LOCK_CONSISTENCY_VI
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get4, 43, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.suspiciously_read`,<Write trace>,access to `this.suspiciously_read`] codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get4, 43, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.suspiciously_read`,<Write trace>,access to `this.suspiciously_read`]
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get5, 45, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to basics::Basic_get_private_suspiciously_read,access to `this.suspiciously_read`,<Write trace>,access to `this.suspiciously_read`] codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get5, 45, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to basics::Basic_get_private_suspiciously_read,access to `this.suspiciously_read`,<Write trace>,access to `this.suspiciously_read`]
codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_test_double_lock_bad, 81, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.single_lock_suspiciously_read`,<Write trace>,access to `this.single_lock_suspiciously_read`] codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_test_double_lock_bad, 81, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `this.single_lock_suspiciously_read`,<Write trace>,access to `this.single_lock_suspiciously_read`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`] codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`] codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`] codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`]
codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`] codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_test_unlock, 59, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [<Read trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,<Write trace>,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`]

Write Preview
Loading…
Cancel
Save