[infer][backend] Simplify the code doing the case analysis for execturing the cast instruction

Summary: Pure refactoring simplifying the code doing the case analysis for execturing the cast instruction.

Reviewed By: dulmarod

Differential Revision: D4215238

fbshipit-source-id: 9f0f163

infer/src/IR/Subtype.re

@@ -61,10 +61,38 @@ type subtMap = SubtypesMap.t bool;
 
 let subtMap: ref subtMap = ref SubtypesMap.empty;
 
-let check_subtype f c1 c2 =>
+let is_interface tenv (class_name: Typename.t) =>
+  switch (class_name, Tenv.lookup tenv class_name) {
+  | (TN_csu (Class Java) _, Some {fields: [], methods: []}) => true
+  | _ => false
+  };
+
+let is_root_class class_name =>
+  switch class_name {
+  | Typename.TN_csu (Csu.Class Csu.Java) _ =>
+    Typename.equal class_name Typename.Java.java_lang_object
+  | Typename.TN_csu (Csu.Class Csu.CPP) _ => false
+  | _ => false
+  };
+
+
+/** check if c1 is a subclass of c2 */
+let check_subclass_tenv tenv c1 c2 => {
+  let rec check (cn: Typename.t) =>
+    Typename.equal cn c2 ||
+    is_root_class c2 || (
+      switch (cn, Tenv.lookup tenv cn) {
+      | (TN_csu (Class _) _, Some {supers}) => IList.exists check supers
+      | _ => false
+      }
+    );
+  check c1
+};
+
+let check_subtype tenv c1 c2 =>
   try (SubtypesMap.find (c1, c2) !subtMap) {
   | Not_found =>
-    let is_subt = f c1 c2;
+    let is_subt = check_subclass_tenv tenv c1 c2;
     subtMap := SubtypesMap.add (c1, c2) is_subt !subtMap;
     is_subt
   };
@@ -190,26 +218,26 @@ let subtypes_to_string t =>
   };
 
 /* c is a subtype when it does not appear in the list l of no-subtypes */
-let is_subtype f c l =>
+let is_subtype tenv c l =>
   try {
-    ignore (IList.find (f c) l);
+    ignore (IList.find (check_subtype tenv c) l);
     false
   } {
   | Not_found => true
   };
 
-let is_strict_subtype f c1 c2 => f c1 c2 && not (Typename.equal c1 c2);
+let is_strict_subtype tenv c1 c2 => check_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:
    1) not (Xi <: A) because removing the subtypes of Xi has no effect unless Xi is a subtype of A
    2) Xi <: Xj because the subtypes of Xi are a subset of the subtypes of Xj */
