diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 8dd40cf09..2604dcbe8 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -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) diff --git a/infer/src/IR/Cg.re b/infer/src/IR/Cg.re index dcd1efcf8..8ba75cbf3 100644 --- a/infer/src/IR/Cg.re +++ b/infer/src/IR/Cg.re @@ -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; diff --git a/infer/src/IR/Cg.rei b/infer/src/IR/Cg.rei index 84f494ca2..d4106faf8 100644 --- a/infer/src/IR/Cg.rei +++ b/infer/src/IR/Cg.rei @@ -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 */ diff --git a/infer/src/backend/DB.ml b/infer/src/backend/DB.ml index 9af438f45..c174d9cab 100644 --- a/infer/src/backend/DB.ml +++ b/infer/src/backend/DB.ml @@ -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 *) diff --git a/infer/src/backend/DB.mli b/infer/src/backend/DB.mli index f533e0840..081a93b6f 100644 --- a/infer/src/backend/DB.mli +++ b/infer/src/backend/DB.mli @@ -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 diff --git a/infer/src/backend/InferPrint.re b/infer/src/backend/InferPrint.re index 4f771eea2..b60e4de2f 100644 --- a/infer/src/backend/InferPrint.re +++ b/infer/src/backend/InferPrint.re @@ -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 "@[%a@]" (Specs.pp_summary (pe_latex Black) Config.whole_seconds) summary + F.fprintf + fmt "@[%a@]" (Specs.pp_summary_latex Black whole_seconds::Config.whole_seconds) summary }; let pp_summary_xml summary fname => if Config.xml_specs { diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index ff772bd9d..771f2ede7 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -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 ***********) diff --git a/infer/src/backend/dotty.mli b/infer/src/backend/dotty.mli index 1094cd4b8..502f9e880 100644 --- a/infer/src/backend/dotty.mli +++ b/infer/src/backend/dotty.mli @@ -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 diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index ff26a821a..2c84a3f24 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -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 diff --git a/infer/src/backend/errlog.ml b/infer/src/backend/errlog.ml index a3aa9bac7..b8d8a459f 100644 --- a/infer/src/backend/errlog.ml +++ b/infer/src/backend/errlog.ml @@ -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 diff --git a/infer/src/backend/errlog.mli b/infer/src/backend/errlog.mli index 6031dd780..92def2318 100644 --- a/infer/src/backend/errlog.mli +++ b/infer/src/backend/errlog.mli @@ -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 diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml index 78f5bf653..a7b27788d 100644 --- a/infer/src/backend/exe_env.ml +++ b/infer/src/backend/exe_env.ml @@ -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 diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 019643d69..772b875c1 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -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 diff --git a/infer/src/backend/io_infer.ml b/infer/src/backend/io_infer.ml index 3bc1494c1..0e4e5aeb7 100644 --- a/infer/src/backend/io_infer.ml +++ b/infer/src/backend/io_infer.ml @@ -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 =============== *) diff --git a/infer/src/backend/io_infer.mli b/infer/src/backend/io_infer.mli index 446b4c402..95a150a10 100644 --- a/infer/src/backend/io_infer.mli +++ b/infer/src/backend/io_infer.mli @@ -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 diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 5c1ea27dc..1652e7976 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -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@." diff --git a/infer/src/backend/ondemand.mli b/infer/src/backend/ondemand.mli index 6edf64d36..5edb90f20 100644 --- a/infer/src/backend/ondemand.mli +++ b/infer/src/backend/ondemand.mli @@ -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 diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 2b725d4fd..c47845cc4 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -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 "

Cfg Node %a

" - (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 "
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 "
@\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%a%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 "%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 "%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 "

Procedure %a

@\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
" ^ err_string ^ "
" -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 = "

File " ^ - (DB.source_file_to_string !DB.current_source) ^ + (DB.source_file_to_string filename) ^ "

