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

Logging: merge d_str_color with d_str

Browse Source 
Reviewed By: jeremydubreil

Differential Revision: D12840541

fbshipit-source-id: 41aab06e1
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent b6323db37b
commit 1606b95f1b
9 changed files with 38 additions and 54 deletions
Show Stats Download Patch File Download Diff File

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

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

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

@ -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 "<span class='%s'>%a</span>" (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 *)

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

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

12
infer/src/biabduction/Dom.ml
Unescape View File

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

10
infer/src/biabduction/Prover.ml
Unescape View File

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

4
infer/src/biabduction/Rearrange.ml
Unescape View File

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

2
infer/src/biabduction/Tabulation.ml
Unescape View File

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

6
infer/src/biabduction/interproc.ml
Unescape View File

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

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

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

Write Preview
Loading…
Cancel
Save