From 1ef7c253b28abbbec328ed9ca52f342be15d766d Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 7 Mar 2017 09:39:01 -0800 Subject: [PATCH] [thread-safety] report on protected write/unprotected read races Summary: Previously, we wouldn't report races where the write was under synchronization. Reviewed By: peterogithub Differential Revision: D4658850 fbshipit-source-id: e9f4c41 --- infer/src/checkers/ThreadSafety.ml | 12 +++++-- .../java/threadsafety/ReadWriteRaces.java | 33 ++++++++++++++----- .../java/threadsafety/issues.exp | 3 ++ 3 files changed, 37 insertions(+), 11 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 83fc7c502..904936a41 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -529,8 +529,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let writes = match lhs_exp with | Lfield (base_exp, _, typ) -> - if is_unprotected astate.locks (* abstracts no lock being held *) && - not (is_marked_functional rhs_exp lhs_typ astate.attribute_map) + if is_marked_functional rhs_exp lhs_typ astate.attribute_map + then + (* we want to forget about writes to @Functional fields altogether, otherwise we'll + report spurious read/write races *) + astate.writes + else if is_unprotected astate.locks then match get_formal_index base_exp typ with | Some formal_index -> @@ -853,11 +857,13 @@ let filter_conflicting_sinks sink trace = access-astate is a non-empty collection of conflicting write accesses*) let collect_conflicting_writes sink tab = + let open ThreadSafetyDomain in let procs_and_writes = List.map ~f:(fun (key,(_, _, writes, _)) -> let conflicting_writes = - get_possibly_unsafe_writes writes + AccessDomain.fold + (fun _ accesses acc -> PathDomain.join accesses acc) writes PathDomain.empty |> filter_conflicting_sinks sink in key, conflicting_writes ) diff --git a/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java b/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java index 71ba3d078..cfa7a8f50 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java +++ b/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java @@ -14,8 +14,9 @@ import javax.annotation.concurrent.ThreadSafe; @ThreadSafe class ReadWriteRaces{ -Integer safe_read; -Integer racy; + // read and write outside of sync races + Integer safe_read; + Integer racy; void m0_OK(){ Integer local; @@ -40,24 +41,40 @@ Integer racy; racy = 99; } + // write inside sync, read outside of sync races + Object field1; + Object field2; + Object field3; + // need to report races involving safe writes in order to get this one - public synchronized void FN_syncWrite1() { - racy = 42; + public synchronized void syncWrite1() { + field1 = new Object(); + } + + public Object unprotectedRead1() { + return field1; } - public void FN_syncWrite2() { + public void syncWrite2() { synchronized(this) { - racy = 43; + field2 = new Object(); } } + public Object unprotectedRead2() { + return field2; + } + private synchronized void syncWrite3() { - racy = 44; + field3 = new Object(); } - public void FN_callSyncWrite3() { + public void callSyncWrite3() { syncWrite3(); } + public Object unprotectedRead3() { + return field3; + } } diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 44ab4ee5c..ddd738682 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -48,6 +48,9 @@ codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedIn codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad2(), 2, THREAD_SAFETY_VIOLATION, [call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad3(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to codetoanalyze.java.checkers.Obj.f] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToOwnedInCalleeOk2(), 4, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.Ownership.field] +codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead1(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field1] +codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead2(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field2] +codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead3(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.field3] codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m1(), 2, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.racy] codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m2(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.racy] codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m3(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ReadWriteRaces.racy]