Expand Tvar to Tstruct as needed

Reviewed By: cristianoc

Differential Revision: D3809096

fbshipit-source-id: 7a8d2ac

infer/src/IR/Cfg.re

@@ -659,7 +659,7 @@ let module Node = {
       | exp => exp;
     let extract_class_name =
       fun
-      | Typ.Tptr (Tstruct {name}) _ => Typename.name name
+      | Typ.Tptr (Tvar name | Tstruct {name}) _ => Typename.name name
       | _ => failwith "Expecting classname for Java types";
     let subst_map = ref Ident.IdentMap.empty;
     let redirected_class_name origin_id =>

infer/src/IR/Sil.re

@@ -181,10 +181,13 @@ let hpred_get_lhs h =>
 
 
 /** {2 Comparision and Inspection Functions} */
-let has_objc_ref_counter _tenv hpred =>
+let has_objc_ref_counter tenv hpred =>
   switch hpred {
-  | Hpointsto _ _ (Sizeof (Tstruct struct_typ) _ _) =>
-    IList.exists Typ.is_objc_ref_counter_field struct_typ.instance_fields
+  | Hpointsto _ _ (Sizeof typ _ _) =>
+    switch (Tenv.expand_type tenv typ) {
+    | Tstruct {instance_fields} => IList.exists Typ.is_objc_ref_counter_field instance_fields
+    | _ => false
+    }
   | _ => false
   };
 

infer/src/IR/Tenv.re

@@ -41,6 +41,11 @@ let lookup tenv name =>
   };
 
 
+/** resolve a type string to a Java *class* type. For strings that may represent primitive or array
+    typs, use [lookup_java_typ_from_string] */
+let lookup_java_class_from_string tenv typ_str => lookup tenv (Typename.Java.from_string typ_str);
+
+
 /** Lookup Java types by name */
 let lookup_java_typ_from_string tenv typ_str => {
   let rec loop =
@@ -64,26 +69,14 @@ let lookup_java_typ_from_string tenv typ_str => {
       }
     | typ_str =>
       /* non-primitive/non-array type--resolve it in the tenv */
-      {
-        let typename = Typename.Java.from_string typ_str;
-        switch (lookup tenv typename) {
+      switch (lookup_java_class_from_string tenv typ_str) {
       | Some struct_typ => Some (Typ.Tstruct struct_typ)
       | None => None
-        }
       };
   loop typ_str
 };
 
 
-/** resolve a type string to a Java *class* type. For strings that may represent primitive or array
-    typs, use [lookup_java_typ_from_string] */
-let lookup_java_class_from_string tenv typ_str =>
-  switch (lookup_java_typ_from_string tenv typ_str) {
-  | Some (Typ.Tstruct struct_typ) => Some struct_typ
-  | _ => None
-  };
-
-
 /** Add a (name,type) pair to the global type environment. */
 let add tenv name struct_typ => TypenameHash.replace tenv name struct_typ;
 
@@ -120,25 +113,37 @@ let get_overriden_method tenv pname_java => {
     | [] => None
     };
   switch (proc_extract_declaring_class_typ tenv pname_java) {
-  | Some proc_struct_typ =>
-    get_overriden_method_in_superclasses pname_java proc_struct_typ.superclasses
+  | Some {Typ.superclasses: superclasses} =>
+    get_overriden_method_in_superclasses pname_java superclasses
   | _ => None
   }
 };
 
 
 /** expand a type if it is a typename by looking it up in the type environment */
-let expand_type tenv typ =>
+let expand_type tenv (typ: Typ.t) =>
   switch typ {
-  | Typ.Tvar tname =>
+  | Tvar tname =>
     switch (lookup tenv tname) {
-    | None => assert false
     | Some struct_typ => Typ.Tstruct struct_typ
+    | None => typ
     }
   | _ => typ
   };
 
 
+/** expand a type if it is a (pointer to a) typename by looking it up in the type environment */
+let expand_ptr_type tenv (typ: Typ.t) =>
+  switch typ {
+  | Tptr (Tvar tname) k =>
+    switch (lookup tenv tname) {
+    | Some struct_typ => Typ.Tptr (Tstruct struct_typ) k
+    | None => typ
+    }
+  | _ => expand_type tenv typ
+  };
+
+
 /** Serializer for type environments */
 let tenv_serializer: Serialization.serializer t = Serialization.create_serializer Serialization.tenv_key;
 

infer/src/IR/Tenv.rei

@@ -29,6 +29,10 @@ let create: unit => t;
 let expand_type: t => Typ.t => Typ.t;
 
 
+/** Expand a type if it is a (pointer to a) typename by looking it up in the type environment. */
+let expand_ptr_type: t => Typ.t => Typ.t;
+
+
 /** Fold a function over the elements of the type environment. */
 let fold: (Typename.t => Typ.struct_typ => 'a => 'a) => t => 'a => 'a;
 

infer/src/IR/Typ.re

@@ -483,22 +483,23 @@ let array_elem default_opt =>
 
 
 /** the element typ of the final extensible array in the given typ, if any */
-let rec get_extensible_array_element_typ =
-  fun
+let rec get_extensible_array_element_typ expand_type::expand_type typ =>
+  switch (expand_type typ) {
   | Tarray typ _ => Some typ
   | Tstruct {instance_fields} =>
     Option.map_default
-      (fun (_, fld_typ, _) => get_extensible_array_element_typ fld_typ)
+      (fun (_, fld_typ, _) => get_extensible_array_element_typ expand_type::expand_type fld_typ)
       None
       (IList.last instance_fields)
-  | _ => None;
+  | _ => None
+  };
 
 
 /** If a struct type with field f, return the type of f.
     If not, return the default type if given, otherwise raise an exception */
