From 93cc3266e80ad07374c3b51688ca12d5fc6b6e70 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 5 Jun 2017 08:59:08 -0700 Subject: [PATCH] [log] log to a single file with different categories and debug levels Summary: Change the API of `Logging` wrt to writing to files and to the console (see changes in logging.mli). Write only to one log file: infer-out/log. Prefix each line with the kind of warning and the PID of the process emitting it. Writing with `O_APPEND` is atomic so the file should not get garbled by concurrent writes. To get the output of a single process, find out which one interests you by looking at infer-out/log, then `grep ^[] infer-out/log`. Introduce 3 log levels for debug output and command-line options to set them for various categories individually. Change tons of `"\n"` to `"@\n"` so the `Format` module is aware of newlines without us having to look through every character of every logged string for `\n` characters. Reviewed By: mbouaziz Differential Revision: D5165317 fbshipit-source-id: 93c922f --- infer/src/IR/Cfg.re | 13 +- infer/src/IR/Cg.re | 4 +- infer/src/IR/Errlog.ml | 2 +- infer/src/IR/Io_infer.ml | 2 +- infer/src/IR/Procdesc.re | 4 +- infer/src/IR/Typ.re | 10 +- infer/src/backend/BuiltinDefn.ml | 6 +- infer/src/backend/InferAnalyze.re | 13 +- infer/src/backend/InferPrint.re | 38 +- infer/src/backend/OndemandCapture.ml | 10 +- infer/src/backend/Tasks.ml | 5 +- infer/src/backend/abs.ml | 21 +- infer/src/backend/cluster.ml | 4 +- infer/src/backend/clusterMakefile.ml | 2 +- infer/src/backend/dotty.ml | 201 ++++---- infer/src/backend/errdesc.ml | 3 +- infer/src/backend/errdesc.mli | 2 +- infer/src/backend/exe_env.ml | 4 +- infer/src/backend/infer.ml | 59 +-- infer/src/backend/inferconfig.ml | 10 +- infer/src/backend/interproc.ml | 62 +-- infer/src/backend/match.ml | 8 +- infer/src/backend/mergeCapture.ml | 16 +- infer/src/backend/ondemand.ml | 7 +- infer/src/backend/printer.ml | 8 +- infer/src/backend/prop.ml | 18 +- infer/src/backend/rearrange.ml | 2 +- infer/src/backend/specs.ml | 6 +- infer/src/backend/symExec.ml | 3 +- infer/src/backend/timeout.ml | 2 +- infer/src/base/Config.ml | 90 +++- infer/src/base/Config.mli | 8 +- infer/src/base/DB.ml | 4 +- infer/src/base/Epilogues.ml | 3 +- infer/src/base/Logging.ml | 441 +++++++++++------- infer/src/base/Logging.mli | 115 +++-- infer/src/base/Process.ml | 10 +- infer/src/base/ProcessPool.ml | 2 +- infer/src/base/ProcessPool.mli | 1 + infer/src/base/Serialization.ml | 6 +- infer/src/base/Utils.ml | 2 +- .../src/bufferoverrun/bufferOverrunChecker.ml | 90 ++-- .../src/bufferoverrun/bufferOverrunDomain.ml | 3 +- infer/src/checkers/Stacktrace.ml | 2 +- infer/src/checkers/ThreadSafety.ml | 2 +- infer/src/checkers/checkers.ml | 15 +- infer/src/checkers/constantPropagation.ml | 8 +- infer/src/checkers/dataflow.ml | 4 +- infer/src/checkers/printfArgs.ml | 2 +- infer/src/clang/ALVar.ml | 4 +- infer/src/clang/CType.ml | 11 +- infer/src/clang/Capture.re | 29 +- infer/src/clang/ClangCommand.re | 6 +- infer/src/clang/ClangWrapper.re | 10 +- infer/src/clang/ast_expressions.ml | 6 +- infer/src/clang/cArithmetic_trans.ml | 14 +- infer/src/clang/cAst_utils.ml | 10 +- infer/src/clang/cField_decl.ml | 6 +- infer/src/clang/cFrontend.ml | 10 +- infer/src/clang/cFrontend_checkers_main.ml | 29 +- infer/src/clang/cFrontend_decl.ml | 19 +- infer/src/clang/cFrontend_errors.ml | 48 +- infer/src/clang/cFrontend_errors.mli | 2 +- infer/src/clang/cIssue.ml | 14 +- infer/src/clang/cMethod_trans.ml | 4 +- infer/src/clang/cPredicates.ml | 8 +- infer/src/clang/cTL.ml | 29 +- infer/src/clang/cTrans.ml | 126 ++--- infer/src/clang/cTrans_utils.ml | 19 +- infer/src/clang/cType_to_sil_type.ml | 4 +- infer/src/clang/ctl_parser.mly | 83 ++-- infer/src/clang/ctl_parser_types.ml | 13 +- infer/src/clang/objcCategory_decl.ml | 7 +- infer/src/clang/objcInterface_decl.ml | 22 +- infer/src/clang/objcProtocol_decl.ml | 2 +- infer/src/clang/types_parser.mly | 8 +- infer/src/eradicate/AnnotatedSignature.ml | 4 +- infer/src/eradicate/eradicate.ml | 6 +- infer/src/eradicate/models.ml | 6 +- infer/src/eradicate/typeCheck.ml | 2 +- infer/src/eradicate/typeErr.ml | 4 +- infer/src/harness/inhabit.ml | 4 +- .../integration/CaptureCompilationDatabase.ml | 20 +- infer/src/integration/Clang.ml | 47 +- infer/src/integration/ClangQuotes.re | 6 +- infer/src/integration/CompilationDatabase.ml | 6 +- infer/src/integration/Javac.ml | 11 +- infer/src/integration/Maven.ml | 6 +- infer/src/java/jClasspath.ml | 4 +- infer/src/java/jFrontend.ml | 7 +- infer/src/java/jMain.ml | 11 +- infer/src/java/jTrans.ml | 6 +- infer/src/java/jTransType.ml | 5 +- infer/src/quandary/TaintAnalysis.ml | 2 +- 94 files changed, 1161 insertions(+), 892 deletions(-) diff --git a/infer/src/IR/Cfg.re b/infer/src/IR/Cfg.re index 0b1a1ff45..b8ba58b0b 100644 --- a/infer/src/IR/Cfg.re +++ b/infer/src/IR/Cfg.re @@ -109,7 +109,7 @@ let check_cfg_connectedness cfg => { let nodes = Procdesc.get_nodes pd; let broken = List.exists f::broken_node nodes; if broken { - L.out "\n ***BROKEN CFG: '%s'\n" pname + L.internal_error "@\n ***BROKEN CFG: '%s'@\n" pname } }; let pdescs = get_all_procs cfg; @@ -150,13 +150,12 @@ let save_attributes source_file cfg => { /** Inline a synthetic (access or bridge) method. */ let inline_synthetic_method ret_id etl pdesc loc_call :option Sil.instr => { let modified = ref None; - let debug = false; let found instr instr' => { modified := Some instr'; - if debug { - L.stderr "XX inline_synthetic_method found instr: %a@." (Sil.pp_instr Pp.text) instr; - L.stderr "XX inline_synthetic_method instr': %a@." (Sil.pp_instr Pp.text) instr' - } + L.(debug Analysis Verbose) + "XX inline_synthetic_method found instr: %a@." (Sil.pp_instr Pp.text) instr; + L.(debug Analysis Verbose) + "XX inline_synthetic_method instr': %a@." (Sil.pp_instr Pp.text) instr' }; let do_instr _ instr => switch (instr, ret_id, etl) { @@ -499,7 +498,7 @@ let specialize_types callee_pdesc resolved_pname args => { }; let pp_proc_signatures fmt cfg => { - F.fprintf fmt "METHOD SIGNATURES\n@."; + F.fprintf fmt "METHOD SIGNATURES@\n@."; let sorted_procs = List.sort cmp::Procdesc.compare (get_all_procs cfg); List.iter f::(fun pdesc => F.fprintf fmt "%a@." Procdesc.pp_signature pdesc) sorted_procs }; diff --git a/infer/src/IR/Cg.re b/infer/src/IR/Cg.re index 12325ffcd..e5fbc9831 100644 --- a/infer/src/IR/Cg.re +++ b/infer/src/IR/Cg.re @@ -136,7 +136,7 @@ let get_ancestors (g: t) node => { info.ancestors = Some ancestors; let size = Typ.Procname.Set.cardinal ancestors; if (size > 1000) { - L.out "%a has %d ancestors@." Typ.Procname.pp node size + L.(debug Analysis Medium) "%a has %d ancestors@." Typ.Procname.pp node size }; ancestors | Some ancestors => ancestors @@ -153,7 +153,7 @@ let get_heirs (g: t) node => { info.heirs = Some heirs; let size = Typ.Procname.Set.cardinal heirs; if (size > 1000) { - L.out "%a has %d heirs@." Typ.Procname.pp node size + L.(debug Analysis Medium) "%a has %d heirs@." Typ.Procname.pp node size }; heirs | Some heirs => heirs diff --git a/infer/src/IR/Errlog.ml b/infer/src/IR/Errlog.ml index 1b2f5afb1..c1ab49098 100644 --- a/infer/src/IR/Errlog.ml +++ b/infer/src/IR/Errlog.ml @@ -262,7 +262,7 @@ let log_issue err_kind err_log loc (node_id, node_key) session ltr ?linters_def_ | _ -> added in let print_now () = let ex_name, desc, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in - L.out "@\n%a@\n@?" + L.(debug Analysis Medium) "@\n%a@\n@?" (Exceptions.pp_err ~node_key loc err_kind ex_name desc ml_loc_opt) (); if err_kind <> Exceptions.Kerror then begin let warn_str = diff --git a/infer/src/IR/Io_infer.ml b/infer/src/IR/Io_infer.ml index be60cfa24..b91e18f84 100644 --- a/infer/src/IR/Io_infer.ml +++ b/infer/src/IR/Io_infer.ml @@ -338,7 +338,7 @@ struct and pp_forest newline indent fmt forest = List.iter ~f:(pp_node newline indent fmt) forest - let pp_prelude fmt = pp fmt "%s" "\n" + let pp_prelude fmt = pp fmt "%s" "@\n" let pp_open fmt name = pp_prelude fmt; diff --git a/infer/src/IR/Procdesc.re b/infer/src/IR/Procdesc.re index 3c70b4e12..6aad03177 100644 --- a/infer/src/IR/Procdesc.re +++ b/infer/src/IR/Procdesc.re @@ -120,7 +120,7 @@ module Node = { let get_proc_name node => switch node.pname_opt { | None => - L.out "get_proc_name: at node %d@\n" node.id; + L.internal_error "get_proc_name: at node %d@\n" node.id; assert false | Some pname => pname }; @@ -265,7 +265,7 @@ module Node = { | Start_node _ => "Start" | Join_node => "Join" }; - let pp fmt => F.fprintf fmt "%s\n%a@?" str (pp_instrs pe None sub_instrs::true) node; + let pp fmt => F.fprintf fmt "%s@\n%a@?" str (pp_instrs pe None sub_instrs::true) node; F.asprintf "%t" pp }; }; diff --git a/infer/src/IR/Typ.re b/infer/src/IR/Typ.re index 33dc69f2a..a25b0e178 100644 --- a/infer/src/IR/Typ.re +++ b/infer/src/IR/Typ.re @@ -374,7 +374,7 @@ let unsome s => fun | Some default_typ => default_typ | None => { - L.out "No default typ in %s@." s; + L.internal_error "No default typ in %s@." s; assert false }; @@ -1043,19 +1043,19 @@ module Struct = { /* change false to true to print the details of struct */ F.fprintf f - "%a \n\tfields: {%a\n\t}\n\tsupers: {%a\n\t}\n\tmethods: {%a\n\t}\n\tannots: {%a\n\t}" + "%a @\n\tfields: {%a@\n\t}@\n\tsupers: {%a@\n\t}@\n\tmethods: {%a@\n\t}@\n\tannots: {%a@\n\t}" Name.pp name ( Pp.seq ( fun f (fld, t, a) => - F.fprintf f "\n\t\t%a %a %a" (pp_full pe) t Fieldname.pp fld Annot.Item.pp a + F.fprintf f "@\n\t\t%a %a %a" (pp_full pe) t Fieldname.pp fld Annot.Item.pp a ) ) fields - (Pp.seq (fun f n => F.fprintf f "\n\t\t%a" Name.pp n)) + (Pp.seq (fun f n => F.fprintf f "@\n\t\t%a" Name.pp n)) supers - (Pp.seq (fun f m => F.fprintf f "\n\t\t%a" Procname.pp m)) + (Pp.seq (fun f m => F.fprintf f "@\n\t\t%a" Procname.pp m)) methods Annot.Item.pp annots diff --git a/infer/src/backend/BuiltinDefn.ml b/infer/src/backend/BuiltinDefn.ml index e4a1fa907..378ed97fa 100644 --- a/infer/src/backend/BuiltinDefn.ml +++ b/infer/src/backend/BuiltinDefn.ml @@ -130,13 +130,13 @@ let execute___set_array_length { Builtin.tenv; pdesc; prop_; path; ret_id; args; let execute___print_value { Builtin.tenv; pdesc; prop_; path; args; } : Builtin.ret_typ = - L.out "__print_value: "; + L.(debug Analysis Medium) "__print_value: "; let pname = Procdesc.get_proc_name pdesc in let do_arg (lexp, _) = let n_lexp, _ = check_arith_norm_exp tenv pname lexp prop_ in - L.out "%a " Exp.pp n_lexp in + L.(debug Analysis Medium) "%a " Exp.pp n_lexp in List.iter ~f:do_arg args; - L.out "@."; + L.(debug Analysis Medium) "@."; [(prop_, path)] let is_undefined_opt tenv prop n_lexp = diff --git a/infer/src/backend/InferAnalyze.re b/infer/src/backend/InferAnalyze.re index b694cd578..c8768e228 100644 --- a/infer/src/backend/InferAnalyze.re +++ b/infer/src/backend/InferAnalyze.re @@ -18,7 +18,7 @@ module F = Format; /** Create tasks to analyze an execution environment */ let analyze_exe_env_tasks cluster exe_env :Tasks.t => { - L.log_progress_file (); + L.progressbar_file (); Specs.clear_spec_tbl (); Random.self_init (); let biabduction_only = Config.equal_analyzer Config.analyzer Config.BiAbduction; @@ -62,7 +62,8 @@ let analyze_cluster_tasks cluster_num (cluster: Cluster.t) :Tasks.t => { let exe_env = Exe_env.from_cluster cluster; let defined_procs = Cg.get_defined_nodes (Exe_env.get_cg exe_env); let num_procs = List.length defined_procs; - L.out "@.Processing cluster #%d with %d procedures@." (cluster_num + 1) num_procs; + L.(debug Analysis Medium) + "@\nProcessing cluster #%d with %d procedures@." (cluster_num + 1) num_procs; analyze_exe_env_tasks cluster exe_env }; @@ -82,14 +83,14 @@ let output_json_makefile_stats clusters => { let process_cluster_cmdline fname => switch (Cluster.load_from_file (DB.filename_from_string fname)) { - | None => L.stderr "Cannot find cluster file %s@." fname + | None => L.internal_error "Cannot find cluster file %s@." fname | Some (nr, cluster) => analyze_cluster (nr - 1) cluster }; let print_legend () => { L.progress "Starting analysis...@\n"; L.progress "@\n"; - L.progress "legend:@\n"; + L.progress "legend:@."; L.progress " \"%s\" analyzing a file@\n" Config.log_analysis_file; L.progress " \"%s\" analyzing a procedure@\n" Config.log_analysis_procedure; if (Config.stats_mode || Config.debug_mode) { @@ -169,13 +170,13 @@ let main makefile => { f::(fun cl => DB.string_crc_has_extension ext::"java" (DB.source_dir_to_string cl)) all_clusters; if Config.print_active_checkers { - L.stderr "Active checkers: %a@." RegisterCheckers.pp_active_checkers () + L.result "Active checkers: %a@." RegisterCheckers.pp_active_checkers () }; print_legend (); if (Config.per_procedure_parallelism && not (is_java ())) { /* Java uses ZipLib which is incompatible with forking */ /* per-procedure parallelism */ - L.out "Per-procedure parallelism jobs: %d@." Config.jobs; + L.environment_info "Per-procedure parallelism jobs: %d@." Config.jobs; if (makefile != "") { ClusterMakefile.create_cluster_makefile [] makefile }; diff --git a/infer/src/backend/InferPrint.re b/infer/src/backend/InferPrint.re index f7071ec41..f2ba33283 100644 --- a/infer/src/backend/InferPrint.re +++ b/infer/src/backend/InferPrint.re @@ -18,7 +18,7 @@ module L = Logging; module F = Format; let print_usage_exit err_s => { - L.stderr "Load Error: %s@.@." err_s; + L.user_error "Load Error: %s@\n@." err_s; Config.print_usage_exit () }; @@ -427,7 +427,7 @@ let potential_exception_message = "potential exception at line"; module IssuesJson = { let is_first_item = ref true; let pp_json_open fmt () => F.fprintf fmt "[@?"; - let pp_json_close fmt () => F.fprintf fmt "]\n@?"; + let pp_json_close fmt () => F.fprintf fmt "]@\n@?"; /** Write bug report in JSON format */ let pp_issues_of_error_log fmt error_filter _ proc_loc_opt procname err_log => { @@ -478,7 +478,7 @@ module IssuesJson = { let potential_exception_message = Format.asprintf "%a: %s %d" MarkupFormatter.pp_bold "Note" potential_exception_message line; - Format.sprintf "%s\n%s" base_qualifier potential_exception_message + Format.sprintf "%s@\n%s" base_qualifier potential_exception_message } } else { base_qualifier @@ -795,7 +795,7 @@ module Summary = { let pp_summary_out summary => { let proc_name = Specs.get_proc_name summary; if (CLOpt.equal_command Config.command CLOpt.Report && not Config.quiet) { - L.stdout "Procedure: %a@\n%a@." Typ.Procname.pp proc_name Specs.pp_summary_text summary + L.result "Procedure: %a@\n%a@." Typ.Procname.pp proc_name Specs.pp_summary_text summary } }; @@ -869,24 +869,24 @@ module PreconditionStats = { switch (Prop.CategorizePreconditions.categorize preconditions) { | Prop.CategorizePreconditions.Empty => incr nr_empty; - L.stdout "Procedure: %a footprint:Empty@." Typ.Procname.pp proc_name + L.result "Procedure: %a footprint:Empty@." Typ.Procname.pp proc_name | Prop.CategorizePreconditions.OnlyAllocation => incr nr_onlyallocation; - L.stdout "Procedure: %a footprint:OnlyAllocation@." Typ.Procname.pp proc_name + L.result "Procedure: %a footprint:OnlyAllocation@." Typ.Procname.pp proc_name | Prop.CategorizePreconditions.NoPres => incr nr_nopres; - L.stdout "Procedure: %a footprint:NoPres@." Typ.Procname.pp proc_name + L.result "Procedure: %a footprint:NoPres@." Typ.Procname.pp proc_name | Prop.CategorizePreconditions.DataConstraints => incr nr_dataconstraints; - L.stdout "Procedure: %a footprint:DataConstraints@." Typ.Procname.pp proc_name + L.result "Procedure: %a footprint:DataConstraints@." Typ.Procname.pp proc_name } }; let pp_stats () => { - L.stdout "@.Precondition stats@."; - L.stdout "Procedures with no preconditions: %d@." !nr_nopres; - L.stdout "Procedures with empty precondition: %d@." !nr_empty; - L.stdout "Procedures with only allocation conditions: %d@." !nr_onlyallocation; - L.stdout "Procedures with data constraints: %d@." !nr_dataconstraints + L.result "@.Precondition stats@."; + L.result "Procedures with no preconditions: %d@." !nr_nopres; + L.result "Procedures with empty precondition: %d@." !nr_empty; + L.result "Procedures with only allocation conditions: %d@." !nr_onlyallocation; + L.result "Procedures with data constraints: %d@." !nr_dataconstraints }; }; @@ -1130,8 +1130,8 @@ module AnalysisResults = { let load_file fname => switch (Specs.load_summary (DB.filename_from_string fname)) { | None => - L.stderr "Error: cannot open file %s@." fname; - exit 0 + L.user_error "Error: cannot open file %s@." fname; + exit 1 | Some summary => summaries := [(fname, summary), ...!summaries] }; apply_without_gc (List.iter f::load_file) (spec_files_from_cmdline ()); @@ -1157,8 +1157,8 @@ module AnalysisResults = { let do_spec f fname => switch (Specs.load_summary (DB.filename_from_string fname)) { | None => - L.stderr "Error: cannot open file %s@." fname; - exit 0 + L.user_error "Error: cannot open file %s@." fname; + exit 1 | Some summary => f (fname, summary) }; let iterate f => List.iter f::(do_spec f) sorted_spec_files; @@ -1195,8 +1195,8 @@ module AnalysisResults = { switch (load_analysis_results_from_file (DB.filename_from_string fname)) { | Some r => iterator_of_summary_list r | None => - L.stderr "Error: cannot open analysis results file %s@." fname; - exit 0 + L.user_error "Error: cannot open analysis results file %s@." fname; + exit 1 } } }; diff --git a/infer/src/backend/OndemandCapture.ml b/infer/src/backend/OndemandCapture.ml index 2cde80942..c8e72cbc8 100644 --- a/infer/src/backend/OndemandCapture.ml +++ b/infer/src/backend/OndemandCapture.ml @@ -8,6 +8,8 @@ *) open! IStd +module L = Logging + let compilation_db = lazy (CompilationDatabase.from_json_files !Config.clang_compilation_dbs) (** Given proc_attributes try to produce proc_attributes' where proc_attributes'.is_defined = true @@ -28,7 +30,7 @@ let try_capture (attributes : ProcAttributes.t) : ProcAttributes.t option = Cfg.store_cfg_to_file *) let cfg_filename = DB.source_dir_get_internal_file source_dir ".cfg" in if not (DB.file_exists cfg_filename) then ( - Logging.out_debug "Started capture of %a...@\n" SourceFile.pp definition_file; + L.(debug Capture Verbose) "Started capture of %a...@\n" SourceFile.pp definition_file; Timeout.suspend_existing_timeout ~keep_symop_total:true; protect ~f:(fun () -> CaptureCompilationDatabase.capture_file_in_database cdb definition_file) @@ -37,13 +39,13 @@ let try_capture (attributes : ProcAttributes.t) : ProcAttributes.t option = Option.is_none (AttributesTable.load_defined_attributes ~cache_none:false attributes.proc_name) then ( (* peek at the results to know if capture succeeded, but only in debug mode *) - Logging.out_debug + L.(debug Capture Verbose) "Captured file %a to get procedure %a but it wasn't found there@\n" SourceFile.pp definition_file Typ.Procname.pp attributes.proc_name ) ) else ( - Logging.out_debug + L.(debug Capture Verbose) "Wanted to capture file %a to get procedure %a but file was already captured@\n" SourceFile.pp definition_file Typ.Procname.pp attributes.proc_name @@ -51,7 +53,7 @@ let try_capture (attributes : ProcAttributes.t) : ProcAttributes.t option = in match definition_file_opt with | None -> - Logging.out "Couldn't find source file for %a (declared in %a)@\n" + L.(debug Capture Medium) "Couldn't find source file for %a (declared in %a)@\n" Typ.Procname.pp attributes.proc_name SourceFile.pp decl_file | Some file -> try_compile file diff --git a/infer/src/backend/Tasks.ml b/infer/src/backend/Tasks.ml index 1430e3129..129001108 100644 --- a/infer/src/backend/Tasks.ml +++ b/infer/src/backend/Tasks.ml @@ -9,9 +9,10 @@ open! IStd -module L = Logging module F = Format +module L = Logging + type closure = unit -> unit type t = { @@ -61,7 +62,7 @@ module Runner = struct let pool = runner.pool in Queue.enqueue_all runner.all_continuations (Queue.to_list tasks.continuations); List.iter - ~f:(fun x -> ProcessPool.start_child ~f:(fun f -> f ()) ~pool x) + ~f:(fun x -> ProcessPool.start_child ~f:(fun f -> L.reset_formatters (); f ()) ~pool x) tasks.closures let complete runner = diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index f3eb250f3..0cb9a89bd 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -99,7 +99,9 @@ let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para: Sil.hpara) = let (para_fst_start, para_fst_rest) = let mark_impl_flag hpred = { Match.hpred = hpred; Match.flag = impl_ok1 } in match para_fst with - | [] -> L.out "@.@.ERROR (Empty Para): %a @.@." (Sil.pp_hpara Pp.text) para; assert false + | [] -> + L.internal_error "@\n@\nERROR (Empty Para): %a@\n@." (Sil.pp_hpara Pp.text) para; + assert false | hpred :: hpreds -> let hpat = mark_impl_flag hpred in let hpats = List.map ~f:mark_impl_flag hpreds in @@ -128,7 +130,9 @@ let mk_rule_ptsls_ls tenv k2 impl_ok1 impl_ok2 para = let (ids_exist, para_inst) = Sil.hpara_instantiate para exp_base exp_next exps_shared in let (para_inst_start, para_inst_rest) = match para_inst with - | [] -> L.out "@.@.ERROR (Empty Para): %a @.@." (Sil.pp_hpara Pp.text) para; assert false + | [] -> + L.internal_error "@\n@\nERROR (Empty Para): %a@\n@." (Sil.pp_hpara Pp.text) para; + assert false | hpred :: hpreds -> let allow_impl hpred = { Match.hpred = hpred; Match.flag = impl_ok1 } in (allow_impl hpred, List.map ~f:allow_impl hpreds) in @@ -252,7 +256,9 @@ let mk_rule_ptspts_dll tenv impl_ok1 impl_ok2 para = let (para_fst_start, para_fst_rest) = let mark_impl_flag hpred = { Match.hpred = hpred; Match.flag = impl_ok1 } in match para_fst with - | [] -> L.out "@.@.ERROR (Empty DLL para): %a@.@." (Sil.pp_hpara_dll Pp.text) para; assert false + | [] -> + L.internal_error "@\n@\nERROR (Empty DLL Para): %a@\n@." (Sil.pp_hpara_dll Pp.text) para; + assert false | hpred :: hpreds -> let hpat = mark_impl_flag hpred in let hpats = List.map ~f:mark_impl_flag hpreds in @@ -422,7 +428,8 @@ let typ_get_recursive_flds tenv typ_exp = match Tenv.lookup tenv name with | Some { fields } -> List.map ~f:fst3 (List.filter ~f:(filter typ) fields) | None -> - L.out "@.typ_get_recursive: unexpected type expr: %a@." Exp.pp typ_exp; + L.(debug Analysis Quiet) "@\ntyp_get_recursive: unexpected type expr: %a@." + Exp.pp typ_exp; [] (* ToDo: assert false *) ) | Tint _ | Tvoid | Tfun _ | Tptr _ | Tfloat _ | Tarray _ | TVar _ -> [] @@ -430,7 +437,7 @@ let typ_get_recursive_flds tenv typ_exp = | Exp.Var _ -> [] (* type of |-> not known yet *) | Exp.Const _ -> [] | _ -> - L.out "@.typ_get_recursive: unexpected type expr: %a@." Exp.pp typ_exp; + L.internal_error "@\ntyp_get_recursive: unexpected type expr: %a@." Exp.pp typ_exp; assert false let discover_para_roots tenv p root1 next1 root2 next2 : Sil.hpara option = @@ -602,7 +609,9 @@ let eqs_solve ids_in eqs_in = if not (List.exists ~f:(fun id' -> Ident.equal id id') ids_in) then None else let sub' = match Sil.extend_sub sub id e with - | None -> L.out "@.@.ERROR : Buggy Implementation.@.@."; assert false + | None -> + L.internal_error "@\n@\nERROR : Buggy Implementation.@\n@."; + assert false | Some sub' -> sub' in let eqs_rest' = eqs_sub sub' eqs_rest in solve sub' eqs_rest' in diff --git a/infer/src/backend/cluster.ml b/infer/src/backend/cluster.ml index 5b836fb7f..b7ddaf83b 100644 --- a/infer/src/backend/cluster.ml +++ b/infer/src/backend/cluster.ml @@ -41,7 +41,7 @@ let pp_cluster fmt (nr, cluster) = let pp_cl fmt n = Format.fprintf fmt "%s" (cl_name n) in store_to_file (DB.filename_from_string fname) (nr, cluster); F.fprintf fmt "%a: @\n" pp_cl nr; - F.fprintf fmt "\t@@$(INFERANALYZE) --cluster '%s'@\n" fname; + F.fprintf fmt "\t%@$(INFERANALYZE) --cluster '%s'@\n" fname; (* touch the target of the rule to let `make` know that the job has been done *) - F.fprintf fmt "\t@@touch $@@@\n"; + F.fprintf fmt "\t%@touch $%@@\n"; F.fprintf fmt "@\n" diff --git a/infer/src/backend/clusterMakefile.ml b/infer/src/backend/clusterMakefile.ml index 1086d91db..0bdddd09d 100644 --- a/infer/src/backend/clusterMakefile.ml +++ b/infer/src/backend/clusterMakefile.ml @@ -37,7 +37,7 @@ let pp_prolog fmt clusters = F.fprintf fmt "@\n@\ndefault: test@\n@\nall: test@\n@\n"; F.fprintf fmt "test: $(CLUSTERS)@\n"; - if Config.show_progress_bar then F.fprintf fmt "\t@@echo@\n@." + if Config.show_progress_bar then F.fprintf fmt "\t%@echo@\n@." let pp_epilog fmt () = F.fprintf fmt "@.clean:@.\trm -f $(CLUSTERS)@." diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index 01fd5c19d..743a452aa 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -116,7 +116,8 @@ let strip_special_chars b = try String.set st idx c'; st - with Invalid_argument _ -> L.out "@\n@\n Invalid argument!!! @\n @.@.@."; assert false + with Invalid_argument _ -> + L.internal_error "@\n@\nstrip_special_chars: Invalid argument!@\n@."; assert false end else st in let s0 = replace b '(' 'B' in let s1 = replace s0 '$' 'D' in @@ -429,7 +430,7 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle = end else [(LinkStructToExp, Fieldname.to_string fn, n,"")] | _ -> (* by construction there must be at most 2 nodes for an expression*) - L.out "@\n Too many nodes! Error! @\n@.@."; assert false) + L.internal_error "@\n Too many nodes! Error! @\n@."; assert false) | Sil.Estruct (_, _) -> [] (* inner struct are printed by print_struc function *) | Sil.Earray _ -> [] (* inner arrays are printed by print_array function *) in match list_fld with @@ -462,7 +463,7 @@ let rec compute_target_array_elements dotnodes list_elements p f lambda = end else [(LinkArrayToExp, Exp.to_string idx, n,"")] | _ -> (* by construction there must be at most 2 nodes for an expression*) - L.out "@\n Too many nodes! Error! @\n@.@."; assert false + L.internal_error "@\nToo many nodes! Error!@\n@."; assert false ) | Sil.Estruct (_, _) -> [] (* inner struct are printed by print_struc function *) | Sil.Earray _ ->[] (* inner arrays are printed by print_array function *) @@ -589,25 +590,34 @@ let print_kind f kind = | Spec_precondition -> incr dotty_state_count; current_pre:=!dotty_state_count; - F.fprintf f "\n PRE%iL0 [label=\"PRE %i \", style=filled, color= yellow]\n" !dotty_state_count !spec_counter; + F.fprintf f "@\n PRE%iL0 [label=\"PRE %i \", style=filled, color= yellow]@\n" + !dotty_state_count !spec_counter; print_stack_info:= true; | Spec_postcondition _ -> - F.fprintf f "\n POST%iL0 [label=\"POST %i \", style=filled, color= yellow]\n" !dotty_state_count !post_counter; + F.fprintf f "@\n POST%iL0 [label=\"POST %i \", style=filled, color= yellow]@\n" + !dotty_state_count !post_counter; print_stack_info:= true; | Generic_proposition -> if !print_full_prop then - F.fprintf f "\n HEAP%iL0 [label=\"HEAP %i \", style=filled, color= yellow]\n" + F.fprintf f "@\n HEAP%iL0 [label=\"HEAP %i \", style=filled, color= yellow]@\n" !dotty_state_count !proposition_counter | Lambda_pred (no, lev, array) -> match array with | false -> - F.fprintf f "style=dashed; color=blue \n state%iL%i [label=\"INTERNAL STRUCTURE %i \", style=filled, color= lightblue]\n" !dotty_state_count !lambda_counter !lambda_counter ; - F.fprintf f "state%iL%i -> state%iL%i [color=\"lightblue \" arrowhead=none] \n" !dotty_state_count !lambda_counter no lev; + F.fprintf f "style=dashed; color=blue \ + @\n state%iL%i \ + [label=\"INTERNAL STRUCTURE %i \", style=filled, color= lightblue]@\n" + !dotty_state_count !lambda_counter !lambda_counter ; + F.fprintf f "state%iL%i -> state%iL%i [color=\"lightblue \" arrowhead=none] @\n" + !dotty_state_count !lambda_counter no lev; | true -> - F.fprintf f "style=dashed; color=blue \n state%iL%i [label=\"INTERNAL STRUCTURE %i \", style=filled, color= lightblue]\n" !dotty_state_count !lambda_counter !lambda_counter ; - (* F.fprintf f "state%iL%i -> struct%iL%i:%s [color=\"lightblue \" arrowhead=none] \n" !dotty_state_count !lambda_counter no lev lab;*) - + F.fprintf f "style=dashed; color=blue \ + @\n state%iL%i \ + [label=\"INTERNAL STRUCTURE %i \", style=filled, color= lightblue]@\n" + !dotty_state_count !lambda_counter !lambda_counter ; + (* F.fprintf f "state%iL%i -> struct%iL%i:%s [color=\"lightblue \" arrowhead=none] @\n" + !dotty_state_count !lambda_counter no lev lab;*) incr dotty_state_count (* print a link between two nodes in the graph *) @@ -620,25 +630,29 @@ let dotty_pp_link f link = let trg_fld = link.trg_fld in match n2, link.kind with | 0, _ when !print_full_prop -> - F.fprintf f "state%iL%i -> state%iL%i[label=\"%s DANG\", color= red];\n" n1 lambda1 n2 lambda2 src_fld + F.fprintf f "state%iL%i -> state%iL%i[label=\"%s DANG\", color= red];@\n" + n1 lambda1 n2 lambda2 src_fld | _, LinkToArray when !print_full_prop -> - F.fprintf f "state%iL%i -> struct%iL%i:%s%iL%i[label=\"\"]\n" n1 lambda1 n2 lambda2 trg_fld n2 lambda2 + F.fprintf f "state%iL%i -> struct%iL%i:%s%iL%i[label=\"\"]@\n" + n1 lambda1 n2 lambda2 trg_fld n2 lambda2 | _, LinkExpToStruct when !print_full_prop -> - F.fprintf f "state%iL%i -> struct%iL%i:%s%iL%i[label=\"\"]\n" n1 lambda1 n2 lambda2 trg_fld n2 lambda2 + F.fprintf f "state%iL%i -> struct%iL%i:%s%iL%i[label=\"\"]@\n" + n1 lambda1 n2 lambda2 trg_fld n2 lambda2 | _, LinkStructToExp when !print_full_prop -> - F.fprintf f "struct%iL%i:%s%iL%i -> state%iL%i[label=\"\"]\n" + F.fprintf f "struct%iL%i:%s%iL%i -> state%iL%i[label=\"\"]@\n" n1 lambda1 src_fld n1 lambda1 n2 lambda2 | _, LinkRetainCycle -> - F.fprintf f "struct%iL%i:%s%iL%i -> struct%iL%i:%s%iL%i[label=\"\", color= red]\n" + F.fprintf f "struct%iL%i:%s%iL%i -> struct%iL%i:%s%iL%i[label=\"\", color= red]@\n" n1 lambda1 src_fld n1 lambda1 n2 lambda2 trg_fld n2 lambda2 | _, LinkStructToStruct when !print_full_prop -> - F.fprintf f "struct%iL%i:%s%iL%i -> struct%iL%i:%s%iL%i[label=\"\"]\n" n1 lambda1 src_fld n1 lambda1 n2 lambda2 trg_fld n2 lambda2 + F.fprintf f "struct%iL%i:%s%iL%i -> struct%iL%i:%s%iL%i[label=\"\"]@\n" + n1 lambda1 src_fld n1 lambda1 n2 lambda2 trg_fld n2 lambda2 | _, LinkArrayToExp when !print_full_prop -> - F.fprintf f "struct%iL%i:%s -> state%iL%i[label=\"\"]\n" n1 lambda1 src_fld n2 lambda2 + F.fprintf f "struct%iL%i:%s -> state%iL%i[label=\"\"]@\n" n1 lambda1 src_fld n2 lambda2 | _, LinkArrayToStruct when !print_full_prop -> - F.fprintf f "struct%iL%i:%s -> struct%iL%i[label=\"\"]\n" n1 lambda1 src_fld n2 lambda2 + F.fprintf f "struct%iL%i:%s -> struct%iL%i[label=\"\"]@\n" n1 lambda1 src_fld n2 lambda2 | _, _ -> if !print_full_prop then - F.fprintf f "state%iL%i -> state%iL%i[label=\"%s\"];\n" n1 lambda1 n2 lambda2 src_fld + F.fprintf f "state%iL%i -> state%iL%i[label=\"%s\"];@\n" n1 lambda1 n2 lambda2 src_fld else () (* given the list of nodes and links get rid of spec nodes that are not pointed to by anybody*) @@ -703,26 +717,29 @@ let rec print_struct f pe e te l coo c = let n = coo.id in let lambda = coo.lambda in let e_no_special_char = strip_special_chars (Exp.to_string e) in - F.fprintf f "subgraph structs_%iL%i {\n" n lambda ; + F.fprintf f "subgraph structs_%iL%i {@\n" n lambda ; if !print_full_prop then F.fprintf f - " node [shape=record]; \n struct%iL%i \ - [label=\"{<%s%iL%i> STRUCT: %a } | %a\" ] fontcolor=%s\n" - n lambda e_no_special_char n lambda (Sil.pp_exp_printenv pe) e (struct_to_dotty_str pe coo) l c + " node [shape=record]; @\n struct%iL%i \ + [label=\"{<%s%iL%i> STRUCT: %a } | %a\" ] fontcolor=%s@\n" + n lambda + e_no_special_char n lambda (Sil.pp_exp_printenv pe) e (struct_to_dotty_str pe coo) l c else F.fprintf f - " node [shape=record]; \n struct%iL%i \ - [label=\"{<%s%iL%i> OBJECT: %s } | %a\" ] fontcolor=%s\n" + " node [shape=record]; @\n struct%iL%i \ + [label=\"{<%s%iL%i> OBJECT: %s } | %a\" ] fontcolor=%s@\n" n lambda e_no_special_char n lambda print_type (struct_to_dotty_str pe coo) l c; - F.fprintf f "}\n" + F.fprintf f "}@\n" and print_array f pe e1 e2 l coo c = let n = coo.id in let lambda = coo.lambda in let e_no_special_char = strip_special_chars (Exp.to_string e1) in - F.fprintf f "subgraph structs_%iL%i {\n" n lambda ; - F.fprintf f " node [shape=record]; \n struct%iL%i [label=\"{<%s%iL%i> ARRAY| SIZE: %a } | %a\" ] fontcolor=%s\n" n lambda e_no_special_char n lambda (Sil.pp_exp_printenv pe) e2 (get_contents pe coo) l c; - F.fprintf f "}\n" + F.fprintf f "subgraph structs_%iL%i {@\n" n lambda ; + F.fprintf f " node [shape=record]; @\n struct%iL%i \ + [label=\"{<%s%iL%i> ARRAY| SIZE: %a } | %a\" ] fontcolor=%s@\n" + n lambda e_no_special_char n lambda (Sil.pp_exp_printenv pe) e2 (get_contents pe coo) l c; + F.fprintf f "}@\n" and print_sll f pe nesting k e1 coo = let n = coo.id in @@ -731,15 +748,21 @@ and print_sll f pe nesting k e1 coo = incr dotty_state_count; begin match k with - | Sil.Lseg_NE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white]; label=\"list NE\";" n' lambda (*pp_nesting nesting*) - | Sil.Lseg_PE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white]; label=\"list PE\";" n' lambda (*pp_nesting nesting *) + | Sil.Lseg_NE -> + F.fprintf f "subgraph cluster_%iL%i { \ + style=filled; color=lightgrey; node [style=filled,color=white]; \ + label=\"list NE\";" n' lambda (*pp_nesting nesting*) + | Sil.Lseg_PE -> + F.fprintf f "subgraph cluster_%iL%i { \ + style=filled; color=lightgrey; node [style=filled,color=white]; \ + label=\"list PE\";" n' lambda (*pp_nesting nesting *) end; - F.fprintf f "state%iL%i [label=\"%a\"]\n" n lambda (Sil.pp_exp_printenv pe) e1; + F.fprintf f "state%iL%i [label=\"%a\"]@\n" n lambda (Sil.pp_exp_printenv pe) e1; let n' = !dotty_state_count in incr dotty_state_count; - F.fprintf f "state%iL%i [label=\"... \" style=filled color=lightgrey] \n" n' lambda ; - F.fprintf f "state%iL%i -> state%iL%i [label=\" \"] \n" n lambda n' lambda ; - F.fprintf f "state%iL%i [label=\" \"] \n" (n + 1) lambda ; + F.fprintf f "state%iL%i [label=\"... \" style=filled color=lightgrey] @\n" n' lambda ; + F.fprintf f "state%iL%i -> state%iL%i [label=\" \"] @\n" n lambda n' lambda ; + F.fprintf f "state%iL%i [label=\" \"] @\n" (n + 1) lambda ; F.fprintf f "state%iL%i -> state%iL%i [label=\" \"] }" n' lambda (n + 1) lambda ; incr lambda_counter; pp_dotty f (Lambda_pred(n + 1, lambda, false)) @@ -752,18 +775,24 @@ and print_dll f pe nesting k e1 e4 coo = incr dotty_state_count; begin match k with - | Sil.Lseg_NE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white]; label=\"doubly-linked list NE\";" n' lambda (*pp_nesting nesting *) - | Sil.Lseg_PE -> F.fprintf f "subgraph cluster_%iL%i { style=filled; color=lightgrey; node [style=filled,color=white]; label=\"doubly-linked list PE\";" n' lambda (*pp_nesting nesting *) + | Sil.Lseg_NE -> + F.fprintf f "subgraph cluster_%iL%i { \ + style=filled; color=lightgrey; node [style=filled,color=white]; \ + label=\"doubly-linked list NE\";" n' lambda (*pp_nesting nesting *) + | Sil.Lseg_PE -> + F.fprintf f "subgraph cluster_%iL%i { \ + style=filled; color=lightgrey; node [style=filled,color=white]; \ + label=\"doubly-linked list PE\";" n' lambda (*pp_nesting nesting *) end; - F.fprintf f "state%iL%i [label=\"%a\"]\n" n lambda (Sil.pp_exp_printenv pe) e1; + F.fprintf f "state%iL%i [label=\"%a\"]@\n" n lambda (Sil.pp_exp_printenv pe) e1; let n' = !dotty_state_count in incr dotty_state_count; - F.fprintf f "state%iL%i [label=\"... \" style=filled color=lightgrey] \n" n' lambda; - F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]\n" n lambda n' lambda; - F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]\n" n' lambda n lambda; - F.fprintf f "state%iL%i [label=\"%a\"]\n" (n + 1) lambda (Sil.pp_exp_printenv pe) e4; - F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]\n" (n + 1) lambda n' lambda; - F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]}\n" n' lambda (n + 1) lambda ; + F.fprintf f "state%iL%i [label=\"... \" style=filled color=lightgrey] @\n" n' lambda; + F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]@\n" n lambda n' lambda; + F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]@\n" n' lambda n lambda; + F.fprintf f "state%iL%i [label=\"%a\"]@\n" (n + 1) lambda (Sil.pp_exp_printenv pe) e4; + F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]@\n" (n + 1) lambda n' lambda; + F.fprintf f "state%iL%i -> state%iL%i [label=\" \"]}@\n" n' lambda (n + 1) lambda ; incr lambda_counter; pp_dotty f (Lambda_pred(n', lambda, false)) (Prop.normalize (Tenv.create ()) (Prop.from_sigma nesting)) None @@ -773,12 +802,14 @@ and dotty_pp_state f pe cycle dotnode = let n = coo.id in let lambda = coo.lambda in if is_dangling then - F.fprintf f "state%iL%i [label=\"%a \", color=red, style=dashed, fontcolor=%s]\n" n lambda (Sil.pp_exp_printenv pe) e c + F.fprintf f "state%iL%i [label=\"%a \", color=red, style=dashed, fontcolor=%s]@\n" + n lambda (Sil.pp_exp_printenv pe) e c else - F.fprintf f "state%iL%i [label=\"%a\" fontcolor=%s]\n" n lambda (Sil.pp_exp_printenv pe) e c in + F.fprintf f "state%iL%i [label=\"%a\" fontcolor=%s]@\n" + n lambda (Sil.pp_exp_printenv pe) e c in match dotnode with | Dotnil coo when !print_full_prop -> - F.fprintf f "state%iL%i [label=\"NIL \", color=green, style=filled]\n" coo.id coo.lambda + F.fprintf f "state%iL%i [label=\"NIL \", color=green, style=filled]@\n" coo.id coo.lambda | Dotdangling(coo, e, c) when !print_full_prop -> dotty_exp coo e c true | Dotpointsto(coo, e1, c) when !print_full_prop -> dotty_exp coo e1 c false | Dotstruct(coo, e1, l, c,te) -> @@ -816,20 +847,23 @@ and build_visual_graph f pe p cycle = and display_pure_info f pe prop = let print_invisible_objects () = for j = 1 to 4 do - F.fprintf f " inv_%i%i [style=invis]\n" !spec_counter j; - F.fprintf f " inv_%i%i%i [style=invis]\n" !spec_counter j j; - F.fprintf f " inv_%i%i%i%i [style=invis]\n" !spec_counter j j j; + F.fprintf f " inv_%i%i [style=invis]@\n" !spec_counter j; + F.fprintf f " inv_%i%i%i [style=invis]@\n" !spec_counter j j; + F.fprintf f " inv_%i%i%i%i [style=invis]@\n" !spec_counter j j j; done; for j = 1 to 4 do - F.fprintf f " state_pi_%i -> inv_%i%i [style=invis]\n" !proposition_counter !spec_counter j; - F.fprintf f " inv_%i%i -> inv_%i%i%i [style=invis]\n" !spec_counter j !spec_counter j j; - F.fprintf f " inv_%i%i%i -> inv_%i%i%i%i [style=invis]\n" !spec_counter j j !spec_counter j j j; + F.fprintf f " state_pi_%i -> inv_%i%i [style=invis]@\n" !proposition_counter !spec_counter j; + F.fprintf f " inv_%i%i -> inv_%i%i%i [style=invis]@\n" !spec_counter j !spec_counter j j; + F.fprintf f " inv_%i%i%i -> inv_%i%i%i%i [style=invis]@\n" + !spec_counter j j !spec_counter j j j; done in let pure = Prop.get_pure prop in - F.fprintf f "subgraph {\n"; - F.fprintf f " node [shape=box]; \n state_pi_%i [label=\"STACK \\n\\n %a\" color=orange style=filled]\n" !proposition_counter (Prop.pp_pi pe) pure; + F.fprintf f "subgraph {@\n"; + F.fprintf f " node [shape=box]; \ + @\n state_pi_%i [label=\"STACK \\n\\n %a\" color=orange style=filled]@\n" + !proposition_counter (Prop.pp_pi pe) pure; if !invisible_arrows then print_invisible_objects (); - F.fprintf f "}\n" + F.fprintf f "}@\n" (** Pretty print a proposition in dotty format. *) and pp_dotty f kind (_prop: Prop.normal Prop.t) cycle = @@ -852,13 +886,13 @@ and pp_dotty f kind (_prop: Prop.normal Prop.t) cycle = nil_dotboxes :=[]; set_exps_neq_zero prop.Prop.pi; incr dotty_state_count; - F.fprintf f "\n subgraph cluster_prop_%i { color=black \n" !proposition_counter; + F.fprintf f "@\n subgraph cluster_prop_%i { color=black @\n" !proposition_counter; print_kind f kind; if !print_stack_info then begin display_pure_info f pe prop; print_stack_info:= false end; - (* F.fprintf f "\n subgraph cluster_%i { color=black \n" !dotty_state_count; *) + (* F.fprintf f "@\n subgraph cluster_%i { color=black @\n" !dotty_state_count; *) let (nodes, links) = build_visual_graph f pe prop cycle in let all_nodes = (nodes @ !dangling_dotboxes @ !nil_dotboxes) in if !print_full_prop then @@ -867,24 +901,25 @@ and pp_dotty f kind (_prop: Prop.normal Prop.t) cycle = List.iter ~f:(fun node -> if node_in_cycle cycle node then (dotty_pp_state f pe) cycle node) all_nodes; List.iter ~f:(dotty_pp_link f) links; - (* F.fprintf f "\n } \n"; *) - F.fprintf f "\n } \n" + (* F.fprintf f "@\n } @\n"; *) + F.fprintf f "@\n } @\n" let pp_dotty_one_spec f pre posts = post_counter := 0; incr spec_counter; incr proposition_counter; incr dotty_state_count; - F.fprintf f "\n subgraph cluster_%i { color=blue \n" !dotty_state_count; + F.fprintf f "@\n subgraph cluster_%i { color=blue @\n" !dotty_state_count; incr dotty_state_count; - F.fprintf f "\n state%iL0 [label=\"SPEC %i \", style=filled, color= lightblue]\n" !dotty_state_count !spec_counter; + F.fprintf f "@\n state%iL0 [label=\"SPEC %i \", style=filled, color= lightblue]@\n" + !dotty_state_count !spec_counter; spec_id:=!dotty_state_count; invisible_arrows:= true; pp_dotty f Spec_precondition pre None; invisible_arrows:= false; List.iter ~f:(fun (po, _) -> incr post_counter ; pp_dotty f (Spec_postcondition pre) po None; for j = 1 to 4 do - F.fprintf f " inv_%i%i%i%i -> state_pi_%i [style=invis]\n" + F.fprintf f " inv_%i%i%i%i -> state_pi_%i [style=invis]@\n" !spec_counter j j @@ -892,26 +927,27 @@ let pp_dotty_one_spec f pre posts = !target_invisible_arrow_pre; done ) posts; - F.fprintf f "\n } \n" + F.fprintf f "@\n } @\n" (* this is used to print a list of proposition when considered in a path of nodes *) let pp_dotty_prop_list_in_path f plist prev_n curr_n = try incr proposition_counter; incr dotty_state_count; - F.fprintf f "\n subgraph cluster_%i { color=blue \n" !dotty_state_count; + F.fprintf f "@\n subgraph cluster_%i { color=blue @\n" !dotty_state_count; incr dotty_state_count; - F.fprintf f "\n state%iN [label=\"NODE %i \", style=filled, color= lightblue]\n" curr_n curr_n; + F.fprintf f "@\n state%iN [label=\"NODE %i \", style=filled, color= lightblue]@\n" + curr_n curr_n; List.iter ~f:(fun po -> incr proposition_counter ; pp_dotty f Generic_proposition po None) plist; - if prev_n <> - 1 then F.fprintf f "\n state%iN ->state%iN\n" prev_n curr_n; - F.fprintf f "\n } \n" + if prev_n <> - 1 then F.fprintf f "@\n state%iN ->state%iN@\n" prev_n curr_n; + F.fprintf f "@\n } @\n" with exn when SymOp.exn_not_failure exn -> () let pp_dotty_prop fmt (prop, cycle) = reset_proposition_counter (); - Format.fprintf fmt "@\n@\n@\ndigraph main { \nnode [shape=box]; @\n"; + Format.fprintf fmt "@\n@\n@\ndigraph main { @\nnode [shape=box]; @\n"; Format.fprintf fmt "@\n compound = true; rankdir =LR; @\n"; pp_dotty fmt Generic_proposition prop (Some cycle); Format.fprintf fmt "@\n}" @@ -931,16 +967,17 @@ let dotty_prop_to_dotty_file fname prop cycle = with exn when SymOp.exn_not_failure exn -> () -(* this is used only to print a list of prop parsed with the external parser. Basically deprecated.*) +(* This is used only to print a list of prop parsed with the external parser. Basically + deprecated.*) let pp_proplist_parsed2dotty_file filename plist = try let pp_list f plist = reset_proposition_counter (); - F.fprintf f "\n\n\ndigraph main { \nnode [shape=box];\n"; - F.fprintf f "\n compound = true; \n"; - F.fprintf f "\n /* size=\"12,7\"; ratio=fill;*/ \n"; + F.fprintf f "@\n@\n@\ndigraph main { @\nnode [shape=box];@\n"; + F.fprintf f "@\n compound = true; @\n"; + F.fprintf f "@\n /* size=\"12,7\"; ratio=fill;*/ @\n"; ignore (List.map ~f:(pp_dotty f Generic_proposition) plist); - F.fprintf f "\n}" in + F.fprintf f "@\n}" in let outc = open_out filename in let fmt = F.formatter_of_out_channel outc in F.fprintf fmt "#### Dotty version: ####@.%a@.@." pp_list plist; @@ -1007,7 +1044,7 @@ let pp_cfgnodeshape fmt (n: Procdesc.Node.t) = let pp_cfgnode pdesc fmt (n: Procdesc.Node.t) = let pname = Procdesc.get_proc_name pdesc in - F.fprintf fmt "%a [label=\"%a\" %a]\n\t\n" + F.fprintf fmt "%a [label=\"%a\" %a]@\n\t@\n" (pp_cfgnodename pname) n (pp_cfgnodelabel pdesc) n pp_cfgnodeshape n; @@ -1018,7 +1055,7 @@ let pp_cfgnode pdesc fmt (n: Procdesc.Node.t) = when is_exn -> (* don't print exception edges to the exit node *) () | _ -> - F.fprintf fmt "\n\t %a -> %a %s;" + F.fprintf fmt "@\n\t %a -> %a %s;" (pp_cfgnodename pname) n1 (pp_cfgnodename pname) n2 color in @@ -1039,16 +1076,16 @@ let print_icfg source fmt cfg = let print_node pdesc node = let loc = Procdesc.Node.get_loc node in if (Config.dotty_cfg_libs || SourceFile.equal loc.Location.file source) then - F.fprintf fmt "%a\n" (pp_cfgnode pdesc) node in + F.fprintf fmt "%a@\n" (pp_cfgnode pdesc) node in Cfg.iter_all_nodes ~sorted:true print_node cfg 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"; + F.fprintf fmt "/* %@%s */@\ndigraph iCFG {@\n" "generated"; print_icfg source fmt cfg; - F.fprintf fmt "}\n"; + F.fprintf fmt "}@\n"; Out_channel.close chan let print_icfg_dotty source cfg = @@ -1072,9 +1109,9 @@ let pp_speclist_dotty f (splist: Prop.normal Specs.spec list) = Config.pp_simple := true; reset_proposition_counter (); reset_dotty_spec_counter (); - F.fprintf f "@\n@\n\ndigraph main { \nnode [shape=box]; @\n"; + F.fprintf f "@\n@\n@\ndigraph main { @\nnode [shape=box]; @\n"; F.fprintf f "@\n compound = true; @\n"; - (* F.fprintf f "\n size=\"12,7\"; ratio=fill; \n"; *) + (* F.fprintf f "@\n size=\"12,7\"; ratio=fill; @\n"; *) List.iter ~f:(fun s -> pp_dotty_one_spec f (Specs.Jprop.to_prop s.Specs.pre) s.Specs.posts) splist; diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 3485b1c6a..1afbc2941 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -1156,6 +1156,5 @@ let explain_null_test_after_dereference tenv exp node line loc = Localise.desc_null_test_after_dereference expr_str line loc | None -> Localise.no_desc -(** Print a warning to the err stream at the given location (note: only prints in developer mode) *) let warning_err loc fmt_string = - L.out ("%a: Warning: " ^^ fmt_string) Location.pp loc + L.(debug Analysis Medium) ("%a: Warning: " ^^ fmt_string) Location.pp loc diff --git a/infer/src/backend/errdesc.mli b/infer/src/backend/errdesc.mli index 7766144ec..bdfb08df5 100644 --- a/infer/src/backend/errdesc.mli +++ b/infer/src/backend/errdesc.mli @@ -132,7 +132,7 @@ val explain_memory_access : Tenv.t -> Localise.deref_str -> 'a Prop.t -> Locatio val explain_null_test_after_dereference : Tenv.t -> Exp.t -> Procdesc.Node.t -> int -> Location.t -> Localise.error_desc -(** Print a warning to the err stream at the given location (note: only prints in developer mode) *) +(** warn at the given location *) val warning_err : Location.t -> ('a, Format.formatter, unit) format -> 'a (* offset of an expression found following a program variable *) diff --git a/infer/src/backend/exe_env.ml b/infer/src/backend/exe_env.ml index e76d00767..c2969a4cb 100644 --- a/infer/src/backend/exe_env.ml +++ b/infer/src/backend/exe_env.ml @@ -87,7 +87,7 @@ let add_cg (exe_env: t) (source_dir : DB.source_dir) = let cg_fname = DB.source_dir_get_internal_file source_dir ".cg" in match Cg.load_from_file cg_fname with | None -> - L.stderr "Error: cannot load %s@." (DB.filename_to_string cg_fname) + L.internal_error "Error: cannot load %s@." (DB.filename_to_string cg_fname) | Some cg -> let source = Cg.get_source cg in exe_env.source_files <- SourceFile.Set.add source exe_env.source_files; @@ -129,7 +129,7 @@ let get_file_data exe_env pname = let source_file_opt = match AttributesTable.load_attributes ~cache:true pname with | None -> - L.out "can't find tenv_cfg_object for %a@." Typ.Procname.pp pname; + L.(debug Analysis Medium) "can't find tenv_cfg_object for %a@." Typ.Procname.pp pname; None | Some proc_attributes when Config.reactive_capture -> let get_captured_file {ProcAttributes.source_file_captured} = source_file_captured in diff --git a/infer/src/backend/infer.ml b/infer/src/backend/infer.ml index 0eae07e4e..4bf5209b2 100644 --- a/infer/src/backend/infer.ml +++ b/infer/src/backend/infer.ml @@ -132,7 +132,8 @@ let remove_results_dir () = let create_results_dir () = Unix.mkdir_p (Config.results_dir ^/ Config.attributes_dir_name) ; Unix.mkdir_p (Config.results_dir ^/ Config.captured_dir_name) ; - Unix.mkdir_p (Config.results_dir ^/ Config.specs_dir_name) + Unix.mkdir_p (Config.results_dir ^/ Config.specs_dir_name); + L.setup_log_file () let clean_results_dir () = let dirs = ["classnames"; "filelists"; "multicore"; "sources"; "log"; @@ -174,9 +175,9 @@ let check_captured_empty driver_mode = if Utils.dir_is_empty Config.captured_dir && not Config.merge then (( match clean_command_opt with | Some clean_command -> - Logging.stderr "@\nNothing to compile. Try running `%s` first.@." clean_command + L.user_warning "@\nNothing to compile. Try running `%s` first.@." clean_command | None -> - Logging.stderr "@\nNothing to compile. Try cleaning the build first.@." + L.user_warning "@\nNothing to compile. Try cleaning the build first.@." ); true ) else @@ -219,11 +220,10 @@ let check_xcpretty () = match Unix.system "xcpretty --version" with | Ok () -> () | Error _ -> - L.stderr - "@.xcpretty not found in the path. Please consider installing xcpretty \ + L.user_error + "@\nxcpretty not found in the path. Please consider installing xcpretty \ for a more robust integration with xcodebuild. Otherwise use the option \ - --no-xcpretty.@.@."; - exit 1 + --no-xcpretty.@\n@." let capture_with_compilation_database db_files = let root = Unix.getcwd () in @@ -363,7 +363,8 @@ let report () = "--results-dir"; Config.results_dir ] in if is_error (Unix.waitpid (Unix.fork_exec ~prog ~args:(prog :: args) ())) then - L.stderr "** Error running the reporting script:@\n** %s %s@\n** See error above@." + L.external_error + "** Error running the reporting script:@\n** %s %s@\n** See error above@." prog (String.concat ~sep:" " args) let analyze driver_mode = @@ -384,7 +385,7 @@ let analyze driver_mode = if (should_analyze || should_report) && (((Sys.file_exists Config.captured_dir) <> `Yes) || check_captured_empty driver_mode) then ( - L.stderr "There was nothing to analyze.@\n@." ; + L.user_error "There was nothing to analyze.@\n@." ; ) else if should_analyze then execute_analyze (); if should_report && Config.report then report () @@ -399,12 +400,13 @@ let fail_on_issue_epilogue () = | None -> () let log_infer_args driver_mode = - L.out "INFER_ARGS = %s@\n" (Option.value (Sys.getenv CLOpt.args_env_var) ~default:""); - List.iter ~f:(L.out "anon arg: %s@\n") Config.anon_args; - List.iter ~f:(L.out "rest arg: %s@\n") Config.rest; - L.out "Project root = %s@\n" Config.project_root; - L.out "CWD = %s@\n" (Sys.getcwd ()); - L.out "Driver mode:@\n%a@." pp_driver_mode driver_mode + L.environment_info "INFER_ARGS = %s@\n" + (Option.value (Sys.getenv CLOpt.args_env_var) ~default:""); + List.iter ~f:(L.environment_info "anon arg: %s@\n") Config.anon_args; + List.iter ~f:(L.environment_info "rest arg: %s@\n") Config.rest; + L.environment_info "Project root = %s@\n" Config.project_root; + L.environment_info "CWD = %s@\n" (Sys.getcwd ()); + L.environment_info "Driver mode:@\n%a@." pp_driver_mode driver_mode let assert_supported_mode required_analyzer requested_mode_string = let analyzer_enabled = match required_analyzer with @@ -497,9 +499,7 @@ let infer_mode () = Config.(buck || continue_capture || maven || reactive_mode)) then remove_results_dir () ; create_results_dir () ; - (* re-set log files, as default files were in results_dir removed above *) - if not Config.buck_cache_mode then L.set_log_file_identifier CLOpt.Run None; - if CLOpt.is_originator then L.do_out "%s@\n" Config.version_string ; + if CLOpt.is_originator then L.environment_info "%a@\n" Config.pp_version () ; if Config.debug_mode || Config.stats_mode then log_infer_args driver_mode ; if Config.dump_duplicate_symbols then reset_duplicates_file (); (* infer might be called from a Makefile and itself uses `make` to run the analysis in parallel, @@ -528,7 +528,7 @@ let differential_mode () = (* at least one report must be passed in input to compute differential *) (match Config.report_current, Config.report_previous with | None, None -> - failwith "Expected at least one argument among 'report-current' and 'report-previous'\n" + failwith "Expected at least one argument among 'report-current' and 'report-previous'@\n" | _ -> ()); let load_report filename_opt : Jsonbug_t.report = let empty_report = [] in @@ -550,9 +550,11 @@ let differential_mode () = let assert_results_dir advice = if Sys.file_exists Config.results_dir <> `Yes then ( - L.stderr "ERROR: results directory %s does not exist@\nERROR: %s@." Config.results_dir advice; + L.user_error "ERROR: results directory %s does not exist@\nERROR: %s@." + Config.results_dir advice; exit 1 - ) + ); + L.setup_log_file () let setup_results_dir () = match Config.command with @@ -568,8 +570,10 @@ let () = setup_results_dir (); match Config.command with | Analyze -> - Logging.set_log_file_identifier - CommandLineOption.Analyze (Option.map ~f:Filename.basename Config.cluster_cmdline); + let pp_cluster_opt fmt = function + | None -> F.fprintf fmt "(no cluster)" + | Some cluster -> F.fprintf fmt "of cluster %s" (Filename.basename cluster) in + L.environment_info "Starting analysis %a" pp_cluster_opt Config.cluster_cmdline; InferAnalyze.register_perf_stats_report (); analyze Analyze | Clang -> @@ -577,6 +581,9 @@ let () = | prog::args -> prog, args | [] -> assert false (* Sys.argv is never empty *) in ClangWrapper.exe ~prog ~args - | Report -> InferPrint.main_from_config () - | ReportDiff -> differential_mode () - | Capture | Compile | Run -> infer_mode () + | Report -> + InferPrint.main_from_config () + | ReportDiff -> + differential_mode () + | Capture | Compile | Run -> + infer_mode () diff --git a/infer/src/backend/inferconfig.ml b/infer/src/backend/inferconfig.ml index 9608777d7..2d12bcba7 100644 --- a/infer/src/backend/inferconfig.ml +++ b/infer/src/backend/inferconfig.ml @@ -169,7 +169,7 @@ module FileOrProcMatcher = struct | None -> pp_string fmt "None" | Some value -> Format.fprintf fmt "%a" pp_value value in let pp_key_value pp_value fmt (key, value) = - Format.fprintf fmt " %s: %a,\n" key (pp_option pp_value) value in + Format.fprintf fmt " %s: %a,@\n" key (pp_option pp_value) value in let pp_method_pattern fmt mp = let pp_params fmt l = Format.fprintf fmt "[%a]" @@ -179,13 +179,13 @@ module FileOrProcMatcher = struct (pp_key_value pp_string) ("method", mp.method_name) (pp_key_value pp_params) ("parameters", mp.parameters) and pp_source_contains fmt sc = - Format.fprintf fmt " pattern: %s\n" sc in + Format.fprintf fmt " pattern: %s@\n" sc in match pattern with | Method_pattern (language, mp) -> - Format.fprintf fmt "Method pattern (%s) {\n%a}\n" + Format.fprintf fmt "Method pattern (%s) {@\n%a}@\n" (Config.string_of_language language) pp_method_pattern mp | Source_contains (language, sc) -> - Format.fprintf fmt "Source contains (%s) {\n%a}\n" + Format.fprintf fmt "Source contains (%s) {@\n%a}@\n" (Config.string_of_language language) pp_source_contains sc end (* of module FileOrProcMatcher *) @@ -380,7 +380,7 @@ let test () = let matching = matching_analyzers source_file in if matching <> [] then let matching_s = String.concat ~sep:", " (List.map ~f:fst matching) in - L.stderr "%s -> {%s}@." + L.result "%s -> {%s}@." (SourceFile.to_rel_path source_file) matching_s) (Sys.getcwd ()) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index b5f13940e..d379e0d6e 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -116,10 +116,9 @@ module Worklist = struct wl.visit_map <- Procdesc.NodeMap.add min.node (min.visits + 1) wl.visit_map; (* increase the visits *) min.node - with Not_found -> begin - L.out "@\n...Work list is empty! Impossible to remove edge...@\n"; - assert false - end + with Not_found -> + L.internal_error "@\n...Work list is empty! Impossible to remove edge...@\n"; + assert false end (* =============== END of module Worklist =============== *) @@ -162,7 +161,7 @@ let path_set_checkout_todo (wl : Worklist.t) (node: Procdesc.Node.t) : Paths.Pat Hashtbl.replace wl.Worklist.path_set_visited node_id new_visited; todo with Not_found -> - L.out "@.@.ERROR: could not find todo for node %a@.@." Procdesc.Node.pp node; + L.internal_error "@\n@\nERROR: could not find todo for node %a@\n@." Procdesc.Node.pp node; assert false (* =============== END of the edge_set object =============== *) @@ -1004,7 +1003,8 @@ let perform_analysis_phase tenv (summary : Specs.summary) (pdesc : Procdesc.t) let add pset prop = Paths.PathSet.add_renamed_prop prop (Paths.Path.start start_node) pset in Propset.fold add Paths.PathSet.empty init_props in - L.out "@.#### Start: Footprint Computation for %a ####@." Typ.Procname.pp pname; + L.(debug Analysis Medium) "@\n#### Start: Footprint Computation for %a ####@." + Typ.Procname.pp pname; L.d_increase_indent 1; L.d_strln "initial props ="; Propset.d Prop.prop_emp init_props; L.d_ln (); L.d_ln(); @@ -1019,11 +1019,11 @@ let perform_analysis_phase tenv (summary : Specs.summary) (pdesc : Procdesc.t) let get_results (wl : Worklist.t) () = State.process_execution_failures Reporting.log_warning pname; let results = collect_analysis_result tenv wl pdesc in - L.out "#### [FUNCTION %a] ... OK #####@\n" Typ.Procname.pp pname; - L.out "#### Finished: Footprint Computation for %a %a ####@." + L.(debug Analysis Medium) "#### [FUNCTION %a] ... OK #####@\n" Typ.Procname.pp pname; + L.(debug Analysis Medium) "#### Finished: Footprint Computation for %a %a ####@." Typ.Procname.pp pname (pp_intra_stats wl pdesc) pname; - L.out "#### [FUNCTION %a] Footprint Analysis result ####@\n%a@." + L.(debug Analysis Medium) "#### [FUNCTION %a] Footprint Analysis result ####@\n%a@." Typ.Procname.pp pname (Paths.PathSet.pp Pp.text) results; let specs = try extract_specs tenv pdesc results with @@ -1044,7 +1044,7 @@ let perform_analysis_phase tenv (summary : Specs.summary) (pdesc : Procdesc.t) (Specs.get_specs_from_payload summary) in let valid_specs = ref [] in let go () = - L.out "@.#### Start: Re-Execution for %a ####@." Typ.Procname.pp pname; + L.(debug Analysis Medium) "@.#### Start: Re-Execution for %a ####@." Typ.Procname.pp pname; let filter p = let wl = path_set_create_worklist pdesc in let speco = execute_filter_prop wl tenv pdesc start_node p in @@ -1054,7 +1054,7 @@ let perform_analysis_phase tenv (summary : Specs.summary) (pdesc : Procdesc.t) valid_specs := !valid_specs @ [spec]; true in let outcome = if is_valid then "pass" else "fail" in - L.out "Finished re-execution for precondition %d %a (%s)@." + L.(debug Analysis Medium) "Finished re-execution for precondition %d %a (%s)@." (Specs.Jprop.to_number p) (pp_intra_stats wl pdesc) pname outcome; @@ -1065,8 +1065,8 @@ let perform_analysis_phase tenv (summary : Specs.summary) (pdesc : Procdesc.t) ignore (List.map ~f:filter candidate_preconditions) in let get_results () = let specs = !valid_specs in - L.out "#### [FUNCTION %a] ... OK #####@\n" Typ.Procname.pp pname; - L.out "#### Finished: Re-Execution for %a ####@." Typ.Procname.pp pname; + L.(debug Analysis Medium) "#### [FUNCTION %a] ... OK #####@\n" Typ.Procname.pp pname; + L.(debug Analysis Medium) "#### Finished: Re-Execution for %a ####@." Typ.Procname.pp pname; let valid_preconditions = List.map ~f:(fun spec -> spec.Specs.pre) specs in let source = (Procdesc.get_loc pdesc).file in @@ -1076,14 +1076,16 @@ let perform_analysis_phase tenv (summary : Specs.summary) (pdesc : Procdesc.t) [(Typ.Procname.to_filename pname)] in if Config.write_dotty then Dotty.pp_speclist_dotty_file filename specs; - L.out "@.@.================================================"; - L.out "@. *** CANDIDATE PRECONDITIONS FOR %a: " Typ.Procname.pp pname; - L.out "@.================================================@."; - L.out "@.%a @.@." (Specs.Jprop.pp_list Pp.text false) candidate_preconditions; - L.out "@.@.================================================"; - L.out "@. *** VALID PRECONDITIONS FOR %a: " Typ.Procname.pp pname; - L.out "@.================================================@."; - L.out "@.%a @.@." (Specs.Jprop.pp_list Pp.text true) valid_preconditions; + L.(debug Analysis Medium) "@\n@\n================================================"; + L.(debug Analysis Medium) "@\n *** CANDIDATE PRECONDITIONS FOR %a: " Typ.Procname.pp pname; + L.(debug Analysis Medium) "@\n================================================@\n"; + L.(debug Analysis Medium) "@\n%a @\n@\n" + (Specs.Jprop.pp_list Pp.text false) candidate_preconditions; + L.(debug Analysis Medium) "@\n@\n================================================"; + L.(debug Analysis Medium) "@\n *** VALID PRECONDITIONS FOR %a: " Typ.Procname.pp pname; + L.(debug Analysis Medium) "@\n================================================@\n"; + L.(debug Analysis Medium) "@\n%a @\n@." + (Specs.Jprop.pp_list Pp.text true) valid_preconditions; specs, Specs.RE_EXECUTION in go, get_results in @@ -1229,7 +1231,7 @@ let update_specs tenv prev_summary phase (new_specs : Specs.NormSpec.t list) new_specs) then begin changed:= true; - L.out "Specs changed: removing pre of spec@\n%a@." + L.(debug Analysis Medium) "Specs changed: removing pre of spec@\n%a@." (Specs.pp_spec Pp.text None) old_spec; current_specs := SpecMap.remove old_spec.Specs.pre !current_specs end else () in @@ -1243,7 +1245,7 @@ let update_specs tenv prev_summary phase (new_specs : Specs.NormSpec.t list) Specs.Visitedset.union old_visited spec.Specs.visited in if not (Paths.PathSet.equal old_post new_post) then begin changed := true; - L.out "Specs changed: added new post@\n%a@." + L.(debug Analysis Medium) "Specs changed: added new post@\n%a@." (Propset.pp Pp.text (Specs.Jprop.to_prop spec.Specs.pre)) (Paths.PathSet.to_propset tenv new_post); current_specs := @@ -1252,7 +1254,7 @@ let update_specs tenv prev_summary phase (new_specs : Specs.NormSpec.t list) with Not_found -> changed := true; - L.out "Specs changed: added new pre@\n%a@." + L.(debug Analysis Medium) "Specs changed: added new pre@\n%a@." (Specs.Jprop.pp_short Pp.text) spec.Specs.pre; current_specs := SpecMap.add @@ -1316,7 +1318,7 @@ let analyze_proc tenv proc_desc : Specs.summary = (** Perform the transition from [FOOTPRINT] to [RE_EXECUTION] in spec table *) let transition_footprint_re_exe tenv proc_name joined_pres = - L.out "Transition %a from footprint to re-exe@." Typ.Procname.pp proc_name; + L.(debug Analysis Medium) "Transition %a from footprint to re-exe@." Typ.Procname.pp proc_name; let summary = Specs.get_summary_unsafe "transition_footprint_re_exe" proc_name in let summary' = if Config.only_footprint then @@ -1363,10 +1365,11 @@ let perform_transition proc_desc tenv proc_name = with exn when SymOp.exn_not_failure exn -> apply_start_node do_after_node; Config.allow_leak := allow_leak; - L.out "Error in collect_preconditions for %a@." Typ.Procname.pp proc_name; + L.(debug Analysis Medium) "Error in collect_preconditions for %a@." + Typ.Procname.pp proc_name; let err_name, _, ml_loc_opt, _, _, _, _ = Exceptions.recognize_exception exn in let err_str = "exception raised " ^ (Localise.to_issue_id err_name) in - L.out "Error: %s %a@." err_str L.pp_ml_loc_opt ml_loc_opt; + L.(debug Analysis Medium) "Error: %s %a@." err_str L.pp_ml_loc_opt ml_loc_opt; [] in transition_footprint_re_exe tenv proc_name joined_pres in match Specs.get_summary proc_name with @@ -1523,7 +1526,8 @@ let print_stats_cfg proc_shadowed source cfg = match Specs.get_summary proc_name with | None -> () | Some _ when proc_shadowed proc_desc -> - L.out "print_stats: ignoring function %a which is also defined in another file@." + L.(debug Analysis Medium) + "print_stats: ignoring function %a which is also defined in another file@." Typ.Procname.pp proc_name | Some summary -> let stats = summary.Specs.stats in @@ -1580,7 +1584,7 @@ let print_stats_cfg proc_shadowed source cfg = Out_channel.close outc with Sys_error _ -> () in List.iter ~f:compute_stats_proc (Cfg.get_defined_procs cfg); - L.out "%a" print_file_stats (); + L.(debug Analysis Medium) "%a" print_file_stats (); save_file_stats () (** Print the stats for all the files in the cluster *) diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml index 865fe4f68..c70ca3aaf 100644 --- a/infer/src/backend/match.ml +++ b/infer/src/backend/match.ml @@ -143,9 +143,11 @@ and isel_match isel1 sub vars isel2 = let sanity_check = not (List.exists ~f:(fun id -> Sil.ident_in_exp id idx2) vars) in if (not sanity_check) then begin let pe = Pp.text in - L.out "@[.... Sanity Check Failure while Matching Index-Strexps ....@."; - L.out "@[<4> IDX1: %a, STREXP1: %a@." (Sil.pp_exp_printenv pe) idx1 (Sil.pp_sexp pe) se1'; - L.out "@[<4> IDX2: %a, STREXP2: %a@\n@." (Sil.pp_exp_printenv pe) idx2 (Sil.pp_sexp pe) se2'; + L.internal_error "@[.... Sanity Check Failure while Matching Index-Strexps ....@\n"; + L.internal_error "@[<4> IDX1: %a, STREXP1: %a@\n" + (Sil.pp_exp_printenv pe) idx1 (Sil.pp_sexp pe) se1'; + L.internal_error "@[<4> IDX2: %a, STREXP2: %a@\n@." + (Sil.pp_exp_printenv pe) idx2 (Sil.pp_sexp pe) se2'; assert false end else if Exp.equal idx1 idx2 then begin diff --git a/infer/src/backend/mergeCapture.ml b/infer/src/backend/mergeCapture.ml index 3168361f1..5a2c3a282 100644 --- a/infer/src/backend/mergeCapture.ml +++ b/infer/src/backend/mergeCapture.ml @@ -34,8 +34,6 @@ let modified_file file = | None -> () -let debug = 0 - type stats = { mutable files_linked: int; @@ -105,8 +103,7 @@ let create_multilinks () = Replicate the structure of the source directory in the destination, with files replaced by links to the source. *) let rec slink ~stats ~skiplevels src dst = - if debug >=3 - then L.stderr "slink src:%s dst:%s skiplevels:%d@." src dst skiplevels; + L.(debug MergeCapture Verbose) "slink src:%s dst:%s skiplevels:%d@." src dst skiplevels; if Sys.is_directory src = `Yes then begin @@ -135,9 +132,7 @@ let should_link ~target ~target_results_dir ~stats infer_out_src infer_out_dst = let filename = DB.filename_from_string file in let time_orig = DB.file_modified_time ~symlink:false filename in let time_link = DB.file_modified_time ~symlink:true filename in - if debug >= 2 then - L.stderr "file:%s time_orig:%f time_link:%f@." - file time_orig time_link; + L.(debug MergeCapture Verbose) "file:%s time_orig:%f time_link:%f@." file time_orig time_link; time_link > time_orig in let symlinks_up_to_date captured_file = if Sys.is_directory captured_file = `Yes then @@ -174,10 +169,9 @@ let should_link ~target ~target_results_dir ~stats infer_out_src infer_out_dst = was_modified () || not (was_copied ()) in if r then stats.targets_merged <- stats.targets_merged + 1; - if debug >= 2 - then L.stderr "lnk:%s:%d %s@." (if r then "T" else "F") !num_captured_files target_results_dir - else if debug >= 1 && r - then L.stderr "%s@."target_results_dir; + L.(debug MergeCapture Verbose) "lnk:%s:%d %s@." (if r then "T" else "F") !num_captured_files + target_results_dir; + if r then L.(debug MergeCapture Medium) "%s@."target_results_dir; r (** should_link needs to know whether the source file has changed, diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 68b7ef509..56d70b8ab 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -122,12 +122,11 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc let start_time = Unix.gettimeofday () in fun () -> let elapsed_time = Unix.gettimeofday () -. start_time in - L.out "Elapsed analysis time: %a: %f\n" + L.(debug Analysis Medium) "Elapsed analysis time: %a: %f@\n" Typ.Procname.pp callee_pname elapsed_time in - (* Dot means start of a procedure *) - L.log_progress_procedure (); + L.progressbar_procedure (); if Config.trace_ondemand then L.progress "[%d] run_proc_analysis %a -> %a@." !nesting Typ.Procname.pp curr_pname @@ -167,7 +166,7 @@ let run_proc_analysis ~propagate_exceptions analyze_proc curr_pdesc callee_pdesc restore_global_state old_state; summary with exn -> - L.stderr "@.ONDEMAND EXCEPTION %a %s@.@.BACK TRACE@.%s@?" + L.internal_error "@\nONDEMAND EXCEPTION %a %s@.@.BACK TRACE@.%s@?" Typ.Procname.pp callee_pname (Exn.to_string exn) (Printexc.get_backtrace ()); diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 09bc19072..98b65debb 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -133,7 +133,7 @@ end = struct (F.fprintf fmt "

Cfg Node %a

" (Io_infer.Html.pp_line_link source ~text: (Some (string_of_int nodeid)) [".."]) loc.Location.line; - F.fprintf fmt "PROC: %a LINE:%a\n" + F.fprintf fmt "PROC: %a LINE:%a@\n" (Io_infer.Html.pp_proc_link [".."] proc_name) (Escape.escape_xml (Typ.Procname.to_string proc_name)) (Io_infer.Html.pp_line_link source [".."]) loc.Location.line; @@ -493,7 +493,7 @@ let write_html_file linereader filename procs = (DB.Results_dir.Abs_source_dir filename) [".."; fname_encoding] in let pp_prelude () = - F.fprintf fmt "

File %a

\n\n" + F.fprintf fmt "

File %a

@\n
@\n" SourceFile.pp filename in let print_one_line proof_cover table_nodes_at_linenum table_err_per_line line_number = let line_html = @@ -556,7 +556,7 @@ let write_html_file linereader filename procs = ~f:(fun err_string -> F.fprintf fmt "%s" (create_err_message err_string)) errors_at_linenum; - F.fprintf fmt "%s" "\n" in + F.fprintf fmt "%s" "@\n" in pp_prelude (); let global_err_log = Errlog.empty () in @@ -572,7 +572,7 @@ let write_html_file linereader filename procs = print_one_line proof_cover table_nodes_at_linenum table_err_per_line !linenum done with End_of_file -> - (F.fprintf fmt "%s" "
\n"; + (F.fprintf fmt "%s" "@\n"; Errlog.pp_html filename [fname_encoding] fmt global_err_log; Io_infer.Html.close (fd, fmt)) diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index b022a9a14..64bd0fbd9 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1356,7 +1356,7 @@ module Normalize = struct | Var _ -> Estruct ([], inst) | te -> - L.out "trying to create ptsto with type: %a@\n@." (Sil.pp_texp_full Pp.text) te; + L.internal_error "trying to create ptsto with type: %a@." (Sil.pp_texp_full Pp.text) te; assert false in let strexp : Sil.strexp = match expo with | Some e -> Eexp (e, inst) @@ -2149,10 +2149,10 @@ let exist_quantify tenv fav (prop : normal t) : normal t = if Sil.equal_subst sub prop.sub then prop else unsafe_cast_to_normal (set prop ~sub) in (* - L.out "@[<2>.... Existential Quantification ....\n"; - L.out "SUB:%a\n" pp_sub prop'.sub; - L.out "PI:%a\n" pp_pi prop'.pi; - L.out "PROP:%a\n@." pp_prop prop'; + L.out "@[<2>.... Existential Quantification ....@\n"; + L.out "SUB:%a@\n" pp_sub prop'.sub; + L.out "PI:%a@\n" pp_pi prop'.pi; + L.out "PROP:%a@\n@." pp_prop prop'; *) prop_ren_sub tenv ren_sub prop' @@ -2361,10 +2361,10 @@ let prop_iter_make_id_primed tenv id iter = begin match eq with | Aeq (Var id1, e1) when Sil.ident_in_exp id1 e1 -> - L.out "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n"; - L.out "Broken Assumption: id notin e for all (id,e) in sub@\n"; - L.out "(id,e) : (%a,%a)@\n" (Ident.pp Pp.text) id1 Exp.pp e1; - L.out "PROP : %a@\n@." (pp_prop Pp.text) (prop_iter_to_prop tenv iter); + L.internal_error "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n"; + L.internal_error "Broken Assumption: id notin e for all (id,e) in sub@\n"; + L.internal_error "(id,e) : (%a,%a)@\n" (Ident.pp Pp.text) id1 Exp.pp e1; + L.internal_error "PROP : %a@\n@." (pp_prop Pp.text) (prop_iter_to_prop tenv iter); assert false | Aeq (Var id1, e1) when Ident.equal pid id1 -> split pairs_unpid ((id1, e1):: pairs_pid) eqs_cur diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index 43ba01bad..4e3941201 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -432,7 +432,7 @@ let mk_ptsto_exp_footprint * will fix them during the re - execution phase *) if not (Config.angelic_execution && !Config.footprint) then begin - L.out "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp; + L.internal_error "!!!! Footprint Error, Bad Root : %a !!!! @\n" Exp.pp lexp; let deref_str = Localise.deref_str_dangling None in let err_desc = Errdesc.explain_dereference tenv deref_str orig_prop (State.get_loc ()) in diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 4a3ed2d3d..db67c078d 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -355,7 +355,7 @@ let pp_failure_kind_opt fmt failure_kind_opt = match failure_kind_opt with | None -> F.fprintf fmt "NONE" let pp_errlog fmt err_log = - F.fprintf fmt "ERRORS: @[%a@]@." Errlog.pp_errors err_log; + F.fprintf fmt "ERRORS: @[%a@]@\n%!" Errlog.pp_errors err_log; F.fprintf fmt "WARNINGS: @[%a@]" Errlog.pp_warnings err_log let pp_stats fmt stats = @@ -441,7 +441,7 @@ let pp_payload pe fmt { preposts; typestate; crashcontext_frame; quandary; siof; threadsafety; buffer_overrun; annot_map } = let pp_opt prefix pp fmt = function - | Some x -> F.fprintf fmt "%s: %a\n" prefix pp x + | Some x -> F.fprintf fmt "%s: %a@\n" prefix pp x | None -> () in F.fprintf fmt "%a%a%a%a%a%a%a%a@\n" (pp_opt "PrePosts" (pp_specs pe)) (Option.map ~f:NormSpec.tospecs preposts) @@ -509,7 +509,7 @@ let summary_compact sh summary = (** Add the summary to the table for the given function *) let add_summary (proc_name : Typ.Procname.t) (summary: summary) : unit = - L.out "Adding summary for %a@\n@[ %a@]@." + L.(debug Analysis Medium) "Adding summary for %a@\n@[ %a@]@." Typ.Procname.pp proc_name pp_summary_text summary; Typ.Procname.Hash.replace spec_tbl proc_name summary diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 94495c39c..f3895bdd6 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1235,7 +1235,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path | [], _ -> ret_old_path [prop_] | _ -> - L.out "Pvar %a appears on the LHS of >1 heap predicate!@." (Pvar.pp Pp.text) pvar; + L.internal_error "Pvar %a appears on the LHS of >1 heap predicate!@." + (Pvar.pp Pp.text) pvar; assert false end | Sil.Abstract _ -> diff --git a/infer/src/backend/timeout.ml b/infer/src/backend/timeout.ml index 007360d9b..068080012 100644 --- a/infer/src/backend/timeout.ml +++ b/infer/src/backend/timeout.ml @@ -124,7 +124,7 @@ let exe_timeout f x = with | SymOp.Analysis_failure_exe kind -> resume_previous_timeout (); - L.log_progress_timeout_event kind; + L.progressbar_timeout_event kind; Errdesc.warning_err (State.get_loc ()) "TIMEOUT: %a@." SymOp.pp_failure_kind kind; Some kind | exe -> diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 8b98c571e..3b1bd4203 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -254,11 +254,11 @@ type dynamic_dispatch_policy = [ (** Compile time configuration values *) -let version_string = - "Infer version " - ^ Version.versionString - ^ "\nCopyright 2009 - present Facebook. All Rights Reserved." +let pp_version fmt () = + F.fprintf fmt "Infer version %s@\nCopyright 2009 - present Facebook. All Rights Reserved." + Version.versionString +let version_string = F.asprintf "%a" pp_version () (** System call configuration values *) @@ -645,10 +645,6 @@ and bootclasspath = ~in_help:CLOpt.[Capture, manual_java] "Specify the Java bootclasspath" -and bo_debug = - CLOpt.mk_int ~default:0 ~long:"bo-debug" - ~in_help:CLOpt.[Analyze, manual_buffer_overrun] "Debug mode for buffer-overrun checker" - (** Automatically set when running from within Buck *) and buck = CLOpt.mk_bool ~long:"buck" @@ -778,9 +774,13 @@ and cxx = "Analyze C++ methods" and ( + bo_debug, developer_mode, debug, debug_exceptions, + debug_level_analysis, + debug_level_capture, + debug_level_linters, default_linters, failures_allowed, filtering, @@ -795,15 +795,40 @@ and ( write_html, write_dotty ) = - let failures_allowed = - CLOpt.mk_bool ~deprecated_no:["-no_failures_allowed"] ~long:"failures-allowed" ~default:true - "Fail if at least one of the translations fails (clang only)" + let all_generic_manuals = + List.filter_map CLOpt.all_commands + ~f:(fun cmd -> + if CLOpt.(equal_command cmd Clang) then None + else Some (cmd, manual_generic)) in + + let bo_debug = + CLOpt.mk_int ~default:0 ~long:"bo-debug" + ~in_help:CLOpt.[Analyze, manual_buffer_overrun] "Debug level for buffer-overrun checker (0-4)" + + and debug_level_analysis = + CLOpt.mk_int ~long:"debug-level-analysis" ~default:0 + ~in_help:all_generic_manuals + "Debug level for the analysis. See $(b,--debug-level) for accepted values." + + and debug_level_capture = + CLOpt.mk_int ~long:"debug-level-capture" ~default:0 + ~in_help:all_generic_manuals + "Debug level for the capture. See $(b,--debug-level) for accepted values." + + and debug_level_linters = + CLOpt.mk_int ~long:"debug-level-linters" ~default:0 + ~in_help:(CLOpt.(Capture, manual_clang_linters)::all_generic_manuals) + "Debug level for the linters. See $(b,--debug-level) for accepted values." and developer_mode = CLOpt.mk_bool ~long:"developer-mode" ~default:(Option.value_map ~default:false ~f:(CLOpt.(equal_command Report)) initial_command) "Show internal exceptions" + and failures_allowed = + CLOpt.mk_bool ~deprecated_no:["-no_failures_allowed"] ~long:"failures-allowed" ~default:true + "Fail if at least one of the translations fails (clang only)" + and filtering = CLOpt.mk_bool ~deprecated_no:["nf"] ~long:"filtering" ~short:'f' ~default:true ~in_help:CLOpt.[Report, manual_generic] @@ -839,16 +864,34 @@ and ( CLOpt.mk_bool ~long:"write-dotty" "Produce dotty files for specs in the results directory" in + + let set_debug_level level = + bo_debug := level; + debug_level_analysis := level; + debug_level_capture := level; + debug_level_linters := level in + let debug = CLOpt.mk_bool_group ~deprecated:["debug"] ~long:"debug" ~short:'g' - ~in_help:CLOpt.[Capture, manual_generic; Report, manual_generic; Run, manual_generic] - "Debug mode (also sets $(b,--developer-mode), $(b,--no-filtering), $(b,--print-buckets), \ - $(b,--print-types), $(b,--reports-include-ml-loc), $(b,--no-test), $(b,--trace-error), \ - $(b,--write-dotty), $(b,--write-html))" + ~in_help:all_generic_manuals + "Debug mode (also sets $(b,--debug-level 2), $(b,--developer-mode), $(b,--no-filtering), \ + $(b,--print-buckets), $(b,--print-types), $(b,--reports-include-ml-loc), $(b,--no-test), \ + $(b,--trace-error), $(b,--write-dotty), $(b,--write-html))" + ~f:(fun debug -> if debug then set_debug_level 2 else set_debug_level 0; debug) [developer_mode; print_buckets; print_types; reports_include_ml_loc; trace_error; write_html; write_dotty] [filtering; test] + and _ : int option ref = + CLOpt.mk_int_opt ~long:"debug-level" + ~in_help:all_generic_manuals ~meta:"level" + ~f:(fun level -> set_debug_level level; level) + "Debug level (sets $(b,--bo-debug) $(i,level), $(b,--debug-level-analysis) $(i,level), \ + $(b,--debug-level-capture) $(i,level), $(b,--debug-level-linters) $(i,level)):\ + \n - 0: only basic debugging enabled\ + \n - 1: verbose debugging enabled\ + \n - 2: very verbose debugging enabled" + and debug_exceptions = CLOpt.mk_bool_group ~long:"debug-exceptions" "Generate lightweight debugging information: just print the internal exceptions during \ @@ -879,14 +922,19 @@ and ( CLOpt.mk_bool_group ~long:"linters-developer-mode" ~in_help:CLOpt.[Capture, manual_clang_linters] "Debug mode for developing new linters. (Sets the analyzer to $(b,linters); also sets \ - $(b,--debug), $(b,--developer-mode), $(b,--print-logs), and \ + $(b,--debug), $(b,--debug-level-linters 2), $(b,--developer-mode), $(b,--print-logs), and \ unsets $(b,--allowed-failures) and $(b,--default-linters)." + ~f:(fun debug -> debug_level_linters := if debug then 2 else 0; debug) [debug; developer_mode; print_logs] [failures_allowed; default_linters] in ( + bo_debug, developer_mode, debug, debug_exceptions, + debug_level_analysis, + debug_level_capture, + debug_level_linters, default_linters, failures_allowed, filtering, @@ -902,6 +950,7 @@ and ( write_dotty ) + and dependencies = CLOpt.mk_bool ~deprecated:["dependencies"] ~long:"dependencies" ~in_help:CLOpt.[Capture, manual_java] @@ -1103,8 +1152,8 @@ and latex = "Write a latex report of the analysis results to a file" and log_file = - CLOpt.mk_path_opt ~deprecated:["out_file"; "-out-file"] ~long:"log-file" - ~meta:"file" "Specify the file to use for logging" + CLOpt.mk_string ~deprecated:["out_file"; "-out-file"] ~long:"log-file" + ~meta:"file" ~default:"logs" "Specify the file to use for logging" and linter = CLOpt.mk_string_opt ~long:"linter" ~in_help:CLOpt.[Capture, manual_clang_linters] @@ -1793,8 +1842,11 @@ and copy_propagation = !copy_propagation and crashcontext = !crashcontext and create_harness = !android_harness and cxx = !cxx -and debug_mode = !debug +and debug_level_analysis = !debug_level_analysis +and debug_level_capture = !debug_level_capture +and debug_level_linters = !debug_level_linters and debug_exceptions = !debug_exceptions +and debug_mode = !debug and dependency_mode = !dependencies and developer_mode = !developer_mode and disable_checks = !disable_checks diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 2eca81f7a..794788bf2 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -127,6 +127,7 @@ val patterns_never_returning_null : string * Yojson.Basic.json val patterns_skip_translation : string * Yojson.Basic.json val per_procedure_parallelism : bool val perf_stats_prefix : string +val pp_version : Format.formatter -> unit -> unit val proc_stats_filename : string val property_attributes : string val report : bool @@ -207,8 +208,11 @@ val copy_propagation : bool val crashcontext : bool val create_harness : bool val cxx : bool -val debug_mode : bool +val debug_level_analysis : int +val debug_level_capture : int +val debug_level_linters : int val debug_exceptions : bool +val debug_mode : bool val dependency_mode : bool val developer_mode : bool val disable_checks : string list @@ -276,7 +280,7 @@ val linters_def_file : string list val linters_def_folder : string list val linters_developer_mode : bool val load_analysis_results : string option -val log_file : string option +val log_file : string val makefile_cmdline : string val maven : bool val merge : bool diff --git a/infer/src/base/DB.ml b/infer/src/base/DB.ml index 523ccf56e..7331ec0a8 100644 --- a/infer/src/base/DB.ml +++ b/infer/src/base/DB.ml @@ -149,7 +149,7 @@ let update_file_with_lock dir fname update = let n = Unix.lseek fd 0L ~mode:Unix.SEEK_SET in if n <> 0L then begin - L.stderr "reset_file: lseek fail@."; + L.internal_error "reset_file: lseek fail@."; assert false end in Utils.create_dir dir; @@ -164,7 +164,7 @@ let update_file_with_lock dir fname update = Unix.lockf fd ~mode:Unix.F_ULOCK ~len:0L; Unix.close fd ) else ( - L.out "@.save_with_lock: fail on path: %s@." path; + L.internal_error "@\nsave_with_lock: fail on path: %s@." path; assert false ) diff --git a/infer/src/base/Epilogues.ml b/infer/src/base/Epilogues.ml index ebf99e406..235847a7d 100644 --- a/infer/src/base/Epilogues.ml +++ b/infer/src/base/Epilogues.ml @@ -27,7 +27,8 @@ let register ~f desc = try f () with exn -> - F.eprintf "Error while running epilogue %s:@ %a.@ Powering through...@." desc Exn.pp exn in + F.eprintf "Error while running epilogue \"%s\":@ %a.@ Powering through...@." + desc Exn.pp exn in (* We call `exit` in a bunch of places, so register the epilogues with [at_exit]. *) Pervasives.at_exit f_no_exn; (* Register signal masking. *) diff --git a/infer/src/base/Logging.ml b/infer/src/base/Logging.ml index 63d25dbd2..f2f803f77 100644 --- a/infer/src/base/Logging.ml +++ b/infer/src/base/Logging.ml @@ -13,97 +13,282 @@ open! IStd (** log messages at different levels of verbosity *) module F = Format + module CLOpt = CommandLineOption (* log files *) -let dup_formatter fmt1 fmt2 = - let (out_string1, flush1) = - Format.pp_get_formatter_output_functions fmt1 () in - let (out_string2, flush2) = - Format.pp_get_formatter_output_functions fmt2 () in - (* crude multiplexing; may cause garbled output if a formatter is shared between several - processes *) - let out_string s p n = out_string1 s p n; out_string2 s p n in - let flush () = flush1 (); flush2 () in - Format.pp_set_formatter_output_functions fmt1 out_string flush - -(** Name of dir for logging the output in the specific executable *) -let log_dir_of_command (command : CLOpt.command) = match command with - | Analyze -> "analyze" - | Capture | Clang | Compile -> "capture" - | Report -> "report" - | ReportDiff -> "reportdiff" - | Run -> "driver" - -let log_file = ( - lazy F.std_formatter, - lazy Pervasives.stderr, - lazy "out log file not initialized, stderr used instead" -) - -let close_log_file fmt chan file = - (* evaluating any of the three values will evaluate the rest *) - if Lazy.is_val fmt || Lazy.is_val chan || Lazy.is_val file then ( - F.pp_print_flush (Lazy.force fmt) () ; - let c = Lazy.force chan in - if c <> stdout && c <> stderr then +(* make a copy of [f] *) +let copy_formatter f = + let out_string, flush = F.pp_get_formatter_output_functions f () in + let out_funs = F.pp_get_formatter_out_functions f () in + let new_f = F.make_formatter out_string flush in + F.pp_set_formatter_out_functions new_f out_funs; + new_f + +(* Return a formatter that multiplexes to [fmt1] and [fmt2]. + + If [copy] is true then the formatter is created from a fresh copy of [fmt1]. + If [copy] is false then [fmt1] is mutated instead. *) +let dup_formatter ~copy fmt1 fmt2 = + let out_funs1 = F.pp_get_formatter_out_functions fmt1 () in + let out_funs2 = F.pp_get_formatter_out_functions fmt2 () in + let f = if copy then copy_formatter fmt1 else fmt1 in + F.pp_set_formatter_out_functions f { + F.out_string = (fun s p n -> out_funs1.out_string s p n; out_funs2.out_string s p n); + out_flush = (fun () -> out_funs1.out_flush (); out_funs2.out_flush ()); + out_newline = (fun () -> out_funs1.out_newline (); out_funs2.out_newline ()); + out_spaces = (fun n -> out_funs1.out_spaces n; out_funs2.out_spaces n); + }; + f + +(* should be set up to emit to a file later on; initially a string buffer so that logging is not + lost in the meantime *) +let log_file = + let b = Buffer.create 256 in + let f = F.formatter_of_buffer b in + if Config.print_logs then dup_formatter ~copy:false f F.err_formatter |> ignore; + ref (f, `Buffer b) + +type formatters = { + file : F.formatter; (** send to log file *) + console_file : F.formatter; (** send both to console and log file *) +} + +let logging_formatters = ref [] + +(* shared ref is less punishing to sloppy accounting of newlines *) +let is_newline = ref true +let prev_category = ref "" + +let mk_file_formatter category0 = + (* make a copy of file_fmt *) + let f = copy_formatter (fst !log_file) in + let out_functions_orig = F.pp_get_formatter_out_functions f () in + let prefix = Printf.sprintf "[%d][%s] " (Pid.to_int (Unix.getpid ())) category0 in + let print_prefix_if_newline () = + let category_has_changed = + (* take category + PID into account *) + not (phys_equal !prev_category prefix) in + if !is_newline || category_has_changed then ( + if not !is_newline && category_has_changed then + (* category change but previous line has not ended: print newline *) + out_functions_orig.out_newline (); + is_newline := false; + prev_category := prefix; + out_functions_orig.out_string prefix 0 (String.length prefix) + ) in + let out_string s p n = + print_prefix_if_newline (); + out_functions_orig.out_string s p n in + let out_newline () = + print_prefix_if_newline (); + out_functions_orig.out_newline (); + is_newline := true in + let out_spaces n = + print_prefix_if_newline (); + out_functions_orig.out_spaces n in + F.pp_set_formatter_out_functions f + { F.out_string; out_flush=out_functions_orig.out_flush; out_newline; out_spaces }; + f + +let register_formatter = + let all_prefixes = ref [] in + fun ?(use_stdout=false) prefix -> + all_prefixes := prefix::!all_prefixes; + (* lazy so that we get a chance to register all prefixes before computing their max length for + alignment purposes *) + lazy ( + let max_prefix = List.map ~f:String.length !all_prefixes |> List.fold_left ~f:max ~init:0 in + let fill = + let n = max_prefix - (String.length prefix) in + String.make n ' ' in + let justified_prefix = fill ^ prefix in + let mk_formatters () = + let file = mk_file_formatter justified_prefix in + let console_file = + let console = if use_stdout then F.std_formatter else F.err_formatter in + dup_formatter ~copy:true console file in + { file; console_file } in + let formatters = mk_formatters () in + let formatters_ref = ref formatters in + logging_formatters := ((formatters_ref, mk_formatters), formatters) + ::!logging_formatters; + formatters_ref + ) + +let flush_formatters {file; console_file} = + F.pp_print_flush file (); + F.pp_print_flush console_file () + +let reset_formatters () = + let refresh_formatter ((formatters_ref, mk_formatters), formatters) = + (* flush to be nice *) + flush_formatters formatters; + (* recreate formatters, in particular update PID info *) + formatters_ref := mk_formatters () in + let previous_formatters = !logging_formatters in + (* delete previous formatters *) + logging_formatters := []; + (* create new formatters *) + List.iter ~f:refresh_formatter previous_formatters; + if not !is_newline then F.pp_print_newline (fst !log_file) (); + is_newline := true + +let close_logs () = + let close_fmt (_, formatters) = flush_formatters formatters in + List.iter ~f:close_fmt !logging_formatters; + let fmt, chan = !log_file in + F.pp_print_flush fmt (); + match chan with + | `Buffer b -> + CLOpt.warnf + "WARNING: log file is still a temporary buffer, with contents %s" (Buffer.contents b) + | `Channel c -> Out_channel.close c - ) - -let create_log_file command name_prefix = - let log_dir = Config.results_dir ^/ Config.log_dir_name ^/ log_dir_of_command command in - let file = match Config.log_file with - | Some file -> - (* the command-line option takes precedence if specified *) - file - | None -> - log_dir ^/ name_prefix ^ ".log" in - Unix.mkdir_p log_dir ; - let chan = Pervasives.open_out_gen [Open_append; Open_creat] 0o666 file in - let file_fmt = F.formatter_of_out_channel chan in - F.fprintf file_fmt - "---- start logging from %d -------------------------------------------@." - (Pid.to_int (Unix.getpid ())); - if Config.print_logs then ( - dup_formatter file_fmt Format.err_formatter - ); - Epilogues.register - ~f:(fun () -> close_log_file (lazy file_fmt) (lazy chan) (lazy file)) - "log files flushing"; - (file_fmt, chan, file) - -let should_setup_log_files (command : CLOpt.command) = match command with - | Analyze | Capture | Clang | Compile -> - Config.debug_mode || Config.stats_mode - | Run -> - true - | Report | ReportDiff -> - false - -let setup_log_file command prefix_opt = - let lazy3 x = (lazy (fst3 (Lazy.force x)), - lazy (snd3 (Lazy.force x)), - lazy (trd3 (Lazy.force x))) in - if should_setup_log_files command then - let name_prefix = match prefix_opt with - | Some name -> name ^ "-" - | None -> "" in - lazy (create_log_file command name_prefix) |> lazy3 - else - log_file - -let (out_formatter, out_chan, out_file) = - let (o_fmt, o_c, o_f) = setup_log_file Config.command None in - (ref o_fmt, ref o_c, ref o_f) - -let set_log_file_identifier command prefix_opt = - let (o_fmt, o_c, o_f) = setup_log_file command prefix_opt in - (* close previous log files *) - close_log_file !out_formatter !out_chan !out_file; - out_formatter := o_fmt; out_chan := o_c; out_file := o_f - -let log_file_name () = Lazy.force !out_file + +let () = Epilogues.register ~f:close_logs "flushing logs and closing log file" + +let log ~to_console ?(to_file=true) (lazy formatters) = + match to_console, to_file with + | false, false -> + F.ifprintf F.std_formatter + | true, _ when not Config.print_logs -> + F.fprintf !formatters.console_file + | _ -> + (* to_console might be true, but in that case so is Config.print_logs so do not print to + stderr because it will get logs from the log file already *) + F.fprintf !formatters.file + +let debug_file_fmts = register_formatter "debug" +let environment_info_file_fmts = register_formatter "environment" +let external_warning_file_fmts = register_formatter "extern warn" +let external_error_file_fmts = register_formatter "extern err" +let internal_error_file_fmts = register_formatter "intern err" +let progress_file_fmts = register_formatter "progress" +let result_file_fmts = register_formatter ~use_stdout:true "result" +let user_warning_file_fmts = register_formatter "user warn" +let user_error_file_fmts = register_formatter "user err" + +let progress fmt = + log ~to_console:(not Config.quiet) progress_file_fmts fmt + +let progress_bar text = + log ~to_console:(Config.show_progress_bar && not Config.quiet) + ~to_file:true progress_file_fmts "%s@?" text + +let progressbar_file () = + progress_bar Config.log_analysis_file + +let progressbar_procedure () = + progress_bar Config.log_analysis_procedure + +let progressbar_timeout_event failure_kind = + if Config.stats_mode || Config.debug_mode then + begin + match failure_kind with + | SymOp.FKtimeout -> + progress_bar Config.log_analysis_wallclock_timeout + | SymOp.FKsymops_timeout _ -> + progress_bar Config.log_analysis_symops_timeout + | SymOp.FKrecursion_timeout _ -> + progress_bar Config.log_analysis_recursion_timeout + | SymOp.FKcrash msg -> + progress_bar (Printf.sprintf "%s(%s)" Config.log_analysis_crash msg) + end + +let user_warning fmt = + log ~to_console:(not Config.quiet) user_warning_file_fmts fmt + +let user_error fmt = + log ~to_console:(not Config.quiet) user_error_file_fmts fmt + +type debug_level = Quiet | Medium | Verbose [@@deriving compare] + +let debug_level_of_int n = + if n <= 0 then Quiet + else if Int.equal n 1 then Medium + else (* >= 2 *) Verbose + +let analysis_debug_level = debug_level_of_int Config.debug_level_analysis +let bufferoverrun_debug_level = debug_level_of_int Config.bo_debug +let capture_debug_level = debug_level_of_int Config.debug_level_capture +let linters_debug_level = debug_level_of_int Config.debug_level_linters +let mergecapture_debug_level = Quiet + +type debug_kind = + | Analysis + | BufferOverrun + | Capture + | Linters + | MergeCapture + +let debug kind level fmt = + let base_level = match kind with + | Analysis -> analysis_debug_level + | BufferOverrun -> bufferoverrun_debug_level + | Capture -> capture_debug_level + | Linters -> linters_debug_level + | MergeCapture -> mergecapture_debug_level in + let to_file = compare_debug_level level base_level <= 0 in + log ~to_console:false ~to_file debug_file_fmts fmt + +let result fmt = + log ~to_console:true result_file_fmts fmt + +let environment_info fmt = + log ~to_console:false environment_info_file_fmts fmt + +let external_warning fmt = + log ~to_console:(not Config.quiet) external_warning_file_fmts fmt + +let external_error fmt = + log ~to_console:(not Config.quiet) external_error_file_fmts fmt + +let internal_error fmt = + log ~to_console:(not Config.developer_mode) internal_error_file_fmts fmt + +(** Type of location in ml source: __POS__ *) +type ml_loc = string * int * int * int + +(** Convert a ml location to a string *) +let ml_loc_to_string (file, lnum, cnum, enum) = + Printf.sprintf "%s:%d:%d-%d:" file lnum cnum enum + +(** Pretty print a location of ml source *) +let pp_ml_loc fmt ml_loc = + F.fprintf fmt "%s" (ml_loc_to_string ml_loc) + +let pp_ml_loc_opt fmt ml_loc_opt = + if Config.developer_mode then match ml_loc_opt with + | None -> () + | Some ml_loc -> F.fprintf fmt "(%a)" pp_ml_loc ml_loc + +(* create new channel from the log file, and dumps the contents of the temporary log buffer there *) +let setup_log_file () = + match !log_file with + | _, `Channel _ -> + (* already set up *) + () + | _, `Buffer b -> + let fmt, chan, preexisting_logfile = + if Config.buck_cache_mode then + (* suppress log file in order not to cause flakiness in the Buck cache *) + let devnull_chan = open_out "/dev/null" in + let devnull_fmt = F.formatter_of_out_channel devnull_chan in + devnull_fmt, devnull_chan, true + else + (* assumes Config.results_dir exists already *) + let logfile_path = Config.results_dir ^/ Config.log_file in + let preexisting_logfile = PVariant.(=) (Sys.file_exists logfile_path) `Yes in + let chan = Pervasives.open_out_gen [Open_append; Open_creat] 0o666 logfile_path in + let file_fmt = F.formatter_of_out_channel chan in + if Config.print_logs then dup_formatter ~copy:false file_fmt F.err_formatter |> ignore; + file_fmt, chan, preexisting_logfile in + log_file := fmt, `Channel chan; + if preexisting_logfile then is_newline := false; + reset_formatters (); + Buffer.output_buffer chan b (** type of printable elements *) @@ -159,7 +344,7 @@ let printer_hook = ref (fun _ -> failwith "uninitialized printer hook") (** extend the current print log *) let add_print_action pact = if Config.write_html then delayed_actions := pact :: !delayed_actions - else if not Config.test then !printer_hook (Lazy.force !out_formatter) pact + else if not Config.test then !printer_hook (fst !log_file) pact (** reset the delayed print actions *) let reset_delayed_prints () = @@ -173,64 +358,6 @@ let get_delayed_prints () = let set_delayed_prints new_delayed_actions = delayed_actions := new_delayed_actions -let do_print (lazy fmt) = F.fprintf fmt - -let do_print_in_debug_or_stats_mode (lazy fmt) = - if Config.debug_mode || Config.stats_mode then - F.fprintf fmt - else - F.ifprintf fmt - -let do_print_in_debug_mode (lazy fmt) = - if Config.debug_mode then - F.fprintf fmt - else - F.ifprintf fmt - -let out fmt_string = - do_print_in_debug_or_stats_mode !out_formatter fmt_string - -let out_debug fmt_string = - do_print_in_debug_mode !out_formatter fmt_string - -let do_out fmt_string = - do_print !out_formatter fmt_string - -let stderr = F.eprintf - -let progress fmt_string = - if Config.quiet then F.ifprintf F.err_formatter fmt_string - else F.fprintf F.err_formatter fmt_string - -let stdout fmt_string = F.printf fmt_string - -(** Type of location in ml source: __POS__ *) -type ml_loc = string * int * int * int - -(** Convert a ml location to a string *) -let ml_loc_to_string (file, lnum, cnum, enum) = - Printf.sprintf "%s:%d:%d-%d:" file lnum cnum enum - -(** Pretty print a location of ml source *) -let pp_ml_loc fmt ml_loc = - F.fprintf fmt "%s" (ml_loc_to_string ml_loc) - -let pp_ml_loc_opt fmt ml_loc_opt = - if Config.developer_mode then match ml_loc_opt with - | None -> () - | Some ml_loc -> F.fprintf fmt "(%a)" pp_ml_loc ml_loc - -let assert_false ((file, lnum, cnum, _) as ml_loc) = - Printf.eprintf "\nASSERT FALSE %s\nCALL STACK\n%s\n%!" - (ml_loc_to_string ml_loc) - (Printexc.get_backtrace ()); - raise (Assert_failure (file, lnum, cnum)) - -(** print a warning with information of the position in the ml source where it oririnated. - use as: warning_position "description" __POS__; *) -let warning_position (s: string) (ml_loc: ml_loc) = - out "WARNING: %s in %a@." s pp_ml_loc_opt (Some ml_loc) - (** dump a string *) let d_str (s: string) = add_print_action (PTstr, Obj.repr s) @@ -268,27 +395,3 @@ let d_increase_indent (indent: int) = (** dump command to decrease the indentation level *) let d_decrease_indent (indent: int) = add_print_action (PTdecrease_indent, Obj.repr indent) - -let log_progress_simple text = - if Config.show_progress_bar && not Config.quiet then - F.fprintf F.err_formatter "%s@?" text - -let log_progress_file () = - log_progress_simple Config.log_analysis_file - -let log_progress_procedure () = - log_progress_simple Config.log_analysis_procedure - -let log_progress_timeout_event failure_kind = - if Config.stats_mode || Config.debug_mode then - begin - match failure_kind with - | SymOp.FKtimeout -> - log_progress_simple Config.log_analysis_wallclock_timeout - | SymOp.FKsymops_timeout _ -> - log_progress_simple Config.log_analysis_symops_timeout - | SymOp.FKrecursion_timeout _ -> - log_progress_simple Config.log_analysis_recursion_timeout - | SymOp.FKcrash msg -> - log_progress_simple (Printf.sprintf "%s(%s)" Config.log_analysis_crash msg) - end diff --git a/infer/src/base/Logging.mli b/infer/src/base/Logging.mli index 55de4d907..3278feae8 100644 --- a/infer/src/base/Logging.mli +++ b/infer/src/base/Logging.mli @@ -12,6 +12,70 @@ open! IStd (** log messages at different levels of verbosity *) +(** log information about the environment *) +val environment_info : ('a, Format.formatter, unit) format -> 'a + +(** print immediately to standard error unless --quiet is specified *) +val progress : ('a, Format.formatter, unit) format -> 'a + +(** Progress bar: start of the analysis of a file. *) +val progressbar_file : unit -> unit + +(** Progress bar: start of the analysis of a procedure. *) +val progressbar_procedure : unit -> unit + +(** Progress bar: log a timeout event if in developer mode. *) +val progressbar_timeout_event : SymOp.failure_kind -> unit + +(** Emit a result to stdout. Use only if the output format is stable and useful enough that it may + conceivably get piped to another program, ie, almost never (use [progress] instead otherwise). +*) +val result : ('a, Format.formatter, unit) format -> 'a + +(** bad input, etc. detected *) +val user_error : ('a, Format.formatter, unit) format -> 'a +val user_warning : ('a, Format.formatter, unit) format -> 'a + +(** huho, infer has a bug *) +val internal_error : ('a, Format.formatter, unit) format -> 'a + +(** some other tool has a bug or is called wrongly *) +val external_error : ('a, Format.formatter, unit) format -> 'a +val external_warning : ('a, Format.formatter, unit) format -> 'a + +(** *) +type debug_kind = Analysis | BufferOverrun | Capture | Linters | MergeCapture + +(** Level of verbosity for debug output. Each level enables all the levels before it. *) +type debug_level = + | Quiet (** innocuous, eg emitted once per toplevel execution *) + | Medium (** still fairly lightweight, eg emitted O() *) + | Verbose (** go crazy *) + +(** log debug info *) +val debug : debug_kind -> debug_level -> ('a, Format.formatter, unit) format -> 'a + +(** Type of location in ml source: __POS__ *) +type ml_loc = string * int * int * int + +(** Convert a ml location to a string *) +val ml_loc_to_string : ml_loc -> string + +(** Pretty print a location of ml source *) +val pp_ml_loc_opt : Format.formatter -> ml_loc option -> unit + + +(** log management *) + +(** Set up logging to go to the log file. Call this once the results directory has been set up. *) +val setup_log_file : unit -> unit + +(** Reset the formatters used for logging. Call this when you fork(2). *) +val reset_formatters : unit -> unit + + +(** Delayed printing (HTML debug, ...) *) + (** type of printable elements *) type print_type = | PTatom @@ -72,45 +136,6 @@ val set_delayed_prints : print_action list -> unit (** reset the delayed print actions *) val reset_delayed_prints : unit -> unit -(** Set a custom identifier to be part of the filename of the current logfiles. *) -val set_log_file_identifier : CommandLineOption.command -> string option -> unit - -(** print to the current out stream, as specified in set_log_file_identifier - (note: only prints in debug or in stats mode) *) -val out : ('a, Format.formatter, unit) format -> 'a - -(** print to the current out stream, as specified in set_log_file_identifier - (note: only prints in debug mode) *) -val out_debug : ('a, Format.formatter, unit) format -> 'a - -(** print to the current out stream, as specified in set_log_file_identifier *) -val do_out : ('a, Format.formatter, unit) format -> 'a - -(** print immediately to standard error *) -val stderr : ('a, Format.formatter, unit) format -> 'a - -(** print immediately to standard error unless --quiet is specified *) -val progress : ('a, Format.formatter, unit) format -> 'a - -(** print immediately to standard output *) -val stdout : ('a, Format.formatter, unit) format -> 'a - -(** Type of location in ml source: __POS__ *) -type ml_loc = string * int * int * int - -(** Convert a ml location to a string *) -val ml_loc_to_string : ml_loc -> string - -(** Pretty print a location of ml source *) -val pp_ml_loc_opt : Format.formatter -> ml_loc option -> unit - -(** Print stack trace and throw assert false *) -val assert_false : ml_loc -> 'a - -(** print a warning with information of the position in the ml source where it oririnated. - use as: warning_position "description" __POS__; *) -val warning_position: string -> ml_loc -> unit - (** dump a string *) val d_str : string -> unit @@ -143,15 +168,3 @@ val d_increase_indent : int -> unit (** dump command to decrease the indentation level *) val d_decrease_indent : int -> unit - -(** Progress bar: start of the analysis of a file. *) -val log_progress_file : unit -> unit - -(** Progress bar: start of the analysis of a procedure. *) -val log_progress_procedure : unit -> unit - -(** Progress bar: log a timeout event if in developer mode. *) -val log_progress_timeout_event : SymOp.failure_kind -> unit - -(** Name of current log file *) -val log_file_name : unit -> string diff --git a/infer/src/base/Process.ml b/infer/src/base/Process.ml index 194f144c6..1daab50ce 100644 --- a/infer/src/base/Process.ml +++ b/infer/src/base/Process.ml @@ -15,9 +15,7 @@ module F = Format found in that file, and exits, with default code 1 or a given code. *) let print_error_and_exit ?(exit_code=1) fmt = F.kfprintf (fun _ -> - L.do_out "%s" (F.flush_str_formatter ()); - let log_file = L.log_file_name () in - L.stderr "@\nAn error occured. Please find details in %s@\n@\n%!" log_file; + L.external_error "%s" (F.flush_str_formatter ()); exit exit_code ) F.str_formatter fmt @@ -31,7 +29,7 @@ let create_process_and_wait ~prog ~args = |> function | Ok () -> () | Error err as status -> - L.stderr "Error executing: %s@\n%s@\n" + L.external_error "Error executing: %s@\n%s@\n" (String.concat ~sep:" " (prog :: args)) (Unix.Exit_or_signal.to_string_hum status) ; exit (match err with `Exit_non_zero i -> i | `Signal _ -> 1) @@ -39,7 +37,7 @@ let create_process_and_wait ~prog ~args = represents, prints a message explaining the command and its status, if in debug or stats mode. It also prints a dot to show progress of jobs being finished. *) let print_status ~fail_on_failed_job f pid status = - L.out "%a%s@." + L.(debug Analysis Medium) "%a%s@." (fun fmt pid -> F.pp_print_string fmt (f pid)) pid (Unix.Exit_or_signal.to_string_hum status) ; L.progress ".%!"; @@ -98,7 +96,7 @@ let run_jobs_in_parallel ?(fail_on_failed_job=false) jobs_stack gen_prog prog_to done in run_job (); L.progress ".@."; - L.out "Waited for %d jobs" !waited_for_jobs + L.(debug Analysis Medium) "Waited for %d jobs" !waited_for_jobs let pipeline ~producer_prog ~producer_args ~consumer_prog ~consumer_args = let pipe_in, pipe_out = Unix.pipe () in diff --git a/infer/src/base/ProcessPool.ml b/infer/src/base/ProcessPool.ml index 9bbf22b10..ed76a9a89 100644 --- a/infer/src/base/ProcessPool.ml +++ b/infer/src/base/ProcessPool.ml @@ -8,7 +8,7 @@ *) open! IStd -(* Keep track of whether the current execution is in a child process *) +(** Keep track of whether the current execution is in a child process *) let in_child = ref false type t = diff --git a/infer/src/base/ProcessPool.mli b/infer/src/base/ProcessPool.mli index fe436dd23..594c97d7c 100644 --- a/infer/src/base/ProcessPool.mli +++ b/infer/src/base/ProcessPool.mli @@ -21,4 +21,5 @@ val start_child : f:('a -> unit) -> pool:t -> 'a -> unit (** Wait until all the currently executing processes terminate *) val wait_all : t -> unit +(** Keep track of whether the current execution is in a child process *) val in_child : bool ref diff --git a/infer/src/base/Serialization.ml b/infer/src/base/Serialization.ml index 7f80f0a8a..dd24b60a2 100644 --- a/infer/src/base/Serialization.ml +++ b/infer/src/base/Serialization.ml @@ -58,12 +58,14 @@ let create_serializer (key : Key.t) : 'a serializer = let read_data ((key': Key.t), (version': int), (value: 'a)) source_msg = if key <> key' then begin - L.stderr "Wrong key in when loading data from %s@\n" source_msg; + L.user_error "Wrong key in when loading data from %s -- are you running infer with results \ + coming from a previous version of infer?@\n" source_msg; None end else if version <> version' then begin - L.stderr "Wrong version in when loading data from %s@\n" source_msg; + L.user_error "Wrong version in when loading data from %s -- are you running infer with \ + results coming from a previous version of infer?@\n" source_msg; None end else Some value in diff --git a/infer/src/base/Utils.ml b/infer/src/base/Utils.ml index e4cee7d10..aa1f90eea 100644 --- a/infer/src/base/Utils.ml +++ b/infer/src/base/Utils.ml @@ -264,7 +264,7 @@ let realpath path = realpath | exception Unix.Unix_error (code, f, arg) -> F.eprintf - "WARNING: Failed to resolve file %s with \"%s\" \n@." arg (Unix.error_message code); + "WARNING: Failed to resolve file %s with \"%s\" @\n@." arg (Unix.error_message code); (* cache failures as well *) Hashtbl.add realpath_cache path (Error (code, f, arg)); raise (Unix.Unix_error (code, f, arg)) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index d71fe415a..d014babfe 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -38,10 +38,9 @@ struct let set_uninitialized node (typ : Typ.t) loc mem = match typ.desc with | Tint _ | Tfloat _ -> Dom.Mem.weak_update_heap loc Dom.Val.Itv.top mem | _ -> - if Config.bo_debug >= 3 then - L.out "/!\\ Do not know how to uninitialize type %a at %a@\n" - (Typ.pp Pp.text) typ - Location.pp (CFG.loc node); + L.(debug BufferOverrun Verbose) "/!\\ Do not know how to uninitialize type %a at %a@\n" + (Typ.pp Pp.text) typ + Location.pp (CFG.loc node); mem (* NOTE: heuristic *) @@ -65,9 +64,8 @@ struct |> Dom.Mem.add_stack (Loc.of_id id) v |> set_uninitialized node typ (Dom.Val.get_array_locs v) | _ -> - if Config.bo_debug >= 3 then - L.out "/!\\ Do not know where to model malloc at %a@\n" - Location.pp (CFG.loc node); + L.(debug BufferOverrun Verbose) "/!\\ Do not know where to model malloc at %a@\n" + Location.pp (CFG.loc node); mem let model_realloc @@ -81,9 +79,8 @@ struct | Some (id, _) -> Dom.Mem.add_stack (Loc.of_id id) value mem | None -> - if Config.bo_debug >= 3 then - L.out "/!\\ Do not know where to model value %a@\n" - Dom.Val.pp value; + L.(debug BufferOverrun Verbose) "/!\\ Do not know where to model value %a@\n" + Dom.Val.pp value; mem let model_infer_print @@ -91,10 +88,9 @@ struct = fun params mem loc -> match params with | (e, _) :: _ -> - if Config.bo_debug >= 1 then - L.out "@[=== Infer Print === at %a@,%a@]%!" - Location.pp loc - Dom.Val.pp (Sem.eval e mem loc); + L.(debug BufferOverrun Quiet) "@[=== Infer Print === at %a@,%a@]%!" + Location.pp loc + Dom.Val.pp (Sem.eval e mem loc); mem | _ -> mem @@ -129,10 +125,9 @@ struct | "__set_array_length" -> model_infer_set_array_length pname node params mem loc | "strlen" -> model_by_value Dom.Val.Itv.nat ret mem | proc_name -> - if Config.bo_debug >= 3 then - L.out "/!\\ Unknown call to %s at %a@\n" - proc_name - Location.pp loc; + L.(debug BufferOverrun Verbose) "/!\\ Unknown call to %s at %a@\n" + proc_name + Location.pp loc; model_by_value Dom.Val.Itv.top ret mem let rec declare_array @@ -191,10 +186,9 @@ struct in (Dom.Mem.add_heap field v mem, sym_num + 4) | _ -> - if Config.bo_debug >= 3 then - L.out "/!\\ decl_fld of unhandled type: %a at %a@." - (Typ.pp Pp.text) typ - Location.pp (CFG.loc node); + L.(debug BufferOverrun Verbose) "/!\\ decl_fld of unhandled type: %a at %a@." + (Typ.pp Pp.text) typ + Location.pp (CFG.loc node); (mem, sym_num) in match typ.Typ.desc with @@ -222,8 +216,8 @@ struct in (mem, inst_num + 1, sym_num) | _ -> - if Config.bo_debug >= 3 then - L.out "declare_symbolic_parameter of unhandled type: %a@." (Typ.pp Pp.text) typ; + L.(debug BufferOverrun Verbose) "declare_symbolic_parameter of unhandled type: %a@." + (Typ.pp Pp.text) typ; (mem, inst_num, sym_num) (* TODO: add other cases if necessary *) in List.fold ~f:add_formal ~init:(mem, inst_num, 0) (Sem.get_formals pdesc) @@ -248,16 +242,13 @@ struct let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.Mem.astate -> unit = fun instr pre post -> - if Config.bo_debug >= 2 then - begin - L.out "@\n@\n================================@\n"; - L.out "@[Pre-state : @,%a" Dom.Mem.pp pre; - L.out "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr; - L.out "@\n@\n"; - L.out "@[Post-state : @,%a" Dom.Mem.pp post; - L.out "@]@\n"; - L.out "================================@\n@." - end + L.(debug BufferOverrun Medium) "@\n@\n================================@\n"; + L.(debug BufferOverrun Medium) "@[Pre-state : @,%a" Dom.Mem.pp pre; + L.(debug BufferOverrun Medium) "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr; + L.(debug BufferOverrun Medium) "@\n@\n"; + L.(debug BufferOverrun Medium) "@[Post-state : @,%a" Dom.Mem.pp post; + L.(debug BufferOverrun Medium) "@]@\n"; + L.(debug BufferOverrun Medium) "================================@\n@." let exec_instr : Dom.Mem.astate -> extras ProcData.t -> CFG.node -> Sil.instr -> Dom.Mem.astate @@ -305,10 +296,9 @@ struct declare_symbolic_parameter pdesc tenv node inst_num mem | Call (_, fun_exp, _, loc, _) -> let () = - if Config.bo_debug >= 3 then - L.out "/!\\ Call to non-const function %a at %a" - Exp.pp fun_exp - Location.pp loc + L.(debug BufferOverrun Verbose) "/!\\ Call to non-const function %a at %a" + Exp.pp fun_exp + Location.pp loc in mem | Remove_temps _ @@ -355,11 +345,10 @@ struct let size = ArrayBlk.sizeof arr in let offset = ArrayBlk.offsetof arr in let idx = (if is_plus then Itv.plus else Itv.minus) offset idx in - (if Config.bo_debug >= 2 then - (L.out "@[Add condition :@,"; - L.out "array: %a@," ArrayBlk.pp arr; - L.out " idx: %a@," Itv.pp idx; - L.out "@]@.")); + L.(debug BufferOverrun Verbose) "@[Add condition :@,"; + L.(debug BufferOverrun Verbose) "array: %a@," ArrayBlk.pp arr; + L.(debug BufferOverrun Verbose) " idx: %a@," Itv.pp idx; + L.(debug BufferOverrun Verbose) "@]@."; if size <> Itv.bot && idx <> Itv.bot then Dom.ConditionSet.add_bo_safety pname loc site ~size ~idx cond_set else cond_set @@ -382,13 +371,12 @@ struct let print_debug_info : Sil.instr -> Dom.Mem.astate -> Dom.ConditionSet.t -> unit = fun instr pre cond_set -> - if Config.bo_debug >= 2 then - (L.out "@\n@\n================================@\n"; - L.out "@[Pre-state : @,%a" Dom.Mem.pp pre; - L.out "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr; - L.out "@[@\n@\n%a" Dom.ConditionSet.pp cond_set; - L.out "@]@\n"; - L.out "================================@\n@.") + L.(debug BufferOverrun Verbose) "@\n@\n================================@\n"; + L.(debug BufferOverrun Verbose) "@[Pre-state : @,%a" Dom.Mem.pp pre; + L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr; + L.(debug BufferOverrun Verbose) "@[@\n@\n%a" Dom.ConditionSet.pp cond_set; + L.(debug BufferOverrun Verbose) "@]@\n"; + L.(debug BufferOverrun Verbose) "================================@\n@." let is_last_statement_of_if_branch rem_instrs node = if rem_instrs <> [] then false @@ -512,7 +500,7 @@ let compute_post let print_summary : Typ.Procname.t -> Dom.Summary.t -> unit = fun proc_name s -> - L.out "@\n@[Summary of %a :@,%a@]@." + L.(debug BufferOverrun Medium) "@\n@[Summary of %a :@,%a@]@." Typ.Procname.pp proc_name Dom.Summary.pp_summary s diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index b0b1221d2..a84b875fe 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -663,8 +663,7 @@ struct then strong_update_heap ploc v s else let () = - if Config.bo_debug >= 3 then - L.out "Weak update for %a <- %a@." PowLoc.pp ploc Val.pp v + L.(debug BufferOverrun Verbose) "Weak update for %a <- %a@." PowLoc.pp ploc Val.pp v in weak_update_heap ploc v s end diff --git a/infer/src/checkers/Stacktrace.ml b/infer/src/checkers/Stacktrace.ml index 1cb5d24ad..e786090e1 100644 --- a/infer/src/checkers/Stacktrace.ml +++ b/infer/src/checkers/Stacktrace.ml @@ -111,5 +111,5 @@ let of_json_file filename = try of_json filename (Yojson.Basic.from_file filename) with Sys_error msg | Yojson.Json_error msg -> - failwithf "Could not read or parse the supplied JSON stacktrace file %s :\n %s" + failwithf "Could not read or parse the supplied JSON stacktrace file %s :@\n %s" filename msg diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 62449c001..cb777ef53 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -932,7 +932,7 @@ let calculate_addendum_message tenv pname = if not (List.mem ~equal:Typ.Name.equal thread_safe_annotated_classes current_class) then match thread_safe_annotated_classes with | hd::_ -> - F.asprintf "\n Note: Superclass %a is marked %a." + F.asprintf "@\n Note: Superclass %a is marked %a." (MF.wrap_monospaced Typ.Name.pp) hd MF.pp_monospaced "@ThreadSafe" | [] -> "" diff --git a/infer/src/checkers/checkers.ml b/infer/src/checkers/checkers.ml index f06ddebcd..8e5405941 100644 --- a/infer/src/checkers/checkers.ml +++ b/infer/src/checkers/checkers.ml @@ -14,8 +14,6 @@ open! IStd module L = Logging module F = Format -let verbose = ref true - (** Convenience functions for checkers to print information *) module PP = struct (** Print a range of lines of the source file in [loc], including [nbefore] lines before loc @@ -111,14 +109,11 @@ module ST = struct if not suppressed then begin - if !verbose then - begin - L.stdout "%s: %a: %s@." - (Localise.to_issue_id kind) - SourceFile.pp loc.Location.file - (Typ.Procname.to_string proc_name); - L.stdout "%s@." description - end; + L.progress "%s: %a: %s@\n" + (Localise.to_issue_id kind) + SourceFile.pp loc.Location.file + (Typ.Procname.to_string proc_name); + L.progress "%s@." description; Reporting.log_error proc_name ~loc ~ltr:trace exn end end diff --git a/infer/src/checkers/constantPropagation.ml b/infer/src/checkers/constantPropagation.ml index 36fa30f8e..ac0ffa0b3 100644 --- a/infer/src/checkers/constantPropagation.ml +++ b/infer/src/checkers/constantPropagation.ml @@ -110,10 +110,10 @@ module ConstantFlow = Dataflow.MakeDF(struct if verbose then begin - L.stdout "Node %i:" (Procdesc.Node.get_id node :> int); - L.stdout "%a" pp constants; + L.(debug Analysis Verbose) "Node %i:" (Procdesc.Node.get_id node :> int); + L.(debug Analysis Verbose) "%a" pp constants; List.iter - ~f:(fun instr -> L.stdout "%a@." (Sil.pp_instr Pp.text) instr) + ~f:(fun instr -> L.(debug Analysis Verbose) "%a@." (Sil.pp_instr Pp.text) instr) (Procdesc.Node.get_instrs node) end; let constants = @@ -121,7 +121,7 @@ module ConstantFlow = Dataflow.MakeDF(struct ~f:do_instr ~init:constants (Procdesc.Node.get_instrs node) in - if verbose then L.stdout "%a\n@." pp constants; + if verbose then L.(debug Analysis Verbose) "%a@\n@." pp constants; [constants], [constants] end) diff --git a/infer/src/checkers/dataflow.ml b/infer/src/checkers/dataflow.ml index c37f9f493..b2896fc76 100644 --- a/infer/src/checkers/dataflow.ml +++ b/infer/src/checkers/dataflow.ml @@ -82,7 +82,6 @@ let node_throws pdesc node (proc_throws : Typ.Procname.t -> throws) : throws = module MakeDF(St: DFStateType) : DF with type state = St.t = struct module S = Procdesc.NodeSet module H = Procdesc.NodeHash - module N = Procdesc.Node type worklist = S.t type statemap = St.t H.t @@ -178,7 +177,8 @@ let callback_test_dataflow { Callbacks.proc_desc; tenv; summary } = let equal = Int.equal let join n m = if Int.equal n 0 then m else n let do_node _ n s = - if verbose then L.stdout "visiting node %a with state %d@." Procdesc.Node.pp n s; + if verbose then + L.(debug Analysis Verbose) "visiting node %a with state %d@." Procdesc.Node.pp n s; [s + 1], [s + 1] let proc_throws _ = DoesNotThrow end) in diff --git a/infer/src/checkers/printfArgs.ml b/infer/src/checkers/printfArgs.ml index 6cb94df7b..2084290b6 100644 --- a/infer/src/checkers/printfArgs.ml +++ b/infer/src/checkers/printfArgs.ml @@ -198,7 +198,7 @@ let check_printf_args_ok tenv cl "Format string must be string literal" with e -> - L.stderr + L.internal_error "%s Exception when analyzing %s: %s@." (Localise.to_issue_id Localise.checkers_printf_args) (Typ.Procname.to_string proc_name) diff --git a/infer/src/clang/ALVar.ml b/infer/src/clang/ALVar.ml index e7743c042..d9df9a82f 100644 --- a/infer/src/clang/ALVar.ml +++ b/infer/src/clang/ALVar.ml @@ -8,6 +8,8 @@ *) open! IStd +module L = Logging + type keyword = | Report_when | Message @@ -96,7 +98,7 @@ let compare_str_with_alexp s ae = | Regexp re -> str_match_regex s re | _ -> - Logging.out "[WARNING]: ALVAR expression '%s' is not a constant/var or regexp\n" + L.(debug Linters Medium) "[WARNING]: ALVAR expression '%s' is not a constant/var or regexp@\n" (alexp_to_string ae); false diff --git a/infer/src/clang/CType.ml b/infer/src/clang/CType.ml index 37891499d..04ae1100f 100644 --- a/infer/src/clang/CType.ml +++ b/infer/src/clang/CType.ml @@ -26,7 +26,7 @@ let objc_classname_of_type typ = | Typ.Tstruct name -> name | Typ.Tfun _ -> Typ.Name.Objc.from_string CFrontend_config.objc_object | _ -> - Logging.out_debug + L.(debug Capture Verbose) "Classname of type cannot be extracted in type %s" (Typ.to_string typ); Typ.Name.Objc.from_string "undefined" @@ -45,11 +45,11 @@ let rec return_type_of_function_qual_type (qual_type : Clang_ast_t.qual_type) = | Some BlockPointerType (_, in_qual) -> return_type_of_function_qual_type in_qual | Some _ -> - L.out_debug "Warning: Type pointer %s is not a function type." + L.(debug Capture Verbose) "Warning: Type pointer %s is not a function type." (Clang_ast_extend.type_ptr_to_string qual_type.qt_type_ptr); {qual_type with qt_type_ptr=Clang_ast_extend.ErrorType} | None -> - L.out_debug "Warning: Type pointer %s not found." + L.(debug Capture Verbose) "Warning: Type pointer %s not found." (Clang_ast_extend.type_ptr_to_string qual_type.qt_type_ptr); {qual_type with qt_type_ptr=Clang_ast_extend.ErrorType} @@ -79,9 +79,10 @@ let get_name_from_type_pointer custom_type_pointer = let rec get_type_list nn ll = match ll with | [] -> [] - | (n, t):: ll' -> (* Logging.out_debug ">>>>>Searching for type '%s'. Seen '%s'.@." nn n; *) + | (n, t):: ll' -> + (* L.(debug Capture Verbose) ">>>>>Searching for type '%s'. Seen '%s'.@." nn n; *) if n = nn then ( - Logging.out_debug ">>>>>>>>>>>>>>>>>>>>>>>NOW Found, Its type is: '%s'@." + L.(debug Capture Verbose) ">>>>>>>>>>>>>>>>>>>>>>>NOW Found, Its type is: '%s'@." (Typ.to_string t); [t] ) else get_type_list nn ll' diff --git a/infer/src/clang/Capture.re b/infer/src/clang/Capture.re index 5824bc0bf..df33c81a5 100644 --- a/infer/src/clang/Capture.re +++ b/infer/src/clang/Capture.re @@ -10,6 +10,8 @@ open! IStd; module CLOpt = CommandLineOption; +module L = Logging; + /** enable debug mode (to get more data saved to disk for future inspections) */ let debug_mode = Config.debug_mode || Config.frontend_stats || Config.frontend_debug; @@ -22,7 +24,7 @@ let catch_biniou_buffer_errors f x => /* suppress warning: allow this one case because we're just reraising the error with another error message so it doesn't really matter if this eventually fails */ | Invalid_argument "Bi_inbuf.refill_from_channel" => - Logging.out "WARNING: biniou buffer too short, skipping the file@\n"; + L.external_error "WARNING: biniou buffer too short, skipping the file@\n"; assert false } ) @@ -47,8 +49,8 @@ let register_perf_stats_report source_file => { }; let init_global_state_for_capture_and_linters source_file => { - Logging.set_log_file_identifier - CLOpt.Clang (Some (Filename.basename (SourceFile.to_abs_path source_file))); + L.(debug Capture Medium) + "Processing %s" (Filename.basename (SourceFile.to_abs_path source_file)); register_perf_stats_report source_file; Config.curr_language := Config.Clang; DB.Results_dir.init source_file; @@ -59,7 +61,7 @@ let run_clang_frontend ast_source => { let init_time = Unix.gettimeofday (); let print_elapsed () => { let elapsed = Unix.gettimeofday () -. init_time; - Logging.out "Elapsed: %07.3f seconds.@\n" elapsed + L.(debug Capture Quiet) "Elapsed: %07.3f seconds.@\n" elapsed }; let ast_decl = switch ast_source { @@ -90,8 +92,8 @@ let run_clang_frontend ast_source => { Format.fprintf fmt "stdin of %a" SourceFile.pp trans_unit_ctx.CFrontend_config.source_file }; ClangPointers.populate_all_tables ast_decl; - Logging.out "Clang frontend action is %s@\n" Config.clang_frontend_action_string; - Logging.out + L.(debug Capture Quiet) "Clang frontend action is %s@\n" Config.clang_frontend_action_string; + L.(debug Capture Medium) "Start %s of AST from %a@\n" Config.clang_frontend_action_string pp_ast_filename ast_source; if Config.clang_frontend_do_lint { CFrontend_checkers_main.do_frontend_checks trans_unit_ctx ast_decl @@ -99,7 +101,7 @@ let run_clang_frontend ast_source => { if Config.clang_frontend_do_capture { CFrontend.do_source_file trans_unit_ctx ast_decl }; - Logging.out "End translation AST file %a... OK!@\n" pp_ast_filename ast_source; + L.(debug Capture Medium) "End translation AST file %a... OK!@\n" pp_ast_filename ast_source; print_elapsed () }; @@ -113,7 +115,7 @@ let run_and_validate_clang_frontend ast_source => let run_clang clang_command read => { let exit_with_error exit_code => { - Logging.stderr + L.external_error "Error: the following clang command did not run successfully:@\n %s@\n" clang_command; exit exit_code }; @@ -156,18 +158,19 @@ let cc1_capture clang_cmd => { /* the source file is always the last argument of the original -cc1 clang command */ Utils.filename_to_absolute ::root orig_argv.(Array.length orig_argv - 1) }; - Logging.out "@\n*** Beginning capture of file %s ***@\n" source_path; + L.(debug Capture Quiet) "@\n*** Beginning capture of file %s ***@\n" source_path; if ( Config.equal_analyzer Config.analyzer Config.CompileOnly || not Config.skip_analysis_in_path_skips_compilation && CLocation.is_file_blacklisted source_path ) { - Logging.out "@\n Skip the analysis of source file %s@\n@\n" source_path; + L.(debug Capture Quiet) "@\n Skip the analysis of source file %s@\n@\n" source_path; /* We still need to run clang, but we don't have to attach the plugin. */ run_clang (ClangCommand.command_to_run clang_cmd) Utils.consume_in } else if ( Config.skip_analysis_in_path_skips_compilation && CLocation.is_file_blacklisted source_path ) { - Logging.out "@\n Skip compilation and analysis of source file %s@\n@\n" source_path; + L.(debug Capture Quiet) + "@\n Skip compilation and analysis of source file %s@\n@\n" source_path; () } else { switch Config.clang_biniou_file { @@ -176,8 +179,6 @@ let cc1_capture clang_cmd => { run_plugin_and_frontend source_path (fun chan_in => run_and_validate_clang_frontend (`Pipe chan_in)) clang_cmd }; - /* reset logging to stop capturing log output into the source file's log */ - Logging.set_log_file_identifier CLOpt.Capture None; () } }; @@ -192,6 +193,6 @@ let capture clang_cmd => further since `clang -### ...` will only output commands that invoke binaries using their absolute paths. */ let command_to_run = ClangCommand.command_to_run clang_cmd; - Logging.out "Running non-cc command without capture: %s@\n" command_to_run; + L.(debug Capture Quiet) "Running non-cc command without capture: %s@\n" command_to_run; run_clang command_to_run Utils.consume_in }; diff --git a/infer/src/clang/ClangCommand.re b/infer/src/clang/ClangCommand.re index 31f4b40a1..7c4710e3f 100644 --- a/infer/src/clang/ClangCommand.re +++ b/infer/src/clang/ClangCommand.re @@ -8,6 +8,8 @@ */ open! IStd; +module L = Logging; + type t = { exec: string, argv: list string, @@ -57,7 +59,7 @@ let can_attach_ast_exporter cmd => { let is_supported_language cmd => switch (value_of_option cmd "-x") { | None => - Logging.stderr "malformed -cc1 command has no \"-x\" flag!"; + L.external_warning "malformed -cc1 command has no \"-x\" flag!"; false | Some lang when String.is_prefix prefix::"assembler" lang => false | Some _ => true @@ -116,7 +118,7 @@ let clang_cc1_cmd_sanitizer cmd => { arg }; let args_defines = - if (Config.bufferoverrun) { + if Config.bufferoverrun { ["-D__INFER_BUFFEROVERRUN"] } else { [] diff --git a/infer/src/clang/ClangWrapper.re b/infer/src/clang/ClangWrapper.re index 318c4f2e7..ee9c166ae 100644 --- a/infer/src/clang/ClangWrapper.re +++ b/infer/src/clang/ClangWrapper.re @@ -12,6 +12,8 @@ commands by our own clang with our plugin attached for each source file. */ open! IStd; +module L = Logging; + type action_item = | Command ClangCommand.t | ClangError string @@ -77,7 +79,7 @@ let normalize ::prog ::args :list action_item => { "-Wno-ignored-optimization-argument" ] |> ClangCommand.command_to_run ); - Logging.out "clang -### invocation: %s@\n" clang_hashhashhash; + L.(debug Capture Medium) "clang -### invocation: %s@\n" clang_hashhashhash; let normalized_commands = ref []; let one_line line => if (String.is_prefix prefix::" \"" line) { @@ -128,7 +130,7 @@ let exec_action_item = failwithf "@\n*** ERROR: Failed to execute compilation command. Output:@\n%s@\n*** Infer needs a working compilation command to run.@." error - | ClangWarning warning => Logging.stderr "%s@\n" warning + | ClangWarning warning => L.external_warning "%s@\n" warning | Command clang_cmd => Capture.capture clang_cmd; let exe ::prog ::args => { @@ -143,7 +145,7 @@ let exe ::prog ::args => { switch Config.fcp_apple_clang { | Some bin => let bin_xx = bin ^ xx_suffix; - Logging.out "Will run Apple clang %s" bin_xx; + L.(debug Capture Medium) "Will run Apple clang %s" bin_xx; (bin_xx, true) | None => (clang_xx, false) }; @@ -158,7 +160,7 @@ let exe ::prog ::args => { - the user tries to run `infer -- clang -c file_that_does_not_exist.c`. In this case, this will fail with the appropriate error message from clang instead of silently analyzing 0 files. */ - Logging.out + L.(debug Capture Quiet) "WARNING: `clang -### ` returned an empty set of commands to run and no error. Will run the original command directly:@\n %s@\n" (String.concat sep::" " @@ [prog, ...args]) }; diff --git a/infer/src/clang/ast_expressions.ml b/infer/src/clang/ast_expressions.ml index a6062a08b..f64fd8cb5 100644 --- a/infer/src/clang/ast_expressions.ml +++ b/infer/src/clang/ast_expressions.ml @@ -7,9 +7,11 @@ * of patent rights can be found in the PATENTS file in the same directory. *) +(** This module creates extra ast constructs that are needed for the translation *) + open! IStd -(** This module creates extra ast constructs that are needed for the translation *) +module L = Logging let dummy_source_range () = let dummy_source_loc = { @@ -562,7 +564,7 @@ let translate_block_enumerate block_name stmt_info stmt_list ei = let translated_stmt, op = translate bdi.bdi_parameters s block_decl bei.ei_qual_type in CompoundStmt (stmt_info, translated_stmt), vars_to_register @ op @ bv | _ -> (* When it is not the method we expect with only one parameter, we don't translate *) - Logging.out_debug "WARNING: Block Enumeration called at %s not translated." + L.(debug Capture Verbose) "WARNING: Block Enumeration called at %s not translated." (Clang_ast_j.string_of_stmt_info stmt_info); CompoundStmt (stmt_info, stmt_list), [] diff --git a/infer/src/clang/cArithmetic_trans.ml b/infer/src/clang/cArithmetic_trans.ml index 031c41568..619c6133a 100644 --- a/infer/src/clang/cArithmetic_trans.ml +++ b/infer/src/clang/cArithmetic_trans.ml @@ -7,9 +7,11 @@ * of patent rights can be found in the PATENTS file in the same directory. *) +(** Utility module for translating unary and binary operations and compound assignments *) + open! IStd -(** Utility module for translating unary and binary operations and compound assignments *) +module L = Logging (* Returns the translation of assignment when ARC mode is enabled in Obj-C *) (* For __weak and __unsafe_unretained the translation is the same as non-ARC *) @@ -129,8 +131,8 @@ let binary_operation_instruction boi e1 typ e2 loc rhs_owning_method = (* We should not get here. *) (* These should be treated by compound_assignment_binary_operation_instruction*) | bok -> - Logging.out - "\nWARNING: Missing translation for Binary Operator Kind %s. Construct ignored...\n" + L.(debug Capture Medium) + "@\nWARNING: Missing translation for Binary Operator Kind %s. Construct ignored...@\n" (Clang_ast_j.string_of_binary_operator_kind bok); (Exp.minus_one, []) @@ -176,8 +178,10 @@ let unary_operation_instruction translation_unit_context uoi e typ loc = | `AddrOf -> (e, []) | `Real | `Imag | `Extension | `Coawait -> let uok = Clang_ast_j.string_of_unary_operator_kind (uoi.Clang_ast_t.uoi_kind) in - Logging.out - "\nWARNING: Missing translation for Unary Operator Kind %s. The construct has been ignored...\n" uok; + L.(debug Capture Medium) + "@\nWARNING: Missing translation for Unary Operator Kind %s. \ + The construct has been ignored...@\n" + uok; (e, []) let bin_op_to_string boi = diff --git a/infer/src/clang/cAst_utils.ml b/infer/src/clang/cAst_utils.ml index 2844155d7..effd8613d 100644 --- a/infer/src/clang/cAst_utils.ml +++ b/infer/src/clang/cAst_utils.ml @@ -62,7 +62,7 @@ let type_from_unary_expr_or_type_trait_expr_info info = let get_decl decl_ptr = let decl = Int.Table.find ClangPointers.pointer_decl_table decl_ptr in - if Option.is_none decl then Logging.out "decl with pointer %d not found\n" decl_ptr; + if Option.is_none decl then L.internal_error "decl with pointer %d not found@\n" decl_ptr; decl let get_decl_opt decl_ptr_opt = @@ -72,7 +72,7 @@ let get_decl_opt decl_ptr_opt = let get_stmt stmt_ptr = let stmt = Int.Table.find ClangPointers.pointer_stmt_table stmt_ptr in - if Option.is_none stmt then Logging.out "stmt with pointer %d not found\n" stmt_ptr; + if Option.is_none stmt then L.internal_error "stmt with pointer %d not found\n" stmt_ptr; stmt let get_stmt_opt stmt_ptr_opt = @@ -87,7 +87,7 @@ let get_decl_opt_with_decl_ref decl_ref_opt = let get_property_of_ivar decl_ptr = let decl = Int.Table.find ClangPointers.ivar_to_property_table decl_ptr in - if Option.is_none decl then Logging.out "property with pointer %d not found\n" decl_ptr; + if Option.is_none decl then L.internal_error "property with pointer %d not found\n" decl_ptr; decl let update_sil_types_map type_ptr sil_type = @@ -114,12 +114,12 @@ let get_type type_ptr = match type_ptr with | Clang_ast_types.TypePtr.Ptr raw_ptr -> let typ = Int.Table.find ClangPointers.pointer_type_table raw_ptr in - if Option.is_none typ then Logging.out "type with pointer %d not found\n" raw_ptr; + if Option.is_none typ then L.internal_error "type with pointer %d not found\n" raw_ptr; typ | _ -> (* otherwise, function fails *) let type_str = Clang_ast_extend.type_ptr_to_string type_ptr in - Logging.out "type %s is not clang pointer\n" type_str; + L.(debug Capture Medium) "type %s is not clang pointer@\n" type_str; None let get_desugared_type type_ptr = diff --git a/infer/src/clang/cField_decl.ml b/infer/src/clang/cField_decl.ml index 6e8cb83e3..03861d1e8 100644 --- a/infer/src/clang/cField_decl.ml +++ b/infer/src/clang/cField_decl.ml @@ -16,7 +16,8 @@ module L = Logging type field_type = Fieldname.t * Typ.t * (Annot.t * bool) list let rec get_fields_super_classes tenv super_class = - Logging.out_debug " ... Getting fields of superclass '%s'\n" (Typ.Name.to_string super_class); + L.(debug Capture Verbose) " ... Getting fields of superclass '%s'@\n" + (Typ.Name.to_string super_class); match Tenv.lookup tenv super_class with | None -> [] | Some { fields; supers = super_class :: _ } -> @@ -83,7 +84,8 @@ let add_missing_fields tenv class_name missing_fields = | Some ({ fields } as struct_typ) -> let new_fields = CGeneral_utils.append_no_duplicates_fields fields missing_fields in ignore (Tenv.mk_struct tenv ~default:struct_typ ~fields:new_fields ~statics:[] class_tn_name); - Logging.out_debug " Updating info for class '%a' in tenv\n" QualifiedCppName.pp class_name + L.(debug Capture Verbose) " Updating info for class '%a' in tenv@\n" + QualifiedCppName.pp class_name | _ -> () let modelled_fields_in_classes = diff --git a/infer/src/clang/cFrontend.ml b/infer/src/clang/cFrontend.ml index deab5694e..4ed15a054 100644 --- a/infer/src/clang/cFrontend.ml +++ b/infer/src/clang/cFrontend.ml @@ -22,13 +22,13 @@ let compute_icfg trans_unit_ctx tenv ast = match ast with | Clang_ast_t.TranslationUnitDecl(_, decl_list, _, _) -> CFrontend_config.global_translation_unit_decls := decl_list; - Logging.out_debug "@\n Start creating icfg@\n"; + L.(debug Capture Verbose) "@\n Start creating icfg@\n"; let cg = Cg.create trans_unit_ctx.CFrontend_config.source_file in let cfg = Cfg.create_cfg () in List.iter ~f:(CFrontend_declImpl.translate_one_declaration trans_unit_ctx tenv cg cfg `DeclTraversal) decl_list; - Logging.out_debug "\n Finished creating icfg\n"; + L.(debug Capture Verbose) "@\n Finished creating icfg@\n"; (cg, cfg) | _ -> assert false (* NOTE: Assumes that an AST alsways starts with a TranslationUnitDecl *) @@ -42,10 +42,10 @@ let do_source_file translation_unit_context ast = CType_decl.add_predefined_types tenv; init_global_state_capture (); let source_file = translation_unit_context.CFrontend_config.source_file in - Logging.out_debug "@\n Start building call/cfg graph for '%a'....@\n" + L.(debug Capture Verbose) "@\n Start building call/cfg graph for '%a'....@\n" SourceFile.pp source_file; let call_graph, cfg = compute_icfg translation_unit_context tenv ast in - Logging.out_debug "@\n End building call/cfg graph for '%a'.@\n" + L.(debug Capture Verbose) "@\n End building call/cfg graph for '%a'.@\n" SourceFile.pp source_file; (* This part below is a boilerplate in every frontends. *) (* This could be moved in the cfg_infer module *) @@ -68,6 +68,6 @@ let do_source_file translation_unit_context ast = || Option.is_some Config.icfg_dotty_outfile then (Dotty.print_icfg_dotty source_file cfg; Cg.save_call_graph_dotty source_file call_graph); - Logging.out_debug "%a" Cfg.pp_proc_signatures cfg; + L.(debug Capture Verbose) "%a" Cfg.pp_proc_signatures cfg; (* NOTE: nothing should be written to source_dir after this *) DB.mark_file_updated (DB.source_dir_to_string source_dir) diff --git a/infer/src/clang/cFrontend_checkers_main.ml b/infer/src/clang/cFrontend_checkers_main.ml index dfe11acc3..0b79e7db5 100644 --- a/infer/src/clang/cFrontend_checkers_main.ml +++ b/infer/src/clang/cFrontend_checkers_main.ml @@ -8,9 +8,12 @@ *) open! IStd + open Lexing open Ctl_lexer +module L = Logging + let parse_al_file fname channel : CTL.al_file option = let pos_str lexbuf = let pos = lexbuf.lex_curr_p in @@ -39,18 +42,18 @@ let rec parse_import_file import_file channel : CTL.clause list = | Some {import_files = imports; global_macros = curr_file_macros; checkers = _} -> already_imported_files := import_file :: !already_imported_files; collect_all_macros imports curr_file_macros - | None -> Logging.out "No macros found.\n";[]) + | None -> L.(debug Linters Medium) "No macros found.@\n";[]) and collect_all_macros imports curr_file_macros = - Logging.out "#### Start parsing import macros #####\n"; + L.(debug Linters Medium) "#### Start parsing import macros #####@\n"; let import_macros = parse_imports imports in - Logging.out "#### Add global macros to import macros #####\n"; + L.(debug Linters Medium) "#### Add global macros to import macros #####@\n"; List.append import_macros curr_file_macros (* Parse import files with macro definitions, and it returns a list of LET clauses *) and parse_imports imports_files : CTL.clause list = let parse_one_import_file fimport macros = - Logging.out " Loading import macros from file %s\n" fimport; + L.(debug Linters Medium) " Loading import macros from file %s@\n" fimport; let in_channel = open_in fimport in let parsed_macros = parse_import_file fimport in_channel in In_channel.close in_channel; @@ -63,17 +66,17 @@ let parse_ctl_file linters_def_file channel : CFrontend_errors.linter list = already_imported_files := [linters_def_file]; let macros = collect_all_macros imports curr_file_macros in let macros_map = CFrontend_errors.build_macros_map macros in - Logging.out "#### Start Expanding checkers #####\n"; + L.(debug Linters Medium) "#### Start Expanding checkers #####@\n"; let exp_checkers = CFrontend_errors.expand_checkers macros_map parsed_checkers in - Logging.out "#### Checkers Expanded #####\n"; + L.(debug Linters Medium) "#### Checkers Expanded #####@\n"; if Config.debug_mode then List.iter ~f:CTL.print_checker exp_checkers; CFrontend_errors.create_parsed_linters linters_def_file exp_checkers - | None -> Logging.out "No linters found.\n";[] + | None -> L.(debug Linters Medium) "No linters found.@\n";[] (* Parse the files with linters definitions, and it returns a list of linters *) let parse_ctl_files linters_def_files : CFrontend_errors.linter list = let collect_parsed_linters linters_def_file linters = - Logging.out "Loading linters rules from %s\n" linters_def_file; + L.(debug Linters Medium) "Loading linters rules from %s@\n" linters_def_file; let in_channel = open_in linters_def_file in let parsed_linters = parse_ctl_file linters_def_file in_channel in In_channel.close in_channel; @@ -267,7 +270,7 @@ let linters_files = List.dedup ~compare:String.compare (find_linters_files () @ Config.linters_def_file) let do_frontend_checks (trans_unit_ctx: CFrontend_config.translation_unit_context) ast = - Logging.out "Loading the following linters files: %a\n" + L.(debug Capture Quiet) "Loading the following linters files: %a@\n" (Pp.comma_seq Format.pp_print_string) linters_files; CTL.create_ctl_evaluation_tracker trans_unit_ctx.source_file; try @@ -276,9 +279,9 @@ let do_frontend_checks (trans_unit_ctx: CFrontend_config.translation_unit_contex CFrontend_errors.filter_parsed_linters parsed_linters trans_unit_ctx.source_file in CFrontend_errors.parsed_linters := filtered_parsed_linters; let source_file = trans_unit_ctx.CFrontend_config.source_file in - Logging.out "Start linting file %a with rules: @\n%s@\n" + L.(debug Linters Medium) "Start linting file %a with rules: @\n%a@\n" SourceFile.pp source_file - (CFrontend_errors.linters_to_string filtered_parsed_linters); + CFrontend_errors.pp_linters filtered_parsed_linters; match ast with | Clang_ast_t.TranslationUnitDecl(_, decl_list, _, _) -> let context = @@ -292,10 +295,10 @@ let do_frontend_checks (trans_unit_ctx: CFrontend_config.translation_unit_contex List.iter ~f:(do_frontend_checks_decl context) allowed_decls; if (LintIssues.exists_issues ()) then store_issues source_file; - Logging.out "End linting file %a@\n" SourceFile.pp source_file; + L.(debug Linters Medium) "End linting file %a@\n" SourceFile.pp source_file; CTL.save_dotty_when_in_debug_mode trans_unit_ctx.CFrontend_config.source_file; | _ -> assert false (* NOTE: Assumes that an AST always starts with a TranslationUnitDecl *) with | Assert_failure (file, line, column) as exn -> - Logging.stderr "Fatal error: exception Assert_failure(%s, %d, %d)@\n%!" file line column; + L.internal_error "Fatal error: exception Assert_failure(%s, %d, %d)@\n%!" file line column; raise exn diff --git a/infer/src/clang/cFrontend_decl.ml b/infer/src/clang/cFrontend_decl.ml index 1a9a9dc2f..d86172768 100644 --- a/infer/src/clang/cFrontend_decl.ml +++ b/infer/src/clang/cFrontend_decl.ml @@ -25,7 +25,7 @@ struct Cfg.remove_proc_desc cfg procname; CMethod_trans.create_external_procdesc cfg procname is_objc_method None in - Logging.out_debug + L.(debug Capture Verbose) "@\n@\n>>---------- ADDING METHOD: '%s' ---------<<@\n@." (Typ.Procname.to_string procname); try (match Cfg.find_proc_desc_from_name cfg procname with @@ -36,8 +36,8 @@ struct has_return_param is_objc_method outer_context_opt in let start_node = Procdesc.get_start_node procdesc in let exit_node = Procdesc.get_exit_node procdesc in - Logging.out_debug - "\n\n>>---------- Start translating body of function: '%s' ---------<<\n@." + L.(debug Capture Verbose) + "@\n@\n>>---------- Start translating body of function: '%s' ---------<<@\n@." (Typ.Procname.to_string procname); let meth_body_nodes = T.instructions_trans context body extra_instrs exit_node in let proc_attributes = Procdesc.get_attributes procdesc in @@ -53,10 +53,10 @@ struct functions. This is to make sure I'm not wrong. *) assert false | CTrans_utils.TemplatedCodeException _ -> - Logging.out "Fatal error: frontend doesn't support translation of templated code\n"; + L.internal_error "Fatal error: frontend doesn't support translation of templated code@\n"; handle_translation_failure () | Assert_failure (file, line, column) when Config.failures_allowed -> - Logging.out "Fatal error: exception Assert_failure(%s, %d, %d)\n%!" file line column; + L.internal_error "Fatal error: exception Assert_failure(%s, %d, %d)@\n%!" file line column; handle_translation_failure () let function_decl trans_unit_ctx tenv cfg cg func_decl block_data_opt = @@ -124,8 +124,8 @@ struct | EmptyDecl _ | ObjCIvarDecl _ | ObjCPropertyDecl _ -> () | _ -> - Logging.out - "\nWARNING: found Method Declaration '%s' skipped. NEED TO BE FIXED\n\n" + L.internal_error + "@\nWARNING: found Method Declaration '%s' skipped. NEED TO BE FIXED@\n@\n" (Clang_ast_proj.get_decl_kind_string dec); () @@ -223,7 +223,8 @@ struct let curr_class = CContext.ContextClsDeclPtr parent_ptr in process_methods trans_unit_ctx tenv cg cfg curr_class [dec] | Some dec -> - Logging.out "Methods of %s skipped\n" (Clang_ast_proj.get_decl_kind_string dec) + L.(debug Capture Verbose) "Methods of %s skipped@\n" + (Clang_ast_proj.get_decl_kind_string dec) | None -> ()) | VarDecl (decl_info, named_decl_info, qt, ({ vdi_is_global; vdi_init_expr } as vdi)) when vdi_is_global && Option.is_some vdi_init_expr -> @@ -264,7 +265,7 @@ struct match dec with | EnumDecl _ -> ignore (CEnum_decl.enum_decl dec) | LinkageSpecDecl (_, decl_list, _) -> - Logging.out_debug "ADDING: LinkageSpecDecl decl list@\n"; + L.(debug Capture Verbose) "ADDING: LinkageSpecDecl decl list@\n"; List.iter ~f:translate decl_list | NamespaceDecl (_, _, decl_list, _, _) -> List.iter ~f:translate decl_list diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index ae322115b..244ca8ba2 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -9,6 +9,9 @@ open! IStd +module F = Format + +module L = Logging module MF = MarkupFormatter type linter = { @@ -43,10 +46,10 @@ let filter_parsed_linters parsed_linters source_file = let linters = filter_parsed_linters_developer parsed_linters in filter_parsed_linters_by_path linters source_file -let linters_to_string linters = - let linter_to_string linters = - List.map ~f:(fun (rule : linter) -> rule.issue_desc.name) linters in - String.concat ~sep:"\n" (linter_to_string linters) +let pp_linters fmt linters = + let pp_linter fmt {issue_desc={name}} = + F.fprintf fmt "%s@\n" name in + List.iter ~f:(pp_linter fmt) linters (* Map a formula id to a triple (visited, parameters, definition). Visited is used during the expansion phase to understand if the @@ -97,8 +100,9 @@ let evaluate_place_holder ph an = | "%type%" -> MF.monospaced_to_string (Ctl_parser_types.ast_node_type an) | "%child_type%" -> MF.monospaced_to_string (Ctl_parser_types.stmt_node_child_type an) | "%eventual_child_name%" -> MF.monospaced_to_string (Ctl_parser_types.eventual_child_name an) - | _ -> (Logging.out "ERROR: helper function %s is unknown. Stop.\n" ph; - assert false) + | _ -> + L.internal_error "ERROR: helper function %s is unknown. Stop.@\n" ph; + assert false (* given a message this function searches for a place-holder identifier, eg %id%. Then it evaluates id and replaces %id% in message @@ -113,11 +117,11 @@ let rec expand_message_string message an = let _ = Str.search_forward re message 0 in let ms = Str.matched_string message in let res = evaluate_place_holder ms an in - Logging.out "\nMatched string '%s'\n" ms; + L.(debug Linters Medium) "@\nMatched string '%s'@\n" ms; let re_ms = Str.regexp_string ms in let message' = Str.replace_first re_ms res message in - Logging.out "Replacing %s in message: \n %s \n" ms message; - Logging.out "Resulting message: \n %s \n" message'; + L.(debug Linters Medium) "Replacing %s in message: @\n %s @\n" ms message; + L.(debug Linters Medium) "Resulting message: @\n %s @\n" message'; expand_message_string message' an with Not_found -> message @@ -130,16 +134,17 @@ let string_to_err_kind = function | "INFO" -> Exceptions.Kinfo | "ADVICE" -> Exceptions.Kadvice | "LIKE" -> Exceptions.Klike - | s -> (Logging.out "\n[ERROR] Severity %s does not exist. Stop.\n" s; - assert false) + | s -> + L.internal_error "@\n[ERROR] Severity %s does not exist. Stop.@\n" s; + assert false let string_to_issue_mode m = match m with | "ON" -> CIssue.On | "OFF" -> CIssue.Off | s -> - (Logging.out "\n[ERROR] Mode %s does not exist. Please specify ON/OFF\n" s; - assert false) + L.internal_error "@\n[ERROR] Mode %s does not exist. Please specify ON/OFF@\n" s; + assert false let string_to_path path = Some path @@ -147,7 +152,7 @@ let string_to_path path = Some path let create_parsed_linters linters_def_file checkers : linter list = let open CIssue in let open CTL in - Logging.out "\n Converting checkers in (condition, issue) pairs\n"; + L.(debug Linters Medium) "@\nConverting checkers in (condition, issue) pairs@\n"; let do_one_checker checker : linter = let dummy_issue = { name = checker.name; @@ -177,10 +182,9 @@ let create_parsed_linters linters_def_file checkers : linter list = ~f:process_linter_definitions ~init:(dummy_issue, CTL.False, None) checker.definitions in - Logging.out "\nMaking condition and issue desc for checker '%s'\n" - checker.name; - Logging.out "\nCondition =\n %a\n" CTL.Debug.pp_formula condition; - Logging.out "\nIssue_desc = %a\n" CIssue.pp_issue issue_desc; + L.(debug Linters Medium) "@\nMaking condition and issue desc for checker '%s'@\n" checker.name; + L.(debug Linters Medium) "@\nCondition =@\n %a@\n" CTL.Debug.pp_formula condition; + L.(debug Linters Medium) "@\nIssue_desc = %a@\n" CIssue.pp_issue issue_desc; {condition; issue_desc; def_file = Some linters_def_file; path;} in List.map ~f:do_one_checker checkers @@ -231,7 +235,7 @@ let rec apply_substitution f sub = let expand_formula phi _map _error_msg = let fail_with_circular_macro_definition name error_msg = - failwithf "Macro '%s' has a circular definition.\n Cycle:\n%s" name error_msg in + failwithf "Macro '%s' has a circular definition.@\n Cycle:@\n%s" name error_msg in let open CTL in let rec expand acc map error_msg = match acc with @@ -239,7 +243,7 @@ let expand_formula phi _map _error_msg = | False -> acc | Atomic (ALVar.Formula_id (name) as av, actual_param) -> (* it may be a macro *) (let error_msg' = - error_msg ^ " -Expanding formula identifier '" ^ name ^"'\n" in + error_msg ^ " -Expanding formula identifier '" ^ name ^"'@\n" in (try match ALVar.FormulaIdMap.find av map with | (true, _, _) -> @@ -289,12 +293,12 @@ let build_macros_map macros = let expand_checkers macro_map checkers = let open CTL in let expand_one_checker c = - Logging.out " +Start expanding %s\n" c.name; + L.(debug Linters Medium) " +Start expanding %s@\n" c.name; let map = _build_macros_map c.definitions macro_map in let exp_defs = List.fold ~f:(fun defs clause -> match clause with | CSet (report_when_const, phi) -> - Logging.out " -Expanding report_when\n"; + L.(debug Linters Medium) " -Expanding report_when@\n"; CSet (report_when_const, expand_formula phi map "") :: defs | cl -> cl :: defs) ~init:[] c.definitions in { c with definitions = exp_defs} in diff --git a/infer/src/clang/cFrontend_errors.mli b/infer/src/clang/cFrontend_errors.mli index 64f1ea1b1..18b213abf 100644 --- a/infer/src/clang/cFrontend_errors.mli +++ b/infer/src/clang/cFrontend_errors.mli @@ -18,7 +18,7 @@ type linter = { val filter_parsed_linters : linter list -> SourceFile.t -> linter list -val linters_to_string : linter list -> string +val pp_linters : Format.formatter -> linter list -> unit (* map used to expand macro. It maps a formula id to a triple (visited, parameters, definition). diff --git a/infer/src/clang/cIssue.ml b/infer/src/clang/cIssue.ml index 7cf135bfb..bfb00189e 100644 --- a/infer/src/clang/cIssue.ml +++ b/infer/src/clang/cIssue.ml @@ -26,15 +26,15 @@ let string_of_mode m = | Off -> "Off" let pp_issue fmt issue = - Format.fprintf fmt "{\n Name = %s\n" (issue.name); - Format.fprintf fmt " Severity = %s \n" (Exceptions.err_kind_string issue.severity); - Format.fprintf fmt " Mode = %s \n" (string_of_mode issue.mode); - Format.fprintf fmt " Descrption = %s \n" issue.description; + Format.fprintf fmt "{@\n Name = %s@\n" (issue.name); + Format.fprintf fmt " Severity = %s@\n" (Exceptions.err_kind_string issue.severity); + Format.fprintf fmt " Mode = %s@\n" (string_of_mode issue.mode); + Format.fprintf fmt " Descrption = %s@\n" issue.description; (match issue.suggestion with - | Some s -> Format.fprintf fmt " Suggestion = %s\n" s + | Some s -> Format.fprintf fmt " Suggestion = %s@\n" s | _ -> ()); - Format.fprintf fmt " Loc = %s \n" (Location.to_string issue.loc); - Format.fprintf fmt "}\n" + Format.fprintf fmt " Loc = %s@\n" (Location.to_string issue.loc); + Format.fprintf fmt "}@\n" let should_run_check mode = match mode with diff --git a/infer/src/clang/cMethod_trans.ml b/infer/src/clang/cMethod_trans.ml index 11eba6172..5a8bfe3d7 100644 --- a/infer/src/clang/cMethod_trans.ml +++ b/infer/src/clang/cMethod_trans.ml @@ -404,8 +404,8 @@ let create_local_procdesc ?(set_objc_accessor_attr=false) trans_unit_ctx cfg ten ~shift:(List.length captured_mangled) (CMethod_signature.ms_get_args ms) in let source_range = CMethod_signature.ms_get_loc ms in - Logging.out_debug "\nCreating a new procdesc for function: '%s'\n@." pname; - Logging.out_debug "\nms = %s\n@." (CMethod_signature.ms_to_string ms); + L.(debug Capture Verbose) "@\nCreating a new procdesc for function: '%s'@\n@." pname; + L.(debug Capture Verbose) "@\nms = %s@\n@." (CMethod_signature.ms_to_string ms); let loc_start = CLocation.get_sil_location_from_range trans_unit_ctx source_range true in let loc_exit = CLocation.get_sil_location_from_range trans_unit_ctx source_range false in let ret_type = get_return_type tenv ms in diff --git a/infer/src/clang/cPredicates.ml b/infer/src/clang/cPredicates.ml index d4dc2e975..c1315503d 100644 --- a/infer/src/clang/cPredicates.ml +++ b/infer/src/clang/cPredicates.ml @@ -11,6 +11,8 @@ open! IStd open Lexing open Types_lexer +module L = Logging + let parsed_type_map : Ctl_parser_types.abs_ctype String.Map.t ref = ref String.Map.empty let get_available_attr_ios_sdk an = @@ -369,7 +371,7 @@ let type_ptr_equal_type type_ptr type_str = match CAst_utils.get_type type_ptr with | Some c_type' -> Ctl_parser_types.c_type_equal c_type' abs_ctype - | _ -> Logging.out "Couldn't find type....\n"; false + | _ -> L.(debug Linters Medium) "Couldn't find type....@\n"; false let has_type an _typ = match an, _typ with @@ -386,10 +388,10 @@ let has_type an _typ = | _ -> false let method_return_type an _typ = - Logging.out "\n Executing method_return_type..."; + L.(debug Linters Verbose) "@\n Executing method_return_type..."; match an, _typ with | Ctl_parser_types.Decl (Clang_ast_t.ObjCMethodDecl (_, _, mdi)), ALVar.Const typ -> - Logging.out "\n with parameter `%s`...." typ; + L.(debug Linters Verbose) "@\n with parameter `%s`...." typ; let qual_type = mdi.Clang_ast_t.omdi_result_type in type_ptr_equal_type qual_type.Clang_ast_t.qt_type_ptr typ | _ -> false diff --git a/infer/src/clang/cTL.ml b/infer/src/clang/cTL.ml index 5722bc5f3..35f47c179 100644 --- a/infer/src/clang/cTL.ml +++ b/infer/src/clang/cTL.ml @@ -10,6 +10,8 @@ open! IStd open Ctl_parser_types +module L = Logging + (* This module defines a language to define checkers. These checkers are intepreted over the AST of the program. A checker is defined by a CTL formula which express a condition saying when the checker should @@ -281,7 +283,8 @@ module Debug = struct (pp_ast ~ast_node_to_highlight ~prettifier:(ANSITerminal.sprintf highlight_style "%s")) ast_root in - Logging.out "\nNode ID: %d\tEvaluation stack level: %d\tSource line-number: %s\n" + L.(debug Linters Medium) + "@\nNode ID: %d\tEvaluation stack level: %d\tSource line-number: %s@\n" eval_node.id (Stack.length t.eval_stack) (Option.value_map @@ -290,13 +293,13 @@ module Debug = struct | Eval_undefined -> true | _ -> false in if is_last_occurrence && is_eval_result_undefined then - Logging.out - "From this step, a transition to a different part of the AST may follow.\n"; + L.(debug Linters Medium) + "From this step, a transition to a different part of the AST may follow.@\n"; let phi_str = Format.asprintf "%a" pp_formula eval_node.content.phi in - Logging.out "CTL Formula: %s\n\n" phi_str; - Logging.out "%s\n" ast_str; + L.(debug Linters Medium) "CTL Formula: %s@\n@\n" phi_str; + L.(debug Linters Medium) "%s@\n" ast_str; let quit_token = "q" in - Logging.out "Press Enter to continue or type %s to quit... @?" quit_token; + L.(debug Linters Medium) "Press Enter to continue or type %s to quit... @?" quit_token; match read_line () |> String.lowercase with | s when String.equal s quit_token -> exit 0 | _ -> @@ -309,7 +312,7 @@ module Debug = struct ) in match t.debugger_active, t.breakpoint_line, line_number eval_node.content.ast_node with | false, Some break_point_ln, Some ln when ln >= break_point_ln -> - Logging.out "Attaching debugger at line %d" ln; + L.(debug Linters Medium) "Attaching debugger at line %d" ln; stop_and_explain_step (); {t with debugger_active = true} | true, _, _ -> @@ -425,22 +428,22 @@ module Debug = struct end let print_checker c = - Logging.out "\n-------------------- \n"; - Logging.out "\nChecker name: %s\n" c.name; + L.(debug Linters Medium) "@\n-------------------- @\n"; + L.(debug Linters Medium) "@\nChecker name: %s@\n" c.name; List.iter ~f:(fun d -> (match d with | CSet (keyword, phi) -> let cn_str = ALVar.keyword_to_string keyword in - Logging.out " %s= \n %a\n\n" + L.(debug Linters Medium) " %s= @\n %a@\n@\n" cn_str Debug.pp_formula phi | CLet (exp, _, phi) -> let cn_str = ALVar.formula_id_to_string exp in - Logging.out " %s= \n %a\n\n" + L.(debug Linters Medium) " %s= @\n %a@\n@\n" cn_str Debug.pp_formula phi | CDesc (keyword, s) -> let cn_str = ALVar.keyword_to_string keyword in - Logging.out " %s= \n %s\n\n" cn_str s) + L.(debug Linters Medium) " %s= @\n %s@\n@\n" cn_str s) ) c.definitions; - Logging.out "\n-------------------- \n" + L.(debug Linters Medium) "@\n-------------------- @\n" let ctl_evaluation_tracker = ref None diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 51b6fa9ca..67b974309 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -113,9 +113,9 @@ struct let item_annot = Annot.Item.empty in fname, typ, item_annot in let fields = List.map ~f:mk_field_from_captured_var captured_vars in - Logging.out_debug "Block %s field:\n" block_name; + L.(debug Capture Verbose) "Block %s field:@\n" block_name; List.iter ~f:(fun (fn, _, _) -> - Logging.out_debug "-----> field: '%s'\n" (Fieldname.to_string fn)) fields; + L.(debug Capture Verbose) "-----> field: '%s'@\n" (Fieldname.to_string fn)) fields; let block_typename = Typ.Name.Objc.from_string block_name in ignore (Tenv.mk_struct tenv ~fields block_typename); let block_type = Typ.mk (Typ.Tstruct block_typename) in @@ -180,7 +180,7 @@ struct (* the parameter f will be called with function instruction *) let exec_with_block_priority_exception f trans_state e stmt_info = if (is_block_expr e) && (PriorityNode.own_priority_node trans_state.priority stmt_info) then ( - Logging.out_debug "Translating block expression by freeing the priority"; + L.(debug Capture Verbose) "Translating block expression by freeing the priority"; f { trans_state with priority = Free } e) else f trans_state e @@ -236,7 +236,7 @@ struct | None -> assert false in let res_trans = f trans_state stmt in let (exp, typ) = extract_exp_from_list res_trans.exps - "[Warning] Need exactly one expression to add reference type\n" in + "[Warning] Need exactly one expression to add reference type@\n" in { res_trans with exps = [(exp, add_reference_if_glvalue typ expr_info)] } (* Execute translation of e forcing to release priority @@ -430,9 +430,9 @@ struct let sizeof_data = {Exp.typ=sizeof_typ; nbytes; dynamic_length=None; subtype=Subtype.exact} in { empty_res_trans with exps = [(Exp.Sizeof sizeof_data, sizeof_typ)] } - | k -> Logging.out - "\nWARNING: Missing translation of Uniry_Expression_Or_Trait of kind: \ - %s . Expression ignored, returned -1... \n" + | k -> L.(debug Capture Medium) + "@\nWARNING: Missing translation of Uniry_Expression_Or_Trait of kind: \ + %s . Expression ignored, returned -1... @\n" (Clang_ast_j.string_of_unary_expr_or_type_trait_kind k); { empty_res_trans with exps =[(Exp.minus_one, typ)]} @@ -495,10 +495,10 @@ struct let context = trans_state.context in let sil_loc = CLocation.get_sil_location stmt_info context in let name_info, _, qual_type = CAst_utils.get_info_from_decl_ref decl_ref in - Logging.out_debug "!!!!! Dealing with field '%s' @." name_info.Clang_ast_t.ni_name; + L.(debug Capture Verbose) "!!!!! Dealing with field '%s' @." name_info.Clang_ast_t.ni_name; let field_typ = CType_decl.qual_type_to_sil_type context.tenv qual_type in let (obj_sil, class_typ) = extract_exp_from_list pre_trans_result.exps - "WARNING: in Field dereference we expect to know the object\n" in + "WARNING: in Field dereference we expect to know the object@\n" in let is_pointer_typ = match class_typ.desc with | Typ.Tptr _ -> true | _ -> false in @@ -506,7 +506,7 @@ struct match class_typ.desc with | Typ.Tptr (t, _) -> t | _ -> class_typ in - Logging.out_debug "Type is '%s' @." (Typ.to_string class_typ); + L.(debug Capture Verbose) "Type is '%s' @." (Typ.to_string class_typ); let field_name = CGeneral_utils.mk_class_field_name name_info in let field_exp = Exp.Lfield (obj_sil, field_name, class_typ) in (* In certain cases, there is be no LValueToRValue cast, but backend needs dereference*) @@ -535,7 +535,7 @@ struct let decl_opt = CAst_utils.get_function_decl_with_body decl_ptr in Option.iter ~f:(call_translation context) decl_opt; let method_name = CAst_utils.get_unqualified_name name_info in - Logging.out_debug "!!!!! Dealing with method '%s' @." method_name; + L.(debug Capture Verbose) "!!!!! Dealing with method '%s' @." method_name; let method_typ = CType_decl.qual_type_to_sil_type context.tenv qual_type in let ms_opt = CMethod_trans.method_signature_of_pointer context.translation_unit_context context.tenv decl_ptr in @@ -651,7 +651,7 @@ struct let typ = CType.add_pointer_to_typ (Typ.mk (Tstruct class_typename)) in [(var_exp, typ)] else [(var_exp, typ)] in - Logging.out_debug "\n\n PVAR ='%s'\n\n" (Pvar.to_string pvar); + L.(debug Capture Verbose) "@\n@\n PVAR ='%s'@\n@\n" (Pvar.to_string pvar); let res_trans = { empty_res_trans with exps } in match typ.desc with | Tptr (_, Pk_reference) -> @@ -660,7 +660,7 @@ struct | _ -> res_trans and decl_ref_trans trans_state pre_trans_result stmt_info decl_ref ~is_constructor_init = - Logging.out_debug " priority node free = '%s'@\n@." + L.(debug Capture Verbose) " priority node free = '%s'@\n@." (string_of_bool (PriorityNode.is_priority_free trans_state)); let decl_kind = decl_ref.Clang_ast_t.dr_kind in match decl_kind with @@ -674,14 +674,14 @@ struct method_deref_trans trans_state pre_trans_result decl_ref stmt_info decl_kind | _ -> let print_error decl_kind = - Logging.out + L.(debug Capture Medium) "Warning: Decl ref expression %s with pointer %d still needs to be translated " (Clang_ast_j.string_of_decl_kind decl_kind) decl_ref.Clang_ast_t.dr_decl_pointer in print_error decl_kind; assert false and declRefExpr_trans trans_state stmt_info decl_ref_expr_info _ = - Logging.out_debug " priority node free = '%s'\n@." + L.(debug Capture Verbose) " priority node free = '%s'@\n@." (string_of_bool (PriorityNode.is_priority_free trans_state)); let decl_ref = match decl_ref_expr_info.Clang_ast_t.drti_decl_ref with | Some dr -> dr @@ -695,7 +695,7 @@ struct (match enum_constant_decl_info.Clang_ast_t.ecdi_init_expr with | Some stmt -> expression_trans context stmt - "WARNING: Expression in Enumeration constant not found\n" + "WARNING: Expression in Enumeration constant not found@\n" | None -> match prev_enum_constant_opt with | Some prev_constant_pointer -> @@ -735,9 +735,9 @@ struct let res_trans_a = instruction trans_state array_stmt in let res_trans_idx = instruction trans_state idx_stmt in let (a_exp, _) = extract_exp_from_list res_trans_a.exps - "WARNING: In ArraySubscriptExpr there was a problem in translating array exp.\n" in + "WARNING: In ArraySubscriptExpr there was a problem in translating array exp.@\n" in let (i_exp, _) = extract_exp_from_list res_trans_idx.exps - "WARNING: In ArraySubscriptExpr there was a problem in translating index exp.\n" in + "WARNING: In ArraySubscriptExpr there was a problem in translating index exp.@\n" in let array_exp = Exp.Lindex (a_exp, i_exp) in let root_nodes = @@ -768,8 +768,8 @@ struct and binaryOperator_trans trans_state binary_operator_info stmt_info expr_info stmt_list = let bok = Clang_ast_j.string_of_binary_operator_kind binary_operator_info.Clang_ast_t.boi_kind in - Logging.out_debug " BinaryOperator '%s' " bok; - Logging.out_debug " priority node free = '%s'\n@." + L.(debug Capture Verbose) " BinaryOperator '%s' " bok; + L.(debug Capture Verbose) " priority node free = '%s'@\n@." (string_of_bool (PriorityNode.is_priority_free trans_state)); let context = trans_state.context in let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in @@ -786,14 +786,14 @@ struct (* translating the operands. *) let res_trans_e1 = exec_with_self_exception instruction trans_state' s1 in let (var_exp, var_exp_typ) = extract_exp_from_list res_trans_e1.exps - "\nWARNING: Missing LHS operand in BinOp. Returning -1. Fix needed...\n" in + "@\nWARNING: Missing LHS operand in BinOp. Returning -1. Fix needed...@\n" in let trans_state'' = { trans_state' with var_exp_typ = Some (var_exp, var_exp_typ) } in let res_trans_e2 = (* translation of s2 is done taking care of block special case *) exec_with_block_priority_exception (exec_with_self_exception instruction) trans_state'' s2 stmt_info in let (sil_e2, _) = extract_exp_from_list res_trans_e2.exps - "\nWARNING: Missing RHS operand in BinOp. Returning -1. Fix needed...\n" in + "@\nWARNING: Missing RHS operand in BinOp. Returning -1. Fix needed...@\n" in let binop_res_trans, exp_to_parent = if List.exists ~f:(Exp.equal var_exp) res_trans_e2.initd_exps then [], [] else @@ -879,9 +879,9 @@ struct let params = List.tl_exn (collect_exprs result_trans_subexprs) in if Int.equal (List.length params) (List.length params_stmt) then params - else - (Logging.out "ERROR: stmt_list and res_trans_par.exps must have same size\n"; - assert false) in + else ( + L.internal_error "ERROR: stmt_list and res_trans_par.exps must have same size@\n"; + assert false) in let act_params = if is_cf_retain_release then (Exp.Const (Const.Cint IntLit.one), Typ.mk (Tint Typ.IBool)) :: act_params else act_params in @@ -1056,7 +1056,7 @@ struct | [] -> obj_c_message_expr_info, [empty_res_trans] and objCMessageExpr_trans trans_state si obj_c_message_expr_info stmt_list expr_info = - Logging.out_debug " priority node free = '%s'\n@." + L.(debug Capture Verbose) " priority node free = '%s'@\n@." (string_of_bool (PriorityNode.is_priority_free trans_state)); let context = trans_state.context in let sil_loc = CLocation.get_sil_location si context in @@ -1100,12 +1100,13 @@ struct and dispatch_function_trans trans_state stmt_info stmt_list n = - Logging.out_debug "\n Call to a dispatch function treated as special case...\n"; + L.(debug Capture Verbose) "@\n Call to a dispatch function treated as special case...@\n"; let transformed_stmt = Ast_expressions.translate_dispatch_function stmt_info stmt_list n in instruction trans_state transformed_stmt and block_enumeration_trans trans_state stmt_info stmt_list ei = - Logging.out_debug "\n Call to a block enumeration function treated as special case...\n@."; + L.(debug Capture Verbose) + "@\n Call to a block enumeration function treated as special case...@\n@."; let procname = Procdesc.get_proc_name trans_state.context.CContext.procdesc in let pvar = CProcname.get_next_block_pvar procname in let transformed_stmt, _ = @@ -1125,7 +1126,7 @@ struct let trans_state' = { trans_state_pri with succ_nodes = [] } in let res_trans_b = instruction trans_state' stmt in let (e', _) = extract_exp_from_list res_trans_b.exps - "\nWARNING: Missing branch expression for Conditional operator. Need to be fixed\n" in + "@\nWARNING: Missing branch expression for Conditional operator. Need to be fixed@\n" in let set_temp_var = [ Sil.Store (Exp.Lvar pvar, var_typ, e', sil_loc) ] in @@ -1189,7 +1190,7 @@ struct let root_nodes = init_res_trans'.root_nodes in let root_nodes' = if root_nodes <> [] then root_nodes else op_res_trans.root_nodes in { op_res_trans with root_nodes = root_nodes'; } - | _ -> Logging.out "BinaryConditionalOperator not translated@."; + | _ -> L.(debug Capture Medium) "BinaryConditionalOperator not translated@."; assert false (* Translate a condition for if/loops statement. It shorts-circuit and/or. *) @@ -1203,10 +1204,10 @@ struct create_prune_node b e ins sil_loc (Sil.Ik_if) context in let extract_exp el = extract_exp_from_list el - "\nWARNING: Missing expression for Conditional operator. Need to be fixed" in + "@\nWARNING: Missing expression for Conditional operator. Need to be fixed" in (* this function translate cond without doing shortcircuit *) let no_short_circuit_cond () = - Logging.out_debug " No short-circuit condition\n"; + L.(debug Capture Verbose) " No short-circuit condition@\n"; let res_trans_cond = if is_null_stmt cond then { empty_res_trans with exps = [(Exp.Const (Const.Cint IntLit.one), Typ.mk (Tint Typ.IBool))] @@ -1267,7 +1268,8 @@ struct instrs = res_trans_s1.instrs@res_trans_s2.instrs; exps = [(e_cond, typ1)]; } in - Logging.out_debug "Translating Condition for If-then-else/Loop/Conditional Operator \n"; + L.(debug Capture Verbose) + "Translating Condition for If-then-else/Loop/Conditional Operator @\n"; let open Clang_ast_t in match cond with | BinaryOperator(_, [s1; s2], _, boi) -> @@ -1353,7 +1355,7 @@ struct else [switch_special_cond_node] in let (switch_e_cond', switch_e_cond'_typ) = extract_exp_from_list res_trans_cond_tmp.exps - "\nWARNING: The condition of the SwitchStmt is not singleton. Need to be fixed\n" in + "@\nWARNING: The condition of the SwitchStmt is not singleton. Need to be fixed@\n" in let res_trans_cond = { res_trans_cond_tmp with root_nodes = root_nodes; leaf_nodes = [switch_special_cond_node] @@ -1474,7 +1476,7 @@ struct and stmtExpr_trans trans_state stmt_list = let stmt = - extract_stmt_from_singleton stmt_list "ERROR: StmtExpr should have only one statement.\n" in + extract_stmt_from_singleton stmt_list "ERROR: StmtExpr should have only one statement.@\n" in let res_trans_stmt = instruction trans_state stmt in let exps' = List.rev res_trans_stmt.exps in match exps' with @@ -1683,7 +1685,7 @@ struct let trans_state_pri = PriorityNode.try_claim_priority_node trans_state array_stmt_info in let dynlength_trans_result = instruction trans_state_pri dynlength_stmt in let dynlength_exp_typ = extract_exp_from_list dynlength_trans_result.exps - "WARNING: There should be one expression.\n" in + "WARNING: There should be one expression.@\n" in let sil_loc = CLocation.get_sil_location dynlength_stmt_info trans_state_pri.context in let call_instr = let call_exp = Exp.Const (Const.Cfun BuiltinDecl.__set_array_length) in @@ -1722,7 +1724,7 @@ struct exec_with_self_exception (exec_with_glvalue_as_reference instruction) in exec_with_block_priority_exception instruction' trans_state' ie var_stmt_info in let (sil_e1', ie_typ) = extract_exp_from_list res_trans_ie.exps - "WARNING: In DeclStmt we expect only one expression returned in recursive call\n" in + "WARNING: In DeclStmt we expect only one expression returned in recursive call@\n" in let rhs_owning_method = CTrans_utils.is_owning_method ie in let _, instrs_assign = (* variable might be initialized already - do nothing in that case*) @@ -1792,7 +1794,7 @@ struct | RecordDecl _ :: _ -> (* Case for struct *) collect_all_decl trans_state decl_list succ_nodes stmt_info | _ -> - Logging.out + L.(debug Capture Medium) "WARNING: In DeclStmt found an unknown declaration type. \ RETURNING empty list of declaration. NEED TO BE FIXED"; empty_res_trans in @@ -1805,7 +1807,7 @@ struct (* For OpaqueValueExpr we return the translation generated from its source expression*) and opaqueValueExpr_trans trans_state opaque_value_expr_info = - Logging.out_debug " priority node free = '%s'\n@." + L.(debug Capture Verbose) " priority node free = '%s'@\n@." (string_of_bool (PriorityNode.is_priority_free trans_state)); match trans_state.opaque_exp with | Some exp -> { empty_res_trans with exps = [exp] } @@ -1833,7 +1835,7 @@ struct (* to translate the CallToSetter which is how x.f = a is actually implemented by the runtime.*) and pseudoObjectExpr_trans trans_state stmt_list = - Logging.out_debug " priority node free = '%s'\n@." + L.(debug Capture Verbose) " priority node free = '%s'@\n@." (string_of_bool (PriorityNode.is_priority_free trans_state)); let rec do_semantic_elements el = let open Clang_ast_t in @@ -1849,11 +1851,11 @@ struct (* Cast expression are treated the same apart from the cast operation kind*) and cast_exprs_trans trans_state stmt_info stmt_list expr_info cast_expr_info = let context = trans_state.context in - Logging.out_debug " priority node free = '%s'\n@." + L.(debug Capture Verbose) " priority node free = '%s'@\n@." (string_of_bool (PriorityNode.is_priority_free trans_state)); let sil_loc = CLocation.get_sil_location stmt_info context in let stmt = extract_stmt_from_singleton stmt_list - "WARNING: In CastExpr There must be only one stmt defining the expression to be cast.\n" in + "WARNING: In CastExpr There must be only one stmt defining the expression to be cast.@\n" in let res_trans_stmt = instruction trans_state stmt in let typ = CType_decl.qual_type_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_qual_type in @@ -1872,7 +1874,7 @@ struct (* function used in the computation for both Member_Expr and ObjCIVarRefExpr *) and do_memb_ivar_ref_exp trans_state stmt_info stmt_list decl_ref = let exp_stmt = extract_stmt_from_singleton stmt_list - "WARNING: in MemberExpr there must be only one stmt defining its expression.\n" in + "WARNING: in MemberExpr there must be only one stmt defining its expression.@\n" in (* Don't pass var_exp_typ to child of MemberExpr - this may lead to initializing variable *) (* with wrong value. For example, we don't want p to be initialized with X(1) for:*) (* int p = X(1).field; *) @@ -1896,13 +1898,13 @@ struct let trans_state_pri = PriorityNode.try_claim_priority_node trans_state stmt_info in let stmt = extract_stmt_from_singleton stmt_list "WARNING: We expect only one element in stmt list defining \ - the operand in UnaryOperator. NEED FIXING\n" in + the operand in UnaryOperator. NEED FIXING@\n" in let trans_state' = { trans_state_pri with succ_nodes = [] } in let res_trans_stmt = instruction trans_state' stmt in (* Assumption: the operand does not create a cfg node*) let (sil_e', _) = extract_exp_from_list res_trans_stmt.exps - "\nWARNING: Missing operand in unary operator. NEED FIXING.\n" in + "@\nWARNING: Missing operand in unary operator. NEED FIXING.@\n" in let ret_typ = CType_decl.qual_type_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_qual_type in @@ -1947,7 +1949,7 @@ struct var_exp_typ = Some (ret_exp, ret_typ) } in let res_trans_stmt = exec_with_self_exception instruction trans_state' stmt in let (sil_expr, _) = extract_exp_from_list res_trans_stmt.exps - "WARNING: There should be only one return expression.\n" in + "WARNING: There should be only one return expression.@\n" in let ret_instrs = if List.exists ~f:(Exp.equal ret_exp) res_trans_stmt.initd_exps then [] @@ -1967,9 +1969,9 @@ struct | [] -> (* return; *) let ret_node = mk_ret_node [] in { empty_res_trans with root_nodes = [ret_node]; leaf_nodes = []} - | _ -> Logging.out_debug - "\nWARNING: Missing translation of Return Expression. \ - Return Statement ignored. Need fixing!\n"; + | _ -> L.(debug Capture Verbose) + "@\nWARNING: Missing translation of Return Expression. \ + Return Statement ignored. Need fixing!@\n"; { empty_res_trans with root_nodes = succ_nodes }) in (* We expect a return with only one expression *) trans_result @@ -1980,7 +1982,7 @@ struct (* In paren expression there should be only one stmt that defines the expression *) and parenExpr_trans trans_state stmt_list = let stmt = extract_stmt_from_singleton stmt_list - "WARNING: In ParenExpression there should be only one stmt.\n" in + "WARNING: In ParenExpression there should be only one stmt.@\n" in instruction trans_state stmt and objCBoxedExpr_trans trans_state info sel stmt_info stmts = @@ -2201,7 +2203,7 @@ struct let trans_state_param = { trans_state_pri with succ_nodes = [] } in let result_trans_param = exec_with_self_exception instruction trans_state_param param in let exp = extract_exp_from_list result_trans_param.exps - "WARNING: There should be one expression to delete. \n" in + "WARNING: There should be one expression to delete. @\n" in let call_instr = Sil.Call (None, Exp.Const (Const.Cfun fname), [exp], sil_loc, CallFlags.default) in let call_res_trans = { empty_res_trans with instrs = [call_instr] } in @@ -2237,7 +2239,7 @@ struct let var_exp_typ = (Exp.Lvar pvar, typ_tmp) in let res_trans = init_expr_trans trans_state var_exp_typ stmt_info (Some temp_exp) in let _, typ = extract_exp_from_list res_trans.exps - "MaterializeExpr initializer missing\n" in + "MaterializeExpr initializer missing@\n" in Procdesc.append_locals procdesc [(Pvar.get_name pvar, typ)]; res_trans @@ -2402,7 +2404,7 @@ struct let stmt_kind = Clang_ast_proj.get_stmt_kind_string instr in let stmt_info, _ = Clang_ast_proj.get_stmt_tuple instr in let stmt_pointer = stmt_info.Clang_ast_t.si_pointer in - Logging.out_debug "\nPassing from %s '%d' \n" stmt_kind stmt_pointer; + L.(debug Capture Verbose) "@\nPassing from %s '%d' @\n" stmt_kind stmt_pointer; let open Clang_ast_t in match instr with | GotoStmt(stmt_info, _, { Clang_ast_t.gsi_label = label_name; _ }) -> @@ -2455,8 +2457,8 @@ struct switchStmt_trans trans_state stmt_info switch_stmt_list | CaseStmt _ -> - Logging.out_debug - "FATAL: Passing from CaseStmt outside of SwitchStmt, terminating.\n"; + L.(debug Capture Verbose) + "FATAL: Passing from CaseStmt outside of SwitchStmt, terminating.@\n"; assert false | StmtExpr(_, stmt_list, _) -> @@ -2604,8 +2606,8 @@ struct | ObjCAtTryStmt (_, stmts) -> compoundStmt_trans trans_state stmts | CXXTryStmt (_, stmts) -> - (Logging.out - "\n!!!!WARNING: found statement %s. \nTranslation need to be improved.... \n" + (L.(debug Capture Medium) + "@\n!!!!WARNING: found statement %s. @\nTranslation need to be improved.... @\n" (Clang_ast_proj.get_stmt_kind_string instr); compoundStmt_trans trans_state stmts) @@ -2690,9 +2692,9 @@ struct | SubstNonTypeTemplateParmPackExpr _ | CXXDependentScopeMemberExpr _ -> raise (CTrans_utils.TemplatedCodeException instr) - | s -> (Logging.out - "\n!!!!WARNING: found statement %s. \nACTION REQUIRED: \ - Translation need to be defined. Statement ignored.... \n" + | s -> (L.(debug Capture Medium) + "@\n!!!!WARNING: found statement %s. @\nACTION REQUIRED: \ + Translation need to be defined. Statement ignored.... @\n" (Clang_ast_proj.get_stmt_kind_string s); assert false) @@ -2716,7 +2718,7 @@ struct let var_res_trans = match ctor_init.Clang_ast_t.xci_subject with | `Delegating _ | `BaseClass _ -> let this_exp, this_typ = extract_exp_from_list this_res_trans.exps - "WARNING: There should be one expression for 'this' in constructor. \n" in + "WARNING: There should be one expression for 'this' in constructor. @\n" in (* Hack: Strip pointer from type here since cxxConstructExpr_trans expects it this way *) (* it will add pointer back before making it a parameter to a call *) let class_typ = match this_typ.Typ.desc with Tptr (t, _) -> t | _ -> assert false in @@ -2725,7 +2727,7 @@ struct decl_ref_trans trans_state' this_res_trans child_stmt_info decl_ref ~is_constructor_init:true in let var_exp_typ = extract_exp_from_list var_res_trans.exps - "WARNING: There should be one expression to initialize in constructor initializer. \n" in + "WARNING: There should be one expression to initialize in constructor initializer. @\n" in let init_expr = ctor_init.Clang_ast_t.xci_init_expr in let init_res_trans = init_expr_trans trans_state' var_exp_typ child_stmt_info init_expr in PriorityNode.compute_results_to_parent trans_state' sil_loc "Constructor Init" diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index f3ce10e89..986250e8a 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -23,7 +23,7 @@ exception TemplatedCodeException of Clang_ast_t.stmt let extract_item_from_singleton l warning_string failure_val = match l with | [item] -> item - | _ -> L.out_debug "%s" warning_string; failure_val + | _ -> L.(debug Capture Medium) "%s" warning_string; failure_val let dummy_exp = (Exp.minus_one, Typ.mk (Tint Typ.IInt)) @@ -59,7 +59,7 @@ struct let create_prune_node branch e_cond instrs_cond loc ik context = let (e_cond', _) = extract_exp_from_list e_cond - "\nWARNING: Missing expression for Conditional operator. Need to be fixed" in + "@\nWARNING: Missing expression for Conditional operator. Need to be fixed" in let e_cond'' = if branch then Exp.BinOp(Binop.Ne, e_cond', Exp.zero) @@ -214,11 +214,11 @@ struct let try_claim_priority_node trans_state stmt_info = match trans_state.priority with | Free -> - Logging.out_debug "Priority is free. Locking priority node in %d\n@." + L.(debug Capture Verbose) "Priority is free. Locking priority node in %d@\n@." stmt_info.Clang_ast_t.si_pointer; { trans_state with priority = Busy stmt_info.Clang_ast_t.si_pointer } | _ -> - Logging.out_debug "Priority busy in %d. No claim possible\n@." + L.(debug Capture Verbose) "Priority busy in %d. No claim possible@\n@." stmt_info.Clang_ast_t.si_pointer; trans_state @@ -442,8 +442,8 @@ let cast_operation trans_state cast_kind exps cast_typ sil_loc is_objc_bridged = if Exp.is_zero exp then ([], (Exp.null, cast_typ)) else ([], (exp, cast_typ)) | _ -> - L.out_debug - "\nWARNING: Missing translation for Cast Kind %s. The construct has been ignored...\n" + L.(debug Capture Verbose) + "@\nWARNING: Missing translation for Cast Kind %s. The construct has been ignored...@\n" (Clang_ast_j.string_of_cast_kind cast_kind); ([], (exp, cast_typ)) @@ -510,7 +510,8 @@ let cxx_method_builtin_trans trans_state loc params_trans_res pname = None let define_condition_side_effects e_cond instrs_cond sil_loc = - let (e', typ) = extract_exp_from_list e_cond "\nWARNING: Missing expression in IfStmt. Need to be fixed\n" in + let (e', typ) = extract_exp_from_list e_cond + "@\nWARNING: Missing expression in IfStmt. Need to be fixed@\n" in match e' with | Exp.Lvar pvar -> let id = Ident.create_fresh Ident.knormal in @@ -572,7 +573,7 @@ let rec get_type_from_exp_stmt stmt = get_type_from_exp_stmt (extract_stmt_from_singleton stmt_list "WARNING: We expect only one stmt.") | DeclRefExpr(_, _, _, info) -> do_decl_ref_exp info | _ -> - Logging.out "Failing with: %s@\n%!" (Clang_ast_j.string_of_stmt stmt); + L.internal_error "Failing with: %s@\n%!" (Clang_ast_j.string_of_stmt stmt); assert false module Self = @@ -749,7 +750,7 @@ let var_or_zero_in_init_list tenv e typ ~return_zero:return_zero = let extract_item_from_option op warning_string = match op with | Some item -> item - | _ -> L.out_debug warning_string; assert false + | _ -> L.(debug Capture Verbose) warning_string; assert false let extract_id_from_singleton id_list warning_string = extract_item_from_singleton id_list warning_string (dummy_id ()) diff --git a/infer/src/clang/cType_to_sil_type.ml b/infer/src/clang/cType_to_sil_type.ml index 8d3fcc145..6fe3f111a 100644 --- a/infer/src/clang/cType_to_sil_type.ml +++ b/infer/src/clang/cType_to_sil_type.ml @@ -147,11 +147,11 @@ and decl_ptr_to_type_desc translate_decl tenv decl_ptr : Typ.desc = | Some (ObjCCategoryImplDecl _ as d) | Some (EnumDecl _ as d) -> translate_decl tenv d | Some _ -> - L.out_debug "Warning: Wrong decl found for pointer %s " + L.(debug Capture Verbose) "Warning: Wrong decl found for pointer %s " (Clang_ast_j.string_of_pointer decl_ptr); Typ.Tvoid | None -> - L.out_debug "Warning: Decl pointer %s not found." + L.(debug Capture Verbose) "Warning: Decl pointer %s not found." (Clang_ast_j.string_of_pointer decl_ptr); Typ.Tvoid diff --git a/infer/src/clang/ctl_parser.mly b/infer/src/clang/ctl_parser.mly index 14d57d583..fab84e211 100644 --- a/infer/src/clang/ctl_parser.mly +++ b/infer/src/clang/ctl_parser.mly @@ -8,6 +8,7 @@ */ %{ + module L = Logging open! IStd @@ -22,11 +23,10 @@ let is_defined_identifier id = if (List.mem ~equal:ALVar.equal !formal_params (ALVar.Var id)) then - Logging.out "\tParsed exp '%s' as variable" id + L.(debug Linters Verbose) "\tParsed exp '%s' as variable" id else - raise (Ctl_parser_types.ALParsingException - ("ERROR: Variable '" ^ id ^ "' is undefined")) - + raise (Ctl_parser_types.ALParsingException + ("ERROR: Variable '" ^ id ^ "' is undefined")) %} %token EU @@ -101,13 +101,13 @@ al_file: import_files: | { [] } | HASHIMPORT LESS_THAN file_identifier GREATER_THAN import_files - { Logging.out "Parsed import clauses...\n\n"; $3 :: $5 } + { L.(debug Linters Verbose) "Parsed import clauses...@\n@\n"; $3 :: $5 } ; global_macros: | { [] } | GLOBAL_MACROS LEFT_BRACE let_clause_list RIGHT_BRACE SEMICOLON - { Logging.out "Parsed global macro definitions...\n\n"; $3 } + { L.(debug Linters Verbose) "Parsed global macro definitions...@\n@\n"; $3 } ; checkers_list: @@ -118,7 +118,7 @@ checkers_list: checker: DEFINE_CHECKER identifier ASSIGNMENT LEFT_BRACE clause_list RIGHT_BRACE { - Logging.out "\nParsed checker definition\n"; + L.(debug Linters Verbose) "@\nParsed checker definition@\n"; let c = { CTL.name = $2; CTL.definitions = $5 } in CTL.print_checker c; c @@ -137,14 +137,14 @@ let_clause_list: clause: | SET identifier ASSIGNMENT formula - { Logging.out "\tParsed SET clause\n"; + { L.(debug Linters Verbose) "\tParsed SET clause@\n"; let alvar = match $2 with | "report_when" -> ALVar.Report_when | _ -> failwith "string '%s' cannot be set to a variable. \ Use the reserverd variable 'report_when'" in CTL.CSet (alvar, $4) } | SET identifier ASSIGNMENT STRING - { Logging.out "\tParsed SET clause\n"; + { L.(debug Linters Verbose) "\tParsed SET clause@\n"; let alvar = match $2 with | "message" -> ALVar.Message | "suggestion" -> ALVar.Suggestion @@ -160,28 +160,28 @@ clause: let_clause: | LET formula_id_def ASSIGNMENT formula - { Logging.out "\tParsed LET clause\n"; CTL.CLet ($2, [], $4) } + { L.(debug Linters Verbose) "\tParsed LET clause@\n"; CTL.CLet ($2, [], $4) } | LET formula_id_def LEFT_PAREN formal_params RIGHT_PAREN ASSIGNMENT formula - { Logging.out "\tParsed let clause with formula identifier '%s(....)' \n" - (ALVar.formula_id_to_string $2); - CTL.CLet ($2, $4, $7) } + { L.(debug Linters Verbose) "\tParsed let clause with formula identifier '%s(....)'@\n" + (ALVar.formula_id_to_string $2); + CTL.CLet ($2, $4, $7) } ; atomic_formula: - | TRUE { Logging.out "\tParsed True\n"; CTL.True } - | FALSE { Logging.out "\tParsed False\n"; CTL.False } + | TRUE { L.(debug Linters Verbose) "\tParsed True@\n"; CTL.True } + | FALSE { L.(debug Linters Verbose) "\tParsed False@\n"; CTL.False } | identifier LEFT_PAREN actual_params RIGHT_PAREN - { Logging.out "\tParsed predicate\n"; CTL.Atomic(ALVar.Formula_id $1, $3) } + { L.(debug Linters Verbose) "\tParsed predicate@\n"; CTL.Atomic(ALVar.Formula_id $1, $3) } ; formula_id_def: - | identifier { Logging.out "\tParsed formula identifier '%s' \n" $1; + | identifier { L.(debug Linters Verbose) "\tParsed formula identifier '%s'@\n" $1; formal_params := []; ALVar.Formula_id $1 } ; formula_id: - | identifier { Logging.out "\tParsed formula identifier '%s' \n" $1; + | identifier { L.(debug Linters Verbose) "\tParsed formula identifier '%s'@\n" $1; ALVar.Formula_id $1 } ; @@ -212,54 +212,55 @@ formula_with_paren: formula: | formula_with_paren { $1 } | formula_id { CTL.Atomic($1, []) } - | atomic_formula { Logging.out "\tParsed atomic formula\n"; $1 } - | formula EU formula { Logging.out "\tParsed EU\n"; CTL.EU (None, $1, $3) } - | formula AU formula { Logging.out "\tParsed AU\n"; CTL.AU (None,$1, $3) } - | formula AF { Logging.out "\tParsed AF\n"; CTL.AF (None,$1) } - | formula EX { Logging.out "\tParsed EX\n"; CTL.EX (None, $1) } - | formula AX { Logging.out "\tParsed AX\n"; CTL.AX (None, $1) } - | formula EG { Logging.out "\tParsed EG\n"; CTL.EG (None, $1) } - | formula AG { Logging.out "\tParsed AG\n"; CTL.AG (None, $1) } - | formula EH node_list { Logging.out "\tParsed EH\n"; CTL.EH ($3, $1) } - | formula EF { Logging.out "\tParsed EF\n"; CTL.EF (None, $1) } + | atomic_formula { L.(debug Linters Verbose) "\tParsed atomic formula@\n"; $1 } + | formula EU formula { L.(debug Linters Verbose) "\tParsed EU@\n"; CTL.EU (None, $1, $3) } + | formula AU formula { L.(debug Linters Verbose) "\tParsed AU@\n"; CTL.AU (None,$1, $3) } + | formula AF { L.(debug Linters Verbose) "\tParsed AF@\n"; CTL.AF (None,$1) } + | formula EX { L.(debug Linters Verbose) "\tParsed EX@\n"; CTL.EX (None, $1) } + | formula AX { L.(debug Linters Verbose) "\tParsed AX@\n"; CTL.AX (None, $1) } + | formula EG { L.(debug Linters Verbose) "\tParsed EG@\n"; CTL.EG (None, $1) } + | formula AG { L.(debug Linters Verbose) "\tParsed AG@\n"; CTL.AG (None, $1) } + | formula EH node_list { L.(debug Linters Verbose) "\tParsed EH@\n"; CTL.EH ($3, $1) } + | formula EF { L.(debug Linters Verbose) "\tParsed EF@\n"; CTL.EF (None, $1) } | WHEN formula HOLDS_IN_NODE node_list - { Logging.out "\tParsed InNode\n"; CTL.InNode ($4, $2)} + { L.(debug Linters Verbose) "\tParsed InNode@\n"; CTL.InNode ($4, $2)} | ET node_list WITH_TRANSITION transition_label formula_EF - { Logging.out "\tParsed ET with transition '%s'\n" (fst $4); + { L.(debug Linters Verbose) "\tParsed ET with transition '%s'@\n" (fst $4); CTL.ET ($2, snd $4, $5)} | ETX node_list WITH_TRANSITION transition_label formula_EF - { Logging.out "\tParsed ETX ith transition '%s'\n" (fst $4); + { L.(debug Linters Verbose) "\tParsed ETX ith transition '%s'@\n" (fst $4); CTL.ETX ($2, snd $4, $5)} | EX WITH_TRANSITION transition_label formula_with_paren - { Logging.out "\tParsed EX with transition '%s'\n" (fst $3); + { L.(debug Linters Verbose) "\tParsed EX with transition '%s'@\n" (fst $3); CTL.EX (snd $3, $4)} | AX WITH_TRANSITION transition_label formula_with_paren - { Logging.out "\tParsed AX with transition '%s'\n" (fst $3); + { L.(debug Linters Verbose) "\tParsed AX with transition '%s'@\n" (fst $3); CTL.AX (snd $3, $4)} - | formula AND formula { Logging.out "\tParsed AND\n"; CTL.And ($1, $3) } - | formula OR formula { Logging.out "\tParsed OR\n"; CTL.Or ($1, $3) } - | formula IMPLIES formula { Logging.out "\tParsed IMPLIES\n"; CTL.Implies ($1, $3) } - | NOT formula { Logging.out "\tParsed NOT\n"; CTL.Not ($2) } + | formula AND formula { L.(debug Linters Verbose) "\tParsed AND@\n"; CTL.And ($1, $3) } + | formula OR formula { L.(debug Linters Verbose) "\tParsed OR@\n"; CTL.Or ($1, $3) } + | formula IMPLIES formula + { L.(debug Linters Verbose) "\tParsed IMPLIES@\n"; CTL.Implies ($1, $3) } + | NOT formula { L.(debug Linters Verbose) "\tParsed NOT@\n"; CTL.Not ($2) } ; alexp: | STRING { is_not_infer_reserved_id $1; - Logging.out "\tParsed string constant '%s' \n" $1; + L.(debug Linters Verbose) "\tParsed string constant '%s'@\n" $1; ALVar.Const $1 } | REGEXP LEFT_PAREN STRING RIGHT_PAREN - { Logging.out "\tParsed regular expression '%s' \n" $3; + { L.(debug Linters Verbose) "\tParsed regular expression '%s'@\n" $3; ALVar.Regexp $3 } | identifier { is_defined_identifier $1; ALVar.Var $1 } ; identifier: | IDENTIFIER { is_not_infer_reserved_id $1; - Logging.out "\tParsed identifier '%s' \n" $1; $1 } + L.(debug Linters Verbose) "\tParsed identifier '%s'@\n" $1; $1 } ; file_identifier: | FILE_IDENTIFIER { is_not_infer_reserved_id $1; - Logging.out "\tParsed file identifier '%s' \n" $1; $1 } + L.(debug Linters Verbose) "\tParsed file identifier '%s'@\n" $1; $1 } ; %% diff --git a/infer/src/clang/ctl_parser_types.ml b/infer/src/clang/ctl_parser_types.ml index 15ea0c666..178c6e78b 100644 --- a/infer/src/clang/ctl_parser_types.ml +++ b/infer/src/clang/ctl_parser_types.ml @@ -7,10 +7,11 @@ * of patent rights can be found in the PATENTS file in the same directory. *) -open! IStd +(* Types used by the ctl parser *) +open! IStd -(* Types used by the ctl parser *) +module L = Logging (** the kind of AST nodes where formulas are evaluated *) type ast_node = @@ -127,10 +128,10 @@ type abs_ctype = | TypeName of ALVar.alexp let display_equality_warning () = - Logging.out + L.(debug Linters Medium) "[WARNING:] Type Comparison failed... \ This might indicate that the types are different or the specified type \ - is internally represented in a different way and therefore not recognized.\n" + is internally represented in a different way and therefore not recognized.@\n" let rec abs_ctype_to_string t = match t with @@ -203,9 +204,9 @@ and typename_equal pointer typename = by the types_parser. It needs to be replaced by a real comparison function for Clang_ast_t.c_type *) and c_type_equal c_type abs_ctype = - Logging.out + L.(debug Linters Medium) "Comparing c_type/abs_ctype for equality... \ - Type compared: \nc_type = `%s` \nabs_ctype =`%s`\n" + Type compared: @\nc_type = `%s` @\nabs_ctype =`%s`@\n" (Clang_ast_j.string_of_c_type c_type) (abs_ctype_to_string abs_ctype); let open Clang_ast_t in diff --git a/infer/src/clang/objcCategory_decl.ml b/infer/src/clang/objcCategory_decl.ml index a1cb385c8..c0080c4ee 100644 --- a/infer/src/clang/objcCategory_decl.ml +++ b/infer/src/clang/objcCategory_decl.ml @@ -77,7 +77,8 @@ let process_category qual_type_to_sil_type tenv class_name decl_info decl_list = ignore( Tenv.mk_struct tenv ~default:struct_typ ~fields:new_fields ~statics:[] ~methods:[] class_tn_name ); - Logging.out_debug " Updating info for class '%a' in tenv\n" QualifiedCppName.pp class_name + L.(debug Capture Verbose) " Updating info for class '%a' in tenv@\n" + QualifiedCppName.pp class_name | _ -> ()); class_tn_desc @@ -87,7 +88,7 @@ let category_decl qual_type_to_sil_type tenv decl = | ObjCCategoryDecl (decl_info, name_info, decl_list, _, cdi) -> let name = CAst_utils.get_qualified_name name_info in let class_name = get_classname_from_category_decl cdi in - Logging.out_debug "ADDING: ObjCCategoryDecl for '%a'\n" QualifiedCppName.pp name; + L.(debug Capture Verbose) "ADDING: ObjCCategoryDecl for '%a'@\n" QualifiedCppName.pp name; let _ = add_class_decl qual_type_to_sil_type tenv cdi in let typ = process_category qual_type_to_sil_type tenv class_name decl_info decl_list in let _ = add_category_implementation qual_type_to_sil_type tenv cdi in @@ -100,7 +101,7 @@ let category_impl_decl qual_type_to_sil_type tenv decl = | ObjCCategoryImplDecl (decl_info, name_info, decl_list, _, cii) -> let name = CAst_utils.get_qualified_name name_info in let class_name = get_classname_from_category_impl cii in - Logging.out_debug "ADDING: ObjCCategoryImplDecl for '%a'\n" QualifiedCppName.pp name; + L.(debug Capture Verbose) "ADDING: ObjCCategoryImplDecl for '%a'@\n" QualifiedCppName.pp name; let _ = add_category_decl qual_type_to_sil_type tenv cii in let typ = process_category qual_type_to_sil_type tenv class_name decl_info decl_list in typ diff --git a/infer/src/clang/objcInterface_decl.ml b/infer/src/clang/objcInterface_decl.ml index 1896ee3ff..582401a28 100644 --- a/infer/src/clang/objcInterface_decl.ml +++ b/infer/src/clang/objcInterface_decl.ml @@ -76,7 +76,7 @@ let create_supers_fields qual_type_to_sil_type tenv decl_list (* Adds pairs (interface name, interface_type_info) to the global environment. *) let add_class_to_tenv qual_type_to_sil_type tenv decl_info name_info decl_list ocidi = let class_name = CAst_utils.get_qualified_name name_info in - Logging.out_debug "ADDING: ObjCInterfaceDecl for '%a'\n" QualifiedCppName.pp class_name; + L.(debug Capture Verbose) "ADDING: ObjCInterfaceDecl for '%a'@\n" QualifiedCppName.pp class_name; let interface_name = Typ.Name.Objc.from_qual_name class_name in let interface_desc = Typ.Tstruct interface_name in let decl_key = Clang_ast_extend.DeclPtr decl_info.Clang_ast_t.di_pointer in @@ -87,8 +87,8 @@ let add_class_to_tenv qual_type_to_sil_type tenv decl_info name_info decl_list o ocidi.Clang_ast_t.otdi_protocols in let fields_sc = CField_decl.fields_superclass tenv ocidi in List.iter ~f:(fun (fn, ft, _) -> - Logging.out_debug "----->SuperClass field: '%s' " (Fieldname.to_string fn); - Logging.out_debug "type: '%s'\n" (Typ.to_string ft)) fields_sc; + L.(debug Capture Verbose) "----->SuperClass field: '%s' " (Fieldname.to_string fn); + L.(debug Capture Verbose) "type: '%s'@\n" (Typ.to_string ft)) fields_sc; (*In case we found categories, or partial definition of this class earlier and they are already in the tenv *) let fields, (supers : Typ.Name.t list) = match Tenv.lookup tenv interface_name with @@ -101,19 +101,19 @@ let add_class_to_tenv qual_type_to_sil_type tenv decl_info name_info decl_list o (* We add the special hidden counter_field for implementing reference counting *) let modelled_fields = Typ.Struct.objc_ref_counter_field :: CField_decl.modelled_field name_info in let all_fields = CGeneral_utils.append_no_duplicates_fields modelled_fields fields in - Logging.out_debug "Class %a field:\n" QualifiedCppName.pp class_name; + L.(debug Capture Verbose) "Class %a field:@\n" QualifiedCppName.pp class_name; List.iter ~f:(fun (fn, _, _) -> - Logging.out_debug "-----> field: '%s'\n" (Fieldname.to_string fn)) all_fields; + L.(debug Capture Verbose) "-----> field: '%s'@\n" (Fieldname.to_string fn)) all_fields; ignore( Tenv.mk_struct tenv ~fields: all_fields ~supers ~methods:[] ~annots:Annot.Class.objc interface_name ); - Logging.out_debug - " >>>Verifying that Typename '%s' is in tenv\n" (Typ.Name.to_string interface_name); + L.(debug Capture Verbose) + " >>>Verifying that Typename '%s' is in tenv@\n" (Typ.Name.to_string interface_name); (match Tenv.lookup tenv interface_name with | Some st -> - Logging.out_debug " >>>OK. Found typ='%a'\n" + L.(debug Capture Verbose) " >>>OK. Found typ='%a'@\n" (Typ.Struct.pp Pp.text interface_name) st - | None -> Logging.out_debug " >>>NOT Found!!\n"); + | None -> L.(debug Capture Verbose) " >>>NOT Found!!@\n"); interface_desc (* Interface_type_info has the name of instance variables and the name of methods. *) @@ -137,8 +137,8 @@ let interface_impl_declaration qual_type_to_sil_type tenv decl = match decl with | ObjCImplementationDecl (decl_info, name_info, decl_list, _, idi) -> let class_name = CAst_utils.get_qualified_name name_info in - Logging.out_debug - "ADDING: ObjCImplementationDecl for class '%a'\n" QualifiedCppName.pp class_name; + L.(debug Capture Verbose) + "ADDING: ObjCImplementationDecl for class '%a'@\n" QualifiedCppName.pp class_name; let _ = add_class_decl qual_type_to_sil_type tenv idi in let fields = CField_decl.get_fields qual_type_to_sil_type tenv decl_list in CField_decl.add_missing_fields tenv class_name fields; diff --git a/infer/src/clang/objcProtocol_decl.ml b/infer/src/clang/objcProtocol_decl.ml index a1d06d19e..69db70f26 100644 --- a/infer/src/clang/objcProtocol_decl.ml +++ b/infer/src/clang/objcProtocol_decl.ml @@ -24,7 +24,7 @@ let protocol_decl qual_type_to_sil_type tenv decl = (* Protocol_type_info contains the methods composing the protocol. *) (* Here we are giving a similar treatment as interfaces (see above)*) (* It may turn out that we need a more specific treatment for protocols*) - Logging.out_debug "ADDING: ObjCProtocolDecl for '%a'\n" QualifiedCppName.pp name; + L.(debug Capture Verbose) "ADDING: ObjCProtocolDecl for '%a'@\n" QualifiedCppName.pp name; let protocol_name = Typ.Name.Objc.protocol_from_qual_name name in let protocol_desc = Typ.Tstruct protocol_name in let decl_key = Clang_ast_extend.DeclPtr decl_info.Clang_ast_t.di_pointer in diff --git a/infer/src/clang/types_parser.mly b/infer/src/clang/types_parser.mly index 72e71c8fe..e3404092b 100644 --- a/infer/src/clang/types_parser.mly +++ b/infer/src/clang/types_parser.mly @@ -12,6 +12,8 @@ open Ctl_parser_types + module L = Logging + (* See StringRef BuiltinType::getName in https://clang.llvm.org/doxygen/Type_8cpp_source.html *) let tokens_to_abs_types l = @@ -68,7 +70,7 @@ abs_ctype: | ctype_specifier_seq EOF { - Logging.out "\tType effectively parsed: `%s`\n" + L.(debug Linters Verbose) "\tType effectively parsed: `%s`@\n" (Ctl_parser_types.abs_ctype_to_string $1); $1 } ; @@ -130,10 +132,10 @@ simple_type_specifier: ; alexp: - | STRING { Logging.out "\tParsed string constant '%s' \n" $1; + | STRING { L.(debug Linters Verbose) "\tParsed string constant '%s' @\n" $1; ALVar.Const $1 } | REGEXP LEFT_PAREN REARG RIGHT_PAREN - { Logging.out "\tParsed regular expression '%s' \n" $3; + { L.(debug Linters Verbose) "\tParsed regular expression '%s' @\n" $3; ALVar.Regexp $3 } | IDENTIFIER { ALVar.Var $1 } ; diff --git a/infer/src/eradicate/AnnotatedSignature.ml b/infer/src/eradicate/AnnotatedSignature.ml index 1aa80c3f6..c9908ddb9 100644 --- a/infer/src/eradicate/AnnotatedSignature.ml +++ b/infer/src/eradicate/AnnotatedSignature.ml @@ -118,10 +118,10 @@ let mark proc_name ann asig (b, bs) = (s, ia', t) in let params' = let fail () = - L.stderr + L.internal_error "INTERNAL ERROR: annotation for procedure %s has wrong number of arguments@." (Typ.Procname.to_unique_id proc_name); - L.stderr " ANNOTATED SIGNATURE: %a@." (pp proc_name) asig; + L.internal_error " ANNOTATED SIGNATURE: %a@." (pp proc_name) asig; assert false in let rec combine l1 l2 = match l1, l2 with | (p, ia, t):: l1', l2' when String.equal (Mangled.to_string p) "this" -> diff --git a/infer/src/eradicate/eradicate.ml b/infer/src/eradicate/eradicate.ml index fea04f9f4..2337fd503 100644 --- a/infer/src/eradicate/eradicate.ml +++ b/infer/src/eradicate/eradicate.ml @@ -107,7 +107,7 @@ struct let do_before_dataflow initial_typestate = if Config.eradicate_verbose then - L.stdout "Initial Typestate@\n%a@." + L.result "Initial Typestate@\n%a@." (TypeState.pp Extension.ext) initial_typestate in let do_after_dataflow find_canonical_duplicate final_typestate = @@ -324,7 +324,7 @@ struct proc_loc end; if Config.eradicate_verbose then - L.stdout "Final Typestate@\n%a@." + L.result "Final Typestate@\n%a@." (TypeState.pp Extension.ext) typestate in match typestate_opt with | None -> () @@ -366,7 +366,7 @@ struct let loc = Procdesc.get_loc proc_desc in let linereader = Printer.LineReader.create () in if Config.eradicate_verbose then - L.stdout "%a@." (AnnotatedSignature.pp proc_name) annotated_signature; + L.result "%a@." (AnnotatedSignature.pp proc_name) annotated_signature; callback2 calls_this checks callback_args annotated_signature linereader loc diff --git a/infer/src/eradicate/models.ml b/infer/src/eradicate/models.ml index 787695e50..5fdfe1a72 100644 --- a/infer/src/eradicate/models.ml +++ b/infer/src/eradicate/models.ml @@ -45,7 +45,7 @@ module Inference = struct if String.is_empty s_old then 0 else try int_of_string s_old with | Failure _ -> - L.stderr "int_of_string %s@." s_old; + L.internal_error "int_of_string %s@." s_old; assert false in string_of_int (n + 1) @@ -57,8 +57,8 @@ module Inference = struct let mark_file update_str dir fname = DB.update_file_with_lock dir fname update_str; match DB.read_file_with_lock dir fname with - | Some buf -> L.stderr "Read %s: %s@." fname buf - | None -> L.stderr "Read %s: None@." fname + | Some buf -> L.internal_error "Read %s: %s@." fname buf + | None -> L.internal_error "Read %s: None@." fname let mark_file_count = mark_file update_count_str diff --git a/infer/src/eradicate/typeCheck.ml b/infer/src/eradicate/typeCheck.ml index c8763fe6b..47cc3352b 100644 --- a/infer/src/eradicate/typeCheck.ml +++ b/infer/src/eradicate/typeCheck.ml @@ -886,7 +886,7 @@ let typecheck_instr let unique_id = Typ.Procname.to_unique_id callee_pname in let classification = EradicateChecks.classify_procedure callee_attributes in - L.stdout " %s unique id: %s@." classification unique_id + L.result " %s unique id: %s@." classification unique_id end; if cflags.CallFlags.cf_virtual && checks.eradicate then EradicateChecks.check_call_receiver tenv diff --git a/infer/src/eradicate/typeErr.ml b/infer/src/eradicate/typeErr.ml index 7e8e79af0..fe9b243b3 100644 --- a/infer/src/eradicate/typeErr.ml +++ b/infer/src/eradicate/typeErr.ml @@ -243,13 +243,13 @@ let report_error_now tenv (st_report_error : st_report_error) err_instance loc pdesc : unit = let pname = Procdesc.get_proc_name pdesc in let do_print ew_string kind s = - L.stdout "%a:%d " SourceFile.pp loc.Location.file loc.Location.line; + L.progress "%a:%d " SourceFile.pp loc.Location.file loc.Location.line; let mname = match pname with | Typ.Procname.Java pname_java -> Typ.Procname.java_get_method pname_java | _ -> Typ.Procname.to_simplified_string pname in - L.stdout "%s %s in %s %s@." ew_string (Localise.to_issue_id kind) mname s in + L.progress "%s %s in %s %s@." ew_string (Localise.to_issue_id kind) mname s in let is_err, kind, description, advice, field_name, origin_loc = match err_instance with | Condition_redundant (b, s_opt, nonnull) -> diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index 8c803fbcd..411af409d 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -142,7 +142,7 @@ let rec inhabit_typ tenv typ cfg env = | Typ.Tint (_) -> (Exp.Const (Const.Cint (IntLit.zero)), env) | Typ.Tfloat (_) -> (Exp.Const (Const.Cfloat 0.0), env) | _ -> - L.out "Couldn't inhabit typ: %a@." (Typ.pp Pp.text) typ; + L.internal_error "Couldn't inhabit typ: %a@." (Typ.pp Pp.text) typ; assert false in let (inhabited_exp, env') = inhabit_internal typ { env with cur_inhabiting = TypSet.add typ env.cur_inhabiting } in @@ -215,7 +215,7 @@ let create_dummy_harness_filename harness_name = let write_harness_to_file harness_instrs harness_file_name = let harness_file = Utils.create_outfile harness_file_name in let pp_harness fmt = List.iter ~f:(fun instr -> - Format.fprintf fmt "%a\n" (Sil.pp_instr Pp.text) instr) harness_instrs in + Format.fprintf fmt "%a@\n" (Sil.pp_instr Pp.text) instr) harness_instrs in Utils.do_outf harness_file (fun outf -> pp_harness outf.fmt; Utils.close_outf outf) diff --git a/infer/src/integration/CaptureCompilationDatabase.ml b/infer/src/integration/CaptureCompilationDatabase.ml index b777d54fe..3367a756a 100644 --- a/infer/src/integration/CaptureCompilationDatabase.ml +++ b/infer/src/integration/CaptureCompilationDatabase.ml @@ -9,9 +9,11 @@ open! IStd -module CLOpt = CommandLineOption module F = Format +module CLOpt = CommandLineOption +module L = Logging + let capture_text = if Config.equal_analyzer Config.analyzer Config.Linters then "linting" else "translating" @@ -22,7 +24,7 @@ let should_capture_file_from_index () = | None -> (match Config.changed_files_index with | Some index -> - Process.print_error_and_exit "Error reading the changed files index %s.\n%!" index + Process.print_error_and_exit "Error reading the changed files index %s.@\n%!" index | None -> function _ -> true) | Some files_set -> function source_file -> SourceFile.Set.mem source_file files_set @@ -58,13 +60,13 @@ let run_compilation_file compilation_database file = (Option.to_list (Sys.getenv CLOpt.args_env_var) @ ["--fcp-syntax-only"]))] in (Some compilation_data.dir, wrapper_cmd, args, env) with Not_found -> - Process.print_error_and_exit "Failed to find compilation data for %a \n%!" + Process.print_error_and_exit "Failed to find compilation data for %a@\n%!" SourceFile.pp file let run_compilation_database compilation_database should_capture_file = let number_of_files = CompilationDatabase.get_size compilation_database in - Logging.out "Starting %s %d files \n%!" capture_text number_of_files; - Logging.progress "Starting %s %d files \n%!" capture_text number_of_files; + L.(debug Capture Quiet) "Starting %s %d files@\n%!" capture_text number_of_files; + L.progress "Starting %s %d files@\n%!" capture_text number_of_files; let jobs_stack = create_files_stack compilation_database should_capture_file in let capture_text_upper = String.capitalize capture_text in let job_to_string = @@ -99,9 +101,9 @@ let get_compilation_database_files_buck ~prog ~args = (Unix.Exit_or_signal.to_string_hum status) | Ok () -> match output with - | [] -> Logging.stderr "There are no files to process, exiting@."; exit 0 + | [] -> L.external_error "There are no files to process, exiting@."; exit 0 | lines -> - Logging.out "Reading compilation database from:@\n%s@\n" + L.(debug Capture Quiet) "Reading compilation database from:@\n%s@\n" (String.concat ~sep:"\n" lines); (* this assumes that flavors do not contain spaces *) let split_regex = Str.regexp "#[^ ]* " in @@ -128,7 +130,7 @@ let get_compilation_database_files_xcodebuild ~prog ~args = let xcpretty_prog = "xcpretty" in let xcpretty_args = [xcpretty_prog; "--report"; "json-compilation-database"; "--output"; tmp_file] in - Logging.out "Running %s | %s\n@." (List.to_string ~f:Fn.id xcodebuild_args) + L.(debug Capture Quiet) "Running %s | %s@\n@." (List.to_string ~f:Fn.id xcodebuild_args) (List.to_string ~f:Fn.id xcpretty_args); let producer_status, consumer_status = Process.pipeline @@ -137,7 +139,7 @@ let get_compilation_database_files_xcodebuild ~prog ~args = match producer_status, consumer_status with | Ok (), Ok () -> [`Escaped tmp_file] | _ -> - Logging.stderr "There was an error executing the build command"; + L.external_error "There was an error executing the build command"; exit 1 let capture_files_in_database compilation_database = diff --git a/infer/src/integration/Clang.ml b/infer/src/integration/Clang.ml index d69dda78a..074337092 100644 --- a/infer/src/integration/Clang.ml +++ b/infer/src/integration/Clang.ml @@ -8,38 +8,49 @@ *) open! IStd +module F = Format + +module L = Logging + type compiler = | Clang | Make [@@deriving compare] -let extended_env_to_string (env : Unix.env) = +let rec pp_list pp fmt = function + | [] -> () + | x::[] -> pp fmt x + | x::tl -> F.fprintf fmt "%a@\n%a" pp x (pp_list pp) tl + +let pp_env fmt env = + pp_list (fun fmt s -> F.fprintf fmt "%s" s) fmt env + +let pp_extended_env fmt (env : Unix.env) = + let pp_pair fmt (var, value) = + F.fprintf fmt "%s=%s" var value in + let pp_pair_list = pp_list pp_pair in match env with - | `Replace values + | `Replace values -> + pp_pair_list fmt values | `Extend values -> - let concat_elt (el1, el2) = String.concat ~sep:"=" [el1; el2] in - String.concat ~sep:"\n" (List.map ~f:concat_elt values) + let is_extended s = + match String.lsplit2 s ~on:'=' with + | Some (var, _) -> List.exists ~f:(fun (var', _) -> String.equal var var') values + | None -> false in + let env_not_extended = Unix.environment () |> Array.to_list + |> List.filter ~f:(Fn.non is_extended) in + F.fprintf fmt "%a@\n%a" pp_env env_not_extended pp_pair_list values | `Replace_raw values -> - String.concat ~sep:"\n" values - -let env_to_string ?exclude_var env = - let env_element_to_string elt acc = - match exclude_var with - | Some var when String.is_prefix ~prefix:var elt -> "" - | _ -> - String.concat [elt; acc] ~sep:"\n" in - Array.fold_right ~init:"" ~f:env_element_to_string env + pp_env fmt values let capture compiler ~prog ~args = match compiler with - | Clang -> ClangWrapper.exe ~prog ~args + | Clang -> + ClangWrapper.exe ~prog ~args | Make -> let path_var = "PATH" in let new_path = Config.wrappers_dir ^ ":" ^ (Sys.getenv_exn path_var) in let extended_env = `Extend [path_var, new_path] in - Logging.out "Running command %s with env:\n%s %s\n@." - prog - (env_to_string ~exclude_var:path_var (Unix.environment ())) - (extended_env_to_string extended_env); + L.environment_info "Running command %s with env:@\n%a@\n@." prog pp_extended_env extended_env; Unix.fork_exec ~prog:prog ~args:(prog::args) ~env:extended_env () |> Unix.waitpid |> function diff --git a/infer/src/integration/ClangQuotes.re b/infer/src/integration/ClangQuotes.re index c7f27e692..07de124f3 100644 --- a/infer/src/integration/ClangQuotes.re +++ b/infer/src/integration/ClangQuotes.re @@ -6,9 +6,11 @@ * LICENSE file in the root directory of this source tree. An additional grant * of patent rights can be found in the PATENTS file in the same directory. */ +/* module for escaping clang arguments on the command line and put them into files */ open! IStd; -/* module for escaping clang arguments on the command line and put them into files */ +module L = Logging; + /** quoting style of the arguments */ type style = @@ -37,6 +39,6 @@ let mk_arg_file prefix style args => { let write_args outc => output_string outc (List.map f::(quote style) args |> String.concat sep::" "); Utils.with_file_out file f::write_args |> ignore; - Logging.out "Clang options stored in file %s@\n" file; + L.(debug Capture Medium) "Clang options stored in file %s@\n" file; file }; diff --git a/infer/src/integration/CompilationDatabase.ml b/infer/src/integration/CompilationDatabase.ml index c67c6eecf..78c53e341 100644 --- a/infer/src/integration/CompilationDatabase.ml +++ b/infer/src/integration/CompilationDatabase.ml @@ -9,6 +9,8 @@ open! IStd +module L = Logging + type compilation_data = { dir : string; command : string; @@ -44,7 +46,7 @@ let decode_json_file (database : t) json_format = | `Escaped _ -> Utils.with_process_in (Printf.sprintf "/bin/sh -c 'printf \"%%s\" %s'" s) input_line |> fst in - Logging.out "parsing compilation database from %s@\n" json_path; + L.(debug Capture Quiet) "parsing compilation database from %s@\n" json_path; let exit_format_error () = failwith ("Json file doesn't have the expected format") in let json = Yojson.Basic.from_file json_path in @@ -85,5 +87,5 @@ let decode_json_file (database : t) json_format = let from_json_files db_json_files = let db = empty () in List.iter ~f:(decode_json_file db) db_json_files; - Logging.out "created database with %d entries@\n" (get_size db); + L.(debug Capture Quiet) "created database with %d entries@\n" (get_size db); db diff --git a/infer/src/integration/Javac.ml b/infer/src/integration/Javac.ml index 97419ef14..766296c3d 100644 --- a/infer/src/integration/Javac.ml +++ b/infer/src/integration/Javac.ml @@ -46,20 +46,21 @@ let compile compiler build_prog build_args = file in let cli_file_args = cli_args @ ["@" ^ args_file] in let args = prog_args @ cli_file_args in - L.out "Current working directory: '%s'@." (Sys.getcwd ()); + L.(debug Capture Quiet) "Current working directory: '%s'@." (Sys.getcwd ()); let verbose_out_file = Filename.temp_file "javac_" ".out" in let try_run cmd error_k = let shell_cmd = Utils.shell_escape_command cmd in let shell_cmd_redirected = Printf.sprintf "%s 2>'%s'" shell_cmd verbose_out_file in - L.out "Trying to execute: %s@." shell_cmd_redirected; + L.(debug Capture Quiet) "Trying to execute: %s@." shell_cmd_redirected; let error_k_or_fail err_msg = match error_k, err_msg with | Some k, (`UnixError (err, log)) -> - L.out "*** Failed: %s!@\n%s@." (Unix.Exit_or_signal.to_string_hum (Error err)) log; + L.(debug Capture Quiet) "*** Failed: %s!@\n%s@." + (Unix.Exit_or_signal.to_string_hum (Error err)) log; k () | Some k, (`ExceptionError exn) -> - L.out "*** Failed: %a!@\n" Exn.pp exn; + L.(debug Capture Quiet) "*** Failed: %a!@\n" Exn.pp exn; k () | None, (`UnixError (err, log)) -> let verbose_errlog = Utils.with_file_in verbose_out_file ~f:In_channel.input_all in @@ -74,7 +75,7 @@ let compile compiler build_prog build_args = | exception exn -> error_k_or_fail (`ExceptionError exn) | (log, Ok ()) -> - L.out "*** Success. Logs:@\n%s" log in + L.(debug Capture Quiet) "*** Success. Logs:@\n%s" log in let fallback () = try_run ("javac"::cli_file_args) None in try_run (prog::args) (Some fallback); verbose_out_file diff --git a/infer/src/integration/Maven.ml b/infer/src/integration/Maven.ml index f3bb31986..790773304 100644 --- a/infer/src/integration/Maven.ml +++ b/infer/src/integration/Maven.ml @@ -87,11 +87,11 @@ let add_infer_profile_to_xml dir maven_xml infer_xml = Xmlm.output xml_out elt_in; (match tag_stack with | "id"::"profile"::"profiles"::_ when String.equal data infer_profile_name -> - L.do_out "Found infer profile, not adding one@."; + L.(debug Capture Quiet) "Found infer profile, not adding one@."; found_infer_profile := true | "module"::"modules"::_ -> let abs_data = dir ^/ data in - L.do_out "Adding maven module %s@." abs_data; + L.(debug Capture Quiet) "Adding maven module %s@." abs_data; pom_worklist := abs_data::!pom_worklist | _ -> () ); @@ -149,7 +149,7 @@ let capture ~prog ~args = done; let extra_args = "-P"::infer_profile_name::[] in let capture_args = args @ extra_args in - L.do_out "Running maven capture:@\n%s %s@." prog + L.(debug Capture Quiet) "Running maven capture:@\n%s %s@." prog (String.concat ~sep:" " (List.map ~f:(Printf.sprintf "'%s'") capture_args)); (* let children infer processes know that they are spawned by Maven *) Unix.fork_exec ~prog ~args:(prog::capture_args) ~env:Config.env_inside_maven () diff --git a/infer/src/java/jClasspath.ml b/infer/src/java/jClasspath.ml index 2e84a0704..3e249d131 100644 --- a/infer/src/java/jClasspath.ml +++ b/infer/src/java/jClasspath.ml @@ -326,7 +326,7 @@ let collect_classes start_classmap jar_filename = let load_program classpath classes = - L.out_debug "loading program ... %!"; + L.(debug Capture Medium) "loading program ... %!"; let models = if String.equal !models_jar "" then JBasics.ClassMap.empty else collect_classes JBasics.ClassMap.empty !models_jar in @@ -338,5 +338,5 @@ let load_program classpath classes = JBasics.ClassSet.iter (fun cn -> ignore (lookup_node cn program)) classes; - L.out_debug "done@."; + L.(debug Capture Medium) "done@."; program diff --git a/infer/src/java/jFrontend.ml b/infer/src/java/jFrontend.ml index 02616007d..669895563 100644 --- a/infer/src/java/jFrontend.ml +++ b/infer/src/java/jFrontend.ml @@ -138,14 +138,15 @@ let is_classname_cached cn = 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 source_file linereader program icfg cn node = - L.out_debug "\tclassname: %s@." (JBasics.cn_name cn); + L.(debug Capture Verbose) "\tclassname: %s@." (JBasics.cn_name cn); if Config.dependency_mode && not (is_classname_cached cn) then cache_classname cn; let translate m = let proc_name = JTransType.translate_method_name m in if JClasspath.is_model proc_name then (* do not translate the method if there is a model for it *) - L.out_debug "Skipping method with a model: %s@." (Typ.Procname.to_string proc_name) + L.(debug Capture Verbose) "Skipping method with a model: %s@." + (Typ.Procname.to_string proc_name) else try (* each procedure has different scope: start names from id 0 *) @@ -161,7 +162,7 @@ let create_icfg source_file linereader program icfg cn node = end; Cg.add_defined_node icfg.JContext.cg proc_name with JBasics.Class_structure_error _ -> - L.stderr + L.internal_error "create_icfg raised JBasics.Class_structure_error on %a@." Typ.Procname.pp proc_name in Javalib.m_iter translate node diff --git a/infer/src/java/jMain.ml b/infer/src/java/jMain.ml index b344694a5..77d22d2c8 100644 --- a/infer/src/java/jMain.ml +++ b/infer/src/java/jMain.ml @@ -54,8 +54,7 @@ let store_icfg source_file tenv cg cfg = let do_source_file linereader classes program tenv source_basename package_opt source_file = - L.out_debug "\nfilename: %a (%s)@." - SourceFile.pp source_file source_basename; + L.(debug Capture Medium) "@\nfilename: %a (%s)@." SourceFile.pp source_file source_basename; let call_graph, cfg = JFrontend.compute_source_icfg linereader classes program tenv @@ -99,13 +98,13 @@ let save_tenv tenv = if not Config.models_mode then JTransType.add_models_types tenv; (* TODO: this prevents per compilation step incremental analysis at this stage *) if DB.file_exists DB.global_tenv_fname then DB.file_remove DB.global_tenv_fname; - L.out_debug "writing new tenv %s@." (DB.filename_to_string DB.global_tenv_fname); + L.(debug Capture Medium) "writing new tenv %s@." (DB.filename_to_string DB.global_tenv_fname); Tenv.store_to_file DB.global_tenv_fname tenv (* The program is loaded and translated *) let do_all_files classpath sources classes = - L.do_out "Translating %d source files (%d classes)@." + L.(debug Capture Quiet) "Translating %d source files (%d classes)@." (String.Map.length sources) (JBasics.ClassSet.cardinal classes); let program = JClasspath.load_program classpath classes in @@ -130,14 +129,14 @@ let do_all_files classpath sources classes = | JClasspath.Duplicate source_files -> List.iter ~f:(fun (package, source_file) -> - translate_source_file basename (Some package, source_file) source_file) + translate_source_file basename (Some package, source_file) source_file) source_files) sources; if Config.dependency_mode then capture_libs linereader program tenv; save_tenv tenv; JClasspath.cleanup program; - L.out_debug "done @." + L.(debug Capture Quiet) "done capturing all files@." (* loads the source files and translates them *) let main load_sources_and_classes = diff --git a/infer/src/java/jTrans.ml b/infer/src/java/jTrans.ml index b263064a4..a1a50f8f7 100644 --- a/infer/src/java/jTrans.ml +++ b/infer/src/java/jTrans.ml @@ -115,7 +115,7 @@ let get_field_name program static tenv cn fs = fieldname | None -> (* TODO: understand why fields cannot be found here *) - L.stderr "cannot find %s.%s@." (JBasics.cn_name cn) (JBasics.fs_name fs); + L.internal_error "cannot find %s.%s@." (JBasics.cn_name cn) (JBasics.fs_name fs); raise (Frontend_error "Cannot find fieldname") @@ -380,7 +380,7 @@ let create_cm_procdesc source_file program linereader icfg cm proc_name = procdesc in Some (procdesc, bytecode, jbir_code) with JBir.Subroutine -> - L.stderr + L.internal_error "create_procdesc raised JBir.Subroutine on %a@." Typ.Procname.pp proc_name; None @@ -1067,5 +1067,5 @@ let rec instruction (context : JContext.t) pc instr : translation = | _ -> Skip with Frontend_error s -> - L.stderr "Skipping because of: %s@." s; + L.internal_error "Skipping because of: %s@." s; Skip diff --git a/infer/src/java/jTransType.ml b/infer/src/java/jTransType.ml index 025fffde3..1b3f2035f 100644 --- a/infer/src/java/jTransType.ml +++ b/infer/src/java/jTransType.ml @@ -13,6 +13,8 @@ open! IStd open Javalib_pack open Sawja_pack +module L = Logging + (** Type transformations between Javalib datatypes and sil datatypes *) exception Type_tranlsation_error of string @@ -249,7 +251,8 @@ let collect_models_class_fields classpath_field_map cn cf fields = if Typ.equal classpath_ft field_type then fields else (* TODO (#6711750): fix type equality for arrays before failing here *) - let () = Logging.stderr "Found inconsistent types for %s\n\tclasspath: %a\n\tmodels: %a\n@." + let () = L.(debug Capture Quiet) + "Found inconsistent types for %s@\n\tclasspath: %a@\n\tmodels: %a@\n@." (Fieldname.to_string field_name) (Typ.pp_full Pp.text) classpath_ft (Typ.pp_full Pp.text) field_type in fields diff --git a/infer/src/quandary/TaintAnalysis.ml b/infer/src/quandary/TaintAnalysis.ml index b1c318dd5..e4d08da4e 100644 --- a/infer/src/quandary/TaintAnalysis.ml +++ b/infer/src/quandary/TaintAnalysis.ml @@ -446,7 +446,7 @@ module Make (TaintSpecification : TaintSpec.S) = struct called_pname :: call_flags.cf_targets else begin - L.out + L.(debug Analysis Medium) "Skipping highly polymorphic call site for %a@." Typ.Procname.pp called_pname; [called_pname] end in