diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 74627798b..50918e058 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -459,7 +459,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | NoEffect -> match get_summary pdesc callee_pname actuals ~f_resolve_id loc tenv with - | Some ( callee_threads, callee_locks, callee_accesses, return_attributes) -> + | Some (callee_threads, callee_locks, callee_accesses, return_attributes) -> let call_site = CallSite.make callee_pname loc in let combine_accesses_for_pre pre ~caller_accesses ~callee_accesses = let combined_accesses = @@ -467,88 +467,111 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (AccessDomain.get_accesses pre callee_accesses) call_site |> PathDomain.join (AccessDomain.get_accesses pre caller_accesses) in AccessDomain.add pre combined_accesses caller_accesses in - let combined_safe_accesses = - combine_accesses_for_pre - AccessPrecondition.Protected - ~caller_accesses:astate.accesses - ~callee_accesses in let locks' = callee_locks || astate.locks in let threads' = callee_threads || astate.threads in let astate' = - if is_unprotected locks' pdesc - then - let add_conditional_accesses index accesses_acc (actual_exp, actual_typ) = - if is_constant actual_exp - then - (* the actual is a constant, so it's owned in the caller. *) - accesses_acc - else - let callee_conditional_accesses = - PathDomain.with_callsite - (AccessDomain.get_accesses (ProtectedIf (Some index)) callee_accesses) - call_site in - begin - match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with - | Some actual_access_path -> - if is_owned actual_access_path astate.attribute_map - then - (* the actual passed to the current callee is owned. drop all the - conditional accesses for that actual, since they're all safe *) - accesses_acc - else - let base = fst actual_access_path in - begin - match FormalMap.get_formal_index base extras with - | Some formal_index -> - (* the actual passed to the current callee is rooted in a - formal. add to conditional accesses *) - PathDomain.Sinks.fold - (AccessDomain.add_access - (ProtectedIf (Some formal_index))) - (PathDomain.sinks callee_conditional_accesses) - accesses_acc - | None -> - begin - match - AttributeMapDomain.get_conditional_ownership_index - actual_access_path - astate.attribute_map - with - |(Some formal_index) -> - (* access path conditionally owned, add to - protected-if accesses *) - PathDomain.Sinks.fold - (AccessDomain.add_access - (ProtectedIf (Some formal_index))) - (PathDomain.sinks callee_conditional_accesses) - accesses_acc - | None -> - (* access path not owned and not rooted in a formal. - add to unprotected accesses *) - PathDomain.Sinks.fold - (AccessDomain.add_access - AccessPrecondition.unprotected) - (PathDomain.sinks callee_conditional_accesses) - accesses_acc - end - end - | None -> - PathDomain.Sinks.fold - (AccessDomain.add_access AccessPrecondition.unprotected) - (PathDomain.sinks callee_conditional_accesses) - accesses_acc - end in - - let unsafe_accesses = + let unprotected = is_unprotected locks' pdesc in + let add_conditional_accesses index accesses_acc (actual_exp, actual_typ) = + if is_constant actual_exp + then + (* the actual is a constant, so it's owned in the caller. *) + accesses_acc + else + let callee_conditional_accesses = + PathDomain.with_callsite + (AccessDomain.get_accesses (ProtectedIf (Some index)) callee_accesses) + call_site in + begin + match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with + | Some actual_access_path -> + if is_owned actual_access_path astate.attribute_map + then + (* the actual passed to the current callee is owned. drop all the + conditional accesses for that actual, since they're all safe *) + accesses_acc + else + let base = fst actual_access_path in + begin + match FormalMap.get_formal_index base extras with + | Some formal_index -> + let pre = + if unprotected + then AccessPrecondition.ProtectedIf (Some formal_index) + else AccessPrecondition.Protected in + (* the actual passed to the current callee is rooted in a + formal. add to conditional accesses *) + PathDomain.Sinks.fold + (AccessDomain.add_access pre) + (PathDomain.sinks callee_conditional_accesses) + accesses_acc + | None -> + begin + match + AttributeMapDomain.get_conditional_ownership_index + actual_access_path + astate.attribute_map + with + | (Some formal_index) -> + let pre = + if unprotected + then + AccessPrecondition.ProtectedIf (Some formal_index) + else + AccessPrecondition.Protected in + (* access path conditionally owned, add to protected + accesses if lock held, protected-if accesses + otherwise *) + PathDomain.Sinks.fold + (AccessDomain.add_access pre) + (PathDomain.sinks callee_conditional_accesses) + accesses_acc + | None -> + (* access path not owned and not rooted in a formal. + add to protected accesses if lock held, unprotected + accesses otherwise *) + let pre = + if unprotected + then AccessPrecondition.unprotected + else AccessPrecondition.Protected in + PathDomain.Sinks.fold + (AccessDomain.add_access pre) + (PathDomain.sinks callee_conditional_accesses) + accesses_acc + end + end + | None -> + PathDomain.Sinks.fold + (AccessDomain.add_access AccessPrecondition.unprotected) + (PathDomain.sinks callee_conditional_accesses) + accesses_acc + end in + + let combined_safe_accesses = + combine_accesses_for_pre + AccessPrecondition.Protected + ~caller_accesses:astate.accesses + ~callee_accesses in + let unsafe_accesses = + if unprotected + then combine_accesses_for_pre AccessPrecondition.unprotected ~caller_accesses:combined_safe_accesses - ~callee_accesses in - let accesses = - List.foldi ~f:add_conditional_accesses ~init:unsafe_accesses actuals in - { astate with accesses; } - else - { astate with accesses = combined_safe_accesses; } in + ~callee_accesses + else + (* add callee unsafe accesses to caller safe accesses *) + let combined_accesses = + PathDomain.with_callsite + (AccessDomain.get_accesses + AccessPrecondition.unprotected callee_accesses) call_site + |> PathDomain.join + (AccessDomain.get_accesses + AccessPrecondition.Protected combined_safe_accesses) in + AccessDomain.add + AccessPrecondition.Protected combined_accesses combined_safe_accesses in + let accesses = + List.foldi ~f:add_conditional_accesses ~init:unsafe_accesses actuals in + { astate with accesses; } in let attribute_map = propagate_return_attributes ret_opt diff --git a/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java b/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java index 58eeb5894..41c6099b6 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java +++ b/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java @@ -9,10 +9,23 @@ package codetoanalyze.java.checkers; +import java.util.concurrent.locks.ReentrantLock; import javax.annotation.concurrent.ThreadSafe; +class C { + private int x = 0; + + public int get() { + return x; + } + + public void set(int v) { + x = v; + } +} + @ThreadSafe -class ReadWriteRaces{ +class ReadWriteRaces { // read and write outside of sync races Integer safe_read; @@ -85,4 +98,15 @@ class ReadWriteRaces{ return field3; } + private final C c = new C(); + private final ReentrantLock lock = new ReentrantLock(); + + public void readInCalleeOutsideSyncBad(int i) { + if (c.get() > i) { // should report read/write race here + lock.lock(); + c.set(i); + lock.unlock(); + } + } + } diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 5acd5f3e2..8966399d4 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -66,6 +66,7 @@ codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unpro 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] +codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.readInCalleeOutsideSyncBad(int), 1, THREAD_SAFETY_VIOLATION, [call to int C.get(),access to codetoanalyze.java.checkers.C.x] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ExtendsThreadSafeExample.field] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.ExtendsThreadSafeExample.field] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void NonThreadSafeClass.threadSafeMethod(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.NonThreadSafeClass.field]