Fix type checker crash caused by large number of uses of Shape::keyExists

andrewjkennedy · fredemmott · commit 101d32457e8b · 2018-07-12T14:01:43.000-07:00
Summary: After a conditional we create a "union" of types. These can grow very large e.g. with shape refinement, as in this example: ``` type example_shape = shape( ?'example_1' => int, ?'example_2' => int, ?'example_3' => int, ?'example_4' => int, ?'example_5' => int, ); function takes_example_shape(example_shape $in): string { if (Shapes::keyExists($in, 'example_1')) { ... } if (Shapes::keyExists($in, 'example_2')) { ... } if (Shapes::keyExists($in, 'example_3')) { ... } if (Shapes::keyExists($in, 'example_4')) { ... } if (Shapes::keyExists($in, 'example_5')) { ... } ... ``` Eventually, Hack crashes. The crux of the problem is the "union" operation on locals that takes one very large shape type of the form `shape(?'x' => t, <more stuff>)` and computes the union with another very large shape type `shape('x' => t, <more stuff>)`. Spot the difference: just the `?`. In fact, the latter type is a subtype of the former, so the union is equivalent just to the former type. The fix is to avoid constructing an explicit union if one type is a subtype of the other. To do this, we adapt the `simplify_subtype` function to construct a helper function `is_sub_type_alt` that returns `Some b` if one type is definitely a subtype, or definitely *not* a subtype of the other, and returns `None` if it doesn't know. (There is already an `is_sub_type` function but it's quite hacky and we want to move to a more careful approach that doesn't "force" a subtype, or generate errors and then back off). Part of the diff involves changing `simplify_subtype` and helpers so that it doesn't generate errors. Fixes #8249 Reviewed By: manzyuk Differential Revision: D8731917 fbshipit-source-id: 753ddd507ad7f918c6648825a7ab1f4901044f2a
diff --git a/hphp/hack/src/typing/typing_lenv.ml b/hphp/hack/src/typing/typing_lenv.ml
@@ -81,6 +81,10 @@ let intersect env parent_lenv lenv1 lenv2 =
           let env, ty =
             if Typing_defs.ty_equal ty1 ty2
             then env, ty1
+            else if Typing_subtype.is_sub_type_alt env ty1 ty2 = Some true
+            then env, ty2
+            else if Typing_subtype.is_sub_type_alt env ty2 ty1 = Some true
+            then env, ty1
             else
               let env, ty1 = TUtils.unresolved env ty1 in
               let env, ty2 = TUtils.unresolved env ty2 in
diff --git a/hphp/hack/src/typing/typing_subtype.ml b/hphp/hack/src/typing/typing_subtype.ml
@@ -44,7 +44,7 @@ module Phase = Typing_phase
  *)
 type simplification_result = {
   constraints: (locl ty * Ast.constraint_kind * locl ty) list;
-  failed_subtype: (locl ty * locl ty) option;
+  failed_subtype: (locl ty * locl ty * (unit -> unit)) option;
 }
 
 let rec simplify_subtype
@@ -66,9 +66,12 @@ let rec simplify_subtype
   let again env res ty_sub =
     simplify_subtype ~deep ~this_ty ty_sub ty_super (env, res) in
   (* We *know* that the assertion is unsatisfiable *)
