[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

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

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
 
 

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

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