diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index db9fdcfd6..1e6c27ec3 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -48,7 +48,7 @@ let get_container_write_desc sink = -> get_container_write_desc_ call_name (F.asprintf "%a" Var.pp base_var) | _ -> None ) - | Read _ + | Read _ | InterfaceCall _ -> (* TODO: support Read *) None @@ -264,6 +264,47 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let is_unprotected is_locked is_threaded pdesc = not is_locked && not is_threaded && not (Procdesc.is_java_synchronized pdesc) + (** return true if this function is library code from the JDK core libraries or Android *) + let is_java_library = function + | Typ.Procname.Java java_pname -> ( + match Typ.Procname.java_get_package java_pname with + | Some package_name + -> String.is_prefix ~prefix:"java." package_name + || String.is_prefix ~prefix:"android." package_name + || String.is_prefix ~prefix:"com.google." package_name + | None + -> false ) + | _ + -> false + + let is_builder_function = function + | Typ.Procname.Java java_pname + -> String.is_suffix ~suffix:"$Builder" (Typ.Procname.java_get_class_name java_pname) + | _ + -> false + + let has_return_annot predicate pn = + Annotations.pname_has_return_annot pn ~attrs_of_pname:Specs.proc_resolve_attributes predicate + + let add_unannotated_call_access pname (call_flags: CallFlags.t) loc tenv ~locks ~threads + attribute_map (proc_data: FormalMap.t ProcData.t) = + if call_flags.cf_interface && Typ.Procname.is_java pname + && not (is_java_library pname || 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 Annotations.ia_is_thread_safe tenv pname) + && not (has_return_annot Annotations.ia_is_thread_safe pname) + then + let open Domain in + let pre = + if is_unprotected locks threads proc_data.pdesc then AccessPrecondition.unprotected + else + AccessPrecondition.Protected + (make_excluder (locks || Procdesc.is_java_synchronized proc_data.pdesc) threads) + in + AccessDomain.add_access pre (make_unannotated_call_access pname loc) attribute_map + else attribute_map + let add_access exp loc ~is_write_access accesses locks threads attribute_map (proc_data: FormalMap.t ProcData.t) = let open Domain in @@ -294,12 +335,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct || is_safe_access access prefix_path proc_data.tenv then access_acc else - (* TODO: I think there's a utility function for this somewhere *) - let accesses = AccessDomain.get_accesses pre access_acc in - let accesses' = - PathDomain.add_sink (make_access access_path ~is_write loc) accesses - in - AccessDomain.add pre accesses' access_acc + AccessDomain.add_access pre (make_field_access access_path ~is_write loc) access_acc in add_field_accesses pre access_path access_acc' access_list' in @@ -321,9 +357,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in List.fold ~f:add_access_ ~init:accesses (HilExp.get_access_paths exp) - let has_return_annot predicate pn = - Annotations.pname_has_return_annot pn ~attrs_of_pname:Specs.proc_resolve_attributes predicate - let is_functional pname = let is_annotated_functional = has_return_annot Annotations.ia_is_functional in let is_modeled_functional = function @@ -472,7 +505,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (fst receiver_ap, snd receiver_ap @ [AccessPath.FieldAccess dummy_fieldname]) in AccessDomain.add_access (Unprotected (Some 0)) - (make_access dummy_access_ap ~is_write:true callee_loc) AccessDomain.empty + (make_field_access dummy_access_ap ~is_write:true callee_loc) AccessDomain.empty in (* TODO: for now all formals escape *) (* we need a more intelligent escape analysis, that branches on whether @@ -545,9 +578,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {astate with accesses; attribute_map; escapees} | 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 + ~threads:astate.threads astate.accesses proc_data + in let accesses = - add_reads actuals loc astate.accesses astate.locks astate.threads astate.attribute_map - proc_data + add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads + astate.attribute_map proc_data in let astate = {astate with accesses} in let astate = @@ -1057,12 +1094,12 @@ let pp_access fmt sink = match get_container_write_desc sink with | Some container_write_desc -> pp_container_access fmt container_write_desc - | None - -> let access_path = - match ThreadSafetyDomain.PathDomain.Sink.kind sink - with Read access_path | Write access_path -> access_path - in - F.fprintf fmt "%a" (MF.wrap_monospaced AccessPath.pp_access_list) (snd access_path) + | None -> + match ThreadSafetyDomain.PathDomain.Sink.kind sink with + | Read access_path | Write access_path + -> F.fprintf fmt "%a" (MF.wrap_monospaced AccessPath.pp_access_list) (snd access_path) + | InterfaceCall _ as access + -> F.fprintf fmt "%a" ThreadSafetyDomain.Access.pp access let desc_of_sink sink = match get_container_write_desc sink with @@ -1071,7 +1108,11 @@ let desc_of_sink sink = | None -> let sink_pname = CallSite.pname (ThreadSafetyDomain.PathDomain.Sink.call_site sink) in if Typ.Procname.equal sink_pname Typ.Procname.empty_block then - F.asprintf "access to %a" pp_access sink + match ThreadSafetyDomain.PathDomain.Sink.kind sink with + | Read _ | Write _ + -> F.asprintf "access to %a" pp_access sink + | InterfaceCall interface_pname + -> F.asprintf "call to %a" Typ.Procname.pp interface_pname else F.asprintf "call to %a" Typ.Procname.pp sink_pname let trace_of_pname orig_sink orig_pdesc callee_pname = @@ -1130,6 +1171,20 @@ let report_thread_safety_violation tenv pdesc ~make_description ~conflicts acces let trace_of_pname = trace_of_pname access pdesc in Option.iter ~f:report_one_path (PathDomain.get_reportable_sink_path access ~trace_of_pname) +let report_unannotated_interface_violation tenv pdesc access reported_pname = + match reported_pname with + | Typ.Procname.Java java_pname + -> let class_name = Typ.Procname.java_get_class_name java_pname in + let make_description _ _ _ _ _ = + F.asprintf + "Unprotected call to method of un-annotated interface %s. Consider annotating the class with %a or adding a lock" + class_name MF.pp_monospaced "@ThreadSafe" + in + report_thread_safety_violation tenv pdesc ~make_description ~conflicts:[] access + | _ + -> (* skip reporting on C++ *) + () + let pp_procname_short fmt = function | Typ.Procname.Java java -> F.fprintf fmt "%s.%s" (Typ.Procname.java_get_class_name java) @@ -1225,12 +1280,14 @@ let report_unsafe_accesses aggregated_access_map = let open ThreadSafetyDomain in let is_duplicate_report access pname {reported_sites; reported_writes; reported_reads} = CallSite.Set.mem (TraceElem.call_site access) reported_sites - || Typ.Procname.Set.mem pname - ( match TraceElem.kind access with - | Access.Write _ - -> reported_writes - | Access.Read _ - -> reported_reads ) + || + match TraceElem.kind access with + | Access.Write _ + -> Typ.Procname.Set.mem pname reported_writes + | Access.Read _ + -> Typ.Procname.Set.mem pname reported_reads + | Access.InterfaceCall _ + -> false in let update_reported access pname reported = let reported_sites = CallSite.Set.add (TraceElem.call_site access) reported.reported_sites in @@ -1241,12 +1298,21 @@ let report_unsafe_accesses aggregated_access_map = | Access.Read _ -> let reported_reads = Typ.Procname.Set.add pname reported.reported_reads in {reported with reported_reads; reported_sites} + | Access.InterfaceCall _ + -> reported in let report_unsafe_access (access, pre, threaded, tenv, pdesc) accesses reported_acc = let pname = Procdesc.get_proc_name pdesc in if is_duplicate_report access pname reported_acc then reported_acc else match (TraceElem.kind access, pre) with + | Access.InterfaceCall unannoted_call_pname, AccessPrecondition.Unprotected _ + -> (* un-annotated interface call + no lock. warn *) + report_unannotated_interface_violation tenv pdesc access unannoted_call_pname ; + update_reported access pname reported_acc + | Access.InterfaceCall _, AccessPrecondition.Protected _ + -> (* un-annotated interface call, but it's protected by a lock/thread. don't report *) + reported_acc | Access.Write _, AccessPrecondition.Unprotected _ -> ( match Procdesc.get_proc_name pdesc with | Java _ diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 589f5f76e..63be40ff5 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -11,17 +11,28 @@ open! IStd module F = Format module Access = struct - type t = Read of AccessPath.Raw.t | Write of AccessPath.Raw.t [@@deriving compare] + type t = + | Read of AccessPath.Raw.t + | Write of AccessPath.Raw.t + | InterfaceCall of Typ.Procname.t + [@@deriving compare] - let make access_path ~is_write = if is_write then Write access_path else Read access_path + let make_field_access access_path ~is_write = + if is_write then Write access_path else Read access_path - let get_access_path = function Read access_path | Write access_path -> Some access_path + let get_access_path = function + | Read access_path | Write access_path + -> Some access_path + | InterfaceCall _ + -> None let pp fmt = function | Read access_path -> F.fprintf fmt "Read of %a" AccessPath.Raw.pp access_path | Write access_path -> F.fprintf fmt "Write to %a" AccessPath.Raw.pp access_path + | InterfaceCall pname + -> F.fprintf fmt "Call to un-annotated interface method %a" Typ.Procname.pp pname end module TraceElem = struct @@ -29,9 +40,12 @@ module TraceElem = struct type t = {site: CallSite.t; kind: Kind.t} [@@deriving compare] - let is_read {kind} = match kind with Read _ -> true | Write _ -> false + let is_read {kind} = match kind with Read _ -> true | InterfaceCall _ | Write _ -> false - let is_write {kind} = match kind with Read _ -> false | Write _ -> true + let is_write {kind} = match kind with InterfaceCall _ | Read _ -> false | Write _ -> true + + let is_interface_call {kind} = + match kind with InterfaceCall _ -> true | Read _ | Write _ -> false let call_site {site} = site @@ -52,9 +66,13 @@ module TraceElem = struct end) end -let make_access access_path ~is_write loc = +let make_field_access access_path ~is_write loc = + let site = CallSite.make Typ.Procname.empty_block loc in + TraceElem.make (Access.make_field_access access_path ~is_write) site + +let make_unannotated_call_access pname loc = let site = CallSite.make Typ.Procname.empty_block loc in - TraceElem.make (Access.make access_path ~is_write) site + TraceElem.make (Access.InterfaceCall pname) site (* In this domain true<=false. The intended denotations [[.]] are [[true]] = the set of all states where we know according, to annotations diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 921e243f8..abed57c13 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -11,7 +11,12 @@ open! IStd module F = Format module Access : sig - type t = Read of AccessPath.Raw.t | Write of AccessPath.Raw.t [@@deriving compare] + type t = + | Read of AccessPath.Raw.t (** Field read *) + | Write of AccessPath.Raw.t (** Field write *) + | InterfaceCall of Typ.Procname.t + (** Call to method of interface not annotated with @ThreadSafe *) + [@@deriving compare] val get_access_path : t -> AccessPath.Raw.t option @@ -24,6 +29,8 @@ module TraceElem : sig val is_write : t -> bool val is_read : t -> bool + + val is_interface_call : t -> bool end (** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes @@ -171,6 +178,8 @@ type summary = include AbstractDomain.WithBottom with type astate := astate -val make_access : AccessPath.Raw.t -> is_write:bool -> Location.t -> TraceElem.t +val make_field_access : AccessPath.Raw.t -> is_write:bool -> Location.t -> TraceElem.t + +val make_unannotated_call_access : Typ.Procname.t -> Location.t -> TraceElem.t val pp_summary : F.formatter -> summary -> unit diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index 393420d98..4b95748dc 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -179,6 +179,8 @@ let ia_is_returns_ownership ia = ia_ends_with ia returns_ownership let ia_is_synchronized_collection ia = ia_ends_with ia synchronized_collection +let ia_is_thread_safe ia = ia_ends_with ia thread_safe + let ia_is_true_on_null ia = ia_ends_with ia true_on_null let ia_is_initializer ia = ia_ends_with ia initializer_ diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index 91c8b4591..2db2fdded 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -124,6 +124,8 @@ val ia_is_returns_ownership : Annot.Item.t -> bool val ia_is_synchronized_collection : Annot.Item.t -> bool +val ia_is_thread_safe : Annot.Item.t -> bool + val ia_is_thread_confined : Annot.Item.t -> bool val ia_is_ui_thread : Annot.Item.t -> bool diff --git a/infer/tests/codetoanalyze/java/threadsafety/Dispatch.java b/infer/tests/codetoanalyze/java/threadsafety/Dispatch.java new file mode 100644 index 000000000..187144fb7 --- /dev/null +++ b/infer/tests/codetoanalyze/java/threadsafety/Dispatch.java @@ -0,0 +1,58 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ + +package codetoanalyze.java.checkers; + +import com.facebook.infer.annotation.ThreadSafe; + +interface UnannotatedInterface { + public void foo(); +} + +@ThreadSafe +interface AnnotatedInterface { + public void foo(); +} + +interface AnnotatedInterfaceMethod { + + @ThreadSafe public void foo(); +} + +class NotThreadSafe { + void notThreadSafeOk(UnannotatedInterface i) { + i.foo(); // ok + } +} + + +@ThreadSafe +public class Dispatch { + + void callUnannotatedInterfaceBad(UnannotatedInterface i) { + i.foo(); + } + + void callUnannotatedInterfaceIndirectBad(NotThreadSafe s, UnannotatedInterface i) { + s.notThreadSafeOk(i); + } + + synchronized void callUnannotatedInterfaceUnderLockOk(NotThreadSafe s, UnannotatedInterface i) { + s.notThreadSafeOk(i); + } + + void callAnnotatedInterfaceOk(AnnotatedInterface i) { + i.foo(); + } + + void callAnnotatedInterfaceMethodOk(AnnotatedInterfaceMethod i) { + i.foo(); + } + +} diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index e19373eab..22d322126 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -47,6 +47,8 @@ codetoanalyze/java/threadsafety/DeDup.java, void DeDup.two_reads(), 3, THREAD_SA codetoanalyze/java/threadsafety/DeDup.java, void DeDup.two_writes(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.DeDup.field`] codetoanalyze/java/threadsafety/DeDup.java, void DeDup.write_read(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.DeDup.field`] codetoanalyze/java/threadsafety/DeDup.java, void DeDup.write_read(), 3, THREAD_SAFETY_VIOLATION, [,access to `codetoanalyze.java.checkers.DeDup.field`,,access to `codetoanalyze.java.checkers.DeDup.field`] +codetoanalyze/java/threadsafety/Dispatch.java, void Dispatch.callUnannotatedInterfaceBad(UnannotatedInterface), 1, THREAD_SAFETY_VIOLATION, [call to void UnannotatedInterface.foo()] +codetoanalyze/java/threadsafety/Dispatch.java, void Dispatch.callUnannotatedInterfaceIndirectBad(NotThreadSafe,UnannotatedInterface), 1, THREAD_SAFETY_VIOLATION, [call to void NotThreadSafe.notThreadSafeOk(UnannotatedInterface),call to void UnannotatedInterface.foo()] codetoanalyze/java/threadsafety/Locks.java, void Locks.FP_unlockOneLock(), 4, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/threadsafety/Locks.java, void Locks.afterReentrantLockUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Locks.f`] codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Locks.f`]