Move Fieldname module inside Typ

Reviewed By: mbouaziz

Differential Revision: D5291900

fbshipit-source-id: 2bf232a
master
Andrzej Kotulski 8 years ago committed by Facebook Github Bot
parent a8ad84b9d3
commit 61aa7aaae5

@ -21,7 +21,7 @@ type t =
| Cstr string /** string constants */ | Cstr string /** string constants */
| Cfloat float /** float constants */ | Cfloat float /** float constants */
| Cclass Ident.name /** class constant */ | Cclass Ident.name /** class constant */
| Cptr_to_fld Fieldname.t Typ.t /** pointer to field constant, and type of the surrounding Csu.t type */ | Cptr_to_fld Typ.Fieldname.t Typ.t /** pointer to field constant, and type of the surrounding Csu.t type */
[@@deriving compare]; [@@deriving compare];
let equal = [%compare.equal : t]; let equal = [%compare.equal : t];
@ -49,7 +49,7 @@ let pp pe f =>
| Cstr s => F.fprintf f "\"%s\"" (String.escaped s) | Cstr s => F.fprintf f "\"%s\"" (String.escaped s)
| Cfloat v => F.fprintf f "%f" v | Cfloat v => F.fprintf f "%f" v
| Cclass c => F.fprintf f "%a" Ident.pp_name c | Cclass c => F.fprintf f "%a" Ident.pp_name c
| Cptr_to_fld fn _ => F.fprintf f "__fld_%a" Fieldname.pp fn; | Cptr_to_fld fn _ => F.fprintf f "__fld_%a" Typ.Fieldname.pp fn;
let to_string c => F.asprintf "%a" (pp Pp.text) c; let to_string c => F.asprintf "%a" (pp Pp.text) c;

@ -23,7 +23,7 @@ type t =
| Cstr string /** string constants */ | Cstr string /** string constants */
| Cfloat float /** float constants */ | Cfloat float /** float constants */
| Cclass Ident.name /** class constant */ | Cclass Ident.name /** class constant */
| Cptr_to_fld Fieldname.t Typ.t /** pointer to field constant, and type of the surrounding Csu.t type */ | Cptr_to_fld Typ.Fieldname.t Typ.t /** pointer to field constant, and type of the surrounding Csu.t type */
[@@deriving compare]; [@@deriving compare];
let equal: t => t => bool; let equal: t => t => bool;

