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

[log] log to a single file with different categories and debug levels

Browse Source 
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 ^[<PID>] 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
master
Jules Villard 8 years ago committed by Facebook Github Bot
parent 03bd3f1df1
commit 93cc3266e8
94 changed files with 1161 additions and 892 deletions
Show Stats Download Patch File Download Diff File

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

@ -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
};

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

@ -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

2
infer/src/IR/Errlog.ml
Unescape View File

@ -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 =

2
infer/src/IR/Io_infer.ml
Unescape View File

@ -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" "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n"
let pp_prelude fmt = pp fmt "%s" "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n"
let pp_open fmt name =
pp_prelude fmt;

4
infer/src/IR/Procdesc.re
Unescape View File

@ -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
};
};

10
infer/src/IR/Typ.re
Unescape View File

@ -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

6
infer/src/backend/BuiltinDefn.ml
Unescape View File

@ -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 =

13
infer/src/backend/InferAnalyze.re
Unescape View File

@ -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
};

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

@ -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
}
}
};

10
infer/src/backend/OndemandCapture.ml
Unescape View File

@ -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

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

@ -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 =

21
infer/src/backend/abs.ml
Unescape View File

@ -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

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

@ -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"

2
infer/src/backend/clusterMakefile.ml
Unescape View File

@ -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)@."

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

@ -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;

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

@ -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

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

@ -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 *)

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

@ -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

59
infer/src/backend/infer.ml
Unescape View File

@ -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:"<not found>");
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:"<not found>");
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 ()

10
infer/src/backend/inferconfig.ml
Unescape View File

@ -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 ())

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

@ -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 *)

8
infer/src/backend/match.ml
Unescape View File

@ -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

16
infer/src/backend/mergeCapture.ml
Unescape View File

@ -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,

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

@ -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 ());

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

@ -133,7 +133,7 @@ end = struct
(F.fprintf fmt "<center><h1>Cfg Node %a</h1></center>"
(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 "<center><h1>File %a </h1></center>\n<table class=\"code\">\n"
F.fprintf fmt "<center><h1>File %a </h1></center>@\n<table class=\"code\">@\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" "</td></tr>\n" in
F.fprintf fmt "%s" "</td></tr>@\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" "</table>\n";
(F.fprintf fmt "%s" "</table>@\n";
Errlog.pp_html filename [fname_encoding] fmt global_err_log;
Io_infer.Html.close (fd, fmt))

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

@ -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

2
infer/src/backend/rearrange.ml
Unescape View File

@ -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

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

@ -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: @[<h>%a@]@." Errlog.pp_errors err_log;
F.fprintf fmt "ERRORS: @[<h>%a@]@\n%!" Errlog.pp_errors err_log;
F.fprintf fmt "WARNINGS: @[<h>%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@[<v 2> %a@]@."
L.(debug Analysis Medium) "Adding summary for %a@\n@[<v 2> %a@]@."
Typ.Procname.pp proc_name
pp_summary_text summary;
Typ.Procname.Hash.replace spec_tbl proc_name summary

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

@ -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 _ ->

2
infer/src/backend/timeout.ml
Unescape View File

@ -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 ->

90
infer/src/base/Config.ml
Unescape View File

@ -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

8
infer/src/base/Config.mli
Unescape View File

@ -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

4
infer/src/base/DB.ml
Unescape View File

@ -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
)

3
infer/src/base/Epilogues.ml
Unescape View File

@ -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. *)

441
infer/src/base/Logging.ml
Unescape View File

@ -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

115
infer/src/base/Logging.mli
Unescape View File

@ -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(<number of infer processes>) *)
| 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

10
infer/src/base/Process.ml
Unescape View File

@ -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

2
infer/src/base/ProcessPool.ml
Unescape View File

@ -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 =

1
infer/src/base/ProcessPool.mli
Unescape View File

@ -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

6
infer/src/base/Serialization.ml
Unescape View File

@ -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

2
infer/src/base/Utils.ml
Unescape View File

@ -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))

90
infer/src/bufferoverrun/bufferOverrunChecker.ml
Unescape View File

