[nullsafe][refactor] Clean up code responsible for manipulations with `containsKey()`

Summary:
The whole TypeCheck.ml is exceptionally hard to read and maintain, lets
clean up it a bit.

Reviewed By: ngorogiannis

Differential Revision: D19743632

fbshipit-source-id: c24c21a85

infer/src/nullsafe/ErrorRenderingUtils.ml

@@ -7,7 +7,7 @@
 
 open! IStd
 
-let is_object_nullability_self_explanatory ~object_expression object_origin =
+let is_object_nullability_self_explanatory ~object_expression (object_origin : TypeOrigin.t) =
   (* Fundamentally, object can be of two kinds:
      1. Indirect: local variable that was instantiated before.
      In this case, normally origin is NOT trivial
@@ -19,21 +19,21 @@ let is_object_nullability_self_explanatory ~object_expression object_origin =
      to be 100% precise.
   *)
   match object_origin with
-  | TypeOrigin.NullConst _ ->
+  | NullConst _ ->
       (* Expect either a local variable or null literal (latter case is trivial) *)
       String.equal object_expression "null"
-  | TypeOrigin.MethodParameter {mangled} ->
+  | MethodParameter {mangled} ->
       (* Either local variable or literally parameter. In latter case, its nullability is
          self-explanatory because the user can quickly see the current method signature.
       *)
       let param_name = Mangled.to_string mangled in
       String.equal object_expression param_name
-  | TypeOrigin.Field {field_name} ->
+  | Field {field_name} ->
       (* Either local variable or expression like `<smth>.field_name`. Latter case is trivial:
          the user can quickly go to field_name definition and see if its annotation. *)
       let field_name_str = Fieldname.get_field_name field_name in
       String.is_suffix object_expression ~suffix:field_name_str
-  | TypeOrigin.MethodCall {pname; annotated_signature= {model_source}} ->
+  | MethodCall {pname; annotated_signature= {model_source}} ->
       let is_modelled = Option.is_some model_source in
       if is_modelled then (* This is non-trivial and should always be explained to the user *)
         false
@@ -47,14 +47,15 @@ let is_object_nullability_self_explanatory ~object_expression object_origin =
   (* These cases are not yet supported because they normally mean non-nullable case, for which
      we don't render important messages yet.
   *)
-  | TypeOrigin.NonnullConst _
+  | NonnullConst _
-  | TypeOrigin.This
+  | This
-  | TypeOrigin.New
+  | New
-  | TypeOrigin.ArrayLengthResult
+  | CallToGetKnownToContainsKey
-  | TypeOrigin.ArrayAccess
+  | ArrayLengthResult
-  | TypeOrigin.InferredNonnull _
+  | ArrayAccess
-  | TypeOrigin.OptimisticFallback
+  | InferredNonnull _
-  | TypeOrigin.Undef ->
+  | OptimisticFallback
+  | Undef ->
       false
 
 

infer/src/nullsafe/typeCheck.ml

@@ -677,10 +677,14 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
   in
   (* check if the expression is coming from Map.containsKey *)
   let from_containsKey e : Exp.t option = from_call ComplexExpressions.procname_containsKey e in
-  (* Turn x.containsKey(e) into the pvar for x.get(e) *)
+  (* Call to x.containsKey(e) returned `true`.
-  (* which is then treated as a normal condition != null. *)
+     It means that subsequent calls to `x.get(e)` should be inferred as non-nullables.
-  let handle_containsKey e =
+     We achieve this behavior by adding the result of a call to `x.get(e)` (in form of corresponding pvar)
-    let map_dexp = function
+     to a typestate, with correspnding (non-null) type origin.
+  *)
+  let handle_containsKey_returned_true call_to_containsKey_exr =
+    let replace_contains_key_with_get_in_a_function_call_expression = function
+      (* This will replace x.containsKey(e) to x.get(e) *)
       | Some
           (DExp.Dretcall
             (DExp.Dconst (Const.Cfun (Procname.Java pname_java)), args, loc, call_flags)) ->
@@ -695,19 +699,20 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
       | _ ->
           None
     in
-    match ComplexExpressions.exp_to_string_map_dexp tenv map_dexp node e with
+    let string_representing_call_to_get =
-    | Some e_str ->
+      ComplexExpressions.exp_to_string_map_dexp tenv
-        let pvar = Pvar.mk (Mangled.from_string e_str) curr_pname in
+        replace_contains_key_with_get_in_a_function_call_expression node call_to_containsKey_exr
-        let e1 = Exp.Lvar pvar in
+    in
-        let typ, ta =
+    match string_representing_call_to_get with
-          typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks
+    | Some expr_str ->
-            tenv original_node instr_ref typestate e1 Typ.void TypeOrigin.OptimisticFallback loc
+        (* Add pvar representing call to `get` to a typestate, indicating that it is a non-nullable *)
-        in
+        let pvar = Pvar.mk (Mangled.from_string expr_str) curr_pname in
-        let range = (typ, ta) in
+        let pvar_expr = Exp.Lvar pvar in
-        let typestate1 = TypeState.add pvar range typestate in
+        let range = (Typ.void, InferredNullability.create TypeOrigin.CallToGetKnownToContainsKey) in
-        (typestate1, e1, EradicateChecks.From_containsKey)
+        let typestate_with_new_pvar = TypeState.add pvar range typestate in
+        (typestate_with_new_pvar, pvar_expr, EradicateChecks.From_containsKey)
     | None ->
