From 5653dfac3252423df6821550aa225d8f36865e14 Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Tue, 30 Oct 2018 04:33:43 -0700
Subject: [PATCH] [inferbo] Give limit on pretty print of condition set

Summary:
Sometimes in debug mode, the condition set is too big to print in the
log file.  This diff limits the maximum number of conditions to print
as 30.

Reviewed By: mbouaziz

Differential Revision: D12836661

fbshipit-source-id: 8ddfe64a7
---
 infer/src/bufferoverrun/bufferOverrunChecker.ml    |  2 +-
 .../bufferoverrun/bufferOverrunProofObligations.ml |  4 ++--
 infer/src/istd/IList.ml                            | 14 ++++++++++++++
 infer/src/istd/IList.mli                           |  8 ++++++++
 4 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml
index 5739a8c83..cacc9e25a 100644
--- a/infer/src/bufferoverrun/bufferOverrunChecker.ml
+++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml
@@ -662,7 +662,7 @@ module Report = struct
     L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ;
     L.(debug BufferOverrun Verbose) "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre ;
     L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr ~print_types:true Pp.text) instr ;
-    L.(debug BufferOverrun Verbose) "@[<v 2>@\n@\n%a" PO.ConditionSet.pp cond_set ;
+    L.(debug BufferOverrun Verbose) "@\n@\n@[<v 2>%a" PO.ConditionSet.pp cond_set ;
     L.(debug BufferOverrun Verbose) "@]@\n" ;
     L.(debug BufferOverrun Verbose) "================================@\n@."
 
diff --git a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
index 603041961..61d1b5b51 100644
--- a/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
+++ b/infer/src/bufferoverrun/bufferOverrunProofObligations.ml
@@ -851,9 +851,9 @@ module ConditionSet = struct
 
   let pp : Format.formatter -> t -> unit =
    fun fmt condset ->
-    let pp_sep fmt () = F.fprintf fmt ",@," in
+    let pp_sep fmt () = F.fprintf fmt ",@;" in
     F.fprintf fmt "Safety conditions:@;@[<hov 2>{ %a }@]"
-      (F.pp_print_list ~pp_sep ConditionWithTrace.pp)
+      (IList.pp_print_list ~max:30 ~pp_sep ConditionWithTrace.pp)
       condset
 
 
diff --git a/infer/src/istd/IList.ml b/infer/src/istd/IList.ml
index a3a370a58..23bd5b81c 100644
--- a/infer/src/istd/IList.ml
+++ b/infer/src/istd/IList.ml
@@ -171,3 +171,17 @@ let remove_first =
         if f hd then Some (List.rev_append rev_front tl) else aux tl ~f (hd :: rev_front)
   in
   fun list ~f -> aux list ~f []
+
+
+let pp_print_list ~max ?(pp_sep = Format.pp_print_cut) pp_v ppf =
+  let rec aux n = function
+    | [] ->
+        ()
+    | v :: rest ->
+        if n >= max then Format.fprintf ppf " ..."
+        else (
+          pp_sep ppf () ;
+          pp_v ppf v ;
+          aux (n + 1) rest )
+  in
+  function [] -> () | [v] -> pp_v ppf v | v :: rest -> pp_v ppf v ; aux 1 rest
diff --git a/infer/src/istd/IList.mli b/infer/src/istd/IList.mli
index 9c4e9be9e..ed01e0a50 100644
--- a/infer/src/istd/IList.mli
+++ b/infer/src/istd/IList.mli
@@ -41,3 +41,11 @@ val opt_cons : 'a option -> 'a list -> 'a list
 (** [opt_cons None l] returns [l]. [opt_cons (Some x) l] returns [x :: l]*)
 
 val remove_first : 'a list -> f:('a -> bool) -> 'a list option
+
+val pp_print_list :
+     max:int
+  -> ?pp_sep:(Format.formatter -> unit -> unit)
+  -> (Format.formatter -> 'a -> unit)
+  -> Format.formatter
+  -> 'a list
+  -> unit