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

[backend] Remove the global reference DB.current_source and clean up the flow of information about the current source file.

Browse Source 
Summary:
The global reference `DB.current_source` is used internally in the module DB, by all the front-ends, and directly and indirectly by the back-end, including saving and restoring the state in case of on-demand procedure calls. In particular, it is heavily used in printing functions.
This diff cleans up the flow of information about what the current file is, making it explicit, and removes the reference.

Reviewed By: jberdine

Differential Revision: D3901247

fbshipit-source-id: ef596bd
master
Cristiano Calcagno 8 years ago committed by Facebook Github Bot
parent 526cf6da6a
commit 4cee6907ec
41 changed files with 395 additions and 383 deletions
Show Stats Download Patch File Download Diff File

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

@ -1168,13 +1168,6 @@ let save_attributes source_file cfg => {
};
{...attributes, loc: loc', source_file_captured: source_file}
};
/*
L.stderr "save_proc@. proc_name:%a@. filename:%s@. current_source:%s@. loc:%s@."
Procname.pp (Procdesc.get_proc_name proc_desc)
(DB.filename_to_string filename)
(DB.source_file_to_string !DB.current_source)
(Location.to_string loc);
*/
AttributesTable.store_attributes attributes'
};
IList.iter save_proc (get_all_procs cfg)

27
infer/src/IR/Cg.re
Unescape View File

