From 660eceb20f971014e9a66af6fa3ee381c59f5854 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 28 Jul 2020 03:51:40 -0700 Subject: [PATCH] [pulse] log summary creation Summary: This step does extra normalization so it's useful to see what's going on when debugging. Log stuff in the html debug of the exit node. Reviewed By: da319 Differential Revision: D22596248 fbshipit-source-id: cde3bbb6c --- infer/src/pulse/PulseExecutionDomain.ml | 4 +++- infer/src/pulse/PulseSummary.ml | 8 ++++++-- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml index 0ab123aa8..459e44efd 100644 --- a/infer/src/pulse/PulseExecutionDomain.ml +++ b/infer/src/pulse/PulseExecutionDomain.ml @@ -7,6 +7,7 @@ open! IStd module F = Format +module L = Logging module AbductiveDomain = PulseAbductiveDomain type t = @@ -48,7 +49,8 @@ let map ~f exec_state = let of_posts pdesc posts = - List.filter_map posts ~f:(fun exec_state -> + List.filter_mapi posts ~f:(fun i exec_state -> let (AbortProgram astate | ContinueProgram astate | ExitProgram astate) = exec_state in + L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ; if PulseArithmetic.is_unsat_expensive astate then None else Some (map exec_state ~f:(AbductiveDomain.of_post pdesc)) ) diff --git a/infer/src/pulse/PulseSummary.ml b/infer/src/pulse/PulseSummary.ml index ee933d5c2..bfd6032a6 100644 --- a/infer/src/pulse/PulseSummary.ml +++ b/infer/src/pulse/PulseSummary.ml @@ -11,11 +11,15 @@ open PulseDomainInterface type t = ExecutionDomain.t list -let of_posts pdesc posts = ExecutionDomain.of_posts pdesc posts - let pp fmt summary = F.open_vbox 0 ; F.fprintf fmt "%d pre/post(s)@;" (List.length summary) ; List.iteri summary ~f:(fun i pre_post -> F.fprintf fmt "#%d: @[%a@]@;" i ExecutionDomain.pp pre_post ) ; F.close_box () + + +let of_posts pdesc posts = + AnalysisCallbacks.html_debug_new_node_session (Procdesc.get_exit_node pdesc) + ~pp_name:(fun fmt -> F.pp_print_string fmt "pulse summary creation") + ~f:(fun () -> ExecutionDomain.of_posts pdesc posts)