[backend][cleanup] Move proc_attributes to a separate module.

Summary:
Move proc_attributes to a separate module.
Field err_log, in common between proc desc and summary, can now be moved to ProcAttributes without creating cycles of dependencies.
master
Cristiano Calcagno 10 years ago
parent a9b6f33940
commit ea7c13ff6c

@ -64,8 +64,8 @@ let proc_inline_synthetic_methods cfg proc_desc : unit =
| Some pd ->
let is_access = Procname.java_is_access_method pn in
let attributes = Cfg.Procdesc.get_attributes pd in
let is_synthetic = attributes.Sil.is_synthetic_method in
let is_bridge = attributes.Sil.is_bridge_method in
let is_synthetic = attributes.ProcAttributes.is_synthetic_method in
let is_bridge = attributes.ProcAttributes.is_bridge_method in
if is_access || is_bridge || is_synthetic
then inline_synthetic_method ret_ids etl pd pn loc
else None
@ -121,7 +121,7 @@ let get_procedure_definition exe_env proc_name =
(fun proc_desc ->
proc_inline_synthetic_methods cfg proc_desc;
let idenv = Idenv.create cfg proc_desc
and language = (Cfg.Procdesc.get_attributes proc_desc).Sil.language in
and language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in
(idenv, tenv, proc_name, proc_desc, language))
(Cfg.Procdesc.find_from_name cfg proc_name)
@ -224,7 +224,7 @@ let iterate_callbacks store_summary call_graph exe_env =
let loc = match procdesc_opt with
| Some proc_desc ->
Cfg.Procdesc.get_loc proc_desc
| None -> Location.loc_none in
| None -> Location.dummy in
Specs.reset_summary call_graph proc_name loc in

@ -40,12 +40,11 @@ module Node = struct
mutable nd_succs : t list; (** successor nodes in the cfg *)
}
and proc_desc = { (** procedure description *)
pd_attributes : Sil.proc_attributes; (** attributes of the procedure *)
pd_attributes : ProcAttributes.t; (** attributes of the procedure *)
pd_id : int; (** unique proc_desc identifier *)
mutable pd_nodes : t list; (** list of nodes of this procedure *)
mutable pd_start_node : t; (** start node of this procedure *)
mutable pd_exit_node : t; (** exit node of ths procedure *)
pd_err_log: Errlog.t; (** error log at translation time *)
mutable pd_changed : bool; (** true if proc has changed since last analysis *)
}
@ -104,9 +103,10 @@ module Node = struct
try
list_for_all2 node_eq n1s n2s
with Invalid_argument _ -> false in
pd1.pd_attributes.Sil.is_defined = pd2.pd_attributes.Sil.is_defined &&
Sil.typ_equal pd1.pd_attributes.Sil.ret_type pd2.pd_attributes.Sil.ret_type &&
formals_eq pd1.pd_attributes.Sil.formals pd2.pd_attributes.Sil.formals &&
let att1 = pd1.pd_attributes and att2 = pd2.pd_attributes in
att1.ProcAttributes.is_defined = att2.ProcAttributes.is_defined &&
Sil.typ_equal att1.ProcAttributes.ret_type att2.ProcAttributes.ret_type &&
formals_eq att1.ProcAttributes.formals att2.ProcAttributes.formals &&
nodes_eq pd1.pd_nodes pd2.pd_nodes in
let old_procs = cfg_old.name_pdesc_tbl in
let new_procs = cfg_new.name_pdesc_tbl in
@ -131,12 +131,12 @@ module Node = struct
let node_list' =
let filter_node node = match node.nd_proc with
| None -> true
| Some pdesc -> is_enabled pdesc.pd_attributes.Sil.proc_name in
| Some pdesc -> is_enabled pdesc.pd_attributes.ProcAttributes.proc_name in
list_filter filter_node !(cfg.node_list) in
let procs_to_remove =
let psetr = ref Procname.Set.empty in
let do_proc pname pdesc =
if pdesc.pd_attributes.Sil.is_defined &&
if pdesc.pd_attributes.ProcAttributes.is_defined &&
not (is_enabled pname) &&
not (in_address_set pname) then
psetr := Procname.Set.add pname !psetr in
@ -179,7 +179,7 @@ module Node = struct
nd_dead_pvars_before = [];
nd_instrs = [];
nd_kind = Skip_node "dummy";
nd_loc = Location.loc_none;
nd_loc = Location.dummy;
nd_proc = None;
nd_succs = []; nd_preds = []; nd_exn = [];
}
@ -384,15 +384,15 @@ module Node = struct
node.nd_instrs <- instrs
let proc_desc_get_ret_var pdesc =
Sil.get_ret_pvar pdesc.pd_attributes.Sil.proc_name
Sil.get_ret_pvar pdesc.pd_attributes.ProcAttributes.proc_name
(** Add declarations for local variables and return variable to the node *)
let add_locals_ret_declaration node locals =
let loc = get_loc node in
let pdesc = get_proc_desc node in
let proc_name = pdesc.pd_attributes.Sil.proc_name in
let proc_name = pdesc.pd_attributes.ProcAttributes.proc_name in
let ret_var =
let ret_type = pdesc.pd_attributes.Sil.ret_type in
let ret_type = pdesc.pd_attributes.ProcAttributes.ret_type in
(proc_desc_get_ret_var pdesc, ret_type) in
let construct_decl (x, typ) =
(Sil.mk_pvar x proc_name, typ) in
@ -429,7 +429,7 @@ module Node = struct
proc_desc.pd_start_node
let proc_desc_get_err_log proc_desc =
proc_desc.pd_err_log
proc_desc.pd_attributes.ProcAttributes.err_log
let proc_desc_get_attributes proc_desc =
proc_desc.pd_attributes
@ -462,33 +462,33 @@ module Node = struct
(** Set a flag for the proc desc *)
let proc_desc_set_flag pdesc key value =
proc_flags_add pdesc.pd_attributes.Sil.proc_flags key value
proc_flags_add pdesc.pd_attributes.ProcAttributes.proc_flags key value
(** Return the return type of the procedure *)
let proc_desc_get_ret_type proc_desc =
proc_desc.pd_attributes.Sil.ret_type
proc_desc.pd_attributes.ProcAttributes.ret_type
let proc_desc_get_proc_name proc_desc =
proc_desc.pd_attributes.Sil.proc_name
proc_desc.pd_attributes.ProcAttributes.proc_name
(** Return [true] iff the procedure is defined, and not just declared *)
let proc_desc_is_defined proc_desc =
proc_desc.pd_attributes.Sil.is_defined
proc_desc.pd_attributes.ProcAttributes.is_defined
let proc_desc_get_loc proc_desc =
proc_desc.pd_attributes.Sil.loc
proc_desc.pd_attributes.ProcAttributes.loc
(** Return name and type of formal parameters *)
let proc_desc_get_formals proc_desc =
proc_desc.pd_attributes.Sil.formals
proc_desc.pd_attributes.ProcAttributes.formals
(** Return name and type of local variables *)
let proc_desc_get_locals proc_desc =
proc_desc.pd_attributes.Sil.locals
proc_desc.pd_attributes.ProcAttributes.locals
(** Return name and type of captured variables *)
let proc_desc_get_captured proc_desc =
proc_desc.pd_attributes.Sil.captured
proc_desc.pd_attributes.ProcAttributes.captured
let proc_desc_get_nodes proc_desc =
proc_desc.pd_nodes
@ -503,11 +503,12 @@ module Node = struct
(** Get flags for the proc desc *)
let proc_desc_get_flags proc_desc =
proc_desc.pd_attributes.Sil.proc_flags
proc_desc.pd_attributes.ProcAttributes.proc_flags
(** Append the locals to the list of local variables *)
let proc_desc_append_locals proc_desc new_locals =
proc_desc.pd_attributes.Sil.locals <- proc_desc.pd_attributes.Sil.locals @ new_locals
proc_desc.pd_attributes.ProcAttributes.locals <-
proc_desc.pd_attributes.ProcAttributes.locals @ new_locals
(** Get the cyclomatic complexity for the procedure *)
let proc_desc_get_cyclomatic proc_desc =
@ -681,7 +682,7 @@ module Procdesc = struct
type proc_desc_builder =
{ cfg : cfg;
proc_attributes : Sil.proc_attributes;
proc_attributes : ProcAttributes.t;
}
let create (b : proc_desc_builder) =
@ -694,10 +695,9 @@ module Procdesc = struct
pd_nodes = [];
pd_start_node = dummy ();
pd_exit_node = dummy ();
pd_err_log = Errlog.empty ();
pd_changed = true
} in
pdesc_tbl_add b.cfg b.proc_attributes.Sil.proc_name pdesc;
pdesc_tbl_add b.cfg b.proc_attributes.ProcAttributes.proc_name pdesc;
pdesc
let remove = Node.proc_desc_remove
@ -762,7 +762,7 @@ let get_defined_procs cfg =
let get_objc_generated_procs cfg =
list_filter (
fun procdesc ->
(Procdesc.get_attributes procdesc).Sil.is_generated) (get_all_procs cfg)
(Procdesc.get_attributes procdesc).ProcAttributes.is_generated) (get_all_procs cfg)
(** get the function names which should be analyzed before the other ones *)
let get_priority_procnames cfg =

