big refactoring to improve API for subtyping related operations

Reviewed By: jeremydubreil

Differential Revision: D3187979

fb-gh-sync-id: 31d19b9
fbshipit-source-id: 31d19b9

infer/src/IR/sil.ml

@@ -908,7 +908,7 @@ let rec is_array_of_cpp_class typ =
 let is_pointer_to_cpp_class typ =
   match typ with
   | Tptr (t, _) -> is_cpp_class t
-	| _ -> false
+  | _ -> false
 
 (** turn a *T into a T. fails if [typ] is not a pointer type *)
 let typ_strip_ptr = function
@@ -1300,6 +1300,9 @@ and struct_typ_compare struct_typ1 struct_typ2 =
       if n <> 0 then n else let n = Csu.compare struct_typ1.csu struct_typ2.csu in
         if n <> 0 then n else cname_opt_compare struct_typ1.struct_name struct_typ2.struct_name
 
+and struct_typ_equal struct_typ1 struct_typ2 =
+  struct_typ_compare struct_typ1 struct_typ2 = 0
+
 (** Comparision for types. *)
 and typ_compare t1 t2 =
   if t1 == t2 then 0 else match t1, t2 with
@@ -1610,6 +1613,11 @@ let hpara_dll_equal hpara1 hpara2 =
   (hpara_dll_compare hpara1 hpara2 = 0)
 
 (** {2 Sets and maps of types} *)