-        (typestate, e, EradicateChecks.From_condition)
+        (typestate, call_to_containsKey_exr, EradicateChecks.From_condition)
   in
   let set_nonnull e' typestate2 =
     let handle_pvar typestate' pvar =
@@ -775,7 +780,7 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
           | Some e1 ->
               (typestate, e1, EradicateChecks.From_is_false_on_null)
           | None ->
-              if Option.is_some (from_containsKey e) then handle_containsKey e
+              if Option.is_some (from_containsKey e) then handle_containsKey_returned_true e
               else (typestate, e, EradicateChecks.From_condition) )
       in
       let e', typestate2 =

infer/src/nullsafe/typeErr.ml

@@ -250,6 +250,7 @@ let get_nonnull_explanation_for_condition_redudant (nonnull_origin : TypeOrigin.
   (* TODO: this could be specified more precisely *)
   | NonnullConst _
   | Field _
+  | CallToGetKnownToContainsKey
   | MethodParameter _
   | This
   | New

infer/src/nullsafe/typeOrigin.ml

@@ -16,6 +16,9 @@ type t =
   | MethodParameter of AnnotatedSignature.param_signature  (** A method's parameter *)
   | This (* `this` object. Can not be null, according to Java rules. *)
   | MethodCall of method_call_origin  (** A result of a method call *)
+  | CallToGetKnownToContainsKey
+      (** This is a result of accessing a map element that is known to contains this particular key,
+          normally because it was explicitly checked for presense before *)
   | New  (** A new object creation *)
   | ArrayLengthResult  (** integer value - result of accessing array.length *)
   | ArrayAccess  (** Result of accessing an array by index *)
@@ -52,6 +55,7 @@ let get_nullability = function
   | This (* `this` can not be null according to Java rules *)
   | New (* In Java `new` always create a non-null object  *)
   | ArrayLengthResult (* integer hence non-nullable *)
+  | CallToGetKnownToContainsKey (* non-nullable by definition *)
   | InferredNonnull _
   (* WARNING: we trade soundness for usability.
      In Java, arrays are initialized with null, so accessing array is nullable until it was initialized.
@@ -86,14 +90,16 @@ let rec to_string = function
       "this"
   | MethodCall {pname} ->
       Printf.sprintf "Fun %s" (Procname.to_simplified_string pname)
+  | CallToGetKnownToContainsKey ->
+      "CallToGetKnownToContainsKey"
   | New ->
       "New"
   | ArrayLengthResult ->
       "ArrayLength"
   | ArrayAccess ->
       "ArrayAccess"
-  | InferredNonnull _ ->
+  | InferredNonnull {previous_origin} ->
-      "InferredNonnull"
+      Format.sprintf "InferredNonnull(prev:%s)" (to_string previous_origin)
   | OptimisticFallback ->
       "OptimisticFallback"
   | Undef ->
@@ -153,7 +159,13 @@ let get_description origin =
      But for these issues we currently don't print origins in the error string.
      It is a good idea to change this and start printing origins for these origins as well.
   *)
-  | This | New | NonnullConst _ | ArrayLengthResult | ArrayAccess | InferredNonnull _ ->
+  | This
+  | New
+  | NonnullConst _
+  | ArrayLengthResult
+  | ArrayAccess
+  | InferredNonnull _
+  | CallToGetKnownToContainsKey ->
       None
   (* Two special cases - should not really occur in normal code *)
   | OptimisticFallback | Undef ->

infer/src/nullsafe/typeOrigin.mli

@@ -14,6 +14,9 @@ type t =
   | MethodParameter of AnnotatedSignature.param_signature  (** A method's parameter *)
   | This (* `this` object. Can not be null, according to Java rules. *)
   | MethodCall of method_call_origin  (** A result of a method call *)
+  | CallToGetKnownToContainsKey
+      (** This is a result of accessing a map element that is known to contains this particular key,
+          normally because it was explicitly checked for presense before *)
   | New  (** A new object creation *)
   | ArrayLengthResult  (** integer value - result of accessing array.length *)
   | ArrayAccess  (** Result of accessing an array by index *)