diff --git a/infer/src/checkers/NullabilitySuggest.ml b/infer/src/checkers/NullabilitySuggest.ml index cff78c5d3..7cf68f496 100644 --- a/infer/src/checkers/NullabilitySuggest.ml +++ b/infer/src/checkers/NullabilitySuggest.ml @@ -15,7 +15,8 @@ module MF = MarkupFormatter module UseDefChain = struct type astate = | DependsOn of (Location.t * AccessPath.Raw.t) - | NullDef of (Location.t * AccessPath.Raw.t) + | NullDefCompare of (Location.t * AccessPath.Raw.t) + | NullDefAssign of (Location.t * AccessPath.Raw.t) [@@deriving compare] let (<=) ~lhs ~rhs = @@ -30,8 +31,10 @@ module UseDefChain = struct join prev next let pp fmt = function - | NullDef (loc, ap) -> - F.fprintf fmt "NullDef(%a, %a)" Location.pp loc AccessPath.Raw.pp ap + | NullDefAssign (loc, ap) -> + F.fprintf fmt "NullDefAssign(%a, %a)" Location.pp loc AccessPath.Raw.pp ap + | NullDefCompare (loc, ap) -> + F.fprintf fmt "NullDefCompare(%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 @@ -61,19 +64,40 @@ module TransferFunctions (CFG : ProcCfg.S) = struct 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)) + Some (UseDefChain.NullDefAssign (loc, lhs)) | HilExp.AccessPath ap -> - if Domain.mem ap astate then - Some (UseDefChain.DependsOn (loc, ap)) - else - None + begin + try + match Domain.find ap astate with + | UseDefChain.NullDefCompare _ -> + (* Stop NullDefCompare from propagating here because we want to prevent + * the checker from suggesting @Nullable on y in the following case: + * if (x == null) ... else { y = x; } *) + None + | _ -> + Some (UseDefChain.DependsOn (loc, ap)) + with + | Not_found -> None + end + | _ -> None + + let extract_null_compare_expr = function + | HilExp.BinaryOperator ((Eq | Ne), HilExp.AccessPath ap, exp) + | HilExp.BinaryOperator ((Eq | Ne), exp, HilExp.AccessPath ap) -> + Option.some_if (HilExp.is_null_literal exp) ap | _ -> None 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 + | Assume (expr, _, _, loc) -> + begin + match extract_null_compare_expr expr with + | Some ap when not (is_access_nullable ap proc_data) -> + let udchain = UseDefChain.NullDefCompare (loc, ap) in + Domain.add ap udchain astate + | _ -> + astate + end | Call _ -> (* For now we just assume the callee always return non-null *) astate @@ -106,10 +130,14 @@ let make_error_trace astate ap ud = in let open UseDefChain in let rec error_trace_impl depth ap = function - | NullDef (loc, src) -> + | NullDefAssign (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) + | NullDefCompare (loc, src) -> + let msg = F.sprintf "%s is compared to 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 diff --git a/infer/tests/codetoanalyze/java/checkers/ExpensiveCallExample.java b/infer/tests/codetoanalyze/java/checkers/ExpensiveCallExample.java index d5c5d611b..a311cc597 100644 --- a/infer/tests/codetoanalyze/java/checkers/ExpensiveCallExample.java +++ b/infer/tests/codetoanalyze/java/checkers/ExpensiveCallExample.java @@ -15,7 +15,7 @@ import android.view.View; import com.facebook.infer.annotation.Expensive; import com.facebook.infer.annotation.PerformanceCritical; - +import javax.annotation.Nullable; interface AnnotatedInterface { @@ -100,7 +100,7 @@ class PerformanceCriticalSubclass extends PerformanceCriticalClass { public class ExpensiveCallExample implements AnnotatedInterface { - Other mOther; + @Nullable Other mOther; void nonExpensiveMethod() {} diff --git a/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java b/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java index bc0e849a9..3aa117eec 100644 --- a/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java +++ b/infer/tests/codetoanalyze/java/checkers/NullableSuggest.java @@ -63,8 +63,9 @@ public class NullableSuggest { for (int i = 0; i < n; ++i) { arr[i] = origin; } - if (n > 0) + if (n > 0) { obj1 = arr[0]; + } } public void assignNullToFieldTransitiveLoopBad(int n) { @@ -73,16 +74,35 @@ public class NullableSuggest { for (int i = 0; i < n; ++i) { arr[i] = origin; } - if (n > 0) + if (n > 0) { obj0 = arr[0]; + } } public void multipleChainsAlwaysSelectShortestBad(boolean flag) { Object o0 = null; Object o1 = null; - if (flag) + if (flag) { o1 = o0; + } obj0 = o1; // The analysis should report error trace o1->obj0, rather than o0->o1->obj0 } + + public void compareNullToFieldBad() { + OtherClass oc = new OtherClass(); + if (obj0 == null) { + // Pretend that we did something here... + } + else { + // The analysis should not suggest @Nullable on OtherClass.obj2 here + oc.obj2 = obj0; + } + } + + public void compareNullToNullableFieldOk() { + if (obj1 == null) { + // Pretend that we did something here... + } + } } diff --git a/infer/tests/codetoanalyze/java/checkers/issues.exp b/infer/tests/codetoanalyze/java/checkers/issues.exp index 41643ba4d..012b8884b 100644 --- a/infer/tests/codetoanalyze/java/checkers/issues.exp +++ b/infer/tests/codetoanalyze/java/checkers/issues.exp @@ -40,7 +40,8 @@ codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNul 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/NullableSuggest.java, void NullableSuggest.compareNullToFieldBad(), 2, FIELD_SHOULD_BE_NULLABLE, [Field obj0 is compared to null here] +codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.multipleChainsAlwaysSelectShortestBad(boolean), 6, 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]