\n" ^ "\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" "
\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. *) diff --git a/infer/src/backend/printer.mli b/infer/src/backend/printer.mli index ed444ed6b..aa6a36981 100644 --- a/infer/src/backend/printer.mli +++ b/infer/src/backend/printer.mli @@ -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 diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml index 62aca4b7a..f51bec908 100644 --- a/infer/src/backend/prover.ml +++ b/infer/src/backend/prover.ml @@ -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 (); diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index ee7bac418..e6c3cb243 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -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 "
%a
@\n" (pp_stats whole_seconds) summary.stats; - Errlog.pp_html [] fmt err_log; - Io_infer.Html.pp_hline fmt (); - F.fprintf fmt "@\n"; - pp_specs pe fmt (get_specs_from_payload summary); - F.fprintf fmt "@\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 "
%a
@\n" (pp_stats whole_seconds) summary.stats; + Errlog.pp_html source [] fmt err_log; + Io_infer.Html.pp_hline fmt (); + F.fprintf fmt "@\n"; + pp_specs pe fmt (get_specs_from_payload summary); + F.fprintf fmt "@\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@[ %a@]@." Procname.pp proc_name (pp_summary pe_text false) summary; + L.out "Adding summary for %a@\n@[ %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 *) diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index f5a8a13d5..f8971a0d1 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -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 diff --git a/infer/src/checkers/abstractInterpreter.ml b/infer/src/checkers/abstractInterpreter.ml index 9c510a740..d9b4a3045 100644 --- a/infer/src/checkers/abstractInterpreter.ml +++ b/infer/src/checkers/abstractInterpreter.ml @@ -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 diff --git a/infer/src/clang/cFrontend.ml b/infer/src/clang/cFrontend.ml index 5904f93fb..a37e3cb32 100644 --- a/infer/src/clang/cFrontend.ml +++ b/infer/src/clang/cFrontend.ml @@ -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) diff --git a/infer/src/clang/cFrontend_config.ml b/infer/src/clang/cFrontend_config.ml index af4f63227..6b68468c2 100644 --- a/infer/src/clang/cFrontend_config.ml +++ b/infer/src/clang/cFrontend_config.ml @@ -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 diff --git a/infer/src/clang/cFrontend_config.mli b/infer/src/clang/cFrontend_config.mli index 5d3cd72f8..d0df06dc6 100644 --- a/infer/src/clang/cFrontend_config.mli +++ b/infer/src/clang/cFrontend_config.mli @@ -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 diff --git a/infer/src/clang/cLocation.ml b/infer/src/clang/cLocation.ml index e0f694b42..c7799d191 100644 --- a/infer/src/clang/cLocation.ml +++ b/infer/src/clang/cLocation.ml @@ -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 diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index 276ea024b..109bc9e71 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -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 diff --git a/infer/src/java/jContext.ml b/infer/src/java/jContext.ml index 658e03b63..7003d21de 100644 --- a/infer/src/java/jContext.ml +++ b/infer/src/java/jContext.ml @@ -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 diff --git a/infer/src/java/jContext.mli b/infer/src/java/jContext.mli index 4c8a34f2d..9def43146 100644 --- a/infer/src/java/jContext.mli +++ b/infer/src/java/jContext.mli @@ -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 diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml index 3169d6185..18a02eeb2 100644 --- a/infer/src/java/jFrontend.ml +++ b/infer/src/java/jFrontend.ml @@ -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 diff --git a/infer/src/java/jFrontend.mli b/infer/src/java/jFrontend.mli index 5c4518cc9..bc545eb16 100644 --- a/infer/src/java/jFrontend.mli +++ b/infer/src/java/jFrontend.mli @@ -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 -> diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index a13a75ae0..7bda86201 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -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 diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index fe7fb96de..9123e679f 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -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 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 diff --git a/infer/src/java/jTrans.mli b/infer/src/java/jTrans.mli index c564bd139..704e92bdb 100644 --- a/infer/src/java/jTrans.mli +++ b/infer/src/java/jTrans.mli @@ -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 *) diff --git a/infer/src/java/jTransExn.ml b/infer/src/java/jTransExn.ml index 6dc92153e..d8be17b80 100644 --- a/infer/src/java/jTransExn.ml +++ b/infer/src/java/jTransExn.ml @@ -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 diff --git a/infer/src/java/jTransStaticField.ml b/infer/src/java/jTransStaticField.ml index 4fdfbf1aa..4271e4bbf 100644 --- a/infer/src/java/jTransStaticField.ml +++ b/infer/src/java/jTransStaticField.ml @@ -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 diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index e4eb29f8a..ac5af2971 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -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) diff --git a/infer/src/llvm/lMain.ml b/infer/src/llvm/lMain.ml index 9e24e960c..e725d9e2d 100644 --- a/infer/src/llvm/lMain.ml +++ b/infer/src/llvm/lMain.ml @@ -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 diff --git a/infer/src/llvm/lTrans.ml b/infer/src/llvm/lTrans.ml index 8d9cfdb3b..934070bb0 100644 --- a/infer/src/llvm/lTrans.ml +++ b/infer/src/llvm/lTrans.ml @@ -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) diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index 733203837..7def0f929 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -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