+module StructTypSet = Set.Make(struct
+    type t = struct_typ
+    let compare = struct_typ_compare
+  end)
+
 module TypSet = Set.Make(struct
     type t = typ
     let compare = typ_compare

infer/src/IR/sil.mli

@@ -355,7 +355,11 @@ and exp =
   (** A sizeof expression *)
   | Sizeof of typ * Subtype.t
 
+val struct_typ_equal : struct_typ -> struct_typ -> bool
+
 (** Sets of types. *)
+module StructTypSet : Set.S with type elt = struct_typ
+
 module TypSet : Set.S with type elt = typ
 
 (** Maps with type keys. *)

infer/src/backend/interproc.ml

@@ -612,13 +612,14 @@ let report_context_leaks pname sigma tenv =
       Prop.compute_reachable_hpreds sigma fld_exps in
     (* raise an error if any Context expression is in [reachable_exps] *)
     IList.iter
-      (fun (context_exp, typ) ->
+      (fun (context_exp, struct_typ) ->
          if Sil.ExpSet.mem context_exp reachable_exps then
            let leak_path =
              match Prop.get_fld_typ_path_opt fld_exps context_exp reachable_hpreds with
              | Some path -> path
              | None -> assert false in (* a path must exist in order for a leak to be reported *)
-           let err_desc = Errdesc.explain_context_leak pname typ fld_name leak_path in
+           let err_desc =
+             Errdesc.explain_context_leak pname (Sil.Tstruct struct_typ) fld_name leak_path in
            let exn = Exceptions.Context_leak (err_desc, __POS__) in
            Reporting.log_error pname exn)
       context_exps in
@@ -626,10 +627,10 @@ let report_context_leaks pname sigma tenv =
   let context_exps =
     IList.fold_left
       (fun exps hpred -> match hpred with
-         | Sil.Hpointsto (_, Sil.Eexp (exp, _), Sil.Sizeof (Sil.Tptr (typ, _), _))
-           when AndroidFramework.is_context typ tenv
-             && not (AndroidFramework.is_application typ tenv) ->
-             (exp, typ) :: exps
+         | Sil.Hpointsto (_, Eexp (exp, _), Sizeof (Tptr (Tstruct struct_typ, _), _))
+           when AndroidFramework.is_context tenv struct_typ &&
+                not (AndroidFramework.is_application tenv struct_typ) ->
+             (exp, struct_typ) :: exps
          | _ -> exps)
       []
       sigma in
@@ -1067,7 +1068,7 @@ let exception_preconditions tenv pname summary =
   let collect_exceptions pre exns (prop, _) =
     if Tabulation.prop_is_exn pname prop then
       let exn_name = Tabulation.prop_get_exn_name pname prop in
-      if AndroidFramework.is_runtime_exception tenv exn_name then
+      if PatternMatch.is_runtime_exception tenv exn_name then
         (pre, exn_name):: exns
       else exns
     else exns in

infer/src/checkers/annotationReachability.ml

@@ -113,7 +113,7 @@ let is_modeled_expensive =
         not (Builtin.is_registered proc_name) &&
         let classname =
           Typename.Java.from_string (Procname.java_get_class_name proc_name_java) in
-        (Lazy.force matcher) (AndroidFramework.is_subclass tenv classname) proc_name
+        (Lazy.force matcher) (PatternMatch.is_subtype_of_str tenv classname) proc_name
     | _ ->
         false
 
@@ -196,7 +196,7 @@ let is_allocator tenv pname = match pname with
       let is_throwable () =
         let class_name =
           Typename.Java.from_string (Procname.java_get_class_name pname_java) in
-        AndroidFramework.is_throwable tenv class_name in
+        PatternMatch.is_throwable tenv class_name in
       Procname.is_constructor pname
       && not (Builtin.is_registered pname)
       && not (is_throwable ())

infer/src/checkers/checkers.ml

@@ -203,7 +203,10 @@ let callback_check_write_to_parcel_java
     let type_match () =
       let class_name =
         Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "android.os.Parcelable") in
-      PatternMatch.is_direct_subtype_of this_type class_name in
+      match this_type with
+      | Sil.Tptr (Sil.Tstruct struct_typ, _) | Sil.Tstruct struct_typ ->
+          PatternMatch.is_immediate_subtype struct_typ class_name
+      | _ -> false in
     method_match () && expr_match () && type_match () in
 
   let is_parcel_constructor proc_name =

infer/src/checkers/fragmentRetainsViewChecker.ml

@@ -30,7 +30,7 @@ let callback_fragment_retains_view_java
     | Sil.Tptr (Sil.Tvar tname, _) ->
         begin
           match Tenv.lookup tenv tname with
-          | Some struct_typ -> AndroidFramework.is_view (Sil.Tstruct struct_typ) tenv
+          | Some struct_typ -> AndroidFramework.is_view tenv struct_typ
           | None -> false
         end
     | _ -> false in
@@ -44,7 +44,7 @@ let callback_fragment_retains_view_java
         Typename.Java.from_string (Procname.java_get_class_name pname_java) in
       match Tenv.lookup tenv class_typename with
       | Some ({ Sil.struct_name = Some _; instance_fields } as struct_typ)
-        when AndroidFramework.is_fragment (Sil.Tstruct struct_typ) tenv ->
+        when AndroidFramework.is_fragment tenv struct_typ ->
           let declared_view_fields =
             IList.filter (is_declared_view_typ class_typename) instance_fields in
           let fields_nullified = PatternMatch.get_fields_nullified proc_desc in

infer/src/checkers/patternMatch.ml

@@ -36,10 +36,36 @@ let java_proc_name_with_class_method pn_java class_with_path method_name =
      Procname.java_get_method pn_java = method_name
    with _ -> false)
 
-let is_direct_subtype_of this_type super_type_name =
-  match this_type with
-  | Sil.Tptr (Sil.Tstruct { Sil.superclasses }, _) ->
-      IList.exists (fun cn -> Typename.equal cn super_type_name) superclasses
+(** get the superclasses of [typ]. does not include [typ] itself *)
+let get_strict_supertypes tenv orig_struct_typ =
+  let get_direct_supers = function
+    | { Sil.csu = Csu.Class _; superclasses } -> superclasses
+    | _ -> [] in
+  let rec add_typ class_name struct_typs =
+    match Tenv.lookup tenv class_name with
+    | Some struct_typ -> get_supers_rec struct_typ (Sil.StructTypSet.add struct_typ struct_typs)
+    | None -> struct_typs
+  and get_supers_rec struct_typ all_supers =
+    let direct_supers = get_direct_supers struct_typ in
+    IList.fold_left
+      (fun struct_typs class_name -> add_typ class_name struct_typs)
+      all_supers
+      direct_supers in
+  get_supers_rec orig_struct_typ Sil.StructTypSet.empty
+
+let is_immediate_subtype this_type super_type_name =
+  IList.exists (fun cn -> Typename.equal cn super_type_name) this_type.Sil.superclasses
+
+(** return true if [typ0] <: [typ1] *)
+let is_subtype tenv struct_typ0 struct_typ1 =
+  Sil.struct_typ_equal struct_typ0 struct_typ1 ||
+  Sil.StructTypSet.mem struct_typ1 (get_strict_supertypes tenv struct_typ0)
+
+let is_subtype_of_str tenv cn1 classname_str =
+  let typename = Typename.Java.from_string classname_str in
+  let lookup = Tenv.lookup tenv in
+  match lookup cn1, lookup typename with
+  | Some struct_typ1, Some struct_typ2 -> is_subtype tenv struct_typ1 struct_typ2
   | _ -> false
 
 (** The type the method is invoked on *)
