[racerd] kill stability

Reviewed By: jvillard

Differential Revision: D13180369

fbshipit-source-id: 5684ed318
master
Nikos Gorogiannis 6 years ago committed by Facebook Github Bot
parent f4e9975783
commit 2c6a705116

@ -120,7 +120,6 @@ DIRECT_TESTS += \
java_purity \ java_purity \
java_quandary \ java_quandary \
java_racerd \ java_racerd \
java_stability \
java_starvation \ java_starvation \
java_tracing \ java_tracing \
@ -136,7 +135,6 @@ ifneq ($(filter build_systems_tests config_tests test test-replace,${MAKECMDGOAL
build_genrule_print: build_buck_print build_genrule_print: build_buck_print
build_genrule_replace: build_buck_replace build_genrule_replace: build_buck_replace
build_genrule_test: build_buck_test build_genrule_test: build_buck_test
direct_java_racerd_path_stability_test: direct_java_racerd_test
endif endif
endif endif
ifneq ($(MVN),no) ifneq ($(MVN),no)

@ -1342,10 +1342,6 @@ INTERNAL OPTIONS
--profiler-samples-reset --profiler-samples-reset
Cancel the effect of --profiler-samples. Cancel the effect of --profiler-samples.
--racerd-use-path-stability
Activates: Use access path stability to prune RacerD false
positives (Conversely: --no-racerd-use-path-stability)
--reactive-capture --reactive-capture
Activates: Compile source files only when required by analyzer Activates: Compile source files only when required by analyzer
(clang only) (Conversely: --no-reactive-capture) (clang only) (Conversely: --no-reactive-capture)

@ -1824,11 +1824,6 @@ and quiet =
"Do not print specs on standard output (default: only print for the $(b,report) command)" "Do not print specs on standard output (default: only print for the $(b,report) command)"
and racerd_use_path_stability =
CLOpt.mk_bool ~long:"racerd-use-path-stability" ~default:false
"Use access path stability to prune RacerD false positives"
and reactive = and reactive =
CLOpt.mk_bool ~deprecated:["reactive"] ~long:"reactive" ~short:'r' CLOpt.mk_bool ~deprecated:["reactive"] ~long:"reactive" ~short:'r'
~in_help:InferCommand.[(Analyze, manual_generic)] ~in_help:InferCommand.[(Analyze, manual_generic)]
@ -2852,8 +2847,6 @@ and quiet = !quiet
and racerd = !racerd and racerd = !racerd
and racerd_use_path_stability = !racerd_use_path_stability
and reactive_mode = !reactive || InferCommand.(equal Diff) command and reactive_mode = !reactive || InferCommand.(equal Diff) command
and reactive_capture = !reactive_capture and reactive_capture = !reactive_capture

@ -561,8 +561,6 @@ val quandary_sinks : Yojson.Basic.json
val quiet : bool val quiet : bool
val racerd_use_path_stability : bool
val reactive_mode : bool val reactive_mode : bool
val reactive_capture : bool val reactive_capture : bool

@ -371,8 +371,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let ownership = let ownership =
OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned astate.ownership OwnershipDomain.add ret_access_path OwnershipAbstractValue.owned astate.ownership
in in
let wobbly_paths = StabilityDomain.add_path ret_access_path astate.wobbly_paths in {astate with accesses; ownership}
{astate with accesses; ownership; wobbly_paths}
| Call (ret_base, 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 ret_access_path = (ret_base, []) in
let accesses_with_unannotated_calls = let accesses_with_unannotated_calls =
@ -383,8 +382,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 = StabilityDomain.add_path ret_access_path astate.wobbly_paths in let astate = {astate with accesses} in
let astate = {astate with accesses; wobbly_paths} in
let astate = let astate =
match get_thread callee_pname with match get_thread callee_pname with
| BackgroundThread -> | BackgroundThread ->
@ -440,13 +438,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in in
{summary with accesses= rebased_accesses} ) {summary with accesses= rebased_accesses} )
with with
| Some | Some {threads; locks; accesses; return_ownership; return_attributes} ->
{ threads
; locks
; accesses
; return_ownership
; return_attributes
; wobbly_paths= callee_wps } ->
let locks = let locks =
LocksDomain.integrate_summary ~caller_astate:astate.locks LocksDomain.integrate_summary ~caller_astate:astate.locks
~callee_astate:locks ~callee_astate:locks
@ -462,15 +454,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let attribute_map = let attribute_map =
AttributeMapDomain.add ret_access_path return_attributes astate.attribute_map AttributeMapDomain.add ret_access_path return_attributes astate.attribute_map
in in
let wobbly_paths =
StabilityDomain.integrate_summary actuals callee_pdesc ~callee:callee_wps
~caller:wobbly_paths
in
let threads = let threads =
ThreadsDomain.integrate_summary ~caller_astate:astate.threads ThreadsDomain.integrate_summary ~caller_astate:astate.threads
~callee_astate:threads ~callee_astate:threads
in in
{locks; threads; accesses; ownership; attribute_map; wobbly_paths} {locks; threads; accesses; ownership; attribute_map}
| None -> | None ->
call_without_summary callee_pname ret_access_path call_flags actuals astate ) call_without_summary callee_pname ret_access_path call_flags actuals astate )
in in
@ -533,10 +521,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let attribute_map = let attribute_map =
AttributeMapDomain.propagate_assignment lhs_access_path rhs_exp astate.attribute_map AttributeMapDomain.propagate_assignment lhs_access_path rhs_exp astate.attribute_map
in in
let wobbly_paths = {astate with accesses; ownership; attribute_map}
StabilityDomain.add_assign lhs_access_path rhs_exp astate.wobbly_paths
in
{astate with accesses; ownership; attribute_map; wobbly_paths}
| Assume (assume_exp, _, _, loc) -> | Assume (assume_exp, _, _, loc) ->
let rec eval_binop op var e1 e2 = let rec eval_binop op var e1 e2 =
match (eval_bexp var e1, eval_bexp var e2) with match (eval_bexp var e1, eval_bexp var e2) with
@ -691,7 +676,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
{RacerDDomain.empty with ownership; threads} {RacerDDomain.empty with ownership; threads}
in in
match Analyzer.compute_post proc_data ~initial with match Analyzer.compute_post proc_data ~initial with
| Some {threads; locks; accesses; ownership; attribute_map; wobbly_paths} -> | Some {threads; locks; accesses; ownership; attribute_map} ->
let return_var_ap = let return_var_ap =
AccessPath.of_pvar AccessPath.of_pvar
(Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc)) (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc))
@ -702,7 +687,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
try AttributeMapDomain.find return_var_ap attribute_map with Caml.Not_found -> try AttributeMapDomain.find return_var_ap attribute_map with Caml.Not_found ->
AttributeSetDomain.empty AttributeSetDomain.empty
in in
let post = {threads; locks; accesses; return_ownership; return_attributes; wobbly_paths} in let post = {threads; locks; accesses; return_ownership; return_attributes} in
Payload.update_summary post summary Payload.update_summary post summary
| None -> | None ->
summary summary
@ -872,28 +857,12 @@ let make_trace ~report_kind original_path pdesc =
(original_trace, original_end, None) (original_trace, original_end, None)
(* Checking for a wobbly path *)
let is_contaminated access wobbly_paths =
let ignore_var ((v, _), _) = Var.is_global v || Var.is_return v in
let open RacerDDomain in
match TraceElem.kind access with
| TraceElem.Kind.Read access_path
| Write access_path
(* Access paths rooted in static variables are always race-prone,
hence do not complain about contamination. *)
when not (ignore_var access_path) ->
StabilityDomain.exists_proper_prefix access_path wobbly_paths
| _ ->
false
let log_issue current_pname ~loc ~ltr ~access issue_type error_message = let log_issue current_pname ~loc ~ltr ~access issue_type error_message =
Reporting.log_issue_external current_pname Exceptions.Error ~loc ~ltr ~access issue_type Reporting.log_issue_external current_pname Exceptions.Error ~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 thread =
wobbly_paths =
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 report_one_path ((_, sinks) as path) =
@ -903,7 +872,6 @@ let report_thread_safety_violation tenv pdesc ~make_description ~report_kind acc
(* 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. *)
if (not Config.filtering) || (not (Typ.Procname.is_java pname)) || is_full_trace then if (not Config.filtering) || (not (Typ.Procname.is_java pname)) || is_full_trace then
if (not Config.racerd_use_path_stability) || not (is_contaminated access wobbly_paths) then
let final_sink_site = PathDomain.Sink.call_site final_sink in let final_sink_site = PathDomain.Sink.call_site final_sink in
let initial_sink_site = PathDomain.Sink.call_site initial_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
@ -932,7 +900,7 @@ let report_unannotated_interface_violation tenv pdesc access thread reported_pna
Typ.Procname.pp reported_pname class_name MF.pp_monospaced "@ThreadSafe" Typ.Procname.pp reported_pname class_name MF.pp_monospaced "@ThreadSafe"
in in
report_thread_safety_violation tenv pdesc ~make_description ~report_kind:UnannotatedInterface report_thread_safety_violation tenv pdesc ~make_description ~report_kind:UnannotatedInterface
access thread RacerDDomain.StabilityDomain.empty access thread
| _ -> | _ ->
(* skip reporting on C++ *) (* skip reporting on C++ *)
() ()
@ -951,8 +919,7 @@ type reported_access =
{ threads: RacerDDomain.ThreadsDomain.astate { threads: RacerDDomain.ThreadsDomain.astate
; snapshot: RacerDDomain.AccessSnapshot.t ; snapshot: RacerDDomain.AccessSnapshot.t
; tenv: Tenv.t ; tenv: Tenv.t
; procdesc: Procdesc.t ; procdesc: Procdesc.t }
; wobbly_paths: RacerDDomain.StabilityDomain.astate }
let make_read_write_race_description ~read_is_sync (conflict : reported_access) pname let make_read_write_race_description ~read_is_sync (conflict : reported_access) pname
final_sink_site initial_sink_site final_sink = final_sink_site initial_sink_site final_sink =
@ -1156,8 +1123,7 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) =
{reported with reported_unannotated_calls; reported_sites} {reported with reported_unannotated_calls; reported_sites}
else reported else reported
in in
let report_unsafe_access accesses reported_acc {snapshot; threads; tenv; procdesc; wobbly_paths} let report_unsafe_access accesses reported_acc {snapshot; threads; tenv; procdesc} =
=
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
@ -1192,7 +1158,7 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) =
then ( then (
report_thread_safety_violation tenv procdesc report_thread_safety_violation tenv procdesc
~make_description:make_unprotected_write_description ~make_description:make_unprotected_write_description
~report_kind:(WriteWriteRace conflict) snapshot.access threads wobbly_paths ; ~report_kind:(WriteWriteRace conflict) snapshot.access threads ;
update_reported snapshot.access pname reported_acc ) update_reported snapshot.access pname reported_acc )
else reported_acc else reported_acc
| Access.Write _ | ContainerWrite _ -> | Access.Write _ | ContainerWrite _ ->
@ -1215,7 +1181,7 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) =
in in
let report_kind = ReadWriteRace conflict.snapshot.access in let report_kind = ReadWriteRace conflict.snapshot.access in
report_thread_safety_violation tenv procdesc ~make_description ~report_kind report_thread_safety_violation tenv procdesc ~make_description ~report_kind
snapshot.access threads wobbly_paths ; snapshot.access threads ;
update_reported snapshot.access pname reported_acc ) update_reported snapshot.access pname reported_acc )
| Access.Read _ | ContainerRead _ -> | Access.Read _ | ContainerRead _ ->
(* protected read. report unprotected writes and opposite protected writes as conflicts *) (* protected read. report unprotected writes and opposite protected writes as conflicts *)
@ -1236,7 +1202,7 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) =
in in
let report_kind = ReadWriteRace conflict.snapshot.access in let report_kind = ReadWriteRace conflict.snapshot.access in
report_thread_safety_violation tenv procdesc ~make_description ~report_kind report_thread_safety_violation tenv procdesc ~make_description ~report_kind
snapshot.access threads wobbly_paths ; snapshot.access threads ;
update_reported snapshot.access pname reported_acc ) update_reported snapshot.access pname reported_acc )
in in
let report_accesses_on_location (grouped_accesses : reported_access list) reported_acc = let report_accesses_on_location (grouped_accesses : reported_access list) reported_acc =
@ -1262,9 +1228,9 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) =
that x.f.g may point to during execution *) that x.f.g may point to during execution *)
let make_results_table file_env = let make_results_table file_env =
let open RacerDDomain in let open RacerDDomain in
let aggregate_post acc ({threads; accesses; wobbly_paths}, tenv, procdesc) = let aggregate_post acc ({threads; accesses}, tenv, procdesc) =
AccessDomain.fold AccessDomain.fold
(fun snapshot acc -> ReportMap.add {threads; snapshot; tenv; procdesc; wobbly_paths} acc) (fun snapshot acc -> ReportMap.add {threads; snapshot; tenv; procdesc} acc)
accesses acc accesses acc
in in
List.filter_map file_env ~f:(fun (tenv, proc_desc) -> List.filter_map file_env ~f:(fun (tenv, proc_desc) ->

@ -521,103 +521,12 @@ module AttributeMapDomain = struct
add lhs_access_path rhs_attributes attribute_map add lhs_access_path rhs_attributes attribute_map
end end
module StabilityDomain = struct
include AbstractDomain.FiniteSet (AccessPath)
let is_prefix (base, accesses) (base', accesses') =
AccessPath.equal_base base base'
&& List.is_prefix ~equal:AccessPath.equal_access ~prefix:accesses accesses'
let is_proper_prefix (base, accesses) (base', accesses') =
let rec aux xs ys =
match (xs, ys) with
| [], _ ->
not (List.is_empty ys)
| _, [] ->
false
| w :: ws, z :: zs ->
AccessPath.equal_access w z && aux ws zs
in
AccessPath.equal_base base base' && aux accesses accesses'
let exists_prefix path_to_check t = exists (fun path -> is_prefix path path_to_check) t
let exists_proper_prefix path_to_check t =
exists (fun path -> is_proper_prefix path path_to_check) t
let add_path path_to_add 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
let add_exp exp paths =
if not Config.racerd_use_path_stability then 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 actual_to_access_path actual_exp =
match HilExp.get_access_exprs actual_exp with
| [actual] ->
Some (AccessExpression.to_access_path actual)
| _ ->
None
let rebase actuals pdesc t =
let formal_map = FormalMap.make pdesc in
let expand_path ((base, accesses) as p) =
FormalMap.get_formal_index base formal_map
|> Option.bind ~f:(List.nth actuals)
|> Option.bind ~f:actual_to_access_path
|> Option.value_map ~default:p ~f:(fun ap -> AccessPath.append ap accesses)
in
fold
(fun ((_, accesses) as path) acc ->
if List.is_empty accesses then acc else add_path (expand_path path) acc )
t empty
let integrate_summary actuals pdesc_opt ~callee ~caller =
if not Config.racerd_use_path_stability then caller
else
let rebased =
Option.value_map pdesc_opt ~default:callee ~f:(fun pdesc -> rebase actuals pdesc callee)
in
let joined = join rebased caller in
let actual_aps = List.filter_map actuals ~f:actual_to_access_path in
let rec aux acc left right =
match right with
| [] ->
acc
| ap :: aps ->
let all = List.rev_append left aps in
let acc' = if List.exists all ~f:(is_prefix ap) then add_path ap acc else acc in
aux acc' (ap :: left) aps
in
aux joined [] actual_aps
end
type astate = type astate =
{ threads: ThreadsDomain.astate { threads: ThreadsDomain.astate
; locks: LocksDomain.astate ; locks: LocksDomain.astate
; accesses: AccessDomain.astate ; accesses: AccessDomain.astate
; ownership: OwnershipDomain.astate ; ownership: OwnershipDomain.astate
; attribute_map: AttributeMapDomain.astate ; attribute_map: AttributeMapDomain.astate }
; wobbly_paths: StabilityDomain.astate }
let empty = let empty =
let threads = ThreadsDomain.empty in let threads = ThreadsDomain.empty in
@ -625,15 +534,13 @@ let empty =
let accesses = AccessDomain.empty in let accesses = AccessDomain.empty in
let ownership = OwnershipDomain.empty in let ownership = OwnershipDomain.empty in
let attribute_map = AttributeMapDomain.empty in let attribute_map = AttributeMapDomain.empty in
let wobbly_paths = StabilityDomain.empty in {threads; locks; accesses; ownership; attribute_map}
{threads; locks; accesses; ownership; attribute_map; wobbly_paths}
let is_empty {threads; locks; accesses; ownership; attribute_map; wobbly_paths} = let is_empty {threads; locks; accesses; ownership; attribute_map} =
ThreadsDomain.is_empty threads && LocksDomain.is_empty locks && AccessDomain.is_empty accesses ThreadsDomain.is_empty threads && LocksDomain.is_empty locks && AccessDomain.is_empty accesses
&& OwnershipDomain.is_empty ownership && OwnershipDomain.is_empty ownership
&& AttributeMapDomain.is_empty attribute_map && AttributeMapDomain.is_empty attribute_map
&& StabilityDomain.is_empty wobbly_paths
let ( <= ) ~lhs ~rhs = let ( <= ) ~lhs ~rhs =
@ -643,7 +550,6 @@ let ( <= ) ~lhs ~rhs =
&& LocksDomain.( <= ) ~lhs:lhs.locks ~rhs:rhs.locks && LocksDomain.( <= ) ~lhs:lhs.locks ~rhs:rhs.locks
&& AccessDomain.( <= ) ~lhs:lhs.accesses ~rhs:rhs.accesses && AccessDomain.( <= ) ~lhs:lhs.accesses ~rhs:rhs.accesses
&& AttributeMapDomain.( <= ) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map && AttributeMapDomain.( <= ) ~lhs:lhs.attribute_map ~rhs:rhs.attribute_map
&& StabilityDomain.( <= ) ~lhs:lhs.wobbly_paths ~rhs:rhs.wobbly_paths
let join astate1 astate2 = let join astate1 astate2 =
@ -654,8 +560,7 @@ let join astate1 astate2 =
let accesses = AccessDomain.join astate1.accesses astate2.accesses in let accesses = AccessDomain.join astate1.accesses astate2.accesses in
let ownership = OwnershipDomain.join astate1.ownership astate2.ownership in let ownership = OwnershipDomain.join astate1.ownership astate2.ownership in
let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in
let wobbly_paths = StabilityDomain.join astate1.wobbly_paths astate2.wobbly_paths in {threads; locks; accesses; ownership; attribute_map}
{threads; locks; accesses; ownership; attribute_map; wobbly_paths}
let widen ~prev ~next ~num_iters = let widen ~prev ~next ~num_iters =
@ -668,10 +573,7 @@ let widen ~prev ~next ~num_iters =
let attribute_map = let attribute_map =
AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters
in in
let wobbly_paths = {threads; locks; accesses; ownership; attribute_map}
StabilityDomain.widen ~prev:prev.wobbly_paths ~next:next.wobbly_paths ~num_iters
in
{threads; locks; accesses; ownership; attribute_map; wobbly_paths}
type summary = type summary =
@ -679,37 +581,24 @@ type summary =
; locks: LocksDomain.astate ; locks: LocksDomain.astate
; accesses: AccessDomain.astate ; accesses: AccessDomain.astate
; return_ownership: OwnershipAbstractValue.astate ; return_ownership: OwnershipAbstractValue.astate
; return_attributes: AttributeSetDomain.astate ; return_attributes: AttributeSetDomain.astate }
; wobbly_paths: StabilityDomain.astate }
let empty_summary = let empty_summary =
{ threads= ThreadsDomain.empty { threads= ThreadsDomain.empty
; locks= LocksDomain.empty ; locks= LocksDomain.empty
; accesses= AccessDomain.empty ; accesses= AccessDomain.empty
; return_ownership= OwnershipAbstractValue.unowned ; return_ownership= OwnershipAbstractValue.unowned
; return_attributes= AttributeSetDomain.empty ; return_attributes= AttributeSetDomain.empty }
; wobbly_paths= StabilityDomain.empty }
let pp_summary fmt {threads; locks; accesses; return_ownership; return_attributes; wobbly_paths} = let pp_summary fmt {threads; locks; accesses; return_ownership; return_attributes} =
F.fprintf fmt F.fprintf fmt
"@\n\ "@\nThreads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nReturn Attributes: %a @\n"
Threads: %a, Locks: %a @\n\
Accesses %a @\n\
Ownership: %a @\n\
Return Attributes: %a @\n\
Wobbly Paths: %a@\n"
ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses
OwnershipAbstractValue.pp return_ownership AttributeSetDomain.pp return_attributes OwnershipAbstractValue.pp return_ownership AttributeSetDomain.pp return_attributes
StabilityDomain.pp wobbly_paths
let pp fmt {threads; locks; accesses; ownership; attribute_map; wobbly_paths} = let pp fmt {threads; locks; accesses; ownership; attribute_map} =
F.fprintf fmt F.fprintf fmt "Threads: %a, Locks: %a @\nAccesses %a @\nOwnership: %a @\nAttributes: %a @\n"
"Threads: %a, Locks: %a @\n\
Accesses %a @\n\
Ownership: %a @\n\
Attributes: %a @\n\
Non-stable Paths: %a@\n"
ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp
ownership AttributeMapDomain.pp attribute_map StabilityDomain.pp wobbly_paths ownership AttributeMapDomain.pp attribute_map

