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

Logging.d_printf

Browse Source 
Reviewed By: jeremydubreil

Differential Revision: D12840615

fbshipit-source-id: aa338085d
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 320a859a8a
commit 18c45947da
32 changed files with 159 additions and 216 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/IR/DecompiledExp.mli
Unescape View File

@ -31,6 +31,8 @@ type t =
each expression represents a path, with Dpvar being the simplest one *)
type vpath = t option
val pp : F.formatter -> t -> unit
val to_string : t -> string
(** convert to a string *)

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

@ -571,9 +571,8 @@ let print_exception_html s exn =
| Some ocaml_pos ->
" " ^ 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
(F.sprintf "%s%s %s%s" s error.name.IssueType.unique_id desc_str ocaml_pos_string)
L.d_printfln ~color:Red "%s%s %a%s" s error.name.IssueType.unique_id Localise.pp_error_desc
error.description ocaml_pos_string
(** string describing an error kind *)

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

@ -263,4 +263,4 @@ let to_string pe = function
let pp pe fmt a = F.pp_print_string fmt (to_string pe a)
(** dump an attribute *)
let d_attribute (a : t) = L.add_print_with_pe pp a
let d_attribute (a : t) = L.d_pp_with_pe pp a

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

@ -326,7 +326,7 @@ module Node = struct
(** Dump extended instructions for the node *)
let d_instrs ~(sub_instrs : bool) (curr_instr : Sil.instr option) (node : t) =
L.add_print_with_pe ~color:Pp.Green (pp_instrs ~sub_instrs ~instro:curr_instr) node
L.d_pp_with_pe ~color:Pp.Green (pp_instrs ~sub_instrs ~instro:curr_instr) node
(** Return a description of the cfg node *)

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

@ -93,7 +93,7 @@ let pp pe f pv =
(** Dump a program variable. *)
let d (pvar : t) = L.add_print_with_pe pp pvar
let d (pvar : t) = L.d_pp_with_pe pp pvar
let get_name pv = pv.pv_name

23
infer/src/IR/Sil.ml
Unescape View File

@ -273,13 +273,13 @@ let pp_exp_printenv ?(print_types = false) pe0 f e0 =
(** dump an expression. *)
let d_exp (e : Exp.t) = L.add_print_with_pe pp_exp_printenv e
let d_exp (e : Exp.t) = L.d_pp_with_pe pp_exp_printenv e
(** Pretty print a list of expressions. *)
let pp_exp_list pe f expl = Pp.seq (pp_exp_printenv pe) f expl
(** dump a list of expressions. *)
let d_exp_list (el : Exp.t list) = L.add_print_with_pe pp_exp_list el
let d_exp_list (el : Exp.t list) = L.d_pp_with_pe pp_exp_list el
let pp_texp pe f = function
| Exp.Sizeof {typ; nbytes; dynamic_length; subtype} ->
@ -303,7 +303,7 @@ let pp_texp_full pe f = function
(** Dump a type expression with all the details. *)
let d_texp_full (te : Exp.t) = L.add_print_with_pe pp_texp_full te
let d_texp_full (te : Exp.t) = L.d_pp_with_pe pp_texp_full te
(** Pretty print an offset *)
let pp_offset pe f = function
@ -313,9 +313,6 @@ let pp_offset pe f = function
(pp_exp_printenv pe) f exp
(** Convert an offset to a string *)
let offset_to_string e = F.asprintf "%a" (pp_offset Pp.text) e
(** Pretty print a list of offsets *)
let rec pp_offset_list pe f = function
| [] ->
@ -327,7 +324,7 @@ let rec pp_offset_list pe f = function
(** Dump a list of offsets *)
let d_offset_list (offl : offset list) = L.add_print_with_pe pp_offset_list offl
let d_offset_list (offl : offset list) = L.d_pp_with_pe pp_offset_list offl
let pp_exp_typ pe f (e, t) = F.fprintf f "%a:%a" (pp_exp_printenv pe) e (Typ.pp pe) t
@ -426,7 +423,7 @@ let add_with_block_parameters_flag instr =
let is_block_pvar pvar = Typ.has_block_prefix (Mangled.to_string (Pvar.get_name pvar))
(** Dump an instruction. *)
let d_instr (i : instr) = L.add_print_with_pe ~color:Pp.Green (pp_instr ~print_types:true) i
let d_instr (i : instr) = L.d_pp_with_pe ~color:Pp.Green (pp_instr ~print_types:true) i
let pp_atom pe0 f a =
let pe, changed = color_pre_wrapper pe0 f a in
@ -445,7 +442,7 @@ let pp_atom pe0 f a =
(** dump an atom *)
let d_atom (a : atom) = L.add_print_with_pe pp_atom a
let d_atom (a : atom) = L.d_pp_with_pe pp_atom a
let pp_lseg_kind f = function Lseg_NE -> F.pp_print_string f "ne" | Lseg_PE -> ()
@ -669,14 +666,12 @@ let pp_inst f inst =
F.fprintf f "return_from_call: %d" n
let inst_to_string inst = F.asprintf "%a" pp_inst inst
exception JoinFail
(** join of instrumentations, can raise JoinFail *)
let inst_partial_join inst1 inst2 =
let fail () =
L.d_strln ("inst_partial_join failed on " ^ inst_to_string inst1 ^ " " ^ inst_to_string inst2) ;
L.d_printfln "inst_partial_join failed on %a %a" pp_inst inst1 pp_inst inst2 ;
raise JoinFail
in
if equal_inst inst1 inst2 then inst1
@ -878,10 +873,10 @@ let pp_hpara_dll pe f = pp_hpara_dll_env pe None f
let pp_hpred pe f = pp_hpred_env pe None f
(** dump a strexp. *)
let d_sexp (se : strexp) = L.add_print_with_pe pp_sexp se
let d_sexp (se : strexp) = L.d_pp_with_pe pp_sexp se
(** dump a hpred. *)
let d_hpred (hpred : hpred) = L.add_print_with_pe pp_hpred hpred
let d_hpred (hpred : hpred) = L.d_pp_with_pe pp_hpred hpred
(** {2 Functions for traversing SIL data types} *)

6
infer/src/IR/Sil.mli
Unescape View File

@ -273,8 +273,7 @@ val d_texp_full : Exp.t -> unit
val d_exp_list : Exp.t list -> unit
(** Dump a list of expressions. *)
val offset_to_string : offset -> string
(** Convert an offset to a string *)
val pp_offset : Pp.env -> F.formatter -> offset -> unit
val d_offset_list : offset list -> unit
(** Dump a list of offsets *)
@ -300,9 +299,6 @@ val pp_atom : Pp.env -> F.formatter -> atom -> unit
val d_atom : atom -> unit
(** Dump an atom. *)
val inst_to_string : inst -> string
(** return a string representing the inst *)
val pp_inst : F.formatter -> inst -> unit
(** pretty-print an inst *)

4
infer/src/IR/Typ.ml
Unescape View File

@ -496,12 +496,12 @@ module Name = struct
end
(** dump a type with all the details. *)
let d_full (t : t) = L.add_print_with_pe pp_full t
let d_full (t : t) = L.d_pp_with_pe pp_full t
(** dump a list of types. *)
let d_list (tl : t list) =
let pp pe = Pp.seq (pp pe) in
L.add_print_with_pe pp tl
L.d_pp_with_pe pp tl
let name typ = match typ.desc with Tstruct name -> Some name | _ -> None

