[infer][backend] Add functions to separate the cases when the subtyping relation can be proven from the case where the no subtyping relation can be proven.

Summary:
The two concepts are not negation of each other. The type environment created by the different frontends is not guaranteed to contain a full view of the type hierarchy. In this case, there can be holes preventing Infer to prove that `t <: t'` if the type definition between `t` and `t'` is missing. There are now two functions:
# `is_known_subtype` when the subtyping relation can be proven
# `is_known_not_subtype` when it can be proven that there is no subtyping relation between two types

This diff is intended to make no functional changes but to add functionality to detect cast error angelically, i.e. assuming that the program is probably fine where there is not enough information to prove the cast error.

Reviewed By: jberdine

Differential Revision: D4345803

fbshipit-source-id: 39b79bc

infer/src/IR/Subtype.re

@@ -54,15 +54,18 @@ type kind =
 
 type t = (t', kind) [@@deriving compare];
 
-let module SubtypesPair = {
+type result =
-  type t = (Typename.t, Typename.t) [@@deriving compare];
+  | No
-};
+  | Unknown
-
+  | Yes
-let module SubtypesMap = Caml.Map.Make SubtypesPair;
+[@@deriving compare];
-
-type subtMap = SubtypesMap.t bool;
 
-let subtMap: ref subtMap = ref SubtypesMap.empty;
+let max_result res1 res2 =>
+  if (compare_result res1 res2 <= 0) {
+    res2
+  } else {
+    res1
+  };
 
 let is_interface tenv (class_name: Typename.t) =>
   switch (class_name, Tenv.lookup tenv class_name) {
@@ -80,25 +83,55 @@ let is_root_class class_name =>
 
 
 /** check if c1 is a subclass of c2 */
-let check_subclass_tenv tenv c1 c2 => {
+let check_subclass_tenv tenv c1 c2 :result => {
-  let rec check (cn: Typename.t) =>
+  let rec loop best_result classnames :result =>
-    Typename.equal cn c2 ||
+    /* Check if the name c2 is found in the list of super types and
-    is_root_class c2 || (
+       keep the best results according to Yes > Unknown > No */
-      switch (cn, Tenv.lookup tenv cn) {
+    if (best_result == Yes) {
-      | (TN_csu (Class _) _, Some {supers}) => IList.exists check supers
+      Yes
-      | _ => false
+    } else {
+      switch classnames {
+      | [] => best_result
+      | [cn, ...cns] => loop (max_result best_result (check cn)) cns
+      }
+    }
+  and check cn :result =>
+    if (Typename.equal cn c2) {
+      Yes
+    } else {
+      switch (Tenv.lookup tenv cn) {
+      | None when is_root_class cn => No
+      | None => Unknown
+      | Some {supers} => loop No supers
       }
-    );
+    };
-  check c1
+  if (is_root_class c2) {
+    Yes
+  } else {
+    check c1
+  }
 };
 
-let check_subtype tenv c1 c2 =>
+let module SubtypesMap = Caml.Map.Make {
-  try (SubtypesMap.find (c1, c2) !subtMap) {
+  /* pair of subtypes */
-  | Not_found =>
+  type t = (Typename.t, Typename.t) [@@deriving compare];
-    let is_subt = check_subclass_tenv tenv c1 c2;
+};
-    subtMap := SubtypesMap.add (c1, c2) is_subt !subtMap;
+
-    is_subt
+let check_subtype = {
-  };
+  let subtMap = ref SubtypesMap.empty;
+  fun tenv c1 c2 => (
+    try (SubtypesMap.find (c1, c2) !subtMap) {
+    | Not_found =>
+      let is_subt = check_subclass_tenv tenv c1 c2;
+      subtMap := SubtypesMap.add (c1, c2) is_subt !subtMap;
+      is_subt
+    }: result
+  )
+};
+
+let is_known_subtype tenv c1 c2 :bool => check_subtype tenv c1 c2 == Yes;
+
+let is_known_not_subtype tenv c1 c2 :bool => check_subtype tenv c1 c2 == No;
 
 let flag_to_string flag =>
   switch flag {
@@ -196,15 +229,9 @@ let subtypes_to_string t =>
   };
 
 /* c is a subtype when it does not appear in the list l of no-subtypes */
-let is_subtype tenv c l =>
+let no_subtype_in_list tenv c l => not (IList.exists (is_known_subtype tenv c) l);
-  try {
-    ignore (IList.find (check_subtype tenv c) l);
-    false
-  } {
-  | Not_found => true
-  };
 
-let is_strict_subtype tenv c1 c2 => check_subtype tenv c1 c2 && not (Typename.equal c1 c2);
+let is_strict_subtype tenv c1 c2 => is_known_subtype tenv c1 c2 && not (Typename.equal c1 c2);
 
 /* checks for redundancies when adding c to l
    Xi in A - { X1,..., Xn } is redundant in two cases:
@@ -213,9 +240,9 @@ let is_strict_subtype tenv c1 c2 => check_subtype tenv c1 c2 && not (Typename.eq
 let check_redundancies tenv c l => {
   let aux (l, add) ci => {
     let (l, should_add) =
-      if (check_subtype tenv ci c) {
+      if (is_known_subtype tenv ci c) {
         (l, true)
-      } else if (check_subtype tenv c ci) {
+      } else if (is_known_subtype tenv c ci) {
         ([ci, ...l], false)
       } else {
         ([ci, ...l], true)
@@ -242,7 +269,7 @@ let rec add_not_subtype tenv c1 l1 l2 =>
   switch l2 {
   | [] => l1
   | [c, ...rest] =>
-    if (check_subtype tenv c1 c) {
+    if (is_known_subtype tenv c1 c) {
       add_not_subtype tenv c1 l1 rest
     } else {
       /* checks for inconsistencies */
@@ -257,7 +284,7 @@ let rec add_not_subtype tenv c1 l1 l2 =>
   };
 
 let get_subtypes tenv (c1, (st1, flag1): t) (c2, (st2, flag2): t) => {
-  let is_sub = check_subtype tenv c1 c2;
+  let is_sub = is_known_subtype tenv c1 c2;
   let (pos_st, neg_st) =
     switch (st1, st2) {
     | (Exact, Exact) =>
@@ -267,7 +294,7 @@ let get_subtypes tenv (c1, (st1, flag1): t) (c2, (st2, flag2): t) => {
         (None, Some st1)
       }
     | (Exact, Subtypes l2) =>
-      if (is_sub && is_subtype tenv c1 l2) {
+      if (is_sub && no_subtype_in_list tenv c1 l2) {
         (Some st1, None)
       } else {
         (None, Some st1)
@@ -277,7 +304,7 @@ let get_subtypes tenv (c1, (st1, flag1): t) (c2, (st2, flag2): t) => {
         (Some st1, None)
       } else {
         let l1' = updates_head tenv c2 l1;
-        if (is_subtype tenv c2 l1) {
+        if (no_subtype_in_list tenv c2 l1) {
           (Some (Subtypes l1'), Some (Subtypes (add_not_subtype tenv c1 l1 [c2])))
         } else {
           (None, Some st1)
@@ -285,14 +312,14 @@ let get_subtypes tenv (c1, (st1, flag1): t) (c2, (st2, flag2): t) => {
       }
     | (Subtypes l1, Subtypes l2) =>
       if (is_interface tenv c2 || is_sub) {
-        if (is_subtype tenv c1 l2) {
+        if (no_subtype_in_list tenv c1 l2) {
           let l2' = updates_head tenv c1 l2;
           (Some (Subtypes (add_not_subtype tenv c1 l1 l2')), None)
         } else {
           (None, Some st1)
         }
       } else if (
-        (is_interface tenv c1 || check_subtype tenv c2 c1) && is_subtype tenv c2 l1
+        (is_interface tenv c1 || is_known_subtype tenv c2 c1) && no_subtype_in_list tenv c2 l1
       ) {
         let l1' = updates_head tenv c2 l1;
         (
@@ -308,9 +335,9 @@ let get_subtypes tenv (c1, (st1, flag1): t) (c2, (st2, flag2): t) => {
 
 let case_analysis_basic tenv (c1, st) (c2, (_, flag2)) => {
   let (pos_st, neg_st) =
-    if (check_subtype tenv c1 c2) {
+    if (is_known_subtype tenv c1 c2) {
       (Some st, None)
-    } else if (check_subtype tenv c2 c1) {
+    } else if (is_known_subtype tenv c2 c1) {
       switch st {
       | (Exact, _) =>
         if (Typename.equal c1 c2) {

infer/src/IR/Subtype.rei

@@ -33,14 +33,26 @@ let subtypes_instof: t;
 let join: t => t => t;
 
 
-/** [case_analysis tenv (c1, st1) (c2,st2)] performs case analysis on [c1 <: c2] according
+/** [case_analysis tenv (c1, st1) (c2, st2)] performs case analysis on [c1 <: c2] according
     to [st1] and [st2].
     [case_analysis] returns a pair:
     - whether [st1] and [st2] admit [c1 <: c2], and in case returns the updated subtype [st1]
     - whether [st1] and [st2] admit [not(c1 <: c2)], and in case returns the updated subtype [st1] */
 let case_analysis: Tenv.t => (Typename.t, t) => (Typename.t, t) => (option t, option t);
 
-let check_subtype: Tenv.t => Typename.t => Typename.t => bool;
+
+/** [is_known_subtype tenv c1 c2] returns true if there is enough information in [tenv] to prove
+    that [c1] is a subtype of [c2].
+    Note that [not (is_known_subtype tenv c1 c2) == true] does not imply
+    that [is_known_not_subtype tenv c1 c2 == true] */
+let is_known_subtype: Tenv.t => Typename.t => Typename.t => bool;
+
+
+/** [is_known_not_subtype tenv c1 c2] returns true if there is enough information in [tenv] to prove
+    that [c1] is not a subtype of [c2].
+    Note that [not (is_known_not_subtype tenv c1 c2) == true] does not imply
+    that [is_known_subtype tenv c1 c2 == true] */
+let is_known_not_subtype: Tenv.t => Typename.t => Typename.t => bool;
 
 let subtypes_to_string: t => string;
 

infer/src/backend/prover.ml

@@ -1544,7 +1544,7 @@ struct
   let rec check_subtype_java tenv (t1: Typ.t) (t2: Typ.t) =
     match t1, t2 with
     | Tstruct (TN_csu (Class Java, _) as cn1), Tstruct (TN_csu (Class Java, _) as cn2) ->
-        Subtype.check_subtype tenv cn1 cn2
+        Subtype.is_known_subtype tenv cn1 cn2
     | Tarray (dom_type1, _), Tarray (dom_type2, _) ->
         check_subtype_java tenv dom_type1 dom_type2
     | Tptr (dom_type1, _), Tptr (dom_type2, _) ->
@@ -1562,7 +1562,7 @@ struct
       check_subtype_java tenv t1 t2
     else
       match Typ.name t1, Typ.name t2 with
-      | Some cn1, Some cn2 -> Subtype.check_subtype tenv cn1 cn2
+      | Some cn1, Some cn2 -> Subtype.is_known_subtype tenv cn1 cn2
       | _ -> false
 
   let rec case_analysis_type tenv ((t1: Typ.t), st1) ((t2: Typ.t), st2) =
@@ -1580,7 +1580,7 @@ struct
       (* that get through the type system, but not in C++ because of multiple inheritance, *)
       (* and not in ObjC because of being weakly typed, *)
       (* and the algorithm will only work correctly if this is the case *)
-      when Subtype.check_subtype tenv cn1 cn2 || Subtype.check_subtype tenv cn2 cn1 ->
+      when Subtype.is_known_subtype tenv cn1 cn2 || Subtype.is_known_subtype tenv cn2 cn1 ->
         Subtype.case_analysis tenv (cn1, st1) (cn2, st2)
     | Tarray (dom_type1, _), Tarray (dom_type2, _) ->
         case_analysis_type tenv (dom_type1, st1) (dom_type2, st2)