@ -33,7 +33,7 @@ module Procdesc : sig
type proc_desc_builder =
{ cfg : cfg;
proc_attributes : Sil.proc_attributes;
proc_attributes : ProcAttributes.t;
}
(** Create a procdesc *)
@ -47,7 +47,7 @@ module Procdesc : sig
val find_from_name : cfg -> Procname.t -> t option
(** Get the attributes of the procedure. *)
val get_attributes : t -> Sil.proc_attributes
val get_attributes : t -> ProcAttributes.t
(** Get the cyclomatic complexity for the procedure *)
val get_cyclomatic : t -> int

@ -903,7 +903,10 @@ let pp_cfgnodelabel fmt (n : Cfg.Node.t) =
let pp_label fmt n =
match Cfg.Node.get_kind n with
| Cfg.Node.Start_node (pdesc) ->
let gen = if (Cfg.Procdesc.get_attributes pdesc).Sil.is_generated then " (generated)" else "" in
let gen =
if (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.is_generated
then " (generated)"
else "" in
(* let def = if Cfg.Procdesc.is_defined pdesc then "defined" else "declared" in *)
(* Format.fprintf fmt "Start %a (%s)" pp_id (Procname.to_string (Cfg.Procdesc.get_proc_name pdesc)) def *)
Format.fprintf fmt "Start %s%s\\nFormals: %a\\nLocals: %a"

@ -437,7 +437,7 @@ let post_process_procs exe_env procs_done =
let check_no_specs pn =
if Specs.get_specs pn = [] then begin
Errdesc.warning_err
(Specs.get_summary_unsafe pn).Specs.attributes.Sil.loc
(Specs.get_summary_unsafe pn).Specs.attributes.ProcAttributes.loc
"No specs found for %a@." Procname.pp pn
end in
let cg = Exe_env.get_cg exe_env in
@ -583,7 +583,7 @@ let parallel_execution exe_env num_processes analyze_proc filter_out process_res
|| not (proc_is_up_to_date call_graph pname)) in
let process_one_proc pname (calls: Cg.in_out_calls) =
DB.current_source :=
(Specs.get_summary_unsafe pname).Specs.attributes.Sil.loc.Location.file;
(Specs.get_summary_unsafe pname).Specs.attributes.ProcAttributes.loc.Location.file;
if !trace then
begin
let whole_seconds = false in
@ -637,7 +637,7 @@ let parallel_execution exe_env num_processes analyze_proc filter_out process_res
let (pname, weight) = Process.get_last_input p_str in
(try
DB.current_source :=
(Specs.get_summary_unsafe pname).Specs.attributes.Sil.loc.Location.file;
(Specs.get_summary_unsafe pname).Specs.attributes.ProcAttributes.loc.Location.file;
process_result exe_env (pname, weight) summ
with exn -> assert false);
Timing_log.event_finish (Procname.to_string pname);

