From 2001d39e9a208be45939f8147130e680748eaf20 Mon Sep 17 00:00:00 2001
From: Mitya Lyubarskiy <mityal@fb.com>
Date: Fri, 7 Feb 2020 02:17:15 -0800
Subject: [PATCH] [nullsafe][refactor] Simplify and document code processing
 particular part of prune instruction

Summary:
This refactoring is made possible by previous stack, which ensured we
don't do two completely different things in one code anymore (processing
results of functions returning booleans and objects in generic fashion).

Follow up diffs will clean up the code for Prune(a != zero) case.

Reviewed By: dulmarod

Differential Revision: D19745050

fbshipit-source-id: 61d3d02ad
---
 infer/src/nullsafe/eradicateChecks.ml |  1 -
 infer/src/nullsafe/typeCheck.ml       | 50 ++++++++++++---------------
 2 files changed, 22 insertions(+), 29 deletions(-)

diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml
index 06fe8283d..c7242517b 100644
--- a/infer/src/nullsafe/eradicateChecks.ml
+++ b/infer/src/nullsafe/eradicateChecks.ml
@@ -50,7 +50,6 @@ type from_call =
   | From_condition  (** Direct condition *)
   | From_instanceof  (** x instanceof C *)
   | From_is_false_on_null  (** returns false on null *)
-  | From_is_true_on_null  (** returns true on null *)
   | From_containsKey  (** x.containsKey *)
 [@@deriving compare]
 
diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml
index 4b286c7c7..8b3d40965 100644
--- a/infer/src/nullsafe/typeCheck.ml
+++ b/infer/src/nullsafe/typeCheck.ml
@@ -735,29 +735,30 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
         typestate2
   in
   match[@warning "-57"] c with
-  | Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), e)
-  | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i))
+  | Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), expr)
+  | Exp.BinOp (Binop.Eq, expr, Exp.Const (Const.Cint i))
     when IntLit.iszero i -> (
-      let typestate1, e1, from_call =
-        match from_is_true_on_null e with
-        | Some e1 ->
-            (typestate, e1, EradicateChecks.From_is_true_on_null)
-        | None ->
-            (typestate, e, EradicateChecks.From_condition)
-      in
-      let e', typestate2 =
-        convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature ~node
-          ~original_node ~is_assignment:false e1 typestate1 loc
-      in
-      match from_call with
-      | EradicateChecks.From_is_true_on_null ->
-          (* if f returns true on null, then false branch implies != null *)
-          set_nonnull e' typestate2
-      | _ ->
-          typestate2 )
+    (* Zero literal has two different meanings important for Nullsafe:
+       `null` and `false`.
+       We don't currently have a logic for `a == null` case, but `a == false` is important.
+    *)
+    match from_is_true_on_null expr with
+    | Some argument ->
+        (* [expr] is a call to function known to return true on `null`.
+           According to PRUNE semantics, we just ensured that the result is `false`.
+           It means that [argument] can not be `null`, hence we can infer its nullability as a non-null.
+        *)
+        (* Trace the origin of [argument] back to pvar that originated it, so its nullability can be updated in typestate. *)
+        let pvar_expr, updated_typestate =
+          convert_complex_exp_to_pvar tenv idenv curr_pname curr_annotated_signature ~node
+            ~original_node ~is_assignment:false argument typestate loc
+        in
+        set_nonnull pvar_expr updated_typestate
+    | None ->
+        typestate )
   | Exp.BinOp (Binop.Ne, Exp.Const (Const.Cint i), e)
   | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i))
-    when IntLit.iszero i -> (
+    when IntLit.iszero i ->
       let typestate1, e1, from_call =
         match from_instanceof e with
         | Some e1 ->
@@ -785,14 +786,7 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
         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
-      | EradicateChecks.From_condition
-      | EradicateChecks.From_containsKey
-      | EradicateChecks.From_instanceof
-      | EradicateChecks.From_is_false_on_null ->
-          set_nonnull e' typestate2 )
+      set_nonnull e' typestate2
   | Exp.UnOp (Unop.LNot, Exp.BinOp (Binop.Eq, e1, e2), _) ->
       check_condition_for_sil_prune tenv idenv calls_this find_canonical_duplicate loc curr_pname
         curr_pdesc curr_annotated_signature linereader typestate checks true_branch instr_ref