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

Logging: increase/decrease indent

Browse Source 
Reviewed By: jeremydubreil

Differential Revision: D12840641

fbshipit-source-id: faed7dfc7
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 18c45947da
commit 17ff54f17a
8 changed files with 91 additions and 93 deletions
Show Stats Download Patch File Download Diff File

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

@ -348,8 +348,8 @@ let setup_log_file () =
(** delayable print action *) (** delayable print action *)
type print_action = type print_action =
| PTdecrease_indent : int -> print_action | PTdecrease_indent : print_action
| PTincrease_indent : int -> print_action | PTincrease_indent : print_action
| PTstr : {s: string; color: Pp.color option; ln: bool} -> print_action | PTstr : {s: string; color: Pp.color option; ln: bool} -> print_action
| PTwarning : string -> print_action | PTwarning : string -> print_action
| PTerror : string -> print_action | PTerror : string -> print_action
@ -377,12 +377,10 @@ let pp_maybe_with_color ?color pp fmt x =
(** Execute the delayed print actions *) (** Execute the delayed print actions *)
let force_delayed_print fmt = function let force_delayed_print fmt = function
| PTdecrease_indent n -> | PTdecrease_indent ->
for _ = 1 to n do F.pp_close_box fmt ()
F.fprintf fmt "@]" | PTincrease_indent ->
done F.fprintf fmt " @["
| PTincrease_indent n ->
F.fprintf fmt "%s@[" (String.make (2 * n) ' ')
| PTstr {s; color; ln} -> | PTstr {s; color; ln} ->
pp_maybe_with_color ?color F.pp_print_string fmt s ; pp_maybe_with_color ?color F.pp_print_string fmt s ;
if ln then F.pp_force_newline fmt () if ln then F.pp_force_newline fmt ()
@ -458,7 +456,7 @@ let d_indent indent =
(** dump command to increase the indentation level *) (** dump command to increase the indentation level *)
let d_increase_indent (indent : int) = add_print_action (PTincrease_indent indent) let d_increase_indent () = add_print_action PTincrease_indent
(** dump command to decrease the indentation level *) (** dump command to decrease the indentation level *)
let d_decrease_indent (indent : int) = add_print_action (PTdecrease_indent indent) let d_decrease_indent () = add_print_action PTdecrease_indent

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

@ -126,8 +126,8 @@ val d_info : string -> unit
val d_indent : int -> unit val d_indent : int -> unit
(** dump an indentation *) (** dump an indentation *)
val d_increase_indent : int -> unit val d_increase_indent : unit -> unit
(** dump command to increase the indentation level *) (** dump command to increase the indentation level *)
val d_decrease_indent : int -> unit val d_decrease_indent : unit -> unit
(** dump command to decrease the indentation level *) (** dump command to decrease the indentation level *)

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