@ -49,7 +49,14 @@ type t = {
node_map: Procname.Hash.t node_info /** map from node to node_info */
};
let create () => {source: !DB.current_source, nLOC: !Config.nLOC, node_map: Procname.Hash.create 3};
let create source_opt => {
let source =
switch source_opt {
| None => DB.source_file_empty
| Some source => source
};
{source, nLOC: !Config.nLOC, node_map: Procname.Hash.create 3}
};
let add_node g n defined::defined =>
try {
@ -355,11 +362,11 @@ let callgraph_serializer: Serialization.serializer (DB.source_file, int, nodes_a
/** Load a call graph from a file */
let load_from_file (filename: DB.filename) :option t => {
let g = create ();
let load_from_file (filename: DB.filename) :option t =>
switch (Serialization.from_file callgraph_serializer filename) {
| None => None
| Some (source, nLOC, (nodes, edges)) =>
let g = create (Some source);
IList.iter
(
fun (node, defined) =>
@ -369,11 +376,9 @@ let load_from_file (filename: DB.filename) :option t => {
)
nodes;
IList.iter (fun (nfrom, nto) => add_edge g nfrom nto) edges;
g.source = source;
g.nLOC = nLOC;
Some g
}
};
};
/** Save a call graph into a file */
@ -431,14 +436,10 @@ let pp_graph_dotty get_specs (g: t) fmt => {
};
/** Print the current call graph as a dotty file.
If the filename is [None], use the current file dir inside the DB dir. */
let save_call_graph_dotty fname_opt get_specs (g: t) => {
/** Print the call graph as a dotty file. */
let save_call_graph_dotty source get_specs (g: t) => {
let fname_dot =
switch fname_opt {
| None => DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir ["call_graph.dot"]
| Some fname => fname
};
DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source) ["call_graph.dot"];
let outc = open_out (DB.filename_to_string fname_dot);
let fmt = F.formatter_of_out_channel outc;
pp_graph_dotty get_specs g fmt;

7
infer/src/IR/Cg.rei
Unescape View File

@ -43,7 +43,7 @@ let calls_recursively: t => Procname.t => Procname.t => bool;
/** Create an empty call graph */
let create: unit => t;
let create: option DB.source_file => t;
/** [extend cg1 gc2] extends [cg1] in place with nodes and edges from [gc2];
@ -123,9 +123,8 @@ let node_defined: t => Procname.t => bool;
let remove_node_defined: t => Procname.t => unit;
/** Print the current call graph as a dotty file. If the filename is [None],
use the current file dir inside the DB dir. */
let save_call_graph_dotty: option DB.filename => (Procname.t => list 'a) => t => unit;
/** Print the call graph as a dotty file. */
let save_call_graph_dotty: DB.source_file => (Procname.t => list 'a) => t => unit;
/** Save a call graph into a file */

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

@ -101,9 +101,6 @@ let source_file_encoding source_file =
let source_file_empty = Absolute ""
(** current source file *)
let current_source = ref source_file_empty
(** {2 Source Dirs} *)
(** source directory: the directory inside the results dir corresponding to a source file *)
@ -281,9 +278,12 @@ module Results_dir = struct
(** kind of path: specifies how to interpret a path *)
type path_kind =
| Abs_root (** absolute path implicitly rooted at the root of the results dir *)
| Abs_source_dir (** absolute path implicitly rooted at the source directory for the current file *)
| Rel (** relative path *)
| Abs_root
(** absolute path implicitly rooted at the root of the results dir *)
| Abs_source_dir of source_file
(** absolute path implicitly rooted at the source directory for the file *)
| Rel
(** relative path *)
let filename_from_base base path =
let rec f = function
@ -296,8 +296,8 @@ module Results_dir = struct
let path_to_filename pk path =
let base = match pk with
| Abs_root -> Config.results_dir
| Abs_source_dir ->
let dir = source_dir_from_source_file !current_source in
| Abs_source_dir source ->
let dir = source_dir_from_source_file source in
source_dir_to_string dir
| Rel -> Filename.current_dir_name in
filename_from_base base path
@ -306,14 +306,14 @@ module Results_dir = struct
let specs_dir = path_to_filename Abs_root [Config.specs_dir_name]
(** initialize the results directory *)
let init () =
let init source =
create_dir Config.results_dir;
create_dir specs_dir;
create_dir (path_to_filename Abs_root [Config.attributes_dir_name]);
create_dir (path_to_filename Abs_root [Config.sources_dir_name]);
create_dir (path_to_filename Abs_root [Config.captured_dir_name]);
if not (source_file_equal !current_source source_file_empty) then
create_dir (path_to_filename Abs_source_dir [])
if not (source_file_equal source source_file_empty) then
create_dir (path_to_filename (Abs_source_dir source) [])
let clean_specs_dir () =
create_dir specs_dir; (* create dir just in case it doesn't exist to avoid errors *)

18
infer/src/backend/DB.mli
Unescape View File

@ -35,6 +35,8 @@ val file_modified_time : ?symlink:bool -> filename -> float
(** Return whether filename was updated after analysis started. File doesn't have to exist *)
val file_was_updated_after_start : filename -> bool
type source_file
(** {2 Results Directory} *)
module Results_dir : sig
@ -43,9 +45,12 @@ module Results_dir : sig
(** kind of path: specifies how to interpret a path *)
type path_kind =
| Abs_root (** absolute path implicitly rooted at the root of the results dir *)
| Abs_source_dir (** absolute path implicitly rooted at the source directory for the current file *)
| Rel (** relative path *)
| Abs_root
(** absolute path implicitly rooted at the root of the results dir *)
| Abs_source_dir of source_file
(** absolute path implicitly rooted at the source directory for the file *)
| Rel
(** relative path *)
(** convert a path to a filename *)
val path_to_filename : path_kind -> path -> filename
@ -54,7 +59,7 @@ module Results_dir : sig
val specs_dir : filename
(** Initialize the results directory *)
val init : unit -> unit
val init : source_file -> unit
(** Clean up specs directory *)
val clean_specs_dir : unit -> unit
@ -71,17 +76,12 @@ type origin =
(** {2 Source Files} *)
type source_file
(** Maps from source_file *)
module SourceFileMap : Map.S with type key = source_file
(** Set of source files *)
module SourceFileSet : Set.S with type elt = source_file
(** current source file *)
val current_source : source_file ref
(** comparison of source files *)
val source_file_compare : source_file -> source_file -> int

5
infer/src/backend/InferPrint.re
Unescape View File

@ -871,7 +871,7 @@ let module Summary = {
"Procedure: %a@\n%a@."
Procname.pp
proc_name
(Specs.pp_summary pe_text Config.whole_seconds)
(Specs.pp_summary_text whole_seconds::Config.whole_seconds)
summary
}
};
@ -881,7 +881,8 @@ let module Summary = {
let proc_name = Specs.get_proc_name summary;
Latex.pp_section
fmt ("Analysis of function " ^ Latex.convert_string (Procname.to_string proc_name));
F.fprintf fmt "@[<v>%a@]" (Specs.pp_summary (pe_latex Black) Config.whole_seconds) summary
F.fprintf
fmt "@[<v>%a@]" (Specs.pp_summary_latex Black whole_seconds::Config.whole_seconds) summary
};
let pp_summary_xml summary fname =>
if Config.xml_specs {

18
infer/src/backend/dotty.ml
Unescape View File

@ -1017,31 +1017,33 @@ let pp_cfgnode fmt (n: Cfg.Node.t) =
(* Print the extra information related to the inteprocedural aspect, ie., *)
(* special node, and call / return edges *)
let print_icfg fmt cfg =
let print_icfg source fmt cfg =
let print_node node =
let loc = Cfg.Node.get_loc node in
if (Config.dotty_cfg_libs || DB.source_file_equal loc.Location.file !DB.current_source) then
if (Config.dotty_cfg_libs || DB.source_file_equal loc.Location.file source) then
F.fprintf fmt "%a\n" pp_cfgnode node in
IList.iter print_node (Cfg.Node.get_all_nodes cfg)
let write_icfg_dotty_to_file cfg fname =
let write_icfg_dotty_to_file source cfg fname =
let chan = open_out fname in
let fmt = Format.formatter_of_out_channel chan in
(* avoid phabricator thinking this file was generated by substituting substring with %s *)
F.fprintf fmt "/* @@%s */@\ndigraph iCFG {@\n" "generated";
print_icfg fmt cfg;
print_icfg source fmt cfg;
F.fprintf fmt "}\n";
close_out chan
let print_icfg_dotty cfg =
let print_icfg_dotty source cfg =
let fname =
if Config.frontend_tests
then
(DB.source_file_to_string !DB.current_source) ^ ".test.dot"
(DB.source_file_to_string source) ^ ".test.dot"
else
DB.filename_to_string
(DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [Config.dotty_output]) in
write_icfg_dotty_to_file cfg fname
(DB.Results_dir.path_to_filename
(DB.Results_dir.Abs_source_dir source)
[Config.dotty_output]) in
write_icfg_dotty_to_file source cfg fname
(********** END of Printing dotty files ***********)

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

@ -34,7 +34,7 @@ val pp_proplist_parsed2dotty_file : string -> Prop.normal Prop.t list -> unit
(** {2 Contol-Flow Graph} *)
(** Print the cfg *)
val print_icfg_dotty : Cfg.cfg -> unit
val print_icfg_dotty : DB.source_file -> Cfg.cfg -> unit
(** {2 Specs} *)
val reset_dotty_spec_counter : unit -> unit

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

@ -1143,5 +1143,5 @@ let explain_null_test_after_dereference tenv exp node line loc =
(** Print a warning to the err stream at the given location (note: only prints in developer mode) *)
let warning_err loc fmt_string =
L.err ("%s:%d: Warning: " ^^ fmt_string)
(DB.source_file_to_string !DB.current_source) loc.Location.line
L.err ("%a: Warning: " ^^ fmt_string)
Location.pp loc

4
infer/src/backend/errlog.ml
Unescape View File

@ -109,11 +109,11 @@ let pp_warnings fmt (errlog : t) =
ErrLogHash.iter f errlog
(** Print an error log in html format *)
let pp_html path_to_root fmt (errlog: t) =
let pp_html source path_to_root fmt (errlog: t) =
let pp_eds fmt eds =
let pp_nodeid_session_loc
fmt ((nodeid, _), session, loc, _, _, _, _) =
Io_infer.Html.pp_session_link path_to_root fmt (nodeid, session, loc.Location.line) in
Io_infer.Html.pp_session_link source path_to_root fmt (nodeid, session, loc.Location.line) in
ErrDataSet.iter (pp_nodeid_session_loc fmt) eds in
let f do_fp ek (ekind, infp, err_name, desc, _) eds =
if ekind == ek && do_fp == infp

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

@ -51,7 +51,7 @@ val pp_errors : Format.formatter -> t -> unit
val pp_warnings : Format.formatter -> t -> unit
(** Print an error log in html format *)
val pp_html : DB.Results_dir.path -> Format.formatter -> t -> unit
val pp_html : DB.source_file -> DB.Results_dir.path -> Format.formatter -> t -> unit
(** Return the number of elements in the error log which satisfy the filter. *)
val size : (Exceptions.err_kind -> bool -> bool) -> t -> int

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

@ -62,7 +62,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 ();
{ cg = Cg.create None;
proc_map = Procname.Hash.create 17;
source_files = DB.SourceFileSet.empty;
}
@ -184,7 +184,6 @@ let iter_files f exe_env =
then seen_files_acc
else
begin
DB.current_source := fname;
Config.nLOC := file_data.nLOC;
Option.may (fun cfg -> f fname cfg) (file_data_to_cfg file_data);
DB.SourceFileSet.add fname seen_files_acc

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

@ -334,17 +334,17 @@ let reset_prop_metrics () =
exception RE_EXE_ERROR
let do_before_node session node =
let do_before_node source session node =
let loc = Cfg.Node.get_loc node in
let proc_desc = Cfg.Node.get_proc_desc node in
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
State.set_node node;
State.set_session session;
L.reset_delayed_prints ();
Printer.node_start_session node loc proc_name (session :> int)
Printer.node_start_session node loc proc_name (session :> int) source
let do_after_node node =
Printer.node_finish_session node
let do_after_node source node =
Printer.node_finish_session node source
(** Return the list of normal ids occurring in the instructions *)
let instrs_get_normal_vars instrs =
@ -494,7 +494,7 @@ let mark_visited summary node =
else
stats.Specs.nodes_visited_re <- IntSet.add (node_id :> int) stats.Specs.nodes_visited_re
let forward_tabulate tenv wl =
let forward_tabulate tenv wl source =
let handled_some_exception = ref false in
let handle_exn curr_node exn =
let curr_pdesc = Cfg.Node.get_proc_desc curr_node in
@ -524,7 +524,7 @@ let forward_tabulate tenv wl =
let session =
incr summary.Specs.sessions;
!(summary.Specs.sessions) in
do_before_node session curr_node;
do_before_node source session curr_node;
let pathset_todo = path_set_checkout_todo wl curr_node in
let succ_nodes = Cfg.Node.get_succs curr_node in
let exn_nodes = Cfg.Node.get_exn curr_node in
@ -605,13 +605,13 @@ let forward_tabulate tenv wl =
begin
doit();
if !handled_some_exception then Printer.force_delayed_prints ();
do_after_node curr_node
do_after_node source curr_node
end
with
| exn when Exceptions.handle_exception exn ->
handle_exn curr_node exn;
Printer.force_delayed_prints ();
do_after_node curr_node;
do_after_node source curr_node;
if not !Config.footprint then raise RE_EXE_ERROR
done;
L.d_strln ".... Work list empty. Stop ...."; L.d_ln ()
@ -915,10 +915,10 @@ let initial_prop_from_pre tenv curr_f pre =
initial_prop tenv curr_f pre false
(** Re-execute one precondition and return some spec if there was no re-execution error. *)
let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Specs.Jprop.t)
let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Specs.Jprop.t) source
: Prop.normal Specs.spec option =
let proc_name = Cfg.Procdesc.get_proc_name pdesc in
do_before_node 0 init_node;
do_before_node source 0 init_node;
L.d_strln ("#### Start: RE-execution for " ^ Procname.to_string proc_name ^ " ####");
L.d_indent 1;
L.d_strln "Precond:"; Specs.Jprop.d_shallow precondition;
@ -930,13 +930,14 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
init_prop
(Paths.Path.start init_node)
Paths.PathSet.empty in
do_after_node init_node;
do_after_node source init_node;
try
Worklist.add wl init_node;
ignore (path_set_put_todo wl init_node init_edgeset);
forward_tabulate tenv wl;
do_before_node 0 init_node;
L.d_strln_color Green ("#### Finished: RE-execution for " ^ Procname.to_string proc_name ^ " ####");
forward_tabulate tenv wl source;
do_before_node source 0 init_node;
L.d_strln_color Green
("#### Finished: RE-execution for " ^ Procname.to_string proc_name ^ " ####");
L.d_increase_indent 1;
L.d_strln "Precond:"; Prop.d_prop (Specs.Jprop.to_prop precondition);
L.d_ln ();
@ -954,10 +955,10 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
| Specs.Jprop.Joined (n, _, jp1, jp2) -> Specs.Jprop.Joined (n, p, jp1, jp2) in
let spec = { Specs.pre = pre; Specs.posts = posts; Specs.visited = visited } in
L.d_decrease_indent 1;
do_after_node init_node;
do_after_node source init_node;
Some spec
with RE_EXE_ERROR ->
do_before_node 0 init_node;
do_before_node source 0 init_node;
Printer.force_delayed_prints ();
L.d_strln_color Red ("#### [FUNCTION " ^ Procname.to_string proc_name ^ "] ...ERROR");
L.d_increase_indent 1;
@ -965,7 +966,7 @@ let execute_filter_prop wl tenv pdesc init_node (precondition : Prop.normal Spec
Prop.d_prop (Specs.Jprop.to_prop precondition);
L.d_strln "This precondition is filtered out.";
L.d_decrease_indent 1;
do_after_node init_node;
do_after_node source init_node;
None
(** get all the nodes in the current call graph with their defined children *)
@ -992,7 +993,7 @@ let pp_intra_stats wl proc_desc fmt _ =
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 : Cfg.Procdesc.t)
let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t) source
: (unit -> unit) * (unit -> Prop.normal Specs.spec list * Specs.phase) =
let start_node = Cfg.Procdesc.get_start_node pdesc in
@ -1032,7 +1033,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
(Cfg.Procdesc.get_flags pdesc)
Mleak_buckets.objc_arc_flag;
ignore (path_set_put_todo wl start_node init_edgeset);
forward_tabulate tenv wl in
forward_tabulate tenv wl source in
let get_results (wl : Worklist.t) () =
State.process_execution_failures Reporting.log_warning pname;
let results = collect_analysis_result tenv wl pdesc in
@ -1067,7 +1068,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
check_recursion_level ();
let filter p =
let wl = path_set_create_worklist pdesc in
let speco = execute_filter_prop wl tenv pdesc start_node p in
let speco = execute_filter_prop wl tenv pdesc start_node p source in
let is_valid = match speco with
| None -> false
| Some spec ->
@ -1091,7 +1092,7 @@ let perform_analysis_phase tenv (pname : Procname.t) (pdesc : Cfg.Procdesc.t)
IList.map (fun spec -> spec.Specs.pre) specs in
let filename =
DB.Results_dir.path_to_filename
DB.Results_dir.Abs_source_dir
(DB.Results_dir.Abs_source_dir source)
[(Procname.to_filename proc_name)] in
if Config.write_dotty then
Dotty.pp_speclist_dotty_file filename specs;
@ -1322,12 +1323,12 @@ let update_summary tenv prev_summary specs phase proc_name elapsed res =
(** Analyze the procedure and return the resulting summary. *)
let analyze_proc exe_env proc_desc : Specs.summary =
let analyze_proc source exe_env proc_desc : Specs.summary =
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
let init_time = Unix.gettimeofday () in
let tenv = Exe_env.get_tenv exe_env proc_name in
reset_global_values proc_desc;
let go, get_results = perform_analysis_phase tenv proc_name proc_desc in
let go, get_results = perform_analysis_phase tenv proc_name proc_desc source in
let res = Timeout.exe_timeout go () in
let specs, phase = get_results () in
let elapsed = Unix.gettimeofday () -. init_time in
@ -1373,7 +1374,7 @@ let transition_footprint_re_exe tenv proc_name joined_pres =
(** Perform phase transition from [FOOTPRINT] to [RE_EXECUTION] for
the procedures enabled after the analysis of [proc_name] *)
let perform_transition exe_env tenv proc_name =
let perform_transition exe_env tenv proc_name source =
let transition () =
(* disable exceptions for leaks and protect against any other errors *)
let joined_pres =
@ -1387,15 +1388,15 @@ let perform_transition exe_env tenv proc_name =
f start_node
| None -> ()
with exn when SymOp.exn_not_failure exn -> () in
apply_start_node (do_before_node 0);
apply_start_node (do_before_node source 0);
try
Config.allow_leak := true;
let res = collect_preconditions tenv proc_name in
Config.allow_leak := allow_leak;
apply_start_node do_after_node;
apply_start_node (do_after_node source);
res
with exn when SymOp.exn_not_failure exn ->
apply_start_node do_after_node;
apply_start_node (do_after_node source);
Config.allow_leak := allow_leak;
L.err "Error in collect_preconditions for %a@." Procname.pp proc_name;
let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in
@ -1475,7 +1476,7 @@ let do_analysis exe_env =
let callbacks =
let get_proc_desc proc_name =
Exe_env.get_proc_desc exe_env proc_name in
let analyze_ondemand proc_desc =
let analyze_ondemand source proc_desc =
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
let tenv = Exe_env.get_tenv exe_env proc_name in
if not (Config.eradicate || Config.checkers)
@ -1484,13 +1485,13 @@ let do_analysis exe_env =
the preanalysis inserts. *)
Preanal.doit proc_desc (Exe_env.get_cg exe_env) tenv;
let summaryfp =
Config.run_in_footprint_mode (analyze_proc exe_env) proc_desc in
Config.run_in_footprint_mode (analyze_proc source exe_env) proc_desc in
Specs.add_summary proc_name summaryfp;
perform_transition exe_env tenv proc_name;
perform_transition exe_env tenv proc_name source;
let summaryre =
Config.run_in_re_execution_mode (analyze_proc exe_env) proc_desc in
Config.run_in_re_execution_mode (analyze_proc source exe_env) proc_desc in
Specs.add_summary proc_name summaryre in
{
Ondemand.analyze_ondemand;
@ -1522,7 +1523,7 @@ let visited_and_total_nodes cfg =
(** Print the stats for the given cfg.
Consider every defined proc unless a proc with the same name
was defined in another module, and was the one which was analyzed *)
let print_stats_cfg proc_shadowed cfg =
let print_stats_cfg proc_shadowed source cfg =
let err_table = Errlog.create_err_table () in
let nvisited, ntotal = visited_and_total_nodes cfg in
let node_filter n =
@ -1572,7 +1573,7 @@ let print_stats_cfg proc_shadowed cfg =
F.fprintf fmt "TOTAL: %a@\n" (pp_seq pp_node) nodes_total; *)
F.fprintf fmt "@\n++++++++++++++++++++++++++++++++++++++++++++++++++@\n";
F.fprintf fmt "+ FILE: %s LOC: %n VISITED: %d/%d SYMOPS: %d@\n"
(DB.source_file_to_string !DB.current_source)
(DB.source_file_to_string source)
!Config.nLOC
(IList.length nodes_visited)
(IList.length nodes_total)
@ -1591,7 +1592,7 @@ let print_stats_cfg proc_shadowed cfg =
F.fprintf fmt "++++++++++++++++++++++++++++++++++++++++++++++++++@\n";
Errlog.print_err_table_details fmt err_table in
let save_file_stats () =
let source_dir = DB.source_dir_from_source_file !DB.current_source in
let source_dir = DB.source_dir_from_source_file source in
let stats_file = DB.source_dir_get_internal_file source_dir ".stats" in
try
let outc = open_out (DB.filename_to_string stats_file) in
@ -1607,10 +1608,10 @@ let print_stats_cfg proc_shadowed cfg =
let print_stats exe_env =
if Config.developer_mode then
Exe_env.iter_files
(fun fname cfg ->
(fun source cfg ->
let proc_shadowed proc_desc =
(* return true if a proc with the same name in another module was analyzed instead *)
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
Exe_env.get_source exe_env proc_name <> Some fname in
print_stats_cfg proc_shadowed cfg)
Exe_env.get_source exe_env proc_name <> Some source in
print_stats_cfg proc_shadowed source cfg)
exe_env

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

@ -126,17 +126,17 @@ struct
(fd, fmt)
(** Get the full html filename from a path *)
let get_full_fname path =
let get_full_fname source path =
let dir_path = match IList.rev path with
| fname :: path_rev ->
IList.rev ((fname ^ ".html") :: path_rev)
| [] ->
raise (Failure "Html.open_out") in
DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir dir_path
DB.Results_dir.path_to_filename (DB.Results_dir.Abs_source_dir source) dir_path
(** Open an Html file to append data *)
let open_out path =
let full_fname = get_full_fname path in
let open_out source path =
let full_fname = get_full_fname source path in
let fd =
Unix.openfile
(DB.filename_to_string full_fname)
@ -147,8 +147,8 @@ struct
(fd, fmt)
(** Return true if the html file was modified since the beginning of the analysis *)
let modified_during_analysis path =
let fname = get_full_fname path in
let modified_during_analysis source path =
let fname = get_full_fname source path in
if DB.file_exists fname then
DB.file_modified_time fname >= Config.initial_analysis_time
else false
@ -220,8 +220,8 @@ struct
pp_link ~path: (path_to_root @ [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) path_to_root fmt linenum =
let fname = DB.source_file_encoding !DB.current_source in
let pp_line_link ?(with_name = false) ?(text = None) source path_to_root fmt linenum =
let fname = DB.source_file_encoding source in
let linenum_str = string_of_int linenum in
let name = "LINE" ^ linenum_str in
pp_link
@ -232,7 +232,7 @@ struct
(match text with Some s -> s | None -> linenum_str)
(** Print an html link given node id and session *)
let pp_session_link ?(with_name = false) path_to_root fmt (node_id, session, linenum) =
let pp_session_link ?(with_name = false) source path_to_root fmt (node_id, session, linenum) =
let node_name = "node" ^ (string_of_int node_id) in
let path_to_node = path_to_root @ ["nodes"; node_name] in
let pos = "session" ^ (string_of_int session) in
@ -242,7 +242,7 @@ struct
~path: path_to_node
fmt
(node_name ^ "#" ^ pos);
F.fprintf fmt "(%a)" (pp_line_link path_to_root) linenum
F.fprintf fmt "(%a)" (pp_line_link source path_to_root) linenum
end
(* =============== END of module Html =============== *)

8
infer/src/backend/io_infer.mli
Unescape View File

@ -21,15 +21,15 @@ module Html : sig
DB.Results_dir.path_kind -> DB.Results_dir.path -> Unix.file_descr * Format.formatter
(** Return true if the html file was modified since the beginning of the analysis *)
val modified_during_analysis : DB.Results_dir.path -> bool
val modified_during_analysis : DB.source_file -> DB.Results_dir.path -> bool
(** Open an Html file to append data *)
val open_out : DB.Results_dir.path -> Unix.file_descr * Format.formatter
val open_out : DB.source_file -> DB.Results_dir.path -> Unix.file_descr * Format.formatter
(** Print an html link to the given line number of the current source file *)
val pp_line_link :
?with_name: bool -> ?text: (string option) ->
DB.Results_dir.path -> Format.formatter -> int -> unit
DB.source_file -> DB.Results_dir.path -> Format.formatter -> int -> unit
(** Print a horizontal line *)
val pp_hline : Format.formatter -> unit -> unit
@ -54,7 +54,7 @@ module Html : sig
(** Print an html link given node id and session *)
val pp_session_link :
?with_name: bool -> string list -> Format.formatter -> int * int * int -> unit
?with_name: bool -> DB.source_file -> string list -> Format.formatter -> int * int * int -> unit
(** Print start color *)
val pp_start_color : Format.formatter -> color -> unit

37
infer/src/backend/ondemand.ml
Unescape View File

@ -34,7 +34,7 @@ let read_dirs_to_analyze () =
let dirs_to_analyze =
lazy (read_dirs_to_analyze ())
type analyze_ondemand = Cfg.Procdesc.t -> unit
type analyze_ondemand = DB.source_file -> Cfg.Procdesc.t -> unit
type get_proc_desc = Procname.t -> Cfg.Procdesc.t option
@ -79,7 +79,6 @@ type global_state =
{
abs_val : int;
abstraction_rules : Abs.rules;
current_source : DB.source_file;
delayed_prints : L.print_action list;
footprint_mode : bool;
html_formatter : F.formatter;
@ -93,7 +92,6 @@ let save_global_state () =
{
abs_val = !Config.abs_val;
abstraction_rules = Abs.get_current_rules ();
current_source = !DB.current_source;
delayed_prints = L.get_delayed_prints ();
footprint_mode = !Config.footprint;
html_formatter = !Printer.curr_html_formatter;
@ -104,7 +102,6 @@ let save_global_state () =
let restore_global_state st =
Config.abs_val := st.abs_val;
Abs.set_current_rules st.abstraction_rules;
DB.current_source := st.current_source;
L.set_delayed_prints st.delayed_prints;
Config.footprint := st.footprint_mode;
Printer.curr_html_formatter := st.html_formatter;
@ -128,22 +125,24 @@ let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_
incr nesting;
let attributes_opt =
Specs.proc_resolve_attributes callee_pname in
Option.may
(fun attribute ->
DB.current_source := attribute.ProcAttributes.loc.Location.file;
let attribute_pname = attribute.ProcAttributes.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)))
attributes_opt;
let source = Option.map_default
(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));
attributes.loc.file)
DB.source_file_empty
attributes_opt in
let call_graph =
let cg = Cg.create () in
let cg = Cg.create (Some source) in
Cg.add_defined_node cg callee_pname;
cg in
Specs.reset_summary call_graph callee_pname attributes_opt;
Specs.set_status callee_pname Specs.ACTIVE in
Specs.set_status callee_pname Specs.ACTIVE;
source in
let postprocess () =
let postprocess source =
decr nesting;
let summary = Specs.get_summary_unsafe "ondemand" callee_pname in
let summary' =
@ -152,7 +151,7 @@ let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_
timestamp = summary.Specs.timestamp + 1 } in
Specs.add_summary callee_pname summary';
Checkers.ST.store_summary tenv callee_pname;
Printer.write_proc_html false callee_pdesc in
Printer.write_proc_html source false callee_pdesc in
let log_error_and_continue exn kind =
Reporting.log_error callee_pname exn;
@ -166,10 +165,10 @@ let run_proc_analysis tenv ~propagate_exceptions analyze_proc curr_pdesc callee_
Specs.add_summary callee_pname new_summary in
let old_state = save_global_state () in
preprocess ();
let source = preprocess () in
try
analyze_proc callee_pdesc;
postprocess ();
analyze_proc source callee_pdesc;
postprocess source;
restore_global_state old_state;
with exn ->
L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.CALL STACK@.%s@.BACK TRACE@.%s@."

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

@ -14,7 +14,7 @@ open! Utils
(** Optional set of source dirs to analyze in on-demand mode. *)
val dirs_to_analyze : StringSet.t option Lazy.t
type analyze_ondemand = Cfg.Procdesc.t -> unit
type analyze_ondemand = DB.source_file -> Cfg.Procdesc.t -> unit
type get_proc_desc = Procname.t -> Cfg.Procdesc.t option

69
infer/src/backend/printer.ml
Unescape View File

@ -102,31 +102,35 @@ let is_visited node =
when starting and finishing the processing of a node *)
module NodesHtml : sig
val start_node :
int -> Location.t -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list -> bool
val finish_node : int -> unit
int -> Location.t -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list ->
DB.source_file -> bool
val finish_node : int -> DB.source_file -> unit
end = struct
let log_files = Hashtbl.create 11
let id_to_fname id = "node" ^ string_of_int id
let start_node nodeid loc proc_name preds succs exn =
let start_node nodeid loc proc_name preds succs exns source =
let node_fname = id_to_fname nodeid in
let modified = Io_infer.Html.modified_during_analysis ["nodes"; node_fname] in
let modified = Io_infer.Html.modified_during_analysis source ["nodes"; node_fname] in
let needs_initialization, (fd, fmt) =
if modified then
(false, Io_infer.Html.open_out ["nodes"; node_fname])
(false, Io_infer.Html.open_out source ["nodes"; node_fname])
else
(true, Io_infer.Html.create DB.Results_dir.Abs_source_dir ["nodes"; node_fname]) in
(true,
Io_infer.Html.create
(DB.Results_dir.Abs_source_dir source)
["nodes"; node_fname]) in
curr_html_formatter := fmt;
Hashtbl.replace log_files (node_fname, !DB.current_source) fd;
Hashtbl.replace log_files (node_fname, source) fd;
if needs_initialization then
(F.fprintf fmt "<center><h1>Cfg Node %a</h1></center>"
(Io_infer.Html.pp_line_link ~text: (Some (string_of_int nodeid)) [".."])
(Io_infer.Html.pp_line_link source ~text: (Some (string_of_int nodeid)) [".."])
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))
(Io_infer.Html.pp_line_link [".."]) loc.Location.line;
(Io_infer.Html.pp_line_link source [".."]) loc.Location.line;
F.fprintf fmt "<br>PREDS:@\n";
IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] ""
@ -147,16 +151,16 @@ end = struct
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list)
(is_visited node) false fmt (Cfg.Node.get_id node :> int)) exn;
(is_visited node) false fmt (Cfg.Node.get_id node :> int)) exns;
F.fprintf fmt "<br>@\n";
F.pp_print_flush fmt ();
true
)
else false
let finish_node nodeid =
let finish_node nodeid source =
let fname = id_to_fname nodeid in
let fd = Hashtbl.find log_files (fname, !DB.current_source) in
let fd = Hashtbl.find log_files (fname, source) in
Unix.close fd;
curr_html_formatter := F.std_formatter
end
@ -360,13 +364,14 @@ let force_delayed_prints () =
Config.forcing_delayed_prints := false
(** Start a session, and create a new html fine for the node if it does not exist yet *)
let start_session node (loc: Location.t) proc_name session =
let start_session node (loc: Location.t) proc_name session source =
let node_id = Cfg.Node.get_id node in
(if NodesHtml.start_node
(node_id :> int) loc proc_name
(Cfg.Node.get_preds node)
(Cfg.Node.get_succs node)
(Cfg.Node.get_exn node)
source
then
F.fprintf !curr_html_formatter "%a<LISTING>%a</LISTING>%a"
Io_infer.Html.pp_start_color Green
@ -374,37 +379,39 @@ let start_session node (loc: Location.t) proc_name session =
Io_infer.Html.pp_end_color ());
F.fprintf !curr_html_formatter "%a%a"
Io_infer.Html.pp_hline ()
(Io_infer.Html.pp_session_link ~with_name: true [".."])
(Io_infer.Html.pp_session_link source ~with_name: true [".."])
((node_id :> int), session, loc.Location.line);
F.fprintf !curr_html_formatter "<LISTING>%a"
Io_infer.Html.pp_start_color Black
let node_start_session node loc proc_name session =
let node_start_session node loc proc_name session source =
if Config.write_html then
start_session node loc proc_name session
start_session node loc proc_name session source
(** Finish a session, and perform delayed print actions if required *)
let node_finish_session node =
let node_finish_session node source =
if Config.test == false then force_delayed_prints ()
else L.reset_delayed_prints ();
if Config.write_html then begin
F.fprintf !curr_html_formatter "</LISTING>%a"
Io_infer.Html.pp_end_color ();
NodesHtml.finish_node (Cfg.Node.get_id node :> int)
NodesHtml.finish_node (Cfg.Node.get_id node :> int) source
end
(** Write html file for the procedure.
The boolean indicates whether to print whole seconds only *)
let write_proc_html whole_seconds pdesc =
let write_proc_html source whole_seconds pdesc =
if Config.write_html then
begin
let pname = Cfg.Procdesc.get_proc_name pdesc in
let nodes = IList.sort Cfg.Node.compare (Cfg.Procdesc.get_nodes pdesc) in
let linenum = (Cfg.Node.get_loc (IList.hd nodes)).Location.line in
let fd, fmt =
Io_infer.Html.create DB.Results_dir.Abs_source_dir [Procname.to_filename pname] in
Io_infer.Html.create
(DB.Results_dir.Abs_source_dir source)
[Procname.to_filename pname] in
F.fprintf fmt "<center><h1>Procedure %a</h1></center>@\n"
(Io_infer.Html.pp_line_link
(Io_infer.Html.pp_line_link source
~text: (Some (Escape.escape_xml (Procname.to_string pname)))
[])
linenum;
@ -421,7 +428,7 @@ let write_proc_html whole_seconds pdesc =
| None ->
()
| Some summary ->
Specs.pp_summary (pe_html Black) whole_seconds fmt summary;
Specs.pp_summary_html source Black ~whole_seconds fmt summary;
Io_infer.Html.close (fd, fmt))
end
@ -445,7 +452,7 @@ let create_table_err_per_line err_log =
let create_err_message err_string =
"\n<div class=\"msg\" style=\"margin-left:9ex\">" ^ err_string ^ "</div>"
let write_html_proc proof_cover table_nodes_at_linenum global_err_log proc_desc =
let write_html_proc source proof_cover table_nodes_at_linenum global_err_log proc_desc =
let proc_name = Cfg.Procdesc.get_proc_name proc_desc in
let process_node nodes_tbl n =
let lnum = (Cfg.Node.get_loc n).Location.line in
@ -456,7 +463,7 @@ let write_html_proc proof_cover table_nodes_at_linenum global_err_log proc_desc
let proc_loc = Cfg.Procdesc.get_loc proc_desc in
let process_proc =
Cfg.Procdesc.is_defined proc_desc &&
DB.source_file_equal proc_loc.Location.file !DB.current_source &&
DB.source_file_equal proc_loc.Location.file source &&
match AttributesTable.find_file_capturing_procedure proc_name with
| None -> true
| Some (source_captured, _) ->
@ -477,19 +484,21 @@ let write_html_proc proof_cover table_nodes_at_linenum global_err_log proc_desc
(** Create filename.ext.html. *)
let write_html_file linereader filename procs =
DB.current_source := filename;
let fname_encoding = DB.source_file_encoding filename in
let (fd, fmt) = Io_infer.Html.create DB.Results_dir.Abs_source_dir [".."; fname_encoding] in
let (fd, fmt) =
Io_infer.Html.create
(DB.Results_dir.Abs_source_dir filename)
[".."; fname_encoding] in
let pp_prelude () =
let s =
"<center><h1>File " ^
(DB.source_file_to_string !DB.current_source) ^
(DB.source_file_to_string filename) ^
"</h1></center>\n" ^
"<table class=\"code\">\n" in
F.fprintf fmt "%s" s in
let print_one_line proof_cover table_nodes_at_linenum table_err_per_line line_number =
let line_html =
match LineReader.from_file_linenum linereader !DB.current_source line_number with
match LineReader.from_file_linenum linereader filename line_number with
| Some line_raw ->
Escape.escape_xml line_raw
| None ->
@ -552,7 +561,7 @@ let write_html_file linereader filename procs =
let global_err_log = Errlog.empty () in
let table_nodes_at_linenum = Hashtbl.create 11 in
let proof_cover = ref Specs.Visitedset.empty in
IList.iter (write_html_proc proof_cover table_nodes_at_linenum global_err_log) procs;
IList.iter (write_html_proc filename proof_cover table_nodes_at_linenum global_err_log) procs;
let table_err_per_line = create_table_err_per_line global_err_log in
let linenum = ref 0 in
@ -563,7 +572,7 @@ let write_html_file linereader filename procs =
done
with End_of_file ->
(F.fprintf fmt "%s" "</table>\n";
Errlog.pp_html [fname_encoding] fmt global_err_log;
Errlog.pp_html filename [fname_encoding] fmt global_err_log;
Io_infer.Html.close (fd, fmt))
(** Create filename.ext.html for each file in the exe_env. *)

