diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index afa631ab9..15b170c04 100644 --- a/infer/src/IR/Cfg.re +++ b/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 => diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 05a42cd14..0e5c64cc0 100644 --- a/infer/src/IR/Sil.re +++ b/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 }; diff --git a/infer/src/IR/Tenv.re b/infer/src/IR/Tenv.re index f7ce17c60..bae45213b 100644 --- a/infer/src/IR/Tenv.re +++ b/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) { - | Some struct_typ => Some (Typ.Tstruct struct_typ) - | None => None - } + 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; diff --git a/infer/src/IR/Tenv.rei b/infer/src/IR/Tenv.rei index 0cb0671dc..f4afbb4d0 100644 --- a/infer/src/IR/Tenv.rei +++ b/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; diff --git a/infer/src/IR/Typ.re b/infer/src/IR/Typ.re index 4f78bd401..2b3667e9d 100644 --- a/infer/src/IR/Typ.re +++ b/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 }; diff --git a/infer/src/IR/Typ.rei b/infer/src/IR/Typ.rei index b6f72ded4..6a5f37877 100644 --- a/infer/src/IR/Typ.rei +++ b/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; diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index b67c8a7b0..050324d79 100644 --- a/infer/src/backend/abs.ml +++ b/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') -> diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml index b317e01f8..5b707982f 100644 --- a/infer/src/backend/absarray.ml +++ b/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) -> diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 9a7b3bd62..1b65fc01c 100644 --- a/infer/src/backend/errdesc.ml +++ b/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 - let _, t, _ = - IList.find (fun (f', _, _) -> - Ident.fieldname_equal f' f) - struct_typ.Typ.instance_fields in - Some t - with Not_found -> None) + | 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) + instance_fields in + Some t + with Not_found -> None + ) + | _ -> + None + ) | _ -> None in res := Some (DExp.Ddot (DExp.Dpvar pv, f)), typo | Exp.Var id -> diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 318cc9a18..6e369ae38 100644 --- a/infer/src/backend/interproc.ml +++ b/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, _), _, _)) - when AndroidFramework.is_context tenv struct_typ && - not (AndroidFramework.is_application tenv struct_typ) -> - (exp, struct_typ) :: exps + | 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 diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index 7492bf4b6..14fb85fad 100644 --- a/infer/src/backend/localise.ml +++ b/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 = diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml index 23c410af2..985bb60b5 100644 --- a/infer/src/backend/modelBuiltins.ml +++ b/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 diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 608516ed0..542688c3e 100644 --- a/infer/src/backend/prop.ml +++ b/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: diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 7874b3a4a..e511bef27 100644 --- a/infer/src/backend/prover.ml +++ b/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 diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 996de2614..0c045955c 100644 --- a/infer/src/backend/rearrange.ml +++ b/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,16 +1081,21 @@ 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)) :: _ -> - (* access through field: get the struct type from the field *) - if Config.trace_rearrange then begin - L.d_increase_indent 1; - L.d_str "iter_rearrange: root of lexp accesses field "; L.d_strln (Ident.fieldname_to_string f); - L.d_str " struct type from field: "; Typ.d_full struct_typ; L.d_ln(); - L.d_decrease_indent 1; - L.d_ln(); - end; - 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; + L.d_str "iter_rearrange: root of lexp accesses field "; L.d_strln (Ident.fieldname_to_string f); + L.d_str " struct type from field: "; Typ.d_full struct_typ; L.d_ln(); + L.d_decrease_indent 1; + 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) = diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 1d0d1e677..1d20aae8e 100644 --- a/infer/src/backend/symExec.ml +++ b/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 *) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 9c8be1bce..3cb6d3632 100644 --- a/infer/src/backend/tabulation.ml +++ b/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 diff --git a/infer/src/backend/taint.ml b/infer/src/backend/taint.ml index ea7f6b3be..1bfaa06e2 100644 --- a/infer/src/backend/taint.ml +++ b/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 diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index 0cff9bc8c..1db65026f 100644 --- a/infer/src/checkers/checkers.ml +++ b/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 diff --git a/infer/src/checkers/fragmentRetainsViewChecker.ml b/infer/src/checkers/fragmentRetainsViewChecker.ml index 3722ec9c2..924b54db3 100644 --- a/infer/src/checkers/fragmentRetainsViewChecker.ml +++ b/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 diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index b095e9044..c857487f8 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/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 diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index a1bf71e27..dea69f64f 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/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 diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index d6e848e6d..b201e1d07 100644 --- a/infer/src/clang/cTrans.ml +++ b/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) -> diff --git a/infer/src/clang/objcInterface_decl.ml b/infer/src/clang/objcInterface_decl.ml index 6ed249b99..c02894b3e 100644 --- a/infer/src/clang/objcInterface_decl.ml +++ b/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 = diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml index 20489622d..149fa963e 100644 --- a/infer/src/eradicate/eradicateChecks.ml +++ b/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 diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 8a80b8b7e..772a84c77 100644 --- a/infer/src/harness/inhabit.ml +++ b/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 = diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index e88200ee1..b545b6e4e 100644 --- a/infer/src/java/jTrans.ml +++ b/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 diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 64a30bdb3..1abb12743 100644 --- a/infer/src/java/jTransType.ml +++ b/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