-let struct_typ_fld default_opt f => {
+let struct_typ_fld expand_type::expand_type default_opt f typ => {
   let def () => unsome "struct_typ_fld" default_opt;
-  fun
+  switch (expand_type typ) {
   | Tstruct struct_typ =>
     try (
       (fun (_, y, _) => y) (
@@ -508,10 +509,11 @@ let struct_typ_fld default_opt f => {
     | Not_found => def ()
     }
   | _ => def ()
+  }
 };
 
-let get_field_type_and_annotation fn =>
-  fun
+let get_field_type_and_annotation expand_ptr_type::expand_ptr_type fn typ =>
+  switch (expand_ptr_type typ) {
   | Tptr (Tstruct struct_typ) _
   | Tstruct struct_typ =>
     try {
@@ -523,7 +525,8 @@ let get_field_type_and_annotation fn =>
     } {
     | Not_found => None
     }
-  | _ => None;
+  | _ => None
+  };
 
 
 /** if [struct_typ] is a class, return its class kind (Java, CPP, or Obj-C) */
@@ -557,27 +560,30 @@ let struct_typ_is_objc_class struct_typ =>
   | _ => false
   };
 
-let is_class_of_kind typ ck =>
-  switch typ {
+let is_class_of_kind expand_type::expand_type typ ck =>
+  switch (expand_type typ) {
   | Tstruct {name: TN_csu (Class ck') _} => ck == ck'
   | _ => false
   };
 
-let is_objc_class typ => is_class_of_kind typ Csu.Objc;
+let is_objc_class expand_type::expand_type typ =>
+  is_class_of_kind expand_type::expand_type typ Csu.Objc;
 
-let is_cpp_class typ => is_class_of_kind typ Csu.CPP;
+let is_cpp_class expand_type::expand_type typ =>
+  is_class_of_kind expand_type::expand_type typ Csu.CPP;
 
-let is_java_class typ => is_class_of_kind typ Csu.Java;
+let is_java_class expand_type::expand_type typ =>
+  is_class_of_kind expand_type::expand_type typ Csu.Java;
 
-let rec is_array_of_cpp_class typ =>
+let rec is_array_of_cpp_class expand_type::expand_type typ =>
   switch typ {
-  | Tarray typ _ => is_array_of_cpp_class typ
-  | _ => is_cpp_class typ
+  | Tarray typ _ => is_array_of_cpp_class expand_type::expand_type typ
+  | _ => is_cpp_class expand_type::expand_type typ
   };
 
-let is_pointer_to_cpp_class typ =>
+let is_pointer_to_cpp_class expand_type::expand_type typ =>
   switch typ {
-  | Tptr t _ => is_cpp_class t
+  | Tptr t _ => is_cpp_class expand_type::expand_type t
   | _ => false
   };
 

infer/src/IR/Typ.rei

@@ -223,16 +223,17 @@ let array_elem: option t => t => t;
 
 
 /** the element typ of the final extensible array in the given typ, if any */
-let get_extensible_array_element_typ: t => option t;
+let get_extensible_array_element_typ: expand_type::(t => t) => t => option t;
 
 
 /** If a struct type with field f, return the type of f.
     If not, return the default type if given, otherwise raise an exception */
-let struct_typ_fld: option t => Ident.fieldname => t => t;
+let struct_typ_fld: expand_type::(t => t) => option t => Ident.fieldname => t => t;
 
 
 /** Return the type of the field [fn] and its annotation, None if [typ] has no field named [fn] */
-let get_field_type_and_annotation: Ident.fieldname => t => option (t, item_annotation);
+let get_field_type_and_annotation:
+  expand_ptr_type::(t => t) => Ident.fieldname => t => option (t, item_annotation);
 
 
 /** if [struct_typ] is a class, return its class kind (Java, CPP, or Obj-C) */
@@ -250,15 +251,15 @@ 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;
 
-let is_objc_class: t => bool;
+let is_objc_class: expand_type::(t => t) => t => bool;
 
-let is_cpp_class: t => bool;
+let is_cpp_class: expand_type::(t => t) => t => bool;
 
-let is_java_class: t => bool;
+let is_java_class: expand_type::(t => t) => t => bool;
 
-let is_array_of_cpp_class: t => bool;
+let is_array_of_cpp_class: expand_type::(t => t) => t => bool;
 
-let is_pointer_to_cpp_class: t => bool;
+let is_pointer_to_cpp_class: expand_type::(t => t) => t => bool;
 
 let has_block_prefix: string => bool;
 

infer/src/backend/abs.ml

@@ -999,10 +999,10 @@ let remove_opt _prop =
 
 (** Checks if cycle has fields (derived from a property or directly defined as ivar) with attributes
     weak/unsafe_unretained/assing *)
-let cycle_has_weak_or_unretained_or_assign_field _tenv cycle =
+let cycle_has_weak_or_unretained_or_assign_field tenv cycle =
   (* returns items annotation for field fn in struct t *)
   let get_item_annotation t fn =
-    match t with
+    match Tenv.expand_type tenv t with
     | Typ.Tstruct { Typ.instance_fields; static_fields } ->
         let ia = ref [] in
         IList.iter (fun (fn', _, ia') ->

infer/src/backend/absarray.ml

@@ -65,7 +65,7 @@ end = struct
 
   (** Find a strexp and a type at the given syntactic offset list *)
   let rec get_strexp_at_syn_offsets tenv se t syn_offs =
-    match se, t, syn_offs with
+    match se, Tenv.expand_type tenv t, syn_offs with
     | _, _, [] -> (se, t)
     | Sil.Estruct (fsel, _), Typ.Tstruct { Typ.instance_fields }, Field (fld, _) :: syn_offs' ->
         let se' = snd (IList.find (fun (f', _) -> Ident.fieldname_equal f' fld) fsel) in
@@ -84,7 +84,7 @@ end = struct
 
   (** Replace a strexp at the given syntactic offset list *)
   let rec replace_strexp_at_syn_offsets tenv se t syn_offs update =
-    match se, t, syn_offs with
+    match se, Tenv.expand_type tenv t, syn_offs with
     | _, _, [] ->
         update se
     | Sil.Estruct (fsel, inst), Typ.Tstruct { Typ.instance_fields }, Field (fld, _) :: syn_offs' ->
@@ -143,14 +143,14 @@ end = struct
     (sigma, hpred, syn_offs)
 
   (** Find a sub strexp with the given property. Can raise [Not_found] *)
-  let find _tenv (sigma : sigma) (pred : strexp_data -> bool) : t list =
+  let find tenv (sigma : sigma) (pred : strexp_data -> bool) : t list =
     let found = ref [] in
     let rec find_offset_sexp sigma_other hpred root offs se typ =
       let offs' = IList.rev offs in
       let path = (root, offs') in
       if pred (path, se, typ) then found := (sigma, hpred, offs') :: !found
       else begin
-        match se, typ with
+        match se, Tenv.expand_type tenv typ with
         | Sil.Estruct (fsel, _), Typ.Tstruct { Typ.instance_fields } ->
             find_offset_fsel sigma_other hpred root offs fsel instance_fields typ
         | Sil.Earray (_, esel, _), Typ.Tarray (t, _) ->
@@ -526,6 +526,7 @@ let report_error prop =
 
 (** Check performed after the array abstraction to see whether it was successful. Raise assert false in case of failure *)
 let check_after_array_abstraction tenv prop =
+  let expand_type = Tenv.expand_type tenv in
   let check_index root offs (ind, _) =
     if !Config.footprint then
       let path = StrexpMatch.path_from_exp_offsets root offs in
@@ -541,7 +542,7 @@ let check_after_array_abstraction tenv prop =
         else IList.iter (fun (ind, se) -> check_se root (offs @ [Sil.Off_index ind]) typ_elem se) esel
     | Sil.Estruct (fsel, _) ->
         IList.iter (fun (f, se) ->
-            let typ_f = Typ.struct_typ_fld (Some Typ.Tvoid) f typ in
+            let typ_f = Typ.struct_typ_fld ~expand_type (Some Typ.Tvoid) f typ in
             check_se root (offs @ [Sil.Off_fld (f, typ)]) typ_f se) fsel in
   let check_hpred = function
     | Sil.Hpointsto (root, se, texp) ->

infer/src/backend/errdesc.ml

@@ -573,7 +573,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
 
 (** find the dexp, if any, where the given value is stored
     also return the type of the value if found *)
-let vpath_find _tenv prop _exp : DExp.t option * Typ.t option =
+let vpath_find tenv prop _exp : DExp.t option * Typ.t option =
   if verbose then (L.d_str "in vpath_find exp:"; Sil.d_exp _exp; L.d_ln ());
   let rec find sigma_acc sigma_todo exp =
     let do_fse res sigma_acc' sigma_todo' lexp texp (f, se) = match se with
@@ -582,14 +582,19 @@ let vpath_find _tenv prop _exp : DExp.t option * Typ.t option =
           (match lexp with
            | Exp.Lvar pv ->
                let typo = match texp with
-                 | Exp.Sizeof (Typ.Tstruct struct_typ, _, _) ->
-                     (try
+                 | Exp.Sizeof (typ, _, _) -> (
+                     match Tenv.expand_type tenv typ with
+                     | Tstruct {instance_fields} -> (
+                         try
                            let _, t, _ =
-                          IList.find (fun (f', _, _) ->
-                              Ident.fieldname_equal f' f)
-                            struct_typ.Typ.instance_fields in
+                             IList.find (fun (f', _, _) -> Ident.fieldname_equal f' f)
+                               instance_fields in
                            Some t
-                      with Not_found -> None)
+                         with Not_found -> None
+                       )
+                     | _ ->
+                         None
+                   )
                  | _ -> None in
                res := Some (DExp.Ddot (DExp.Dpvar pv, f)), typo
            | Exp.Var id ->

infer/src/backend/interproc.ml

@@ -316,7 +316,7 @@ let prop_max_size = ref (0, Prop.prop_emp)
 let prop_max_chain_size = ref (0, Prop.prop_emp)
 
 (* Check if the prop exceeds the current max *)
-let check_prop_size p _ =
+let check_prop_size_ p _ =
   let size = Prop.Metrics.prop_size p in
   if size > fst !prop_max_size then
     (prop_max_size := (size, p);
@@ -326,7 +326,7 @@ let check_prop_size p _ =
 
 (* Check prop size and filter out possible unabstracted lists *)
 let check_prop_size edgeset_todo =
-  if Config.monitor_prop_size then Paths.PathSet.iter check_prop_size edgeset_todo
+  if Config.monitor_prop_size then Paths.PathSet.iter check_prop_size_ edgeset_todo
 
 let reset_prop_metrics () =
   prop_max_size := (0, Prop.prop_emp);
@@ -675,10 +675,15 @@ let report_context_leaks pname sigma tenv =
   let context_exps =
     IList.fold_left
       (fun exps hpred -> match hpred with
-         | Sil.Hpointsto (_, Eexp (exp, _), Sizeof (Tptr (Tstruct struct_typ, _), _, _))
+         | Sil.Hpointsto (_, Eexp (exp, _), Sizeof (Tptr (typ, _), _, _)) -> (
+             match Tenv.expand_type tenv typ with
+             | Tstruct struct_typ
                when AndroidFramework.is_context tenv struct_typ &&
                     not (AndroidFramework.is_application tenv struct_typ) ->
                  (exp, struct_typ) :: exps
+             | _ ->
+                 exps
+           )
          | _ -> exps)
       []
       sigma in

infer/src/backend/localise.ml

@@ -685,7 +685,8 @@ let desc_leak hpred_type_opt value_str_opt resource_opt resource_action_opt loc
           s, " to ", " on " in
     let typ_str =
       match hpred_type_opt with
-      | Some (Exp.Sizeof (Tstruct { name = TN_csu (Class _, _) as name; }, _, _)) ->
+      | Some (Exp.Sizeof (( Tvar (TN_csu (Class _, _) as name)
+                          | Tstruct { name = TN_csu (Class _, _) as name; }), _, _)) ->
           " of type " ^ Typename.name name ^ " "
       | _ -> " " in
     let desc_str =

infer/src/backend/modelBuiltins.ml

@@ -758,7 +758,8 @@ let execute_alloc mk can_return_null
         evaluate_char_sizeof (Exp.Const (Const.Cint len))
     | Exp.Sizeof _ -> e in
   let size_exp, procname = match args with
-    | [(Exp.Sizeof (Tstruct { name = TN_csu (Class Objc, _) as name } as s, len, subt), _)] ->
+    | [(Exp.Sizeof (( Tvar (TN_csu (Class Objc, _) as name)
+                    | Tstruct { name = TN_csu (Class Objc, _) as name; }) as s, len, subt), _)] ->
         let struct_type =
           match AttributesTable.get_correct_type_from_objc_class_name name with
           | Some struct_type -> struct_type

infer/src/backend/prop.ml

@@ -501,7 +501,7 @@ let rec create_strexp_of_type tenv struct_init_mode (typ : Typ.t) len inst : Sil
       | _ -> Exp.zero
     else
       create_fresh_var () in
-  match typ, len with
+  match Tenv.expand_type tenv typ, len with
   | (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), None ->
       Eexp (init_value (), inst)
   | Tstruct { Typ.instance_fields }, _ -> (
@@ -570,8 +570,9 @@ let sigma_get_unsigned_exps sigma =
 (** Collapse consecutive indices that should be added. For instance,
     this function reduces x[1][1] to x[2]. The [typ] argument is used
     to ensure the soundness of this collapsing. *)
-let exp_collapse_consecutive_indices_prop _tenv (typ : Typ.t) exp =
-  let typ_is_base (typ1 : Typ.t) = match typ1 with
+let exp_collapse_consecutive_indices_prop tenv (typ : Typ.t) exp =
+  let typ_is_base (typ1 : Typ.t) =
+    match Tenv.expand_type tenv typ1 with
     | Tint _ | Tfloat _ | Tstruct _ | Tvoid | Tfun _ ->
         true
     | _ ->
@@ -720,7 +721,8 @@ module Normalize = struct
   let (--) = IntLit.sub
   let (++) = IntLit.add
 
-  let sym_eval _tenv abs e =
+  let sym_eval tenv abs e =
+    let expand_type = Tenv.expand_type tenv in
     let rec eval (e : Exp.t) : Exp.t =
       (* L.d_str " ["; Sil.d_exp e; L.d_str"] "; *)
       match e with
@@ -890,7 +892,8 @@ module Normalize = struct
             | _ -> BinOp (ominus, x, y) in
           (* test if the extensible array at the end of [typ] has elements of type [elt] *)
           let extensible_array_element_typ_equal elt typ =
-            Option.map_default (Typ.equal elt) false (Typ.get_extensible_array_element_typ typ) in
+            Option.map_default (Typ.equal elt) false
+              (Typ.get_extensible_array_element_typ ~expand_type typ) in
           begin
             match e1', e2' with
             (* pattern for arrays and extensible structs:

infer/src/backend/prover.ml

@@ -40,7 +40,8 @@ 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 tenv = function
+let rec is_java_class tenv typ =
+  match Tenv.expand_type tenv typ with
   | Typ.Tstruct struct_typ -> Typ.struct_typ_is_java_class struct_typ
   | Typ.Tarray (inner_typ, _) | Tptr (inner_typ, _) -> is_java_class tenv inner_typ
   | _ -> false
@@ -379,7 +380,8 @@ end = struct
     IList.iter process_atom pi;
     saturate { leqs = !leqs; lts = !lts; neqs = !neqs }
 
-  let from_sigma _tenv sigma =
+  let from_sigma tenv sigma =
+    let expand_ptr_type = Tenv.expand_ptr_type tenv in
     let leqs = ref [] in
     let lts = ref [] in
     let add_lt_minus1_e e =
@@ -399,8 +401,9 @@ end = struct
           if type_opt_is_unsigned t then add_lt_minus1_e e
       | Sil.Estruct (fsel, _), t ->
           let get_field_type f =
-            Option.map_default
-              (fun t' -> Option.map fst @@ Typ.get_field_type_and_annotation f t') None t in
+            Option.map_default (fun t' ->
+                Option.map fst @@ Typ.get_field_type_and_annotation ~expand_ptr_type f t'
+              ) None t in
           IList.iter (fun (f, se) -> strexp_extract (se, get_field_type f)) fsel
       | Sil.Earray (len, isel, _), t ->
           let elt_t = match t with
@@ -1323,13 +1326,14 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2 :
       raise (Exceptions.Abduction_case_not_implemented __POS__)
 
 and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Ident.fieldname * Sil.strexp) list) * ((Ident.fieldname * Sil.strexp) list) =
+  let expand_type = Tenv.expand_type tenv in
   match fsel1, fsel2 with
   | _, [] -> subs, fsel1, []
   | (f1, se1) :: fsel1', (f2, se2) :: fsel2' ->
       begin
         match Ident.fieldname_compare f1 f2 with
         | 0 ->
-            let typ' = Typ.struct_typ_fld (Some Typ.Tvoid) f2 typ2 in
+            let typ' = Typ.struct_typ_fld ~expand_type (Some Typ.Tvoid) f2 typ2 in
             let subs', se_frame, se_missing =
               sexp_imply tenv (Exp.Lfield (source, f2, typ2)) false calc_missing subs se1 se2 typ' in
             let subs'', fld_frame, fld_missing = struct_imply tenv source calc_missing subs' fsel1' fsel2' typ2 in
@@ -1344,7 +1348,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Ide
             let subs', fld_frame, fld_missing = struct_imply tenv source calc_missing subs fsel1' fsel2 typ2 in
             subs', ((f1, se1) :: fld_frame), fld_missing
         | _ ->
-            let typ' = Typ.struct_typ_fld (Some Typ.Tvoid) f2 typ2 in
+            let typ' = Typ.struct_typ_fld ~expand_type (Some Typ.Tvoid) f2 typ2 in
             let subs' =
               sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' in
             let subs', fld_frame, fld_missing = struct_imply tenv source calc_missing subs' fsel1 fsel2' typ2 in
@@ -1352,7 +1356,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Ide
             subs', fld_frame, fld_missing'
       end
   | [], (f2, se2) :: fsel2' ->
-      let typ' = Typ.struct_typ_fld (Some Typ.Tvoid) f2 typ2 in
+      let typ' = Typ.struct_typ_fld ~expand_type (Some Typ.Tvoid) f2 typ2 in
       let subs' = sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' in
       let subs'', fld_frame, fld_missing = struct_imply tenv source calc_missing subs' [] fsel2' typ2 in
       subs'', fld_frame, (f2, se2):: fld_missing
@@ -1462,10 +1466,11 @@ let move_primed_lhs_from_front subs sigma = match sigma with
 
 (** [expand_hpred_pointer calc_index_frame hpred] expands [hpred] if it is a |-> whose lhs is a Lfield or Lindex or ptr+off.
     Return [(changed, calc_index_frame', hpred')] where [changed] indicates whether the predicate has changed. *)
-let expand_hpred_pointer _tenv calc_index_frame hpred : bool * bool * Sil.hpred =
+let expand_hpred_pointer tenv calc_index_frame hpred : bool * bool * Sil.hpred =
   let rec expand changed calc_index_frame hpred = match hpred with
     | Sil.Hpointsto (Lfield (adr_base, fld, adr_typ), cnt, cnt_texp) ->
-        let cnt_texp' = match adr_typ, cnt_texp with
+        let cnt_texp' =
+          match Tenv.expand_type tenv adr_typ, cnt_texp with
           | Tstruct _, _ ->
               (* type of struct at adr_base is known *)
               Exp.Sizeof (adr_typ, None, Subtype.exact)
@@ -1553,7 +1558,7 @@ struct
 
   (** check if t1 is a subtype of t2, in Java *)
   let rec check_subtype_java tenv t1 t2 =
-    match t1, t2 with
+    match Tenv.expand_type tenv t1, Tenv.expand_type tenv t2 with
     | Typ.Tstruct { name = TN_csu (Class Java, _) as cn1 },
       Typ.Tstruct { name = TN_csu (Class Java, _) as cn2 } ->
         check_subclass tenv cn1 cn2
@@ -1572,7 +1577,7 @@ struct
 
   let get_type_name (t: Typ.t) =
     match t with
-    | Tstruct { name } -> Some name
+    | Tvar name | Tstruct { name } -> Some name
     | _ -> None
 
   (** check if t1 is a subtype of t2 *)
@@ -1586,7 +1591,7 @@ struct
       | _ -> false
 
   let rec case_analysis_type_java tenv (t1, st1) (t2, st2) =
-    match t1, t2 with
+    match Tenv.expand_type tenv t1, Tenv.expand_type tenv t2 with
     | Typ.Tstruct { name = TN_csu (Class Java, _) as cn1 },
       Typ.Tstruct { name = TN_csu (Class Java, _) as cn2 } ->
         Subtype.case_analysis (cn1, st1) (cn2, st2)
@@ -1658,7 +1663,8 @@ let cast_exception tenv texp1 texp2 e1 subs =
     Note: supertype should be a type T rather than a pointer to type T
     Note: [pname] wil never be included in the returned result *)
 let get_overrides_of tenv supertype pname =
-  let typ_has_method pname = function
+  let typ_has_method pname typ =
+    match Tenv.expand_type tenv typ with
     | Typ.Tstruct { Typ.def_methods } ->
         IList.exists (fun m -> Procname.equal pname m) def_methods
     | _ -> false in
@@ -1686,17 +1692,20 @@ let texp_equal_modulo_subtype_flag texp1 texp2 = match texp1, texp2 with
 let texp_imply tenv subs texp1 texp2 e1 calc_missing =
   (* check whether the types could be subject to dynamic cast: *)
   (* classes and arrays in Java, and just classes in C++ and ObjC *)
+  let expand_type = Tenv.expand_type tenv in
   let types_subject_to_dynamic_cast =
     match texp1, texp2 with
-    | Exp.Sizeof ((Typ.Tstruct _) as typ1, _, _), Exp.Sizeof (Typ.Tstruct _, _, _)
-    | Exp.Sizeof ((Typ.Tarray _) as typ1, _, _), Exp.Sizeof (Typ.Tarray _, _, _)
-    | Exp.Sizeof ((Typ.Tarray _) as typ1, _, _), Exp.Sizeof (Typ.Tstruct _, _, _)
-    | Exp.Sizeof ((Typ.Tstruct _) as typ1, _, _), Exp.Sizeof (Typ.Tarray _, _, _)
-      when is_java_class tenv typ1 -> true
-
-    | Exp.Sizeof (typ1, _, _), Exp.Sizeof (typ2, _, _) ->
-        (Typ.is_cpp_class typ1 && Typ.is_cpp_class typ2) ||
-        (Typ.is_objc_class typ1 && Typ.is_objc_class typ2)
+    | Exp.Sizeof (typ1_0, _, _), Exp.Sizeof (typ2_0, _, _) -> (
+        let typ1 = expand_type typ1_0 in
+        let typ2 = expand_type typ2_0 in
+        match typ1, typ2 with
+        | (Tstruct _ | Tarray _), (Tstruct _ | Tarray _) ->
+            is_java_class tenv typ1
+            || (Typ.is_cpp_class ~expand_type typ1 && Typ.is_cpp_class ~expand_type typ2)
+            || (Typ.is_objc_class ~expand_type typ1 && Typ.is_objc_class ~expand_type typ2)
+        | _ ->
+            false
+      )
     | _ -> false in
   if types_subject_to_dynamic_cast then
     begin

infer/src/backend/rearrange.ml

@@ -97,7 +97,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
     incr max_stamp;
     Ident.create kind !max_stamp in
   let res =
-    match t, off with
+    match Tenv.expand_type tenv t, off with
     | Typ.Tstruct _, [] ->
         ([], Sil.Estruct ([], inst), t)
     | Typ.Tstruct ({ Typ.instance_fields; static_fields } as struct_typ ),
@@ -192,7 +192,7 @@ let rec _strexp_extend_values
   let new_id () =
     incr max_stamp;
     Ident.create kind !max_stamp in
-  match off, se, typ with
+  match off, se, Tenv.expand_type tenv typ with
   | [], Sil.Eexp _, _
   | [], Sil.Estruct _, _ ->
       [([], se, typ)]
@@ -613,6 +613,7 @@ let prop_iter_add_hpred_footprint_to_prop pname tenv prop (lexp, typ) inst =
 (** If [lexp] is an access to a field that is annotated with @GuardedBy, add constraints to [prop]
     expressing the safety conditions for the access. Complain if these conditions cannot be met. *)
 let add_guarded_by_constraints tenv prop lexp pdesc =
+  let expand_ptr_type = Tenv.expand_ptr_type tenv in
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let excluded_guardedby_string str =
     (* nothing with a space in it can be a valid Java expression, shouldn't warn *)
@@ -653,7 +654,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
     IList.find_map_opt annot_extract_guarded_by_str item_annot in
   (* if [fld] is annotated with @GuardedBy("mLock"), return mLock *)
   let get_guarded_by_fld_str fld typ =
-    match Typ.get_field_type_and_annotation fld typ with
+    match Typ.get_field_type_and_annotation ~expand_ptr_type fld typ with
     | Some (_, item_annot) ->
         begin
           match extract_guarded_by_str item_annot with
@@ -681,7 +682,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
               try
                 let fld, strexp = IList.find f flds in
                 begin
-                  match Typ.get_field_type_and_annotation fld typ with
+                  match Typ.get_field_type_and_annotation ~expand_ptr_type fld typ with
                   | Some (fld_typ, _) -> Some (strexp, fld_typ)
                   | None -> None
                 end
@@ -1026,8 +1027,9 @@ let iter_rearrange_pe_dllseg_last tenv recurse_on_iters default_case_iter iter p
   recurse_on_iters iter_subcases
 
 (** find the type at the offset from the given type expression, if any *)
-let type_at_offset _tenv texp off =
-  let rec strip_offset off typ = match off, typ with
+let type_at_offset tenv texp off =
+  let rec strip_offset off typ =
+    match off, Tenv.expand_type tenv typ with
     | [], _ -> Some typ
     | (Sil.Off_fld (f, _)):: off', Typ.Tstruct { Typ.instance_fields } ->
         (try
@@ -1079,7 +1081,9 @@ let rec iter_rearrange
     pname tenv lexp typ_from_instr prop iter
     inst: (Sil.offset list) Prop.prop_iter list =
   let rec root_typ_of_offsets = function
-    | Sil.Off_fld (f, ((Typ.Tstruct _) as struct_typ)) :: _ ->
+    | Sil.Off_fld (f, fld_typ) :: _ -> (
+        match Tenv.expand_type tenv fld_typ with
+        | Tstruct _ as struct_typ ->
             (* access through field: get the struct type from the field *)
             if Config.trace_rearrange then begin
               L.d_increase_indent 1;
@@ -1089,6 +1093,9 @@ let rec iter_rearrange
               L.d_ln();
             end;
             struct_typ
+        | _ ->
+            typ_from_instr
+      )
     | Sil.Off_index _ :: off ->
         Typ.Tarray (root_typ_of_offsets off, None)
     | _ ->
@@ -1187,6 +1194,7 @@ let is_weak_captured_var pdesc pvar =
 
 (** Check for dereference errors: dereferencing 0, a freed value, or an undefined value *)
 let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc =
+  let expand_ptr_type = Tenv.expand_ptr_type tenv in
   let nullable_obj_str = ref None in
   let nullable_str_is_weak_captured_var = ref false in
   (* return true if deref_exp is only pointed to by fields/params with @Nullable annotations *)
@@ -1218,7 +1226,7 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc =
              is_nullable || Pvar.is_local pvar
          | Sil.Hpointsto (_, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) ->
              let fld_is_nullable fld =
-               match Typ.get_field_type_and_annotation fld typ with
+               match Typ.get_field_type_and_annotation ~expand_ptr_type fld typ with
                | Some (_, annot) -> Annotations.ia_is_nullable annot
                | _ -> false in
              let is_strexp_pt_by_nullable_fld (fld, strexp) =

infer/src/backend/symExec.ml

@@ -534,7 +534,7 @@ let resolve_typename prop receiver_exp =
       | _ :: hpreds -> loop hpreds in
     loop prop.Prop.sigma in
   match typexp_opt with
-  | Some (Exp.Sizeof (Tstruct { name }, _, _)) -> Some name
+  | Some (Exp.Sizeof ((Tvar name | Tstruct { name }), _, _)) -> Some name
   | _ -> None
 
 (** If the dynamic type of the receiver actual T_actual is a subtype of the reciever type T_formal
@@ -1302,7 +1302,8 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
         if already_has_abduced_retval prop then prop
         else
         if !Config.footprint then
-          let prop', abduced_strexp = match actual_typ with
+          let prop', abduced_strexp =
+            match Tenv.expand_type tenv actual_typ with
             | Typ.Tptr ((Typ.Tstruct _) as typ, _) ->
                 (* for struct types passed by reference, do abduction on the fields of the
                    struct *)

infer/src/backend/tabulation.ml

@@ -457,7 +457,7 @@ and sexp_star_fld se1 se2 : Sil.strexp =
       L.d_ln ();
       assert false
 
-let texp_star _tenv texp1 texp2 =
+let texp_star tenv texp1 texp2 =
   let rec ftal_sub ftal1 ftal2 = match ftal1, ftal2 with
     | [], _ -> true
     | _, [] -> false
@@ -466,7 +466,8 @@ let texp_star _tenv texp1 texp2 =
           | n when n < 0 -> false
           | 0 -> ftal_sub ftal1' ftal2'
           | _ -> ftal_sub ftal1 ftal2' end in
-  let typ_star t1 t2 = match t1, t2 with
+  let typ_star t1 t2 =
+    match Tenv.expand_type tenv t1, Tenv.expand_type tenv t2 with
     | Typ.Tstruct { instance_fields = instance_fields1; name = TN_csu (csu1, _) },
       Typ.Tstruct { instance_fields = instance_fields2; name = TN_csu (csu2, _) }
       when csu1 = csu2 ->
@@ -625,7 +626,9 @@ let prop_get_exn_name pname prop =
   let ret_pvar = Exp.Lvar (Pvar.get_ret_pvar pname) in
   let rec search_exn e = function
     | [] -> None
-    | Sil.Hpointsto (e1, _, Sizeof (Tstruct { name }, _, _)) :: _ when Exp.equal e1 e -> Some name
+    | Sil.Hpointsto (e1, _, Sizeof ((Tvar name | Tstruct { name }), _, _)) :: _
+      when Exp.equal e1 e ->
+        Some name
     | _ :: tl -> search_exn e tl in
   let rec find_exn_name hpreds = function
     | [] -> None

infer/src/backend/taint.ml

@@ -14,7 +14,7 @@ module L = Logging
 open PatternMatch
 
 (* list of sources that return a tainted value *)
-let sources = [
+let sources0 = [
   (* for testing only *)
   {
     classname = "com.facebook.infer.models.InferTaint";
@@ -284,7 +284,7 @@ let taint_spec_to_taint_info taint_spec =
   { PredSymb.taint_source; taint_kind = taint_spec.taint_kind }
 
 let sources =
-  IList.map taint_spec_to_taint_info sources
+  IList.map taint_spec_to_taint_info sources0
 
 let mk_pname_param_num methods =
   IList.map

infer/src/checkers/checkers.ml

@@ -75,6 +75,7 @@ module ST = struct
       ?(exception_kind = fun k d -> Exceptions.Checkers (k, d))
       ?(always_report = false)
       description =
+    let expand_ptr_type = Tenv.expand_ptr_type tenv in
     let localized_description = Localise.custom_desc_with_advice
         description
         (Option.default "" advice)
@@ -112,7 +113,7 @@ module ST = struct
       let is_field_suppressed =
         match field_name, PatternMatch.get_this_type proc_attributes with
         | Some field_name, Some t -> begin
-            match (Typ.get_field_type_and_annotation field_name t) with
+            match Typ.get_field_type_and_annotation ~expand_ptr_type field_name t with
             | Some (_, ia) -> Annotations.ia_has_annotation_with ia annotation_matches
             | None -> false
           end
@@ -208,7 +209,7 @@ 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
-      match this_type with
+      match Tenv.expand_ptr_type tenv this_type with
       | Typ.Tptr (Typ.Tstruct struct_typ, _) | Typ.Tstruct struct_typ ->
           PatternMatch.is_immediate_subtype struct_typ class_name
       | _ -> false in
@@ -219,7 +220,8 @@ let callback_check_write_to_parcel_java
     PatternMatch.has_formal_method_argument_type_names
       proc_desc pname_java ["android.os.Parcel"] in
 
-  let parcel_constructors _tenv = function
+  let parcel_constructors tenv typ =
+    match Tenv.expand_ptr_type tenv typ with
     | Typ.Tptr (Typ.Tstruct { Typ.def_methods }, _) ->
         IList.filter is_parcel_constructor def_methods
     | _ -> [] in
@@ -317,17 +319,18 @@ let callback_check_write_to_parcel ({ Callbacks.proc_name } as args) =
       ()
 
 (** Monitor calls to Preconditions.checkNotNull and detect inconsistent uses. *)
-let callback_monitor_nullcheck { Callbacks.proc_desc; idenv; proc_name } =
+let callback_monitor_nullcheck { Callbacks.tenv; proc_desc; idenv; proc_name } =
   let verbose = ref false in
 
   let class_formal_names = lazy (
     let formals = Cfg.Procdesc.get_formals proc_desc in
     let class_formals =
-      let is_class_type = function
-        | p, Typ.Tptr _ when Mangled.to_string p = "this" ->
+      let is_class_type (p, typ) =
+        match Tenv.expand_ptr_type tenv typ with
+        | Typ.Tptr _ when Mangled.to_string p = "this" ->
             false (* no need to null check 'this' *)
-        | _, Typ.Tstruct _ -> true
-        | _, Typ.Tptr (Typ.Tstruct _, _) -> true
+        | Typ.Tstruct _ -> true
+        | Typ.Tptr (Typ.Tstruct _, _) -> true
         | _ -> false in
       IList.filter is_class_type formals in
     IList.map fst class_formals) in

infer/src/checkers/fragmentRetainsViewChecker.ml

@@ -27,6 +27,8 @@ let callback_fragment_retains_view_java
   let is_on_destroy_view = Procname.java_get_method pname_java = "onDestroyView" in
   (* this is needlessly complicated because field types are Tvars instead of Tstructs *)
   let fld_typ_is_view = function
+    | Typ.Tptr (Tstruct struct_typ, _) ->
+        AndroidFramework.is_view tenv struct_typ
     | Typ.Tptr (Typ.Tvar tname, _) ->
         begin
           match Tenv.lookup tenv tname with

infer/src/checkers/patternMatch.ml

@@ -24,7 +24,8 @@ type taint_spec = {
   language : Config.language
 }
 
-let type_is_object _tenv = function
+let type_is_object tenv typ =
+  match Tenv.expand_ptr_type tenv typ with
   | Typ.Tptr (Tstruct { name }, _) -> string_equal (Typename.name name) JConfig.object_cl
   | _ -> false
 
@@ -77,7 +78,8 @@ let get_this_type proc_attributes = match proc_attributes.ProcAttributes.formals
   | (_, t):: _ -> Some t
   | _ -> None
 
-let type_get_direct_supertypes _tenv = function
+let type_get_direct_supertypes tenv typ =
+  match Tenv.expand_ptr_type tenv typ with
   | Typ.Tptr (Tstruct { superclasses }, _)
   | Typ.Tstruct { superclasses } ->
       superclasses
@@ -88,9 +90,9 @@ let type_get_class_name = function
   | Typ.Tptr (typ, _) -> Typ.name typ
   | _ -> None
 
-let type_get_annotation _tenv
+let type_get_annotation tenv
     (t: Typ.t): Typ.item_annotation option =
-  match t with
+  match Tenv.expand_ptr_type tenv t with
   | Typ.Tptr (Typ.Tstruct { Typ.struct_annotations }, _)
   | Typ.Tstruct { Typ.struct_annotations } ->
       Some struct_annotations
@@ -108,7 +110,7 @@ let type_has_supertype
       false
     else
       begin
-        match Tenv.expand_type tenv typ with
+        match Tenv.expand_ptr_type tenv typ with
         | Typ.Tptr (Typ.Tstruct { Typ.superclasses }, _)
         | Typ.Tstruct { Typ.superclasses } ->
             let match_supertype cn =
@@ -135,10 +137,10 @@ let rec get_type_name = function
   | Typ.Tptr (t, _) -> get_type_name t
   | _ -> "_"
 
-let get_field_type_name _tenv
+let get_field_type_name tenv
     (typ: Typ.t)
     (fieldname: Ident.fieldname): string option =
-  match typ with
+  match Tenv.expand_ptr_type tenv typ with
   | Typ.Tstruct { Typ.instance_fields }
   | Typ.Tptr (Typ.Tstruct { Typ.instance_fields }, _) -> (
       try
@@ -249,7 +251,8 @@ let get_java_method_call_formal_signature = function
   | _ -> None
 
 
-let type_is_class _tenv = function
+let type_is_class tenv typ =
+  match Tenv.expand_ptr_type tenv typ with
   | Typ.Tptr (Typ.Tstruct _, _) -> true
   | Typ.Tptr (Typ.Tvar _, _) -> true
   | Typ.Tptr (Typ.Tarray _, _) -> true

infer/src/clang/cMethod_trans.ml

@@ -61,8 +61,8 @@ let get_class_param function_method_decl_info =
   else []
 
 
-let should_add_return_param _tenv return_type ~is_objc_method =
-  match return_type with
+let should_add_return_param tenv return_type ~is_objc_method =
+  match Tenv.expand_type tenv return_type with
   | Typ.Tstruct _ -> not is_objc_method
   | _ -> false
 
@@ -111,7 +111,8 @@ let get_parameters tenv function_method_decl_info =
     | Clang_ast_t.ParmVarDecl (_, name_info, qt, var_decl_info) ->
         let _, mangled = General_utils.get_var_name_mangled name_info var_decl_info in
         let param_typ = CTypes_decl.type_ptr_to_sil_type tenv qt.Clang_ast_t.qt_type_ptr in
-        let qt_type_ptr = match param_typ with
+        let qt_type_ptr =
+          match Tenv.expand_type tenv param_typ with
           | Typ.Tstruct _ when General_utils.is_cpp_translation ->
               Ast_expressions.create_reference_type qt.Clang_ast_t.qt_type_ptr
           | _ -> qt.Clang_ast_t.qt_type_ptr in
@@ -121,7 +122,7 @@ let get_parameters tenv function_method_decl_info =
   get_class_param function_method_decl_info @ pars @ get_return_param tenv function_method_decl_info
 
 (** get return type of the function and optionally type of function's return parameter *)
-let get_return_type tenv function_method_decl_info =
+let get_return_val_and_param_types tenv function_method_decl_info =
   let return_type_ptr = get_original_return_type function_method_decl_info in
   let return_typ = CTypes_decl.type_ptr_to_sil_type tenv return_type_ptr in
   let is_objc_method = is_objc_method function_method_decl_info in
@@ -132,7 +133,7 @@ let get_return_type tenv function_method_decl_info =
 let build_method_signature tenv decl_info procname function_method_decl_info
     parent_pointer pointer_to_property_opt =
   let source_range = decl_info.Clang_ast_t.di_source_range in
-  let tp, return_param_type_opt = get_return_type tenv function_method_decl_info in
+  let tp, return_param_type_opt = get_return_val_and_param_types tenv function_method_decl_info in
   let is_instance_method = is_instance_method function_method_decl_info in
   let parameters = get_parameters tenv function_method_decl_info in
   let attributes = decl_info.Clang_ast_t.di_attributes in

infer/src/clang/cTrans.ml

@@ -627,10 +627,11 @@ struct
 
   and var_deref_trans trans_state stmt_info (decl_ref : Clang_ast_t.decl_ref) =
     let context = trans_state.context in
-    let _tenv = context.tenv in
+    let tenv = context.tenv in
     let _, _, type_ptr = Ast_utils.get_info_from_decl_ref decl_ref in
     let ast_typ = CTypes_decl.type_ptr_to_sil_type context.tenv type_ptr in
-    let typ = match ast_typ with
+    let typ =
+      match Tenv.expand_type tenv ast_typ with
       | Tstruct _ when decl_ref.dr_kind = `ParmVar ->
           if General_utils.is_cpp_translation then
             Typ.Tptr (ast_typ, Pk_reference)
@@ -649,7 +650,7 @@ struct
       let is_global_const, init_expr =
         match Ast_utils.get_decl decl_ref.dr_decl_pointer with
         | Some VarDecl (_, _, qual_type, vdi) ->
-            (match ast_typ with
+            (match Tenv.expand_type tenv ast_typ with
              | Tstruct _
                when not General_utils.is_cpp_translation ->
                  (* Do not convert a global struct to a local because SIL
@@ -2074,9 +2075,10 @@ struct
         }
     | _ -> assert false
 
-  and initListExpr_initializers_trans trans_state var_exp n stmts typ is_dyn_array stmt_info =
+  and initListExpr_initializers_trans ({context = {tenv}} as trans_state) var_exp n stmts typ is_dyn_array stmt_info =
+    let expand_type = Tenv.expand_ptr_type tenv in
     let (var_exp_inside, typ_inside) = match typ with
-      | Typ.Tarray (t, _) when Typ.is_array_of_cpp_class typ ->
+      | Typ.Tarray (t, _) when Typ.is_array_of_cpp_class ~expand_type typ ->
           Exp.Lindex (var_exp, Exp.Const (Const.Cint (IntLit.of_int n))), t
       | _ when is_dyn_array ->
           Exp.Lindex (var_exp, Exp.Const (Const.Cint (IntLit.of_int n))), typ
@@ -2117,6 +2119,7 @@ struct
 
   and cxxNewExpr_trans trans_state stmt_info expr_info cxx_new_expr_info =
     let context = trans_state.context in
+    let expand_type = Tenv.expand_ptr_type context.CContext.tenv in
     let typ = CTypes_decl.get_type_from_expr_info expr_info context.CContext.tenv in
     let sil_loc = CLocation.get_sil_location stmt_info context in
     let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in
@@ -2143,7 +2146,7 @@ struct
     let init_stmt_info = { stmt_info with
                            Clang_ast_t.si_pointer = Ast_utils.get_fresh_pointer () } in
     let res_trans_init =
-      if is_dyn_array && Typ.is_pointer_to_cpp_class typ then
+      if is_dyn_array && Typ.is_pointer_to_cpp_class ~expand_type typ then
         let rec create_stmts stmt_opt size_exp_opt =
           match stmt_opt, size_exp_opt with
           | Some stmt, Some (Exp.Const (Const.Cint n)) when not (IntLit.iszero n) ->

infer/src/clang/objcInterface_decl.ml

@@ -21,12 +21,13 @@ open CFrontend_utils
 module L = Logging
 
 let is_pointer_to_objc_class tenv typ =
+  let expand_type = Tenv.expand_ptr_type tenv in
   match typ with
   | Typ.Tptr (Typ.Tvar (Typename.TN_csu (Csu.Class Csu.Objc, cname)), _) ->
       (match Tenv.lookup tenv (Typename.TN_csu (Csu.Class Csu.Objc, cname)) with
-       | Some struct_typ when Typ.is_objc_class (Typ.Tstruct struct_typ) -> true
+       | Some struct_typ when Typ.is_objc_class ~expand_type (Typ.Tstruct struct_typ) -> true
        | _ -> false)
-  | Typ.Tptr (typ, _) when Typ.is_objc_class typ -> true
+  | Typ.Tptr (typ, _) when Typ.is_objc_class ~expand_type typ -> true
   | _ -> false
 
 let get_super_interface_decl otdi_super =

infer/src/eradicate/eradicateChecks.ml

@@ -39,8 +39,9 @@ let return_nonnull_silent = true
 let check_library_calls = false
 
 
-let get_field_annotation _tenv fn typ =
-  match Typ.get_field_type_and_annotation fn typ with
+let get_field_annotation tenv fn typ =
+  let expand_ptr_type = Tenv.expand_ptr_type tenv in
+  match Typ.get_field_type_and_annotation ~expand_ptr_type fn typ with
   | None -> None
   | Some (t, ia) ->
       let ia' =
@@ -135,7 +136,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname
     let loc = Cfg.Node.get_loc node in
     let throwable_found = ref false in
     let typ_is_throwable = function
-      | Typ.Tstruct { name = TN_csu (Class _, _) as name } ->
+      | Typ.Tvar name | Typ.Tstruct { name = TN_csu (Class _, _) as name } ->
           string_equal (Typename.name name) "java.lang.Throwable"
       | _ -> false in
     let do_instr = function
@@ -255,7 +256,10 @@ let check_constructor_initialization tenv
   State.set_node start_node;
   if Procname.is_constructor curr_pname
   then begin
-    match PatternMatch.get_this_type (Cfg.Procdesc.get_attributes curr_pdesc) with
+    match
+      Option.map (Tenv.expand_ptr_type tenv)
+        (PatternMatch.get_this_type (Cfg.Procdesc.get_attributes curr_pdesc))
+    with
     | Some (Tptr (Tstruct { instance_fields; name } as ts, _)) ->
         let do_field (fn, ft, _) =
           let annotated_with f = match get_field_annotation tenv fn ts with

infer/src/harness/inhabit.ml

@@ -94,7 +94,8 @@ let rec inhabit_typ tenv typ cfg env =
           let (allocated_obj_exp, env) = inhabit_alloc typ None typ ModelBuiltins.__new env in
           (* select methods that are constructors and won't force us into infinite recursion because
            * we are already inhabiting one of their argument types *)
-          let get_all_suitable_constructors typ = match typ with
+          let get_all_suitable_constructors typ =
+            match Tenv.expand_type tenv typ with
             | Typ.Tstruct { name = TN_csu (Class _, _); def_methods } ->
                 let is_suitable_constructor p =
                   let try_get_non_receiver_formals p =

infer/src/java/jTrans.ml

@@ -107,7 +107,7 @@ let retrieve_fieldname fieldname =
 
 
 let get_field_name program static tenv cn fs =
-  match JTransType.get_class_type_no_pointer program tenv cn with
+  match Tenv.expand_type tenv (JTransType.get_class_type_no_pointer program tenv cn) with
   | Typ.Tstruct { Typ.instance_fields; static_fields; name = TN_csu (Class _, _) } ->
       let fieldname, _, _ =
         try

infer/src/java/jTransType.ml

@@ -86,8 +86,8 @@ let rec create_array_type typ dim =
     Typ.Tptr(Typ.Tarray (content_typ, None), Typ.Pk_pointer)
   else typ
 
-let extract_cn_no_obj _tenv typ =
-  match typ with
+let extract_cn_no_obj tenv typ =
+  match Tenv.expand_ptr_type tenv typ with
   | Typ.Tptr (Tstruct { name = TN_csu (Class _, _) as name }, Pk_pointer) ->
       let class_name = Typename.name name in
       if class_name = JConfig.object_cl then None
@@ -287,6 +287,11 @@ let rec get_all_fields program tenv cn =
   let extract_class_fields classname =
     match get_class_type_no_pointer program tenv classname with
     | Typ.Tstruct { Typ.instance_fields; static_fields } -> (static_fields, instance_fields)
+    | Typ.Tvar name -> (
+        match Tenv.lookup tenv name with
+        | Some { instance_fields; static_fields } -> (static_fields, instance_fields)
+        | None -> assert false
+      )
     | _ -> assert false in
   let trans_fields classname =
     match JClasspath.lookup_node classname program with
@@ -330,6 +335,7 @@ and create_sil_type program tenv cn =
               | Some super_cn ->
                   let super_classname =
                     match get_class_type_no_pointer program tenv super_cn with
+                    | Typ.Tvar name
                     | Typ.Tstruct { name } -> name
                     | _ -> assert false in
                   super_classname :: interface_list in