Use Typename.t for the type of the supertypes in the defintion of classes.

Summary:
public
Using Typename.t in the list of superclasses to match the type for the key of the type environment. This avoids to make back and forth convertions from typename to type (csu, mangled name).

Depends on D2786574

Reviewed By: jberdine

Differential Revision: D2792116

fb-gh-sync-id: 6100f1a

infer/src/backend/exceptions.ml

@@ -55,7 +55,7 @@ exception Frontend_warning of string * Localise.error_desc * ml_location
 exception Checkers of string * Localise.error_desc
 exception Inherently_dangerous_function of Localise.error_desc
 exception Internal_error of Localise.error_desc
-exception Java_runtime_exception of Mangled.t * string * Localise.error_desc
+exception Java_runtime_exception of Typename.t * string * Localise.error_desc
 exception Leak of bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc) * bool * Sil.resource * ml_location
 exception Missing_fld of Ident.fieldname * ml_location
 exception Premature_nil_termination of Localise.error_desc * ml_location
@@ -159,7 +159,7 @@ let recognize_exception exn =
         let desc = Localise.verbatim_desc s in
         (Localise.from_string "Invalid_argument", desc, None, Exn_system, Low, None, Nocat)
     | Java_runtime_exception (exn_name, pre_str, desc) ->
-        let exn_str = Mangled.to_string exn_name in
+        let exn_str = Typename.name exn_name in
         (Localise.from_string exn_str, desc, None, Exn_user, High, None, Prover)
     | Leak (fp_part, _, _, (exn_vis, error_desc), done_array_abstraction, resource, mloc) ->
         if done_array_abstraction

infer/src/backend/exceptions.mli

@@ -55,7 +55,7 @@ exception Checkers of string * Localise.error_desc
 exception Frontend_warning of string * Localise.error_desc * ml_location
 exception Inherently_dangerous_function of Localise.error_desc
 exception Internal_error of Localise.error_desc
-exception Java_runtime_exception of Mangled.t * string * Localise.error_desc
+exception Java_runtime_exception of Typename.t * string * Localise.error_desc
 exception Leak of bool * Prop.normal Prop.t * Sil.hpred * (exception_visibility * Localise.error_desc) * bool * Sil.resource * ml_location
 exception Missing_fld of Ident.fieldname * ml_location
 exception Premature_nil_termination of Localise.error_desc * ml_location

infer/src/backend/localise.ml

@@ -361,7 +361,7 @@ let deref_str_uninitialized alloc_att_opt =
 (** Java unchecked exceptions errors *)
 let java_unchecked_exn_desc proc_name exn_name pre_str : error_desc =
   ([Procname.to_string proc_name;
-    "can throw "^(Mangled.to_string exn_name);
+    "can throw "^(Typename.name exn_name);
     "whenever "^pre_str], None, [])
 
 let desc_context_leak pname context_typ fieldname leak_path : error_desc =

infer/src/backend/localise.mli

@@ -195,7 +195,7 @@ val desc_leak :
 
 val desc_null_test_after_dereference : string -> int -> Location.t -> error_desc
 
-val java_unchecked_exn_desc : Procname.t -> Mangled.t -> string -> error_desc
+val java_unchecked_exn_desc : Procname.t -> Typename.t -> string -> error_desc
 
 val desc_context_leak :
   Procname.t -> Sil.typ -> Ident.fieldname -> (Ident.fieldname option * Sil.typ) list -> error_desc

infer/src/backend/paths.ml

@@ -47,7 +47,7 @@ module Path : sig
   val equal : t -> t -> bool
 
   (** extend a path with a new node reached from the given session, with an optional string for exceptions *)
-  val extend : Cfg.node -> Mangled.t option -> session -> t -> t
+  val extend : Cfg.node -> Typename.t option -> session -> t -> t
 
   (** extend a path with a new node reached from the given session, with an optional string for exceptions *)
   val add_description : t -> string -> t
@@ -60,7 +60,8 @@ module Path : sig
   (** iterate over the longest sequence belonging to the path, restricting to those containing the given position if given.
       Do not iterate past the given position.
       [f level path session exn_opt] is passed the current nesting [level] and [path] and previous [session] *)
-  val iter_longest_sequence : (int -> t -> int -> Mangled.t option -> unit) -> Sil.path_pos option -> t -> unit
+  val iter_longest_sequence :
+    (int -> t -> int -> Typename.t option -> unit) -> Sil.path_pos option -> t -> unit
 
   (** join two paths *)
   val join : t -> t -> t
@@ -83,7 +84,9 @@ end = struct
     (* INVARIANT: stats are always set to dummy_stats unless we are in the middle of a traversal *)
     (* in particular: a new traversal cannot be initiated during an existing traversal *)
     | Pstart of Cfg.node * stats (** start node *)
-    | Pnode of Cfg.node * Mangled.t option * session * path * stats * string option (** we got to [node] from last [session] perhaps propagating exception [exn_opt], and continue with [path].  *)
+    | Pnode of Cfg.node * Typename.t option * session * path * stats * string option
+    (** we got to [node] from last [session] perhaps propagating exception [exn_opt],
+        and continue with [path].  *)
     | Pjoin of path * path * stats (** join of two paths *)
     | Pcall of path * Procname.t * path * stats (** add a sub-path originating from a call *)
 
@@ -125,7 +128,7 @@ end = struct
     | None, None -> 0
     | None, _ -> -1
     | _, None -> 1
-    | Some n1, Some n2 -> Mangled.compare n1 n2
+    | Some n1, Some n2 -> Typename.compare n1 n2
 
   let rec compare p1 p2 : int =
     if p1 == p2 then 0 else match p1, p2 with
@@ -281,7 +284,9 @@ end = struct
 
   (** iterate over the longest sequence belonging to the path, restricting to those where [filter] holds of some element.
       if a node is reached via an exception, pass the exception information to [f] on the previous node *)
