pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Remove Tstruct in favor of Tvar

Browse Source 
Summary:
This diff removes the redundancy in the representation of types where
struct types could be represented either directly using Tstruct or
indirectly using Tvar to refer to the type environment.  A consequence
is that it is much harder to construct large type values.

Reviewed By: sblackshear, cristianoc

Differential Revision: D3839753

fbshipit-source-id: cf04ea5
master
Josh Berdine 9 years ago committed by Facebook Github Bot 6
parent 050d90b356
commit 8589dc4868
58 changed files with 979 additions and 1136 deletions
Show Stats Download Patch File Download Diff File

14
infer/src/IR/AttributesTable.re
Unescape View File

@ -106,13 +106,13 @@ let get_tenv proc_name =>
/** Given the name of an ObjC class, extract the type from the tenv where the class was defined. We
do this by adding a method that is unique to each class, and then finding the tenv that
corresponds to the class definition. */
let get_correct_type_from_objc_class_name type_name => {
let class_method = Procname.get_default_objc_class_method (Typename.name type_name);
switch (find_tenv_from_class_of_proc class_method) {
| None => None
| Some tenv => Option.map (fun st => Typ.Tstruct st) (Tenv.lookup tenv type_name)
}
};
let get_correct_type_from_objc_class_name type_name =>
/* ToDo: this function should return a type that includes a reference to the tenv computed by:
let class_method = Procname.get_default_objc_class_method (Typename.name type_name);
switch (find_tenv_from_class_of_proc class_method) {
| Some tenv =>
*/
Some (Typ.Tstruct type_name);
/** Returns true if the method is defined as a C++ model */

2
infer/src/IR/Cfg.re
Unescape View File

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

10
infer/src/IR/Sil.re
Unescape View File

