diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 8caeaa9e6..9f0dbb8f9 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -106,12 +106,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let add_access exp loc ~is_write_access accesses locks threads ownership (proc_data: extras ProcData.t) = let open Domain in - let is_static_access = function - | Var.ProgramVar pvar -> - Pvar.is_static_local pvar - | _ -> - false - in let rec add_field_accesses prefix_path access_acc = function | [] -> access_acc @@ -145,7 +139,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct List.fold ~f:(fun acc access_expr -> let base, accesses = AccessExpression.to_access_path access_expr in - if is_static_access (fst base) then acc else add_field_accesses (base, []) acc accesses ) + add_field_accesses (base, []) acc accesses ) ~init:accesses (HilExp.get_access_exprs exp) diff --git a/infer/src/concurrency/RacerDConfig.mli b/infer/src/concurrency/RacerDConfig.mli index 8038b7c37..e46ca1407 100644 --- a/infer/src/concurrency/RacerDConfig.mli +++ b/infer/src/concurrency/RacerDConfig.mli @@ -15,10 +15,9 @@ module Models : sig type container_access = ContainerRead | ContainerWrite - (* TODO: clean this up so it takes only a procname *) - val is_thread_utils_method : string -> Typ.Procname.t -> bool - (** return true if the given method name is a utility class for checking what thread we're on *) + (** return true if the given method name is a utility class for checking what thread we're on + TODO: clean this up so it takes only a procname *) val get_lock : Typ.Procname.t -> HilExp.t list -> lock (** describe how this procedure behaves with respect to locking *) diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 927b7695a..e7772851c 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -8,6 +8,17 @@ open! IStd module F = Format +(** 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 + appear in source code (eg, temporary variables and frontend introduced variables). + This is because currently reports on these variables would not be easily actionable. + + This is here and not in RacerDConfig to avoid dependency cycles. *) +let should_skip_var v = + not (Var.appears_in_source_code v) + || match v with Var.ProgramVar pvar -> Pvar.is_static_local pvar | _ -> false + + module Access = struct type t = | Read of AccessPath.t @@ -304,7 +315,16 @@ module AccessSnapshot = struct thread lock OwnershipPrecondition.pp ownership_precondition end -module AccessDomain = AbstractDomain.FiniteSet (AccessSnapshot) +module AccessDomain = struct + include AbstractDomain.FiniteSet (AccessSnapshot) + + let add ({AccessSnapshot.access= {kind}} as s) astate = + let skip = + Access.get_access_path kind + |> Option.value_map ~default:false ~f:(fun ((v, _), _) -> should_skip_var v) + in + if skip then astate else add s astate +end module OwnershipAbstractValue = struct type astate = Owned | OwnedIf of IntSet.t | Unowned [@@deriving compare] @@ -498,7 +518,7 @@ module StabilityDomain = struct let add_path (access_path: AccessPath.t) t = let (base, _), accesses = access_path in (* Without this check, short prefixes will override longer paths in the tree *) - if mem (AccessPath.Abs.Abstracted access_path) t then t + if should_skip_var base || mem (AccessPath.Abs.Abstracted access_path) t then t else match (base, accesses) with (* Do not add a vanilla "this" as a prefix *) diff --git a/infer/tests/codetoanalyze/cpp/racerd/constructor_ownership.cpp b/infer/tests/codetoanalyze/cpp/racerd/constructor_ownership.cpp index b195a2311..f8e8133e2 100644 --- a/infer/tests/codetoanalyze/cpp/racerd/constructor_ownership.cpp +++ b/infer/tests/codetoanalyze/cpp/racerd/constructor_ownership.cpp @@ -77,7 +77,7 @@ struct TSL { BSS().toJson_ok(); } - void not_locked_race(dynamic& ret) { BSS().toJson_race(ret); } + void FN_not_locked_race(dynamic& ret) { BSS().toJson_race(ret); } void locked_race(dynamic& ret) { std::lock_guard lock(mutex_); diff --git a/infer/tests/codetoanalyze/cpp/racerd/issues.exp b/infer/tests/codetoanalyze/cpp/racerd/issues.exp index 019ee7414..9a3ebdc03 100644 --- a/infer/tests/codetoanalyze/cpp/racerd/issues.exp +++ b/infer/tests/codetoanalyze/cpp/racerd/issues.exp @@ -2,7 +2,6 @@ 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, [,access to `this.suspiciously_read`,,access to `this.suspiciously_read`] codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_get5, 45, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to basics::Basic_get_private_suspiciously_read,access to `this.suspiciously_read`,,access to `this.suspiciously_read`] codetoanalyze/cpp/racerd/basics.cpp, basics::Basic_test_double_lock_bad, 81, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,access to `this.single_lock_suspiciously_read`,,access to `this.single_lock_suspiciously_read`] -codetoanalyze/cpp/racerd/constructor_ownership.cpp, constructors::TSL_not_locked_race, 80, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to constructors::BSS_toJson_race,call to constructors::dynamic_operator=,access to `this.type_`,,call to constructors::BSS_toJson_race,call to constructors::dynamic_operator=,access to `this.type_`] codetoanalyze/cpp/racerd/dereferencing.cpp, dereferencing::Basic_call1, 51, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.u`,,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, [,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x1.w`,,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, [,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`,,call to dereferencing::Basic_call1,call to dereferencing::Basic_mixed_deref_race,access to `xparam.x2.a.b.c`] diff --git a/infer/tests/codetoanalyze/java/racerd/Ownership.java b/infer/tests/codetoanalyze/java/racerd/Ownership.java index d317761cb..f169aa80d 100644 --- a/infer/tests/codetoanalyze/java/racerd/Ownership.java +++ b/infer/tests/codetoanalyze/java/racerd/Ownership.java @@ -353,7 +353,7 @@ public class Ownership { castThenReturn(o).f = new Object(); } - void castThenReturnBad() { + void FN_castThenReturnBad() { Obj o = getMaybeUnownedObj(); castThenReturn(o).f = new Object(); } @@ -450,7 +450,7 @@ public class Ownership { o.f = null; // don't know that this.unownedField2 is owned } - void reassignParamToUnownedBad() { + void FN_reassignParamToUnownedBad() { reassignParamToUnowned(new Obj()); // although o is owned here, it gets reassigned in the callee } diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index 06ba30e08..ef59cf642 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -72,14 +72,12 @@ codetoanalyze/java/racerd/Ownership.java, Ownership.(Obj,Object), 65, THRE codetoanalyze/java/racerd/Ownership.java, int Ownership.readGlobalBad(), 401, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `checkers.Ownership.codetoanalyze.java.checkers.Ownership.global`,,access to `checkers.Ownership.codetoanalyze.java.checkers.Ownership.global`] codetoanalyze/java/racerd/Ownership.java, void Ownership.cantOwnThisBad(), 170, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void Ownership.setField(Obj),access to `this.codetoanalyze.java.checkers.Ownership.field`] codetoanalyze/java/racerd/Ownership.java, void Ownership.castThenCallBad(), 343, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void Ownership.castThenCall(Obj),call to void Subclass.doWrite(),access to `this.codetoanalyze.java.checkers.Obj.f`] -codetoanalyze/java/racerd/Ownership.java, void Ownership.castThenReturnBad(), 358, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `n$5.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.conditionalAliasBad(Obj), 504, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void Ownership.conditionalAlias(Obj,Obj),access to `alias.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.notOwnedInCalleeBad(Obj), 232, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void Ownership.mutateIfNotNull(Obj),access to `o.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.notPropagatingOwnershipToAccessPathRootedAtFormalBad(Obj), 419, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `m.codetoanalyze.java.checkers.Obj.g`] codetoanalyze/java/racerd/Ownership.java, void Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad(), 425, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.codetoanalyze.java.checkers.Ownership.field`,,call to void Ownership.setField(Obj),access to `this.codetoanalyze.java.checkers.Ownership.field`] codetoanalyze/java/racerd/Ownership.java, void Ownership.notPropagatingOwnershipToUnownedLocalAccessPathBad(), 426, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `m.codetoanalyze.java.checkers.Obj.g`] codetoanalyze/java/racerd/Ownership.java, void Ownership.ownInOneBranchBad(Obj,boolean), 81, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `formal.codetoanalyze.java.checkers.Obj.f`] -codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignParamToUnownedBad(), 454, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void Ownership.reassignParamToUnowned(Obj),access to `o.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignToFormalBad(Obj), 86, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `formal.codetoanalyze.java.checkers.Obj.g`] codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignToFormalBad(Obj), 87, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `formal.codetoanalyze.java.checkers.Obj.g.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.reassignToFormalBad(Obj), 87, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `formal.codetoanalyze.java.checkers.Obj.g`,,access to `formal.codetoanalyze.java.checkers.Obj.g`]