diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index c70016835..4caffe594 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -99,6 +99,7 @@ let eradicate_return_value_not_present = from_string "ERADICATE_RETURN_VALUE_NOT_PRESENT" ~hum:"Return Value Not Present" let eradicate_value_not_present = from_string "ERADICATE_VALUE_NOT_PRESENT" ~hum:"Value Not Present" +let field_should_be_nullable = from_string "FIELD_SHOULD_BE_NULLABLE" let field_not_null_checked = from_string "IVAR_NOT_NULL_CHECKED" let inherently_dangerous_function = from_string "INHERENTLY_DANGEROUS_FUNCTION" let memory_leak = from_string "MEMORY_LEAK" diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index c0cc3c0a9..188955543 100644 --- a/infer/src/IR/Localise.mli +++ b/infer/src/IR/Localise.mli @@ -72,6 +72,7 @@ val eradicate_return_not_nullable : t val eradicate_return_over_annotated : t val eradicate_return_value_not_present : t val eradicate_value_not_present : t +val field_should_be_nullable : t val field_not_null_checked : t val inherently_dangerous_function : t val memory_leak : t diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 80b139797..3dafe94e9 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -520,7 +520,8 @@ and (annotation_reachability, quandary, repeated_calls, siof, - threadsafety) = + threadsafety, + suggest_nullable) = let annotation_reachability = CLOpt.mk_bool ~long:"annotation-reachability" ~in_help:CLOpt.[Analyze, manual_generic] ~default:true @@ -578,7 +579,11 @@ and (annotation_reachability, and threadsafety = CLOpt.mk_bool ~long:"threadsafety" ~in_help:CLOpt.[Analyze, manual_generic] ~default:true - "the thread safety analysis" in + "the thread safety analysis" + + and suggest_nullable = + CLOpt.mk_bool ~long:"suggest-nullable" ~default:false + "Nullable annotation sugesstions analysis (experimental)" in (* IMPORTANT: keep in sync with the checkers that have ~default:true above *) let default_checkers = @@ -602,7 +607,8 @@ and (annotation_reachability, quandary, repeated_calls, siof, - threadsafety) + threadsafety, + suggest_nullable) and annotation_reachability_custom_pairs = CLOpt.mk_json ~long:"annotation-reachability-custom-pairs" @@ -1819,6 +1825,7 @@ and models_mode = !models_mode and modified_targets = !modified_targets and monitor_prop_size = !monitor_prop_size and nelseg = !nelseg +and suggest_nullable = !suggest_nullable and no_translate_libs = not !headers and objc_memory_model_on = !objc_memory_model and only_footprint = !only_footprint diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 23ae1836a..13f7f7697 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -332,6 +332,7 @@ val stacktraces_dir : string option val stats_mode : bool val stats_report : string option val subtype_multirange : bool +val suggest_nullable: bool val svg : bool val symops_per_iteration : int option val test : bool diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml new file mode 100644 index 000000000..4328616ca --- /dev/null +++ b/infer/src/checkers/NullabilitySuggest.ml @@ -0,0 +1,98 @@ +(* + * 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. + *) +open! IStd + +module F = Format +module L = Logging + +module Domain = + AbstractDomain.FiniteSet(struct + type t = AccessPath.Raw.t * Location.t + + (* Ignore location while comparing access paths. + * They are there just for error reporting purpose, and are pretty much irrelevant + * from the analysis' perspective *) + let compare (ap0, _) (ap1, _) = [%compare: AccessPath.Raw.t] ap0 ap1 + + let pp fmt (ap, loc) = F.fprintf fmt "(%a, %a)" AccessPath.Raw.pp ap Location.pp loc + end) + +(* Right now this is just a placeholder. We'll change it to something useful when necessary *) +module Summary = Summary.Make(struct + type payload = unit + + let update_payload _ summary = summary + let read_payload _ = None + end) + +type extras = unit + +module TransferFunctions (CFG : ProcCfg.S) = struct + module CFG = CFG + module Domain = Domain + type nonrec extras = extras + + let is_null = HilExp.is_null_literal + + let is_access_nullable ap proc_data = + match AccessPath.Raw.get_field_and_annotation ap proc_data.ProcData.tenv with + | Some (_, annot_item) -> + Annotations.ia_is_nullable annot_item + | _ -> false + + let exec_instr (astate : Domain.astate) proc_data _ (instr : HilInstr.t) = + match instr with + | Assume _ -> + (* For now we just assume that conditionals does not have any implications on nullability *) + astate + | Call _ -> + (* For now we just assume the callee always return non-null *) + astate + | Assign (lhs, rhs, loc) -> + if is_null rhs && not (is_access_nullable lhs proc_data) then + Domain.add (lhs, loc) astate + else + astate +end + +module Analyzer = + AbstractInterpreter.Make + (ProcCfg.Exceptional) + (LowerHil.Make (TransferFunctions)) +module Interprocedural = AbstractInterpreter.Interprocedural (Summary) + +let checker callback = + let report nullable_aps (proc_data : extras ProcData.t) = + let report_access_path (ap, loc) = + let pname = Procdesc.get_proc_name proc_data.pdesc in + let issue_kind = Localise.to_issue_id Localise.field_should_be_nullable in + match AccessPath.Raw.get_field_and_annotation ap proc_data.tenv with + | Some (field_name, _) -> + let message = + F.asprintf "Field %s should be annotated with @Nullable" + (Fieldname.to_string field_name) in + let exn = Exceptions.Checkers (issue_kind, Localise.verbatim_desc message) in + Reporting.log_warning pname ~loc exn + | _ -> () + in + Domain.iter report_access_path nullable_aps + in + let compute_post (proc_data : extras ProcData.t) = + (* Assume all fields are not null in the beginning *) + let initial = Domain.empty, IdAccessPathMapDomain.empty in + match Analyzer.compute_post proc_data ~initial ~debug:false with + | Some (post, _) -> + report post proc_data; + Some () + | None -> + failwithf + "Analyzer failed to compute post for %a" + Typ.Procname.pp (Procdesc.get_proc_name proc_data.pdesc) + in + Interprocedural.compute_and_store_post ~compute_post ~make_extras:(fun _ -> ()) callback diff --git a/infer/src/checkers/NullabilitySuggest.mli b/infer/src/checkers/NullabilitySuggest.mli new file mode 100644 index 000000000..4e3825c84 --- /dev/null +++ b/infer/src/checkers/NullabilitySuggest.mli @@ -0,0 +1,13 @@ +(* + * 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. + *) + +(* Module that suggest adding nullability annotations *) + +open! IStd +val checker: Callbacks.proc_callback_t diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index b839fe6b2..c36427508 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -50,20 +50,62 @@ module Raw = struct | base, _ :: [] -> base, [] | base, accesses -> base, List.rev (List.tl_exn (List.rev accesses)) - let get_typ ((_, base_typ), accesses) tenv = - let rec accesses_get_typ last_typ tenv = function + let lookup_field_type_annot tenv base_typ field_name = + let lookup = Tenv.lookup tenv in + Typ.Struct.get_field_type_and_annotation ~lookup field_name base_typ + + (* Get the type of an access, or None if the type cannot be determined *) + let get_access_type tenv base_typ = function + | FieldAccess field_name -> + Option.map (lookup_field_type_annot tenv base_typ field_name) ~f:fst + | ArrayAccess array_typ -> + Some array_typ + + (* For field access, get the field name and the annotation associated with it + * Return None if given an array access, or if the info cannot be obtained *) + let get_access_field_annot tenv base_typ = function + | FieldAccess field_name -> + Option.map (lookup_field_type_annot tenv base_typ field_name) ~f:( + fun (_, annot) -> (field_name, annot) + ) + | ArrayAccess _ -> + None + + (* Extract the last access of the given access path together with its base type. + * Here the base type is defined to be the declaring class of the last accessed field, + * or the type of base if the access list is empty. + * For example: + * - for x.f.g, the base type of the last access is typ(f); + * - for x.f[][], the base type of the last access is typ(x); + * - for x, the base type of the last access is type(x) *) + let last_access_info ((_, base_typ), accesses) tenv = + let rec last_access_info_impl tenv base_typ = function | [] -> - Some last_typ - | FieldAccess field_name :: accesses -> - let lookup = Tenv.lookup tenv in - begin - match Typ.Struct.get_field_type_and_annotation ~lookup field_name last_typ with - | Some (field_typ, _) -> accesses_get_typ field_typ tenv accesses - | None -> None - end - | ArrayAccess array_typ :: accesses -> - accesses_get_typ array_typ tenv accesses in - accesses_get_typ base_typ tenv accesses + Some base_typ, None + | [last_access] -> + Some base_typ, Some last_access + | curr_access :: rest -> + match get_access_type tenv base_typ curr_access with + | Some access_typ -> + last_access_info_impl tenv access_typ rest + | None -> + None, None + in + last_access_info_impl tenv base_typ accesses + + let get_field_and_annotation ap tenv = + match last_access_info ap tenv with + | Some base_typ, Some access -> + get_access_field_annot tenv base_typ access + | _ -> None + + let get_typ ap tenv = + match last_access_info ap tenv with + | (Some _) as typ, None -> typ + | Some base_typ, Some access -> + get_access_type tenv base_typ access + | _ -> + None let pp fmt = function | base, [] -> pp_base fmt base diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index dc9e8a2bb..4d9d0a4ca 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -27,6 +27,10 @@ module Raw : sig original access path if the access list is empty *) val truncate : t -> t + (** get the field name and the annotation of the last access in the list of accesses if + the list is non-empty and the last access is a field access *) + val get_field_and_annotation : t -> Tenv.t -> (Fieldname.t * Annot.Item.t) option + (** get the typ of the last access in the list of accesses if the list is non-empty, or the base if the list is empty. that is, for x.f.g, return typ(g), and for x, return typ(x) *) val get_typ : t -> Tenv.t -> Typ.t option diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 7e3737a68..bc35dda49 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -37,6 +37,8 @@ let checkers = [ "immutable cast", Config.immutable_cast, [Procedure ImmutableChecker.callback_check_immutable_cast, Config.Java]; "printf args", Config.printf_args, [Procedure PrintfArgs.callback_printf_args, Config.Java]; + "nullable suggestion", Config.suggest_nullable, + [Procedure NullabilitySuggest.checker, Config.Java]; "quandary", Config.quandary, [Procedure JavaTaintAnalysis.checker, Config.Java; Procedure ClangTaintAnalysis.checker, Config.Clang]; diff --git a/infer/tests/codetoanalyze/java/checkers/FragmentDoesNotRetainViewExample.java b/infer/tests/codetoanalyze/java/checkers/FragmentDoesNotRetainViewExample.java index cfc6cc281..ec467c839 100644 --- a/infer/tests/codetoanalyze/java/checkers/FragmentDoesNotRetainViewExample.java +++ b/infer/tests/codetoanalyze/java/checkers/FragmentDoesNotRetainViewExample.java @@ -16,6 +16,7 @@ import android.view.LayoutInflater; import android.view.View; import android.view.ViewGroup; import android.widget.ListView; +import javax.annotation.Nullable; public class FragmentDoesNotRetainViewExample extends Fragment { @@ -27,10 +28,10 @@ public class FragmentDoesNotRetainViewExample extends Fragment { } - View mView1; - View mView2; - ViewGroup mViewSubclass; - CustomView mCustomView; + @Nullable View mView1; + @Nullable View mView2; + @Nullable ViewGroup mViewSubclass; + @Nullable CustomView mCustomView; boolean b; diff --git a/infer/tests/codetoanalyze/java/checkers/Makefile b/infer/tests/codetoanalyze/java/checkers/Makefile index 4d7f6f984..b2270782a 100644 --- a/infer/tests/codetoanalyze/java/checkers/Makefile +++ b/infer/tests/codetoanalyze/java/checkers/Makefile @@ -8,7 +8,7 @@ TESTS_DIR = ../../.. ANALYZER = checkers -INFER_OPTIONS = --no-filtering --debug-exceptions --default-checkers --resource-leak +INFER_OPTIONS = --no-filtering --debug-exceptions --default-checkers --resource-leak --suggest-nullable INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java b/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java new file mode 100644 index 000000000..133bfa204 --- /dev/null +++ b/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java @@ -0,0 +1,47 @@ +/* + * 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 javax.annotation.Nullable; + +public class NullableSuggest { + private Object obj0; + @Nullable private Object obj1; + + private static class OtherClass { + private Object obj2; + @Nullable private Object obj3; + } + + public void noAssignNullOk() { + } + + public void assignNotNullOk() { + obj0 = new Object(); + obj1 = new Object(); + } + + public void assignNullBad() { + obj0 = null; + } + + public void assignNullToNullableOk() { + obj1 = null; + } + + public void assignNullToFieldInOtherClassBad() { + OtherClass oc = new OtherClass(); + oc.obj2 = null; + } + + public void assignNullToNullableFieldInOtherClassOk() { + OtherClass oc = new OtherClass(); + oc.obj3 = null; + } +} diff --git a/infer/tests/codetoanalyze/java/checkers/issues.exp b/infer/tests/codetoanalyze/java/checkers/issues.exp index 7eaf5930f..3b6fc8306 100644 --- a/infer/tests/codetoanalyze/java/checkers/issues.exp +++ b/infer/tests/codetoanalyze/java/checkers/issues.exp @@ -36,6 +36,8 @@ codetoanalyze/java/checkers/Leaks.java, void Leaks.basicLeakBad(), 2, RESOURCE_L codetoanalyze/java/checkers/Leaks.java, void Leaks.doubleLeakBad(), 3, RESOURCE_LEAK, [] codetoanalyze/java/checkers/NoAllocationExample.java, void NoAllocationExample.directlyAllocatingMethod(), 1, CHECKERS_ALLOCATES_MEMORY, [] codetoanalyze/java/checkers/NoAllocationExample.java, void NoAllocationExample.indirectlyAllocatingMethod(), 1, CHECKERS_ALLOCATES_MEMORY, [] +codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullBad(), 1, FIELD_SHOULD_BE_NULLABLE, [] +codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullToFieldInOtherClassBad(), 2, FIELD_SHOULD_BE_NULLABLE, [] codetoanalyze/java/checkers/PrintfArgsChecker.java, void PrintfArgsChecker.formatStringIsNotLiteral(PrintStream), 2, CHECKERS_PRINTF_ARGS, [Format string must be string literal] codetoanalyze/java/checkers/PrintfArgsChecker.java, void PrintfArgsChecker.stringInsteadOfInteger(PrintStream), 1, CHECKERS_PRINTF_ARGS, [printf(...) at line 40: parameter 2 is expected to be of type java.lang.Integer but java.lang.String was given.] codetoanalyze/java/checkers/PrintfArgsChecker.java, void PrintfArgsChecker.wrongNumberOfArguments(PrintStream), 1, CHECKERS_PRINTF_ARGS, [format string arguments don't mach provided arguments in printf(...) at line 44]