@ -183,9 +183,9 @@ let hpred_get_lhs h =>
/** {2 Comparision and Inspection Functions} */
let has_objc_ref_counter tenv hpred =>
switch hpred {
| Hpointsto _ _ (Sizeof typ _ _) =>
switch (Tenv.expand_type tenv typ) {
| Tstruct {fields} => IList.exists Typ.is_objc_ref_counter_field fields
| Hpointsto _ _ (Sizeof (Tstruct name) _ _) =>
switch (Tenv.lookup tenv name) {
| Some {fields} => IList.exists Typ.is_objc_ref_counter_field fields
| _ => false
}
| _ => false
@ -626,6 +626,10 @@ let pp_offset pe f =>
| Off_index exp => F.fprintf f "%a" (pp_exp pe) exp;
/** Convert an offset to a string */
let offset_to_string e => pp_to_string (pp_offset pe_text) e;
/** dump an offset. */
let d_offset (off: offset) => L.add_print_action (L.PToff, Obj.repr off);

4
infer/src/IR/Sil.rei
Unescape View File

@ -353,6 +353,10 @@ let d_exp_list: list Exp.t => unit;
let pp_offset: printenv => F.formatter => offset => unit;
/** Convert an offset to a string */
let offset_to_string: offset => string;
/** Dump an offset */
let d_offset: offset => unit;

104
infer/src/IR/Tenv.re
Unescape View File

@ -40,21 +40,6 @@ let mk_struct
supers::supers=?
annots::annots=?
name => {
let normalize_fields fs =>
IList.map_changed
(
fun ((fld, typ, ann) as fta) =>
switch typ {
| Typ.Tstruct {name} => (fld, Typ.Tvar name, ann)
| _ => fta
}
)
fs;
let fields =
switch fields {
| Some fields => Some (normalize_fields fields)
| None => fields
};
let struct_typ =
Typ.internal_mk_struct
default::?default
@ -76,58 +61,35 @@ let mem tenv name => TypenameHash.mem tenv name;
/** Look up a name in the global type environment. */
let lookup tenv name =>
try (Some (TypenameHash.find tenv name)) {
| Not_found => None
};
/** 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 =
fun
| ""
| "void" => Some Typ.Tvoid
| "int" => Some (Typ.Tint Typ.IInt)
| "byte" => Some (Typ.Tint Typ.IShort)
| "short" => Some (Typ.Tint Typ.IShort)
| "boolean" => Some (Typ.Tint Typ.IBool)
| "char" => Some (Typ.Tint Typ.IChar)
| "long" => Some (Typ.Tint Typ.ILong)
| "float" => Some (Typ.Tfloat Typ.FFloat)
| "double" => Some (Typ.Tfloat Typ.FDouble)
| typ_str when String.contains typ_str '[' => {
let stripped_typ = String.sub typ_str 0 (String.length typ_str - 2);
switch (loop stripped_typ) {
| Some typ => Some (Typ.Tptr (Typ.Tarray typ None) Typ.Pk_pointer)
| None => None
}
| Not_found =>
/* ToDo: remove the following additional lookups once C/C++ interop is resolved */
switch (name: Typename.t) {
| TN_csu Struct m =>
try (Some (TypenameHash.find tenv (TN_csu (Class CPP) m))) {
| Not_found => None
}
| typ_str =>
/* non-primitive/non-array type--resolve it in the tenv */
switch (lookup_java_class_from_string tenv typ_str) {
| Some struct_typ => Some (Typ.Tstruct struct_typ)
| None => None
};
loop typ_str
};
| TN_csu (Class CPP) m =>
try (Some (TypenameHash.find tenv (TN_csu Struct m))) {
| Not_found => None
}
| _ => None
}
};
/** Add a (name,type) pair to the global type environment. */
let add tenv name struct_typ => TypenameHash.replace tenv name struct_typ;
/** Return the declaring class type of [pname_java] */
let proc_extract_declaring_class_typ tenv pname_java =>
lookup_java_class_from_string tenv (Procname.java_get_class_name pname_java);
/** 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 :option Typ.struct_typ =>
lookup tenv (Typename.Java.from_string typ_str);
/** Return the return type of [pname_java]. */
let proc_extract_return_typ tenv pname_java =>
lookup_java_typ_from_string tenv (Procname.java_get_return_type pname_java);
/** Return the declaring class type of [pname_java] */
let lookup_declaring_class tenv pname_java =>
lookup_java_class_from_string tenv (Procname.java_get_class_name pname_java);
/** Get method that is being overriden by java_pname (if any) **/
@ -147,37 +109,13 @@ let get_overriden_method tenv pname_java => {
}
| [] => None
};
switch (proc_extract_declaring_class_typ tenv pname_java) {
switch (lookup_declaring_class tenv pname_java) {
| Some {Typ.supers: supers} => get_overriden_method_in_supers pname_java supers
| _ => None
}
};
/** expand a type if it is a typename by looking it up in the type environment */
let expand_type tenv (typ: Typ.t) =>
switch typ {
| Tvar tname =>
switch (lookup tenv tname) {
| 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;

25
infer/src/IR/Tenv.rei
Unescape View File

@ -25,14 +25,6 @@ let add: t => Typename.t => Typ.struct_typ => unit;
let create: unit => t;
/** Expand a type if it is a typename by looking it up in the type environment. */
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;
@ -49,13 +41,8 @@ let load_from_file: DB.filename => option t;
let lookup: t => Typename.t => option Typ.struct_typ;
/** Lookup Java types by name. */
let lookup_java_typ_from_string: t => string => option Typ.t;
/** 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: t => string => option Typ.struct_typ;
/** Return the declaring class type of [pname_java] */
let lookup_declaring_class: t => Procname.java => option Typ.struct_typ;
/** Construct a struct_typ, normalizing field types */
@ -71,14 +58,6 @@ let mk_struct:
Typ.struct_typ;
/** Return the declaring class type of [pname_java] */
let proc_extract_declaring_class_typ: t => Procname.java => option Typ.struct_typ;
/** Return the return type of [pname_java]. */
let proc_extract_return_typ: t => Procname.java => option Typ.t;
/** Check if typename is found in t */
let mem: t => Typename.t => bool;

280
infer/src/IR/Typ.re
Unescape View File

@ -280,56 +280,39 @@ let ptr_kind_string =
/** statically determined length of an array type, if any */
type static_length = option IntLit.t;
type struct_fields = list (Ident.fieldname, t, item_annotation)
/** Type for a structured value. */
and struct_typ = {
name: Typename.t, /** name */
fields: struct_fields, /** non-static fields */
statics: struct_fields, /** static fields */
supers: list Typename.t, /** list of superclasses */
methods: list Procname.t, /** methods defined */
annots: item_annotation /** annotations */
}
/** types for sil (structured) expressions */
and t =
| Tvar of Typename.t /** named type */
type t =
| Tint of ikind /** integer type */
| Tfloat of fkind /** float type */
| Tvoid /** void type */
| Tfun of bool /** function type with noreturn attribute */
| Tptr of t ptr_kind /** pointer type */
| Tstruct of struct_typ /** Type for a structured value */
| Tstruct of Typename.t /** structured value type name */
| Tarray of t static_length /** array type with statically fixed length */;
let rec fld_typ_ann_compare fta1 fta2 =>
triple_compare Ident.fieldname_compare compare item_annotation_compare fta1 fta2
and fld_typ_ann_list_compare ftal1 ftal2 => IList.compare fld_typ_ann_compare ftal1 ftal2
and struct_typ_compare struct_typ1 struct_typ2 =>
switch (struct_typ1.name, struct_typ2.name) {
| (TN_csu (Class Java) _, TN_csu (Class Java) _) =>
Typename.compare struct_typ1.name struct_typ2.name
| _ =>
let n = fld_typ_ann_list_compare struct_typ1.fields struct_typ2.fields;
if (n != 0) {
n
} else {
let n = fld_typ_ann_list_compare struct_typ1.statics struct_typ2.statics;
if (n != 0) {
n
} else {
Typename.compare struct_typ1.name struct_typ2.name
}
}
}
type struct_fields = list (Ident.fieldname, t, item_annotation);
/** Type for a structured value. */
type struct_typ = {
name: Typename.t, /** name */
fields: struct_fields, /** non-static fields */
statics: struct_fields, /** static fields */
supers: list Typename.t, /** superclasses */
methods: list Procname.t, /** methods defined */
annots: item_annotation /** annotations */
};
type lookup = Typename.t => option struct_typ;
/** Comparision for types. */
and compare t1 t2 =>
let rec compare t1 t2 =>
if (t1 === t2) {
0
} else {
switch (t1, t2) {
| (Tvar tn1, Tvar tn2) => Typename.compare tn1 tn2
| (Tvar _, _) => (-1)
| (_, Tvar _) => 1
| (Tint ik1, Tint ik2) => ikind_compare ik1 ik2
| (Tint _, _) => (-1)
| (_, Tint _) => 1
@ -351,37 +334,46 @@ and compare t1 t2 =>
}
| (Tptr _, _) => (-1)
| (_, Tptr _) => 1
| (Tstruct struct_typ1, Tstruct struct_typ2) => struct_typ_compare struct_typ1 struct_typ2
| (Tstruct tn1, Tstruct tn2) => Typename.compare tn1 tn2
| (Tstruct _, _) => (-1)
| (_, Tstruct _) => 1
| (Tarray t1 _, Tarray t2 _) => compare t1 t2
}
};
let equal t1 t2 => compare t1 t2 == 0;
let fld_typ_ann_compare fta1 fta2 =>
triple_compare Ident.fieldname_compare compare item_annotation_compare fta1 fta2;
let fld_typ_ann_list_compare ftal1 ftal2 => IList.compare fld_typ_ann_compare ftal1 ftal2;
let struct_typ_compare struct_typ1 struct_typ2 =>
switch (struct_typ1.name, struct_typ2.name) {
| (TN_csu (Class Java) _, TN_csu (Class Java) _) =>
Typename.compare struct_typ1.name struct_typ2.name
| _ =>
let n = fld_typ_ann_list_compare struct_typ1.fields struct_typ2.fields;
if (n != 0) {
n
} else {
let n = fld_typ_ann_list_compare struct_typ1.statics struct_typ2.statics;
if (n != 0) {
n
} else {
Typename.compare struct_typ1.name struct_typ2.name
}
}
};
let struct_typ_equal struct_typ1 struct_typ2 => struct_typ_compare struct_typ1 struct_typ2 == 0;
let equal t1 t2 => compare t1 t2 == 0;
let rec pp_struct_typ pe pp_base f {fields, name} =>
if false {
/* change false to true to print the details of struct */
F.fprintf
f
"%a {%a} %a"
Typename.pp
name
(pp_seq (fun f (fld, t, _) => F.fprintf f "%a %a" (pp_full pe) t Ident.pp_fieldname fld))
fields
pp_base
()
} else {
F.fprintf f "%a %a" Typename.pp name pp_base ()
}
/** Pretty print a type declaration.
pp_base prints the variable for a declaration, or can be skip to print only the type */
and pp_decl pe pp_base f =>
let rec pp_decl pe pp_base f =>
fun
| Tvar tname => F.fprintf f "%s %a" (Typename.to_string tname) pp_base ()
| Tstruct tname => F.fprintf f "%s %a" (Typename.to_string tname) pp_base ()
| Tint ik => F.fprintf f "%s %a" (ikind_to_string ik) pp_base ()
| Tfloat fk => F.fprintf f "%s %a" (fkind_to_string fk) pp_base ()
| Tvoid => F.fprintf f "void %a" pp_base ()
@ -395,7 +387,6 @@ and pp_decl pe pp_base f =>
let pp_base' fmt () => F.fprintf fmt "%s%a" (ptr_kind_string pk) pp_base ();
pp_decl pe pp_base' f typ
}
| Tstruct struct_typ => pp_struct_typ pe pp_base f struct_typ
| Tarray typ static_len => {
let pp_array_static_len fmt => (
fun
@ -404,17 +395,37 @@ and pp_decl pe pp_base f =>
);
let pp_base' fmt () => F.fprintf fmt "%a[%a]" pp_base () pp_array_static_len static_len;
pp_decl pe pp_base' f typ
}
};
/** Pretty print a type with all the details, using the C syntax. */
and pp_full pe => pp_decl pe (fun _ () => ())
let pp_full pe => pp_decl pe (fun _ () => ());
/** Pretty print a type. Do nothing by default. */
and pp pe f te =>
let pp pe f te =>
if Config.print_types {
pp_full pe f te
} else {
()
};
let pp_struct_typ pe pp_base f {fields, name} =>
if false {
/* change false to true to print the details of struct */
F.fprintf
f
"%a {%a} %a"
Typename.pp
name
(pp_seq (fun f (fld, t, _) => F.fprintf f "%a %a" (pp_full pe) t Ident.pp_fieldname fld))
fields
pp_base
()
} else {
F.fprintf f "%a %a" Typename.pp name pp_base ()
};
let to_string typ => {
let pp fmt () => pp_full pe_text fmt typ;
pp_to_string pp ()
@ -496,8 +507,7 @@ let internal_mk_struct
let name =
fun
| Tvar name
| Tstruct {name} => Some name
| Tstruct name => Some name
| _ => None;
let unsome s =>
@ -525,46 +535,49 @@ 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 expand_type::expand_type typ =>
switch (expand_type typ) {
let rec get_extensible_array_element_typ lookup::lookup typ =>
switch typ {
| Tarray typ _ => Some typ
| Tstruct {fields} =>
Option.map_default
(fun (_, fld_typ, _) => get_extensible_array_element_typ expand_type::expand_type fld_typ)
None
(IList.last fields)
| Tstruct name =>
switch (lookup name) {
| Some {fields} =>
switch (IList.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 type if given, otherwise raise an exception */
let struct_typ_fld expand_type::expand_type default_opt f typ => {
let def () => unsome "struct_typ_fld" default_opt;
switch (expand_type typ) {
| Tstruct struct_typ =>
try (
(fun (_, y, _) => y) (
IList.find (fun (_f, _, _) => Ident.fieldname_equal _f f) struct_typ.fields
)
) {
| Not_found => def ()
/** If a struct type with field f, return the type of f. If not, return the default */
let struct_typ_fld lookup::lookup default::default fn typ =>
switch typ {
| Tstruct name =>
switch (lookup name) {
| Some {fields} =>
try (snd3 (IList.find (fun (f, _, _) => Ident.fieldname_equal f fn) fields)) {
| Not_found => default
}
| None => default
}
| _ => def ()
}
};
| _ => default
};
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 {
let (_, t, a) =
IList.find
(fun (f, _, _) => Ident.fieldname_equal f fn) (struct_typ.fields @ struct_typ.statics);
Some (t, a)
} {
| Not_found => None
let get_field_type_and_annotation lookup::lookup fn typ =>
switch typ {
| Tstruct name
| Tptr (Tstruct name) _ =>
switch (lookup name) {
| Some {fields, statics} =>
try {
let (_, t, a) = IList.find (fun (f, _, _) => Ident.fieldname_equal f fn) (fields @ statics);
Some (t, a)
} {
| Not_found => None
}
| None => None
}
| _ => None
};
@ -577,54 +590,27 @@ let struct_typ_get_class_kind struct_typ =>
| _ => None
};
/** return true if [struct_typ] is a Java class */
let struct_typ_is_java_class struct_typ =>
switch (struct_typ_get_class_kind struct_typ) {
| Some Csu.Java => true
| _ => false
};
/** return true if [struct_typ] is a C++ class. Note that this returns false for raw structs. */
let struct_typ_is_cpp_class struct_typ =>
switch (struct_typ_get_class_kind struct_typ) {
| Some Csu.CPP => true
| _ => false
};
/** 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 =>
switch (struct_typ_get_class_kind struct_typ) {
| Some Csu.Objc => true
| _ => false
};
let is_class_of_kind expand_type::expand_type typ ck =>
switch (expand_type typ) {
| Tstruct {name: TN_csu (Class ck') _} => ck == ck'
let is_class_of_kind typ ck =>
switch typ {
| Tstruct (TN_csu (Class ck') _) => ck == ck'
| _ => false
};
let is_objc_class expand_type::expand_type typ =>
is_class_of_kind expand_type::expand_type typ Csu.Objc;
let is_objc_class typ => is_class_of_kind typ Csu.Objc;
let is_cpp_class expand_type::expand_type typ =>
is_class_of_kind expand_type::expand_type typ Csu.CPP;
let is_cpp_class typ => is_class_of_kind typ Csu.CPP;
let is_java_class expand_type::expand_type typ =>
is_class_of_kind expand_type::expand_type typ Csu.Java;
let is_java_class typ => is_class_of_kind typ Csu.Java;
let rec is_array_of_cpp_class expand_type::expand_type typ =>
let rec is_array_of_cpp_class typ =>
switch typ {
| Tarray typ _ => is_array_of_cpp_class expand_type::expand_type typ
| _ => is_cpp_class expand_type::expand_type typ
| Tarray typ _ => is_array_of_cpp_class typ
| _ => is_cpp_class typ
};
let is_pointer_to_cpp_class expand_type::expand_type typ =>
let is_pointer_to_cpp_class typ =>
switch typ {
| Tptr t _ => is_cpp_class expand_type::expand_type t
| Tptr t _ => is_cpp_class t
| _ => false
};
@ -646,3 +632,31 @@ let objc_ref_counter_field = (Ident.fieldname_hidden, Tint IInt, objc_ref_counte
let is_objc_ref_counter_field (fld, _, a) =>
Ident.fieldname_is_hidden fld && item_annotation_compare a objc_ref_counter_annot == 0;
/** Java types by name */
let rec java_from_string =
fun
| ""
| "void" => Tvoid
| "int" => Tint IInt
| "byte" => Tint IShort
| "short" => Tint IShort
| "boolean" => Tint IBool
| "char" => Tint IChar
| "long" => Tint ILong
| "float" => Tfloat FFloat
| "double" => Tfloat FDouble
| typ_str when String.contains typ_str '[' => {
let stripped_typ = String.sub typ_str 0 (String.length typ_str - 2);
Tptr (Tarray (java_from_string stripped_typ) None) Pk_pointer
}
| typ_str => Tstruct (Typename.Java.from_string typ_str);
/** Return the return type of [pname_java]. */
let java_proc_return_typ pname_java =>
switch (java_from_string (Procname.java_get_return_type pname_java)) {
| Tstruct _ as typ => Tptr typ Pk_pointer
| typ => typ
};

63
infer/src/IR/Typ.rei
Unescape View File

@ -135,27 +135,32 @@ let ptr_kind_compare: ptr_kind => ptr_kind => int;
/** statically determined length of an array type, if any */
type static_length = option IntLit.t;
type struct_fields = list (Ident.fieldname, t, item_annotation)
/** Type for a structured value. */
and struct_typ = private {
name: Typename.t, /** name */
fields: struct_fields, /** non-static fields */
statics: struct_fields, /** static fields */
supers: list Typename.t, /** list of supers */
methods: list Procname.t, /** methods defined */
annots: item_annotation /** annotations */
}
/** types for sil (structured) expressions */
and t =
| Tvar of Typename.t /** named type */
type t =
| Tint of ikind /** integer type */
| Tfloat of fkind /** float type */
| Tvoid /** void type */
| Tfun of bool /** function type with noreturn attribute */
| Tptr of t ptr_kind /** pointer type */
| Tstruct of struct_typ /** Type for a structured value */
| Tstruct of Typename.t /** structured value type name */
| Tarray of t static_length /** array type with statically fixed length */;
type struct_fields = list (Ident.fieldname, t, item_annotation);
/** Type for a structured value. */
type struct_typ = private {
name: Typename.t, /** name */
fields: struct_fields, /** non-static fields */
statics: struct_fields, /** static fields */
supers: list Typename.t, /** supers */
methods: list Procname.t, /** methods defined */
annots: item_annotation /** annotations */
};
type lookup = Typename.t => option struct_typ;
/** Comparision for fieldnames * types * item annotations. */
let fld_typ_ann_compare:
@ -235,43 +240,31 @@ 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: expand_type::(t => t) => t => option t;
let get_extensible_array_element_typ: lookup::lookup => 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: expand_type::(t => t) => option t => Ident.fieldname => t => t;
let struct_typ_fld: lookup::lookup => default::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:
expand_ptr_type::(t => t) => Ident.fieldname => t => option (t, item_annotation);
lookup::lookup => Ident.fieldname => t => option (t, item_annotation);
/** if [struct_typ] is a class, return its class kind (Java, CPP, or Obj-C) */
let struct_typ_get_class_kind: struct_typ => option Csu.class_kind;
let is_objc_class: t => bool;
/** return true if [struct_typ] is a Java class */
let struct_typ_is_java_class: struct_typ => bool;
/** return true if [struct_typ] is a C++ class. Note that this returns false for raw structs. */
let struct_typ_is_cpp_class: struct_typ => bool;
let is_cpp_class: t => bool;
let is_java_class: t => 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_array_of_cpp_class: t => bool;
let is_objc_class: expand_type::(t => t) => t => bool;
let is_cpp_class: expand_type::(t => t) => t => bool;
let is_java_class: expand_type::(t => t) => t => bool;
let is_array_of_cpp_class: expand_type::(t => t) => t => bool;
let is_pointer_to_cpp_class: expand_type::(t => t) => t => bool;
let is_pointer_to_cpp_class: t => bool;
let has_block_prefix: string => bool;
@ -286,3 +279,7 @@ let objc_ref_counter_field: (Ident.fieldname, t, item_annotation);
let is_objc_ref_counter_field: (Ident.fieldname, t, item_annotation) => bool;
let unsome: string => option t => t;
/** Return the return type of [pname_java]. */
let java_proc_return_typ: Procname.java => t;

4
infer/src/IR/Typename.re
Unescape View File

@ -44,6 +44,10 @@ let equal tn1 tn2 => compare tn1 tn2 == 0;
let module Java = {
let from_string class_name_str =>
TN_csu (Csu.Class Csu.Java) (Mangled.from_string class_name_str);
let is_class =
fun
| TN_csu (Class Java) _ => true
| _ => false;
};
type typename_t = t;

3
infer/src/IR/Typename.rei
Unescape View File

@ -37,6 +37,9 @@ let equal: t => t => bool;
let module Java: {
/** Create a typename from a Java classname in the form "package.class" */
let from_string: string => t;
/** [is_class name] holds if [name] names a Java class */
let is_class: t => bool;
};
let module Set: Set.S with type elt = t;

51
infer/src/backend/abs.ml
Unescape View File

@ -406,27 +406,27 @@ let mk_rules_for_dll tenv (para : Sil.hpara_dll) : rule list =
(****************** Start of Predicate Discovery ******************)
let typ_get_recursive_flds tenv typ_exp =
let filter typ (_, t, _) =
let filter typ (_, (t: Typ.t), _) =
match t with
| Typ.Tvar _ | Typ.Tint _ | Typ.Tfloat _ | Typ.Tvoid | Typ.Tfun _ -> false
| Typ.Tptr (Typ.Tvar tname', _) ->
let typ' = match Tenv.lookup tenv tname' with
| None ->
L.err "@.typ_get_recursive: Undefined type %s@." (Typename.to_string tname');
t
| Some st -> Typ.Tstruct st in
| Tstruct _ | Tint _ | Tfloat _ | Tvoid | Tfun _ ->
false
| Tptr (Tstruct _ as typ', _) ->
Typ.equal typ' typ
| Typ.Tptr _ | Typ.Tstruct _ | Typ.Tarray _ ->
| Tptr _ | Tarray _ ->
false
in
match typ_exp with
| Exp.Sizeof (typ, _, _) ->
(match Tenv.expand_type tenv typ with
| Typ.Tint _ | Typ.Tvoid | Typ.Tfun _ | Typ.Tptr _ | Typ.Tfloat _ -> []
| Typ.Tstruct { fields } ->
IList.map (fun (x, _, _) -> x) (IList.filter (filter typ) fields)
| Typ.Tarray _ -> []
| Typ.Tvar _ -> assert false)
| Exp.Sizeof (typ, _, _) -> (
match typ with
| Tstruct name -> (
match Tenv.lookup tenv name with
| Some { fields } -> IList.map fst3 (IList.filter (filter typ) fields)
| None ->
L.err "@.typ_get_recursive: unexpected type expr: %a@." (Sil.pp_exp pe_text) typ_exp;
[] (* ToDo: assert false *)
)
| Tint _ | Tvoid | Tfun _ | Tptr _ | Tfloat _ | Tarray _ -> []
)
| Exp.Var _ -> [] (* type of |-> not known yet *)
| Exp.Const _ -> []
| _ ->
@ -1001,14 +1001,17 @@ let remove_opt _prop =
weak/unsafe_unretained/assing *)
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 Tenv.expand_type tenv t with
| Tstruct { fields; statics } ->
let ia = ref [] in
IList.iter (fun (fn', _, ia') ->
if Ident.fieldname_equal fn fn' then ia := ia')
(fields @ statics);
!ia
let get_item_annotation (t: Typ.t) fn =
match t with
| Tstruct name -> (
let equal_fn (fn', _, _) = Ident.fieldname_equal fn fn' in
match Tenv.lookup tenv name with
| Some { fields; statics } -> (
try trd3 (IList.find equal_fn (fields @ statics))
with Not_found -> []
)
| None -> []
)
| _ -> [] in
let rec has_weak_or_unretained_or_assign params =
match params with

82
infer/src/backend/absarray.ml
Unescape View File

@ -64,41 +64,52 @@ end = struct
type path = Exp.t * (syn_offset list)
(** 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, Tenv.expand_type tenv t, syn_offs with
let rec get_strexp_at_syn_offsets tenv se (t: Typ.t) syn_offs =
let fail () =
L.d_strln "Failure of get_strexp_at_syn_offsets";
L.d_str "se: "; Sil.d_sexp se; L.d_ln ();
L.d_str "t: "; Typ.d_full t; L.d_ln ();
assert false
in
match se, t, syn_offs with
| _, _, [] -> (se, t)
| Sil.Estruct (fsel, _), Tstruct { fields }, Field (fld, _) :: syn_offs' ->
let se' = snd (IList.find (fun (f', _) -> Ident.fieldname_equal f' fld) fsel) in
let t' = (fun (_,y,_) -> y)
(IList.find (fun (f', _, _) ->
Ident.fieldname_equal f' fld) fields) in
get_strexp_at_syn_offsets tenv se' t' syn_offs'
| Sil.Estruct (fsel, _), Tstruct name, Field (fld, _) :: syn_offs' -> (
match Tenv.lookup tenv name with
| Some { fields } ->
let se' = snd (IList.find (fun (f', _) -> Ident.fieldname_equal f' fld) fsel) in
let t' = snd3 (IList.find (fun (f', _, _) -> Ident.fieldname_equal f' fld) fields) in
get_strexp_at_syn_offsets tenv se' t' syn_offs'
| None ->
fail ()
)
| Sil.Earray (_, esel, _), Typ.Tarray (t', _), Index ind :: syn_offs' ->
let se' = snd (IList.find (fun (i', _) -> Exp.equal i' ind) esel) in
get_strexp_at_syn_offsets tenv se' t' syn_offs'
| _ ->
L.d_strln "Failure of get_strexp_at_syn_offsets";
L.d_str "se: "; Sil.d_sexp se; L.d_ln ();
L.d_str "t: "; Typ.d_full t; L.d_ln ();
assert false
fail ()
(** Replace a strexp at the given syntactic offset list *)
let rec replace_strexp_at_syn_offsets tenv se t syn_offs update =
match se, Tenv.expand_type tenv t, syn_offs with
let rec replace_strexp_at_syn_offsets tenv se (t: Typ.t) syn_offs update =
match se, t, syn_offs with
| _, _, [] ->
update se
| Sil.Estruct (fsel, inst), Tstruct { fields }, Field (fld, _) :: syn_offs' ->
let se' = snd (IList.find (fun (f', _) -> Ident.fieldname_equal f' fld) fsel) in
let t' = (fun (_,y,_) -> y)
(IList.find (fun (f', _, _) ->
Ident.fieldname_equal f' fld) fields) in
let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in
let fsel' =
IList.map (fun (f'', se'') ->
if Ident.fieldname_equal f'' fld then (fld, se_mod) else (f'', se'')
) fsel in
Sil.Estruct (fsel', inst)
| Sil.Earray (len, esel, inst), Typ.Tarray (t', _), Index idx :: syn_offs' ->
| Sil.Estruct (fsel, inst), Tstruct name, Field (fld, _) :: syn_offs' -> (
match Tenv.lookup tenv name with
| Some { fields } ->
let se' = snd (IList.find (fun (f', _) -> Ident.fieldname_equal f' fld) fsel) in
let t' = (fun (_,y,_) -> y)
(IList.find (fun (f', _, _) ->
Ident.fieldname_equal f' fld) fields) in
let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in
let fsel' =
IList.map (fun (f'', se'') ->
if Ident.fieldname_equal f'' fld then (fld, se_mod) else (f'', se'')
) fsel in
Sil.Estruct (fsel', inst)
| None ->
assert false
)
| Sil.Earray (len, esel, inst), Tarray (t', _), Index idx :: syn_offs' ->
let se' = snd (IList.find (fun (i', _) -> Exp.equal i' idx) esel) in
let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in
let esel' =
@ -145,15 +156,20 @@ end = struct
(** Find a sub strexp with the given property. Can raise [Not_found] *)
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 rec find_offset_sexp sigma_other hpred root offs se (typ: Typ.t) =
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, Tenv.expand_type tenv typ with
| Sil.Estruct (fsel, _), Tstruct { fields } ->
find_offset_fsel sigma_other hpred root offs fsel fields typ
| Sil.Earray (_, esel, _), Typ.Tarray (t, _) ->
match se, typ with
| Sil.Estruct (fsel, _), Tstruct name -> (
match Tenv.lookup tenv name with
| Some { fields } ->
find_offset_fsel sigma_other hpred root offs fsel fields typ
| None ->
()
)
| Sil.Earray (_, esel, _), Tarray (t, _) ->
find_offset_esel sigma_other hpred root offs esel t
| _ -> ()
end
@ -526,7 +542,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 lookup = Tenv.lookup tenv in
let check_index root offs (ind, _) =
if !Config.footprint then
let path = StrexpMatch.path_from_exp_offsets root offs in
@ -542,7 +558,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 ~expand_type (Some Typ.Tvoid) f typ in
let typ_f = Typ.struct_typ_fld ~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) ->

22
infer/src/backend/errdesc.ml
Unescape View File

@ -509,11 +509,8 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
(Pvar.is_local pvar || Pvar.is_global pvar) &&
not (Pvar.is_frontend_tmp pvar) &&
match hpred_typ_opt, find_typ_without_ptr prop pvar with
| Some (Exp.Sizeof (t1, _, _)), Some (Exp.Sizeof (Typ.Tptr (t2_, _), _, _)) ->
(try
let t2 = Tenv.expand_type tenv t2_ in
Typ.equal t1 t2
with exn when SymOp.exn_not_failure exn -> false)
| Some (Exp.Sizeof (t1, _, _)), Some (Exp.Sizeof (Typ.Tptr (t2, _), _, _)) ->
Typ.equal t1 t2
| Some (Exp.Sizeof (Typ.Tint _, _, _)), Some (Exp.Sizeof (Typ.Tint _, _, _))
when is_file -> (* must be a file opened with "open" *)
true
@ -582,15 +579,12 @@ 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, _, _) -> (
match Tenv.expand_type tenv typ with
| Tstruct {fields} -> (
try
let _, t, _ =
IList.find (fun (f', _, _) -> Ident.fieldname_equal f' f)
fields in
Some t
with Not_found -> None
| Exp.Sizeof (Tstruct name, _, _) -> (
match Tenv.lookup tenv name with
| Some {fields} -> (
match IList.find (fun (f', _, _) -> Ident.fieldname_equal f' f) fields with
| _, t, _ -> Some t
| exception Not_found -> None
)
| _ ->
None

10
infer/src/backend/interproc.ml
Unescape View File

@ -660,14 +660,14 @@ let report_context_leaks pname sigma tenv =
Prop.compute_reachable_hpreds sigma fld_exps in
(* raise an error if any Context expression is in [reachable_exps] *)
IList.iter
(fun (context_exp, struct_typ) ->
(fun (context_exp, {Typ.name}) ->
if Exp.Set.mem context_exp reachable_exps then
let leak_path =
match get_fld_typ_path_opt fld_exps context_exp reachable_hpreds with
| Some path -> path
| None -> assert false (* a path must exist in order for a leak to be reported *) in
let err_desc =
Errdesc.explain_context_leak pname (Typ.Tstruct struct_typ) fld_name leak_path in
Errdesc.explain_context_leak pname (Typ.Tstruct name) fld_name leak_path in
let exn = Exceptions.Context_leak (err_desc, __POS__) in
Reporting.log_error pname exn)
context_exps in
@ -675,9 +675,9 @@ 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 (typ, _), _, _)) -> (
match Tenv.expand_type tenv typ with
| Tstruct struct_typ
| Sil.Hpointsto (_, Eexp (exp, _), Sizeof (Tptr (Tstruct name, _), _, _)) -> (
match Tenv.lookup tenv name with
| Some struct_typ
when AndroidFramework.is_context tenv struct_typ &&
not (AndroidFramework.is_application tenv struct_typ) ->
(exp, struct_typ) :: exps

6
infer/src/backend/localise.ml
Unescape View File

@ -247,8 +247,7 @@ let by_call_to_ra tags ra =
let rec format_typ = function
| Typ.Tptr (typ, _) when !Config.curr_language = Config.Java ->
format_typ typ
| Typ.Tstruct { name }
| Typ.Tvar name ->
| Typ.Tstruct name ->
Typename.name name
| typ ->
Typ.to_string typ
@ -685,8 +684,7 @@ 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 (( Tvar (TN_csu (Class _, _) as name)
| Tstruct { name = TN_csu (Class _, _) as name; }), _, _)) ->
| Some (Exp.Sizeof (Tstruct (TN_csu (Class _, _) as name), _, _)) ->
" of type " ^ Typename.name name ^ " "
| _ -> " " in
let desc_str =

47
infer/src/backend/modelBuiltins.ml
Unescape View File

@ -81,7 +81,7 @@ let add_array_to_prop tenv pdesc prop_ lexp typ =
let prop''= Prop.set prop' ~sigma_fp:(hpred:: sigma_fp) in
let prop''= Prop.normalize tenv prop'' in
Some (len, prop'')
| _ -> None
| _ -> None
end
(* Add an array in prop if it is not allocated.*)
@ -154,8 +154,7 @@ let create_type tenv n_lexp typ prop =
match typ with
| Typ.Tptr (typ', _) ->
let sexp = Sil.Estruct ([], Sil.inst_none) in
let typ'' = Tenv.expand_type tenv typ' in
let texp = Exp.Sizeof (typ'', None, Subtype.subtypes) in
let texp = Exp.Sizeof (typ', None, Subtype.subtypes) in
let hpred = Prop.mk_ptsto tenv n_lexp sexp texp in
Some hpred
| Typ.Tarray _ ->
@ -457,31 +456,22 @@ let execute___objc_counter_update
{ Builtin.pdesc; tenv; prop_; path; args; loc; }
: Builtin.ret_typ =
match args with
| [(lexp, typ)] ->
let typ' = (match Tenv.expand_type tenv typ with
| Typ.Tstruct _ as s -> s
| Typ.Tptr(t, _) -> Tenv.expand_type tenv t
| s' ->
L.d_str
("Trying to update hidden field of not a struc. Type: " ^
(Typ.to_string s'));
assert false) in
| [(lexp, (Typ.Tstruct _ as typ | Tptr (Tstruct _ as typ, _)))] ->
(* Assumes that lexp is a temp n$1 that has the value of the object. *)
(* This is the case as a call f(o) it's translates as n$1=*&o; f(n$1) *)
(* n$2 = *n$1.hidden *)
let tmp = Ident.create_fresh Ident.knormal in
let hidden_field = Exp.Lfield (lexp, Ident.fieldname_hidden, typ') in
let counter_to_tmp = Sil.Load (tmp, hidden_field, typ', loc) in
let hidden_field = Exp.Lfield (lexp, Ident.fieldname_hidden, typ) in
let counter_to_tmp = Sil.Load (tmp, hidden_field, typ, loc) in
(* *n$1.hidden = (n$2 +/- delta) *)
let update_counter =
Sil.Store
(hidden_field,
typ',
Exp.BinOp(op, Exp.Var tmp, Exp.Const (Const.Cint delta)),
loc) in
Sil.Store (hidden_field, typ, BinOp (op, Var tmp, Const (Cint delta)), loc) in
let update_counter_instrs =
[ counter_to_tmp; update_counter; Sil.Remove_temps([tmp], loc) ] in
SymExec.instrs ~mask_errors tenv pdesc update_counter_instrs [(prop_, path)]
| [(_, typ)] ->
L.d_str ("Trying to update hidden field of non-struct value. Type: " ^ (Typ.to_string typ));
assert false
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
(* Given a list of args checks if the first is the flag indicating whether is a call to
@ -758,8 +748,7 @@ 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 (( Tvar (TN_csu (Class Objc, _) as name)
| Tstruct { name = TN_csu (Class Objc, _) as name; }) as s, len, subt), _)] ->
| [(Exp.Sizeof (Tstruct (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
@ -1175,11 +1164,8 @@ let arrayWithObjects_pname = mk_objc_class_method "NSArray" "arrayWithObjects:"
let arrayWithObjectsCount_pname = mk_objc_class_method "NSArray" "arrayWithObjects:count:"
let execute_objc_NSArray_alloc_no_fail
({ Builtin.tenv; } as builtin_args) symb_state pname =
let nsarray_typ_ =
Typ.Tvar (Typename.TN_csu (Csu.Class Csu.Objc, Mangled.from_string "NSArray")) in
let nsarray_typ = Tenv.expand_type tenv nsarray_typ_ in
let execute_objc_NSArray_alloc_no_fail builtin_args symb_state pname =
let nsarray_typ = Typ.Tstruct (TN_csu (Class Objc, Mangled.from_string "NSArray")) in
execute_objc_alloc_no_fail symb_state nsarray_typ (Some pname) builtin_args
let execute_NSArray_arrayWithObjects_count builtin_args =
@ -1198,13 +1184,8 @@ let _ =
(* NSDictionary models *)
let execute_objc_NSDictionary_alloc_no_fail
symb_state pname
({ Builtin.tenv; } as builtin_args) =
let nsdictionary_typ_ =
Typ.Tvar (Typename.TN_csu (Csu.Class Csu.Objc, Mangled.from_string "NSDictionary")) in
let nsdictionary_typ =
Tenv.expand_type tenv nsdictionary_typ_ in
let execute_objc_NSDictionary_alloc_no_fail symb_state pname builtin_args =
let nsdictionary_typ = Typ.Tstruct (TN_csu (Class Objc, Mangled.from_string "NSDictionary")) in
execute_objc_alloc_no_fail symb_state nsdictionary_typ (Some pname) builtin_args
let __objc_dictionary_literal_pname =

3
infer/src/backend/objc_models.ml
Unescape View File

@ -208,8 +208,7 @@ struct
match typ with
| Typ.Tptr (styp, _ ) ->
is_core_lib lib styp
| Typ.Tvar name
| Typ.Tstruct { name } ->
| Typ.Tstruct name ->
let core_lib_types = core_lib_to_type_list lib in
IList.mem string_equal (Typename.name name) core_lib_types
| _ -> false

21
infer/src/backend/prop.ml
Unescape View File

@ -501,14 +501,12 @@ let rec create_strexp_of_type tenv struct_init_mode (typ : Typ.t) len inst : Sil
| _ -> Exp.zero
else
create_fresh_var () in
match Tenv.expand_type tenv typ, len with
match typ, len with
| (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), None ->
Eexp (init_value (), inst)
| Tstruct { fields }, _ -> (
match struct_init_mode with
| No_init ->
Estruct ([], inst)
| Fld_init ->
| Tstruct name, _ -> (
match struct_init_mode, Tenv.lookup tenv name with
| Fld_init, Some { fields } ->
(* 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) =
@ -518,6 +516,8 @@ let rec create_strexp_of_type tenv struct_init_mode (typ : Typ.t) len inst : Sil
((fld, create_strexp_of_type tenv struct_init_mode t len inst) :: flds, None) in
let flds, _ = IList.fold_right f fields ([], len) in
Estruct (flds, inst)
| _ ->
Estruct ([], inst)
)
| Tarray (_, len_opt), None ->
let len = match len_opt with
@ -526,7 +526,6 @@ let rec create_strexp_of_type tenv struct_init_mode (typ : Typ.t) len inst : Sil
Earray (len, [], inst)
| Tarray _, Some len ->
Earray (len, [], inst)
| Tvar _, _
| (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), Some _ ->
assert false
@ -570,9 +569,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 exp_collapse_consecutive_indices_prop (typ : Typ.t) exp =
let typ_is_base (typ1 : Typ.t) =
match Tenv.expand_type tenv typ1 with
match typ1 with
| Tint _ | Tfloat _ | Tstruct _ | Tvoid | Tfun _ ->
true
| _ ->
@ -722,7 +721,7 @@ module Normalize = struct
let (++) = IntLit.add
let sym_eval tenv abs e =
let expand_type = Tenv.expand_type tenv in
let lookup = Tenv.lookup tenv in
let rec eval (e : Exp.t) : Exp.t =
(* L.d_str " ["; Sil.d_exp e; L.d_str"] "; *)
match e with
@ -893,7 +892,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.map_default (Typ.equal elt) false
(Typ.get_extensible_array_element_typ ~expand_type typ) in
(Typ.get_extensible_array_element_typ ~lookup typ) in
begin
match e1', e2' with
(* pattern for arrays and extensible structs:

2
infer/src/backend/prop.mli
Unescape View File

@ -174,7 +174,7 @@ val exp_normalize_noabs : Tenv.t -> Sil.subst -> Exp.t -> Exp.t
(** 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. *)
val exp_collapse_consecutive_indices_prop : Tenv.t -> Typ.t -> Exp.t -> Exp.t
val exp_collapse_consecutive_indices_prop : Typ.t -> Exp.t -> Exp.t
(** Normalize [exp] used for the address of a heap cell.
This normalization does not combine two offsets inside [exp]. *)

197
infer/src/backend/prover.ml
Unescape View File

@ -40,10 +40,10 @@ 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 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
let rec is_java_class tenv (typ: Typ.t) =
match typ with
| Tstruct name -> Typename.Java.is_class name
| Tarray (inner_typ, _) | Tptr (inner_typ, _) -> is_java_class tenv inner_typ
| _ -> false
(** Negate an atom *)
@ -381,7 +381,7 @@ end = struct
saturate { leqs = !leqs; lts = !lts; neqs = !neqs }
let from_sigma tenv sigma =
let expand_ptr_type = Tenv.expand_ptr_type tenv in
let lookup = Tenv.lookup tenv in
let leqs = ref [] in
let lts = ref [] in
let add_lt_minus1_e e =
@ -402,7 +402,7 @@ end = struct
| Sil.Estruct (fsel, _), t ->
let get_field_type f =
Option.map_default (fun t' ->
Option.map fst @@ Typ.get_field_type_and_annotation ~expand_ptr_type f t'
Option.map fst @@ Typ.get_field_type_and_annotation ~lookup f t'
) None t in
IList.iter (fun (f, se) -> strexp_extract (se, get_field_type f)) fsel
| Sil.Earray (len, isel, _), t ->
@ -1326,14 +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
let lookup = Tenv.lookup 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 ~expand_type (Some Typ.Tvoid) f2 typ2 in
let typ' = Typ.struct_typ_fld ~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
@ -1348,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 ~expand_type (Some Typ.Tvoid) f2 typ2 in
let typ' = Typ.struct_typ_fld ~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
@ -1356,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 ~expand_type (Some Typ.Tvoid) f2 typ2 in
let typ' = Typ.struct_typ_fld ~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
@ -1466,45 +1466,57 @@ 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 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 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)
| _, Sizeof (cnt_typ, len, st) ->
(* type of struct at adr_base is unknown (typically Tvoid), but
type of contents is known, so construct struct type for single fld:cnt_typ *)
let struct_typ =
Typ.Tstruct
(Typ.internal_mk_struct
~fields: [(fld, cnt_typ, Typ.item_annotation_empty)]
(TN_csu (Struct, Mangled.from_string "counterfeit"))) in
Exp.Sizeof (struct_typ, len, st)
| _ ->
(* type of struct at adr_base and of contents are both unknown: give up *)
raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lfield") in
let hpred' = Sil.Hpointsto (adr_base, Estruct ([(fld, cnt)], Sil.inst_none), cnt_texp') in
expand true true hpred'
| Sil.Hpointsto (Exp.Lindex (e, ind), se, t) ->
let t' = match t with
| Exp.Sizeof (t_, len, st) -> Exp.Sizeof (Typ.Tarray (t_, None), len, st)
| _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in
let len = match t' with
| Exp.Sizeof (_, Some len, _) -> len
| _ -> Exp.get_undefined false in
let hpred' = Sil.Hpointsto (e, Sil.Earray (len, [(ind, se)], Sil.inst_none), t') in
expand true true hpred'
| Sil.Hpointsto (Exp.BinOp (Binop.PlusPI, e1, e2), Sil.Earray (len, esel, inst), t) ->
let shift_exp e = Exp.BinOp (Binop.PlusA, e, e2) in
let len' = shift_exp len in
let esel' = IList.map (fun (e, se) -> (shift_exp e, se)) esel in
let hpred' = Sil.Hpointsto (e1, Sil.Earray (len', esel', inst), t) in
expand true calc_index_frame hpred'
| _ -> changed, calc_index_frame, hpred in
expand false calc_index_frame hpred
let expand_hpred_pointer =
let count = ref 0 in
fun tenv calc_index_frame 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
match adr_typ with
| Tstruct name -> (
match Tenv.lookup tenv name with
| Some _ ->
(* type of struct at adr_base is known *)
Some (Exp.Sizeof (adr_typ, None, Subtype.exact))
| None -> None
)
| _ -> None
with
| Some se -> se
| None ->
match cnt_texp with
| Sizeof (cnt_typ, len, st) ->
(* type of struct at adr_base is unknown (typically Tvoid), but
type of contents is known, so construct struct type for single fld:cnt_typ *)
let mangled = Mangled.from_string ("counterfeit" ^ string_of_int !count) in
let name = Typename.TN_csu (Struct, mangled) in
incr count ;
let fields = [(fld, cnt_typ, Typ.item_annotation_empty)] in
ignore (Tenv.mk_struct tenv ~fields name) ;
Exp.Sizeof (Tstruct name, len, st)
| _ ->
(* type of struct at adr_base and of contents are both unknown: give up *)
raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lfield") in
let hpred' = Sil.Hpointsto (adr_base, Estruct ([(fld, cnt)], Sil.inst_none), cnt_texp') in
expand true true hpred'
| Sil.Hpointsto (Exp.Lindex (e, ind), se, t) ->
let t' = match t with
| Exp.Sizeof (t_, len, st) -> Exp.Sizeof (Typ.Tarray (t_, None), len, st)
| _ -> raise (Failure "expand_hpred_pointer: Unexpected non-sizeof type in Lindex") in
let len = match t' with
| Exp.Sizeof (_, Some len, _) -> len
| _ -> Exp.get_undefined false in
let hpred' = Sil.Hpointsto (e, Sil.Earray (len, [(ind, se)], Sil.inst_none), t') in
expand true true hpred'
| Sil.Hpointsto (Exp.BinOp (Binop.PlusPI, e1, e2), Sil.Earray (len, esel, inst), t) ->
let shift_exp e = Exp.BinOp (Binop.PlusA, e, e2) in
let len' = shift_exp len in
let esel' = IList.map (fun (e, se) -> (shift_exp e, se)) esel in
let hpred' = Sil.Hpointsto (e1, Sil.Earray (len', esel', inst), t) in
expand true calc_index_frame hpred'
| _ -> changed, calc_index_frame, hpred in
expand false calc_index_frame hpred
module Subtyping_check =
struct
@ -1554,66 +1566,52 @@ struct
| _ -> false
(** check if t1 is a subtype of t2, in Java *)
let rec check_subtype_java tenv t1 t2 =
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 } ->
let rec check_subtype_java tenv (t1: Typ.t) (t2: Typ.t) =
match t1, t2 with
| Tstruct (TN_csu (Class Java, _) as cn1), Tstruct (TN_csu (Class Java, _) as cn2) ->
check_subclass tenv cn1 cn2
| Typ.Tarray (dom_type1, _), Typ.Tarray (dom_type2, _) ->
| Tarray (dom_type1, _), Tarray (dom_type2, _) ->
check_subtype_java tenv dom_type1 dom_type2
| Typ.Tptr (dom_type1, _), Typ.Tptr (dom_type2, _) ->
| Tptr (dom_type1, _), Tptr (dom_type2, _) ->
check_subtype_java tenv dom_type1 dom_type2
| Typ.Tarray _, Typ.Tstruct { name = TN_csu (Class Java, _) as cn2 } ->
| Tarray _, Tstruct (TN_csu (Class Java, _) as cn2) ->
Typename.equal cn2 serializable_type
|| Typename.equal cn2 cloneable_type
|| Typename.equal cn2 object_type
| _ -> check_subtype_basic_type t1 t2
let get_type_name (t: Typ.t) =
match t with
| Tvar name | Tstruct { name } -> Some name
| _ -> None
(** check if t1 is a subtype of t2 *)
let check_subtype tenv t1 t2 =
if is_java_class tenv t1
then
check_subtype_java tenv t1 t2
else
match get_type_name t1, get_type_name t2 with
match Typ.name t1, Typ.name t2 with
| Some cn1, Some cn2 -> check_subclass tenv cn1 cn2
| _ -> false
let rec case_analysis_type_java tenv (t1, st1) (t2, st2) =
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 } ->
let rec case_analysis_type_java tenv ((t1: Typ.t), st1) ((t2: Typ.t), st2) =
match t1, t2 with
| Tstruct (TN_csu (Class Java, _) as cn1), Tstruct (TN_csu (Class Java, _) as cn2) ->
Subtype.case_analysis (cn1, st1) (cn2, st2)
(check_subclass tenv) (is_interface tenv)
| Typ.Tarray (dom_type1, _), Typ.Tarray (dom_type2, _) ->
| Tarray (dom_type1, _), Tarray (dom_type2, _) ->
case_analysis_type_java tenv (dom_type1, st1) (dom_type2, st2)
| Typ.Tptr (dom_type1, _), Typ.Tptr (dom_type2, _) ->
| Tptr (dom_type1, _), Tptr (dom_type2, _) ->
case_analysis_type_java tenv (dom_type1, st1) (dom_type2, st2)
| Typ.Tstruct { name = TN_csu (Class Java, _) as cn1 }, Typ.Tarray _ ->
| Tstruct (TN_csu (Class Java, _) as cn1), Tarray _ ->
if (Typename.equal cn1 serializable_type
|| Typename.equal cn1 cloneable_type
|| Typename.equal cn1 object_type) &&
st1 <> Subtype.exact then Some st1, None
else (None, Some st1)
| _ -> if check_subtype_basic_type t1 t2 then Some st1, None
else None, Some st1
let case_analysis_type tenv (t1, st1) (t2, st2) =
if is_java_class tenv t1 then
case_analysis_type_java tenv (t1, st1) (t2, st2)
else match get_type_name t1, get_type_name t2 with
else match Typ.name t1, Typ.name t2 with
| Some cn1, Some cn2 ->
(* cn1 <: cn2 or cn2 <: cn1 is implied in Java when we get two types compared *)
(* that get through the type system, but not in C++ because of multiple inheritance, *)
@ -1660,13 +1658,18 @@ 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 typ =
match Tenv.expand_type tenv typ with
| Tstruct { methods } ->
IList.exists (fun m -> Procname.equal pname m) methods
let typ_has_method pname (typ: Typ.t) =
match typ with
| Tstruct name -> (
match Tenv.lookup tenv name with
| Some { methods } ->
IList.exists (fun m -> Procname.equal pname m) methods
| None ->
false
)
| _ -> false in
let gather_overrides tname struct_typ overrides_acc =
let typ = Typ.Tstruct struct_typ in
let gather_overrides tname {Typ.name} overrides_acc =
let typ = Typ.Tstruct name in
(* get all types in the type environment that are non-reflexive subtypes of [supertype] *)
if not (Typ.equal typ supertype) && Subtyping_check.check_subtype tenv typ supertype then
(* only select the ones that implement [pname] as overrides *)
@ -1689,17 +1692,14 @@ 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 (typ1_0, _, _), Exp.Sizeof (typ2_0, _, _) -> (
let typ1 = expand_type typ1_0 in
let typ2 = expand_type typ2_0 in
| Exp.Sizeof (typ1, _, _), Exp.Sizeof (typ2, _, _) -> (
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)
|| (Typ.is_cpp_class typ1 && Typ.is_cpp_class typ2)
|| (Typ.is_objc_class typ1 && Typ.is_objc_class typ2)
| _ ->
false
)
@ -1760,11 +1760,10 @@ let handle_parameter_subtype tenv prop1 sigma2 subs (e1, se1, texp1) (se2, texp2
| _ -> false in
if IList.exists filter sigma2 then !sub_opt else None in
let add_subtype () = match texp1, texp2, se1, se2 with
| Exp.Sizeof (Typ.Tptr (t1_, _), None, _), Exp.Sizeof (Typ.Tptr (t2_, _), None, _),
| Exp.Sizeof (Tptr (t1, _), None, _), Exp.Sizeof (Tptr (t2, _), None, _),
Sil.Eexp (e1', _), Sil.Eexp (e2', _)
when not (is_allocated_lhs e1') ->
begin
let t1, t2 = Tenv.expand_type tenv t1_, Tenv.expand_type tenv t2_ in
match type_rhs e2' with
| Some (t2_ptsto, len2, sub2) ->
if not (Typ.equal t1 t2) && Subtyping_check.check_subtype tenv t1 t2
@ -2009,12 +2008,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
| Config.Clang ->
Exp.Sizeof (Typ.Tarray (Typ.Tint Typ.IChar, Some len), None, Subtype.exact)
| Config.Java ->
let object_type =
Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.String") in
let typ = match Tenv.lookup tenv object_type with
| Some typ -> typ
| None -> assert false in
Exp.Sizeof (Typ.Tstruct typ, None, Subtype.exact) in
let object_type = Typename.Java.from_string "java.lang.String" in
Exp.Sizeof (Tstruct object_type, None, Subtype.exact) in
Sil.Hpointsto (root, sexp, const_string_texp) in
let mk_constant_class_hpred s = (* creat an hpred from a constant class *)
let root = Exp.Const (Const.Cclass (Ident.string_to_name s)) in
@ -2023,12 +2018,8 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
([(Ident.create_fieldname (Mangled.from_string "java.lang.Class.name") 0,
Sil.Eexp ((Exp.Const (Const.Cstr s), Sil.Inone)))], Sil.inst_none) in
let class_texp =
let class_type =
Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string "java.lang.Class") in
let typ = match Tenv.lookup tenv class_type with
| Some typ -> typ
| None -> assert false in
Exp.Sizeof (Typ.Tstruct typ, None, Subtype.exact) in
let class_type = Typename.Java.from_string "java.lang.Class" in
Exp.Sizeof (Tstruct class_type, None, Subtype.exact) in
Sil.Hpointsto (root, sexp, class_texp) in
try
(match move_primed_lhs_from_front subs sigma2 with

218
infer/src/backend/rearrange.ml
Unescape View File

@ -84,7 +84,7 @@ let bounds_check tenv pname prop len e =
end;
check_bad_index tenv pname prop len e
let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp t
let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp (t: Typ.t)
(off: Sil.offset list) inst : Sil.atom list * Sil.strexp * Typ.t =
if Config.trace_rearrange then
begin
@ -97,27 +97,35 @@ 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 Tenv.expand_type tenv t, off with
let fail t off pos =
L.d_str "create_struct_values type:"; Typ.d_full t;
L.d_str " off: "; Sil.d_offset_list off; L.d_ln();
raise (Exceptions.Bad_footprint pos) in
match t, off with
| Tstruct _, [] ->
([], Sil.Estruct ([], inst), t)
| Tstruct ({ name; fields; statics } as struct_typ ),
(Sil.Off_fld (f, _)):: off' ->
let _, t', _ =
try
IList.find (fun (f', _, _) -> Ident.fieldname_equal f f')
(fields @ statics)
with Not_found ->
raise (Exceptions.Bad_footprint __POS__) in
let atoms', se', res_t' =
create_struct_values
pname tenv orig_prop footprint_part kind max_stamp t' off' inst in
let se = Sil.Estruct ([(f, se')], inst) in
let replace_typ_of_f (f', t', a') =
if Ident.fieldname_equal f f' then (f, res_t', a') else (f', t', a') in
let fields' =
IList.sort Typ.fld_typ_ann_compare (IList.map replace_typ_of_f fields) in
(atoms', se, Typ.Tstruct (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name))
| Typ.Tstruct _, (Sil.Off_index e):: off' ->
| Tstruct name, (Off_fld (f, _)) :: off' -> (
match Tenv.lookup tenv name with
| Some ({ name; fields; statics; } as struct_typ) -> (
match IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') (fields @ statics) with
| _, t', _ ->
let atoms', se', res_t' =
create_struct_values
pname tenv orig_prop footprint_part kind max_stamp t' off' inst in
let se = Sil.Estruct ([(f, se')], inst) in
let replace_typ_of_f (f', t', a') =
if Ident.fieldname_equal f f' then (f, res_t', a') else (f', t', a') in
let fields' =
IList.sort Typ.fld_typ_ann_compare (IList.map replace_typ_of_f fields) in
ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ;
(atoms', se, t)
| exception Not_found ->
fail t off __POS__
)
| None ->
fail t off __POS__
)
| Tstruct _, (Off_index e) :: off' ->
let atoms', se', res_t' =
create_struct_values
pname tenv orig_prop footprint_part kind max_stamp t off' inst in
@ -125,8 +133,8 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
let len = Exp.Var (new_id ()) in
let se = Sil.Earray (len, [(e', se')], inst) in
let res_t = Typ.Tarray (res_t', None) in
(Sil.Aeq(e, e') :: atoms', se, res_t)
| Typ.Tarray (t', len_), off ->
(Sil.Aeq (e, e') :: atoms', se, res_t)
| Tarray (t', len_), off ->
let len = match len_ with
| None -> Exp.Var (new_id ())
| Some len -> Exp.Const (Const.Cint len) in
@ -145,10 +153,10 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
| (Sil.Off_fld _) :: _ ->
assert false
)
| Typ.Tint _, [] | Typ.Tfloat _, [] | Typ.Tvoid, [] | Typ.Tfun _, [] | Typ.Tptr _, [] ->
| Tint _, [] | Tfloat _, [] | Tvoid, [] | Tfun _, [] | Tptr _, [] ->
let id = new_id () in
([], Sil.Eexp (Exp.Var id, inst), t)
| (Typ.Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), (Sil.Off_index e)::off' ->
| (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _), (Off_index e) :: off' ->
(* In this case, we lift t to the t array. *)
let t' = match t with
| Typ.Tptr(t', _) -> t'
@ -160,17 +168,10 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
let e' = Sil.array_clean_new_index footprint_part e in
let se = Sil.Earray (len, [(e', se')], inst) in
let res_t = Typ.Tarray (res_t', None) in
(Sil.Aeq(e, e'):: atoms', se, res_t)
| Typ.Tint _, _ | Typ.Tfloat _, _ | Typ.Tvoid, _ | Typ.Tfun _, _ | Typ.Tptr _, _ ->
L.d_str "create_struct_values type:"; Typ.d_full t;
L.d_str " off: "; Sil.d_offset_list off; L.d_ln();
raise (Exceptions.Bad_footprint __POS__)
| Typ.Tvar _, _ ->
L.d_str "create_struct_values type:"; Typ.d_full t;
L.d_str " off: "; Sil.d_offset_list off; L.d_ln();
assert false in
(Sil.Aeq(e, e') :: atoms', se, res_t)
| Tint _, _ | Tfloat _, _ | Tvoid, _ | Tfun _, _ | Tptr _, _ ->
fail t off __POS__
in
if Config.trace_rearrange then
begin
let _, se, _ = res in
@ -188,68 +189,68 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
we need to change this function. *)
let rec _strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp
se typ (off : Sil.offset list) inst =
se (typ: Typ.t) (off : Sil.offset list) inst =
let new_id () =
incr max_stamp;
Ident.create kind !max_stamp in
match off, se, Tenv.expand_type tenv typ with
match off, se, typ with
| [], Sil.Eexp _, _
| [], Sil.Estruct _, _ ->
[([], se, typ)]
| [], Sil.Earray _, _ ->
let off_new = Sil.Off_index(Exp.zero):: off in
let off_new = Sil.Off_index (Exp.zero):: off in
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
| (Sil.Off_fld _) :: _, Sil.Earray _, Typ.Tarray _ ->
let off_new = Sil.Off_index(Exp.zero):: off in
| (Off_fld _) :: _, Sil.Earray _, Tarray _ ->
let off_new = Sil.Off_index (Exp.zero):: off in
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se typ off_new inst
| (Sil.Off_fld (f, _)):: off', Sil.Estruct (fsel, inst'),
Tstruct ({ name; fields; statics } as struct_typ) ->
let replace_fv new_v fv = if Ident.fieldname_equal (fst fv) f then (f, new_v) else fv in
let _, typ', _ =
try
IList.find (fun (f', _, _) -> Ident.fieldname_equal f f')
(fields @ statics)
with Not_found ->
raise (Exceptions.Missing_fld (f, __POS__)) in
begin
try
let _, se' = IList.find (fun (f', _) -> Ident.fieldname_equal f f') fsel in
let atoms_se_typ_list' =
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se' typ' off' inst in
let replace acc (res_atoms', res_se', res_typ') =
let replace_fse = replace_fv res_se' in
let res_fsel' = IList.sort Sil.fld_strexp_compare (IList.map replace_fse fsel) in
let replace_fta (f, t, a) = let f', t' = replace_fv res_typ' (f, t) in (f', t', a) in
let fields' =
IList.sort Typ.fld_typ_ann_compare (IList.map replace_fta fields) in
let struct_typ =
Typ.Tstruct (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) in
(res_atoms', Sil.Estruct (res_fsel', inst'), struct_typ) :: acc in
IList.fold_left replace [] atoms_se_typ_list'
with Not_found ->
let atoms', se', res_typ' =
create_struct_values
pname tenv orig_prop footprint_part kind max_stamp typ' off' inst in
let res_fsel' = IList.sort Sil.fld_strexp_compare ((f, se'):: fsel) in
let replace_fta (f', t', a') = if Ident.fieldname_equal f' f then (f, res_typ', a') else (f', t', a') in
let fields' =
IList.sort Typ.fld_typ_ann_compare (IList.map replace_fta fields) in
let struct_typ =
Typ.Tstruct (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) in
[(atoms', Sil.Estruct (res_fsel', inst'), struct_typ)]
end
| (Sil.Off_fld (_, _)):: _, _, _ ->
| (Off_fld (f, _)) :: off', Sil.Estruct (fsel, inst'), Tstruct name -> (
match Tenv.lookup tenv name with
| Some ({ name; fields; statics; } as struct_typ) -> (
let replace_fv new_v fv = if Ident.fieldname_equal (fst fv) f then (f, new_v) else fv in
match IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') (fields @ statics) with
| _, typ', _ -> (
match IList.find (fun (f', _) -> Ident.fieldname_equal f f') fsel with
| _, se' ->
let atoms_se_typ_list' =
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se' typ' off' inst in
let replace acc (res_atoms', res_se', res_typ') =
let replace_fse = replace_fv res_se' in
let res_fsel' =
IList.sort Sil.fld_strexp_compare (IList.map replace_fse fsel) in
let replace_fta (f, t, a) =
let f', t' = replace_fv res_typ' (f, t) in
(f', t', a) in
let fields' =
IList.sort Typ.fld_typ_ann_compare (IList.map 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
IList.fold_left replace [] atoms_se_typ_list'
| exception Not_found ->
let atoms', se', res_typ' =
create_struct_values
pname tenv orig_prop footprint_part kind max_stamp typ' off' inst in
let res_fsel' = IList.sort Sil.fld_strexp_compare ((f, se'):: fsel) in
let replace_fta (f', t', a') =
if Ident.fieldname_equal f' f then (f, res_typ', a') else (f', t', a') in
let fields' =
IList.sort Typ.fld_typ_ann_compare (IList.map replace_fta fields) in
ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ;
[(atoms', Sil.Estruct (res_fsel', inst'), typ)]
)
| exception Not_found ->
raise (Exceptions.Missing_fld (f, __POS__))
)
| None ->
raise (Exceptions.Missing_fld (f, __POS__))
)
| (Off_fld _) :: _, _, _ ->
raise (Exceptions.Bad_footprint __POS__)
| (Sil.Off_index _):: _, Sil.Eexp _, Typ.Tint _
| (Sil.Off_index _):: _, Sil.Eexp _, Typ.Tfloat _
| (Sil.Off_index _):: _, Sil.Eexp _, Typ.Tvoid
| (Sil.Off_index _):: _, Sil.Eexp _, Typ.Tfun _
| (Sil.Off_index _):: _, Sil.Eexp _, Typ.Tptr _
| (Sil.Off_index _):: _, Sil.Estruct _, Typ.Tstruct _ ->
| (Off_index _) :: _, Sil.Eexp _, (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _)
| (Off_index _) :: _, Sil.Estruct _, Tstruct _ ->
(* L.d_strln_color Orange "turn into an array"; *)
let len = match se with
| Sil.Eexp (_, Sil.Ialloc) -> Exp.one (* if allocated explicitly, we know len is 1 *)
@ -260,11 +261,10 @@ let rec _strexp_extend_values
let typ_new = Typ.Tarray (typ, None) in
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se_new typ_new off inst
| (Sil.Off_index e) :: off', Sil.Earray (len, esel, inst_arr), Typ.Tarray (typ', len_for_typ') ->
| (Off_index e) :: off', Sil.Earray (len, esel, inst_arr), Tarray (typ', len_for_typ') -> (
bounds_check tenv pname orig_prop len e (State.get_loc ());
begin
try
let _, se' = IList.find (fun (e', _) -> Exp.equal e e') esel in
match IList.find (fun (e', _) -> Exp.equal e e') esel with
| _, se' ->
let atoms_se_typ_list' =
_strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se' typ' off' inst in
@ -279,13 +279,13 @@ let rec _strexp_extend_values
else
raise (Exceptions.Bad_footprint __POS__) in
IList.fold_left replace [] atoms_se_typ_list'
with Not_found ->
| exception Not_found ->
array_case_analysis_index pname tenv orig_prop
footprint_part kind max_stamp
len esel
len_for_typ' typ'
e off' inst_arr inst
end
)
| _, _, _ ->
raise (Exceptions.Bad_footprint __POS__)
@ -614,7 +614,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 lookup = Tenv.lookup 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 *)
@ -655,7 +655,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 ~expand_ptr_type fld typ with
match Typ.get_field_type_and_annotation ~lookup fld typ with
| Some (_, item_annot) ->
begin
match extract_guarded_by_str item_annot with
@ -683,7 +683,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 ~expand_ptr_type fld typ with
match Typ.get_field_type_and_annotation ~lookup fld typ with
| Some (fld_typ, _) -> Some (strexp, fld_typ)
| None -> None
end
@ -731,8 +731,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
let rec is_read_write_lock typ =
let str_is_read_write_lock str = string_is_suffix "ReadWriteUpdateLock" str in
match typ with
| Typ.Tvar name
| Typ.Tstruct { name } -> str_is_read_write_lock (Typename.name name)
| Typ.Tstruct name -> str_is_read_write_lock (Typename.name name)
| Typ.Tptr (typ, _) -> is_read_write_lock typ
| _ -> false in
let has_lock guarded_by_exp =
@ -1029,17 +1028,20 @@ let iter_rearrange_pe_dllseg_last tenv recurse_on_iters default_case_iter iter p
(** 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, Tenv.expand_type tenv typ with
let rec strip_offset (off: Sil.offset list) (typ: Typ.t) =
match off, typ with
| [], _ -> Some typ
| (Sil.Off_fld (f, _)):: off', Tstruct { fields } ->
(try
let typ' =
(fun (_, y, _) -> y)
(IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') fields) in
strip_offset off' typ'
with Not_found -> None)
| (Sil.Off_index _) :: off', Typ.Tarray (typ', _) ->
| (Off_fld (f, _)) :: off', Tstruct name -> (
match Tenv.lookup tenv name with
| Some { fields } -> (
match IList.find (fun (f', _, _) -> Ident.fieldname_equal f f') fields with
| _, typ', _ -> strip_offset off' typ'
| exception Not_found -> None
)
| None ->
None
)
| (Off_index _) :: off', Tarray (typ', _) ->
strip_offset off' typ'
| _ -> None in
match texp with
@ -1083,7 +1085,7 @@ let rec iter_rearrange
inst: (Sil.offset list) Prop.prop_iter list =
let rec root_typ_of_offsets = function
| Sil.Off_fld (f, fld_typ) :: _ -> (
match Tenv.expand_type tenv fld_typ with
match fld_typ with
| Tstruct _ as struct_typ ->
(* access through field: get the struct type from the field *)
if Config.trace_rearrange then begin
@ -1195,7 +1197,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 lookup = Tenv.lookup 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 *)
@ -1227,7 +1229,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 ~expand_ptr_type fld typ with
match Typ.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) =

201
infer/src/backend/symExec.ml
Unescape View File

@ -19,29 +19,29 @@ let rec fldlist_assoc fld = function
| [] -> raise Not_found
| (fld', x, _):: l -> if Ident.fieldname_equal fld fld' then x else fldlist_assoc fld l
let rec unroll_type tenv typ off =
let unroll_type tenv (typ: Typ.t) (off: Sil.offset) =
let fail fld_to_string fld =
L.d_strln ".... Invalid Field Access ....";
L.d_str ("Fld : " ^ fld_to_string fld); L.d_ln ();
L.d_str "Type : "; Typ.d_full typ; L.d_ln ();
raise (Exceptions.Bad_footprint __POS__)
in
match (typ, off) with
| Typ.Tvar _, _ ->
let typ' = Tenv.expand_type tenv typ in
unroll_type tenv typ' off
| Typ.Tstruct { fields; statics }, Sil.Off_fld (fld, _) ->
begin
try fldlist_assoc fld (fields @ statics)
with Not_found ->
L.d_strln ".... Invalid Field Access ....";
L.d_strln ("Fld : " ^ Ident.fieldname_to_string fld);
L.d_str "Type : "; Typ.d_full typ; L.d_ln ();
raise (Exceptions.Bad_footprint __POS__)
end
| Typ.Tarray (typ', _), Sil.Off_index _ ->
| Tstruct name, Off_fld (fld, _) -> (
match Tenv.lookup tenv name with
| Some { fields; statics } -> (
try fldlist_assoc fld (fields @ statics)
with Not_found -> fail Ident.fieldname_to_string fld
)
| None ->
fail Ident.fieldname_to_string fld
)
| Tarray (typ', _), Off_index _ ->
typ'
| _, Sil.Off_index (Exp.Const (Const.Cint i)) when IntLit.iszero i ->
| _, Off_index (Const (Cint i)) when IntLit.iszero i ->
typ
| _ ->
L.d_strln ".... Invalid Field Access ....";
L.d_str "Fld : "; Sil.d_offset off; L.d_ln ();
L.d_str "Type : "; Typ.d_full typ; L.d_ln ();
assert false
fail Sil.offset_to_string off
(** Given a node, returns a list of pvar of blocks that have been nullified in the block. *)
let get_blocks_nullified node =
@ -90,8 +90,8 @@ let rec apply_offlist
L.d_str "offlist : "; Sil.d_offset_list offlist; L.d_ln ();
L.d_str "type : "; Typ.d_full typ; L.d_ln ();
L.d_str "prop : "; Prop.d_prop p; L.d_ln (); L.d_ln () in
match offlist, strexp with
| [], Sil.Eexp (e, inst_curr) ->
match offlist, strexp, typ with
| [], Sil.Eexp (e, inst_curr), _ ->
let inst_is_uninitialized = function
| Sil.Ialloc ->
(* java allocation initializes with default values *)
@ -122,7 +122,7 @@ let rec apply_offlist
| _ -> Sil.update_inst inst_curr inst in
let e' = f (Some e) in
(e', Sil.Eexp (e', inst_new), typ, None)
| [], Sil.Estruct (fesl, inst') ->
| [], Sil.Estruct (fesl, inst'), _ ->
if not nullify_struct then (f None, Sil.Estruct (fesl, inst'), typ, None)
else if fp_root then (pp_error(); assert false)
else
@ -130,76 +130,73 @@ let rec apply_offlist
L.d_strln "WARNING: struct assignment treated as nondeterministic assignment";
(f None, Prop.create_strexp_of_type tenv Prop.Fld_init typ None inst, typ, None)
end
| [], Sil.Earray _ ->
| [], Sil.Earray _, _ ->
let offlist' = (Sil.Off_index Exp.zero):: offlist in
apply_offlist
pdesc tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist' f inst lookup_inst
| (Sil.Off_fld _):: _, Sil.Earray _ ->
| (Sil.Off_fld _) :: _, Sil.Earray _, _ ->
let offlist_new = Sil.Off_index(Exp.zero) :: offlist in
apply_offlist
pdesc tenv p fp_root nullify_struct (root_lexp, strexp, typ) offlist_new f inst lookup_inst
| (Sil.Off_fld (fld, fld_typ)):: offlist', Sil.Estruct (fsel, inst') ->
begin
let typ' = Tenv.expand_type tenv typ in
let { Typ.name; fields; } as struct_typ =
match typ' with
| Tstruct struct_typ -> struct_typ
| _ -> assert false in
let t' = unroll_type tenv typ (Sil.Off_fld (fld, fld_typ)) in
try
let _, se' = IList.find (fun fse -> Ident.fieldname_equal fld (fst fse)) fsel in
let res_e', res_se', res_t', res_pred_insts_op' =
apply_offlist
pdesc tenv p fp_root nullify_struct
(root_lexp, se', t') offlist' f inst lookup_inst in
let replace_fse fse =
if Ident.fieldname_equal fld (fst fse) then (fld, res_se') else fse in
let res_se = Sil.Estruct (IList.map replace_fse fsel, inst') in
let replace_fta (f, t, a) =
if Ident.fieldname_equal fld f then (fld, res_t', a) else (f, t, a) in
let fields' = IList.map replace_fta fields in
let res_t = Typ.Tstruct (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) in
(res_e', res_se, res_t, res_pred_insts_op')
with Not_found ->
| (Sil.Off_fld (fld, fld_typ)) :: offlist', Sil.Estruct (fsel, inst'), Typ.Tstruct name -> (
match Tenv.lookup tenv name with
| Some ({fields} as struct_typ) -> (
let t' = unroll_type tenv typ (Sil.Off_fld (fld, fld_typ)) in
match IList.find (fun fse -> Ident.fieldname_equal fld (fst fse)) fsel with
| _, se' ->
let res_e', res_se', res_t', res_pred_insts_op' =
apply_offlist
pdesc tenv p fp_root nullify_struct
(root_lexp, se', t') offlist' f inst lookup_inst in
let replace_fse fse =
if Ident.fieldname_equal fld (fst fse) then (fld, res_se') else fse in
let res_se = Sil.Estruct (IList.map replace_fse fsel, inst') in
let replace_fta (f, t, a) =
if Ident.fieldname_equal fld f then (fld, res_t', a) else (f, t, a) in
let fields' = IList.map replace_fta fields in
ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ;
(res_e', res_se, typ, res_pred_insts_op')
| exception Not_found ->
(* This case should not happen. The rearrangement should
have materialized all the accessed cells. *)
pp_error();
assert false
)
| None ->
pp_error();
assert false
(* This case should not happen. The rearrangement should
have materialized all the accessed cells. *)
end
| (Sil.Off_fld _):: _, _ ->
)
| (Sil.Off_fld _) :: _, _, _ ->
pp_error();
assert false
| (Sil.Off_index idx) :: offlist', Sil.Earray (len, esel, inst1) ->
| (Sil.Off_index idx) :: offlist', Sil.Earray (len, esel, inst1), Typ.Tarray (t', len') -> (
let nidx = Prop.exp_normalize_prop tenv p idx in
begin
let typ' = Tenv.expand_type tenv typ in
let t', len' = match typ' with Typ.Tarray (t', len') -> (t', len') | _ -> assert false in
try
let idx_ese', se' = IList.find (fun ese -> Prover.check_equal tenv p nidx (fst ese)) esel in
let res_e', res_se', res_t', res_pred_insts_op' =
apply_offlist
pdesc tenv p fp_root nullify_struct
(root_lexp, se', t') offlist' f inst lookup_inst in
let replace_ese ese =
if Exp.equal idx_ese' (fst ese)
then (idx_ese', res_se')
else ese in
let res_se = Sil.Earray (len, IList.map replace_ese esel, inst1) in
let res_t = Typ.Tarray (res_t', len') in
(res_e', res_se, res_t, res_pred_insts_op')
with Not_found ->
(* return a nondeterministic value if the index is not found after rearrangement *)
L.d_str "apply_offlist: index "; Sil.d_exp idx;
L.d_strln " not materialized -- returning nondeterministic value";
let res_e' = Exp.Var (Ident.create_fresh Ident.kprimed) in
(res_e', strexp, typ, None)
end
| (Sil.Off_index _):: _, _ ->
try
let idx_ese', se' = IList.find (fun ese -> Prover.check_equal tenv p nidx (fst ese)) esel in
let res_e', res_se', res_t', res_pred_insts_op' =
apply_offlist
pdesc tenv p fp_root nullify_struct
(root_lexp, se', t') offlist' f inst lookup_inst in
let replace_ese ese =
if Exp.equal idx_ese' (fst ese)
then (idx_ese', res_se')
else ese in
let res_se = Sil.Earray (len, IList.map replace_ese esel, inst1) in
let res_t = Typ.Tarray (res_t', len') in
(res_e', res_se, res_t, res_pred_insts_op')
with Not_found ->
(* return a nondeterministic value if the index is not found after rearrangement *)
L.d_str "apply_offlist: index "; Sil.d_exp idx;
L.d_strln " not materialized -- returning nondeterministic value";
let res_e' = Exp.Var (Ident.create_fresh Ident.kprimed) in
(res_e', strexp, typ, None)
)
| (Sil.Off_index _) :: _, _, _ ->
(* This case should not happen. The rearrangement should
have materialized all the accessed cells. *)
pp_error();
raise (Exceptions.Internal_error (Localise.verbatim_desc "Array out of bounds in Symexec"))
(* This case should not happen. The rearrangement should
have materialized all the accessed cells. *)
(** Given [lexp |-> se: typ], if the location [offlist] exists in [se],
function [ptsto_lookup p (lexp, se, typ) offlist id] returns a tuple.
@ -532,7 +529,7 @@ let resolve_typename prop receiver_exp =
| _ :: hpreds -> loop hpreds in
loop prop.Prop.sigma in
match typexp_opt with
| Some (Exp.Sizeof ((Tvar name | Tstruct { name }), _, _)) -> Some name
| Some (Exp.Sizeof (Tstruct name, _, _)) -> Some name
| _ -> None
(** If the dynamic type of the receiver actual T_actual is a subtype of the reciever type T_formal
@ -545,8 +542,8 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t
match pname with
| Procname.Java pname_java ->
begin
match Tenv.proc_extract_declaring_class_typ tenv pname_java with
| Some struct_typ -> Typ.Tptr (Tstruct struct_typ, Pk_pointer)
match Tenv.lookup_declaring_class tenv pname_java with
| Some {name} -> Typ.Tptr (Tstruct name, Pk_pointer)
| None -> fallback_typ
end
| _ ->
@ -873,11 +870,7 @@ let add_taint prop lhs_id rhs_exp pname tenv =
else
prop in
match rhs_exp with
| Exp.Lfield (_, fieldname, Tptr (Tstruct struct_typ, _))
| Exp.Lfield (_, fieldname, Tstruct struct_typ) ->
add_attribute_if_field_tainted prop fieldname struct_typ
| Exp.Lfield (_, fieldname, Tptr (Tvar typname, _))
| Exp.Lfield (_, fieldname, Tvar typname) ->
| Exp.Lfield (_, fieldname, (Tstruct typname | Tptr (Tstruct typname, _))) ->
begin
match Tenv.lookup tenv typname with
| Some struct_typ -> add_attribute_if_field_tainted prop fieldname struct_typ
@ -923,7 +916,7 @@ let execute_load ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ loc
assert false in
try
let n_rhs_exp, prop = check_arith_norm_exp tenv pname rhs_exp prop_ in
let n_rhs_exp' = Prop.exp_collapse_consecutive_indices_prop tenv typ n_rhs_exp in
let n_rhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_rhs_exp in
match check_constant_string_dereference n_rhs_exp' with
| Some value ->
[Prop.conjoin_eq tenv (Exp.Var id) value prop]
@ -983,7 +976,7 @@ let execute_store ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_e
let n_lhs_exp, prop_' = check_arith_norm_exp tenv pname lhs_exp prop_ in
let n_rhs_exp, prop = check_arith_norm_exp tenv pname rhs_exp prop_' in
let prop = Attribute.replace_objc_null tenv prop n_lhs_exp n_rhs_exp in
let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop tenv typ n_lhs_exp in
let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in
let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in
IList.rev (IList.fold_left (execute_store_ pdesc tenv n_rhs_exp) [] iter_list)
with Rearrange.ARRAY_ACCESS ->
@ -1084,11 +1077,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
begin
match summary_opt with
| None ->
let ret_typ =
match Tenv.proc_extract_return_typ tenv callee_pname_java with
| Some (Typ.Tstruct _ as typ) -> Typ.Tptr (typ, Pk_pointer)
| Some typ -> typ
| None -> Typ.Tvoid in
let ret_typ = Typ.java_proc_return_typ callee_pname_java in
let ret_annots = load_ret_annots callee_pname in
exec_skip_call resolved_pname ret_annots ret_typ
| Some summary when call_should_be_skipped resolved_pname summary ->
@ -1114,11 +1103,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
skip_call norm_prop path pname ret_annots loc ret_ids (Some ret_type) url_handled_args in
match Specs.get_summary pname with
| None ->
let ret_typ =
match Tenv.proc_extract_return_typ tenv callee_pname_java with
| Some (Typ.Tstruct _ as typ) -> Typ.Tptr (typ, Pk_pointer)
| Some typ -> typ
| None -> Typ.Tvoid in
let ret_typ = Typ.java_proc_return_typ callee_pname_java in
let ret_annots = load_ret_annots callee_pname in
exec_skip_call ret_annots ret_typ
| Some summary when call_should_be_skipped pname summary ->
@ -1301,8 +1286,8 @@ and add_constraints_on_actuals_by_ref tenv prop actuals_by_ref callee_pname call
else
if !Config.footprint then
let prop', abduced_strexp =
match Tenv.expand_type tenv actual_typ with
| Typ.Tptr ((Typ.Tstruct _) as typ, _) ->
match actual_typ with
| Typ.Tptr ((Tstruct _) as typ, _) ->
(* for struct types passed by reference, do abduction on the fields of the
struct *)
add_struct_value_to_footprint tenv abduced_ref_pv typ prop
@ -1523,12 +1508,8 @@ and sym_exec_objc_getter field_name ret_typ tenv ret_ids pdesc pname loc args pr
| [ret_id] -> ret_id
| _ -> assert false in
match args with
| [(lexp, typ)] ->
let typ' = (match Tenv.expand_type tenv typ with
| Typ.Tstruct _ as s -> s
| Typ.Tptr (t, _) -> Tenv.expand_type tenv t
| _ -> assert false) in
let field_access_exp = Exp.Lfield (lexp, field_name, typ') in
| [(lexp, (Typ.Tstruct _ as typ | Tptr (Tstruct _ as typ, _)))] ->
let field_access_exp = Exp.Lfield (lexp, field_name, typ) in
execute_load
~report_deref_errors:false pname pdesc tenv ret_id field_access_exp ret_typ loc prop
| _ -> raise (Exceptions.Wrong_argument_number __POS__)
@ -1537,12 +1518,8 @@ and sym_exec_objc_setter field_name _ tenv _ pdesc pname loc args prop =
L.d_strln ("No custom setter found. Executing the ObjC builtin setter with ivar "^
(Ident.fieldname_to_string field_name)^".");
match args with
| (lexp1, typ1) :: (lexp2, typ2)::_ ->
let typ1' = (match Tenv.expand_type tenv typ1 with
| Typ.Tstruct _ as s -> s
| Typ.Tptr (t, _) -> Tenv.expand_type tenv t
| _ -> assert false) in
let field_access_exp = Exp.Lfield (lexp1, field_name, typ1') in
| (lexp1, (Typ.Tstruct _ as typ1 | Tptr (typ1, _))) :: (lexp2, typ2) :: _ ->
let field_access_exp = Exp.Lfield (lexp1, field_name, typ1) in
execute_store ~report_deref_errors:false pname pdesc tenv field_access_exp typ2 lexp2 loc prop
| _ -> raise (Exceptions.Wrong_argument_number __POS__)

20
infer/src/backend/tabulation.ml
Unescape View File

@ -466,13 +466,17 @@ 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 Tenv.expand_type tenv t1, Tenv.expand_type tenv t2 with
| Tstruct { fields = fields1; name = TN_csu (csu1, _) },
Tstruct { fields = fields2; name = TN_csu (csu2, _) }
when csu1 = csu2 ->
if ftal_sub fields1 fields2 then t2 else t1
| _ -> t1 in
let typ_star (t1: Typ.t) (t2: Typ.t) =
match t1, t2 with
| Tstruct (TN_csu (csu1, _) as name1), Tstruct (TN_csu (csu2, _) as name2) when csu1 = csu2 -> (
match Tenv.lookup tenv name1, Tenv.lookup tenv name2 with
| Some { fields = fields1 }, Some { fields = fields2 } when ftal_sub fields1 fields2 ->
t2
| _ ->
t1
)
| _ ->
t1 in
match texp1, texp2 with
| Exp.Sizeof (t1, len1, st1), Exp.Sizeof (t2, _, st2) ->
Exp.Sizeof (typ_star t1 t2, len1, Subtype.join st1 st2)
@ -626,7 +630,7 @@ 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 ((Tvar name | Tstruct { name }), _, _)) :: _
| Sil.Hpointsto (e1, _, Sizeof (Tstruct name, _, _)) :: _
when Exp.equal e1 e ->
Some name
| _ :: tl -> search_exn e tl in

2
infer/src/checkers/annotationReachability.ml
Unescape View File

@ -139,7 +139,7 @@ let check_attributes check tenv pname =
let check_class_annots { Typ.annots; } =
check annots in
begin
match Tenv.proc_extract_declaring_class_typ tenv java_pname with
match Tenv.lookup_declaring_class tenv java_pname with
| Some current_class ->
check_class_annots current_class ||
PatternMatch.strict_supertype_exists tenv check_class_annots current_class

8
infer/src/checkers/annotations.ml
Unescape View File

@ -38,7 +38,7 @@ let suppressLint = "android.annotation.SuppressLint"
(** Return the annotations on the declaring class of [pname]. Only works for Java *)
let get_declaring_class_annotations pname tenv =
match Tenv.proc_extract_declaring_class_typ tenv pname with
match Tenv.lookup_declaring_class tenv pname with
| Some { annots } -> Some annots
| None -> None
@ -256,9 +256,9 @@ let get_annotated_signature proc_attributes : annotated_signature =
(** Check if the annotated signature is for a wrapper of an anonymous inner class method.
These wrappers have the same name as the original method, every type is Object, and the parameters
are called x0, x1, x2. *)
let annotated_signature_is_anonymous_inner_class_wrapper tenv ann_sig proc_name =
let annotated_signature_is_anonymous_inner_class_wrapper ann_sig proc_name =
let check_ret (ia, t) =
Typ.item_annotation_is_empty ia && PatternMatch.type_is_object tenv t in
Typ.item_annotation_is_empty ia && PatternMatch.type_is_object t in
let x_param_found = ref false in
let name_is_x_number name =
let name_str = Mangled.to_string name in
@ -278,7 +278,7 @@ let annotated_signature_is_anonymous_inner_class_wrapper tenv ann_sig proc_name
else
name_is_x_number name &&
Typ.item_annotation_is_empty ia &&
PatternMatch.type_is_object tenv t in
PatternMatch.type_is_object t in
Procname.java_is_anonymous_inner_class proc_name
&& check_ret ann_sig.ret
&& IList.for_all check_param ann_sig.params

2
infer/src/checkers/annotations.mli
Unescape View File

@ -32,7 +32,7 @@ type annotated_signature = {
(** Check if the annotated signature is for a wrapper of an anonymous inner class method.
These wrappers have the same name as the original method, every type is Object, and the parameters
are called x0, x1, x2. *)
val annotated_signature_is_anonymous_inner_class_wrapper : Tenv.t -> annotated_signature -> Procname.t -> bool
val annotated_signature_is_anonymous_inner_class_wrapper : annotated_signature -> Procname.t -> bool
(** Check if the given parameter has a Nullable annotation in the given signature *)
val param_is_nullable : Pvar.t -> annotated_signature -> bool

26
infer/src/checkers/checkers.ml
Unescape View File

@ -75,7 +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 lookup = Tenv.lookup tenv in
let localized_description = Localise.custom_desc_with_advice
description
(Option.default "" advice)
@ -113,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 ~expand_ptr_type field_name t with
match Typ.get_field_type_and_annotation ~lookup field_name t with
| Some (_, ia) -> Annotations.ia_has_annotation_with ia annotation_matches
| None -> false
end
@ -209,9 +209,12 @@ 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 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
match this_type with
| Typ.Tptr (Tstruct name, _) | Tstruct name -> (
match Tenv.lookup tenv name with
| Some struct_typ -> PatternMatch.is_immediate_subtype struct_typ class_name
| None -> false
)
| _ -> false in
method_match () && expr_match () && type_match () in
@ -221,9 +224,12 @@ let callback_check_write_to_parcel_java
proc_desc pname_java ["android.os.Parcel"] in
let parcel_constructors tenv typ =
match Tenv.expand_ptr_type tenv typ with
| Tptr (Tstruct { methods }, _) ->
IList.filter is_parcel_constructor methods
match typ with
| Typ.Tptr (Tstruct name, _) -> (
match Tenv.lookup tenv name with
| Some { methods } -> IList.filter is_parcel_constructor methods
| None -> []
)
| _ -> [] in
let check r_desc w_desc =
@ -319,14 +325,14 @@ 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.tenv; proc_desc; idenv; proc_name } =
let callback_monitor_nullcheck { Callbacks.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 (p, typ) =
match Tenv.expand_ptr_type tenv typ with
match typ with
| Typ.Tptr _ when Mangled.to_string p = "this" ->
false (* no need to null check 'this' *)
| Typ.Tstruct _ -> true

8
infer/src/checkers/fragmentRetainsViewChecker.ml
Unescape View File

@ -25,11 +25,8 @@ let callback_fragment_retains_view_java
(* TODO: complain if onDestroyView is not defined, yet the Fragment has View fields *)
(* TODO: handle fields nullified in callees in the same file *)
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, _) ->
| Typ.Tptr (Typ.Tstruct tname, _) ->
begin
match Tenv.lookup tenv tname with
| Some struct_typ -> AndroidFramework.is_view tenv struct_typ
@ -55,8 +52,7 @@ let callback_fragment_retains_view_java
(fun (fname, fld_typ, _) ->
if not (Ident.FieldSet.mem fname fields_nullified) then
report_error
(Typ.Tstruct struct_typ) fname fld_typ
(Procname.Java pname_java) proc_desc)
(Tstruct class_typename) fname fld_typ (Procname.Java pname_java) proc_desc)
declared_view_fields
| _ -> ()
end

90
infer/src/checkers/patternMatch.ml
Unescape View File

@ -24,9 +24,9 @@ type taint_spec = {
language : Config.language
}
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
let type_is_object typ =
match typ with
| Typ.Tptr (Tstruct name, _) -> string_equal (Typename.name name) JConfig.object_cl
| _ -> false
let java_proc_name_with_class_method pn_java class_with_path method_name =
@ -75,14 +75,17 @@ let is_subtype_of_str tenv cn1 classname_str =
(** The type the method is invoked on *)
let get_this_type proc_attributes = match proc_attributes.ProcAttributes.formals with
| (_, t):: _ -> Some t
| (_, t) :: _ -> Some t
| _ -> None
let type_get_direct_supertypes tenv typ =
match Tenv.expand_ptr_type tenv typ with
| Tptr (Tstruct { supers }, _)
| Tstruct { supers } ->
supers
let type_get_direct_supertypes tenv (typ: Typ.t) =
match typ with
| Tptr (Tstruct name, _)
| Tstruct name -> (
match Tenv.lookup tenv name with
| Some { supers } -> supers
| None -> []
)
| _ ->
[]
@ -90,11 +93,14 @@ let type_get_class_name = function
| Typ.Tptr (typ, _) -> Typ.name typ
| _ -> None
let type_get_annotation tenv (t: Typ.t): Typ.item_annotation option =
match Tenv.expand_ptr_type tenv t with
| Tptr (Tstruct { annots }, _)
| Tstruct { annots } ->
Some annots
let type_get_annotation tenv (typ: Typ.t): Typ.item_annotation option =
match typ with
| Tptr (Tstruct name, _)
| Tstruct name -> (
match Tenv.lookup tenv name with
| Some { annots } -> Some annots
| None -> None
)
| _ -> None
let type_has_direct_supertype tenv (typ : Typ.t) (class_name : Typename.t) =
@ -108,21 +114,12 @@ let type_has_supertype
if Typ.Set.mem typ visited then
false
else
begin
match Tenv.expand_ptr_type tenv typ with
| Tptr (Tstruct { supers }, _)
| Tstruct { supers } ->
let match_supertype cn =
let match_name () = Typename.equal cn class_name in
let has_indirect_supertype () =
match Tenv.lookup tenv cn with
| Some supertype ->
has_supertype (Typ.Tstruct supertype) (Typ.Set.add typ visited)
| None -> false in
(match_name () || has_indirect_supertype ()) in
IList.exists match_supertype supers
| _ -> false
end in
let supers = type_get_direct_supertypes tenv typ in
let match_supertype cn =
let match_name () = Typename.equal cn class_name in
let has_indirect_supertype () = has_supertype (Typ.Tstruct cn) (Typ.Set.add typ visited) in
(match_name () || has_indirect_supertype ()) in
IList.exists match_supertype supers in
has_supertype typ Typ.Set.empty
let type_is_nested_in_direct_supertype tenv t n =
@ -130,8 +127,7 @@ let type_is_nested_in_direct_supertype tenv t n =
IList.exists (is_nested_in n) (type_get_direct_supertypes tenv t)
let rec get_type_name = function
| Typ.Tvar name
| Typ.Tstruct { name } ->
| Typ.Tstruct name ->
Typename.name name
| Typ.Tptr (t, _) -> get_type_name t
| _ -> "_"
@ -139,15 +135,16 @@ let rec get_type_name = function
let get_field_type_name tenv
(typ: Typ.t)
(fieldname: Ident.fieldname): string option =
match Tenv.expand_ptr_type tenv typ with
| Tstruct { fields }
| Tptr (Tstruct { fields }, _) -> (
try
let _, ft, _ = IList.find
(function | (fn, _, _) -> Ident.fieldname_equal fn fieldname)
fields in
Some (get_type_name ft)
with Not_found -> None)
match typ with
| Tstruct name | Tptr (Tstruct name, _) -> (
match Tenv.lookup tenv name with
| Some { fields } -> (
match IList.find (function | (fn, _, _) -> Ident.fieldname_equal fn fieldname) fields with
| _, ft, _ -> Some (get_type_name ft)
| exception Not_found -> None
)
| None -> None
)
| _ -> None
let java_get_const_type_name
@ -250,10 +247,9 @@ let get_java_method_call_formal_signature = function
| _ -> None
let type_is_class tenv typ =
match Tenv.expand_ptr_type tenv typ with
let type_is_class typ =
match typ with
| Typ.Tptr (Typ.Tstruct _, _) -> true
| Typ.Tptr (Typ.Tvar _, _) -> true
| Typ.Tptr (Typ.Tarray _, _) -> true
| Typ.Tstruct _ -> true
| _ -> false
@ -357,14 +353,12 @@ let proc_iter_overridden_methods f tenv proc_name =
match proc_name with
| Procname.Java proc_name_java ->
let type_name =
let class_name = Procname.java_get_class_name proc_name_java in
Typename.TN_csu (Csu.Class Csu.Java, Mangled.from_string class_name) in
let type_name = Typename.Java.from_string (Procname.java_get_class_name proc_name_java) in
(match Tenv.lookup tenv type_name with
| Some curr_struct_typ ->
| Some {name} ->
IList.iter
(do_super_type tenv)
(type_get_direct_supertypes tenv (Typ.Tstruct curr_struct_typ))
(type_get_direct_supertypes tenv (Typ.Tstruct name))
| None ->
())
| _ ->

4
infer/src/checkers/patternMatch.mli
Unescape View File

@ -94,12 +94,12 @@ val type_get_direct_supertypes : Tenv.t -> Typ.t -> Typename.t list
val type_has_direct_supertype : Tenv.t -> Typ.t -> Typename.t -> bool
(** Is the type a class type *)
val type_is_class : Tenv.t -> Typ.t -> bool
val type_is_class : Typ.t -> bool
val type_is_nested_in_direct_supertype : Tenv.t -> Typ.t -> Typename.t -> bool
(** Is the type java.lang.Object *)
val type_is_object : Tenv.t -> Typ.t -> bool
val type_is_object : Typ.t -> bool
(** return the set of instance fields that are assigned to a null literal in [procdesc] *)
val get_fields_nullified : Cfg.Procdesc.t -> Ident.FieldSet.t

4
infer/src/clang/cArithmetic_trans.ml
Unescape View File

@ -98,7 +98,7 @@ let compound_assignment_binary_operation_instruction boi e1 typ e2 loc =
(* is returned when we are calculating an expression "instructions" is not *)
(* empty when the binary operator is actually a statement like an *)
(* assignment. *)
let binary_operation_instruction context boi e1 typ e2 loc rhs_owning_method =
let binary_operation_instruction boi e1 typ e2 loc rhs_owning_method =
let binop_exp op = Exp.BinOp(op, e1, e2) in
match boi.Clang_ast_t.boi_kind with
| `Add -> (binop_exp (Binop.PlusA), [])
@ -120,7 +120,7 @@ let binary_operation_instruction context boi e1 typ e2 loc rhs_owning_method =
| `LAnd -> (binop_exp (Binop.LAnd), [])
| `LOr -> (binop_exp (Binop.LOr), [])
| `Assign ->
if !Config.arc_mode && ObjcInterface_decl.is_pointer_to_objc_class context.CContext.tenv typ then
if !Config.arc_mode && ObjcInterface_decl.is_pointer_to_objc_class typ then
assignment_arc_mode e1 typ e2 loc rhs_owning_method false
else
(e1, [Sil.Store (e1, typ, e2, loc)])

2
infer/src/clang/cArithmetic_trans.mli
Unescape View File

@ -14,7 +14,7 @@ open! Utils
val bin_op_to_string : Clang_ast_t.binary_operator_info -> string
val binary_operation_instruction :
CContext.t -> Clang_ast_t.binary_operator_info -> Exp.t -> Typ.t -> Exp.t ->
Clang_ast_t.binary_operator_info -> Exp.t -> Typ.t -> Exp.t ->
Location.t -> bool -> Exp.t * Sil.instr list
val unary_operation_instruction :

10
infer/src/clang/cMethod_trans.ml
Unescape View File

@ -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 Tenv.expand_type tenv return_type with
let should_add_return_param return_type ~is_objc_method =
match return_type with
| Typ.Tstruct _ -> not is_objc_method
| _ -> false
@ -75,7 +75,7 @@ let get_return_param tenv function_method_decl_info =
let is_objc_method = is_objc_method function_method_decl_info in
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
if should_add_return_param tenv return_typ ~is_objc_method then
if should_add_return_param return_typ ~is_objc_method then
[(Mangled.from_string CFrontend_config.return_param,
Ast_expressions.create_pointer_qual_type ~is_const:false return_type_ptr)]
else
@ -112,7 +112,7 @@ let get_parameters tenv function_method_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 Tenv.expand_type tenv param_typ with
match 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
@ -126,7 +126,7 @@ 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
if should_add_return_param tenv return_typ ~is_objc_method then
if should_add_return_param return_typ ~is_objc_method then
Ast_expressions.create_void_type, Some (Typ.Tptr (return_typ, Typ.Pk_pointer))
else return_type_ptr, None

2
infer/src/clang/cMethod_trans.mli
Unescape View File

@ -21,7 +21,7 @@ type method_call_type =
| MCNoVirtual
| MCStatic
val should_add_return_param : Tenv.t -> Typ.t -> is_objc_method:bool -> bool
val should_add_return_param : Typ.t -> is_objc_method:bool -> bool
val create_local_procdesc : Cfg.cfg -> Tenv.t -> CMethod_signature.method_signature ->
Clang_ast_t.stmt list -> (Pvar.t * Typ.t) list -> bool -> bool

53
infer/src/clang/cTrans.ml
Unescape View File

@ -80,7 +80,7 @@ struct
let method_name = Procname.get_method (Cfg.Procdesc.get_proc_name context.CContext.procdesc) in
if !Config.arc_mode &&
not (CTrans_utils.is_owning_name method_name) &&
ObjcInterface_decl.is_pointer_to_objc_class context.CContext.tenv typ then
ObjcInterface_decl.is_pointer_to_objc_class typ then
let fname = ModelBuiltins.__set_autorelease_attribute in
let ret_id = Ident.create_fresh Ident.knormal in
let stmt_call =
@ -126,8 +126,7 @@ struct
Printing.log_out "-----> field: '%s'\n" (Ident.fieldname_to_string fn)) fields;
let mblock = Mangled.from_string block_name in
let block_name = Typename.TN_csu (Csu.Class Csu.Objc, mblock) in
let block_struct_typ = Tenv.mk_struct tenv ~fields block_name in
let block_type = Typ.Tstruct block_struct_typ in
let block_type = Typ.Tstruct (Tenv.mk_struct tenv ~fields block_name).name in
let trans_res =
CTrans_utils.alloc_trans
trans_state loc (Ast_expressions.dummy_stmt_info ()) block_type true None in
@ -203,9 +202,8 @@ struct
with Self.SelfClassException class_name ->
let typ =
CTypes_decl.objc_class_name_to_sil_type trans_state.context.CContext.tenv class_name in
let expanded_type = CTypes.expand_structured_type trans_state.context.CContext.tenv typ in
{ empty_res_trans with
exps = [(Exp.Sizeof(expanded_type, None, Subtype.exact), Typ.Tint Typ.IULong)] }
exps = [(Exp.Sizeof (typ, None, Subtype.exact), Tint IULong)] }
let add_reference_if_glvalue typ expr_info =
(* glvalue definition per C++11:*)
@ -270,12 +268,11 @@ struct
let create_call_instr trans_state return_type function_sil params_sil sil_loc
call_flags ~is_objc_method =
let {context = {tenv}} = trans_state in
let ret_id = if (Typ.equal return_type Typ.Tvoid) then []
else [Ident.create_fresh Ident.knormal] in
let ret_id', params, initd_exps, ret_exps =
(* Assumption: should_add_return_param will return true only for struct types *)
if CMethod_trans.should_add_return_param tenv return_type ~is_objc_method then
if CMethod_trans.should_add_return_param return_type ~is_objc_method then
let param_type = Typ.Tptr (return_type, Typ.Pk_pointer) in
let var_exp = match trans_state.var_exp_typ with
| Some (exp, _) -> exp
@ -496,7 +493,7 @@ struct
| _ -> false in
let class_typ =
match class_typ with
| Typ.Tptr (t, _) -> CTypes.expand_structured_type context.CContext.tenv t
| Typ.Tptr (t, _) -> t
| t -> t in
Printing.log_out "Type is '%s' @." (Typ.to_string class_typ);
let field_name = General_utils.mk_class_field_name name_info in
@ -548,7 +545,6 @@ struct
(* We need to add a dereference before a method call to find null dereferences when *)
(* calling a method with null *)
| [(exp, Typ.Tptr (typ, _) )] when decl_kind <> `CXXConstructor ->
let typ = CTypes.expand_structured_type context.tenv typ in
let no_id = Ident.create_none () in
let extra_instrs = [Sil.Load (no_id, exp, typ, sil_loc)] in
pre_trans_result.exps, extra_instrs
@ -618,11 +614,10 @@ 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 _, _, 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 Tenv.expand_type tenv ast_typ with
match ast_typ with
| Tstruct _ when decl_ref.dr_kind = `ParmVar ->
if General_utils.is_cpp_translation then
Typ.Tptr (ast_typ, Pk_reference)
@ -640,14 +635,13 @@ struct
let trans_result' =
let is_global_const, init_expr =
match Ast_utils.get_decl decl_ref.dr_decl_pointer with
| Some VarDecl (_, _, qual_type, vdi) ->
(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
values do not include structs, they must all be heap-allocated *)
false, None
| _ -> vdi.vdi_is_global && qual_type.qt_is_const, vdi.vdi_init_expr)
| Some VarDecl (_, _, qual_type, vdi) -> (
match ast_typ with
| Tstruct _ when not General_utils.is_cpp_translation ->
(* Do not convert a global struct to a local because SIL
values do not include structs, they must all be heap-allocated *)
false, None
| _ -> vdi.vdi_is_global && qual_type.qt_is_const, vdi.vdi_init_expr)
| _ -> false, None in
if is_global_const then
init_expr_trans trans_state (var_exp, typ) stmt_info init_expr
@ -657,8 +651,7 @@ struct
if (CTypes.is_class typ) then
raise (Self.SelfClassException (CContext.get_curr_class_name curr_class))
else
let typ = CTypes.add_pointer_to_typ
(CTypes_decl.get_type_curr_class_objc context.tenv curr_class) in
let typ = CTypes.add_pointer_to_typ (CTypes_decl.get_type_curr_class_objc curr_class) in
[(var_exp, typ)]
else [(var_exp, typ)] in
Printing.log_out "\n\n PVAR ='%s'\n\n" (Pvar.to_string pvar);
@ -807,7 +800,7 @@ struct
else
let exp_op, instr_bin =
CArithmetic_trans.binary_operation_instruction
context binary_operator_info var_exp typ sil_e2 sil_loc rhs_owning_method in
binary_operator_info var_exp typ sil_e2 sil_loc rhs_owning_method in
(* Create a node if the priority if free and there are instructions *)
let creating_node =
@ -894,7 +887,7 @@ struct
(Exp.Const (Const.Cint IntLit.one), Typ.Tint Typ.IBool) :: act_params
else act_params in
let res_trans_call =
let cast_trans_fun = cast_trans context act_params sil_loc function_type in
let cast_trans_fun = cast_trans act_params sil_loc function_type in
match Option.map_default cast_trans_fun None callee_pname_opt with
| Some (instr, cast_exp) ->
{ empty_res_trans with
@ -1699,7 +1692,7 @@ struct
if IList.exists (Exp.equal var_exp) res_trans_ie.initd_exps then ([], [])
else if !Config.arc_mode &&
(CTrans_utils.is_method_call ie ||
ObjcInterface_decl.is_pointer_to_objc_class context.CContext.tenv ie_typ)
ObjcInterface_decl.is_pointer_to_objc_class ie_typ)
then
(* In arc mode, if it's a method call or we are initializing
with a pointer to objc class *)
@ -2030,7 +2023,7 @@ struct
let procname = Cfg.Procdesc.get_proc_name context.CContext.procdesc in
let loc =
(match stmt_info.Clang_ast_t.si_source_range with (l1, _) ->
CLocation.clang_to_sil_location l1 (Some context.CContext.procdesc)) in
CLocation.clang_to_sil_location l1 (Some context.CContext.procdesc)) in
(* Given a captured var, return the instruction to assign it to a temp *)
let assign_captured_var (cvar, typ) =
let id = Ident.create_fresh Ident.knormal in
@ -2066,10 +2059,9 @@ struct
}
| _ -> assert false
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
and initListExpr_initializers_trans trans_state var_exp n stmts typ is_dyn_array stmt_info =
let (var_exp_inside, typ_inside) = match typ with
| Typ.Tarray (t, _) when Typ.is_array_of_cpp_class ~expand_type typ ->
| Typ.Tarray (t, _) when Typ.is_array_of_cpp_class 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
@ -2110,7 +2102,6 @@ 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
@ -2126,7 +2117,7 @@ struct
| _ -> None, empty_res_trans)
| None -> Some (Exp.Const (Const.Cint (IntLit.minus_one))), empty_res_trans
else None, empty_res_trans in
let res_trans_new = cpp_new_trans trans_state_pri sil_loc typ size_exp_opt in
let res_trans_new = cpp_new_trans sil_loc typ size_exp_opt in
let stmt_opt = Ast_utils.get_stmt_opt cxx_new_expr_info.Clang_ast_t.xnei_initializer_expr in
let trans_state_init = { trans_state_pri with succ_nodes = []; } in
let var_exp_typ = match res_trans_new.exps with
@ -2137,7 +2128,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 ~expand_type typ then
if is_dyn_array && Typ.is_pointer_to_cpp_class 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) ->

50
infer/src/clang/cTrans_utils.ml
Unescape View File

@ -288,7 +288,7 @@ struct
end
(** This function handles ObjC new/alloc and C++ new calls *)
let create_alloc_instrs context sil_loc function_type fname size_exp_opt procname_opt =
let create_alloc_instrs sil_loc function_type fname size_exp_opt procname_opt =
let function_type, function_type_np =
match function_type with
| Typ.Tptr (styp, Typ.Pk_pointer)
@ -297,7 +297,6 @@ let create_alloc_instrs context sil_loc function_type fname size_exp_opt procnam
| Typ.Tptr (styp, Typ.Pk_objc_autoreleasing) ->
function_type, styp
| _ -> Typ.Tptr (function_type, Typ.Pk_pointer), function_type in
let function_type_np = CTypes.expand_structured_type context.CContext.tenv function_type_np in
let sizeof_exp_ = Exp.Sizeof (function_type_np, None, Subtype.exact) in
let sizeof_exp = match size_exp_opt with
| Some exp -> Exp.BinOp (Binop.Mult, sizeof_exp_, exp)
@ -318,7 +317,7 @@ let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc pro
else
ModelBuiltins.__objc_alloc in
let (function_type, stmt_call, exp) =
create_alloc_instrs trans_state.context loc function_type fname None procname_opt in
create_alloc_instrs loc function_type fname None procname_opt in
let res_trans_tmp = { empty_res_trans with instrs =[stmt_call]} in
let res_trans =
let nname = "Call alloc" in
@ -328,7 +327,7 @@ let alloc_trans trans_state loc stmt_info function_type is_cf_non_null_alloc pro
let objc_new_trans trans_state loc stmt_info cls_name function_type =
let fname = ModelBuiltins.__objc_alloc_no_fail in
let (alloc_ret_type, alloc_stmt_call, alloc_ret_exp) =
create_alloc_instrs trans_state.context loc function_type fname None None in
create_alloc_instrs loc function_type fname None None in
let init_ret_id = Ident.create_fresh Ident.knormal in
let is_instance = true in
let call_flags = { CallFlags.default with CallFlags.cf_virtual = is_instance; } in
@ -359,31 +358,30 @@ let new_or_alloc_trans trans_state loc stmt_info type_ptr class_name_opt selecto
objc_new_trans trans_state loc stmt_info class_name function_type
else assert false
let cpp_new_trans trans_state sil_loc function_type size_exp_opt =
let cpp_new_trans sil_loc function_type size_exp_opt =
let fname =
match size_exp_opt with
| Some _ -> ModelBuiltins.__new_array
| None -> ModelBuiltins.__new in
let (function_type, stmt_call, exp) =
create_alloc_instrs trans_state.context sil_loc function_type fname size_exp_opt None in
create_alloc_instrs sil_loc function_type fname size_exp_opt None in
{ empty_res_trans with instrs = [stmt_call]; exps = [(exp, function_type)] }
let create_cast_instrs context exp cast_from_typ cast_to_typ sil_loc =
let create_cast_instrs exp cast_from_typ cast_to_typ sil_loc =
let ret_id = Ident.create_fresh Ident.knormal in
let typ = CTypes.remove_pointer_to_typ cast_to_typ in
let cast_typ_no_pointer = CTypes.expand_structured_type context.CContext.tenv typ in
let sizeof_exp = Exp.Sizeof (cast_typ_no_pointer, None, Subtype.exact) in
let sizeof_exp = Exp.Sizeof (typ, None, Subtype.exact) in
let pname = ModelBuiltins.__objc_cast in
let args = [(exp, cast_from_typ); (sizeof_exp, Typ.Tint Typ.IULong)] in
let stmt_call =
Sil.Call ([ret_id], Exp.Const (Const.Cfun pname), args, sil_loc, CallFlags.default) in
(stmt_call, Exp.Var ret_id)
let cast_trans context exps sil_loc function_type pname =
let cast_trans exps sil_loc function_type pname =
if CTrans_models.is_toll_free_bridging pname then
match exps with
| [exp, typ] ->
Some (create_cast_instrs context exp typ function_type sil_loc)
Some (create_cast_instrs exp typ function_type sil_loc)
| _ -> assert false
else None
@ -425,7 +423,7 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged =
match trans_state.obj_bridged_cast_typ with
| Some typ -> typ
| None -> cast_typ in
let instr, exp = create_cast_instrs trans_state.context exp typ objc_cast_typ sil_loc in
let instr, exp = create_cast_instrs exp typ objc_cast_typ sil_loc in
[instr], (exp, cast_typ)
| `LValueToRValue ->
(* Takes an LValue and allow it to use it as RValue. *)
@ -581,9 +579,9 @@ struct
let add_self_parameter_for_super_instance context procname loc mei =
if is_superinstance mei then
let typ, self_expr, ins =
let t' = CTypes.add_pointer_to_typ
(CTypes_decl.get_type_curr_class_objc
context.CContext.tenv context.CContext.curr_class) in
let t' =
CTypes.add_pointer_to_typ
(CTypes_decl.get_type_curr_class_objc context.CContext.curr_class) in
let e = Exp.Lvar (Pvar.mk (Mangled.from_string CFrontend_config.self) procname) in
let id = Ident.create_fresh Ident.knormal in
t', Exp.Var id, [Sil.Load (id, e, t', loc)] in
@ -713,17 +711,17 @@ let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero =
let rec var_or_zero_in_init_list' e typ tns =
let open General_utils in
match typ with
| Typ.Tvar tn ->
(match Tenv.lookup tenv tn with
| Some struct_typ -> var_or_zero_in_init_list' e (Typ.Tstruct struct_typ) tns
| _ -> [[(e, typ)]] (*This case is an error, shouldn't happen.*))
| Typ.Tstruct { fields } as type_struct ->
let lh_exprs = IList.map ( fun (fieldname, _, _) ->
Exp.Lfield (e, fieldname, type_struct) ) fields in
let lh_types = IList.map ( fun (_, fieldtype, _) -> fieldtype) fields in
let exp_types = zip lh_exprs lh_types in
IList.map (fun (e, t) ->
IList.flatten (var_or_zero_in_init_list' e t tns)) exp_types
| Typ.Tstruct tn -> (
match Tenv.lookup tenv tn with
| Some { fields } ->
let lh_exprs =
IList.map (fun (fieldname, _, _) -> Exp.Lfield (e, fieldname, typ)) fields in
let lh_types = IList.map (fun (_, fieldtype, _) -> fieldtype) fields in
let exp_types = zip lh_exprs lh_types in
IList.map (fun (e, t) -> IList.flatten (var_or_zero_in_init_list' e t tns)) exp_types
| None ->
assert false
)
| Typ.Tarray (arrtyp, Some n) ->
let size = IntLit.to_int n in
let indices = list_range 0 (size - 1) in

5
infer/src/clang/cTrans_utils.mli
Unescape View File

@ -111,11 +111,10 @@ val alloc_trans :
val new_or_alloc_trans : trans_state -> Location.t -> Clang_ast_t.stmt_info ->
Clang_ast_t.type_ptr -> string option -> string -> trans_result
val cpp_new_trans : trans_state -> Location.t -> Typ.t -> Exp.t option -> trans_result
val cpp_new_trans : Location.t -> Typ.t -> Exp.t option -> trans_result
val cast_trans :
CContext.t -> (Exp.t * Typ.t) list -> Location.t -> Typ.t -> Procname.t ->
(Sil.instr * Exp.t) option
(Exp.t * Typ.t) list -> Location.t -> Typ.t -> Procname.t -> (Sil.instr * Exp.t) option
val dereference_var_sil : Exp.t * Typ.t -> Location.t -> Sil.instr list * Exp.t

6
infer/src/clang/cType_to_sil_type.ml
Unescape View File

@ -17,7 +17,7 @@ let get_builtin_objc_typename builtin_type =
| `ObjCClass -> Typename.TN_csu (Csu.Struct, (Mangled.from_string CFrontend_config.objc_class))
let get_builtin_objc_type builtin_type =
let typ = Typ.Tvar (get_builtin_objc_typename builtin_type) in
let typ = Typ.Tstruct (get_builtin_objc_typename builtin_type) in
match builtin_type with
| `ObjCId -> typ
| `ObjCClass -> Typ.Tptr (typ, Typ.Pk_pointer)
@ -182,7 +182,7 @@ and type_ptr_to_sil_type translate_decl tenv type_ptr =
Typ.Tptr (sil_typ, Typ.Pk_reference)
| `ClassType (name, lang) ->
let kind = match lang with `OBJC -> Csu.Objc | `CPP -> Csu.CPP in
Typ.Tvar (CTypes.mk_classname name kind)
| `StructType name -> Typ.Tvar (CTypes.mk_structname name)
Typ.Tstruct (CTypes.mk_classname name kind)
| `StructType name -> Typ.Tstruct (CTypes.mk_structname name)
| `DeclPtr ptr -> decl_ptr_to_sil_type translate_decl tenv ptr
| `ErrorType -> Typ.Tvoid

21
infer/src/clang/cTypes.ml
Unescape View File

@ -24,8 +24,7 @@ let remove_pointer_to_typ typ =
let classname_of_type typ =
match typ with
| Typ.Tvar name
| Typ.Tstruct { name } -> Typename.name name
| Typ.Tstruct name -> Typename.name name
| Typ.Tfun _ -> CFrontend_config.objc_object
| _ ->
Printing.log_out
@ -38,8 +37,7 @@ let mk_structname n = Typename.TN_csu (Csu.Struct, Mangled.from_string n)
let is_class typ =
match typ with
| Typ.Tptr (Tvar ((TN_csu _) as name), _)
| Typ.Tptr (Tstruct { name }, _) ->
| Typ.Tptr (Tstruct ((TN_csu _) as name), _) ->
string_equal (Typename.name name) CFrontend_config.objc_class
| _ -> false
@ -75,21 +73,6 @@ let is_reference_type tp =
| Some Clang_ast_t.RValueReferenceType _ -> true
| _ -> false
(* Expand a named type Tvar if it has a definition in tenv. This is used for Tenum, Tstruct, etc. *)
let rec expand_structured_type tenv typ =
match typ with
| Typ.Tvar tn ->
(match Tenv.lookup tenv tn with
| Some ts ->
let t = Typ.Tstruct ts in
Printing.log_out " Type expanded with type '%s' found in tenv@." (Typ.to_string t);
if Typ.equal t typ then
typ
else expand_structured_type tenv t
| None -> typ)
| Typ.Tptr _ -> typ (*do not expand types under pointers *)
| _ -> typ
(* To be called with strings of format "<pointer_type_info>*<class_name>" *)
let get_name_from_type_pointer custom_type_pointer =
match Str.split (Str.regexp "*") custom_type_pointer with

2
infer/src/clang/cTypes.mli
Unescape View File

@ -29,6 +29,4 @@ val is_block_type : Clang_ast_t.type_ptr -> bool
val is_reference_type : Clang_ast_t.type_ptr -> bool
val expand_structured_type : Tenv.t -> Typ.t -> Typ.t
val get_name_from_type_pointer : string -> string * string

34
infer/src/clang/cTypes_decl.ml
Unescape View File

@ -34,7 +34,7 @@ let add_predefined_basic_types () =
Ast_utils.update_sil_types_map tp return_type in
let sil_void_type = CType_to_sil_type.sil_type_of_builtin_type_kind `Void in
let sil_char_type = CType_to_sil_type.sil_type_of_builtin_type_kind `Char_S in
let sil_nsarray_type = Typ.Tvar (CTypes.mk_classname CFrontend_config.nsarray_cl Csu.Objc) in
let sil_nsarray_type = Typ.Tstruct (CTypes.mk_classname CFrontend_config.nsarray_cl Csu.Objc) in
let sil_id_type = CType_to_sil_type.get_builtin_objc_type `ObjCId in
add_basic_type create_int_type `Int;
add_basic_type create_void_type `Void;
@ -117,12 +117,6 @@ let get_superclass_list_cpp decl =
Typename.TN_csu (Csu.Class Csu.CPP, decl_to_mangled_name super_decl) in
IList.map get_super_field base_decls
let add_struct_to_tenv tenv typ =
match typ with
| Typ.Tstruct ({name} as struct_typ) ->
Tenv.add tenv name struct_typ
| _ -> assert false
let get_translate_as_friend_decl decl_list =
let is_translate_as_friend_name (_, name_info) =
let translate_as_str = "infer_traits::TranslateAsType" in
@ -191,7 +185,7 @@ and get_record_declaration_struct_type tenv decl =
if csu = Csu.Class Csu.CPP then Typ.cpp_class_annotation
else Typ.item_annotation_empty (* No annotations for structs *) in
if is_complete_definition then (
Ast_utils.update_sil_types_map type_ptr (Typ.Tvar sil_typename);
Ast_utils.update_sil_types_map type_ptr (Typ.Tstruct sil_typename);
let non_statics = get_struct_fields tenv decl in
let fields = General_utils.append_no_duplicates_fields non_statics extra_fields in
let statics = [] in (* Note: We treat static field same as global variables *)
@ -199,21 +193,18 @@ and get_record_declaration_struct_type tenv decl =
let supers = get_superclass_list_cpp decl in
let sil_type =
Typ.Tstruct
(Tenv.mk_struct tenv ~fields ~statics ~methods ~supers ~annots sil_typename) in
(Tenv.mk_struct tenv ~fields ~statics ~methods ~supers ~annots sil_typename).name in
Ast_utils.update_sil_types_map type_ptr sil_type;
sil_type
) else (
match Tenv.lookup tenv sil_typename with
| Some struct_typ -> Typ.Tstruct struct_typ (* just reuse what is already in tenv *)
| Some {name} -> Typ.Tstruct name (* just reuse what is already in tenv *)
| None ->
(* This is first forward definition seen so far. Instead of adding *)
(* empty Tstruct to sil_types_map add Tvar so that frontend doeasn't expand *)
(* type too early. Since tenv doesn't allow to put Tvars, add empty Tstruct there *)
(* Later, when we see definition, it will be updated with a new value. *)
(* Note: we know that this type will be wrapped with pointer type because *)
(* there was no full definition of that type yet. *)
ignore (Typ.Tstruct (Tenv.mk_struct tenv ~fields:extra_fields sil_typename));
let tvar_type = Typ.Tvar sil_typename in
(* This is first forward declaration seen. Add Tstruct to sil_types_map and struct with
only ref counter field to tenv. Later, when we see the definition, the tenv will be
updated with a new struct including the other fields. *)
ignore (Tenv.mk_struct tenv ~fields:extra_fields sil_typename);
let tvar_type = Typ.Tstruct sil_typename in
Ast_utils.update_sil_types_map type_ptr tvar_type;
tvar_type)
| _ -> assert false
@ -244,7 +235,7 @@ let get_type_from_expr_info ei tenv =
let class_from_pointer_type tenv type_ptr =
match type_ptr_to_sil_type tenv type_ptr with
| Typ.Tptr( Typ.Tvar (Typename.TN_csu (_, name)), _) -> Mangled.to_string name
| Typ.Tptr( Typ.Tstruct (Typename.TN_csu (_, name)), _) -> Mangled.to_string name
| _ -> assert false
let get_class_type_np tenv expr_info obj_c_message_expr_info =
@ -254,7 +245,6 @@ let get_class_type_np tenv expr_info obj_c_message_expr_info =
| _ -> expr_info.Clang_ast_t.ei_type_ptr in
type_ptr_to_sil_type tenv tp
let get_type_curr_class_objc tenv curr_class_opt =
let get_type_curr_class_objc curr_class_opt =
let name = CContext.get_curr_class_name curr_class_opt in
let typ = Typ.Tvar (Typename.TN_csu (Csu.Class Csu.Objc, (Mangled.from_string name))) in
CTypes.expand_structured_type tenv typ
Typ.Tstruct (TN_csu (Class Objc, (Mangled.from_string name)))

4
infer/src/clang/cTypes_decl.mli
Unescape View File

@ -11,8 +11,6 @@ open! Utils
(** Processes types and record declarations by adding them to the tenv *)
val add_struct_to_tenv : Tenv.t -> Typ.t -> unit
val get_record_name : Clang_ast_t.decl -> string
val add_types_from_decl_to_tenv : Tenv.t -> Clang_ast_t.decl -> Typ.t
@ -28,7 +26,7 @@ val class_from_pointer_type : Tenv.t -> Clang_ast_t.type_ptr -> string
val get_class_type_np : Tenv.t -> Clang_ast_t.expr_info ->
Clang_ast_t.obj_c_message_expr_info -> Typ.t
val get_type_curr_class_objc : Tenv.t -> CContext.curr_class -> Typ.t
val get_type_curr_class_objc : CContext.curr_class -> Typ.t
val get_type_from_expr_info : Clang_ast_t.expr_info -> Tenv.t -> Typ.t

4
infer/src/clang/objcCategory_decl.ml
Unescape View File

@ -76,7 +76,7 @@ let process_category type_ptr_to_sil_type tenv curr_class decl_info decl_list =
let mang_name = Mangled.from_string class_name in
let class_tn_name = Typename.TN_csu (Csu.Class Csu.Objc, mang_name) in
let decl_key = `DeclPtr decl_info.Clang_ast_t.di_pointer in
Ast_utils.update_sil_types_map decl_key (Typ.Tvar class_tn_name);
Ast_utils.update_sil_types_map decl_key (Typ.Tstruct class_tn_name);
(match Tenv.lookup tenv class_tn_name with
| Some ({ fields; methods } as struct_typ) ->
let new_fields = General_utils.append_no_duplicates_fields decl_fields fields in
@ -86,7 +86,7 @@ let process_category type_ptr_to_sil_type tenv curr_class decl_info decl_list =
~default:struct_typ ~fields:new_fields ~statics:[] ~methods:new_methods class_tn_name );
Printing.log_out " Updating info for class '%s' in tenv\n" class_name
| _ -> ());
Typ.Tvar class_tn_name
Typ.Tstruct class_tn_name
let category_decl type_ptr_to_sil_type tenv decl =
let open Clang_ast_t in

20
infer/src/clang/objcInterface_decl.ml
Unescape View File

@ -20,14 +20,9 @@ open CFrontend_utils
module L = Logging
let is_pointer_to_objc_class tenv typ =
let expand_type = Tenv.expand_ptr_type tenv in
let is_pointer_to_objc_class typ =
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 ~expand_type (Typ.Tstruct struct_typ) -> true
| _ -> false)
| Typ.Tptr (typ, _) when Typ.is_objc_class ~expand_type typ -> true
| Typ.Tptr (typ, _) when Typ.is_objc_class typ -> true
| _ -> false
let get_super_interface_decl otdi_super =
@ -104,7 +99,7 @@ let add_class_to_tenv type_ptr_to_sil_type tenv curr_class decl_info name_info d
Printing.log_out "ADDING: ObjCInterfaceDecl for '%s'\n" class_name;
let interface_name = CTypes.mk_classname class_name Csu.Objc in
let decl_key = `DeclPtr decl_info.Clang_ast_t.di_pointer in
Ast_utils.update_sil_types_map decl_key (Typ.Tvar interface_name);
Ast_utils.update_sil_types_map decl_key (Typ.Tstruct interface_name);
let supers, fields =
create_supers_fields type_ptr_to_sil_type tenv curr_class decl_list
ocidi.Clang_ast_t.otdi_super
@ -135,15 +130,16 @@ let add_class_to_tenv type_ptr_to_sil_type tenv curr_class decl_info name_info d
Printing.log_out
" >>>Verifying that Typename '%s' is in tenv\n" (Typename.to_string interface_name);
(match Tenv.lookup tenv interface_name with
| Some st -> Printing.log_out " >>>OK. Found typ='%s'\n" (Typ.to_string (Typ.Tstruct st))
| Some st ->
Printing.log_out " >>>OK. Found typ='%a'\n" (Typ.pp_struct_typ pe_text (fun _ () -> ())) st
| None -> Printing.log_out " >>>NOT Found!!\n");
Typ.Tvar interface_name
Typ.Tstruct interface_name
let add_missing_methods tenv class_name ck decl_info decl_list curr_class =
let decl_methods = ObjcProperty_decl.get_methods curr_class decl_list in
let class_tn_name = Typename.TN_csu (Csu.Class ck, (Mangled.from_string class_name)) in
let decl_key = `DeclPtr decl_info.Clang_ast_t.di_pointer in
Ast_utils.update_sil_types_map decl_key (Typ.Tvar class_tn_name);
Ast_utils.update_sil_types_map decl_key (Typ.Tstruct class_tn_name);
begin
match Tenv.lookup tenv class_tn_name with
| Some ({ statics = []; name = TN_csu (Class _, _); methods; } as struct_typ) ->
@ -151,7 +147,7 @@ let add_missing_methods tenv class_name ck decl_info decl_list curr_class =
ignore( Tenv.mk_struct tenv ~default:struct_typ ~methods class_tn_name )
| _ -> ()
end;
Typ.Tvar class_tn_name
Typ.Tstruct class_tn_name
(* Interface_type_info has the name of instance variables and the name of methods. *)
let interface_declaration type_ptr_to_sil_type tenv decl =

2
infer/src/clang/objcInterface_decl.mli
Unescape View File

@ -19,7 +19,7 @@ val interface_declaration : Ast_utils.type_ptr_to_sil_type -> Tenv.t -> Clang_as
val interface_impl_declaration : Ast_utils.type_ptr_to_sil_type -> Tenv.t -> Clang_ast_t.decl ->
Typ.t
val is_pointer_to_objc_class : Tenv.t -> Typ.t -> bool
val is_pointer_to_objc_class : Typ.t -> bool
val get_curr_class : string -> Clang_ast_t.obj_c_interface_decl_info -> CContext.curr_class

4
infer/src/clang/objcProtocol_decl.ml
Unescape View File

@ -31,11 +31,11 @@ let protocol_decl type_ptr_to_sil_type tenv decl =
let mang_name = Mangled.from_string name in
let protocol_name = Typename.TN_csu (Csu.Protocol, mang_name) in
let decl_key = `DeclPtr decl_info.Clang_ast_t.di_pointer in
Ast_utils.update_sil_types_map decl_key (Typ.Tvar protocol_name);
Ast_utils.update_sil_types_map decl_key (Typ.Tstruct protocol_name);
let methods = ObjcProperty_decl.get_methods curr_class decl_list in
ignore( Tenv.mk_struct tenv ~methods protocol_name );
add_protocol_super type_ptr_to_sil_type tenv obj_c_protocol_decl_info;
Typ.Tvar protocol_name
Typ.Tstruct protocol_name
| _ -> assert false
let is_protocol decl =

4
infer/src/clang/printing.ml
Unescape View File

@ -59,8 +59,8 @@ let print_tenv_struct_unions tenv =
(Typename.to_string typname)^"\n"^
"\t---> fields "^(IList.to_string (fun (fieldname, typ, _) ->
match typ with
| Typ.Tvar tname -> "tvar"^(Typename.to_string tname)
| Typ.Tstruct _ | _ ->
| Typ.Tstruct tname -> "tvar"^(Typename.to_string tname)
| _ ->
"\t struct "^(Ident.fieldname_to_string fieldname)^" "^
(Typ.to_string typ)^"\n") struct_t.fields
)

2
infer/src/eradicate/eradicate.ml
Unescape View File

@ -119,7 +119,7 @@ struct
let module DFTypeCheck = MakeDF(struct
type t = Extension.extension TypeState.t
let equal = TypeState.equal
let join = TypeState.join tenv Extension.ext
let join = TypeState.join Extension.ext
let do_node tenv node typestate =
State.set_node node;
let typestates_succ, typestates_exn =

167
infer/src/eradicate/eradicateChecks.ml
Unescape View File

@ -40,8 +40,8 @@ let check_library_calls = false
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
let lookup = Tenv.lookup tenv in
match Typ.get_field_type_and_annotation ~lookup fn typ with
| None -> None
| Some (t, ia) ->
let ia' =
@ -136,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.Tvar name | Typ.Tstruct { name = TN_csu (Class _, _) as name } ->
| Typ.Tstruct (TN_csu (Class Java, _) as name) ->
string_equal (Typename.name name) "java.lang.Throwable"
| _ -> false in
let do_instr = function
@ -166,7 +166,7 @@ let check_condition tenv case_zero find_canonical_duplicate curr_pname
(activate_condition_redundant || nonnull) &&
true_branch &&
(not is_temp || nonnull) &&
PatternMatch.type_is_class tenv typ &&
PatternMatch.type_is_class typ &&
not (from_try_with_resources ()) &&
from_call = From_condition &&
not (TypeAnnotation.origin_is_fun_library ta) in
@ -204,7 +204,7 @@ let check_field_assignment tenv
false in
TypeAnnotation.get_value Annotations.Nullable ta_lhs = false &&
TypeAnnotation.get_value Annotations.Nullable ta_rhs = true &&
PatternMatch.type_is_class tenv t_lhs &&
PatternMatch.type_is_class t_lhs &&
not (Ident.java_fieldname_is_outer_instance fname) &&
not (field_is_field_injector_readwrite ()) in
let should_report_absent =
@ -256,82 +256,83 @@ let check_constructor_initialization tenv
State.set_node start_node;
if Procname.is_constructor curr_pname
then begin
match
Option.map (Tenv.expand_ptr_type tenv)
(PatternMatch.get_this_type (Cfg.Procdesc.get_attributes curr_pdesc))
with
| Some (Tptr (Tstruct { fields; name } as ts, _)) ->
let do_field (fn, ft, _) =
let annotated_with f = match get_field_annotation tenv fn ts with
| None -> false
| Some (_, ia) -> f ia in
let nullable_annotated = annotated_with Annotations.ia_is_nullable in
let nonnull_annotated = annotated_with Annotations.ia_is_nonnull in
let injector_readonly_annotated =
annotated_with Annotations.ia_is_field_injector_readonly in
let final_type_annotation_with unknown list f =
let filter_range_opt = function
| Some (_, ta, _) -> f ta
| None -> unknown in
IList.exists
(function pname, typestate ->
let pvar = Pvar.mk
(Mangled.from_string (Ident.fieldname_to_string fn))
pname in
filter_range_opt (TypeState.lookup_pvar pvar typestate))
list in
let may_be_assigned_in_final_typestate =
final_type_annotation_with
false
(Lazy.force final_initializer_typestates)
(fun ta -> TypeAnnotation.get_origin ta <> TypeOrigin.Undef) in
let may_be_nullable_in_final_typestate () =
final_type_annotation_with
true
(Lazy.force final_constructor_typestates)
(fun ta -> TypeAnnotation.get_value Annotations.Nullable ta = true) in
let should_check_field_initialization =
let in_current_class =
let fld_cname = Ident.java_fieldname_get_class fn in
string_equal (Typename.name name) fld_cname in
not injector_readonly_annotated &&
PatternMatch.type_is_class tenv ft &&
in_current_class &&
not (Ident.java_fieldname_is_outer_instance fn) in
if should_check_field_initialization then
begin
if Models.Inference.enabled then Models.Inference.field_add_nullable_annotation fn;
(* Check if field is missing annotation. *)
if not (nullable_annotated || nonnull_annotated) &&
not may_be_assigned_in_final_typestate then
report_error tenv
find_canonical_duplicate
start_node
(TypeErr.Field_not_initialized (fn, curr_pname))
None
loc
curr_pname;
(* Check if field is over-annotated. *)
if activate_field_over_annotated &&
nullable_annotated &&
not (may_be_nullable_in_final_typestate ()) then
report_error tenv
find_canonical_duplicate
start_node
(TypeErr.Field_over_annotated (fn, curr_pname))
None
loc
curr_pname;
end in
IList.iter do_field fields
match PatternMatch.get_this_type (Cfg.Procdesc.get_attributes curr_pdesc) with
| Some (Tptr (Tstruct name as ts, _)) -> (
match Tenv.lookup tenv name with
| Some { fields } ->
let do_field (fn, ft, _) =
let annotated_with f = match get_field_annotation tenv fn ts with
| None -> false
| Some (_, ia) -> f ia in
let nullable_annotated = annotated_with Annotations.ia_is_nullable in
let nonnull_annotated = annotated_with Annotations.ia_is_nonnull in
let injector_readonly_annotated =
annotated_with Annotations.ia_is_field_injector_readonly in
let final_type_annotation_with unknown list f =
let filter_range_opt = function
| Some (_, ta, _) -> f ta
| None -> unknown in
IList.exists
(function pname, typestate ->
let pvar = Pvar.mk
(Mangled.from_string (Ident.fieldname_to_string fn))
pname in
filter_range_opt (TypeState.lookup_pvar pvar typestate))
list in
let may_be_assigned_in_final_typestate =
final_type_annotation_with
false
(Lazy.force final_initializer_typestates)
(fun ta -> TypeAnnotation.get_origin ta <> TypeOrigin.Undef) in
let may_be_nullable_in_final_typestate () =
final_type_annotation_with
true
(Lazy.force final_constructor_typestates)
(fun ta -> TypeAnnotation.get_value Annotations.Nullable ta = true) in
let should_check_field_initialization =
let in_current_class =
let fld_cname = Ident.java_fieldname_get_class fn in
string_equal (Typename.name name) fld_cname in
not injector_readonly_annotated &&
PatternMatch.type_is_class ft &&
in_current_class &&
not (Ident.java_fieldname_is_outer_instance fn) in
if should_check_field_initialization then (
if Models.Inference.enabled then Models.Inference.field_add_nullable_annotation fn;
(* Check if field is missing annotation. *)
if not (nullable_annotated || nonnull_annotated) &&
not may_be_assigned_in_final_typestate then
report_error tenv
find_canonical_duplicate
start_node
(TypeErr.Field_not_initialized (fn, curr_pname))
None
loc
curr_pname;
(* Check if field is over-annotated. *)
if activate_field_over_annotated &&
nullable_annotated &&
not (may_be_nullable_in_final_typestate ()) then
report_error tenv
find_canonical_duplicate
start_node
(TypeErr.Field_over_annotated (fn, curr_pname))
None
loc
curr_pname;
) in
IList.iter do_field fields
| None ->
()
)
| _ -> ()
end
@ -466,13 +467,13 @@ let check_call_parameters tenv
(t2, TypeAnnotation.const Annotations.Nullable false TypeOrigin.ONone, []) loc in
let parameter_not_nullable =
not param_is_this &&
PatternMatch.type_is_class tenv t1 &&
PatternMatch.type_is_class t1 &&
not formal_is_nullable &&
TypeAnnotation.get_value Annotations.Nullable ta2 in
let parameter_absent =
activate_optional_present &&
not param_is_this &&
PatternMatch.type_is_class tenv t1 &&
PatternMatch.type_is_class t1 &&
formal_is_present &&
not (TypeAnnotation.get_value Annotations.Present ta2) in
if parameter_not_nullable || parameter_absent then

12
infer/src/eradicate/typeCheck.ml
Unescape View File

@ -172,7 +172,7 @@ let rec typecheck_expr
| None -> tr_default)
| Exp.Const (Const.Cint i) when IntLit.iszero i ->
let (typ, _, locs) = tr_default in
if PatternMatch.type_is_class tenv typ
if PatternMatch.type_is_class typ
then (typ, TypeAnnotation.const Annotations.Nullable true (TypeOrigin.Const loc), locs)
else
let t, ta, ll = tr_default in
@ -583,15 +583,7 @@ let typecheck_instr
else Printf.sprintf "arg%d" i in
(Mangled.from_string arg, typ))
etl_ in
let ret_type =
match Tenv.proc_extract_return_typ tenv callee_pname_java with
| Some (Typ.Tstruct _ as typ) ->
Typ.Tptr (typ, Pk_pointer)
| Some typ ->
typ
| None ->
let ret_typ_string = Procname.java_get_return_type callee_pname_java in
Typ.Tptr (Tvar (Typename.Java.from_string ret_typ_string), Pk_pointer) in
let ret_type = Typ.java_proc_return_typ callee_pname_java in
let proc_attributes =
{ (ProcAttributes.default callee_pname Config.Java) with
ProcAttributes.formals;

12
infer/src/eradicate/typeState.ml
Unescape View File

@ -75,8 +75,8 @@ let pp ext fmt typestate =
pp_map typestate.map;
ext.pp fmt typestate.extension
let type_join tenv typ1 typ2 =
if PatternMatch.type_is_object tenv typ1 then typ2 else typ1
let type_join typ1 typ2 =
if PatternMatch.type_is_object typ1 then typ2 else typ1
let locs_join locs1 locs2 =
IList.merge_sorted_nodup Location.compare [] locs1 locs2
@ -86,13 +86,13 @@ let range_add_locs (typ, ta, locs1) locs2 =
(typ, ta, locs')
(** Join m2 to m1 if there are no inconsistencies, otherwise return m1. *)
let map_join tenv m1 m2 =
let map_join m1 m2 =
let tjoined = ref m1 in
let range_join (typ1, ta1, locs1) (typ2, ta2, locs2) =
match TypeAnnotation.join ta1 ta2 with
| None -> None
| Some ta' ->
let typ' = type_join tenv typ1 typ2 in
let typ' = type_join typ1 typ2 in
let locs' = locs_join locs1 locs2 in
Some (typ', ta', locs') in
let extend_lhs exp2 range2 = (* extend lhs if possible, otherwise return false *)
@ -119,13 +119,13 @@ let map_join tenv m1 m2 =
!tjoined
)
let join tenv ext t1 t2 =
let join ext t1 t2 =
if Config.from_env_variable "ERADICATE_TRACE"
then L.stderr "@.@.**********join@.-------@.%a@.------@.%a@.********@.@."
(pp ext) t1
(pp ext) t2;
{
map = map_join tenv t1.map t2.map;
map = map_join t1.map t2.map;
extension = ext.join t1.extension t2.extension;
}

2
infer/src/eradicate/typeState.mli
Unescape View File

@ -38,7 +38,7 @@ val add : Pvar.t -> range -> 'a t -> 'a t
val empty : 'a ext -> 'a t
val equal : 'a t -> 'a t -> bool
val get_extension : 'a t -> 'a
val join : Tenv.t -> 'a ext -> 'a t -> 'a t -> 'a t
val join : 'a ext -> 'a t -> 'a t -> 'a t
val lookup_id : Ident.t -> 'a t -> range option
val lookup_pvar : Pvar.t -> 'a t -> range option
val pp : 'a ext -> Format.formatter -> 'a t -> unit

2
infer/src/harness/harness.ml
Unescape View File

@ -21,7 +21,7 @@ let try_create_lifecycle_trace struct_typ lifecycle_struct_typ lifecycle_procs t
| { Typ.name = TN_csu (Class Java, _) as name } ->
if PatternMatch.is_subtype tenv struct_typ lifecycle_struct_typ &&
not (AndroidFramework.is_android_lib_class name) then
let ptr_to_struct_typ = Some (Typ.Tptr (Tstruct struct_typ, Pk_pointer)) in
let ptr_to_struct_typ = Some (Typ.Tptr (Tstruct name, Pk_pointer)) in
IList.fold_left
(fun trace lifecycle_proc ->
(* given a lifecycle subclass T, resolve the call T.lifecycle_proc() to the procname

27
infer/src/harness/inhabit.ml
Unescape View File

@ -94,16 +94,23 @@ 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 Tenv.expand_type tenv typ with
| Typ.Tstruct { name = TN_csu (Class _, _); methods } ->
let is_suitable_constructor p =
let try_get_non_receiver_formals p =
get_non_receiver_formals (formals_from_name cfg p) in
Procname.is_constructor p && IList.for_all (fun (_, typ) ->
not (TypSet.mem typ env.cur_inhabiting)) (try_get_non_receiver_formals p) in
IList.filter (fun p -> is_suitable_constructor p) methods
| _ -> [] in
let get_all_suitable_constructors (typ: Typ.t) =
match typ with
| Tstruct name -> (
match Tenv.lookup tenv name with
| Some { name = TN_csu (Class _, _); methods } ->
let is_suitable_constructor p =
let try_get_non_receiver_formals p =
get_non_receiver_formals (formals_from_name cfg p) in
Procname.is_constructor p
&& IList.for_all (fun (_, typ) ->
not (TypSet.mem typ env.cur_inhabiting)
) (try_get_non_receiver_formals p) in
IList.filter (fun p -> is_suitable_constructor p) methods
| _ -> []
)
| _ -> []
in
let (env, typ_class_name) = match get_all_suitable_constructors typ with
| constructor :: _ ->
(* arbitrarily choose a constructor for typ and invoke it. eventually, we may want to

25
infer/src/java/jTrans.ml
Unescape View File

@ -107,19 +107,18 @@ let retrieve_fieldname fieldname =
let get_field_name program static tenv cn fs =
match Tenv.expand_type tenv (JTransType.get_class_type_no_pointer program tenv cn) with
| Tstruct { fields; statics; name = TN_csu (Class _, _) } ->
let fieldname, _, _ =
try
IList.find
(fun (fieldname, _, _) -> retrieve_fieldname fieldname = JBasics.fs_name fs)
(if static then statics else fields)
with Not_found ->
(* TODO: understand why fields cannot be found here *)
JUtils.log "cannot find %s.%s@." (JBasics.cn_name cn) (JBasics.fs_name fs);
raise (Frontend_error "Cannot find fieldname") in
let { Typ.fields; statics; } = JTransType.get_class_struct_typ program tenv cn in
match
IList.find
(fun (fieldname, _, _) -> retrieve_fieldname fieldname = JBasics.fs_name fs)
(if static then statics else fields)
with
| fieldname, _, _ ->
fieldname
| _ -> assert false
| exception Not_found ->
(* TODO: understand why fields cannot be found here *)
JUtils.log "cannot find %s.%s@." (JBasics.cn_name cn) (JBasics.fs_name fs);
raise (Frontend_error "Cannot find fieldname")
let formals_from_signature program tenv cn ms kind =
@ -962,7 +961,7 @@ let rec instruction context pc instr : translation =
match instruction_thread_start context original_cn ms obj args var_opt with
| Some start_call -> instruction context pc start_call
| None ->
let cn' = match JTransType.extract_cn_no_obj tenv sil_obj_type with
let cn' = match JTransType.extract_cn_no_obj sil_obj_type with
| Some cn -> cn
| None -> original_cn in
let call_node = create_call_node cn' invoke_kind in

97
infer/src/java/jTransType.ml
Unescape View File

@ -70,7 +70,7 @@ let rec get_named_type vt =
| JBasics.TArray vt ->
let content_type = get_named_type vt in
Typ.Tptr (Typ.Tarray (content_type, None), Typ.Pk_pointer)
| JBasics.TClass cn -> Typ.Tptr (Typ.Tvar (typename_of_classname cn), Typ.Pk_pointer)
| JBasics.TClass cn -> Typ.Tptr (Typ.Tstruct (typename_of_classname cn), Typ.Pk_pointer)
end
@ -86,9 +86,9 @@ 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 Tenv.expand_ptr_type tenv typ with
| Typ.Tptr (Tstruct { name = TN_csu (Class _, _) as name }, Pk_pointer) ->
let extract_cn_no_obj typ =
match typ with
| Typ.Tptr (Tstruct (TN_csu (Class _, _) as name), Pk_pointer) ->
let class_name = Typename.name name in
if class_name = JConfig.object_cl then None
else
@ -274,14 +274,8 @@ let add_model_fields program classpath_fields cn =
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 { fields; statics } -> (statics, fields)
| Typ.Tvar name -> (
match Tenv.lookup tenv name with
| Some { fields; statics } -> (statics, fields)
| None -> assert false
)
| _ -> assert false in
let { Typ.fields; statics } = get_class_struct_typ program tenv classname in
(statics, fields) in
let trans_fields classname =
match JClasspath.lookup_node classname program with
| Some (Javalib.JClass jclass) ->
@ -298,50 +292,47 @@ let rec get_all_fields program tenv cn =
trans_fields cn
and create_sil_type program tenv cn =
match JClasspath.lookup_node cn program with
and get_class_struct_typ program tenv cn =
let name = typename_of_classname cn in
match Tenv.lookup tenv name with
| Some struct_typ ->
struct_typ
| None ->
Typ.Tstruct (Tenv.mk_struct tenv (typename_of_classname cn))
| Some node ->
let create_super_list interface_names =
IList.iter (fun cn -> ignore (get_class_type_no_pointer program tenv cn)) interface_names;
IList.map typename_of_classname interface_names in
let supers, fields, statics, annots =
match node with
| Javalib.JInterface jinterface ->
let statics, _ = get_all_fields program tenv cn in
let sil_interface_list = create_super_list jinterface.Javalib.i_interfaces in
let item_annotation = JAnnotation.translate_item jinterface.Javalib.i_annotations in
(sil_interface_list, [], statics, item_annotation)
| Javalib.JClass jclass ->
let statics, nonstatics =
let classpath_static, classpath_nonstatic = get_all_fields program tenv cn in
add_model_fields program (classpath_static, classpath_nonstatic) cn in
let item_annotation = JAnnotation.translate_item jclass.Javalib.c_annotations in
let interface_list = create_super_list jclass.Javalib.c_interfaces in
let super_classname_list =
match jclass.Javalib.c_super_class with
| None -> interface_list (* base case of the recursion *)
| 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
(super_classname_list, nonstatics, statics, item_annotation) in
let methods = IList.map (fun j -> Procname.Java j) (get_class_procnames cn node) in
Typ.Tstruct
(Tenv.mk_struct tenv ~fields ~statics ~methods ~supers ~annots (typename_of_classname cn))
and get_class_type_no_pointer program tenv cn =
match Tenv.lookup tenv (typename_of_classname cn) with
| None -> create_sil_type program tenv cn
| Some struct_typ -> Typ.Tstruct struct_typ
match JClasspath.lookup_node cn program with
| None ->
Tenv.mk_struct tenv name
| Some node ->
let create_super_list interface_names =
IList.iter (fun cn -> ignore (get_class_struct_typ program tenv cn)) interface_names;
IList.map typename_of_classname interface_names in
let supers, fields, statics, annots =
match node with
| Javalib.JInterface jinterface ->
let statics, _ = get_all_fields program tenv cn in
let sil_interface_list = create_super_list jinterface.Javalib.i_interfaces in
let item_annotation = JAnnotation.translate_item jinterface.Javalib.i_annotations in
(sil_interface_list, [], statics, item_annotation)
| Javalib.JClass jclass ->
let statics, nonstatics =
let classpath_static, classpath_nonstatic = get_all_fields program tenv cn in
add_model_fields program (classpath_static, classpath_nonstatic) cn in
let item_annotation = JAnnotation.translate_item jclass.Javalib.c_annotations in
let interface_list = create_super_list jclass.Javalib.c_interfaces in
let super_classname_list =
match jclass.Javalib.c_super_class with
| None -> interface_list (* base case of the recursion *)
| Some super_cn ->
let super_classname = (get_class_struct_typ program tenv super_cn).Typ.name in
super_classname :: interface_list in
(super_classname_list, nonstatics, statics, item_annotation) in
let methods = IList.map (fun j -> Procname.Java j) (get_class_procnames cn node) in
Tenv.mk_struct tenv ~fields ~statics ~methods ~supers ~annots name
let get_class_type_no_pointer program tenv cn =
Typ.Tstruct ((get_class_struct_typ program tenv cn).name)
let get_class_type program tenv cn =
let t = get_class_type_no_pointer program tenv cn in
Typ.Tptr (t, Typ.Pk_pointer)
Typ.Tptr (get_class_type_no_pointer program tenv cn, Pk_pointer)
(** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *)
let is_autogenerated_assert_field field_name =

5
infer/src/java/jTransType.mli
Unescape View File

@ -28,6 +28,9 @@ val get_method_kind : JCode.jcode Javalib.jmethod -> Procname.method_kind
val get_method_procname :
JBasics.class_name -> JBasics.method_signature -> Procname.method_kind -> Procname.java
(** [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 -> Typ.struct_typ
(** [get_class_type_no_pointer program tenv cn] returns the sil type representation of the class
without the pointer part *)
val get_class_type_no_pointer: JClasspath.program -> Tenv.t -> JBasics.class_name -> Typ.t
@ -75,7 +78,7 @@ val create_array_type : Typ.t -> int -> Typ.t
val extract_cn_type_np : Typ.t -> Typ.t
(** [extract_cn_type_np] returns the Java class name of typ when typ is a pointer type, otherwise returns None *)
val extract_cn_no_obj : Tenv.t -> Typ.t -> JBasics.class_name option
val extract_cn_no_obj : Typ.t -> JBasics.class_name option
(** returns a string representation of a Java basic type. *)
val string_of_basic_type : JBasics.java_basic_type -> string

8
infer/src/quandary/TaintAnalysis.ml
Unescape View File

@ -226,13 +226,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
let ret_typ =
match callee_pname with
| Procname.Java java_pname ->
let ret_typ_str = Procname.java_get_return_type java_pname in
begin
match Tenv.lookup_java_typ_from_string (proc_data.ProcData.tenv) ret_typ_str with
| Some (Typ.Tstruct _ as typ) -> Typ.Tptr (typ, Typ.Pk_pointer)
| Some typ -> typ
| None -> Typ.Tvoid
end
Typ.java_proc_return_typ java_pname
| Procname.C _ ->
Typ.Tvoid (* for tests only, since tests use C-style procnames *)
| _ ->

Write Preview
Loading…
Cancel
Save