@@ -48,10 +74,11 @@ let get_this_type proc_attributes = match proc_attributes.ProcAttributes.formals
   | _ -> None
 
 let type_get_direct_supertypes = function
-  | Sil.Tptr (Sil.Tstruct { Sil.superclasses }, _)
-  | Sil.Tstruct { Sil.superclasses } ->
+  | Sil.Tptr (Tstruct { superclasses }, _)
+  | Sil.Tstruct { superclasses } ->
       superclasses
-  | _ -> []
+  | _ ->
+      []
 
 let type_get_class_name t = match t with
   | Sil.Tptr (Sil.Tstruct { Sil.struct_name = Some cn }, _) ->
@@ -363,3 +390,15 @@ let get_fields_nullified procdesc =
     Cfg.Procdesc.fold_instrs
       collect_nullified_flds (Ident.FieldSet.empty, Ident.IdentSet.empty) procdesc in
   nullified_flds
+
+(** Checks if the exception is an unchecked exception *)
+let is_runtime_exception tenv typename =
+  is_subtype_of_str tenv typename "java.lang.RuntimeException"
+
+(** Checks if the class name is a Java exception *)
+let is_exception tenv typename =
+  is_subtype_of_str tenv typename "java.lang.Exception"
+
+(** Checks if the class name is a Java exception *)
+let is_throwable tenv typename =
+  is_subtype_of_str tenv typename "java.lang.Throwable"

infer/src/checkers/patternMatch.mli

@@ -49,8 +49,17 @@ val is_getter : Procname.java -> bool
 (** Is this a setter proc name? *)
 val is_setter : Procname.java -> bool
 
-(** Is the type a direct subtype of *)
-val is_direct_subtype_of : Sil.typ -> Typename.t -> bool
+(** Is the type a direct subtype of the typename? *)
+val is_immediate_subtype : Sil.struct_typ -> Typename.t -> bool
+
+(** Is the type a transitive subtype of the typename? *)
+val is_subtype : Tenv.t -> Sil.struct_typ -> Sil.struct_typ -> bool
+
+(** Resolve [typ_str] in [tenv], then check [typ] <: [typ_str] *)
+val is_subtype_of_str : Tenv.t -> Typename.t -> string -> bool
+
+(** get the superclasses of [typ]. does not include [typ] itself *)
+val get_strict_supertypes : Tenv.t -> Sil.struct_typ -> Sil.StructTypSet.t
 
 (** Get the name of the type of a constant *)
 val java_get_const_type_name : Sil.const -> string
@@ -95,3 +104,13 @@ val type_is_object : Sil.typ -> bool
 
 (** return the set of instance fields that are assigned to a null literal in [procdesc] *)
 val get_fields_nullified : Cfg.Procdesc.t -> Ident.FieldSet.t
+
+(** [is_exception tenv class_name] checks if class_name is of type java.lang.Exception *)
+val is_exception : Tenv.t -> Typename.t -> bool
+
+(** [is_throwable tenv class_name] checks if class_name is of type java.lang.Throwable *)
+val is_throwable : Tenv.t -> Typename.t -> bool
+
+(** [is_runtime_exception tenv class_name] checks if classname is
+    of type java.lang.RuntimeException *)
+val is_runtime_exception : Tenv.t -> Typename.t -> bool

infer/src/harness/androidFramework.ml

@@ -11,7 +11,7 @@ open! Utils
 
 module L = Logging
 module F = Format
-module TypSet = Sil.TypSet
+module TypSet = Sil.StructTypSet
 
 (** Android lifecycle types and their lifecycle methods that are called by the framework *)
 
