From fdcd4cf591b27777a3ab8d643a8bb02958cf78f0 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 28 Mar 2019 05:55:08 -0700 Subject: [PATCH] [racerd] modulo loc Reviewed By: jvillard Differential Revision: D14616104 fbshipit-source-id: 314a14069 --- infer/src/concurrency/RacerDDomain.ml | 6 ++++-- infer/tests/build_systems/racerd_dedup/issues.exp | 4 ++-- infer/tests/codetoanalyze/java/racerd/issues.exp | 5 ++--- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index eecc03688..88862733e 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -120,8 +120,10 @@ module Access = struct end module TraceElem = struct - (* FIXME evaluate modulo location functor *) - include ExplicitTrace.MakeTraceElem (Access) + (** This choice means the comparator is insensitive to the location access. + This preserves correctness only if the overlying comparator (AccessSnapshot) + takes into account the characteristics of the access (eg lock status). *) + include ExplicitTrace.MakeTraceElemModuloLocation (Access) let is_write {elem} = Access.is_write elem diff --git a/infer/tests/build_systems/racerd_dedup/issues.exp b/infer/tests/build_systems/racerd_dedup/issues.exp index 181092728..0129c0121 100644 --- a/infer/tests/build_systems/racerd_dedup/issues.exp +++ b/infer/tests/build_systems/racerd_dedup/issues.exp @@ -2,7 +2,7 @@ DeDup.java, build_systems.threadsafety.DeDup.colocated_read_write():void, 63, TH 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, 50, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void DeDup.writeToField(),access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.two_fields():void, 20, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to void DeDup.foo(),access to `this.fielda`] -DeDup.java, build_systems.threadsafety.DeDup.two_reads():void, 38, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.field`,,access to `this.field`] -DeDup.java, build_systems.threadsafety.DeDup.two_writes():void, 31, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`] +DeDup.java, build_systems.threadsafety.DeDup.two_reads():void, 37, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.field`,,access to `this.field`] +DeDup.java, build_systems.threadsafety.DeDup.two_writes():void, 30, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.write_read():void, 44, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.field`] DeDup.java, build_systems.threadsafety.DeDup.write_read():void, 45, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.field`,,access to `this.field`] diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index bd40ada35..0a906b784 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -25,7 +25,6 @@ codetoanalyze/java/racerd/Constructors.java, Constructors.FP_singleton2Ok():Cons codetoanalyze/java/racerd/Constructors.java, Constructors.singleton1Bad():Constructors, 57, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [call to Constructors.(Object),access to `Constructors.staticField`] codetoanalyze/java/racerd/Constructors.java, Constructors.singleton2Bad():Constructors, 63, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `Constructors.sSingleton2`,,access to `Constructors.sSingleton2`] codetoanalyze/java/racerd/Constructors.java, Constructors.singleton2Bad():Constructors, 64, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `Constructors.sSingleton2`] -codetoanalyze/java/racerd/Constructors.java, Constructors.singleton2Bad():Constructors, 66, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `Constructors.sSingleton2`,,access to `Constructors.sSingleton2`] codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.addToSimpleArrayMapBad(android.support.v4.util.SimpleArrayMap):void, 279, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [Write to container `map` via call to `put`] codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.addToSparseArrayBad(android.util.SparseArray):void, 269, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [Write to container `sparseArray` via call to `put`] codetoanalyze/java/racerd/Containers.java, codetoanalyze.java.checkers.Containers.addToSparseArrayCompatBad(android.support.v4.util.SparseArrayCompat):void, 260, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [Write to container `sparseArray` via call to `put`] @@ -93,9 +92,9 @@ codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.R codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional_isMainThread_Negation_Bad():void, 168, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.conditional_isUiThread_ElseBranch_Bad():void, 162, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.confusedAssertBad(boolean):void, 191, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.mFld`] -codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.readProtectedUnthreadedBad():void, 98, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.f`,,access to `this.f`] +codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.readProtectedUnthreadedBad():void, 98, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.f`,,call to void RaceWithMainThread.main_thread_OK(),access to `this.f`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.read_unprotected_unthreaded1_Bad():void, 64, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.f1`,,access to `this.f1`] -codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.read_unprotected_unthreaded_Bad():void, 59, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.f`,,access to `this.f`] +codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.read_unprotected_unthreaded_Bad():void, 59, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.f`,,call to void RaceWithMainThread.main_thread_OK(),access to `this.f`] codetoanalyze/java/racerd/RaceWithMainThread.java, codetoanalyze.java.checkers.RaceWithMainThread.writeAfterConditionalMainThreadInCalleeBad():void, 228, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [access to `this.mSharedField`] codetoanalyze/java/racerd/ReadWriteRaces.java, codetoanalyze.java.checkers.ReadWriteRaces.callUnprotecteReadInCallee():java.lang.Object, 74, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,call to Object ReadWriteRaces.unprotectedReadInCallee(),access to `this.field1`,,access to `this.field1`] codetoanalyze/java/racerd/ReadWriteRaces.java, codetoanalyze.java.checkers.ReadWriteRaces.m1():void, 44, THREAD_SAFETY_VIOLATION, no_bucket, ERROR, [,access to `this.racy`,,access to `this.racy`]