From 745f04f77dcf145b95ab05b116f7187710968b3d Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Mon, 15 Feb 2021 02:52:00 -0800 Subject: [PATCH] [racerd] races in nullsafe classes Summary: Races in Nullsafe classes can undermine NPE safety despite the class passing the type checks. This diff adds to the report text of THREAD_SAFETY_VIOLATION and GUARDEDBY_VIOLATION the following trailer: > Data races in `Nullsafe` classes may still cause NPEs. This only happens if the race is directly on a non-primitively-typed member field of the class. It also uses distinct bug types (adds the suffix _NULLSAFE to the bug types above) for easier accounting. Reviewed By: ezgicicek Differential Revision: D26403274 fbshipit-source-id: 3cd6ca082 --- infer/man/man1/infer-full.txt | 2 + infer/man/man1/infer-report.txt | 2 + infer/man/man1/infer.txt | 2 + infer/src/IR/Typ.mli | 3 + infer/src/absint/annotations.mli | 2 + infer/src/absint/exe_env.ml | 24 ++- infer/src/absint/exe_env.mli | 5 +- infer/src/backend/CallbackOfChecker.ml | 4 +- infer/src/backend/StarvationGlobalAnalysis.ml | 4 +- infer/src/backend/preanal.ml | 2 +- infer/src/base/IssueType.ml | 14 +- infer/src/base/IssueType.mli | 6 +- infer/src/biabduction/Tabulation.ml | 2 +- infer/src/concurrency/RacerDFileAnalysis.ml | 146 +++++++++++------- infer/src/concurrency/starvation.ml | 2 +- infer/src/cost/cost.ml | 2 +- infer/src/cost/hoisting.ml | 2 +- .../java/racerd/NullsafeMode.java | 38 +++++ .../codetoanalyze/java/racerd/issues.exp | 4 + 19 files changed, 194 insertions(+), 72 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/racerd/NullsafeMode.java diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 6ffe40b46..d8995269f 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -467,6 +467,7 @@ OPTIONS GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL (disabled by default), GUARDEDBY_VIOLATION (enabled by default), + GUARDEDBY_VIOLATION_NULLSAFE (enabled by default), IMPURE_FUNCTION (enabled by default), INEFFICIENT_KEYSET_ITERATOR (enabled by default), INFERBO_ALLOC_IS_BIG (enabled by default), @@ -527,6 +528,7 @@ OPTIONS STRONG_SELF_NOT_CHECKED (enabled by default), Symexec_memory_error (enabled by default), THREAD_SAFETY_VIOLATION (enabled by default), + THREAD_SAFETY_VIOLATION_NULLSAFE (enabled by default), TOPL_BIABD_ERROR (enabled by default), TOPL_PULSE_ERROR (enabled by default), UNINITIALIZED_VALUE (enabled by default), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 173fa22e8..11ec2a2a3 100644 --- a/infer/man/man1/infer-report.txt +++ b/infer/man/man1/infer-report.txt @@ -170,6 +170,7 @@ OPTIONS GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL (disabled by default), GUARDEDBY_VIOLATION (enabled by default), + GUARDEDBY_VIOLATION_NULLSAFE (enabled by default), IMPURE_FUNCTION (enabled by default), INEFFICIENT_KEYSET_ITERATOR (enabled by default), INFERBO_ALLOC_IS_BIG (enabled by default), @@ -230,6 +231,7 @@ OPTIONS STRONG_SELF_NOT_CHECKED (enabled by default), Symexec_memory_error (enabled by default), THREAD_SAFETY_VIOLATION (enabled by default), + THREAD_SAFETY_VIOLATION_NULLSAFE (enabled by default), TOPL_BIABD_ERROR (enabled by default), TOPL_PULSE_ERROR (enabled by default), UNINITIALIZED_VALUE (enabled by default), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index b5d45721a..19477edef 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -467,6 +467,7 @@ OPTIONS GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL (disabled by default), GUARDEDBY_VIOLATION (enabled by default), + GUARDEDBY_VIOLATION_NULLSAFE (enabled by default), IMPURE_FUNCTION (enabled by default), INEFFICIENT_KEYSET_ITERATOR (enabled by default), INFERBO_ALLOC_IS_BIG (enabled by default), @@ -527,6 +528,7 @@ OPTIONS STRONG_SELF_NOT_CHECKED (enabled by default), Symexec_memory_error (enabled by default), THREAD_SAFETY_VIOLATION (enabled by default), + THREAD_SAFETY_VIOLATION_NULLSAFE (enabled by default), TOPL_BIABD_ERROR (enabled by default), TOPL_PULSE_ERROR (enabled by default), UNINITIALIZED_VALUE (enabled by default), diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index a659c3afe..de199d76b 100644 --- a/infer/src/IR/Typ.mli +++ b/infer/src/IR/Typ.mli @@ -325,6 +325,9 @@ val is_char : t -> bool val is_csharp_type : t -> bool (** is [t] a type produced by the Java frontend? *) +val is_java_primitive_type : t -> bool +(** is [t] a primitive type produced by the Java frontend? *) + val is_java_type : t -> bool (** is [t] a type produced by the Java frontend? *) diff --git a/infer/src/absint/annotations.mli b/infer/src/absint/annotations.mli index 60b56016a..167f287dc 100644 --- a/infer/src/absint/annotations.mli +++ b/infer/src/absint/annotations.mli @@ -25,6 +25,8 @@ val no_allocation : string val nullable : string +val nullsafe : string + val nonnull : string val performance_critical : string diff --git a/infer/src/absint/exe_env.ml b/infer/src/absint/exe_env.ml index f75dfe431..a6749cc21 100644 --- a/infer/src/absint/exe_env.ml +++ b/infer/src/absint/exe_env.ml @@ -24,22 +24,22 @@ let new_file_data source = lazy (Option.first_some (Typ.IntegerWidths.load source) (Some Typ.IntegerWidths.java)) } -let file_data_of_source table source = - match SourceFile.Hash.find_opt table source with +type t = {proc_map: SourceFile.t Procname.Hash.t; file_map: file_data SourceFile.Hash.t} + +let file_data_of_source {file_map} source = + match SourceFile.Hash.find_opt file_map source with | Some file_data -> file_data | None -> let file_data = new_file_data source in - SourceFile.Hash.add table source file_data ; + SourceFile.Hash.add file_map source file_data ; file_data -type t = {proc_map: SourceFile.t Procname.Hash.t; file_map: file_data SourceFile.Hash.t} - let get_file_data exe_env pname = match Procname.Hash.find_opt exe_env.proc_map pname with | Some source -> - Some (file_data_of_source exe_env.file_map source) + Some (file_data_of_source exe_env source) | None -> ( match Attributes.load pname with | None -> @@ -47,7 +47,7 @@ let get_file_data exe_env pname = None | Some proc_attributes -> let source_file = proc_attributes.ProcAttributes.translation_unit in - let file_data = file_data_of_source exe_env.file_map source_file in + let file_data = file_data_of_source exe_env source_file in Procname.Hash.add exe_env.proc_map pname source_file ; Some file_data ) @@ -101,11 +101,19 @@ let get_column_value ~value_on_java ~file_data_to_value ~column_name exe_env pro (** return the type environment associated to the procedure *) -let get_tenv = +let get_proc_tenv = get_column_value ~value_on_java:java_global_tenv ~file_data_to_value:file_data_to_tenv ~column_name:"tenv" +let get_sourcefile_tenv exe_env sourcefile = + match file_data_of_source exe_env sourcefile |> file_data_to_tenv with + | Some tenv -> + tenv + | None -> + L.die InternalError "get_sourcefile_tenv: tenv not found for %a" SourceFile.pp sourcefile + + (** return the integer type widths associated to the procedure *) let get_integer_type_widths = get_column_value diff --git a/infer/src/absint/exe_env.mli b/infer/src/absint/exe_env.mli index 95f223d54..e997583d5 100644 --- a/infer/src/absint/exe_env.mli +++ b/infer/src/absint/exe_env.mli @@ -16,9 +16,12 @@ type t val mk : unit -> t (** Create a new cache *) -val get_tenv : t -> Procname.t -> Tenv.t +val get_proc_tenv : t -> Procname.t -> Tenv.t (** return the type environment associated with the procedure *) +val get_sourcefile_tenv : t -> SourceFile.t -> Tenv.t +(** return the type environment associated with the source file *) + val load_java_global_tenv : t -> Tenv.t (** Load Java type environment (if not done yet), and return it. Useful for accessing type info not related to any concrete function. *) diff --git a/infer/src/backend/CallbackOfChecker.ml b/infer/src/backend/CallbackOfChecker.ml index 4cfc01b03..b95b45013 100644 --- a/infer/src/backend/CallbackOfChecker.ml +++ b/infer/src/backend/CallbackOfChecker.ml @@ -17,7 +17,7 @@ let () = let mk_interprocedural_t ~f_analyze_dep ~get_payload exe_env summary - ?(tenv = Exe_env.get_tenv exe_env (Summary.get_proc_name summary)) () = + ?(tenv = Exe_env.get_proc_tenv exe_env (Summary.get_proc_name summary)) () = let analyze_dependency proc_name = let summary = Ondemand.analyze_proc_name exe_env ~caller_summary:summary proc_name in Option.bind summary ~f:(fun {Summary.payloads; proc_desc; _} -> @@ -69,7 +69,7 @@ let interprocedural_file payload_field checker {Callbacks.procedures; exe_env; s let to_intraprocedural_t {Callbacks.summary; exe_env} = { IntraproceduralAnalysis.proc_desc= Summary.get_proc_desc summary - ; tenv= Exe_env.get_tenv exe_env (Summary.get_proc_name summary) + ; tenv= Exe_env.get_proc_tenv exe_env (Summary.get_proc_name summary) ; err_log= Summary.get_err_log summary } diff --git a/infer/src/backend/StarvationGlobalAnalysis.ml b/infer/src/backend/StarvationGlobalAnalysis.ml index 48853fe41..5b251c673 100644 --- a/infer/src/backend/StarvationGlobalAnalysis.ml +++ b/infer/src/backend/StarvationGlobalAnalysis.ml @@ -33,7 +33,7 @@ let iter_summary ~f exe_env (summary : Summary.t) = Payloads.starvation summary.payloads |> Option.iter ~f:(fun (payload : summary) -> let pname = Summary.get_proc_name summary in - let tenv = Exe_env.get_tenv exe_env pname in + let tenv = Exe_env.get_proc_tenv exe_env pname in if StarvationModels.is_java_main_method pname || ConcurrencyModels.is_android_lifecycle_method tenv pname @@ -67,7 +67,7 @@ let report exe_env work_set = |> Option.fold ~init ~f:(fun acc summary -> let pdesc = Summary.get_proc_desc summary in let pattrs = Procdesc.get_attributes pdesc in - let tenv = Exe_env.get_tenv exe_env procname in + let tenv = Exe_env.get_proc_tenv exe_env procname in let acc = Starvation.report_on_pair ~analyze_ondemand:(fun pname -> diff --git a/infer/src/backend/preanal.ml b/infer/src/backend/preanal.ml index a5589aa3a..a0cb84077 100644 --- a/infer/src/backend/preanal.ml +++ b/infer/src/backend/preanal.ml @@ -461,7 +461,7 @@ end let do_preanalysis exe_env pdesc = let summary = Summary.OnDisk.reset pdesc in - let tenv = Exe_env.get_tenv exe_env (Procdesc.get_proc_name pdesc) in + let tenv = Exe_env.get_proc_tenv exe_env (Procdesc.get_proc_name pdesc) in let proc_name = Procdesc.get_proc_name pdesc in if Procname.is_java proc_name || Procname.is_csharp proc_name then InlineJavaSyntheticMethods.process pdesc ; diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 3d127e765..e7d8d82f8 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -617,11 +617,17 @@ let _global_variable_initialized_with_function_or_method_call = "../../documentation/issues/GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL.md"] -let guardedby_violation_racerd = +let guardedby_violation = register Warning ~id:"GUARDEDBY_VIOLATION" ~hum:"GuardedBy Violation" RacerD ~user_documentation:[%blob "../../documentation/issues/GUARDEDBY_VIOLATION.md"] +let guardedby_violation_nullsafe = + register Warning ~id:"GUARDEDBY_VIOLATION_NULLSAFE" + ~hum:"GuardedBy Violation in `@Nullsafe` Class" RacerD + ~user_documentation:[%blob "../../documentation/issues/GUARDEDBY_VIOLATION.md"] + + let impure_function = register ~id:"IMPURE_FUNCTION" Error Impurity ~user_documentation:[%blob "../../documentation/issues/IMPURE_FUNCTION.md"] @@ -894,6 +900,12 @@ let thread_safety_violation = ~user_documentation:[%blob "../../documentation/issues/THREAD_SAFETY_VIOLATION.md"] +let thread_safety_violation_nullsafe = + register Warning ~id:"THREAD_SAFETY_VIOLATION_NULLSAFE" RacerD + ~hum:"Thread Safety Violation in `@Nullsafe` Class" + ~user_documentation:[%blob "../../documentation/issues/THREAD_SAFETY_VIOLATION.md"] + + let complexity_increase ~kind ~is_on_ui_thread = register_cost ~kind ~is_on_ui_thread "%s_COMPLEXITY_INCREASE" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 5a6e258b9..c758c96f0 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -200,7 +200,9 @@ val failure_exe : t val field_not_null_checked : t -val guardedby_violation_racerd : t +val guardedby_violation : t + +val guardedby_violation_nullsafe : t val impure_function : t @@ -318,6 +320,8 @@ val symexec_memory_error : t val thread_safety_violation : t +val thread_safety_violation_nullsafe : t + val topl_biabd_error : t val topl_pulse_error : t diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 5fea408e5..d6eb14d95 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -1029,7 +1029,7 @@ let add_missing_field_to_tenv ~missing_sigma exe_env caller_tenv callee_pname hp (* if the callee is a model, then we don't have a tenv for it *) if (not callee_attributes.ProcAttributes.is_biabduction_model) && add_fields then let callee_tenv_opt = - try Some (Exe_env.get_tenv exe_env callee_pname) + try Some (Exe_env.get_proc_tenv exe_env callee_pname) with _ -> let source_file = callee_attributes.ProcAttributes.loc.Location.file in Tenv.load source_file diff --git a/infer/src/concurrency/RacerDFileAnalysis.ml b/infer/src/concurrency/RacerDFileAnalysis.ml index fdc4fc686..e35e5ddb6 100644 --- a/infer/src/concurrency/RacerDFileAnalysis.ml +++ b/infer/src/concurrency/RacerDFileAnalysis.ml @@ -18,7 +18,7 @@ type report_kind = | UnannotatedInterface (** Explain why we are reporting this access, in Java *) -let get_reporting_explanation_java report_kind tenv pname thread = +let get_reporting_explanation_java ~nullsafe report_kind tenv pname thread = let open RacerDModels in (* best explanation is always that the current class or method is annotated thread-safe. try for that first. *) @@ -46,46 +46,62 @@ let get_reporting_explanation_java report_kind tenv pname thread = | _ -> None ) in - match (report_kind, annotation_explanation_opt) with - | GuardedByViolation, _ -> - ( IssueType.guardedby_violation_racerd - , F.asprintf "@\n Reporting because field is annotated %a" MF.pp_monospaced "@GuardedBy" ) - | UnannotatedInterface, Some threadsafe_explanation -> - (IssueType.interface_not_thread_safe, F.asprintf "%s." threadsafe_explanation) - | UnannotatedInterface, None -> - Logging.die InternalError - "Reporting non-threadsafe interface call, but can't find a @ThreadSafe annotation" - | _, Some threadsafe_explanation when RacerDDomain.ThreadsDomain.is_any thread -> - ( IssueType.thread_safety_violation - , F.asprintf - "%s, so we assume that this method can run in parallel with other non-private methods in \ - the class (including itself)." - threadsafe_explanation ) - | _, Some threadsafe_explanation -> - ( IssueType.thread_safety_violation - , F.asprintf - "%s. Although this access is not known to run on a background thread, it may happen in \ - parallel with another access that does." - threadsafe_explanation ) - | _, None -> - (* failed to explain based on @ThreadSafe annotation; have to justify using background thread *) - if RacerDDomain.ThreadsDomain.is_any thread then - ( IssueType.thread_safety_violation - , F.asprintf "@\n Reporting because this access may occur on a background thread." ) - else - ( IssueType.thread_safety_violation + let issue_type, explanation, should_add_nullsafe_trailer = + match (report_kind, annotation_explanation_opt) with + | GuardedByViolation, _ -> + ( IssueType.(if nullsafe then guardedby_violation_nullsafe else guardedby_violation) + , F.asprintf "@\n Reporting because field is annotated %a" MF.pp_monospaced "@GuardedBy" + , nullsafe ) + | UnannotatedInterface, Some threadsafe_explanation -> + (IssueType.interface_not_thread_safe, F.asprintf "%s." threadsafe_explanation, false) + | UnannotatedInterface, None -> + Logging.die InternalError + "Reporting non-threadsafe interface call, but can't find a @ThreadSafe annotation" + | _, Some threadsafe_explanation when RacerDDomain.ThreadsDomain.is_any thread -> + ( IssueType.(if nullsafe then thread_safety_violation_nullsafe else thread_safety_violation) , F.asprintf - "@\n\ - \ Reporting because another access to the same memory occurs on a background thread, \ - although this access may not." ) + "%s, so we assume that this method can run in parallel with other non-private methods \ + in the class (including itself)." + threadsafe_explanation + , nullsafe ) + | _, Some threadsafe_explanation -> + ( IssueType.(if nullsafe then thread_safety_violation_nullsafe else thread_safety_violation) + , F.asprintf + "%s. Although this access is not known to run on a background thread, it may happen in \ + parallel with another access that does." + threadsafe_explanation + , nullsafe ) + | _, None -> + (* failed to explain based on @ThreadSafe annotation; have to justify using background thread *) + if RacerDDomain.ThreadsDomain.is_any thread then + ( IssueType.( + if nullsafe then thread_safety_violation_nullsafe else thread_safety_violation) + , F.asprintf "@\n Reporting because this access may occur on a background thread." + , nullsafe ) + else + ( IssueType.( + if nullsafe then thread_safety_violation_nullsafe else thread_safety_violation) + , F.asprintf + "@\n\ + \ Reporting because another access to the same memory occurs on a background thread, \ + although this access may not." + , nullsafe ) + in + let explanation = + if should_add_nullsafe_trailer then + F.sprintf "%s@\n Data races in `@Nullsafe` classes may still cause NPEs." explanation + else explanation + in + (issue_type, explanation) (** Explain why we are reporting this access, in C++ *) let get_reporting_explanation_cpp = (IssueType.lock_consistency_violation, "") (** Explain why we are reporting this access *) -let get_reporting_explanation report_kind tenv pname thread = - if Procname.is_java pname then get_reporting_explanation_java report_kind tenv pname thread +let get_reporting_explanation ~nullsafe report_kind tenv pname thread = + if Procname.is_java pname then + get_reporting_explanation_java ~nullsafe report_kind tenv pname thread else get_reporting_explanation_cpp @@ -137,7 +153,7 @@ type reported_access = ; tenv: Tenv.t ; procname: Procname.t } -let report_thread_safety_violation ~make_description ~report_kind +let report_thread_safety_violation ~make_description ~report_kind ~nullsafe ({threads; snapshot; tenv; procname= pname} : reported_access) issue_log = let open RacerDDomain in let final_pname = List.last snapshot.trace |> Option.value_map ~default:pname ~f:CallSite.pname in @@ -148,7 +164,9 @@ let report_thread_safety_violation ~make_description ~report_kind (* what the potential bug is *) let description = make_description pname final_sink_site initial_sink_site snapshot in (* why we are reporting it *) - let issue_type, explanation = get_reporting_explanation report_kind tenv pname threads in + let issue_type, explanation = + get_reporting_explanation ~nullsafe report_kind tenv pname threads + in let error_message = F.sprintf "%s%s" description explanation in let end_locs = Option.to_list original_end @ Option.to_list conflict_end in let access = IssueAuxData.encode end_locs in @@ -165,8 +183,8 @@ let report_unannotated_interface_violation reported_pname reported_access issue_ interface with %a or adding a lock." describe_pname reported_pname MF.pp_monospaced class_name MF.pp_monospaced "@ThreadSafe" in - report_thread_safety_violation ~make_description ~report_kind:UnannotatedInterface - reported_access issue_log + report_thread_safety_violation ~nullsafe:false ~make_description + ~report_kind:UnannotatedInterface reported_access issue_log | _ -> (* skip reporting on C++ *) issue_log @@ -403,6 +421,17 @@ let should_report_guardedby_violation classname ({snapshot; tenv; procname} : re false +let should_report_race_in_nullsafe_class ({snapshot; tenv} : reported_access) = + match snapshot.elem.access with + | Read {exp= (FieldOffset (Dereference (Base _), _) | FieldOffset (Base _, _)) as exp} + | Write {exp= (FieldOffset (Dereference (Base _), _) | FieldOffset (Base _, _)) as exp} -> + AccessExpression.get_typ exp tenv + |> Option.exists ~f:(fun typ -> Typ.is_java_type typ && not (Typ.is_java_primitive_type typ)) + | _ -> + (* allow normal reporting for all other cases *) + false + + (** Report accesses that may race with each other. Principles for race reporting. @@ -430,21 +459,28 @@ let should_report_guardedby_violation classname ({snapshot; tenv; procname} : re The above is tempered at the moment by abstractions of "same lock" and "same thread": we are currently not distinguishing different locks, and are treating "known to be confined to a thread" as if "known to be confined to UI thread". *) -let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportMap.t) = +let report_unsafe_accesses ~issue_log file_tenv classname (aggregated_access_map : ReportMap.t) = let open RacerDDomain in let open RacerDModels in - let report_thread_safety_violation ~acc ~make_description ~report_kind reported_access = + let class_is_annotated_nullsafe = + Tenv.lookup file_tenv classname + |> Option.exists ~f:(fun tstruct -> + Annotations.(struct_typ_has_annot tstruct (fun annot -> ia_ends_with annot nullsafe)) ) + in + let report_thread_safety_violation ~acc ~make_description ~report_kind ~nullsafe reported_access = ReportedSet.deduplicate - ~f:(report_thread_safety_violation ~make_description ~report_kind) + ~f:(report_thread_safety_violation ~make_description ~report_kind ~nullsafe) reported_access acc in let report_unannotated_interface_violation ~acc reported_pname reported_access = - ReportedSet.deduplicate + ReportedSet.deduplicate reported_access acc ~f:(report_unannotated_interface_violation reported_pname) - reported_access acc in let report_unsafe_access accesses acc ({snapshot; threads; tenv; procname= pname} as reported_access) = + let nullsafe = + class_is_annotated_nullsafe && should_report_race_in_nullsafe_class reported_access + in match snapshot.elem.access with | InterfaceCall {pname= reported_pname} when AccessSnapshot.is_unprotected snapshot @@ -472,7 +508,7 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM && (Option.is_some conflict || ThreadsDomain.is_any threads) then report_thread_safety_violation ~acc ~make_description:make_unprotected_write_description - ~report_kind:(WriteWriteRace conflict) reported_access + ~report_kind:(WriteWriteRace conflict) ~nullsafe reported_access else acc | Write _ | ContainerWrite _ -> (* Do not report unprotected writes for ObjC_Cpp *) @@ -493,7 +529,8 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM make_read_write_race_description ~read_is_sync:false conflict in let report_kind = ReadWriteRace conflict.snapshot in - report_thread_safety_violation ~acc ~make_description ~report_kind reported_access ) + report_thread_safety_violation ~acc ~make_description ~report_kind ~nullsafe + reported_access ) | (Read _ | ContainerRead _) when Procname.is_java pname -> (* protected read. report unprotected writes and opposite protected writes as conflicts *) let can_conflict (snapshot1 : AccessSnapshot.t) (snapshot2 : AccessSnapshot.t) = @@ -512,7 +549,8 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM make_read_write_race_description ~read_is_sync:true conflict in let report_kind = ReadWriteRace conflict.snapshot in - report_thread_safety_violation ~acc ~make_description ~report_kind reported_access ) + report_thread_safety_violation ~acc ~make_description ~report_kind ~nullsafe + reported_access ) | Read _ | ContainerRead _ -> (* Do not report protected reads for ObjC_Cpp *) acc @@ -529,8 +567,9 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM if Config.racerd_guardedby then List.fold grouped_accesses ~init ~f:(fun acc r -> if should_report_guardedby_violation classname r then + let nullsafe = class_is_annotated_nullsafe && should_report_race_in_nullsafe_class r in report_thread_safety_violation ~acc ~report_kind:GuardedByViolation - ~make_description:make_guardedby_violation_description r + ~make_description:make_guardedby_violation_description ~nullsafe r else acc ) else init in @@ -540,7 +579,8 @@ let report_unsafe_accesses ~issue_log classname (aggregated_access_map : ReportM |> report_guardedby_violations_on_location grouped_accesses |> report_accesses_on_location grouped_accesses in - ReportMap.fold report aggregated_access_map (ReportedSet.empty_of_issue_log issue_log) + ReportedSet.empty_of_issue_log issue_log + |> ReportMap.fold report aggregated_access_map |> ReportedSet.to_issue_log @@ -557,7 +597,7 @@ let make_results_table exe_env summaries = in List.fold summaries ~init:ReportMap.empty ~f:(fun acc (proc_desc, summary) -> let procname = Procdesc.get_proc_name proc_desc in - let tenv = Exe_env.get_tenv exe_env procname in + let tenv = Exe_env.get_proc_tenv exe_env procname in aggregate_post tenv procname acc summary ) @@ -589,7 +629,7 @@ let aggregate_by_class {InterproceduralAnalysis.procedures; file_exe_env; analyz |> Option.bind ~f:(fun classname -> analyze_file_dependency procname |> Option.filter ~f:(fun (pdesc, _) -> - let tenv = Exe_env.get_tenv file_exe_env procname in + let tenv = Exe_env.get_proc_tenv file_exe_env procname in should_report_on_proc tenv pdesc ) |> Option.map ~f:(fun summary_proc_desc -> Typ.Name.Map.update classname @@ -605,9 +645,11 @@ let aggregate_by_class {InterproceduralAnalysis.procedures; file_exe_env; analyz (** Gathers results by analyzing all the methods in a file, then post-processes the results to check an (approximation of) thread safety *) -let analyze ({InterproceduralAnalysis.file_exe_env} as file_t) = +let analyze ({InterproceduralAnalysis.file_exe_env; source_file} as file_t) = let class_map = aggregate_by_class file_t in Typ.Name.Map.fold (fun classname methods issue_log -> - make_results_table file_exe_env methods |> report_unsafe_accesses ~issue_log classname ) + let file_tenv = Exe_env.get_sourcefile_tenv file_exe_env source_file in + make_results_table file_exe_env methods + |> report_unsafe_accesses ~issue_log file_tenv classname ) class_map IssueLog.empty diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 96befa192..4bbfdd2ac 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -862,7 +862,7 @@ let reporting {InterproceduralAnalysis.procedures; file_exe_env; analyze_file_de analyze_file_dependency procname |> Option.value_map ~default:report_map ~f:(fun (proc_desc, summary) -> let attributes = Procdesc.get_attributes proc_desc in - let tenv = Exe_env.get_tenv file_exe_env procname in + let tenv = Exe_env.get_proc_tenv file_exe_env procname in if should_report attributes then report_on_proc tenv attributes report_map summary else report_map ) in diff --git a/infer/src/cost/cost.ml b/infer/src/cost/cost.ml index 6a12d2d3d..8407b6c5b 100644 --- a/infer/src/cost/cost.ml +++ b/infer/src/cost/cost.ml @@ -400,7 +400,7 @@ let just_throws_exception proc_desc = let checker ({InterproceduralAnalysis.proc_desc; exe_env; analyze_dependency} as analysis_data) = let proc_name = Procdesc.get_proc_name proc_desc in - let tenv = Exe_env.get_tenv exe_env proc_name in + let tenv = Exe_env.get_proc_tenv exe_env proc_name in let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in let inferbo_invariant_map = BufferOverrunAnalysis.cached_compute_invariant_map diff --git a/infer/src/cost/hoisting.ml b/infer/src/cost/hoisting.ml index bcaaa979a..f9e7337bd 100644 --- a/infer/src/cost/hoisting.ml +++ b/infer/src/cost/hoisting.ml @@ -160,7 +160,7 @@ let report_errors proc_desc tenv err_log get_callee_purity reaching_defs_invaria let checker ({InterproceduralAnalysis.proc_desc; exe_env; err_log; analyze_dependency} as analysis_data) = let proc_name = Procdesc.get_proc_name proc_desc in - let tenv = Exe_env.get_tenv exe_env proc_name in + let tenv = Exe_env.get_proc_tenv exe_env proc_name in let integer_type_widths = Exe_env.get_integer_type_widths exe_env proc_name in let cfg = InstrCFG.from_pdesc proc_desc in (* computes reaching defs: node -> (var -> node set) *) diff --git a/infer/tests/codetoanalyze/java/racerd/NullsafeMode.java b/infer/tests/codetoanalyze/java/racerd/NullsafeMode.java new file mode 100644 index 000000000..73670ad4c --- /dev/null +++ b/infer/tests/codetoanalyze/java/racerd/NullsafeMode.java @@ -0,0 +1,38 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +package codetoanalyze.java.checkers; + +import com.facebook.infer.annotation.Nullsafe; +import javax.annotation.Nullable; +import javax.annotation.concurrent.GuardedBy; +import javax.annotation.concurrent.ThreadSafe; + +@Nullsafe(Nullsafe.Mode.LOCAL) +@ThreadSafe +public class NullsafeMode { + private @Nullable Object nullableField; + + public void resetBad() { + this.nullableField = null; + } + + public String getStringBad() { + if (this.nullableField != null) { + return nullableField.toString(); + } else { + return ""; + } + } + + @GuardedBy("this") + private @Nullable Object nullableGuardedField; + + public void unlockedWriteBad() { + nullableGuardedField = null; + } +} diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index 3cc89b0e6..9bb9ddef0 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -75,6 +75,10 @@ codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.tryLockN codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.tryLockWrongBranchBad():void, 98, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.f`] codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.unownedReadBad():java.lang.Object, 362, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [,access to `this.mField3`,,call to void Locks.lockedWriteInCallee2(),access to `this.mField3`] codetoanalyze/java/racerd/Locks.java, codetoanalyze.java.checkers.Locks.useLockInCalleeBad():void, 221, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `this.f`] +codetoanalyze/java/racerd/NullsafeMode.java, codetoanalyze.java.checkers.NullsafeMode.getStringBad():java.lang.String, 25, THREAD_SAFETY_VIOLATION_NULLSAFE, no_bucket, WARNING, [,access to `this.nullableField`,,access to `this.nullableField`] +codetoanalyze/java/racerd/NullsafeMode.java, codetoanalyze.java.checkers.NullsafeMode.resetBad():void, 21, THREAD_SAFETY_VIOLATION_NULLSAFE, no_bucket, WARNING, [access to `this.nullableField`] +codetoanalyze/java/racerd/NullsafeMode.java, codetoanalyze.java.checkers.NullsafeMode.unlockedWriteBad():void, 36, GUARDEDBY_VIOLATION_NULLSAFE, no_bucket, WARNING, [access to `this.nullableGuardedField`] +codetoanalyze/java/racerd/NullsafeMode.java, codetoanalyze.java.checkers.NullsafeMode.unlockedWriteBad():void, 36, THREAD_SAFETY_VIOLATION_NULLSAFE, no_bucket, WARNING, [access to `this.nullableGuardedField`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.(codetoanalyze.java.checkers.Obj,java.lang.Object), 66, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [access to `obj.f`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.cantOwnThisBad():void, 171, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.setField(Obj),access to `this.field`] codetoanalyze/java/racerd/Ownership.java, codetoanalyze.java.checkers.Ownership.notOwnedInCalleeBad(codetoanalyze.java.checkers.Obj):void, 226, THREAD_SAFETY_VIOLATION, no_bucket, WARNING, [call to void Ownership.mutateIfNotNull(Obj),access to `o.f`]