[new-env] Implement reading and refining in new environment

Summary:
This is the key rad work dsainati1 did previously in D28412985 updated to work with the new model of the env builder.

When we read a variable, we find a set of env builder writes, which can be locations, uninitialized, or another set of writes that have been refined. We look up locations in the var env, and if they're part of a refined set we join them into a tvar, refine that tvar with predicates, and flow the result into the overall type. this recursive process generates an overall, summarized view of a variable.

As a side note, this diff includes some verbose-debug printing, but since there isn't a trace available here it also makes traces optional for debug printing, which causes minor changes in lots of places.

Reviewed By: jbrown215

Differential Revision: D29858582

fbshipit-source-id: 2eb078000ed672c8d7cabdf91c5a9fb10b5529ee

src/typing/debug_js.ml

@@ -1764,7 +1764,8 @@ let dump_error_message =
         (dump_reason cx reason_prop)
 
 module Verbose = struct
-  let print_if_verbose_lazy cx trace ?(delim = "") ?(indent = 0) (lines : string list Lazy.t) =
+  let print_if_verbose_lazy
+      cx ?(trace = Trace.dummy_trace) ?(delim = "") ?(indent = 0) (lines : string list Lazy.t) =
     match Context.verbose cx with
     | Some { Verbose.indent = num_spaces; _ } ->
       let indent = max (indent + Trace.trace_depth trace - 1) 0 in
@@ -1775,9 +1776,10 @@ module Verbose = struct
       prerr_endline (String.concat delim lines)
     | None -> ()
 
-  let print_if_verbose cx trace ?(delim = "") ?(indent = 0) (lines : string list) =
+  let print_if_verbose
+      cx ?(trace = Trace.dummy_trace) ?(delim = "") ?(indent = 0) (lines : string list) =
     match Context.verbose cx with
-    | Some _ -> print_if_verbose_lazy cx trace ~delim ~indent (lazy lines)
+    | Some _ -> print_if_verbose_lazy cx ~trace ~delim ~indent (lazy lines)
     | None -> ()
 
   let print_types_if_verbose cx trace ?(note : string option) ((l : Type.t), (u : Type.use_t)) =
@@ -1788,6 +1790,6 @@ module Verbose = struct
         | Some x -> spf " ~> %s" x
         | None -> " ~>"
       in
-      print_if_verbose cx trace ~delim [dump_t ~depth cx l; dump_use_t ~depth cx u]
+      print_if_verbose cx ~trace ~delim [dump_t ~depth cx l; dump_use_t ~depth cx u]
     | None -> ()
 end

src/typing/debug_js.mli

@@ -43,10 +43,10 @@ val dump_flow : ?depth:int -> Context.t -> Type.t * Type.use_t -> string
 
 module Verbose : sig
   val print_if_verbose_lazy :
-    Context.t -> Type.trace -> ?delim:string -> ?indent:int -> string list Lazy.t -> unit
+    Context.t -> ?trace:Type.trace -> ?delim:string -> ?indent:int -> string list Lazy.t -> unit
 
   val print_if_verbose :
-    Context.t -> Type.trace -> ?delim:string -> ?indent:int -> string list -> unit
+    Context.t -> ?trace:Type.trace -> ?delim:string -> ?indent:int -> string list -> unit
 
   val print_types_if_verbose :
     Context.t -> Type.trace -> ?note:string -> Type.t * Type.use_t -> unit

src/typing/flow_common.ml

@@ -40,7 +40,7 @@ module type BASE = sig
   val rec_unify :
     Context.t -> Type.trace -> use_op:Type.use_op -> ?unify_any:bool -> Type.t -> Type.t -> unit
 
-  val unify : Context.t -> Type.t -> Type.t -> unit
+  val unify : Context.t -> ?use_op:Type.use_op -> Type.t -> Type.t -> unit
 
   val unify_opt :
     Context.t ->

src/typing/flow_js.ml

@@ -281,7 +281,7 @@ struct
          discarded depending on whether the case that created the action is
          selected or not. *)
       if Speculation.defer_action cx (Speculation_state.FlowAction (l, u)) then
-        print_if_verbose cx trace ~indent:1 ["deferred during speculation"]
+        print_if_verbose cx ~trace ~indent:1 ["deferred during speculation"]
       else if
         match l with
         | AnyT _ ->
@@ -9558,7 +9558,7 @@ struct
                       ~printer:
                         (print_if_verbose_lazy
                            cx
-                           (Base.Option.value trace ~default:Trace.dummy_trace))
+                           ~trace:(Base.Option.value trace ~default:Trace.dummy_trace))
                       generic_state
                       generic
                       ro ))
@@ -9650,11 +9650,7 @@ struct
             in
             let tset = TypeExSet.add elemt tset in
             let generic =
