diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index 848d29485..2c7dc6a4c 100644 --- a/infer/src/IR/Typ.ml +++ b/infer/src/IR/Typ.ml @@ -989,6 +989,24 @@ module Procname = struct t + let get_class_type_name = function + | Java java_pname -> + Some (Java.get_class_type_name java_pname) + | ObjC_Cpp objc_pname -> + Some (ObjC_Cpp.get_class_type_name objc_pname) + | _ -> + None + + + let get_class_name = function + | Java java_pname -> + Some (Java.get_class_name java_pname) + | ObjC_Cpp objc_pname -> + Some (ObjC_Cpp.get_class_name objc_pname) + | _ -> + None + + let is_method_in_objc_protocol t = match t with ObjC_Cpp osig -> Name.is_objc_protocol osig.class_name | _ -> false diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index e8ea5f5fb..529b66dd2 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -418,7 +418,7 @@ being the name of the struct, [None] means the parameter is of some other type. val get_class_name : t -> string - val get_class_type_name : t -> Name.t + val get_class_type_name : t -> Name.t [@@warning "-32"] val get_class_qualifiers : t -> QualifiedCppName.t @@ -488,6 +488,10 @@ being the name of the struct, [None] means the parameter is of some other type. val equal : t -> t -> bool + val get_class_type_name : t -> Name.t option [@@warning "-32"] + + val get_class_name : t -> string option + val get_parameters : t -> Parameter.t list val replace_parameters : Parameter.t list -> t -> t diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 5f5986985..86f75da47 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -168,13 +168,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> OwnershipAbstractValue.unowned in - Some - { locks= LocksDomain.empty - ; threads= ThreadsDomain.empty - ; accesses= callee_accesses - ; return_ownership - ; return_attributes= AttributeSetDomain.empty - ; wobbly_paths= StabilityDomain.empty } + Some {empty_summary with accesses= callee_accesses; return_ownership} let get_summary caller_pdesc callee_pname actuals callee_loc tenv (astate : Domain.astate) = @@ -620,15 +614,6 @@ end module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions) -let empty_post : RacerDDomain.summary = - { threads= RacerDDomain.ThreadsDomain.empty - ; locks= RacerDDomain.LocksDomain.empty - ; accesses= RacerDDomain.AccessDomain.empty - ; return_ownership= RacerDDomain.OwnershipAbstractValue.unowned - ; return_attributes= RacerDDomain.AttributeSetDomain.empty - ; wobbly_paths= RacerDDomain.StabilityDomain.empty } - - let analyze_procedure {Callbacks.proc_desc; tenv; summary} = let open RacerDModels in let open ConcurrencyModels in @@ -691,19 +676,17 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} = else (* express that the constructor owns [this] *) let init = add_owned_formal own_locals 0 in - List.fold ~f:add_conditional_owned_formal ~init - (List.filter - ~f:(fun (_, index) -> not (Int.equal index 0)) - (FormalMap.get_formals_indexes formal_map)) + FormalMap.get_formals_indexes formal_map + |> List.filter ~f:(fun (_, index) -> not (Int.equal 0 index)) + |> List.fold ~init ~f:add_conditional_owned_formal in {RacerDDomain.empty with ownership; threads} else (* add Owned(formal_index) predicates for each formal to indicate that each one is owned if it is owned in the caller *) let ownership = - List.fold ~f:add_conditional_owned_formal + List.fold ~init:own_locals ~f:add_conditional_owned_formal (FormalMap.get_formals_indexes formal_map) - ~init:own_locals in {RacerDDomain.empty with ownership; threads} in @@ -723,7 +706,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} = Payload.update_summary post summary | None -> summary - else Payload.update_summary empty_post summary + else Payload.update_summary empty_summary summary type conflict = RacerDDomain.TraceElem.t @@ -1090,6 +1073,34 @@ end = struct M.fold f map a end +let should_report_on_proc procdesc tenv = + let proc_name = Procdesc.get_proc_name procdesc in + match proc_name with + | Java java_pname -> + (* return true if procedure is at an abstraction boundary or reporting has been explicitly + requested via @ThreadSafe in java *) + RacerDModels.is_thread_safe_method proc_name tenv + || Procdesc.get_access procdesc <> PredSymb.Private + && (not (Typ.Procname.Java.is_autogen_method java_pname)) + && not (Annotations.pdesc_return_annot_ends_with procdesc Annotations.visibleForTesting) + | ObjC_Cpp objc_cpp_pname -> + ( match objc_cpp_pname.Typ.Procname.ObjC_Cpp.kind with + | CPPMethod _ | CPPConstructor _ | CPPDestructor _ -> + Procdesc.get_access procdesc <> PredSymb.Private + | ObjCClassMethod | ObjCInstanceMethod | ObjCInternalMethod -> + (* ObjC has no private methods, just a convention that they start with an underscore *) + not (String.is_prefix objc_cpp_pname.Typ.Procname.ObjC_Cpp.method_name ~prefix:"_") ) + && + let matcher = ConcurrencyModels.cpp_lock_types_matcher in + Option.exists (Tenv.lookup tenv objc_cpp_pname.class_name) ~f:(fun class_str -> + (* check if the class contains a lock member *) + List.exists class_str.Typ.Struct.fields ~f:(fun (_, ft, _) -> + Option.exists (Typ.name ft) ~f:(fun name -> + QualifiedCppName.Match.match_qualifiers matcher (Typ.Name.qual_name name) ) ) ) + | _ -> + false + + (** Report accesses that may race with each other. Principles for race reporting. @@ -1203,7 +1214,7 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) = (* Do not report unprotected writes when an access can't run in parallel with itself, or for ObjC_Cpp *) reported_acc ) - | (Access.Read _ | ContainerRead _) when AccessSnapshot.is_unprotected snapshot -> ( + | (Access.Read _ | ContainerRead _) when AccessSnapshot.is_unprotected snapshot -> (* unprotected read. report all writes as conflicts for java. for c++ filter out unprotected writes *) let is_conflict {snapshot; threads= other_threads} = @@ -1213,15 +1224,15 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) = ThreadsDomain.is_any threads || ThreadsDomain.is_any other_threads else not (AccessSnapshot.is_unprotected snapshot) in - match List.find ~f:is_conflict accesses with - | None -> - reported_acc - | Some conflict -> - report_thread_safety_violation tenv procdesc - ~make_description:(make_read_write_race_description ~read_is_sync:false conflict) - ~report_kind:(ReadWriteRace conflict.snapshot.access) snapshot.access threads - wobbly_paths ; - update_reported snapshot.access pname reported_acc ) + List.find ~f:is_conflict accesses + |> Option.value_map ~default:reported_acc ~f:(fun conflict -> + let make_description = + make_read_write_race_description ~read_is_sync:false conflict + in + let report_kind = ReadWriteRace conflict.snapshot.access in + report_thread_safety_violation tenv procdesc ~make_description ~report_kind + snapshot.access threads wobbly_paths ; + update_reported snapshot.access pname reported_acc ) | Access.Read _ | ContainerRead _ -> (* protected read. report unprotected writes and opposite protected writes as conflicts *) let can_conflict (snapshot1 : AccessSnapshot.t) (snapshot2 : AccessSnapshot.t) = @@ -1257,14 +1268,7 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) = let should_report {tenv; procdesc} = List.exists grouped_accesses ~f:(fun ({threads} : reported_access) -> ThreadsDomain.is_any threads ) - && - match Procdesc.get_proc_name procdesc with - | Java _ -> - should_report_in_java procdesc tenv - | ObjC_Cpp objc_cpp -> - should_report_in_objcpp procdesc objc_cpp tenv - | _ -> - false + && should_report_on_proc procdesc tenv in let reportable_accesses = List.filter ~f:should_report grouped_accesses in List.fold reportable_accesses ~init:reported ~f:(report_unsafe_access reportable_accesses) @@ -1278,39 +1282,30 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) = that x.f.g may point to during execution *) let make_results_table file_env = let open RacerDDomain in - let aggregate_post tenv procdesc acc {threads; accesses; wobbly_paths} = + let aggregate_post acc ({threads; accesses; wobbly_paths}, tenv, procdesc) = AccessDomain.fold (fun snapshot acc -> ReportMap.add {threads; snapshot; tenv; procdesc; wobbly_paths} acc) accesses acc in - let aggregate_posts acc (tenv, proc_desc) = - Payload.read proc_desc (Procdesc.get_proc_name proc_desc) - |> Option.fold ~init:acc ~f:(aggregate_post tenv proc_desc) - in - List.fold file_env ~init:ReportMap.empty ~f:aggregate_posts + List.filter_map file_env ~f:(fun (tenv, proc_desc) -> + Procdesc.get_proc_name proc_desc |> Payload.read proc_desc + |> Option.map ~f:(fun payload -> (payload, tenv, proc_desc)) ) + |> List.fold ~init:ReportMap.empty ~f:aggregate_post (* aggregate all of the procedures in the file env by their declaring class. this lets us analyze each class individually *) let aggregate_by_class file_env = List.fold file_env ~init:String.Map.empty ~f:(fun acc ((_, pdesc) as proc) -> - let classname = - match Procdesc.get_proc_name pdesc with - | Typ.Procname.Java java_pname -> - Some (Typ.Procname.Java.get_class_name java_pname) - | ObjC_Cpp objc_cpp_pname -> - Some (Typ.Procname.ObjC_Cpp.get_class_name objc_cpp_pname) - | _ -> - None - in - Option.fold classname ~init:acc ~f:(fun acc classname -> - String.Map.add_multi acc ~key:classname ~data:proc ) ) + Procdesc.get_proc_name pdesc |> Typ.Procname.get_class_name + |> Option.fold ~init:acc ~f:(fun acc classname -> + String.Map.add_multi acc ~key:classname ~data:proc ) ) (* Gathers results by analyzing all the methods in a file, then post-processes the results to check an (approximation of) thread safety *) let file_analysis {Callbacks.procedures; source_file} = - String.Map.iter (aggregate_by_class procedures) ~f:(fun class_env -> - report_unsafe_accesses (make_results_table class_env) ) ; + aggregate_by_class procedures + |> String.Map.iter ~f:(fun class_env -> report_unsafe_accesses (make_results_table class_env)) ; IssueLog.store Config.racerd_issues_dir_name source_file diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 1ea23849d..527f7ed4b 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -682,6 +682,15 @@ type summary = ; return_attributes: AttributeSetDomain.astate ; wobbly_paths: StabilityDomain.astate } +let empty_summary = + { threads= ThreadsDomain.empty + ; locks= LocksDomain.empty + ; accesses= AccessDomain.empty + ; return_ownership= OwnershipAbstractValue.unowned + ; return_attributes= AttributeSetDomain.empty + ; wobbly_paths= StabilityDomain.empty } + + let pp_summary fmt {threads; locks; accesses; return_ownership; return_attributes; wobbly_paths} = F.fprintf fmt "@\n\ @@ -699,7 +708,7 @@ let pp fmt {threads; locks; accesses; ownership; attribute_map; wobbly_paths} = F.fprintf fmt "Threads: %a, Locks: %a @\n\ Accesses %a @\n\ - \ Ownership: %a @\n\ + Ownership: %a @\n\ Attributes: %a @\n\ Non-stable Paths: %a@\n" ThreadsDomain.pp threads LocksDomain.pp locks AccessDomain.pp accesses OwnershipDomain.pp diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index f5ca4f334..f04d97d2c 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -235,6 +235,8 @@ type summary = ; return_attributes: AttributeSetDomain.astate ; wobbly_paths: StabilityDomain.astate } +val empty_summary : summary + include AbstractDomain.WithBottom with type astate := astate val pp_summary : F.formatter -> summary -> unit diff --git a/infer/src/concurrency/RacerDModels.ml b/infer/src/concurrency/RacerDModels.ml index c31b880b6..c0822b3bc 100644 --- a/infer/src/concurrency/RacerDModels.ml +++ b/infer/src/concurrency/RacerDModels.ml @@ -368,30 +368,3 @@ let is_thread_safe_method pname tenv = let is_marked_thread_safe pdesc tenv = let pname = Procdesc.get_proc_name pdesc in is_thread_safe_class pname tenv || is_thread_safe_method pname tenv - - -(* return true if procedure is at an abstraction boundary or reporting has been explicitly - requested via @ThreadSafe in java *) -let should_report_in_java proc_desc tenv = - let proc_name = Procdesc.get_proc_name proc_desc in - is_thread_safe_method proc_name tenv - || (not - ( match proc_name with - | Typ.Procname.Java java_pname -> - Typ.Procname.Java.is_autogen_method java_pname - | _ -> - false )) - && Procdesc.get_access proc_desc <> PredSymb.Private - && not (Annotations.pdesc_return_annot_ends_with proc_desc Annotations.visibleForTesting) - - -let should_report_in_objcpp proc_desc objc_cpp tenv = - Procdesc.get_access proc_desc <> PredSymb.Private - && - let class_name = Typ.Procname.ObjC_Cpp.get_class_type_name objc_cpp in - let matcher = ConcurrencyModels.cpp_lock_types_matcher in - Option.exists (Tenv.lookup tenv class_name) ~f:(fun class_str -> - (* check if the class contains a lock member *) - List.exists class_str.Typ.Struct.fields ~f:(fun (_, ft, _) -> - Option.exists (Typ.name ft) ~f:(fun name -> - QualifiedCppName.Match.match_qualifiers matcher (Typ.Name.qual_name name) ) ) ) diff --git a/infer/src/concurrency/RacerDModels.mli b/infer/src/concurrency/RacerDModels.mli index b7fc5a1c9..792c68299 100644 --- a/infer/src/concurrency/RacerDModels.mli +++ b/infer/src/concurrency/RacerDModels.mli @@ -50,10 +50,3 @@ val is_thread_safe_method : Typ.Procname.t -> Tenv.t -> bool as an alias of @ThreadSafe in a .inferconfig file. *) val is_marked_thread_safe : Procdesc.t -> Tenv.t -> bool - -val should_report_in_java : Procdesc.t -> Tenv.t -> bool -(** return true if procedure is at an abstraction boundary or reporting has been explicitly - requested via @ThreadSafe *) - -val should_report_in_objcpp : Procdesc.t -> Typ.Procname.ObjC_Cpp.t -> Tenv.t -> bool -(** check if the class contains a lock member *) diff --git a/infer/tests/codetoanalyze/objcpp/racerd/Basic.mm b/infer/tests/codetoanalyze/objcpp/racerd/Basic.mm index 42a382822..28b1e6333 100644 --- a/infer/tests/codetoanalyze/objcpp/racerd/Basic.mm +++ b/infer/tests/codetoanalyze/objcpp/racerd/Basic.mm @@ -9,6 +9,7 @@ @interface Basic : NSObject - (int)read; +- (void)_private_write_no_top_level_report:(int)data; - (void)write:(int)data; @end @@ -21,9 +22,13 @@ return data_; } +- (void)_private_write_no_top_level_report:(int)data { + data_ = data; +} + - (void)write:(int)data { mutex_.lock(); - data_ = data; + [self _private_write_no_top_level_report:data]; mutex_.unlock(); } @end diff --git a/infer/tests/codetoanalyze/objcpp/racerd/issues.exp b/infer/tests/codetoanalyze/objcpp/racerd/issues.exp index 8bb20fc28..2140bba1e 100644 --- a/infer/tests/codetoanalyze/objcpp/racerd/issues.exp +++ b/infer/tests/codetoanalyze/objcpp/racerd/issues.exp @@ -1 +1 @@ -codetoanalyze/objcpp/racerd/Basic.mm, Basic_read, 21, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,access to `self.data_`,,access to `self.data_`] +codetoanalyze/objcpp/racerd/Basic.mm, Basic_read, 22, LOCK_CONSISTENCY_VIOLATION, no_bucket, ERROR, [,access to `self.data_`,,call to Basic__private_write_no_top_level_report:,access to `self.data_`]