14
infer/src/absint/AbstractInterpreter.ml
Unescape View File

@ -121,9 +121,7 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
else if phys_equal result right then F.pp_print_string f "= RIGHT"
else Domain.pp f result
in
L.d_strln
( Format.asprintf "LEFT: %a@.RIGHT: %t@.RESULT: %t@." Domain.pp left pp_right pp_result
|> Escape.escape_xml ) ;
L.d_printfln_escaped "LEFT: %a@.RIGHT: %t@.RESULT: %t@." Domain.pp left pp_right pp_result ;
NodePrinter.finish_session underlying_node
@ -164,10 +162,8 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
if phys_equal astate_post pre then F.pp_print_string f "= PRE"
else Domain.pp f astate_post
in
L.d_strln
( Format.asprintf "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %t@]@." Domain.pp pre
(Instrs.pp Pp.text) instrs pp_post
|> Escape.escape_xml ) ;
L.d_printfln_escaped "@[PRE: %a@]@\n@[INSTRS: %a@]@[POST: %t@]@." Domain.pp pre
(Instrs.pp Pp.text) instrs pp_post ;
NodePrinter.finish_session (Node.underlying_node node) ) ;
InvariantMap.add node_id {State.pre; post= astate_post; visit_count} inv_map
in
@ -309,11 +305,11 @@ module MakeUsingWTO (TransferFunctions : TransferFunctions.SIL) = struct
let underlying_node = Node.underlying_node node in
NodePrinter.start_session ~pp_name underlying_node ;
let pp_node fmt node = node |> Node.id |> Node.pp_id fmt in
L.d_strln (Format.asprintf "%a" (WeakTopologicalOrder.Partition.pp ~pp_node) wto) ;
L.d_printfln "%a" (WeakTopologicalOrder.Partition.pp ~pp_node) wto ;
let loop_heads =
wto |> IContainer.to_rev_list ~fold:WeakTopologicalOrder.Partition.fold_heads |> List.rev
in
L.d_strln (Format.asprintf "Loop heads: %a" (Pp.seq pp_node) loop_heads) ;
L.d_printfln "Loop heads: %a" (Pp.seq pp_node) loop_heads ;
NodePrinter.finish_session underlying_node

6
infer/src/absint/LowerHil.ml
Unescape View File

@ -37,10 +37,8 @@ struct
if phys_equal post pre then Format.pp_print_string f "= PRE"
else TransferFunctions.Domain.pp f post
in
L.d_strln
( Format.asprintf "PRE: %a@.INSTR: %a@.POST: %t@." TransferFunctions.Domain.pp pre
HilInstr.pp hil_instr pp_post
|> Escape.escape_xml ) ;
L.d_printfln_escaped "PRE: %a@.INSTR: %a@.POST: %t@." TransferFunctions.Domain.pp pre
HilInstr.pp hil_instr pp_post ;
NodePrinter.finish_session underyling_node )

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