-              Generic.ArraySpread.merge
-                ~printer:(print_if_verbose_lazy cx Trace.dummy_trace)
-                generic
-                generic'
-                ro
+              Generic.ArraySpread.merge ~printer:(print_if_verbose_lazy cx) generic generic' ro
             in
             flatten cx r args (Some (tset, generic)) rest
       in
@@ -10270,8 +10266,8 @@ struct
 
   (* Externally visible function for unification. *)
   (* Calls internal entry point and traps runaway recursion. *)
-  and unify cx t1 t2 =
-    try unify_opt cx ~use_op:unknown_use ~unify_any:true t1 t2 with
+  and unify cx ?(use_op = unknown_use) t1 t2 =
+    try unify_opt cx ~use_op ~unify_any:true t1 t2 with
     | RecursionCheck.LimitExceeded trace ->
       (* log and continue *)
       let reasons = FlowError.ordered_reasons (reason_of_t t1, reason_of_t t2) in

src/typing/flow_js.mli

@@ -15,7 +15,7 @@ val flow : Context.t -> Type.t * Type.use_t -> unit
 
 val flow_t : Context.t -> Type.t * Type.t -> unit
 
-val unify : Context.t -> Type.t -> Type.t -> unit
+val unify : Context.t -> ?use_op:Type.use_op -> Type.t -> Type.t -> unit
 
 val flow_p :
   Context.t ->

src/typing/new_env.ml

@@ -5,6 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+open Utils_js
 open Type
 open Reason
 open Loc_collections
@@ -13,16 +14,93 @@ open Loc_collections
 (* Helpers **************)
 (************************)
 
-let _find_var { Env_api.env_values; _ } loc = ALocMap.find loc env_values
+let find_var { Env_api.env_values; _ } loc = ALocMap.find loc env_values
 
-let _find_refi { Env_api.refinement_of_id; _ } = refinement_of_id
+let find_refi { Env_api.refinement_of_id; _ } = refinement_of_id
 
 let _is_provider { Env_api.providers; _ } = Env_api.Provider_api.is_provider providers
 
 let _find_providers { Env_api.providers; _ } loc =
   Env_api.Provider_api.providers_of_def providers loc
   |> Base.Option.value ~default:[]
   |> Base.List.map ~f:Reason.aloc_of_reason
+(*************)
+(*  Reading  *)
+(*************)
+
+(** Computes the phi type for a node given all its lower bounds
+ *  Currently, this just produces a new type variable with the types of
+ *  all the incoming writes as lower bounds. In the future, however, we
+ *  may want to compute a more specific least upper bound for these writes.
+ *)
+let phi cx reason ts =
+  Tvar.mk_where cx reason (fun tvar -> Base.List.iter ts ~f:(fun t -> Flow_js.flow_t cx (t, tvar)))
+
+let rec predicate_of_refinement cx =
+  Env_api.Refi.(
+    function
+    | AndR (r1, r2) -> AndP (predicate_of_refinement cx r1, predicate_of_refinement cx r2)
+    | OrR (r1, r2) -> OrP (predicate_of_refinement cx r1, predicate_of_refinement cx r2)
+    | NotR r -> NotP (predicate_of_refinement cx r)
+    | TruthyR loc -> ExistsP (Some loc)
+    | NullR -> NullP
+    | UndefinedR -> VoidP
+    | MaybeR -> MaybeP
+    | InstanceOfR loc ->
+      (* Instanceof refinements store the loc they check against, which is a read in the env *)
+      let reason = mk_reason (RCustom "RHS of `instanceof` operator") loc in
+      let t = read cx loc reason in
+      Flow_js.flow cx (t, AssertInstanceofRHST reason);
+      LeftP (InstanceofTest, t)
+    | IsArrayR -> ArrP
+    | BoolR loc -> BoolP loc
+    | FunctionR -> FunP
+    | NumberR loc -> NumP loc
+    | ObjectR -> ObjP
+    | StringR loc -> StrP loc
+    | SymbolR loc -> SymbolP loc
+    | SingletonBoolR { loc; sense = _; lit } -> SingletonBoolP (loc, lit)
+    | SingletonStrR { loc; sense; lit } -> SingletonStrP (loc, sense, lit)
+    | SingletonNumR { loc; sense; lit } -> SingletonNumP (loc, sense, lit)
+    | SentinelR (prop, loc) ->
+      PropExistsP (prop, mk_reason (RProperty (Some (OrdinaryName prop))) loc))
+
+and refine cx reason loc refi t =
+  Base.Option.value_map
+    ~f:(fun predicate ->
+      let predicate = predicate |> snd |> predicate_of_refinement cx in
+      let reason = mk_reason (RRefined (desc_of_reason reason)) loc in
+      Tvar.mk_no_wrap_where cx reason (fun tvar ->
+          Flow_js.flow cx (t, PredicateT (predicate, tvar))))
+    ~default:t
+    refi
+
+and read cx loc reason =
+  let ({ Loc_env.var_info; _ } as env) = Context.environment cx in
+  let rec type_of_state states refi =
+    Base.List.map
+      ~f:(function
+        | Env_api.With_ALoc.Uninitialized -> Type.(VoidT.at loc |> with_trust Trust.bogus_trust)
+        | Env_api.With_ALoc.Write reason ->
+          Debug_js.Verbose.print_if_verbose
+            cx
+            [
+              spf
+                "reading %s from location %s"
+                (ALoc.debug_to_string loc)
+                (Reason.aloc_of_reason reason |> ALoc.debug_to_string);
+            ];
+          Base.Option.value_exn (Reason.aloc_of_reason reason |> Loc_env.find_write env)
+        | Env_api.With_ALoc.Refinement { refinement_id; writes } ->
+          find_refi var_info refinement_id |> Base.Option.some |> type_of_state writes
+        | Env_api.With_ALoc.Global name -> Flow_js.get_builtin cx (Reason.OrdinaryName name) reason)
+      states
+    |> phi cx reason
+    |> refine cx reason loc refi
+  in
+  let var_state = find_var var_info loc in
+  let t = type_of_state var_state None in
+  Flow_js.reposition cx loc t
 
 (************************)
 (* Variable Declaration *)