@@ -56,56 +56,31 @@ let android_lifecycles =
      fragment_lifecycle);
   ]
 
-(** return the complete set of superclasses of [typ *)
-(* TODO (t4644852): factor out subtyping functions into some sort of JavaUtil module *)
-let get_all_supertypes typ tenv =
-  let get_direct_supers = function
-    | Sil.Tstruct { Sil.csu = Csu.Class _; superclasses } ->
-        superclasses
-    | _ -> [] in
-  let rec add_typ class_name typs =
-    match Tenv.lookup tenv class_name with
-    | Some struct_typ ->
-        let typ' = Sil.Tstruct struct_typ in
-        get_supers_rec typ' (TypSet.add typ' typs)
-    | None -> typs
-  and get_supers_rec typ all_supers =
-    let direct_supers = get_direct_supers typ in
-    IList.fold_left
-      (fun typs class_name -> add_typ class_name typs)
-      all_supers direct_supers in
-  get_supers_rec typ (TypSet.add typ TypSet.empty)
-
-(** return true if [typ0] <: [typ1] *)
-let is_subtype (typ0 : Sil.typ) (typ1 : Sil.typ) tenv =
-  TypSet.mem typ1 (get_all_supertypes typ0 tenv)
-
-let is_subtype_package_class typ package classname tenv =
+let is_subtype_package_class tenv struct_typ package classname =
   let classname = Mangled.from_package_class package classname in
   match Tenv.lookup tenv (Typename.TN_csu (Csu.Class Csu.Java, classname)) with
-  | Some found_struct_typ -> is_subtype typ (Sil.Tstruct found_struct_typ) tenv
+  | Some found_struct_typ -> PatternMatch.is_subtype tenv struct_typ found_struct_typ
   | _ -> false
 
-let is_context typ tenv =
-  is_subtype_package_class typ "android.content" "Context" tenv
+let is_context tenv typ =
+  is_subtype_package_class tenv typ "android.content" "Context"
 
-let is_application typ tenv =
-  is_subtype_package_class typ "android.app" "Application" tenv
+let is_application tenv typ =
+  is_subtype_package_class tenv typ "android.app" "Application"
 
-let is_activity typ tenv =
-  is_subtype_package_class typ "android.app" "Activity" tenv
+let is_activity tenv typ =
+  is_subtype_package_class tenv typ "android.app" "Activity"
 
-let is_view typ tenv =
-  is_subtype_package_class typ "android.view" "View" tenv
+let is_view tenv typ =
+  is_subtype_package_class tenv typ "android.view" "View"
 
-let is_fragment typ tenv =
-  is_subtype_package_class typ "android.app" "Fragment" tenv ||
-  is_subtype_package_class typ "android.support.v4.app" "Fragment" tenv
+let is_fragment tenv typ =
+  is_subtype_package_class tenv typ "android.app" "Fragment" ||
+  is_subtype_package_class tenv typ "android.support.v4.app" "Fragment"
 
-(** return true if [typ] is a subclass of [lifecycle_typ] *)
-let typ_is_lifecycle_typ typ lifecycle_typ tenv =
-  let supers = get_all_supertypes typ tenv in
-  TypSet.mem lifecycle_typ supers
+(** return true if [struct_typ] is a subclass of [lifecycle_struct_typ] *)
+let typ_is_lifecycle_typ tenv struct_typ lifecycle_struct_typ =
+  TypSet.mem lifecycle_struct_typ (PatternMatch.get_strict_supertypes tenv struct_typ)
 
 (** return true if [class_name] is the name of a class that belong to the Android framework *)
 let is_android_lib_class class_name =
@@ -114,7 +89,7 @@ let is_android_lib_class class_name =
 
 (** given an Android framework type mangled string [lifecycle_typ] (e.g., android.app.Activity) and
     a list of method names [lifecycle_procs_strs], get the appropriate typ and procnames *)
-let get_lifecycle_for_framework_typ_opt lifecycle_typ lifecycle_proc_strs tenv =
+let get_lifecycle_for_framework_typ_opt tenv lifecycle_typ lifecycle_proc_strs =
   match Tenv.lookup tenv (Typename.TN_csu (Csu.Class Csu.Java, lifecycle_typ)) with
   | Some ({ Sil.csu = Csu.Class _; struct_name = Some _; def_methods } as lifecycle_typ) ->
       (* TODO (t4645631): collect the procedures for which is_java is returning false *)