@ -82,11 +82,9 @@ let find_normal_variable_funcall (node : Procdesc.Node.t) (id : Ident.t) :
None
in
let res = Procdesc.Node.find_in_node_or_preds node ~f:find_declaration in
if verbose && is_none res then (
L.d_str
( "find_normal_variable_funcall could not find " ^ Ident.to_string id ^ " in node "
^ string_of_int (Procdesc.Node.get_id node :> int) ) ;
L.d_ln () ) ;
if verbose && is_none res then
L.d_printfln "find_normal_variable_funcall could not find %a in node %a" Ident.pp id
Procdesc.Node.pp node ;
res
@ -198,11 +196,9 @@ let rec find_normal_variable_load_ tenv (seen : Exp.Set.t) node id : DExp.t opti
None
in
let res = Procdesc.Node.find_in_node_or_preds node ~f:find_declaration in
if verbose && is_none res then (
L.d_str
( "find_normal_variable_load could not find " ^ Ident.to_string id ^ " in node "
^ string_of_int (Procdesc.Node.get_id node :> int) ) ;
L.d_ln () ) ;
if verbose && is_none res then
L.d_printfln "find_normal_variable_load could not find %a in node %a" Ident.pp id
Procdesc.Node.pp node ;
res
@ -269,8 +265,7 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
if verbose then (
L.d_str "exp_lv_dexp: Lfield with var " ;
Sil.d_exp (Exp.Var id) ;
L.d_str (" " ^ Typ.Fieldname.to_string f) ;
L.d_ln () ) ;
L.d_printfln " %a" Typ.Fieldname.pp f ) ;
match find_normal_variable_load_ tenv seen node id with
| None ->
None
@ -280,8 +275,7 @@ and exp_lv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
if verbose then (
L.d_str "exp_lv_dexp: Lfield " ;
Sil.d_exp e1 ;
L.d_str (" " ^ Typ.Fieldname.to_string f) ;
L.d_ln () ) ;
L.d_printfln " %a" Typ.Fieldname.pp f ) ;
match exp_lv_dexp_ tenv seen node e1 with
| None ->
None
@ -337,8 +331,7 @@ and exp_rv_dexp_ tenv (seen_ : Exp.Set.t) node e : DExp.t option =
if verbose then (
L.d_str "exp_rv_dexp: Lfield " ;
Sil.d_exp e1 ;
L.d_str (" " ^ Typ.Fieldname.to_string f) ;
L.d_ln () ) ;
L.d_printfln " %a" Typ.Fieldname.pp f ) ;
match exp_rv_dexp_ tenv seen node e1 with
| None ->
None
@ -504,9 +497,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
let value_str =
match instro with
| None ->
if verbose then (
L.d_str "explain_leak: no current instruction" ;
L.d_ln () ) ;
if verbose then L.d_strln "explain_leak: no current instruction" ;
value_str_from_pvars_vpath [] vpath
| Some (Sil.Nullify (pvar, _)) when check_pvar pvar -> (
if verbose then (
@ -519,9 +510,7 @@ let explain_leak tenv hpred prop alloc_att_opt bucket =
| _ ->
None )
| Some (Sil.Abstract _) ->
if verbose then (
L.d_str "explain_leak: current instruction is Abstract" ;
L.d_ln () ) ;
if verbose then L.d_strln "explain_leak: current instruction is Abstract" ;
let get_nullify = function
| Sil.Nullify (pvar, _) when check_pvar pvar ->
if verbose then (
@ -675,9 +664,7 @@ let vpath_find tenv prop exp_ : DExp.t option * Typ.t option =
Sil.d_exp exp_ ;
L.d_ln ()
| Some de, typo -> (
L.d_str "vpath_find: found " ;
L.d_str (DExp.to_string de) ;
L.d_str " : " ;
L.d_printf "vpath_find: found %a :" DExp.pp de ;
match typo with None -> L.d_str " No type" | Some typ -> Typ.d_full typ ; L.d_ln () ) ) ;
res
@ -693,8 +680,7 @@ let access_opt ?(is_nullable = false) inst =
| Sil.Ialloc when Language.curr_language_is Java ->
Some Localise.Initialized_automatically
| inst ->
if verbose then
L.d_strln ("explain_dexp_access: inst is not an update " ^ Sil.inst_to_string inst) ;
if verbose then L.d_printfln "explain_dexp_access: inst is not an update %a" Sil.pp_inst inst ;
None
@ -726,7 +712,7 @@ let explain_dexp_access prop dexp is_nullable =
let rec lookup_fld fsel f =
match fsel with
| [] ->
if verbose then L.d_strln ("lookup_fld: can't find field " ^ Typ.Fieldname.to_string f) ;
if verbose then L.d_printfln "lookup_fld: can't find field %a" Typ.Fieldname.pp f ;
None
| (f1, se) :: fsel' ->
if Typ.Fieldname.equal f1 f then Some se else lookup_fld fsel' f
@ -766,9 +752,7 @@ let explain_dexp_access prop dexp is_nullable =
| Some (Sil.Estruct (fsel, _)) ->
lookup_fld fsel f
| Some _ ->
if verbose then (
L.d_str "lookup: case not matched on Darrow " ;
L.d_ln () ) ;
if verbose then L.d_strln "lookup: case not matched on Darrow" ;
None )
| DExp.Darrow (de1, f) -> (
match lookup (DExp.Dderef de1) with
@ -777,9 +761,7 @@ let explain_dexp_access prop dexp is_nullable =
| Some (Sil.Estruct (fsel, _)) ->
lookup_fld fsel f
| Some _ ->
if verbose then (
L.d_str "lookup: case not matched on Darrow " ;
L.d_ln () ) ;
if verbose then L.d_strln "lookup: case not matched on Darrow" ;
None )
| DExp.Ddot (de1, f) -> (
match lookup de1 with
@ -790,20 +772,18 @@ let explain_dexp_access prop dexp is_nullable =
| Some (Sil.Eexp (Const (Cfun _), _) as fun_strexp) ->
Some fun_strexp
| Some _ ->
if verbose then (
L.d_str "lookup: case not matched on Ddot " ;
L.d_ln () ) ;
if verbose then L.d_strln "lookup: case not matched on Ddot" ;
None )
| DExp.Dpvar pvar ->
if verbose then ( L.d_str "lookup: found Dpvar " ; L.d_ln () ) ;
if verbose then L.d_strln "lookup: found Dpvar" ;
find_ptsto (Exp.Lvar pvar)
| DExp.Dderef de -> (
match lookup de with None -> None | Some (Sil.Eexp (e, _)) -> find_ptsto e | Some _ -> None )
| DExp.Dbinop (Binop.PlusPI, DExp.Dpvar _, DExp.Dconst _) as de ->
if verbose then L.d_strln ("lookup: case )pvar + constant) " ^ DExp.to_string de) ;
if verbose then L.d_printfln "lookup: case )pvar + constant) %a" DExp.pp de ;
None
| DExp.Dfcall (DExp.Dconst c, _, loc, _) -> (
if verbose then L.d_strln "lookup: found Dfcall " ;
if verbose then L.d_strln "lookup: found Dfcall" ;
match c with
| Const.Cfun _ ->
(* Treat function as an update *)
@ -811,17 +791,17 @@ let explain_dexp_access prop dexp is_nullable =
| _ ->
None )
| DExp.Dpvaraddr pvar ->
L.d_strln ("lookup: found Dvaraddr " ^ DExp.to_string (DExp.Dpvaraddr pvar)) ;
L.d_printfln "lookup: found Dvaraddr %a" DExp.pp (DExp.Dpvaraddr pvar) ;
find_ptsto (Exp.Lvar pvar)
| de ->
if verbose then L.d_strln ("lookup: unknown case not matched " ^ DExp.to_string de) ;
if verbose then L.d_printfln "lookup: unknown case not matched %a" DExp.pp de ;
None
in
match sexpo_to_inst (lookup dexp) with
| Some inst ->
access_opt inst ~is_nullable
| None ->
if verbose then L.d_strln ("explain_dexp_access: cannot find inst of " ^ DExp.to_string dexp) ;
if verbose then L.d_printfln "explain_dexp_access: cannot find inst of %a" DExp.pp dexp ;
None
@ -1107,14 +1087,14 @@ let explain_dereference_as_caller_expression proc_name tenv ?(use_buckets = fals
in
match find_with_exp spec_pre exp with
| Some (pv, pvar_off) ->
if verbose then L.d_strln ("pvar: " ^ Pvar.to_string pv) ;
if verbose then L.d_printfln "pvar: %s" (Pvar.to_string pv) ;
let pv_name = Pvar.get_name pv in
if Pvar.is_global pv then
let dexp = exp_lv_dexp tenv node (Exp.Lvar pv) in
create_dereference_desc proc_name tenv ~use_buckets dexp deref_str actual_pre loc
else if Pvar.is_callee pv then (
let position = find_formal_param_number pv_name in
if verbose then L.d_strln ("parameter number: " ^ string_of_int position) ;
if verbose then L.d_printfln "parameter number: %d" position ;
explain_nth_function_parameter proc_name tenv use_buckets deref_str actual_pre position
pvar_off )
else if Attribute.has_dangling_uninit tenv spec_pre exp then
@ -1124,8 +1104,7 @@ let explain_dereference_as_caller_expression proc_name tenv ?(use_buckets = fals
if verbose then (
L.d_str "explain_dereference_as_caller_expression " ;
Sil.d_exp exp ;
L.d_str ": cannot explain None " ;
L.d_ln () ) ;
L.d_strln ": cannot explain None" ) ;
Localise.no_desc

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

@ -413,9 +413,9 @@ let add_print_action pact =
Option.iter !log_file ~f:(function file_fmt, _ -> force_delayed_print file_fmt pact)
let add_print pp x = add_print_action (PT_generic (pp, x))
let d_pp pp x = add_print_action (PT_generic (pp, x))
let add_print_with_pe ?color pp x = add_print_action (PT_generic_with_pe (color, pp, x))
let d_pp_with_pe ?color pp x = add_print_action (PT_generic_with_pe (color, pp, x))
(** reset the delayed print actions *)
let reset_delayed_prints () = delayed_actions := []
@ -444,6 +444,12 @@ let d_strln ?color (s : string) = add_print_action (PTstr {s; color; ln= true})
(** dump a newline *)
let d_ln () = d_strln ""
let d_printf ?color fmt = F.kasprintf (d_str ?color) fmt
let d_printfln ?color fmt = F.kasprintf (d_strln ?color) fmt
let d_printfln_escaped fmt = F.kasprintf (fun s -> d_strln (Escape.escape_xml s)) fmt
(** dump an indentation *)
let d_indent indent =
if indent <> 0 then

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

@ -84,9 +84,9 @@ val reset_formatters : unit -> unit
type delayed_prints
val add_print : (F.formatter -> 'a -> unit) -> 'a -> unit
val d_pp : (F.formatter -> 'a -> unit) -> 'a -> unit
val add_print_with_pe : ?color:Pp.color -> (Pp.env -> F.formatter -> 'a -> unit) -> 'a -> unit
val d_pp_with_pe : ?color:Pp.color -> (Pp.env -> F.formatter -> 'a -> unit) -> 'a -> unit
val force_delayed_prints : F.formatter -> delayed_prints -> unit
@ -108,6 +108,12 @@ val d_strln : ?color:Pp.color -> string -> unit
val d_ln : unit -> unit
(** dump a newline *)
val d_printf : ?color:Pp.color -> ('a, F.formatter, unit) format -> 'a
val d_printfln : ?color:Pp.color -> ('a, F.formatter, unit) format -> 'a
val d_printfln_escaped : ('a, F.formatter, unit) format -> 'a
val d_error : string -> unit
(** dump an error string *)

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

@ -1018,7 +1018,7 @@ let check_junk pname tenv prop =
let entries = Sil.hpred_entries hpred in
if should_remove_hpred entries then (
let part = if fp_part then "footprint" else "normal" in
L.d_strln (".... Prop with garbage in " ^ part ^ " part ....") ;
L.d_printfln ".... Prop with garbage in %s part ...." part ;
L.d_increase_indent 1 ;
L.d_strln "PROP:" ;
Prop.d_prop prop ;

15
infer/src/biabduction/Absarray.ml
Unescape View File

@ -208,8 +208,7 @@ end = struct
| Some (_, t, _) ->
find_offset_sexp sigma_other hpred root (Field (f, typ) :: offs) se t
| None ->
L.d_strln ("Can't find field " ^ Typ.Fieldname.to_string f ^ " in StrexpMatch.find")
) ;
L.d_printfln "Can't find field %a in StrexpMatch.find" Typ.Fieldname.pp f ) ;
find_offset_fsel sigma_other hpred root offs fsel' ftal typ
and find_offset_esel sigma_other hpred root offs esel t =
match esel with
@ -378,7 +377,7 @@ let generic_strexp_abstract tenv (abstraction_name : string) (p_in : Prop.normal
try
let matched, footprint_part, matchings_cur_fp' = match_select_next matchings_cur_fp in
let n = List.length (snd matchings_cur_fp') + 1 in
if Config.trace_absarray then L.d_strln ("Num of fp candidates " ^ string_of_int n) ;
if Config.trace_absarray then L.d_printfln "Num of fp candidates %d" n ;
let strexp_data = StrexpMatch.get_data tenv matched in
let p1, changed = do_abstract footprint_part p0 strexp_data in
if changed then (p1, true) else match_abstract p0 matchings_cur_fp'
@ -388,7 +387,7 @@ let generic_strexp_abstract tenv (abstraction_name : string) (p_in : Prop.normal
if Int.equal bound 0 then p0
else (
if Config.trace_absarray then (
L.d_strln ("Applying " ^ abstraction_name ^ " to") ;
L.d_printfln "Applying %s to" abstraction_name ;
Prop.d_prop p0 ;
L.d_ln () ;
L.d_ln () ) ;
@ -513,12 +512,8 @@ let strexp_can_abstract ((_, se, typ) : StrexpMatch.strexp_data) : bool =
(** This function abstracts a strexp *)
let strexp_do_abstract tenv footprint_part p ((path, se_in, _) : StrexpMatch.strexp_data) :
Prop.normal Prop.t * bool =
if Config.trace_absarray && footprint_part then (
L.d_str "strexp_do_abstract (footprint)" ;
L.d_ln () ) ;
if Config.trace_absarray && not footprint_part then (
L.d_str "strexp_do_abstract (nonfootprint)" ;
L.d_ln () ) ;
if Config.trace_absarray && footprint_part then L.d_strln "strexp_do_abstract (footprint)" ;
if Config.trace_absarray && not footprint_part then L.d_strln "strexp_do_abstract (nonfootprint)" ;
let prune_and_blur d_keys keep blur path keep_keys blur_keys =
let p2, changed2 =
if Config.trace_absarray then ( L.d_str "keep " ; d_keys keep_keys ; L.d_ln () ) ;

15
infer/src/biabduction/BiabductionSummary.ml
Unescape View File

@ -60,7 +60,7 @@ module Jprop = struct
let pp_short pe f jp = Prop.pp_prop pe f (to_prop jp)
(** Dump the toplevel prop *)
let d_shallow (jp : Prop.normal t) = L.add_print_with_pe pp_short jp
let d_shallow (jp : Prop.normal t) = L.d_pp_with_pe pp_short jp
(** Get identifies of the jprop *)
let get_id = function Prop (n, _) -> n | Joined (n, _, _, _) -> n
@ -85,7 +85,7 @@ module Jprop = struct
(** dump a joined prop list, the boolean indicates whether to print toplevel props only *)
let d_list ~(shallow : bool) (jplist : Prop.normal t list) =
L.add_print_with_pe (pp_list ~shallow) jplist
L.d_pp_with_pe (pp_list ~shallow) jplist
let rec gen_free_vars =
@ -238,7 +238,7 @@ let string_of_phase = function FOOTPRINT -> "FOOTPRINT" | RE_EXECUTION -> "RE_EX
let string_of_phase_short = function FOOTPRINT -> "FP" | RE_EXECUTION -> "RE"
(** Print the spec *)
let pp_spec pe num_opt fmt spec =
let pp_spec0 pe num_opt fmt spec =
let pp_num_opt fmt = function
| None ->
F.pp_print_string fmt "----------"
@ -265,19 +265,16 @@ let pp_spec pe num_opt fmt spec =
F.pp_print_string fmt "----------------------------------------------------------------"
(** Dump a spec *)
let d_spec (spec : 'a spec) =
L.add_print (pp_spec (if Config.write_html then Pp.html Blue else Pp.text) None) spec
let pp_spec f spec = pp_spec0 (if Config.write_html then Pp.html Blue else Pp.text) None f spec
let pp_specs pe fmt specs =
let total = List.length specs in
match pe.Pp.kind with
| TEXT ->
List.iteri specs ~f:(fun cnt spec -> pp_spec pe (Some (cnt + 1, total)) fmt spec)
List.iteri specs ~f:(fun cnt spec -> pp_spec0 pe (Some (cnt + 1, total)) fmt spec)
| HTML ->
List.iteri specs ~f:(fun cnt spec ->
F.fprintf fmt "%a<br>@\n" (pp_spec pe (Some (cnt + 1, total))) spec )
F.fprintf fmt "%a<br>@\n" (pp_spec0 pe (Some (cnt + 1, total))) spec )
let get_specs_from_preposts preposts = Option.value_map ~f:NormSpec.tospecs ~default:[] preposts

3
infer/src/biabduction/BiabductionSummary.mli
Unescape View File

@ -64,8 +64,7 @@ end
val normalized_specs_to_specs : NormSpec.t list -> Prop.normal spec list
(** Cast a list of normalized specs to a list of specs *)
val d_spec : _ spec -> unit
(** Dump a spec *)
val pp_spec : Format.formatter -> _ spec -> unit
val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t
(** Convert spec into normal form w.r.t. variable renaming *)

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

@ -658,7 +658,7 @@ let execute_pthread_create ({Builtin.tenv; pdesc; prop_; path; args; exe_env} as
L.d_strln ", skipping call." ;
[(prop_, path)]
| Some pname -> (
L.d_strln ("pthread_create: calling function " ^ Typ.Procname.to_string pname) ;
L.d_printfln "pthread_create: calling function %a" Typ.Procname.pp pname ;
match Ondemand.analyze_proc_name ~caller_pdesc:pdesc pname with
| None ->
(* no precondition to check, skip *)

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

@ -1980,12 +1980,10 @@ let list_reduce name dd f list =
((x, p1), List.rev acc)
| (y, p2) :: ys -> (
L.d_strln ("COMBINE[" ^ name ^ "] ....") ;
L.d_str "ENTRY1: " ;
L.d_ln () ;
L.d_strln "ENTRY1:" ;
dd x ;
L.d_ln () ;
L.d_str "ENTRY2: " ;
L.d_ln () ;
L.d_strln "ENTRY2:" ;
dd y ;
L.d_ln () ;
L.d_ln () ;
@ -2086,10 +2084,10 @@ let pathset_join pname tenv (pset1 : Paths.PathSet.t) (pset2 : Paths.PathSet.t)
(ppa2, List.rev ppalist2_acc)
| ((p2', pa2') as ppa2') :: ppalist2_rest -> (
L.d_strln ".... JOIN ...." ;
L.d_strln "JOIN SYM HEAP1: " ;
L.d_strln "JOIN SYM HEAP1:" ;
Prop.d_prop p2 ;
L.d_ln () ;
L.d_strln "JOIN SYM HEAP2: " ;
L.d_strln "JOIN SYM HEAP2:" ;
Prop.d_prop p2' ;
L.d_ln () ;
L.d_ln () ;
@ -2140,10 +2138,10 @@ let proplist_meet_generate tenv plist =
SymOp.pay () ;
(* pay one symop *)
L.d_strln ".... MEET ...." ;
L.d_strln "MEET SYM HEAP1: " ;
L.d_strln "MEET SYM HEAP1:" ;
Prop.d_prop p ;
L.d_ln () ;
L.d_strln "MEET SYM HEAP2: " ;
L.d_strln "MEET SYM HEAP2:" ;
Prop.d_prop pcombined ;
L.d_ln () ;
match prop_partial_meet tenv p pcombined with

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

@ -134,7 +134,7 @@ let pp_sub pe f sub =
(** Dump a substitution. *)
let d_sub (sub : Sil.subst) = L.add_print_with_pe pp_sub sub
let d_sub (sub : Sil.subst) = L.d_pp_with_pe pp_sub sub
let pp_sub_entry pe0 f entry =
let pe, changed = Sil.color_pre_wrapper pe0 f entry in
@ -156,7 +156,7 @@ let pp_pi pe =
(** Dump a pi. *)
let d_pi (pi : pi) = L.add_print_with_pe pp_pi pi
let d_pi (pi : pi) = L.d_pp_with_pe pp_pi pi
(** Pretty print a sigma. *)
let pp_sigma pe = Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred pe)
@ -189,7 +189,7 @@ let pp_sigma_simple pe env fmt sigma =
(** Dump a sigma. *)
let d_sigma (sigma : sigma) = L.add_print_with_pe pp_sigma sigma
let d_sigma (sigma : sigma) = L.d_pp_with_pe pp_sigma sigma
(** Dump a pi and a sigma *)
let d_pi_sigma pi sigma =
@ -325,7 +325,7 @@ let pp_prop pe0 f prop =
let pp_prop_with_typ pe f p = pp_prop {pe with opt= SIM_WITH_TYP} f p
(** Dump a proposition. *)
let d_prop (prop : 'a t) = L.add_print_with_pe pp_prop prop
let d_prop (prop : 'a t) = L.d_pp_with_pe pp_prop prop
(** Print a list of propositions, prepending each one with the given string *)
let pp_proplist_with_typ pe f plist =
@ -341,7 +341,7 @@ let pp_proplist_with_typ pe f plist =
(** dump a proplist *)
let d_proplist_with_typ (pl : 'a t list) = L.add_print_with_pe pp_proplist_with_typ pl
let d_proplist_with_typ (pl : 'a t list) = L.d_pp_with_pe pp_proplist_with_typ pl
(** {1 Functions for computing free non-program variables} *)

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

@ -263,4 +263,4 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist =
(** dump a propset *)
let d_proplist (p : 'a Prop.t) (pl : 'b Prop.t list) =
let pp pe = pp_proplist pe "PROP" (p, false) in
L.add_print_with_pe pp pl
L.d_pp_with_pe pp pl

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

@ -888,13 +888,11 @@ let check_atom tenv prop a0 =
in
let outc = Out_channel.create (DB.filename_to_string key_filename) in
let fmt = F.formatter_of_out_channel outc in
L.d_str ("ID: " ^ key) ;
L.d_ln () ;
L.d_printfln "ID: %s" key ;
L.d_str "CHECK_ATOM_BOUND: " ;
Sil.d_atom a ;
L.d_ln () ;
L.d_str "WHERE:" ;
L.d_ln () ;
L.d_strln "WHERE:" ;
Prop.d_prop prop_no_fp ;
L.d_ln () ;
L.d_ln () ;
@ -1218,18 +1216,18 @@ end = struct
Prop.d_sub sub ;
L.d_decrease_indent 1 ;
if !missing_pi <> [] && !missing_sigma <> [] then (
L.d_ln () ; Prop.d_pi !missing_pi ; L.d_str "*" ; L.d_ln () ; Prop.d_sigma !missing_sigma )
L.d_ln () ; Prop.d_pi !missing_pi ; L.d_strln "*" ; Prop.d_sigma !missing_sigma )
else if !missing_pi <> [] then ( L.d_ln () ; Prop.d_pi !missing_pi )
else if !missing_sigma <> [] then ( L.d_ln () ; Prop.d_sigma !missing_sigma ) ;
if !missing_fld <> [] then (
L.d_ln () ;
L.d_strln "MISSING FLD: " ;
L.d_strln "MISSING FLD:" ;
L.d_increase_indent 1 ;
Prop.d_sigma !missing_fld ;
L.d_decrease_indent 1 ) ;
if !missing_typ <> [] then (
L.d_ln () ;
L.d_strln "MISSING TYPING: " ;
L.d_strln "MISSING TYPING:" ;
L.d_increase_indent 1 ;
d_typings !missing_typ ;
L.d_decrease_indent 1 )
@ -1303,7 +1301,7 @@ end = struct
L.d_strln "$$$$$$$ Implication" ;
d_implication subs (p1, p2) ;
L.d_ln () ;
L.d_str ("$$$$$$ error: " ^ s) ;
L.d_printf "$$$$$$ error: %s" s ;
d_inner () ;
L.d_strln " returning FALSE" ;
L.d_ln ()
@ -2431,7 +2429,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
| _ ->
normal_case hpred2 )
with IMPL_EXC (s, _, _) when calc_missing ->
L.d_strln ("Adding rhs as missing: " ^ s) ;
L.d_printfln "Adding rhs as missing: %s" s ;
ProverState.add_missing_sigma sigma2 ;
(subs, prop1)
@ -2561,12 +2559,12 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
L.d_ln () ;
if pi2_bcheck <> [] then ( L.d_str "pi2 bounds checks: " ; Prop.d_pi pi2_bcheck ; L.d_ln () ) ;
L.d_strln "returns" ;
L.d_strln "sub1: " ;
L.d_strln "sub1:" ;
L.d_increase_indent 1 ;
Prop.d_sub (fst subs) ;
L.d_decrease_indent 1 ;
L.d_ln () ;
L.d_strln "sub2: " ;
L.d_strln "sub2:" ;
L.d_increase_indent 1 ;
Prop.d_sub (snd subs) ;
L.d_decrease_indent 1 ;
@ -2594,7 +2592,7 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
d_impl_err (s, subs, body) ;
None
| MISSING_EXC s ->
L.d_strln ("WARNING: footprint failed to find MISSING because: " ^ s) ;
L.d_printfln "WARNING: footprint failed to find MISSING because: %s" s ;
None
| Exceptions.Abduction_case_not_implemented _ as exn ->
Reporting.log_issue_deprecated_using_state Exceptions.Error pname exn ;

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

@ -1087,7 +1087,7 @@ let rearrange_arith tenv lexp prop =
let pp_rearrangement_error message prop lexp =
L.d_strln (".... Rearrangement Error .... " ^ message) ;
L.d_printfln ".... Rearrangement Error .... %s" message ;
L.d_str "Exp:" ;
Sil.d_exp lexp ;
L.d_ln () ;
@ -1362,8 +1362,7 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst :
(* access through field: get the struct type from the field *)
if Config.trace_rearrange then (
L.d_increase_indent 1 ;
L.d_str "iter_rearrange: root of lexp accesses field " ;
L.d_strln (Typ.Fieldname.to_string f) ;
L.d_printfln "iter_rearrange: root of lexp accesses field %a" Typ.Fieldname.pp f ;
L.d_str " struct type from field: " ;
Typ.d_full fld_typ ;
L.d_ln () ;
@ -1757,8 +1756,7 @@ let rearrange ?(report_deref_errors = true) pdesc tenv lexp typ prop loc :
L.d_str "Exp: " ;
Sil.d_exp nlexp ;
L.d_ln () ;
L.d_str "Prop: " ;
L.d_ln () ;
L.d_strln "Prop:" ;
Prop.d_prop prop ;
L.d_ln () ;
L.d_ln () ;

3
infer/src/biabduction/RetainCyclesType.ml
Unescape View File

@ -113,8 +113,7 @@ let pp_retain_cycle_edge f (edge : retain_cycle_edge) =
let d_retain_cycle cycle =
Logging.d_strln "Cycle=" ;
Logging.d_strln
(Format.asprintf "\t%a" (Pp.seq ~sep:"->" pp_retain_cycle_edge) cycle.rc_elements)
Logging.d_printfln "\t%a" (Pp.seq ~sep:"->" pp_retain_cycle_edge) cycle.rc_elements
let find_minimum_element cycle =

43
infer/src/biabduction/SymExec.ml
Unescape View File

@ -21,10 +21,9 @@ let rec fldlist_assoc fld = function
let unroll_type tenv (typ : Typ.t) (off : Sil.offset) =
let fail fld_to_string fld =
let fail pp_fld fld =
L.d_strln ".... Invalid Field Access ...." ;
L.d_str ("Fld : " ^ fld_to_string fld) ;
L.d_ln () ;
L.d_printfln "Fld : %a" pp_fld fld ;
L.d_str "Type : " ;
Typ.d_full typ ;
L.d_ln () ;
@ -34,16 +33,15 @@ let unroll_type tenv (typ : Typ.t) (off : Sil.offset) =
| Tstruct name, Off_fld (fld, _) -> (
match Tenv.lookup tenv name with
| Some {fields; statics} -> (
try fldlist_assoc fld (fields @ statics) with Caml.Not_found ->
fail Typ.Fieldname.to_string fld )
try fldlist_assoc fld (fields @ statics) with Caml.Not_found -> fail Typ.Fieldname.pp fld )
| None ->
fail Typ.Fieldname.to_string fld )
fail Typ.Fieldname.pp fld )
| Tarray {elt}, Off_index _ ->
elt
| _, Off_index (Const (Cint i)) when IntLit.iszero i ->
typ
| _ ->
fail Sil.offset_to_string off
fail (Sil.pp_offset Pp.text) off
(** Apply function [f] to the expression at position [offlist] in [strexp].
@ -547,7 +545,8 @@ let resolve_method tenv class_name proc_name =
in
match found_class with
| None ->
Logging.d_strln ("Couldn't find method in the hierarchy of type " ^ Typ.Name.name class_name) ;
Logging.d_printfln "Couldn't find method in the hierarchy of type %s"
(Typ.Name.name class_name) ;
proc_name
| Some proc_name ->
proc_name
@ -846,9 +845,8 @@ let handle_objc_instance_method_call_or_skip pdesc tenv actual_pars path callee_
if is_receiver_null then (
(* objective-c instance method with a null receiver just return objc_null(res). *)
let path = Paths.Path.add_description path path_description in
L.d_strln
(F.sprintf "Object-C method %s called with nil receiver. Returning 0/nil"
(Typ.Procname.to_string callee_pname)) ;
L.d_printfln "Object-C method %a called with nil receiver. Returning 0/nil" Typ.Procname.pp
callee_pname ;
(* We wish to nullify the result. However, in some cases,
we want to add the attribute OBJC_NULL to it so that we
can keep track of how this object became null,
@ -1239,8 +1237,7 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t)
let skip_res () =
let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in
Reporting.log_issue_deprecated_using_state Exceptions.Info current_pname exn ;
L.d_strln
(F.sprintf "Skipping function '%s': %s" (Typ.Procname.to_string callee_pname) reason) ;
L.d_printfln "Skipping function '%a': %s" Typ.Procname.pp callee_pname reason ;
Tabulation.log_call_trace ~caller_name:current_pname ~callee_name:callee_pname
?callee_attributes ~reason loc Tabulation.CR_skip ;
unknown_or_scan_call ~is_scan:false ~reason ret_typ ret_annots
@ -1402,8 +1399,8 @@ let rec sym_exec exe_env tenv current_pdesc instr_ (prop_ : Prop.normal Prop.t)
let resolved_pdesc_opt = resolve_and_analyze_result.resolved_procdesc_opt in
let resolved_summary_opt = resolve_and_analyze_result.resolved_summary_opt in
let dynamic_dispatch_status = resolve_and_analyze_result.dynamic_dispatch_status in
Logging.d_strln ("Original callee " ^ Typ.Procname.to_unique_id callee_pname) ;
Logging.d_strln ("Resolved callee " ^ Typ.Procname.to_unique_id resolved_pname) ;
Logging.d_printfln "Original callee %s" (Typ.Procname.to_unique_id callee_pname) ;
Logging.d_printfln "Resolved callee %s" (Typ.Procname.to_unique_id resolved_pname) ;
let sentinel_result =
if Language.curr_language_is Clang then
check_variadic_sentinel_if_present
@ -1631,7 +1628,7 @@ and add_constraints_on_actuals_by_ref tenv caller_pdesc prop actuals_by_ref call
| Some attrs ->
let is_const = List.mem ~equal:Int.equal attrs.ProcAttributes.const_formals i in
if is_const then (
L.d_str (Printf.sprintf "Not havocing const argument number %d: " i) ;
L.d_printf "Not havocing const argument number %d: " i ;
Sil.d_exp e ;
L.d_ln () ) ;
not is_const
@ -1783,9 +1780,8 @@ and check_variadic_sentinel_if_present ({Builtin.prop_; path; proc_name} as buil
and sym_exec_objc_getter field ret_typ tenv ret_id pdesc pname loc args prop =
let field_name, _, _ = field in
L.d_strln
(F.sprintf "No custom getter found. Executing the ObjC builtin getter with ivar %s."
(Typ.Fieldname.to_string field_name)) ;
L.d_printfln "No custom getter found. Executing the ObjC builtin getter with ivar %a."
Typ.Fieldname.pp field_name ;
match args with
| [ ( lexp
, ( ({Typ.desc= Tstruct struct_name} as typ)
@ -1800,9 +1796,8 @@ and sym_exec_objc_getter field ret_typ tenv ret_id pdesc pname loc args prop =
and sym_exec_objc_setter field _ tenv _ pdesc pname loc args prop =
let field_name, _, _ = field in
L.d_strln
(F.sprintf "No custom setter found. Executing the ObjC builtin setter with ivar %s."
(Typ.Fieldname.to_string field_name)) ;
L.d_printfln "No custom setter found. Executing the ObjC builtin setter with ivar %a."
Typ.Fieldname.pp field_name ;
match args with
| ( lexp1
, ( ({Typ.desc= Tstruct struct_name} as typ1)
@ -1880,8 +1875,8 @@ and proc_call ?dynamic_dispatch exe_env callee_summary
L.d_ln () ;
actual_pars
| [], _ ->
L.d_str ("**** ERROR: Procedure " ^ Typ.Procname.to_string callee_pname) ;
L.d_strln " mismatch in the number of parameters ****" ;
L.d_printfln "**** ERROR: Procedure %a mismatch in the number of parameters ****"
Typ.Procname.pp callee_pname ;
L.d_str "actual parameters: " ;
Sil.d_exp_list (List.map ~f:fst actual_pars) ;
L.d_ln () ;

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

@ -11,7 +11,6 @@ open! IStd
(** Interprocedural footprint analysis *)
module L = Logging
module F = Format
type splitting =
{ sub: Sil.subst
@ -175,8 +174,7 @@ let spec_find_rename trace_call summary :
let formal_parameters = List.map ~f:(fun (x, _) -> Pvar.mk_callee x proc_name) formals in
(List.map ~f:rename_vars specs, formal_parameters)
with Caml.Not_found ->
L.d_strln
("ERROR: found no entry for procedure " ^ Typ.Procname.to_string proc_name ^ ". Give up...") ;
L.d_printfln "ERROR: found no entry for procedure %a. Give up..." Typ.Procname.pp proc_name ;
raise
(Exceptions.Precondition_not_found
(Localise.verbatim_desc (Typ.Procname.to_string proc_name), __POS__))
@ -374,7 +372,7 @@ let check_dereferences caller_pname tenv callee_pname actual_pre sub spec_pre fo
L.d_ln () ;
L.d_str "exp " ;
Sil.d_exp e ;
L.d_strln (F.asprintf " desc: %a" Localise.pp_error_desc error_desc) ;
L.d_printfln " desc: %a" Localise.pp_error_desc error_desc ;
error_desc
in
let deref_no_null_check_pos =
@ -1147,7 +1145,7 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop
let posts = mk_posts tenv prop callee_pname spec.BiabductionSummary.posts in
let actual_pre = mk_actual_precondition tenv prop actual_params formal_params in
let spec_pre = BiabductionSummary.Jprop.to_prop spec.BiabductionSummary.pre in
L.d_strln ("EXECUTING SPEC " ^ string_of_int n ^ "/" ^ string_of_int nspecs) ;
L.d_printfln "EXECUTING SPEC %d/%d" n nspecs ;
L.d_strln "ACTUAL PRECONDITION =" ;
L.d_increase_indent 1 ;
Prop.d_prop actual_pre ;
@ -1155,7 +1153,7 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop
L.d_ln () ;
L.d_strln "SPEC =" ;
L.d_increase_indent 1 ;
BiabductionSummary.d_spec spec ;
L.d_pp BiabductionSummary.pp_spec spec ;
L.d_decrease_indent 1 ;
L.d_ln () ;
SymOp.pay () ;
@ -1463,10 +1461,8 @@ let exe_function_call ?dynamic_dispatch exe_env callee_summary tenv ret_id calle
in
let spec_list, formal_params = spec_find_rename trace_call callee_summary in
let nspecs = List.length spec_list in
L.d_strln
(F.sprintf "Found %d specs for function %s" nspecs (Typ.Procname.to_unique_id callee_pname)) ;
L.d_strln
(F.sprintf "START EXECUTING SPECS FOR %s from state" (Typ.Procname.to_unique_id callee_pname)) ;
L.d_printfln "Found %d specs for function %s" nspecs (Typ.Procname.to_unique_id callee_pname) ;
L.d_printfln "START EXECUTING SPECS FOR %s from state" (Typ.Procname.to_unique_id callee_pname) ;
Prop.d_prop prop ;
L.d_ln () ;
let exe_one_spec (n, spec) =

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

@ -214,7 +214,7 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
let f p = Prop.prop_normal_vars_to_primed_vars tenv p in
Propset.map tenv f pset
in
L.d_strln ("#### Extracted footprint of " ^ Typ.Procname.to_string proc_name ^ ": ####") ;
L.d_printfln "#### Extracted footprint of %a: ####" Typ.Procname.pp proc_name ;
L.d_increase_indent 1 ;
Propset.d Prop.prop_emp pset' ;
L.d_decrease_indent 1 ;
@ -222,7 +222,7 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
L.d_ln () ;
let pset'' = collect_do_abstract_pre proc_name tenv pset' in
let plist_meet = do_meet_pre tenv pset'' in
L.d_strln ("#### Footprint of " ^ Typ.Procname.to_string proc_name ^ " after Meet ####") ;
L.d_printfln "#### Footprint of %a after Meet ####" Typ.Procname.pp proc_name ;
L.d_increase_indent 1 ;
Propgraph.d_proplist Prop.prop_emp plist_meet ;
L.d_decrease_indent 1 ;
@ -233,7 +233,7 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
let jplist = do_join_pre tenv plist_meet in
L.d_decrease_indent 2 ;
L.d_ln () ;
L.d_strln ("#### Footprint of " ^ Typ.Procname.to_string proc_name ^ " after Join ####") ;
L.d_printfln "#### Footprint of %a after Join ####" Typ.Procname.pp proc_name ;
L.d_increase_indent 1 ;
BiabductionSummary.Jprop.d_list ~shallow:false jplist ;
L.d_decrease_indent 1 ;
@ -241,7 +241,7 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
let jplist' =
List.map ~f:(BiabductionSummary.Jprop.map (Prop.prop_rename_primed_footprint_vars tenv)) jplist
in
L.d_strln ("#### Renamed footprint of " ^ Typ.Procname.to_string proc_name ^ ": ####") ;
L.d_printfln "#### Renamed footprint of %a: ####" Typ.Procname.pp proc_name ;
L.d_increase_indent 1 ;
BiabductionSummary.Jprop.d_list ~shallow:false jplist' ;
L.d_decrease_indent 1 ;
@ -252,7 +252,7 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
in
List.map ~f:(BiabductionSummary.Jprop.map f) jplist'
in
L.d_strln ("#### Abstracted footprint of " ^ Typ.Procname.to_string proc_name ^ ": ####") ;
L.d_printfln "#### Abstracted footprint of %a: ####" Typ.Procname.pp proc_name ;
L.d_increase_indent 1 ;
BiabductionSummary.Jprop.d_list ~shallow:false jplist'' ;
L.d_decrease_indent 1 ;
@ -341,7 +341,7 @@ let check_prop_size_ p _ =
let size = Prop.Metrics.prop_size p in
if size > fst !prop_max_size then (
prop_max_size := (size, p) ;
L.d_strln ("Prop with new max size " ^ string_of_int size ^ ":") ;
L.d_printfln "Prop with new max size %d:" size ;
Prop.d_prop p ;
L.d_ln () )
@ -442,22 +442,17 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
F.sprintf "[%s:%s] %s" phase_string (Summary.Status.to_string status)
(Typ.Procname.to_string proc_name)
in
L.d_strln
( "**** " ^ log_string pname ^ " " ^ "Node: "
^ string_of_int (Procdesc.Node.get_id curr_node :> int)
^ ", " ^ "Procedure: " ^ Typ.Procname.to_string pname ^ ", " ^ "Session: "
^ string_of_int session ^ ", " ^ "Todo: "
^ string_of_int (Paths.PathSet.size pathset_todo)
^ " ****" ) ;
L.d_printfln "**** %s Node: %a, Procedure: %a, Session: %d, Todo: %d ****" (log_string pname)
Procdesc.Node.pp curr_node Typ.Procname.pp pname session (Paths.PathSet.size pathset_todo) ;
L.d_increase_indent 1 ;
Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv pathset_todo) ;
L.d_strln ".... Instructions: .... " ;
L.d_strln ".... Instructions: ...." ;
Procdesc.Node.d_instrs ~sub_instrs:true (State.get_instr ()) curr_node ;
L.d_ln () ;
L.d_ln ()
in
let do_prop (curr_node : ProcCfg.Exceptional.Node.t) handle_exn prop path cnt num_paths =
L.d_strln ("Processing prop " ^ string_of_int cnt ^ "/" ^ string_of_int num_paths) ;
L.d_printfln "Processing prop %d/%d" cnt num_paths ;
L.d_increase_indent 1 ;
try
State.reset_diverging_states_node () ;
@ -656,7 +651,7 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * BiabductionSumma
| _ ->
pathset
in
L.d_strln ("#### [FUNCTION " ^ Typ.Procname.to_string pname ^ "] Analysis result ####") ;
L.d_printfln "#### [FUNCTION %a] Analysis result ####" Typ.Procname.pp pname ;
Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv pathset) ;
L.d_ln () ;
let res =
@ -674,7 +669,7 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * BiabductionSumma
L.d_strln "Leak in post collection" ;
assert false
in
L.d_strln ("#### [FUNCTION " ^ Typ.Procname.to_string pname ^ "] Postconditions after join ####") ;
L.d_printfln "#### [FUNCTION %a] Postconditions after join ####" Typ.Procname.pp pname ;
L.d_increase_indent 1 ;
Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv (fst res)) ;
L.d_decrease_indent 1 ;
@ -762,7 +757,7 @@ let execute_filter_prop summary exe_env tenv proc_cfg
let pdesc = ProcCfg.Exceptional.proc_desc proc_cfg in
let pname = Procdesc.get_proc_name pdesc in
do_before_node 0 init_node ;
L.d_strln ("#### Start: RE-execution for " ^ Typ.Procname.to_string pname ^ " ####") ;
L.d_printfln "#### Start: RE-execution for %a ####" Typ.Procname.pp pname ;
L.d_indent 1 ;
L.d_strln "Precond:" ;
BiabductionSummary.Jprop.d_shallow precondition ;
@ -780,8 +775,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
("#### Finished: RE-execution for " ^ Typ.Procname.to_string pname ^ " ####") ;
L.d_printfln ~color:Green "#### Finished: RE-execution for %a ####" Typ.Procname.pp pname ;
L.d_increase_indent 1 ;
L.d_strln "Precond:" ;
Prop.d_prop (BiabductionSummary.Jprop.to_prop precondition) ;
@ -810,7 +804,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_printfln ~color:Red "#### [FUNCTION %a] ...ERROR" Typ.Procname.pp pname ;
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_printfln ~color:Pp.Red "Pruned %a that represents multiple values" pp x ;
x

14
infer/src/checkers/PulseDomain.ml
Unescape View File

@ -309,10 +309,9 @@ module Domain : AbstractDomain.S with type astate = t = struct
L.d_increase_indent 1 ;
Container.iter state.subst ~fold:AddressUF.fold_sets
~f:(fun ((repr : AddressUF.Repr.t), set) ->
L.d_strln
(F.asprintf "%a=%a" AbstractAddress.pp
(repr :> AbstractAddress.t)
AddressUnionSet.pp set) ) ;
L.d_printfln "%a=%a" AbstractAddress.pp
(repr :> AbstractAddress.t)
AddressUnionSet.pp set ) ;
L.d_decrease_indent 1 ;
let stack = AliasingDomain.map (to_canonical_address state.subst) state.astate.stack in
let invalids =
@ -468,10 +467,9 @@ module Operations = struct
let walk_access_expr ~on_last astate access_expr location =
let (access_var, _), access_list = AccessExpression.to_accesses access_expr in
if Config.write_html then
L.d_strln
(F.asprintf "Accessing %a -> [%a]" Var.pp access_var
(Pp.seq ~sep:"," AccessExpression.Access.pp)
access_list) ;
L.d_printfln "Accessing %a -> [%a]" Var.pp access_var
(Pp.seq ~sep:"," AccessExpression.Access.pp)
access_list ;
match (on_last, access_list) with
| `Overwrite new_addr, [] ->
let stack = AliasingDomain.add access_var new_addr astate.stack in

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

@ -768,7 +768,7 @@ let checker ({Callbacks.tenv; proc_desc} as callback_args) : Summary.t =
let get_node_nb_exec =
let debug =
if Config.write_html then
let f fmt = F.kasprintf L.d_strln fmt in
let f fmt = L.d_printfln fmt in
{ConstraintSolver.f}
else
let f fmt = L.(debug Analysis Verbose) fmt in

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

@ -91,7 +91,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct
find_canonical_duplicate annotated_signature typestate node linereader
in
if Config.write_html then (
let d_typestate ts = L.d_strln (F.asprintf "%a" TypeState.pp ts) in
let d_typestate ts = L.d_printfln "%a" TypeState.pp ts in
L.d_strln "before:" ;
d_typestate typestate ;
L.d_strln "after:" ;

5
infer/src/eradicate/typeState.ml
Unescape View File

@ -89,9 +89,8 @@ let map_join m1 m2 =
let join t1 t2 =
let tjoin = map_join t1 t2 in
( if Config.write_html then
let s = F.asprintf "State 1:@.%a@.State 2:@.%a@.After Join:@.%a@." pp t1 pp t2 pp tjoin in
L.d_strln s ) ;
if Config.write_html then
L.d_printfln "State 1:@.%a@.State 2:@.%a@.After Join:@.%a@." pp t1 pp t2 pp tjoin ;
tjoin

Write Preview
Loading…
Cancel
Save