6
infer/src/backend/printer.mli
Unescape View File

@ -37,17 +37,17 @@ val curr_html_formatter : Format.formatter ref
val force_delayed_prints : unit -> unit
(** Finish a session, and perform delayed print actions if required *)
val node_finish_session : Cfg.node -> unit
val node_finish_session : Cfg.node -> DB.source_file -> unit
(** Return true if the node was visited during footprint and during re-execution *)
val node_is_visited : Cfg.Node.t -> bool * bool
(** Start a session, and create a new html fine for the node if it does not exist yet *)
val node_start_session : Cfg.node -> Location.t -> Procname.t -> int -> unit
val node_start_session : Cfg.node -> Location.t -> Procname.t -> int -> DB.source_file -> unit
(** Write html file for the procedure.
The boolean indicates whether to print whole seconds only. *)
val write_proc_html : bool -> Cfg.Procdesc.t -> unit
val write_proc_html : DB.source_file -> bool -> Cfg.Procdesc.t -> unit
val write_html_file : LineReader.t -> DB.source_file -> Cfg.Procdesc.t list -> unit

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

@ -749,7 +749,10 @@ let check_atom tenv prop a0 =
if Config.smt_output then begin
let key = get_smt_key a prop_no_fp in
let key_filename =
DB.Results_dir.path_to_filename DB.Results_dir.Abs_source_dir [(key ^ ".cns")] in
let source = (State.get_loc ()).file in
DB.Results_dir.path_to_filename
(DB.Results_dir.Abs_source_dir source)
[(key ^ ".cns")] in
let outc = open_out (DB.filename_to_string key_filename) in
let fmt = F.formatter_of_out_channel outc in
L.d_str ("ID: "^key); L.d_ln ();