@@ -132,38 +107,12 @@ let get_lifecycle_for_framework_typ_opt lifecycle_typ lifecycle_proc_strs tenv =
             try (lookup_proc lifecycle_proc_str) :: lifecycle_procs
             with Not_found -> lifecycle_procs)
           [] lifecycle_proc_strs in
-      Some (Sil.Tstruct lifecycle_typ, lifecycle_procs)
+      Some (lifecycle_typ, lifecycle_procs)
   | _ -> None
 
 (** return the complete list of (package, lifecycle_classname, lifecycle_methods) trios *)
 let get_lifecycles = android_lifecycles
 
-
-let is_subclass tenv cn1 classname_str =
-  let typename =
-    Typename.Java.from_string classname_str in
-  let lookup = Tenv.lookup tenv in
-  match lookup cn1, lookup typename with
-  | Some typ1, Some typ2 ->
-      is_subtype (Sil.Tstruct typ1) (Sil.Tstruct typ2) tenv
-  | _ -> false
-
-
-(** Checks if the exception is an uncheched exception *)
-let is_runtime_exception tenv typename =
-  is_subclass tenv typename "java.lang.RuntimeException"
-
-
-(** Checks if the class name is a Java exception *)
-let is_exception tenv typename =
-  is_subclass tenv typename "java.lang.Exception"
-
-
-(** Checks if the class name is a Java exception *)
-let is_throwable tenv typename =
-  is_subclass tenv typename "java.lang.Throwable"
-
-
 let non_stub_android_jar () =
   let root_dir = Filename.dirname (Filename.dirname Sys.executable_name) in
   IList.fold_left Filename.concat root_dir ["lib"; "java"; "android"; "android-19.jar"]

infer/src/harness/androidFramework.mli

@@ -15,21 +15,21 @@ open! Utils
 val get_lifecycles : (string * string * string list) list
 
 (** return true if [typ] is a subclass of [lifecycle_typ] *)
-val typ_is_lifecycle_typ : Sil.typ -> Sil.typ -> Tenv.t -> bool
+val typ_is_lifecycle_typ : Tenv.t -> Sil.struct_typ -> Sil.struct_typ -> bool
 
 (** return true if [typ] <: android.content.Context *)
-val is_context : Sil.typ -> Tenv.t -> bool
+val is_context : Tenv.t -> Sil.struct_typ -> bool
 
-(** return true if [typ] <: android.app.Application *)
-val is_application : Sil.typ -> Tenv.t -> bool
+(** return true if [struct_typ] <: android.app.Application *)
+val is_application : Tenv.t -> Sil.struct_typ -> bool
 
-(** return true if [typ] <: android.app.Activity *)
-val is_activity : Sil.typ -> Tenv.t -> bool
+(** return true if [struct_typ] <: android.app.Activity *)
+val is_activity : Tenv.t -> Sil.struct_typ -> bool
 
-(** return true if [typ] <: android.view.View *)
-val is_view : Sil.typ -> Tenv.t -> bool
+(** return true if [struct_typ] <: android.view.View *)
+val is_view : Tenv.t -> Sil.struct_typ -> bool
 
-val is_fragment : Sil.typ -> Tenv.t -> bool
+val is_fragment : Tenv.t -> Sil.struct_typ -> bool
 
 (** return true if [procname] is a special lifecycle cleanup method *)
 val is_destroy_method : Procname.t -> bool
@@ -37,22 +37,10 @@ val is_destroy_method : Procname.t -> bool
 (** given an Android framework type mangled string [lifecycle_typ] (e.g., android.app.Activity)
     and a list of method names [lifecycle_procs_strs], get the appropriate typ and procnames *)
 val get_lifecycle_for_framework_typ_opt :
-  Mangled.t -> string list -> Tenv.t -> (Sil.typ * Procname.t list) option
+  Tenv.t -> Mangled.t -> string list -> (Sil.struct_typ * Procname.t list) option
 
 (** return true if [class_name] is the name of a class that belong to the Android framework *)
 val is_android_lib_class : Typename.t -> bool
 
 (** Path to the android.jar file containing real code, not just the method stubs as in the SDK *)
 val non_stub_android_jar : unit -> string
