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

[racerd] generalize access preconditions

Browse Source 
Summary:
Previously, we could understand than an access was safe either because it was possibly owned or protected by a thread/lock, but not both. If an access was both protected by a lock and rooted in a paramer (i.e., possibly owned), we would forget the ownership part of the precondition and remember only the lock bit. This leads to false positives in cases where an access protected by a lock is owned, but another unowned access to the same memory is not protected by a lock (see the new `unownedLockedWriteOk` E2E test for an example).

This diff makes access safety conditions disjunctive so we can simultaneously track whether an access is owned and whether an access is protected by a thread/lock. This will fix false positives like the one explained in T24015160.

Reviewed By: jberdine

Differential Revision: D6671489

fbshipit-source-id: d17715f
master
Sam Blackshear 7 years ago committed by Facebook Github Bot
parent 8a9fcdc43f
commit 268e0b9b5f
7 changed files with 266 additions and 201 deletions
Show Stats Download Patch File Download Diff File

251
infer/src/concurrency/RacerD.ml
Unescape View File

@ -161,7 +161,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
&& not (has_return_annot thread_safe_or_thread_confined pname) && not (has_return_annot thread_safe_or_thread_confined pname)
then then
let open Domain in let open Domain in
let pre = AccessPrecondition.make_protected locks threads proc_data.pdesc in let pre = AccessData.make locks threads False proc_data.pdesc in
AccessDomain.add_access pre (TraceElem.make_unannotated_call_access pname loc) attribute_map AccessDomain.add_access pre (TraceElem.make_unannotated_call_access pname loc) attribute_map
else attribute_map else attribute_map
@ -208,17 +208,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
if is_safe_access access prefix_path proc_data.tenv then if is_safe_access access prefix_path proc_data.tenv then
add_field_accesses prefix_path' access_acc access_list add_field_accesses prefix_path' access_acc access_list
else else
match AccessPrecondition.make_protected locks threads proc_data.pdesc with
| AccessPrecondition.Protected _ as excluder ->
add_field_access excluder
| _ ->
match OwnershipDomain.get_owned prefix_path ownership with match OwnershipDomain.get_owned prefix_path ownership with
| OwnershipAbstractValue.OwnedIf formal_indexes -> | OwnershipAbstractValue.OwnedIf formal_indexes ->
add_field_access (AccessPrecondition.make_unprotected formal_indexes) let pre =
AccessData.make locks threads
(AccessData.Precondition.Conjunction formal_indexes) proc_data.pdesc
in
add_field_access pre
| OwnershipAbstractValue.Owned -> | OwnershipAbstractValue.Owned ->
add_field_accesses prefix_path' access_acc access_list add_field_accesses prefix_path' access_acc access_list
| OwnershipAbstractValue.Unowned -> | OwnershipAbstractValue.Unowned ->
add_field_access AccessPrecondition.totally_unprotected let pre = AccessData.make locks threads False proc_data.pdesc in
add_field_access pre
in in
List.fold List.fold
~f:(fun acc (base, accesses) -> ~f:(fun acc (base, accesses) ->
@ -339,7 +340,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
false false
let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv = let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc
(astate: Domain.astate) =
(* create a dummy write that represents mutating the contents of the container *) (* create a dummy write that represents mutating the contents of the container *)
let open Domain in let open Domain in
let callee_accesses = let callee_accesses =
@ -348,9 +350,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let container_access = let container_access =
TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc
in in
AccessDomain.add_access let pre =
(AccessPrecondition.make_unprotected (IntSet.singleton 0)) AccessData.make astate.locks astate.threads
container_access AccessDomain.empty (AccessData.Precondition.Conjunction (IntSet.singleton 0)) caller_pdesc
in
AccessDomain.add_access pre container_access AccessDomain.empty
in in
(* if a container c is owned in cpp, make c[i] owned for all i *) (* if a container c is owned in cpp, make c[i] owned for all i *)
let return_ownership = let return_ownership =
@ -368,7 +372,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
; return_attributes= AttributeSetDomain.empty } ; return_attributes= AttributeSetDomain.empty }
let get_summary caller_pdesc callee_pname actuals callee_loc tenv = let get_summary caller_pdesc callee_pname actuals callee_loc tenv (astate: Domain.astate) =
let open RacerDConfig in let open RacerDConfig in
let get_receiver_ap actuals = let get_receiver_ap actuals =
match List.hd actuals with match List.hd actuals with
@ -382,9 +386,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
match (Models.get_container_access callee_pname tenv, callee_pname) with match (Models.get_container_access callee_pname tenv, callee_pname) with
| Some ContainerWrite, _ -> | Some ContainerWrite, _ ->
make_container_access callee_pname ~is_write:true (get_receiver_ap actuals) callee_loc tenv make_container_access callee_pname ~is_write:true (get_receiver_ap actuals) callee_loc tenv
caller_pdesc astate
| Some ContainerRead, _ -> | Some ContainerRead, _ ->
make_container_access callee_pname ~is_write:false (get_receiver_ap actuals) callee_loc make_container_access callee_pname ~is_write:false (get_receiver_ap actuals) callee_loc
tenv tenv caller_pdesc astate
| None, _ -> | None, _ ->
Summary.read_summary caller_pdesc callee_pname Summary.read_summary caller_pdesc callee_pname
@ -459,6 +464,84 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
AccessDomain.map expand_pre accesses AccessDomain.map expand_pre accesses
let add_callee_accesses (caller_astate: Domain.astate) accesses locks threads actuals
callee_pname pdesc loc =
let open Domain in
let update_caller_accesses pre callee_accesses caller_accesses =
let combined_accesses =
PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc)
|> PathDomain.join (AccessDomain.get_accesses pre caller_accesses)
in
AccessDomain.add pre combined_accesses caller_accesses
in
let conjoin_ownership_pre actual_exp actual_indexes : AccessData.Precondition.t =
match actual_exp with
| HilExp.Constant _ ->
(* the actual is a constant, so it's owned in the caller. *)
Conjunction actual_indexes
| HilExp.AccessPath actual_access_path
-> (
if OwnershipDomain.is_owned actual_access_path caller_astate.ownership then
(* the actual passed to the current callee is owned. drop all the conditional accesses
for that actual, since they're all safe *)
Conjunction actual_indexes
else
let base = fst actual_access_path in
match OwnershipDomain.get_owned (base, []) caller_astate.ownership with
| OwnedIf formal_indexes ->
(* the actual passed to the current callee is rooted in a formal *)
Conjunction (IntSet.union formal_indexes actual_indexes)
| Unowned | Owned ->
match OwnershipDomain.get_owned actual_access_path caller_astate.ownership with
| OwnedIf formal_indexes ->
(* access path conditionally owned if [formal_indexes] are owned *)
Conjunction (IntSet.union formal_indexes actual_indexes)
| Owned ->
assert false
| Unowned ->
(* access path not rooted in a formal and not conditionally owned *)
False )
| _ ->
(* couldn't find access path, don't know if it's owned. assume not *)
False
in
let update_ownership_pre actual_index (acc: AccessData.Precondition.t) =
match acc with
| False ->
(* precondition can't be satisfied *)
acc
| Conjunction actual_indexes ->
match List.nth actuals actual_index with
| Some actual ->
conjoin_ownership_pre actual actual_indexes
| None ->
L.internal_error "Bad actual index %d for callee %a with %d actuals." actual_index
Typ.Procname.pp callee_pname (List.length actuals) ;
acc
in
let update_accesses (pre: AccessData.t) callee_accesses accesses_acc =
(* update precondition with caller ownership info *)
let ownership_precondition' =
match pre.ownership_precondition with
| Conjunction indexes ->
let empty_pre = AccessData.Precondition.Conjunction IntSet.empty in
IntSet.fold update_ownership_pre indexes empty_pre
| False ->
pre.ownership_precondition
in
if AccessData.Precondition.is_true ownership_precondition' then accesses_acc
else
let locks' = locks || pre.lock in
(* if the access occurred on a main thread in the callee, we should remember this when
moving it to the callee. if we don't know what thread it ran on, use the caller's
thread *)
let threads' = if pre.thread then ThreadsDomain.AnyThreadButSelf else threads in
let pre' = AccessData.make locks' threads' ownership_precondition' pdesc in
update_caller_accesses pre' callee_accesses accesses_acc
in
AccessDomain.fold update_accesses accesses caller_astate.accesses
let exec_instr (astate: Domain.astate) ({ProcData.tenv; extras; pdesc} as proc_data) _ let exec_instr (astate: Domain.astate) ({ProcData.tenv; extras; pdesc} as proc_data) _
(instr: HilInstr.t) = (instr: HilInstr.t) =
let open Domain in let open Domain in
@ -537,7 +620,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
"Procedure %a specified as returning boolean, but returns nothing" "Procedure %a specified as returning boolean, but returns nothing"
Typ.Procname.pp callee_pname ) Typ.Procname.pp callee_pname )
| NoEffect -> | NoEffect ->
let summary_opt = get_summary pdesc callee_pname actuals loc tenv in let summary_opt = get_summary pdesc callee_pname actuals loc tenv astate in
let callee_pdesc = extras callee_pname in let callee_pdesc = extras callee_pname in
match match
Option.map summary_opt ~f:(fun summary -> Option.map summary_opt ~f:(fun summary ->
@ -548,13 +631,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
{summary with accesses= rebased_accesses} ) {summary with accesses= rebased_accesses} )
with with
| Some {threads; locks; accesses; return_ownership; return_attributes} -> | Some {threads; locks; accesses; return_ownership; return_attributes} ->
let update_caller_accesses pre callee_accesses caller_accesses =
let combined_accesses =
PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc)
|> PathDomain.join (AccessDomain.get_accesses pre caller_accesses)
in
AccessDomain.add pre combined_accesses caller_accesses
in
let locks = locks || astate.locks in let locks = locks || astate.locks in
let threads = let threads =
match (astate.threads, threads) with match (astate.threads, threads) with
@ -565,73 +641,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| _ -> | _ ->
ThreadsDomain.join threads astate.threads ThreadsDomain.join threads astate.threads
in in
(* add [ownership_accesses] to the [accesses_acc] with a protected pre if
[exp] is owned, and an appropriate unprotected pre otherwise *)
let add_ownership_access ownership_accesses actual_exp accesses_acc =
match actual_exp with
| HilExp.Constant _ ->
(* the actual is a constant, so it's owned in the caller. *)
accesses_acc
| HilExp.AccessPath actual_access_path ->
if OwnershipDomain.is_owned actual_access_path astate.ownership 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 pre =
match AccessPrecondition.make_protected locks threads pdesc with
| AccessPrecondition.Protected _ as excluder (* access protected *) ->
excluder
| _ ->
let base = fst actual_access_path in
match OwnershipDomain.get_owned (base, []) astate.ownership with
| OwnershipAbstractValue.OwnedIf formal_indexes ->
(* the actual passed to the current callee is rooted in a
formal *)
AccessPrecondition.make_unprotected formal_indexes
| OwnershipAbstractValue.Unowned | OwnershipAbstractValue.Owned ->
match
OwnershipDomain.get_owned actual_access_path astate.ownership
with
| OwnershipAbstractValue.OwnedIf formal_indexes ->
(* access path conditionally owned if [formal_indexes] are
owned *)
AccessPrecondition.make_unprotected formal_indexes
| OwnershipAbstractValue.Owned ->
assert false
| OwnershipAbstractValue.Unowned ->
(* access path not rooted in a formal and not conditionally
owned *)
AccessPrecondition.totally_unprotected
in
update_caller_accesses pre ownership_accesses accesses_acc
| _ ->
(* couldn't find access path, don't know if it's owned *)
update_caller_accesses AccessPrecondition.totally_unprotected
ownership_accesses accesses_acc
in
let accesses = let accesses =
let update_accesses pre callee_accesses accesses_acc = add_callee_accesses astate accesses locks threads actuals callee_pname pdesc
match pre with loc
| AccessPrecondition.Protected _ ->
update_caller_accesses pre callee_accesses accesses_acc
| AccessPrecondition.TotallyUnprotected ->
let pre' = AccessPrecondition.make_protected locks threads pdesc in
update_caller_accesses pre' callee_accesses accesses_acc
| AccessPrecondition.Unprotected formal_indexes ->
IntSet.fold
(fun index acc ->
match List.nth actuals index with
| Some actual ->
add_ownership_access callee_accesses actual acc
| None ->
L.internal_error
"Bad actual index %d for callee %a with %d actuals." index
Typ.Procname.pp callee_pname (List.length actuals) ;
acc )
formal_indexes accesses_acc
in
AccessDomain.fold update_accesses accesses astate.accesses
in in
let ownership, attribute_map = let ownership, attribute_map =
propagate_return ret_opt return_ownership return_attributes actuals astate propagate_return ret_opt return_ownership return_attributes actuals astate
@ -1255,7 +1267,7 @@ let make_unprotected_write_description pname final_sink_site initial_sink_site f
type reported_access = type reported_access =
{ access: RacerDDomain.TraceElem.t { access: RacerDDomain.TraceElem.t
; threads: RacerDDomain.ThreadsDomain.astate ; threads: RacerDDomain.ThreadsDomain.astate
; precondition: RacerDDomain.AccessPrecondition.t ; precondition: RacerDDomain.AccessData.t
; tenv: Tenv.t ; tenv: Tenv.t
; procdesc: Procdesc.t } ; procdesc: Procdesc.t }
@ -1370,20 +1382,17 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
let pname = Procdesc.get_proc_name procdesc in let pname = Procdesc.get_proc_name procdesc in
if is_duplicate_report access pname reported_acc then reported_acc if is_duplicate_report access pname reported_acc then reported_acc
else else
match (TraceElem.kind access, precondition) with match TraceElem.kind access with
| ( Access.InterfaceCall unannoted_call_pname | Access.InterfaceCall unannoted_call_pname ->
, (AccessPrecondition.Unprotected _ | AccessPrecondition.TotallyUnprotected) ) -> if AccessData.is_unprotected precondition && ThreadsDomain.is_any threads
if ThreadsDomain.is_any threads && is_marked_thread_safe procdesc tenv then ( && is_marked_thread_safe procdesc tenv
then (
(* un-annotated interface call + no lock in method marked thread-safe. warn *) (* un-annotated interface call + no lock in method marked thread-safe. warn *)
report_unannotated_interface_violation tenv procdesc access threads report_unannotated_interface_violation tenv procdesc access threads
unannoted_call_pname ; unannoted_call_pname ;
update_reported access pname reported_acc ) update_reported access pname reported_acc )
else reported_acc else reported_acc
| Access.InterfaceCall _, AccessPrecondition.Protected _ -> | Access.Write _ | ContainerWrite _ -> (
(* un-annotated interface call, but it's protected by a lock/thread. don't report *)
reported_acc
| ( (Access.Write _ | ContainerWrite _)
, (AccessPrecondition.Unprotected _ | AccessPrecondition.TotallyUnprotected) ) -> (
match Procdesc.get_proc_name procdesc with match Procdesc.get_proc_name procdesc with
| Java _ -> | Java _ ->
let writes_on_background_thread = let writes_on_background_thread =
@ -1401,7 +1410,8 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
else None ) else None )
accesses accesses
in in
if not (List.is_empty writes_on_background_thread && not (ThreadsDomain.is_any threads)) if AccessData.is_unprotected precondition
&& (not (List.is_empty writes_on_background_thread) || ThreadsDomain.is_any threads)
then then
let conflict = List.hd writes_on_background_thread in let conflict = List.hd writes_on_background_thread in
report_thread_safety_violation tenv procdesc report_thread_safety_violation tenv procdesc
@ -1413,19 +1423,11 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
(* Do not report unprotected writes when an access can't run in parallel with itself, or (* Do not report unprotected writes when an access can't run in parallel with itself, or
for ObjC_Cpp *) for ObjC_Cpp *)
reported_acc ) reported_acc )
| (Access.Write _ | ContainerWrite _), AccessPrecondition.Protected _ -> | (Access.Read _ | ContainerRead _) when AccessData.is_unprotected precondition ->
(* protected write, do nothing *)
reported_acc
| ( (Access.Read _ | ContainerRead _)
, (AccessPrecondition.Unprotected _ | AccessPrecondition.TotallyUnprotected) ) ->
(* unprotected read. report all writes as conflicts for java. for c++ filter out (* unprotected read. report all writes as conflicts for java. for c++ filter out
unprotected writes *) unprotected writes *)
let is_cpp_protected_write pre = let is_cpp_protected_write pre =
match pre with Typ.Procname.is_java pname || not (AccessData.is_unprotected pre)
| AccessPrecondition.Unprotected _ | TotallyUnprotected ->
Typ.Procname.is_java pname
| AccessPrecondition.Protected _ ->
true
in in
let is_conflict other_access pre other_thread = let is_conflict other_access pre other_thread =
TraceElem.is_write other_access TraceElem.is_write other_access
@ -1447,27 +1449,24 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi
~report_kind:(ReadWriteRace conflict.access) access threads ; ~report_kind:(ReadWriteRace conflict.access) access threads ;
update_reported access pname reported_acc update_reported access pname reported_acc
else reported_acc else reported_acc
| (Access.Read _ | ContainerRead _), AccessPrecondition.Protected excl -> | Access.Read _ | ContainerRead _ ->
(* protected read. report unprotected writes and opposite protected writes as conflicts (* protected read. report unprotected writes and opposite protected writes as conflicts *)
Thread and Lock are opposites of one another, and Both has no opposite *) let can_conflict (pre1: AccessData.t) (pre2: AccessData.t) =
let is_opposite = function if pre1.lock && pre2.lock then false
| Excluder.Lock, Excluder.Thread -> else if pre1.thread && pre2.thread then false
true else true
| Excluder.Thread, Excluder.Lock ->
true
| _, _ ->
false
in in
let conflicting_writes = let conflicting_writes =
List.filter List.filter
~f:(fun {access; precondition; threads= other_threads} -> ~f:
TraceElem.is_write access (fun { access= other_access
&& ; precondition= other_precondition
match precondition with ; threads= other_threads } ->
| Unprotected _ | TotallyUnprotected -> if AccessData.is_unprotected other_precondition then
ThreadsDomain.is_any other_threads TraceElem.is_write other_access && ThreadsDomain.is_any other_threads
| Protected other_excl -> else
is_opposite (excl, other_excl) ) TraceElem.is_write other_access && can_conflict precondition other_precondition
)
accesses accesses
in in
if not (List.is_empty conflicting_writes) then if not (List.is_empty conflicting_writes) then

