From fa077c75d05f184f77ff954fc2068abb01e5e826 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Mon, 30 May 2016 08:33:56 -0700 Subject: [PATCH] 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 | 32 ++++++++++++++++++++++++++++++++ infer/src/IR/Sil.rei | 16 ++++++++++++++++ infer/src/backend/prover.ml | 27 +++++++++++++++++---------- 3 files changed, 65 insertions(+), 10 deletions(-) diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 674de061c..1f8e2bd1f 100644 --- a/infer/src/IR/Sil.re +++ b/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; diff --git a/infer/src/IR/Sil.rei b/infer/src/IR/Sil.rei index 3cd1b9a36..ea00a4b45 100644 --- a/infer/src/IR/Sil.rei +++ b/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; diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 7dc3cde07..ea0f665e2 100644 --- a/infer/src/backend/prover.ml +++ b/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) ||