diff --git a/infer/src/IR/AccessPath.ml b/infer/src/IR/AccessPath.ml index e249b9212..d33f9d988 100644 --- a/infer/src/IR/AccessPath.ml +++ b/infer/src/IR/AccessPath.ml @@ -54,11 +54,12 @@ module Raw = struct let equal = [%compare.equal : t] - let truncate = function - | base, [] | base, [_] -> - (base, []) - | base, accesses -> - (base, List.rev (List.tl_exn (List.rev accesses))) + let truncate ((base, accesses) as t) = + match List.rev accesses with + | [] -> + (t, None) + | last_access :: accesses -> + ((base, List.rev accesses), Some last_access) let lookup_field_type_annot tenv base_typ field_name = diff --git a/infer/src/IR/AccessPath.mli b/infer/src/IR/AccessPath.mli index 22fb8c62a..78d541062 100644 --- a/infer/src/IR/AccessPath.mli +++ b/infer/src/IR/AccessPath.mli @@ -22,9 +22,9 @@ type access = representedas (x, [f; g]) *) and t = base * access list [@@deriving compare] -val truncate : t -> t -(** remove the last access of the access path if the access list is non-empty. returns the - original access path if the access list is empty *) +val truncate : t -> t * access option +(** remove and return the last access of the access path if the access list is non-empty. returns + the original access path * None if the access list is empty *) val get_last_access : t -> access option (** get the last access in the list. returns None if the list is empty *) diff --git a/infer/src/checkers/NullabilityCheck.ml b/infer/src/checkers/NullabilityCheck.ml index 89445e7c4..784fc3490 100644 --- a/infer/src/checkers/NullabilityCheck.ml +++ b/infer/src/checkers/NullabilityCheck.ml @@ -214,9 +214,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (remove_call_sites ap aps, updated_pnames) - let rec longest_nullable_prefix ap ((nulable_aps, _) as astate) = - try Some (ap, NullableAP.find ap nulable_aps) with Not_found -> - match ap with _, [] -> None | p -> longest_nullable_prefix (AccessPath.truncate p) astate + let rec longest_nullable_prefix ap ((nullable_aps, _) as astate) = + try Some (ap, NullableAP.find ap nullable_aps) with Not_found -> + match ap with + | _, [] -> + None + | p -> + longest_nullable_prefix (fst (AccessPath.truncate p)) astate let check_ap proc_data loc ap astate = diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index b3589f389..7b01cd44e 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -89,18 +89,48 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (ownership', attribute_map') - let add_unannotated_call_access pname (call_flags: CallFlags.t) loc tenv ~locks ~threads + (* we don't want to warn on accesses to the field if it is (a) thread-confined, or + (b) volatile *) + let is_safe_access access prefix_path tenv = + match (access, AccessPath.get_typ prefix_path tenv) with + | ( AccessPath.FieldAccess fieldname + , Some ({Typ.desc= Tstruct typename} | {desc= Tptr ({desc= Tstruct typename}, _)}) ) -> ( + match Tenv.lookup tenv typename with + | Some struct_typ -> + Annotations.struct_typ_has_annot struct_typ Annotations.ia_is_thread_confined + || Annotations.field_has_annot fieldname struct_typ Annotations.ia_is_thread_confined + || Annotations.field_has_annot fieldname struct_typ Annotations.ia_is_volatile + | None -> + false ) + | _ -> + false + + + let add_unannotated_call_access pname actuals (call_flags: CallFlags.t) loc tenv ~locks ~threads attribute_map (proc_data: extras ProcData.t) = let open RacerDConfig in let thread_safe_or_thread_confined annot = Annotations.ia_is_thread_safe annot || Annotations.ia_is_thread_confined annot in + let is_receiver_safe = function + | (HilExp.AccessExpression receiver_access_exp) :: _ + -> ( + let receiver_access_path = AccessExpression.to_access_path receiver_access_exp in + match AccessPath.truncate receiver_access_path with + | receiver_prefix, Some receiver_field -> + is_safe_access receiver_field receiver_prefix tenv + | _ -> + false ) + | _ -> + false + in if call_flags.cf_interface && Typ.Procname.is_java pname && not (Models.is_java_library pname || Models.is_builder_function pname) (* can't ask anyone to annotate interfaces in library code, and Builder's should always be thread-safe (would be unreasonable to ask everyone to annotate them) *) && not (PatternMatch.check_class_attributes thread_safe_or_thread_confined tenv pname) && not (Models.has_return_annot thread_safe_or_thread_confined pname) + && not (is_receiver_safe actuals) then let open Domain in let pre = AccessData.make locks threads False proc_data.pdesc in @@ -117,22 +147,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> false in - (* we don't want to warn on accesses to the field if it is (a) thread-confined, or - (b) volatile *) - let is_safe_access access prefix_path tenv = - match (access, AccessPath.get_typ prefix_path tenv) with - | ( AccessPath.FieldAccess fieldname - , Some ({Typ.desc= Tstruct typename} | {desc= Tptr ({desc= Tstruct typename}, _)}) ) -> ( - match Tenv.lookup tenv typename with - | Some struct_typ -> - Annotations.struct_typ_has_annot struct_typ Annotations.ia_is_thread_confined - || Annotations.field_has_annot fieldname struct_typ Annotations.ia_is_thread_confined - || Annotations.field_has_annot fieldname struct_typ Annotations.ia_is_volatile - | None -> - false ) - | _ -> - false - in + (* TODO: simplify this with AccessPath.truncate *) let rec add_field_accesses prefix_path access_acc = function | [] -> access_acc @@ -411,7 +426,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | Call (ret_opt, Direct callee_pname, actuals, call_flags, loc) -> ( let accesses_with_unannotated_calls = - add_unannotated_call_access callee_pname call_flags loc tenv ~locks:astate.locks + add_unannotated_call_access callee_pname actuals call_flags loc tenv ~locks:astate.locks ~threads:astate.threads astate.accesses proc_data in let accesses = @@ -980,7 +995,7 @@ let get_contaminated_race_message access wobbly_paths = (* Access paths rooted in static variables are always race-prone, hence do not complain about contamination. *) when not (access_path |> fst |> fst |> ignore_var) -> - let proper_prefix_path = AccessPath.truncate access_path in + let proper_prefix_path, _ = AccessPath.truncate access_path in let base, accesses = proper_prefix_path in let rec prefix_in_wobbly_paths prefix = function | [] -> diff --git a/infer/tests/codetoanalyze/java/racerd/Dispatch.java b/infer/tests/codetoanalyze/java/racerd/Dispatch.java index fd1f97315..1510c3439 100644 --- a/infer/tests/codetoanalyze/java/racerd/Dispatch.java +++ b/infer/tests/codetoanalyze/java/racerd/Dispatch.java @@ -89,3 +89,17 @@ class Some { d.callUnderLock(i); } } + +@ThreadSafe +class ThreadConfinedField { + @ThreadConfined(ThreadConfined.ANY) UnannotatedInterface mThreadConfined; + UnannotatedInterface mNormal; + + void interfaceCallOnThreadConfinedFieldOk() { + mThreadConfined.foo(); + } + + void interfaceCallOnNormalFieldBad() { + mNormal.foo(); + } +} diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index aaffbec05..fae96dbdc 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -50,6 +50,7 @@ codetoanalyze/java/racerd/DeepOwnership.java, void DeepOwnership.globalNotOwnedB codetoanalyze/java/racerd/DeepOwnership.java, void DeepOwnership.reassignBaseToGlobalBad(), 3, THREAD_SAFETY_VIOLATION, ERROR, [access to `x.DeepOwnership.next`] codetoanalyze/java/racerd/Dispatch.java, void Dispatch.callUnannotatedInterfaceBad(UnannotatedInterface), 1, INTERFACE_NOT_THREAD_SAFE, ERROR, [Call to un-annotated interface method void UnannotatedInterface.foo()] codetoanalyze/java/racerd/Dispatch.java, void Dispatch.callUnannotatedInterfaceIndirectBad(NotThreadSafe,UnannotatedInterface), 1, INTERFACE_NOT_THREAD_SAFE, ERROR, [call to void NotThreadSafe.notThreadSafeOk(UnannotatedInterface),Call to un-annotated interface method void UnannotatedInterface.foo()] +codetoanalyze/java/racerd/Dispatch.java, void ThreadConfinedField.interfaceCallOnNormalFieldBad(), 1, INTERFACE_NOT_THREAD_SAFE, ERROR, [Call to un-annotated interface method void UnannotatedInterface.foo()] codetoanalyze/java/racerd/Inference.java, int Inference.read4OutsideSyncBad(), 1, THREAD_SAFETY_VIOLATION, ERROR, [,access to `this.codetoanalyze.java.checkers.Inference.mField4`,,access to `this.codetoanalyze.java.checkers.Inference.mField4`] codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead1Bad(), 1, THREAD_SAFETY_VIOLATION, ERROR, [,access to `this.codetoanalyze.java.checkers.Inference.mField1`,,access to `this.codetoanalyze.java.checkers.Inference.mField1`] codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead2Bad(), 1, THREAD_SAFETY_VIOLATION, ERROR, [,access to `this.codetoanalyze.java.checkers.Inference.mField2`,,access to `this.codetoanalyze.java.checkers.Inference.mField2`]