58
infer/src/concurrency/RacerDDomain.ml
Unescape View File

@ -361,55 +361,43 @@ module AttributeMapDomain = struct
add access_path attribute_set t add access_path attribute_set t
end end
module Excluder = struct module AccessData = struct
type t = Thread | Lock | Both [@@deriving compare] module Precondition = struct
type t = Conjunction of IntSet.t | False [@@deriving compare]
let pp fmt = function (* precondition is true if the conjunction of owned indexes is empty *)
| Thread -> let is_true = function False -> false | Conjunction set -> IntSet.is_empty set
F.fprintf fmt "Thread"
| Lock ->
F.fprintf fmt "Lock"
| Both ->
F.fprintf fmt "both Thread and Lock"
end
module AccessPrecondition = struct
type t =
| Protected of Excluder.t
| Unprotected of IntSet.t
| TotallyUnprotected
[@@deriving compare]
let pp fmt = function let pp fmt = function
| Protected excl -> | Conjunction indexes ->
F.fprintf fmt "ProtectedBy(%a)" Excluder.pp excl F.fprintf fmt "Owned(%a)"
| TotallyUnprotected ->
F.fprintf fmt "TotallyUnprotected"
| Unprotected indexes ->
F.fprintf fmt "Unprotected(%a)"
(PrettyPrintable.pp_collection ~pp_item:Int.pp) (PrettyPrintable.pp_collection ~pp_item:Int.pp)
(IntSet.elements indexes) (IntSet.elements indexes)
| False ->
F.fprintf fmt "False"
end
type t = {thread: bool; lock: bool; ownership_precondition: Precondition.t} [@@deriving compare]
let make_protected locks thread pdesc = let make locks threads ownership_precondition pdesc =
let is_main_thread = ThreadsDomain.is_any_but_self thread in (* shouldn't be creating metadata for accesses that are known to be owned; we should discard
let locked = locks || Procdesc.is_java_synchronized pdesc in such accesses *)
if not locked && not is_main_thread then TotallyUnprotected assert (not (Precondition.is_true ownership_precondition)) ;
else if locked && is_main_thread then Protected Excluder.Both let thread = ThreadsDomain.is_any_but_self threads in
else if locked then Protected Excluder.Lock let lock = locks || Procdesc.is_java_synchronized pdesc in
else Protected Excluder.Thread {thread; lock; ownership_precondition}
let make_unprotected indexes = let is_unprotected {thread; lock; ownership_precondition} =
assert (not (IntSet.is_empty indexes)) ; not thread && not lock && not (Precondition.is_true ownership_precondition)
Unprotected indexes
let totally_unprotected = TotallyUnprotected let pp fmt {thread; lock; ownership_precondition} =
F.fprintf fmt "Thread: %b Lock: %b Pre: %a" thread lock Precondition.pp ownership_precondition
end end
module AccessDomain = struct module AccessDomain = struct
include AbstractDomain.Map (AccessPrecondition) (PathDomain) include AbstractDomain.Map (AccessData) (PathDomain)
let add_access precondition access_path t = let add_access precondition access_path t =
let precondition_accesses = try find precondition t with Not_found -> PathDomain.empty in let precondition_accesses = try find precondition t with Not_found -> PathDomain.empty in

