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
master
Josh Berdine 8 years ago committed by Facebook Github Bot
parent f5bb35e245
commit 95725e4dd0

@ -232,7 +232,7 @@ let has_objc_ref_counter tenv hpred =>
switch hpred { switch hpred {
| Hpointsto _ _ (Sizeof (Tstruct name) _ _) => | Hpointsto _ _ (Sizeof (Tstruct name) _ _) =>
switch (Tenv.lookup tenv 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
} }
| _ => false | _ => false

@ -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;

@ -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;

@ -22,14 +22,14 @@ let module TypenameHash = Hashtbl.Make {
/** Type for type environment. */ /** Type for type environment. */
type t = TypenameHash.t StructTyp.t; type t = TypenameHash.t Typ.Struct.t;
let pp fmt (tenv: t) => let pp fmt (tenv: t) =>
TypenameHash.iter TypenameHash.iter
( (
fun name typ => { fun name typ => {
Format.fprintf fmt "@[<6>NAME: %s@." (Typename.to_string name); 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; tenv;
@ -50,7 +50,7 @@ let mk_struct
annots::annots=? annots::annots=?
name => { name => {
let struct_typ = let struct_typ =
StructTyp.internal_mk_struct Typ.Struct.internal_mk_struct
default::?default default::?default
fields::?fields fields::?fields
statics::?statics statics::?statics
@ -68,7 +68,7 @@ let mem tenv name => TypenameHash.mem tenv name;
/** Look up a name in the global type environment. */ /** 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)) { try (Some (TypenameHash.find tenv name)) {
| Not_found => | Not_found =>
/* ToDo: remove the following additional lookups once C/C++ interop is resolved */ /* 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) **/ /** Get method that is being overriden by java_pname (if any) **/
let get_overriden_method tenv pname_java => { 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 List.find_exn
f::(fun meth => String.equal method_name (Procname.get_method meth)) struct_typ.methods; f::(fun meth => String.equal method_name (Procname.get_method meth)) struct_typ.methods;
let rec get_overriden_method_in_supers pname_java supers => let rec get_overriden_method_in_supers pname_java supers =>

@ -14,7 +14,7 @@ type t; /** Type for type environment. */
/** Add a (name,typename) pair to the global 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. */ /** Create a new type environment. */
@ -22,11 +22,11 @@ let create: unit => t;
/** Fold a function over the elements of the type environment. */ /** 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 */ /** 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 */ /** 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. */ /** 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 */ /** Construct a struct_typ, normalizing field types */
let mk_struct: let mk_struct:
t => t =>
default::StructTyp.t? => default::Typ.Struct.t? =>
fields::StructTyp.fields? => fields::Typ.Struct.fields? =>
statics::StructTyp.fields? => statics::Typ.Struct.fields? =>
methods::list Procname.t? => methods::list Procname.t? =>
supers::list Typename.t? => supers::list Typename.t? =>
annots::Annot.Item.t? => annots::Annot.Item.t? =>
Typename.t => Typename.t =>
StructTyp.t; Typ.Struct.t;
/** Check if typename is found in t */ /** Check if typename is found in t */

@ -122,19 +122,31 @@ let ptr_kind_string =
/** statically determined length of an array type, if any */ /** statically determined length of an array type, if any */
type static_length = option IntLit.t [@@deriving compare]; 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++ */ /** 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. */ /** dump a list of types. */
let d_list (tl: list t) => L.add_print_action (L.PTtyp_list, Obj.repr tl); 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 = let name =
fun fun
| Tstruct name => Some name | Tstruct name => Some name
@ -301,3 +295,122 @@ let java_proc_return_typ pname_java =>
| Tstruct _ as typ => Tptr typ Pk_pointer | Tstruct _ as typ => Tptr typ Pk_pointer
| typ => typ | 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;
};

@ -82,14 +82,24 @@ type t =
[@@deriving compare]; [@@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. */ /** Equality for types. */
let equal: t => t => bool; 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. */ /** Pretty print a type with all the details. */
let pp_full: Pp.env => F.formatter => t => unit; let pp_full: Pp.env => F.formatter => t => unit;
@ -108,16 +118,6 @@ let d_full: t => unit;
let d_list: list 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 */ /** The name of a type */
let name: t => option Typename.t; let name: t => option Typename.t;
@ -151,3 +151,49 @@ let unsome: string => option t => t;
/** Return the return type of [pname_java]. */ /** Return the return type of [pname_java]. */
let java_proc_return_typ: Procname.java => t; 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;
};

@ -549,7 +549,7 @@ let check_after_array_abstraction tenv prop =
esel esel
| Sil.Estruct (fsel, _) -> | Sil.Estruct (fsel, _) ->
List.iter ~f:(fun (f, se) -> 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 check_se root (offs @ [Sil.Off_fld (f, typ)]) typ_f se) fsel in
let check_hpred = function let check_hpred = function
| Sil.Hpointsto (root, se, texp) -> | Sil.Hpointsto (root, se, texp) ->

@ -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 (* 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 *) field, but always return None so that only the last field receives len *)
let f (fld, t, a) (flds, 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) ((fld, Sil.Eexp (Exp.one, inst)) :: flds, None)
else else
((fld, create_strexp_of_type tenv struct_init_mode t len inst) :: flds, None) in ((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] *) (* test if the extensible array at the end of [typ] has elements of type [elt] *)
let extensible_array_element_typ_equal elt typ = let extensible_array_element_typ_equal elt typ =
Option.value_map ~f:(Typ.equal elt) ~default:false 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 begin
match e1', e2' with match e1', e2' with
(* pattern for arrays and extensible structs: (* pattern for arrays and extensible structs:

@ -395,7 +395,7 @@ end = struct
| Sil.Estruct (fsel, _), t -> | Sil.Estruct (fsel, _), t ->
let get_field_type f = let get_field_type f =
Option.bind t (fun t' -> 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 ) in
List.iter ~f:(fun (f, se) -> strexp_extract (se, get_field_type f)) fsel List.iter ~f:(fun (f, se) -> strexp_extract (se, get_field_type f)) fsel
| Sil.Earray (len, isel, _), t -> | 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 se2' = Sil.Earray (len, [(Exp.zero, se2)], inst) in
let typ2' = Typ.Tarray (typ2, None) in let typ2' = Typ.Tarray (typ2, None) in
(* In the sexp_imply, struct_imply, array_imply, and sexp_imply_nolhs functions, the typ2 (* 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, argument is only used by eventually passing its value to Typ.Struct.fld, Exp.Lfield,
StructTyp.fld, or Typ.array_elem. None of these are sensitive to the length field 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. *) 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 *) 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 begin
match Ident.compare_fieldname f1 f2 with match Ident.compare_fieldname f1 f2 with
| 0 -> | 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 = let subs', se_frame, se_missing =
sexp_imply tenv (Exp.Lfield (source, f2, typ2)) false calc_missing subs se1 se2 typ' in 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 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 let subs', fld_frame, fld_missing = struct_imply tenv source calc_missing subs fsel1' fsel2 typ2 in
subs', ((f1, se1) :: fld_frame), fld_missing 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' = let subs' =
sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' in 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 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' subs', fld_frame, fld_missing'
end end
| [], (f2, se2) :: fsel2' -> | [], (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' = 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 let subs'', fld_frame, fld_missing = struct_imply tenv source calc_missing subs' [] fsel2' typ2 in
subs'', fld_frame, (f2, se2):: fld_missing subs'', fld_frame, (f2, se2):: fld_missing

@ -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') = let replace_typ_of_f (f', t', a') =
if Ident.equal_fieldname f f' then (f, res_t', a') else (f', t', a') in if Ident.equal_fieldname f f' then (f, res_t', a') else (f', t', a') in
let fields' = 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) ; ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ;
(atoms', se, t) (atoms', se, t)
| None -> | None ->
@ -226,7 +226,7 @@ let rec _strexp_extend_values
let replace_fta ((f1, _, a1) as fta1) = let replace_fta ((f1, _, a1) as fta1) =
if Ident.equal_fieldname f f1 then (f1, res_typ', a1) else fta1 in if Ident.equal_fieldname f f1 then (f1, res_typ', a1) else fta1 in
let fields' = 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) ; ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ;
(res_atoms', Sil.Estruct (res_fsel', inst'), typ) :: acc in (res_atoms', Sil.Estruct (res_fsel', inst'), typ) :: acc in
List.fold ~f:replace ~init:[] atoms_se_typ_list' List.fold ~f:replace ~init:[] atoms_se_typ_list'
@ -239,7 +239,7 @@ let rec _strexp_extend_values
let replace_fta (f', t', a') = let replace_fta (f', t', a') =
if Ident.equal_fieldname f' f then (f, res_typ', a') else (f', t', a') in if Ident.equal_fieldname f' f then (f, res_typ', a') else (f', t', a') in
let fields' = 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) ; ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ;
[(atoms', Sil.Estruct (res_fsel', inst'), typ)] [(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 List.find_map ~f:annot_suppress_warnings_str item_annot in
(* if [fld] is annotated with @GuardedBy("mLock"), return mLock *) (* if [fld] is annotated with @GuardedBy("mLock"), return mLock *)
let get_guarded_by_fld_str fld typ = 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) -> | Some (_, item_annot) ->
begin begin
match extract_guarded_by_str item_annot with 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 get_fld_strexp_and_typ typ f flds =
let match_one (fld, strexp) = 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) | Some (fld_typ, _) when f fld fld_typ -> Some (strexp, fld_typ)
| _ -> None in | _ -> None in
List.find_map ~f:match_one flds 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 is_nullable || Pvar.is_local pvar
| Sil.Hpointsto (_, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) -> | Sil.Hpointsto (_, Sil.Estruct (flds, _), Exp.Sizeof (typ, _, _)) ->
let fld_is_nullable fld = 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 | Some (_, annot) -> Annotations.ia_is_nullable annot
| _ -> false in | _ -> false in
let is_strexp_pt_by_nullable_fld (fld, strexp) = let is_strexp_pt_by_nullable_fld (fld, strexp) =

@ -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 List.map ~f:(fun param_num -> param_num, taint_info.PredSymb.taint_kind) tainted_param_indices
| None -> [] | 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) = let fld_has_taint_annot (fname, _, annot) =
Ident.equal_fieldname fieldname fname && Ident.equal_fieldname fieldname fname &&
(Annotations.ia_is_privacy_source annot || Annotations.ia_is_integrity_source annot) in (Annotations.ia_is_privacy_source annot || Annotations.ia_is_integrity_source annot) in

@ -21,7 +21,7 @@ val accepts_sensitive_params :
val tainted_params : Procname.t -> (int * PredSymb.taint_kind) list val tainted_params : Procname.t -> (int * PredSymb.taint_kind) list
(** returns the taint_kind of [fieldname] if it has a taint source annotation *) (** 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 val add_tainting_attribute : Tenv.t -> PredSymb.t -> Pvar.t -> Prop.normal Prop.t -> Prop.normal Prop.t

@ -161,7 +161,7 @@ struct
| Typ.Tstruct typename -> | Typ.Tstruct typename ->
(match Tenv.lookup tenv typename with (match Tenv.lookup tenv typename with
| Some str -> | 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))
| _ -> (mem, sym_num + 6) | _ -> (mem, sym_num + 6)

@ -298,7 +298,7 @@ struct
| Typ.Tptr (Typ.Tstruct typename, _) -> | Typ.Tptr (Typ.Tstruct typename, _) ->
(match Tenv.lookup tenv typename with (match Tenv.lookup tenv typename with
| Some str -> | 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 List.fold ~f:(add_pair_field v1 v2) ~init:pairs fns
| _ -> pairs) | _ -> pairs)
| Typ.Tptr (_ ,_) -> | Typ.Tptr (_ ,_) ->

@ -61,7 +61,7 @@ module Raw = struct
| FieldAccess field_name :: accesses -> | FieldAccess field_name :: accesses ->
let lookup = Tenv.lookup tenv in let lookup = Tenv.lookup tenv in
begin 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 | Some (field_typ, _) -> accesses_get_typ field_typ tenv accesses
| None -> None | None -> None
end end

@ -108,13 +108,13 @@ let pname_has_return_annot pname ~attrs_of_pname predicate =
| Some attributes -> predicate (fst attributes.ProcAttributes.method_annotation) | Some attributes -> predicate (fst attributes.ProcAttributes.method_annotation)
| None -> false | 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) = let fld_has_taint_annot (fname, _, annot) =
Ident.equal_fieldname fieldname fname && predicate annot in 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.fields ||
List.exists ~f:fld_has_taint_annot struct_typ.statics 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 predicate struct_typ.annots
let ia_is_not_thread_safe ia = let ia_is_not_thread_safe ia =

@ -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 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] *) (** 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

@ -104,7 +104,7 @@ module ST = struct
let is_field_suppressed = let is_field_suppressed =
match field_name, PatternMatch.get_this_type proc_attributes with match field_name, PatternMatch.get_this_type proc_attributes with
| Some field_name, Some t -> begin | 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 | Some (_, ia) -> Annotations.ia_has_annotation_with ia annotation_matches
| None -> false | None -> false
end end

@ -388,7 +388,7 @@ let is_throwable tenv typename =
including for supertypes*) including for supertypes*)
let check_class_attributes check tenv = function let check_class_attributes check tenv = function
| Procname.Java java_pname -> | 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 supertype_exists tenv
check_class_annots check_class_annots
(Procname.java_get_class_type_name java_pname) (Procname.java_get_class_type_name java_pname)

@ -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 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 *) (** 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 (** Return the first non-None result found when applying the given function to supertypes of the
named type, including the type itself *) named type, including the type itself *)
val supertype_find_map_opt : 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 *) (** Get the name of the type of a constant *)
val java_get_const_type_name : Const.t -> string val java_get_const_type_name : Const.t -> string