-  let iter_longest_sequence_filter (f : int -> t -> int -> Mangled.t option -> unit) (filter: Cfg.Node.t -> bool) (path: t) : unit =
+  let iter_longest_sequence_filter
+      (f : int -> t -> int -> Typename.t option -> unit)
+      (filter: Cfg.Node.t -> bool) (path: t) : unit =
     let rec doit level session path prev_exn_opt = match path with
       | Pstart _ -> f level path session prev_exn_opt
       | Pnode (node, exn_opt, session', p, _, _) ->
@@ -301,7 +306,9 @@ end = struct
   (** iterate over the longest sequence belonging to the path, restricting to those containing the given position if given.
       Do not iterate past the last occurrence of the given position.
       [f level path session exn_opt] is passed the current nesting [level] and [path] and previous [session] and possible exception [exn_opt] *)
-  let iter_longest_sequence (f : int -> t -> int -> Mangled.t option -> unit) (pos_opt : Sil.path_pos option) (path: t) : unit =
+  let iter_longest_sequence
+      (f : int -> t -> int -> Typename.t option -> unit)
+      (pos_opt : Sil.path_pos option) (path: t) : unit =
     let filter node = match pos_opt with
       | None -> true
       | Some pos -> Sil.path_pos_equal (get_path_pos node) pos in
@@ -478,7 +485,7 @@ end = struct
                   match exn_opt with
                   | None -> "", []
                   | Some exn_name ->
-                      let exn_str = Mangled.to_string exn_name in
+                      let exn_str = Typename.name exn_name in
                       if exn_str = ""
                       then "exception", [(Io_infer.Xml.tag_kind,"exception")]
                       else

infer/src/backend/paths.mli

@@ -40,7 +40,7 @@ module Path : sig
   val d_stats : t -> unit
 
   (** extend a path with a new node reached from the given session, with an optional string for exceptions *)
-  val extend : Cfg.node -> Mangled.t option -> session -> t -> t
+  val extend : Cfg.node -> Typename.t option -> session -> t -> t
 
   val add_description : t -> string -> t
 
@@ -50,7 +50,8 @@ module Path : sig
   (** iterate over the longest sequence belonging to the path, restricting to those containing the given position if given.
       Do not iterate past the given position.
       [f level path session exn_opt] is passed the current nesting [level] and [path] and previous [session] and possible exception [exn_opt] *)
-  val iter_longest_sequence : (int -> t -> int -> Mangled.t option -> unit) -> Sil.path_pos option -> t -> unit
+  val iter_longest_sequence :
+    (int -> t -> int -> Typename.t option -> unit) -> Sil.path_pos option -> t -> unit
 
   (** join two paths *)
   val join : t -> t -> t

infer/src/backend/prover.ml

@@ -1440,27 +1440,27 @@ let expand_hpred_pointer calc_index_frame hpred : bool * bool * Sil.hpred =
     | _ -> changed, calc_index_frame, hpred in
   expand false calc_index_frame hpred
 
-let object_type = Mangled.from_string "java.lang.Object"
+let object_type = Typename.Java.from_string "java.lang.Object"
 
-let serializable_type = Mangled.from_string "java.io.Serializable"
+let serializable_type = Typename.Java.from_string "java.io.Serializable"
 
-let cloneable_type = Mangled.from_string "java.lang.Cloneable"
+let cloneable_type = Typename.Java.from_string "java.lang.Cloneable"
 
-let is_interface tenv c =
-  match Sil.tenv_lookup tenv (Typename.TN_csu (Csu.Class, c)) with
+let is_interface tenv class_name =
+  match Sil.tenv_lookup tenv class_name with
   | Some (Sil.Tstruct (fields, sfields, Csu.Class, Some c1', supers1, methods, iann)) ->
       (IList.length fields = 0) && (IList.length methods = 0)
   | _ -> false
 
 (** check if c1 is a subclass of c2 *)
 let check_subclass_tenv tenv c1 c2 =
-  let rec check (_, c) =
-    Mangled.equal c c2 || (Mangled.equal c2 object_type) ||
-    match Sil.tenv_lookup tenv (Typename.TN_csu (Csu.Class, c)) with
+  let rec check cn =
+    Typename.equal cn c2 || Typename.equal c2 object_type ||
+    match Sil.tenv_lookup tenv cn with
     | Some (Sil.Tstruct (_, _, Csu.Class, Some c1', supers1, _, _)) ->
         IList.exists check supers1
     | _ -> false in
-  (check (Csu.Class, c1))
+  check c1
 
 let check_subclass tenv c1 c2 =
   let f = check_subclass_tenv tenv in
@@ -1480,7 +1480,9 @@ let rec check_subtype tenv t1 t2 =
   match t1, t2 with
   | Sil.Tstruct (_, _, Csu.Class, Some c1, _, _, _),
     Sil.Tstruct (_, _, Csu.Class, Some c2, _, _, _) ->
-      (check_subclass tenv c1 c2)
+      let cn1 = Typename.TN_csu (Csu.Class, c1)
+      and cn2 = Typename.TN_csu (Csu.Class, c2) in
+      (check_subclass tenv cn1 cn2)
 
   | Sil.Tarray (dom_type1, _), Sil.Tarray (dom_type2, _) ->
       check_subtype tenv dom_type1 dom_type2
@@ -1489,7 +1491,10 @@ let rec check_subtype tenv t1 t2 =
       check_subtype tenv dom_type1 dom_type2
 
   | Sil.Tarray _, Sil.Tstruct (_, _, Csu.Class, Some c2, _, _, _) ->
-      (Mangled.equal c2 serializable_type) || (Mangled.equal c2 cloneable_type) || (Mangled.equal c2 object_type)
+      let cn2 = Typename.TN_csu (Csu.Class, c2) in
+      Typename.equal cn2 serializable_type
+      || Typename.equal cn2 cloneable_type
+      || Typename.equal cn2 object_type
 
   | _ -> (check_subtype_basic_type t1 t2)
 
@@ -1497,7 +1502,9 @@ let rec case_analysis_type tenv (t1, st1) (t2, st2) =
   match t1, t2 with
   | Sil.Tstruct (_, _, Csu.Class, Some c1, _, _, _),
     Sil.Tstruct (_, _, Csu.Class, Some c2, _, _, _) ->
-      (Sil.Subtype.case_analysis (c1, st1) (c2, st2) (check_subclass tenv) (is_interface tenv))
+      let cn1 = Typename.TN_csu (Csu.Class, c1)
+      and cn2 = Typename.TN_csu (Csu.Class, c2) in
+      (Sil.Subtype.case_analysis (cn1, st1) (cn2, st2) (check_subclass tenv) (is_interface tenv))
 
   | Sil.Tarray (dom_type1, _), Sil.Tarray (dom_type2, _) ->
       (case_analysis_type tenv (dom_type1, st1) (dom_type2, st2))
@@ -1506,7 +1513,10 @@ let rec case_analysis_type tenv (t1, st1) (t2, st2) =
       (case_analysis_type tenv (dom_type1, st1) (dom_type2, st2))
 
   | Sil.Tstruct (_, _, Csu.Class, Some c1, _, _, _), Sil.Tarray _ ->
-      if ((Mangled.equal c1 serializable_type) || (Mangled.equal c1 cloneable_type) || (Mangled.equal c1 object_type)) &&
+      let cn1 = Typename.TN_csu (Csu.Class, c1) in
+      if (Typename.equal cn1 serializable_type
+          || Typename.equal cn1 cloneable_type
+          || Typename.equal cn1 object_type) &&
          (st1 <> Sil.Subtype.exact) then (Some st1, None)
       else (None, Some st1)
 

infer/src/backend/sil.ml

@@ -202,14 +202,15 @@ module Subtype = struct
       | [] -> ""
       | el:: rest ->
           let s = (aux rest) in
-          if (s = "") then (Mangled.to_string el)
-          else (Mangled.to_string el)^", "^s in
+          if (s = "") then (Typename.name el)
+          else (Typename.name el)^", "^s in
     if (IList.length list = 0) then "( sub )"
     else ("- {"^(aux list)^"}")
 
   type t' =
     | Exact (** denotes the current type only *)
-    | Subtypes of Mangled.t list(** denotes the current type and a list of types that are not their subtypes  *)
+    | Subtypes of Typename.t list
+    (** denotes the current type and a list of types that are not their subtypes  *)
 
   type kind =
     | CAST
@@ -219,10 +220,10 @@ module Subtype = struct
   type t = t' * kind
 
   module SubtypesPair = struct
-    type t = (Mangled.t * Mangled.t)
+    type t = (Typename.t * Typename.t)
 
     let compare (e1 : t)(e2 : t) : int =
-      pair_compare Mangled.compare Mangled.compare e1 e2
+      pair_compare Typename.compare Typename.compare e1 e2
   end
 
   module SubtypesMap = Map.Make (SubtypesPair)
@@ -246,9 +247,12 @@ module Subtype = struct
     | NORMAL -> ""
 
   let pp f (t, flag) =
-    match t with
-    | Exact -> if !Config.print_types then F.fprintf f "%s" (flag_to_string flag)
-    | Subtypes list -> if !Config.print_types then F.fprintf f "%s" ((list_to_string list)^(flag_to_string flag))
+    if !Config.print_types then
+      match t with
+      | Exact ->
+          F.fprintf f "%s" (flag_to_string flag)
+      | Subtypes list ->
+          F.fprintf f "%s" ((list_to_string list)^(flag_to_string flag))
 
   let exact = Exact, NORMAL
   let all_subtypes = Subtypes []
@@ -275,12 +279,12 @@ module Subtype = struct
       match s1, s2 with
       | Exact, _ -> s2
       | _, Exact -> s1
-      | Subtypes l1, Subtypes l2 -> Subtypes (list_intersect Mangled.equal l1 l2) in
+      | Subtypes l1, Subtypes l2 -> Subtypes (list_intersect Typename.equal l1 l2) in
     let flag = join_flag flag1 flag2 in
     s, flag
 
   let subtypes_compare l1 l2 =
-    IList.compare Mangled.compare l1 l2
+    IList.compare Typename.compare l1 l2
 
   let compare_flag flag1 flag2 =
     match flag1, flag2 with
@@ -309,7 +313,7 @@ module Subtype = struct
   let update_flag c1 c2 flag flag' =
     match flag with
     | INSTOF ->
-        if (Mangled.equal c1 c2) then flag else flag'
+        if (Typename.equal c1 c2) then flag else flag'
     | _ -> flag'
 
   let change_flag st_opt c1 c2 flag' =
@@ -331,7 +335,7 @@ module Subtype = struct
         (match t with
          | Exact -> Some (t, new_flag)
          | Subtypes l ->
-             Some (Subtypes (IList.sort Mangled.compare l), new_flag))
+             Some (Subtypes (IList.sort Typename.compare l), new_flag))
     | None -> None
 
   let subtypes_to_string t =
@@ -345,7 +349,7 @@ module Subtype = struct
     with Not_found -> true
 
   let is_strict_subtype f c1 c2 =
-    f c1 c2 && not (Mangled.equal c1 c2)
+    f 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:
@@ -381,8 +385,6 @@ module Subtype = struct
 
   let get_subtypes (c1, (st1, flag1)) (c2, (st2, flag2)) f is_interface =
     let is_sub = f c1 c2 in
-    (* L.d_strln_color Orange ((Mangled.to_string c1)^(subtypes_to_string (st1, flag1))^" <: "^ *)
-    (* (Mangled.to_string c2)^(subtypes_to_string (st2, flag2))^" ?"^(string_of_bool is_sub)); *)
     let pos_st, neg_st = match st1, st2 with
       | Exact, Exact ->
           if (is_sub) then (Some st1, None)
@@ -414,11 +416,11 @@ module Subtype = struct
       else if f c2 c1 then
         match st with
         | Exact, flag ->
-            if Mangled.equal c1 c2
+            if Typename.equal c1 c2
             then (Some st, None)
             else (None, Some st)
         | Subtypes _ , flag ->
-            if Mangled.equal c1 c2
+            if Typename.equal c1 c2
             then (Some st, None)
             else (Some st, Some st)
       else (None, Some st) in
@@ -651,7 +653,7 @@ and typ =
   | Tfun of bool (** function type with noreturn attribute *)
   | Tptr of typ * ptr_kind (** pointer type *)
   | Tstruct of struct_fields * struct_fields * Csu.t * Mangled.t option *
-               (Csu.t * Mangled.t) list * Procname.t list * item_annotation
+               Typename.t list * Procname.t list * item_annotation
   (** Structure type with nonstatic and static fields, class/struct/union flag, name,
       list of superclasses, methods defined, and annotations.
       The fld - typ pairs are always sorted. This means that we don't support programs that exploit specific layouts

infer/src/backend/sil.mli

@@ -140,13 +140,15 @@ module Subtype : sig
   val subtypes_cast : t
   val subtypes_instof : t
   val join : t -> t -> t
-  (** [case_analysis (c1, st1) (c2,st2) f] performs case analysis on [c1 <: c2] according to [st1] and [st2]
-      where f c1 c2 is true if c1 is a subtype of c2.
+  (** [case_analysis (c1, st1) (c2,st2) f] performs case analysis on [c1 <: c2] according
+      to [st1] and [st2] where f c1 c2 is true if c1 is a subtype of c2.
       get_subtypes returning a pair:
       - 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] *)
-  val case_analysis : (Mangled.t * t) -> (Mangled.t * t) -> (Mangled.t -> Mangled.t -> bool) -> (Mangled.t -> bool) -> t option * t option
-  val check_subtype : (Mangled.t -> Mangled.t -> bool) -> Mangled.t -> Mangled.t -> bool
+      - whether [st1] and [st2] admit [not(c1 <: c2)], and in case return
+      the updated subtype [st1] *)
+  val case_analysis : (Typename.t * t) -> (Typename.t * t) ->
+    (Typename.t -> Typename.t -> bool) -> (Typename.t -> bool) -> t option * t option
+  val check_subtype : (Typename.t -> Typename.t -> bool) -> Typename.t -> Typename.t -> bool
   val subtypes_to_string : t -> string
   val is_cast : t -> bool
   val is_instof : t -> bool
@@ -286,7 +288,7 @@ and typ =
   | Tfun of bool (** function type with noreturn attribute *)
   | Tptr of typ * ptr_kind (** pointer type *)
   | Tstruct of struct_fields * struct_fields * Csu.t * Mangled.t option *
-               (Csu.t * Mangled.t) list * Procname.t list * item_annotation
+               Typename.t list * Procname.t list * item_annotation
   (** Structure type with nonstatic and static fields, class/struct/union flag, name, list of superclasses,
       methods defined, and annotations.
       The fld - typ pairs are always sorted. This means that we don't support programs that exploit specific layouts

infer/src/backend/symExec.ml

@@ -598,23 +598,22 @@ let method_exists right_proc_name methods =
 
 let resolve_method tenv class_name proc_name =
   let found_class =
-    let visited = ref Mangled.MangledSet.empty in
+    let visited = ref Typename.Set.empty in
     let rec resolve class_name =
-      visited := Mangled.MangledSet.add class_name !visited;
+      visited := Typename.Set.add class_name !visited;
       let right_proc_name =
         if Procname.is_java proc_name then
-          Procname.java_replace_class proc_name (Mangled.to_string class_name)
-        else Procname.c_method_replace_class proc_name (Mangled.to_string class_name) in
-      let type_name = Typename.TN_csu (Csu.Class, class_name) in
-      match Sil.tenv_lookup tenv type_name with
+          Procname.java_replace_class proc_name (Typename.name class_name)
+        else Procname.c_method_replace_class proc_name (Typename.name class_name) in
+      match Sil.tenv_lookup tenv class_name with
       | Some (Sil.Tstruct (_, _, Csu.Class, cls, super_classes, methods, iann)) ->
           if method_exists right_proc_name methods then
             Some right_proc_name
           else
             (match super_classes with
-             | (Csu.Class, super_class):: interfaces ->
-                 if not (Mangled.MangledSet.mem super_class !visited)
-                 then resolve super_class
+             | super_classname:: interfaces ->
+                 if not (Typename.Set.mem super_classname !visited)
+                 then resolve super_classname
                  else None
              | _ -> None)
       | _ -> None in
@@ -622,7 +621,7 @@ let resolve_method tenv class_name proc_name =
   match found_class with
   | None ->
       Logging.d_strln
-        ("Couldn't find method in the hierarchy of type "^(Mangled.to_string class_name));
+        ("Couldn't find method in the hierarchy of type "^(Typename.name class_name));
       proc_name
   | Some proc_name -> proc_name
 
@@ -635,8 +634,9 @@ let resolve_typename prop arg =
       | _ :: hpreds -> loop hpreds in
     loop (Prop.get_sigma prop) in
   match typexp_opt with
-  | Some (Sil.Sizeof (Sil.Tstruct (_, _, Csu.Class, class_name_opt, _, _, _), _)) ->
-      class_name_opt
+  | Some (Sil.Sizeof (Sil.Tstruct (_, _, _, None, _, _, _), _)) -> None
+  | Some (Sil.Sizeof (Sil.Tstruct (_, _, Csu.Class, Some name, _, _, _), _)) ->
+      Some (Typename.TN_csu (Csu.Class, name))
   | _ -> None
 
 (** If the dynamic type of the object calling a method is known, the method from the dynamic type
@@ -648,7 +648,7 @@ let resolve_virtual_pname cfg tenv prop args pname : Procname.t =
       begin
         match resolve_typename prop obj_exp with
         | Some class_name -> resolve_method tenv class_name pname
-        | _ -> pname
+        | None -> pname
       end
 
 (* let resolve_procname cfg tenv prop args pname : Procname.t = *)

infer/src/backend/symExec.mli

@@ -24,7 +24,7 @@ val lifted_sym_exec : (exn -> unit) -> Cfg.cfg -> Sil.tenv -> Cfg.Procdesc.t ->
  * the procname that the method name will actually resolve to at runtime. For example, if we have
  * a procname like Foo.toString() and Foo does not override toString(), we must resolve the call to
  * toString(). We will end up with Super.toString() where Super is some superclass of Foo. *)
-val resolve_method : Sil.tenv -> Mangled.t -> Procname.t -> Procname.t
+val resolve_method : Sil.tenv -> Typename.t -> Procname.t -> Procname.t
 (** {2 Functions for handling builtins } *)
 
 module ModelBuiltins : sig

infer/src/backend/tabulation.ml

@@ -594,11 +594,12 @@ let prop_is_exn pname prop =
 (** when prop is an exception, return the exception name *)
 let prop_get_exn_name pname prop =
   let ret_pvar = Sil.Lvar (Sil.get_ret_pvar pname) in
-  let exn_name = ref (Mangled.from_string "") in
+  let exn_name = ref (Typename.Java.from_string "") in
   let find_exn_name e =
     let do_hpred = function
       | Sil.Hpointsto (e1, _, Sil.Sizeof(Sil.Tstruct (_, _, _, Some name, _, _, _), _)) when Sil.exp_equal e1 e ->
-          exn_name := name
+          let found_exn_name = Typename.TN_csu (Csu.Class, name) in
+          exn_name := found_exn_name
       | _ -> () in
     IList.iter do_hpred (Prop.get_sigma prop) in
   let find_ret () =

infer/src/backend/tabulation.mli

@@ -30,7 +30,7 @@ val raise_cast_exception :
 val prop_is_exn : Procname.t -> 'a Prop.t -> bool
 
 (** when prop is an exception, return the exception name *)
-val prop_get_exn_name : Procname.t -> 'a Prop.t -> Mangled.t
+val prop_get_exn_name : Procname.t -> 'a Prop.t -> Typename.t
 
 (** search in prop contains an error state *)
 val lookup_custom_errors : 'a Prop.t -> string option

infer/src/backend/type_prop.ml

@@ -311,8 +311,8 @@ let initial_node = ref (Cfg.Node.dummy ())
 
 let rec super tenv t =
   match t with
-  | Sil.Tstruct (_, _, Csu.Class, Some c2, (Csu.Class, super):: rest, _, _) ->
-      Sil.tenv_lookup tenv (Typename.TN_csu (Csu.Class, super))
+  | Sil.Tstruct (_, _, Csu.Class, Some c2, class_name :: rest, _, _) ->
+      Sil.tenv_lookup tenv class_name
   | Sil.Tarray (dom_type, _) -> None
   | Sil.Tptr (dom_type, p) ->
       let super_dom_type = super tenv dom_type in

infer/src/backend/typename.ml

@@ -7,6 +7,9 @@
  * of patent rights can be found in the PATENTS file in the same directory.
  *)
 
+open Utils
+module F = Format
+
 (** Named types. *)
 type t =
   | TN_typedef of Mangled.t
@@ -19,6 +22,9 @@ let to_string = function
   | TN_csu (csu, name) ->
       Csu.name csu ^ " " ^ Mangled.to_string name
 
+let pp f typename =
+  F.fprintf f "%s" (to_string typename)
+
 let name = function
   | TN_enum name
   | TN_typedef name
@@ -37,3 +43,18 @@ let compare tn1 tn2 = match tn1, tn2 with
 
 let equal tn1 tn2 =
   compare tn1 tn2 = 0
+
+module Java =
+struct
+
+  let from_string class_name_str =
+    TN_csu (Csu.Class, Mangled.from_string class_name_str)
+
+end
+
+type typename_t = t
+module Set = Set.Make(
+  struct
+    type t = typename_t
+    let compare = compare
+  end)

infer/src/backend/typename.mli

@@ -16,6 +16,8 @@ type t =
 (** convert the typename to a string *)
 val to_string : t -> string
 
+val pp : Format.formatter -> t -> unit
+
 (** name of the typename without qualifier *)
 val name : t -> string
 
@@ -24,3 +26,12 @@ val compare : t -> t -> int
 
 (** Equality for typenames *)
 val equal : t -> t -> bool
+
+module Java : sig
+
+  (** Create a typename from a Java classname in the form "package.class" *)
+  val from_string : string -> t
+
+end
+
+module Set : Set.S with type elt = t

infer/src/checkers/checkers.ml

@@ -197,7 +197,9 @@ let callback_check_write_to_parcel all_procs get_proc_desc idenv tenv proc_name
   let is_write_to_parcel this_expr this_type =
     let method_match () = Procname.java_get_method proc_name = "writeToParcel" in
     let expr_match () = Sil.exp_is_this this_expr in
-    let type_match () = PatternMatch.is_direct_subtype_of this_type "android.os.Parcelable" in
+    let type_match () =
+      let class_name = Typename.TN_csu (Csu.Class, Mangled.from_string "android.os.Parcelable") in
+      PatternMatch.is_direct_subtype_of this_type class_name in
     method_match () && expr_match () && type_match () in
 
   let is_parcel_constructor proc_name =

infer/src/checkers/patternMatch.ml

@@ -28,7 +28,7 @@ let java_proc_name_with_class_method pn class_with_path method_name =
 let is_direct_subtype_of this_type super_type_name =
   match this_type with
   | Sil.Tptr (Sil.Tstruct (_, _, _, _, supertypes, _, _), _) ->
-      IList.exists (fun (x, y) -> super_type_name = Mangled.to_string y) supertypes
+      IList.exists (fun cn -> Typename.equal cn super_type_name) supertypes
   | _ -> false
 
 (** The type the method is invoked on *)
@@ -38,8 +38,7 @@ let get_this_type proc_attributes = match proc_attributes.ProcAttributes.formals
 
 let type_get_direct_supertypes = function
   | Sil.Tptr (Sil.Tstruct (_, _, _, _, supertypes, _, _), _)
-  | Sil.Tstruct (_, _, _, _, supertypes, _, _) ->
-      IList.map (fun (_, m) -> m) supertypes
+  | Sil.Tstruct (_, _, _, _, supertypes, _, _) -> supertypes
   | _ -> []
 
 let type_get_class_name t = match t with
@@ -59,13 +58,13 @@ let type_get_annotation
 let type_has_class_name t name =
   type_get_class_name t = Some name
 
-let type_has_direct_supertype (t : Sil.typ) (s : Mangled.t) =
-  IList.exists (fun c -> c = s) (type_get_direct_supertypes t)
+let type_has_direct_supertype (typ : Sil.typ) (class_name : Typename.t) =
+  IList.exists (fun cn -> Typename.equal cn class_name) (type_get_direct_supertypes typ)
 
 let type_has_supertype
     (tenv: Sil.tenv)
     (typ: Sil.typ)
-    (name: Mangled.t): bool =
+    (class_name: Typename.t): bool =
   let rec has_supertype typ visited =
     if Sil.TypSet.mem typ visited then
       false
@@ -74,10 +73,10 @@ let type_has_supertype
         match Sil.expand_type tenv typ with
         | Sil.Tptr (Sil.Tstruct (_, _, _, _, supertypes, _, _), _)
         | Sil.Tstruct (_, _, _, _, supertypes, _, _) ->
-            let match_supertype (csu, m) =
-              let match_name () = Mangled.equal m name in
+            let match_supertype cn =
+              let match_name () = Typename.equal cn class_name in
               let has_indirect_supertype () =
-                match Sil.tenv_lookup tenv (Typename.TN_csu (Csu.Class, m)) with
+                match Sil.tenv_lookup tenv cn with
                 | Some supertype -> has_supertype supertype (Sil.TypSet.add typ visited)
                 | None -> false in
               (match_name () || has_indirect_supertype ()) in
@@ -93,7 +92,7 @@ let type_is_nested_in_type t n = match t with
   | _ -> false
 
 let type_is_nested_in_direct_supertype t n =
-  let is_nested_in m2 m1 = string_is_prefix (Mangled.to_string m2 ^ "$") (Mangled.to_string m1) in
+  let is_nested_in cn1 cn2 = string_is_prefix (Typename.name cn1 ^ "$") (Typename.name cn2) in
   IList.exists (is_nested_in n) (type_get_direct_supertypes t)
 
 let rec get_type_name = function
@@ -224,12 +223,15 @@ let type_is_class = function
   | Sil.Tstruct _ -> true
   | _ -> false
 
-let initializer_classes = IList.map Mangled.from_string [
-    "android.app.Activity";
-    "android.app.Application";
-    "android.app.Fragment";
-    "android.support.v4.app.Fragment";
-  ]
+let initializer_classes =
+  IList.map
+    (fun name -> Typename.TN_csu (Csu.Class, Mangled.from_string name))
+    [
+      "android.app.Activity";
+      "android.app.Application";
+      "android.app.Fragment";
+      "android.support.v4.app.Fragment";
+    ]
 
 let initializer_methods = [
   "onActivityCreated";
@@ -242,7 +244,7 @@ let initializer_methods = [
 let type_has_initializer
     (tenv: Sil.tenv)
     (t: Sil.typ): bool =
-  let check_candidate cname = type_has_supertype tenv t cname in
+  let check_candidate class_name = type_has_supertype tenv t class_name in
   IList.exists check_candidate initializer_classes
 
 (** Check if the method is one of the known initializer methods. *)
@@ -300,9 +302,8 @@ let proc_calls resolve_attributes pname pdesc filter : (Procname.t * ProcAttribu
 let proc_iter_overridden_methods f tenv proc_name =
   let do_super_type tenv super_class_name =
     let super_proc_name =
-      Procname.java_replace_class proc_name (Mangled.to_string super_class_name) in
-    let type_name = Typename.TN_csu (Csu.Class, super_class_name) in
-    match Sil.tenv_lookup tenv type_name with
+      Procname.java_replace_class proc_name (Typename.name super_class_name) in
+    match Sil.tenv_lookup tenv super_class_name with
     | Some (Sil.Tstruct (_, _, _, _, _, methods, _)) ->
         let is_override pname =
           Procname.equal pname super_proc_name &&

infer/src/checkers/patternMatch.mli

@@ -38,7 +38,7 @@ val is_getter : Procname.t -> bool
 val is_setter : Procname.t -> bool
 
 (** Is the type a direct subtype of *)
-val is_direct_subtype_of : Sil.typ -> string -> bool
+val is_direct_subtype_of : Sil.typ -> Typename.t -> bool
 
 (** Get the name of the type of a constant *)
 val java_get_const_type_name : Sil.const -> string
@@ -64,17 +64,17 @@ val type_get_annotation : Sil.typ -> Sil.item_annotation option
 (** Get the class name of the type *)
 val type_get_class_name : Sil.typ -> Mangled.t option
 
-val type_get_direct_supertypes : Sil.typ -> Mangled.t list
+val type_get_direct_supertypes : Sil.typ -> Typename.t list
 
 (** Is the type a class with the given name *)
 val type_has_class_name : Sil.typ -> Mangled.t -> bool
 
-val type_has_direct_supertype : Sil.typ -> Mangled.t -> bool
+val type_has_direct_supertype : Sil.typ -> Typename.t -> bool
 
 (** Is the type a class type *)
 val type_is_class : Sil.typ -> bool
 
-val type_is_nested_in_direct_supertype : Sil.typ -> Mangled.t -> bool
+val type_is_nested_in_direct_supertype : Sil.typ -> Typename.t -> bool
 
 val type_is_nested_in_type : Sil.typ -> Mangled.t -> bool
 

infer/src/clang/cContext.ml

@@ -119,7 +119,7 @@ let create_curr_class tenv class_name =
   let class_tn_name = Typename.TN_csu (Csu.Class, (Mangled.from_string class_name)) in
   match Sil.tenv_lookup tenv class_tn_name with
   | Some Sil.Tstruct(intf_fields, _, _, _, superclasses, methods, annotation) ->
-      (let superclasses_names = IList.map (fun (_, name) -> Mangled.to_string name) superclasses in
+      (let superclasses_names = IList.map Typename.name superclasses in
        match superclasses_names with
        | superclass:: protocols ->
            ContextCls (class_name, Some superclass, protocols)

infer/src/clang/cField_decl.ml

@@ -20,8 +20,8 @@ let rec get_fields_super_classes tenv super_class =
   Printing.log_out "   ... Getting fields of superclass '%s'\n" (Typename.to_string super_class);
   match Sil.tenv_lookup tenv super_class with
   | None -> []
-  | Some Sil.Tstruct (fields, _, _, _, (Csu.Class, sc):: _, _, _) ->
-      let sc_fields = get_fields_super_classes tenv (Typename.TN_csu (Csu.Class, sc)) in
+  | Some Sil.Tstruct (fields, _, _, _, super_class :: _, _, _) ->
+      let sc_fields = get_fields_super_classes tenv super_class in
       General_utils.append_no_duplicates_fields fields sc_fields
   | Some Sil.Tstruct (fields, _, _, _, _, _, _) -> fields
   | Some _ -> []

infer/src/clang/cFrontend_utils.ml

@@ -48,9 +48,8 @@ struct
              | Sil.Tstruct (fields, _, _, cls, super_classes, methods, iann) ->
                  print_endline (
                    (Typename.to_string typname) ^ "\n"^
-                   "---> superclass and protocols " ^ (IList.to_string (fun (csu, x) ->
-                       let nsu = Typename.TN_csu (csu, x) in
-                       "\t" ^ (Typename.to_string nsu) ^ "\n") super_classes) ^
+                   "---> superclass and protocols " ^ (IList.to_string (fun tn ->
+                       "\t" ^ (Typename.to_string tn) ^ "\n") super_classes) ^
                    "---> methods " ^
                    (IList.to_string (fun x ->"\t" ^ (Procname.to_string x) ^ "\n") methods)
                    ^ "  " ^
@@ -430,10 +429,7 @@ struct
     | [] -> list1
 
   let append_no_duplicates_csu list1 list2 =
-    append_no_duplicates
-      (fun (ds1, n1) (ds2, n2) ->
-         Csu.equal ds1 ds2 && Mangled.equal n1 n2)
-      list1 list2
+    append_no_duplicates Typename.equal list1 list2
 
   let append_no_duplicates_methods list1 list2 =
     append_no_duplicates Procname.equal list1 list2

infer/src/clang/cFrontend_utils.mli

@@ -139,7 +139,7 @@ sig
     (Ident.fieldname * Sil.typ * Sil.item_annotation) list -> (Ident.fieldname * Sil.typ * Sil.item_annotation) list
 
   val append_no_duplicates_csu :
-    (Csu.t * Mangled.t) list -> (Csu.t * Mangled.t) list -> (Csu.t * Mangled.t) list
+    Typename.t list -> Typename.t list -> Typename.t list
 
   val append_no_duplicates_methods : Procname.t list -> Procname.t list -> Procname.t list
 

infer/src/clang/cMethod_trans.ml

@@ -191,8 +191,8 @@ let get_superclass_curr_class context =
     let iname = Typename.TN_csu (Csu.Class, Mangled.from_string cname) in
     Printing.log_out "Checking for superclass = '%s'\n\n%!" (Typename.to_string iname);
     match Sil.tenv_lookup (CContext.get_tenv context) iname with
-    | Some Sil.Tstruct(_, _, _, _, (_, super_name):: _, _, _) ->
-        Mangled.to_string super_name
+    | Some Sil.Tstruct(_, _, _, _, super_name :: _, _, _) ->
+        Typename.name super_name
     | _ ->
         Printing.log_err "NOT FOUND superclass = '%s'\n\n%!" (Typename.to_string iname);
         (match super_opt with

infer/src/clang/cTypes_decl.ml

@@ -143,7 +143,7 @@ let get_superclass_decls decl =
 let get_superclass_list decl =
   let base_decls = get_superclass_decls decl in
   let decl_to_mangled_name decl = Mangled.from_string (get_record_name decl) in
-  let get_super_field super_decl = (Csu.Class, decl_to_mangled_name super_decl) in
+  let get_super_field super_decl = Typename.TN_csu (Csu.Class, decl_to_mangled_name super_decl) in
   IList.map get_super_field base_decls
 
 let add_struct_to_tenv tenv typ =

infer/src/clang/objcInterface_decl.ml

@@ -92,9 +92,9 @@ let get_interface_superclasses super_opt protocols =
   let super_class =
     match super_opt with
     | None -> []
-    | Some super -> [(Csu.Class, Mangled.from_string super)] in
+    | Some super -> [Typename.TN_csu (Csu.Class, Mangled.from_string super)] in
   let protocol_names = IList.map (
-      fun name -> (Csu.Protocol, Mangled.from_string name)
+      fun name -> Typename.TN_csu (Csu.Protocol, Mangled.from_string name)
     ) protocols in
   let super_classes = super_class@protocol_names in
   super_classes
@@ -123,9 +123,9 @@ let add_class_to_tenv type_ptr_to_sil_type tenv curr_class decl_info class_name
       Printing.log_out "----->SuperClass field: '%s' " (Ident.fieldname_to_string fn);
       Printing.log_out "type: '%s'\n" (Sil.typ_to_string ft)) fields_sc;
   (*In case we found categories, or partial definition of this class earlier and they are already in the tenv *)
-  let fields, superclasses, methods =
+  let fields, (superclasses : Typename.t list), methods =
     match Sil.tenv_lookup tenv interface_name with
-    | Some Sil.Tstruct(saved_fields, _, _, _, saved_superclasses, saved_methods, _) ->
+    | Some (Sil.Tstruct (saved_fields, _, _, _, saved_superclasses, saved_methods, _)) ->
         General_utils.append_no_duplicates_fields fields saved_fields,
         General_utils.append_no_duplicates_csu superclasses saved_superclasses,
         General_utils.append_no_duplicates_methods methods saved_methods

infer/src/harness/androidFramework.ml

@@ -255,14 +255,15 @@ let get_all_supertypes typ tenv =
   let get_direct_supers = function
     | Sil.Tstruct (_, _, Csu.Class, _, supers, _, _) -> supers
     | _ -> [] in
-  let rec add_typ name typs =
-    let typename = Typename.TN_csu (Csu.Class, name) in
-    match Sil.tenv_lookup tenv typename with
+  let rec add_typ class_name typs =
+    match Sil.tenv_lookup tenv class_name with
     | Some typ -> get_supers_rec typ tenv (TypSet.add typ typs)
     | None -> typs
   and get_supers_rec typ tenv all_supers =
     let direct_supers = get_direct_supers typ in
-    IList.fold_left (fun typs (_, name) -> add_typ name typs) all_supers direct_supers in
+    IList.fold_left
+      (fun typs class_name -> add_typ class_name typs)
+      all_supers direct_supers in
   get_supers_rec typ tenv (TypSet.add typ TypSet.empty)
 
 (** return true if [typ0] <: [typ1] *)
@@ -305,7 +306,7 @@ let typ_is_lifecycle_typ typ lifecycle_typ tenv =
 
 (** return true if [class_name] is the name of a class that belong to the Android framework *)
 let is_android_lib_class class_name =
-  let class_str = Mangled.to_string class_name in
+  let class_str = Typename.name class_name in
   string_is_prefix "android" class_str || string_is_prefix "com.android" class_str
 
 (** returns an option containing the var name and type of a callback registered by [procname], None
@@ -378,10 +379,8 @@ let get_lifecycles = android_lifecycles
 let is_runtime_exception tenv exn =
   let lookup = Sil.tenv_lookup tenv in
   let runtime_exception_typename =
-    let name = Mangled.from_package_class "java.lang" "RuntimeException" in
-    Typename.TN_csu (Csu.Class, name)
-  and exn_typename = Typename.TN_csu (Csu.Class, exn) in
-  match lookup runtime_exception_typename, lookup exn_typename with
+    Typename.Java.from_string "java.lang.RuntimeException" in
+  match lookup runtime_exception_typename, lookup exn with
   | Some runtime_exception_type, Some exn_type ->
       is_subtype exn_type runtime_exception_type tenv
   | _ -> false

infer/src/harness/androidFramework.mli

@@ -47,10 +47,10 @@ val get_callbacks_registered_by_proc : Cfg.Procdesc.t -> Sil.tenv -> Sil.typ lis
 val get_lifecycle_for_framework_typ_opt : Mangled.t -> string list -> Sil.tenv -> (Sil.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 : Mangled.t -> bool
+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
 
 (** [is_runtime_exception tenv exn] checks if exn is an unchecked exception *)
-val is_runtime_exception : Sil.tenv -> Mangled.t -> bool
+val is_runtime_exception : Sil.tenv -> Typename.t -> bool

infer/src/harness/harness.ml

@@ -53,7 +53,7 @@ let extract_callbacks procdesc cfg_file cfg tenv harness_name harness_lvar callb
         | l ->
             (* choose to describe this anonymous inner class with one of the interfaces that it
              * implements. translation always places interfaces at the end of the supertypes list *)
-            Mangled.get_mangled (IList.hd (IList.rev l))
+            Typename.name (IList.hd (IList.rev l))
       else typ_str in
     Mangled.from_string (pretty_typ_str ^ "[line " ^ Location.to_string loc ^ "]") in
   let create_instrumentation_fields created_flds node instr = match instr with
@@ -118,16 +118,19 @@ let find_registered_callbacks lifecycle_trace harness_name proc_file_map tenv =
 (** 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 proc_file_map tenv = match typ with
-  | Sil.Tstruct(_, _, Csu.Class, Some class_name, _, methods, _)
-    when AndroidFramework.typ_is_lifecycle_typ typ lifecycle_typ tenv &&
-         not (AndroidFramework.is_android_lib_class class_name) ->
-      let ptr_to_typ = Some (Sil.Tptr (typ, Sil.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
+  | Sil.Tstruct(_, _, Csu.Class, Some name, _, methods, _) ->
+      let class_name = Typename.TN_csu (Csu.Class, name) in
+      if AndroidFramework.typ_is_lifecycle_typ typ lifecycle_typ tenv &&
+         not (AndroidFramework.is_android_lib_class class_name) then
+        let ptr_to_typ = Some (Sil.Tptr (typ, Sil.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 []
   | _ -> []
 
 (** get all the callbacks registered in [lifecycle_trace], transform the SIL to "extract" them into

infer/src/java/jTransType.ml

@@ -306,15 +306,12 @@ and create_sil_type program tenv cn =
   | None -> dummy_type cn
   | Some node ->
       let create_super_list interface_names =
-        (IList.map (fun i -> Mangled.from_string (JBasics.cn_name i)) interface_names) in
+        IList.map typename_of_classname interface_names in
       let (super_list, nonstatic_fields, static_fields, item_annotation) =
         match node with
         | Javalib.JInterface jinterface ->
             let static_fields, _ = get_all_fields program tenv cn in
-            let sil_interface_list =
-              IList.map
-                (fun c -> (Csu.Class, c))
-                (create_super_list jinterface.Javalib.i_interfaces) in
+            let sil_interface_list = create_super_list jinterface.Javalib.i_interfaces in
             let item_annotation = JAnnotation.translate_item jinterface.Javalib.i_annotations in
             (sil_interface_list, [], static_fields, item_annotation)
         | Javalib.JClass jclass ->
@@ -329,12 +326,11 @@ and create_sil_type program tenv cn =
               | Some super_cn ->
                   let super_classname =
                     match get_class_type_no_pointer program tenv super_cn with
-                    | Sil.Tstruct (_, _, _, Some classname, _, _, _) -> classname
+                    | Sil.Tstruct (_, _, _, Some classname, _, _, _) ->
+                        Typename.TN_csu (Csu.Class, classname)
                     | _ -> assert false in
                   super_classname :: interface_list in
-            let super_sil_classname_list =
-              IList.map (fun c -> (Csu.Class, c)) super_classname_list in
-            (super_sil_classname_list, nonstatic_fields, static_fields, item_annotation) in
+            (super_classname_list, nonstatic_fields, static_fields, item_annotation) in
       let classname = Mangled.from_string (JBasics.cn_name cn) in
       let method_procnames = get_class_procnames cn node in
       Sil.Tstruct (nonstatic_fields, static_fields, Csu.Class,