@ -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 "@[<v>=== Infer Print === at %a@,%a@]%!"
Location.pp loc
Dom.Val.pp (Sem.eval e mem loc);
L.(debug BufferOverrun Quiet) "@[<v>=== 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 "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre;
L.out "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr;
L.out "@\n@\n";
L.out "@[<v 2>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) "@[<v 2>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) "@[<v 2>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 "@[<v 2>Add condition :@,";
L.out "array: %a@," ArrayBlk.pp arr;
L.out " idx: %a@," Itv.pp idx;
L.out "@]@."));
L.(debug BufferOverrun Verbose) "@[<v 2>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 "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre;
L.out "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr;
L.out "@[<v 2>@\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) "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre;
L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr;
L.(debug BufferOverrun Verbose) "@[<v 2>@\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@[<v 2>Summary of %a :@,%a@]@."
L.(debug BufferOverrun Medium) "@\n@[<v 2>Summary of %a :@,%a@]@."
Typ.Procname.pp proc_name
Dom.Summary.pp_summary s

3
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -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

2
infer/src/checkers/Stacktrace.ml
Unescape View File

@ -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

2
infer/src/checkers/ThreadSafety.ml
Unescape View File

@ -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"
| [] -> ""

15
infer/src/checkers/checkers.ml
Unescape View File

@ -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

8
infer/src/checkers/constantPropagation.ml
Unescape View File

@ -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)

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

@ -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

2
infer/src/checkers/printfArgs.ml
Unescape View File

@ -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)

4
infer/src/clang/ALVar.ml
Unescape View File

@ -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

11
infer/src/clang/CType.ml
Unescape View File

@ -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'

29
infer/src/clang/Capture.re
Unescape View File

@ -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
};

6
infer/src/clang/ClangCommand.re
Unescape View File

@ -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 {
[]

10
infer/src/clang/ClangWrapper.re
Unescape View File

@ -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 -### <args>` 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])
};

6
infer/src/clang/ast_expressions.ml
Unescape View File

@ -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), []

14
infer/src/clang/cArithmetic_trans.ml
Unescape View File

@ -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 =

10
infer/src/clang/cAst_utils.ml
Unescape View File

@ -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 =

6
infer/src/clang/cField_decl.ml
Unescape View File

@ -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 =

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

@ -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)

29
infer/src/clang/cFrontend_checkers_main.ml
Unescape View File

@ -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

19
infer/src/clang/cFrontend_decl.ml
Unescape View File

@ -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

48
infer/src/clang/cFrontend_errors.ml
Unescape View File

@ -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

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

@ -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).

14
infer/src/clang/cIssue.ml
Unescape View File

@ -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

4
infer/src/clang/cMethod_trans.ml
Unescape View File

@ -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

8
infer/src/clang/cPredicates.ml
Unescape View File

@ -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

29
infer/src/clang/cTL.ml
Unescape View File

@ -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

126
infer/src/clang/cTrans.ml
Unescape View File

@ -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"

19
infer/src/clang/cTrans_utils.ml
Unescape View File

@ -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 ())

4
infer/src/clang/cType_to_sil_type.ml
Unescape View File

@ -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

83
infer/src/clang/ctl_parser.mly
Unescape View File

@ -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 }
;
%%

13
infer/src/clang/ctl_parser_types.ml
Unescape View File

@ -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

7
infer/src/clang/objcCategory_decl.ml
Unescape View File

@ -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

22
infer/src/clang/objcInterface_decl.ml
Unescape View File

@ -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;

2
infer/src/clang/objcProtocol_decl.ml
Unescape View File

@ -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

8
infer/src/clang/types_parser.mly
Unescape View File

@ -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 }
;

4
infer/src/eradicate/AnnotatedSignature.ml
Unescape View File

@ -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" ->

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

@ -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

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

@ -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

2
infer/src/eradicate/typeCheck.ml
Unescape View File

@ -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

4
infer/src/eradicate/typeErr.ml
Unescape View File

@ -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) ->

4
infer/src/harness/inhabit.ml
Unescape View File

@ -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)

20
infer/src/integration/CaptureCompilationDatabase.ml
Unescape View File

@ -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 =

47
infer/src/integration/Clang.ml
Unescape View File

@ -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

6
infer/src/integration/ClangQuotes.re
Unescape View File

@ -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
};

6
infer/src/integration/CompilationDatabase.ml
Unescape View File

@ -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

11
infer/src/integration/Javac.ml
Unescape View File

@ -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

6
infer/src/integration/Maven.ml
Unescape View File

@ -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 ()

4
infer/src/java/jClasspath.ml
Unescape View File

@ -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

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

@ -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

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

@ -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 =

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

@ -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

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

@ -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

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

@ -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

Write Preview
Loading…
Cancel
Save