@ -207,7 +207,7 @@ let () = (* parse command-line arguments *)
module Simulator = struct (** Simulate the analysis only *)
let reset_summaries cg =
list_iter
(fun (pname, in_out_calls) -> Specs.reset_summary cg pname Location.loc_none)
(fun (pname, in_out_calls) -> Specs.reset_summary cg pname Location.dummy)
(Cg.get_nodes_and_calls cg)
(** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for

@ -245,6 +245,8 @@ type summary_val =
(** compute values from summary data to export to csv and xml format *)
let summary_values top_proc_set summary =
let stats = summary.Specs.stats in
let attributes = summary.Specs.attributes in
let err_log = attributes.ProcAttributes.err_log in
let proc_name = Specs.get_proc_name summary in
let is_top = Procname.Set.mem proc_name top_proc_set in
let signature = Specs.get_signature summary in
@ -283,11 +285,11 @@ let summary_values top_proc_set summary =
vsymop = stats.Specs.symops;
verr = Errlog.size
(fun ekind in_footprint -> ekind = Exceptions.Kerror && in_footprint)
stats.Specs.err_log;
vflags = summary.Specs.attributes.Sil.proc_flags;
vfile = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file;
vline = summary.Specs.attributes.Sil.loc.Location.line;
vloc = summary.Specs.attributes.Sil.loc.Location.nLOC;
err_log;
vflags = attributes.ProcAttributes.proc_flags;
vfile = DB.source_file_to_string attributes.ProcAttributes.loc.Location.file;
vline = attributes.ProcAttributes.loc.Location.line;
vloc = attributes.ProcAttributes.loc.Location.nLOC;
vtop = if is_top then "Y" else "N";
vsignature = signature;
vweight = nodes_nr;
@ -402,7 +404,7 @@ module BugsCsv = struct
(** Write bug report in csv format *)
let pp_bugs error_filter fname fmt summary =
let pp x = F.fprintf fmt x in
let err_log = summary.Specs.stats.Specs.err_log in
let err_log = summary.Specs.attributes.ProcAttributes.err_log in
let pp_row (node_id, node_key) loc ekind in_footprint error_name error_desc severity ltr pre_opt eclass =
if in_footprint && error_filter error_desc error_name then
let err_desc_string = error_desc_to_csv_string error_desc in
@ -415,7 +417,8 @@ module BugsCsv = struct
let kind = Exceptions.err_kind_string ekind in
let type_str = Localise.to_string error_name in
let procedure_id = Procname.to_filename (Specs.get_proc_name summary) in
let filename = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file in
let filename =
DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file in
let always_report =
match Localise.error_desc_extract_tag_value error_desc "always_report" with
| "" -> "false"
@ -450,13 +453,14 @@ module BugsJson = struct
(** Write bug report in JSON format *)
let pp_bugs error_filter fname fmt summary =
let pp x = F.fprintf fmt x in
let err_log = summary.Specs.stats.Specs.err_log in
let err_log = summary.Specs.attributes.ProcAttributes.err_log in
let pp_row (node_id, node_key) loc ekind in_footprint error_name error_desc severity ltr pre_opt eclass =
if in_footprint && error_filter error_desc error_name then
let kind = Exceptions.err_kind_string ekind in
let bug_type = Localise.to_string error_name in
let procedure_id = Procname.to_filename (Specs.get_proc_name summary) in
let file = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file in
let file =
DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file in
let bug = {
bug_class = Exceptions.err_class_string eclass;
kind = kind;
@ -480,7 +484,7 @@ end
module BugsTxt = struct
(** Write bug report in text format *)
let pp_bugs error_filter fname fmt summary =
let err_log = summary.Specs.stats.Specs.err_log in
let err_log = summary.Specs.attributes.ProcAttributes.err_log in
let pp_row (node_id, node_key) loc ekind in_footprint error_name error_desc severity ltr pre_opt eclass =
if in_footprint && error_filter error_desc error_name then
Exceptions.pp_err (node_id, node_key) loc ekind error_name error_desc None fmt () in
@ -520,7 +524,7 @@ module BugsXml = struct
(** print bugs from summary in xml *)
let pp_bugs error_filter linereader fmt summary =
let err_log = summary.Specs.stats.Specs.err_log in
let err_log = summary.Specs.attributes.ProcAttributes.err_log in
let do_row (node_id, node_key) loc ekind in_footprint error_name error_desc severity ltr pre_opt eclass =
if in_footprint && error_filter error_desc error_name then
let err_desc_string = error_desc_to_xml_string error_desc in
@ -541,7 +545,8 @@ module BugsXml = struct
let proc_name = Specs.get_proc_name summary in
let procedure_name = Procname.to_string proc_name in
let procedure_id = Procname.to_filename proc_name in
let filename = DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file in
let filename =
DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file in
let bug_hash = get_bug_hash kind type_str procedure_id filename node_key error_desc in
let forest =
[
@ -589,7 +594,7 @@ module CallsCsv = struct
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," (DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file);
pp "%s," (DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file);
pp "%d," loc.Location.line;
pp "%a@\n" Specs.CallStats.pp_trace trace in
Specs.CallStats.iter do_call stats.Specs.call_stats
@ -606,7 +611,7 @@ module UnitTest = struct
let do_spec spec =
incr cnt;
let c_file = Filename.basename
(DB.source_file_to_string summary.Specs.attributes.Sil.loc.Location.file) in
(DB.source_file_to_string summary.Specs.attributes.ProcAttributes.loc.Location.file) in
let code =
Autounit.genunit c_file proc_name !cnt (Specs.get_formals summary) spec in
F.fprintf fmt "%a@." Autounit.pp_code code in
@ -734,8 +739,8 @@ module Stats = struct
let process_summary error_filter summary linereader stats =
let specs = Specs.get_specs_from_payload summary in
let found_errors =
process_err_log error_filter linereader summary.Specs.stats.Specs.err_log stats in
let found_errors = process_err_log
error_filter linereader summary.Specs.attributes.ProcAttributes.err_log stats in
let is_defective = found_errors in
let is_verified = specs <> [] && not is_defective in
let is_checked = not (is_defective || is_verified) in
@ -744,7 +749,7 @@ module Stats = struct
if is_verified then stats.nverified <- stats.nverified + 1;
if is_checked then stats.nchecked <- stats.nchecked + 1;
if is_defective then stats.ndefective <- stats.ndefective + 1;
process_loc summary.Specs.attributes.Sil.loc stats
process_loc summary.Specs.attributes.ProcAttributes.loc stats
let num_files stats =
Hashtbl.length stats.files
@ -817,7 +822,7 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna
let error_filter error_desc error_name =
let always_report () =
Localise.error_desc_extract_tag_value error_desc "always_report" = "true" in
(filters.Inferconfig.path_filter summary.Specs.attributes.Sil.loc.Location.file
(filters.Inferconfig.path_filter summary.Specs.attributes.ProcAttributes.loc.Location.file
|| always_report ()) &&
filters.Inferconfig.error_filter error_name && filters.Inferconfig.proc_filter proc_name in
do_outf procs_csv (fun outf -> F.fprintf outf.fmt "%a" (ProcsCsv.pp_summary fname top_proc_set) summary);
@ -856,7 +861,7 @@ let process_summary filters linereader stats (top_proc_set: Procname.Set.t) (fna
do_outf xml_out (fun outf ->
Dotty.print_specs_xml
(Specs.get_signature summary)
specs summary.Specs.attributes.Sil.loc outf.fmt;
specs summary.Specs.attributes.ProcAttributes.loc outf.fmt;
close_outf outf)
end
end
@ -907,12 +912,12 @@ module AnalysisResults = struct
let summ_cmp (fname1, summ1) (fname2, summ2) =
let n =
DB.source_file_compare
summ1.Specs.attributes.Sil.loc.Location.file
summ2.Specs.attributes.Sil.loc.Location.file in
summ1.Specs.attributes.ProcAttributes.loc.Location.file
summ2.Specs.attributes.ProcAttributes.loc.Location.file in
if n <> 0 then n
else int_compare
summ1.Specs.attributes.Sil.loc.Location.line
summ2.Specs.attributes.Sil.loc.Location.line in
summ1.Specs.attributes.ProcAttributes.loc.Location.line
summ2.Specs.attributes.ProcAttributes.loc.Location.line in
list_sort summ_cmp !summaries
(** Create an iterator which loads spec files one at a time *)

@ -982,7 +982,7 @@ let perform_analysis_phase cfg tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t
re_execution pname
let set_current_language cfg proc_desc =
let language = (Cfg.Procdesc.get_attributes proc_desc).Sil.language in
let language = (Cfg.Procdesc.get_attributes proc_desc).ProcAttributes.language in
Config.curr_language := language
(** reset counters before analysing a procedure *)
@ -1041,7 +1041,7 @@ let remove_this_not_null prop =
let report_runtime_exceptions tenv cfg pdesc summary =
let pname = Specs.get_proc_name summary in
let is_public_method =
(Specs.get_attributes summary).Sil.access = Sil.Public in
(Specs.get_attributes summary).ProcAttributes.access = Sil.Public in
let is_main =
is_public_method
&& Procname.is_java pname
@ -1232,12 +1232,14 @@ let do_analysis exe_env =
let static_err_log = Cfg.Procdesc.get_err_log pdesc in (** err log from translation *)
let calls = get_calls pdesc in
let cyclomatic = Cfg.Procdesc.get_cyclomatic pdesc in
let attributes = Cfg.Procdesc.get_attributes pdesc in
let attributes =
{ (Cfg.Procdesc.get_attributes pdesc) with
ProcAttributes.err_log = static_err_log; } in
Callbacks.proc_inline_synthetic_methods cfg pdesc;
Specs.init_summary
(dep, nodes, proc_flags,
static_err_log, calls, cyclomatic, None, attributes) in
calls, cyclomatic, None, attributes) in
let filter =
if !Config.only_skips then (filter_skipped_procs cg procs_and_defined_children)
else if !Config.only_nospecs then filter_nospecs
@ -1288,6 +1290,7 @@ let print_stats_cfg proc_shadowed proc_is_active cfg =
else
let summary = Specs.get_summary_unsafe proc_name in
let stats = summary.Specs.stats in
let err_log = summary.Specs.attributes.ProcAttributes.err_log in
incr num_proc;
let specs = Specs.get_specs_from_payload summary in
tot_specs := (list_length specs) + !tot_specs;
@ -1295,14 +1298,14 @@ let print_stats_cfg proc_shadowed proc_is_active cfg =
match specs,
Errlog.size
(fun ekind in_footprint -> ekind = Exceptions.Kerror && in_footprint)
stats.Specs.err_log with
err_log with
| [], 0 -> incr num_nospec_noerror_proc
| _, 0 -> incr num_spec_noerror_proc
| [], _ -> incr num_nospec_error_proc
| _, _ -> incr num_spec_error_proc in
tot_symops := !tot_symops + stats.Specs.symops;
if stats.Specs.stats_timeout then incr num_timeout;
Errlog.extend_table err_table stats.Specs.err_log in
Errlog.extend_table err_table err_log in
let print_file_stats fmt () =
let num_errors = Errlog.err_table_size_footprint Exceptions.Kerror err_table in
let num_warnings = Errlog.err_table_size_footprint Exceptions.Kwarning err_table in

@ -26,6 +26,7 @@ let compare loc1 loc2 =
(** Dump a location *)
let d (loc: t) = L.add_print_action (L.PTloc, Obj.repr loc)
(** Dummy location *)
let dummy = {
line = -1;
col = -1;
@ -36,14 +37,6 @@ let dummy = {
let equal loc1 loc2 =
compare loc1 loc2 = 0
(** Unknown location *)
let loc_none = {
line = - 1;
col = - 1;
file = DB.source_file_empty;
nLOC = 0;
}
(** Pretty print a location *)
let pp f (loc: t) =
F.fprintf f "[line %d]" loc.line

@ -20,13 +20,11 @@ val compare : t -> t -> int
(** Dump a location. *)
val d : t -> unit
(** Dummy location *)
val dummy : t
val equal : t -> t -> bool
(** Unknown location *)
val loc_none : t
(** Pretty print a location. *)
val pp : Format.formatter -> t -> unit

@ -62,7 +62,7 @@ let fill_generated_proc_map generated_proc_map =
let update_generate_proc_map generated_proc_map =
let update_generated_pname_to_map cfg source_dir procdesc () =
let cfg_pname = Cfg.Procdesc.get_proc_name procdesc in
if not (Cfg.Procdesc.get_attributes procdesc).Sil.is_generated then
if not (Cfg.Procdesc.get_attributes procdesc).ProcAttributes.is_generated then
try ignore(Procname.Hash.find generated_proc_map cfg_pname);
Procname.Hash.replace generated_proc_map cfg_pname true
with Not_found -> () in

@ -400,7 +400,7 @@ let c_file_write_html proc_is_active linereader fname tenv cfg =
list_iter
(fun sp -> proof_cover := Specs.Visitedset.union sp.Specs.visited !proof_cover)
(Specs.get_specs_from_payload summary);
Errlog.update global_err_log summary.Specs.stats.Specs.err_log
Errlog.update global_err_log summary.Specs.attributes.ProcAttributes.err_log
end in
Cfg.iter_proc_desc cfg do_proc;
let err_per_line = create_errors_per_line global_err_log in

@ -0,0 +1,82 @@
(*
* Copyright (c) 2015 - 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.
*)
(** Attributes of a procedure. *)
module L = Logging
module F = Format
open Utils
type t =
{
access : Sil.access; (** visibility access *)
captured : (Mangled.t * Sil.typ) list; (** name and type of variables captured in blocks *)
err_log: Errlog.t; (** Error log for the procedure *)
exceptions : string list; (** exceptions thrown by the procedure *)
formals : (string * Sil.typ) list; (** name and type of formal parameters *)
func_attributes : Sil.func_attribute list;
is_abstract : bool; (** the procedure is abstract *)
mutable is_bridge_method : bool; (** the procedure is a bridge method *)
is_defined : bool; (** true if the procedure is defined, and not just declared *)
is_generated : bool; (** the procedure has been generated *)
is_objc_instance_method : bool; (** the procedure is an objective-C instance method *)
mutable is_synthetic_method : bool; (** the procedure is a synthetic method *)
language : Config.language; (** language of the procedure *)
loc : Location.t; (** location of this procedure in the source code *)
mutable locals : (Mangled.t * Sil.typ) list; (** name and type of local variables *)
method_annotation : Sil.method_annotation; (** annotations for java methods *)
proc_flags : proc_flags; (** flags of the procedure *)
proc_name : Procname.t; (** name of the procedure *)
ret_type : Sil.typ; (** return type *)
}
let copy pa =
{
access = pa.access;
captured = pa.captured;
err_log = pa.err_log;
exceptions = pa.exceptions;
formals = pa.formals;
func_attributes = pa.func_attributes;
is_abstract = pa.is_abstract;
is_bridge_method = pa.is_bridge_method;
is_defined = pa.is_defined;
is_generated = pa.is_generated;
is_objc_instance_method = pa.is_objc_instance_method;
is_synthetic_method = pa.is_synthetic_method;
language = pa.language;
loc = pa.loc;
locals = pa.locals;
method_annotation = pa.method_annotation;
proc_flags = pa.proc_flags;
proc_name = pa.proc_name;
ret_type = pa.ret_type;
}
let default proc_name language = {
access = Sil.Default;
formals = [];
captured = [];
err_log = Errlog.empty ();
exceptions = [];
func_attributes = [];
is_abstract = false;
is_defined = false;
is_bridge_method = false;
is_generated = false;
is_objc_instance_method = false;
is_synthetic_method = false;
language;
loc = Location.dummy;
locals = [];
method_annotation = Sil.method_annotation_empty;
proc_flags = proc_flags_empty ();
proc_name;
ret_type = Sil.Tvoid;
}

@ -0,0 +1,41 @@
(*
* Copyright (c) 2015 - 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.
*)
(** Attributes of a procedure. *)
open Utils
type t =
{
access : Sil.access; (** visibility access *)
captured : (Mangled.t * Sil.typ) list; (** name and type of variables captured in blocks *)
err_log: Errlog.t; (** Error log for the procedure *)
exceptions : string list; (** exceptions thrown by the procedure *)
formals : (string * Sil.typ) list; (** name and type of formal parameters *)
func_attributes : Sil.func_attribute list;
is_abstract : bool; (** the procedure is abstract *)
mutable is_bridge_method : bool; (** the procedure is a bridge method *)
is_defined : bool; (** true if the procedure is defined, and not just declared *)
is_generated : bool; (** the procedure has been generated *)
is_objc_instance_method : bool; (** the procedure is an objective-C instance method *)
mutable is_synthetic_method : bool; (** the procedure is a synthetic method *)
language : Config.language; (** language of the procedure *)
loc : Location.t; (** location of this procedure in the source code *)
mutable locals : (Mangled.t * Sil.typ) list; (** name and type of local variables *)
method_annotation : Sil.method_annotation; (** annotations for java methods *)
proc_flags : proc_flags; (** flags of the procedure *)
proc_name : Procname.t; (** name of the procedure *)
ret_type : Sil.typ; (** return type *)
}
(** Create a copy of a proc_attributes *)
val copy : t -> t
(** Create a proc_attributes with default values. *)
val default : Procname.t -> Config.language -> t

@ -834,7 +834,7 @@ let check_inconsistency_base prop =
Sil.exp_equal e Sil.exp_zero &&
Sil.pvar_is_seed pv &&
Sil.pvar_get_name pv = Mangled.from_string "self" &&
procedure_attr.Sil.is_objc_instance_method &&
procedure_attr.ProcAttributes.is_objc_instance_method &&
not (Procname.is_constructor procname)
| _ -> false in
list_exists do_hpred sigma in

@ -31,7 +31,7 @@ let log_issue
exn =
match Specs.get_summary proc_name with
| Some summary ->
let err_log = summary.Specs.stats.Specs.err_log in
let err_log = summary.Specs.attributes.ProcAttributes.err_log in
let loc = match loc with
| None -> State.get_loc ()
| Some loc -> loc in

@ -678,51 +678,6 @@ and exp =
| Lindex of exp * exp (** an array index offset: exp1[exp2] *)
| Sizeof of typ * Subtype.t (** a sizeof expression *)
(** Attributes of a procedure. *)
type proc_attributes =
{
access : access; (** visibility access *)
captured : (Mangled.t * typ) list; (** name and type of variables captured in blocks *)
exceptions : string list; (** exceptions thrown by the procedure *)
formals : (string * typ) list; (** name and type of formal parameters *)
func_attributes : func_attribute list;
is_abstract : bool; (** the procedure is abstract *)
mutable is_bridge_method : bool; (** the procedure is a bridge method *)
is_defined : bool; (** true if the procedure is defined, and not just declared *)
is_generated : bool; (** the procedure has been generated *)
is_objc_instance_method : bool; (** the procedure is an objective-C instance method *)
mutable is_synthetic_method : bool; (** the procedure is a synthetic method *)
language : Config.language; (** language of the procedure *)
loc : Location.t; (** location of this procedure in the source code *)
mutable locals : (Mangled.t * typ) list; (** name and type of local variables *)
method_annotation : method_annotation; (** annotations for java methods *)
proc_flags : proc_flags; (** flags of the procedure *)
proc_name : Procname.t; (** name of the procedure *)
ret_type : typ; (** return type *)
}
let copy_proc_attributes pa =
{
access = pa.access;
captured = pa.captured;
exceptions = pa.exceptions;
formals = pa.formals;
func_attributes = pa.func_attributes;
is_abstract = pa.is_abstract;
is_bridge_method = pa.is_bridge_method;
is_defined = pa.is_defined;
is_generated = pa.is_generated;
is_objc_instance_method = pa.is_objc_instance_method;
is_synthetic_method = pa.is_synthetic_method;
language = pa.language;
loc = pa.loc;
locals = pa.locals;
method_annotation = pa.method_annotation;
proc_flags = pa.proc_flags;
proc_name = pa.proc_name;
ret_type = pa.ret_type;
}
(** Kind of prune instruction *)
type if_kind =
| Ik_bexp (* boolean expressions, and exp ? exp : exp *)

@ -313,32 +313,6 @@ and exp =
| Lindex of exp * exp (** an array index offset: [exp1\[exp2\]] *)
| Sizeof of typ * Subtype.t (** a sizeof expression *)
(** Attributes of a procedure. *)
type proc_attributes =
{
access : access; (** visibility access *)
captured : (Mangled.t * typ) list; (** name and type of variables captured in blocks *)
exceptions : string list; (** exceptions thrown by the procedure *)
formals : (string * typ) list; (** name and type of formal parameters *)
func_attributes : func_attribute list;
is_abstract : bool; (** the procedure is abstract *)
mutable is_bridge_method : bool; (** the procedure is a bridge method *)
is_defined : bool; (** true if the procedure is defined, and not just declared *)
is_generated : bool; (** the procedure has been generated *)
is_objc_instance_method : bool; (** the procedure is an objective-C instance method *)
mutable is_synthetic_method : bool; (** the procedure is a synthetic method *)
language : Config.language; (** language of the procedure *)
loc : Location.t; (** location of this procedure in the source code *)
mutable locals : (Mangled.t * typ) list; (** name and type of local variables *)
method_annotation : method_annotation; (** annotations for java methods *)
proc_flags : proc_flags; (** flags of the procedure *)
proc_name : Procname.t; (** name of the procedure *)
ret_type : typ; (** return type *)
}
(** Create a copy of a proc_attributes *)
val copy_proc_attributes : proc_attributes -> proc_attributes
(** Sets of types. *)
module TypSet : Set.S with type elt = typ

@ -291,7 +291,6 @@ type stats =
stats_timeout: bool; (** Flag to indicate whether a timeout occurred *)
stats_calls: Cg.in_out_calls; (** num of procs calling, and called *)
symops: int; (** Number of SymOp's throughout the whole analysis of the function *)
err_log: Errlog.t; (** Error log for the procedure *)
mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *)
mutable nodes_visited_re : IntSet.t; (** Nodes visited during the re-execution phase *)
call_stats : call_stats;
@ -320,7 +319,7 @@ type summary =
stats: stats; (** statistics: execution time and list of errors *)
status: status; (** ACTIVE when the proc is being analyzed *)
timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *)
attributes : Sil.proc_attributes; (** Attributes of the procedure *)
attributes : ProcAttributes.t; (** Attributes of the procedure *)
}
(** origin of a summary: current results dir, a spec library, or models *)
@ -344,9 +343,9 @@ let pp_timeout fmt = function
| true -> F.fprintf fmt "Y"
| false -> F.fprintf fmt "N"
let pp_stats whole_seconds fmt stats =
let pp_stats err_log whole_seconds fmt stats =
F.fprintf fmt "TIME:%a TIMEOUT:%a SYMOPS:%d CALLS:%d,%d@\n" (pp_time whole_seconds) stats.stats_time pp_timeout stats.stats_timeout stats.symops stats.stats_calls.Cg.in_calls stats.stats_calls.Cg.out_calls;
F.fprintf fmt "ERRORS: @[<h>%a@]" Errlog.pp stats.err_log
F.fprintf fmt "ERRORS: @[<h>%a@]" Errlog.pp err_log
(** Print the spec *)
let pp_spec pe num_opt fmt spec =
@ -406,11 +405,11 @@ let get_signature summary =
let pp_name f () = F.fprintf f "%s" p in
let pp f () = Sil.pp_type_decl pe_text pp_name Sil.pp_exp f typ in
let decl = pp_to_string pp () in
s := if !s = "" then decl else !s ^ ", " ^ decl) summary.attributes.Sil.formals;
s := if !s = "" then decl else !s ^ ", " ^ decl) summary.attributes.ProcAttributes.formals;
let pp_procname f () = F.fprintf f "%a"
Procname.pp summary.attributes.Sil.proc_name in
Procname.pp summary.attributes.ProcAttributes.proc_name in
let pp f () =
Sil.pp_type_decl pe_text pp_procname Sil.pp_exp f summary.attributes.Sil.ret_type in
Sil.pp_type_decl pe_text pp_procname Sil.pp_exp f summary.attributes.ProcAttributes.ret_type in
let decl = pp_to_string pp () in
decl ^ "(" ^ !s ^ ")"
@ -422,24 +421,26 @@ let pp_summary_no_stats_specs fmt summary =
F.fprintf fmt "%a@\n" pp_pair (describe_phase summary);
F.fprintf fmt "Dependency_map: @[%a@]@\n" pp_dependency_map summary.dependency_map
let pp_stats_html fmt stats =
Errlog.pp_html [] fmt stats.err_log
let pp_stats_html err_log fmt stats =
Errlog.pp_html [] fmt err_log
let get_specs_from_payload summary = match summary.payload with
| PrePosts specs -> NormSpec.tospecs specs
| TypeState _ -> []
(** Print the summary *)
let pp_summary pe whole_seconds fmt summary = match pe.pe_kind with
let pp_summary pe whole_seconds fmt summary =
let err_log = summary.attributes.ProcAttributes.err_log in
match pe.pe_kind with
| PP_TEXT ->
pp_summary_no_stats_specs fmt summary;
F.fprintf fmt "%a@\n" (pp_stats whole_seconds) summary.stats;
F.fprintf fmt "%a@\n" (pp_stats err_log whole_seconds) summary.stats;
F.fprintf fmt "%a" (pp_specs pe) (get_specs_from_payload summary)
| PP_HTML ->
Io_infer.Html.pp_start_color fmt Black;
F.fprintf fmt "@\n%a" pp_summary_no_stats_specs summary;
Io_infer.Html.pp_end_color fmt ();
pp_stats_html fmt summary.stats;
pp_stats_html err_log fmt summary.stats;
Io_infer.Html.pp_hline fmt ();
F.fprintf fmt "<LISTING>@\n";
pp_specs pe fmt (get_specs_from_payload summary);
@ -447,7 +448,7 @@ let pp_summary pe whole_seconds fmt summary = match pe.pe_kind with
| PP_LATEX ->
F.fprintf fmt "\\begin{verbatim}@\n";
pp_summary_no_stats_specs fmt summary;
F.fprintf fmt "%a@\n" (pp_stats whole_seconds) summary.stats;
F.fprintf fmt "%a@\n" (pp_stats err_log whole_seconds) summary.stats;
F.fprintf fmt "\\end{verbatim}@\n";
F.fprintf fmt "%a@\n" (pp_specs pe) (get_specs_from_payload summary)
@ -455,7 +456,7 @@ let pp_summary pe whole_seconds fmt summary = match pe.pe_kind with
let pp_spec_table pe whole_seconds fmt () =
Procname.Hash.iter (fun proc_name (summ, orig) -> F.fprintf fmt "PROC %a@\n%a@\n" Procname.pp proc_name (pp_summary pe whole_seconds) summ) spec_tbl
let empty_stats err_log calls cyclomatic in_out_calls_opt =
let empty_stats calls cyclomatic in_out_calls_opt =
{ stats_time = 0.0;
stats_timeout = false;
stats_calls =
@ -463,7 +464,6 @@ let empty_stats err_log calls cyclomatic in_out_calls_opt =
| Some in_out_calls -> in_out_calls
| None -> { Cg.in_calls = 0; Cg.out_calls = 0 });
symops = 0;
err_log = err_log;
nodes_visited_fp = IntSet.empty;
nodes_visited_re = IntSet.empty;
call_stats = CallStats.init calls;
@ -627,7 +627,7 @@ let proc_is_library proc_name proc_desc =
else false
(** Get the attributes of a procedure, looking first in the procdesc and then in the .specs file. *)
let proc_get_attributes proc_name proc_desc : Sil.proc_attributes =
let proc_get_attributes proc_name proc_desc : ProcAttributes.t =
let from_proc_desc = Cfg.Procdesc.get_attributes proc_desc in
let defined = Cfg.Procdesc.is_defined proc_desc in
if not defined then
@ -638,7 +638,7 @@ let proc_get_attributes proc_name proc_desc : Sil.proc_attributes =
else from_proc_desc
let proc_get_method_annotation proc_name proc_desc =
(proc_get_attributes proc_name proc_desc).Sil.method_annotation
(proc_get_attributes proc_name proc_desc).ProcAttributes.method_annotation
let get_origin proc_name =
match get_summary_origin proc_name with
@ -663,13 +663,13 @@ let get_timestamp summary =
summary.timestamp
let get_proc_name summary =
summary.attributes.Sil.proc_name
summary.attributes.ProcAttributes.proc_name
let get_ret_type summary =
summary.attributes.Sil.ret_type
summary.attributes.ProcAttributes.ret_type
let get_formals summary =
summary.attributes.Sil.formals
summary.attributes.ProcAttributes.formals
let get_attributes summary =
summary.attributes
@ -680,7 +680,7 @@ let get_flag proc_name key =
match get_summary proc_name with
| None -> None
| Some summary ->
let proc_flags = summary.attributes.Sil.proc_flags in
let proc_flags = summary.attributes.ProcAttributes.proc_flags in
try
Some (Hashtbl.find proc_flags key)
with Not_found -> None
@ -692,7 +692,7 @@ let get_iterations proc_name =
| None ->
raise (Failure ("Specs.get_iterations: " ^ (Procname.to_string proc_name) ^ "Not_found"))
| Some summary ->
let proc_flags = summary.attributes.Sil.proc_flags in
let proc_flags = summary.attributes.ProcAttributes.proc_flags in
try
let time_str = Hashtbl.find proc_flags proc_flag_iterations in
Pervasives.int_of_string time_str
@ -747,11 +747,11 @@ let update_dependency_map proc_name =
set_summary_origin proc_name { summary with dependency_map = current_dependency_map } origin
(** [init_summary (depend_list, nodes,
proc_flags, initial_err_log, calls, cyclomatic, in_out_calls_opt, proc_attributes)]
proc_flags, calls, cyclomatic, in_out_calls_opt, proc_attributes)]
initializes the summary for [proc_name] given dependent procs in list [depend_list]. *)
let init_summary
(depend_list, nodes,
proc_flags, initial_err_log, calls, cyclomatic, in_out_calls_opt,
proc_flags, calls, cyclomatic, in_out_calls_opt,
proc_attributes) =
let dependency_map = mk_initial_dependency_map depend_list in
let summary =
@ -761,42 +761,24 @@ let init_summary
phase = FOOTPRINT;
sessions = ref 0;
payload = PrePosts [];
stats = empty_stats initial_err_log calls cyclomatic in_out_calls_opt;
stats = empty_stats calls cyclomatic in_out_calls_opt;
status = INACTIVE;
timestamp = 0;
attributes =
{ proc_attributes with
Sil.proc_flags = proc_flags; };
ProcAttributes.proc_flags = proc_flags; };
} in
Procname.Hash.replace spec_tbl proc_attributes.Sil.proc_name (summary, Res_dir)
Procname.Hash.replace spec_tbl proc_attributes.ProcAttributes.proc_name (summary, Res_dir)
let reset_summary call_graph proc_name loc =
let dependents = Cg.get_defined_children call_graph proc_name in
let proc_attributes = {
Sil.access = Sil.Default;
formals = [];
captured = [];
exceptions = [];
func_attributes = [];
is_abstract = false;
is_defined = false;
is_bridge_method = false;
is_generated = false;
is_objc_instance_method = false;
is_synthetic_method = false;
language = !Config.curr_language;
loc;
locals = [];
method_annotation = Sil.method_annotation_empty;
proc_flags = proc_flags_empty ();
proc_name;
ret_type = Sil.Tvoid;
} in
let proc_attributes =
{ (ProcAttributes.default proc_name !Config.curr_language) with
loc; } in
init_summary (
Procname.Set.elements dependents,
[],
proc_flags_empty (),
Errlog.empty (),
[],
0,
Some (Cg.get_calls call_graph proc_name),

@ -105,7 +105,6 @@ type stats =
stats_timeout: bool; (** Flag to indicate whether a timeout occurred *)
stats_calls: Cg.in_out_calls; (** num of procs calling, and called *)
symops: int; (** Number of SymOp's throughout the whole analysis of the function *)
err_log: Errlog.t; (** Error log for the procedure *)
mutable nodes_visited_fp : IntSet.t; (** Nodes visited during the footprint phase *)
mutable nodes_visited_re : IntSet.t; (** Nodes visited during the re-execution phase *)
call_stats : CallStats.t;
@ -133,7 +132,7 @@ type summary =
stats: stats; (** statistics: execution time and list of errors *)
status: status; (** ACTIVE when the proc is being analyzed *)
timestamp: int; (** Timestamp of the specs, >= 0, increased every time the specs change *)
attributes : Sil.proc_attributes; (** Attributes of the procedure *)
attributes : ProcAttributes.t; (** Attributes of the procedure *)
}
(** origin of a summary: current results dir, a spec library, or models *)
@ -161,7 +160,7 @@ val d_spec : 'a spec -> unit
val get_proc_name : summary -> Procname.t
(** Get the attributes of the procedure. *)
val get_attributes : summary -> Sil.proc_attributes
val get_attributes : summary -> ProcAttributes.t
(** Get the return type of the procedure *)
val get_ret_type : summary -> Sil.typ
@ -217,11 +216,10 @@ val init_summary :
(Procname.t list * (** depend list *)
int list * (** nodes *)
proc_flags * (** procedure flags *)
Errlog.t * (** initial error log *)
(Procname.t * Location.t) list * (** calls *)
int * (** cyclomatic *)
(Cg.in_out_calls option) * (** in and out calls *)
Sil.proc_attributes) (** attributes of the procedure *)
ProcAttributes.t) (** attributes of the procedure *)
-> unit
val reset_summary : Cg.t -> Procname.t -> Location.t -> unit
@ -248,7 +246,7 @@ val pp_specs : printenv -> Format.formatter -> Prop.normal spec list -> unit
val pp_summary : printenv -> bool -> Format.formatter -> summary -> unit
(** Get the attributes of a procedure, looking first in the procdesc and then in the .specs file. *)
val proc_get_attributes : Procname.t -> Cfg.Procdesc.t -> Sil.proc_attributes
val proc_get_attributes : Procname.t -> Cfg.Procdesc.t -> ProcAttributes.t
val proc_get_method_annotation : Procname.t -> Cfg.Procdesc.t -> Sil.method_annotation