@ -24,8 +24,8 @@ type t =
| Dsizeof Typ.t (option t) Subtype.t | Dsizeof Typ.t (option t) Subtype.t
| Dderef t | Dderef t
| Dfcall t (list t) Location.t CallFlags.t | Dfcall t (list t) Location.t CallFlags.t
| Darrow t Fieldname.t | Darrow t Typ.Fieldname.t
| Ddot t Fieldname.t | Ddot t Typ.Fieldname.t
| Dpvar Pvar.t | Dpvar Pvar.t
| Dpvaraddr Pvar.t | Dpvaraddr Pvar.t
| Dunop Unop.t t | Dunop Unop.t t
@ -90,25 +90,25 @@ let rec to_string =
} }
| Darrow (Dpvar pv) f when Pvar.is_this pv => | Darrow (Dpvar pv) f when Pvar.is_this pv =>
/* this->fieldname */ /* this->fieldname */
Fieldname.to_simplified_string f Typ.Fieldname.to_simplified_string f
| Darrow de f => | Darrow de f =>
if (Fieldname.is_hidden f) { if (Typ.Fieldname.is_hidden f) {
to_string de to_string de
} else if (java ()) { } else if (java ()) {
to_string de ^ "." ^ Fieldname.to_flat_string f to_string de ^ "." ^ Typ.Fieldname.to_flat_string f
} else { } else {
to_string de ^ "->" ^ Fieldname.to_string f to_string de ^ "->" ^ Typ.Fieldname.to_string f
} }
| Ddot (Dpvar _) fe when eradicate_java () => | Ddot (Dpvar _) fe when eradicate_java () =>
/* static field access */ /* static field access */
Fieldname.to_simplified_string fe Typ.Fieldname.to_simplified_string fe
| Ddot de f => | Ddot de f =>
if (Fieldname.is_hidden f) { if (Typ.Fieldname.is_hidden f) {
"&" ^ to_string de "&" ^ to_string de
} else if (java ()) { } else if (java ()) {
to_string de ^ "." ^ Fieldname.to_flat_string f to_string de ^ "." ^ Typ.Fieldname.to_flat_string f
} else { } else {
to_string de ^ "." ^ Fieldname.to_string f to_string de ^ "." ^ Typ.Fieldname.to_string f
} }
| Dpvar pv => Mangled.to_string (Pvar.get_name pv) | Dpvar pv => Mangled.to_string (Pvar.get_name pv)
| Dpvaraddr pv => { | Dpvaraddr pv => {

@ -24,8 +24,8 @@ type t =
| Dsizeof Typ.t (option t) Subtype.t | Dsizeof Typ.t (option t) Subtype.t
| Dderef t | Dderef t
| Dfcall t (list t) Location.t CallFlags.t | Dfcall t (list t) Location.t CallFlags.t
| Darrow t Fieldname.t | Darrow t Typ.Fieldname.t
| Ddot t Fieldname.t | Ddot t Typ.Fieldname.t
| Dpvar Pvar.t | Dpvar Pvar.t
| Dpvaraddr Pvar.t | Dpvaraddr Pvar.t
| Dunop Unop.t t | Dunop Unop.t t

@ -77,7 +77,7 @@ exception Java_runtime_exception of Typ.Name.t * string * Localise.error_desc
exception Leak of exception Leak of
bool * Sil.hpred * (visibility * Localise.error_desc) bool * Sil.hpred * (visibility * Localise.error_desc)
* bool * PredSymb.resource * L.ml_loc * bool * PredSymb.resource * L.ml_loc
exception Missing_fld of Fieldname.t * L.ml_loc exception Missing_fld of Typ.Fieldname.t * L.ml_loc
exception Premature_nil_termination of Localise.error_desc * L.ml_loc exception Premature_nil_termination of Localise.error_desc * L.ml_loc
exception Null_dereference of Localise.error_desc * L.ml_loc exception Null_dereference of Localise.error_desc * L.ml_loc
exception Null_test_after_dereference of Localise.error_desc * L.ml_loc exception Null_test_after_dereference of Localise.error_desc * L.ml_loc
@ -235,7 +235,7 @@ let recognize_exception exn =
(Localise.from_string "Match failure", (Localise.from_string "Match failure",
Localise.no_desc, Some ml_loc, Exn_developer, High, None, Nocat) Localise.no_desc, Some ml_loc, Exn_developer, High, None, Nocat)
| Missing_fld (fld, ml_loc) -> | Missing_fld (fld, ml_loc) ->
let desc = Localise.verbatim_desc (Fieldname.to_string fld) in let desc = Localise.verbatim_desc (Typ.Fieldname.to_string fld) in
(Localise.from_string "Missing_fld" ~hum:"Missing Field", (Localise.from_string "Missing_fld" ~hum:"Missing Field",
desc, Some ml_loc, Exn_developer, Medium, None, Nocat) desc, Some ml_loc, Exn_developer, Medium, None, Nocat)
| Premature_nil_termination (desc, ml_loc) -> | Premature_nil_termination (desc, ml_loc) ->

@ -72,7 +72,7 @@ exception Java_runtime_exception of Typ.Name.t * string * Localise.error_desc
exception Leak of exception Leak of
bool * Sil.hpred * (visibility * Localise.error_desc) bool * Sil.hpred * (visibility * Localise.error_desc)
* bool * PredSymb.resource * Logging.ml_loc * bool * PredSymb.resource * Logging.ml_loc
exception Missing_fld of Fieldname.t * Logging.ml_loc exception Missing_fld of Typ.Fieldname.t * Logging.ml_loc
exception Premature_nil_termination of Localise.error_desc * Logging.ml_loc exception Premature_nil_termination of Localise.error_desc * Logging.ml_loc
exception Null_dereference of Localise.error_desc * Logging.ml_loc exception Null_dereference of Localise.error_desc * Logging.ml_loc
exception Null_test_after_dereference of Localise.error_desc * Logging.ml_loc exception Null_test_after_dereference of Localise.error_desc * Logging.ml_loc

@ -53,7 +53,7 @@ and t =
/** The address of a program variable */ /** The address of a program variable */
| Lvar Pvar.t | Lvar Pvar.t
/** A field offset, the type is the surrounding struct type */ /** A field offset, the type is the surrounding struct type */
| Lfield t Fieldname.t Typ.t | Lfield t Typ.Fieldname.t Typ.t
/** An array index offset: [exp1\[exp2\]] */ /** An array index offset: [exp1\[exp2\]] */
| Lindex t t | Lindex t t
| Sizeof sizeof_data | Sizeof sizeof_data
@ -252,7 +252,7 @@ let rec pp_ pe pp_t f e => {
let id_exps = List.map f::(fun (id_exp, _, _) => id_exp) captured_vars; let id_exps = List.map f::(fun (id_exp, _, _) => id_exp) captured_vars;
F.fprintf f "(%a)" (Pp.comma_seq pp_exp) [Const (Cfun name), ...id_exps] F.fprintf f "(%a)" (Pp.comma_seq pp_exp) [Const (Cfun name), ...id_exps]
| Lvar pv => Pvar.pp pe f pv | Lvar pv => Pvar.pp pe f pv
| Lfield e fld _ => F.fprintf f "%a.%a" pp_exp e Fieldname.pp fld | Lfield e fld _ => F.fprintf f "%a.%a" pp_exp e Typ.Fieldname.pp fld
| Lindex e1 e2 => F.fprintf f "%a[%a]" pp_exp e1 pp_exp e2 | Lindex e1 e2 => F.fprintf f "%a[%a]" pp_exp e1 pp_exp e2
| Sizeof {typ, nbytes, dynamic_length, subtype} => | Sizeof {typ, nbytes, dynamic_length, subtype} =>
let pp_len f l => Option.iter f::(F.fprintf f "[%a]" pp_exp) l; let pp_len f l => Option.iter f::(F.fprintf f "[%a]" pp_exp) l;

@ -46,7 +46,7 @@ and t =
/** The address of a program variable */ /** The address of a program variable */
| Lvar Pvar.t | Lvar Pvar.t
/** A field offset, the type is the surrounding struct type */ /** A field offset, the type is the surrounding struct type */
| Lfield t Fieldname.t Typ.t | Lfield t Typ.Fieldname.t Typ.t
/** An array index offset: [exp1\[exp2\]] */ /** An array index offset: [exp1\[exp2\]] */
| Lindex t t | Lindex t t
| Sizeof sizeof_data | Sizeof sizeof_data

@ -1,125 +0,0 @@
/*
* Copyright (c) 2017 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
open! IStd;
module Hashtbl = Caml.Hashtbl;
type clang_field_info = {qual_class: QualifiedCppName.t, field_name: string} [@@deriving compare];
type t =
| Hidden /* Backend relies that Hidden is the smallest (first) field in Abs.should_raise_objc_leak */
| Clang clang_field_info
| Java string
[@@deriving compare];
let hidden_str = ".hidden";
let equal = [%compare.equal : t];
module Set =
Caml.Set.Make {
type nonrec t = t;
let compare = compare;
};
module Map =
Caml.Map.Make {
type nonrec t = t;
let compare = compare;
};
module Clang = {
let from_qualified qual_class field_name => Clang {qual_class, field_name};
};
module Java = {
let from_string n => Java n;
};
/** Convert a fieldname to a string. */
let to_string =
fun
| Hidden => hidden_str
| Java fname => fname
| Clang {field_name} => field_name;
/** Convert a fieldname to a simplified string with at most one-level path. */
let to_simplified_string fn => {
let s = to_string fn;
switch (String.rsplit2 s on::'.') {
| Some (s1, s2) =>
switch (String.rsplit2 s1 on::'.') {
| Some (_, s4) => s4 ^ "." ^ s2
| _ => s
}
| _ => s
}
};
/** Convert a fieldname to a flat string without path. */
let to_flat_string fn => {
let s = to_string fn;
switch (String.rsplit2 s on::'.') {
| Some (_, s2) => s2
| _ => s
}
};
let pp f =>
fun
| Hidden => Format.fprintf f "%s" hidden_str
| Java field_name
| Clang {field_name} => Format.fprintf f "%s" field_name;
let pp_latex style f fn => Latex.pp_string style f (to_string fn);
/** Returns the class part of the fieldname */
let java_get_class fn => {
let fn = to_string fn;
let ri = String.rindex_exn fn '.';
String.slice fn 0 ri
};
/** Returns the last component of the fieldname */
let java_get_field fn => {
let fn = to_string fn;
let ri = 1 + String.rindex_exn fn '.';
String.slice fn ri 0
};
/** Check if the field is the synthetic this$n of a nested class, used to access the n-th outher instance. */
let java_is_outer_instance fn => {
let fn = to_string fn;
let fn_len = String.length fn;
fn_len != 0 && {
let this = ".this$";
let last_char = fn.[fn_len - 1];
(last_char >= '0' && last_char <= '9') &&
String.is_suffix fn suffix::(this ^ String.of_char last_char)
}
};
let clang_get_qual_class =
fun
| Clang {qual_class} => Some qual_class
| _ => None;
/** hidded fieldname constant */
let hidden = Hidden;
/** hidded fieldname constant */
let is_hidden fn => equal fn hidden;

@ -1,81 +0,0 @@
/*
* Copyright (c) 2017 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
open! IStd;
/** Names for fields of class/struct/union */
type t [@@deriving compare];
/** Equality for field names. */
let equal: t => t => bool;
/** Set for fieldnames */
module Set: Caml.Set.S with type elt = t;
/** Map for fieldnames */
module Map: Caml.Map.S with type key = t;
module Clang: {
/** Create a clang field name from qualified c++ name */
let from_qualified: QualifiedCppName.t => string => t;
};
module Java: {
/** Create a java field name from string */
let from_string: string => t;
};
/** Convert a field name to a string. */
let to_string: t => string;
/** Convert a fieldname to a simplified string with at most one-level path. */
let to_simplified_string: t => string;
/** Convert a fieldname to a flat string without path. */
let to_flat_string: t => string;
/** Pretty print a field name. */
let pp: Format.formatter => t => unit;
/** Pretty print a field name in latex. */
let pp_latex: Latex.style => Format.formatter => t => unit;
/** The class part of the fieldname */
let java_get_class: t => string;
/** The last component of the fieldname */
let java_get_field: t => string;
/** Check if the field is the synthetic this$n of a nested class, used to access the n-th outher instance. */
let java_is_outer_instance: t => bool;
/** get qualified classname of a field if it's coming from clang frontend. returns None otherwise */
let clang_get_qual_class: t => option QualifiedCppName.t;
/** hidded fieldname constant */
let hidden: t;
/** hidded fieldname constant */
let is_hidden: t => bool;

@ -333,8 +333,8 @@ let rec format_typ typ = match typ.Typ.desc with
let format_field f = let format_field f =
if Config.curr_language_is Config.Java if Config.curr_language_is Config.Java
then Fieldname.java_get_field f then Typ.Fieldname.java_get_field f
else Fieldname.to_string f else Typ.Fieldname.to_string f
let format_method pname = let format_method pname =
match pname with match pname with
@ -490,11 +490,11 @@ let java_unchecked_exn_desc proc_name exn_name pre_str : error_desc =
} }
let desc_context_leak pname context_typ fieldname leak_path : error_desc = let desc_context_leak pname context_typ fieldname leak_path : error_desc =
let fld_str = Fieldname.to_string fieldname in let fld_str = Typ.Fieldname.to_string fieldname in
let leak_root = "Static field " ^ fld_str ^ " |->\n" in let leak_root = "Static field " ^ fld_str ^ " |->\n" in
let leak_path_entry_to_str acc entry = let leak_path_entry_to_str acc entry =
let entry_str = match entry with let entry_str = match entry with
| (Some fld, _) -> Fieldname.to_string fld | (Some fld, _) -> Typ.Fieldname.to_string fld
| (None, typ) -> Typ.to_string typ in | (None, typ) -> Typ.to_string typ in
(* intentionally omit space; [typ_to_string] adds an extra space *) (* intentionally omit space; [typ_to_string] adds an extra space *)
acc ^ entry_str ^ " |->\n" in acc ^ entry_str ^ " |->\n" in
@ -527,7 +527,7 @@ let desc_double_lock pname_opt object_str loc =
let desc_unsafe_guarded_by_access accessed_fld guarded_by_str loc = let desc_unsafe_guarded_by_access accessed_fld guarded_by_str loc =
let line_info = at_line (Tags.create ()) loc in let line_info = at_line (Tags.create ()) loc in
let accessed_fld_str = Fieldname.to_string accessed_fld in let accessed_fld_str = Typ.Fieldname.to_string accessed_fld in
let annot_str = Printf.sprintf "@GuardedBy(\"%s\")" guarded_by_str in let annot_str = Printf.sprintf "@GuardedBy(\"%s\")" guarded_by_str in
let syncronized_str = let syncronized_str =
MF.monospaced_to_string (Printf.sprintf "synchronized(%s)" guarded_by_str) in MF.monospaced_to_string (Printf.sprintf "synchronized(%s)" guarded_by_str) in
@ -629,7 +629,7 @@ let parameter_field_not_null_checked_desc (desc : error_desc) exp =
let field_not_nullable_desc exp = let field_not_nullable_desc exp =
let rec exp_to_string exp = let rec exp_to_string exp =
match exp with match exp with
| Exp.Lfield (exp', field, _) -> (exp_to_string exp')^" -> "^(Fieldname.to_string field) | Exp.Lfield (exp', field, _) -> (exp_to_string exp')^" -> "^(Typ.Fieldname.to_string field)
| Exp.Lvar pvar -> Mangled.to_string (Pvar.get_name pvar) | Exp.Lvar pvar -> Mangled.to_string (Pvar.get_name pvar)
| _ -> "" in | _ -> "" in
let var_s = exp_to_string exp in let var_s = exp_to_string exp in
@ -871,7 +871,7 @@ let desc_retain_cycle cycle loc cycle_dotty =
match se with match se with
| Sil.Eexp(Exp.Lvar pvar, _) when Pvar.equal pvar Sil.block_pvar -> | Sil.Eexp(Exp.Lvar pvar, _) when Pvar.equal pvar Sil.block_pvar ->
str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") a block capturing " ^ str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") a block capturing " ^
MF.monospaced_to_string (Fieldname.to_string f)^"; "; MF.monospaced_to_string (Typ.Fieldname.to_string f)^"; ";
ct:=!ct +1; ct:=!ct +1;
| Sil.Eexp(Exp.Lvar pvar as e, _) -> | Sil.Eexp(Exp.Lvar pvar as e, _) ->
let e_str = Exp.to_string e in let e_str = Exp.to_string e in
@ -879,14 +879,14 @@ let desc_retain_cycle cycle loc cycle_dotty =
remove_old e_str remove_old e_str
else e_str in else e_str in
str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") object "^e_str^" retaining " ^ str_cycle:=!str_cycle^" ("^(string_of_int !ct)^") object "^e_str^" retaining " ^
MF.monospaced_to_string (e_str^"."^(Fieldname.to_string f))^", "; MF.monospaced_to_string (e_str^"."^(Typ.Fieldname.to_string f))^", ";
ct:=!ct +1 ct:=!ct +1
| Sil.Eexp (Exp.Sizeof {typ}, _) -> | Sil.Eexp (Exp.Sizeof {typ}, _) ->
let step = let step =
" (" ^ (string_of_int !ct) ^ ") an object of " ^ " (" ^ (string_of_int !ct) ^ ") an object of " ^
MF.monospaced_to_string (Typ.to_string typ) ^ MF.monospaced_to_string (Typ.to_string typ) ^
" retaining another object via instance variable " ^ " retaining another object via instance variable " ^
MF.monospaced_to_string (Fieldname.to_string f) ^ ", " in MF.monospaced_to_string (Typ.Fieldname.to_string f) ^ ", " in
str_cycle := !str_cycle ^ step; str_cycle := !str_cycle ^ step;
ct:=!ct +1 ct:=!ct +1
| _ -> () in | _ -> () in

@ -273,11 +273,11 @@ val desc_null_test_after_dereference : string -> int -> Location.t -> error_desc
val java_unchecked_exn_desc : Typ.Procname.t -> Typ.Name.t -> string -> error_desc val java_unchecked_exn_desc : Typ.Procname.t -> Typ.Name.t -> string -> error_desc
val desc_context_leak : val desc_context_leak :
Typ.Procname.t -> Typ.t -> Fieldname.t -> Typ.Procname.t -> Typ.t -> Typ.Fieldname.t ->
(Fieldname.t option * Typ.t) list -> error_desc (Typ.Fieldname.t option * Typ.t) list -> error_desc
val desc_fragment_retains_view : val desc_fragment_retains_view :
Typ.t -> Fieldname.t -> Typ.t -> Typ.Procname.t -> error_desc Typ.t -> Typ.Fieldname.t -> Typ.t -> Typ.Procname.t -> error_desc
(* Create human-readable error description for assertion failures *) (* Create human-readable error description for assertion failures *)
val desc_custom_error : Location.t -> error_desc val desc_custom_error : Location.t -> error_desc
@ -292,7 +292,7 @@ val desc_precondition_not_met : pnm_kind option -> Typ.Procname.t -> Location.t
val desc_return_expression_required : string -> Location.t -> error_desc val desc_return_expression_required : string -> Location.t -> error_desc
val desc_retain_cycle : val desc_retain_cycle :
((Sil.strexp * Typ.t) * Fieldname.t * Sil.strexp) list -> ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list ->
Location.t -> string option -> error_desc Location.t -> string option -> error_desc
val registered_observer_being_deallocated_str : string -> string val registered_observer_being_deallocated_str : string -> string
@ -312,7 +312,7 @@ val desc_inherently_dangerous_function : Typ.Procname.t -> error_desc
val desc_unary_minus_applied_to_unsigned_expression : val desc_unary_minus_applied_to_unsigned_expression :
string option -> string -> Location.t -> error_desc string option -> string -> Location.t -> error_desc
val desc_unsafe_guarded_by_access : Fieldname.t -> string -> Location.t -> error_desc val desc_unsafe_guarded_by_access : Typ.Fieldname.t -> string -> Location.t -> error_desc
val desc_tainted_value_reaching_sensitive_function : val desc_tainted_value_reaching_sensitive_function :
PredSymb.taint_kind -> string -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> error_desc PredSymb.taint_kind -> string -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> error_desc

@ -38,8 +38,8 @@ let proc_flags_find proc_flags key => Hashtbl.find proc_flags key;
/** Type for ObjC accessors */ /** Type for ObjC accessors */
type objc_accessor_type = type objc_accessor_type =
| Objc_getter Fieldname.t | Objc_getter Typ.Fieldname.t
| Objc_setter Fieldname.t | Objc_setter Typ.Fieldname.t
[@@deriving compare]; [@@deriving compare];
type t = { type t = {

@ -33,8 +33,8 @@ let proc_flags_add: proc_flags => string => string => unit;
let proc_flags_find: proc_flags => string => string; let proc_flags_find: proc_flags => string => string;
type objc_accessor_type = type objc_accessor_type =
| Objc_getter Fieldname.t | Objc_getter Typ.Fieldname.t
| Objc_setter Fieldname.t | Objc_setter Typ.Fieldname.t
[@@deriving compare]; [@@deriving compare];
type t = { type t = {

@ -570,8 +570,10 @@ let pp_variable_list fmt etl =>
let pp_objc_accessor fmt accessor => let pp_objc_accessor fmt accessor =>
switch accessor { switch accessor {
| Some (ProcAttributes.Objc_getter name) => Format.fprintf fmt "Getter of %a, " Fieldname.pp name | Some (ProcAttributes.Objc_getter name) =>
| Some (ProcAttributes.Objc_setter name) => Format.fprintf fmt "Setter of %a, " Fieldname.pp name Format.fprintf fmt "Getter of %a, " Typ.Fieldname.pp name
| Some (ProcAttributes.Objc_setter name) =>
Format.fprintf fmt "Setter of %a, " Typ.Fieldname.pp name
| None => () | None => ()
}; };

@ -80,7 +80,7 @@ let instr_is_auxiliary =
/** offset for an lvalue */ /** offset for an lvalue */
type offset = type offset =
| Off_fld Fieldname.t Typ.t | Off_fld Typ.Fieldname.t Typ.t
| Off_index Exp.t; | Off_index Exp.t;
@ -144,7 +144,7 @@ let equal_inst = [%compare.equal : inst];
/** structured expressions represent a value of structured type, such as an array or a struct. */ /** structured expressions represent a value of structured type, such as an array or a struct. */
type strexp0 'inst = type strexp0 'inst =
| Eexp Exp.t 'inst /** Base case: expression with instrumentation */ | Eexp Exp.t 'inst /** Base case: expression with instrumentation */
| Estruct (list (Fieldname.t, strexp0 'inst)) 'inst /** C structure */ | Estruct (list (Typ.Fieldname.t, strexp0 'inst)) 'inst /** C structure */
/** Array of given length /** Array of given length
There are two conditions imposed / used in the array case. There are two conditions imposed / used in the array case.
First, if some index and value pair appears inside an array First, if some index and value pair appears inside an array
@ -419,7 +419,7 @@ let d_texp_full (te: Exp.t) => L.add_print_action (L.PTtexp_full, Obj.repr te);
/** Pretty print an offset */ /** Pretty print an offset */
let pp_offset pe f => let pp_offset pe f =>
fun fun
| Off_fld fld _ => F.fprintf f "%a" Fieldname.pp fld | Off_fld fld _ => F.fprintf f "%a" Typ.Fieldname.pp fld
| Off_index exp => F.fprintf f "%a" (pp_exp_printenv pe) exp; | Off_index exp => F.fprintf f "%a" (pp_exp_printenv pe) exp;
@ -927,11 +927,11 @@ let rec pp_sexp_env pe0 envo f se => {
switch pe.Pp.kind { switch pe.Pp.kind {
| TEXT | TEXT
| HTML => | HTML =>
let pp_diff f (n, se) => F.fprintf f "%a:%a" Fieldname.pp n (pp_sexp_env pe envo) se; let pp_diff f (n, se) => F.fprintf f "%a:%a" Typ.Fieldname.pp n (pp_sexp_env pe envo) se;
F.fprintf f "{%a}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst F.fprintf f "{%a}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst
| LATEX => | LATEX =>
let pp_diff f (n, se) => let pp_diff f (n, se) =>
F.fprintf f "%a:%a" (Fieldname.pp_latex Latex.Boldface) n (pp_sexp_env pe envo) se; F.fprintf f "%a:%a" (Typ.Fieldname.pp_latex Latex.Boldface) n (pp_sexp_env pe envo) se;
F.fprintf f "\\{%a\\}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst F.fprintf f "\\{%a\\}%a" (pp_seq_diff pp_diff pe) fel (pp_inst_if_trace pe) inst
} }
| Earray len nel inst => | Earray len nel inst =>
@ -2054,7 +2054,7 @@ let rec exp_compare_structural e1 e2 exp_map => {
if (n != 0) { if (n != 0) {
n n
} else { } else {
let n = Fieldname.compare f1 f2; let n = Typ.Fieldname.compare f1 f2;
if (n != 0) { if (n != 0) {
n n
} else { } else {

@ -77,7 +77,7 @@ let instr_is_auxiliary: instr => bool;
/** Offset for an lvalue. */ /** Offset for an lvalue. */
type offset = type offset =
| Off_fld Fieldname.t Typ.t | Off_fld Typ.Fieldname.t Typ.t
| Off_index Exp.t; | Off_index Exp.t;
@ -185,7 +185,7 @@ let inst_partial_meet: inst => inst => inst;
/** structured expressions represent a value of structured type, such as an array or a struct. */ /** structured expressions represent a value of structured type, such as an array or a struct. */
type strexp0 'inst = type strexp0 'inst =
| Eexp Exp.t 'inst /** Base case: expression with instrumentation */ | Eexp Exp.t 'inst /** Base case: expression with instrumentation */
| Estruct (list (Fieldname.t, strexp0 'inst)) 'inst /** C structure */ | Estruct (list (Typ.Fieldname.t, strexp0 'inst)) 'inst /** C structure */
/** Array of given length /** Array of given length
There are two conditions imposed / used in the array case. There are two conditions imposed / used in the array case.
First, if some index and value pair appears inside an array First, if some index and value pair appears inside an array

@ -1029,6 +1029,101 @@ let java_proc_return_typ pname_java :t => {
} }
}; };
module Fieldname = {
type clang_field_info = {qual_class: QualifiedCppName.t, field_name: string}
[@@deriving compare];
type t =
| Hidden /* Backend relies that Hidden is the smallest (first) field in Abs.should_raise_objc_leak */
| Clang clang_field_info
| Java string
[@@deriving compare];
let hidden_str = ".hidden";
let equal = [%compare.equal : t];
module T = {
type nonrec t = t;
let compare = compare;
};
module Set = Caml.Set.Make T;
module Map = Caml.Map.Make T;
module Clang = {
let from_qualified qual_class field_name => Clang {qual_class, field_name};
};
module Java = {
let from_string n => Java n;
};
/** Convert a fieldname to a string. */
let to_string =
fun
| Hidden => hidden_str
| Java fname => fname
| Clang {field_name} => field_name;
/** Convert a fieldname to a simplified string with at most one-level path. */
let to_simplified_string fn => {
let s = to_string fn;
switch (String.rsplit2 s on::'.') {
| Some (s1, s2) =>
switch (String.rsplit2 s1 on::'.') {
| Some (_, s4) => s4 ^ "." ^ s2
| _ => s
}
| _ => s
}
};
/** Convert a fieldname to a flat string without path. */
let to_flat_string fn => {
let s = to_string fn;
switch (String.rsplit2 s on::'.') {
| Some (_, s2) => s2
| _ => s
}
};
let pp f =>
fun
| Hidden => Format.fprintf f "%s" hidden_str
| Java field_name
| Clang {field_name} => Format.fprintf f "%s" field_name;
let pp_latex style f fn => Latex.pp_string style f (to_string fn);
/** Returns the class part of the fieldname */
let java_get_class fn => {
let fn = to_string fn;
let ri = String.rindex_exn fn '.';
String.slice fn 0 ri
};
/** Returns the last component of the fieldname */
let java_get_field fn => {
let fn = to_string fn;
let ri = 1 + String.rindex_exn fn '.';
String.slice fn ri 0
};
/** Check if the field is the synthetic this$n of a nested class, used to access the n-th outher instance. */
let java_is_outer_instance fn => {
let fn = to_string fn;
let fn_len = String.length fn;
fn_len != 0 && {
let this = ".this$";
let last_char = fn.[fn_len - 1];
(last_char >= '0' && last_char <= '9') &&
String.is_suffix fn suffix::(this ^ String.of_char last_char)
}
};
let clang_get_qual_class =
fun
| Clang {qual_class} => Some qual_class
| _ => None;
/** hidded fieldname constant */
let hidden = Hidden;
/** hidded fieldname constant */
let is_hidden fn => equal fn hidden;
};
module Struct = { module Struct = {
type field = (Fieldname.t, T.t, Annot.Item.t) [@@deriving compare]; type field = (Fieldname.t, T.t, Annot.Item.t) [@@deriving compare];
type fields = list field; type fields = list field;

@ -477,6 +477,64 @@ module Procname: {
/** Return the return type of [pname_java]. */ /** Return the return type of [pname_java]. */
let java_proc_return_typ: Procname.java => t; let java_proc_return_typ: Procname.java => t;
module Fieldname: {
/** Names for fields of class/struct/union */
type t [@@deriving compare];
/** Equality for field names. */
let equal: t => t => bool;
/** Set for fieldnames */
module Set: Caml.Set.S with type elt = t;
/** Map for fieldnames */
module Map: Caml.Map.S with type key = t;
module Clang: {
/** Create a clang field name from qualified c++ name */
let from_qualified: QualifiedCppName.t => string => t;
};
module Java: {
/** Create a java field name from string */
let from_string: string => t;
};
/** Convert a field name to a string. */
let to_string: t => string;
/** Convert a fieldname to a simplified string with at most one-level path. */
let to_simplified_string: t => string;
/** Convert a fieldname to a flat string without path. */
let to_flat_string: t => string;
/** Pretty print a field name. */
let pp: Format.formatter => t => unit;
/** Pretty print a field name in latex. */
let pp_latex: Latex.style => Format.formatter => t => unit;
/** The class part of the fieldname */
let java_get_class: t => string;
/** The last component of the fieldname */
let java_get_field: t => string;
/** Check if the field is the synthetic this$n of a nested class, used to access the n-th outher instance. */
let java_is_outer_instance: t => bool;
/** get qualified classname of a field if it's coming from clang frontend. returns None otherwise */
let clang_get_qual_class: t => option QualifiedCppName.t;
/** hidded fieldname constant */
let hidden: t;
/** hidded fieldname constant */
let is_hidden: t => bool;
};
module Struct: { module Struct: {
type field = (Fieldname.t, typ, Annot.Item.t) [@@deriving compare]; type field = (Fieldname.t, typ, Annot.Item.t) [@@deriving compare];
type fields = list field; type fields = list field;

@ -23,7 +23,7 @@ module ST : sig
Localise.t -> Localise.t ->
Location.t -> Location.t ->
?advice: string option -> ?advice: string option ->
?field_name: Fieldname.t option -> ?field_name: Typ.Fieldname.t option ->
?origin_loc: Location.t option -> ?origin_loc: Location.t option ->
?exception_kind: (string -> Localise.error_desc -> exn) -> ?exception_kind: (string -> Localise.error_desc -> exn) ->
?always_report: bool -> ?always_report: bool ->

@ -107,13 +107,13 @@ let rec get_type_name {Typ.desc} =
let get_field_type_name tenv let get_field_type_name tenv
(typ: Typ.t) (typ: Typ.t)
(fieldname: Fieldname.t): string option = (fieldname: Typ.Fieldname.t): string option =
match typ.desc with match typ.desc with
| Tstruct name | Tptr ({desc=Tstruct name}, _) -> ( | Tstruct name | Tptr ({desc=Tstruct name}, _) -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields } -> ( | Some { fields } -> (
match List.find match List.find
~f:(function | (fn, _, _) -> Fieldname.equal fn fieldname) ~f:(function | (fn, _, _) -> Typ.Fieldname.equal fn fieldname)
fields with fields with
| Some (_, ft, _) -> Some (get_type_name ft) | Some (_, ft, _) -> Some (get_type_name ft)
| None -> None | None -> None
@ -204,7 +204,7 @@ let is_setter pname_java =
(** Returns the signature of a field access (class name, field name, field type name) *) (** Returns the signature of a field access (class name, field name, field type name) *)
let get_java_field_access_signature = function let get_java_field_access_signature = function
| Sil.Load (_, Exp.Lfield (_, fn, ft), bt, _) -> | Sil.Load (_, Exp.Lfield (_, fn, ft), bt, _) ->
Some (get_type_name bt, Fieldname.java_get_field fn, get_type_name ft) Some (get_type_name bt, Typ.Fieldname.java_get_field fn, get_type_name ft)
| _ -> None | _ -> None
(** Returns the formal signature (class name, method name, (** Returns the formal signature (class name, method name,
@ -343,13 +343,13 @@ let get_fields_nullified procdesc =
let collect_nullified_flds (nullified_flds, this_ids) _ = function let collect_nullified_flds (nullified_flds, this_ids) _ = function
| Sil.Store (Exp.Lfield (Exp.Var lhs, fld, _), _, rhs, _) | Sil.Store (Exp.Lfield (Exp.Var lhs, fld, _), _, rhs, _)
when Exp.is_null_literal rhs && Ident.IdentSet.mem lhs this_ids -> when Exp.is_null_literal rhs && Ident.IdentSet.mem lhs this_ids ->
(Fieldname.Set.add fld nullified_flds, this_ids) (Typ.Fieldname.Set.add fld nullified_flds, this_ids)
| Sil.Load (id, rhs, _, _) when Exp.is_this rhs -> | Sil.Load (id, rhs, _, _) when Exp.is_this rhs ->
(nullified_flds, Ident.IdentSet.add id this_ids) (nullified_flds, Ident.IdentSet.add id this_ids)
| _ -> (nullified_flds, this_ids) in | _ -> (nullified_flds, this_ids) in
let (nullified_flds, _) = let (nullified_flds, _) =
Procdesc.fold_instrs Procdesc.fold_instrs
collect_nullified_flds (Fieldname.Set.empty, Ident.IdentSet.empty) procdesc in collect_nullified_flds (Typ.Fieldname.Set.empty, Ident.IdentSet.empty) procdesc in
nullified_flds nullified_flds
(** Checks if the exception is an unchecked exception *) (** Checks if the exception is an unchecked exception *)

@ -102,7 +102,7 @@ val type_is_class : Typ.t -> bool
val type_is_object : 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] *) (** return the set of instance fields that are assigned to a null literal in [procdesc] *)
val get_fields_nullified : Procdesc.t -> Fieldname.Set.t val get_fields_nullified : Procdesc.t -> Typ.Fieldname.Set.t
(** [is_exception tenv class_name] checks if class_name is of type java.lang.Exception *) (** [is_exception tenv class_name] checks if class_name is of type java.lang.Exception *)
val is_exception : Tenv.t -> Typ.Name.t -> bool val is_exception : Tenv.t -> Typ.Name.t -> bool

@ -391,7 +391,7 @@ let execute___get_hidden_field { Builtin.tenv; pdesc; prop_; path; ret_id; args;
| Some e -> return_result tenv e p ret_id | Some e -> return_result tenv e p ret_id
| None -> p in | None -> p in
let foot_var = lazy (Exp.Var (Ident.create_fresh Ident.kfootprint)) in let foot_var = lazy (Exp.Var (Ident.create_fresh Ident.kfootprint)) in
let filter_fld_hidden (f, _ ) = Fieldname.is_hidden f in let filter_fld_hidden (f, _ ) = Typ.Fieldname.is_hidden f in
let has_fld_hidden fsel = List.exists ~f:filter_fld_hidden fsel in let has_fld_hidden fsel = List.exists ~f:filter_fld_hidden fsel in
let do_hpred in_foot hpred = match hpred with let do_hpred in_foot hpred = match hpred with
| Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp) | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp)
@ -399,7 +399,7 @@ let execute___get_hidden_field { Builtin.tenv; pdesc; prop_; path; ret_id; args;
let foot_e = Lazy.force foot_var in let foot_e = Lazy.force foot_var in
ret_val := Some foot_e; ret_val := Some foot_e;
let se = Sil.Eexp(foot_e, Sil.inst_none) in let se = Sil.Eexp(foot_e, Sil.inst_none) in
let fsel' = (Fieldname.hidden, se) :: fsel in let fsel' = (Typ.Fieldname.hidden, se) :: fsel in
Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp) Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp)
| Sil.Hpointsto(e, Sil.Estruct (fsel, _), _) | Sil.Hpointsto(e, Sil.Estruct (fsel, _), _)
when Exp.equal e n_lexp && not in_foot && has_fld_hidden fsel -> when Exp.equal e n_lexp && not in_foot && has_fld_hidden fsel ->
@ -429,21 +429,21 @@ let execute___set_hidden_field { Builtin.tenv; pdesc; prop_; path; args; }
let n_lexp1, prop__ = check_arith_norm_exp tenv pname lexp1 prop_ in let n_lexp1, prop__ = check_arith_norm_exp tenv pname lexp1 prop_ in
let n_lexp2, prop = check_arith_norm_exp tenv pname lexp2 prop__ in let n_lexp2, prop = check_arith_norm_exp tenv pname lexp2 prop__ in
let foot_var = lazy (Exp.Var (Ident.create_fresh Ident.kfootprint)) in let foot_var = lazy (Exp.Var (Ident.create_fresh Ident.kfootprint)) in
let filter_fld_hidden (f, _ ) = Fieldname.is_hidden f in let filter_fld_hidden (f, _ ) = Typ.Fieldname.is_hidden f in
let has_fld_hidden fsel = List.exists ~f:filter_fld_hidden fsel in let has_fld_hidden fsel = List.exists ~f:filter_fld_hidden fsel in
let do_hpred in_foot hpred = match hpred with let do_hpred in_foot hpred = match hpred with
| Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp) | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp)
when Exp.equal e n_lexp1 && not in_foot -> when Exp.equal e n_lexp1 && not in_foot ->
let se = Sil.Eexp(n_lexp2, Sil.inst_none) in let se = Sil.Eexp(n_lexp2, Sil.inst_none) in
let fsel' = let fsel' =
(Fieldname.hidden, se) :: (Typ.Fieldname.hidden, se) ::
(List.filter ~f:(fun x -> not (filter_fld_hidden x)) fsel) in (List.filter ~f:(fun x -> not (filter_fld_hidden x)) fsel) in
Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp) Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp)
| Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp) | Sil.Hpointsto(e, Sil.Estruct (fsel, inst), texp)
when Exp.equal e n_lexp1 && in_foot && not (has_fld_hidden fsel) -> when Exp.equal e n_lexp1 && in_foot && not (has_fld_hidden fsel) ->
let foot_e = Lazy.force foot_var in let foot_e = Lazy.force foot_var in
let se = Sil.Eexp(foot_e, Sil.inst_none) in let se = Sil.Eexp(foot_e, Sil.inst_none) in
let fsel' = (Fieldname.hidden, se) :: fsel in let fsel' = (Typ.Fieldname.hidden, se) :: fsel in
Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp) Sil.Hpointsto(e, Sil.Estruct (fsel', inst), texp)
| _ -> hpred in | _ -> hpred in
let sigma' = List.map ~f:(do_hpred false) prop.Prop.sigma in let sigma' = List.map ~f:(do_hpred false) prop.Prop.sigma in
@ -465,7 +465,7 @@ let execute___objc_counter_update
(* This is the case as a call f(o) it's translates as n$1=*&o; f(n$1) *) (* This is the case as a call f(o) it's translates as n$1=*&o; f(n$1) *)
(* n$2 = *n$1.hidden *) (* n$2 = *n$1.hidden *)
let tmp = Ident.create_fresh Ident.knormal in let tmp = Ident.create_fresh Ident.knormal in
let hidden_field = Exp.Lfield (lexp, Fieldname.hidden, typ) in let hidden_field = Exp.Lfield (lexp, Typ.Fieldname.hidden, typ) in
let counter_to_tmp = Sil.Load (tmp, hidden_field, typ, loc) in let counter_to_tmp = Sil.Load (tmp, hidden_field, typ, loc) in
(* *n$1.hidden = (n$2 +/- delta) *) (* *n$1.hidden = (n$2 +/- delta) *)
let update_counter = let update_counter =

@ -478,7 +478,7 @@ let discover_para_candidates tenv p =
let edges = ref [] in let edges = ref [] in
let add_edge edg = edges := edg :: !edges in let add_edge edg = edges := edg :: !edges in
let get_edges_strexp rec_flds root se = let get_edges_strexp rec_flds root se =
let is_rec_fld fld = List.exists ~f:(Fieldname.equal fld) rec_flds in let is_rec_fld fld = List.exists ~f:(Typ.Fieldname.equal fld) rec_flds in
match se with match se with
| Sil.Eexp _ | Sil.Earray _ -> () | Sil.Eexp _ | Sil.Earray _ -> ()
| Sil.Estruct (fsel, _) -> | Sil.Estruct (fsel, _) ->
@ -514,7 +514,7 @@ let discover_para_dll_candidates tenv p =
let edges = ref [] in let edges = ref [] in
let add_edge edg = (edges := edg :: !edges) in let add_edge edg = (edges := edg :: !edges) in
let get_edges_strexp rec_flds root se = let get_edges_strexp rec_flds root se =
let is_rec_fld fld = List.exists ~f:(Fieldname.equal fld) rec_flds in let is_rec_fld fld = List.exists ~f:(Typ.Fieldname.equal fld) rec_flds in
match se with match se with
| Sil.Eexp _ | Sil.Earray _ -> () | Sil.Eexp _ | Sil.Earray _ -> ()
| Sil.Estruct (fsel, _) -> | Sil.Estruct (fsel, _) ->
@ -893,7 +893,7 @@ let get_cycle root prop =
match e, e' with match e, e' with
| Sil.Eexp (e, _), Sil.Eexp (e', _) -> | Sil.Eexp (e, _), Sil.Eexp (e', _) ->
L.d_str ("("^(Exp.to_string e)^": "^(Typ.to_string t)^", " L.d_str ("("^(Exp.to_string e)^": "^(Typ.to_string t)^", "
^(Fieldname.to_string f)^", "^(Exp.to_string e')^")") ^(Typ.Fieldname.to_string f)^", "^(Exp.to_string e')^")")
| _ -> ()) cyc; | _ -> ()) cyc;
L.d_strln "") in L.d_strln "") in
(* Perform a dfs of a graph stopping when e_root is reached. (* Perform a dfs of a graph stopping when e_root is reached.
@ -938,7 +938,7 @@ let should_raise_objc_leak hpred =
match hpred with match hpred with
| Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Exp.Const (Const.Cint i)), _)):: _, _), | Sil.Hpointsto(_, Sil.Estruct((fn, Sil.Eexp( (Exp.Const (Const.Cint i)), _)):: _, _),
Exp.Sizeof {typ}) Exp.Sizeof {typ})
when Fieldname.is_hidden fn && IntLit.gt i IntLit.zero (* counter > 0 *) -> when Typ.Fieldname.is_hidden fn && IntLit.gt i IntLit.zero (* counter > 0 *) ->
Mleak_buckets.should_raise_objc_leak typ Mleak_buckets.should_raise_objc_leak typ
| _ -> None | _ -> None
@ -1003,7 +1003,7 @@ let cycle_has_weak_or_unretained_or_assign_field tenv cycle =
let get_item_annotation (t: Typ.t) fn = let get_item_annotation (t: Typ.t) fn =
match t.desc with match t.desc with
| Tstruct name -> ( | Tstruct name -> (
let equal_fn (fn', _, _) = Fieldname.equal fn fn' in let equal_fn (fn', _, _) = Typ.Fieldname.equal fn fn' in
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields; statics } -> ( | Some { fields; statics } -> (
List.find ~f:equal_fn (fields @ statics) |> List.find ~f:equal_fn (fields @ statics) |>

@ -58,7 +58,7 @@ module StrexpMatch : sig
end = struct end = struct
(** syntactic offset *) (** syntactic offset *)
type syn_offset = Field of Fieldname.t * Typ.t | Index of Exp.t type syn_offset = Field of Typ.Fieldname.t * Typ.t | Index of Exp.t
(** path through an Estruct *) (** path through an Estruct *)
type path = Exp.t * (syn_offset list) type path = Exp.t * (syn_offset list)
@ -77,9 +77,9 @@ end = struct
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields } -> | Some { fields } ->
let se' = let se' =
snd (List.find_exn ~f:(fun (f', _) -> Fieldname.equal f' fld) fsel) in snd (List.find_exn ~f:(fun (f', _) -> Typ.Fieldname.equal f' fld) fsel) in
let t' = let t' =
snd3 (List.find_exn ~f:(fun (f', _, _) -> Fieldname.equal f' fld) fields) in snd3 (List.find_exn ~f:(fun (f', _, _) -> Typ.Fieldname.equal f' fld) fields) in
get_strexp_at_syn_offsets tenv se' t' syn_offs' get_strexp_at_syn_offsets tenv se' t' syn_offs'
| None -> | None ->
fail () fail ()
@ -98,14 +98,14 @@ end = struct
| Sil.Estruct (fsel, inst), Tstruct name, Field (fld, _) :: syn_offs' -> ( | Sil.Estruct (fsel, inst), Tstruct name, Field (fld, _) :: syn_offs' -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields } -> | Some { fields } ->
let se' = snd (List.find_exn ~f:(fun (f', _) -> Fieldname.equal f' fld) fsel) in let se' = snd (List.find_exn ~f:(fun (f', _) -> Typ.Fieldname.equal f' fld) fsel) in
let t' = (fun (_,y,_) -> y) let t' = (fun (_,y,_) -> y)
(List.find_exn ~f:(fun (f', _, _) -> (List.find_exn ~f:(fun (f', _, _) ->
Fieldname.equal f' fld) fields) in Typ.Fieldname.equal f' fld) fields) in
let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in let se_mod = replace_strexp_at_syn_offsets tenv se' t' syn_offs' update in
let fsel' = let fsel' =
List.map ~f:(fun (f'', se'') -> List.map ~f:(fun (f'', se'') ->
if Fieldname.equal f'' fld then (fld, se_mod) else (f'', se'') if Typ.Fieldname.equal f'' fld then (fld, se_mod) else (f'', se'')
) fsel in ) fsel in
Sil.Estruct (fsel', inst) Sil.Estruct (fsel', inst)
| None -> | None ->
@ -179,12 +179,12 @@ end = struct
| [] -> () | [] -> ()
| (f, se) :: fsel' -> | (f, se) :: fsel' ->
begin begin
match List.find ~f:(fun (f', _, _) -> Fieldname.equal f' f) ftal with match List.find ~f:(fun (f', _, _) -> Typ.Fieldname.equal f' f) ftal with
| Some (_, t, _) -> | Some (_, t, _) ->
find_offset_sexp sigma_other hpred root ((Field (f, typ)) :: offs) se t find_offset_sexp sigma_other hpred root ((Field (f, typ)) :: offs) se t
| None -> | None ->
L.d_strln L.d_strln
("Can't find field " ^ (Fieldname.to_string f) ^ " in StrexpMatch.find") ("Can't find field " ^ (Typ.Fieldname.to_string f) ^ " in StrexpMatch.find")
end; end;
find_offset_fsel sigma_other hpred root offs fsel' ftal typ find_offset_fsel sigma_other hpred root offs fsel' ftal typ
and find_offset_esel sigma_other hpred root offs esel t = match esel with and find_offset_esel sigma_other hpred root offs esel t = match esel with

@ -965,7 +965,7 @@ let rec exp_partial_join (e1: Exp.t) (e2: Exp.t) : Exp.t =
if not (Pvar.equal pvar1 pvar2) then (L.d_strln "failure reason 25"; raise Sil.JoinFail) if not (Pvar.equal pvar1 pvar2) then (L.d_strln "failure reason 25"; raise Sil.JoinFail)
else e1 else e1
| Exp.Lfield(e1, f1, t1), Exp.Lfield(e2, f2, _) -> | Exp.Lfield(e1, f1, t1), Exp.Lfield(e2, f2, _) ->
if not (Fieldname.equal f1 f2) then (L.d_strln "failure reason 26"; raise Sil.JoinFail) if not (Typ.Fieldname.equal f1 f2) then (L.d_strln "failure reason 26"; raise Sil.JoinFail)
else Exp.Lfield(exp_partial_join e1 e2, f1, t1) (* should be t1 = t2 *) else Exp.Lfield(exp_partial_join e1 e2, f1, t1) (* should be t1 = t2 *)
| Exp.Lindex(e1, e1'), Exp.Lindex(e2, e2') -> | Exp.Lindex(e1, e1'), Exp.Lindex(e2, e2') ->
let e1'' = exp_partial_join e1 e2 in let e1'' = exp_partial_join e1 e2 in
@ -1058,7 +1058,7 @@ let rec exp_partial_meet (e1: Exp.t) (e2: Exp.t) : Exp.t =
if not (Pvar.equal pvar1 pvar2) then (L.d_strln "failure reason 35"; raise Sil.JoinFail) if not (Pvar.equal pvar1 pvar2) then (L.d_strln "failure reason 35"; raise Sil.JoinFail)
else e1 else e1
| Exp.Lfield(e1, f1, t1), Exp.Lfield(e2, f2, _) -> | Exp.Lfield(e1, f1, t1), Exp.Lfield(e2, f2, _) ->
if not (Fieldname.equal f1 f2) then (L.d_strln "failure reason 36"; raise Sil.JoinFail) if not (Typ.Fieldname.equal f1 f2) then (L.d_strln "failure reason 36"; raise Sil.JoinFail)
else Exp.Lfield(exp_partial_meet e1 e2, f1, t1) (* should be t1 = t2 *) else Exp.Lfield(exp_partial_meet e1 e2, f1, t1) (* should be t1 = t2 *)
| Exp.Lindex(e1, e1'), Exp.Lindex(e2, e2') -> | Exp.Lindex(e1, e1'), Exp.Lindex(e2, e2') ->
let e1'' = exp_partial_meet e1 e2 in let e1'' = exp_partial_meet e1 e2 in
@ -1085,7 +1085,7 @@ let rec strexp_partial_join mode (strexp1: Sil.strexp) (strexp2: Sil.strexp) : S
| JoinState.Post -> Sil.Estruct (List.rev acc, inst) | JoinState.Post -> Sil.Estruct (List.rev acc, inst)
end end
| (fld1, se1):: fld_se_list1', (fld2, se2):: fld_se_list2' -> | (fld1, se1):: fld_se_list1', (fld2, se2):: fld_se_list2' ->
let comparison = Fieldname.compare fld1 fld2 in let comparison = Typ.Fieldname.compare fld1 fld2 in
if Int.equal comparison 0 then if Int.equal comparison 0 then
let strexp' = strexp_partial_join mode se1 se2 in let strexp' = strexp_partial_join mode se1 se2 in
let fld_se_list_new = (fld1, strexp') :: acc in let fld_se_list_new = (fld1, strexp') :: acc in
@ -1149,7 +1149,7 @@ let rec strexp_partial_meet (strexp1: Sil.strexp) (strexp2: Sil.strexp) : Sil.st
| _, [] -> | _, [] ->
Sil.Estruct (construct Lhs acc fld_se_list1, inst) Sil.Estruct (construct Lhs acc fld_se_list1, inst)
| (fld1, se1):: fld_se_list1', (fld2, se2):: fld_se_list2' -> | (fld1, se1):: fld_se_list1', (fld2, se2):: fld_se_list2' ->
let comparison = Fieldname.compare fld1 fld2 in let comparison = Typ.Fieldname.compare fld1 fld2 in
if comparison < 0 then if comparison < 0 then
let se' = strexp_construct_fresh Lhs se1 in let se' = strexp_construct_fresh Lhs se1 in
let acc_new = (fld1, se'):: acc in let acc_new = (fld1, se'):: acc in

@ -66,7 +66,7 @@ type dotty_node =
(* Dotpointsto(coo,e,c): basic memory cell box for expression e at coordinate coo and color c *) (* Dotpointsto(coo,e,c): basic memory cell box for expression e at coordinate coo and color c *)
| Dotpointsto of coordinate * Exp.t * string | Dotpointsto of coordinate * Exp.t * string
(* Dotstruct(coo,e,l,c): struct box for expression e with field list l at coordinate coo and color c *) (* Dotstruct(coo,e,l,c): struct box for expression e with field list l at coordinate coo and color c *)
| Dotstruct of coordinate * Exp.t * (Fieldname.t * Sil.strexp) list * string * Exp.t | Dotstruct of coordinate * Exp.t * (Typ.Fieldname.t * Sil.strexp) list * string * Exp.t
(* Dotarray(coo,e1,e2,l,t,c): array box for expression e1 with field list l at coordinate coo and color c*) (* Dotarray(coo,e1,e2,l,t,c): array box for expression e1 with field list l at coordinate coo and color c*)
(* e2 is the len and t is the type *) (* e2 is the len and t is the type *)
| Dotarray of coordinate * Exp.t * Exp.t * (Exp.t * Sil.strexp) list * Typ.t * string | Dotarray of coordinate * Exp.t * Exp.t * (Exp.t * Sil.strexp) list * Typ.t * string
@ -146,8 +146,8 @@ let rec strexp_to_string pe coo f se =
and struct_to_dotty_str pe coo f ls : unit = and struct_to_dotty_str pe coo f ls : unit =
match ls with match ls with
| [] -> () | [] -> ()
| (fn, se)::[]-> F.fprintf f "{ <%s%iL%i> %s: %a } " (Fieldname.to_string fn) coo.id coo.lambda (Fieldname.to_string fn) (strexp_to_string pe coo) se | (fn, se)::[]-> F.fprintf f "{ <%s%iL%i> %s: %a } " (Typ.Fieldname.to_string fn) coo.id coo.lambda (Typ.Fieldname.to_string fn) (strexp_to_string pe coo) se
| (fn, se):: ls'-> F.fprintf f " { <%s%iL%i> %s: %a } | %a" (Fieldname.to_string fn) coo.id coo.lambda (Fieldname.to_string fn) (strexp_to_string pe coo) se (struct_to_dotty_str pe coo) ls' | (fn, se):: ls'-> F.fprintf f " { <%s%iL%i> %s: %a } | %a" (Typ.Fieldname.to_string fn) coo.id coo.lambda (Typ.Fieldname.to_string fn) (strexp_to_string pe coo) se (struct_to_dotty_str pe coo) ls'
and get_contents_sexp pe coo f se = and get_contents_sexp pe coo f se =
match se with match se with
@ -390,7 +390,7 @@ let in_cycle cycle edge =
| Some cycle' -> | Some cycle' ->
let (fn, se) = edge in let (fn, se) = edge in
List.exists List.exists
~f:(fun (_,fn',se') -> Fieldname.equal fn fn' && Sil.equal_strexp se se') ~f:(fun (_,fn',se') -> Typ.Fieldname.equal fn fn' && Sil.equal_strexp se se')
cycle' cycle'
| _ -> false | _ -> false
@ -409,7 +409,7 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle =
if is_nil e p then begin if is_nil e p then begin
let n'= make_nil_node lambda in let n'= make_nil_node lambda in
if !print_full_prop then if !print_full_prop then
[(LinkStructToExp, Fieldname.to_string fn, n',"")] [(LinkStructToExp, Typ.Fieldname.to_string fn, n',"")]
else [] else []
end else end else
let nodes_e = select_nodes_exp_lambda dotnodes e lambda in let nodes_e = select_nodes_exp_lambda dotnodes e lambda in
@ -417,7 +417,7 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle =
| [] -> | [] ->
(match box_dangling e with (match box_dangling e with
| None -> [] | None -> []
| Some n' -> [(LinkStructToExp, Fieldname.to_string fn, n',"")] | Some n' -> [(LinkStructToExp, Typ.Fieldname.to_string fn, n',"")]
) )
| [node] | [Dotpointsto _ ; node] | [node; Dotpointsto _] -> | [node] | [Dotpointsto _ ; node] | [node; Dotpointsto _] ->
let n = get_coordinate_id node in let n = get_coordinate_id node in
@ -426,9 +426,9 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle =
let link_kind = if (in_cycle cycle (fn, se)) && (not !print_full_prop) then let link_kind = if (in_cycle cycle (fn, se)) && (not !print_full_prop) then
LinkRetainCycle LinkRetainCycle
else LinkStructToStruct in else LinkStructToStruct in
[(link_kind, Fieldname.to_string fn, n, e_no_special_char)] [(link_kind, Typ.Fieldname.to_string fn, n, e_no_special_char)]
end else end else
[(LinkStructToExp, Fieldname.to_string fn, n,"")] [(LinkStructToExp, Typ.Fieldname.to_string fn, n,"")]
| _ -> (* by construction there must be at most 2 nodes for an expression*) | _ -> (* by construction there must be at most 2 nodes for an expression*)
L.internal_error "@\n Too many nodes! Error! @\n@."; assert false) L.internal_error "@\n Too many nodes! Error! @\n@."; assert false)
| Sil.Estruct (_, _) -> [] (* inner struct are printed by print_struc function *) | Sil.Estruct (_, _) -> [] (* inner struct are printed by print_struc function *)
@ -1283,7 +1283,7 @@ let rec compute_target_nodes_from_sexp nodes se prop field_lab =
(match lfld with (match lfld with
| [] -> [] | [] -> []
| (fn, se2):: l' -> | (fn, se2):: l' ->
compute_target_nodes_from_sexp nodes se2 prop (Fieldname.to_string fn) @ compute_target_nodes_from_sexp nodes se2 prop (Typ.Fieldname.to_string fn) @
compute_target_nodes_from_sexp nodes (Sil.Estruct (l', inst)) prop "" compute_target_nodes_from_sexp nodes (Sil.Estruct (l', inst)) prop ""
) )
| Sil.Earray (len, lie, inst) -> | Sil.Earray (len, lie, inst) ->
@ -1354,7 +1354,7 @@ let rec pointsto_contents_to_xml (co: Sil.strexp) : Io_infer.Xml.node =
| Sil.Eexp (e, _) -> | Sil.Eexp (e, _) ->
Io_infer.Xml.create_tree "cell" [("content-value", exp_to_xml_string e)] [] Io_infer.Xml.create_tree "cell" [("content-value", exp_to_xml_string e)] []
| Sil.Estruct (fel, _) -> | Sil.Estruct (fel, _) ->
let f (fld, exp) = Io_infer.Xml.create_tree "struct-field" [("id", Fieldname.to_string fld)] [(pointsto_contents_to_xml exp)] in let f (fld, exp) = Io_infer.Xml.create_tree "struct-field" [("id", Typ.Fieldname.to_string fld)] [(pointsto_contents_to_xml exp)] in
Io_infer.Xml.create_tree "struct" [] (List.map ~f fel) Io_infer.Xml.create_tree "struct" [] (List.map ~f fel)
| Sil.Earray (len, nel, _) -> | Sil.Earray (len, nel, _) ->
let f (e, se) = Io_infer.Xml.create_tree "array-element" [("index", exp_to_xml_string e)] [pointsto_contents_to_xml se] in let f (e, se) = Io_infer.Xml.create_tree "array-element" [("index", exp_to_xml_string e)] [pointsto_contents_to_xml se] in

@ -23,7 +23,7 @@ type kind_of_dotty_prop =
val reset_proposition_counter : unit -> unit val reset_proposition_counter : unit -> unit
val pp_dotty : Format.formatter -> kind_of_dotty_prop -> Prop.normal Prop.t -> val pp_dotty : Format.formatter -> kind_of_dotty_prop -> Prop.normal Prop.t ->
((Sil.strexp * Typ.t) * Fieldname.t * Sil.strexp) list option -> unit ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list option -> unit
(** {2 Sets and lists of propositions} *) (** {2 Sets and lists of propositions} *)
@ -44,10 +44,10 @@ val pp_speclist_dotty_file : DB.filename -> Prop.normal Specs.spec list -> unit
(* create a dotty file with a single proposition *) (* create a dotty file with a single proposition *)
val dotty_prop_to_dotty_file : string -> Prop.normal Prop.t -> val dotty_prop_to_dotty_file : string -> Prop.normal Prop.t ->
((Sil.strexp * Typ.t) * Fieldname.t * Sil.strexp) list -> unit ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list -> unit
val dotty_prop_to_str : Prop.normal Prop.t -> val dotty_prop_to_str : Prop.normal Prop.t ->
((Sil.strexp * Typ.t) * Fieldname.t * Sil.strexp) list -> string option ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list -> string option
(** reset the counter used for node and heap identifiers *) (** reset the counter used for node and heap identifiers *)
val reset_node_counter : unit -> unit val reset_node_counter : unit -> unit

@ -40,8 +40,8 @@ let is_vector_method pname =
is_method_of_objc_cpp_class pname vector_matcher is_method_of_objc_cpp_class pname vector_matcher
let is_special_field matcher field_name_opt field = let is_special_field matcher field_name_opt field =
let field_name = Fieldname.to_flat_string field in let field_name = Typ.Fieldname.to_flat_string field in
let class_qual_opt = Fieldname.clang_get_qual_class field in let class_qual_opt = Typ.Fieldname.clang_get_qual_class field in
let field_ok = let field_ok =
match field_name_opt with match field_name_opt with
| Some field_name' -> String.equal field_name' field_name | Some field_name' -> String.equal field_name' field_name
@ -320,7 +320,7 @@ and _exp_lv_dexp tenv (_seen : Exp.Set.t) node e : DExp.t option =
begin begin
L.d_str "exp_lv_dexp: Lfield with var "; L.d_str "exp_lv_dexp: Lfield with var ";
Sil.d_exp (Exp.Var id); Sil.d_exp (Exp.Var id);
L.d_str (" " ^ Fieldname.to_string f); L.d_str (" " ^ Typ.Fieldname.to_string f);
L.d_ln () L.d_ln ()
end; end;
(match _find_normal_variable_load tenv seen node id with (match _find_normal_variable_load tenv seen node id with
@ -331,7 +331,7 @@ and _exp_lv_dexp tenv (_seen : Exp.Set.t) node e : DExp.t option =
begin begin
L.d_str "exp_lv_dexp: Lfield "; L.d_str "exp_lv_dexp: Lfield ";
Sil.d_exp e1; Sil.d_exp e1;
L.d_str (" " ^ Fieldname.to_string f); L.d_str (" " ^ Typ.Fieldname.to_string f);
L.d_ln () L.d_ln ()
end; end;
(match _exp_lv_dexp tenv seen node e1 with (match _exp_lv_dexp tenv seen node e1 with
@ -379,7 +379,7 @@ and _exp_rv_dexp tenv (_seen : Exp.Set.t) node e : DExp.t option =
begin begin
L.d_str "exp_rv_dexp: Lfield "; L.d_str "exp_rv_dexp: Lfield ";
Sil.d_exp e1; Sil.d_exp e1;
L.d_str (" " ^ Fieldname.to_string f); L.d_str (" " ^ Typ.Fieldname.to_string f);
L.d_ln () L.d_ln ()
end; end;
(match _exp_rv_dexp tenv seen node e1 with (match _exp_rv_dexp tenv seen node e1 with
@ -587,7 +587,7 @@ let vpath_find tenv prop _exp : DExp.t option * Typ.t option =
| Exp.Sizeof {typ={Typ.desc=Tstruct name}} -> ( | Exp.Sizeof {typ={Typ.desc=Tstruct name}} -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some {fields} -> | Some {fields} ->
List.find ~f:(fun (f', _, _) -> Fieldname.equal f' f) fields |> List.find ~f:(fun (f', _, _) -> Typ.Fieldname.equal f' f) fields |>
Option.map ~f:snd3 Option.map ~f:snd3
| _ -> | _ ->
None None
@ -684,10 +684,10 @@ let explain_dexp_access prop dexp is_nullable =
| [] -> | [] ->
if verbose if verbose
then then
(L.d_strln ("lookup_fld: can't find field " ^ Fieldname.to_string f)); (L.d_strln ("lookup_fld: can't find field " ^ Typ.Fieldname.to_string f));
None None
| (f1, se):: fsel' -> | (f1, se):: fsel' ->
if Fieldname.equal f1 f then Some se if Typ.Fieldname.equal f1 f then Some se
else lookup_fld fsel' f in else lookup_fld fsel' f in
let rec lookup_esel esel e = match esel with let rec lookup_esel esel e = match esel with
| [] -> | [] ->
@ -958,7 +958,7 @@ type pvar_off =
| Fpvar | Fpvar
(* value obtained by dereferencing the pvar and following a sequence of fields *) (* value obtained by dereferencing the pvar and following a sequence of fields *)
| Fstruct of Fieldname.t list | Fstruct of Typ.Fieldname.t list
let dexp_apply_pvar_off dexp pvar_off = let dexp_apply_pvar_off dexp pvar_off =
let rec add_ddot de = function let rec add_ddot de = function

@ -42,8 +42,8 @@ val find_boolean_assignment : Procdesc.Node.t -> Pvar.t -> bool -> Procdesc.Node
val exp_rv_dexp : Tenv.t -> Procdesc.Node.t -> Exp.t -> DecompiledExp.t option val exp_rv_dexp : Tenv.t -> Procdesc.Node.t -> Exp.t -> DecompiledExp.t option
(** Produce a description of a persistent reference to an Android Context *) (** Produce a description of a persistent reference to an Android Context *)
val explain_context_leak : Typ.Procname.t -> Typ.t -> Fieldname.t -> val explain_context_leak : Typ.Procname.t -> Typ.t -> Typ.Fieldname.t ->
(Fieldname.t option * Typ.t) list -> Localise.error_desc (Typ.Fieldname.t option * Typ.t) list -> Localise.error_desc
(** Produce a description of a mismatch between an allocation function and a deallocation function *) (** Produce a description of a mismatch between an allocation function and a deallocation function *)
val explain_allocation_mismatch : val explain_allocation_mismatch :
@ -105,7 +105,7 @@ val explain_return_statement_missing : Location.t -> Localise.error_desc
(** explain a retain cycle *) (** explain a retain cycle *)
val explain_retain_cycle : val explain_retain_cycle :
((Sil.strexp * Typ.t) * Fieldname.t * Sil.strexp) list -> ((Sil.strexp * Typ.t) * Typ.Fieldname.t * Sil.strexp) list ->
Location.t -> string option -> Localise.error_desc Location.t -> string option -> Localise.error_desc
(** explain unary minus applied to unsigned expression *) (** explain unary minus applied to unsigned expression *)
@ -138,7 +138,7 @@ val warning_err : Location.t -> ('a, Format.formatter, unit) format -> 'a
(* offset of an expression found following a program variable *) (* offset of an expression found following a program variable *)
type pvar_off = type pvar_off =
| Fpvar (* value of a pvar *) | Fpvar (* value of a pvar *)
| Fstruct of Fieldname.t list (* value obtained by dereferencing the pvar and following a sequence of fields *) | Fstruct of Typ.Fieldname.t list (* value obtained by dereferencing the pvar and following a sequence of fields *)
(** Find a program variable whose value is [exp] or pointing to a struct containing [exp] *) (** Find a program variable whose value is [exp] or pointing to a struct containing [exp] *)
val find_with_exp : 'a Prop.t -> Exp.t -> (Pvar.t * pvar_off) option val find_with_exp : 'a Prop.t -> Exp.t -> (Pvar.t * pvar_off) option

@ -74,7 +74,7 @@ let rec exp_match e1 sub vars e2 : (Sil.subst * Ident.t list) option =
check_equal sub vars e1 e2 check_equal sub vars e1 e2
| Exp.Lvar _, _ | _, Exp.Lvar _ -> | Exp.Lvar _, _ | _, Exp.Lvar _ ->
check_equal sub vars e1 e2 check_equal sub vars e1 e2
| Exp.Lfield(e1', fld1, _), Exp.Lfield(e2', fld2, _) when (Fieldname.equal fld1 fld2) -> | Exp.Lfield(e1', fld1, _), Exp.Lfield(e2', fld2, _) when (Typ.Fieldname.equal fld1 fld2) ->
exp_match e1' sub vars e2' exp_match e1' sub vars e2'
| Exp.Lfield _, _ | _, Exp.Lfield _ -> | Exp.Lfield _, _ | _, Exp.Lfield _ ->
None None
@ -121,7 +121,7 @@ and fsel_match fsel1 sub vars fsel2 =
if (Config.abs_struct <= 0) then None if (Config.abs_struct <= 0) then None
else Some (sub, vars) (* This can lead to great information loss *) else Some (sub, vars) (* This can lead to great information loss *)
| (fld1, se1') :: fsel1', (fld2, se2') :: fsel2' -> | (fld1, se1') :: fsel1', (fld2, se2') :: fsel2' ->
let n = Fieldname.compare fld1 fld2 in let n = Typ.Fieldname.compare fld1 fld2 in
if Int.equal n 0 then begin if Int.equal n 0 then begin
match strexp_match se1' sub vars se2' with match strexp_match se1' sub vars se2' with
| None -> None | None -> None
@ -514,7 +514,7 @@ and generate_todos_from_fel mode todos fel1 fel2 =
| _, [] -> | _, [] ->
if equal_iso_mode mode LFieldForget then Some todos else None if equal_iso_mode mode LFieldForget then Some todos else None
| (fld1, strexp1) :: fel1', (fld2, strexp2) :: fel2' -> | (fld1, strexp1) :: fel1', (fld2, strexp2) :: fel2' ->
let n = Fieldname.compare fld1 fld2 in let n = Typ.Fieldname.compare fld1 fld2 in
if Int.equal n 0 then if Int.equal n 0 then
begin begin
match generate_todos_from_strexp mode todos strexp1 strexp2 with match generate_todos_from_strexp mode todos strexp1 strexp2 with

@ -1253,7 +1253,7 @@ module Normalize = struct
(* n1-e1 == n2 -> e1==n1-n2 *) (* n1-e1 == n2 -> e1==n1-n2 *)
(e1, Exp.int (n1 -- n2)) (e1, Exp.int (n1 -- n2))
| Lfield (e1', fld1, _), Lfield (e2', fld2, _) -> | Lfield (e1', fld1, _), Lfield (e2', fld2, _) ->
if Fieldname.equal fld1 fld2 if Typ.Fieldname.equal fld1 fld2
then normalize_eq (e1', e2') then normalize_eq (e1', e2')
else eq else eq
| Lindex (e1', idx1), Lindex (e2', idx2) -> | Lindex (e1', idx1), Lindex (e2', idx2) ->
@ -1321,7 +1321,7 @@ module Normalize = struct
let fld_cnts' = let fld_cnts' =
List.map ~f:(fun (fld, cnt) -> List.map ~f:(fun (fld, cnt) ->
fld, strexp_normalize tenv sub cnt) fld_cnts in fld, strexp_normalize tenv sub cnt) fld_cnts in
let fld_cnts'' = List.sort ~cmp:[%compare: Fieldname.t * Sil.strexp] fld_cnts' in let fld_cnts'' = List.sort ~cmp:[%compare: Typ.Fieldname.t * Sil.strexp] fld_cnts' in
Estruct (fld_cnts'', inst) Estruct (fld_cnts'', inst)
end end
| Earray (len, idx_cnts, inst) -> | Earray (len, idx_cnts, inst) ->
@ -2452,7 +2452,7 @@ let rec strexp_gc_fields (fav: Sil.fav) (se : Sil.strexp) =
let fsel' = let fsel' =
let fselo' = List.filter ~f:(function | (_, Some _) -> true | _ -> false) fselo in let fselo' = List.filter ~f:(function | (_, Some _) -> true | _ -> false) fselo in
List.map ~f:(function (f, seo) -> (f, unSome seo)) fselo' in List.map ~f:(function (f, seo) -> (f, unSome seo)) fselo' in
if [%compare.equal: (Fieldname.t * Sil.strexp) list] fsel fsel' then Some se if [%compare.equal: (Typ.Fieldname.t * Sil.strexp) list] fsel fsel' then Some se
else Some (Sil.Estruct (fsel', inst)) else Some (Sil.Estruct (fsel', inst))
| Earray _ -> | Earray _ ->
Some se Some se

@ -143,7 +143,7 @@ let rec compute_sexp_diff (se1: Sil.strexp) (se2: Sil.strexp) : Obj.t list = mat
and compute_fsel_diff fsel1 fsel2 : Obj.t list = match fsel1, fsel2 with and compute_fsel_diff fsel1 fsel2 : Obj.t list = match fsel1, fsel2 with
| ((f1, se1):: fsel1'), (((f2, se2) as x):: fsel2') -> | ((f1, se1):: fsel1'), (((f2, se2) as x):: fsel2') ->
(match Fieldname.compare f1 f2 with (match Typ.Fieldname.compare f1 f2 with
| n when n < 0 -> compute_fsel_diff fsel1' fsel2 | n when n < 0 -> compute_fsel_diff fsel1' fsel2
| 0 -> compute_sexp_diff se1 se2 @ compute_fsel_diff fsel1' fsel2' | 0 -> compute_sexp_diff se1 se2 @ compute_fsel_diff fsel1' fsel2'
| _ -> (Obj.repr x) :: compute_fsel_diff fsel1 fsel2') | _ -> (Obj.repr x) :: compute_fsel_diff fsel1 fsel2')

@ -1242,7 +1242,7 @@ let exp_imply tenv calc_missing subs e1_in e2_in : subst2 =
raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2)))) raise (IMPL_EXC ("expressions not equal", subs, (EXC_FALSE_EXPS (e1, e2))))
| e1, Exp.Const _ -> | e1, Exp.Const _ ->
raise (IMPL_EXC ("lhs not constant", subs, (EXC_FALSE_EXPS (e1, e2)))) raise (IMPL_EXC ("lhs not constant", subs, (EXC_FALSE_EXPS (e1, e2))))
| Exp.Lfield(e1, fd1, _), Exp.Lfield(e2, fd2, _) when Fieldname.equal fd1 fd2 -> | Exp.Lfield(e1, fd1, _), Exp.Lfield(e2, fd2, _) when Typ.Fieldname.equal fd1 fd2 ->
do_imply subs e1 e2 do_imply subs e1 e2
| Exp.Lindex(e1, f1), Exp.Lindex(e2, f2) -> | Exp.Lindex(e1, f1), Exp.Lindex(e2, f2) ->
do_imply (do_imply subs e1 e2) f1 f2 do_imply (do_imply subs e1 e2) f1 f2
@ -1263,7 +1263,7 @@ let path_to_id path =
| Exp.Lfield (e, fld, _) -> | Exp.Lfield (e, fld, _) ->
(match f e with (match f e with
| None -> None | None -> None
| Some s -> Some (s ^ "_" ^ (Fieldname.to_string fld))) | Some s -> Some (s ^ "_" ^ (Typ.Fieldname.to_string fld)))
| Exp.Lindex (e, ind) -> | Exp.Lindex (e, ind) ->
(match f e with (match f e with
| None -> None | None -> None
@ -1360,13 +1360,13 @@ let rec sexp_imply tenv source calc_index_frame calc_missing subs se1 se2 typ2 :
d_impl_err ("sexp_imply not implemented", subs, (EXC_FALSE_SEXPS (se1, se2))); d_impl_err ("sexp_imply not implemented", subs, (EXC_FALSE_SEXPS (se1, se2)));
raise (Exceptions.Abduction_case_not_implemented __POS__) raise (Exceptions.Abduction_case_not_implemented __POS__)
and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Fieldname.t * Sil.strexp) list) * ((Fieldname.t * Sil.strexp) list) = and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 : subst2 * ((Typ.Fieldname.t * Sil.strexp) list) * ((Typ.Fieldname.t * Sil.strexp) list) =
let lookup = Tenv.lookup tenv in let lookup = Tenv.lookup tenv in
match fsel1, fsel2 with match fsel1, fsel2 with
| _, [] -> subs, fsel1, [] | _, [] -> subs, fsel1, []
| (f1, se1) :: fsel1', (f2, se2) :: fsel2' -> | (f1, se1) :: fsel1', (f2, se2) :: fsel2' ->
begin begin
match Fieldname.compare f1 f2 with match Typ.Fieldname.compare f1 f2 with
| 0 -> | 0 ->
let typ' = Typ.Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f2 typ2 in let typ' = Typ.Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f2 typ2 in
let subs', se_frame, se_missing = let subs', se_frame, se_missing =
@ -1997,7 +1997,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
(Exp.int len, [(index, Sil.Eexp (Exp.zero, Sil.inst_none))], Sil.inst_none) (Exp.int len, [(index, Sil.Eexp (Exp.zero, Sil.inst_none))], Sil.inst_none)
| Config.Java -> | Config.Java ->
let mk_fld_sexp s = let mk_fld_sexp s =
let fld = Fieldname.Java.from_string s in let fld = Typ.Fieldname.Java.from_string s in
let se = Sil.Eexp (Exp.Var (Ident.create_fresh Ident.kprimed), Sil.Inone) in let se = Sil.Eexp (Exp.Var (Ident.create_fresh Ident.kprimed), Sil.Inone) in
(fld, se) in (fld, se) in
let fields = ["java.lang.String.count"; "java.lang.String.hash"; let fields = ["java.lang.String.count"; "java.lang.String.hash";
@ -2018,7 +2018,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : (subst2 *
let root = Exp.Const (Const.Cclass (Ident.string_to_name s)) in let root = Exp.Const (Const.Cclass (Ident.string_to_name s)) in
let sexp = (* TODO: add appropriate fields *) let sexp = (* TODO: add appropriate fields *)
Sil.Estruct Sil.Estruct
([(Fieldname.Java.from_string "java.lang.Class.name", ([(Typ.Fieldname.Java.from_string "java.lang.Class.name",
Sil.Eexp ((Exp.Const (Const.Cstr s), Sil.Inone)))], Sil.inst_none) in Sil.Eexp ((Exp.Const (Const.Cstr s), Sil.Inone)))], Sil.inst_none) in
let class_texp = let class_texp =
let class_type = Typ.Name.Java.from_string "java.lang.Class" in let class_type = Typ.Name.Java.from_string "java.lang.Class" in

@ -107,7 +107,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some ({ fields; statics; } as struct_typ) -> ( | Some ({ fields; statics; } as struct_typ) -> (
match List.find match List.find
~f:(fun (f', _, _) -> Fieldname.equal f f') ~f:(fun (f', _, _) -> Typ.Fieldname.equal f f')
(fields @ statics) with (fields @ statics) with
| Some (_, t', _) -> | Some (_, t', _) ->
let atoms', se', res_t' = let atoms', se', res_t' =
@ -115,7 +115,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
pname tenv orig_prop footprint_part kind max_stamp t' off' inst in pname tenv orig_prop footprint_part kind max_stamp t' off' inst in
let se = Sil.Estruct ([(f, se')], inst) in let se = Sil.Estruct ([(f, se')], inst) in
let replace_typ_of_f (f', t', a') = let replace_typ_of_f (f', t', a') =
if Fieldname.equal f f' then (f, res_t', a') else (f', t', a') in if Typ.Fieldname.equal f f' then (f, res_t', a') else (f', t', a') in
let fields' = let fields' =
List.sort ~cmp:Typ.Struct.compare_field (List.map ~f:replace_typ_of_f fields) in List.sort ~cmp:Typ.Struct.compare_field (List.map ~f:replace_typ_of_f fields) in
ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ; ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ;
@ -209,22 +209,22 @@ let rec _strexp_extend_values
| (Off_fld (f, _)) :: off', Sil.Estruct (fsel, inst'), Tstruct name -> ( | (Off_fld (f, _)) :: off', Sil.Estruct (fsel, inst'), Tstruct name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some ({ fields; statics; } as struct_typ) -> ( | Some ({ fields; statics; } as struct_typ) -> (
match List.find ~f:(fun (f', _, _) -> Fieldname.equal f f') (fields @ statics) with match List.find ~f:(fun (f', _, _) -> Typ.Fieldname.equal f f') (fields @ statics) with
| Some (_, typ', _) -> ( | Some (_, typ', _) -> (
match List.find ~f:(fun (f', _) -> Fieldname.equal f f') fsel with match List.find ~f:(fun (f', _) -> Typ.Fieldname.equal f f') fsel with
| Some (_, se') -> | Some (_, se') ->
let atoms_se_typ_list' = let atoms_se_typ_list' =
_strexp_extend_values _strexp_extend_values
pname tenv orig_prop footprint_part kind max_stamp se' typ' off' inst in 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 acc (res_atoms', res_se', res_typ') =
let replace_fse ((f1, _) as ft1) = let replace_fse ((f1, _) as ft1) =
if Fieldname.equal f1 f then (f1, res_se') else ft1 in if Typ.Fieldname.equal f1 f then (f1, res_se') else ft1 in
let res_fsel' = let res_fsel' =
List.sort List.sort
~cmp:[%compare: Fieldname.t * Sil.strexp] ~cmp:[%compare: Typ.Fieldname.t * Sil.strexp]
(List.map ~f:replace_fse fsel) in (List.map ~f:replace_fse fsel) in
let replace_fta ((f1, _, a1) as fta1) = let replace_fta ((f1, _, a1) as fta1) =
if Fieldname.equal f f1 then (f1, res_typ', a1) else fta1 in if Typ.Fieldname.equal f f1 then (f1, res_typ', a1) else fta1 in
let fields' = let fields' =
List.sort ~cmp:Typ.Struct.compare_field (List.map ~f:replace_fta fields) in List.sort ~cmp:Typ.Struct.compare_field (List.map ~f:replace_fta fields) in
ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ; ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ;
@ -235,9 +235,9 @@ let rec _strexp_extend_values
create_struct_values create_struct_values
pname tenv orig_prop footprint_part kind max_stamp typ' off' inst in pname tenv orig_prop footprint_part kind max_stamp typ' off' inst in
let res_fsel' = let res_fsel' =
List.sort ~cmp:[%compare: Fieldname.t * Sil.strexp] ((f, se'):: fsel) in List.sort ~cmp:[%compare: Typ.Fieldname.t * Sil.strexp] ((f, se'):: fsel) in
let replace_fta (f', t', a') = let replace_fta (f', t', a') =
if Fieldname.equal f' f then (f, res_typ', a') else (f', t', a') in if Typ.Fieldname.equal f' f then (f, res_typ', a') else (f', t', a') in
let fields' = let fields' =
List.sort ~cmp:Typ.Struct.compare_field (List.map ~f:replace_fta fields) in List.sort ~cmp:Typ.Struct.compare_field (List.map ~f:replace_fta fields) in
ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ; ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ;
@ -482,7 +482,7 @@ let prop_iter_check_fields_ptsto_shallow tenv iter lexp =
| (Sil.Off_fld (fld, _)):: off' -> | (Sil.Off_fld (fld, _)):: off' ->
(match se with (match se with
| Sil.Estruct (fsel, _) -> | Sil.Estruct (fsel, _) ->
(match List.find ~f:(fun (fld', _) -> Fieldname.equal fld fld') fsel with (match List.find ~f:(fun (fld', _) -> Typ.Fieldname.equal fld fld') fsel with
| Some (_, se') -> | Some (_, se') ->
check_offset se' off' check_offset se' off'
| None -> Some fld) | None -> Some fld)
@ -716,7 +716,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
match extract_guarded_by_str item_annot with match extract_guarded_by_str item_annot with
| Some "this" -> | Some "this" ->
(* expand "this" into <classname>.this *) (* expand "this" into <classname>.this *)
Some (Printf.sprintf "%s.this" (Fieldname.java_get_class fld)) Some (Printf.sprintf "%s.this" (Typ.Fieldname.java_get_class fld))
| guarded_by_str_opt -> | guarded_by_str_opt ->
guarded_by_str_opt guarded_by_str_opt
end end
@ -727,8 +727,8 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
let is_guarded_by_fld guarded_by_str fld _ = let is_guarded_by_fld guarded_by_str fld _ =
(* this comparison needs to be somewhat fuzzy, since programmers are free to write (* this comparison needs to be somewhat fuzzy, since programmers are free to write
@GuardedBy("mLock"), @GuardedBy("MyClass.mLock"), or use other conventions *) @GuardedBy("mLock"), @GuardedBy("MyClass.mLock"), or use other conventions *)
String.equal (Fieldname.to_flat_string fld) guarded_by_str || String.equal (Typ.Fieldname.to_flat_string fld) guarded_by_str ||
String.equal (Fieldname.to_string fld) guarded_by_str in String.equal (Typ.Fieldname.to_string fld) guarded_by_str in
let get_fld_strexp_and_typ typ f flds = let get_fld_strexp_and_typ typ f flds =
let match_one (fld, strexp) = let match_one (fld, strexp) =
@ -784,7 +784,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
nothing we can do to disambiguate them. *) nothing we can do to disambiguate them. *)
get_fld_strexp_and_typ get_fld_strexp_and_typ
typ typ
(fun f _ -> Fieldname.java_is_outer_instance f) (fun f _ -> Typ.Fieldname.java_is_outer_instance f)
flds flds
| None -> | None ->
(* can't find an exact match. try a different convention. *) (* can't find an exact match. try a different convention. *)
@ -841,7 +841,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
(Attribute.get_for_exp tenv prop guarded_by_exp) in (Attribute.get_for_exp tenv prop guarded_by_exp) in
let guardedby_is_self_referential = let guardedby_is_self_referential =
String.equal "itself" (String.lowercase guarded_by_str) || String.equal "itself" (String.lowercase guarded_by_str) ||
String.is_suffix ~suffix:guarded_by_str (Fieldname.to_string accessed_fld) in String.is_suffix ~suffix:guarded_by_str (Typ.Fieldname.to_string accessed_fld) in
let proc_has_suppress_guarded_by_annot pdesc = let proc_has_suppress_guarded_by_annot pdesc =
match extract_suppress_warnings_str (Annotations.pdesc_get_return_annot pdesc) with match extract_suppress_warnings_str (Annotations.pdesc_get_return_annot pdesc) with
| Some suppression_str-> | Some suppression_str->
@ -861,7 +861,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
List.exists List.exists
~f:(fun (fld, strexp) -> match strexp with ~f:(fun (fld, strexp) -> match strexp with
| Sil.Eexp (rhs_exp, _) -> | Sil.Eexp (rhs_exp, _) ->
Exp.equal exp rhs_exp && not (Fieldname.equal fld accessed_fld) Exp.equal exp rhs_exp && not (Typ.Fieldname.equal fld accessed_fld)
| _ -> | _ ->
false) false)
flds flds
@ -1140,7 +1140,7 @@ let type_at_offset tenv texp off =
| (Off_fld (f, _)) :: off', Tstruct name -> ( | (Off_fld (f, _)) :: off', Tstruct name -> (
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields } -> ( | Some { fields } -> (
match List.find ~f:(fun (f', _, _) -> Fieldname.equal f f') fields with match List.find ~f:(fun (f', _, _) -> Typ.Fieldname.equal f f') fields with
| Some (_, typ', _) -> strip_offset off' typ' | Some (_, typ', _) -> strip_offset off' typ'
| None -> None | None -> None
) )
@ -1195,7 +1195,7 @@ let rec iter_rearrange
(* access through field: get the struct type from the field *) (* access through field: get the struct type from the field *)
if Config.trace_rearrange then begin if Config.trace_rearrange then begin
L.d_increase_indent 1; L.d_increase_indent 1;
L.d_str "iter_rearrange: root of lexp accesses field "; L.d_strln (Fieldname.to_string f); L.d_str "iter_rearrange: root of lexp accesses field "; L.d_strln (Typ.Fieldname.to_string f);
L.d_str " struct type from field: "; Typ.d_full fld_typ; L.d_ln(); L.d_str " struct type from field: "; Typ.d_full fld_typ; L.d_ln();
L.d_decrease_indent 1; L.d_decrease_indent 1;
L.d_ln(); L.d_ln();
@ -1324,7 +1324,7 @@ let is_strexp_pt_fld_with_annot tenv obj_str is_annotation typ deref_exp (fld,
| Sil.Eexp (Exp.Var _ as exp, _) when Exp.equal exp deref_exp -> | Sil.Eexp (Exp.Var _ as exp, _) when Exp.equal exp deref_exp ->
let has_annot = fld_has_annot fld in let has_annot = fld_has_annot fld in
if has_annot then if has_annot then
obj_str := Some (Fieldname.to_simplified_string fld); obj_str := Some (Typ.Fieldname.to_simplified_string fld);
has_annot has_annot
| _ -> true | _ -> true

@ -18,7 +18,7 @@ module F = Format
let rec fldlist_assoc fld = function let rec fldlist_assoc fld = function
| [] -> raise Not_found | [] -> raise Not_found
| (fld', x, _):: l -> if Fieldname.equal fld fld' then x else fldlist_assoc fld l | (fld', x, _):: l -> if Typ.Fieldname.equal fld fld' then x else fldlist_assoc fld l
let unroll_type tenv (typ: Typ.t) (off: Sil.offset) = let unroll_type tenv (typ: Typ.t) (off: Sil.offset) =
let fail fld_to_string fld = let fail fld_to_string fld =
@ -32,10 +32,10 @@ let unroll_type tenv (typ: Typ.t) (off: Sil.offset) =
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some { fields; statics } -> ( | Some { fields; statics } -> (
try fldlist_assoc fld (fields @ statics) try fldlist_assoc fld (fields @ statics)
with Not_found -> fail Fieldname.to_string fld with Not_found -> fail Typ.Fieldname.to_string fld
) )
| None -> | None ->
fail Fieldname.to_string fld fail Typ.Fieldname.to_string fld
) )
| Tarray (typ', _, _), Off_index _ -> | Tarray (typ', _, _), Off_index _ ->
typ' typ'
@ -102,7 +102,7 @@ let rec apply_offlist
let is_hidden_field () = let is_hidden_field () =
match State.get_instr () with match State.get_instr () with
| Some (Sil.Load (_, Exp.Lfield (_, fieldname, _), _, _)) -> | Some (Sil.Load (_, Exp.Lfield (_, fieldname, _), _, _)) ->
Fieldname.is_hidden fieldname Typ.Fieldname.is_hidden fieldname
| _ -> false in | _ -> false in
let inst_new = match inst with let inst_new = match inst with
| Sil.Ilookup when inst_is_uninitialized inst_curr && not (is_hidden_field()) -> | Sil.Ilookup when inst_is_uninitialized inst_curr && not (is_hidden_field()) ->
@ -142,17 +142,17 @@ let rec apply_offlist
match Tenv.lookup tenv name with match Tenv.lookup tenv name with
| Some ({fields} as struct_typ) -> ( | Some ({fields} as struct_typ) -> (
let t' = unroll_type tenv typ (Sil.Off_fld (fld, fld_typ)) in let t' = unroll_type tenv typ (Sil.Off_fld (fld, fld_typ)) in
match List.find ~f:(fun fse -> Fieldname.equal fld (fst fse)) fsel with match List.find ~f:(fun fse -> Typ.Fieldname.equal fld (fst fse)) fsel with
| Some (_, se') -> | Some (_, se') ->
let res_e', res_se', res_t', res_pred_insts_op' = let res_e', res_se', res_t', res_pred_insts_op' =
apply_offlist apply_offlist
pdesc tenv p fp_root nullify_struct pdesc tenv p fp_root nullify_struct
(root_lexp, se', t') offlist' f inst lookup_inst in (root_lexp, se', t') offlist' f inst lookup_inst in
let replace_fse fse = let replace_fse fse =
if Fieldname.equal fld (fst fse) then (fld, res_se') else fse in if Typ.Fieldname.equal fld (fst fse) then (fld, res_se') else fse in
let res_se = Sil.Estruct (List.map ~f:replace_fse fsel, inst') in let res_se = Sil.Estruct (List.map ~f:replace_fse fsel, inst') in
let replace_fta (f, t, a) = let replace_fta (f, t, a) =
if Fieldname.equal fld f then (fld, res_t', a) else (f, t, a) in if Typ.Fieldname.equal fld f then (fld, res_t', a) else (f, t, a) in
let fields' = List.map ~f:replace_fta fields in let fields' = List.map ~f:replace_fta fields in
ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ; ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:fields' name) ;
(res_e', res_se, typ, res_pred_insts_op') (res_e', res_se, typ, res_pred_insts_op')
@ -1528,7 +1528,7 @@ and check_variadic_sentinel_if_present
and sym_exec_objc_getter field_name ret_typ tenv ret_id pdesc pname loc args prop = and sym_exec_objc_getter field_name ret_typ tenv ret_id pdesc pname loc args prop =
L.d_strln ("No custom getter found. Executing the ObjC builtin getter with ivar "^ L.d_strln ("No custom getter found. Executing the ObjC builtin getter with ivar "^
(Fieldname.to_string field_name)^"."); (Typ.Fieldname.to_string field_name)^".");
let ret_id = let ret_id =
match ret_id with match ret_id with
| Some (ret_id, _) -> ret_id | Some (ret_id, _) -> ret_id
@ -1542,7 +1542,7 @@ and sym_exec_objc_getter field_name ret_typ tenv ret_id pdesc pname loc args pro
and sym_exec_objc_setter field_name _ tenv _ pdesc pname loc args prop = 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 "^ L.d_strln ("No custom setter found. Executing the ObjC builtin setter with ivar "^
(Fieldname.to_string field_name)^"."); (Typ.Fieldname.to_string field_name)^".");
match args with match args with
| (lexp1, ({Typ.desc=Tstruct _} as typ1 | {Typ.desc=Tptr (typ1, _)})) :: (lexp2, typ2) :: _ -> | (lexp1, ({Typ.desc=Tstruct _} as typ1 | {Typ.desc=Tptr (typ1, _)})) :: (lexp2, typ2) :: _ ->
let field_access_exp = Exp.Lfield (lexp1, field_name, typ1) in let field_access_exp = Exp.Lfield (lexp1, field_name, typ1) in

@ -424,7 +424,7 @@ let rec fsel_star_fld fsel1 fsel2 = match fsel1, fsel2 with
| [], fsel2 -> fsel2 | [], fsel2 -> fsel2
| fsel1,[] -> fsel1 | fsel1,[] -> fsel1
| (f1, se1):: fsel1', (f2, se2):: fsel2' -> | (f1, se1):: fsel1', (f2, se2):: fsel2' ->
(match Fieldname.compare f1 f2 with (match Typ.Fieldname.compare f1 f2 with
| 0 -> (f1, sexp_star_fld se1 se2) :: fsel_star_fld fsel1' fsel2' | 0 -> (f1, sexp_star_fld se1 se2) :: fsel_star_fld fsel1' fsel2'
| n when n < 0 -> (f1, se1) :: fsel_star_fld fsel1' fsel2 | n when n < 0 -> (f1, se1) :: fsel_star_fld fsel1' fsel2
| _ -> (f2, se2) :: fsel_star_fld fsel1 fsel2') | _ -> (f2, se2) :: fsel_star_fld fsel1 fsel2')
@ -467,7 +467,7 @@ let texp_star tenv texp1 texp2 =
| [], _ -> true | [], _ -> true
| _, [] -> false | _, [] -> false
| (f1, _, _):: ftal1', (f2, _, _):: ftal2' -> | (f1, _, _):: ftal1', (f2, _, _):: ftal2' ->
begin match Fieldname.compare f1 f2 with begin match Typ.Fieldname.compare f1 f2 with
| n when n < 0 -> false | n when n < 0 -> false
| 0 -> ftal_sub ftal1' ftal2' | 0 -> ftal_sub ftal1' ftal2'
| _ -> ftal_sub ftal1 ftal2' end in | _ -> ftal_sub ftal1 ftal2' end in
@ -1086,7 +1086,7 @@ let exe_spec
let split = do_split () in let split = do_split () in
(* check if a missing_fld hpred is about a hidden field *) (* check if a missing_fld hpred is about a hidden field *)
let hpred_missing_hidden = function let hpred_missing_hidden = function
| Sil.Hpointsto (_, Sil.Estruct ([(fld, _)], _), _) -> Fieldname.is_hidden fld | Sil.Hpointsto (_, Sil.Estruct ([(fld, _)], _), _) -> Typ.Fieldname.is_hidden fld
| _ -> false in | _ -> false in
(* missing fields minus hidden fields *) (* missing fields minus hidden fields *)
let missing_fld_nohidden = let missing_fld_nohidden =

@ -352,7 +352,7 @@ let tainted_params callee_pname =
let has_taint_annotation fieldname (struct_typ: Typ.Struct.t) = let has_taint_annotation fieldname (struct_typ: Typ.Struct.t) =
let fld_has_taint_annot (fname, _, annot) = let fld_has_taint_annot (fname, _, annot) =
Fieldname.equal fieldname fname && Typ.Fieldname.equal fieldname fname &&
(Annotations.ia_is_privacy_source annot || Annotations.ia_is_integrity_source annot) in (Annotations.ia_is_privacy_source annot || Annotations.ia_is_integrity_source annot) in
List.exists ~f:fld_has_taint_annot struct_typ.fields || List.exists ~f:fld_has_taint_annot struct_typ.fields ||
List.exists ~f:fld_has_taint_annot struct_typ.statics List.exists ~f:fld_has_taint_annot struct_typ.statics

@ -21,7 +21,7 @@ val accepts_sensitive_params :
val tainted_params : Typ.Procname.t -> (int * PredSymb.taint_kind) list val tainted_params : Typ.Procname.t -> (int * PredSymb.taint_kind) list
(** returns the taint_kind of [fieldname] if it has a taint source annotation *) (** returns the taint_kind of [fieldname] if it has a taint source annotation *)
val has_taint_annotation : Fieldname.t -> Typ.Struct.t -> bool val has_taint_annotation : Typ.Fieldname.t -> Typ.Struct.t -> bool
val add_tainting_attribute : Tenv.t -> PredSymb.t -> Pvar.t -> Prop.normal Prop.t -> Prop.normal Prop.t val add_tainting_attribute : Tenv.t -> PredSymb.t -> Pvar.t -> Prop.normal Prop.t -> Prop.normal Prop.t

@ -27,7 +27,7 @@ struct
type t = type t =
| Var of Var.t | Var of Var.t
| Allocsite of Allocsite.t | Allocsite of Allocsite.t
| Field of t * Fieldname.t | Field of t * Typ.Fieldname.t
[@@deriving compare] [@@deriving compare]
let unknown = Allocsite Allocsite.unknown let unknown = Allocsite Allocsite.unknown
@ -39,7 +39,7 @@ struct
F.fprintf fmt "%s" (String.sub s ~pos:1 ~len:(String.length s - 1)) F.fprintf fmt "%s" (String.sub s ~pos:1 ~len:(String.length s - 1))
else F.fprintf fmt "%s" s else F.fprintf fmt "%s" s
| Allocsite a -> Allocsite.pp fmt a | Allocsite a -> Allocsite.pp fmt a
| Field (l, f) -> F.fprintf fmt "%a.%a" pp l Fieldname.pp f | Field (l, f) -> F.fprintf fmt "%a.%a" pp l Typ.Fieldname.pp f
let is_var = function Var _ -> true | _ -> false let is_var = function Var _ -> true | _ -> false
let is_logical_var = function let is_logical_var = function
| Var (Var.LogicalVar _) -> true | Var (Var.LogicalVar _) -> true

@ -74,7 +74,7 @@ struct
| Exp.Lvar x1, Exp.Lvar x2 -> | Exp.Lvar x1, Exp.Lvar x2 ->
Pvar.equal x1 x2 Pvar.equal x1 x2
| Exp.Lfield (e1, fld1, _), Exp.Lfield (e2, fld2, _) -> | Exp.Lfield (e1, fld1, _), Exp.Lfield (e2, fld2, _) ->
must_alias e1 e2 m && Fieldname.equal fld1 fld2 must_alias e1 e2 m && Typ.Fieldname.equal fld1 fld2
| Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) -> | Exp.Lindex (e11, e12), Exp.Lindex (e21, e22) ->
must_alias e11 e21 m && must_alias e12 e22 m must_alias e11 e21 m && must_alias e12 e22 m
| Exp.Sizeof {nbytes=Some nbytes1}, Exp.Sizeof {nbytes=Some nbytes2} -> | Exp.Sizeof {nbytes=Some nbytes1}, Exp.Sizeof {nbytes=Some nbytes2} ->

@ -16,10 +16,10 @@ module L = Logging
module FieldsAssignedInConstructors = module FieldsAssignedInConstructors =
AbstractDomain.FiniteSet(struct AbstractDomain.FiniteSet(struct
type t = Fieldname.t * Typ.t [@@deriving compare] type t = Typ.Fieldname.t * Typ.t [@@deriving compare]
let pp fmt (fieldname, typ) = let pp fmt (fieldname, typ) =
F.fprintf fmt "(%a, %a)" Fieldname.pp fieldname (Typ.pp_full Pp.text) typ F.fprintf fmt "(%a, %a)" Typ.Fieldname.pp fieldname (Typ.pp_full Pp.text) typ
end) end)
module TransferFunctions (CFG : ProcCfg.S) = struct module TransferFunctions (CFG : ProcCfg.S) = struct
@ -69,7 +69,7 @@ let add_annot annot annot_name =
({ Annot.class_name = annot_name; parameters = []; }, true) :: annot ({ Annot.class_name = annot_name; parameters = []; }, true) :: annot
let add_nonnull_to_selected_field given_field ((fieldname, typ, annot) as field) = let add_nonnull_to_selected_field given_field ((fieldname, typ, annot) as field) =
if Fieldname.equal fieldname given_field && if Typ.Fieldname.equal fieldname given_field &&
not (Annotations.ia_is_nullable annot) then not (Annotations.ia_is_nullable annot) then
let new_annot = add_annot annot Annotations.nonnull in let new_annot = add_annot annot Annotations.nonnull in
(fieldname, typ, new_annot) (fieldname, typ, new_annot)

@ -113,7 +113,7 @@ let make_error_trace astate ap ud =
let name_of ap = let name_of ap =
match AccessPath.Raw.get_last_access ap with match AccessPath.Raw.get_last_access ap with
| Some (AccessPath.FieldAccess field_name) -> | Some (AccessPath.FieldAccess field_name) ->
"Field " ^ (Fieldname.to_flat_string field_name) "Field " ^ (Typ.Fieldname.to_flat_string field_name)
| Some (AccessPath.ArrayAccess _) -> | Some (AccessPath.ArrayAccess _) ->
"Some array element" "Some array element"
| None -> | None ->
@ -146,14 +146,14 @@ let pretty_field_name proc_data field_name =
match Procdesc.get_proc_name proc_data.ProcData.pdesc with match Procdesc.get_proc_name proc_data.ProcData.pdesc with
| Typ.Procname.Java jproc_name -> | Typ.Procname.Java jproc_name ->
let proc_class_name = Typ.Procname.java_get_class_name jproc_name in let proc_class_name = Typ.Procname.java_get_class_name jproc_name in
let field_class_name = Fieldname.java_get_class field_name in let field_class_name = Typ.Fieldname.java_get_class field_name in
if String.equal proc_class_name field_class_name then if String.equal proc_class_name field_class_name then
Fieldname.to_flat_string field_name Typ.Fieldname.to_flat_string field_name
else else
Fieldname.to_simplified_string field_name Typ.Fieldname.to_simplified_string field_name
| _ -> | _ ->
(* This format is subject to change once this checker gets to run on C/Cpp/ObjC *) (* This format is subject to change once this checker gets to run on C/Cpp/ObjC *)
Fieldname.to_string field_name Typ.Fieldname.to_string field_name
let checker { Callbacks.summary; proc_desc; tenv; } = let checker { Callbacks.summary; proc_desc; tenv; } =
let report astate (proc_data : extras ProcData.t) = let report astate (proc_data : extras ProcData.t) =

@ -33,13 +33,13 @@ let container_write_string = "infer.dummy.__CONTAINERWRITE__"
let get_container_write_desc sink = let get_container_write_desc sink =
let (base_var, _), access_list = fst (ThreadSafetyDomain.TraceElem.kind sink) in let (base_var, _), access_list = fst (ThreadSafetyDomain.TraceElem.kind sink) in
let get_container_write_desc_ call_name container_name = let get_container_write_desc_ call_name container_name =
match String.chop_prefix (Fieldname.to_string call_name) ~prefix:container_write_string with match String.chop_prefix (Typ.Fieldname.to_string call_name) ~prefix:container_write_string with
| Some call_name -> Some (container_name, call_name) | Some call_name -> Some (container_name, call_name)
| None -> None in | None -> None in
match List.rev access_list with match List.rev access_list with
| FieldAccess call_name :: FieldAccess container_name :: _ -> | FieldAccess call_name :: FieldAccess container_name :: _ ->
get_container_write_desc_ call_name (Fieldname.to_string container_name) get_container_write_desc_ call_name (Typ.Fieldname.to_string container_name)
| [FieldAccess call_name] -> | [FieldAccess call_name] ->
get_container_write_desc_ call_name (F.asprintf "%a" Var.pp base_var) get_container_write_desc_ call_name (F.asprintf "%a" Var.pp base_var)
| _ -> | _ ->
@ -438,7 +438,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| AccessPath.FieldAccess base_field :: | AccessPath.FieldAccess base_field ::
AccessPath.FieldAccess container_field :: _-> AccessPath.FieldAccess container_field :: _->
let base_typename = let base_typename =
Typ.Name.Java.from_string (Fieldname.java_get_class base_field) in Typ.Name.Java.from_string (Typ.Fieldname.java_get_class base_field) in
is_annotated_synchronized base_typename container_field tenv is_annotated_synchronized base_typename container_field tenv
| [AccessPath.FieldAccess container_field] -> | [AccessPath.FieldAccess container_field] ->
begin begin
@ -460,7 +460,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
AccessDomain.empty AccessDomain.empty
else else
let dummy_fieldname = let dummy_fieldname =
Fieldname.Java.from_string Typ.Fieldname.Java.from_string
(container_write_string ^ (Typ.Procname.get_method callee_pname)) in (container_write_string ^ (Typ.Procname.get_method callee_pname)) in
let dummy_access_ap = let dummy_access_ap =
fst receiver_ap, (snd receiver_ap) @ [AccessPath.FieldAccess dummy_fieldname] in fst receiver_ap, (snd receiver_ap) @ [AccessPath.FieldAccess dummy_fieldname] in
@ -1396,7 +1396,7 @@ let may_alias tenv p1 p2 =
| FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _ -> false | FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _ -> false
(* fields in Java contain the class name /declaring/ them (* fields in Java contain the class name /declaring/ them
thus two fields can be aliases *iff* they are equal *) thus two fields can be aliases *iff* they are equal *)
| FieldAccess f1, FieldAccess f2 -> Fieldname.equal f1 f2 | FieldAccess f1, FieldAccess f2 -> Typ.Fieldname.equal f1 f2
(* if arrays of objects that have an inheritance rel then they can alias *) (* if arrays of objects that have an inheritance rel then they can alias *)
| ArrayAccess {desc=Tptr ({desc=Tstruct tn1}, _)}, | ArrayAccess {desc=Tptr ({desc=Tstruct tn1}, _)},
ArrayAccess {desc=Tptr ({desc=Tstruct tn2}, _)} -> ArrayAccess {desc=Tptr ({desc=Tstruct tn2}, _)} ->
@ -1441,7 +1441,7 @@ let should_filter_access (_, path) =
let check_access_step = function let check_access_step = function
| AccessPath.ArrayAccess _ -> false | AccessPath.ArrayAccess _ -> false
| AccessPath.FieldAccess fld -> | AccessPath.FieldAccess fld ->
String.is_substring ~substring:"$SwitchMap" (Fieldname.to_string fld) in String.is_substring ~substring:"$SwitchMap" (Typ.Fieldname.to_string fld) in
List.exists path ~f:check_access_step List.exists path ~f:check_access_step
(* create a map from [abstraction of a memory loc] -> accesses that may touch that memory loc. for (* create a map from [abstraction of a memory loc] -> accesses that may touch that memory loc. for

@ -23,7 +23,7 @@ let equal_base = [%compare.equal : base]
type access = type access =
| ArrayAccess of Typ.t | ArrayAccess of Typ.t
| FieldAccess of Fieldname.t | FieldAccess of Typ.Fieldname.t
[@@deriving compare] [@@deriving compare]
let equal_access = [%compare.equal : access] let equal_access = [%compare.equal : access]
@ -34,7 +34,7 @@ let pp_base fmt (pvar, _) =
Var.pp fmt pvar Var.pp fmt pvar
let pp_access fmt = function let pp_access fmt = function
| FieldAccess field_name -> Fieldname.pp fmt field_name | FieldAccess field_name -> Typ.Fieldname.pp fmt field_name
| ArrayAccess _ -> F.fprintf fmt "[_]" | ArrayAccess _ -> F.fprintf fmt "[_]"
let pp_access_list fmt accesses = let pp_access_list fmt accesses =

@ -15,7 +15,7 @@ type base = Var.t * Typ.t [@@deriving compare]
type access = type access =
| ArrayAccess of Typ.t (* array element type. index is unknown *) | ArrayAccess of Typ.t (* array element type. index is unknown *)
| FieldAccess of Fieldname.t (* field name *) | FieldAccess of Typ.Fieldname.t (* field name *)
[@@deriving compare] [@@deriving compare]
module Raw : sig module Raw : sig
@ -32,7 +32,7 @@ module Raw : sig
(** get the field name and the annotation of the last access in the list of accesses if (** get the field name and the annotation of the last access in the list of accesses if
the list is non-empty and the last access is a field access *) the list is non-empty and the last access is a field access *)
val get_field_and_annotation : t -> Tenv.t -> (Fieldname.t * Annot.Item.t) option val get_field_and_annotation : t -> Tenv.t -> (Typ.Fieldname.t * Annot.Item.t) option
(** get the typ of the last access in the list of accesses if the list is non-empty, or the base (** get the typ of the last access in the list of accesses if the list is non-empty, or the base
if the list is empty. that is, for x.f.g, return typ(g), and for x, return typ(x) *) if the list is empty. that is, for x.f.g, return typ(g), and for x, return typ(x) *)

@ -112,7 +112,7 @@ let pname_has_return_annot pname ~attrs_of_pname predicate =
let field_has_annot fieldname (struct_typ : Typ.Struct.t) predicate = let field_has_annot fieldname (struct_typ : Typ.Struct.t) predicate =
let fld_has_taint_annot (fname, _, annot) = let fld_has_taint_annot (fname, _, annot) =
Fieldname.equal fieldname fname && predicate annot in Typ.Fieldname.equal fieldname fname && predicate annot in
List.exists ~f:fld_has_taint_annot struct_typ.fields || List.exists ~f:fld_has_taint_annot struct_typ.fields ||
List.exists ~f:fld_has_taint_annot struct_typ.statics List.exists ~f:fld_has_taint_annot struct_typ.statics

@ -109,7 +109,7 @@ val pdesc_return_annot_ends_with : Procdesc.t -> string -> bool
val ma_has_annotation_with : Annot.Method.t -> (Annot.t -> bool) -> bool val ma_has_annotation_with : Annot.Method.t -> (Annot.t -> bool) -> bool
val field_has_annot : Fieldname.t -> Typ.Struct.t -> (Annot.Item.t -> bool) -> bool val field_has_annot : Typ.Fieldname.t -> Typ.Struct.t -> (Annot.Item.t -> bool) -> bool
(** return true if the given predicate evaluates to true on some annotation of [struct_typ] *) (** return true if the given predicate evaluates to true on some annotation of [struct_typ] *)
val struct_typ_has_annot : Typ.Struct.t -> (Annot.Item.t -> bool) -> bool val struct_typ_has_annot : Typ.Struct.t -> (Annot.Item.t -> bool) -> bool

@ -31,7 +31,7 @@ let callback_fragment_retains_view_java
| _ -> false in | _ -> false in
(* is [fldname] a View type declared by [class_typename]? *) (* is [fldname] a View type declared by [class_typename]? *)
let is_declared_view_typ class_typename (fldname, fld_typ, _) = let is_declared_view_typ class_typename (fldname, fld_typ, _) =
let fld_classname = Typ.Name.Java.from_string (Fieldname.java_get_class fldname) in let fld_classname = Typ.Name.Java.from_string (Typ.Fieldname.java_get_class fldname) in
Typ.Name.equal fld_classname class_typename && fld_typ_is_view fld_typ in Typ.Name.equal fld_classname class_typename && fld_typ_is_view fld_typ in
if is_on_destroy_view then if is_on_destroy_view then
begin begin
@ -45,7 +45,7 @@ let callback_fragment_retains_view_java
(* report if a field is declared by C, but not nulled out in C.onDestroyView *) (* report if a field is declared by C, but not nulled out in C.onDestroyView *)
List.iter List.iter
~f:(fun (fname, fld_typ, _) -> ~f:(fun (fname, fld_typ, _) ->
if not (Fieldname.Set.mem fname fields_nullified) then if not (Typ.Fieldname.Set.mem fname fields_nullified) then
report_error report_error
(Typ.mk (Tstruct class_typename)) fname fld_typ summary proc_desc) (Typ.mk (Tstruct class_typename)) fname fld_typ summary proc_desc)
declared_view_fields declared_view_fields

@ -13,7 +13,7 @@ open! IStd
module L = Logging module L = Logging
type field_type = Fieldname.t * Typ.t * (Annot.t * bool) list type field_type = Typ.Fieldname.t * Typ.t * (Annot.t * bool) list
let rec get_fields_super_classes tenv super_class = let rec get_fields_super_classes tenv super_class =
L.(debug Capture Verbose) " ... Getting fields of superclass '%s'@\n" L.(debug Capture Verbose) " ... Getting fields of superclass '%s'@\n"

@ -11,7 +11,7 @@ open! IStd
(** Utility module to retrieve fields of structs of classes *) (** Utility module to retrieve fields of structs of classes *)
type field_type = Fieldname.t * Typ.t * (Annot.t * bool) list type field_type = Typ.Fieldname.t * Typ.t * (Annot.t * bool) list
val get_fields : CAst_utils.qual_type_to_sil_type -> Tenv.t -> Clang_ast_t.decl list -> val get_fields : CAst_utils.qual_type_to_sil_type -> Tenv.t -> Clang_ast_t.decl list ->
field_type list field_type list

@ -49,7 +49,7 @@ let add_no_duplicates_fields field_tuple l =
match field_tuple, l with match field_tuple, l with
| (field, typ, annot), ((old_field, old_typ, old_annot) as old_field_tuple :: rest) -> | (field, typ, annot), ((old_field, old_typ, old_annot) as old_field_tuple :: rest) ->
let ret_list, ret_found = replace_field field_tuple rest found in let ret_list, ret_found = replace_field field_tuple rest found in
if Fieldname.equal field old_field && Typ.equal typ old_typ then if Typ.Fieldname.equal field old_field && Typ.equal typ old_typ then
let annotations = append_no_duplicates_annotations annot old_annot in let annotations = append_no_duplicates_annotations annot old_annot in
(field, typ, annotations) :: ret_list, true (field, typ, annotations) :: ret_list, true
else old_field_tuple :: ret_list, ret_found else old_field_tuple :: ret_list, ret_found
@ -67,7 +67,7 @@ let rec append_no_duplicates_fields list1 list2 =
let sort_fields fields = let sort_fields fields =
let compare (name1, _, _) (name2, _, _) = let compare (name1, _, _) (name2, _, _) =
Fieldname.compare name1 name2 in Typ.Fieldname.compare name1 name2 in
List.sort ~cmp:compare fields List.sort ~cmp:compare fields
@ -102,7 +102,7 @@ let replicate n el = List.map ~f:(fun _ -> el) (list_range 0 (n -1))
let mk_class_field_name field_qual_name = let mk_class_field_name field_qual_name =
let field_name = field_qual_name.Clang_ast_t.ni_name in let field_name = field_qual_name.Clang_ast_t.ni_name in
let class_name = CAst_utils.get_class_name_from_member field_qual_name in let class_name = CAst_utils.get_class_name_from_member field_qual_name in
Fieldname.Clang.from_qualified class_name field_name Typ.Fieldname.Clang.from_qualified class_name field_name
let is_cpp_translation translation_unit_context = let is_cpp_translation translation_unit_context =
let lang = translation_unit_context.CFrontend_config.lang in let lang = translation_unit_context.CFrontend_config.lang in

@ -16,16 +16,16 @@ type var_info = Clang_ast_t.decl_info * Clang_ast_t.qual_type * Clang_ast_t.var_
val string_from_list : string list -> string val string_from_list : string list -> string
val append_no_duplicates_fields : (Fieldname.t * Typ.t * Annot.Item.t) list -> val append_no_duplicates_fields : (Typ.Fieldname.t * Typ.t * Annot.Item.t) list ->
(Fieldname.t * Typ.t * Annot.Item.t) list -> (Typ.Fieldname.t * Typ.t * Annot.Item.t) list ->
(Fieldname.t * Typ.t * Annot.Item.t) list (Typ.Fieldname.t * Typ.t * Annot.Item.t) list
val append_no_duplicates_csu : val append_no_duplicates_csu :
Typ.Name.t list -> Typ.Name.t list -> Typ.Name.t list Typ.Name.t list -> Typ.Name.t list -> Typ.Name.t list
val sort_fields : val sort_fields :
(Fieldname.t * Typ.t * Annot.Item.t) list -> (Typ.Fieldname.t * Typ.t * Annot.Item.t) list ->
(Fieldname.t * Typ.t * Annot.Item.t) list (Typ.Fieldname.t * Typ.t * Annot.Item.t) list
val sort_fields_tenv : Tenv.t -> unit val sort_fields_tenv : Tenv.t -> unit
@ -43,7 +43,7 @@ val list_range: int -> int -> int list
val replicate: int -> 'a -> 'a list val replicate: int -> 'a -> 'a list
val mk_class_field_name : Clang_ast_t.named_decl_info -> Fieldname.t val mk_class_field_name : Clang_ast_t.named_decl_info -> Typ.Fieldname.t
val get_var_name_mangled : Clang_ast_t.named_decl_info -> Clang_ast_t.var_decl_info -> val get_var_name_mangled : Clang_ast_t.named_decl_info -> Clang_ast_t.var_decl_info ->
(string * Mangled.t) (string * Mangled.t)

@ -115,7 +115,7 @@ struct
let fields = List.map ~f:mk_field_from_captured_var captured_vars in let fields = List.map ~f:mk_field_from_captured_var captured_vars in
L.(debug Capture Verbose) "Block %s field:@\n" block_name; L.(debug Capture Verbose) "Block %s field:@\n" block_name;
List.iter ~f:(fun (fn, _, _) -> List.iter ~f:(fun (fn, _, _) ->
L.(debug Capture Verbose) "-----> field: '%s'@\n" (Fieldname.to_string fn)) fields; L.(debug Capture Verbose) "-----> field: '%s'@\n" (Typ.Fieldname.to_string fn)) fields;
let block_typename = Typ.Name.Objc.from_string block_name in let block_typename = Typ.Name.Objc.from_string block_name in
ignore (Tenv.mk_struct tenv ~fields block_typename); ignore (Tenv.mk_struct tenv ~fields block_typename);
let block_type = Typ.mk (Typ.Tstruct block_typename) in let block_type = Typ.mk (Typ.Tstruct block_typename) in

@ -87,7 +87,7 @@ let add_class_to_tenv qual_type_to_sil_type tenv decl_info name_info decl_list o
ocidi.Clang_ast_t.otdi_protocols in ocidi.Clang_ast_t.otdi_protocols in
let fields_sc = CField_decl.fields_superclass tenv ocidi in let fields_sc = CField_decl.fields_superclass tenv ocidi in
List.iter ~f:(fun (fn, ft, _) -> List.iter ~f:(fun (fn, ft, _) ->
L.(debug Capture Verbose) "----->SuperClass field: '%s' " (Fieldname.to_string fn); L.(debug Capture Verbose) "----->SuperClass field: '%s' " (Typ.Fieldname.to_string fn);
L.(debug Capture Verbose) "type: '%s'@\n" (Typ.to_string ft)) fields_sc; L.(debug Capture Verbose) "type: '%s'@\n" (Typ.to_string ft)) fields_sc;
(*In case we found categories, or partial definition of this class earlier and they are already in the tenv *) (*In case we found categories, or partial definition of this class earlier and they are already in the tenv *)
let fields, (supers : Typ.Name.t list) = let fields, (supers : Typ.Name.t list) =
@ -103,7 +103,7 @@ let add_class_to_tenv qual_type_to_sil_type tenv decl_info name_info decl_list o
let all_fields = CGeneral_utils.append_no_duplicates_fields modelled_fields fields in let all_fields = CGeneral_utils.append_no_duplicates_fields modelled_fields fields in
L.(debug Capture Verbose) "Class %a field:@\n" QualifiedCppName.pp class_name; L.(debug Capture Verbose) "Class %a field:@\n" QualifiedCppName.pp class_name;
List.iter ~f:(fun (fn, _, _) -> List.iter ~f:(fun (fn, _, _) ->
L.(debug Capture Verbose) "-----> field: '%s'@\n" (Fieldname.to_string fn)) all_fields; L.(debug Capture Verbose) "-----> field: '%s'@\n" (Typ.Fieldname.to_string fn)) all_fields;
ignore( ignore(
Tenv.mk_struct tenv Tenv.mk_struct tenv
~fields: all_fields ~supers ~methods:[] ~annots:Annot.Class.objc interface_name ); ~fields: all_fields ~supers ~methods:[] ~annots:Annot.Class.objc interface_name );

@ -189,13 +189,13 @@ let check_field_assignment tenv
not (TypeAnnotation.get_value AnnotatedSignature.Nullable ta_lhs) && not (TypeAnnotation.get_value AnnotatedSignature.Nullable ta_lhs) &&
TypeAnnotation.get_value AnnotatedSignature.Nullable ta_rhs && TypeAnnotation.get_value AnnotatedSignature.Nullable ta_rhs &&
PatternMatch.type_is_class t_lhs && PatternMatch.type_is_class t_lhs &&
not (Fieldname.java_is_outer_instance fname) && not (Typ.Fieldname.java_is_outer_instance fname) &&
not (field_is_field_injector_readwrite ()) in not (field_is_field_injector_readwrite ()) in
let should_report_absent = let should_report_absent =
Config.eradicate_optional_present && Config.eradicate_optional_present &&
TypeAnnotation.get_value AnnotatedSignature.Present ta_lhs && TypeAnnotation.get_value AnnotatedSignature.Present ta_lhs &&
not (TypeAnnotation.get_value AnnotatedSignature.Present ta_rhs) && not (TypeAnnotation.get_value AnnotatedSignature.Present ta_rhs) &&
not (Fieldname.java_is_outer_instance fname) in not (Typ.Fieldname.java_is_outer_instance fname) in
let should_report_mutable = let should_report_mutable =
let field_is_mutable () = match t_ia_opt with let field_is_mutable () = match t_ia_opt with
| Some (_, ia) -> Annotations.ia_is_mutable ia | Some (_, ia) -> Annotations.ia_is_mutable ia
@ -261,7 +261,7 @@ let check_constructor_initialization tenv
List.exists List.exists
~f:(function pname, typestate -> ~f:(function pname, typestate ->
let pvar = Pvar.mk let pvar = Pvar.mk
(Mangled.from_string (Fieldname.to_string fn)) (Mangled.from_string (Typ.Fieldname.to_string fn))
pname in pname in
filter_range_opt (TypeState.lookup_pvar pvar typestate)) filter_range_opt (TypeState.lookup_pvar pvar typestate))
list in list in
@ -288,12 +288,12 @@ let check_constructor_initialization tenv
let should_check_field_initialization = let should_check_field_initialization =
let in_current_class = let in_current_class =
let fld_cname = Fieldname.java_get_class fn in let fld_cname = Typ.Fieldname.java_get_class fn in
String.equal (Typ.Name.name name) fld_cname in String.equal (Typ.Name.name name) fld_cname in
not injector_readonly_annotated && not injector_readonly_annotated &&
PatternMatch.type_is_class ft && PatternMatch.type_is_class ft &&
in_current_class && in_current_class &&
not (Fieldname.java_is_outer_instance fn) in not (Typ.Fieldname.java_is_outer_instance fn) in
if should_check_field_initialization then ( if should_check_field_initialization then (
if Models.Inference.enabled then Models.Inference.field_add_nullable_annotation fn; if Models.Inference.enabled then Models.Inference.field_add_nullable_annotation fn;

@ -25,7 +25,7 @@ module Inference = struct
let get_dir () = Filename.concat Config.results_dir "eradicate" let get_dir () = Filename.concat Config.results_dir "eradicate"
let field_get_dir_fname fn = let field_get_dir_fname fn =
let fname = Fieldname.to_string fn in let fname = Typ.Fieldname.to_string fn in
(get_dir (), fname) (get_dir (), fname)
let field_is_marked fn = let field_is_marked fn =

@ -93,7 +93,7 @@ module ComplexExpressions = struct
dexp_to_string de1 ^ "[" ^ dexp_to_string de2 ^ "]" dexp_to_string de1 ^ "[" ^ dexp_to_string de2 ^ "]"
| DExp.Darrow (de, f) | DExp.Darrow (de, f)
| DExp.Ddot (de, f) -> | DExp.Ddot (de, f) ->
dexp_to_string de ^ "." ^ Fieldname.to_string f dexp_to_string de ^ "." ^ Typ.Fieldname.to_string f
| DExp.Dbinop (op, de1, de2) -> | DExp.Dbinop (op, de1, de2) ->
"(" ^ dexp_to_string de1 ^ (Binop.str Pp.text op) ^ dexp_to_string de2 ^ ")" "(" ^ dexp_to_string de1 ^ (Binop.str Pp.text op) ^ dexp_to_string de2 ^ ")"
| DExp.Dconst (Const.Cfun pn) -> | DExp.Dconst (Const.Cfun pn) ->
@ -221,7 +221,7 @@ let rec typecheck_expr
match EradicateChecks.explain_expr tenv node index_exp with match EradicateChecks.explain_expr tenv node index_exp with
| Some s -> s | Some s -> s
| None -> "?" in | None -> "?" in
let fname = Fieldname.Java.from_string index in let fname = Typ.Fieldname.Java.from_string index in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_array_access tenv EradicateChecks.check_array_access tenv
find_canonical_duplicate find_canonical_duplicate
@ -368,13 +368,13 @@ let typecheck_instr
let res = match exp' with let res = match exp' with
| Exp.Lvar pv when is_parameter_field pv || is_static_field pv -> | Exp.Lvar pv when is_parameter_field pv || is_static_field pv ->
let fld_name = pvar_to_str pv ^ Fieldname.to_string fn in let fld_name = pvar_to_str pv ^ Typ.Fieldname.to_string fn in
let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in
let typestate' = update_typestate_fld pvar inner_origin fn typ in let typestate' = update_typestate_fld pvar inner_origin fn typ in
(Exp.Lvar pvar, typestate') (Exp.Lvar pvar, typestate')
| Exp.Lfield (_exp', fn', _) when Fieldname.java_is_outer_instance fn' -> | Exp.Lfield (_exp', fn', _) when Typ.Fieldname.java_is_outer_instance fn' ->
(* handle double dereference when accessing a field from an outer class *) (* handle double dereference when accessing a field from an outer class *)
let fld_name = Fieldname.to_string fn' ^ "_" ^ Fieldname.to_string fn in let fld_name = Typ.Fieldname.to_string fn' ^ "_" ^ Typ.Fieldname.to_string fn in
let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in let pvar = Pvar.mk (Mangled.from_string fld_name) curr_pname in
let typestate' = update_typestate_fld pvar inner_origin fn typ in let typestate' = update_typestate_fld pvar inner_origin fn typ in
(Exp.Lvar pvar, typestate') (Exp.Lvar pvar, typestate')
@ -558,7 +558,7 @@ let typecheck_instr
node node
instr_ref instr_ref
array_exp array_exp
(Fieldname.Java.from_string "length") (Typ.Fieldname.Java.from_string "length")
ta ta
loc loc
false; false;

@ -70,11 +70,11 @@ type err_instance =
| Condition_redundant of (bool * (string option) * bool) | Condition_redundant of (bool * (string option) * bool)
| Inconsistent_subclass_return_annotation of Typ.Procname.t * Typ.Procname.t | Inconsistent_subclass_return_annotation of Typ.Procname.t * Typ.Procname.t
| Inconsistent_subclass_parameter_annotation of string * int * Typ.Procname.t * Typ.Procname.t | Inconsistent_subclass_parameter_annotation of string * int * Typ.Procname.t * Typ.Procname.t
| Field_not_initialized of Fieldname.t * Typ.Procname.t | Field_not_initialized of Typ.Fieldname.t * Typ.Procname.t
| Field_not_mutable of Fieldname.t * origin_descr | Field_not_mutable of Typ.Fieldname.t * origin_descr
| Field_annotation_inconsistent of AnnotatedSignature.annotation * Fieldname.t * origin_descr | Field_annotation_inconsistent of AnnotatedSignature.annotation * Typ.Fieldname.t * origin_descr
| Field_over_annotated of Fieldname.t * Typ.Procname.t | Field_over_annotated of Typ.Fieldname.t * Typ.Procname.t
| Null_field_access of string option * Fieldname.t * origin_descr * bool | Null_field_access of string option * Typ.Fieldname.t * origin_descr * bool
| Call_receiver_annotation_inconsistent | Call_receiver_annotation_inconsistent
of AnnotatedSignature.annotation * string option * Typ.Procname.t * origin_descr of AnnotatedSignature.annotation * string option * Typ.Procname.t * origin_descr
| Parameter_annotation_inconsistent of parameter_not_nullable | Parameter_annotation_inconsistent of parameter_not_nullable
@ -94,15 +94,15 @@ module H = Hashtbl.Make(struct
| Condition_redundant (b, so, nn) -> | Condition_redundant (b, so, nn) ->
Hashtbl.hash (1, b, string_opt_hash so, nn) Hashtbl.hash (1, b, string_opt_hash so, nn)
| Field_not_initialized (fn, pn) -> | Field_not_initialized (fn, pn) ->
Hashtbl.hash (2, string_hash ((Fieldname.to_string fn) ^ (Typ.Procname.to_string pn))) Hashtbl.hash (2, string_hash ((Typ.Fieldname.to_string fn) ^ (Typ.Procname.to_string pn)))
| Field_not_mutable (fn, _) -> | Field_not_mutable (fn, _) ->
Hashtbl.hash (3, string_hash (Fieldname.to_string fn)) Hashtbl.hash (3, string_hash (Typ.Fieldname.to_string fn))
| Field_annotation_inconsistent (ann, fn, _) -> | Field_annotation_inconsistent (ann, fn, _) ->
Hashtbl.hash (4, ann, string_hash (Fieldname.to_string fn)) Hashtbl.hash (4, ann, string_hash (Typ.Fieldname.to_string fn))
| Field_over_annotated (fn, pn) -> | Field_over_annotated (fn, pn) ->
Hashtbl.hash (5, string_hash ((Fieldname.to_string fn) ^ (Typ.Procname.to_string pn))) Hashtbl.hash (5, string_hash ((Typ.Fieldname.to_string fn) ^ (Typ.Procname.to_string pn)))
| Null_field_access (so, fn, _, _) -> | Null_field_access (so, fn, _, _) ->
Hashtbl.hash (6, string_opt_hash so, string_hash (Fieldname.to_string fn)) Hashtbl.hash (6, string_opt_hash so, string_hash (Typ.Fieldname.to_string fn))
| Call_receiver_annotation_inconsistent (ann, so, pn, _) -> | Call_receiver_annotation_inconsistent (ann, so, pn, _) ->
Hashtbl.hash (7, ann, string_opt_hash so, Typ.Procname.hash_pname pn) Hashtbl.hash (7, ann, string_opt_hash so, Typ.Procname.hash_pname pn)
| Parameter_annotation_inconsistent (ann, s, n, pn, _, _) -> | Parameter_annotation_inconsistent (ann, s, n, pn, _, _) ->
@ -231,7 +231,7 @@ type st_report_error =
Localise.t -> Localise.t ->
Location.t -> Location.t ->
?advice: string option -> ?advice: string option ->
?field_name: Fieldname.t option -> ?field_name: Typ.Fieldname.t option ->
?origin_loc: Location.t option -> ?origin_loc: Location.t option ->
?exception_kind: (string -> Localise.error_desc -> exn) -> ?exception_kind: (string -> Localise.error_desc -> exn) ->
?always_report: bool -> ?always_report: bool ->
@ -282,7 +282,7 @@ let report_error_now tenv
Localise.eradicate_field_not_initialized, Localise.eradicate_field_not_initialized,
Format.asprintf Format.asprintf
"Field %a is not initialized in %s and is not declared %a" "Field %a is not initialized in %s and is not declared %a"
MF.pp_monospaced (Fieldname.to_simplified_string fn) MF.pp_monospaced (Typ.Fieldname.to_simplified_string fn)
constructor_name constructor_name
MF.pp_monospaced "@Nullable", MF.pp_monospaced "@Nullable",
None, None,
@ -293,7 +293,7 @@ let report_error_now tenv
Localise.eradicate_field_not_mutable, Localise.eradicate_field_not_mutable,
Format.asprintf Format.asprintf
"Field %a is modified but is not declared %a. %s" "Field %a is modified but is not declared %a. %s"
MF.pp_monospaced (Fieldname.to_simplified_string fn) MF.pp_monospaced (Typ.Fieldname.to_simplified_string fn)
MF.pp_monospaced "@Mutable" MF.pp_monospaced "@Mutable"
origin_description, origin_description,
None, None,
@ -305,14 +305,14 @@ let report_error_now tenv
Localise.eradicate_field_not_nullable, Localise.eradicate_field_not_nullable,
Format.asprintf Format.asprintf
"Field %a can be null but is not declared %a. %s" "Field %a can be null but is not declared %a. %s"
MF.pp_monospaced (Fieldname.to_simplified_string fn) MF.pp_monospaced (Typ.Fieldname.to_simplified_string fn)
MF.pp_monospaced "@Nullable" MF.pp_monospaced "@Nullable"
origin_description origin_description
| AnnotatedSignature.Present -> | AnnotatedSignature.Present ->
Localise.eradicate_field_value_absent, Localise.eradicate_field_value_absent,
Format.asprintf Format.asprintf
"Field %a is assigned a possibly absent value but is declared %a. %s" "Field %a is assigned a possibly absent value but is declared %a. %s"
MF.pp_monospaced (Fieldname.to_simplified_string fn) MF.pp_monospaced (Typ.Fieldname.to_simplified_string fn)
MF.pp_monospaced "@Present" MF.pp_monospaced "@Present"
origin_description in origin_description in
true, true,
@ -335,7 +335,7 @@ let report_error_now tenv
Localise.eradicate_field_over_annotated, Localise.eradicate_field_over_annotated,
Format.asprintf Format.asprintf
"Field %a is always initialized in %s but is declared %a" "Field %a is always initialized in %s but is declared %a"
MF.pp_monospaced (Fieldname.to_simplified_string fn) MF.pp_monospaced (Typ.Fieldname.to_simplified_string fn)
constructor_name constructor_name
MF.pp_monospaced "@Nullable", MF.pp_monospaced "@Nullable",
None, None,
@ -349,7 +349,7 @@ let report_error_now tenv
"Object %a could be null when accessing %s %a. %s" "Object %a could be null when accessing %s %a. %s"
MF.pp_monospaced (Option.value s_opt ~default:"") MF.pp_monospaced (Option.value s_opt ~default:"")
at_index at_index
MF.pp_monospaced (Fieldname.to_simplified_string fn) MF.pp_monospaced (Typ.Fieldname.to_simplified_string fn)
origin_description, origin_description,
None, None,
None, None,

@ -52,11 +52,11 @@ type err_instance =
| Condition_redundant of (bool * (string option) * bool) | Condition_redundant of (bool * (string option) * bool)
| Inconsistent_subclass_return_annotation of Typ.Procname.t * Typ.Procname.t | Inconsistent_subclass_return_annotation of Typ.Procname.t * Typ.Procname.t
| Inconsistent_subclass_parameter_annotation of string * int * Typ.Procname.t * Typ.Procname.t | Inconsistent_subclass_parameter_annotation of string * int * Typ.Procname.t * Typ.Procname.t
| Field_not_initialized of Fieldname.t * Typ.Procname.t | Field_not_initialized of Typ.Fieldname.t * Typ.Procname.t
| Field_not_mutable of Fieldname.t * origin_descr | Field_not_mutable of Typ.Fieldname.t * origin_descr
| Field_annotation_inconsistent of AnnotatedSignature.annotation * Fieldname.t * origin_descr | Field_annotation_inconsistent of AnnotatedSignature.annotation * Typ.Fieldname.t * origin_descr
| Field_over_annotated of Fieldname.t * Typ.Procname.t | Field_over_annotated of Typ.Fieldname.t * Typ.Procname.t
| Null_field_access of string option * Fieldname.t * origin_descr * bool | Null_field_access of string option * Typ.Fieldname.t * origin_descr * bool
| Call_receiver_annotation_inconsistent | Call_receiver_annotation_inconsistent
of AnnotatedSignature.annotation * string option * Typ.Procname.t * origin_descr of AnnotatedSignature.annotation * string option * Typ.Procname.t * origin_descr
| Parameter_annotation_inconsistent of parameter_not_nullable | Parameter_annotation_inconsistent of parameter_not_nullable
@ -72,7 +72,7 @@ type st_report_error =
Localise.t -> Localise.t ->
Location.t -> Location.t ->
?advice: string option -> ?advice: string option ->
?field_name: Fieldname.t option -> ?field_name: Typ.Fieldname.t option ->
?origin_loc: Location.t option -> ?origin_loc: Location.t option ->
?exception_kind: (string -> Localise.error_desc -> exn) -> ?exception_kind: (string -> Localise.error_desc -> exn) ->
?always_report: bool -> ?always_report: bool ->

@ -26,7 +26,7 @@ type proc_origin =
type t = type t =
| Const of Location.t | Const of Location.t
| Field of t * Fieldname.t * Location.t | Field of t * Typ.Fieldname.t * Location.t
| Formal of Mangled.t | Formal of Mangled.t
| Proc of proc_origin | Proc of proc_origin
| New | New
@ -40,7 +40,7 @@ let rec to_string = function
| Const _ -> | Const _ ->
"Const" "Const"
| Field (o, fn, _) -> | Field (o, fn, _) ->
"Field " ^ Fieldname.to_simplified_string fn ^ (" (inner: " ^ to_string o ^ ")") "Field " ^ Typ.Fieldname.to_simplified_string fn ^ (" (inner: " ^ to_string o ^ ")")
| Formal s -> | Formal s ->
"Formal " ^ Mangled.to_string s "Formal " ^ Mangled.to_string s
| Proc po -> | Proc po ->
@ -61,7 +61,7 @@ let get_description tenv origin =
| Const loc -> | Const loc ->
Some ("null constant" ^ atline loc, Some loc, None) Some ("null constant" ^ atline loc, Some loc, None)
| Field (_, fn, loc) -> | Field (_, fn, loc) ->
Some ("field " ^ Fieldname.to_simplified_string fn ^ atline loc, Some loc, None) Some ("field " ^ Typ.Fieldname.to_simplified_string fn ^ atline loc, Some loc, None)
| Formal s -> | Formal s ->
Some ("method parameter " ^ Mangled.to_string s, None, None) Some ("method parameter " ^ Mangled.to_string s, None, None)
| Proc po -> | Proc po ->

@ -20,7 +20,7 @@ type proc_origin =
type t = type t =
| Const of Location.t (** A constant in the source *) | Const of Location.t (** A constant in the source *)
| Field of t * Fieldname.t * Location.t (** A field access *) | Field of t * Typ.Fieldname.t * Location.t (** A field access *)
| Formal of Mangled.t (** A formal parameter *) | Formal of Mangled.t (** A formal parameter *)
| Proc of proc_origin (** A procedure call *) | Proc of proc_origin (** A procedure call *)
| New (** A new object creation *) | New (** A new object creation *)

@ -96,7 +96,7 @@ let get_undefined_method_call ovt =
let retrieve_fieldname fieldname = let retrieve_fieldname fieldname =
try try
let subs = Str.split (Str.regexp (Str.quote ".")) (Fieldname.to_string fieldname) in let subs = Str.split (Str.regexp (Str.quote ".")) (Typ.Fieldname.to_string fieldname) in
if Int.equal (List.length subs) 0 then if Int.equal (List.length subs) 0 then
assert false assert false
else else

@ -210,7 +210,7 @@ let translate_method_name m =
let fieldname_create cn fs = let fieldname_create cn fs =
let fieldname = (JBasics.fs_name fs) in let fieldname = (JBasics.fs_name fs) in
let classname = (JBasics.cn_name cn) in let classname = (JBasics.cn_name cn) in
Fieldname.Java.from_string (classname^"."^fieldname) Typ.Fieldname.Java.from_string (classname^"."^fieldname)
let create_sil_class_field cn cf = let create_sil_class_field cn cf =
let fs = cf.Javalib.cf_signature in let fs = cf.Javalib.cf_signature in
@ -247,13 +247,13 @@ let collect_models_class_fields classpath_field_map cn cf fields =
let static, nonstatic = fields in let static, nonstatic = fields in
let field_name, field_type, annotation = create_sil_class_field cn cf in let field_name, field_type, annotation = create_sil_class_field cn cf in
try try
let classpath_ft = Fieldname.Map.find field_name classpath_field_map in let classpath_ft = Typ.Fieldname.Map.find field_name classpath_field_map in
if Typ.equal classpath_ft field_type then fields if Typ.equal classpath_ft field_type then fields
else else
(* TODO (#6711750): fix type equality for arrays before failing here *) (* TODO (#6711750): fix type equality for arrays before failing here *)
let () = L.(debug Capture Quiet) let () = L.(debug Capture Quiet)
"Found inconsistent types for %s@\n\tclasspath: %a@\n\tmodels: %a@\n@." "Found inconsistent types for %s@\n\tclasspath: %a@\n\tmodels: %a@\n@."
(Fieldname.to_string field_name) (Typ.Fieldname.to_string field_name)
(Typ.pp_full Pp.text) classpath_ft (Typ.pp_full Pp.text) classpath_ft
(Typ.pp_full Pp.text) field_type in fields (Typ.pp_full Pp.text) field_type in fields
with Not_found -> with Not_found ->
@ -268,8 +268,8 @@ let add_model_fields program classpath_fields cn =
let classpath_field_map = let classpath_field_map =
let collect_fields map = let collect_fields map =
List.fold List.fold
~f:(fun map (fn, ft, _) -> Fieldname.Map.add fn ft map) ~init:map in ~f:(fun map (fn, ft, _) -> Typ.Fieldname.Map.add fn ft map) ~init:map in
collect_fields (collect_fields Fieldname.Map.empty statics) nonstatics in collect_fields (collect_fields Typ.Fieldname.Map.empty statics) nonstatics in
try try
match JBasics.ClassMap.find cn (JClasspath.get_models program) with match JBasics.ClassMap.find cn (JClasspath.get_models program) with
| Javalib.JClass _ as jclass -> | Javalib.JClass _ as jclass ->
@ -351,7 +351,7 @@ let get_class_type program tenv cn =
(** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *) (** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *)
let is_autogenerated_assert_field field_name = let is_autogenerated_assert_field field_name =
String.equal (Fieldname.java_get_field field_name) "$assertionsDisabled" String.equal (Typ.Fieldname.java_get_field field_name) "$assertionsDisabled"
let is_closeable program tenv typ = let is_closeable program tenv typ =
let closeable_cn = JBasics.make_cn "java.io.Closeable" in let closeable_cn = JBasics.make_cn "java.io.Closeable" in

@ -20,7 +20,7 @@ val get_named_type : JBasics.value_type -> Typ.t
val typename_of_classname : JBasics.class_name -> Typ.Name.t val typename_of_classname : JBasics.class_name -> Typ.Name.t
(** returns a name for a field based on a class name and a field name *) (** returns a name for a field based on a class name and a field name *)
val fieldname_create : JBasics.class_name -> JBasics.field_signature -> Fieldname.t val fieldname_create : JBasics.class_name -> JBasics.field_signature -> Typ.Fieldname.t
val get_method_kind : JCode.jcode Javalib.jmethod -> Typ.Procname.method_kind val get_method_kind : JCode.jcode Javalib.jmethod -> Typ.Procname.method_kind
@ -42,7 +42,7 @@ val get_class_type_no_pointer: JClasspath.program -> Tenv.t -> JBasics.class_nam
val get_class_type : JClasspath.program -> Tenv.t -> JBasics.class_name -> Typ.t val get_class_type : JClasspath.program -> Tenv.t -> JBasics.class_name -> Typ.t
(** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *) (** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *)
val is_autogenerated_assert_field : Fieldname.t -> bool val is_autogenerated_assert_field : Typ.Fieldname.t -> bool
(** [is_closeable program tenv typ] check if typ is an implemtation of the Closeable interface *) (** [is_closeable program tenv typ] check if typ is an implemtation of the Closeable interface *)
val is_closeable : JClasspath.program -> Tenv.t -> Typ.t -> bool val is_closeable : JClasspath.program -> Tenv.t -> Typ.t -> bool

@ -15,7 +15,7 @@ let make_var var_str =
let make_base ?(typ=Typ.mk Tvoid) base_str = let make_base ?(typ=Typ.mk Tvoid) base_str =
AccessPath.base_of_pvar (make_var base_str) typ AccessPath.base_of_pvar (make_var base_str) typ
let make_fieldname = Fieldname.Java.from_string let make_fieldname = Typ.Fieldname.Java.from_string
let make_field_access access_str = let make_field_access access_str =
AccessPath.FieldAccess (make_fieldname access_str) AccessPath.FieldAccess (make_fieldname access_str)

@ -11,7 +11,7 @@ open! IStd
val make_var : string -> Pvar.t val make_var : string -> Pvar.t
val make_fieldname : string -> Fieldname.t val make_fieldname : string -> Typ.Fieldname.t
val make_base : ?typ:Typ.t -> string -> AccessPath.base val make_base : ?typ:Typ.t -> string -> AccessPath.base

Loading…
Cancel
Save