52
infer/src/concurrency/RacerDDomain.mli
Unescape View File

@ -141,48 +141,44 @@ module AttributeMapDomain : sig
val add_attribute : AccessPath.t -> Attribute.t -> astate -> astate val add_attribute : AccessPath.t -> Attribute.t -> astate -> astate
end end
(** Excluders: Two things can provide for mutual exclusion: holding a lock, (** Data shared among a set of accesses: current thread, lock(s) held, ownership precondition *)
and knowing that you are on a particular thread. Here, we module AccessData : sig
abstract it to "some" lock and "any particular" thread (typically, UI thread) (** Precondition for owned access; access is owned if it evaluates to ture *)
For a more precide semantics we would replace Thread by representatives of module Precondition : sig
thread id's and Lock by multiple differnet lock id's. type t =
Both indicates that you both know the thread and hold a lock. | Conjunction of IntSet.t
There is no need for a lattice relation between Thread, Lock and Both: (** Conjunction of "formal index must be owned" predicates.
you don't ever join Thread and Lock, rather, they are treated pointwise. true if empty *)
**) | False
module Excluder : sig [@@deriving compare]
type t = Thread | Lock | Both [@@deriving compare]
val is_true : t -> bool
(** return [true] if the precondition evaluates to true *)
val pp : F.formatter -> t -> unit [@@warning "-32"]
end end
module AccessPrecondition : sig
type t = private type t = private
| Protected of Excluder.t {thread: bool; lock: bool; ownership_precondition: Precondition.t}
(** access potentially protected for mutual exclusion by
lock or thread or both *)
| Unprotected of IntSet.t
(** access rooted in formal(s) at indexes i. Safe if actuals passed at given indexes are
owned (i.e., !owned(i) implies an unsafe access). *)
| TotallyUnprotected (** access is unsafe unless a lock is held in a caller *)
[@@deriving compare] [@@deriving compare]
val pp : F.formatter -> t -> unit val make : LocksDomain.astate -> ThreadsDomain.astate -> Precondition.t -> Procdesc.t -> t
val make_protected : LocksDomain.astate -> ThreadsDomain.astate -> Procdesc.t -> t
val make_unprotected : IntSet.t -> t val is_unprotected : t -> bool
(** return true if not protected by lock, thread, or ownership *)
val totally_unprotected : t val pp : F.formatter -> t -> unit
end end
(** map of access precondition |-> set of accesses. the map should hold all accesses to a (** map of access metadata |-> set of accesses. the map should hold all accesses to a
possibly-unowned access path *) possibly-unowned access path *)
module AccessDomain : sig module AccessDomain : sig
include module type of AbstractDomain.Map (AccessPrecondition) (PathDomain) include module type of AbstractDomain.Map (AccessData) (PathDomain)
val add_access : AccessPrecondition.t -> TraceElem.t -> astate -> astate val add_access : AccessData.t -> TraceElem.t -> astate -> astate
(** add the given (access, precondition) pair to the map *) (** add the given (access, precondition) pair to the map *)
val get_accesses : AccessPrecondition.t -> astate -> PathDomain.astate val get_accesses : AccessData.t -> astate -> PathDomain.astate
(** get all accesses with the given precondition *) (** get all accesses with the given precondition *)
end end

13
infer/tests/codetoanalyze/java/racerd/Dispatch.java
Unescape View File

@ -75,4 +75,17 @@ public class Dispatch {
t.foo(); t.foo();
} }
public void callUnderLock(AnnotatedInterface i) {
synchronized(this) {
i.foo();
}
}
}
class Some {
void callFromElsewhere(Dispatch d, AnnotatedInterface i) {
d.callUnderLock(i);
}
} }