64
infer/src/backend/specs.ml
Unescape View File

@ -446,38 +446,36 @@ let get_specs_from_payload summary =
| Some specs -> NormSpec.tospecs specs
| None -> []
(** Print the summary *)
let pp_summary pe whole_seconds fmt summary =
let pp_summary_text ~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_errlog err_log;
F.fprintf fmt "%a@\n" (pp_stats 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 ();
F.fprintf fmt "<br />%a<br />@\n" (pp_stats whole_seconds) summary.stats;
Errlog.pp_html [] fmt err_log;
Io_infer.Html.pp_hline fmt ();
F.fprintf fmt "<LISTING>@\n";
pp_specs pe fmt (get_specs_from_payload summary);
F.fprintf fmt "</LISTING>@\n"
| PP_LATEX ->
F.fprintf fmt "\\begin{verbatim}@\n";
pp_summary_no_stats_specs fmt summary;
F.fprintf fmt "%a@\n" pp_errlog err_log;
F.fprintf fmt "%a@\n" (pp_stats whole_seconds) summary.stats;
F.fprintf fmt "\\end{verbatim}@\n";
F.fprintf fmt "%a@\n" (pp_specs pe) (get_specs_from_payload summary)
(** Print the spec table *)
let pp_spec_table pe whole_seconds fmt () =
Procname.Hash.iter (fun proc_name (summ, _) ->
F.fprintf fmt "PROC %a@\n%a@\n" Procname.pp proc_name (pp_summary pe whole_seconds) summ
) spec_tbl
let pe = pe_text in
pp_summary_no_stats_specs fmt summary;
F.fprintf fmt "%a@\n" pp_errlog err_log;
F.fprintf fmt "%a@\n" (pp_stats whole_seconds) summary.stats;
F.fprintf fmt "%a" (pp_specs pe) (get_specs_from_payload summary)
let pp_summary_latex ~whole_seconds color fmt summary =
let err_log = summary.attributes.ProcAttributes.err_log in
let pe = pe_latex color in
F.fprintf fmt "\\begin{verbatim}@\n";
pp_summary_no_stats_specs fmt summary;
F.fprintf fmt "%a@\n" pp_errlog err_log;
F.fprintf fmt "%a@\n" (pp_stats whole_seconds) summary.stats;
F.fprintf fmt "\\end{verbatim}@\n";
F.fprintf fmt "%a@\n" (pp_specs pe) (get_specs_from_payload summary)
let pp_summary_html ~whole_seconds source color fmt summary =
let err_log = summary.attributes.ProcAttributes.err_log in
let pe = pe_html color in
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 ();
F.fprintf fmt "<br />%a<br />@\n" (pp_stats whole_seconds) summary.stats;
Errlog.pp_html source [] fmt err_log;
Io_infer.Html.pp_hline fmt ();
F.fprintf fmt "<LISTING>@\n";
pp_specs pe fmt (get_specs_from_payload summary);
F.fprintf fmt "</LISTING>@\n"
let empty_stats calls in_out_calls_opt =
{ stats_time = 0.0;
@ -509,7 +507,9 @@ let set_summary_origin proc_name summary origin =
Procname.Hash.replace spec_tbl proc_name (summary, origin)
let add_summary_origin (proc_name : Procname.t) (summary: summary) (origin: DB.origin) : unit =
L.out "Adding summary for %a@\n@[<v 2> %a@]@." Procname.pp proc_name (pp_summary pe_text false) summary;
L.out "Adding summary for %a@\n@[<v 2> %a@]@."
Procname.pp proc_name
(pp_summary_text ~whole_seconds:false) summary;
set_summary_origin proc_name summary origin
(** Add the summary to the table for the given function *)

14
infer/src/backend/specs.mli
Unescape View File

@ -234,14 +234,18 @@ val normalized_specs_to_specs : NormSpec.t list -> Prop.normal spec list
(** Print the spec *)
val pp_spec : printenv -> (int * int) option -> Format.formatter -> Prop.normal spec -> unit
(** Print the spec table, the bool indicates whether to print whole seconds only *)
val pp_spec_table : printenv -> bool -> Format.formatter -> unit -> unit
(** Print the specs *)
val pp_specs : printenv -> Format.formatter -> Prop.normal spec list -> unit
(** Print the summary, the bool indicates whether to print whole seconds only *)
val pp_summary : printenv -> bool -> Format.formatter -> summary -> unit
(** Print the summary in html format *)
val pp_summary_html :
whole_seconds:bool -> DB.source_file -> color -> Format.formatter -> summary -> unit
(** Print the summary in latext format *)
val pp_summary_latex : whole_seconds:bool -> color -> Format.formatter -> summary -> unit
(** Print the summary in text format *)
val pp_summary_text : whole_seconds:bool -> Format.formatter -> summary -> unit
(** Like proc_resolve_attributes but start from a proc_desc. *)
val pdesc_resolve_attributes : Cfg.Procdesc.t -> ProcAttributes.t

4
infer/src/checkers/abstractInterpreter.ml
Unescape View File

@ -120,7 +120,7 @@ module MakeNoCFG
let checker { Callbacks.get_proc_desc; proc_desc; proc_name; tenv; } extras =
let post_opt = ref None in
let analyze_ondemand pdesc =
let analyze_ondemand _source pdesc =
match compute_post (ProcData.make pdesc tenv extras) with
| Some post ->
Summ.write_summary (Cfg.Procdesc.get_proc_name pdesc) post;
@ -136,7 +136,7 @@ module MakeNoCFG
then
begin
Ondemand.set_callbacks callbacks;
analyze_ondemand proc_desc;
analyze_ondemand DB.source_file_empty proc_desc;
Ondemand.unset_callbacks ();
end;
!post_opt

18
infer/src/clang/cFrontend.ml
Unescape View File

@ -20,12 +20,12 @@ and CFrontend_declImpl : CFrontend_decl.CFrontend_decl =
CFrontend_decl.CFrontend_decl_funct(CTransImpl)
(* Translates a file by translating the ast into a cfg. *)
let compute_icfg tenv ast =
let compute_icfg source tenv ast =
match ast with
| Clang_ast_t.TranslationUnitDecl(_, decl_list, _, _) ->
CFrontend_config.global_translation_unit_decls := decl_list;
Printing.log_out "\n Start creating icfg\n";
let cg = Cg.create () in
let cg = Cg.create (Some source) in
let cfg = Cfg.Node.create_cfg () in
if Config.clang_frontend_do_capture then
IList.iter (CFrontend_declImpl.translate_one_declaration tenv cg cfg `DeclTraversal)
@ -45,8 +45,8 @@ let register_perf_stats_report source_file =
let init_global_state source_file =
register_perf_stats_report source_file ;
Config.curr_language := Config.Clang;
DB.current_source := source_file;
DB.Results_dir.init ();
CFrontend_config.current_source := source_file;
DB.Results_dir.init source_file;
Ident.NameGenerator.reset ();
CFrontend_config.global_translation_unit_decls := [];
CFrontend_utils.General_utils.reset_block_counter ()
@ -58,7 +58,7 @@ let do_source_file source_file ast =
Config.nLOC := FileLOC.file_get_loc (DB.source_file_to_string source_file);
Printing.log_out "\n Start building call/cfg graph for '%s'....\n"
(DB.source_file_to_string source_file);
let call_graph, cfg = compute_icfg tenv ast in
let call_graph, cfg = compute_icfg source_file tenv ast in
Printing.log_out "\n End building call/cfg graph for '%s'.\n"
(DB.source_file_to_string source_file);
(* TODO (t12740727): Move this call to cMain once the transition to linters mode is finished *)
@ -66,12 +66,12 @@ let do_source_file source_file ast =
CFrontend_checkers_main.do_frontend_checks cfg call_graph source_file ast;
(* This part below is a boilerplate in every frontends. *)
(* This could be moved in the cfg_infer module *)
let source_dir = DB.source_dir_from_source_file !DB.current_source in
let source_dir = DB.source_dir_from_source_file source_file in
let tenv_file = DB.source_dir_get_internal_file source_dir ".tenv" in
let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in
Cg.store_to_file cg_file call_graph;
Cfg.store_cfg_to_file ~source_file:!DB.current_source cfg_file cfg;
Cfg.store_cfg_to_file ~source_file cfg_file cfg;
(*Logging.out "Tenv %a@." Sil.pp_tenv tenv;*)
(* Printing.print_tenv tenv; *)
(*Printing.print_procedures cfg; *)
@ -82,5 +82,5 @@ let do_source_file source_file ast =
|| Config.debug_mode
|| Config.testing_mode
|| Config.frontend_tests then
(Dotty.print_icfg_dotty cfg;
Cg.save_call_graph_dotty None Specs.get_specs call_graph)
(Dotty.print_icfg_dotty source_file cfg;
Cg.save_call_graph_dotty source_file Specs.get_specs call_graph)

1
infer/src/clang/cFrontend_config.ml
Unescape View File

@ -78,6 +78,7 @@ let modeled_function_attributes = [replace_with_deref_first_arg_attr]
(** Global state *)
let current_source = ref DB.source_file_empty
let enum_map = ref Clang_ast_main.PointerMap.empty
let global_translation_unit_decls : Clang_ast_t.decl list ref = ref []
let ivar_to_property_index = ref Clang_ast_main.PointerMap.empty

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

@ -79,6 +79,8 @@ val modeled_function_attributes : string list
(** Global state *)
val current_source : DB.source_file ref
(** Map from enum constants pointers to their predecesor and their sil value *)
val enum_map : (Clang_ast_t.pointer option * Exp.t option) Clang_ast_main.PointerMap.t ref
val global_translation_unit_decls : Clang_ast_t.decl list ref

9
infer/src/clang/cLocation.ml
Unescape View File

@ -38,7 +38,8 @@ let choose_sloc sloc1 sloc2 =
let choose_sloc_to_update_curr_file sloc1 sloc2 =
match sloc2.Clang_ast_t.sl_file with
| Some f when DB.source_file_equal (source_file_from_path f) !DB.current_source -> sloc2
| Some f when DB.source_file_equal (source_file_from_path f) !CFrontend_config.current_source ->
sloc2
| _ -> sloc1
let update_curr_file di =
@ -67,7 +68,7 @@ let clang_to_sil_location clang_loc procdesc_opt =
| Some f ->
let file_db = source_file_from_path f in
let nloc =
if (DB.source_file_equal file_db !DB.current_source) then
if (DB.source_file_equal file_db !CFrontend_config.current_source) then
!Config.nLOC
else -1 in
file_db, nloc
@ -90,7 +91,7 @@ let should_do_frontend_check (loc_start, _) =
match loc_start.Clang_ast_t.sl_file with
| Some file ->
let equal_current_source file =
DB.source_file_equal (source_file_from_path file) !DB.current_source in
DB.source_file_equal (source_file_from_path file) !CFrontend_config.current_source in
equal_current_source file ||
(file_in_project file && not Config.testing_mode)
| None -> false
@ -112,7 +113,7 @@ let should_translate (loc_start, loc_end) decl_trans_context ~translate_when_use
map_path_of path_pred loc
in
let equal_current_source file =
DB.source_file_equal file !DB.current_source
DB.source_file_equal file !CFrontend_config.current_source
in
let file_in_project = map_path_of file_in_project loc_end
|| map_path_of file_in_project loc_start in

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

@ -279,8 +279,8 @@ struct
let initializers_current_class =
pname_and_pdescs_with
(function (pname, proc_attributes) ->
is_initializer proc_attributes &&
get_class pname = get_class curr_pname) in
is_initializer proc_attributes &&
get_class pname = get_class curr_pname) in
final_typestates
((curr_pname, curr_pdesc) :: initializers_current_class)
end
@ -405,7 +405,7 @@ let callback_eradicate
check_ret_type = [];
} in
let callbacks =
let analyze_ondemand pdesc =
let analyze_ondemand _ pdesc =
let idenv_pname = Idenv.create_from_idenv idenv pdesc in
Main.callback checks
{ callback_args with

34
infer/src/java/jContext.ml
Unescape View File

@ -40,38 +40,30 @@ type t =
goto_jumps : (int, jump_kind) Hashtbl.t;
cn : JBasics.class_name;
meth_kind : meth_kind;
node : JCode.jcode Javalib.interface_or_class;
source_file : DB.source_file;
program : JClasspath.program;
}
let create_context icfg procdesc impl cn meth_kind node program =
{ icfg = icfg;
procdesc = procdesc;
impl = impl;
let create_context icfg procdesc impl cn meth_kind source_file program =
{ icfg;
procdesc;
impl;
var_map = JBir.VarMap.empty;
if_jumps = NodeTbl.create 10;
goto_jumps = Hashtbl.create 10;
cn = cn;
meth_kind = meth_kind;
node = node;
program = program;
cn;
meth_kind;
source_file;
program;
}
let get_icfg context = context.icfg
let get_cfg context = context.icfg.cfg
let get_cg context = context.icfg.cg
let get_tenv context = context.icfg.tenv
let get_procdesc context = context.procdesc
let get_cn context = context.cn
let get_node context = context.node
let get_program context = context.program
let get_impl context = context.impl
let get_var_map context = context.var_map
let set_var_map context var_map = context.var_map <- var_map
let get_meth_kind context = context.meth_kind
let get_or_set_pvar_type context var typ =
let var_map = get_var_map context in
let var_map = context.var_map in
try
let (pvar, otyp, _) = (JBir.VarMap.find var var_map) in
let tenv = get_tenv context in
@ -81,7 +73,7 @@ let get_or_set_pvar_type context var typ =
else set_var_map context (JBir.VarMap.add var (pvar, typ, typ) var_map);
(pvar, typ)
with Not_found ->
let procname = (Cfg.Procdesc.get_proc_name (get_procdesc context)) in
let procname = (Cfg.Procdesc.get_proc_name context.procdesc) in
let varname = Mangled.from_string (JBir.var_name_g var) in
let pvar = Pvar.mk varname procname in
set_var_map context (JBir.VarMap.add var (pvar, typ, typ) var_map);
@ -90,7 +82,7 @@ let get_or_set_pvar_type context var typ =
let set_pvar context var typ = fst (get_or_set_pvar_type context var typ)
let reset_pvar_type context =
let var_map = get_var_map context in
let var_map = context.var_map in
let aux var item =
match item with (pvar, otyp, _) ->
set_var_map context (JBir.VarMap.add var (pvar, otyp, otyp) var_map) in
@ -98,7 +90,7 @@ let reset_pvar_type context =
let get_var_type context var =
try
let (_, _, otyp) = JBir.VarMap.find var (get_var_map context) in
let (_, _, otyp) = JBir.VarMap.find var context.var_map in
Some otyp
with Not_found -> None

38
infer/src/java/jContext.mli
Unescape View File

@ -40,7 +40,18 @@ type icfg = {
}
(** data structure for storing the context elements. *)
type t
type t = private
{ icfg : icfg;
procdesc : Cfg.Procdesc.t;
impl : JBir.t;
mutable var_map : (Pvar.t * Typ.t * Typ.t) JBir.VarMap.t;
if_jumps : int NodeTbl.t;
goto_jumps : (int, jump_kind) Hashtbl.t;
cn : JBasics.class_name;
meth_kind : meth_kind;
source_file : DB.source_file;
program : JClasspath.program;
}
(** cretes a context for a given method. *)
@ -50,19 +61,10 @@ val create_context :
JBir.t ->
JBasics.class_name ->
meth_kind ->
JCode.jcode Javalib.interface_or_class ->
DB.source_file ->
JClasspath.program ->
t
(** returns the intermediate representation of the Java file from the context. *)
val get_icfg : t -> icfg
(** returns the code of the method from the context *)
val get_impl : t -> JBir.t
(** returns the class where the method is defined from the context *)
val get_cn : t -> JBasics.class_name
(** returns the type environment that corresponds to the current file. *)
val get_tenv : t -> Tenv.t
@ -72,14 +74,6 @@ val get_cg : t -> Cg.t
(** returns the control flow graph that corresponds to the current file. *)
val get_cfg : t -> Cfg.cfg
(** returns the procedure description in the intermediate language for the
current method. *)
val get_procdesc : t -> Cfg.Procdesc.t
(** returns the method kind of the current method: standard or initialiser of
static fields. *)
val get_meth_kind : t -> meth_kind
(** adds to the context the line that an if-node will jump to *)
val add_if_jump : t -> Cfg.Node.t -> int -> unit
@ -96,12 +90,6 @@ val get_goto_jump : t -> int -> jump_kind
(** returns whether the given line corresponds to a goto instruction. *)
val is_goto_jump : t -> int -> bool
(** returns the Java program *)
val get_program : t -> JClasspath.program
(** returns the current node *)
val get_node : t -> JCode.jcode Javalib.interface_or_class
(** [set_pvar context var type] adds a variable with a type to the context *)
val set_pvar : t -> JBir.var -> Typ.t -> Pvar.t

27
infer/src/java/jFrontend.ml
Unescape View File

@ -16,8 +16,9 @@ open Sawja_pack
module L = Logging
let add_edges context start_node exn_node exit_nodes method_body_nodes impl super_call =
let cfg = (JContext.get_icfg context).cfg in
let add_edges
(context : JContext.t) start_node exn_node exit_nodes method_body_nodes impl super_call =
let cfg = context.icfg.cfg in
let pc_nb = Array.length method_body_nodes in
let last_pc = pc_nb - 1 in
let is_last pc = (pc = last_pc) in
@ -73,7 +74,7 @@ let add_edges context start_node exn_node exit_nodes method_body_nodes impl supe
Array.iteri connect_nodes method_body_nodes
(** Add a concrete method. *)
let add_cmethod program icfg node cm is_static =
let add_cmethod source_file program icfg node cm is_static =
let cfg = icfg.JContext.cfg in
let tenv = icfg.JContext.tenv in
let cn, ms = JBasics.cms_split cm.Javalib.cm_class_method_signature in
@ -101,7 +102,7 @@ let add_cmethod program icfg node cm is_static =
(instrs, JContext.Init)
else (JBir.code impl), JContext.Normal in
let context =
JContext.create_context icfg procdesc impl cn meth_kind node program in
JContext.create_context icfg procdesc impl cn meth_kind source_file program in
let method_body_nodes = Array.mapi (JTrans.instruction context) instrs in
let procname = Cfg.Procdesc.get_proc_name procdesc in
add_edges context start_node exn_node [exit_node] method_body_nodes impl false;
@ -157,20 +158,20 @@ let is_classname_cached cn =
(* Given a source file and a class, translates the code of this class.
In init - mode, finds out whether this class contains initializers at all,
in this case translates it. In standard mode, all methods are translated *)
let create_icfg linereader program icfg cn node =
let create_icfg source_file linereader program icfg cn node =
JUtils.log "\tclassname: %s@." (JBasics.cn_name cn);
cache_classname cn;
let cfg = icfg.JContext.cfg in
let tenv = icfg.JContext.tenv in
begin
Javalib.m_iter (JTrans.create_local_procdesc program linereader cfg tenv node) node;
Javalib.m_iter (JTrans.create_local_procdesc source_file program linereader cfg tenv node) node;
Javalib.m_iter (fun m ->
(* each procedure has different scope: start names from id 0 *)
Ident.NameGenerator.reset ();
let method_kind = JTransType.get_method_kind m in
match m with
| Javalib.ConcreteMethod cm ->
add_cmethod program icfg node cm method_kind
add_cmethod source_file program icfg node cm method_kind
| Javalib.AbstractMethod am ->
add_amethod program icfg am method_kind
) node
@ -213,9 +214,9 @@ let should_capture classes package_opt source_basename node =
source file. *)
let compute_source_icfg
linereader classes program tenv
source_basename package_opt =
source_basename package_opt source_file =
let icfg =
{ JContext.cg = Cg.create ();
{ JContext.cg = Cg.create (Some source_file);
JContext.cfg = Cfg.Node.create_cfg ();
JContext.tenv = tenv } in
let select test procedure cn node =
@ -229,18 +230,18 @@ let compute_source_icfg
JBasics.ClassMap.iter
(select
(should_capture classes package_opt source_basename)
(create_icfg linereader program icfg))
(create_icfg source_file linereader program icfg))
(JClasspath.get_classmap program) in
(icfg.JContext.cg, icfg.JContext.cfg)
let compute_class_icfg linereader program tenv node =
let compute_class_icfg source_file linereader program tenv node =
let icfg =
{ JContext.cg = Cg.create ();
{ JContext.cg = Cg.create (Some source_file);
JContext.cfg = Cfg.Node.create_cfg ();
JContext.tenv = tenv } in
begin
try
create_icfg linereader program icfg (Javalib.get_name node) node
create_icfg source_file linereader program icfg (Javalib.get_name node) node
with
| Bir.Subroutine -> ()
| e -> raise e

2
infer/src/java/jFrontend.mli
Unescape View File

@ -29,10 +29,12 @@ val compute_source_icfg :
Tenv.t ->
string ->
string option ->
DB.source_file ->
Cg.t * Cfg.cfg
(** Compute the CFG for a class *)
val compute_class_icfg :
DB.source_file ->
Printer.LineReader.t ->
JClasspath.program ->
Tenv.t ->

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

@ -34,26 +34,25 @@ let register_perf_stats_report source_file =
let init_global_state source_file =
register_perf_stats_report source_file ;
Config.curr_language := Config.Java;
DB.current_source := source_file;
DB.Results_dir.init ();
DB.Results_dir.init source_file;
Ident.NameGenerator.reset ();
JContext.reset_exn_node_table ();
let nLOC = FileLOC.file_get_loc (DB.source_file_to_string source_file) in
Config.nLOC := nLOC
let store_icfg tenv cg cfg =
let source_dir = DB.source_dir_from_source_file !DB.current_source in
let store_icfg source_file tenv cg cfg =
let source_dir = DB.source_dir_from_source_file source_file in
begin
let cfg_file = DB.source_dir_get_internal_file source_dir ".cfg" in
let cg_file = DB.source_dir_get_internal_file source_dir ".cg" in
if Config.create_harness then Harness.create_harness cfg cg tenv;
Cg.store_to_file cg_file cg;
Cfg.store_cfg_to_file ~source_file:!DB.current_source cfg_file cfg;
Cfg.store_cfg_to_file ~source_file cfg_file cfg;
if Config.debug_mode || Config.frontend_tests then
begin
Dotty.print_icfg_dotty cfg;
Cg.save_call_graph_dotty None Specs.get_specs cg
Dotty.print_icfg_dotty source_file cfg;
Cg.save_call_graph_dotty source_file Specs.get_specs cg
end
end
@ -62,14 +61,14 @@ let store_icfg tenv cg cfg =
(* environment are obtained and saved. *)
let do_source_file
linereader classes program tenv
source_basename (package_opt, source_file) =
source_basename package_opt source_file =
JUtils.log "\nfilename: %s (%s)@."
(DB.source_file_to_string source_file) source_basename;
let call_graph, cfg =
JFrontend.compute_source_icfg
linereader classes program tenv
source_basename package_opt in
store_icfg tenv call_graph cfg
source_basename package_opt source_file in
store_icfg source_file tenv call_graph cfg
let capture_libs linereader program tenv =
@ -83,8 +82,8 @@ let capture_libs linereader program tenv =
JClasspath.java_source_file_from_path (JFrontend.path_of_cached_classname cn) in
init_global_state fake_source_file;
let call_graph, cfg =
JFrontend.compute_class_icfg linereader program tenv node in
store_icfg tenv call_graph cfg;
JFrontend.compute_class_icfg fake_source_file linereader program tenv node in
store_icfg fake_source_file tenv call_graph cfg;
JFrontend.cache_classname cn;
end in
JBasics.ClassMap.iter (capture_class tenv) (JClasspath.get_classmap program)
@ -131,7 +130,7 @@ let do_all_files classpath sources classes =
let translate_source_file basename (package_opt, _) source_file =
init_global_state source_file;
if not (skip source_file) then
do_source_file linereader classes program tenv basename (package_opt, source_file) in
do_source_file linereader classes program tenv basename package_opt source_file in
StringMap.iter
(fun basename file_entry ->
match file_entry with

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

@ -53,7 +53,7 @@ let fix_method_definition_line linereader proc_name_java loc =
{ loc with Location.line = !line }
with Not_found -> loc
let get_location impl pc meth_kind cn =
let get_location source_file impl pc meth_kind cn =
if meth_kind = JContext.Init then
try
JBasics.ClassMap.find cn !init_loc_map
@ -68,7 +68,7 @@ let get_location impl pc meth_kind cn =
| Some n -> n in
{ Location.line = line_number;
col = -1;
file = !DB.current_source;
file = source_file;
nLOC = !Config.nLOC }
let get_undefined_method_call ovt =
@ -255,7 +255,7 @@ let update_init_loc cn ms loc_start =
with Not_found -> init_loc_map := (JBasics.ClassMap.add cn loc_start !init_loc_map)
(** Creates a procedure description. *)
let create_local_procdesc program linereader cfg tenv node m =
let create_local_procdesc source_file program linereader cfg tenv node m =
let cn, ms = JBasics.cms_split (Javalib.get_class_method_signature m) in
let meth_kind =
if JBasics.ms_equal ms JBasics.clinit_signature then JContext.Init
@ -320,9 +320,11 @@ let create_local_procdesc program linereader cfg tenv node m =
let impl = get_implementation cm in
let locals, formals = locals_formals program tenv cn impl meth_kind in
let loc_start =
let loc = (get_location impl 0 JContext.Normal cn) in
let loc = (get_location source_file impl 0 JContext.Normal cn) in
fix_method_definition_line linereader proc_name_java loc in
let loc_exit = (get_location impl (Array.length (JBir.code impl) - 1) JContext.Normal cn) in
let loc_exit =
get_location
source_file impl (Array.length (JBir.code impl) - 1) JContext.Normal cn in
let method_annotation =
JAnnotation.translate_method proc_name_java cm.Javalib.cm_annotations in
update_constr_loc cn ms loc_start;
@ -393,8 +395,8 @@ let rec get_method_procdesc program cfg tenv cn ms kind =
get_method_procdesc program cfg tenv cn ms kind
| Created status -> status
let use_static_final_fields context =
(not Config.no_static_final) && (JContext.get_meth_kind context) <> JContext.Init
let use_static_final_fields (context : JContext.t) =
(not Config.no_static_final) && context.meth_kind <> JContext.Init
let builtin_new =
Exp.Const (Const.Cfun ModelBuiltins.__new)
@ -407,11 +409,17 @@ let create_sil_deref exp typ loc =
Sil.Load (no_id, exp, typ, loc)
(** translate an expression used as an r-value *)
let rec expression context pc expr =
let rec expression (context : JContext.t) pc expr =
(* JUtils.log "\t\t\t\texpr: %s@." (JBir.print_expr expr); *)
let cn = (JContext.get_cn context) in
let program = JContext.get_program context in
let loc = get_location (JContext.get_impl context) pc (JContext.get_meth_kind context) cn in
let cn = context.cn in
let program = context.program in
let loc =
get_location
context.source_file
context.impl
pc
context.meth_kind
cn in
let tenv = JContext.get_tenv context in
let type_of_expr = JTransType.expr_type context expr in
let trans_var pvar =
@ -427,7 +435,7 @@ let rec expression context pc expr =
match c with (* We use the constant <field> internally to mean a variable. *)
| `String s when (JBasics.jstr_pp s) = JConfig.field_cst ->
let varname = JConfig.field_st in
let procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
let procname = (Cfg.Procdesc.get_proc_name context.procdesc) in
let pvar = Pvar.mk varname procname in
trans_var pvar
| _ -> ([], Exp.Const (get_constant c), type_of_expr)
@ -531,13 +539,14 @@ let rec expression context pc expr =
let lderef_instr = Sil.Load (tmp_id, sil_expr, sil_type, loc) in
(instrs @ [lderef_instr], Exp.Var tmp_id, type_of_expr)
let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_code method_kind =
let method_invocation
(context : JContext.t) loc pc var_opt cn ms sil_obj_opt expr_list invoke_code method_kind =
(* This function tries to recursively search for the classname of the class *)
(* where the method is defined. It returns the classname given as argument*)
(* when this classname cannot be found *)
let resolve_method context cn ms =
let resolve_method (context : JContext.t) cn ms =
let rec loop fallback_cn cn =
match JClasspath.lookup_node cn (JContext.get_program context) with
match JClasspath.lookup_node cn context.program with
| None -> fallback_cn
| Some node ->
if Javalib.defines_method node ms then cn
@ -553,7 +562,7 @@ let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_
loop cn cn in
let cn' = resolve_method context cn ms in
let tenv = JContext.get_tenv context in
let program = JContext.get_program context in
let program = context.program in
let cf_virtual, cf_interface = match invoke_code with
| I_Virtual -> (true, false)
| I_Interface -> (true, true)
@ -688,7 +697,7 @@ type translation =
(* TODO: unclear if this corresponds to what JControlFlow.resolve_method'*)
(* is trying to do. Normally, this implementation below goes deeper into *)
(* the type hierarchy and it is not clear why we should not do that *)
let extends context node1 node2 =
let extends (context : JContext.t) node1 node2 =
let is_matching cn =
JBasics.cn_equal cn (Javalib.get_name node2) in
let rec check cn_list =
@ -697,7 +706,7 @@ let extends context node1 node2 =
iterate cn_list
and iterate cn_list =
let per_classname cn =
match JClasspath.lookup_node cn (JContext.get_program context) with
match JClasspath.lookup_node cn context.program with
| None -> false (* TODO: should capture the class instead of returning false *)
| Some node ->
let super_cn_list =
@ -729,14 +738,14 @@ let instruction_array_call ms obj_type obj args var_opt =
(* special translation of the method start() of a Thread or a Runnable object.
We translate it directly as the run() method *)
let instruction_thread_start context cn ms obj args var_opt =
match JClasspath.lookup_node cn (JContext.get_program context) with
let instruction_thread_start (context : JContext.t) cn ms obj args var_opt =
match JClasspath.lookup_node cn context.program with
| None ->
let () = JUtils.log "\t\t\tWARNING: %s should normally be found@." (JBasics.cn_name cn) in
None
| Some node ->
begin
match JClasspath.lookup_node (JBasics.make_cn JConfig.thread_class) (JContext.get_program context) with
match JClasspath.lookup_node (JBasics.make_cn JConfig.thread_class) context.program with
| None -> None (* TODO: should load the class instead of returning None *)
| Some thread_node ->
if ((JBasics.ms_name ms) = JConfig.start_method) && (extends context node thread_node) then
@ -765,25 +774,26 @@ let assume_not_null loc sil_expr =
let call_args = [(not_null_expr, Typ.Tint Typ.IBool)] in
Sil.Call ([], builtin_infer_assume, call_args, loc, assume_call_flag)
let rec instruction context pc instr : translation =
let rec instruction (context : JContext.t) pc instr : translation =
let cfg = JContext.get_cfg context in
let tenv = JContext.get_tenv context in
let cg = JContext.get_cg context in
let cn = JContext.get_cn context in
let program = JContext.get_program context in
let meth_kind = JContext.get_meth_kind context in
let proc_name = Cfg.Procdesc.get_proc_name (JContext.get_procdesc context) in
let cn = context.cn in
let program = context.program in
let meth_kind = context.meth_kind in
let proc_name = Cfg.Procdesc.get_proc_name context.procdesc in
let ret_var = Pvar.get_ret_pvar proc_name in
let ret_type = Cfg.Procdesc.get_ret_type (JContext.get_procdesc context) in
let loc = get_location (JContext.get_impl context) pc meth_kind cn in
let ret_type = Cfg.Procdesc.get_ret_type context.procdesc in
let loc =
get_location context.source_file context.impl pc meth_kind cn in
let match_never_null = Inferconfig.never_return_null_matcher in
let create_node node_kind sil_instrs =
Cfg.Node.create
cfg
(get_location (JContext.get_impl context) pc meth_kind cn)
(get_location context.source_file context.impl pc meth_kind cn)
node_kind
sil_instrs
(JContext.get_procdesc context) in
context.procdesc in
let return_not_null () =
match_never_null loc.Location.file proc_name
||
@ -882,7 +892,7 @@ let rec instruction context pc instr : translation =
and prune_node_false =
create_node node_kind_false (instrs1 @ instrs2 @ [sil_instrs_false]) in
JContext.add_if_jump context prune_node_false if_pc;
if detect_loop pc (JContext.get_impl context) then
if detect_loop pc context.impl then
let join_node_kind = Cfg.Node.Join_node in
let join_node = create_node join_node_kind [] in
Loop (join_node, prune_node_true, prune_node_false)
@ -913,7 +923,7 @@ let rec instruction context pc instr : translation =
let instrs = (new_instr :: call_instrs) @ [set_instr] in
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string constr_procname)) in
let node = create_node node_kind instrs in
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
let caller_procname = (Cfg.Procdesc.get_proc_name context.procdesc) in
Cg.add_edge cg caller_procname constr_procname;
Instr node
| JBir.NewArray (var, vt, expr_list) ->
@ -942,11 +952,11 @@ let rec instruction context pc instr : translation =
method_invocation context loc pc var_opt cn ms sil_obj_opt args I_Static Procname.Static in
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
let call_node = create_node node_kind (instrs @ call_instrs) in
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
let caller_procname = (Cfg.Procdesc.get_proc_name context.procdesc) in
Cg.add_edge cg caller_procname callee_procname;
Instr call_node
| JBir.InvokeVirtual (var_opt, obj, call_kind, ms, args) ->
let caller_procname = (Cfg.Procdesc.get_proc_name (JContext.get_procdesc context)) in
let caller_procname = (Cfg.Procdesc.get_proc_name context.procdesc) in
let (instrs, sil_obj_expr, sil_obj_type) = expression context pc obj in
let create_call_node cn invoke_kind =
let callee_procname, call_instrs =
@ -985,7 +995,7 @@ let rec instruction context pc instr : translation =
method_invocation context loc pc var_opt cn ms (Some (sil_obj_expr, sil_obj_type)) args I_Special Procname.Non_Static in
let node_kind = Cfg.Node.Stmt_node ("Call "^(Procname.to_string callee_procname)) in
let call_node = create_node node_kind (instrs @ call_instrs) in
let procdesc = (JContext.get_procdesc context) in
let procdesc = context.procdesc in
let caller_procname = (Cfg.Procdesc.get_proc_name procdesc) in
Cg.add_edge cg caller_procname callee_procname;
Instr call_node

2
infer/src/java/jTrans.mli
Unescape View File

@ -31,7 +31,7 @@ val get_method_procdesc : JClasspath.program -> Cfg.cfg -> Tenv.t -> JBasics.cla
(** [create_local_procdesc linereader cfg tenv program m] creates a procedure description for the method m and adds it to cfg *)
val create_local_procdesc :
JClasspath.program -> Printer.LineReader.t -> Cfg.cfg -> Tenv.t ->
DB.source_file -> JClasspath.program -> Printer.LineReader.t -> Cfg.cfg -> Tenv.t ->
JCode.jcode Javalib.interface_or_class -> JCode.jcode Javalib.jmethod -> unit
(** returns the implementation of a given method *)

7
infer/src/java/jTransExn.ml
Unescape View File

@ -26,10 +26,10 @@ let create_handler_table impl =
IList.iter collect (JBir.exception_edges impl);
handler_tb
let translate_exceptions context exit_nodes get_body_nodes handler_table =
let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handler_table =
let catch_block_table = Hashtbl.create 1 in
let exn_message = "exception handler" in
let procdesc = JContext.get_procdesc context in
let procdesc = context.procdesc in
let cfg = JContext.get_cfg context in
let create_node loc node_kind instrs = Cfg.Node.create cfg loc node_kind instrs procdesc in
let ret_var = Cfg.Procdesc.get_ret_var procdesc in
@ -62,7 +62,8 @@ let translate_exceptions context exit_nodes get_body_nodes handler_table =
match handler.JBir.e_catch_type with
| None -> JBasics.make_cn "java.lang.Exception"
| Some cn -> cn in
match JTransType.get_class_type (JContext.get_program context) (JContext.get_tenv context) class_name with
match JTransType.get_class_type
context.program (JContext.get_tenv context) class_name with
| Typ.Tptr (typ, _) -> typ
| _ -> assert false in
let id_instanceof = Ident.create_fresh Ident.knormal in

8
infer/src/java/jTransStaticField.ml
Unescape View File

@ -179,9 +179,9 @@ let static_field_init node cn code =
with Not_found -> code
(* when accessing a static final field, we call the initialiser method. *)
let translate_instr_static_field context callee_procdesc fs field_type loc =
let translate_instr_static_field (context : JContext.t) callee_procdesc fs field_type loc =
let cg = JContext.get_cg context in
let caller_procdesc = JContext.get_procdesc context in
let caller_procdesc = context.procdesc in
let ret_id = Ident.create_fresh Ident.knormal in
let caller_procname = (Cfg.Procdesc.get_proc_name caller_procdesc) in
let callee_procname = Cfg.Procdesc.get_proc_name callee_procdesc in
@ -193,8 +193,8 @@ let translate_instr_static_field context callee_procdesc fs field_type loc =
([call_instr], Exp.Var ret_id)
let is_static_final_field context cn fs =
match JClasspath.lookup_node cn (JContext.get_program context) with
let is_static_final_field (context : JContext.t) cn fs =
match JClasspath.lookup_node cn context.program with
| None -> false
| Some node ->
try

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

@ -376,15 +376,15 @@ let param_type program tenv cn name vt =
else value_type program tenv vt
let get_var_type_from_sig context var =
let program = JContext.get_program context in
let get_var_type_from_sig (context : JContext.t) var =
let program = context.program in
try
let tenv = JContext.get_tenv context in
let vt', var' =
IList.find
(fun (_, var') -> JBir.var_equal var var')
(JBir.params (JContext.get_impl context)) in
Some (param_type program tenv (JContext.get_cn context) var' vt')
(JBir.params context.impl) in
Some (param_type program tenv context.cn var' vt')
with Not_found -> None
@ -403,8 +403,8 @@ let extract_array_type typ =
(** translate the type of an expression, looking in the method signature for formal parameters
this is because variables in expressions do not have accurate types *)
let rec expr_type context expr =
let program = JContext.get_program context in
let rec expr_type (context : JContext.t) expr =
let program = context.program in
let tenv = JContext.get_tenv context in
match expr with
| JBir.Const const -> value_type program tenv (const_type const)

43
infer/src/llvm/lMain.ml
Unescape View File

@ -17,30 +17,24 @@ let register_perf_stats_report source_file =
DB.create_dir stats_dir ;
PerfStats.register_report_at_exit (Filename.concat stats_dir stats_file)
let init_global_state source_filename =
let init_global_state source_file =
Config.curr_language := Config.Clang;
begin match Config.project_root with
| None -> DB.current_source := DB.abs_source_file_from_path source_filename
| Some project_root ->
DB.current_source := DB.rel_source_file_from_abs_path project_root
(filename_to_absolute source_filename)
end;
register_perf_stats_report !DB.current_source ;
DB.Results_dir.init ();
register_perf_stats_report source_file;
DB.Results_dir.init source_file;
Ident.NameGenerator.reset ();
Config.nLOC := FileLOC.file_get_loc source_filename
Config.nLOC := FileLOC.file_get_loc (DB.source_file_to_string source_file)
let store_icfg cg cfg =
let source_dir = DB.source_dir_from_source_file !DB.current_source in
let store_icfg source_file cg cfg =
let source_dir = DB.source_dir_from_source_file source_file in
let get_internal_file = DB.source_dir_get_internal_file source_dir in
let cg_file = get_internal_file ".cg" in
let cfg_file = get_internal_file ".cfg" in
Cg.store_to_file cg_file cg;
Cfg.store_cfg_to_file ~source_file:!DB.current_source cfg_file cfg;
Cfg.store_cfg_to_file ~source_file cfg_file cfg;
if Config.debug_mode || Config.frontend_tests then
begin
Dotty.print_icfg_dotty cfg;
Cg.save_call_graph_dotty None Specs.get_specs cg
Dotty.print_icfg_dotty source_file cfg;
Cg.save_call_graph_dotty source_file Specs.get_specs cg
end
let store_tenv tenv =
@ -48,12 +42,19 @@ let store_tenv tenv =
Tenv.store_to_file DB.global_tenv_fname tenv
let () =
begin match Config.source_file with
| None -> Config.print_usage_exit ()
| Some source_filename -> init_global_state source_filename
end;
let source_file = match Config.source_file with
| None ->
Config.print_usage_exit ()
| Some source_file ->
begin match Config.project_root with
| None ->
DB.abs_source_file_from_path source_file
| Some project_root ->
DB.rel_source_file_from_abs_path project_root (filename_to_absolute source_file)
end in
init_global_state source_file;
let lexbuf = Lexing.from_channel stdin in
let prog = LParser.program LLexer.token lexbuf in
let (cfg, cg, tenv) = LTrans.trans_program prog in
store_icfg cg cfg;
let (cfg, cg, tenv) = LTrans.trans_program source_file prog in
store_icfg source_file cg cfg;
store_tenv tenv

35
infer/src/llvm/lTrans.ml
Unescape View File

@ -15,8 +15,8 @@ exception ImproperTypeError of string
exception MalformedMetadata of string
exception Unimplemented of string
let source_only_location () : Location.t =
let open Location in { line = -1; col = -1; file = !DB.current_source; nLOC = !Config.nLOC }
let source_only_location source_file : Location.t =
let open Location in { line = -1; col = -1; file = source_file; nLOC = !Config.nLOC }
let ident_of_variable (var : LAst.variable) : Ident.t = (* TODO: use unique stamps *)
Ident.create_normal (Ident.string_to_name (LAst.string_of_variable var)) 0
@ -41,17 +41,17 @@ let rec trans_typ : LAst.typ -> Typ.t = function
| Tlabel -> raise (ImproperTypeError "Tried to generate Sil type from LLVM label type.")
| Tmetadata -> raise (ImproperTypeError "Tried to generate Sil type from LLVM metadata type.")
let location_of_annotation_option (metadata : LAst.metadata_map)
let location_of_annotation_option source_file (metadata : LAst.metadata_map)
: LAst.annotation option -> Location.t = function
| None -> source_only_location () (* no source line/column numbers *)
| None -> source_only_location source_file (* no source line/column numbers *)
| Some (Annotation i) ->
begin match MetadataMap.find i metadata with
| Components (TypOperand (_, Const (Cint line_num)) :: _) ->
let open Location in
{ line = line_num; col = -1; file = !DB.current_source; nLOC = !Config.nLOC }
{ line = line_num; col = -1; file = source_file; nLOC = !Config.nLOC }
| Location loc ->
let open Location in
{ line = loc.line; col = loc.col; file = !DB.current_source; nLOC = !Config.nLOC }
{ line = loc.line; col = loc.col; file = source_file; nLOC = !Config.nLOC }
| _ -> raise (MalformedMetadata ("Instruction annotation refers to metadata node " ^
"without line number as first component."))
end
@ -61,12 +61,13 @@ let procname_of_function_variable (func_var : LAst.variable) : Procname.t =
(* Generate list of SIL instructions and list of local variables *)
let rec trans_annotated_instructions
source_file
(cfg : Cfg.cfg) (procdesc : Cfg.Procdesc.t) (metadata : LAst.metadata_map)
: LAst.annotated_instruction list -> Sil.instr list * (Mangled.t * Typ.t) list = function
| [] -> ([], [])
| (instr, anno) :: t ->
let (sil_instrs, locals) = trans_annotated_instructions cfg procdesc metadata t in
let location = location_of_annotation_option metadata anno in
let (sil_instrs, locals) = trans_annotated_instructions source_file cfg procdesc metadata t in
let location = location_of_annotation_option source_file metadata anno in
begin match instr with
| Ret None -> (sil_instrs, locals)
| Ret (Some (tp, exp)) ->
@ -116,7 +117,7 @@ let callees_of_function_def : LAst.function_def -> Procname.t list = function
annotated_instrs)
(* Update CFG and call graph with new function definition *)
let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map)
let trans_function_def source_file (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map)
(func_def : LAst.function_def) : unit =
(* each procedure has different scope: start names from id 0 *)
@ -134,15 +135,17 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map)
ProcAttributes.formals =
IList.map (fun (tp, name) -> (Mangled.from_string name, trans_typ tp)) params;
is_defined = true; (* is defined and not just declared *)
loc = source_only_location ();
loc = source_only_location source_file;
locals = []; (* TODO *)
ret_type;
} in
let procdesc = Cfg.Procdesc.create cfg proc_attrs in
let start_kind = Cfg.Node.Start_node procdesc in
let start_node = Cfg.Node.create cfg (source_only_location ()) start_kind [] procdesc in
let start_node =
Cfg.Node.create cfg (source_only_location source_file) start_kind [] procdesc in
let exit_kind = Cfg.Node.Exit_node procdesc in
let exit_node = Cfg.Node.create cfg (source_only_location ()) exit_kind [] procdesc in
let exit_node =
Cfg.Node.create cfg (source_only_location source_file) exit_kind [] procdesc in
let node_of_sil_instr cfg procdesc sil_instr =
Cfg.Node.create cfg (Sil.instr_get_loc sil_instr) (Cfg.Node.Stmt_node "method_body")
[sil_instr] procdesc in
@ -153,7 +156,7 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map)
| nd :: nds ->
Cfg.Node.set_succs_exn cfg start_node [nd] [exit_node]; link_nodes nd nds in
let (sil_instrs, locals) =
trans_annotated_instructions cfg procdesc metadata annotated_instrs in
trans_annotated_instructions source_file cfg procdesc metadata annotated_instrs in
let nodes = IList.map (node_of_sil_instr cfg procdesc) sil_instrs in
Cfg.Procdesc.set_start_node procdesc start_node;
Cfg.Procdesc.set_exit_node procdesc exit_node;
@ -162,10 +165,10 @@ let trans_function_def (cfg : Cfg.cfg) (cg: Cg.t) (metadata : LAst.metadata_map)
Cg.add_defined_node cg proc_name;
IList.iter (Cg.add_edge cg proc_name) (callees_of_function_def func_def)
let trans_program : LAst.program -> Cfg.cfg * Cg.t * Tenv.t = function
let trans_program source_file : LAst.program -> Cfg.cfg * Cg.t * Tenv.t = function
Program (func_defs, metadata) ->
let cfg = Cfg.Node.create_cfg () in
let cg = Cg.create () in
let cg = Cg.create (Some source_file) in
let tenv = Tenv.create () in
IList.iter (trans_function_def cfg cg metadata) func_defs;
IList.iter (trans_function_def source_file cfg cg metadata) func_defs;
(cfg, cg, tenv)

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

@ -410,10 +410,10 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
AccessPath.BaseMap.fold add_formal_summaries formal_map []
|> add_return_summaries
let dummy_cg = Cg.create ()
let dummy_cg = Cg.create None
let checker { Callbacks.get_proc_desc; proc_name; proc_desc; tenv; } =
let analyze_ondemand pdesc =
let analyze_ondemand _ pdesc =
let make_formal_access_paths pdesc =
let pname = Cfg.Procdesc.get_proc_name pdesc in
let attrs = Cfg.Procdesc.get_attributes pdesc in
@ -445,7 +445,7 @@ module Make (TraceDomain : QuandarySummary.Trace) = struct
begin
Preanal.doit proc_desc dummy_cg tenv;
Ondemand.set_callbacks callbacks;
analyze_ondemand proc_desc;
analyze_ondemand DB.source_file_empty proc_desc;
Ondemand.unset_callbacks ();
end

Write Preview
Loading…
Cancel
Save