@ -178,7 +178,7 @@ and get_record_struct_type tenv definition_decl =
| None -> | None ->
let is_complete_definition = record_decl_info.Clang_ast_t.rdi_is_complete_definition in 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 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 else [] in
let annots = let annots =
if Csu.equal csu (Csu.Class Csu.CPP) then Annot.Class.cpp if Csu.equal csu (Csu.Class Csu.CPP) then Annot.Class.cpp

@ -75,7 +75,7 @@ let sort_fields fields =
let sort_fields_tenv tenv = 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 ignore (Tenv.mk_struct tenv ~default:st ~fields:(sort_fields fields) name) in
Tenv.iter sort_fields_struct tenv Tenv.iter sort_fields_struct tenv

@ -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 decl_fields, decl_supers, decl_methods in
let fields = CGeneral_utils.append_no_duplicates_fields fields fields_sc in let fields = CGeneral_utils.append_no_duplicates_fields fields fields_sc in
(* We add the special hidden counter_field for implementing reference counting *) (* 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 let all_fields = CGeneral_utils.append_no_duplicates_fields modelled_fields fields in
Logging.out_debug "Class %s field:\n" class_name; Logging.out_debug "Class %s field:\n" class_name;
List.iter ~f:(fun (fn, _, _) -> 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 (match Tenv.lookup tenv interface_name with
| Some st -> | Some st ->
Logging.out_debug " >>>OK. Found typ='%a'\n" 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"); | None -> Logging.out_debug " >>>NOT Found!!\n");
Typ.Tstruct interface_name Typ.Tstruct interface_name

@ -22,7 +22,7 @@ let check_library_calls = false
let get_field_annotation tenv fn typ = let get_field_annotation tenv fn typ =
let lookup = Tenv.lookup tenv in 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 | None -> None
| Some (t, ia) -> | Some (t, ia) ->
let ia' = let ia' =

@ -105,7 +105,7 @@ let retrieve_fieldname fieldname =
let get_field_name program static tenv cn fs = 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 match
List.find List.find
~f:(fun (fieldname, _, _) -> String.equal (retrieve_fieldname fieldname) (JBasics.fs_name fs)) ~f:(fun (fieldname, _, _) -> String.equal (retrieve_fieldname fieldname) (JBasics.fs_name fs))

@ -282,7 +282,7 @@ let add_model_fields program classpath_fields cn =
let rec get_all_fields program tenv cn = let rec get_all_fields program tenv cn =
let extract_class_fields classname = 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 (statics, fields) in
let trans_fields classname = let trans_fields classname =
match JClasspath.lookup_node classname program with match JClasspath.lookup_node classname program with

@ -32,7 +32,7 @@ val get_method_procname :
val translate_method_name : JCode.jcode Javalib.jmethod -> Procname.t 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 *) (** [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 (** [get_class_type_no_pointer program tenv cn] returns the sil type representation of the class
without the pointer part *) without the pointer part *)

Loading…
Cancel
Save