From 95725e4dd08f2913bf719a2be98e9d51e20a04e2 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 28 Feb 2017 04:28:47 -0800 Subject: [PATCH] Refactor StructTyp to Typ.Struct Summary: Polymorphic models, and type environment refinements, need mutual references between general types and struct types. Reviewed By: cristianoc Differential Revision: D4620076 fbshipit-source-id: f9d01e6 --- infer/src/IR/Sil.re | 2 +- infer/src/IR/StructTyp.re | 141 --------------- infer/src/IR/StructTyp.rei | 66 ------- infer/src/IR/Tenv.re | 10 +- infer/src/IR/Tenv.rei | 16 +- infer/src/IR/Typ.re | 171 +++++++++++++++--- infer/src/IR/Typ.rei | 74 ++++++-- infer/src/backend/absarray.ml | 2 +- infer/src/backend/prop.ml | 4 +- infer/src/backend/prover.ml | 12 +- infer/src/backend/rearrange.ml | 12 +- infer/src/backend/taint.ml | 2 +- infer/src/backend/taint.mli | 2 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 2 +- .../bufferoverrun/bufferOverrunSemantics.ml | 2 +- infer/src/checkers/accessPath.ml | 2 +- infer/src/checkers/annotations.ml | 4 +- infer/src/checkers/annotations.mli | 4 +- infer/src/checkers/checkers.ml | 2 +- infer/src/checkers/patternMatch.ml | 2 +- infer/src/checkers/patternMatch.mli | 4 +- infer/src/clang/CType_decl.ml | 2 +- infer/src/clang/cGeneral_utils.ml | 2 +- infer/src/clang/objcInterface_decl.ml | 4 +- infer/src/eradicate/eradicateChecks.ml | 2 +- infer/src/java/jTrans.ml | 2 +- infer/src/java/jTransType.ml | 2 +- infer/src/java/jTransType.mli | 2 +- 28 files changed, 252 insertions(+), 300 deletions(-) delete mode 100644 infer/src/IR/StructTyp.re delete mode 100644 infer/src/IR/StructTyp.rei diff --git a/infer/src/IR/Sil.re b/infer/src/IR/Sil.re index 3a5746e46..33b8214e5 100644 --- a/infer/src/IR/Sil.re +++ b/infer/src/IR/Sil.re @@ -232,7 +232,7 @@ let has_objc_ref_counter tenv hpred => switch hpred { | Hpointsto _ _ (Sizeof (Tstruct name) _ _) => switch (Tenv.lookup tenv name) { - | Some {fields} => List.exists f::StructTyp.is_objc_ref_counter_field fields + | Some {fields} => List.exists f::Typ.Struct.is_objc_ref_counter_field fields | _ => false } | _ => false diff --git a/infer/src/IR/StructTyp.re b/infer/src/IR/StructTyp.re deleted file mode 100644 index 627cc476f..000000000 --- a/infer/src/IR/StructTyp.re +++ /dev/null @@ -1,141 +0,0 @@ -/* - * Copyright (c) 2009 - 2013 Monoidics ltd. - * Copyright (c) 2013 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - */ -open! IStd; - - -/** The Smallfoot Intermediate Language: Struct Types */ -let module L = Logging; - -let module F = Format; - -type field = (Ident.fieldname, Typ.t, Annot.Item.t) [@@deriving compare]; - -type fields = list field; - - -/** Type for a structured value. */ -type t = { - fields: fields, /** non-static fields */ - statics: fields, /** static fields */ - supers: list Typename.t, /** superclasses */ - methods: list Procname.t, /** methods defined */ - annots: Annot.Item.t /** annotations */ -}; - -type lookup = Typename.t => option t; - -let pp pe name f {fields, supers, methods, annots} => - if Config.debug_mode { - /* change false to true to print the details of struct */ - F.fprintf - f - "%a \n\tfields: {%a\n\t}\n\tsupers: {%a\n\t}\n\tmethods: {%a\n\t}\n\tannots: {%a\n\t}" - Typename.pp - name - ( - Pp.seq ( - fun f (fld, t, _) => F.fprintf f "\n\t\t%a %a" (Typ.pp_full pe) t Ident.pp_fieldname fld - ) - ) - fields - (Pp.seq (fun f n => F.fprintf f "\n\t\t%a" Typename.pp n)) - supers - (Pp.seq (fun f m => F.fprintf f "\n\t\t%a" Procname.pp m)) - methods - Annot.Item.pp - annots - } else { - F.fprintf f "%a" Typename.pp name - }; - -let internal_mk_struct - default::default=? - fields::fields=? - statics::statics=? - methods::methods=? - supers::supers=? - annots::annots=? - () => { - let mk_struct_ - default::default={fields: [], statics: [], methods: [], supers: [], annots: Annot.Item.empty} - fields::fields=default.fields - statics::statics=default.statics - methods::methods=default.methods - supers::supers=default.supers - annots::annots=default.annots - () => { - fields, - statics, - methods, - supers, - annots - }; - mk_struct_ - default::?default - fields::?fields - statics::?statics - methods::?methods - supers::?supers - annots::?annots - () -}; - - -/** the element typ of the final extensible array in the given typ, if any */ -let rec get_extensible_array_element_typ lookup::lookup (typ: Typ.t) => - switch typ { - | Tarray typ _ => Some typ - | Tstruct name => - switch (lookup name) { - | Some {fields} => - switch (List.last fields) { - | Some (_, fld_typ, _) => get_extensible_array_element_typ lookup::lookup fld_typ - | None => None - } - | None => None - } - | _ => None - }; - - -/** If a struct type with field f, return the type of f. If not, return the default */ -let fld_typ lookup::lookup default::default fn (typ: Typ.t) => - switch typ { - | Tstruct name => - switch (lookup name) { - | Some {fields} => - List.find f::(fun (f, _, _) => Ident.equal_fieldname f fn) fields |> - Option.value_map f::snd3 default::default - | None => default - } - | _ => default - }; - -let get_field_type_and_annotation lookup::lookup fn (typ: Typ.t) => - switch typ { - | Tstruct name - | Tptr (Tstruct name) _ => - switch (lookup name) { - | Some {fields, statics} => - List.find_map - f::(fun (f, t, a) => Ident.equal_fieldname f fn ? Some (t, a) : None) (fields @ statics) - | None => None - } - | _ => None - }; - -let objc_ref_counter_annot = [({Annot.class_name: "ref_counter", parameters: []}, false)]; - - -/** Field used for objective-c reference counting */ -let objc_ref_counter_field = (Ident.fieldname_hidden, Typ.Tint IInt, objc_ref_counter_annot); - -let is_objc_ref_counter_field (fld, _, a) => - Ident.fieldname_is_hidden fld && Annot.Item.equal a objc_ref_counter_annot; diff --git a/infer/src/IR/StructTyp.rei b/infer/src/IR/StructTyp.rei deleted file mode 100644 index 507bdd689..000000000 --- a/infer/src/IR/StructTyp.rei +++ /dev/null @@ -1,66 +0,0 @@ -/* - * Copyright (c) 2009 - 2013 Monoidics ltd. - * Copyright (c) 2013 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - */ -open! IStd; - - -/** The Smallfoot Intermediate Language: Struct Types */ -let module F = Format; - -type field = (Ident.fieldname, Typ.t, Annot.Item.t) [@@deriving compare]; - -type fields = list field; - - -/** Type for a structured value. */ -type t = private { - fields: fields, /** non-static fields */ - statics: fields, /** static fields */ - supers: list Typename.t, /** supers */ - methods: list Procname.t, /** methods defined */ - annots: Annot.Item.t /** annotations */ -}; - -type lookup = Typename.t => option t; - - -/** Pretty print a struct type. */ -let pp: Pp.env => Typename.t => F.formatter => t => unit; - - -/** Construct a struct_typ, normalizing field types */ -let internal_mk_struct: - default::t? => - fields::fields? => - statics::fields? => - methods::list Procname.t? => - supers::list Typename.t? => - annots::Annot.Item.t? => - unit => - t; - - -/** the element typ of the final extensible array in the given typ, if any */ -let get_extensible_array_element_typ: lookup::lookup => Typ.t => option Typ.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 fld_typ: lookup::lookup => default::Typ.t => Ident.fieldname => Typ.t => Typ.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: - lookup::lookup => Ident.fieldname => Typ.t => option (Typ.t, Annot.Item.t); - - -/** Field used for objective-c reference counting */ -let objc_ref_counter_field: (Ident.fieldname, Typ.t, Annot.Item.t); - -let is_objc_ref_counter_field: (Ident.fieldname, Typ.t, Annot.Item.t) => bool; diff --git a/infer/src/IR/Tenv.re b/infer/src/IR/Tenv.re index 170815df0..bc98af770 100644 --- a/infer/src/IR/Tenv.re +++ b/infer/src/IR/Tenv.re @@ -22,14 +22,14 @@ let module TypenameHash = Hashtbl.Make { /** Type for type environment. */ -type t = TypenameHash.t StructTyp.t; +type t = TypenameHash.t Typ.Struct.t; let pp fmt (tenv: t) => TypenameHash.iter ( fun name typ => { Format.fprintf fmt "@[<6>NAME: %s@." (Typename.to_string name); - Format.fprintf fmt "@[<6>TYPE: %a@." (StructTyp.pp Pp.text name) typ + Format.fprintf fmt "@[<6>TYPE: %a@." (Typ.Struct.pp Pp.text name) typ } ) tenv; @@ -50,7 +50,7 @@ let mk_struct annots::annots=? name => { let struct_typ = - StructTyp.internal_mk_struct + Typ.Struct.internal_mk_struct default::?default fields::?fields statics::?statics @@ -68,7 +68,7 @@ let mem tenv name => TypenameHash.mem tenv name; /** Look up a name in the global type environment. */ -let lookup tenv name :option StructTyp.t => +let lookup tenv name :option Typ.Struct.t => try (Some (TypenameHash.find tenv name)) { | Not_found => /* ToDo: remove the following additional lookups once C/C++ interop is resolved */ @@ -92,7 +92,7 @@ let add tenv name struct_typ => TypenameHash.replace tenv name struct_typ; /** Get method that is being overriden by java_pname (if any) **/ let get_overriden_method tenv pname_java => { - let struct_typ_get_method_by_name (struct_typ: StructTyp.t) method_name => + let struct_typ_get_method_by_name (struct_typ: Typ.Struct.t) method_name => List.find_exn f::(fun meth => String.equal method_name (Procname.get_method meth)) struct_typ.methods; let rec get_overriden_method_in_supers pname_java supers => diff --git a/infer/src/IR/Tenv.rei b/infer/src/IR/Tenv.rei index 72688f23a..f8980d427 100644 --- a/infer/src/IR/Tenv.rei +++ b/infer/src/IR/Tenv.rei @@ -14,7 +14,7 @@ type t; /** Type for type environment. */ /** Add a (name,typename) pair to the global type environment. */ -let add: t => Typename.t => StructTyp.t => unit; +let add: t => Typename.t => Typ.Struct.t => unit; /** Create a new type environment. */ @@ -22,11 +22,11 @@ let create: unit => t; /** Fold a function over the elements of the type environment. */ -let fold: (Typename.t => StructTyp.t => 'a => 'a) => t => 'a => 'a; +let fold: (Typename.t => Typ.Struct.t => 'a => 'a) => t => 'a => 'a; /** iterate over a type environment */ -let iter: (Typename.t => StructTyp.t => unit) => t => unit; +let iter: (Typename.t => Typ.Struct.t => unit) => t => unit; /** Load a type environment from a file */ @@ -34,20 +34,20 @@ let load_from_file: DB.filename => option t; /** Look up a name in the global type environment. */ -let lookup: t => Typename.t => option StructTyp.t; +let lookup: t => Typename.t => option Typ.Struct.t; /** Construct a struct_typ, normalizing field types */ let mk_struct: t => - default::StructTyp.t? => - fields::StructTyp.fields? => - statics::StructTyp.fields? => + default::Typ.Struct.t? => + fields::Typ.Struct.fields? => + statics::Typ.Struct.fields? => methods::list Procname.t? => supers::list Typename.t? => annots::Annot.Item.t? => Typename.t => - StructTyp.t; + Typ.Struct.t; /** Check if typename is found in t */ diff --git a/infer/src/IR/Typ.re b/infer/src/IR/Typ.re index 5b17ebb3c..7863e9331 100644 --- a/infer/src/IR/Typ.re +++ b/infer/src/IR/Typ.re @@ -122,19 +122,31 @@ let ptr_kind_string = /** statically determined length of an array type, if any */ type static_length = option IntLit.t [@@deriving compare]; +let module T = { + + /** types for sil (structured) expressions */ + type t = + | Tint ikind /** integer type */ + | Tfloat fkind /** float type */ + | Tvoid /** void type */ + | Tfun bool /** function type with noreturn attribute */ + | Tptr t ptr_kind /** pointer type */ + | Tstruct Typename.t /** structured value type name */ + | Tarray t static_length /** array type with statically fixed length */ + [@@deriving compare]; + let equal = [%compare.equal : t]; + let hash = Hashtbl.hash; +}; + +include T; -/** types for sil (structured) expressions */ -type t = - | Tint ikind /** integer type */ - | Tfloat fkind /** float type */ - | Tvoid /** void type */ - | Tfun bool /** function type with noreturn attribute */ - | Tptr t ptr_kind /** pointer type */ - | Tstruct Typename.t /** structured value type name */ - | Tarray t static_length /** array type with statically fixed length */ -[@@deriving compare]; -let equal = [%compare.equal : t]; +/** {2 Sets and maps of types} */ +let module Set = Caml.Set.Make T; + +let module Map = Caml.Map.Make T; + +let module Tbl = Hashtbl.Make T; /** type comparison that treats T* [] and T** as the same type. Needed for C/C++ */ @@ -194,24 +206,6 @@ let d_full (t: t) => L.add_print_action (L.PTtyp_full, Obj.repr t); /** dump a list of types. */ let d_list (tl: list t) => L.add_print_action (L.PTtyp_list, Obj.repr tl); - -/** {2 Sets and maps of types} */ -let module Set = Caml.Set.Make { - type nonrec t = t; - let compare = compare; -}; - -let module Map = Caml.Map.Make { - type nonrec t = t; - let compare = compare; -}; - -let module Tbl = Hashtbl.Make { - type nonrec t = t; - let equal = equal; - let hash = Hashtbl.hash; -}; - let name = fun | Tstruct name => Some name @@ -301,3 +295,122 @@ let java_proc_return_typ pname_java => | Tstruct _ as typ => Tptr typ Pk_pointer | typ => typ }; + +type typ = t; + +let module Struct = { + type field = (Ident.fieldname, T.t, Annot.Item.t) [@@deriving compare]; + type fields = list field; + + /** Type for a structured value. */ + type t = { + fields: fields, /** non-static fields */ + statics: fields, /** static fields */ + supers: list Typename.t, /** superclasses */ + methods: list Procname.t, /** methods defined */ + annots: Annot.Item.t /** annotations */ + }; + type lookup = Typename.t => option t; + let pp pe name f {fields, supers, methods, annots} => + if Config.debug_mode { + /* change false to true to print the details of struct */ + F.fprintf + f + "%a \n\tfields: {%a\n\t}\n\tsupers: {%a\n\t}\n\tmethods: {%a\n\t}\n\tannots: {%a\n\t}" + Typename.pp + name + ( + Pp.seq ( + fun f (fld, t, _) => F.fprintf f "\n\t\t%a %a" (pp_full pe) t Ident.pp_fieldname fld + ) + ) + fields + (Pp.seq (fun f n => F.fprintf f "\n\t\t%a" Typename.pp n)) + supers + (Pp.seq (fun f m => F.fprintf f "\n\t\t%a" Procname.pp m)) + methods + Annot.Item.pp + annots + } else { + F.fprintf f "%a" Typename.pp name + }; + let internal_mk_struct + default::default=? + fields::fields=? + statics::statics=? + methods::methods=? + supers::supers=? + annots::annots=? + () => { + let mk_struct_ + default:: + default={fields: [], statics: [], methods: [], supers: [], annots: Annot.Item.empty} + fields::fields=default.fields + statics::statics=default.statics + methods::methods=default.methods + supers::supers=default.supers + annots::annots=default.annots + () => { + fields, + statics, + methods, + supers, + annots + }; + mk_struct_ + default::?default + fields::?fields + statics::?statics + methods::?methods + supers::?supers + annots::?annots + () + }; + + /** the element typ of the final extensible array in the given typ, if any */ + let rec get_extensible_array_element_typ lookup::lookup (typ: T.t) => + switch typ { + | Tarray typ _ => Some typ + | Tstruct name => + switch (lookup name) { + | Some {fields} => + switch (List.last fields) { + | Some (_, fld_typ, _) => get_extensible_array_element_typ lookup::lookup fld_typ + | None => None + } + | None => None + } + | _ => None + }; + + /** If a struct type with field f, return the type of f. If not, return the default */ + let fld_typ lookup::lookup default::default fn (typ: T.t) => + switch typ { + | Tstruct name => + switch (lookup name) { + | Some {fields} => + List.find f::(fun (f, _, _) => Ident.equal_fieldname f fn) fields |> + Option.value_map f::snd3 default::default + | None => default + } + | _ => default + }; + let get_field_type_and_annotation lookup::lookup fn (typ: T.t) => + switch typ { + | Tstruct name + | Tptr (Tstruct name) _ => + switch (lookup name) { + | Some {fields, statics} => + List.find_map + f::(fun (f, t, a) => Ident.equal_fieldname f fn ? Some (t, a) : None) (fields @ statics) + | None => None + } + | _ => None + }; + let objc_ref_counter_annot = [({Annot.class_name: "ref_counter", parameters: []}, false)]; + + /** Field used for objective-c reference counting */ + let objc_ref_counter_field = (Ident.fieldname_hidden, T.Tint IInt, objc_ref_counter_annot); + let is_objc_ref_counter_field (fld, _, a) => + Ident.fieldname_is_hidden fld && Annot.Item.equal a objc_ref_counter_annot; +}; diff --git a/infer/src/IR/Typ.rei b/infer/src/IR/Typ.rei index 68a30c461..54baaa2d9 100644 --- a/infer/src/IR/Typ.rei +++ b/infer/src/IR/Typ.rei @@ -82,14 +82,24 @@ type t = [@@deriving compare]; -/** type comparison that treats T* [] and T** as the same type. Needed for C/C++ */ -let array_sensitive_compare: t => t => int; - - /** Equality for types. */ let equal: t => t => bool; +/** Sets of types. */ +let module Set: Caml.Set.S with type elt = t; + + +/** Maps with type keys. */ +let module Map: Caml.Map.S with type key = t; + +let module Tbl: Caml.Hashtbl.S with type key = t; + + +/** type comparison that treats T* [] and T** as the same type. Needed for C/C++ */ +let array_sensitive_compare: t => t => int; + + /** Pretty print a type with all the details. */ let pp_full: Pp.env => F.formatter => t => unit; @@ -108,16 +118,6 @@ let d_full: t => unit; let d_list: list t => unit; -/** Sets of types. */ -let module Set: Caml.Set.S with type elt = t; - - -/** Maps with type keys. */ -let module Map: Caml.Map.S with type key = t; - -let module Tbl: Caml.Hashtbl.S with type key = t; - - /** The name of a type */ let name: t => option Typename.t; @@ -151,3 +151,49 @@ let unsome: string => option t => t; /** Return the return type of [pname_java]. */ let java_proc_return_typ: Procname.java => t; + +type typ = t; + +let module Struct: { + type field = (Ident.fieldname, typ, Annot.Item.t) [@@deriving compare]; + type fields = list field; + + /** Type for a structured value. */ + type t = private { + fields: fields, /** non-static fields */ + statics: fields, /** static fields */ + supers: list Typename.t, /** supers */ + methods: list Procname.t, /** methods defined */ + annots: Annot.Item.t /** annotations */ + }; + type lookup = Typename.t => option t; + + /** Pretty print a struct type. */ + let pp: Pp.env => Typename.t => F.formatter => t => unit; + + /** Construct a struct_typ, normalizing field types */ + let internal_mk_struct: + default::t? => + fields::fields? => + statics::fields? => + methods::list Procname.t? => + supers::list Typename.t? => + annots::Annot.Item.t? => + unit => + t; + + /** the element typ of the final extensible array in the given typ, if any */ + let get_extensible_array_element_typ: lookup::lookup => typ => option typ; + + /** 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 fld_typ: lookup::lookup => default::typ => Ident.fieldname => typ => typ; + + /** Return the type of the field [fn] and its annotation, None if [typ] has no field named [fn] */ + let get_field_type_and_annotation: + lookup::lookup => Ident.fieldname => typ => option (typ, Annot.Item.t); + + /** Field used for objective-c reference counting */ + let objc_ref_counter_field: (Ident.fieldname, typ, Annot.Item.t); + let is_objc_ref_counter_field: (Ident.fieldname, typ, Annot.Item.t) => bool; +}; diff --git a/infer/src/backend/absarray.ml b/infer/src/backend/absarray.ml index 167ba6f59..e79fdb71d 100644 --- a/infer/src/backend/absarray.ml +++ b/infer/src/backend/absarray.ml @@ -549,7 +549,7 @@ let check_after_array_abstraction tenv prop = esel | Sil.Estruct (fsel, _) -> List.iter ~f:(fun (f, se) -> - let typ_f = StructTyp.fld_typ ~lookup ~default:Tvoid f typ in + let typ_f = Typ.Struct.fld_typ ~lookup ~default: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/prop.ml b/infer/src/backend/prop.ml index d597e82ff..55cd53372 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -480,7 +480,7 @@ let rec create_strexp_of_type tenv struct_init_mode (typ : Typ.t) len inst : Sil (* pass len as an accumulator, so that it is passed to create_strexp_of_type for the last field, but always return None so that only the last field receives len *) let f (fld, t, a) (flds, len) = - if StructTyp.is_objc_ref_counter_field (fld, t, a) then + if Typ.Struct.is_objc_ref_counter_field (fld, t, a) then ((fld, Sil.Eexp (Exp.one, inst)) :: flds, None) else ((fld, create_strexp_of_type tenv struct_init_mode t len inst) :: flds, None) in @@ -871,7 +871,7 @@ module Normalize = struct (* test if the extensible array at the end of [typ] has elements of type [elt] *) let extensible_array_element_typ_equal elt typ = Option.value_map ~f:(Typ.equal elt) ~default:false - (StructTyp.get_extensible_array_element_typ ~lookup typ) in + (Typ.Struct.get_extensible_array_element_typ ~lookup 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 541c0c834..be7398030 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -395,7 +395,7 @@ end = struct | Sil.Estruct (fsel, _), t -> let get_field_type f = Option.bind t (fun t' -> - Option.map ~f:fst @@ StructTyp.get_field_type_and_annotation ~lookup f t' + Option.map ~f:fst @@ Typ.Struct.get_field_type_and_annotation ~lookup f t' ) in List.iter ~f:(fun (f, se) -> strexp_extract (se, get_field_type f)) fsel | Sil.Earray (len, isel, _), t -> @@ -1333,8 +1333,8 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2 : let se2' = Sil.Earray (len, [(Exp.zero, se2)], inst) in let typ2' = Typ.Tarray (typ2, None) in (* In the sexp_imply, struct_imply, array_imply, and sexp_imply_nolhs functions, the typ2 - argument is only used by eventually passing its value to StructTyp.fld, Exp.Lfield, - StructTyp.fld, or Typ.array_elem. None of these are sensitive to the length field + argument is only used by eventually passing its value to Typ.Struct.fld, Exp.Lfield, + Typ.Struct.fld, or Typ.array_elem. None of these are sensitive to the length field of Tarray, so forgetting the length of typ2' here is not a problem. *) sexp_imply tenv source true calc_missing subs se1 se2' typ2' (* calculate index_frame because the rhs is a singleton array *) | _ -> @@ -1349,7 +1349,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Ide begin match Ident.compare_fieldname f1 f2 with | 0 -> - let typ' = StructTyp.fld_typ ~lookup ~default:Typ.Tvoid f2 typ2 in + let typ' = Typ.Struct.fld_typ ~lookup ~default: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 @@ -1364,7 +1364,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' = StructTyp.fld_typ ~lookup ~default:Typ.Tvoid f2 typ2 in + let typ' = Typ.Struct.fld_typ ~lookup ~default: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 @@ -1372,7 +1372,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' = StructTyp.fld_typ ~lookup ~default:Typ.Tvoid f2 typ2 in + let typ' = Typ.Struct.fld_typ ~lookup ~default: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 diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index f6e736667..ef66c81ed 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -117,7 +117,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp let replace_typ_of_f (f', t', a') = if Ident.equal_fieldname f f' then (f, res_t', a') else (f', t', a') in let fields' = - List.sort ~cmp:StructTyp.compare_field (List.map ~f:replace_typ_of_f fields) in + List.sort ~cmp:Typ.Struct.compare_field (List.map ~f:replace_typ_of_f fields) in ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ; (atoms', se, t) | None -> @@ -226,7 +226,7 @@ let rec _strexp_extend_values let replace_fta ((f1, _, a1) as fta1) = if Ident.equal_fieldname f f1 then (f1, res_typ', a1) else fta1 in let fields' = - List.sort ~cmp:StructTyp.compare_field (List.map ~f:replace_fta fields) in + List.sort ~cmp:Typ.Struct.compare_field (List.map ~f:replace_fta fields) in ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ; (res_atoms', Sil.Estruct (res_fsel', inst'), typ) :: acc in List.fold ~f:replace ~init:[] atoms_se_typ_list' @@ -239,7 +239,7 @@ let rec _strexp_extend_values let replace_fta (f', t', a') = if Ident.equal_fieldname f' f then (f, res_typ', a') else (f', t', a') in let fields' = - List.sort ~cmp:StructTyp.compare_field (List.map ~f:replace_fta fields) in + List.sort ~cmp:Typ.Struct.compare_field (List.map ~f:replace_fta fields) in ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ; [(atoms', Sil.Estruct (res_fsel', inst'), typ)] ) @@ -705,7 +705,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc = List.find_map ~f:annot_suppress_warnings_str item_annot in (* if [fld] is annotated with @GuardedBy("mLock"), return mLock *) let get_guarded_by_fld_str fld typ = - match StructTyp.get_field_type_and_annotation ~lookup fld typ with + match Typ.Struct.get_field_type_and_annotation ~lookup fld typ with | Some (_, item_annot) -> begin match extract_guarded_by_str item_annot with @@ -727,7 +727,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc = let get_fld_strexp_and_typ typ f flds = let match_one (fld, strexp) = - match StructTyp.get_field_type_and_annotation ~lookup fld typ with + match Typ.Struct.get_field_type_and_annotation ~lookup fld typ with | Some (fld_typ, _) when f fld fld_typ -> Some (strexp, fld_typ) | _ -> None in List.find_map ~f:match_one flds in @@ -1328,7 +1328,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 StructTyp.get_field_type_and_annotation ~lookup fld typ with + match Typ.Struct.get_field_type_and_annotation ~lookup 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/taint.ml b/infer/src/backend/taint.ml index e42ce65d5..88849176b 100644 --- a/infer/src/backend/taint.ml +++ b/infer/src/backend/taint.ml @@ -348,7 +348,7 @@ let tainted_params callee_pname = List.map ~f:(fun param_num -> param_num, taint_info.PredSymb.taint_kind) tainted_param_indices | None -> [] -let has_taint_annotation fieldname (struct_typ: StructTyp.t) = +let has_taint_annotation fieldname (struct_typ: Typ.Struct.t) = let fld_has_taint_annot (fname, _, annot) = Ident.equal_fieldname fieldname fname && (Annotations.ia_is_privacy_source annot || Annotations.ia_is_integrity_source annot) in diff --git a/infer/src/backend/taint.mli b/infer/src/backend/taint.mli index a834bae89..cb6852fc0 100644 --- a/infer/src/backend/taint.mli +++ b/infer/src/backend/taint.mli @@ -21,7 +21,7 @@ val accepts_sensitive_params : val tainted_params : Procname.t -> (int * PredSymb.taint_kind) list (** returns the taint_kind of [fieldname] if it has a taint source annotation *) -val has_taint_annotation : Ident.fieldname -> StructTyp.t -> bool +val has_taint_annotation : Ident.fieldname -> Typ.Struct.t -> bool val add_tainting_attribute : Tenv.t -> PredSymb.t -> Pvar.t -> Prop.normal Prop.t -> Prop.normal Prop.t diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 9c5010813..a26b984ec 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -161,7 +161,7 @@ struct | Typ.Tstruct typename -> (match Tenv.lookup tenv typename with | Some str -> - List.fold ~f:decl_fld ~init:(mem, sym_num + 6) str.StructTyp.fields + List.fold ~f:decl_fld ~init:(mem, sym_num + 6) str.Typ.Struct.fields | _ -> (mem, sym_num + 6)) | _ -> (mem, sym_num + 6) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index af4c7bdcc..70aaa4945 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -298,7 +298,7 @@ struct | Typ.Tptr (Typ.Tstruct typename, _) -> (match Tenv.lookup tenv typename with | Some str -> - let fns = List.map ~f:get_field_name str.StructTyp.fields in + let fns = List.map ~f:get_field_name str.Typ.Struct.fields in List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns | _ -> pairs) | Typ.Tptr (_ ,_) -> diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 130a8a061..42cafa5a0 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -61,7 +61,7 @@ module Raw = struct | FieldAccess field_name :: accesses -> let lookup = Tenv.lookup tenv in begin - match StructTyp.get_field_type_and_annotation ~lookup field_name last_typ with + match Typ.Struct.get_field_type_and_annotation ~lookup field_name last_typ with | Some (field_typ, _) -> accesses_get_typ field_typ tenv accesses | None -> None end diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index 99e9c0d8d..745424d6b 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -108,13 +108,13 @@ let pname_has_return_annot pname ~attrs_of_pname predicate = | Some attributes -> predicate (fst attributes.ProcAttributes.method_annotation) | None -> false -let field_has_annot fieldname (struct_typ : StructTyp.t) predicate = +let field_has_annot fieldname (struct_typ : Typ.Struct.t) predicate = let fld_has_taint_annot (fname, _, annot) = Ident.equal_fieldname fieldname fname && predicate annot in List.exists ~f:fld_has_taint_annot struct_typ.fields || List.exists ~f:fld_has_taint_annot struct_typ.statics -let struct_typ_has_annot (struct_typ : StructTyp.t) predicate = +let struct_typ_has_annot (struct_typ : Typ.Struct.t) predicate = predicate struct_typ.annots let ia_is_not_thread_safe ia = diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index 9f077f05f..cc9d84603 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -105,7 +105,7 @@ val pdesc_return_annot_ends_with : Procdesc.t -> string -> bool val ma_has_annotation_with : Annot.Method.t -> (Annot.t -> bool) -> bool -val field_has_annot : Ident.fieldname -> StructTyp.t -> (Annot.Item.t -> bool) -> bool +val field_has_annot : Ident.fieldname -> Typ.Struct.t -> (Annot.Item.t -> bool) -> bool (** return true if the given predicate evaluates to true on some annotation of [struct_typ] *) -val struct_typ_has_annot : StructTyp.t -> (Annot.Item.t -> bool) -> bool +val struct_typ_has_annot : Typ.Struct.t -> (Annot.Item.t -> bool) -> bool diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index 8da72352e..aa2b6e11a 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -104,7 +104,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 StructTyp.get_field_type_and_annotation ~lookup field_name t with + match Typ.Struct.get_field_type_and_annotation ~lookup field_name t with | Some (_, ia) -> Annotations.ia_has_annotation_with ia annotation_matches | None -> false end diff --git a/infer/src/checkers/patternMatch.ml b/infer/src/checkers/patternMatch.ml index 342e8510d..a05f67d8e 100644 --- a/infer/src/checkers/patternMatch.ml +++ b/infer/src/checkers/patternMatch.ml @@ -388,7 +388,7 @@ let is_throwable tenv typename = including for supertypes*) let check_class_attributes check tenv = function | Procname.Java java_pname -> - let check_class_annots _ { StructTyp.annots; } = check annots in + let check_class_annots _ { Typ.Struct.annots; } = check annots in supertype_exists tenv check_class_annots (Procname.java_get_class_type_name java_pname) diff --git a/infer/src/checkers/patternMatch.mli b/infer/src/checkers/patternMatch.mli index f09d5e61c..db2197670 100644 --- a/infer/src/checkers/patternMatch.mli +++ b/infer/src/checkers/patternMatch.mli @@ -60,12 +60,12 @@ val is_subtype : Tenv.t -> Typename.t -> Typename.t -> bool val is_subtype_of_str : Tenv.t -> Typename.t -> string -> bool (** Holds iff the predicate holds on a supertype of the named type, including the type itself *) -val supertype_exists : Tenv.t -> (Typename.t -> StructTyp.t -> bool) -> Typename.t -> bool +val supertype_exists : Tenv.t -> (Typename.t -> Typ.Struct.t -> bool) -> Typename.t -> bool (** Return the first non-None result found when applying the given function to supertypes of the named type, including the type itself *) val supertype_find_map_opt : - Tenv.t -> (Typename.t -> StructTyp.t -> 'a option) -> Typename.t -> 'a option + Tenv.t -> (Typename.t -> Typ.Struct.t -> 'a option) -> Typename.t -> 'a option (** Get the name of the type of a constant *) val java_get_const_type_name : Const.t -> string diff --git a/infer/src/clang/CType_decl.ml b/infer/src/clang/CType_decl.ml index bba6dad9f..10b3fe6b3 100644 --- a/infer/src/clang/CType_decl.ml +++ b/infer/src/clang/CType_decl.ml @@ -178,7 +178,7 @@ and get_record_struct_type tenv definition_decl = | None -> let is_complete_definition = record_decl_info.Clang_ast_t.rdi_is_complete_definition in let extra_fields = if CTrans_models.is_objc_memory_model_controlled name then - [StructTyp.objc_ref_counter_field] + [Typ.Struct.objc_ref_counter_field] else [] in let annots = if Csu.equal csu (Csu.Class Csu.CPP) then Annot.Class.cpp diff --git a/infer/src/clang/cGeneral_utils.ml b/infer/src/clang/cGeneral_utils.ml index edbaa3c6a..28052bd95 100644 --- a/infer/src/clang/cGeneral_utils.ml +++ b/infer/src/clang/cGeneral_utils.ml @@ -75,7 +75,7 @@ let sort_fields fields = let sort_fields_tenv tenv = - let sort_fields_struct name ({StructTyp.fields} as st) = + let sort_fields_struct name ({Typ.Struct.fields} as st) = ignore (Tenv.mk_struct tenv ~default:st ~fields:(sort_fields fields) name) in Tenv.iter sort_fields_struct tenv diff --git a/infer/src/clang/objcInterface_decl.ml b/infer/src/clang/objcInterface_decl.ml index 579de7e90..669fdda8e 100644 --- a/infer/src/clang/objcInterface_decl.ml +++ b/infer/src/clang/objcInterface_decl.ml @@ -118,7 +118,7 @@ let add_class_to_tenv type_ptr_to_sil_type tenv curr_class decl_info name_info d decl_fields, decl_supers, decl_methods in let fields = CGeneral_utils.append_no_duplicates_fields fields fields_sc in (* We add the special hidden counter_field for implementing reference counting *) - let modelled_fields = StructTyp.objc_ref_counter_field :: CField_decl.modelled_field name_info in + let modelled_fields = Typ.Struct.objc_ref_counter_field :: CField_decl.modelled_field name_info in let all_fields = CGeneral_utils.append_no_duplicates_fields modelled_fields fields in Logging.out_debug "Class %s field:\n" class_name; List.iter ~f:(fun (fn, _, _) -> @@ -131,7 +131,7 @@ let add_class_to_tenv type_ptr_to_sil_type tenv curr_class decl_info name_info d (match Tenv.lookup tenv interface_name with | Some st -> Logging.out_debug " >>>OK. Found typ='%a'\n" - (StructTyp.pp Pp.text interface_name) st + (Typ.Struct.pp Pp.text interface_name) st | None -> Logging.out_debug " >>>NOT Found!!\n"); Typ.Tstruct interface_name diff --git a/infer/src/eradicate/eradicateChecks.ml b/infer/src/eradicate/eradicateChecks.ml index 3ac38e1af..3fa7ad326 100644 --- a/infer/src/eradicate/eradicateChecks.ml +++ b/infer/src/eradicate/eradicateChecks.ml @@ -22,7 +22,7 @@ let check_library_calls = false let get_field_annotation tenv fn typ = let lookup = Tenv.lookup tenv in - match StructTyp.get_field_type_and_annotation ~lookup fn typ with + match Typ.Struct.get_field_type_and_annotation ~lookup fn typ with | None -> None | Some (t, ia) -> let ia' = diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index d1efc27cb..9378288ee 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -105,7 +105,7 @@ let retrieve_fieldname fieldname = let get_field_name program static tenv cn fs = - let { StructTyp.fields; statics; } = JTransType.get_class_struct_typ program tenv cn in + let { Typ.Struct.fields; statics; } = JTransType.get_class_struct_typ program tenv cn in match List.find ~f:(fun (fieldname, _, _) -> String.equal (retrieve_fieldname fieldname) (JBasics.fs_name fs)) diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 7621dc8bf..feb65c52d 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -282,7 +282,7 @@ let add_model_fields program classpath_fields cn = let rec get_all_fields program tenv cn = let extract_class_fields classname = - let { StructTyp.fields; statics } = get_class_struct_typ program tenv classname in + let { Typ.Struct.fields; statics } = get_class_struct_typ program tenv classname in (statics, fields) in let trans_fields classname = match JClasspath.lookup_node classname program with diff --git a/infer/src/java/jTransType.mli b/infer/src/java/jTransType.mli index 68fa7fc27..86946ab71 100644 --- a/infer/src/java/jTransType.mli +++ b/infer/src/java/jTransType.mli @@ -32,7 +32,7 @@ val get_method_procname : val translate_method_name : JCode.jcode Javalib.jmethod -> Procname.t (** [get_class_struct_typ program tenv cn] returns the struct_typ representation of the class *) -val get_class_struct_typ: JClasspath.program -> Tenv.t -> JBasics.class_name -> StructTyp.t +val get_class_struct_typ: JClasspath.program -> Tenv.t -> JBasics.class_name -> Typ.Struct.t (** [get_class_type_no_pointer program tenv cn] returns the sil type representation of the class without the pointer part *)