32
infer/tests/codetoanalyze/java/racerd/Locks.java
Unescape View File

@ -18,7 +18,6 @@ import java.util.concurrent.locks.ReentrantReadWriteLock;
@ThreadSafe @ThreadSafe
public class Locks { public class Locks {
Integer f; Integer f;
Lock mLock; Lock mLock;
@ -233,4 +232,35 @@ public class Locks {
} }
} }
Object mField2;
private synchronized void lockedWriteInCallee() {
this.mField2 = null;
}
public static void ownedLockedReadOk() {
Locks owned = new Locks();
owned.lockedWriteInCallee();
}
public Object unownedReadOk() {
// safe because the only other access to mField is owned
return this.mField2;
}
Object mField3;
private synchronized void lockedWriteInCallee2() {
this.mField3 = null;
}
public void unownedLockedWriteOk() {
lockedWriteInCallee2();
}
public Object unownedReadBad() {
return this.mField3;
}
} }

36
infer/tests/codetoanalyze/java/racerd/RaceWithMainThread.java
Unescape View File

@ -199,8 +199,44 @@ class RaceWithMainThread{
mFld = null; mFld = null;
} }
int mOnlyWrittenOnMain;
private void conditionalMainThreadWrite1(boolean b) {
if (b) {
OurThreadUtil.assertOnUiThread();
mOnlyWrittenOnMain = 7;
}
}
// make sure we don't forget what thread the callee write occurred on
public void conditionalMainThreadWriteOk() {
conditionalMainThreadWrite1(true);
} }
int mWrittenOffMain;
private void conditionalMainThreadWrite2(boolean b) {
if (b) {
OurThreadUtil.assertOnUiThread();
} else {
mOnlyWrittenOnMain = 7;
}
}
public void conditionalMainThreadWriteBad() {
conditionalMainThreadWrite2(false);
}
int mSharedField;
public void writeAfterConditionalMainThreadInCalleeBad() {
conditionalMainThreadWrite1(true);
// one branch of the callee runs on the main thread, but that doesn't mean we can assume that
// the caller does too
mSharedField = 7;
}
}
// not marked thread-safe // not marked thread-safe
class Unmarked { class Unmarked {

3
infer/tests/codetoanalyze/java/racerd/issues.exp
Unescape View File

@ -53,6 +53,7 @@ codetoanalyze/java/racerd/Dispatch.java, void Dispatch.callUnannotatedInterfaceI
codetoanalyze/java/racerd/Inference.java, int Inference.read4OutsideSyncBad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField4`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField4`] codetoanalyze/java/racerd/Inference.java, int Inference.read4OutsideSyncBad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField4`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField4`]
codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead1Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField1`] codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead1Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField1`]
codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead2Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField2`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField2`] codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead2Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField2`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Inference.mField2`]
codetoanalyze/java/racerd/Locks.java, Object Locks.unownedReadBad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField3`,<Write trace>,call to void Locks.lockedWriteInCallee2(),access to `&this.codetoanalyze.java.checkers.Locks.mField3`]
codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock1Bad(), 3, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`] codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock1Bad(), 3, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`]
codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock2Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`] codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock2Bad(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Locks.mField`]
codetoanalyze/java/racerd/Locks.java, void Locks.FP_unlockOneLock(), 4, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/racerd/Locks.java, void Locks.FP_unlockOneLock(), 4, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`]
@ -82,6 +83,7 @@ codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToNotOwnedInCallee
codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad3(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to `&formal.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad3(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to `&formal.codetoanalyze.java.checkers.Obj.f`]
codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToOwnedInCalleeOk2(), 4, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Ownership.field`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Ownership.field`] codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToOwnedInCalleeOk2(), 4, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.Ownership.field`,<Write trace>,access to `&this.codetoanalyze.java.checkers.Ownership.field`]
codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional2_bad(boolean), 6, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional2_bad(boolean), 6, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`]
codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditionalMainThreadWriteBad(), 1, THREAD_SAFETY_VIOLATION, [call to void RaceWithMainThread.conditionalMainThreadWrite2(boolean),access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.mOnlyWrittenOnMain`]
codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional_isMainThread_ElseBranch_Bad(), 7, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional_isMainThread_ElseBranch_Bad(), 7, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`]
codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional_isMainThread_Negation_Bad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional_isMainThread_Negation_Bad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`]
codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional_isUiThread_ElseBranch_Bad(), 7, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional_isUiThread_ElseBranch_Bad(), 7, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`]
@ -89,6 +91,7 @@ codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.confu
codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.readProtectedUnthreadedBad(), 3, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`,<Write trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.readProtectedUnthreadedBad(), 3, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`,<Write trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`]
codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded1_Bad(), 2, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f1`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded1_Bad(), 2, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f1`]
codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded_Bad(), 2, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`,<Write trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded_Bad(), 2, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`,<Write trace>,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`]
codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.writeAfterConditionalMainThreadInCalleeBad(), 4, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.mSharedField`]
codetoanalyze/java/racerd/ReadWriteRaces.java, Object ReadWriteRaces.callUnprotecteReadInCallee(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,call to Object ReadWriteRaces.unprotectedReadInCallee(),access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`] codetoanalyze/java/racerd/ReadWriteRaces.java, Object ReadWriteRaces.callUnprotecteReadInCallee(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,call to Object ReadWriteRaces.unprotectedReadInCallee(),access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`]
codetoanalyze/java/racerd/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead1(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`] codetoanalyze/java/racerd/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead1(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`]
codetoanalyze/java/racerd/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead2(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field2`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field2`] codetoanalyze/java/racerd/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead2(), 1, THREAD_SAFETY_VIOLATION, [<Read trace>,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field2`,<Write trace>,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field2`]

Write Preview
Loading…
Cancel
Save