pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[thread-safety] classify protected-if reads/writes in callees as protected when a lock is held in the caller

Browse Source 
Summary: Fixes bug pointed out by ilyasergey, thanks!

Reviewed By: peterogithub

Differential Revision: D4736873

fbshipit-source-id: f4be32a
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent 9a07318ab7
commit e7e32b038b
3 changed files with 126 additions and 78 deletions
Show Stats Download Patch File Download Diff File

177
infer/src/checkers/ThreadSafety.ml
Unescape View File

@ -459,7 +459,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| NoEffect -> | NoEffect ->
match match
get_summary pdesc callee_pname actuals ~f_resolve_id loc tenv with 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 call_site = CallSite.make callee_pname loc in
let combine_accesses_for_pre pre ~caller_accesses ~callee_accesses = let combine_accesses_for_pre pre ~caller_accesses ~callee_accesses =
let combined_accesses = let combined_accesses =
@ -467,88 +467,111 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
(AccessDomain.get_accesses pre callee_accesses) call_site (AccessDomain.get_accesses pre callee_accesses) call_site
|> PathDomain.join (AccessDomain.get_accesses pre caller_accesses) in |> PathDomain.join (AccessDomain.get_accesses pre caller_accesses) in
AccessDomain.add pre combined_accesses 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 locks' = callee_locks || astate.locks in
let threads' = callee_threads || astate.threads in let threads' = callee_threads || astate.threads in
let astate' = let astate' =
if is_unprotected locks' pdesc let unprotected = is_unprotected locks' pdesc in
then let add_conditional_accesses index accesses_acc (actual_exp, actual_typ) =
let add_conditional_accesses index accesses_acc (actual_exp, actual_typ) = if is_constant actual_exp
if is_constant actual_exp then
then (* the actual is a constant, so it's owned in the caller. *)
(* the actual is a constant, so it's owned in the caller. *) accesses_acc
accesses_acc else
else let callee_conditional_accesses =
let callee_conditional_accesses = PathDomain.with_callsite
PathDomain.with_callsite (AccessDomain.get_accesses (ProtectedIf (Some index)) callee_accesses)
(AccessDomain.get_accesses (ProtectedIf (Some index)) callee_accesses) call_site in
call_site in begin
begin match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with
match AccessPath.of_lhs_exp actual_exp actual_typ ~f_resolve_id with | Some actual_access_path ->
| Some actual_access_path -> if is_owned actual_access_path astate.attribute_map
if is_owned actual_access_path astate.attribute_map then
then (* the actual passed to the current callee is owned. drop all the
(* the actual passed to the current callee is owned. drop all the conditional accesses for that actual, since they're all safe *)
conditional accesses for that actual, since they're all safe *) accesses_acc
accesses_acc else
else let base = fst actual_access_path in
let base = fst actual_access_path in begin
begin match FormalMap.get_formal_index base extras with
match FormalMap.get_formal_index base extras with | Some formal_index ->
| Some formal_index -> let pre =
(* the actual passed to the current callee is rooted in a if unprotected
formal. add to conditional accesses *) then AccessPrecondition.ProtectedIf (Some formal_index)
PathDomain.Sinks.fold else AccessPrecondition.Protected in
(AccessDomain.add_access (* the actual passed to the current callee is rooted in a
(ProtectedIf (Some formal_index))) formal. add to conditional accesses *)
(PathDomain.sinks callee_conditional_accesses) PathDomain.Sinks.fold
accesses_acc (AccessDomain.add_access pre)
| None -> (PathDomain.sinks callee_conditional_accesses)
begin accesses_acc
match | None ->
AttributeMapDomain.get_conditional_ownership_index begin
actual_access_path match
astate.attribute_map AttributeMapDomain.get_conditional_ownership_index
with actual_access_path
|(Some formal_index) -> astate.attribute_map
(* access path conditionally owned, add to with
protected-if accesses *) | (Some formal_index) ->
PathDomain.Sinks.fold let pre =
(AccessDomain.add_access if unprotected
(ProtectedIf (Some formal_index))) then
(PathDomain.sinks callee_conditional_accesses) AccessPrecondition.ProtectedIf (Some formal_index)
accesses_acc else
| None -> AccessPrecondition.Protected in
(* access path not owned and not rooted in a formal. (* access path conditionally owned, add to protected
add to unprotected accesses *) accesses if lock held, protected-if accesses
PathDomain.Sinks.fold otherwise *)
(AccessDomain.add_access PathDomain.Sinks.fold
AccessPrecondition.unprotected) (AccessDomain.add_access pre)
(PathDomain.sinks callee_conditional_accesses) (PathDomain.sinks callee_conditional_accesses)
accesses_acc accesses_acc
end | None ->
end (* access path not owned and not rooted in a formal.
| None -> add to protected accesses if lock held, unprotected
PathDomain.Sinks.fold accesses otherwise *)
(AccessDomain.add_access AccessPrecondition.unprotected) let pre =
(PathDomain.sinks callee_conditional_accesses) if unprotected
accesses_acc then AccessPrecondition.unprotected
end in else AccessPrecondition.Protected in
PathDomain.Sinks.fold
let unsafe_accesses = (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 combine_accesses_for_pre
AccessPrecondition.unprotected AccessPrecondition.unprotected
~caller_accesses:combined_safe_accesses ~caller_accesses:combined_safe_accesses
~callee_accesses in ~callee_accesses
let accesses = else
List.foldi ~f:add_conditional_accesses ~init:unsafe_accesses actuals in (* add callee unsafe accesses to caller safe accesses *)
{ astate with accesses; } let combined_accesses =
else PathDomain.with_callsite
{ astate with accesses = combined_safe_accesses; } in (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 = let attribute_map =
propagate_return_attributes propagate_return_attributes
ret_opt ret_opt

26
infer/tests/codetoanalyze/java/threadsafety/ReadWriteRaces.java
Unescape View File

@ -9,10 +9,23 @@
package codetoanalyze.java.checkers; package codetoanalyze.java.checkers;
import java.util.concurrent.locks.ReentrantLock;
import javax.annotation.concurrent.ThreadSafe; import javax.annotation.concurrent.ThreadSafe;
class C {
private int x = 0;
public int get() {
return x;
}
public void set(int v) {
x = v;
}
}
@ThreadSafe @ThreadSafe
class ReadWriteRaces{ class ReadWriteRaces {
// read and write outside of sync races // read and write outside of sync races
Integer safe_read; Integer safe_read;
@ -85,4 +98,15 @@ class ReadWriteRaces{
return field3; 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();
}
}
} }

1
infer/tests/codetoanalyze/java/threadsafety/issues.exp
Unescape View File

@ -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.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.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.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.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 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] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void NonThreadSafeClass.threadSafeMethod(), 1, THREAD_SAFETY_VIOLATION, [access to codetoanalyze.java.checkers.NonThreadSafeClass.field]

Write Preview
Loading…
Cancel
Save