@ -200,19 +200,6 @@ module AttributeMapDomain : sig
(** propagate attributes from the leaves to the root of an RHS Hil expression *) (** propagate attributes from the leaves to the root of an RHS Hil expression *)
end end
module StabilityDomain : sig
include AbstractDomain.WithBottom
val add_assign : AccessPath.t -> HilExp.t -> astate -> astate
val add_path : AccessPath.t -> astate -> astate
val exists_proper_prefix : AccessPath.t -> astate -> bool
val integrate_summary :
HilExp.t list -> Procdesc.t option -> callee:astate -> caller:astate -> astate
end
type astate = type astate =
{ threads: ThreadsDomain.astate (** current thread: main, background, or unknown *) { threads: ThreadsDomain.astate (** current thread: main, background, or unknown *)
; locks: LocksDomain.astate (** boolean that is true if a lock must currently be held *) ; locks: LocksDomain.astate (** boolean that is true if a lock must currently be held *)
@ -220,9 +207,7 @@ type astate =
(** read and writes accesses performed without ownership permissions *) (** read and writes accesses performed without ownership permissions *)
; ownership: OwnershipDomain.astate (** map of access paths to ownership predicates *) ; ownership: OwnershipDomain.astate (** map of access paths to ownership predicates *)
; attribute_map: AttributeMapDomain.astate ; attribute_map: AttributeMapDomain.astate
(** map of access paths to attributes such as owned, functional, ... *) (** map of access paths to attributes such as owned, functional, ... *) }
; wobbly_paths: StabilityDomain.astate
(** Record the "touched" paths that can compromise the race detection **) }
(** same as astate, but without [attribute_map] (since these involve locals) and with the addition (** same as astate, but without [attribute_map] (since these involve locals) and with the addition
of the ownership/attributes associated with the return value as well as the set of formals which of the ownership/attributes associated with the return value as well as the set of formals which
@ -232,8 +217,7 @@ type summary =
; locks: LocksDomain.astate ; locks: LocksDomain.astate
; accesses: AccessDomain.astate ; accesses: AccessDomain.astate
; return_ownership: OwnershipAbstractValue.astate ; return_ownership: OwnershipAbstractValue.astate
; return_attributes: AttributeSetDomain.astate ; return_attributes: AttributeSetDomain.astate }
; wobbly_paths: StabilityDomain.astate }
val empty_summary : summary val empty_summary : summary

