[nullsafe][refactoring] Simplify call to condition_redundant checks.

Summary:
This refactoring unblocks the changes in follow up diffs (plus fixes a
bug).

So what was happening?

Each comparison with null leads to CFG being splitted into two branches, one branch
is PRUNE(a == null) and another is PRUNE(a != null).

PRUNE(a != null) is where most of logic happens, it is the place where
we infer non-null nullability for a, and this is a natural place to
leave a check for redundancy.

Before this diff we effectively checked the same thing twice, and used
`true_branch` (only one of 2 instruction will have it set to true) as a symmetry breaker.

This diff removes the `true_branch` checks, but leaves only one call out
of two, hence breaking symmetry in a different way.

## Bug fix
The code around the removed check was (crazily) doing two things at
once: it processed results of (returning booleans!)
TrueOnNull-annotated functions AND
results of (returning Objects!) other functions, using the fact that all
of them are encoded as zero literals (sic!).

Not surprisingly that lead to a bug where we accidentally call the check
for non intended places (arguments of trueOnNull functions), which lead
to really weird FP.

This diff fixes it.

Reviewed By: dulmarod

Differential Revision: D19744604

fbshipit-source-id: fe4e65a8f

infer/src/nullsafe/eradicateChecks.ml

@@ -56,9 +56,11 @@ type from_call =
 
 let equal_from_call = [%compare.equal: from_call]
 
-(** Check the normalized "is zero" or "is not zero" condition of a prune instruction. *)
-let check_condition tenv case_zero find_canonical_duplicate curr_pdesc node e typ
-    inferred_nullability true_branch from_call idenv linereader loc instr_ref : unit =
+(** [expr] is an expression that was explicitly compared with `null`. At the same time, [expr] had
+    [inferred_nullability] before the comparision. Check if the comparision is redundant and emit an
+    issue, if this is the case. *)
+let check_condition_for_redundancy tenv ~is_always_true find_canonical_duplicate curr_pdesc node
+    expr typ inferred_nullability idenv linereader loc instr_ref : unit =
   let contains_instanceof_throwable pdesc node =
     (* Check if the current procedure has a catch Throwable. *)
     (* That always happens in the bytecode generated by try-with-resources. *)
@@ -94,37 +96,35 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pdesc node e ty
     | None ->
         false
   in
-  let is_temp = Idenv.exp_is_temp idenv e in
+  let is_temp = Idenv.exp_is_temp idenv expr in
   let should_report =
-    (* TODO: This condition should be extracted into a dedicated rule *)
+    (* NOTE: We have different levels of non-nullability. In practice there is a big difference
+       between certainty for different cases: whether expression is the result of something that can not be null
+       due to language semantics, or comes from something that is merely not declared as nullable.
+       We report both types of issues now, which is OK since this warning is turned off by default.
+       In the future we might as well start reporting only for cases where we are more confident.
+       Hovewer keep in mind that for code analysis purposes all condition redudant warnings can be useful,
+       particularly they help to find popular functions that should have been annotated as nullable, but were not made so.
+    *)
+    (* NOTE: We don't report the opposite case, namely when the expression is known to be always `null`. Consider changing this.
+    *)
     InferredNullability.is_nonnull_or_declared_nonnull inferred_nullability
-    && Config.eradicate_condition_redundant && true_branch && (not is_temp)
-    && PatternMatch.type_is_class typ
+    && Config.eradicate_condition_redundant && (not is_temp) && PatternMatch.type_is_class typ
     && (not (from_try_with_resources ()))
-    && equal_from_call from_call From_condition
     && not (InferredNullability.origin_is_fun_library inferred_nullability)
   in
-  let is_always_true = not case_zero in
   if should_report then
     (* TODO(T61051649) this is not really condition. This is an expression.
        This leads to inconsistent messaging like "condition `some_variable` is always true".
        So Condition_redundant should either accept expression, or this should pass a condition.
     *)
-    let condition_descr = explain_expr tenv node e in
+    let condition_descr = explain_expr tenv node expr in
     let nonnull_origin = InferredNullability.get_origin inferred_nullability in
     report_error tenv find_canonical_duplicate
       (TypeErr.Condition_redundant {is_always_true; condition_descr; nonnull_origin})
       (Some instr_ref) loc curr_pdesc
 
 