-
-val is_subclass : Tenv.t -> Typename.t -> string -> bool
-
-(** [is_exception tenv class_name] checks if class_name is of type java.lang.Exception *)
-val is_exception : Tenv.t -> Typename.t -> bool
-
-(** [is_throwable tenv class_name] checks if class_name is of type java.lang.Throwable *)
-val is_throwable : Tenv.t -> Typename.t -> bool
-
-(** [is_runtime_exception tenv class_name] checks if classname is
-    of type java.lang.RuntimeException *)
-val is_runtime_exception : Tenv.t -> Typename.t -> bool

infer/src/harness/harness.ml

@@ -14,41 +14,45 @@ module F = Format
 
 (** Automatically create a harness method to exercise code under test *)
 
-(** if [typ] is a lifecycle type, generate a list of (method call, receiver) pairs constituting a
-    lifecycle trace *)
-let try_create_lifecycle_trace typ lifecycle_typ lifecycle_procs tenv = match typ with
-  | Sil.Tstruct { Sil.csu = Csu.Class Csu.Java; struct_name = Some name } ->
-      let class_name = Typename.TN_csu (Csu.Class Csu.Java, name) in
-      if AndroidFramework.typ_is_lifecycle_typ typ lifecycle_typ tenv &&
+(** if [struct_typ] is a lifecycle type, generate a list of (method call, receiver) pairs
+    constituting a lifecycle trace *)
+let try_create_lifecycle_trace struct_typ lifecycle_struct_typ lifecycle_procs tenv =
+  match struct_typ with
+  | { Sil.csu = Csu.Class Java; struct_name = Some name } ->
+      let class_name = Typename.TN_csu (Csu.Class Java, name) in
+      if AndroidFramework.typ_is_lifecycle_typ tenv struct_typ lifecycle_struct_typ &&
          not (AndroidFramework.is_android_lib_class class_name) then
-        let ptr_to_typ = Some (Sil.Tptr (typ, Sil.Pk_pointer)) in
+        let ptr_to_struct_typ = Some (Sil.Tptr (Tstruct struct_typ, Pk_pointer)) in
         IList.fold_left
           (fun trace lifecycle_proc ->
              (* given a lifecycle subclass T, resolve the call T.lifecycle_proc() to the procname
               * that will actually be called at runtime *)
              let resolved_proc = SymExec.resolve_method tenv class_name lifecycle_proc in
-             (resolved_proc, ptr_to_typ) :: trace)
-          [] lifecycle_procs
-      else []
+             (resolved_proc, ptr_to_struct_typ) :: trace)
+          []
+          lifecycle_procs
+      else
+        []
   | _ -> []
 
 (** generate a harness for a lifecycle type in an Android application *)
 let create_harness cfg cg tenv =
   IList.iter (fun (pkg, clazz, lifecycle_methods) ->
-      let typ_name = Mangled.from_package_class pkg clazz in
-      match AndroidFramework.get_lifecycle_for_framework_typ_opt typ_name lifecycle_methods tenv with
+      let typname = Mangled.from_package_class pkg clazz in
+      match AndroidFramework.get_lifecycle_for_framework_typ_opt tenv typname lifecycle_methods with
       | Some (framework_typ, framework_procs) ->
           (* iterate through the type environment and generate a lifecycle harness for each
              subclass of [lifecycle_typ] *)
           (* TODO: instead of iterating through the type environment, interate through the types
              declared in [cfg] *)
           Tenv.iter (fun _ struct_typ ->
-              let typ = Sil.Tstruct struct_typ in
-              match try_create_lifecycle_trace typ framework_typ framework_procs tenv with
+              match try_create_lifecycle_trace struct_typ framework_typ framework_procs tenv with
               | [] -> ()
               | lifecycle_trace ->
                   let harness_procname =
-                    let harness_cls_name = PatternMatch.get_type_name typ in
+                    let harness_cls_name = match struct_typ.Sil.struct_name with
+                      | Some name -> Mangled.to_string name
+                      | None -> "NONE" in
                     let pname =
                       Procname.Java
                         (Procname.java