@ -1,91 +0,0 @@
/*
* Copyright (c) 2018-present, Facebook, Inc.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
package codetoanalyze.java.checkers;
import com.facebook.infer.annotation.ThreadSafe;
class Interprocedural {
static class A {
B f = new B();
int h = 0;
}
static class B {
int g = 0;
}
@ThreadSafe
static class Field {
private A a = new A();
private void destabilize() {
B b = a.f;
}
public void unstable_ok() {
int x = 42;
destabilize();
synchronized (this) {
a.f.g = 101;
}
x = a.f.g;
}
public void stable_bad() {
int x = 42;
synchronized (this) {
a.f.g = 101;
}
x = a.f.g;
}
}
@ThreadSafe
static class Param {
private void destabilize(A z) {
B b1 = z.f;
System.out.println(b1);
}
public void unstable_ok(A a) {
int x = 42;
destabilize(a);
synchronized (this) {
a.f.g = 101;
}
x = a.f.g;
}
public void stable_bad(A a) {
int x = 42;
synchronized (this) {
a.f.g = 101;
}
x = a.f.g;
}
}
@ThreadSafe
static class Param2 {
private void destabilize(A z) {
// Do nothing
}
public void stable_bad(A a) {
int x = 42;
destabilize(a); // a leaks, but shouldn't be de-stabilized because callee does nothing
synchronized (this) {
a.f.g = 101;
}
x = a.f.g;
}
}
}

@ -1,86 +0,0 @@
/*
* Copyright (c) 2018-present, Facebook, Inc.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
package codetoanalyze.java.checkers;
import com.facebook.infer.annotation.ThreadSafe;
class Intraprocedural {
static class B {
int g = 0;
}
static class A {
B f = new B();
int h = 0;
}
@ThreadSafe
static class Field {
private A a = new A();
public void unstable_ok() {
int x = 42;
B b = a.f; // destabilizes
synchronized (this) {
a.f.g = 101;
}
x = a.f.g;
}
public void FN_stable_bad() {
int x = 42;
synchronized (this) {
a.f.g = 101;
}
x = a.f.g;
}
}
static class Param {
public void unstable_ok(A a) {
int x = 42;
B b = a.f; // destabilizes
synchronized (this) {
a.f.g = 101;
}
x = a.f.g;
}
public void stable_bad(A a) {
int x = 42;
synchronized (this) {
a.f.g = 101;
}
x = a.f.g;
}
}
@ThreadSafe
static class Global {
private static A a = new A();
public synchronized A getA() {
return a;
}
public synchronized void setA(A newA) {
a = newA;
}
public void unstable_ok() {
int x = 42;
A a = getA(); // destabilizes
synchronized (this) {
a.f.g = 101;
}
x = a.f.g;
}
}
}

@ -1,12 +0,0 @@
# Copyright (c) 2016-present, Facebook, Inc.
#
# This source code is licensed under the MIT license found in the
# LICENSE file in the root directory of this source tree.
TESTS_DIR = ../../..
INFER_OPTIONS = --racerd-only --debug-exceptions --racerd-use-path-stability
INFERPRINT_OPTIONS = --issues-tests
SOURCES = $(wildcard *.java)
include $(TESTS_DIR)/javac.make

@ -1,3 +0,0 @@
codetoanalyze/java/stability/Interprocedural.java, codetoanalyze.java.checkers.Interprocedural$Param.stable_bad(codetoanalyze.java.checkers.Interprocedural$A):void, 71, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,<Write trace>,access to `a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`]
codetoanalyze/java/stability/Interprocedural.java, codetoanalyze.java.checkers.Interprocedural$Param2.stable_bad(codetoanalyze.java.checkers.Interprocedural$A):void, 88, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`,<Write trace>,access to `a.codetoanalyze.java.checkers.Interprocedural$A.f.codetoanalyze.java.checkers.Interprocedural$B.g`]
codetoanalyze/java/stability/Intraprocedural.java, codetoanalyze.java.checkers.Intraprocedural$Param.stable_bad(codetoanalyze.java.checkers.Intraprocedural$A):void, 61, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [<Read trace>,access to `a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`,<Write trace>,access to `a.codetoanalyze.java.checkers.Intraprocedural$A.f.codetoanalyze.java.checkers.Intraprocedural$B.g`]
Loading…
Cancel
Save