diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 169b9eddf..5e5ebc638 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -572,7 +572,7 @@ let print_exception_html s exn = " " ^ L.ocaml_pos_to_string ocaml_pos in let desc_str = F.asprintf "%a" Localise.pp_error_desc error.description in - L.d_strln_color Red + L.d_strln ~color:Red (F.sprintf "%s%s %s%s" s error.name.IssueType.unique_id desc_str ocaml_pos_string) diff --git a/infer/src/base/Logging.ml b/infer/src/base/Logging.ml index 62e6701f5..5d67db8bc 100644 --- a/infer/src/base/Logging.ml +++ b/infer/src/base/Logging.ml @@ -350,10 +350,7 @@ let setup_log_file () = type print_action = | PTdecrease_indent : int -> print_action | PTincrease_indent : int -> print_action - | PTstr : string -> print_action - | PTstr_color : string * Pp.color -> print_action - | PTstrln : string -> print_action - | PTstrln_color : string * Pp.color -> print_action + | PTstr : {s: string; color: Pp.color option; ln: bool} -> print_action | PTwarning : string -> print_action | PTerror : string -> print_action | PTinfo : string -> print_action @@ -370,8 +367,12 @@ let pp_with_html_color color pp fmt x = F.fprintf fmt "%a" (Pp.color_string color) pp x -let pp_maybe_with_color color pp fmt x = - if Config.write_html then pp_with_html_color color pp fmt x else pp fmt x +let pp_maybe_with_color ?color pp fmt x = + match color with + | Some color when Config.write_html -> + pp_with_html_color color pp fmt x + | _ -> + pp fmt x (** Execute the delayed print actions *) @@ -382,20 +383,15 @@ let force_delayed_print fmt = function done | PTincrease_indent n -> F.fprintf fmt "%s@[" (String.make (2 * n) ' ') - | PTstr s -> - F.pp_print_string fmt s - | PTstr_color (s, c) -> - pp_maybe_with_color c F.pp_print_string fmt s - | PTstrln s -> - F.fprintf fmt "%s@\n" s - | PTstrln_color (s, c) -> - F.fprintf fmt "%a@\n" (pp_maybe_with_color c F.pp_print_string) s + | PTstr {s; color; ln} -> + pp_maybe_with_color ?color F.pp_print_string fmt s ; + if ln then F.pp_force_newline fmt () | PTerror s -> - pp_maybe_with_color Pp.Red (fun fmt -> F.fprintf fmt "ERROR: %s") fmt s + pp_maybe_with_color ~color:Pp.Red (fun fmt -> F.fprintf fmt "ERROR: %s") fmt s | PTwarning s -> - pp_maybe_with_color Pp.Orange (fun fmt -> F.fprintf fmt "WARNING: %s") fmt s + pp_maybe_with_color ~color:Pp.Orange (fun fmt -> F.fprintf fmt "WARNING: %s") fmt s | PTinfo s -> - pp_maybe_with_color Pp.Blue (fun fmt -> F.fprintf fmt "INFO: %s") fmt s + pp_maybe_with_color ~color:Pp.Blue (fun fmt -> F.fprintf fmt "INFO: %s") fmt s | PT_generic (pp, x) -> pp fmt x | PT_generic_with_pe (None, pp, x) -> @@ -431,10 +427,7 @@ let get_delayed_prints () = !delayed_actions let set_delayed_prints new_delayed_actions = delayed_actions := new_delayed_actions (** dump a string *) -let d_str (s : string) = add_print_action (PTstr s) - -(** dump a string with the given color *) -let d_str_color (c : Pp.color) (s : string) = add_print_action (PTstr_color (s, c)) +let d_str ?color (s : string) = add_print_action (PTstr {s; color; ln= false}) (** dump an error string *) let d_error (s : string) = add_print_action (PTerror s) @@ -446,19 +439,16 @@ let d_warning (s : string) = add_print_action (PTwarning s) let d_info (s : string) = add_print_action (PTinfo s) (** dump a string plus newline *) -let d_strln (s : string) = add_print_action (PTstrln s) - -(** dump a string plus newline with the given color *) -let d_strln_color (c : Pp.color) (s : string) = add_print_action (PTstrln_color (s, c)) +let d_strln ?color (s : string) = add_print_action (PTstr {s; color; ln= true}) (** dump a newline *) -let d_ln () = add_print_action (PTstrln "") +let d_ln () = d_strln "" (** dump an indentation *) let d_indent indent = if indent <> 0 then let s = String.make (2 * indent) ' ' in - add_print_action (PTstr s) + d_str s (** dump command to increase the indentation level *) diff --git a/infer/src/base/Logging.mli b/infer/src/base/Logging.mli index 56b19115f..827ff0ef3 100644 --- a/infer/src/base/Logging.mli +++ b/infer/src/base/Logging.mli @@ -99,18 +99,12 @@ val set_delayed_prints : delayed_prints -> unit val reset_delayed_prints : unit -> unit (** reset the delayed print actions *) -val d_str : string -> unit +val d_str : ?color:Pp.color -> string -> unit (** dump a string *) -val d_str_color : Pp.color -> string -> unit -(** dump a string with the given color *) - -val d_strln : string -> unit +val d_strln : ?color:Pp.color -> string -> unit (** dump a string plus newline *) -val d_strln_color : Pp.color -> string -> unit -(** dump a string plus newline with the given color *) - val d_ln : unit -> unit (** dump a newline *) diff --git a/infer/src/biabduction/Dom.ml b/infer/src/biabduction/Dom.ml index ada2cf845..1088559b2 100644 --- a/infer/src/biabduction/Dom.ml +++ b/infer/src/biabduction/Dom.ml @@ -1991,10 +1991,10 @@ let list_reduce name dd f list = L.d_ln () ; match f x y with | None -> - L.d_strln_color Red (".... COMBINE[" ^ name ^ "] FAILED ...") ; + L.d_strln ~color:Red (".... COMBINE[" ^ name ^ "] FAILED ...") ; element_list_reduce ((y, p2) :: acc) (x, p1) ys | Some x' -> - L.d_strln_color Green (".... COMBINE[" ^ name ^ "] SUCCEEDED ....") ; + L.d_strln ~color:Green (".... COMBINE[" ^ name ^ "] SUCCEEDED ....") ; L.d_strln "RESULT:" ; dd x' ; L.d_ln () ; @@ -2095,11 +2095,11 @@ let pathset_join pname tenv (pset1 : Paths.PathSet.t) (pset2 : Paths.PathSet.t) L.d_ln () ; match prop_partial_join pname tenv mode p2 p2' with | None -> - L.d_strln_color Red ".... JOIN FAILED ...." ; + L.d_strln ~color:Red ".... JOIN FAILED ...." ; L.d_ln () ; join_proppath_plist (ppa2' :: ppalist2_acc) ppa2 ppalist2_rest | Some p2'' -> - L.d_strln_color Green ".... JOIN SUCCEEDED ...." ; + L.d_strln ~color:Green ".... JOIN SUCCEEDED ...." ; L.d_strln "RESULT SYM HEAP:" ; Prop.d_prop p2'' ; L.d_ln () ; @@ -2148,11 +2148,11 @@ let proplist_meet_generate tenv plist = L.d_ln () ; match prop_partial_meet tenv p pcombined with | None -> - L.d_strln_color Red ".... MEET FAILED ...." ; + L.d_strln ~color:Red ".... MEET FAILED ...." ; L.d_ln () ; (porig, pcombined) | Some pcombined' -> - L.d_strln_color Green ".... MEET SUCCEEDED ...." ; + L.d_strln ~color:Green ".... MEET SUCCEEDED ...." ; L.d_strln "RESULT SYM HEAP:" ; Prop.d_prop pcombined' ; L.d_ln () ; diff --git a/infer/src/biabduction/Prover.ml b/infer/src/biabduction/Prover.ml index 44888a8e6..c113e1d5d 100644 --- a/infer/src/biabduction/Prover.ml +++ b/infer/src/biabduction/Prover.ml @@ -1992,7 +1992,7 @@ let sexp_imply_preprocess se1 texp1 se2 = match (se1, texp1, se2) with | Sil.Eexp (_, inst), Exp.Sizeof _, Sil.Earray _ when Config.type_size -> let se1' = Sil.Earray (texp1, [(Exp.zero, se1)], inst) in - L.d_strln_color Orange "sexp_imply_preprocess" ; + L.d_strln ~color:Orange "sexp_imply_preprocess" ; L.d_str " se1: " ; Sil.d_sexp se1 ; L.d_ln () ; @@ -2217,7 +2217,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2 decrease_indent_when_exception (fun () -> try sigma_imply tenv calc_index_frame calc_missing subs prop1 hpred_list2 with exn when SymOp.exn_not_failure exn -> - L.d_strln_color Red "backtracking lseg: trying rhs of length exactly 1" ; + L.d_strln ~color:Red "backtracking lseg: trying rhs of length exactly 1" ; let _, para_inst3 = Sil.hpara_instantiate para2 e2_ f2_ elist2 in sigma_imply tenv calc_index_frame calc_missing subs prop1 para_inst3 ) in @@ -2502,7 +2502,7 @@ let rec pre_check_pure_implication tenv calc_missing (subs : subst2) pi1 pi2 = let check_array_bounds tenv (sub1, sub2) prop = let check_failed atom = ProverState.checks := Bounds_check :: !ProverState.checks ; - L.d_str_color Red "bounds_check failed: provable atom: " ; + L.d_str ~color:Red "bounds_check failed: provable atom: " ; Sil.d_atom atom ; L.d_ln () ; if not Config.bound_error_allowed_in_procedure_call then @@ -2516,7 +2516,7 @@ let check_array_bounds tenv (sub1, sub2) prop = | ProverState.BClen_imply (len1_, len2_, _indices2) -> let len1 = Sil.exp_sub sub1 len1_ in let len2 = Sil.exp_sub sub2 len2_ in - (* L.d_strln_color Orange "check_bound "; + (* L.d_strln ~color:Orange "check_bound "; Sil.d_exp len1; L.d_str " "; Sil.d_exp len2; L.d_ln(); *) let indices_to_check = [Exp.BinOp (Binop.PlusA None, len2, Exp.minus_one)] @@ -2525,7 +2525,7 @@ let check_array_bounds tenv (sub1, sub2) prop = List.iter ~f:(fail_if_le len1) indices_to_check | ProverState.BCfrom_pre atom_ -> let atom_neg = atom_negate tenv (Sil.atom_sub sub2 atom_) in - (* L.d_strln_color Orange "BCFrom_pre"; Sil.d_atom atom_neg; L.d_ln (); *) + (* L.d_strln ~color:Orange "BCFrom_pre"; Sil.d_atom atom_neg; L.d_ln (); *) if check_atom tenv prop atom_neg then check_failed atom_neg in List.iter ~f:check_bound (ProverState.get_bounds_checks ()) diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index d1be87330..4a76ca990 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -253,7 +253,7 @@ let rec strexp_extend_values_ pname tenv orig_prop footprint_part kind max_stamp raise (Exceptions.Bad_footprint __POS__) | Off_index _ :: _, Sil.Eexp _, (Tint _ | Tfloat _ | Tvoid | Tfun _ | Tptr _) | Off_index _ :: _, Sil.Estruct _, Tstruct _ -> - (* L.d_strln_color Orange "turn into an array"; *) + (* L.d_strln ~color:Orange "turn into an array"; *) let len = match se with | Sil.Eexp (_, Sil.Ialloc) -> @@ -1317,7 +1317,7 @@ let type_at_offset tenv texp off = (** Check that the size of a type coming from an instruction does not exceed the size of the type from the pointsto predicate For example, that a pointer to int is not used to assign to a char *) let check_type_size tenv pname prop texp off typ_from_instr = - L.d_strln_color Orange "check_type_size" ; + L.d_strln ~color:Orange "check_type_size" ; L.d_str "off: " ; Sil.d_offset_list off ; L.d_ln () ; diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index d9f28f2de..722c85634 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -368,7 +368,7 @@ let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre fo Errdesc.explain_dereference_as_caller_expression caller_pname tenv ~use_buckets deref_str actual_pre spec_pre e (State.get_node_exn ()) (State.get_loc_exn ()) formal_params in - L.d_strln_color Red "found error in dereference" ; + L.d_strln ~color:Red "found error in dereference" ; L.d_strln "spec_pre:" ; Prop.d_prop spec_pre ; L.d_ln () ; diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index 13ad15397..18681ff80 100644 --- a/infer/src/biabduction/interproc.ml +++ b/infer/src/biabduction/interproc.ml @@ -299,7 +299,7 @@ let propagate_nodes_divergence tenv (proc_cfg : ProcCfg.Exceptional.t) (pset : P in Paths.PathSet.map mk_incons diverging_states in - L.d_strln_color Orange "Propagating Divergence -- diverging states:" ; + L.d_strln ~color:Orange "Propagating Divergence -- diverging states:" ; Propgraph.d_proplist Prop.prop_emp (Paths.PathSet.to_proplist prop_incons) ; L.d_ln () ; propagate wl pname ~is_exception:false prop_incons exit_node ) ; @@ -780,7 +780,7 @@ let execute_filter_prop summary exe_env tenv proc_cfg ignore (path_set_put_todo wl init_node init_edgeset) ; forward_tabulate summary exe_env tenv proc_cfg wl ; do_before_node 0 init_node ; - L.d_strln_color Green + L.d_strln ~color:Green ("#### Finished: RE-execution for " ^ Typ.Procname.to_string pname ^ " ####") ; L.d_increase_indent 1 ; L.d_strln "Precond:" ; @@ -810,7 +810,7 @@ let execute_filter_prop summary exe_env tenv proc_cfg with RE_EXE_ERROR -> do_before_node 0 init_node ; Printer.force_delayed_prints () ; - L.d_strln_color Red ("#### [FUNCTION " ^ Typ.Procname.to_string pname ^ "] ...ERROR") ; + L.d_strln ~color:Red ("#### [FUNCTION " ^ Typ.Procname.to_string pname ^ "] ...ERROR") ; L.d_increase_indent 1 ; L.d_strln "when starting from pre:" ; Prop.d_prop (BiabductionSummary.Jprop.to_prop precondition) ; diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 7f7e0d879..2d6819b93 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -227,7 +227,7 @@ module Val = struct let warn_against_pruning_multiple_values : t -> t = fun x -> if x.represents_multiple_values && Config.write_html then - L.d_str_color Pp.Red (F.asprintf "Pruned %a that represents multiple values\n" pp x) ; + L.d_str ~color:Pp.Red (F.asprintf "Pruned %a that represents multiple values\n" pp x) ; x