@ -524,7 +524,7 @@ let call_should_be_skipped callee_pname summary =
(* check skip flag *)
|| Specs.get_flag callee_pname proc_flag_skip <> None
(* skip abstract methods *)
|| summary.Specs.attributes.Sil.is_abstract
|| summary.Specs.attributes.ProcAttributes.is_abstract
(* treat calls with no specs as skip functions in angelic mode *)
|| (!Config.angelic_execution && Specs.get_specs_from_payload summary == [])
@ -643,12 +643,11 @@ let proc_desc_copy cfg pdesc pname pname' =
(match Cfg.Procdesc.find_from_name cfg pname' with
| Some pdesc' -> pdesc'
| None ->
let open Cfg.Procdesc in
create {
cfg = cfg;
Cfg.Procdesc.create {
Cfg.Procdesc.cfg = cfg;
proc_attributes =
{ (Sil.copy_proc_attributes (get_attributes pdesc)) with
Sil.proc_name = pname'; };
{ (ProcAttributes.copy (Cfg.Procdesc.get_attributes pdesc)) with
ProcAttributes.proc_name = pname'; };
})
let method_exists right_proc_name methods =
@ -1257,7 +1256,8 @@ and sym_exe_check_variadic_sentinel_if_present cfg pdesc tenv prop path actual_p
| None -> [(prop, path)]
| Some callee_pdesc ->
let proc_attributes = Cfg.Procdesc.get_attributes callee_pdesc in
match Sil.get_sentinel_func_attribute_value proc_attributes.Sil.func_attributes with
match Sil.get_sentinel_func_attribute_value
proc_attributes.ProcAttributes.func_attributes with
| None -> [(prop, path)]
| Some sentinel_arg ->
let formals = Cfg.Procdesc.get_formals callee_pdesc in
@ -1317,7 +1317,7 @@ and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc =
(* In case we call an objc instance method we add and extra spec *)
(* were the receiver is null and the semantics of the call is nop*)
if (!Config.curr_language <> Config.Java) && !Config.objc_method_call_semantics &&
(Specs.get_attributes summary).Sil.is_objc_instance_method then
(Specs.get_attributes summary).ProcAttributes.is_objc_instance_method then
handle_objc_method_call actual_pars actual_params pre tenv cfg ret_ids pdesc callee_pname loc path
else (* non-objective-c method call. Standard tabulation *)
Tabulation.exe_function_call tenv cfg ret_ids pdesc callee_pname loc actual_params pre path

@ -32,7 +32,7 @@ end (* PP *)
(** State that persists in the .specs files. *)
module ST = struct
let add summary key value =
proc_flags_add summary.Specs.attributes.Sil.proc_flags key value
proc_flags_add summary.Specs.attributes.ProcAttributes.proc_flags key value
let pname_add proc_name key value =
let summary = Specs.get_summary_unsafe proc_name in
@ -43,14 +43,14 @@ module ST = struct
let pname_find proc_name key =
if Procname.Set.mem proc_name !files_open then
let summary = Specs.get_summary_unsafe proc_name in
proc_flags_find summary.Specs.attributes.Sil.proc_flags key
proc_flags_find summary.Specs.attributes.ProcAttributes.proc_flags key
else begin
match Specs.get_summary proc_name with
| None -> raise Not_found
| Some summary ->
begin
files_open := Procname.Set.add proc_name !files_open;
proc_flags_find summary.Specs.attributes.Sil.proc_flags key
proc_flags_find summary.Specs.attributes.ProcAttributes.proc_flags key
end
end

@ -49,7 +49,7 @@ module Err = struct
let new_summ = { old_summ with
Specs.attributes =
{ old_summ.Specs.attributes with
Sil.loc = Cfg.Procdesc.get_loc proc_desc };
ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc };
Specs.nodes = nodes;
Specs.payload = Specs.PrePosts specs } in
Specs.add_summary proc_name new_summ

@ -54,7 +54,7 @@ struct
let old_summ = Specs.get_summary_unsafe proc_name in
let nodes = list_map (fun n -> Cfg.Node.get_id n) (Cfg.Procdesc.get_nodes proc_desc) in
let method_annotation =
(Specs.proc_get_attributes proc_name proc_desc).Sil.method_annotation in
(Specs.proc_get_attributes proc_name proc_desc).ProcAttributes.method_annotation in
let new_summ =
{
old_summ with
@ -63,7 +63,7 @@ struct
Specs.attributes =
{
old_summ.Specs.attributes with
Sil.loc = Cfg.Procdesc.get_loc proc_desc;
ProcAttributes.loc = Cfg.Procdesc.get_loc proc_desc;
method_annotation;
};
} in
@ -177,7 +177,8 @@ struct
let do_proc (init_pn, init_pd) =
let filter callee_pn callee_pd =
let is_private =
(Specs.proc_get_attributes callee_pn callee_pd).Sil.access = Sil.Private in
let attr = Specs.proc_get_attributes callee_pn callee_pd in
attr.ProcAttributes.access = Sil.Private in
let same_class =
let get_class_opt pn =
if Procname.is_java pn then Some (Procname.java_get_class pn)
@ -305,12 +306,12 @@ struct
let filter_special_cases () =
if Procname.java_is_access_method proc_name ||
(Specs.proc_get_attributes proc_name proc_desc).Sil.is_bridge_method
(Specs.proc_get_attributes proc_name proc_desc).ProcAttributes.is_bridge_method
then None
else
begin
let annotated_signature = Models.get_annotated_signature proc_desc proc_name in
if (Specs.proc_get_attributes proc_name proc_desc).Sil.is_abstract then
if (Specs.proc_get_attributes proc_name proc_desc).ProcAttributes.is_abstract then
begin
if Models.infer_library_return &&
EradicateChecks.classify_procedure proc_name proc_desc = "L" then

@ -383,7 +383,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
let visible_params = list_drop_first n params in
(* Drop the trailing hidden parameter if the constructor is synthetic. *)
if (Cfg.Procdesc.get_attributes pdesc).Sil.is_synthetic_method then
if (Cfg.Procdesc.get_attributes pdesc).ProcAttributes.is_synthetic_method then
list_drop_last 1 visible_params
else
visible_params
@ -395,7 +395,7 @@ let typecheck_instr ext calls_this checks (node: Cfg.Node.t) idenv get_proc_desc
(* Drop parameters from the signature which we do not check in a call. *)
let drop_unchecked_signature_params pdesc pname annotated_signature =
if Procname.is_constructor pname &&
(Cfg.Procdesc.get_attributes pdesc).Sil.is_synthetic_method then
(Cfg.Procdesc.get_attributes pdesc).ProcAttributes.is_synthetic_method then
list_drop_last 1 annotated_signature.Annotations.params
else
annotated_signature.Annotations.params in
@ -947,7 +947,7 @@ let typecheck_node
let exceptions =
match get_proc_desc callee_pname with
| Some callee_pdesc ->
(Specs.proc_get_attributes callee_pname callee_pdesc).Sil.exceptions
(Specs.proc_get_attributes callee_pname callee_pdesc).ProcAttributes.exceptions
| None -> [] in
if exceptions <> [] then
typestates_exn := typestate :: !typestates_exn

@ -15,30 +15,9 @@ open CFrontend_utils
let create_empty_procdesc () =
let proc_name = Procname.from_string_c_fun "__INFER_$GLOBAL_VAR_env" in
let open Cfg.Procdesc in
let proc_attributes =
{
Sil.access = Sil.Default;
captured = [];
exceptions = [];
formals = [];
func_attributes = [];
is_abstract = false;
is_bridge_method = false;
is_defined = false;
is_generated = false;
is_objc_instance_method = false;
is_synthetic_method = false;
language = Config.C_CPP;
loc = Location.loc_none;
locals = [];
method_annotation = Sil.method_annotation_empty;
proc_flags = proc_flags_empty ();
proc_name;
ret_type = Sil.Tvoid;
} in
create {
cfg = Cfg.Node.create_cfg ();
let proc_attributes = ProcAttributes.default proc_name Config.C_CPP in
Cfg.Procdesc.create {
Cfg.Procdesc.cfg = Cfg.Node.create_cfg ();
proc_attributes = proc_attributes;
}

@ -229,7 +229,7 @@ let should_create_procdesc cfg procname defined generated =
| Some prevoius_procdesc ->
let is_defined_previous = Cfg.Procdesc.is_defined prevoius_procdesc in
let is_generated_previous =
(Cfg.Procdesc.get_attributes prevoius_procdesc).Sil.is_generated in
(Cfg.Procdesc.get_attributes prevoius_procdesc).ProcAttributes.is_generated in
if defined &&
((not is_defined_previous) || (generated && is_generated_previous)) then
(Cfg.Procdesc.remove cfg (Cfg.Procdesc.get_proc_name prevoius_procdesc) true;
@ -256,32 +256,19 @@ let create_local_procdesc cfg tenv ms fbody captured is_objc_inst_method =
let ret_type = get_return_type tenv ms in
let captured' = list_map (fun (s, t, _) -> (s, t)) captured in
let procdesc =
(* This part below is a boilerplate and the following list of *)
(* instructions should be moved in the Cfg.Procdesc module *)
let open Cfg.Procdesc in
let proc_attributes =
{
Sil.access = Sil.Default;
captured = captured';
exceptions = [];
{ (ProcAttributes.default proc_name Config.C_CPP) with
ProcAttributes.captured = captured';
formals;
func_attributes = attributes;
is_abstract = false;
is_bridge_method = false;
is_defined = defined;
is_generated;
is_objc_instance_method = is_objc_inst_method;
is_synthetic_method = false;
language = Config.C_CPP;
loc = loc_start;
locals = [];
method_annotation = Sil.method_annotation_empty;
proc_flags = proc_flags_empty ();
proc_name;
ret_type;
} in
create {
cfg;
Cfg.Procdesc.create {
Cfg.Procdesc.cfg;
proc_attributes;
} in
if defined then
@ -308,32 +295,17 @@ let create_external_procdesc cfg proc_name is_objc_inst_method type_opt =
| Some (ret_type, arg_types) ->
ret_type, list_map (fun typ -> ("x", typ)) arg_types
| None -> Sil.Tvoid, []) in
let loc = Location.loc_none in
let loc = Location.dummy in
let _ =
let open Cfg.Procdesc in
let proc_attributes =
{
Sil.access = Sil.Default;
captured = [];
exceptions = [];
formals;
func_attributes = [];
is_abstract = false;
is_bridge_method = false;
is_defined = false;
is_generated = false;
{ (ProcAttributes.default proc_name Config.C_CPP) with
ProcAttributes.formals;
is_objc_instance_method = is_objc_inst_method;
is_synthetic_method = false;
language = Config.C_CPP;
loc;
locals = [];
method_annotation = Sil.method_annotation_empty;
proc_flags = proc_flags_empty ();
proc_name;
ret_type;
} in
create {
cfg = cfg;
Cfg.Procdesc.create {
Cfg.Procdesc.cfg = cfg;
proc_attributes = proc_attributes;
} in
()

@ -278,30 +278,14 @@ let add_harness_to_cg harness_name harness_cfg harness_node loc cg tenv =
let formals =
let param_strs = Procname.java_get_parameters proc_name in
list_fold_right (fun typ_str params -> ("", lookup_typ typ_str) :: params) param_strs [] in
let open Cfg.Procdesc in
let proc_attributes =
{
Sil.access = Sil.Default;
captured = [];
exceptions = [];
formals;
func_attributes = [];
is_abstract = false;
is_defined = false;
is_bridge_method = false;
is_generated = false;
is_objc_instance_method = false;
is_synthetic_method = false;
language = Config.Java;
{ (ProcAttributes.default proc_name Config.Java) with
ProcAttributes.formals;
loc;
locals = [];
method_annotation = Sil.method_annotation_empty;
proc_flags = proc_flags_empty ();
proc_name;
ret_type;
} in
create {
cfg = harness_cfg;
Cfg.Procdesc.create {
Cfg.Procdesc.cfg = harness_cfg;
proc_attributes = proc_attributes;
} in
list_iter (fun p ->
@ -331,30 +315,13 @@ let setup_harness_cfg harness_name harness_cfg env proc_file_map tenv =
| None -> assert false in
let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in
let procdesc =
let open Cfg.Procdesc in
let proc_attributes =
{
Sil.access = Sil.Default;
captured = [];
exceptions = [];
formals = [];
func_attributes = [];
is_abstract = false;
is_bridge_method = false;
is_defined = true;
is_generated = false;
is_objc_instance_method = false;
is_synthetic_method = false;
language = Config.Java;
{ (ProcAttributes.default harness_name Config.Java) with
ProcAttributes.is_defined = true;
loc = env.pc;
locals = [];
method_annotation = Sil.method_annotation_empty;
proc_flags = proc_flags_empty ();
proc_name = harness_name;
ret_type = Sil.Tvoid;
} in
create {
cfg = harness_cfg;
Cfg.Procdesc.create {
Cfg.Procdesc.cfg = harness_cfg;
proc_attributes;
} in
let harness_node =

@ -286,30 +286,20 @@ let create_local_procdesc program linereader cfg tenv node m =
let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in
let method_annotation = JAnnotation.translate_method am.Javalib.am_annotations in
let procdesc =
let open Cfg.Procdesc in
let proc_attributes =
{
Sil.access = trans_access am.Javalib.am_access;
captured = [];
{ (ProcAttributes.default proc_name Config.Java) with
ProcAttributes.access = trans_access am.Javalib.am_access;
exceptions = list_map JBasics.cn_name am.Javalib.am_exceptions;
formals;
func_attributes = [];
is_abstract = true;
is_bridge_method = am.Javalib.am_bridge;
is_defined = true;
is_generated = false;
is_objc_instance_method = false;
is_synthetic_method = am.Javalib.am_synthetic;
language = Config.Java;
loc = Location.dummy;
locals = [];
method_annotation;
proc_flags = proc_flags_empty ();
proc_name;
ret_type = JTransType.return_type program tenv ms meth_kind;
} in
create {
cfg = cfg;
Cfg.Procdesc.create {
Cfg.Procdesc.cfg = cfg;
proc_attributes;
} in
let start_kind = Cfg.Node.Start_node procdesc in
@ -323,30 +313,18 @@ let create_local_procdesc program linereader cfg tenv node m =
let formals = formals_from_signature program tenv cn ms (JTransType.get_method_kind m) in
let method_annotation = JAnnotation.translate_method cm.Javalib.cm_annotations in
let _procdesc =
let open Cfg.Procdesc in
let proc_attributes =
{
Sil.access = trans_access cm.Javalib.cm_access;
captured = [];
{ (ProcAttributes.default proc_name Config.Java) with
ProcAttributes.access = trans_access cm.Javalib.cm_access;
exceptions = list_map JBasics.cn_name cm.Javalib.cm_exceptions;
formals;
func_attributes = [];
is_abstract = false;
is_bridge_method = cm.Javalib.cm_bridge;
is_defined = false;
is_generated = false;
is_objc_instance_method = false;
is_synthetic_method = cm.Javalib.cm_synthetic;
language = Config.Java;
loc = Location.dummy;
locals = [];
method_annotation;
proc_flags = proc_flags_empty ();
proc_name;
ret_type = JTransType.return_type program tenv ms meth_kind;
} in
create {
cfg = cfg;
Cfg.Procdesc.create {
Cfg.Procdesc.cfg = cfg;
proc_attributes = proc_attributes;
} in
()
@ -361,30 +339,21 @@ let create_local_procdesc program linereader cfg tenv node m =
update_constr_loc cn ms loc_start;
update_init_loc cn ms loc_exit;
let procdesc =
let open Cfg.Procdesc in
let proc_attributes =
{
Sil.access = trans_access cm.Javalib.cm_access;
captured = [];
{ (ProcAttributes.default proc_name Config.Java) with
ProcAttributes.access = trans_access cm.Javalib.cm_access;
exceptions = list_map JBasics.cn_name cm.Javalib.cm_exceptions;
formals;
func_attributes = [];
is_abstract = false;
is_bridge_method = cm.Javalib.cm_bridge;
is_defined = true;
is_generated = false;
is_objc_instance_method = false;
is_synthetic_method = cm.Javalib.cm_synthetic;
language = Config.Java;
loc = loc_start;
locals;
method_annotation;
proc_flags = proc_flags_empty ();
proc_name;
ret_type = JTransType.return_type program tenv ms meth_kind;
} in
create {
cfg = cfg;
Cfg.Procdesc.create {
Cfg.Procdesc.cfg = cfg;
proc_attributes = proc_attributes;
} in
let start_kind = Cfg.Node.Start_node procdesc in
@ -410,7 +379,7 @@ let create_local_procdesc program linereader cfg tenv node m =
create_new_procdesc ()
end
let create_external_procdesc program cfg tenv cn ms method_annotation kind =
let create_external_procdesc program cfg tenv cn ms kind =
let return_type =
match JBasics.ms_rtype ms with
| None -> Sil.Tvoid
@ -418,30 +387,13 @@ let create_external_procdesc program cfg tenv cn ms method_annotation kind =
let formals = formals_from_signature program tenv cn ms kind in
let proc_name = JTransType.get_method_procname cn ms kind in
ignore (
let open Cfg.Procdesc in
let proc_attributes =
{
Sil.access = Sil.Default;
captured = [];
exceptions = [];
formals;
func_attributes = [];
is_abstract = false;
is_bridge_method = false;
is_defined = false;
is_generated = false;
is_objc_instance_method = false;
is_synthetic_method = false;
language = Config.Java;
loc = Location.dummy;
locals = [];
method_annotation;
proc_flags = proc_flags_empty ();
proc_name;
{ (ProcAttributes.default proc_name Config.Java) with
ProcAttributes.formals;
ret_type = return_type;
} in
create {
cfg = cfg;
Cfg.Procdesc.create {
Cfg.Procdesc.cfg = cfg;
proc_attributes = proc_attributes;
})
@ -450,7 +402,7 @@ let rec get_method_procdesc program cfg tenv cn ms kind =
let procname = JTransType.get_method_procname cn ms kind in
match lookup_procdesc cfg procname with
| Unknown ->
create_external_procdesc program cfg tenv cn ms Sil.method_annotation_empty kind;
create_external_procdesc program cfg tenv cn ms kind;
get_method_procdesc program cfg tenv cn ms kind
| Created status -> status

@ -120,30 +120,17 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map)
match ret_tp_opt with
| None -> Sil.Tvoid
| Some ret_tp -> trans_typ ret_tp in
let (proc_attrs : Sil.proc_attributes) =
let (proc_attrs : ProcAttributes.t) =
let open Sil in
{ access = Sil.Default;
captured = [];
exceptions = [];
formals = list_map (fun (tp, name) -> (name, trans_typ tp)) params;
func_attributes = [];
is_abstract = false;
is_bridge_method = false;
{ (ProcAttributes.default proc_name Config.C_CPP) with
ProcAttributes.formals = list_map (fun (tp, name) -> (name, trans_typ tp)) params;
is_defined = true; (** is defined and not just declared *)
is_generated = false;
is_objc_instance_method = false;
is_synthetic_method = false;
language = Config.C_CPP;
loc = source_only_location ();
locals = []; (* TODO *)
method_annotation = Sil.method_annotation_empty;
proc_flags = proc_flags_empty ();
proc_name;
ret_type;
} in
let (procdesc_builder : Cfg.Procdesc.proc_desc_builder) =
let open Cfg.Procdesc in
{ cfg = cfg;
{ Cfg.Procdesc.cfg = cfg;
proc_attributes = proc_attrs;
} in
let procdesc = Cfg.Procdesc.create procdesc_builder in

Loading…
Cancel
Save