-let check_redundancies f c l => {
+let check_redundancies tenv c l => {
   let aux (l, add) ci => {
     let (l, should_add) =
-      if (f ci c) {
+      if (check_subtype tenv ci c) {
         (l, true)
-      } else if (f c ci) {
+      } else if (check_subtype tenv c ci) {
         ([ci, ...l], false)
       } else {
         ([ci, ...l], true)
@@ -232,16 +260,16 @@ let rec updates_head f c l =>
 
 /* adds the classes of l2 to l1 and checks that no redundancies or inconsistencies will occur
    A - { X1,..., Xn } is inconsistent if A <: Xi for some i */
-let rec add_not_subtype f c1 l1 l2 =>
+let rec add_not_subtype tenv c1 l1 l2 =>
   switch l2 {
   | [] => l1
   | [c, ...rest] =>
-    if (f c1 c) {
+    if (check_subtype tenv c1 c) {
-      add_not_subtype f c1 l1 rest
+      add_not_subtype tenv c1 l1 rest
     } else {
       /* checks for inconsistencies */
-      let (l1', should_add) = check_redundancies f c l1; /* checks for redundancies */
+      let (l1', should_add) = check_redundancies tenv c l1; /* checks for redundancies */
-      let rest' = add_not_subtype f c1 l1' rest;
+      let rest' = add_not_subtype tenv c1 l1' rest;
       if should_add {
         [c, ...rest']
       } else {
@@ -250,8 +278,8 @@ let rec add_not_subtype f c1 l1 l2 =>
     }
   };
 
-let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface => {
+let get_subtypes tenv (c1, (st1, flag1): t) (c2, (st2, flag2): t) => {
-  let is_sub = f c1 c2;
+  let is_sub = check_subtype tenv c1 c2;
   let (pos_st, neg_st) =
     switch (st1, st2) {
     | (Exact, Exact) =>
@@ -261,7 +289,7 @@ let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface => {
         (None, Some st1)
       }
     | (Exact, Subtypes l2) =>
-      if (is_sub && is_subtype f c1 l2) {
+      if (is_sub && is_subtype tenv c1 l2) {
         (Some st1, None)
       } else {
         (None, Some st1)
@@ -270,28 +298,28 @@ let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface => {
       if is_sub {
         (Some st1, None)
       } else {
-        let l1' = updates_head f c2 l1;
+        let l1' = updates_head tenv c2 l1;
-        if (is_subtype f c2 l1) {
+        if (is_subtype tenv c2 l1) {
-          (Some (Subtypes l1'), Some (Subtypes (add_not_subtype f c1 l1 [c2])))
+          (Some (Subtypes l1'), Some (Subtypes (add_not_subtype tenv c1 l1 [c2])))
         } else {
           (None, Some st1)
         }
       }
     | (Subtypes l1, Subtypes l2) =>
-      if (is_interface c2 || is_sub) {
+      if (is_interface tenv c2 || is_sub) {
-        if (is_subtype f c1 l2) {
+        if (is_subtype tenv c1 l2) {
-          let l2' = updates_head f c1 l2;
+          let l2' = updates_head tenv c1 l2;
-          (Some (Subtypes (add_not_subtype f c1 l1 l2')), None)
+          (Some (Subtypes (add_not_subtype tenv c1 l1 l2')), None)
         } else {
           (None, Some st1)
         }
       } else if (
-        (is_interface c1 || f c2 c1) && is_subtype f c2 l1
+        (is_interface tenv c1 || check_subtype tenv c2 c1) && is_subtype tenv c2 l1
       ) {
-        let l1' = updates_head f c2 l1;
+        let l1' = updates_head tenv c2 l1;
         (
-          Some (Subtypes (add_not_subtype f c2 l1' l2)),
+          Some (Subtypes (add_not_subtype tenv c2 l1' l2)),
-          Some (Subtypes (add_not_subtype f c1 l1 [c2]))
+          Some (Subtypes (add_not_subtype tenv c1 l1 [c2]))
         )
       } else {
         (None, Some st1)
@@ -300,11 +328,11 @@ let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface => {
   (normalize_subtypes pos_st c1 c2 flag1 flag2, normalize_subtypes neg_st c1 c2 flag1 flag2)
 };
 
-let case_analysis_basic (c1, st) (c2, (_, flag2)) f => {
+let case_analysis_basic tenv (c1, st) (c2, (_, flag2)) => {
   let (pos_st, neg_st) =
-    if (f c1 c2) {
+    if (check_subtype tenv c1 c2) {
       (Some st, None)
-    } else if (f c2 c1) {
+    } else if (check_subtype tenv c2 c1) {
       switch st {
       | (Exact, _) =>
         if (Typename.equal c1 c2) {
@@ -333,11 +361,9 @@ let case_analysis_basic (c1, st) (c2, (_, flag2)) f => {
     - whether [st1] and [st2] admit [c1 <: c2], and in case return the updated subtype [st1]
     - whether [st1] and [st2] admit [not(c1 <: c2)],
     and in case return the updated subtype [st1] */
-let case_analysis (c1, st1) (c2, st2) f is_interface => {
+let case_analysis tenv (c1, st1) (c2, st2) =>
-  let f = check_subtype f;
   if Config.subtype_multirange {
-    get_subtypes (c1, st1) (c2, st2) f is_interface
+    get_subtypes tenv (c1, st1) (c2, st2)
   } else {
-    case_analysis_basic (c1, st1) (c2, st2) f
+    case_analysis_basic tenv (c1, st1) (c2, st2)
-  }
+  };
-};

infer/src/IR/Subtype.rei

@@ -35,20 +35,14 @@ let subtypes_instof: t;
 let join: t => t => t;
 
 
-/** [case_analysis (c1, st1) (c2,st2) f] 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] where f c1 c2 is true if c1 is a subtype of c2.
+    to [st1] and [st2].
-    get_subtypes returning a pair:
+    [case_analysis] returns a pair:
-    - whether [st1] and [st2] admit [c1 <: c2], and in case return the updated subtype [st1]
+    - 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 return
+    - whether [st1] and [st2] admit [not(c1 <: c2)], and in case returns the updated subtype [st1] */
-    the updated subtype [st1] */
+let case_analysis: Tenv.t => (Typename.t, t) => (Typename.t, t) => (option t, option t);
-let case_analysis:
+
-  (Typename.t, t) =>
+let check_subtype: Tenv.t => Typename.t => Typename.t => bool;
-  (Typename.t, t) =>
-  (Typename.t => Typename.t => bool) =>
-  (Typename.t => bool) =>
-  (option t, option t);
-
-let check_subtype: (Typename.t => Typename.t => bool) => Typename.t => Typename.t => bool;
 
 let subtypes_to_string: t => string;
 

infer/src/IR/Typename.re

@@ -45,7 +45,9 @@ let module Java = {
     fun
     | TN_csu (Class Java) _ => true
     | _ => false;
-  let java_lang_Object = from_string "java.lang.Object";
+  let java_lang_object = from_string "java.lang.Object";
+  let java_io_serializable = from_string "java.io.Serializable";
+  let java_lang_cloneable = from_string "java.lang.Cloneable";
 };
 
 type typename_t = t;

infer/src/IR/Typename.rei

@@ -38,7 +38,9 @@ let module Java: {
 
   /** [is_class name] holds if [name] names a Java class */
   let is_class: t => bool;
-  let java_lang_Object: t;
+  let java_lang_object: t;
+  let java_io_serializable: t;
+  let java_lang_cloneable: t;
 };
 
 let module Set: Set.S with type elt = t;

infer/src/backend/BuiltinDefn.ml

@@ -244,9 +244,10 @@ let execute___instanceof_cast ~instof
       (* and throw an exception in case of a cast to a reference. *)
       let should_throw_exception =
         !Config.curr_language = Config.Java || is_cast_to_reference in
-      let deal_with_failed_cast val1 _ texp1 texp2 =
+      let deal_with_failed_cast val1 texp1 texp2 =
-        Tabulation.raise_cast_exception tenv
+        raise
-          __POS__ None texp1 texp2 val1 in
+          (Tabulation.create_cast_exception
+             tenv __POS__ None texp1 texp2 val1) in
       let exe_one_prop prop =
         if Exp.equal texp2 Exp.zero then
           [(return_result tenv Exp.zero prop ret_id, path)]
@@ -268,11 +269,9 @@ let execute___instanceof_cast ~instof
                           else replace_ptsto_texp tenv prop val1 texp1' in
                         [(return_result tenv res_e prop' ret_id, path)] in
                   if instof then (* instanceof *)
-                    begin
+                    let pos_res = mk_res pos_type_opt Exp.one in
-                      let pos_res = mk_res pos_type_opt Exp.one in
+                    let neg_res = mk_res neg_type_opt Exp.zero in
-                      let neg_res = mk_res neg_type_opt Exp.zero in
+                    pos_res @ neg_res
-                      pos_res @ neg_res
-                    end
                   else (* cast *)
                   if not should_throw_exception then (* C++ case when negative cast returns 0 *)
                     let pos_res = mk_res pos_type_opt val1 in
@@ -280,20 +279,16 @@ let execute___instanceof_cast ~instof
                     pos_res @ neg_res
                   else
                     begin
-                      if (!Config.footprint = true) then
+                      if !Config.footprint then
-                        begin
+                        match pos_type_opt with
-                          match pos_type_opt with
+                        | None -> deal_with_failed_cast val1 texp1 texp2
-                          | None -> deal_with_failed_cast val1 typ1 texp1 texp2
+                        | Some _ -> mk_res pos_type_opt val1
-                          | Some _ -> mk_res pos_type_opt val1
+                      else (* !Config.footprint is false *)
-                        end
+                        match neg_type_opt with
-                      else (* !Config.footprint = false *)
+                        | Some _ ->
-                        begin
+                            if is_undefined_opt tenv prop val1 then mk_res pos_type_opt val1
-                          match neg_type_opt with
+                            else deal_with_failed_cast val1 texp1 texp2
-                          | Some _ ->
+                        | None -> mk_res pos_type_opt val1
-                              if is_undefined_opt tenv prop val1 then mk_res pos_type_opt val1
-                              else deal_with_failed_cast val1 typ1 texp1 texp2
-                          | None -> mk_res pos_type_opt val1
-                        end
                     end
               | _ -> []
             with Not_found ->

infer/src/backend/prover.ml

@@ -1525,39 +1525,6 @@ let expand_hpred_pointer =
 module Subtyping_check =
 struct
 
-  let object_type = Typename.Java.java_lang_Object
-
-  let serializable_type = Typename.Java.from_string "java.io.Serializable"
-
-  let cloneable_type = Typename.Java.from_string "java.lang.Cloneable"
-
-  let is_interface tenv (class_name: Typename.t) =
-    match class_name, Tenv.lookup tenv class_name with
-    | TN_csu (Class Java, _), Some { fields = []; methods = []; } -> true
-    | _ -> false
-
-  let is_root_class class_name =
-    match class_name with
-    | Typename.TN_csu (Csu.Class Csu.Java, _) ->
-        Typename.equal class_name object_type
-    | Typename.TN_csu (Csu.Class Csu.CPP, _) ->
-        false
-    | _ -> false
-
-  (** check if c1 is a subclass of c2 *)
-  let check_subclass_tenv tenv c1 c2 =
-    let rec check (cn: Typename.t) =
-      Typename.equal cn c2 || is_root_class c2 ||
-      match cn, Tenv.lookup tenv cn with
-      | TN_csu (Class _, _), Some { supers } ->
-          IList.exists check supers
-      | _ -> false in
-    check c1
-
-  let check_subclass tenv c1 c2 =
-    let f = check_subclass_tenv tenv in
-    Subtype.check_subtype f c1 c2
-
   (** check that t1 and t2 are the same primitive type *)
   let check_subtype_basic_type t1 t2 =
     match t2 with
@@ -1571,15 +1538,15 @@ 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) ->
-        check_subclass tenv cn1 cn2
+        Subtype.check_subtype tenv cn1 cn2
     | Tarray (dom_type1, _), Tarray (dom_type2, _) ->
         check_subtype_java tenv dom_type1 dom_type2
     | Tptr (dom_type1, _), Tptr (dom_type2, _) ->
         check_subtype_java tenv dom_type1 dom_type2
     | Tarray _, Tstruct (TN_csu (Class Java, _) as cn2) ->
-        Typename.equal cn2 serializable_type
+        Typename.equal cn2 Typename.Java.java_io_serializable
-        || Typename.equal cn2 cloneable_type
+        || Typename.equal cn2 Typename.Java.java_lang_cloneable
-        || Typename.equal cn2 object_type
+        || Typename.equal cn2 Typename.Java.java_lang_object
     | _ -> check_subtype_basic_type t1 t2
 
   (** check if t1 is a subtype of t2 *)
@@ -1589,18 +1556,17 @@ struct
       check_subtype_java tenv t1 t2
     else
       match Typ.name t1, Typ.name t2 with
-      | Some cn1, Some cn2 -> check_subclass tenv cn1 cn2
+      | Some cn1, Some cn2 -> Subtype.check_subtype tenv cn1 cn2
       | _ -> false
 
   let rec case_analysis_type tenv ((t1: Typ.t), st1) ((t2: Typ.t), st2) =
     match t1, t2 with
     | Tstruct (TN_csu (Class Java, _) as cn1), Tstruct (TN_csu (Class Java, _) as cn2) ->
-        Subtype.case_analysis
+        Subtype.case_analysis tenv (cn1, st1) (cn2, st2)
-          (cn1, st1) (cn2, st2) (check_subclass tenv) (is_interface tenv)
     | Tstruct (TN_csu (Class Java, _) as cn1), Tarray _
-      when (Typename.equal cn1 serializable_type
+      when (Typename.equal cn1 Typename.Java.java_io_serializable
-            || Typename.equal cn1 cloneable_type
+            || Typename.equal cn1 Typename.Java.java_lang_cloneable
-            || Typename.equal cn1 object_type) &&
+            || Typename.equal cn1 Typename.Java.java_lang_object) &&
            st1 <> Subtype.exact ->
         Some st1, None
     | Tstruct cn1, Tstruct cn2
@@ -1608,9 +1574,8 @@ 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 check_subclass tenv cn1 cn2 || check_subclass tenv cn2 cn1 ->
+      when Subtype.check_subtype tenv cn1 cn2 || Subtype.check_subtype tenv cn2 cn1 ->
-        Subtype.case_analysis
+        Subtype.case_analysis tenv (cn1, st1) (cn2, st2)
-          (cn1, st1) (cn2, st2) (check_subclass tenv) (is_interface tenv)
     | Tarray (dom_type1, _), Tarray (dom_type2, _) ->
         case_analysis_type tenv (dom_type1, st1) (dom_type2, st2)
     | Tptr (dom_type1, _), Tptr (dom_type2, _) ->
@@ -1709,7 +1674,7 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
         | Some texp1' ->
             not (texp_equal_modulo_subtype_flag texp1' texp1)
         | None -> false in
-      if (calc_missing) then (* footprint *)
+      if calc_missing then (* footprint *)
         begin
           match pos_type_opt with
           | None -> cast_exception tenv texp1 texp2 e1 subs

infer/src/backend/tabulation.ml

@@ -986,9 +986,8 @@ let class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc =
       pname_opt texp1 texp2 exp (State.get_node ()) (State.get_loc ()) in
   Exceptions.Class_cast_exception (desc, ml_loc)
 
-let raise_cast_exception tenv ml_loc pname_opt texp1 texp2 exp =
+let create_cast_exception tenv ml_loc pname_opt texp1 texp2 exp =
-  let exn = class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc in
+  class_cast_exn tenv pname_opt texp1 texp2 exp ml_loc
-  raise exn
 
 let get_check_exn tenv check callee_pname loc ml_loc = match check with
   | Prover.Bounds_check ->

infer/src/backend/tabulation.mli

@@ -27,8 +27,8 @@ val check_attr_dealloc_mismatch : PredSymb.t -> PredSymb.t -> unit
 val find_dereference_without_null_check_in_sexp : Sil.strexp -> (int * PredSymb.path_pos) option
 
 (** raise a cast exception *)
-val raise_cast_exception :
+val create_cast_exception :
-  Tenv.t -> Logging.ml_loc -> Procname.t option -> Exp.t -> Exp.t -> Exp.t -> 'a
+  Tenv.t -> Logging.ml_loc -> Procname.t option -> Exp.t -> Exp.t -> Exp.t -> exn
 
 (** check if a prop is an exception *)
 val prop_is_exn : Procname.t -> 'a Prop.t -> bool

infer/src/checkers/patternMatch.ml

@@ -26,7 +26,7 @@ type taint_spec = {
 
 let type_is_object typ =
   match typ with
-  | Typ.Tptr (Tstruct name, _) -> Typename.equal name Typename.Java.java_lang_Object
+  | Typ.Tptr (Tstruct name, _) -> Typename.equal name Typename.Java.java_lang_object
   | _ -> false
 
 let java_proc_name_with_class_method pn_java class_with_path method_name =