src/typing/new_env.mli

@@ -5,4 +5,6 @@
  * LICENSE file in the root directory of this source tree.
  *)
 
+val read : Context.t -> ALoc.t -> Reason.t -> Type.t
+
 val initialize_all : Context.t -> unit

src/typing/subtyping_kit.ml

@@ -1755,7 +1755,7 @@ module Make (Flow : INPUT) : OUTPUT = struct
     | ( GenericT ({ bound = bound1; id = id1; reason = reason1; _ } as g1),
         GenericT ({ bound = bound2; id = id2; reason = reason2; _ } as g2) ) ->
       begin
-        match Generic.satisfies ~printer:(print_if_verbose_lazy cx trace) id1 id2 with
+        match Generic.satisfies ~printer:(print_if_verbose_lazy cx ~trace) id1 id2 with
         | Generic.Satisfied ->
           rec_flow_t
             cx

src/typing/trust_checking.ml

@@ -33,7 +33,7 @@ module TrustKit (Flow : Flow_common.S) : Flow_common.TRUST_CHECKING = struct
      See below for the algorithm that uses these helpers.
   *)
   let set_new_lower_bound cx trace id ltrust utrust new_trust ubounds =
-    print_if_verbose cx trace [Printf.sprintf "Tainting %d to %s" id (string_of_trust new_trust)];
+    print_if_verbose cx ~trace [Printf.sprintf "Tainting %d to %s" id (string_of_trust new_trust)];
     if subtype_trust ltrust utrust then (
       set_trust ubounds new_trust;
       true
@@ -97,7 +97,10 @@ module TrustKit (Flow : Flow_common.S) : Flow_common.TRUST_CHECKING = struct
   (* These functions work exactly as above, except for upper trust bounds
      propagating to lower variable bounds, and with publicity instead of taint. *)
   let set_new_upper_bound cx trace id ltrust utrust new_trust lbounds =
-    print_if_verbose cx trace [Printf.sprintf "Publicizing %d to %s" id (string_of_trust new_trust)];
+    print_if_verbose
+      cx
+      ~trace
+      [Printf.sprintf "Publicizing %d to %s" id (string_of_trust new_trust)];
     if subtype_trust ltrust utrust then (
       set_trust lbounds new_trust;
       true
@@ -155,7 +158,7 @@ module TrustKit (Flow : Flow_common.S) : Flow_common.TRUST_CHECKING = struct
       let utrust = get_trust ub in
       let (u_lowervars, u_uppervars) = get_bounds ub in
       if not (ISet.mem id1 u_lowervars) then (
-        print_if_verbose cx trace [Printf.sprintf "Trust linking %d to %d" id1 id2];
+        print_if_verbose cx ~trace [Printf.sprintf "Trust linking %d to %d" id1 id2];
         if flow_new_lower_bound cx trace ltrust id2 ub then
           if flow_new_upper_bound cx trace utrust id1 lb then (
             let new_upper = ISet.add id2 u_uppervars in
@@ -195,7 +198,6 @@ module TrustKit (Flow : Flow_common.S) : Flow_common.TRUST_CHECKING = struct
       if new_trust <> trust then (
         print_if_verbose
           cx
-          Trace.dummy_trace
           [
             Printf.sprintf
               "Strengthening %d from %s to %s"