From ea8826599f970ea4ab178699a9be7c476bbf4a2e Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 7 Mar 2017 09:05:33 -0800 Subject: [PATCH] [thread-safety] track protected writes Summary: Step 1 (this diff): track protected writes Step 2 (next diff): in the read/write race reporting, take protected writes into consideration when reporting Reviewed By: peterogithub Differential Revision: D4620257 fbshipit-source-id: e94f4ca --- infer/src/checkers/ThreadSafety.ml | 57 +++++++++++-------- .../java/threadsafety/ReadWriteRaces.java | 20 +++++++ 2 files changed, 54 insertions(+), 23 deletions(-) diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 3b92e53c4..83fc7c502 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -160,7 +160,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct attribute_map let add_path_to_state exp typ loc path_state id_map attribute_map tenv = - (* we don't want to warn on writes to the field if it is (a) thread-confined, or (b) volatile *) let is_safe_write access_path tenv = let is_thread_safe_write accesses tenv = @@ -371,11 +370,22 @@ module TransferFunctions (CFG : ProcCfg.S) = struct callee_reads, callee_writes, return_attributes) -> + let call_site = CallSite.make callee_pname loc in + let combine_accesses_for_pre pre ~caller_accesses ~callee_accesses = + let combined_accesses = + PathDomain.with_callsite + (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_writes = + combine_accesses_for_pre + AccessPrecondition.Protected + ~caller_accesses:astate.writes + ~callee_accesses:callee_writes in let locks' = callee_locks || astate.locks in let astate' = if is_unprotected locks' then - let call_site = CallSite.make callee_pname loc in let add_conditional_writes index writes_acc (actual_exp, actual_typ) = if is_constant actual_exp then @@ -424,26 +434,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let reads = PathDomain.with_callsite callee_reads call_site |> PathDomain.join astate.reads in - let combined_unsafe_writes = - PathDomain.with_callsite - (AccessDomain.get_accesses AccessPrecondition.unprotected callee_writes) - call_site - |> PathDomain.join - (AccessDomain.get_accesses - AccessPrecondition.unprotected astate.writes) in - let writes_with_unsafe = - AccessDomain.add + let unsafe_writes = + combine_accesses_for_pre AccessPrecondition.unprotected - combined_unsafe_writes - astate.writes in + ~caller_accesses:combined_safe_writes + ~callee_accesses:callee_writes in let writes = - List.foldi - ~f:add_conditional_writes - ~init:writes_with_unsafe - actuals in + List.foldi ~f:add_conditional_writes ~init:unsafe_writes actuals in { astate with reads; writes; } else - astate in + { astate with writes = combined_safe_writes; } in let attribute_map = propagate_return_attributes ret_opt @@ -528,10 +528,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct false in let writes = match lhs_exp with - | Lfield (base_exp, _, typ) - when is_unprotected astate.locks (* abstracts no lock being held *) && - not (is_marked_functional rhs_exp lhs_typ astate.attribute_map) -> - begin + | 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) + then match get_formal_index base_exp typ with | Some formal_index -> let pre = AccessPrecondition.ProtectedIf (Some formal_index) in @@ -560,7 +560,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct astate.attribute_map tenv in AccessDomain.add AccessPrecondition.unprotected unsafe_writes' astate.writes - end + else + let safe_writes = AccessDomain.get_accesses Protected astate.writes in + let safe_writes' = + add_path_to_state + lhs_exp + typ + loc + safe_writes + astate.id_map + astate.attribute_map + tenv in + AccessDomain.add Protected safe_writes' astate.writes | _ -> astate.writes in let attribute_map = diff --git a/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java b/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java index f5f85488e..71ba3d078 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java +++ b/infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java @@ -40,4 +40,24 @@ Integer racy; racy = 99; } + // need to report races involving safe writes in order to get this one + public synchronized void FN_syncWrite1() { + racy = 42; + } + + public void FN_syncWrite2() { + synchronized(this) { + racy = 43; + } + } + + private synchronized void syncWrite3() { + racy = 44; + } + + public void FN_callSyncWrite3() { + syncWrite3(); + } + + }