From 6fc287656f5dee20effc8362b42f47239655575f Mon Sep 17 00:00:00 2001 From: Jia Chen Date: Thu, 1 Jun 2017 13:31:36 -0700 Subject: [PATCH] Transitively track null assignment in NullabliltySuggest Reviewed By: jeremydubreil, sblackshear Differential Revision: D5158809 fbshipit-source-id: 485c58d --- infer/src/checkers/NullabilitySuggest.ml | 107 +++++++++++++++--- infer/src/checkers/accessPath.ml | 3 + infer/src/checkers/accessPath.mli | 3 + .../java/checkers/NullableSuggest.java | 41 +++++++ .../codetoanalyze/java/checkers/issues.exp | 7 +- 5 files changed, 142 insertions(+), 19 deletions(-) diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index 4328616ca..7e74f755d 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/infer/src/checkers/NullabilitySuggest.ml @@ -11,17 +11,42 @@ open! IStd module F = Format module L = Logging -module Domain = - AbstractDomain.FiniteSet(struct - type t = AccessPath.Raw.t * Location.t +module UseDefChain = struct + type astate = + | NullDef of (Location.t * AccessPath.Raw.t) + | DependsOn of (Location.t * AccessPath.Raw.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 + (* We explicitly write out the comparator here instead of relying on + * [@@deriving compare], as the alternative may not always guarantee the + * desirable order. *) + let compare_astate lhs rhs = match lhs, rhs with + | NullDef lorig, NullDef rorig -> + [%compare : Location.t * AccessPath.Raw.t] rorig lorig + | DependsOn ldep, DependsOn rdep -> + [%compare : Location.t * AccessPath.Raw.t] rdep ldep + | NullDef _, DependsOn _ -> + 1 + | DependsOn _, NullDef _ -> + -1 - let pp fmt (ap, loc) = F.fprintf fmt "(%a, %a)" AccessPath.Raw.pp ap Location.pp loc - end) + let (<=) ~lhs ~rhs = + compare_astate lhs rhs <= 0 + + (* Keep only one chain in join/widen as we are going to report only one + * trace to the user eventually. *) + let join lhs rhs = + if (<=) ~lhs ~rhs then rhs else lhs + + let widen ~prev ~next ~num_iters:_ = + join prev next + + let pp fmt = function + | NullDef (loc, ap) -> + F.fprintf fmt "NullDef(%a, %a)" Location.pp loc AccessPath.Raw.pp ap + | DependsOn (loc, ap) -> + F.fprintf fmt "DependsOn(%a, %a)" Location.pp loc AccessPath.Raw.pp ap +end +module Domain = AbstractDomain.Map (AccessPath.Raw) (UseDefChain) (* Right now this is just a placeholder. We'll change it to something useful when necessary *) module Summary = Summary.Make(struct @@ -38,14 +63,23 @@ module TransferFunctions (CFG : ProcCfg.S) = struct 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 nullable_usedef_chain_of exp lhs astate loc = + match exp with + | HilExp.Constant (Cint n) when IntLit.isnull n -> + Some (UseDefChain.NullDef (loc, lhs)) + | HilExp.AccessPath ap -> + if Domain.mem ap astate then + Some (UseDefChain.DependsOn (loc, ap)) + else + None + | _ -> None + let exec_instr (astate : Domain.astate) proc_data _ (instr : HilInstr.t) = match instr with | Assume _ -> @@ -55,8 +89,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (* 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 + if not (is_access_nullable lhs proc_data) then + match nullable_usedef_chain_of rhs lhs astate loc with + | Some udchain -> + Domain.add lhs udchain astate + | None -> + astate else astate end @@ -67,9 +105,38 @@ module Analyzer = (LowerHil.Make (TransferFunctions)) module Interprocedural = AbstractInterpreter.Interprocedural (Summary) +let make_error_trace astate ap ud = + let name_of ap = + match AccessPath.Raw.get_last_access ap with + | Some (AccessPath.FieldAccess field_name) -> + "Field " ^ (Fieldname.to_flat_string field_name) + | Some (AccessPath.ArrayAccess _) -> + "Some array element" + | None -> + "Variable" + in + let open UseDefChain in + let rec error_trace_impl depth ap = function + | NullDef (loc, src) -> + let msg = F.sprintf "%s is assigned null here" (name_of src) in + let ltr = [Errlog.make_trace_element depth loc msg []] in + Some (loc, ltr) + | DependsOn (loc, dep) -> + try + let ud' = Domain.find dep astate in + let msg = F.sprintf "%s could be assigned here" (name_of ap) in + let trace_elem = Errlog.make_trace_element depth loc msg [] in + Option.map (error_trace_impl (depth+1) dep ud') ~f:( + fun (_, trace) -> loc, trace_elem :: trace + ) + with + Not_found -> None + in + error_trace_impl 0 ap ud + let checker callback = - let report nullable_aps (proc_data : extras ProcData.t) = - let report_access_path (ap, loc) = + let report astate (proc_data : extras ProcData.t) = + let report_access_path ap udchain = 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 @@ -78,10 +145,16 @@ let checker callback = 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 + begin + match make_error_trace astate ap udchain with + | Some (loc, ltr) -> + Reporting.log_warning pname ~loc ~ltr exn + | None -> + Reporting.log_warning pname exn + end | _ -> () in - Domain.iter report_access_path nullable_aps + Domain.iter report_access_path astate in let compute_post (proc_data : extras ProcData.t) = (* Assume all fields are not null in the beginning *) diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index c36427508..72d4804cf 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -93,6 +93,9 @@ module Raw = struct in last_access_info_impl tenv base_typ accesses + let get_last_access (_, accesses) = + List.last accesses + let get_field_and_annotation ap tenv = match last_access_info ap tenv with | Some base_typ, Some access -> diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index 4d9d0a4ca..4e8a4ee66 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -27,6 +27,9 @@ module Raw : sig original access path if the access list is empty *) val truncate : t -> t + (** get the last access in the list. returns None if the list is empty *) + val get_last_access : t -> access option + (** 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 diff --git a/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java b/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java index 133bfa204..bc0e849a9 100644 --- a/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java +++ b/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java @@ -44,4 +44,45 @@ public class NullableSuggest { OtherClass oc = new OtherClass(); oc.obj3 = null; } + + public void assignNullToNullableFieldTransitiveOk(boolean flag) { + Object origin = null; + Object intermediate = flag ? origin : new Object(); + obj1 = intermediate; + } + + public void assignNullToFieldTransitiveBad(boolean flag) { + Object origin = null; + Object intermediate = flag ? origin : new Object(); + obj0 = intermediate; + } + + public void assignNullToNullableFieldTransitiveLoopOk(int n) { + Object origin = null; + Object arr[] = new Object[n]; + for (int i = 0; i < n; ++i) { + arr[i] = origin; + } + if (n > 0) + obj1 = arr[0]; + } + + public void assignNullToFieldTransitiveLoopBad(int n) { + Object origin = null; + Object arr[] = new Object[n]; + for (int i = 0; i < n; ++i) { + arr[i] = origin; + } + if (n > 0) + obj0 = arr[0]; + } + + public void multipleChainsAlwaysSelectShortestBad(boolean flag) { + Object o0 = null; + Object o1 = null; + if (flag) + o1 = o0; + obj0 = o1; + // The analysis should report error trace o1->obj0, rather than o0->o1->obj0 + } } diff --git a/infer/tests/codetoanalyze/java/checkers/issues.exp b/infer/tests/codetoanalyze/java/checkers/issues.exp index 3b6fc8306..41643ba4d 100644 --- a/infer/tests/codetoanalyze/java/checkers/issues.exp +++ b/infer/tests/codetoanalyze/java/checkers/issues.exp @@ -36,8 +36,11 @@ 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/NullableSuggest.java, void NullableSuggest.assignNullBad(), 1, FIELD_SHOULD_BE_NULLABLE, [Field obj0 is assigned null here] +codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullToFieldInOtherClassBad(), 2, FIELD_SHOULD_BE_NULLABLE, [Field obj2 is assigned null here] +codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullToFieldTransitiveBad(boolean), 3, FIELD_SHOULD_BE_NULLABLE, [Field obj0 could be assigned here,Variable could be assigned here,Variable could be assigned here,Variable is assigned null here] +codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullToFieldTransitiveLoopBad(int), 7, FIELD_SHOULD_BE_NULLABLE, [Field obj0 could be assigned here,Some array element could be assigned here,Variable is assigned null here] +codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.multipleChainsAlwaysSelectShortestBad(boolean), 5, FIELD_SHOULD_BE_NULLABLE, [Field obj0 could be assigned here,Variable is assigned null here] 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]