[codemod] Move `Procname` into `Typ.Procname`

Summary:
`Procname` needs to depend on `Typ.t` and `Typ.Struct` depends on `Procname.t`.
To resolve this circular dependency issue, move `Procname` into `Typ`

steps:
1. Move everything from `Procname` to `Typ.Procname`, remove `Procname.re(i)`
2. search & replace `Procname.` with `Typ.Procname.`
3. fix outstanding compilation issues manually
4. `yes | arc lint`

Reviewed By: jberdine

Differential Revision: D4681509

fbshipit-source-id: b07af63
master
Andrzej Kotulski 8 years ago committed by Facebook Github Bot
parent 6125632af3
commit e363958d34

@ -39,7 +39,7 @@ let attributes_filename proc_kind::proc_kind pname_file => {
/** path to the .attr file for the given procedure in the current results directory */
let res_dir_attr_filename proc_kind::proc_kind pname => {
let pname_file = Procname.to_filename pname;
let pname_file = Typ.Procname.to_filename pname;
let attr_fname = attributes_filename proc_kind::proc_kind pname_file;
let bucket_dir = {
let base = pname_file;
@ -154,19 +154,19 @@ let store_attributes (proc_attributes: ProcAttributes.t) => {
}
};
let attr_tbl = Procname.Hash.create 16;
let attr_tbl = Typ.Procname.Hash.create 16;
let defined_attr_tbl = Procname.Hash.create 16;
let defined_attr_tbl = Typ.Procname.Hash.create 16;
let load_attributes proc_name =>
try (Procname.Hash.find attr_tbl proc_name) {
try (Typ.Procname.Hash.find attr_tbl proc_name) {
| Not_found =>
let proc_attributes = load_attr defined_only::false proc_name;
switch proc_attributes {
| Some attrs =>
Procname.Hash.add attr_tbl proc_name proc_attributes;
Typ.Procname.Hash.add attr_tbl proc_name proc_attributes;
if attrs.is_defined {
Procname.Hash.add defined_attr_tbl proc_name proc_attributes
Typ.Procname.Hash.add defined_attr_tbl proc_name proc_attributes
}
| None => ()
};
@ -174,15 +174,15 @@ let load_attributes proc_name =>
};
let load_defined_attributes cache_none::cache_none proc_name =>
try (Procname.Hash.find defined_attr_tbl proc_name) {
try (Typ.Procname.Hash.find defined_attr_tbl proc_name) {
| Not_found =>
let proc_attributes = load_attr defined_only::true proc_name;
if (proc_attributes != None) {
/* procedure just got defined, replace attribute in attr_tbl with defined version */
Procname.Hash.replace attr_tbl proc_name proc_attributes;
Procname.Hash.add defined_attr_tbl proc_name proc_attributes
Typ.Procname.Hash.replace attr_tbl proc_name proc_attributes;
Typ.Procname.Hash.add defined_attr_tbl proc_name proc_attributes
} else if cache_none {
Procname.Hash.add defined_attr_tbl proc_name proc_attributes
Typ.Procname.Hash.add defined_attr_tbl proc_name proc_attributes
};
proc_attributes
};
@ -193,7 +193,7 @@ let load_defined_attributes cache_none::cache_none proc_name =>
corresponds to the class definition. */
let get_correct_type_from_objc_class_name type_name =>
/* ToDo: this function should return a type that includes a reference to the tenv computed by:
let class_method = Procname.get_default_objc_class_method (Typename.name type_name);
let class_method = Typ.Procname.get_default_objc_class_method (Typename.name type_name);
switch (find_tenv_from_class_of_proc class_method) {
| Some tenv =>
*/
@ -246,7 +246,7 @@ let aggregate s => {
};
let stats () => {
let stats = Procname.Hash.stats attr_tbl;
let stats = Typ.Procname.Hash.stats attr_tbl;
let {Hashtbl.num_bindings: num_bindings, num_buckets, max_bucket_length} = stats;
let serialized_size_kb =
Config.developer_mode ?

@ -16,11 +16,11 @@ let store_attributes: ProcAttributes.t => unit;
/** Load the attributes for the procedure from the attributes database. */
let load_attributes: Procname.t => option ProcAttributes.t;
let load_attributes: Typ.Procname.t => option ProcAttributes.t;
/** Load attrubutes for the procedure but only if is_defined is true */
let load_defined_attributes: cache_none::bool => Procname.t => option ProcAttributes.t;
let load_defined_attributes: cache_none::bool => Typ.Procname.t => option ProcAttributes.t;
/** Given the name of an ObjC class, extract the type from the tenv where the class was defined. We
@ -31,7 +31,8 @@ let get_correct_type_from_objc_class_name: Typename.t => option Typ.t;
/* Find the file where the procedure was captured, if a cfg for that file exists.
Return also a boolean indicating whether the procedure is defined in an
include file. */
let find_file_capturing_procedure: Procname.t => option (SourceFile.t, [ | `Include | `Source]);
let find_file_capturing_procedure:
Typ.Procname.t => option (SourceFile.t, [ | `Include | `Source]);
type t;

@ -9,26 +9,26 @@
open! IStd
type t = Procname.t
type t = Typ.Procname.t
let builtin_decls = ref Procname.Set.empty
let builtin_decls = ref Typ.Procname.Set.empty
let register pname =
builtin_decls := Procname.Set.add pname !builtin_decls
builtin_decls := Typ.Procname.Set.add pname !builtin_decls
let create_procname name =
let pname = Procname.from_string_c_fun name in
let pname = Typ.Procname.from_string_c_fun name in
register pname;
pname
let create_objc_class_method class_name method_name =
let method_kind = Procname.ObjCClassMethod in
let method_kind = Typ.Procname.ObjCClassMethod in
let tname = Typename.Objc.from_string class_name in
let pname = Procname.ObjC_Cpp (Procname.objc_cpp tname method_name method_kind) in
let pname = Typ.Procname.ObjC_Cpp (Typ.Procname.objc_cpp tname method_name method_kind) in
register pname;
pname
let is_declared pname = Procname.Set.mem pname !builtin_decls
let is_declared pname = Typ.Procname.Set.mem pname !builtin_decls
let __assert_fail = create_procname "__assert_fail"
let __builtin_va_arg = create_procname "__builtin_va_arg"

@ -10,6 +10,6 @@
open! IStd
(** Procnames for the builtin functions supported *)
include BUILTINS.S with type t = Procname.t
include BUILTINS.S with type t = Typ.Procname.t
val is_declared : Procname.t -> bool
val is_declared : Typ.Procname.t -> bool

@ -22,7 +22,7 @@ type t = {
cf_interface: bool,
cf_noreturn: bool,
cf_is_objc_block: bool,
cf_targets: list Procname.t
cf_targets: list Typ.Procname.t
}
[@@deriving compare];

@ -22,7 +22,7 @@ type t = {
cf_interface: bool,
cf_noreturn: bool,
cf_is_objc_block: bool,
cf_targets: list Procname.t
cf_targets: list Typ.Procname.t
}
[@@deriving compare];

@ -13,7 +13,7 @@ module F = Format
type t =
{
pname : Procname.t;
pname : Typ.Procname.t;
loc : Location.t;
}
[@@deriving compare]
@ -30,10 +30,10 @@ let make pname loc =
{ pname; loc; }
let dummy =
make Procname.empty_block Location.dummy
make Typ.Procname.empty_block Location.dummy
let pp fmt t =
F.fprintf fmt "%a at %a" Procname.pp t.pname Location.pp t.loc
F.fprintf fmt "%a at %a" Typ.Procname.pp t.pname Location.pp t.loc
module Set = PrettyPrintable.MakePPSet(struct
type nonrec t = t

@ -15,11 +15,11 @@ type t [@@deriving compare]
val equal : t -> t -> bool
val pname : t -> Procname.t
val pname : t -> Typ.Procname.t
val loc : t -> Location.t
val make : Procname.t -> Location.t -> t
val make : Typ.Procname.t -> Location.t -> t
val dummy : t

@ -15,20 +15,20 @@ let module F = Format;
/** data type for the control flow graph */
type cfg = {proc_desc_table: Procname.Hash.t Procdesc.t /** Map proc name to procdesc */};
type cfg = {proc_desc_table: Typ.Procname.Hash.t Procdesc.t /** Map proc name to procdesc */};
/** create a new empty cfg */
let create_cfg () => {proc_desc_table: Procname.Hash.create 16};
let create_cfg () => {proc_desc_table: Typ.Procname.Hash.create 16};
let add_proc_desc cfg pname pdesc => Procname.Hash.add cfg.proc_desc_table pname pdesc;
let add_proc_desc cfg pname pdesc => Typ.Procname.Hash.add cfg.proc_desc_table pname pdesc;
let remove_proc_desc cfg pname => Procname.Hash.remove cfg.proc_desc_table pname;
let remove_proc_desc cfg pname => Typ.Procname.Hash.remove cfg.proc_desc_table pname;
let iter_proc_desc cfg f => Procname.Hash.iter f cfg.proc_desc_table;
let iter_proc_desc cfg f => Typ.Procname.Hash.iter f cfg.proc_desc_table;
let find_proc_desc_from_name cfg pname =>
try (Some (Procname.Hash.find cfg.proc_desc_table pname)) {
try (Some (Typ.Procname.Hash.find cfg.proc_desc_table pname)) {
| Not_found => None
};
@ -48,7 +48,7 @@ let iter_all_nodes sorted::sorted=false f cfg => {
if (not sorted) {
iter_proc_desc cfg do_proc_desc
} else {
Procname.Hash.fold
Typ.Procname.Hash.fold
(
fun _ pdesc desc_nodes =>
List.fold
@ -105,7 +105,7 @@ let check_cfg_connectedness cfg => {
}
};
let do_pdesc pd => {
let pname = Procname.to_string (Procdesc.get_proc_name pd);
let pname = Typ.Procname.to_string (Procdesc.get_proc_name pd);
let nodes = Procdesc.get_nodes pd;
let broken = List.exists f::broken_node nodes;
if broken {
@ -212,7 +212,7 @@ let proc_inline_synthetic_methods cfg pdesc :unit => {
| Sil.Call ret_id (Exp.Const (Const.Cfun pn)) etl loc _ =>
switch (find_proc_desc_from_name cfg pn) {
| Some pd =>
let is_access = Procname.java_is_access_method pn;
let is_access = Typ.Procname.java_is_access_method pn;
let attributes = Procdesc.get_attributes pd;
let is_synthetic = attributes.is_synthetic_method;
let is_bridge = attributes.is_bridge_method;
@ -246,7 +246,7 @@ let proc_inline_synthetic_methods cfg pdesc :unit => {
/** Inline the java synthetic methods in the cfg */
let inline_java_synthetic_methods cfg => {
let f pname pdesc =>
if (Procname.is_java pname) {
if (Typ.Procname.is_java pname) {
proc_inline_synthetic_methods cfg pdesc
};
iter_proc_desc cfg f
@ -310,7 +310,7 @@ let mark_unchanged_pdescs cfg_new cfg_old => {
let new_procs = cfg_new.proc_desc_table;
let mark_pdesc_if_unchanged pname (new_pdesc: Procdesc.t) =>
try {
let old_pdesc = Procname.Hash.find old_procs pname;
let old_pdesc = Typ.Procname.Hash.find old_procs pname;
let changed =
/* in continue_capture mode keep the old changed bit */
Config.continue_capture && (Procdesc.get_attributes old_pdesc).changed ||
@ -319,7 +319,7 @@ let mark_unchanged_pdescs cfg_new cfg_old => {
} {
| Not_found => ()
};
Procname.Hash.iter mark_pdesc_if_unchanged new_procs
Typ.Procname.Hash.iter mark_pdesc_if_unchanged new_procs
};
@ -388,7 +388,7 @@ let specialize_types_proc callee_pdesc resolved_pdesc substitutions => {
}
| Sil.Call
return_ids
(Exp.Const (Const.Cfun (Procname.Java callee_pname_java)))
(Exp.Const (Const.Cfun (Typ.Procname.Java callee_pname_java)))
[(Exp.Var id, _), ...origin_args]
loc
call_flags
@ -396,7 +396,7 @@ let specialize_types_proc callee_pdesc resolved_pdesc substitutions => {
let redirected_typename = Option.value_exn (redirect_typename id);
let redirected_typ = mk_ptr_typ redirected_typename;
let redirected_pname =
Procname.replace_class (Procname.Java callee_pname_java) redirected_typename;
Typ.Procname.replace_class (Typ.Procname.Java callee_pname_java) redirected_typename;
let args = {
let other_args = List.map f::(fun (exp, typ) => (convert_exp exp, typ)) origin_args;
[(Exp.Var id, redirected_typ), ...other_args]

@ -35,11 +35,11 @@ let create_proc_desc: cfg => ProcAttributes.t => Procdesc.t;
/** Iterate over all the procdesc's */
let iter_proc_desc: cfg => (Procname.t => Procdesc.t => unit) => unit;
let iter_proc_desc: cfg => (Typ.Procname.t => Procdesc.t => unit) => unit;
/** Find the procdesc given the proc name. Return None if not found. */
let find_proc_desc_from_name: cfg => Procname.t => option Procdesc.t;
let find_proc_desc_from_name: cfg => Typ.Procname.t => option Procdesc.t;
/** Get all the procedures (defined and declared) */
@ -59,13 +59,13 @@ let check_cfg_connectedness: cfg => unit;
/** Remove the procdesc from the control flow graph. */
let remove_proc_desc: cfg => Procname.t => unit;
let remove_proc_desc: cfg => Typ.Procname.t => unit;
/** Creates a copy of a procedure description and a list of type substitutions of the form
(name, typ) where name is a parameter. The resulting procdesc is isomorphic but
all the type of the parameters are replaced in the instructions according to the list.
The virtual calls are also replaced to match the parameter types */
let specialize_types: Procdesc.t => Procname.t => list (Exp.t, Typ.t) => Procdesc.t;
let specialize_types: Procdesc.t => Typ.Procname.t => list (Exp.t, Typ.t) => Procdesc.t;
let pp_proc_signatures: Format.formatter => cfg => unit;

@ -17,7 +17,7 @@ let module L = Logging;
let module F = Format;
type node = Procname.t;
type node = Typ.Procname.t;
type in_out_calls = {
in_calls: int, /** total number of in calls transitively */
@ -27,14 +27,14 @@ type in_out_calls = {
type node_info = {
/** defined procedure as opposed to just declared */
mutable defined: bool,
mutable parents: Procname.Set.t,
mutable children: Procname.Set.t,
mutable parents: Typ.Procname.Set.t,
mutable children: Typ.Procname.Set.t,
/** ancestors are computed lazily */
mutable ancestors: option Procname.Set.t,
mutable ancestors: option Typ.Procname.Set.t,
/** heirs are computed lazily */
mutable heirs: option Procname.Set.t,
mutable heirs: option Typ.Procname.Set.t,
/** recursive dependents are computed lazily */
mutable recursive_dependents: option Procname.Set.t,
mutable recursive_dependents: option Typ.Procname.Set.t,
/** calls are computed lazily */
mutable in_out_calls: option in_out_calls
};
@ -43,7 +43,7 @@ type node_info = {
/** Type for call graph */
type t = {
source: SourceFile.t, /** path for the source file */
node_map: Procname.Hash.t node_info /** map from node to node_info */
node_map: Typ.Procname.Hash.t node_info /** map from node to node_info */
};
let create source_opt => {
@ -52,12 +52,12 @@ let create source_opt => {
| None => SourceFile.empty
| Some source => source
};
{source, node_map: Procname.Hash.create 3}
{source, node_map: Typ.Procname.Hash.create 3}
};
let add_node g n defined::defined =>
try {
let info = Procname.Hash.find g.node_map n;
let info = Typ.Procname.Hash.find g.node_map n;
/* defined and disabled only go from false to true
to avoid accidental overwrite to false by calling add_edge */
if defined {
@ -67,19 +67,19 @@ let add_node g n defined::defined =>
| Not_found =>
let info = {
defined,
parents: Procname.Set.empty,
children: Procname.Set.empty,
parents: Typ.Procname.Set.empty,
children: Typ.Procname.Set.empty,
ancestors: None,
heirs: None,
recursive_dependents: None,
in_out_calls: None
};
Procname.Hash.add g.node_map n info
Typ.Procname.Hash.add g.node_map n info
};
let remove_node_defined g n =>
try {
let info = Procname.Hash.find g.node_map n;
let info = Typ.Procname.Hash.find g.node_map n;
info.defined = false
} {
| Not_found => ()
@ -90,20 +90,20 @@ let add_defined_node g n => add_node g n defined::true;
/** Compute the ancestors of the node, if not already computed */
let compute_ancestors g node => {
let todo = ref (Procname.Set.singleton node);
let seen = ref Procname.Set.empty;
let result = ref Procname.Set.empty;
while (not (Procname.Set.is_empty !todo)) {
let current = Procname.Set.choose !todo;
todo := Procname.Set.remove current !todo;
if (not (Procname.Set.mem current !seen)) {
seen := Procname.Set.add current !seen;
let info = Procname.Hash.find g current;
let todo = ref (Typ.Procname.Set.singleton node);
let seen = ref Typ.Procname.Set.empty;
let result = ref Typ.Procname.Set.empty;
while (not (Typ.Procname.Set.is_empty !todo)) {
let current = Typ.Procname.Set.choose !todo;
todo := Typ.Procname.Set.remove current !todo;
if (not (Typ.Procname.Set.mem current !seen)) {
seen := Typ.Procname.Set.add current !seen;
let info = Typ.Procname.Hash.find g current;
switch info.ancestors {
| Some ancestors => result := Procname.Set.union !result ancestors
| Some ancestors => result := Typ.Procname.Set.union !result ancestors
| None =>
result := Procname.Set.union !result info.parents;
todo := Procname.Set.union !todo info.parents
result := Typ.Procname.Set.union !result info.parents;
todo := Typ.Procname.Set.union !todo info.parents
}
}
};
@ -113,20 +113,20 @@ let compute_ancestors g node => {
/** Compute the heirs of the node, if not already computed */
let compute_heirs g node => {
let todo = ref (Procname.Set.singleton node);
let seen = ref Procname.Set.empty;
let result = ref Procname.Set.empty;
while (not (Procname.Set.is_empty !todo)) {
let current = Procname.Set.choose !todo;
todo := Procname.Set.remove current !todo;
if (not (Procname.Set.mem current !seen)) {
seen := Procname.Set.add current !seen;
let info = Procname.Hash.find g current;
let todo = ref (Typ.Procname.Set.singleton node);
let seen = ref Typ.Procname.Set.empty;
let result = ref Typ.Procname.Set.empty;
while (not (Typ.Procname.Set.is_empty !todo)) {
let current = Typ.Procname.Set.choose !todo;
todo := Typ.Procname.Set.remove current !todo;
if (not (Typ.Procname.Set.mem current !seen)) {
seen := Typ.Procname.Set.add current !seen;
let info = Typ.Procname.Hash.find g current;
switch info.heirs {
| Some heirs => result := Procname.Set.union !result heirs
| Some heirs => result := Typ.Procname.Set.union !result heirs
| None =>
result := Procname.Set.union !result info.children;
todo := Procname.Set.union !todo info.children
result := Typ.Procname.Set.union !result info.children;
todo := Typ.Procname.Set.union !todo info.children
}
}
};
@ -136,14 +136,14 @@ let compute_heirs g node => {
/** Compute the ancestors of the node, if not pre-computed already */
let get_ancestors (g: t) node => {
let info = Procname.Hash.find g.node_map node;
let info = Typ.Procname.Hash.find g.node_map node;
switch info.ancestors {
| None =>
let ancestors = compute_ancestors g.node_map node;
info.ancestors = Some ancestors;
let size = Procname.Set.cardinal ancestors;
let size = Typ.Procname.Set.cardinal ancestors;
if (size > 1000) {
L.err "%a has %d ancestors@." Procname.pp node size
L.err "%a has %d ancestors@." Typ.Procname.pp node size
};
ancestors
| Some ancestors => ancestors
@ -153,14 +153,14 @@ let get_ancestors (g: t) node => {
/** Compute the heirs of the node, if not pre-computed already */
let get_heirs (g: t) node => {
let info = Procname.Hash.find g.node_map node;
let info = Typ.Procname.Hash.find g.node_map node;
switch info.heirs {
| None =>
let heirs = compute_heirs g.node_map node;
info.heirs = Some heirs;
let size = Procname.Set.cardinal heirs;
let size = Typ.Procname.Set.cardinal heirs;
if (size > 1000) {
L.err "%a has %d heirs@." Procname.pp node size
L.err "%a has %d heirs@." Typ.Procname.pp node size
};
heirs
| Some heirs => heirs
@ -169,7 +169,7 @@ let get_heirs (g: t) node => {
let node_defined (g: t) n =>
try {
let info = Procname.Hash.find g.node_map n;
let info = Typ.Procname.Hash.find g.node_map n;
info.defined
} {
| Not_found => false
@ -178,37 +178,37 @@ let node_defined (g: t) n =>
let add_edge g nfrom nto => {
add_node g nfrom defined::false;
add_node g nto defined::false;
let info_from = Procname.Hash.find g.node_map nfrom;
let info_to = Procname.Hash.find g.node_map nto;
info_from.children = Procname.Set.add nto info_from.children;
info_to.parents = Procname.Set.add nfrom info_to.parents
let info_from = Typ.Procname.Hash.find g.node_map nfrom;
let info_to = Typ.Procname.Hash.find g.node_map nto;
info_from.children = Typ.Procname.Set.add nto info_from.children;
info_to.parents = Typ.Procname.Set.add nfrom info_to.parents
};
/** iterate over the elements of a node_map in node order */
let node_map_iter f g => {
let table = ref [];
Procname.Hash.iter (fun node info => table := [(node, info), ...!table]) g.node_map;
let cmp (n1: Procname.t, _) (n2: Procname.t, _) => Procname.compare n1 n2;
Typ.Procname.Hash.iter (fun node info => table := [(node, info), ...!table]) g.node_map;
let cmp (n1: Typ.Procname.t, _) (n2: Typ.Procname.t, _) => Typ.Procname.compare n1 n2;
List.iter f::(fun (n, info) => f n info) (List.sort cmp::cmp !table)
};
let get_nodes (g: t) => {
let nodes = ref Procname.Set.empty;
let f node _ => nodes := Procname.Set.add node !nodes;
let nodes = ref Typ.Procname.Set.empty;
let f node _ => nodes := Typ.Procname.Set.add node !nodes;
node_map_iter f g;
!nodes
};
let compute_calls g node => {
in_calls: Procname.Set.cardinal (get_ancestors g node),
out_calls: Procname.Set.cardinal (get_heirs g node)
in_calls: Typ.Procname.Set.cardinal (get_ancestors g node),
out_calls: Typ.Procname.Set.cardinal (get_heirs g node)
};
/** Compute the calls of the node, if not pre-computed already */
let get_calls (g: t) node => {
let info = Procname.Hash.find g.node_map node;
let info = Typ.Procname.Hash.find g.node_map node;
switch info.in_out_calls {
| None =>
let calls = compute_calls g node;
@ -219,19 +219,19 @@ let get_calls (g: t) node => {
};
let get_all_nodes (g: t) => {
let nodes = Procname.Set.elements (get_nodes g);
let nodes = Typ.Procname.Set.elements (get_nodes g);
List.map f::(fun node => (node, get_calls g node)) nodes
};
let get_nodes_and_calls (g: t) =>
List.filter f::(fun (n, _) => node_defined g n) (get_all_nodes g);
let node_get_num_ancestors g n => (n, Procname.Set.cardinal (get_ancestors g n));
let node_get_num_ancestors g n => (n, Typ.Procname.Set.cardinal (get_ancestors g n));
let get_edges (g: t) :list ((node, int), (node, int)) => {
let edges = ref [];
let f node info =>
Procname.Set.iter
Typ.Procname.Set.iter
(
fun nto =>
edges := [(node_get_num_ancestors g node, node_get_num_ancestors g nto), ...!edges]
@ -243,42 +243,43 @@ let get_edges (g: t) :list ((node, int), (node, int)) => {
/** Return all the children of [n], whether defined or not */
let get_all_children (g: t) n => (Procname.Hash.find g.node_map n).children;
let get_all_children (g: t) n => (Typ.Procname.Hash.find g.node_map n).children;
/** Return the children of [n] which are defined */
let get_defined_children (g: t) n => Procname.Set.filter (node_defined g) (get_all_children g n);
let get_defined_children (g: t) n =>
Typ.Procname.Set.filter (node_defined g) (get_all_children g n);
/** Return the parents of [n] */
let get_parents (g: t) n => (Procname.Hash.find g.node_map n).parents;
let get_parents (g: t) n => (Typ.Procname.Hash.find g.node_map n).parents;
/** Check if [source] recursively calls [dest] */
let calls_recursively (g: t) source dest => Procname.Set.mem source (get_ancestors g dest);
let calls_recursively (g: t) source dest => Typ.Procname.Set.mem source (get_ancestors g dest);
/** Return the children of [n] which are not heirs of [n] */
let get_nonrecursive_dependents (g: t) n => {
let is_not_recursive pn => not (Procname.Set.mem pn (get_ancestors g n));
let res0 = Procname.Set.filter is_not_recursive (get_all_children g n);
let res = Procname.Set.filter (node_defined g) res0;
let is_not_recursive pn => not (Typ.Procname.Set.mem pn (get_ancestors g n));
let res0 = Typ.Procname.Set.filter is_not_recursive (get_all_children g n);
let res = Typ.Procname.Set.filter (node_defined g) res0;
res
};
/** Return the ancestors of [n] which are also heirs of [n] */
let compute_recursive_dependents (g: t) n => {
let reached_from_n pn => Procname.Set.mem n (get_ancestors g pn);
let res0 = Procname.Set.filter reached_from_n (get_ancestors g n);
let res = Procname.Set.filter (node_defined g) res0;
let reached_from_n pn => Typ.Procname.Set.mem n (get_ancestors g pn);
let res0 = Typ.Procname.Set.filter reached_from_n (get_ancestors g n);
let res = Typ.Procname.Set.filter (node_defined g) res0;
res
};
/** Compute the ancestors of [n] which are also heirs of [n], if not pre-computed already */
let get_recursive_dependents (g: t) n => {
let info = Procname.Hash.find g.node_map n;
let info = Typ.Procname.Hash.find g.node_map n;
switch info.recursive_dependents {
| None =>
let recursive_dependents = compute_recursive_dependents g n;
@ -291,21 +292,21 @@ let get_recursive_dependents (g: t) n => {
/** Return the nodes dependent on [n] */
let get_dependents (g: t) n =>
Procname.Set.union (get_nonrecursive_dependents g n) (get_recursive_dependents g n);
Typ.Procname.Set.union (get_nonrecursive_dependents g n) (get_recursive_dependents g n);
/** Return all the nodes with their defined children */
let get_nodes_and_defined_children (g: t) => {
let nodes = ref Procname.Set.empty;
let nodes = ref Typ.Procname.Set.empty;
node_map_iter
(
fun n info =>
if info.defined {
nodes := Procname.Set.add n !nodes
nodes := Typ.Procname.Set.add n !nodes
}
)
g;
let nodes_list = Procname.Set.elements !nodes;
let nodes_list = Typ.Procname.Set.elements !nodes;
List.map f::(fun n => (n, get_defined_children g n)) nodes_list
};
@ -321,7 +322,7 @@ let get_nodes_and_edges (g: t) :nodes_and_edges => {
let do_children node nto => edges := [(node, nto), ...!edges];
let f node info => {
nodes := [(node, info.defined), ...!nodes];
Procname.Set.iter (do_children node) info.children
Typ.Procname.Set.iter (do_children node) info.children
};
node_map_iter f g;
(!nodes, !edges)
@ -395,12 +396,12 @@ let pp_graph_dotty get_specs (g: t) fmt => {
} else {
"diamond"
};
let pp_node fmt (n, _) => F.fprintf fmt "\"%s\"" (Procname.to_filename n);
let pp_node fmt (n, _) => F.fprintf fmt "\"%s\"" (Typ.Procname.to_filename n);
let pp_node_label fmt (n, calls) =>
F.fprintf
fmt
"\"%a | calls=%d %d | specs=%d)\""
Procname.pp
Typ.Procname.pp
n
calls.in_calls
calls.out_calls

@ -19,7 +19,7 @@ type in_out_calls = {
type t; /** the type of a call graph */
/** A call graph consists of a set of nodes (Procname.t), and edges between them.
/** A call graph consists of a set of nodes (Typ.Procname.t), and edges between them.
A node can be defined or undefined (to represent whether we have code for it).
In an edge from [n1] to [n2], indicating that [n1] calls [n2],
[n1] is the parent and [n2] is the child.
@ -28,15 +28,15 @@ type t; /** the type of a call graph */
/** [add_edge cg f t] adds an edge from [f] to [t] in the call graph [cg].
The nodes are also added as undefined, unless already present. */
let add_edge: t => Procname.t => Procname.t => unit;
let add_edge: t => Typ.Procname.t => Typ.Procname.t => unit;
/** Add a node to the call graph as defined */
let add_defined_node: t => Procname.t => unit;
let add_defined_node: t => Typ.Procname.t => unit;
/** Check if [source] recursively calls [dest] */
let calls_recursively: t => Procname.t => Procname.t => bool;
let calls_recursively: t => Typ.Procname.t => Typ.Procname.t => bool;
/** Create an empty call graph */
@ -49,55 +49,55 @@ let extend: t => t => unit;
/** Return all the children of [n], whether defined or not */
let get_all_children: t => Procname.t => Procname.Set.t;
let get_all_children: t => Typ.Procname.t => Typ.Procname.Set.t;
/** Compute the ancestors of the node, if not pre-computed already */
let get_ancestors: t => Procname.t => Procname.Set.t;
let get_ancestors: t => Typ.Procname.t => Typ.Procname.Set.t;
/** Compute the heirs of the node, if not pre-computed already */
let get_heirs: t => Procname.t => Procname.Set.t;
let get_heirs: t => Typ.Procname.t => Typ.Procname.Set.t;
/** Return the in/out calls of the node */
let get_calls: t => Procname.t => in_out_calls;
let get_calls: t => Typ.Procname.t => in_out_calls;
/** Return the list of nodes which are defined */
let get_defined_nodes: t => list Procname.t;
let get_defined_nodes: t => list Typ.Procname.t;
/** Return the children of [n] which are defined */
let get_defined_children: t => Procname.t => Procname.Set.t;
let get_defined_children: t => Typ.Procname.t => Typ.Procname.Set.t;
/** Return the nodes dependent on [n] */
let get_dependents: t => Procname.t => Procname.Set.t;
let get_dependents: t => Typ.Procname.t => Typ.Procname.Set.t;
/** Return the list of nodes with calls */
let get_nodes_and_calls: t => list (Procname.t, in_out_calls);
let get_nodes_and_calls: t => list (Typ.Procname.t, in_out_calls);
/** Return all the nodes with their defined children */
let get_nodes_and_defined_children: t => list (Procname.t, Procname.Set.t);
let get_nodes_and_defined_children: t => list (Typ.Procname.t, Typ.Procname.Set.t);
/** Return the list of nodes, with defined flag, and the list of edges */
let get_nodes_and_edges: t => (list (Procname.t, bool), list (Procname.t, Procname.t));
let get_nodes_and_edges: t => (list (Typ.Procname.t, bool), list (Typ.Procname.t, Typ.Procname.t));
/** Return the children of [n] which are not heirs of [n] and are defined */
let get_nonrecursive_dependents: t => Procname.t => Procname.Set.t;
let get_nonrecursive_dependents: t => Typ.Procname.t => Typ.Procname.Set.t;
/** Return the parents of [n] */
let get_parents: t => Procname.t => Procname.Set.t;
let get_parents: t => Typ.Procname.t => Typ.Procname.Set.t;
/** Return the ancestors of [n] which are also heirs of [n] */
let get_recursive_dependents: t => Procname.t => Procname.Set.t;
let get_recursive_dependents: t => Typ.Procname.t => Typ.Procname.Set.t;
/** Return the path of the source file */
@ -109,15 +109,15 @@ let load_from_file: DB.filename => option t;
/** Returns true if the node is defined */
let node_defined: t => Procname.t => bool;
let node_defined: t => Typ.Procname.t => bool;
/** Remove the defined flag from a node, if it exists. */
let remove_node_defined: t => Procname.t => unit;
let remove_node_defined: t => Typ.Procname.t => unit;
/** Print the call graph as a dotty file. */
let save_call_graph_dotty: SourceFile.t => (Procname.t => list 'a) => t => unit;
let save_call_graph_dotty: SourceFile.t => (Typ.Procname.t => list 'a) => t => unit;
/** Save a call graph into a file */

@ -17,7 +17,7 @@ let module F = Format;
type t =
| Cint IntLit.t /** integer constants */
| Cfun Procname.t /** function names */
| Cfun Typ.Procname.t /** function names */
| Cstr string /** string constants */
| Cfloat float /** float constants */
| Cclass Ident.name /** class constant */
@ -43,8 +43,8 @@ let pp pe f =>
| Cint i => IntLit.pp f i
| Cfun fn =>
switch pe.Pp.kind {
| HTML => F.fprintf f "_fun_%s" (Escape.escape_xml (Procname.to_string fn))
| _ => F.fprintf f "_fun_%s" (Procname.to_string fn)
| HTML => F.fprintf f "_fun_%s" (Escape.escape_xml (Typ.Procname.to_string fn))
| _ => F.fprintf f "_fun_%s" (Typ.Procname.to_string fn)
}
| Cstr s => F.fprintf f "\"%s\"" (String.escaped s)
| Cfloat v => F.fprintf f "%f" v

@ -19,7 +19,7 @@ let module F = Format;
/** Constants */
type t =
| Cint IntLit.t /** integer constants */
| Cfun Procname.t /** function names */
| Cfun Typ.Procname.t /** function names */
| Cstr string /** string constants */
| Cfloat float /** float constants */
| Cclass Ident.name /** class constant */

@ -47,7 +47,7 @@ let rec to_string =
fun
| Darray de1 de2 => to_string de1 ^ "[" ^ to_string de2 ^ "]"
| Dbinop op de1 de2 => "(" ^ to_string de1 ^ Binop.str Pp.text op ^ to_string de2 ^ ")"
| Dconst (Cfun pn) => Procname.to_simplified_string pn
| Dconst (Cfun pn) => Typ.Procname.to_simplified_string pn
| Dconst c => Const.to_string c
| Dderef de => "*" ^ to_string de
| Dfcall fun_dexp args _ {cf_virtual: isvirtual} => {
@ -65,8 +65,8 @@ let rec to_string =
| Dconst (Cfun pname) => {
let s =
switch pname {
| Procname.Java pname_java => Procname.java_get_method pname_java
| _ => Procname.to_string pname
| Typ.Procname.Java pname_java => Typ.Procname.java_get_method pname_java
| _ => Typ.Procname.to_string pname
};
F.fprintf fmt "%s" s
}

@ -22,7 +22,7 @@ type _ident = Ident.t;
let compare__ident x y => Ident.compare y x;
type closure = {name: Procname.t, captured_vars: list (t, Pvar.t, Typ.t)} [@@deriving compare]
type closure = {name: Typ.Procname.t, captured_vars: list (t, Pvar.t, Typ.t)} [@@deriving compare]
/** dynamically determined length of an array value, if any */
and dynamic_length = option t [@@deriving compare]
/** Program expressions. */

@ -15,7 +15,7 @@ let module L = Logging;
let module F = Format;
type closure = {name: Procname.t, captured_vars: list (t, Pvar.t, Typ.t)} [@@deriving compare]
type closure = {name: Typ.Procname.t, captured_vars: list (t, Pvar.t, Typ.t)} [@@deriving compare]
/** dynamically determined length of an array value, if any */
and dynamic_length = option t [@@deriving compare]
/** Program expressions. */

@ -185,7 +185,7 @@ struct
F.fprintf fmt " %s" pr_str
(** File name for the node, given the procedure name and node id *)
let node_filename pname id = (Procname.to_filename pname) ^ "_node" ^ string_of_int id
let node_filename pname id = (Typ.Procname.to_filename pname) ^ "_node" ^ string_of_int id
(** Print an html link to the given node. *)
let pp_node_link path_to_root pname ~description ~preds ~succs ~exn ~isvisited ~isproof fmt id =
@ -219,7 +219,7 @@ struct
(** Print an html link to the given proc *)
let pp_proc_link path_to_root proc_name fmt text =
pp_link ~path: (path_to_root @ [Procname.to_filename proc_name]) fmt text
pp_link ~path: (path_to_root @ [Typ.Procname.to_filename proc_name]) fmt text
(** Print an html link to the given line number of the current source file *)
let pp_line_link ?(with_name = false) ?(text = None) source path_to_root fmt linenum =

@ -24,7 +24,7 @@ module Html : sig
val modified_during_analysis : SourceFile.t -> DB.Results_dir.path -> bool
(** File name for the node, given the procedure name and node id *)
val node_filename : Procname.t -> int -> string
val node_filename : Typ.Procname.t -> int -> string
(** Open an Html file to append data *)
val open_out : SourceFile.t -> DB.Results_dir.path -> Unix.File_descr.t * Format.formatter
@ -45,13 +45,13 @@ module Html : sig
[path_to_root] is the path to the dir for the procedure in the spec db.
[id] is the node identifier. *)
val pp_node_link :
DB.Results_dir.path -> Procname.t ->
DB.Results_dir.path -> Typ.Procname.t ->
description:string -> preds:int list -> succs:int list -> exn:int list ->
isvisited:bool -> isproof:bool -> Format.formatter -> int -> unit
(** Print an html link to the given proc *)
val pp_proc_link :
DB.Results_dir.path -> Procname.t -> Format.formatter -> string -> unit
DB.Results_dir.path -> Typ.Procname.t -> Format.formatter -> string -> unit
(** Print an html link given node id and session *)
val pp_session_link :

@ -11,18 +11,18 @@
open! IStd
let errLogMap = ref Procname.Map.empty
let errLogMap = ref Typ.Procname.Map.empty
let exists_issues () =
not (Procname.Map.is_empty !errLogMap)
not (Typ.Procname.Map.is_empty !errLogMap)
let get_err_log procname =
try Procname.Map.find procname !errLogMap
try Typ.Procname.Map.find procname !errLogMap
with Not_found ->
let errlog = Errlog.empty () in
errLogMap := Procname.Map.add procname errlog !errLogMap; errlog
errLogMap := Typ.Procname.Map.add procname errlog !errLogMap; errlog
let lint_issues_serializer : (Errlog.t Procname.Map.t) Serialization.serializer =
let lint_issues_serializer : (Errlog.t Typ.Procname.Map.t) Serialization.serializer =
Serialization.create_serializer Serialization.Key.lint_issues
(** Save issues to a file *)
@ -41,7 +41,7 @@ let load_issues_to_errlog_map dir =
let file = DB.filename_from_string (Filename.concat issues_dir issues_file) in
match load_issues file with
| Some map ->
errLogMap := Procname.Map.merge (
errLogMap := Typ.Procname.Map.merge (
fun _ issues1 issues2 ->
match issues1, issues2 with
| Some issues1, Some issues2 ->

@ -11,15 +11,15 @@ open! IStd
(** Module to store a set of issues per procedure *)
val errLogMap : Errlog.t Procname.Map.t ref
val errLogMap : Errlog.t Typ.Procname.Map.t ref
val exists_issues : unit -> bool
(** Save issues to a file *)
val get_err_log : Procname.t -> Errlog.t
val get_err_log : Typ.Procname.t -> Errlog.t
(** Load issues from the given file *)
val store_issues : DB.filename -> Errlog.t Procname.Map.t -> unit
val store_issues : DB.filename -> Errlog.t Typ.Procname.Map.t -> unit
(** Load all the lint issues in the given dir and update the issues map *)
val load_issues_to_errlog_map : string -> unit

@ -230,7 +230,7 @@ let at_line tags loc =
at_line_tag tags Tags.line loc
let call_to tags proc_name =
let proc_name_str = Procname.to_simplified_string proc_name in
let proc_name_str = Typ.Procname.to_simplified_string proc_name in
Tags.add tags Tags.call_procedure proc_name_str;
"call to " ^ proc_name_str
@ -258,10 +258,10 @@ let format_field f =
let format_method pname =
match pname with
| Procname.Java pname_java ->
Procname.java_get_method pname_java
| Typ.Procname.Java pname_java ->
Typ.Procname.java_get_method pname_java
| _ ->
Procname.to_string pname
Typ.Procname.to_string pname
let mem_dyn_allocated = "memory dynamically allocated"
let lock_acquired = "lock acquired"
@ -316,18 +316,18 @@ let deref_str_weak_variable_in_block proc_name_opt nullable_obj_str =
let deref_str_nil_argument_in_variadic_method pn total_args arg_number =
let tags = Tags.create () in
let function_method, nil_null =
if Procname.is_c_method pn then ("method", "nil") else ("function", "null") in
if Typ.Procname.is_c_method pn then ("method", "nil") else ("function", "null") in
let problem_str =
Printf.sprintf
"could be %s which results in a call to %s with %d arguments instead of %d \
(%s indicates that the last argument of this variadic %s has been reached)"
nil_null (Procname.to_simplified_string pn) arg_number (total_args - 1) nil_null function_method in
nil_null (Typ.Procname.to_simplified_string pn) arg_number (total_args - 1) nil_null function_method in
_deref_str_null None problem_str tags
(** dereference strings for an undefined value coming from the given procedure *)
let deref_str_undef (proc_name, loc) =
let tags = Tags.create () in
let proc_name_str = Procname.to_simplified_string proc_name in
let proc_name_str = Typ.Procname.to_simplified_string proc_name in
Tags.add tags Tags.call_procedure proc_name_str;
{ tags = tags;
value_pre = Some (pointer_or_object ());
@ -407,7 +407,7 @@ let deref_str_uninitialized alloc_att_opt =
(** Java unchecked exceptions errors *)
let java_unchecked_exn_desc proc_name exn_name pre_str : error_desc =
{ no_desc with descriptions = [
Procname.to_string proc_name;
Typ.Procname.to_string proc_name;
"can throw " ^ (Typename.name exn_name);
"whenever " ^ pre_str];
}
@ -429,10 +429,10 @@ let desc_context_leak pname context_typ fieldname leak_path : error_desc =
path_prefix ^ context_str in
let preamble =
let pname_str = match pname with
| Procname.Java pname_java ->
| Typ.Procname.Java pname_java ->
Printf.sprintf "%s.%s"
(Procname.java_get_class_name pname_java)
(Procname.java_get_method pname_java)
(Typ.Procname.java_get_class_name pname_java)
(Typ.Procname.java_get_method pname_java)
| _ ->
"" in
"Context " ^ context_str ^ " may leak during method " ^ pname_str ^ ":\n" in
@ -450,7 +450,7 @@ let desc_unsafe_guarded_by_access pname accessed_fld guarded_by_str loc =
guarded_by_str
line_info
guarded_by_str
(Procname.to_string pname)
(Typ.Procname.to_string pname)
annot_str in
{ no_desc with descriptions = [msg]; }
@ -565,13 +565,13 @@ let desc_allocation_mismatch alloc dealloc =
let tag_fun, tag_call, tag_line =
if is_alloc then Tags.alloc_function, Tags.alloc_call, Tags.alloc_line
else Tags.dealloc_function, Tags.dealloc_call, Tags.dealloc_line in
Tags.add tags tag_fun (Procname.to_simplified_string primitive_pname);
Tags.add tags tag_call (Procname.to_simplified_string called_pname);
Tags.add tags tag_fun (Typ.Procname.to_simplified_string primitive_pname);
Tags.add tags tag_call (Typ.Procname.to_simplified_string called_pname);
Tags.add tags tag_line (string_of_int loc.Location.line);
let by_call =
if Procname.equal primitive_pname called_pname then ""
else " by call to " ^ Procname.to_simplified_string called_pname in
"using " ^ Procname.to_simplified_string primitive_pname ^ by_call ^ " " ^ at_line (Tags.create ()) (* ignore the tag *) loc in
if Typ.Procname.equal primitive_pname called_pname then ""
else " by call to " ^ Typ.Procname.to_simplified_string called_pname in
"using " ^ Typ.Procname.to_simplified_string primitive_pname ^ by_call ^ " " ^ at_line (Tags.create ()) (* ignore the tag *) loc in
let description = Format.sprintf
"%s %s is deallocated %s"
mem_dyn_allocated
@ -823,12 +823,12 @@ let desc_unary_minus_applied_to_unsigned_expression expr_str_opt typ_str loc =
let desc_skip_function proc_name =
let tags = Tags.create () in
let proc_name_str = Procname.to_string proc_name in
let proc_name_str = Typ.Procname.to_string proc_name in
Tags.add tags Tags.value proc_name_str;
{ no_desc with descriptions = [proc_name_str]; tags = !tags }
let desc_inherently_dangerous_function proc_name =
let proc_name_str = Procname.to_string proc_name in
let proc_name_str = Typ.Procname.to_string proc_name in
let tags = Tags.create () in
Tags.add tags Tags.value proc_name_str;
{ no_desc with descriptions = [proc_name_str]; tags = !tags }

@ -141,16 +141,16 @@ val error_desc_get_dotty : error_desc -> string option
type deref_str
(** dereference strings for null dereference *)
val deref_str_null : Procname.t option -> deref_str
val deref_str_null : Typ.Procname.t option -> deref_str
(** dereference strings for null dereference due to Nullable annotation *)
val deref_str_nullable : Procname.t option -> string -> deref_str
val deref_str_nullable : Typ.Procname.t option -> string -> deref_str
(** dereference strings for null dereference due to weak captured variable in block *)
val deref_str_weak_variable_in_block : Procname.t option -> string -> deref_str
val deref_str_weak_variable_in_block : Typ.Procname.t option -> string -> deref_str
(** dereference strings for an undefined value coming from the given procedure *)
val deref_str_undef : Procname.t * Location.t -> deref_str
val deref_str_undef : Typ.Procname.t * Location.t -> deref_str
(** dereference strings for a freed pointer dereference *)
val deref_str_freed : PredSymb.res_action -> deref_str
@ -165,7 +165,7 @@ val deref_str_array_bound : IntLit.t option -> IntLit.t option -> deref_str
val deref_str_uninitialized : Sil.atom option -> deref_str
(** dereference strings for nonterminal nil arguments in c/objc variadic methods *)
val deref_str_nil_argument_in_variadic_method : Procname.t -> int -> int -> deref_str
val deref_str_nil_argument_in_variadic_method : Typ.Procname.t -> int -> int -> deref_str
(** dereference strings for a pointer size mismatch *)
val deref_str_pointer_size_mismatch : Typ.t -> Typ.t -> deref_str
@ -188,10 +188,10 @@ val is_field_not_null_checked_desc : error_desc -> bool
val is_parameter_field_not_null_checked_desc : error_desc -> bool
val desc_allocation_mismatch :
Procname.t * Procname.t * Location.t -> Procname.t * Procname.t * Location.t -> error_desc
Typ.Procname.t * Typ.Procname.t * Location.t -> Typ.Procname.t * Typ.Procname.t * Location.t -> error_desc
val desc_class_cast_exception :
Procname.t option -> string -> string -> string option -> Location.t -> error_desc
Typ.Procname.t option -> string -> string -> string option -> Location.t -> error_desc
val desc_comparing_floats_for_equality : Location.t -> error_desc
@ -199,13 +199,13 @@ val desc_condition_is_assignment : Location.t -> error_desc
val desc_condition_always_true_false : IntLit.t -> string option -> Location.t -> error_desc
val desc_deallocate_stack_variable : string -> Procname.t -> Location.t -> error_desc
val desc_deallocate_stack_variable : string -> Typ.Procname.t -> Location.t -> error_desc
val desc_deallocate_static_memory : string -> Procname.t -> Location.t -> error_desc
val desc_deallocate_static_memory : string -> Typ.Procname.t -> Location.t -> error_desc
val desc_divide_by_zero : string -> Location.t -> error_desc
val desc_empty_vector_access : Procname.t option -> string -> Location.t -> error_desc
val desc_empty_vector_access : Typ.Procname.t option -> string -> Location.t -> error_desc
val is_empty_vector_access_desc : error_desc -> bool
@ -219,14 +219,14 @@ val desc_buffer_overrun : string -> string -> error_desc
val desc_null_test_after_dereference : string -> int -> Location.t -> error_desc
val java_unchecked_exn_desc : Procname.t -> Typename.t -> string -> error_desc
val java_unchecked_exn_desc : Typ.Procname.t -> Typename.t -> string -> error_desc
val desc_context_leak :
Procname.t -> Typ.t -> Ident.fieldname ->
Typ.Procname.t -> Typ.t -> Ident.fieldname ->
(Ident.fieldname option * Typ.t) list -> error_desc
val desc_fragment_retains_view :
Typ.t -> Ident.fieldname -> Typ.t -> Procname.t -> error_desc
Typ.t -> Ident.fieldname -> Typ.t -> Typ.Procname.t -> error_desc
(* Create human-readable error description for assertion failures *)
val desc_custom_error : Location.t -> error_desc
@ -236,7 +236,7 @@ type pnm_kind =
| Pnm_bounds
| Pnm_dangling
val desc_precondition_not_met : pnm_kind option -> Procname.t -> Location.t -> error_desc
val desc_precondition_not_met : pnm_kind option -> Typ.Procname.t -> Location.t -> error_desc
val desc_return_expression_required : string -> Location.t -> error_desc
@ -250,21 +250,21 @@ val desc_registered_observer_being_deallocated : Pvar.t -> Location.t -> error_d
val desc_return_statement_missing : Location.t -> error_desc
val desc_return_value_ignored : Procname.t -> Location.t -> error_desc
val desc_return_value_ignored : Typ.Procname.t -> Location.t -> error_desc
val desc_stack_variable_address_escape : string -> string option -> Location.t -> error_desc
val desc_skip_function : Procname.t -> error_desc
val desc_skip_function : Typ.Procname.t -> error_desc
val desc_inherently_dangerous_function : Procname.t -> error_desc
val desc_inherently_dangerous_function : Typ.Procname.t -> error_desc
val desc_unary_minus_applied_to_unsigned_expression :
string option -> string -> Location.t -> error_desc
val desc_unsafe_guarded_by_access :
Procname.t -> Ident.fieldname -> string -> Location.t -> error_desc
Typ.Procname.t -> Ident.fieldname -> string -> Location.t -> error_desc
val desc_tainted_value_reaching_sensitive_function :
PredSymb.taint_kind -> string -> Procname.t -> Procname.t -> Location.t -> error_desc
PredSymb.taint_kind -> string -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> error_desc
val desc_uninitialized_dangling_pointer_deref : deref_str -> string -> Location.t -> error_desc

@ -84,7 +84,7 @@ type dangling_kind =
/** position in a path: proc name, node id */
type path_pos = (Procname.t, int) [@@deriving compare];
type path_pos = (Typ.Procname.t, int) [@@deriving compare];
let equal_path_pos = [%compare.equal : path_pos];
@ -96,14 +96,14 @@ type taint_kind =
| Tk_unknown
[@@deriving compare];
type taint_info = {taint_source: Procname.t, taint_kind: taint_kind} [@@deriving compare];
type taint_info = {taint_source: Typ.Procname.t, taint_kind: taint_kind} [@@deriving compare];
/** acquire/release action on a resource */
type res_action = {
ra_kind: res_act_kind, /** kind of action */
ra_res: resource, /** kind of resource */
ra_pname: Procname.t, /** name of the procedure used to acquire/release the resource */
ra_pname: Typ.Procname.t, /** name of the procedure used to acquire/release the resource */
ra_loc: Location.t, /** location of the acquire/release */
ra_vpath: DecompiledExp.vpath /** vpath of the resource value */
};
@ -139,7 +139,7 @@ type t =
| Aautorelease
| Adangling dangling_kind /** dangling pointer */
/** undefined value obtained by calling the given procedure, plus its return value annots */
| Aundef Procname.t _annot_item _location _path_pos
| Aundef Typ.Procname.t _annot_item _location _path_pos
| Ataint taint_info
| Auntaint taint_info
| Alocked
@ -149,7 +149,7 @@ type t =
/** attributed exp is null due to a call to a method with given path as null receiver */
| Aobjc_null
/** value was returned from a call to the given procedure, plus the annots of the return value */
| Aretval Procname.t Annot.Item.t
| Aretval Typ.Procname.t Annot.Item.t
/** denotes an object registered as an observers to a notification center */
| Aobserver
/** denotes an object unsubscribed from observers of a notification center */
@ -162,19 +162,19 @@ let equal = [%compare.equal : t];
/** name of the allocation function for the given memory kind */
let mem_alloc_pname =
fun
| Mmalloc => Procname.from_string_c_fun "malloc"
| Mnew => Procname.from_string_c_fun "new"
| Mnew_array => Procname.from_string_c_fun "new[]"
| Mobjc => Procname.from_string_c_fun "alloc";
| Mmalloc => Typ.Procname.from_string_c_fun "malloc"
| Mnew => Typ.Procname.from_string_c_fun "new"
| Mnew_array => Typ.Procname.from_string_c_fun "new[]"
| Mobjc => Typ.Procname.from_string_c_fun "alloc";
/** name of the deallocation function for the given memory kind */
let mem_dealloc_pname =
fun
| Mmalloc => Procname.from_string_c_fun "free"
| Mnew => Procname.from_string_c_fun "delete"
| Mnew_array => Procname.from_string_c_fun "delete[]"
| Mobjc => Procname.from_string_c_fun "dealloc";
| Mmalloc => Typ.Procname.from_string_c_fun "free"
| Mnew => Typ.Procname.from_string_c_fun "delete"
| Mnew_array => Typ.Procname.from_string_c_fun "delete[]"
| Mobjc => Typ.Procname.from_string_c_fun "dealloc";
/** Categories of attributes */
@ -244,7 +244,7 @@ let to_string pe =>
};
name ^
Binop.str pe Lt ^
Procname.to_string ra.ra_pname ^
Typ.Procname.to_string ra.ra_pname ^
":" ^ string_of_int ra.ra_loc.Location.line ^ Binop.str pe Gt ^ str_vpath
}
| Aautorelease => "AUTORELEASE"
@ -260,14 +260,14 @@ let to_string pe =>
| Aundef pn _ loc _ =>
"UND" ^
Binop.str pe Lt ^
Procname.to_string pn ^ Binop.str pe Gt ^ ":" ^ string_of_int loc.Location.line
| Ataint {taint_source} => "TAINTED[" ^ Procname.to_string taint_source ^ "]"
Typ.Procname.to_string pn ^ Binop.str pe Gt ^ ":" ^ string_of_int loc.Location.line
| Ataint {taint_source} => "TAINTED[" ^ Typ.Procname.to_string taint_source ^ "]"
| Auntaint _ => "UNTAINTED"
| Alocked => "LOCKED"
| Aunlocked => "UNLOCKED"
| Adiv0 (_, _) => "DIV0"
| Aobjc_null => "OBJC_NULL"
| Aretval pn _ => "RET" ^ Binop.str pe Lt ^ Procname.to_string pn ^ Binop.str pe Gt
| Aretval pn _ => "RET" ^ Binop.str pe Lt ^ Typ.Procname.to_string pn ^ Binop.str pe Gt
| Aobserver => "OBSERVER"
| Aunsubscribed_observer => "UNSUBSCRIBED_OBSERVER";

@ -73,7 +73,7 @@ type dangling_kind =
/** position in a path: proc name, node id */
type path_pos = (Procname.t, int) [@@deriving compare];
type path_pos = (Typ.Procname.t, int) [@@deriving compare];
let equal_path_pos: path_pos => path_pos => bool;
@ -84,14 +84,14 @@ type taint_kind =
| Tk_integrity_annotation
| Tk_unknown;
type taint_info = {taint_source: Procname.t, taint_kind: taint_kind};
type taint_info = {taint_source: Typ.Procname.t, taint_kind: taint_kind};
/** acquire/release action on a resource */
type res_action = {
ra_kind: res_act_kind, /** kind of action */
ra_res: resource, /** kind of resource */
ra_pname: Procname.t, /** name of the procedure used to acquire/release the resource */
ra_pname: Typ.Procname.t, /** name of the procedure used to acquire/release the resource */
ra_loc: Location.t, /** location of the acquire/release */
ra_vpath: DecompiledExp.vpath /** vpath of the resource value */
};
@ -110,7 +110,7 @@ type t =
| Aautorelease
| Adangling dangling_kind /** dangling pointer */
/** undefined value obtained by calling the given procedure, plus its return value annots */
| Aundef Procname.t Annot.Item.t Location.t path_pos
| Aundef Typ.Procname.t Annot.Item.t Location.t path_pos
| Ataint taint_info
| Auntaint taint_info
| Alocked
@ -120,7 +120,7 @@ type t =
/** attributed exp is null due to a call to a method with given path as null receiver */
| Aobjc_null
/** value was returned from a call to the given procedure, plus the annots of the return value */
| Aretval Procname.t Annot.Item.t
| Aretval Typ.Procname.t Annot.Item.t
/** denotes an object registered as an observers to a notification center */
| Aobserver
/** denotes an object unsubscribed from observers of a notification center */
@ -131,11 +131,11 @@ let equal: t => t => bool;
/** name of the allocation function for the given memory kind */
let mem_alloc_pname: mem_kind => Procname.t;
let mem_alloc_pname: mem_kind => Typ.Procname.t;
/** name of the deallocation function for the given memory kind */
let mem_dealloc_pname: mem_kind => Procname.t;
let mem_dealloc_pname: mem_kind => Typ.Procname.t;
/** Categories of attributes */

@ -67,7 +67,7 @@ type t = {
method_annotation: Annot.Method.t, /** annotations for java methods */
objc_accessor: option objc_accessor_type, /** type of ObjC accessor, if any */
proc_flags: proc_flags, /** flags of the procedure */
proc_name: Procname.t, /** name of the procedure */
proc_name: Typ.Procname.t, /** name of the procedure */
ret_type: Typ.t, /** return type */
source_file_captured: SourceFile.t /** source file where the procedure was captured */
}

@ -62,7 +62,7 @@ type t = {
method_annotation: Annot.Method.t, /** annotations for java methods */
objc_accessor: option objc_accessor_type, /** type of ObjC accessor, if any */
proc_flags: proc_flags, /** flags of the procedure */
proc_name: Procname.t, /** name of the procedure */
proc_name: Typ.Procname.t, /** name of the procedure */
ret_type: Typ.t, /** return type */
source_file_captured: SourceFile.t /** source file where the procedure was captured */
}
@ -70,4 +70,4 @@ type t = {
/** Create a proc_attributes with default values. */
let default: Procname.t => Config.language => t;
let default: Typ.Procname.t => Config.language => t;

@ -20,8 +20,8 @@ let module Node = {
type id = int [@@deriving compare];
let equal_id = [%compare.equal : id];
type nodekind =
| Start_node Procname.t
| Exit_node Procname.t
| Start_node Typ.Procname.t
| Exit_node Typ.Procname.t
| Stmt_node string
| Join_node
| Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */
@ -46,7 +46,7 @@ let module Node = {
/** predecessor nodes in the cfg */
mutable preds: list t,
/** name of the procedure the node belongs to */
pname_opt: option Procname.t,
pname_opt: option Typ.Procname.t,
/** successor nodes in the cfg */
mutable succs: list t
};
@ -580,7 +580,7 @@ let pp_objc_accessor fmt accessor =>
let pp_signature fmt pdesc => {
let attributes = get_attributes pdesc;
let pname = get_proc_name pdesc;
let pname_string = Procname.to_string pname;
let pname_string = Typ.Procname.to_string pname;
let defined_string = is_defined pdesc ? "defined" : "undefined";
Format.fprintf
fmt

@ -22,8 +22,8 @@ let module Node: {
/** kind of cfg node */
type nodekind =
| Start_node Procname.t
| Exit_node Procname.t
| Start_node Typ.Procname.t
| Exit_node Typ.Procname.t
| Stmt_node string
| Join_node
| Prune_node bool Sil.if_kind string /** (true/false branch, if_kind, comment) */
@ -50,13 +50,13 @@ let module Node: {
let d_instrs: sub_instrs::bool => option Sil.instr => t => unit;
/** Create a dummy node */
let dummy: option Procname.t => t;
let dummy: option Typ.Procname.t => t;
/** Check if two nodes are equal */
let equal: t => t => bool;
/** Get the list of callee procnames from the node */
let get_callees: t => list Procname.t;
let get_callees: t => list Typ.Procname.t;
/** Return a description of the node */
let get_description: Pp.env => t => string;
@ -90,7 +90,7 @@ let module Node: {
let get_preds: t => list t;
/** Get the name of the procedure the node belongs to */
let get_proc_name: t => Procname.t;
let get_proc_name: t => Typ.Procname.t;
/** Get the predecessor nodes of a node where the given predicate evaluates to true */
let get_sliced_preds: t => (t => bool) => list t;
@ -159,7 +159,7 @@ let did_preanalysis: t => bool;
/** fold over the calls from the procedure: (callee, location) pairs */
let fold_calls: ('a => (Procname.t, Location.t) => 'a) => 'a => t => 'a;
let fold_calls: ('a => (Typ.Procname.t, Location.t) => 'a) => 'a => t => 'a;
/** fold over all nodes and their instructions */
@ -207,7 +207,7 @@ let get_locals: t => list (Mangled.t, Typ.t);
let get_nodes: t => list Node.t;
let get_proc_name: t => Procname.t;
let get_proc_name: t => Typ.Procname.t;
/** Return the return type of the procedure and type string */
@ -239,7 +239,7 @@ let is_java_synchronized: t => bool;
/** iterate over the calls from the procedure: (callee, location) pairs */
let iter_calls: ((Procname.t, Location.t) => unit) => t => unit;
let iter_calls: ((Typ.Procname.t, Location.t) => unit) => t => unit;
/** iterate over all nodes and their instructions */
@ -255,7 +255,7 @@ let iter_slope: (Node.t => unit) => t => unit;
/** iterate over all calls until we reach a branching structure */
let iter_slope_calls: (Procname.t => unit) => t => unit;
let iter_slope_calls: (Typ.Procname.t => unit) => t => unit;
/** iterate between two nodes or until we reach a branching structure */

@ -1,587 +0,0 @@
/*
* Copyright (c) 2009 - 2013 Monoidics ltd.
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
open! IStd;
let module Hashtbl = Caml.Hashtbl;
/** Module for Procedure Names */
let module L = Logging;
let module F = Format;
/* e.g. ("", "int") for primitive types or ("java.io", "PrintWriter") for objects */
type java_type = (option string, string);
/* compare in inverse order */
let compare_java_type (p1, c1) (p2, c2) => [%compare : (string, option string)] (c1, p1) (c2, p2);
type method_kind =
| Non_Static /* in Java, procedures called with invokevirtual, invokespecial, and invokeinterface */
| Static /* in Java, procedures called with invokestatic */
[@@deriving compare];
let equal_method_kind = [%compare.equal : method_kind];
/** Type of java procedure names. */
type java = {
method_name: string,
parameters: list java_type,
class_name: Typename.t,
return_type: option java_type, /* option because constructors have no return type */
kind: method_kind
}
[@@deriving compare];
/** Type of c procedure names. */
type c = (string, option string) [@@deriving compare];
type objc_cpp_method_kind =
| CPPMethod (option string) /** with mangling */
| CPPConstructor (option string, bool) /** with mangling + is it constexpr? */
| ObjCClassMethod
| ObjCInstanceMethod
| ObjCInternalMethod
[@@deriving compare];
/** Type of Objective C and C++ procedure names: method signatures. */
type objc_cpp = {method_name: string, class_name: Typename.t, kind: objc_cpp_method_kind}
[@@deriving compare];
/** Type of Objective C block names. */
type block = string [@@deriving compare];
/** Type of procedure names. */
type t =
| Java java
| C c
| Linters_dummy_method
| Block block
| ObjC_Cpp objc_cpp
[@@deriving compare];
let equal = [%compare.equal : t];
/** Level of verbosity of some to_string functions. */
type detail_level =
| Verbose
| Non_verbose
| Simple
[@@deriving compare];
let equal_detail_level = [%compare.equal : detail_level];
let objc_method_kind_of_bool is_instance =>
if is_instance {ObjCInstanceMethod} else {ObjCClassMethod};
let empty_block = Block "";
let is_verbose v =>
switch v {
| Verbose => true
| _ => false
};
/** A type is a pair (package, type_name) that is translated in a string package.type_name */
let java_type_to_string_verbosity p verbosity =>
switch p {
| (None, typ) => typ
| (Some p, cls) =>
if (is_verbose verbosity) {
p ^ "." ^ cls
} else {
cls
}
};
let java_type_to_string p => java_type_to_string_verbosity p Verbose;
/** Given a list of types, it creates a unique string of types separated by commas */
let rec java_param_list_to_string inputList verbosity =>
switch inputList {
| [] => ""
| [head] => java_type_to_string_verbosity head verbosity
| [head, ...rest] =>
java_type_to_string_verbosity head verbosity ^ "," ^ java_param_list_to_string rest verbosity
};
/** It is the same as java_type_to_string, but Java return types are optional because of constructors without type */
let java_return_type_to_string j verbosity =>
switch j.return_type {
| None => ""
| Some typ => java_type_to_string_verbosity typ verbosity
};
/** Given a package.class_name string, it looks for the latest dot and split the string
in two (package, class_name) */
let split_classname package_classname =>
switch (String.rsplit2 package_classname on::'.') {
| Some (x, y) => (Some x, y)
| None => (None, package_classname)
};
let split_typename typename => split_classname (Typename.name typename);
let from_string_c_fun (s: string) => C (s, None);
let c (plain: string) (mangled: string) => (plain, Some mangled);
let java class_name return_type method_name parameters kind => {
class_name,
return_type,
method_name,
parameters,
kind
};
/** Create an objc procedure name from a class_name and method_name. */
let objc_cpp class_name method_name kind => {class_name, method_name, kind};
let get_default_objc_class_method objc_class => {
let objc_cpp = objc_cpp objc_class "__find_class_" ObjCInternalMethod;
ObjC_Cpp objc_cpp
};
/** Create an objc procedure name from a class_name and method_name. */
let mangled_objc_block name => Block name;
let is_java =
fun
| Java _ => true
| _ => false;
let is_c_method =
fun
| ObjC_Cpp _ => true
| _ => false;
let is_constexpr =
fun
| ObjC_Cpp {kind: CPPConstructor (_, true)} => true
| _ => false;
/** Replace the class name component of a procedure name.
In case of Java, replace package and class name. */
let replace_class t (new_class: Typename.t) =>
switch t {
| Java j => Java {...j, class_name: new_class}
| ObjC_Cpp osig => ObjC_Cpp {...osig, class_name: new_class}
| C _
| Block _
| Linters_dummy_method => t
};
/** Get the class name of a Objective-C/C++ procedure name. */
let objc_cpp_get_class_name objc_cpp => Typename.name objc_cpp.class_name;
let objc_cpp_get_class_type_name objc_cpp => objc_cpp.class_name;
/** Return the package.classname of a java procname. */
let java_get_class_name (j: java) => Typename.name j.class_name;
/** Return the package.classname as a typename of a java procname. */
let java_get_class_type_name (j: java) => j.class_name;
/** Return the class name of a java procedure name. */
let java_get_simple_class_name (j: java) => snd (split_classname (java_get_class_name j));
/** Return the package of a java procname. */
let java_get_package (j: java) => fst (split_classname (java_get_class_name j));
/** Return the method of a java procname. */
let java_get_method (j: java) => j.method_name;
/** Replace the method of a java procname. */
let java_replace_method (j: java) mname => {...j, method_name: mname};
/** Replace the return type of a java procname. */
let java_replace_return_type j ret_type => {...j, return_type: Some ret_type};
/** Replace the parameters of a java procname. */
let java_replace_parameters j parameters => {...j, parameters};
/** Return the method/function of a procname. */
let get_method =
fun
| ObjC_Cpp name => name.method_name
| C (name, _) => name
| Block name => name
| Java j => j.method_name
| Linters_dummy_method => "Linters_dummy_method";
/** Return the language of the procedure. */
let get_language =
fun
| ObjC_Cpp _ => Config.Clang
| C _ => Config.Clang
| Block _ => Config.Clang
| Linters_dummy_method => Config.Clang
| Java _ => Config.Java;
/** Return the return type of a java procname. */
let java_get_return_type (j: java) => java_return_type_to_string j Verbose;
/** Return the parameters of a java procname. */
let java_get_parameters j => j.parameters;
/** Return the parameters of a java procname as strings. */
let java_get_parameters_as_strings j =>
List.map f::(fun param => java_type_to_string param) j.parameters;
/** Return true if the java procedure is static */
let java_is_static =
fun
| Java j => equal_method_kind j.kind Static
| _ => false;
/** Prints a string of a java procname with the given level of verbosity */
let java_to_string withclass::withclass=false (j: java) verbosity =>
switch verbosity {
| Verbose
| Non_verbose =>
/* if verbose, then package.class.method(params): rtype,
else rtype package.class.method(params)
verbose is used for example to create unique filenames, non_verbose to create reports */
let return_type = java_return_type_to_string j verbosity;
let params = java_param_list_to_string j.parameters verbosity;
let class_name = java_type_to_string_verbosity (split_typename j.class_name) verbosity;
let separator =
switch (j.return_type, verbosity) {
| (None, _) => ""
| (Some _, Verbose) => ":"
| _ => " "
};
let output = class_name ^ "." ^ j.method_name ^ "(" ^ params ^ ")";
if (equal_detail_level verbosity Verbose) {
output ^ separator ^ return_type
} else {
return_type ^ separator ^ output
}
| Simple =>
/* methodname(...) or without ... if there are no parameters */
let cls_prefix =
if withclass {
java_type_to_string_verbosity (split_typename j.class_name) verbosity ^ "."
} else {
""
};
let params =
switch j.parameters {
| [] => ""
| _ => "..."
};
let method_name =
if (String.equal j.method_name "<init>") {
java_get_simple_class_name j
} else {
cls_prefix ^ j.method_name
};
method_name ^ "(" ^ params ^ ")"
};
/** Check if the class name is for an anonymous inner class. */
let is_anonymous_inner_class_name class_name => {
let class_name_no_package = snd (split_typename class_name);
switch (String.rsplit2 class_name_no_package on::'$') {
| Some (_, s) =>
let is_int =
try {
ignore (int_of_string (String.strip s));
true
} {
| Failure _ => false
};
is_int
| None => false
}
};
/** Check if the procedure belongs to an anonymous inner class. */
let java_is_anonymous_inner_class =
fun
| Java j => is_anonymous_inner_class_name j.class_name
| _ => false;
/** Check if the last parameter is a hidden inner class, and remove it if present.
This is used in private constructors, where a proxy constructor is generated
with an extra parameter and calls the normal constructor. */
let java_remove_hidden_inner_class_parameter =
fun
| Java js =>
switch (List.rev js.parameters) {
| [(_, s), ...par'] =>
if (is_anonymous_inner_class_name (Typename.Java.from_string s)) {
Some (Java {...js, parameters: List.rev par'})
} else {
None
}
| [] => None
}
| _ => None;
/** Check if the procedure name is an anonymous inner class constructor. */
let java_is_anonymous_inner_class_constructor =
fun
| Java js => is_anonymous_inner_class_name js.class_name
| _ => false;
/** Check if the procedure name is an acess method (e.g. access$100 used to
access private members from a nested class. */
let java_is_access_method =
fun
| Java js =>
switch (String.rsplit2 js.method_name on::'$') {
| Some ("access", s) =>
let is_int =
try {
ignore (int_of_string s);
true
} {
| Failure _ => false
};
is_int
| _ => false
}
| _ => false;
/** Check if the procedure name is of an auto-generated method containing '$'. */
let java_is_autogen_method =
fun
| Java js => String.contains js.method_name '$'
| _ => false;
/** Check if the proc name has the type of a java vararg.
Note: currently only checks that the last argument has type Object[]. */
let java_is_vararg =
fun
| Java js =>
switch (List.rev js.parameters) {
| [(_, "java.lang.Object[]"), ..._] => true
| _ => false
}
| _ => false;
let is_objc_constructor method_name =>
String.equal method_name "new" || String.is_prefix prefix::"init" method_name;
let is_objc_kind =
fun
| ObjCClassMethod
| ObjCInstanceMethod
| ObjCInternalMethod => true
| _ => false;
/** [is_constructor pname] returns true if [pname] is a constructor */
let is_constructor =
fun
| Java js => String.equal js.method_name "<init>"
| ObjC_Cpp {kind: CPPConstructor _} => true
| ObjC_Cpp {kind, method_name} when is_objc_kind kind => is_objc_constructor method_name
| _ => false;
let is_objc_dealloc method_name => String.equal method_name "dealloc";
/** [is_dealloc pname] returns true if [pname] is the dealloc method in Objective-C
TODO: add case for C++ */
let is_destructor =
fun
| ObjC_Cpp name => is_objc_dealloc name.method_name
| _ => false;
let java_is_close =
fun
| Java js => String.equal js.method_name "close"
| _ => false;
/** [is_class_initializer pname] returns true if [pname] is a class initializer */
let is_class_initializer =
fun
| Java js => String.equal js.method_name "<clinit>"
| _ => false;
/** [is_infer_undefined pn] returns true if [pn] is a special Infer undefined proc */
let is_infer_undefined pn =>
switch pn {
| Java j =>
let regexp = Str.regexp "com.facebook.infer.builtins.InferUndefined";
Str.string_match regexp (java_get_class_name j) 0
| _ =>
/* TODO: add cases for obj-c, c, c++ */
false
};
let get_global_name_of_initializer =
fun
| C (name, _) when String.is_prefix prefix::Config.clang_initializer_prefix name => {
let prefix_len = String.length Config.clang_initializer_prefix;
Some (String.sub name pos::prefix_len len::(String.length name - prefix_len))
}
| _ => None;
/** to_string for C_function type */
let to_readable_string (c1, c2) verbose => {
let plain = c1;
if verbose {
switch c2 {
| None => plain
| Some s => plain ^ "{" ^ s ^ "}"
}
} else {
plain
}
};
let c_method_to_string osig detail_level =>
switch detail_level {
| Simple => osig.method_name
| Non_verbose => Typename.name osig.class_name ^ "_" ^ osig.method_name
| Verbose =>
let m_str =
switch osig.kind {
| CPPMethod m =>
"(" ^
(
switch m {
| None => ""
| Some s => s
}
) ^ ")"
| CPPConstructor (m, is_constexpr) =>
"{" ^
(
switch m {
| None => ""
| Some s => s
}
) ^
(if is_constexpr {"|constexpr"} else {""}) ^ "}"
| ObjCClassMethod => "class"
| ObjCInstanceMethod => "instance"
| ObjCInternalMethod => "internal"
};
Typename.name osig.class_name ^ "_" ^ osig.method_name ^ m_str
};
/** Very verbose representation of an existing Procname.t */
let to_unique_id pn =>
switch pn {
| Java j => java_to_string j Verbose
| C (c1, c2) => to_readable_string (c1, c2) true
| ObjC_Cpp osig => c_method_to_string osig Verbose
| Block name => name
| Linters_dummy_method => "Linters_dummy_method"
};
/** Convert a proc name to a string for the user to see */
let to_string p =>
switch p {
| Java j => java_to_string j Non_verbose
| C (c1, c2) => to_readable_string (c1, c2) false
| ObjC_Cpp osig => c_method_to_string osig Non_verbose
| Block name => name
| Linters_dummy_method => to_unique_id p
};
/** Convenient representation of a procname for external tools (e.g. eclipse plugin) */
let to_simplified_string withclass::withclass=false p =>
switch p {
| Java j => java_to_string withclass::withclass j Simple
| C (c1, c2) => to_readable_string (c1, c2) false ^ "()"
| ObjC_Cpp osig => c_method_to_string osig Simple
| Block _ => "block"
| Linters_dummy_method => to_unique_id p
};
/** Convert a proc name to a filename */
let to_filename proc_name =>
Escape.escape_filename @@ SourceFile.append_crc_cutoff @@ to_unique_id proc_name;
/** Pretty print a proc name */
let pp f pn => F.fprintf f "%s" (to_string pn);
/** hash function for procname */
let hash_pname = Hashtbl.hash;
let module Hash = Hashtbl.Make {
type nonrec t = t;
let equal = equal;
let hash = hash_pname;
};
let module Map = Caml.Map.Make {
type nonrec t = t;
let compare = compare;
};
let module Set = Caml.Set.Make {
type nonrec t = t;
let compare = compare;
};
/** Pretty print a set of proc names */
let pp_set fmt set => Set.iter (fun pname => F.fprintf fmt "%a " pp pname) set;
let get_qualifiers pname =>
switch pname {
| C c => fst c |> QualifiedCppName.qualifiers_of_qual_name
| ObjC_Cpp objc_cpp =>
List.append
(QualifiedCppName.qualifiers_of_qual_name (Typename.name objc_cpp.class_name))
[objc_cpp.method_name]
| _ => []
};

@ -1,281 +0,0 @@
/*
* Copyright (c) 2009 - 2013 Monoidics ltd.
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
open! IStd;
/** Module for Procedure Names. */
/** Type of java procedure names. */
type java;
/** Type of c procedure names. */
type c;
/** Type of Objective C and C++ procedure names. */
type objc_cpp;
/** Type of Objective C block names. */
type block;
/** Type of procedure names. */
type t =
| Java java
| C c
| Linters_dummy_method
| Block block
| ObjC_Cpp objc_cpp
[@@deriving compare];
/** Equality for proc names. */
let equal: t => t => bool;
type java_type = (option string, string);
type method_kind =
| Non_Static /* in Java, procedures called with invokevirtual, invokespecial, and invokeinterface */
| Static /* in Java, procedures called with invokestatic */;
type objc_cpp_method_kind =
| CPPMethod (option string) /** with mangling */
| CPPConstructor (option string, bool) /** with mangling + is it constexpr? */
| ObjCClassMethod
| ObjCInstanceMethod
| ObjCInternalMethod;
/** Hash tables with proc names as keys. */
let module Hash: Caml.Hashtbl.S with type key = t;
/** Maps from proc names. */
let module Map: Caml.Map.S with type key = t;
/** Sets of proc names. */
let module Set: Caml.Set.S with type elt = t;
/** Create a C procedure name from plain and mangled name. */
let c: string => string => c;
/** Empty block name. */
let empty_block: t;
/** Convert a string to a proc name. */
let from_string_c_fun: string => t;
/** Return the language of the procedure. */
let get_language: t => Config.language;
/** Return the method/function of a procname. */
let get_method: t => string;
/** Hash function for procname. */
let hash_pname: t => int;
/** Check if a class string is an anoynmous inner class name. */
let is_anonymous_inner_class_name: Typename.t => bool;
/** Check if this is an Objective-C/C++ method name. */
let is_c_method: t => bool;
/** Check if this is a constructor method in Objective-C. */
let is_objc_constructor: string => bool;
/** Check if this is a constructor. */
let is_constructor: t => bool;
/** Check if this is a constexpr function. */
let is_constexpr: t => bool;
/** Check if this is a Java procedure name. */
let is_java: t => bool;
/** Check if this is a dealloc method in Objective-C. */
let is_objc_dealloc: string => bool;
/** Check if this is a dealloc method. */
let is_destructor: t => bool;
/** Create a Java procedure name from its
class_name method_name args_type_name return_type_name method_kind. */
let java: Typename.t => option java_type => string => list java_type => method_kind => java;
/** Replace the parameters of a java procname. */
let java_replace_parameters: java => list java_type => java;
/** Replace the method of a java procname. */
let java_replace_return_type: java => java_type => java;
/** Create an objc block name. */
let mangled_objc_block: string => t;
/** Create an objc procedure name from a class_name and method_name. */
let objc_cpp: Typename.t => string => objc_cpp_method_kind => objc_cpp;
let get_default_objc_class_method: Typename.t => t;
/** Get the class name of a Objective-C/C++ procedure name. */
let objc_cpp_get_class_name: objc_cpp => string;
let objc_cpp_get_class_type_name: objc_cpp => Typename.t;
/** Create ObjC method type from a bool is_instance. */
let objc_method_kind_of_bool: bool => objc_cpp_method_kind;
/** Return the class name of a java procedure name. */
let java_get_class_name: java => string;
/** Return the class name as a typename of a java procedure name. */
let java_get_class_type_name: java => Typename.t;
/** Return the simple class name of a java procedure name. */
let java_get_simple_class_name: java => string;
/** Return the package name of a java procedure name. */
let java_get_package: java => option string;
/** Return the method name of a java procedure name. */
let java_get_method: java => string;
/** Return the return type of a java procedure name. */
let java_get_return_type: java => string;
/** Return the parameters of a java procedure name. */
let java_get_parameters: java => list java_type;
/** Return the parameters of a java procname as strings. */
let java_get_parameters_as_strings: java => list string;
/** Check if the procedure name is an acess method (e.g. access$100 used to
access private members from a nested class. */
let java_is_access_method: t => bool;
/** Check if the procedure name is of an auto-generated method containing '$'. */
let java_is_autogen_method: t => bool;
/** Check if the procedure belongs to an anonymous inner class. */
let java_is_anonymous_inner_class: t => bool;
/** Check if the procedure name is an anonymous inner class constructor. */
let java_is_anonymous_inner_class_constructor: t => bool;
/** Check if the method name is "close". */
let java_is_close: t => bool;
/** Check if the java procedure is static. */
let java_is_static: t => bool;
/** Check if the proc name has the type of a java vararg.
Note: currently only checks that the last argument has type Object[]. */
let java_is_vararg: t => bool;
/** Check if the last parameter is a hidden inner class, and remove it if present.
This is used in private constructors, where a proxy constructor is generated
with an extra parameter and calls the normal constructor. */
let java_remove_hidden_inner_class_parameter: t => option t;
/** Replace the method name of an existing java procname. */
let java_replace_method: java => string => java;
/** Convert a java type to a string. */
let java_type_to_string: java_type => string;
/** Check if this is a class initializer. */
let is_class_initializer: t => bool;
/** Check if this is a special Infer undefined procedure. */
let is_infer_undefined: t => bool;
/** Return the name of the global for which this procedure is the initializer if this is an
initializer, None otherwise. */
let get_global_name_of_initializer: t => option string;
/** Pretty print a proc name. */
let pp: Format.formatter => t => unit;
/** Pretty print a set of proc names. */
let pp_set: Format.formatter => Set.t => unit;
/** Replace the class name component of a procedure name.
In case of Java, replace package and class name. */
let replace_class: t => Typename.t => t;
/** Given a package.class_name string, look for the latest dot and split the string
in two (package, class_name). */
let split_classname: string => (option string, string);
/** Convert a proc name to a string for the user to see. */
let to_string: t => string;
/** Convert a proc name into a easy string for the user to see in an IDE. */
let to_simplified_string: withclass::bool? => t => string;
/** Convert a proc name into a unique identifier. */
let to_unique_id: t => string;
/** Convert a proc name to a filename. */
let to_filename: t => string;
let get_qualifiers: t => list string;

@ -18,10 +18,10 @@ let module F = Format;
/** Kind of global variables */
type pvar_kind =
| Local_var Procname.t /** local variable belonging to a function */
| Callee_var Procname.t /** local variable belonging to a callee */
| Abduced_retvar Procname.t Location.t /** synthetic variable to represent return value */
| Abduced_ref_param Procname.t t Location.t
| Local_var Typ.Procname.t /** local variable belonging to a function */
| Callee_var Typ.Procname.t /** local variable belonging to a callee */
| Abduced_retvar Typ.Procname.t Location.t /** synthetic variable to represent return value */
| Abduced_ref_param Typ.Procname.t t Location.t
/** synthetic variable to represent param passed by reference */
| Global_var (SourceFile.t, bool, bool, bool)
/** global variable: translation unit + is it compile constant? + is it POD? + is it a static
@ -43,25 +43,25 @@ let rec _pp f pv => {
if !Config.pp_simple {
F.fprintf f "%a" Mangled.pp name
} else {
F.fprintf f "%a$%a" Procname.pp n Mangled.pp name
F.fprintf f "%a$%a" Typ.Procname.pp n Mangled.pp name
}
| Callee_var n =>
if !Config.pp_simple {
F.fprintf f "%a|callee" Mangled.pp name
} else {
F.fprintf f "%a$%a|callee" Procname.pp n Mangled.pp name
F.fprintf f "%a$%a|callee" Typ.Procname.pp n Mangled.pp name
}
| Abduced_retvar n l =>
if !Config.pp_simple {
F.fprintf f "%a|abducedRetvar" Mangled.pp name
} else {
F.fprintf f "%a$%a%a|abducedRetvar" Procname.pp n Location.pp l Mangled.pp name
F.fprintf f "%a$%a%a|abducedRetvar" Typ.Procname.pp n Location.pp l Mangled.pp name
}
| Abduced_ref_param n pv l =>
if !Config.pp_simple {
F.fprintf f "%a|%a|abducedRefParam" _pp pv Mangled.pp name
} else {
F.fprintf f "%a$%a%a|abducedRefParam" Procname.pp n Location.pp l Mangled.pp name
F.fprintf f "%a$%a%a|abducedRefParam" Typ.Procname.pp n Location.pp l Mangled.pp name
}
| Global_var (fname, is_const, is_pod, _) =>
F.fprintf
@ -256,7 +256,7 @@ let is_frontend_tmp pvar => {
let name = to_string pvar;
is_sil_tmp name || (
switch pvar.pv_kind {
| Local_var pname => Procname.is_java pname && is_bytecode_tmp name
| Local_var pname => Typ.Procname.is_java pname && is_bytecode_tmp name
| _ => false
}
)
@ -282,7 +282,7 @@ let name_hash (name: Mangled.t) => Hashtbl.hash name;
/** [mk name proc_name] creates a program var with the given function name */
let mk (name: Mangled.t) (proc_name: Procname.t) :t => {
let mk (name: Mangled.t) (proc_name: Typ.Procname.t) :t => {
pv_hash: name_hash name,
pv_name: name,
pv_kind: Local_var proc_name
@ -293,7 +293,7 @@ let get_ret_pvar pname => mk Ident.name_return pname;
/** [mk_callee name proc_name] creates a program var
for a callee function with the given function name */
let mk_callee (name: Mangled.t) (proc_name: Procname.t) :t => {
let mk_callee (name: Mangled.t) (proc_name: Typ.Procname.t) :t => {
pv_hash: name_hash name,
pv_name: name,
pv_kind: Callee_var proc_name
@ -323,13 +323,13 @@ let mk_tmp name pname => {
/** create an abduced return variable for a call to [proc_name] at [loc] */
let mk_abduced_ret (proc_name: Procname.t) (loc: Location.t) :t => {
let name = Mangled.from_string ("$RET_" ^ Procname.to_unique_id proc_name);
let mk_abduced_ret (proc_name: Typ.Procname.t) (loc: Location.t) :t => {
let name = Mangled.from_string ("$RET_" ^ Typ.Procname.to_unique_id proc_name);
{pv_hash: name_hash name, pv_name: name, pv_kind: Abduced_retvar proc_name loc}
};
let mk_abduced_ref_param (proc_name: Procname.t) (pv: t) (loc: Location.t) :t => {
let name = Mangled.from_string ("$REF_PARAM_" ^ Procname.to_unique_id proc_name);
let mk_abduced_ref_param (proc_name: Typ.Procname.t) (pv: t) (loc: Location.t) :t => {
let name = Mangled.from_string ("$REF_PARAM_" ^ Typ.Procname.to_unique_id proc_name);
{pv_hash: name_hash name, pv_name: name, pv_kind: Abduced_ref_param proc_name pv loc}
};
@ -355,7 +355,9 @@ let get_initializer_pname {pv_name, pv_kind} =>
switch pv_kind {
| Global_var _ =>
Some (
Procname.from_string_c_fun (Config.clang_initializer_prefix ^ Mangled.to_string_full pv_name)
Typ.Procname.from_string_c_fun (
Config.clang_initializer_prefix ^ Mangled.to_string_full pv_name
)
)
| _ => None
};

@ -44,7 +44,7 @@ let get_name: t => Mangled.t;
/** [get_ret_pvar proc_name] retuns the return pvar associated with the procedure name */
let get_ret_pvar: Procname.t => t;
let get_ret_pvar: Typ.Procname.t => t;
/** Get a simplified version of the name component of a program variable. */
@ -88,20 +88,20 @@ let is_frontend_tmp: t => bool;
/** [mk name proc_name suffix] creates a program var with the given function name and suffix */
let mk: Mangled.t => Procname.t => t;
let mk: Mangled.t => Typ.Procname.t => t;
/** create an abduced variable for a parameter passed by reference */
let mk_abduced_ref_param: Procname.t => t => Location.t => t;
let mk_abduced_ref_param: Typ.Procname.t => t => Location.t => t;
/** create an abduced return variable for a call to [proc_name] at [loc] */
let mk_abduced_ret: Procname.t => Location.t => t;
let mk_abduced_ret: Typ.Procname.t => Location.t => t;
/** [mk_callee name proc_name] creates a program var
for a callee function with the given function name */
let mk_callee: Mangled.t => Procname.t => t;
let mk_callee: Mangled.t => Typ.Procname.t => t;
/** create a global variable with the given name */
@ -110,7 +110,7 @@ let mk_global:
/** create a fresh temporary variable local to procedure [pname]. for use in the frontends only! */
let mk_tmp: string => Procname.t => t;
let mk_tmp: string => Typ.Procname.t => t;
/** Pretty print a program variable. */
@ -126,7 +126,7 @@ let pp_value: Pp.env => F.formatter => t => unit;
/** Turn an ordinary program variable into a callee program variable */
let to_callee: Procname.t => t => t;
let to_callee: Typ.Procname.t => t => t;
/** Turn a pvar into a seed pvar (which stores the initial value of a stack var) */
@ -152,6 +152,6 @@ let is_pod: t => bool;
/** Get the procname of the initializer function for the given global variable */
let get_initializer_pname: t => option Procname.t;
let get_initializer_pname: t => option Typ.Procname.t;
let module Set: PrettyPrintable.PPSet with type elt = t;

@ -515,7 +515,7 @@ let pp_instr pe0 f instr => {
let is_block_pvar pvar => Typ.has_block_prefix (Mangled.to_string (Pvar.get_name pvar));
/* A block pvar used to explain retain cycles */
let block_pvar = Pvar.mk (Mangled.from_string "block") (Procname.from_string_c_fun "");
let block_pvar = Pvar.mk (Mangled.from_string "block") (Typ.Procname.from_string_c_fun "");
/** Dump an instruction. */

@ -96,20 +96,22 @@ let add tenv name struct_typ => TypenameHash.replace tenv name struct_typ;
let get_overriden_method tenv pname_java => {
let struct_typ_get_method_by_name (struct_typ: Typ.Struct.t) method_name =>
List.find_exn
f::(fun meth => String.equal method_name (Procname.get_method meth)) struct_typ.methods;
f::(fun meth => String.equal method_name (Typ.Procname.get_method meth)) struct_typ.methods;
let rec get_overriden_method_in_supers pname_java supers =>
switch supers {
| [superclass, ...supers_tail] =>
switch (lookup tenv superclass) {
| Some struct_typ =>
try (Some (struct_typ_get_method_by_name struct_typ (Procname.java_get_method pname_java))) {
try (
Some (struct_typ_get_method_by_name struct_typ (Typ.Procname.java_get_method pname_java))
) {
| Not_found => get_overriden_method_in_supers pname_java (supers_tail @ struct_typ.supers)
}
| None => get_overriden_method_in_supers pname_java supers_tail
}
| [] => None
};
switch (lookup tenv (Procname.java_get_class_type_name pname_java)) {
switch (lookup tenv (Typ.Procname.java_get_class_type_name pname_java)) {
| Some {supers} => get_overriden_method_in_supers pname_java supers
| _ => None
}

@ -43,7 +43,7 @@ let mk_struct:
default::Typ.Struct.t? =>
fields::Typ.Struct.fields? =>
statics::Typ.Struct.fields? =>
methods::list Procname.t? =>
methods::list Typ.Procname.t? =>
supers::list Typename.t? =>
annots::Annot.Item.t? =>
specialization::Typ.template_spec_info? =>
@ -64,4 +64,4 @@ let store_to_file: DB.filename => t => unit;
/** Get method that is being overriden by java_pname (if any) **/
let get_overriden_method: t => Procname.java => option Procname.t;
let get_overriden_method: t => Typ.Procname.java => option Typ.Procname.t;

@ -288,14 +288,6 @@ let rec java_from_string =
}
| typ_str => Tstruct (Typename.Java.from_string typ_str);
/** Return the return type of [pname_java]. */
let java_proc_return_typ pname_java =>
switch (java_from_string (Procname.java_get_return_type pname_java)) {
| Tstruct _ as typ => Tptr typ Pk_pointer
| typ => typ
};
type typ = t [@@deriving compare];
/* template instantiation arguments */
@ -304,6 +296,509 @@ type template_spec_info =
| Template (string, list (option t))
[@@deriving compare];
let module Procname = {
/* e.g. ("", "int") for primitive types or ("java.io", "PrintWriter") for objects */
type java_type = (option string, string);
/* compare in inverse order */
let compare_java_type (p1, c1) (p2, c2) =>
[%compare : (string, option string)] (c1, p1) (c2, p2);
type method_kind =
| Non_Static /* in Java, procedures called with invokevirtual, invokespecial, and invokeinterface */
| Static /* in Java, procedures called with invokestatic */
[@@deriving compare];
let equal_method_kind = [%compare.equal : method_kind];
/** Type of java procedure names. */
type java = {
method_name: string,
parameters: list java_type,
class_name: Typename.t,
return_type: option java_type, /* option because constructors have no return type */
kind: method_kind
}
[@@deriving compare];
/** Type of c procedure names. */
type c = (string, option string) [@@deriving compare];
type objc_cpp_method_kind =
| CPPMethod (option string) /** with mangling */
| CPPConstructor (option string, bool) /** with mangling + is it constexpr? */
| ObjCClassMethod
| ObjCInstanceMethod
| ObjCInternalMethod
[@@deriving compare];
/** Type of Objective C and C++ procedure names: method signatures. */
type objc_cpp = {method_name: string, class_name: Typename.t, kind: objc_cpp_method_kind}
[@@deriving compare];
/** Type of Objective C block names. */
type block = string [@@deriving compare];
/** Type of procedure names. */
type t =
| Java java
| C c
| Linters_dummy_method
| Block block
| ObjC_Cpp objc_cpp
[@@deriving compare];
let equal = [%compare.equal : t];
/** Level of verbosity of some to_string functions. */
type detail_level =
| Verbose
| Non_verbose
| Simple
[@@deriving compare];
let equal_detail_level = [%compare.equal : detail_level];
let objc_method_kind_of_bool is_instance =>
if is_instance {ObjCInstanceMethod} else {ObjCClassMethod};
let empty_block = Block "";
let is_verbose v =>
switch v {
| Verbose => true
| _ => false
};
/** A type is a pair (package, type_name) that is translated in a string package.type_name */
let java_type_to_string_verbosity p verbosity =>
switch p {
| (None, typ) => typ
| (Some p, cls) =>
if (is_verbose verbosity) {
p ^ "." ^ cls
} else {
cls
}
};
let java_type_to_string p => java_type_to_string_verbosity p Verbose;
/** Given a list of types, it creates a unique string of types separated by commas */
let rec java_param_list_to_string inputList verbosity =>
switch inputList {
| [] => ""
| [head] => java_type_to_string_verbosity head verbosity
| [head, ...rest] =>
java_type_to_string_verbosity head verbosity ^ "," ^ java_param_list_to_string rest verbosity
};
/** It is the same as java_type_to_string, but Java return types are optional because of constructors without type */
let java_return_type_to_string j verbosity =>
switch j.return_type {
| None => ""
| Some typ => java_type_to_string_verbosity typ verbosity
};
/** Given a package.class_name string, it looks for the latest dot and split the string
in two (package, class_name) */
let split_classname package_classname =>
switch (String.rsplit2 package_classname on::'.') {
| Some (x, y) => (Some x, y)
| None => (None, package_classname)
};
let split_typename typename => split_classname (Typename.name typename);
let from_string_c_fun (s: string) => C (s, None);
let c (plain: string) (mangled: string) => (plain, Some mangled);
let java class_name return_type method_name parameters kind => {
class_name,
return_type,
method_name,
parameters,
kind
};
/** Create an objc procedure name from a class_name and method_name. */
let objc_cpp class_name method_name kind => {class_name, method_name, kind};
let get_default_objc_class_method objc_class => {
let objc_cpp = objc_cpp objc_class "__find_class_" ObjCInternalMethod;
ObjC_Cpp objc_cpp
};
/** Create an objc procedure name from a class_name and method_name. */
let mangled_objc_block name => Block name;
let is_java =
fun
| Java _ => true
| _ => false;
let is_c_method =
fun
| ObjC_Cpp _ => true
| _ => false;
let is_constexpr =
fun
| ObjC_Cpp {kind: CPPConstructor (_, true)} => true
| _ => false;
/** Replace the class name component of a procedure name.
In case of Java, replace package and class name. */
let replace_class t (new_class: Typename.t) =>
switch t {
| Java j => Java {...j, class_name: new_class}
| ObjC_Cpp osig => ObjC_Cpp {...osig, class_name: new_class}
| C _
| Block _
| Linters_dummy_method => t
};
/** Get the class name of a Objective-C/C++ procedure name. */
let objc_cpp_get_class_name objc_cpp => Typename.name objc_cpp.class_name;
let objc_cpp_get_class_type_name objc_cpp => objc_cpp.class_name;
/** Return the package.classname of a java procname. */
let java_get_class_name (j: java) => Typename.name j.class_name;
/** Return the package.classname as a typename of a java procname. */
let java_get_class_type_name (j: java) => j.class_name;
/** Return the class name of a java procedure name. */
let java_get_simple_class_name (j: java) => snd (split_classname (java_get_class_name j));
/** Return the package of a java procname. */
let java_get_package (j: java) => fst (split_classname (java_get_class_name j));
/** Return the method of a java procname. */
let java_get_method (j: java) => j.method_name;
/** Replace the method of a java procname. */
let java_replace_method (j: java) mname => {...j, method_name: mname};
/** Replace the return type of a java procname. */
let java_replace_return_type j ret_type => {...j, return_type: Some ret_type};
/** Replace the parameters of a java procname. */
let java_replace_parameters j parameters => {...j, parameters};
/** Return the method/function of a procname. */
let get_method =
fun
| ObjC_Cpp name => name.method_name
| C (name, _) => name
| Block name => name
| Java j => j.method_name
| Linters_dummy_method => "Linters_dummy_method";
/** Return the language of the procedure. */
let get_language =
fun
| ObjC_Cpp _ => Config.Clang
| C _ => Config.Clang
| Block _ => Config.Clang
| Linters_dummy_method => Config.Clang
| Java _ => Config.Java;
/** Return the return type of a java procname. */
let java_get_return_type (j: java) => java_return_type_to_string j Verbose;
/** Return the parameters of a java procname. */
let java_get_parameters j => j.parameters;
/** Return the parameters of a java procname as strings. */
let java_get_parameters_as_strings j =>
List.map f::(fun param => java_type_to_string param) j.parameters;
/** Return true if the java procedure is static */
let java_is_static =
fun
| Java j => equal_method_kind j.kind Static
| _ => false;
/** Prints a string of a java procname with the given level of verbosity */
let java_to_string withclass::withclass=false (j: java) verbosity =>
switch verbosity {
| Verbose
| Non_verbose =>
/* if verbose, then package.class.method(params): rtype,
else rtype package.class.method(params)
verbose is used for example to create unique filenames, non_verbose to create reports */
let return_type = java_return_type_to_string j verbosity;
let params = java_param_list_to_string j.parameters verbosity;
let class_name = java_type_to_string_verbosity (split_typename j.class_name) verbosity;
let separator =
switch (j.return_type, verbosity) {
| (None, _) => ""
| (Some _, Verbose) => ":"
| _ => " "
};
let output = class_name ^ "." ^ j.method_name ^ "(" ^ params ^ ")";
if (equal_detail_level verbosity Verbose) {
output ^ separator ^ return_type
} else {
return_type ^ separator ^ output
}
| Simple =>
/* methodname(...) or without ... if there are no parameters */
let cls_prefix =
if withclass {
java_type_to_string_verbosity (split_typename j.class_name) verbosity ^ "."
} else {
""
};
let params =
switch j.parameters {
| [] => ""
| _ => "..."
};
let method_name =
if (String.equal j.method_name "<init>") {
java_get_simple_class_name j
} else {
cls_prefix ^ j.method_name
};
method_name ^ "(" ^ params ^ ")"
};
/** Check if the class name is for an anonymous inner class. */
let is_anonymous_inner_class_name class_name => {
let class_name_no_package = snd (split_typename class_name);
switch (String.rsplit2 class_name_no_package on::'$') {
| Some (_, s) =>
let is_int =
try {
ignore (int_of_string (String.strip s));
true
} {
| Failure _ => false
};
is_int
| None => false
}
};
/** Check if the procedure belongs to an anonymous inner class. */
let java_is_anonymous_inner_class =
fun
| Java j => is_anonymous_inner_class_name j.class_name
| _ => false;
/** Check if the last parameter is a hidden inner class, and remove it if present.
This is used in private constructors, where a proxy constructor is generated
with an extra parameter and calls the normal constructor. */
let java_remove_hidden_inner_class_parameter =
fun
| Java js =>
switch (List.rev js.parameters) {
| [(_, s), ...par'] =>
if (is_anonymous_inner_class_name (Typename.Java.from_string s)) {
Some (Java {...js, parameters: List.rev par'})
} else {
None
}
| [] => None
}
| _ => None;
/** Check if the procedure name is an anonymous inner class constructor. */
let java_is_anonymous_inner_class_constructor =
fun
| Java js => is_anonymous_inner_class_name js.class_name
| _ => false;
/** Check if the procedure name is an acess method (e.g. access$100 used to
access private members from a nested class. */
let java_is_access_method =
fun
| Java js =>
switch (String.rsplit2 js.method_name on::'$') {
| Some ("access", s) =>
let is_int =
try {
ignore (int_of_string s);
true
} {
| Failure _ => false
};
is_int
| _ => false
}
| _ => false;
/** Check if the procedure name is of an auto-generated method containing '$'. */
let java_is_autogen_method =
fun
| Java js => String.contains js.method_name '$'
| _ => false;
/** Check if the proc name has the type of a java vararg.
Note: currently only checks that the last argument has type Object[]. */
let java_is_vararg =
fun
| Java js =>
switch (List.rev js.parameters) {
| [(_, "java.lang.Object[]"), ..._] => true
| _ => false
}
| _ => false;
let is_objc_constructor method_name =>
String.equal method_name "new" || String.is_prefix prefix::"init" method_name;
let is_objc_kind =
fun
| ObjCClassMethod
| ObjCInstanceMethod
| ObjCInternalMethod => true
| _ => false;
/** [is_constructor pname] returns true if [pname] is a constructor */
let is_constructor =
fun
| Java js => String.equal js.method_name "<init>"
| ObjC_Cpp {kind: CPPConstructor _} => true
| ObjC_Cpp {kind, method_name} when is_objc_kind kind => is_objc_constructor method_name
| _ => false;
let is_objc_dealloc method_name => String.equal method_name "dealloc";
/** [is_dealloc pname] returns true if [pname] is the dealloc method in Objective-C
TODO: add case for C++ */
let is_destructor =
fun
| ObjC_Cpp name => is_objc_dealloc name.method_name
| _ => false;
let java_is_close =
fun
| Java js => String.equal js.method_name "close"
| _ => false;
/** [is_class_initializer pname] returns true if [pname] is a class initializer */
let is_class_initializer =
fun
| Java js => String.equal js.method_name "<clinit>"
| _ => false;
/** [is_infer_undefined pn] returns true if [pn] is a special Infer undefined proc */
let is_infer_undefined pn =>
switch pn {
| Java j =>
let regexp = Str.regexp "com.facebook.infer.builtins.InferUndefined";
Str.string_match regexp (java_get_class_name j) 0
| _ =>
/* TODO: add cases for obj-c, c, c++ */
false
};
let get_global_name_of_initializer =
fun
| C (name, _) when String.is_prefix prefix::Config.clang_initializer_prefix name => {
let prefix_len = String.length Config.clang_initializer_prefix;
Some (String.sub name pos::prefix_len len::(String.length name - prefix_len))
}
| _ => None;
/** to_string for C_function type */
let to_readable_string (c1, c2) verbose => {
let plain = c1;
if verbose {
switch c2 {
| None => plain
| Some s => plain ^ "{" ^ s ^ "}"
}
} else {
plain
}
};
let c_method_to_string osig detail_level =>
switch detail_level {
| Simple => osig.method_name
| Non_verbose => Typename.name osig.class_name ^ "_" ^ osig.method_name
| Verbose =>
let m_str =
switch osig.kind {
| CPPMethod m =>
"(" ^
(
switch m {
| None => ""
| Some s => s
}
) ^ ")"
| CPPConstructor (m, is_constexpr) =>
"{" ^
(
switch m {
| None => ""
| Some s => s
}
) ^
(if is_constexpr {"|constexpr"} else {""}) ^ "}"
| ObjCClassMethod => "class"
| ObjCInstanceMethod => "instance"
| ObjCInternalMethod => "internal"
};
Typename.name osig.class_name ^ "_" ^ osig.method_name ^ m_str
};
/** Very verbose representation of an existing Procname.t */
let to_unique_id pn =>
switch pn {
| Java j => java_to_string j Verbose
| C (c1, c2) => to_readable_string (c1, c2) true
| ObjC_Cpp osig => c_method_to_string osig Verbose
| Block name => name
| Linters_dummy_method => "Linters_dummy_method"
};
/** Convert a proc name to a string for the user to see */
let to_string p =>
switch p {
| Java j => java_to_string j Non_verbose
| C (c1, c2) => to_readable_string (c1, c2) false
| ObjC_Cpp osig => c_method_to_string osig Non_verbose
| Block name => name
| Linters_dummy_method => to_unique_id p
};
/** Convenient representation of a procname for external tools (e.g. eclipse plugin) */
let to_simplified_string withclass::withclass=false p =>
switch p {
| Java j => java_to_string withclass::withclass j Simple
| C (c1, c2) => to_readable_string (c1, c2) false ^ "()"
| ObjC_Cpp osig => c_method_to_string osig Simple
| Block _ => "block"
| Linters_dummy_method => to_unique_id p
};
/** Convert a proc name to a filename */
let to_filename proc_name =>
Escape.escape_filename @@ SourceFile.append_crc_cutoff @@ to_unique_id proc_name;
/** Pretty print a proc name */
let pp f pn => F.fprintf f "%s" (to_string pn);
/** hash function for procname */
let hash_pname = Hashtbl.hash;
let module Hash = Hashtbl.Make {
type nonrec t = t;
let equal = equal;
let hash = hash_pname;
};
let module Map = Caml.Map.Make {
type nonrec t = t;
let compare = compare;
};
let module Set = Caml.Set.Make {
type nonrec t = t;
let compare = compare;
};
/** Pretty print a set of proc names */
let pp_set fmt set => Set.iter (fun pname => F.fprintf fmt "%a " pp pname) set;
let get_qualifiers pname =>
switch pname {
| C c => fst c |> QualifiedCppName.qualifiers_of_qual_name
| ObjC_Cpp objc_cpp =>
List.append
(QualifiedCppName.qualifiers_of_qual_name (Typename.name objc_cpp.class_name))
[objc_cpp.method_name]
| _ => []
};
};
/** Return the return type of [pname_java]. */
let java_proc_return_typ pname_java =>
switch (java_from_string (Procname.java_get_return_type pname_java)) {
| Tstruct _ as typ => Tptr typ Pk_pointer
| typ => typ
};
let module Struct = {
type field = (Ident.fieldname, T.t, Annot.Item.t) [@@deriving compare];
type fields = list field;

@ -148,10 +148,6 @@ let is_block_type: t => bool;
let unsome: string => option t => t;
/** Return the return type of [pname_java]. */
let java_proc_return_typ: Procname.java => t;
type typ = t;
/* template instantiation arguments */
@ -160,6 +156,219 @@ type template_spec_info =
| Template (string, list (option t))
[@@deriving compare];
let module Procname: {
/** Module for Procedure Names. */
/** Type of java procedure names. */
type java;
/** Type of c procedure names. */
type c;
/** Type of Objective C and C++ procedure names. */
type objc_cpp;
/** Type of Objective C block names. */
type block;
/** Type of procedure names. */
type t =
| Java java
| C c
| Linters_dummy_method
| Block block
| ObjC_Cpp objc_cpp
[@@deriving compare];
/** Equality for proc names. */
let equal: t => t => bool;
type java_type = (option string, string);
type method_kind =
| Non_Static /* in Java, procedures called with invokevirtual, invokespecial, and invokeinterface */
| Static /* in Java, procedures called with invokestatic */;
type objc_cpp_method_kind =
| CPPMethod (option string) /** with mangling */
| CPPConstructor (option string, bool) /** with mangling + is it constexpr? */
| ObjCClassMethod
| ObjCInstanceMethod
| ObjCInternalMethod;
/** Hash tables with proc names as keys. */
let module Hash: Caml.Hashtbl.S with type key = t;
/** Maps from proc names. */
let module Map: Caml.Map.S with type key = t;
/** Sets of proc names. */
let module Set: Caml.Set.S with type elt = t;
/** Create a C procedure name from plain and mangled name. */
let c: string => string => c;
/** Empty block name. */
let empty_block: t;
/** Convert a string to a proc name. */
let from_string_c_fun: string => t;
/** Return the language of the procedure. */
let get_language: t => Config.language;
/** Return the method/function of a procname. */
let get_method: t => string;
/** Hash function for procname. */
let hash_pname: t => int;
/** Check if a class string is an anoynmous inner class name. */
let is_anonymous_inner_class_name: Typename.t => bool;
/** Check if this is an Objective-C/C++ method name. */
let is_c_method: t => bool;
/** Check if this is a constructor method in Objective-C. */
let is_objc_constructor: string => bool;
/** Check if this is a constructor. */
let is_constructor: t => bool;
/** Check if this is a constexpr function. */
let is_constexpr: t => bool;
/** Check if this is a Java procedure name. */
let is_java: t => bool;
/** Check if this is a dealloc method in Objective-C. */
let is_objc_dealloc: string => bool;
/** Check if this is a dealloc method. */
let is_destructor: t => bool;
/** Create a Java procedure name from its
class_name method_name args_type_name return_type_name method_kind. */
let java: Typename.t => option java_type => string => list java_type => method_kind => java;
/** Replace the parameters of a java procname. */
let java_replace_parameters: java => list java_type => java;
/** Replace the method of a java procname. */
let java_replace_return_type: java => java_type => java;
/** Create an objc block name. */
let mangled_objc_block: string => t;
/** Create an objc procedure name from a class_name and method_name. */
let objc_cpp: Typename.t => string => objc_cpp_method_kind => objc_cpp;
let get_default_objc_class_method: Typename.t => t;
/** Get the class name of a Objective-C/C++ procedure name. */
let objc_cpp_get_class_name: objc_cpp => string;
let objc_cpp_get_class_type_name: objc_cpp => Typename.t;
/** Create ObjC method type from a bool is_instance. */
let objc_method_kind_of_bool: bool => objc_cpp_method_kind;
/** Return the class name of a java procedure name. */
let java_get_class_name: java => string;
/** Return the class name as a typename of a java procedure name. */
let java_get_class_type_name: java => Typename.t;
/** Return the simple class name of a java procedure name. */
let java_get_simple_class_name: java => string;
/** Return the package name of a java procedure name. */
let java_get_package: java => option string;
/** Return the method name of a java procedure name. */
let java_get_method: java => string;
/** Return the return type of a java procedure name. */
let java_get_return_type: java => string;
/** Return the parameters of a java procedure name. */
let java_get_parameters: java => list java_type;
/** Return the parameters of a java procname as strings. */
let java_get_parameters_as_strings: java => list string;
/** Check if the procedure name is an acess method (e.g. access$100 used to
access private members from a nested class. */
let java_is_access_method: t => bool;
/** Check if the procedure name is of an auto-generated method containing '$'. */
let java_is_autogen_method: t => bool;
/** Check if the procedure belongs to an anonymous inner class. */
let java_is_anonymous_inner_class: t => bool;
/** Check if the procedure name is an anonymous inner class constructor. */
let java_is_anonymous_inner_class_constructor: t => bool;
/** Check if the method name is "close". */
let java_is_close: t => bool;
/** Check if the java procedure is static. */
let java_is_static: t => bool;
/** Check if the proc name has the type of a java vararg.
Note: currently only checks that the last argument has type Object[]. */
let java_is_vararg: t => bool;
/** Check if the last parameter is a hidden inner class, and remove it if present.
This is used in private constructors, where a proxy constructor is generated
with an extra parameter and calls the normal constructor. */
let java_remove_hidden_inner_class_parameter: t => option t;
/** Replace the method name of an existing java procname. */
let java_replace_method: java => string => java;
/** Convert a java type to a string. */
let java_type_to_string: java_type => string;
/** Check if this is a class initializer. */
let is_class_initializer: t => bool;
/** Check if this is a special Infer undefined procedure. */
let is_infer_undefined: t => bool;
/** Return the name of the global for which this procedure is the initializer if this is an
initializer, None otherwise. */
let get_global_name_of_initializer: t => option string;
/** Pretty print a proc name. */
let pp: Format.formatter => t => unit;
/** Pretty print a set of proc names. */
let pp_set: Format.formatter => Set.t => unit;
/** Replace the class name component of a procedure name.
In case of Java, replace package and class name. */
let replace_class: t => Typename.t => t;
/** Given a package.class_name string, look for the latest dot and split the string
in two (package, class_name). */
let split_classname: string => (option string, string);
/** Convert a proc name to a string for the user to see. */
let to_string: t => string;
/** Convert a proc name into a easy string for the user to see in an IDE. */
let to_simplified_string: withclass::bool? => t => string;
/** Convert a proc name into a unique identifier. */
let to_unique_id: t => string;
/** Convert a proc name to a filename. */
let to_filename: t => string;
let get_qualifiers: t => list string;
};
/** Return the return type of [pname_java]. */
let java_proc_return_typ: Procname.java => t;
let module Struct: {
type field = (Ident.fieldname, typ, Annot.Item.t) [@@deriving compare];
type fields = list field;

@ -91,7 +91,7 @@ val nullify_exp_with_objc_null : Tenv.t -> Prop.normal Prop.t -> Exp.t -> Prop.n
(** mark Exp.Var's or Exp.Lvar's as undefined *)
val mark_vars_as_undefined :
Tenv.t -> Prop.normal Prop.t -> Exp.t list -> Procname.t -> Annot.Item.t ->
Tenv.t -> Prop.normal Prop.t -> Exp.t list -> Typ.Procname.t -> Annot.Item.t ->
Location.t -> PredSymb.path_pos -> Prop.normal Prop.t
(** type for arithmetic problems *)

@ -669,7 +669,7 @@ let execute_abort { Builtin.proc_name; }
: Builtin.ret_typ =
raise
(Exceptions.Precondition_not_found
(Localise.verbatim_desc (Procname.to_string proc_name), __POS__))
(Localise.verbatim_desc (Typ.Procname.to_string proc_name), __POS__))
let execute_exit { Builtin.prop_; path; }
: Builtin.ret_typ =
@ -834,7 +834,7 @@ let execute_pthread_create ({ Builtin.tenv; prop_; path; args; } as builtin_args
let fun_string = Mangled.to_string fun_name in
L.d_strln ("pthread_create: calling function " ^ fun_string);
begin
match Specs.get_summary (Procname.from_string_c_fun fun_string) with
match Specs.get_summary (Typ.Procname.from_string_c_fun fun_string) with
| None -> assert false
| Some callee_summary ->
SymExec.proc_call callee_summary

@ -170,8 +170,8 @@ let summary_values summary => {
};
let pp_failure failure => F.asprintf "%a" SymOp.pp_failure_kind failure;
{
vname: Procname.to_string proc_name,
vname_id: Procname.to_filename proc_name,
vname: Typ.Procname.to_string proc_name,
vname_id: Typ.Procname.to_filename proc_name,
vspecs: List.length specs,
vtime: Printf.sprintf "%.0f" stats.Specs.stats_time,
vto: Option.value_map f::pp_failure default::"NONE" stats.Specs.stats_failure,
@ -401,7 +401,7 @@ let module IssuesCsv = {
};
let kind = Exceptions.err_kind_string ekind;
let type_str = Localise.to_string error_name;
let procedure_id = Procname.to_filename procname;
let procedure_id = Typ.Procname.to_filename procname;
let filename = SourceFile.to_string source_file;
let always_report =
switch (Localise.error_desc_extract_tag_value error_desc "always_report") {
@ -416,7 +416,7 @@ let module IssuesCsv = {
pp "\"%s\"," err_desc_string;
pp "%s," severity;
pp "%d," loc.Location.line;
pp "\"%s\"," (Escape.escape_csv (Procname.to_string procname));
pp "\"%s\"," (Escape.escape_csv (Typ.Procname.to_string procname));
pp "\"%s\"," (Escape.escape_csv procedure_id);
pp "%s," filename;
pp "\"%s\"," (Escape.escape_csv trace);
@ -467,7 +467,7 @@ let module IssuesJson = {
) {
let kind = Exceptions.err_kind_string ekind;
let bug_type = Localise.to_string error_name;
let procedure_id = Procname.to_filename procname;
let procedure_id = Typ.Procname.to_filename procname;
let file = SourceFile.to_string source_file;
let json_ml_loc =
switch ml_loc_opt {
@ -485,7 +485,7 @@ let module IssuesJson = {
visibility,
line: loc.Location.line,
column: loc.Location.col,
procedure: Procname.to_string procname,
procedure: Typ.Procname.to_string procname,
procedure_id,
procedure_start_line,
file,
@ -651,8 +651,8 @@ let module IssuesXml = {
let attributes = [("id", string_of_int !xml_issues_id)];
let error_class = Exceptions.err_class_string eclass;
let error_line = string_of_int loc.Location.line;
let procedure_name = Procname.to_string proc_name;
let procedure_id = Procname.to_filename proc_name;
let procedure_name = Typ.Procname.to_string proc_name;
let procedure_id = Typ.Procname.to_filename proc_name;
let filename = SourceFile.to_string source_file;
let bug_hash = get_bug_hash kind type_str procedure_id filename node_key error_desc;
let forest = [
@ -694,10 +694,10 @@ let module CallsCsv = {
let stats = summary.Specs.stats;
let caller_name = Specs.get_proc_name summary;
let do_call (callee_name, loc) trace => {
pp "\"%s\"," (Escape.escape_csv (Procname.to_string caller_name));
pp "\"%s\"," (Escape.escape_csv (Procname.to_filename caller_name));
pp "\"%s\"," (Escape.escape_csv (Procname.to_string callee_name));
pp "\"%s\"," (Escape.escape_csv (Procname.to_filename callee_name));
pp "\"%s\"," (Escape.escape_csv (Typ.Procname.to_string caller_name));
pp "\"%s\"," (Escape.escape_csv (Typ.Procname.to_filename caller_name));
pp "\"%s\"," (Escape.escape_csv (Typ.Procname.to_string callee_name));
pp "\"%s\"," (Escape.escape_csv (Typ.Procname.to_filename callee_name));
pp "%s," (SourceFile.to_string summary.Specs.attributes.ProcAttributes.loc.Location.file);
pp "%d," loc.Location.line;
pp "%a@\n" Specs.CallStats.pp_trace trace
@ -864,7 +864,7 @@ let module Summary = {
} else {
L.stdout
"Procedure: %a@\n%a@."
Procname.pp
Typ.Procname.pp
proc_name
(Specs.pp_summary_text whole_seconds::Config.whole_seconds)
summary
@ -875,7 +875,7 @@ let module Summary = {
let write_summary_latex fmt summary => {
let proc_name = Specs.get_proc_name summary;
Latex.pp_section
fmt ("Analysis of function " ^ Latex.convert_string (Procname.to_string proc_name));
fmt ("Analysis of function " ^ Latex.convert_string (Typ.Procname.to_string proc_name));
F.fprintf
fmt "@[<v>%a@]" (Specs.pp_summary_latex Black whole_seconds::Config.whole_seconds) summary
};
@ -942,16 +942,16 @@ let module PreconditionStats = {
switch (Prop.CategorizePreconditions.categorize preconditions) {
| Prop.CategorizePreconditions.Empty =>
incr nr_empty;
L.stdout "Procedure: %a footprint:Empty@." Procname.pp proc_name
L.stdout "Procedure: %a footprint:Empty@." Typ.Procname.pp proc_name
| Prop.CategorizePreconditions.OnlyAllocation =>
incr nr_onlyallocation;
L.stdout "Procedure: %a footprint:OnlyAllocation@." Procname.pp proc_name
L.stdout "Procedure: %a footprint:OnlyAllocation@." Typ.Procname.pp proc_name
| Prop.CategorizePreconditions.NoPres =>
incr nr_nopres;
L.stdout "Procedure: %a footprint:NoPres@." Procname.pp proc_name
L.stdout "Procedure: %a footprint:NoPres@." Typ.Procname.pp proc_name
| Prop.CategorizePreconditions.DataConstraints =>
incr nr_dataconstraints;
L.stdout "Procedure: %a footprint:DataConstraints@." Procname.pp proc_name
L.stdout "Procedure: %a footprint:DataConstraints@." Typ.Procname.pp proc_name
}
};
let pp_stats () => {
@ -1379,7 +1379,7 @@ let pp_summary_and_issues formats_by_report_kind => {
};
{
LintIssues.load_issues_to_errlog_map Config.lint_issues_dir_name;
Procname.Map.iter
Typ.Procname.Map.iter
(pp_lint_issues filters formats_by_report_kind linereader) !LintIssues.errLogMap
};
finalize_and_close_files formats_by_report_kind stats pdflatex

@ -40,19 +40,19 @@ let try_capture (attributes : ProcAttributes.t) : ProcAttributes.t option =
Logging.out
"Captured file %a to get procedure %a but it wasn't found there@\n"
SourceFile.pp definition_file
Procname.pp attributes.proc_name
Typ.Procname.pp attributes.proc_name
)
) else (
Logging.out
"Wanted to capture file %a to get procedure %a but file was already captured@\n"
SourceFile.pp definition_file
Procname.pp attributes.proc_name
Typ.Procname.pp attributes.proc_name
)
in
match definition_file_opt with
| None ->
Logging.out "Couldn't find source file for %a (declared in %a)@\n"
Procname.pp attributes.proc_name
Typ.Procname.pp attributes.proc_name
SourceFile.pp decl_file
| Some file -> try_compile file
);

@ -12,7 +12,7 @@ let get_name_of_local (curr_f: Procdesc.t) (x, _) => Pvar.mk x (Procdesc.get_pro
/* returns a list of local static variables (ie local variables defined static) in a proposition */
let get_name_of_objc_static_locals (curr_f: Procdesc.t) p => {
let pname = Procname.to_string (Procdesc.get_proc_name curr_f);
let pname = Typ.Procname.to_string (Procdesc.get_proc_name curr_f);
let local_static e =>
switch e {
/* is a local static if it's a global and it has a static local name */

@ -16,27 +16,27 @@ open! IStd
type rules
(** Abstract a proposition. *)
val abstract : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
val abstract : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Check whether the prop contains junk.
If it does, and [Config.allowleak] is true, remove the junk,
otherwise raise a Leak exception. *)
val abstract_junk :
?original_prop:Prop.normal Prop.t ->
Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Abstract a proposition but don't pay a SymOp *)
val abstract_no_symop : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
val abstract_no_symop : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Get the current rules discoveres *)
val get_current_rules : unit -> rules
(** Abstract each proposition in [propset] *)
val lifted_abstract : Procname.t -> Tenv.t -> Propset.t -> Propset.t
val lifted_abstract : Typ.Procname.t -> Tenv.t -> Propset.t -> Propset.t
(** Remove redundant elements in an array, and check for junk afterwards *)
val remove_redundant_array_elements :
Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.normal Prop.t
(** Reset the abstraction rules discovered *)
val reset_current_rules : unit -> unit

@ -19,7 +19,7 @@ type args = {
path : Paths.Path.t;
ret_id : (Ident.t * Typ.t) option;
args : (Exp.t * Typ.t) list;
proc_name : Procname.t;
proc_name : Typ.Procname.t;
loc : Location.t;
}
@ -30,33 +30,33 @@ type t = args -> ret_typ
type registered = t
(** builtin function names for which we do symbolic execution *)
let builtin_functions = Procname.Hash.create 4
let builtin_functions = Typ.Procname.Hash.create 4
let check_register_populated () =
(* check if BuiltinDefn were loaded before accessing register *)
if Int.equal (Procname.Hash.length builtin_functions) 0 then
if Int.equal (Typ.Procname.Hash.length builtin_functions) 0 then
failwith "Builtins were not initialized"
(** check if the function is a builtin *)
let is_registered name =
Procname.Hash.mem builtin_functions name || (check_register_populated (); false)
Typ.Procname.Hash.mem builtin_functions name || (check_register_populated (); false)
(** get the symbolic execution handler associated to the builtin function name *)
let get name : t option =
try Some (Procname.Hash.find builtin_functions name)
try Some (Typ.Procname.Hash.find builtin_functions name)
with Not_found -> (check_register_populated (); None)
(** register a builtin [Procname.t] and symbolic execution handler *)
(** register a builtin [Typ.Procname.t] and symbolic execution handler *)
let register proc_name sym_exe_fun : registered =
Procname.Hash.replace builtin_functions proc_name sym_exe_fun;
Typ.Procname.Hash.replace builtin_functions proc_name sym_exe_fun;
sym_exe_fun
(** print the functions registered *)
let pp_registered fmt () =
let builtin_names = ref [] in
Procname.Hash.iter (fun name _ -> builtin_names := name :: !builtin_names) builtin_functions;
builtin_names := List.sort ~cmp:Procname.compare !builtin_names;
let pp pname = Format.fprintf fmt "%a@\n" Procname.pp pname in
Typ.Procname.Hash.iter (fun name _ -> builtin_names := name :: !builtin_names) builtin_functions;
builtin_names := List.sort ~cmp:Typ.Procname.compare !builtin_names;
let pp pname = Format.fprintf fmt "%a@\n" Typ.Procname.pp pname in
Format.fprintf fmt "Registered builtins:@\n @[";
List.iter ~f:pp !builtin_names;
Format.fprintf fmt "@]@."

@ -19,7 +19,7 @@ type args = {
path : Paths.Path.t;
ret_id : (Ident.t * Typ.t) option;
args : (Exp.t * Typ.t) list;
proc_name : Procname.t;
proc_name : Typ.Procname.t;
loc : Location.t;
}
@ -29,13 +29,13 @@ type t = args -> ret_typ
type registered
val register : Procname.t -> t -> registered
(** Register a builtin [Procname.t] and symbolic execution handler *)
val register : Typ.Procname.t -> t -> registered
(** Register a builtin [Typ.Procname.t] and symbolic execution handler *)
val is_registered : Procname.t -> bool
val is_registered : Typ.Procname.t -> bool
(** Check if the function is a builtin *)
val get : Procname.t -> t option
val get : Typ.Procname.t -> t option
(** Get the symbolic execution handler associated to the builtin function name *)
val print_and_exit : unit -> 'a

@ -14,11 +14,11 @@ module L = Logging
(** Module to register and invoke callbacks *)
type proc_callback_args = {
get_proc_desc : Procname.t -> Procdesc.t option;
get_procs_in_file : Procname.t -> Procname.t list;
get_proc_desc : Typ.Procname.t -> Procdesc.t option;
get_procs_in_file : Typ.Procname.t -> Typ.Procname.t list;
idenv : Idenv.t;
tenv : Tenv.t;
proc_name : Procname.t;
proc_name : Typ.Procname.t;
proc_desc : Procdesc.t;
}
@ -26,9 +26,9 @@ type proc_callback_t = proc_callback_args -> unit
type cluster_callback_t =
Exe_env.t ->
Procname.t list ->
(Procname.t -> Procdesc.t option) ->
(Idenv.t * Tenv.t * Procname.t * Procdesc.t) list ->
Typ.Procname.t list ->
(Typ.Procname.t -> Procdesc.t option) ->
(Idenv.t * Tenv.t * Typ.Procname.t * Procdesc.t) list ->
unit
let procedure_callbacks = ref []
@ -54,7 +54,7 @@ let get_procedure_definition exe_env proc_name =
(idenv, tenv, proc_name, proc_desc, language))
(Exe_env.get_proc_desc exe_env proc_name)
let get_language proc_name = if Procname.is_java proc_name then Config.Java else Config.Clang
let get_language proc_name = if Typ.Procname.is_java proc_name then Config.Java else Config.Clang
let reset_summary proc_name =
@ -163,8 +163,8 @@ let iterate_callbacks call_graph exe_env =
let cluster_id proc_name =
match proc_name with
| Procname.Java pname_java ->
Procname.java_get_class_name pname_java
| Typ.Procname.Java pname_java ->
Typ.Procname.java_get_class_name pname_java
| _ ->
"unknown" in
let cluster proc_names =

@ -12,11 +12,11 @@ open! IStd
(** Module to register and invoke callbacks *)
type proc_callback_args = {
get_proc_desc : Procname.t -> Procdesc.t option;
get_procs_in_file : Procname.t -> Procname.t list;
get_proc_desc : Typ.Procname.t -> Procdesc.t option;
get_procs_in_file : Typ.Procname.t -> Typ.Procname.t list;
idenv : Idenv.t;
tenv : Tenv.t;
proc_name : Procname.t;
proc_name : Typ.Procname.t;
proc_desc : Procdesc.t;
}
@ -30,9 +30,9 @@ type proc_callback_t = proc_callback_args -> unit
type cluster_callback_t =
Exe_env.t ->
Procname.t list ->
(Procname.t -> Procdesc.t option) ->
(Idenv.t * Tenv.t * Procname.t * Procdesc.t) list ->
Typ.Procname.t list ->
(Typ.Procname.t -> Procdesc.t option) ->
(Idenv.t * Tenv.t * Typ.Procname.t * Procdesc.t) list ->
unit
(** register a procedure callback *)

@ -16,7 +16,7 @@ open! IStd
(** Join two pathsets *)
val pathset_join :
Procname.t -> Tenv.t -> Paths.PathSet.t -> Paths.PathSet.t -> Paths.PathSet.t * Paths.PathSet.t
Typ.Procname.t -> Tenv.t -> Paths.PathSet.t -> Paths.PathSet.t -> Paths.PathSet.t * Paths.PathSet.t
val join_time : float ref
@ -25,7 +25,7 @@ val proplist_collapse_pre : Tenv.t -> Prop.normal Prop.t list -> Prop.normal Spe
val pathset_collapse : Tenv.t -> Paths.PathSet.t -> Paths.PathSet.t
(** reduce the pathset only based on implication checking. *)
val pathset_collapse_impl : Procname.t -> Tenv.t -> Paths.PathSet.t -> Paths.PathSet.t
val pathset_collapse_impl : Typ.Procname.t -> Tenv.t -> Paths.PathSet.t -> Paths.PathSet.t
(** {2 Meet Operators} *)

@ -951,7 +951,7 @@ let pp_proplist_parsed2dotty_file filename plist =
(* channel. You have to compute an interprocedural cfg first *)
let pp_cfgnodename pname fmt (n : Procdesc.Node.t) =
F.fprintf fmt "\"%s_%d\"" (Procname.to_filename pname) (Procdesc.Node.get_id n :> int)
F.fprintf fmt "\"%s_%d\"" (Typ.Procname.to_filename pname) (Procdesc.Node.get_id n :> int)
let pp_etlist fmt etl =
List.iter ~f:(fun (id, ty) ->
@ -965,7 +965,7 @@ let pp_cfgnodelabel pdesc fmt (n : Procdesc.Node.t) =
let pp_label fmt n =
match Procdesc.Node.get_kind n with
| Procdesc.Node.Start_node pname ->
let pname_string = Procname.to_string pname in
let pname_string = Typ.Procname.to_string pname in
Format.fprintf fmt "Start %s\\nFormals: %a\\nLocals: %a"
pname_string
pp_etlist (Procdesc.get_formals pdesc)
@ -978,7 +978,7 @@ let pp_cfgnodelabel pdesc fmt (n : Procdesc.Node.t) =
if not (Annot.Method.is_empty method_annotation) then
Format.fprintf fmt "\\nAnnotation: %a" (Annot.Method.pp pname_string) method_annotation
| Procdesc.Node.Exit_node pname ->
Format.fprintf fmt "Exit %s" (Procname.to_string pname)
Format.fprintf fmt "Exit %s" (Typ.Procname.to_string pname)
| Procdesc.Node.Join_node ->
Format.fprintf fmt "+"
| Procdesc.Node.Prune_node (is_true_branch, _, _) ->

@ -26,8 +26,8 @@ let is_one_of_classes class_name classes =
let is_method_of_objc_cpp_class pname classes =
match pname with
| Procname.ObjC_Cpp name ->
let class_name = Procname.objc_cpp_get_class_name name in
| Typ.Procname.ObjC_Cpp name ->
let class_name = Typ.Procname.objc_cpp_get_class_name name in
is_one_of_classes class_name classes
| _ -> false
@ -219,7 +219,7 @@ let rec _find_normal_variable_load tenv (seen : Exp.Set.t) node id : DExp.t opti
Sil.d_exp e; L.d_ln ());
_exp_lv_dexp tenv seen node e
| Sil.Call (Some (id0, _), Exp.Const (Const.Cfun pn), (e, _):: _, _, _)
when Ident.equal id id0 && Procname.equal pn (Procname.from_string_c_fun "__cast") ->
when Ident.equal id id0 && Typ.Procname.equal pn (Typ.Procname.from_string_c_fun "__cast") ->
if verbose
then
(L.d_str "find_normal_variable_load cast on ";
@ -897,7 +897,7 @@ let _explain_access tenv
if verbose then (L.d_str "explain_dereference Binop.Leteref "; Sil.d_exp e; L.d_ln ());
Some e
| Some Sil.Call (_, Exp.Const (Const.Cfun fn), [(e, _)], _, _)
when String.equal (Procname.to_string fn) "free" ->
when String.equal (Typ.Procname.to_string fn) "free" ->
if verbose then (L.d_str "explain_dereference Sil.Call "; Sil.d_exp e; L.d_ln ());
Some e
| Some Sil.Call (_, (Exp.Var _ as e), _, _, _) ->

@ -42,7 +42,7 @@ 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
(** Produce a description of a persistent reference to an Android Context *)
val explain_context_leak : Procname.t -> Typ.t -> Ident.fieldname ->
val explain_context_leak : Typ.Procname.t -> Typ.t -> Ident.fieldname ->
(Ident.fieldname option * Typ.t) list -> Localise.error_desc
(** Produce a description of a mismatch between an allocation function and a deallocation function *)
@ -54,7 +54,7 @@ val explain_array_access : Tenv.t -> Localise.deref_str -> 'a Prop.t -> Location
(** explain a class cast exception *)
val explain_class_cast_exception :
Tenv.t -> Procname.t option -> Exp.t -> Exp.t -> Exp.t ->
Tenv.t -> Typ.Procname.t option -> Exp.t -> Exp.t -> Exp.t ->
Procdesc.Node.t -> Location.t -> Localise.error_desc
(** Explain a deallocate stack variable error *)
@ -112,7 +112,7 @@ val explain_unary_minus_applied_to_unsigned_expression :
(** Explain a tainted value error *)
val explain_tainted_value_reaching_sensitive_function :
Prop.normal Prop.t -> Exp.t -> PredSymb.taint_info -> Procname.t -> Location.t ->
Prop.normal Prop.t -> Exp.t -> PredSymb.taint_info -> Typ.Procname.t -> Location.t ->
Localise.error_desc
(** Produce a description of a leak by looking at the current state.

@ -64,7 +64,7 @@ let create_file_data table source cg_fname =
(** execution environment *)
type t =
{ cg: Cg.t; (** global call graph *)
proc_map: file_data Procname.Hash.t; (** map from procedure name to file data *)
proc_map: file_data Typ.Procname.Hash.t; (** map from procedure name to file data *)
file_map: file_data FilenameHash.t; (** map from cg fname to file data *)
mutable source_files : SourceFile.Set.t; (** Source files in the execution environment *)
}
@ -78,7 +78,7 @@ let freeze exe_env = exe_env (* TODO: unclear what this function is used for *)
(** create a new execution environment *)
let create () =
{ cg = Cg.create None;
proc_map = Procname.Hash.create 17;
proc_map = Typ.Procname.Hash.create 17;
file_map = FilenameHash.create 1;
source_files = SourceFile.Set.empty;
}
@ -109,7 +109,7 @@ let add_cg (exe_env: t) (source_dir : DB.source_dir) =
L.stderr "@.DUPLICATE_SYMBOLS source: %a source_captured:%a pname:%a@."
SourceFile.pp source
SourceFile.pp source_captured
Procname.pp pname
Typ.Procname.pp pname
))
defined_procs;
Cg.extend exe_env.cg cg
@ -120,13 +120,13 @@ let get_cg exe_env =
let get_file_data exe_env pname =
try
Some (Procname.Hash.find exe_env.proc_map pname)
Some (Typ.Procname.Hash.find exe_env.proc_map pname)
with Not_found ->
begin
let source_file_opt =
match AttributesTable.load_attributes pname with
| None ->
L.err "can't find tenv_cfg_object for %a@." Procname.pp pname;
L.err "can't find tenv_cfg_object for %a@." Typ.Procname.pp pname;
None
| Some proc_attributes when Config.reactive_capture ->
let get_captured_file {ProcAttributes.source_file_captured} = source_file_captured in
@ -137,7 +137,7 @@ let get_file_data exe_env pname =
let source_dir = DB.source_dir_from_source_file source_file in
let cg_fname = DB.source_dir_get_internal_file source_dir ".cg" in
let file_data = create_file_data exe_env.file_map source_file cg_fname in
Procname.Hash.replace exe_env.proc_map pname file_data;
Typ.Procname.Hash.replace exe_env.proc_map pname file_data;
file_data in
Option.map ~f:get_file_data_for_source source_file_opt
end
@ -167,10 +167,10 @@ let get_tenv exe_env proc_name =
tenv
| None ->
failwithf "get_tenv: tenv not found for %a in file %s"
Procname.pp proc_name (DB.filename_to_string file_data.tenv_file)
Typ.Procname.pp proc_name (DB.filename_to_string file_data.tenv_file)
)
| None ->
failwithf "get_tenv: file_data not found for %a" Procname.pp proc_name
failwithf "get_tenv: file_data not found for %a" Typ.Procname.pp proc_name
(** return the cfg associated to the procedure *)
let get_cfg exe_env pname =
@ -201,4 +201,4 @@ let iter_files f exe_env =
Option.iter ~f:(fun cfg -> f fname cfg) (file_data_to_cfg file_data);
SourceFile.Set.add fname seen_files_acc
end in
ignore (Procname.Hash.fold do_file exe_env.proc_map SourceFile.Set.empty)
ignore (Typ.Procname.Hash.fold do_file exe_env.proc_map SourceFile.Set.empty)

@ -32,16 +32,16 @@ val add_cg : initial -> DB.source_dir -> unit
val get_cg : t -> Cg.t
(** return the source file associated to the procedure *)
val get_source : t -> Procname.t -> SourceFile.t option
val get_source : t -> Typ.Procname.t -> SourceFile.t option
(** return the type environment associated to the procedure *)
val get_tenv : t -> Procname.t -> Tenv.t
val get_tenv : t -> Typ.Procname.t -> Tenv.t
(** return the cfg associated to the procedure *)
val get_cfg : t -> Procname.t -> Cfg.cfg option
val get_cfg : t -> Typ.Procname.t -> Cfg.cfg option
(** return the proc desc associated to the procedure *)
val get_proc_desc : t -> Procname.t -> Procdesc.t option
val get_proc_desc : t -> Typ.Procname.t -> Procdesc.t option
(** [iter_files f exe_env] applies [f] to the source file and tenv and cfg for each file in [exe_env] *)
val iter_files : (SourceFile.t -> Cfg.cfg -> unit) -> t -> unit

@ -15,7 +15,7 @@ module L = Logging
type path_filter = SourceFile.t -> bool
type error_filter = Localise.t -> bool
type proc_filter = Procname.t -> bool
type proc_filter = Typ.Procname.t -> bool
type filters =
{
@ -57,8 +57,8 @@ let is_matching patterns =
(** Check if a proc name is matching the name given as string. *)
let match_method language proc_name method_name =
not (BuiltinDecl.is_declared proc_name) &&
Config.equal_language (Procname.get_language proc_name) language &&
String.equal (Procname.get_method proc_name) method_name
Config.equal_language (Typ.Procname.get_language proc_name) language &&
String.equal (Typ.Procname.get_method proc_name) method_name
(* Module to create matcher based on strings present in the source file *)
module FileContainsStringMatcher = struct
@ -108,7 +108,7 @@ type pattern =
(* Module to create matcher based on source file names or class names and method names *)
module FileOrProcMatcher = struct
type matcher = SourceFile.t -> Procname.t -> bool
type matcher = SourceFile.t -> Typ.Procname.t -> bool
let default_matcher : matcher =
fun _ _ -> false
@ -128,8 +128,8 @@ module FileOrProcMatcher = struct
~init:String.Map.empty
m_patterns in
let do_java pname_java =
let class_name = Procname.java_get_class_name pname_java
and method_name = Procname.java_get_method pname_java in
let class_name = Typ.Procname.java_get_class_name pname_java
and method_name = Typ.Procname.java_get_method pname_java in
try
let class_patterns = String.Map.find_exn pattern_map class_name in
List.exists
@ -142,7 +142,7 @@ module FileOrProcMatcher = struct
fun _ proc_name ->
match proc_name with
| Procname.Java pname_java ->
| Typ.Procname.Java pname_java ->
do_java pname_java
| _ ->
false

@ -16,7 +16,7 @@ type path_filter = SourceFile.t -> bool
type error_filter = Localise.t -> bool
(** Filter type for a procedure name *)
type proc_filter = Procname.t -> bool
type proc_filter = Typ.Procname.t -> bool
type filters =
{
@ -31,9 +31,9 @@ val do_not_filter : filters
(** Create filters based on the config file *)
val create_filters : Config.analyzer -> filters
val never_return_null_matcher : SourceFile.t -> Procname.t -> bool
val skip_translation_matcher : SourceFile.t -> Procname.t -> bool
val modeled_expensive_matcher : (string -> bool) -> Procname.t -> bool
val never_return_null_matcher : SourceFile.t -> Typ.Procname.t -> bool
val skip_translation_matcher : SourceFile.t -> Typ.Procname.t -> bool
val modeled_expensive_matcher : (string -> bool) -> Typ.Procname.t -> bool
(** Load the config file and list the files to report on *)
val test: unit -> unit

@ -223,30 +223,30 @@ let collect_preconditions tenv proc_name : Prop.normal Specs.Jprop.t list =
let f p = Prop.prop_normal_vars_to_primed_vars tenv p in
Propset.map tenv f pset in
L.d_strln ("#### Extracted footprint of " ^ Procname.to_string proc_name ^ ": ####");
L.d_strln ("#### Extracted footprint of " ^ Typ.Procname.to_string proc_name ^ ": ####");
L.d_increase_indent 1; Propset.d Prop.prop_emp pset'; L.d_decrease_indent 1; L.d_ln ();
L.d_ln ();
let pset'' = collect_do_abstract_pre proc_name tenv pset' in
let plist_meet = do_meet_pre tenv pset'' in
L.d_strln ("#### Footprint of " ^ Procname.to_string proc_name ^ " after Meet ####");
L.d_strln ("#### Footprint of " ^ Typ.Procname.to_string proc_name ^ " after Meet ####");
L.d_increase_indent 1; Propgraph.d_proplist Prop.prop_emp plist_meet;
L.d_decrease_indent 1; L.d_ln ();
L.d_ln ();
L.d_increase_indent 2; (* Indent for the join output *)
let jplist = do_join_pre tenv plist_meet in
L.d_decrease_indent 2; L.d_ln ();
L.d_strln ("#### Footprint of " ^ Procname.to_string proc_name ^ " after Join ####");
L.d_strln ("#### Footprint of " ^ Typ.Procname.to_string proc_name ^ " after Join ####");
L.d_increase_indent 1; Specs.Jprop.d_list false jplist; L.d_decrease_indent 1; L.d_ln ();
let jplist' =
List.map ~f:(Specs.Jprop.map (Prop.prop_rename_primed_footprint_vars tenv)) jplist in
L.d_strln ("#### Renamed footprint of " ^ Procname.to_string proc_name ^ ": ####");
L.d_strln ("#### Renamed footprint of " ^ Typ.Procname.to_string proc_name ^ ": ####");
L.d_increase_indent 1; Specs.Jprop.d_list false jplist'; L.d_decrease_indent 1; L.d_ln ();
let jplist'' =
let f p =
Prop.prop_primed_vars_to_normal_vars tenv
(collect_do_abstract_one proc_name tenv p) in
List.map ~f:(Specs.Jprop.map f) jplist' in
L.d_strln ("#### Abstracted footprint of " ^ Procname.to_string proc_name ^ ": ####");
L.d_strln ("#### Abstracted footprint of " ^ Typ.Procname.to_string proc_name ^ ": ####");
L.d_increase_indent 1; Specs.Jprop.d_list false jplist''; L.d_decrease_indent 1; L.d_ln();
jplist''
@ -535,10 +535,10 @@ let forward_tabulate tenv pdesc wl source =
if Specs.equal_phase (Specs.get_phase summary) Specs.FOOTPRINT then "FP" else "RE" in
let status = Specs.get_status summary in
F.sprintf
"[%s:%s] %s" phase_string (Specs.string_of_status status) (Procname.to_string proc_name) in
"[%s:%s] %s" phase_string (Specs.string_of_status status) (Typ.Procname.to_string proc_name) in
L.d_strln ("**** " ^ (log_string pname) ^ " " ^
"Node: " ^ string_of_int (Procdesc.Node.get_id curr_node :> int) ^ ", " ^
"Procedure: " ^ Procname.to_string pname ^ ", " ^
"Procedure: " ^ Typ.Procname.to_string pname ^ ", " ^
"Session: " ^ string_of_int session ^ ", " ^
"Todo: " ^ string_of_int (Paths.PathSet.size pathset_todo) ^ " ****");
L.d_increase_indent 1;
@ -803,8 +803,8 @@ let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t
(* Assuming C++ developers use RAII, remove resources from the constructor posts *)
let pathset = match pname with
| Procname.ObjC_Cpp _ ->
if (Procname.is_constructor pname) then
| Typ.Procname.ObjC_Cpp _ ->
if (Typ.Procname.is_constructor pname) then
Paths.PathSet.map (fun prop ->
Attribute.remove_resource tenv Racquire (Rmemory Mobjc)
(Attribute.remove_resource tenv Racquire (Rmemory Mmalloc)
@ -814,7 +814,7 @@ let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t
| _ -> pathset in
L.d_strln
("#### [FUNCTION " ^ Procname.to_string pname ^ "] Analysis result ####");
("#### [FUNCTION " ^ Typ.Procname.to_string pname ^ "] Analysis result ####");
Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv pathset);
L.d_ln ();
let res =
@ -831,7 +831,7 @@ let collect_postconditions wl tenv pdesc : Paths.PathSet.t * Specs.Visitedset.t
| exn when (match exn with Exceptions.Leak _ -> true | _ -> false) ->
L.d_strln"Leak in post collection"; assert false in
L.d_strln
("#### [FUNCTION " ^ Procname.to_string pname ^ "] Postconditions after join ####");
("#### [FUNCTION " ^ Typ.Procname.to_string pname ^ "] Postconditions after join ####");
L.d_increase_indent 1;
Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv (fst res));
L.d_decrease_indent 1;
@ -912,7 +912,7 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
: Prop.normal Specs.spec option =
let pname = Procdesc.get_proc_name pdesc in
do_before_node source 0 init_node;
L.d_strln ("#### Start: RE-execution for " ^ Procname.to_string pname ^ " ####");
L.d_strln ("#### Start: RE-execution for " ^ Typ.Procname.to_string pname ^ " ####");
L.d_indent 1;
L.d_strln "Precond:"; Specs.Jprop.d_shallow precondition;
L.d_ln (); L.d_ln ();
@ -930,7 +930,7 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
forward_tabulate tenv pdesc wl source;
do_before_node source 0 init_node;
L.d_strln_color Green
("#### Finished: RE-execution for " ^ Procname.to_string pname ^ " ####");
("#### Finished: RE-execution for " ^ Typ.Procname.to_string pname ^ " ####");
L.d_increase_indent 1;
L.d_strln "Precond:"; Prop.d_prop (Specs.Jprop.to_prop precondition);
L.d_ln ();
@ -953,7 +953,7 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
with RE_EXE_ERROR ->
do_before_node source 0 init_node;
Printer.force_delayed_prints ();
L.d_strln_color Red ("#### [FUNCTION " ^ Procname.to_string pname ^ "] ...ERROR");
L.d_strln_color Red ("#### [FUNCTION " ^ Typ.Procname.to_string pname ^ "] ...ERROR");
L.d_increase_indent 1;
L.d_strln "when starting from pre:";
Prop.d_prop (Specs.Jprop.to_prop precondition);
@ -966,7 +966,7 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
let get_procs_and_defined_children call_graph =
List.map
~f:(fun (n, ns) ->
(n, Procname.Set.elements ns))
(n, Typ.Procname.Set.elements ns))
(Cg.get_nodes_and_defined_children call_graph)
let pp_intra_stats wl proc_desc fmt _ =
@ -988,7 +988,7 @@ type exe_phase = (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.p
and [get_results ()] returns the results computed.
This function is architected so that [get_results ()] can be called even after
[go ()] was interrupted by and exception. *)
let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source
let perform_analysis_phase tenv (pname : Typ.Procname.t) (pdesc : Procdesc.t) source
: exe_phase =
let summary = Specs.get_summary_unsafe "perform_analysis_phase" pname in
let start_node = Procdesc.get_start_node pdesc in
@ -1008,7 +1008,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source
let add pset prop =
Paths.PathSet.add_renamed_prop prop (Paths.Path.start start_node) pset in
Propset.fold add Paths.PathSet.empty init_props in
L.out "@.#### Start: Footprint Computation for %a ####@." Procname.pp pname;
L.out "@.#### Start: Footprint Computation for %a ####@." Typ.Procname.pp pname;
L.d_increase_indent 1;
L.d_strln "initial props =";
Propset.d Prop.prop_emp init_props; L.d_ln (); L.d_ln();
@ -1023,12 +1023,12 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source
let get_results (wl : Worklist.t) () =
State.process_execution_failures Reporting.log_warning pname;
let results = collect_analysis_result tenv wl pdesc in
L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp pname;
L.out "#### [FUNCTION %a] ... OK #####@\n" Typ.Procname.pp pname;
L.out "#### Finished: Footprint Computation for %a %a ####@."
Procname.pp pname
Typ.Procname.pp pname
(pp_intra_stats wl pdesc) pname;
L.out "#### [FUNCTION %a] Footprint Analysis result ####@\n%a@."
Procname.pp pname
Typ.Procname.pp pname
(Paths.PathSet.pp Pp.text) results;
let specs = try extract_specs tenv pdesc results with
| Exceptions.Leak _ ->
@ -1048,7 +1048,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source
(Specs.get_specs pname) in
let valid_specs = ref [] in
let go () =
L.out "@.#### Start: Re-Execution for %a ####@." Procname.pp pname;
L.out "@.#### Start: Re-Execution for %a ####@." Typ.Procname.pp pname;
let filter p =
let wl = path_set_create_worklist pdesc in
let speco = execute_filter_prop wl tenv pdesc start_node p source in
@ -1069,22 +1069,22 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Procdesc.t) source
ignore (List.map ~f:filter candidate_preconditions) in
let get_results () =
let specs = !valid_specs in
L.out "#### [FUNCTION %a] ... OK #####@\n" Procname.pp pname;
L.out "#### Finished: Re-Execution for %a ####@." Procname.pp pname;
L.out "#### [FUNCTION %a] ... OK #####@\n" Typ.Procname.pp pname;
L.out "#### Finished: Re-Execution for %a ####@." Typ.Procname.pp pname;
let valid_preconditions =
List.map ~f:(fun spec -> spec.Specs.pre) specs in
let filename =
DB.Results_dir.path_to_filename
(DB.Results_dir.Abs_source_dir source)
[(Procname.to_filename pname)] in
[(Typ.Procname.to_filename pname)] in
if Config.write_dotty then
Dotty.pp_speclist_dotty_file filename specs;
L.out "@.@.================================================";
L.out "@. *** CANDIDATE PRECONDITIONS FOR %a: " Procname.pp pname;
L.out "@. *** CANDIDATE PRECONDITIONS FOR %a: " Typ.Procname.pp pname;
L.out "@.================================================@.";
L.out "@.%a @.@." (Specs.Jprop.pp_list Pp.text false) candidate_preconditions;
L.out "@.@.================================================";
L.out "@. *** VALID PRECONDITIONS FOR %a: " Procname.pp pname;
L.out "@. *** VALID PRECONDITIONS FOR %a: " Typ.Procname.pp pname;
L.out "@.================================================@.";
L.out "@.%a @.@." (Specs.Jprop.pp_list Pp.text true) valid_preconditions;
specs, Specs.RE_EXECUTION in
@ -1173,9 +1173,9 @@ let report_runtime_exceptions tenv pdesc summary =
is_public_method
&&
(match pname with
| Procname.Java pname_java ->
Procname.java_is_static pname
&& String.equal (Procname.java_get_method pname_java) "main"
| Typ.Procname.Java pname_java ->
Typ.Procname.java_is_static pname
&& String.equal (Typ.Procname.java_get_method pname_java) "main"
| _ ->
false) in
let is_annotated pdesc =
@ -1324,7 +1324,7 @@ let analyze_proc source exe_env proc_desc : Specs.summary =
(** Perform the transition from [FOOTPRINT] to [RE_EXECUTION] in spec table *)
let transition_footprint_re_exe tenv proc_name joined_pres =
L.out "Transition %a from footprint to re-exe@." Procname.pp proc_name;
L.out "Transition %a from footprint to re-exe@." Typ.Procname.pp proc_name;
let summary = Specs.get_summary_unsafe "transition_footprint_re_exe" proc_name in
let summary' =
if Config.only_footprint then
@ -1375,7 +1375,7 @@ let perform_transition exe_env tenv proc_name source =
with exn when SymOp.exn_not_failure exn ->
apply_start_node (do_after_node source);
Config.allow_leak := allow_leak;
L.err "Error in collect_preconditions for %a@." Procname.pp proc_name;
L.err "Error in collect_preconditions for %a@." Typ.Procname.pp proc_name;
let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
let err_str = "exception raised " ^ (Localise.to_string err_name) in
L.err "Error: %s %a@." err_str L.pp_ml_loc_opt ml_loc_opt;
@ -1523,7 +1523,7 @@ let print_stats_cfg proc_shadowed source cfg =
if proc_shadowed proc_desc ||
is_none (Specs.get_summary proc_name) then
L.out "print_stats: ignoring function %a which is also defined in another file@."
Procname.pp proc_name
Typ.Procname.pp proc_name
else
let summary = Specs.get_summary_unsafe "print_stats_cfg" proc_name in
let stats = summary.Specs.stats in

@ -29,7 +29,7 @@ let dirs_to_analyze =
type analyze_ondemand = SourceFile.t -> Procdesc.t -> Specs.summary
type get_proc_desc = Procname.t -> Procdesc.t option
type get_proc_desc = Typ.Procname.t -> Procdesc.t option
type callbacks =
{
@ -116,8 +116,8 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
L.log_progress_procedure ();
if Config.trace_ondemand then L.stderr "[%d] run_proc_analysis %a -> %a@."
!nesting
Procname.pp curr_pname
Procname.pp callee_pname;
Typ.Procname.pp curr_pname
Typ.Procname.pp callee_pname;
let preprocess () =
incr nesting;
@ -127,9 +127,9 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
Option.value_map
~f:(fun (attributes : ProcAttributes.t) ->
let attribute_pname = attributes.proc_name in
if not (Procname.equal callee_pname attribute_pname) then
failwith ("ERROR: "^(Procname.to_string callee_pname)
^" not equal to "^(Procname.to_string attribute_pname));
if not (Typ.Procname.equal callee_pname attribute_pname) then
failwith ("ERROR: "^(Typ.Procname.to_string callee_pname)
^" not equal to "^(Typ.Procname.to_string attribute_pname));
attributes.loc.file)
~default:SourceFile.empty
attributes_opt in
@ -166,7 +166,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc
summary
with exn ->
L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.BACK TRACE@.%s@?"
Procname.pp callee_pname
Typ.Procname.pp callee_pname
(Exn.to_string exn)
(Printexc.get_backtrace ());
restore_global_state old_state;

@ -17,7 +17,7 @@ val dirs_to_analyze : String.Set.t option
type analyze_ondemand = SourceFile.t -> Procdesc.t -> Specs.summary
type get_proc_desc = Procname.t -> Procdesc.t option
type get_proc_desc = Typ.Procname.t -> Procdesc.t option
type callbacks =
{
@ -38,10 +38,10 @@ val analyze_proc_desc :
performs an on-demand analysis of proc_name
triggered during the analysis of curr_pdesc. *)
val analyze_proc_name :
propagate_exceptions:bool -> Procdesc.t -> Procname.t -> Specs.summary option
propagate_exceptions:bool -> Procdesc.t -> Typ.Procname.t -> Specs.summary option
(** Check if the procedure called needs to be analyzed. *)
val procedure_should_be_analyzed : Procname.t -> bool
val procedure_should_be_analyzed : Typ.Procname.t -> bool
(** Set the callbacks used to perform on-demand analysis. *)
val set_callbacks : callbacks -> unit

@ -24,7 +24,7 @@ module Path : sig
type session = int
(** add a call with its sub-path, the boolean indicates whether the subtrace for the procedure should be included *)
val add_call : bool -> t -> Procname.t -> t -> t
val add_call : bool -> t -> Typ.Procname.t -> t -> t
(** check whether a path contains another path *)
val contains : t -> t -> bool
@ -84,7 +84,7 @@ end = struct
type _stats = stats
let compare__stats _ _ = 0
type _procname = Procname.t
type _procname = Typ.Procname.t
let compare__procname _ _ = 0
type _string_option = string option
@ -434,9 +434,9 @@ end = struct
match Procdesc.Node.get_kind curr_node with
| Procdesc.Node.Join_node -> () (* omit join nodes from error traces *)
| Procdesc.Node.Start_node pname ->
let name = Procname.to_string pname in
let name_id = Procname.to_filename pname in
let descr = "start of procedure " ^ (Procname.to_simplified_string pname) in
let name = Typ.Procname.to_string pname in
let name_id = Typ.Procname.to_filename pname in
let descr = "start of procedure " ^ (Typ.Procname.to_simplified_string pname) in
let node_tags =
[(Io_infer.Xml.tag_kind,"procedure_start");
(Io_infer.Xml.tag_name, name);
@ -459,9 +459,9 @@ end = struct
(Io_infer.Xml.tag_branch, if is_true_branch then "true" else "false")] in
trace := Errlog.make_trace_element level curr_loc descr node_tags :: !trace
| Procdesc.Node.Exit_node pname ->
let descr = "return from a call to " ^ (Procname.to_string pname) in
let name = Procname.to_string pname in
let name_id = Procname.to_filename pname in
let descr = "return from a call to " ^ (Typ.Procname.to_string pname) in
let name = Typ.Procname.to_string pname in
let name_id = Typ.Procname.to_filename pname in
let node_tags =
[(Io_infer.Xml.tag_kind,"procedure_end");
(Io_infer.Xml.tag_name, name);

@ -19,7 +19,7 @@ module Path : sig
type session = int
(** add a call with its sub-path, the boolean indicates whether the subtrace for the procedure should be included *)
val add_call : bool -> t -> Procname.t -> t -> t
val add_call : bool -> t -> Typ.Procname.t -> t -> t
(** check whether a path contains another path *)
val contains : t -> t -> bool

@ -37,7 +37,7 @@ let add_dispatch_calls pdesc cg tenv =
receiver_typ in
let sorted_overrides =
let overrides = Prover.get_overrides_of tenv receiver_typ_no_ptr callee_pname in
List.sort ~cmp:(fun (_, p1) (_, p2) -> Procname.compare p1 p2) overrides in
List.sort ~cmp:(fun (_, p1) (_, p2) -> Typ.Procname.compare p1 p2) overrides in
(match sorted_overrides with
| ((_, target_pname) :: _) as all_targets ->
let targets_to_add =
@ -192,7 +192,7 @@ let remove_dead_frontend_stores pdesc liveness_inv_map =
let add_nullify_instrs pdesc tenv liveness_inv_map =
let address_taken_vars =
if Procname.is_java (Procdesc.get_proc_name pdesc)
if Typ.Procname.is_java (Procdesc.get_proc_name pdesc)
then AddressTaken.Domain.empty (* can't take the address of a variable in Java *)
else
let initial = AddressTaken.Domain.empty in
@ -312,7 +312,7 @@ let do_abstraction pdesc =
let do_dynamic_dispatch pdesc cg tenv =
let pname = Procdesc.get_proc_name pdesc in
if Procname.is_java pname &&
if Typ.Procname.is_java pname &&
(Config.dynamic_dispatch = `Interface || Config.dynamic_dispatch = `Sound)
then add_dispatch_calls pdesc cg tenv;
Procdesc.signal_did_preanalysis pdesc

@ -97,10 +97,10 @@ let is_visited node =
when starting and finishing the processing of a node *)
module NodesHtml : sig
val start_node :
int -> Location.t -> Procname.t -> Procdesc.Node.t list ->
int -> Location.t -> Typ.Procname.t -> Procdesc.Node.t list ->
Procdesc.Node.t list -> Procdesc.Node.t list ->
SourceFile.t -> bool
val finish_node : Procname.t -> int -> SourceFile.t -> unit
val finish_node : Typ.Procname.t -> int -> SourceFile.t -> unit
end = struct
let log_files = Hashtbl.create 11
@ -123,7 +123,7 @@ end = struct
loc.Location.line;
F.fprintf fmt "PROC: %a LINE:%a\n"
(Io_infer.Html.pp_proc_link [".."] proc_name)
(Escape.escape_xml (Procname.to_string proc_name))
(Escape.escape_xml (Typ.Procname.to_string proc_name))
(Io_infer.Html.pp_line_link source [".."]) loc.Location.line;
F.fprintf fmt "<br>PREDS:@\n";
List.iter ~f:(fun node ->
@ -423,10 +423,10 @@ let write_proc_html source whole_seconds pdesc =
let fd, fmt =
Io_infer.Html.create
(DB.Results_dir.Abs_source_dir source)
[Procname.to_filename pname] in
[Typ.Procname.to_filename pname] in
F.fprintf fmt "<center><h1>Procedure %a</h1></center>@\n"
(Io_infer.Html.pp_line_link source
~text: (Some (Escape.escape_xml (Procname.to_string pname)))
~text: (Some (Escape.escape_xml (Typ.Procname.to_string pname)))
[])
linenum;
List.iter
@ -556,7 +556,7 @@ let write_html_file linereader filename procs =
| Procdesc.Node.Start_node proc_name ->
let num_specs = List.length (Specs.get_specs proc_name) in
let label =
(Escape.escape_xml (Procname.to_string proc_name)) ^
(Escape.escape_xml (Typ.Procname.to_string proc_name)) ^
": " ^
(string_of_int num_specs) ^
" specs" in

@ -1638,7 +1638,7 @@ let get_overrides_of tenv supertype pname =
| Tstruct name -> (
match Tenv.lookup tenv name with
| Some { methods } ->
List.exists ~f:(fun m -> Procname.equal pname m) methods
List.exists ~f:(fun m -> Typ.Procname.equal pname m) methods
| None ->
false
)
@ -1649,7 +1649,7 @@ let get_overrides_of tenv supertype pname =
if not (Typ.equal typ supertype) && Subtyping_check.check_subtype tenv typ supertype then
(* only select the ones that implement [pname] as overrides *)
let resolved_pname =
Procname.replace_class pname tname in
Typ.Procname.replace_class pname tname in
if typ_has_method resolved_pname typ then (typ, resolved_pname) :: overrides_acc
else overrides_acc
else overrides_acc in

@ -67,7 +67,7 @@ val get_bounds : Tenv.t -> Prop.normal Prop.t -> Exp.t -> IntLit.t option * IntL
(** {2 Abduction prover} *)
(** [check_implication p1 p2] returns true if [p1|-p2] *)
val check_implication : Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.exposed Prop.t -> bool
val check_implication : Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.exposed Prop.t -> bool
type check =
| Bounds_check
@ -86,7 +86,7 @@ type implication_result =
frame)] where [sub] is a substitution which instantiates the
primed vars of [p1] and [p2], which are assumed to be disjoint. *)
val check_implication_for_footprint :
Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.exposed Prop.t -> implication_result
Typ.Procname.t -> Tenv.t -> Prop.normal Prop.t -> Prop.exposed Prop.t -> implication_result
(** {2 Cover: miminum set of pi's whose disjunction is equivalent to true} *)
@ -112,7 +112,7 @@ sig
end
val get_overrides_of : Tenv.t -> Typ.t -> Procname.t -> (Typ.t * Procname.t) list
val get_overrides_of : Tenv.t -> Typ.t -> Typ.Procname.t -> (Typ.t * Typ.Procname.t) list

@ -445,7 +445,7 @@ let mk_ptsto_exp_footprint
| Config.Java -> Subtype.subtypes in
let create_ptsto footprint_part off0 = match root, off0, typ with
| Exp.Lvar pvar, [], Typ.Tfun _ ->
let fun_name = Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in
let fun_name = Typ.Procname.from_string_c_fun (Mangled.to_string (Pvar.get_name pvar)) in
let fun_exp = Exp.Const (Const.Cfun fun_name) in
([], Prop.mk_ptsto tenv root (Sil.Eexp (fun_exp, inst)) (Exp.Sizeof (typ, None, st)))
| _, [], Typ.Tfun _ ->
@ -651,9 +651,9 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
let dollar_normalize s = String.map s ~f:(function '$' -> '.' | c -> c) in
String.is_suffix ~suffix:(dollar_normalize guarded_by_str) (dollar_normalize (class_str ^ ".class")) in
let guarded_by_str_is_current_class guarded_by_str = function
| Procname.Java java_pname ->
| Typ.Procname.Java java_pname ->
(* programmers write @GuardedBy("MyClass.class") when the field is guarded by the class *)
guarded_by_str_is_class guarded_by_str (Procname.java_get_class_name java_pname)
guarded_by_str_is_class guarded_by_str (Typ.Procname.java_get_class_name java_pname)
| _ -> false in
let guarded_by_str_is_class_this class_name guarded_by_str =
@ -665,8 +665,8 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
(* return true if [guarded_by_str] is a suffix of "<name_of_super_class>.this" *)
let guarded_by_str_is_super_class_this guarded_by_str pname =
match pname with
| Procname.Java java_pname ->
let current_class_type_name = (Procname.java_get_class_type_name java_pname) in
| Typ.Procname.Java java_pname ->
let current_class_type_name = (Typ.Procname.java_get_class_type_name java_pname) in
let comparison class_type_name _ =
guarded_by_str_is_class_this (Typename.to_string class_type_name) guarded_by_str in
PatternMatch.supertype_exists tenv comparison current_class_type_name
@ -675,8 +675,8 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
(* return true if [guarded_by_str] is as suffix of "<name_of_current_class>.this" *)
let guarded_by_str_is_current_class_this guarded_by_str = function
| Procname.Java java_pname ->
guarded_by_str_is_class_this (Procname.java_get_class_name java_pname) guarded_by_str
| Typ.Procname.Java java_pname ->
guarded_by_str_is_class_this (Typ.Procname.java_get_class_name java_pname) guarded_by_str
| _ -> false in
let extract_guarded_by_str item_annot =
@ -804,7 +804,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
| None -> false in
let is_synchronized_on_class guarded_by_str =
guarded_by_str_is_current_class guarded_by_str pname &&
Procdesc.is_java_synchronized pdesc && Procname.java_is_static pname in
Procdesc.is_java_synchronized pdesc && Typ.Procname.java_is_static pname in
let warn accessed_fld guarded_by_str =
let loc = State.get_loc () in
let err_desc =
@ -825,7 +825,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
Procdesc.is_java_synchronized pdesc)
||
(guarded_by_str_is_current_class guarded_by_str pname &&
Procdesc.is_java_synchronized pdesc && Procname.java_is_static pname) ||
Procdesc.is_java_synchronized pdesc && Typ.Procname.java_is_static pname) ||
(* or the prop says we already have the lock *)
List.exists
~f:(function
@ -862,7 +862,7 @@ let add_guarded_by_constraints tenv prop lexp pdesc =
prop.Prop.sigma in
Procdesc.get_access pdesc <> PredSymb.Private &&
not (Annotations.pdesc_return_annot_ends_with pdesc Annotations.visibleForTesting) &&
not (Procname.java_is_access_method (Procdesc.get_proc_name pdesc)) &&
not (Typ.Procname.java_is_access_method (Procdesc.get_proc_name pdesc)) &&
not (is_accessible_through_local_ref lexp) &&
not guardedby_is_self_referential &&
not (proc_has_suppress_guarded_by_annot pdesc)
@ -1320,7 +1320,7 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc =
let is_nullable_attr = function
| Sil.Apred ((Aretval (pname, ret_attr) | Aundef (pname, ret_attr, _, _)), _)
when Annotations.ia_is_nullable ret_attr ->
nullable_obj_str := Some (Procname.to_string pname);
nullable_obj_str := Some (Typ.Procname.to_string pname);
true
| _ -> false in
List.exists ~f:is_nullable_attr (Attribute.get_for_exp tenv prop exp) in
@ -1492,8 +1492,8 @@ let rearrange ?(report_deref_errors=true) pdesc tenv lexp typ prop loc
if report_deref_errors then check_dereference_error tenv pdesc prop nlexp (State.get_loc ());
let pname = Procdesc.get_proc_name pdesc in
let prop' =
if Config.csl_analysis && !Config.footprint && Procname.is_java pname &&
not (Procname.is_constructor pname || Procname.is_class_initializer pname)
if Config.csl_analysis && !Config.footprint && Typ.Procname.is_java pname &&
not (Typ.Procname.is_constructor pname || Typ.Procname.is_class_initializer pname)
then add_guarded_by_constraints tenv prop lexp pdesc
else prop in
match Prop.prop_iter_create prop' with

@ -19,7 +19,7 @@ type log_t =
exn ->
unit
type log_issue = Procname.t -> log_t
type log_issue = Typ.Procname.t -> log_t
type log_issue_from_errlog = Errlog.t -> log_t
@ -64,8 +64,8 @@ let log_issue
failwithf
"Trying to report error on procedure %a, but cannot because no summary exists for this \
procedure. Did you mean to log the error on the caller of %a instead?"
Procname.pp proc_name
Procname.pp proc_name
Typ.Procname.pp proc_name
Typ.Procname.pp proc_name
let log_error = log_issue Exceptions.Kerror
let log_warning = log_issue Exceptions.Kwarning

@ -19,7 +19,7 @@ type log_t =
exn ->
unit
type log_issue = Procname.t -> log_t
type log_issue = Typ.Procname.t -> log_t
type log_issue_from_errlog = Errlog.t -> log_t

@ -225,9 +225,9 @@ let normalized_specs_to_specs =
module CallStats = struct (** module for tracing stats of function calls *)
module PnameLocHash = Hashtbl.Make (struct
type t = Procname.t * Location.t
let hash (pname, loc) = Hashtbl.hash (Procname.hash_pname pname, loc.Location.line)
let equal = [%compare.equal: Procname.t * Location.t]
type t = Typ.Procname.t * Location.t
let hash (pname, loc) = Hashtbl.hash (Typ.Procname.hash_pname pname, loc.Location.line)
let equal = [%compare.equal: Typ.Procname.t * Location.t]
end)
(** kind of result of a procedure call *)
@ -278,14 +278,14 @@ module CallStats = struct (** module for tracing stats of function calls *)
PnameLocHash.iter (fun x tr -> elems := (x, tr) :: !elems) t;
let sorted_elems =
let compare (pname_loc1, _) (pname_loc2, _) =
[%compare: Procname.t * Location.t] pname_loc1 pname_loc2 in
[%compare: Typ.Procname.t * Location.t] pname_loc1 pname_loc2 in
List.sort ~cmp:compare !elems in
List.iter ~f:(fun (x, tr) -> f x tr) sorted_elems
(*
let pp fmt t =
let do_call (pname, loc) tr =
F.fprintf fmt "%a %a: %a@\n" Procname.pp pname Location.pp loc pp_trace tr in
F.fprintf fmt "%a %a: %a@\n" Typ.Procname.pp pname Location.pp loc pp_trace tr in
iter do_call t
*)
end
@ -347,11 +347,11 @@ type summary = {
proc_desc_option : Procdesc.t option;
}
type spec_tbl = summary Procname.Hash.t
type spec_tbl = summary Typ.Procname.Hash.t
let spec_tbl: spec_tbl = Procname.Hash.create 128
let spec_tbl: spec_tbl = Typ.Procname.Hash.create 128
let clear_spec_tbl () = Procname.Hash.clear spec_tbl
let clear_spec_tbl () = Typ.Procname.Hash.clear spec_tbl
(** pretty print analysis time; if [whole_seconds] is true, only print time in seconds *)
let pp_time whole_seconds fmt t =
@ -430,7 +430,7 @@ let get_signature summary =
"%a %a"
(Typ.pp_full Pp.text)
summary.attributes.ProcAttributes.ret_type
Procname.pp summary.attributes.ProcAttributes.proc_name in
Typ.Procname.pp summary.attributes.ProcAttributes.proc_name in
let decl = F.asprintf "%t" pp in
decl ^ "(" ^ !s ^ ")"
@ -515,14 +515,14 @@ let summary_compact sh summary =
{ summary with payload = payload_compact sh summary.payload }
(** Add the summary to the table for the given function *)
let add_summary (proc_name : Procname.t) (summary: summary) : unit =
let add_summary (proc_name : Typ.Procname.t) (summary: summary) : unit =
L.out "Adding summary for %a@\n@[<v 2> %a@]@."
Procname.pp proc_name
Typ.Procname.pp proc_name
(pp_summary_text ~whole_seconds:false) summary;
Procname.Hash.replace spec_tbl proc_name summary
Typ.Procname.Hash.replace spec_tbl proc_name summary
let specs_filename pname =
let pname_file = Procname.to_filename pname in
let pname_file = Typ.Procname.to_filename pname in
pname_file ^ Config.specs_files_suffix
(** path to the .specs file for the given procedure in the current results directory *)
@ -582,7 +582,7 @@ let load_summary_to_spec_table proc_name =
let rec get_summary proc_name =
try
Some (Procname.Hash.find spec_tbl proc_name)
Some (Typ.Procname.Hash.find spec_tbl proc_name)
with Not_found ->
if load_summary_to_spec_table proc_name then
get_summary proc_name
@ -591,7 +591,7 @@ let rec get_summary proc_name =
let get_summary_unsafe s proc_name =
match get_summary proc_name with
| None ->
failwithf "[%s] Specs.get_summary_unsafe: %a Not found" s Procname.pp proc_name
failwithf "[%s] Specs.get_summary_unsafe: %a Not found" s Typ.Procname.pp proc_name
| Some summary -> summary
(** Check if the procedure is from a library:
@ -673,7 +673,7 @@ let get_flag summary key =
let get_specs_formals proc_name =
match get_summary proc_name with
| None ->
raise (Failure ("Specs.get_specs_formals: " ^ (Procname.to_string proc_name) ^ "Not_found"))
raise (Failure ("Specs.get_specs_formals: " ^ (Typ.Procname.to_string proc_name) ^ "Not_found"))
| Some summary ->
let specs = get_specs_from_payload summary in
let formals = get_formals summary in
@ -709,7 +709,7 @@ let store_summary (summ1: summary) =
(** Set the current status for the proc *)
let set_status proc_name status =
match get_summary proc_name with
| None -> raise (Failure ("Specs.set_status: " ^ (Procname.to_string proc_name) ^ " Not_found"))
| None -> raise (Failure ("Specs.set_status: " ^ (Typ.Procname.to_string proc_name) ^ " Not_found"))
| Some summary -> add_summary proc_name { summary with status = status }
let empty_payload =
@ -745,7 +745,7 @@ let init_summary
ProcAttributes.proc_flags = proc_flags; };
proc_desc_option;
} in
Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name summary
Typ.Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name summary
(** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
let reset_summary proc_name attributes_opt proc_desc_option =

@ -94,10 +94,10 @@ module CallStats : sig
type trace = (call_result * bool) list
(** iterate over results of procedure calls *)
val iter : (Procname.t * Location.t -> trace -> unit) -> t -> unit
val iter : (Typ.Procname.t * Location.t -> trace -> unit) -> t -> unit
(** trace a procedure call *)
val trace : t -> Procname.t -> Location.t -> call_result -> bool -> unit
val trace : t -> Typ.Procname.t -> Location.t -> call_result -> bool -> unit
(** pretty print a call trace *)
val pp_trace : Format.formatter -> trace -> unit
@ -159,10 +159,10 @@ type summary = {
}
(** Add the summary to the table for the given function *)
val add_summary : Procname.t -> summary -> unit
val add_summary : Typ.Procname.t -> summary -> unit
(** Check if a summary for a given procedure exists in the models directory *)
val summary_exists_in_models : Procname.t -> bool
val summary_exists_in_models : Typ.Procname.t -> bool
(** remove all the elements from the spec table *)
val clear_spec_tbl : unit -> unit
@ -171,10 +171,10 @@ val clear_spec_tbl : unit -> unit
val d_spec : 'a spec -> unit
(** Return the summary option for the procedure name *)
val get_summary : Procname.t -> summary option
val get_summary : Typ.Procname.t -> summary option
(** Get the procedure name *)
val get_proc_name : summary -> Procname.t
val get_proc_name : summary -> Typ.Procname.t
(** Get the attributes of the procedure. *)
val get_attributes : summary -> ProcAttributes.t
@ -195,16 +195,16 @@ val get_phase : summary -> phase
val get_signature : summary -> string
(** Return the specs for the proc in the spec table *)
val get_specs : Procname.t -> Prop.normal spec list
val get_specs : Typ.Procname.t -> Prop.normal spec list
(** Return the specs and formal parameters for the proc in the spec table *)
val get_specs_formals : Procname.t -> Prop.normal spec list * (Mangled.t * Typ.t) list
val get_specs_formals : Typ.Procname.t -> Prop.normal spec list * (Mangled.t * Typ.t) list
(** Get the specs from the payload of the summary. *)
val get_specs_from_payload : summary -> Prop.normal spec list
(** @deprecated Return the summary for the procedure name. Raises an exception when not found. *)
val get_summary_unsafe : string -> Procname.t -> summary
val get_summary_unsafe : string -> Typ.Procname.t -> summary
(** Return the status (active v.s. inactive) of a procedure summary *)
val get_status : summary -> status
@ -217,19 +217,19 @@ val is_active : summary -> bool
val init_summary :
( Procdesc.Node.id list * (* nodes *)
ProcAttributes.proc_flags * (* procedure flags *)
(Procname.t * Location.t) list * (* calls *)
(Typ.Procname.t * Location.t) list * (* calls *)
ProcAttributes.t * (* attributes of the procedure *)
Procdesc.t option) (* procdesc option *)
-> unit
(** Reset a summary rebuilding the dependents and preserving the proc attributes if present. *)
val reset_summary : Procname.t -> ProcAttributes.t option -> Procdesc.t option -> unit
val reset_summary : Typ.Procname.t -> ProcAttributes.t option -> Procdesc.t option -> unit
(** Load procedure summary from the given file *)
val load_summary : DB.filename -> summary option
(** Check if a procedure summary exists for the given procedure name *)
val summary_exists : Procname.t -> bool
val summary_exists : Typ.Procname.t -> bool
(** Cast a list of normalized specs to a list of specs *)
val normalized_specs_to_specs : NormSpec.t list -> Prop.normal spec list
@ -258,20 +258,20 @@ val pdesc_resolve_attributes : Procdesc.t -> ProcAttributes.t
then look at the attributes table.
If no attributes can be found, return None.
*)
val proc_resolve_attributes : Procname.t -> ProcAttributes.t option
val proc_resolve_attributes : Typ.Procname.t -> ProcAttributes.t option
(** Check if the procedure is from a library:
It's not defined, and there is no spec file for it. *)
val proc_is_library : ProcAttributes.t -> bool
(** Set the current status for the proc *)
val set_status : Procname.t -> status -> unit
val set_status : Typ.Procname.t -> status -> unit
(** Convert spec into normal form w.r.t. variable renaming *)
val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t
(** path to the .specs file for the given procedure in the current results dir *)
val res_dir_specs_filename : Procname.t -> DB.filename
val res_dir_specs_filename : Typ.Procname.t -> DB.filename
(** Save summary for the procedure into the spec database *)
val store_summary : summary -> unit

@ -275,7 +275,7 @@ let get_session () =
let get_path_pos () =
let pname = match get_prop_tenv_pdesc () with
| Some (_, _, pdesc) -> Procdesc.get_proc_name pdesc
| None -> Procname.from_string_c_fun "unknown_procedure" in
| None -> Typ.Procname.from_string_c_fun "unknown_procedure" in
let nid = get_node_id () in
(pname, (nid :> int))
@ -307,7 +307,7 @@ let mark_instr_fail exn =
fs.instr_fail <- fs.instr_fail + 1
type log_issue =
Procname.t ->
Typ.Procname.t ->
?loc: Location.t ->
?node_id: (int * int) ->
?session: int ->

@ -85,7 +85,7 @@ val mark_instr_ok : unit -> unit
val mk_find_duplicate_nodes: Procdesc.t -> (Procdesc.Node.t -> Procdesc.NodeSet.t)
type log_issue =
Procname.t ->
Typ.Procname.t ->
?loc: Location.t ->
?node_id: (int * int) ->
?session: int ->
@ -94,7 +94,7 @@ type log_issue =
unit
(** Process the failures during symbolic execution of a procedure *)
val process_execution_failures : log_issue -> Procname.t -> unit
val process_execution_failures : log_issue -> Typ.Procname.t -> unit
(** Reset all the global data. *)
val reset : unit -> unit

@ -55,7 +55,7 @@ let get_blocks_nullified node =
captured variables in the block we obtain a leak. *)
let check_block_retain_cycle tenv caller_pname prop block_nullified =
let mblock = Pvar.get_name block_nullified in
let block_pname = Procname.mangled_objc_block (Mangled.to_string mblock) in
let block_pname = Typ.Procname.mangled_objc_block (Mangled.to_string mblock) in
let block_captured =
match AttributesTable.load_attributes block_pname with
| Some attributes ->
@ -366,10 +366,10 @@ and prune_union tenv ~positive condition1 condition2 prop =
let dangerous_functions =
let dangerous_list = ["gets"] in
ref ((List.map ~f:Procname.from_string_c_fun) dangerous_list)
ref ((List.map ~f:Typ.Procname.from_string_c_fun) dangerous_list)
let check_inherently_dangerous_function caller_pname callee_pname =
if List.exists ~f:(Procname.equal callee_pname) !dangerous_functions then
if List.exists ~f:(Typ.Procname.equal callee_pname) !dangerous_functions then
let exn =
Exceptions.Inherently_dangerous_function
(Localise.desc_inherently_dangerous_function callee_pname) in
@ -472,7 +472,7 @@ let check_deallocate_static_memory prop_after =
let method_exists right_proc_name methods =
if Config.curr_language_is Config.Java then
List.exists ~f:(fun meth_name -> Procname.equal right_proc_name meth_name) methods
List.exists ~f:(fun meth_name -> Typ.Procname.equal right_proc_name meth_name) methods
else (* ObjC/C++ case : The attribute map will only exist when we have code for the method or
the method has been called directly somewhere. It can still be that this is not the
case but we have a model for the method. *)
@ -486,7 +486,7 @@ let resolve_method tenv class_name proc_name =
let rec resolve (class_name: Typename.t) =
visited := Typename.Set.add class_name !visited;
let right_proc_name =
Procname.replace_class proc_name class_name in
Typ.Procname.replace_class proc_name class_name in
match class_name, Tenv.lookup tenv class_name with
| TN_csu (Class _, _), Some { methods; supers } ->
if method_exists right_proc_name methods then
@ -521,15 +521,15 @@ let resolve_typename prop receiver_exp =
(** If the dynamic type of the receiver actual T_actual is a subtype of the reciever type T_formal
in the signature of [pname], resolve [pname] to T_actual.[pname]. *)
let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t list =
let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Typ.Procname.t list =
let resolve receiver_exp pname prop = match resolve_typename prop receiver_exp with
| Some class_name -> resolve_method tenv class_name pname
| None -> pname in
let get_receiver_typ pname fallback_typ =
match pname with
| Procname.Java pname_java ->
| Typ.Procname.Java pname_java ->
begin
let name = Procname.java_get_class_type_name pname_java in
let name = Typ.Procname.java_get_class_type_name pname_java in
match Tenv.lookup tenv name with
| Some _ -> Typ.Tptr (Tstruct name, Pk_pointer)
| None -> fallback_typ
@ -568,7 +568,7 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t
let resolved_pname = do_resolve callee_pname receiver_exp actual_receiver_typ in
let feasible_targets = List.filter ~f:may_dispatch_to targets in
(* make sure [resolved_pname] is not a duplicate *)
if List.mem ~equal:Procname.equal feasible_targets resolved_pname
if List.mem ~equal:Typ.Procname.equal feasible_targets resolved_pname
then feasible_targets
else resolved_pname :: feasible_targets
else
@ -577,7 +577,7 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t
match call_flags.CallFlags.cf_targets with
| target :: _ when call_flags.CallFlags.cf_interface &&
receiver_types_equal callee_pname actual_receiver_typ &&
Procname.equal resolved_target callee_pname ->
Typ.Procname.equal resolved_target callee_pname ->
(* "production mode" of dynamic dispatch for Java: unsound, but faster. the handling
is restricted to interfaces: if we can't resolve an interface call, we pick the
first implementation of the interface and call it *)
@ -590,9 +590,9 @@ let resolve_virtual_pname tenv prop actuals callee_pname call_flags : Procname.t
(** Resolve the name of the procedure to call based on the type of the arguments *)
let resolve_java_pname tenv prop args pname_java call_flags : Procname.java =
let resolve_java_pname tenv prop args pname_java call_flags : Typ.Procname.java =
let resolve_from_args resolved_pname_java args =
let parameters = Procname.java_get_parameters resolved_pname_java in
let parameters = Typ.Procname.java_get_parameters resolved_pname_java in
if List.length args <> List.length parameters then
resolved_pname_java
else
@ -601,10 +601,10 @@ let resolve_java_pname tenv prop args pname_java call_flags : Procname.java =
~f:(fun accu (arg_exp, _) name ->
match resolve_typename prop arg_exp with
| Some class_name ->
(Procname.split_classname (Typename.name class_name)) :: accu
(Typ.Procname.split_classname (Typename.name class_name)) :: accu
| None -> name :: accu)
~init:[] args (Procname.java_get_parameters resolved_pname_java) |> List.rev in
Procname.java_replace_parameters resolved_pname_java resolved_params in
~init:[] args (Typ.Procname.java_get_parameters resolved_pname_java) |> List.rev in
Typ.Procname.java_replace_parameters resolved_pname_java resolved_params in
let resolved_pname_java, other_args =
match args with
| [] ->
@ -615,8 +615,8 @@ let resolve_java_pname tenv prop args pname_java call_flags : Procname.java =
match resolve_typename prop first_arg with
| Some class_name ->
begin
match resolve_method tenv class_name (Procname.Java pname_java) with
| Procname.Java resolved_pname_java ->
match resolve_method tenv class_name (Typ.Procname.Java pname_java) with
| Typ.Procname.Java resolved_pname_java ->
resolved_pname_java
| _ ->
pname_java
@ -625,7 +625,7 @@ let resolve_java_pname tenv prop args pname_java call_flags : Procname.java =
pname_java
end in
resolved, other_args
| _ :: other_args when Procname.is_constructor (Procname.Java pname_java) ->
| _ :: other_args when Typ.Procname.is_constructor (Typ.Procname.Java pname_java) ->
pname_java, other_args
| args ->
pname_java, args in
@ -635,11 +635,11 @@ let resolve_java_pname tenv prop args pname_java call_flags : Procname.java =
(** Resolve the procedure name and run the analysis of the resolved procedure
if not already analyzed *)
let resolve_and_analyze
tenv caller_pdesc prop args callee_proc_name call_flags : Procname.t * Specs.summary option =
tenv caller_pdesc prop args callee_proc_name call_flags : Typ.Procname.t * Specs.summary option =
(* TODO (#15748878): Fix conflict with method overloading by encoding in the procedure name
whether the method is defined or generated by the specialization *)
let analyze_ondemand resolved_pname : Specs.summary option =
if Procname.equal resolved_pname callee_proc_name then
if Typ.Procname.equal resolved_pname callee_proc_name then
Ondemand.analyze_proc_name ~propagate_exceptions:true caller_pdesc callee_proc_name
else
(* Create the type sprecialized procedure description and analyze it directly *)
@ -656,8 +656,8 @@ let resolve_and_analyze
(Ondemand.get_proc_desc callee_proc_name)) in
Option.bind resolved_proc_desc_option analyze in
let resolved_pname = match callee_proc_name with
| Procname.Java callee_proc_name_java ->
Procname.Java
| Typ.Procname.Java callee_proc_name_java ->
Typ.Procname.Java
(resolve_java_pname tenv prop args callee_proc_name_java call_flags)
| _ ->
callee_proc_name in
@ -668,11 +668,11 @@ let resolve_and_analyze
to be only the protocol. *)
let call_constructor_url_update_args pname actual_params =
let url_pname =
Procname.Java
(Procname.java
Typ.Procname.Java
(Typ.Procname.java
(Typename.Java.from_string "java.net.URL") None "<init>"
[(Some "java.lang"), "String"] Procname.Non_Static) in
if (Procname.equal url_pname pname) then
[(Some "java.lang"), "String"] Typ.Procname.Non_Static) in
if (Typ.Procname.equal url_pname pname) then
(match actual_params with
| [this; (Exp.Const (Const.Cstr s), atype)] ->
let parts = Str.split (Str.regexp_string "://") s in
@ -705,9 +705,9 @@ let receiver_self receiver prop =
a check for null, which is considered good practice. *)
let force_objc_init_return_nil pdesc callee_pname tenv ret_id pre path receiver =
let current_pname = Procdesc.get_proc_name pdesc in
if Procname.is_constructor callee_pname &&
if Typ.Procname.is_constructor callee_pname &&
receiver_self receiver pre &&
!Config.footprint && Procname.is_constructor current_pname then
!Config.footprint && Typ.Procname.is_constructor current_pname then
match ret_id with
| Some (ret_id, _) ->
let propset = prune_ne tenv ~positive:false (Exp.Var ret_id) Exp.zero pre in
@ -728,7 +728,7 @@ let handle_objc_instance_method_call_or_skip pdesc tenv actual_pars path callee_
ret_id res =
let path_description =
"Message " ^
(Procname.to_simplified_string callee_pname) ^
(Typ.Procname.to_simplified_string callee_pname) ^
" with receiver nil returns nil." in
let receiver = (match actual_pars with
| (e, _):: _ -> e
@ -756,7 +756,7 @@ let handle_objc_instance_method_call_or_skip pdesc tenv actual_pars path callee_
let path = Paths.Path.add_description path path_description in
L.d_strln
("Object-C method " ^
Procname.to_string callee_pname ^
Typ.Procname.to_string callee_pname ^
" called with nil receiver. Returning 0/nil");
(* We wish to nullify the result. However, in some cases,
we want to add the attribute OBJC_NULL to it so that we *)
@ -826,10 +826,10 @@ let add_struct_value_to_footprint tenv abduced_pv typ prop =
prop', struct_strexp
let add_constraints_on_retval tenv pdesc prop ret_exp ~has_nullable_annot typ callee_pname callee_loc=
if Procname.is_infer_undefined callee_pname then prop
if Typ.Procname.is_infer_undefined callee_pname then prop
else
let is_rec_call pname = (* TODO: (t7147096) extend this to detect mutual recursion *)
Procname.equal pname (Procdesc.get_proc_name pdesc) in
Typ.Procname.equal pname (Procdesc.get_proc_name pdesc) in
let already_has_abduced_retval p abduced_ret_pv =
List.exists
~f:(fun hpred -> match hpred with
@ -1028,7 +1028,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in
Reporting.log_info current_pname exn;
L.d_strln
("Undefined function " ^ Procname.to_string callee_pname
("Undefined function " ^ Typ.Procname.to_string callee_pname
^ ", returning undefined value.");
(match Specs.get_summary current_pname with
| None -> ()
@ -1155,8 +1155,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
let attrs_opt =
let attr_opt = Option.map ~f:Procdesc.get_attributes callee_pdesc_opt in
match attr_opt, resolved_pname with
| Some attrs, Procname.ObjC_Cpp _ -> Some attrs
| None, Procname.ObjC_Cpp _ -> AttributesTable.load_attributes resolved_pname
| Some attrs, Typ.Procname.ObjC_Cpp _ -> Some attrs
| None, Typ.Procname.ObjC_Cpp _ -> AttributesTable.load_attributes resolved_pname
| _ -> None in
let objc_property_accessor_ret_typ_opt =
match attrs_opt with
@ -1203,7 +1203,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
end else begin
L.d_str "Unknown function pointer "; Sil.d_exp fun_exp;
L.d_strln ", returning undefined value.";
let callee_pname = Procname.from_string_c_fun "__function_pointer__" in
let callee_pname = Typ.Procname.from_string_c_fun "__function_pointer__" in
unknown_or_scan_call ~is_scan:false None Annot.Item.empty Builtin.{
pdesc= current_pdesc; instr; tenv; prop_= prop_r; path; ret_id; args= n_actual_params;
proc_name= callee_pname; loc; }
@ -1439,7 +1439,7 @@ and unknown_or_scan_call ~is_scan ret_type_option ret_annots
let pre_final =
(* in Java, assume that skip functions close resources passed as params *)
let pre_1 =
if Procname.is_java callee_pname
if Typ.Procname.is_java callee_pname
then remove_file_attribute pre
else pre in
let pre_2 = match ret_id, ret_type_option with
@ -1588,7 +1588,7 @@ and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_id; args= actu
L.d_str "formal parameters: "; Typ.d_list formal_types; L.d_ln ();
actual_pars
| [], _ ->
L.d_str ("**** ERROR: Procedure " ^ Procname.to_string callee_pname);
L.d_str ("**** ERROR: Procedure " ^ Typ.Procname.to_string callee_pname);
L.d_strln (" mismatch in the number of parameters ****");
L.d_str "actual parameters: "; Sil.d_exp_list (List.map ~f:fst actual_pars); L.d_ln ();
L.d_str "formal parameters: "; Typ.d_list formal_types; L.d_ln ();

@ -32,12 +32,12 @@ val unknown_or_scan_call : is_scan:bool -> Typ.t option -> Annot.Item.t -> Built
val check_variadic_sentinel : ?fails_on_nil:bool -> int -> int * int -> Builtin.t
val check_untainted :
Tenv.t -> Exp.t -> PredSymb.taint_kind -> Procname.t -> Procname.t -> Prop.normal Prop.t ->
Tenv.t -> Exp.t -> PredSymb.taint_kind -> Typ.Procname.t -> Typ.Procname.t -> Prop.normal Prop.t ->
Prop.normal Prop.t
(** Check for arithmetic problems and normalize an expression. *)
val check_arith_norm_exp :
Tenv.t -> Procname.t -> Exp.t -> Prop.normal Prop.t -> Exp.t * Prop.normal Prop.t
Tenv.t -> Typ.Procname.t -> Exp.t -> Prop.normal Prop.t -> Exp.t * Prop.normal Prop.t
val prune : Tenv.t -> positive:bool -> Exp.t -> Prop.normal Prop.t -> Propset.t
@ -45,4 +45,4 @@ val prune : Tenv.t -> positive:bool -> Exp.t -> Prop.normal Prop.t -> Propset.t
the procname that the method name will actually resolve to at runtime. For example, if we have a
procname like Foo.toString() and Foo does not override toString(), we must resolve the call to
toString(). We will end up with Super.toString() where Super is some superclass of Foo. *)
val resolve_method : Tenv.t -> Typename.t -> Procname.t -> Procname.t
val resolve_method : Tenv.t -> Typename.t -> Typ.Procname.t -> Typ.Procname.t

@ -30,7 +30,7 @@ type deref_error =
| Deref_freed of PredSymb.res_action (** dereference a freed pointer *)
| Deref_minusone (** dereference -1 *)
| Deref_null of PredSymb.path_pos (** dereference null *)
| Deref_undef of Procname.t * Location.t * PredSymb.path_pos
| Deref_undef of Typ.Procname.t * Location.t * PredSymb.path_pos
(** dereference a value coming from the given undefined function *)
| Deref_undef_exp (** dereference an undefined expression *)
@ -116,7 +116,7 @@ let spec_rename_vars pname spec =
(** Find and number the specs for [proc_name],
after renaming their vars, and also return the parameters *)
let spec_find_rename trace_call (proc_name : Procname.t)
let spec_find_rename trace_call (proc_name : Typ.Procname.t)
: (int * Prop.exposed Specs.spec) list * Pvar.t list =
try
let count = ref 0 in
@ -127,7 +127,7 @@ let spec_find_rename trace_call (proc_name : Procname.t)
begin
trace_call Specs.CallStats.CR_not_found;
raise (Exceptions.Precondition_not_found
(Localise.verbatim_desc (Procname.to_string proc_name), __POS__))
(Localise.verbatim_desc (Typ.Procname.to_string proc_name), __POS__))
end;
let formal_parameters =
List.map ~f:(fun (x, _) -> Pvar.mk_callee x proc_name) formals in
@ -135,10 +135,10 @@ let spec_find_rename trace_call (proc_name : Procname.t)
with Not_found -> begin
L.d_strln
("ERROR: found no entry for procedure " ^
Procname.to_string proc_name ^
Typ.Procname.to_string proc_name ^
". Give up...");
raise (Exceptions.Precondition_not_found
(Localise.verbatim_desc (Procname.to_string proc_name), __POS__))
(Localise.verbatim_desc (Typ.Procname.to_string proc_name), __POS__))
end
(** Process a splitting coming straight from a call to the prover:
@ -898,7 +898,7 @@ let mk_posts tenv ret_id prop callee_pname callee_attrs posts =
let last_call_ret_non_null =
List.exists
~f:(function
| Sil.Apred (Aretval (pname, _), [exp]) when Procname.equal callee_pname pname ->
| Sil.Apred (Aretval (pname, _), [exp]) when Typ.Procname.equal callee_pname pname ->
Prover.check_disequal tenv prop exp Exp.zero
| _ -> false)
(Attribute.get_all prop) in
@ -1264,8 +1264,8 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re
let returns_nullable ret_annot = Annotations.ia_is_nullable ret_annot in
let should_add_ret_attr _ =
let is_likely_getter = function
| Procname.Java pn_java ->
Int.equal (List.length (Procname.java_get_parameters pn_java)) 0
| Typ.Procname.Java pn_java ->
Int.equal (List.length (Typ.Procname.java_get_parameters pn_java)) 0
| _ ->
false in
(Config.idempotent_getters &&
@ -1298,8 +1298,8 @@ let exe_function_call
("Found " ^
string_of_int nspecs ^
" specs for function " ^
Procname.to_string callee_pname);
L.d_strln ("START EXECUTING SPECS FOR " ^ Procname.to_string callee_pname ^ " from state");
Typ.Procname.to_string callee_pname);
L.d_strln ("START EXECUTING SPECS FOR " ^ Typ.Procname.to_string callee_pname ^ " from state");
Prop.d_prop prop; L.d_ln ();
let exe_one_spec (n, spec) =
exe_spec

@ -28,13 +28,13 @@ val find_dereference_without_null_check_in_sexp : Sil.strexp -> (int * PredSymb.
(** raise a cast exception *)
val create_cast_exception :
Tenv.t -> Logging.ml_loc -> Procname.t option -> Exp.t -> Exp.t -> Exp.t -> exn
Tenv.t -> Logging.ml_loc -> Typ.Procname.t option -> Exp.t -> Exp.t -> Exp.t -> exn
(** check if a prop is an exception *)
val prop_is_exn : Procname.t -> 'a Prop.t -> bool
val prop_is_exn : Typ.Procname.t -> 'a Prop.t -> bool
(** when prop is an exception, return the exception name *)
val prop_get_exn_name : Procname.t -> 'a Prop.t -> Typename.t option
val prop_get_exn_name : Typ.Procname.t -> 'a Prop.t -> Typename.t option
(** search in prop contains an error state *)
val lookup_custom_errors : 'a Prop.t -> string option
@ -44,6 +44,6 @@ val d_splitting : splitting -> unit
(** Execute the function call and return the list of results with return value *)
val exe_function_call:
ProcAttributes.t -> Tenv.t -> (Ident.t * Typ.t) option -> Procdesc.t -> Procname.t ->
ProcAttributes.t -> Tenv.t -> (Ident.t * Typ.t) option -> Procdesc.t -> Typ.Procname.t ->
Location.t -> (Exp.t * Typ.t) list -> Prop.normal Prop.t -> Paths.Path.t ->
(Prop.normal Prop.t * Paths.Path.t) list

@ -262,20 +262,20 @@ let functions_with_tainted_params = [
(* turn string specificiation of Java method into a procname *)
let java_method_to_procname java_method =
Procname.Java
(Procname.java
Typ.Procname.Java
(Typ.Procname.java
(Typename.Java.from_string java_method.classname)
(Some (Procname.split_classname java_method.ret_type))
(Some (Typ.Procname.split_classname java_method.ret_type))
java_method.method_name
(List.map ~f:Procname.split_classname java_method.params)
(if java_method.is_static then Procname.Static else Procname.Non_Static))
(List.map ~f:Typ.Procname.split_classname java_method.params)
(if java_method.is_static then Typ.Procname.Static else Typ.Procname.Non_Static))
(* turn string specificiation of an objc method into a procname *)
let objc_method_to_procname objc_method =
let method_kind = Procname.objc_method_kind_of_bool (not objc_method.is_static) in
let method_kind = Typ.Procname.objc_method_kind_of_bool (not objc_method.is_static) in
let typename = Typename.Objc.from_string objc_method.classname in
Procname.ObjC_Cpp
(Procname.objc_cpp typename objc_method.method_name method_kind)
Typ.Procname.ObjC_Cpp
(Typ.Procname.objc_cpp typename objc_method.method_name method_kind)
let taint_spec_to_taint_info taint_spec =
let taint_source =
@ -306,7 +306,7 @@ let attrs_opt_get_annots = function
(** returns true if [callee_pname] returns a tainted value *)
let returns_tainted callee_pname callee_attrs_opt =
let procname_matches taint_info =
Procname.equal taint_info.PredSymb.taint_source callee_pname in
Typ.Procname.equal taint_info.PredSymb.taint_source callee_pname in
match List.find ~f:procname_matches sources with
| Some taint_info ->
Some taint_info.PredSymb.taint_kind
@ -320,7 +320,7 @@ let returns_tainted callee_pname callee_attrs_opt =
let find_callee taint_infos callee_pname =
List.find
~f:(fun (taint_info, _) -> Procname.equal taint_info.PredSymb.taint_source callee_pname)
~f:(fun (taint_info, _) -> Typ.Procname.equal taint_info.PredSymb.taint_source callee_pname)
taint_infos
(** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *)
@ -328,7 +328,7 @@ let accepts_sensitive_params callee_pname callee_attrs_opt =
match find_callee taint_sinks callee_pname with
| None ->
let _, param_annots = attrs_opt_get_annots callee_attrs_opt in
let offset = if Procname.java_is_static callee_pname then 0 else 1 in
let offset = if Typ.Procname.java_is_static callee_pname then 0 else 1 in
let indices_and_annots =
List.mapi ~f:(fun param_num attr -> param_num + offset, attr) param_annots in
let tag_tainted_indices acc (index, attr) =

@ -10,15 +10,15 @@
open! IStd
(** returns true if [callee_pname] returns a tainted value *)
val returns_tainted : Procname.t -> ProcAttributes.t option -> PredSymb.taint_kind option
val returns_tainted : Typ.Procname.t -> ProcAttributes.t option -> PredSymb.taint_kind option
(** returns list of zero-indexed argument numbers of [callee_pname] that may be tainted *)
val accepts_sensitive_params :
Procname.t -> ProcAttributes.t option -> (int * PredSymb.taint_kind) list
Typ.Procname.t -> ProcAttributes.t option -> (int * PredSymb.taint_kind) list
(** returns list of zero-indexed parameter numbers of [callee_pname] that should be
considered tainted during symbolic execution *)
val tainted_params : 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 *)
val has_taint_annotation : Ident.fieldname -> Typ.Struct.t -> bool

@ -33,7 +33,7 @@ struct
module Domain = Dom.Mem
module Sem = BufferOverrunSemantics.Make (CFG)
type extras = Procname.t -> Procdesc.t option
type extras = Typ.Procname.t -> Procdesc.t option
(* NOTE: heuristic *)
let get_malloc_info : Exp.t -> Typ.t * Exp.t
@ -44,7 +44,7 @@ struct
| x -> (Typ.Tint Typ.IChar, x)
let model_malloc
: Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node
: Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node
-> Dom.Mem.t -> Dom.Mem.t
= fun pname ret params node mem ->
match ret with
@ -56,7 +56,7 @@ struct
| _ -> mem
let model_realloc
: Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node
: Typ.Procname.t -> (Ident.t * Typ.t) option -> (Exp.t * Typ.t) list -> CFG.node
-> Dom.Mem.t -> Dom.Mem.t
= fun pname ret params node mem ->
model_malloc pname ret (List.tl_exn params) node mem
@ -87,11 +87,11 @@ struct
| _ -> mem
let handle_unknown_call
: Procname.t -> (Ident.t * Typ.t) option -> Procname.t
: Typ.Procname.t -> (Ident.t * Typ.t) option -> Typ.Procname.t
-> (Exp.t * Typ.t) list -> CFG.node -> Dom.Mem.t -> Location.t
-> Dom.Mem.t
= fun pname ret callee_pname params node mem loc ->
match Procname.get_method callee_pname with
match Typ.Procname.get_method callee_pname with
| "malloc"
| "__new_array" -> model_malloc pname ret params node mem
| "realloc" -> model_realloc pname ret params node mem
@ -101,7 +101,7 @@ struct
| _ -> model_unknown_itv ret mem
let rec declare_array
: Procname.t -> CFG.node -> Loc.t -> Typ.t -> IntLit.t -> inst_num:int
: Typ.Procname.t -> CFG.node -> Loc.t -> Typ.t -> IntLit.t -> inst_num:int
-> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate
= fun pname node loc typ len ~inst_num ~dimension mem ->
let size = IntLit.to_int len |> Itv.of_int in
@ -123,7 +123,7 @@ struct
| _ -> mem
let declare_symbolic_array
: Procname.t -> Tenv.t -> CFG.node -> Loc.t -> Typ.t -> inst_num:int
: Typ.Procname.t -> Tenv.t -> CFG.node -> Loc.t -> Typ.t -> inst_num:int
-> sym_num:int -> dimension:int -> Dom.Mem.astate -> Dom.Mem.astate * int
= fun pname tenv node loc typ ~inst_num ~sym_num ~dimension mem ->
let offset = Itv.make_sym pname sym_num in
@ -187,7 +187,7 @@ struct
|> fst3
let instantiate_ret
: Tenv.t -> Procdesc.t option -> Procname.t -> (Exp.t * Typ.t) list
: Tenv.t -> Procdesc.t option -> Typ.Procname.t -> (Exp.t * Typ.t) list
-> Dom.Mem.t -> Dom.Summary.t -> Location.t -> Dom.Val.astate
= fun tenv callee_pdesc callee_pname params caller_mem summary loc ->
let callee_entry_mem = Dom.Summary.get_input summary in
@ -279,10 +279,10 @@ module Sem = BufferOverrunSemantics.Make (CFG)
module Report =
struct
type extras = Procname.t -> Procdesc.t option
type extras = Typ.Procname.t -> Procdesc.t option
let add_condition
: Procname.t -> CFG.node -> Exp.t -> Location.t -> Dom.Mem.astate
: Typ.Procname.t -> CFG.node -> Exp.t -> Location.t -> Dom.Mem.astate
-> Dom.ConditionSet.t -> Dom.ConditionSet.t
= fun pname node exp loc mem cond_set ->
let array_access =
@ -318,7 +318,7 @@ struct
| None -> cond_set
let instantiate_cond
: Tenv.t -> Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list
: Tenv.t -> Typ.Procname.t -> Procdesc.t option -> (Exp.t * Typ.t) list
-> Dom.Mem.t -> Summary.summary -> Location.t -> Dom.ConditionSet.t
= fun tenv caller_pname callee_pdesc params caller_mem summary loc ->
let callee_entry_mem = Dom.Summary.get_input summary in
@ -402,7 +402,7 @@ struct
in
match alarm with
| None -> ()
| Some bucket when Procname.equal pname caller_pname ->
| Some bucket when Typ.Procname.equal pname caller_pname ->
let description = Dom.Condition.to_string cond in
let error_desc = Localise.desc_buffer_overrun bucket description in
let exn = Exceptions.Checkers (Localise.to_string Localise.buffer_overrun, error_desc) in
@ -436,10 +436,10 @@ let compute_post
Some (entry_mem, exit_mem, cond_set)
| _ -> None
let print_summary : Procname.t -> Dom.Summary.t -> unit
let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit
= fun proc_name s ->
F.fprintf F.err_formatter "@.@[<v 2>Summary of %a :@,"
Procname.pp proc_name;
Typ.Procname.pp proc_name;
Dom.Summary.pp_summary F.err_formatter s;
F.fprintf F.err_formatter "@]@."

@ -21,13 +21,13 @@ struct
type t =
{ idx : Itv.astate;
size : Itv.astate;
proc_name : Procname.t;
proc_name : Typ.Procname.t;
loc : Location.t;
trace : trace;
id : string }
[@@deriving compare]
and trace = Intra of Procname.t
| Inter of Procname.t * Procname.t * Location.t
and trace = Intra of Typ.Procname.t
| Inter of Typ.Procname.t * Typ.Procname.t * Location.t
[@@deriving compare]
and astate = t
@ -60,7 +60,7 @@ let pp : F.formatter -> t -> unit
else
match c.trace with
Inter (_, pname, loc) ->
let pname = Procname.to_string pname in
let pname = Typ.Procname.to_string pname in
F.fprintf fmt "%a < %a at %a by call %s() at %s"
Itv.pp c.idx Itv.pp c.size pp_location c pname (string_of_location loc)
| Intra _ -> F.fprintf fmt "%a < %a at %a" Itv.pp c.idx Itv.pp c.size pp_location c
@ -71,10 +71,10 @@ let get_location : t -> Location.t
let get_trace : t -> trace
= fun c -> c.trace
let get_proc_name : t -> Procname.t
let get_proc_name : t -> Typ.Procname.t
= fun c -> c.proc_name
let make : Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
let make : Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t
= fun proc_name loc id ~idx ~size ->
{ proc_name; idx; size; loc; id ; trace = Intra proc_name }
@ -129,11 +129,11 @@ let to_string : t -> string
^ (match c.trace with
Inter (_, pname, _) ->
" by call "
^ Procname.to_string pname
^ Typ.Procname.to_string pname
^ "() "
| Intra _ -> "")
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Procname.t -> Procname.t -> Location.t -> t
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t
= fun c subst_map caller_pname callee_pname loc ->
if Itv.is_symbolic c.idx || Itv.is_symbolic c.size then
{ c with idx = Itv.subst c.idx subst_map;
@ -152,11 +152,11 @@ struct
end)
let add_bo_safety
: Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t -> t
: Typ.Procname.t -> Location.t -> string -> idx:Itv.t -> size:Itv.t -> t -> t
= fun pname loc id ~idx ~size cond ->
add (Condition.make pname loc id ~idx ~size) cond
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Procname.t -> Procname.t -> Location.t -> t
let subst : t -> Itv.Bound.t Itv.SubstMap.t -> Typ.Procname.t -> Typ.Procname.t -> Location.t -> t
= fun x subst_map caller_pname callee_pname loc ->
fold (fun e -> add (Condition.subst e subst_map caller_pname callee_pname loc)) x empty
@ -270,7 +270,7 @@ struct
let modify_itv : Itv.t -> t -> t
= fun i x -> { x with itv = i }
let make_sym : Procname.t -> int -> t
let make_sym : Typ.Procname.t -> int -> t
= fun pname i -> { bot with itv = Itv.make_sym pname i }
let unknown_bit : t -> t

@ -123,9 +123,9 @@ struct
| Binop.LOr -> Val.lor_sem v1 v2
| Binop.PtrFld -> raise Not_implemented
let get_allocsite : Procname.t -> CFG.node -> int -> int -> string
let get_allocsite : Typ.Procname.t -> CFG.node -> int -> int -> string
= fun proc_name node inst_num dimension ->
let proc_name = Procname.to_string proc_name in
let proc_name = Typ.Procname.to_string proc_name in
let node_num = CFG.hash node |> string_of_int in
let inst_num = string_of_int inst_num in
let dimension = string_of_int dimension in
@ -133,7 +133,7 @@ struct
|> Allocsite.make
let eval_array_alloc
: Procname.t -> CFG.node -> Typ.t -> Itv.t -> Itv.t -> int -> int -> Val.t
: Typ.Procname.t -> CFG.node -> Typ.t -> Itv.t -> Itv.t -> int -> int -> Val.t
= fun pdesc node typ offset size inst_num dimension ->
let allocsite = get_allocsite pdesc node inst_num dimension in
let stride = sizeof typ |> Itv.of_int in

@ -18,17 +18,17 @@ let sym_size = ref 0
module Symbol =
struct
type t = Procname.t * int [@@deriving compare]
type t = Typ.Procname.t * int [@@deriving compare]
let eq = [%compare.equal : t]
let get_new : Procname.t -> t
let get_new : Typ.Procname.t -> t
= fun pname ->
let i = !sym_size in
sym_size := !sym_size + 1;
(pname, i)
let make : Procname.t -> int -> t
let make : Typ.Procname.t -> int -> t
= fun pname i -> (pname, i)
let pp : F.formatter -> t -> unit
@ -36,7 +36,7 @@ struct
if Config.bo_debug <= 1 then
F.fprintf fmt "s$%d" (snd x)
else
F.fprintf fmt "%s-s$%d" (fst x |> Procname.to_string) (snd x)
F.fprintf fmt "%s-s$%d" (fst x |> Typ.Procname.to_string) (snd x)
end
module SubstMap = Caml.Map.Make (Symbol)
@ -76,10 +76,10 @@ struct
let le : t -> t -> bool
= fun x y -> M.for_all (fun s v -> v <= find s y) x
let get_new : Procname.t -> t
let get_new : Typ.Procname.t -> t
= fun pname -> M.add (Symbol.get_new pname) 1 empty
let make : Procname.t -> int -> t
let make : Typ.Procname.t -> int -> t
= fun pname i -> M.add (Symbol.make pname i) 1 empty
let eq : t -> t -> bool
@ -536,13 +536,13 @@ struct
let of_int : int -> t
= fun n -> (Bound.of_int n, Bound.of_int n)
let get_new_sym : Procname.t -> t
let get_new_sym : Typ.Procname.t -> t
= fun pname ->
let lower = Bound.of_sym (SymLinear.get_new pname) in
let upper = Bound.of_sym (SymLinear.get_new pname) in
(lower, upper)
let make_sym : Procname.t -> int -> t
let make_sym : Typ.Procname.t -> int -> t
= fun pname i ->
let lower = Bound.of_sym (SymLinear.make pname i) in
let upper = Bound.of_sym (SymLinear.make pname (i+1)) in
@ -936,10 +936,10 @@ let plus : t -> t -> t
let minus : t -> t -> t
= lift2 ItvPure.minus
let get_new_sym : Procname.t -> t
let get_new_sym : Typ.Procname.t -> t
= fun pname -> NonBottom (ItvPure.get_new_sym pname)
let make_sym : Procname.t -> int -> t
let make_sym : Typ.Procname.t -> int -> t
= fun pname i -> NonBottom (ItvPure.make_sym pname i)
let neg : t -> t

@ -14,7 +14,7 @@ module L = Logging
(** find transitive procedure calls for each procedure *)
module ProcnameSet = PrettyPrintable.MakePPSet(Procname)
module ProcnameSet = PrettyPrintable.MakePPSet(Typ.Procname)
module Domain = AbstractDomain.FiniteSet(ProcnameSet)
@ -33,7 +33,7 @@ module SpecSummary = Summary.Make (struct
end)
type extras_t = {
get_proc_desc : Procname.t -> Procdesc.t option;
get_proc_desc : Typ.Procname.t -> Procdesc.t option;
stacktraces : Stacktrace.t list;
}
@ -59,12 +59,12 @@ let stacktree_of_pdesc
file = SourceFile.to_string loc.Location.file;
line = Some loc.Location.line;
blame_range = [line_range_of_pdesc pdesc] } in
{ Stacktree_j.method_name = Procname.to_unique_id procname;
{ Stacktree_j.method_name = Typ.Procname.to_unique_id procname;
location = frame_loc;
callees = callees }
let stacktree_stub_of_procname procname =
{ Stacktree_j.method_name = Procname.to_unique_id procname;
{ Stacktree_j.method_name = Typ.Procname.to_unique_id procname;
location = None;
callees = [] }
@ -96,7 +96,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let dir = Filename.concat Config.results_dir "crashcontext" in
let suffix = F.sprintf "%s_%d" location_type loc.Location.line in
let fname = F.sprintf "%s.%s.json"
(Procname.to_filename caller)
(Typ.Procname.to_filename caller)
suffix in
let fpath = Filename.concat dir fname in
Utils.create_dir dir;
@ -109,18 +109,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let caller = Procdesc.get_proc_name proc_data.ProcData.pdesc in
let matches_proc frame =
let matches_class pname = match pname with
| Procname.Java java_proc ->
| Typ.Procname.Java java_proc ->
String.equal
frame.Stacktrace.class_str
(Procname.java_get_class_name java_proc)
| Procname.ObjC_Cpp objc_cpp_prod ->
(Typ.Procname.java_get_class_name java_proc)
| Typ.Procname.ObjC_Cpp objc_cpp_prod ->
String.equal
frame.Stacktrace.class_str
(Procname.objc_cpp_get_class_name objc_cpp_prod)
| Procname.C _ -> true (* Needed for test code. *)
| Procname.Block _ | Procname.Linters_dummy_method ->
(Typ.Procname.objc_cpp_get_class_name objc_cpp_prod)
| Typ.Procname.C _ -> true (* Needed for test code. *)
| Typ.Procname.Block _ | Typ.Procname.Linters_dummy_method ->
failwith "Proc type not supported by crashcontext: block" in
String.equal frame.Stacktrace.method_str (Procname.get_method caller) &&
String.equal frame.Stacktrace.method_str (Typ.Procname.get_method caller) &&
matches_class caller in
let all_frames = List.concat
(List.map ~f:(fun trace -> trace.Stacktrace.frames) traces) in

@ -25,12 +25,12 @@ module type Spec = sig
input is the previous state, current instruction, current node kind, current procedure and
type environment.
*)
val exec_instr : astate -> Sil.instr -> Procdesc.Node.nodekind -> Procname.t -> Tenv.t -> astate
val exec_instr : astate -> Sil.instr -> Procdesc.Node.nodekind -> Typ.Procname.t -> Tenv.t -> astate
(** log errors here.
input is a state, location where the state occurs in the source, and the current procedure.
*)
val report : astate -> Location.t -> Procname.t -> unit
val report : astate -> Location.t -> Typ.Procname.t -> unit
val compare : astate -> astate -> int
end

@ -15,8 +15,8 @@ sig
val initial : astate
val exec_instr :
astate ->
Sil.instr -> Procdesc.Node.nodekind -> Procname.t -> Tenv.t -> astate
val report : astate -> Location.t -> Procname.t -> unit
Sil.instr -> Procdesc.Node.nodekind -> Typ.Procname.t -> Tenv.t -> astate
val report : astate -> Location.t -> Typ.Procname.t -> unit
val compare : astate -> astate -> int
end

@ -16,7 +16,7 @@ module type Kind = sig
include TraceElem.Kind
(** return the parameter index and sink kind for the given call site with the given actuals *)
val get : Procname.t -> (Exp.t * Typ.t) list -> Tenv.t -> (t * int * bool) list
val get : Typ.Procname.t -> (Exp.t * Typ.t) list -> Tenv.t -> (t * int * bool) list
end
module type S = sig

@ -13,7 +13,7 @@ module type Kind = sig
include TraceElem.Kind
(** return the parameter index and sink kind for the given call site with the given actuals *)
val get : Procname.t -> (Exp.t * Typ.t) list -> Tenv.t -> (t * int * bool) list
val get : Typ.Procname.t -> (Exp.t * Typ.t) list -> Tenv.t -> (t * int * bool) list
end
module type S = sig

@ -20,7 +20,7 @@ module type S = sig
type sink_path = Passthroughs.t * (Sink.t * Passthroughs.t) list
(** get a path for each of the reportable flows to a sink in this trace *)
val get_reportable_sink_paths : t -> trace_of_pname:(Procname.t -> t) -> sink_path list
val get_reportable_sink_paths : t -> trace_of_pname:(Typ.Procname.t -> t) -> sink_path list
(** update sink with the given call site *)
val with_callsite : t -> CallSite.t -> t

@ -18,7 +18,7 @@ module type S = sig
type sink_path = Passthrough.Set.t * (Sink.t * Passthrough.Set.t) list
(** get a path for each of the reportable flows to a sink in this trace *)
val get_reportable_sink_paths : t -> trace_of_pname:(Procname.t -> t) -> sink_path list
val get_reportable_sink_paths : t -> trace_of_pname:(Typ.Procname.t -> t) -> sink_path list
(** update sink with the given call site *)
val with_callsite : t -> CallSite.t -> t

@ -16,8 +16,8 @@ module GlobalsAccesses = SiofTrace.GlobalsAccesses
let methods_whitelist = QualifiedCppName.quals_matcher_of_fuzzy_qual_names Config.siof_safe_methods
let is_whitelisted (pname : Procname.t) =
Procname.get_qualifiers pname
let is_whitelisted (pname : Typ.Procname.t) =
Typ.Procname.get_qualifiers pname
|> QualifiedCppName.match_qualifiers methods_whitelist
type siof_model = {
@ -42,7 +42,7 @@ let is_modelled =
List.map models ~f:(fun {qual_name} -> qual_name)
|> QualifiedCppName.quals_matcher_of_fuzzy_qual_names in
fun pname ->
Procname.get_qualifiers pname
Typ.Procname.get_qualifiers pname
|> QualifiedCppName.match_qualifiers models_matcher
module Summary = Summary.Make (struct
@ -129,15 +129,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
~f:(fun {qual_name; initialized_globals} ->
if QualifiedCppName.quals_matcher_of_fuzzy_qual_names [qual_name]
|> Fn.flip QualifiedCppName.match_qualifiers
(Procname.get_qualifiers callee_pname) then
(Typ.Procname.get_qualifiers callee_pname) then
Some initialized_globals
else
None) in
Domain.join astate (Domain.BottomSiofTrace.NonBottom SiofTrace.empty,
Domain.VarNames.of_list init)
| Call (_, Const (Cfun callee_pname), _::params_without_self, loc, _)
when Procname.is_c_method callee_pname && Procname.is_constructor callee_pname
&& Procname.is_constexpr callee_pname ->
when Typ.Procname.is_c_method callee_pname && Typ.Procname.is_constructor callee_pname
&& Typ.Procname.is_constexpr callee_pname ->
add_params_globals astate pdesc loc params_without_self
| Call (_, Const (Cfun callee_pname), params, loc, _) ->
let callsite = CallSite.make callee_pname loc in
@ -250,7 +250,7 @@ let checker ({ Callbacks.proc_desc; } as callback) =
~make_extras:ProcData.make_empty_extras
callback in
let pname = Procdesc.get_proc_name proc_desc in
match Procname.get_global_name_of_initializer pname with
match Typ.Procname.get_global_name_of_initializer pname with
| Some gname ->
siof_check proc_desc gname post
| None ->

@ -62,7 +62,7 @@ end
include SinkTrace.Make(TraceElem)
let make_access kind loc =
let site = CallSite.make Procname.empty_block loc in
let site = CallSite.make Typ.Procname.empty_block loc in
{ TraceElem.kind = (`Access, kind); site; }
let is_intraprocedural_access { TraceElem.kind=(kind, _); } = kind = `Access
@ -73,7 +73,7 @@ let trace_of_error loc gname path =
if is_intraprocedural_access sink then
Format.asprintf "%a" Sink.pp sink
else
Format.asprintf "call to %a" Procname.pp (CallSite.pname callsite) in
Format.asprintf "call to %a" Typ.Procname.pp (CallSite.pname callsite) in
let sink_should_nest sink = not (is_intraprocedural_access sink) in
let trace_elem_of_global =
Errlog.make_trace_element 0 loc

@ -21,7 +21,7 @@ module type Kind = sig
val unknown : t
val get : Procname.t -> Tenv.t -> t option
val get : Typ.Procname.t -> Tenv.t -> t option
val get_tainted_formals : Procdesc.t -> Tenv.t -> (Mangled.t * Typ.t * t option) list
end

@ -19,7 +19,7 @@ module type Kind = sig
val unknown : t
(** return Some (kind) if the procedure is a taint source, None otherwise *)
val get : Procname.t -> Tenv.t -> t option
val get : Typ.Procname.t -> Tenv.t -> t option
(** return each formal of the function paired with either Some(kind) if the formal is a taint
source, or None if the formal is not a taint source *)

@ -52,9 +52,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| NoEffect
let get_lock_model = function
| Procname.Java java_pname ->
| Typ.Procname.Java java_pname ->
begin
match Procname.java_get_class_name java_pname, Procname.java_get_method java_pname with
match Typ.Procname.java_get_class_name java_pname, Typ.Procname.java_get_method java_pname with
| "java.util.concurrent.locks.Lock", "lock" ->
Lock
| ("java.util.concurrent.locks.ReentrantLock"
@ -71,9 +71,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| _ ->
NoEffect
end
| pname when Procname.equal pname BuiltinDecl.__set_locked_attribute ->
| pname when Typ.Procname.equal pname BuiltinDecl.__set_locked_attribute ->
Lock
| pname when Procname.equal pname BuiltinDecl.__delete_locked_attribute ->
| pname when Typ.Procname.equal pname BuiltinDecl.__delete_locked_attribute ->
Unlock
| _ ->
NoEffect
@ -211,10 +211,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let is_annotated_functional =
has_return_annot Annotations.ia_is_functional in
let is_modeled_functional = function
| Procname.Java java_pname ->
| Typ.Procname.Java java_pname ->
begin
match Procname.java_get_class_name java_pname,
Procname.java_get_method java_pname with
match Typ.Procname.java_get_class_name java_pname,
Typ.Procname.java_get_method java_pname with
| "android.content.res.Resources", method_name ->
(* all methods of Resources are considered @Functional except for the ones in this
blacklist *)
@ -236,13 +236,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let acquires_ownership pname tenv =
let is_allocation pn =
Procname.equal pn BuiltinDecl.__new || Procname.equal pn BuiltinDecl.__new_array in
Typ.Procname.equal pn BuiltinDecl.__new || Typ.Procname.equal pn BuiltinDecl.__new_array in
(* identify library functions that maintain ownership invariants behind the scenes *)
let is_owned_in_library = function
| Procname.Java java_pname ->
| Typ.Procname.Java java_pname ->
begin
match Procname.java_get_class_name java_pname,
Procname.java_get_method java_pname with
match Typ.Procname.java_get_class_name java_pname,
Typ.Procname.java_get_method java_pname with
| "javax.inject.Provider", "get" ->
(* in dependency injection, the library allocates fresh values behind the scenes *)
true
@ -263,10 +263,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let exec_instr (astate : Domain.astate) { ProcData.pdesc; tenv; extras; } _ =
let is_container_write pn tenv = match pn with
| Procname.Java java_pname ->
let typename = Typename.Java.from_string (Procname.java_get_class_name java_pname) in
| Typ.Procname.Java java_pname ->
let typename = Typename.Java.from_string (Typ.Procname.java_get_class_name java_pname) in
let is_container_write_ typename _ =
match Typename.name typename, Procname.java_get_method java_pname with
match Typename.name typename, Typ.Procname.java_get_method java_pname with
| "java.util.List", ("add" | "addAll" | "clear" | "remove" | "set") -> true
| "java.util.Map", ("clear" | "put" | "putAll" | "remove") -> true
| _ -> false in
@ -286,7 +286,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let dummy_fieldname =
Ident.create_fieldname
(Mangled.from_string
(container_write_string ^ (Procname.get_method callee_pname))) 0 in
(container_write_string ^ (Typ.Procname.get_method callee_pname))) 0 in
let dummy_access_exp = Exp.Lfield (receiver_exp, dummy_fieldname, receiver_typ) in
let callee_writes =
match AccessPath.of_lhs_exp dummy_access_exp receiver_typ ~f_resolve_id with
@ -301,7 +301,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| _ ->
failwithf
"Call to %a is marked as a container write, but has no receiver"
Procname.pp callee_pname in
Typ.Procname.pp callee_pname in
let get_summary caller_pdesc callee_pname actuals ~f_resolve_id callee_loc tenv =
if is_container_write callee_pname tenv
then
@ -312,9 +312,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
not is_locked && not (Procdesc.is_java_synchronized pdesc) in
(* return true if the given procname boxes a primitive type into a reference type *)
let is_box = function
| Procname.Java java_pname ->
| Typ.Procname.Java java_pname ->
begin
match Procname.java_get_class_name java_pname, Procname.java_get_method java_pname with
match Typ.Procname.java_get_class_name java_pname, Typ.Procname.java_get_method java_pname with
| ("java.lang.Boolean" |
"java.lang.Byte" |
"java.lang.Char" |
@ -348,7 +348,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Sil.Call (Some (ret_id, _), Const (Cfun callee_pname),
(target_exp, target_typ) :: (Exp.Sizeof (cast_typ, _, _), _) :: _ , _, _)
when Procname.equal callee_pname BuiltinDecl.__cast ->
when Typ.Procname.equal callee_pname BuiltinDecl.__cast ->
let lhs_access_path = AccessPath.of_id ret_id (Typ.Tptr (cast_typ, Pk_pointer)) in
let attribute_map =
propagate_attributes
@ -618,11 +618,11 @@ module Analyzer = AbstractInterpreter.Make (ProcCfg.Normal) (TransferFunctions)
module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
(* a results table is a Map where a key is an a procedure environment,
i.e., something of type Idenv.t * Tenv.t * Procname.t * Procdesc.t
i.e., something of type Idenv.t * Tenv.t * Typ.Procname.t * Procdesc.t
*)
module ResultsTableType = Caml.Map.Make (struct
type t = Idenv.t * Tenv.t * Procname.t * Procdesc.t
let compare (_, _, pn1, _) (_,_,pn2,_) = Procname.compare pn1 pn2
type t = Idenv.t * Tenv.t * Typ.Procname.t * Procdesc.t
let compare (_, _, pn1, _) (_,_,pn2,_) = Typ.Procname.compare pn1 pn2
end)
(* we want to consider Builder classes and other safe immutablility-ensuring patterns as
@ -646,12 +646,12 @@ let is_immutable_collection_class class_name tenv =
class_name
let is_call_to_builder_class_method = function
| Procname.Java java_pname -> is_builder_class (Procname.java_get_class_name java_pname)
| Typ.Procname.Java java_pname -> is_builder_class (Typ.Procname.java_get_class_name java_pname)
| _ -> false
let is_call_to_immutable_collection_method tenv = function
| Procname.Java java_pname ->
is_immutable_collection_class (Procname.java_get_class_type_name java_pname) tenv
| Typ.Procname.Java java_pname ->
is_immutable_collection_class (Typ.Procname.java_get_class_type_name java_pname) tenv
| _ ->
false
@ -717,7 +717,7 @@ let pdesc_is_assumed_thread_safe pdesc tenv =
find more bugs. this is just a temporary measure to avoid obvious false positives *)
let should_analyze_proc pdesc tenv =
let pn = Procdesc.get_proc_name pdesc in
not (Procname.is_class_initializer pn) &&
not (Typ.Procname.is_class_initializer pn) &&
not (FbThreadSafety.is_logging_method pn) &&
not (is_call_to_builder_class_method pn) &&
not (is_call_to_immutable_collection_method tenv pn) &&
@ -727,13 +727,13 @@ let should_analyze_proc pdesc tenv =
(* return true if we should report on unprotected accesses during the procedure *)
let should_report_on_proc (_, _, proc_name, proc_desc) =
not (Procname.java_is_autogen_method proc_name) &&
not (Typ.Procname.java_is_autogen_method proc_name) &&
Procdesc.get_access proc_desc <> PredSymb.Private &&
not (Annotations.pdesc_return_annot_ends_with proc_desc Annotations.visibleForTesting)
let analyze_procedure callback =
let is_initializer tenv proc_name =
Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name in
Typ.Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name in
let open ThreadSafetyDomain in
let has_lock = false in
let return_attrs = AttributeSetDomain.empty in
@ -807,8 +807,8 @@ let make_results_table get_proc_desc file_env =
let get_current_class_and_threadsafe_superclasses tenv pname =
match pname with
| Procname.Java java_pname ->
let current_class = Procname.java_get_class_type_name java_pname in
| Typ.Procname.Java java_pname ->
let current_class = Typ.Procname.java_get_class_type_name java_pname in
let thread_safe_annotated_classes =
PatternMatch.find_superclasses_with_attributes
is_thread_safe tenv current_class
@ -950,7 +950,7 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) make_description tr
Format.asprintf "access to %a" (pp_accesses_sink ~is_write_access:true) sink
else
Format.asprintf
"call to %a" Procname.pp (CallSite.pname (PathDomain.Sink.call_site sink)) in
"call to %a" Typ.Procname.pp (CallSite.pname (PathDomain.Sink.call_site sink)) in
let loc = CallSite.loc (PathDomain.Sink.call_site initial_sink) in
let ltr = PathDomain.to_sink_loc_trace ~desc_of_sink path in
let msg = Localise.to_string Localise.thread_safety_violation in
@ -968,7 +968,7 @@ let make_unprotected_write_description
tenv pname final_sink_site initial_sink_site final_sink _ =
Format.asprintf
"Unprotected write. Public method %a%s %s %a outside of synchronization.%s"
Procname.pp pname
Typ.Procname.pp pname
(if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly")
(if is_container_write_sink final_sink then "mutates" else "writes to field")
(pp_accesses_sink ~is_write_access:true) final_sink
@ -983,13 +983,13 @@ let make_read_write_race_description tenv pname final_sink_site initial_sink_sit
conflicting_proc_envs in
let pp_proc_name_list fmt proc_names =
let pp_sep _ _ = F.fprintf fmt " , " in
F.pp_print_list ~pp_sep Procname.pp fmt proc_names in
F.pp_print_list ~pp_sep Typ.Procname.pp fmt proc_names in
let conflicts_description =
Format.asprintf "Potentially races with writes in method%s %a."
(if List.length conflicting_proc_names > 1 then "s" else "")
pp_proc_name_list conflicting_proc_names in
Format.asprintf "Read/Write race. Public method %a%s reads from field %a. %s %s"
Procname.pp pname
Typ.Procname.pp pname
(if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly")
(pp_accesses_sink ~is_write_access:false) final_sink
conflicts_description

@ -40,7 +40,7 @@ module TraceElem = struct
end
let make_access kind loc =
let site = CallSite.make Procname.empty_block loc in
let site = CallSite.make Typ.Procname.empty_block loc in
TraceElem.make kind site
module LocksDomain = AbstractDomain.BooleanAnd

@ -53,7 +53,7 @@ module type S = sig
(** get a path for each of the reportable source -> sink flows in this trace. specifying
[cur_site] restricts the reported paths to ones introduced by the call at [cur_site] *)
val get_reportable_paths :
?cur_site:CallSite.t -> t -> trace_of_pname:(Procname.t -> t) -> path list
?cur_site:CallSite.t -> t -> trace_of_pname:(Typ.Procname.t -> t) -> path list
(** create a loc_trace from a path; [source_should_nest s] should be true when we are going one
deeper into a call-chain, ie when lt_level should be bumper in the next loc_trace_elem, and
@ -87,7 +87,7 @@ module type S = sig
val pp : F.formatter -> t -> unit
(** pretty-print a path in the context of the given procname *)
val pp_path : Procname.t -> F.formatter -> path -> unit
val pp_path : Typ.Procname.t -> F.formatter -> path -> unit
end
(** Expand a trace element (i.e., a source or sink) into a list of trace elements bottoming out in
@ -216,7 +216,7 @@ module Make (Spec : Spec) = struct
Source.pp original_source
Sink.pp final_sink
pp_sources sources_passthroughs
Procname.pp cur_pname
Typ.Procname.pp cur_pname
pp_passthroughs cur_passthroughs
pp_sinks (List.rev sinks_passthroughs)
@ -269,18 +269,18 @@ module Make (Spec : Spec) = struct
let to_loc_trace
?(desc_of_source=fun source ->
let callsite = Source.call_site source in
Format.asprintf "return from %a" Procname.pp (CallSite.pname callsite))
Format.asprintf "return from %a" Typ.Procname.pp (CallSite.pname callsite))
?(source_should_nest=(fun _ -> true))
?(desc_of_sink=fun sink ->
let callsite = Sink.call_site sink in
Format.asprintf "call to %a" Procname.pp (CallSite.pname callsite))
Format.asprintf "call to %a" Typ.Procname.pp (CallSite.pname callsite))
?(sink_should_nest=(fun _ -> true))
(passthroughs, sources, sinks) =
let trace_elems_of_passthroughs lt_level passthroughs acc0 =
let trace_elem_of_passthrough passthrough acc =
let passthrough_site = Passthrough.site passthrough in
let desc = F.asprintf "flow through %a" Procname.pp (CallSite.pname passthrough_site) in
let desc = F.asprintf "flow through %a" Typ.Procname.pp (CallSite.pname passthrough_site) in
(Errlog.make_trace_element lt_level (CallSite.loc passthrough_site) desc []) :: acc in
(* sort passthroughs by ascending line number to create a coherent trace *)
let sorted_passthroughs =

@ -54,7 +54,7 @@ module type S = sig
(** get a path for each of the reportable source -> sink flows in this trace. specifying
[cur_site] restricts the reported paths to ones introduced by the call at [cur_site] *)
val get_reportable_paths :
?cur_site:CallSite.t -> t -> trace_of_pname:(Procname.t -> t) -> path list
?cur_site:CallSite.t -> t -> trace_of_pname:(Typ.Procname.t -> t) -> path list
(** create a loc_trace from a path; [source_should_nest s] should be true when we are going one
deeper into a call-chain, ie when lt_level should be bumper in the next loc_trace_elem, and
@ -89,7 +89,7 @@ module type S = sig
val pp : F.formatter -> t -> unit
(** pretty-print a path in the context of the given procname *)
val pp_path : Procname.t -> F.formatter -> path -> unit
val pp_path : Typ.Procname.t -> F.formatter -> path -> unit
end
module Make (Spec : Spec) : S with module Source = Spec.Source and module Sink = Spec.Sink

@ -113,10 +113,10 @@ let expensive_overrides_unexpensive =
let annotation_reachability_error = "CHECKERS_ANNOTATION_REACHABILITY_ERROR"
let is_modeled_expensive tenv = function
| Procname.Java proc_name_java as proc_name ->
| Typ.Procname.Java proc_name_java as proc_name ->
not (BuiltinDecl.is_declared proc_name) &&
let is_subclass =
let classname = Typename.Java.from_string (Procname.java_get_class_name proc_name_java) in
let classname = Typename.Java.from_string (Typ.Procname.java_get_class_name proc_name_java) in
PatternMatch.is_subtype_of_str tenv classname in
Inferconfig.modeled_expensive_matcher is_subclass proc_name
| _ ->
@ -124,12 +124,12 @@ let is_modeled_expensive tenv = function
let is_allocator tenv pname =
match pname with
| Procname.Java pname_java ->
| Typ.Procname.Java pname_java ->
let is_throwable () =
let class_name =
Typename.Java.from_string (Procname.java_get_class_name pname_java) in
Typename.Java.from_string (Typ.Procname.java_get_class_name pname_java) in
PatternMatch.is_throwable tenv class_name in
Procname.is_constructor pname
Typ.Procname.is_constructor pname
&& not (BuiltinDecl.is_declared pname)
&& not (is_throwable ())
| _ ->
@ -171,7 +171,7 @@ let update_trace loc trace =
Errlog.make_trace_element 0 loc "" [] :: trace
let string_of_pname =
Procname.to_simplified_string ~withclass:true
Typ.Procname.to_simplified_string ~withclass:true
let report_allocation_stack
src_annot pname fst_call_loc trace stack_str constructor_pname call_loc =
@ -180,7 +180,7 @@ let report_allocation_stack
let description =
Printf.sprintf
"Method `%s` annotated with `@%s` allocates `%s` via `%s%s`"
(Procname.to_simplified_string pname)
(Typ.Procname.to_simplified_string pname)
src_annot
constr_str
stack_str
@ -198,7 +198,7 @@ let report_annotation_stack src_annot snk_annot src_pname loc trace stack_str sn
let description =
Printf.sprintf
"Method `%s` annotated with `@%s` calls `%s%s` where `%s` is annotated with `@%s`"
(Procname.to_simplified_string src_pname)
(Typ.Procname.to_simplified_string src_pname)
src_annot
stack_str
exp_pname_str
@ -232,8 +232,8 @@ let report_call_stack end_of_stack lookup_next_calls report call_site calls =
~f:(fun (accu, set) call_site ->
let p = CallSite.pname call_site in
let loc = CallSite.loc call_site in
if Procname.Set.mem p set then (accu, set)
else ((p, loc) :: accu, Procname.Set.add p set))
if Typ.Procname.Set.mem p set then (accu, set)
else ((p, loc) :: accu, Typ.Procname.Set.add p set))
~init:([], visited_pnames)
next_calls in
List.iter ~f:(loop fst_call_loc updated_visited (new_trace, new_stack_str)) unseen_pnames in
@ -242,7 +242,7 @@ let report_call_stack end_of_stack lookup_next_calls report call_site calls =
let fst_callee_pname = CallSite.pname fst_call_site in
let fst_call_loc = CallSite.loc fst_call_site in
let start_trace = update_trace (CallSite.loc call_site) [] in
loop fst_call_loc Procname.Set.empty (start_trace, "") (fst_callee_pname, fst_call_loc))
loop fst_call_loc Typ.Procname.Set.empty (start_trace, "") (fst_callee_pname, fst_call_loc))
calls
module TransferFunctions (CFG : ProcCfg.S) = struct
@ -255,8 +255,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
rarely to not affect the performances *)
let is_unlikely pname =
match pname with
| Procname.Java java_pname ->
String.equal (Procname.java_get_method java_pname) "unlikely"
| Typ.Procname.Java java_pname ->
String.equal (Typ.Procname.java_get_method java_pname) "unlikely"
| _ -> false
let is_tracking_exp astate = function
@ -356,8 +356,8 @@ module Interprocedural = struct
let description =
Printf.sprintf
"Method `%s` overrides unannotated method `%s` and cannot be annotated with `@%s`"
(Procname.to_string proc_name)
(Procname.to_string overridden_pname)
(Typ.Procname.to_string proc_name)
(Typ.Procname.to_string overridden_pname)
Annotations.expensive in
let exn =
Exceptions.Checkers

@ -95,8 +95,8 @@ val pdesc_has_return_annot : Procdesc.t -> (Annot.Item.t -> bool) -> bool
value. the function [attrs_of_pname] should resolve the proc attributes of [pname].
Specs.proc_resolve_attributes is a good choice for this resolution function. *)
val pname_has_return_annot :
Procname.t ->
attrs_of_pname:(Procname.t -> ProcAttributes.t option) ->
Typ.Procname.t ->
attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option) ->
(Annot.Item.t -> bool) ->
bool

@ -103,7 +103,7 @@ let callback_check_dead_code { Callbacks.proc_desc; proc_name; tenv } =
let do_check () =
begin
if verbose then L.stderr "@.--@.PROC: %a@." Procname.pp proc_name;
if verbose then L.stderr "@.--@.PROC: %a@." Typ.Procname.pp proc_name;
let transitions = DFDead.run tenv proc_desc State.initial in
let exit_node = Procdesc.get_exit_node proc_desc in
match transitions exit_node with

Some files were not shown because too many files have changed in this diff Show More

Loading…
Cancel
Save