-  let invalid ()  =
-    (env, { constraints = acc; failed_subtype = Some (ety_sub, ety_super) }) in
-  (* We *know* that the assertion is valid *)
+  let invalid_with f =
+    (env, { constraints = acc; failed_subtype = Some (ety_sub, ety_super, f) }) in
+  let invalid () =
+    invalid_with (fun () ->
+      TUtils.uerror (fst ety_super) (snd ety_super) (fst ety_sub) (snd ety_sub)) in
+    (* We *know* that the assertion is valid *)
   let valid () =
     res in
   (* We don't know whether the assertion is valid or not *)
@@ -267,11 +270,10 @@ let rec simplify_subtype
           | true, _ | false, false ->
             simplify_subtype ~deep ~this_ty ty_sub ty_super res
           | false, true ->
-            Errors.required_field_is_optional
+            invalid_with (fun () -> Errors.required_field_is_optional
               (Reason.to_pos r_sub)
               (Reason.to_pos r_super)
-              (Env.get_shape_field_name name);
-            invalid () in
+              (Env.get_shape_field_name name)) in
       let on_missing_omittable_optional_field res _ _ = res in
       let on_missing_non_omittable_optional_field
           res name { sft_ty = ty_super; _ } =
@@ -285,6 +287,7 @@ let rec simplify_subtype
         ~on_common_field
         ~on_missing_omittable_optional_field
         ~on_missing_non_omittable_optional_field
+        ~on_error:(fun _ f -> invalid_with f)
         res
         (r_super, fields_known_super, fdm_super)
         (r_sub, fields_known_sub, fdm_sub)
@@ -315,17 +318,18 @@ let rec simplify_subtype
         default ()
 
       | Some class_sub ->
-        let ety_env =
-          (* We handle the case where a generic A<T> is used as A *)
-          let tyl_sub =
-            if tyl_sub = [] && not (Env.is_strict env)
-            then List.map class_sub.tc_tparams (fun _ -> (p_sub, Tany))
-            else tyl_sub
-          in
-          if List.length class_sub.tc_tparams <> List.length tyl_sub
-          then
-            Errors.expected_tparam
-              (Reason.to_pos p_sub) (List.length class_sub.tc_tparams);
+        (* We handle the case where a generic A<T> is used as A *)
+        let tyl_sub =
+          if tyl_sub = [] && not (Env.is_strict env)
+          then List.map class_sub.tc_tparams (fun _ -> (p_sub, Tany))
+          else tyl_sub in
+        if List.length class_sub.tc_tparams <> List.length tyl_sub
+        then
+          invalid_with (fun () ->
+          Errors.expected_tparam
+            (Reason.to_pos p_sub) (List.length class_sub.tc_tparams))
+        else
+          let ety_env =
           (* NOTE: We rely on the fact that we fold all ancestors of
            * ty_sub in its class_type so we will never hit this case
            * again. If this ever changes then we would need to store
@@ -1126,8 +1130,8 @@ and sub_type_unwrapped
     simplify_subtype ~deep:false ~this_ty ty_sub ty_super
       (env, { constraints = []; failed_subtype = None }) in
     match failed_subtype with
-    | Some (ty_sub, ty_super) ->
-      TUtils.uerror (fst ty_super) (snd ty_super) (fst ty_sub) (snd ty_sub);
+    | Some (_ty_sub, _ty_super, f) ->
+      f ();
       env
     | None ->
       List.fold_right ~f:(fun (ty1,ck,ty2) env ->
@@ -1672,6 +1676,19 @@ and sub_string
     | Ttuple _ | Tanon (_, _) | Tfun _ | Tshape _) ->
       fst (Unify.unify env (Reason.Rwitness p, Tprim Nast.Tstring) ty2)
 
+(* Non-side-effecting test for subtypes, using simplify_subtype.
+ * Result is
+ *   result = Some true implies ty1 <: ty2
+ *   result = Some false implies NOT ty1 <: ty2
+ *   result = None, we don't know
+ *)
+let is_sub_type_alt env ty1 ty2 =
+  match simplify_subtype ~deep:true ~this_ty:(Some ty1) ty1 ty2
+    (env, { constraints = []; failed_subtype = None }) with
+  | _, { constraints = []; failed_subtype = None } -> Some true
+  | _, { constraints = _; failed_subtype = Some _ }-> Some false
+  | _ -> None
+
 (*****************************************************************************)
 (* Exporting *)
 (*****************************************************************************)
diff --git a/hphp/hack/src/typing/typing_unify.ml b/hphp/hack/src/typing/typing_unify.ml
@@ -378,13 +378,15 @@ and unify_ ?(opts=TUtils.default_unify_opt) env r1 ty1 r2 ty2 =
         ~on_missing_non_omittable_optional_field:(
           on_missing_non_omittable_optional_field p2
         )
+        ~on_error:(fun x f -> f (); x)
         (env, res) (r1, fields_known1, fdm1) (r2, fields_known2, fdm2) in
       let env, res = TUtils.apply_shape
         ~on_common_field
         ~on_missing_omittable_optional_field
         ~on_missing_non_omittable_optional_field:(
           on_missing_non_omittable_optional_field p1
         )
+        ~on_error:(fun x f -> f (); x)
         (env, res) (r2, fields_known2, fdm2) (r1, fields_known1, fdm1) in
         (* After doing apply_shape in both directions we can be sure that
          * fields_known1 = fields_known2 *)
diff --git a/hphp/hack/src/typing/typing_utils.ml b/hphp/hack/src/typing/typing_utils.ml
@@ -352,39 +352,42 @@ let apply_shape
   ~on_common_field
   ~on_missing_omittable_optional_field
   ~on_missing_non_omittable_optional_field
+  ~on_error
   (env, acc)
   (r1, fields_known1, fdm1)
   (r2, fields_known2, fdm2) =
+  let (env, acc) =
   begin match fields_known1, fields_known2 with
     | FieldsFullyKnown, FieldsFullyKnown ->
         (* If both shapes are FieldsFullyKnown, then we must ensure that the
            supertype shape knows about every single field that could possibly
            be present in the subtype shape. *)
-        ShapeMap.iter begin fun name _ ->
+        ShapeMap.fold begin fun name _ (env, acc) ->
           if not @@ ShapeMap.mem name fdm1 then
             let pos1 = Reason.to_pos r1 in
             let pos2 = Reason.to_pos r2 in
-            Errors.unknown_field_disallowed_in_shape
+            on_error (env,acc) (fun () -> Errors.unknown_field_disallowed_in_shape
               pos1
               pos2
-              (get_printable_shape_field_name name)
-        end fdm2
+              (get_printable_shape_field_name name))
+          else (env, acc)
+        end fdm2 (env, acc)
     | FieldsFullyKnown, FieldsPartiallyKnown _  ->
         let pos1 = Reason.to_pos r1 in
         let pos2 = Reason.to_pos r2 in
-        Errors.shape_fields_unknown pos2 pos1
+        on_error (env, acc) (fun () -> Errors.shape_fields_unknown pos2 pos1)
     | FieldsPartiallyKnown unset_fields1,
       FieldsPartiallyKnown unset_fields2 ->
-        ShapeMap.iter begin fun name unset_pos ->
+        ShapeMap.fold begin fun name unset_pos (env, acc) ->
           match ShapeMap.get name unset_fields2 with
-            | Some _ -> ()
+            | Some _ -> (env, acc)
             | None ->
                 let pos2 = Reason.to_pos r2 in
-                Errors.shape_field_unset unset_pos pos2
-                  (get_printable_shape_field_name name);
-        end unset_fields1
-    | _ -> ()
-  end;
+                on_error (env, acc) (fun () -> Errors.shape_field_unset unset_pos pos2
+                  (get_printable_shape_field_name name))
+        end unset_fields1 (env, acc)
+    | _ -> (env, acc)
+  end in
   ShapeMap.fold begin fun name shape_field_type_1 (env, acc) ->
     match ShapeMap.get name fdm2 with
     | None when is_shape_field_optional env shape_field_type_1 ->
@@ -400,8 +403,8 @@ let apply_shape
     | None ->
         let pos1 = Reason.to_pos r1 in
         let pos2 = Reason.to_pos r2 in
-        Errors.missing_field pos2 pos1 (get_printable_shape_field_name name);
-        (env, acc)
+        on_error (env, acc) (fun () ->
+          Errors.missing_field pos2 pos1 (get_printable_shape_field_name name))
     | Some shape_field_type_2 ->
         on_common_field (env, acc) name shape_field_type_1 shape_field_type_2
   end fdm1 (env, acc)
diff --git a/hphp/hack/test/typecheck/arithmetic_any.php.exp b/hphp/hack/test/typecheck/arithmetic_any.php.exp
@@ -27,7 +27,7 @@ File "arithmetic_any.php--file2.php", line 75, characters 35-45:
 File "arithmetic_any.php--file2.php", line 75, characters 48-58:
   _
 File "arithmetic_any.php--file2.php", line 84, characters 3-13:
-  (int | ?int)
+  ?int
 File "arithmetic_any.php--file2.php", line 89, characters 3-13:
   float
 No errors
diff --git a/hphp/hack/test/typecheck/inout/bad_inout_use_assign4.php.exp b/hphp/hack/test/typecheck/inout/bad_inout_use_assign4.php.exp
@@ -1,4 +1,4 @@
-File "bad_inout_use_assign4.php", line 11, characters 10-19:
+File "bad_inout_use_assign4.php", line 15, characters 18-25:
 Invalid assignment to an inout parameter (Typing[4110])
 File "bad_inout_use_assign4.php", line 7, characters 18-23:
 This is a string (inout parameter)
diff --git a/hphp/hack/test/typecheck/is_expression/primitive.php.exp b/hphp/hack/test/typecheck/is_expression/primitive.php.exp
@@ -2,29 +2,29 @@ File "primitive.php", line 15, characters 15-16:
 Invalid argument (Typing[4110])
   File "primitive.php", line 22, characters 22-25:
   This is a bool
-  File "primitive.php", line 8, characters 20-22:
-  It is incompatible with an int
+  File "primitive.php", line 3, characters 15-19:
+  It is incompatible with a mixed value
 File "primitive.php", line 16, characters 16-17:
 Invalid argument (Typing[4110])
   File "primitive.php", line 23, characters 23-27:
   This is a float
-  File "primitive.php", line 4, characters 13-16:
-  It is incompatible with a bool
+  File "primitive.php", line 3, characters 15-19:
+  It is incompatible with a mixed value
 File "primitive.php", line 17, characters 14-15:
 Invalid argument (Typing[4110])
   File "primitive.php", line 24, characters 21-23:
   This is an int
-  File "primitive.php", line 4, characters 13-16:
-  It is incompatible with a bool
+  File "primitive.php", line 3, characters 15-19:
+  It is incompatible with a mixed value
 File "primitive.php", line 18, characters 19-20:
 Invalid argument (Typing[4110])
   File "primitive.php", line 25, characters 26-33:
   This is a resource
-  File "primitive.php", line 4, characters 13-16:
-  It is incompatible with a bool
+  File "primitive.php", line 3, characters 15-19:
+  It is incompatible with a mixed value
 File "primitive.php", line 19, characters 17-18:
 Invalid argument (Typing[4110])
   File "primitive.php", line 26, characters 24-29:
   This is a string
-  File "primitive.php", line 4, characters 13-16:
-  It is incompatible with a bool
+  File "primitive.php", line 3, characters 15-19:
+  It is incompatible with a mixed value
diff --git a/hphp/hack/test/typecheck/is_expression/primitive_union.php.exp b/hphp/hack/test/typecheck/is_expression/primitive_union.php.exp
@@ -8,5 +8,5 @@ File "primitive_union.php", line 10, characters 14-15:
 Invalid argument (Typing[4110])
   File "primitive_union.php", line 14, characters 21-23:
   This is a num (int/float)
-  File "primitive_union.php", line 4, characters 13-20:
-  It is incompatible with an array key (int/string)
+  File "primitive_union.php", line 3, characters 15-19:
+  It is incompatible with a mixed value
diff --git a/hphp/hack/test/typecheck/recursive_non_null_3.php.exp b/hphp/hack/test/typecheck/recursive_non_null_3.php.exp
@@ -1,6 +1,6 @@
 File "recursive_non_null_3.php", line 20, characters 10-13:
 Invalid return type (Typing[4110])
-File "recursive_non_null_3.php", line 11, characters 32-36:
-This is a nonnull value
 File "recursive_non_null_3.php", line 11, characters 50-50:
-It is incompatible with an object of type A
+This is an object of type A
+File "recursive_non_null_3.php", line 11, characters 32-36:
+It is incompatible with a nonnull value
diff --git a/hphp/hack/test/typecheck/shape/disable_optional_and_unknown_shape_fields/shape26.php.exp b/hphp/hack/test/typecheck/shape/disable_optional_and_unknown_shape_fields/shape26.php.exp
@@ -3,7 +3,7 @@ File "shape26.php", line 21, characters 3-13:
 File "shape26.php", line 29, characters 3-13:
   ^(shape('x' => ^(string | int)))
 File "shape26.php", line 37, characters 3-13:
-  ^(shape('x' => int, ...) | shape('x' => int, 'y' => ?string, ...))
+  shape('x' => int, ...)
 File "shape26.php", line 45, characters 3-13:
   ^(shape('x' => ^(int)) | shape('x' => int, 'y' => ?string, ...))
 No errors
diff --git a/hphp/hack/test/typecheck/shape/key_exists_refines_many.php b/hphp/hack/test/typecheck/shape/key_exists_refines_many.php
@@ -0,0 +1,86 @@
+<?hh // strict
+
+type example_shape = shape(
+  ?'example_1' => int,
+  ?'example_2' => int,
+  ?'example_3' => int,
+  ?'example_4' => int,
+  ?'example_5' => int,
+  ?'example_6' => int,
+  ?'example_7' => int,
+  ?'example_8' => int,
+  ?'example_9' => int,
+  ?'example_10' => int,
+  ?'example_11' => int,
+  ?'example_12' => int,
+  ?'example_13' => int,
+  ?'example_14' => int,
+  ?'example_15' => int,
+);
+function takes_example_shape(example_shape $in): string {
+
+  $bits = [];
+
+  if (Shapes::keyExists($in, 'example_1')) {
+    $bits[] = 'example_1';
+  }
+  if (Shapes::keyExists($in, 'example_2')) {
+    $bits[] = 'example_2';
+  }
+  if (Shapes::keyExists($in, 'example_3')) {
+    $bits[] = 'example_3';
+  }
+  if (Shapes::keyExists($in, 'example_4')) {
+    $bits[] = 'example_4';
+  }
+  if (Shapes::keyExists($in, 'example_5')) {
+    $bits[] = 'example_5';
+  }
+  if (Shapes::keyExists($in, 'example_6')) {
+    $bits[] = 'example_6';
+  }
+  if (Shapes::keyExists($in, 'example_7')) {
+    $bits[] = 'example_7';
+  }
+  if (Shapes::keyExists($in, 'example_8')) {
+    $bits[] = 'example_8';
+  }
+  if (Shapes::keyExists($in, 'example_9')) {
+    $bits[] = 'example_9';
+  }
+  if (Shapes::keyExists($in, 'example_10')) {
+    $bits[] = 'example_10';
+  }
+  if (Shapes::keyExists($in, 'example_6')) {
+    $bits[] = 'example_6';
+  }
+  if (Shapes::keyExists($in, 'example_7')) {
+    $bits[] = 'example_7';
+  }
+  if (Shapes::keyExists($in, 'example_8')) {
+    $bits[] = 'example_8';
+  }
+  if (Shapes::keyExists($in, 'example_9')) {
+    $bits[] = 'example_9';
+  }
+  if (Shapes::keyExists($in, 'example_10')) {
+    $bits[] = 'example_10';
+  }
+  if (Shapes::keyExists($in, 'example_11')) {
+    $bits[] = 'example_11';
+  }
+  if (Shapes::keyExists($in, 'example_12')) {
+    $bits[] = 'example_12';
+  }
+  if (Shapes::keyExists($in, 'example_13')) {
+    $bits[] = 'example_13';
+  }
+  if (Shapes::keyExists($in, 'example_14')) {
+    $bits[] = 'example_14';
+  }
+  if (Shapes::keyExists($in, 'example_15')) {
+    $bits[] = 'example_15';
+  }
+
+  return implode(',', $bits);
+}
diff --git a/hphp/hack/test/typecheck/shape/key_exists_refines_many.php.exp b/hphp/hack/test/typecheck/shape/key_exists_refines_many.php.exp
@@ -0,0 +1 @@
+No errors
diff --git a/hphp/hack/test/typecheck/shape26.php.exp b/hphp/hack/test/typecheck/shape26.php.exp
@@ -3,7 +3,7 @@ File "shape26.php", line 25, characters 3-13:
 File "shape26.php", line 33, characters 3-13:
   ^(shape('x' => ^(string | int)))
 File "shape26.php", line 41, characters 3-13:
-  ^(shape('x' => int, ...) | shape('x' => int, 'y' => ?string, ...))
+  shape('x' => int, ...)
 File "shape26.php", line 49, characters 3-13:
   ^(shape('x' => ^(int)) | shape('x' => int, 'y' => ?string, ...))
 No errors
