kill uses of Config.curr_language in subtyping part of prover.ml

Reviewed By: cristianoc

Differential Revision: D3352715

fbshipit-source-id: b10103c

infer/src/IR/Sil.re

@@ -1882,6 +1882,38 @@ let hpara_equal hpara1 hpara2 => hpara_compare hpara1 hpara2 == 0;
 let hpara_dll_equal hpara1 hpara2 => hpara_dll_compare hpara1 hpara2 == 0;
 
 
+/** if [struct_typ] is a class, return its class kind (Java, CPP, or Obj-C) */
+let struct_typ_get_class_kind struct_typ =>
+  switch struct_typ.csu {
+  | Csu.Class class_kind => Some class_kind
+  | _ => None
+  };
+
+
+/** return true if [struct_typ] is a Java class */
+let struct_typ_is_java_class struct_typ =>
+  switch (struct_typ_get_class_kind struct_typ) {
+  | Some Csu.Java => true
+  | _ => false
+  };
+
+
+/** return true if [struct_typ] is a C++ class. Note that this returns false for raw structs. */
+let struct_typ_is_cpp_class struct_typ =>
+  switch (struct_typ_get_class_kind struct_typ) {
+  | Some Csu.CPP => true
+  | _ => false
+  };
+
+
+/** return true if [struct_typ] is an Obj-C class. Note that this returns false for raw structs. */
+let struct_typ_is_objc_class struct_typ =>
+  switch (struct_typ_get_class_kind struct_typ) {
+  | Some Csu.Objc => true
+  | _ => false
+  };
+
+
 /** {2 Sets and maps of types} */
 let module StructTypSet = Set.Make {
   type t = struct_typ;

infer/src/IR/Sil.rei

@@ -348,6 +348,22 @@ and exp =
 let struct_typ_equal: struct_typ => struct_typ => bool;
 
 
+/** if [struct_typ] is a class, return its class kind (Java, CPP, or Obj-C) */
+let struct_typ_get_class_kind: struct_typ => option Csu.class_kind;
+
+
+/** return true if [struct_typ] is a Java class */
+let struct_typ_is_java_class: struct_typ => bool;
+
+
+/** return true if [struct_typ] is a C++ class. Note that this returns false for raw structs. */
+let struct_typ_is_cpp_class: struct_typ => bool;
+
+
+/** return true if [struct_typ] is an Obj-C class. Note that this returns false for raw structs. */
+let struct_typ_is_objc_class: struct_typ => bool;
+
+
 /** Sets of types. */
 let module StructTypSet: Set.S with type elt = struct_typ;
 

infer/src/backend/prover.ml

@@ -40,6 +40,11 @@ let rec remove_redundancy have_same_key acc = function
       if have_same_key x y then remove_redundancy have_same_key acc (x:: l')
       else remove_redundancy have_same_key (x:: acc) l
 
+let rec is_java_class = function
+  | Sil.Tstruct struct_typ -> Sil.struct_typ_is_java_class struct_typ
+  | Sil.Tarray (inner_typ, _) | Tptr (inner_typ, _) -> is_java_class inner_typ
+  | _ -> false
+
 (** {2 Ordinary Theorem Proving} *)
 
 let (++) = Sil.Int.add
@@ -821,13 +826,14 @@ let check_inconsistency_base prop =
     let procedure_attr =
       Cfg.Procdesc.get_attributes procdesc in
     let is_java_this pvar =
-      !Config.curr_language = Config.Java && Pvar.is_this pvar in
+      procedure_attr.ProcAttributes.language = Config.Java && Pvar.is_this pvar in
     let is_objc_instance_self pvar =
-      !Config.curr_language = Config.Clang &&
+      procedure_attr.ProcAttributes.language = Config.Clang &&
       Pvar.get_name pvar = Mangled.from_string "self" &&
       procedure_attr.ProcAttributes.is_objc_instance_method in
     let is_cpp_this pvar =
-      !Config.curr_language = Config.Clang && Pvar.is_this pvar &&
+      procedure_attr.ProcAttributes.language = Config.Clang &&
+      Pvar.is_this pvar &&
       procedure_attr.ProcAttributes.is_cpp_instance_method in
     let do_hpred = function
       | Sil.Hpointsto (Sil.Lvar pv, Sil.Eexp (e, _), _) ->
@@ -1528,7 +1534,8 @@ struct
 
   (** check if t1 is a subtype of t2 *)
   let check_subtype tenv t1 t2 =
-    if !Config.curr_language = Config.Java then
+    if is_java_class t1
+    then
       check_subtype_java tenv t1 t2
     else
       match get_cpp_objc_type_name t1, get_cpp_objc_type_name t2 with
@@ -1562,7 +1569,7 @@ struct
         else None, Some st1
 
   let case_analysis_type tenv (t1, st1) (t2, st2) =
-    if !Config.curr_language = Config.Java then
+    if is_java_class t1 then
       case_analysis_type_java tenv (t1, st1) (t2, st2)
     else match get_cpp_objc_type_name t1, get_cpp_objc_type_name t2 with
       | Some cn1, Some cn2 ->
@@ -1639,11 +1646,11 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
   (* classes and arrays in Java, and just classes in C++ and ObjC *)
   let types_subject_to_dynamic_cast =
     match texp1, texp2 with
-    | Sil.Sizeof (Sil.Tstruct _, _), Sil.Sizeof (Sil.Tstruct _, _)
-    | Sil.Sizeof (Sil.Tarray _, _), Sil.Sizeof (Sil.Tarray _, _)
-    | Sil.Sizeof (Sil.Tarray _, _), Sil.Sizeof (Sil.Tstruct _, _)
-    | Sil.Sizeof (Sil.Tstruct _, _), Sil.Sizeof (Sil.Tarray _, _)
-      when !Config.curr_language = Config.Java -> true
+    | Sil.Sizeof ((Sil.Tstruct _) as typ1, _), Sil.Sizeof (Sil.Tstruct _, _)
+    | Sil.Sizeof ((Sil.Tarray _) as typ1, _), Sil.Sizeof (Sil.Tarray _, _)
+    | Sil.Sizeof ((Sil.Tarray _) as typ1, _), Sil.Sizeof (Sil.Tstruct _, _)
+    | Sil.Sizeof ((Sil.Tstruct _) as typ1, _), Sil.Sizeof (Sil.Tarray _, _)
+      when is_java_class typ1 -> true
 
     | Sil.Sizeof (typ1, _), Sil.Sizeof (typ2, _) ->
         (Sil.is_cpp_class typ1 && Sil.is_cpp_class typ2) ||