-(** Check an "is zero" condition. *)
-let check_zero tenv find_canonical_duplicate = check_condition tenv true find_canonical_duplicate
-
-(** Check an "is not zero" condition. *)
-let check_nonzero tenv find_canonical_duplicate =
-  check_condition tenv false find_canonical_duplicate
-
-
 (** Check an assignment to a field. *)
 let check_field_assignment ~nullsafe_mode tenv find_canonical_duplicate curr_pdesc node instr_ref
     typestate exp_lhs exp_rhs typ loc fname annotated_field_opt typecheck_expr : unit =

infer/src/nullsafe/typeCheck.ml

@@ -749,14 +749,6 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
         convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature ~node
           ~original_node ~is_assignment:false e1 typestate1 loc
       in
-      let typ, inferred_nullability =
-        typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks
-          tenv original_node instr_ref typestate2 e' Typ.void TypeOrigin.OptimisticFallback loc
-      in
-      if checks.eradicate then
-        EradicateChecks.check_zero tenv find_canonical_duplicate curr_pdesc node e' typ
-          inferred_nullability true_branch EradicateChecks.From_condition idenv linereader loc
-          instr_ref ;
       match from_call with
       | EradicateChecks.From_is_true_on_null ->
           (* if f returns true on null, then false branch implies != null *)
@@ -787,9 +779,12 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
         typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks
           tenv original_node instr_ref typestate2 e' Typ.void TypeOrigin.OptimisticFallback loc
       in
-      if checks.eradicate then
-        EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc original_node e' typ
-          inferred_nullability true_branch from_call idenv linereader loc instr_ref ;
+      if checks.eradicate && EradicateChecks.equal_from_call from_call From_condition then
+        (* We are about to set inferred nullability. But what if it was not needed?
+           This indicates that the condition was redundant. *)
+        EradicateChecks.check_condition_for_redundancy ~is_always_true:true_branch tenv
+          find_canonical_duplicate curr_pdesc original_node e' typ inferred_nullability idenv
+          linereader loc instr_ref ;
       match from_call with
       | EradicateChecks.From_is_true_on_null ->
           typestate2

infer/tests/codetoanalyze/java/nullsafe-default/issues.exp

@@ -250,8 +250,6 @@ codetoanalyze/java/nullsafe-default/SwitchCase.java, codetoanalyze.java.nullsafe
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, codetoanalyze.java.nullsafe_default.TrueFalseOnNull$Test.testEarlyReturn(java.lang.CharSequence,java.lang.CharSequence):void, 5, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`s2` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, codetoanalyze.java.nullsafe_default.TrueFalseOnNull$Test.testFalseOnNull(java.lang.CharSequence):void, 6, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`s` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, codetoanalyze.java.nullsafe_default.TrueFalseOnNull$Test.testFalseOnNull(java.lang.CharSequence):void, 10, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`s` is nullable and is not locally checked for null when calling `toString()`.]
-codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, codetoanalyze.java.nullsafe_default.TrueFalseOnNull$Test.testModelledTrueOnNull(java.lang.String):void, 0, ERADICATE_CONDITION_REDUNDANT, no_bucket, ADVICE, [The condition s might be always false according to the existing annotations.]
-codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, codetoanalyze.java.nullsafe_default.TrueFalseOnNull$Test.testModelledTrueOnNull(java.lang.String):void, 5, ERADICATE_CONDITION_REDUNDANT, no_bucket, ADVICE, [The condition s might be always false according to the existing annotations.]
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, codetoanalyze.java.nullsafe_default.TrueFalseOnNull$Test.testTrueOnNull(java.lang.CharSequence):void, 6, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`s` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, codetoanalyze.java.nullsafe_default.TrueFalseOnNull$Test.testTrueOnNull(java.lang.CharSequence):void, 10, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`s` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe-default/third-party-test-code/some/test/pckg/ThirdPartyTestClass.java, some.test.pckg.ThirdPartyTestClass.returnSpecifiedAsNullable():java.lang.String, 0, ERADICATE_RETURN_OVER_ANNOTATED, no_bucket, WARNING, [Method `returnSpecifiedAsNullable()` is annotated with `@Nullable` but never returns null.]