@ -1019,7 +1019,7 @@ let check_junk pname tenv prop =
if should_remove_hpred entries then ( if should_remove_hpred entries then (
let part = if fp_part then "footprint" else "normal" in let part = if fp_part then "footprint" else "normal" in
L.d_printfln ".... Prop with garbage in %s part ...." part ; L.d_printfln ".... Prop with garbage in %s part ...." part ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
L.d_strln "PROP:" ; L.d_strln "PROP:" ;
Prop.d_prop prop ; Prop.d_prop prop ;
L.d_ln () ; L.d_ln () ;
@ -1052,7 +1052,7 @@ let check_junk pname tenv prop =
in in
List.iter ~f:do_entry entries ; !res List.iter ~f:do_entry entries ; !res
in in
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
let is_undefined = let is_undefined =
Option.value_map ~f:PredSymb.is_undef ~default:false alloc_attribute Option.value_map ~f:PredSymb.is_undef ~default:false alloc_attribute
in in

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

@ -15,7 +15,7 @@ module F = Format
let decrease_indent_when_exception thunk = let decrease_indent_when_exception thunk =
try thunk () with exn when SymOp.exn_not_failure exn -> try thunk () with exn when SymOp.exn_not_failure exn ->
IExn.reraise_after exn ~f:(fun () -> L.d_decrease_indent 1) IExn.reraise_after exn ~f:(fun () -> L.d_decrease_indent ())
let compute_max_from_nonempty_int_list l = uw (List.max_elt ~compare:IntLit.compare_value l) let compute_max_from_nonempty_int_list l = uw (List.max_elt ~compare:IntLit.compare_value l)
@ -1212,9 +1212,9 @@ end = struct
let d_missing_ sub = let d_missing_ sub =
L.d_strln "SUB: " ; L.d_strln "SUB: " ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Prop.d_sub sub ; Prop.d_sub sub ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
if !missing_pi <> [] && !missing_sigma <> [] then ( if !missing_pi <> [] && !missing_sigma <> [] then (
L.d_ln () ; Prop.d_pi !missing_pi ; L.d_strln "*" ; 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_pi <> [] then ( L.d_ln () ; Prop.d_pi !missing_pi )
@ -1222,15 +1222,15 @@ end = struct
if !missing_fld <> [] then ( if !missing_fld <> [] then (
L.d_ln () ; L.d_ln () ;
L.d_strln "MISSING FLD:" ; L.d_strln "MISSING FLD:" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Prop.d_sigma !missing_fld ; Prop.d_sigma !missing_fld ;
L.d_decrease_indent 1 ) ; L.d_decrease_indent () ) ;
if !missing_typ <> [] then ( if !missing_typ <> [] then (
L.d_ln () ; L.d_ln () ;
L.d_strln "MISSING TYPING:" ; L.d_strln "MISSING TYPING:" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
d_typings !missing_typ ; d_typings !missing_typ ;
L.d_decrease_indent 1 ) L.d_decrease_indent () )
let d_missing sub = let d_missing sub =
@ -1246,10 +1246,10 @@ end = struct
if !frame_fld <> [] then ( if !frame_fld <> [] then (
L.d_ln () ; L.d_ln () ;
L.d_strln "[FRAME FLD:" ; L.d_strln "[FRAME FLD:" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Prop.d_sigma !frame_fld ; Prop.d_sigma !frame_fld ;
L.d_str "]" ; L.d_str "]" ;
L.d_decrease_indent 1 ) L.d_decrease_indent () )
let d_frame_typ () = let d_frame_typ () =
@ -1257,19 +1257,19 @@ end = struct
if !frame_typ <> [] then ( if !frame_typ <> [] then (
L.d_ln () ; L.d_ln () ;
L.d_strln "[FRAME TYPING:" ; L.d_strln "[FRAME TYPING:" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
d_typings !frame_typ ; d_typings !frame_typ ;
L.d_str "]" ; L.d_str "]" ;
L.d_decrease_indent 1 ) L.d_decrease_indent () )
(** Dump an implication *) (** Dump an implication *)
let d_implication (sub1, sub2) (p1, p2) = let d_implication (sub1, sub2) (p1, p2) =
let p1, p2 = (Prop.prop_sub sub1 p1, Prop.prop_sub sub2 p2) in let p1, p2 = (Prop.prop_sub sub1 p1, Prop.prop_sub sub2 p2) in
L.d_strln "SUB:" ; L.d_strln "SUB:" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Prop.d_sub sub1 ; Prop.d_sub sub1 ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
Prop.d_prop p1 ; Prop.d_prop p1 ;
d_missing sub2 ; d_missing sub2 ;
@ -2114,14 +2114,14 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
let _, para_inst1 = Sil.hpara_instantiate para1 e1 n' elist1 in let _, para_inst1 = Sil.hpara_instantiate para1 e1 n' elist1 in
let hpred_list1 = para_inst1 @ [Prop.mk_lseg tenv Sil.Lseg_PE para1 n' f1 elist1] in let hpred_list1 = para_inst1 @ [Prop.mk_lseg tenv Sil.Lseg_PE para1 n' f1 elist1] in
let iter1'' = Prop.prop_iter_update_current_by_list iter1' hpred_list1 in let iter1'' = Prop.prop_iter_update_current_by_list iter1' hpred_list1 in
L.d_increase_indent 1 ; L.d_increase_indent () ;
let res = let res =
decrease_indent_when_exception (fun () -> decrease_indent_when_exception (fun () ->
hpred_imply tenv calc_index_frame calc_missing subs hpred_imply tenv calc_index_frame calc_missing subs
(Prop.prop_iter_to_prop tenv iter1'') (Prop.prop_iter_to_prop tenv iter1'')
sigma2 hpred2 ) sigma2 hpred2 )
in in
L.d_decrease_indent 1 ; res L.d_decrease_indent () ; res
| Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _ | Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
when Exp.equal (Sil.exp_sub (fst subs) iF1) e2 -> when Exp.equal (Sil.exp_sub (fst subs) iF1) e2 ->
(* Unroll dllseg forward *) (* Unroll dllseg forward *)
@ -2131,14 +2131,14 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
para_inst1 @ [Prop.mk_dllseg tenv Sil.Lseg_PE para1 n' iF1 oF1 iB1 elist1] para_inst1 @ [Prop.mk_dllseg tenv Sil.Lseg_PE para1 n' iF1 oF1 iB1 elist1]
in in
let iter1'' = Prop.prop_iter_update_current_by_list iter1' hpred_list1 in let iter1'' = Prop.prop_iter_update_current_by_list iter1' hpred_list1 in
L.d_increase_indent 1 ; L.d_increase_indent () ;
let res = let res =
decrease_indent_when_exception (fun () -> decrease_indent_when_exception (fun () ->
hpred_imply tenv calc_index_frame calc_missing subs hpred_imply tenv calc_index_frame calc_missing subs
(Prop.prop_iter_to_prop tenv iter1'') (Prop.prop_iter_to_prop tenv iter1'')
sigma2 hpred2 ) sigma2 hpred2 )
in in
L.d_decrease_indent 1 ; res L.d_decrease_indent () ; res
| Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _ | Sil.Hdllseg (Sil.Lseg_NE, para1, iF1, oB1, oF1, iB1, elist1), _
when Exp.equal (Sil.exp_sub (fst subs) iB1) e2 -> when Exp.equal (Sil.exp_sub (fst subs) iB1) e2 ->
(* Unroll dllseg backward *) (* Unroll dllseg backward *)
@ -2148,14 +2148,14 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
para_inst1 @ [Prop.mk_dllseg tenv Sil.Lseg_PE para1 iF1 oB1 iB1 n' elist1] para_inst1 @ [Prop.mk_dllseg tenv Sil.Lseg_PE para1 iF1 oB1 iB1 n' elist1]
in in
let iter1'' = Prop.prop_iter_update_current_by_list iter1' hpred_list1 in let iter1'' = Prop.prop_iter_update_current_by_list iter1' hpred_list1 in
L.d_increase_indent 1 ; L.d_increase_indent () ;
let res = let res =
decrease_indent_when_exception (fun () -> decrease_indent_when_exception (fun () ->
hpred_imply tenv calc_index_frame calc_missing subs hpred_imply tenv calc_index_frame calc_missing subs
(Prop.prop_iter_to_prop tenv iter1'') (Prop.prop_iter_to_prop tenv iter1'')
sigma2 hpred2 ) sigma2 hpred2 )
in in
L.d_decrease_indent 1 ; res L.d_decrease_indent () ; res
| _ -> | _ ->
assert false ) ) ) assert false ) ) )
| Sil.Hlseg (k, para2, e2_, f2_, elist2_) -> ( | Sil.Hlseg (k, para2, e2_, f2_, elist2_) -> (
@ -2182,13 +2182,13 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
| None -> | None ->
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2_ in let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2_ in
let _, para_inst2 = Sil.hpara_instantiate para2 e2 f2 elist2 in let _, para_inst2 = Sil.hpara_instantiate para2 e2 f2 elist2 in
L.d_increase_indent 1 ; L.d_increase_indent () ;
let res = let res =
decrease_indent_when_exception (fun () -> decrease_indent_when_exception (fun () ->
sigma_imply tenv calc_index_frame false subs prop1 para_inst2 ) sigma_imply tenv calc_index_frame false subs prop1 para_inst2 )
in in
(* calc_missing is false as we're checking an instantiation of the original list *) (* calc_missing is false as we're checking an instantiation of the original list *)
L.d_decrease_indent 1 ; res L.d_decrease_indent () ; res
| Some iter1' -> ( | Some iter1' -> (
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2_ in let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2_ in
(* force instantiation of existentials *) (* force instantiation of existentials *)
@ -2210,7 +2210,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
let hpred_list2 = let hpred_list2 =
para_inst2 @ [Prop.mk_lseg tenv Sil.Lseg_PE para2 n' f2_ elist2_] para_inst2 @ [Prop.mk_lseg tenv Sil.Lseg_PE para2 n' f2_ elist2_]
in in
L.d_increase_indent 1 ; L.d_increase_indent () ;
let res = let res =
decrease_indent_when_exception (fun () -> decrease_indent_when_exception (fun () ->
try sigma_imply tenv calc_index_frame calc_missing subs prop1 hpred_list2 try sigma_imply tenv calc_index_frame calc_missing subs prop1 hpred_list2
@ -2219,7 +2219,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
let _, para_inst3 = Sil.hpara_instantiate para2 e2_ f2_ elist2 in let _, para_inst3 = Sil.hpara_instantiate para2 e2_ f2_ elist2 in
sigma_imply tenv calc_index_frame calc_missing subs prop1 para_inst3 ) sigma_imply tenv calc_index_frame calc_missing subs prop1 para_inst3 )
in in
L.d_decrease_indent 1 ; res L.d_decrease_indent () ; res
| Sil.Hdllseg _ -> | Sil.Hdllseg _ ->
assert false ) ) ) assert false ) ) )
| Sil.Hdllseg (Sil.Lseg_PE, _, _, _, _, _, _) -> | Sil.Hdllseg (Sil.Lseg_PE, _, _, _, _, _, _) ->
@ -2261,13 +2261,13 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
else assert false else assert false
(* Only base case of rhs list considered for now *) (* Only base case of rhs list considered for now *)
in in
L.d_increase_indent 1 ; L.d_increase_indent () ;
let res = let res =
decrease_indent_when_exception (fun () -> decrease_indent_when_exception (fun () ->
sigma_imply tenv calc_index_frame false subs prop1 para_inst2 ) sigma_imply tenv calc_index_frame false subs prop1 para_inst2 )
in in
(* calc_missing is false as we're checking an instantiation of the original list *) (* calc_missing is false as we're checking an instantiation of the original list *)
L.d_decrease_indent 1 ; res L.d_decrease_indent () ; res
| Some iter1' -> | Some iter1' ->
(* Only consider implications between identical listsegs for now *) (* Only consider implications between identical listsegs for now *)
let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2 in let elist2 = List.map ~f:(fun e -> Sil.exp_sub (snd subs) e) elist2 in
@ -2376,12 +2376,12 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
let normal_case hpred2' = let normal_case hpred2' =
let subs', prop1' = let subs', prop1' =
try try
L.d_increase_indent 1 ; L.d_increase_indent () ;
let res = let res =
decrease_indent_when_exception (fun () -> decrease_indent_when_exception (fun () ->
hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2' ) hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2' )
in in
L.d_decrease_indent 1 ; res L.d_decrease_indent () ; res
with IMPL_EXC _ when calc_missing -> ( with IMPL_EXC _ when calc_missing -> (
match is_constant_string_class subs hpred2' with match is_constant_string_class subs hpred2' with
| Some (s, is_string) -> | Some (s, is_string) ->
@ -2409,12 +2409,12 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
ProverState.add_missing_sigma [hpred2'] ; ProverState.add_missing_sigma [hpred2'] ;
(subs', prop1) ) (subs', prop1) )
in in
L.d_increase_indent 1 ; L.d_increase_indent () ;
let res = let res =
decrease_indent_when_exception (fun () -> decrease_indent_when_exception (fun () ->
sigma_imply tenv calc_index_frame calc_missing subs' prop1' sigma2' ) sigma_imply tenv calc_index_frame calc_missing subs' prop1' sigma2' )
in in
L.d_decrease_indent 1 ; res L.d_decrease_indent () ; res
in in
match hpred2 with match hpred2 with
| Sil.Hpointsto (e2_, se2, t) -> | Sil.Hpointsto (e2_, se2, t) ->
@ -2548,26 +2548,26 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
List.iter ~f:(fun a -> ProverState.add_bounds_check (ProverState.BCfrom_pre a)) pi2_bcheck ; List.iter ~f:(fun a -> ProverState.add_bounds_check (ProverState.BCfrom_pre a)) pi2_bcheck ;
L.d_strln "pre_check_pure_implication" ; L.d_strln "pre_check_pure_implication" ;
L.d_strln "pi1:" ; L.d_strln "pi1:" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Prop.d_pi pi1 ; Prop.d_pi pi1 ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_strln "pi2:" ; L.d_strln "pi2:" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Prop.d_pi pi2 ; Prop.d_pi pi2 ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
if pi2_bcheck <> [] then ( L.d_str "pi2 bounds checks: " ; Prop.d_pi pi2_bcheck ; 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 "returns" ;
L.d_strln "sub1:" ; L.d_strln "sub1:" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Prop.d_sub (fst subs) ; Prop.d_sub (fst subs) ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_strln "sub2:" ; L.d_strln "sub2:" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Prop.d_sub (snd subs) ; Prop.d_sub (snd subs) ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
let (sub1, sub2), frame_prop = sigma_imply tenv false calc_missing subs prop1 sigma2 in let (sub1, sub2), frame_prop = sigma_imply tenv false calc_missing subs prop1 sigma2 in
let pi1' = Prop.pi_sub sub1 pi1 in let pi1' = Prop.pi_sub sub1 pi1 in
@ -2579,9 +2579,9 @@ let check_implication_base pname tenv check_frame_empty calc_missing prop1 prop2
(* handle implicit bound checks, plus those from array_len_imply *) (* handle implicit bound checks, plus those from array_len_imply *)
check_array_bounds tenv (sub1, sub2) prop_for_impl ; check_array_bounds tenv (sub1, sub2) prop_for_impl ;
L.d_strln "Result of Abduction" ; L.d_strln "Result of Abduction" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
d_impl (sub1, sub2) (prop1, prop2) ; d_impl (sub1, sub2) (prop1, prop2) ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_strln "returning TRUE" ; L.d_strln "returning TRUE" ;
let frame = frame_prop.Prop.sigma in let frame = frame_prop.Prop.sigma in

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

@ -80,7 +80,7 @@ let bounds_check tenv pname prop len e =
let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp (t : Typ.t) let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp (t : Typ.t)
(off : Sil.offset list) inst : Sil.atom list * Sil.strexp * Typ.t = (off : Sil.offset list) inst : Sil.atom list * Sil.strexp * Typ.t =
if Config.trace_rearrange then ( if Config.trace_rearrange then (
L.d_increase_indent 1 ; L.d_increase_indent () ;
L.d_strln "entering create_struct_values" ; L.d_strln "entering create_struct_values" ;
L.d_str "typ: " ; L.d_str "typ: " ;
Typ.d_full t ; Typ.d_full t ;
@ -177,7 +177,7 @@ let rec create_struct_values pname tenv orig_prop footprint_part kind max_stamp
let _, se, _ = res in let _, se, _ = res in
L.d_strln "exiting create_struct_values, returning" ; L.d_strln "exiting create_struct_values, returning" ;
Sil.d_sexp se ; Sil.d_sexp se ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_ln () ) ; L.d_ln () ) ;
res res
@ -1101,7 +1101,7 @@ let pp_rearrangement_error message prop lexp =
(** do re-arrangement for an iter whose current element is a pointsto *) (** do re-arrangement for an iter whose current element is a pointsto *)
let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst = let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
if Config.trace_rearrange then ( if Config.trace_rearrange then (
L.d_increase_indent 1 ; L.d_increase_indent () ;
L.d_strln "entering iter_rearrange_ptsto" ; L.d_strln "entering iter_rearrange_ptsto" ;
L.d_str "lexp: " ; L.d_str "lexp: " ;
Sil.d_exp lexp ; Sil.d_exp lexp ;
@ -1149,7 +1149,7 @@ let iter_rearrange_ptsto pname tenv orig_prop iter lexp inst =
if Config.trace_rearrange then ( if Config.trace_rearrange then (
L.d_strln "exiting iter_rearrange_ptsto, returning results" ; L.d_strln "exiting iter_rearrange_ptsto, returning results" ;
Prop.d_proplist_with_typ (List.map ~f:(Prop.prop_iter_to_prop tenv) res) ; Prop.d_proplist_with_typ (List.map ~f:(Prop.prop_iter_to_prop tenv) res) ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_ln () ) ; L.d_ln () ) ;
res res
@ -1361,12 +1361,12 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst :
| Tstruct _ -> | Tstruct _ ->
(* access through field: get the struct type from the field *) (* access through field: get the struct type from the field *)
if Config.trace_rearrange then ( if Config.trace_rearrange then (
L.d_increase_indent 1 ; L.d_increase_indent () ;
L.d_printfln "iter_rearrange: root of lexp accesses field %a" Typ.Fieldname.pp f ; L.d_printfln "iter_rearrange: root of lexp accesses field %a" Typ.Fieldname.pp f ;
L.d_str " struct type from field: " ; L.d_str " struct type from field: " ;
Typ.d_full fld_typ ; Typ.d_full fld_typ ;
L.d_ln () ; L.d_ln () ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ) ; L.d_ln () ) ;
fld_typ fld_typ
| _ -> | _ ->
@ -1378,7 +1378,7 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst :
in in
let typ = root_typ_of_offsets (Sil.exp_get_offsets lexp) in let typ = root_typ_of_offsets (Sil.exp_get_offsets lexp) in
if Config.trace_rearrange then ( if Config.trace_rearrange then (
L.d_increase_indent 1 ; L.d_increase_indent () ;
L.d_strln "entering iter_rearrange" ; L.d_strln "entering iter_rearrange" ;
L.d_str "lexp: " ; L.d_str "lexp: " ;
Sil.d_exp lexp ; Sil.d_exp lexp ;
@ -1469,7 +1469,7 @@ let rec iter_rearrange pname tenv lexp typ_from_instr prop iter inst :
if Config.trace_rearrange then ( if Config.trace_rearrange then (
L.d_strln "exiting iter_rearrange, returning results" ; L.d_strln "exiting iter_rearrange, returning results" ;
Prop.d_proplist_with_typ (List.map ~f:(Prop.prop_iter_to_prop tenv) res) ; Prop.d_proplist_with_typ (List.map ~f:(Prop.prop_iter_to_prop tenv) res) ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_ln () ) ; L.d_ln () ) ;
res res

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

@ -864,7 +864,7 @@ let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre pat
(Prop.prop_sub split.sub p, path) ) (Prop.prop_sub split.sub p, path) )
posts' posts'
in in
L.d_increase_indent 1 ; L.d_increase_indent () ;
L.d_strln "New footprint:" ; L.d_strln "New footprint:" ;
Prop.d_pi_sigma split.missing_pi split.missing_sigma ; Prop.d_pi_sigma split.missing_pi split.missing_sigma ;
L.d_ln () ; L.d_ln () ;
@ -885,7 +885,7 @@ let combine tenv ret_id (posts : ('a Prop.t * Paths.Path.t) list) actual_pre pat
L.d_ln () ; L.d_ln () ;
L.d_strln "Instantiated post:" ; L.d_strln "Instantiated post:" ;
Propgraph.d_proplist Prop.prop_emp (List.map ~f:fst instantiated_post) ; Propgraph.d_proplist Prop.prop_emp (List.map ~f:fst instantiated_post) ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
let compute_result post_p = let compute_result post_p =
let post_p' = let post_p' =
@ -1147,14 +1147,14 @@ let exe_spec exe_env tenv ret_id (n, nspecs) caller_pdesc callee_pname loc prop
let spec_pre = BiabductionSummary.Jprop.to_prop spec.BiabductionSummary.pre in let spec_pre = BiabductionSummary.Jprop.to_prop spec.BiabductionSummary.pre in
L.d_printfln "EXECUTING SPEC %d/%d" n nspecs ; L.d_printfln "EXECUTING SPEC %d/%d" n nspecs ;
L.d_strln "ACTUAL PRECONDITION =" ; L.d_strln "ACTUAL PRECONDITION =" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Prop.d_prop actual_pre ; Prop.d_prop actual_pre ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_strln "SPEC =" ; L.d_strln "SPEC =" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
L.d_pp BiabductionSummary.pp_spec spec ; L.d_pp BiabductionSummary.pp_spec spec ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
SymOp.pay () ; SymOp.pay () ;
(* pay one symop *) (* pay one symop *)

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

@ -215,36 +215,36 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
Propset.map tenv f pset Propset.map tenv f pset
in in
L.d_printfln "#### Extracted footprint of %a: ####" Typ.Procname.pp proc_name ; L.d_printfln "#### Extracted footprint of %a: ####" Typ.Procname.pp proc_name ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Propset.d Prop.prop_emp pset' ; Propset.d Prop.prop_emp pset' ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_ln () ; L.d_ln () ;
let pset'' = collect_do_abstract_pre proc_name tenv pset' in let pset'' = collect_do_abstract_pre proc_name tenv pset' in
let plist_meet = do_meet_pre tenv pset'' in let plist_meet = do_meet_pre tenv pset'' in
L.d_printfln "#### Footprint of %a after Meet ####" Typ.Procname.pp proc_name ; L.d_printfln "#### Footprint of %a after Meet ####" Typ.Procname.pp proc_name ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Propgraph.d_proplist Prop.prop_emp plist_meet ; Propgraph.d_proplist Prop.prop_emp plist_meet ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_ln () ; L.d_ln () ;
L.d_increase_indent 2 ; L.d_increase_indent () ;
(* Indent for the join output *) (* Indent for the join output *)
let jplist = do_join_pre tenv plist_meet in let jplist = do_join_pre tenv plist_meet in
L.d_decrease_indent 2 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
L.d_printfln "#### Footprint of %a after Join ####" Typ.Procname.pp proc_name ; L.d_printfln "#### Footprint of %a after Join ####" Typ.Procname.pp proc_name ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
BiabductionSummary.Jprop.d_list ~shallow:false jplist ; BiabductionSummary.Jprop.d_list ~shallow:false jplist ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
let jplist' = let jplist' =
List.map ~f:(BiabductionSummary.Jprop.map (Prop.prop_rename_primed_footprint_vars tenv)) jplist List.map ~f:(BiabductionSummary.Jprop.map (Prop.prop_rename_primed_footprint_vars tenv)) jplist
in in
L.d_printfln "#### Renamed footprint of %a: ####" Typ.Procname.pp proc_name ; L.d_printfln "#### Renamed footprint of %a: ####" Typ.Procname.pp proc_name ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
BiabductionSummary.Jprop.d_list ~shallow:false jplist' ; BiabductionSummary.Jprop.d_list ~shallow:false jplist' ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
let jplist'' = let jplist'' =
let f p = let f p =
@ -253,9 +253,9 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
List.map ~f:(BiabductionSummary.Jprop.map f) jplist' List.map ~f:(BiabductionSummary.Jprop.map f) jplist'
in in
L.d_printfln "#### Abstracted footprint of %a: ####" Typ.Procname.pp proc_name ; L.d_printfln "#### Abstracted footprint of %a: ####" Typ.Procname.pp proc_name ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
BiabductionSummary.Jprop.d_list ~shallow:false jplist'' ; BiabductionSummary.Jprop.d_list ~shallow:false jplist'' ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
jplist'' jplist''
@ -444,7 +444,7 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
in in
L.d_printfln "**** %s Node: %a, Procedure: %a, Session: %d, Todo: %d ****" (log_string pname) 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) ; Procdesc.Node.pp curr_node Typ.Procname.pp pname session (Paths.PathSet.size pathset_todo) ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv pathset_todo) ; 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 ; Procdesc.Node.d_instrs ~sub_instrs:true (State.get_instr ()) curr_node ;
@ -453,20 +453,20 @@ let forward_tabulate summary exe_env tenv proc_cfg wl =
in in
let do_prop (curr_node : ProcCfg.Exceptional.Node.t) handle_exn prop path cnt num_paths = let do_prop (curr_node : ProcCfg.Exceptional.Node.t) handle_exn prop path cnt num_paths =
L.d_printfln "Processing prop %d/%d" cnt num_paths ; L.d_printfln "Processing prop %d/%d" cnt num_paths ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
try try
State.reset_diverging_states_node () ; State.reset_diverging_states_node () ;
let pset = let pset =
do_symbolic_execution exe_env summary proc_cfg handle_exn tenv curr_node prop path do_symbolic_execution exe_env summary proc_cfg handle_exn tenv curr_node prop path
in in
propagate_nodes_divergence tenv proc_cfg pset curr_node wl ; propagate_nodes_divergence tenv proc_cfg pset curr_node wl ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () L.d_ln ()
with exn -> with exn ->
IExn.reraise_if exn ~f:(fun () -> IExn.reraise_if exn ~f:(fun () ->
(not !BiabductionConfig.footprint) || not (Exceptions.handle_exception exn) ) ; (not !BiabductionConfig.footprint) || not (Exceptions.handle_exception exn) ) ;
handle_exn exn ; handle_exn exn ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () L.d_ln ()
in in
let do_node curr_node pathset_todo session handle_exn = let do_node curr_node pathset_todo session handle_exn =
@ -670,9 +670,9 @@ let collect_postconditions wl tenv proc_cfg : Paths.PathSet.t * BiabductionSumma
assert false assert false
in in
L.d_printfln "#### [FUNCTION %a] Postconditions after join ####" Typ.Procname.pp pname ; L.d_printfln "#### [FUNCTION %a] Postconditions after join ####" Typ.Procname.pp pname ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv (fst res)) ; Propset.d Prop.prop_emp (Paths.PathSet.to_propset tenv (fst res)) ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
L.d_ln () ; L.d_ln () ;
res res
@ -776,7 +776,7 @@ let execute_filter_prop summary exe_env tenv proc_cfg
forward_tabulate summary exe_env tenv proc_cfg wl ; forward_tabulate summary exe_env tenv proc_cfg wl ;
do_before_node 0 init_node ; do_before_node 0 init_node ;
L.d_printfln ~color:Green "#### Finished: RE-execution for %a ####" Typ.Procname.pp pname ; L.d_printfln ~color:Green "#### Finished: RE-execution for %a ####" Typ.Procname.pp pname ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
L.d_strln "Precond:" ; L.d_strln "Precond:" ;
Prop.d_prop (BiabductionSummary.Jprop.to_prop precondition) ; Prop.d_prop (BiabductionSummary.Jprop.to_prop precondition) ;
L.d_ln () ; L.d_ln () ;
@ -800,16 +800,16 @@ let execute_filter_prop summary exe_env tenv proc_cfg
BiabductionSummary.Jprop.Joined (n, p, jp1, jp2) BiabductionSummary.Jprop.Joined (n, p, jp1, jp2)
in in
let spec = BiabductionSummary.{pre; posts; visited} in let spec = BiabductionSummary.{pre; posts; visited} in
L.d_decrease_indent 1 ; do_after_node init_node ; Some spec L.d_decrease_indent () ; do_after_node init_node ; Some spec
with RE_EXE_ERROR -> with RE_EXE_ERROR ->
do_before_node 0 init_node ; do_before_node 0 init_node ;
Printer.force_delayed_prints () ; Printer.force_delayed_prints () ;
L.d_printfln ~color:Red "#### [FUNCTION %a] ...ERROR" Typ.Procname.pp pname ; L.d_printfln ~color:Red "#### [FUNCTION %a] ...ERROR" Typ.Procname.pp pname ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
L.d_strln "when starting from pre:" ; L.d_strln "when starting from pre:" ;
Prop.d_prop (BiabductionSummary.Jprop.to_prop precondition) ; Prop.d_prop (BiabductionSummary.Jprop.to_prop precondition) ;
L.d_strln "This precondition is filtered out." ; L.d_strln "This precondition is filtered out." ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
do_after_node init_node ; do_after_node init_node ;
None None
@ -846,12 +846,12 @@ let perform_analysis_phase exe_env tenv (summary : Summary.t) (proc_cfg : ProcCf
in in
Propset.fold add Paths.PathSet.empty init_props Propset.fold add Paths.PathSet.empty init_props
in in
L.d_increase_indent 1 ; L.d_increase_indent () ;
L.d_strln "initial props =" ; L.d_strln "initial props =" ;
Propset.d Prop.prop_emp init_props ; Propset.d Prop.prop_emp init_props ;
L.d_ln () ; L.d_ln () ;
L.d_ln () ; L.d_ln () ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
Worklist.add wl start_node ; Worklist.add wl start_node ;
ignore (path_set_put_todo wl start_node init_edgeset) ; ignore (path_set_put_todo wl start_node init_edgeset) ;
forward_tabulate summary exe_env tenv proc_cfg wl forward_tabulate summary exe_env tenv proc_cfg wl

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

@ -306,13 +306,13 @@ module Domain : AbstractDomain.S with type astate = t = struct
in in
if has_converged then ( if has_converged then (
L.d_strln "Join unified addresses:" ; L.d_strln "Join unified addresses:" ;
L.d_increase_indent 1 ; L.d_increase_indent () ;
Container.iter state.subst ~fold:AddressUF.fold_sets Container.iter state.subst ~fold:AddressUF.fold_sets
~f:(fun ((repr : AddressUF.Repr.t), set) -> ~f:(fun ((repr : AddressUF.Repr.t), set) ->
L.d_printfln "%a=%a" AbstractAddress.pp L.d_printfln "%a=%a" AbstractAddress.pp
(repr :> AbstractAddress.t) (repr :> AbstractAddress.t)
AddressUnionSet.pp set ) ; AddressUnionSet.pp set ) ;
L.d_decrease_indent 1 ; L.d_decrease_indent () ;
let stack = AliasingDomain.map (to_canonical_address state.subst) state.astate.stack in let stack = AliasingDomain.map (to_canonical_address state.subst) state.astate.stack in
let invalids = let invalids =
InvalidAddressesDomain.map (to_canonical_address state.subst) state.astate.invalids InvalidAddressesDomain.map (to_canonical_address state.subst) state.astate.invalids

Write Preview
Loading…
Cancel
Save