Replace eager show with lazy pretty during analysis

src/analyses/c2poAnalysis.ml

@@ -100,7 +100,7 @@ struct
     | lval_size, (Some rterm, Some roffset) ->
       let dummy_var = MayBeEqual.dummy_var lval_t in
 
-      if M.tracing then M.trace "c2po-assign" "assigning: var: %s; expr: %s + %s. \nTo_cil: lval: %a; expr: %a\n" (T.show lterm) (T.show rterm) (Z.to_string roffset) d_exp (T.to_cil lterm) d_exp (T.to_cil rterm);
+      if M.tracing then M.trace "c2po-assign" "assigning: var: %a; expr: %a + %a. \nTo_cil: lval: %a; expr: %a\n" T.pretty lterm T.pretty rterm GobZ.pretty roffset d_exp (T.to_cil lterm) d_exp (T.to_cil rterm);
 
       let equal_dummy_rterm = [Equal (dummy_var, rterm, roffset)] in
       let equal_dummy_lterm = [Equal (lterm, dummy_var, Z.zero)] in
@@ -138,7 +138,7 @@ struct
       let cc = assign_lval d ask lval (T.of_cil ask expr) in
       let cc = reset_normal_form cc in
       let res = `Lifted cc in
-      if M.tracing then M.trace "c2po-assign" "assign: var: %a; expr: %a; result: %s.\n" d_lval lval d_plainexp expr (D.show res);
+      if M.tracing then M.trace "c2po-assign" "assign: var: %a; expr: %a; result: %a." d_lval lval d_plainexp expr D.pretty res;
       res
 
   let branch ctx e pos =
@@ -158,7 +158,7 @@ struct
           with Unsat ->
             `Bot
     in
-    if M.tracing then M.trace "c2po" "branch:\n Actual equality: %a; pos: %b; valid_prop_list: %s; is_bot: %b\n" d_exp e pos (show_conj valid_props) (D.is_bot res);
+    if M.tracing then M.trace "c2po" "branch:\n Actual equality: %a; pos: %b; valid_prop_list: %a; is_bot: %b" d_exp e pos pretty_conj valid_props (D.is_bot res);
     if D.is_bot res then raise Deadcode;
     res
 
@@ -188,7 +188,7 @@ struct
         end
       | None -> ctx.local
     in
-    if M.tracing then M.trace "c2po-function" "return: exp_opt: %a; state: %s; result: %s\n" d_exp (BatOption.default (MayBeEqual.dummy_lval_print (TVoid [])) exp_opt) (D.show ctx.local) (D.show res);
+    if M.tracing then M.trace "c2po-function" "return: exp_opt: %a; state: %a; result: %a" d_exp (BatOption.default (MayBeEqual.dummy_lval_print (TVoid [])) exp_opt) D.pretty ctx.local D.pretty res;
     res
 
   (** var_opt is the variable we assign to. It has type lval. v=malloc.*)
@@ -249,7 +249,7 @@ struct
       if M.tracing then begin
         let dummy_lval = Var (Var.dummy_varinfo (TVoid [])), NoOffset in
         let lval = BatOption.default dummy_lval var_opt in
-        M.trace "c2po-function" "enter1: var_opt: %a; state: %s; state_with_ghosts: %s\n" d_lval lval (D.show ctx.local) (C2PODomain.show state_with_ghosts);
+        M.trace "c2po-function" "enter1: var_opt: %a; state: %a; state_with_ghosts: %a" d_lval lval D.pretty ctx.local C2PODomain.pretty state_with_ghosts;
       end;
       (* remove callee vars that are not reachable and not global *)
       let reachable_variables =
@@ -258,7 +258,7 @@ struct
       in
       let new_state = D.remove_terms_not_containing_variables reachable_variables state_with_ghosts.data in
       let new_state = data_to_t new_state in
-      if M.tracing then M.trace "c2po-function" "enter2: result: %s\n" (C2PODomain.show new_state);
+      if M.tracing then M.trace "c2po-function" "enter2: result: %a" C2PODomain.pretty new_state;
       let new_state = reset_normal_form new_state in
       [ctx.local, `Lifted new_state]
 
@@ -282,7 +282,7 @@ struct
       in
       let state_with_assignments = List.fold_left assign_term d arg_assigns in
 
-      if M.tracing then M.trace "c2po-function" "combine_env0: state_with_assignments: %s\n" (C2PODomain.show state_with_assignments);
+      if M.tracing then M.trace "c2po-function" "combine_env0: state_with_assignments: %a" C2PODomain.pretty state_with_assignments;
 
       (*remove all variables that were tainted by the function*)
       let tainted = f_ask.f (MayBeTainted) in
@@ -298,7 +298,7 @@ struct
         if M.tracing then begin
           let dummy_lval = Var (Var.dummy_varinfo (TVoid[])), NoOffset in
           let lval = BatOption.default dummy_lval lval_opt in
-          M.trace "c2po-function" "combine_env2: var_opt: %a; local_state: %s; f_state: %s; meeting everything: %s\n" d_lval lval (D.show ctx.local) (D.show f_d) (C2PODomain.show d)
+          M.trace "c2po-function" "combine_env2: var_opt: %a; local_state: %a; f_state: %a; meeting everything: %a" d_lval lval D.pretty ctx.local D.pretty f_d C2PODomain.pretty d
         end;
         `Lifted d
 
@@ -327,10 +327,10 @@ struct
             let return_var = (Some return_var, Some Z.zero) in
             assign_lval d f_ask lval return_var
         in
-        if M.tracing then M.trace "c2po-function" "combine_assign1: assigning return value: %s\n" (C2PODomain.show d);
+        if M.tracing then M.trace "c2po-function" "combine_assign1: assigning return value: %a" C2PODomain.pretty d;
         let d = remove_out_of_scope_vars d.data f in
         let d = data_to_t d in
-        if M.tracing then M.trace "c2po-function" "combine_assign2: result: %s\n" (C2PODomain.show d);
+        if M.tracing then M.trace "c2po-function" "combine_assign2: result: %a" C2PODomain.pretty d;
         `Lifted d
 
   let startstate v =

src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml

@@ -51,8 +51,8 @@ module ArrayMatrix: ArrayMatrixFunctor =
 
     type t = A.t array array [@@deriving eq, ord, hash]
 
-    let show x =
-      Array.fold_left (^) "" (Array.map (fun v -> V.show @@ V.of_array v) x)
+    let pretty =
+      GoblintCil.Pretty.(docArray ~sep:nil (fun _ x -> V.pretty () (V.of_array x))) (* TODO: avoid of_array *)
 
     let empty () =
       Array.make_matrix 0 0 A.zero

src/cdomains/affineEquality/arrayImplementation/arrayVector.ml

@@ -47,14 +47,8 @@ module ArrayVector: ArrayVectorFunctor =
     include Array
     type t = A.t array [@@deriving eq, ord, hash]
 
-    let show t =
-      let t = Array.to_list t in
-      let rec list_str l =
-        match l with
-        | [] -> "]"
-        | x :: xs -> (A.to_string x) ^" "^(list_str xs)
-      in
-      "["^list_str t^"\n"
+    let pretty () t =
+      GoblintCil.Pretty.(dprintf "[%a]" (docArray ~sep:(text " ") (fun _ x -> text (A.to_string x))) t)
 
     let keep_vals v n =
       if n >= Array.length v then v else

src/cdomains/affineEquality/matrix.ml

@@ -5,7 +5,7 @@ sig
   type vec
   type t [@@deriving eq, ord, hash]
 
-  val show: t -> string
+  val pretty: unit -> t -> GoblintCil.Pretty.doc
 
   val copy: t -> t
 

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

@@ -42,8 +42,8 @@ module ListMatrix: SparseMatrixFunctor =
     type t = V.t list (* List of rows *)
     [@@deriving eq, ord, hash]
 
-    let show x =
-      List.fold_left (^) "" (List.map (fun x -> (V.show x)) x)
+    let pretty =
+      GoblintCil.Pretty.(docList ~sep:nil (V.pretty ()))
 
     let copy m = m
 
@@ -328,7 +328,7 @@ module ListMatrix: SparseMatrixFunctor =
               let normalized_v = V.map_f_preserves_zero (fun x -> x /: value) v_after_elim in
               Some (insert_v_according_to_piv m normalized_v idx pivot_positions)
       in
-      if M.tracing then M.trace "rref_vec" "rref_vec: m:\n%s, v: %s => res:\n%s" (show m) (V.show v) (match res with None -> "None" | Some r -> show r);
+      if M.tracing then M.trace "rref_vec" "rref_vec: m:\n%a, v: %a => res:\n%a" pretty m V.pretty v (GoblintCil.Pretty.docOpt (pretty ())) res;
       res
 
     let rref_vec m v = timing_wrap "rref_vec" (rref_vec m) v
@@ -422,7 +422,7 @@ module ListMatrix: SparseMatrixFunctor =
         let res = map2i (fun i x y -> if i < r then
                             V.map2_f_preserves_zero (fun u j -> u +: y *: j) x a_r
                           else x) a col_b in
-        if M.tracing then M.trace "linear_disjunct_cases" "case_two: \na:\n%s, r:%d,\n col_b: %s, a_r: %s, => res:\n%s" (show a) r (V.show col_b) (V.show a_r) (show res);
+        if M.tracing then M.trace "linear_disjunct_cases" "case_two: \na:\n%a, r:%d,\n col_b: %a, a_r: %a, => res:\n%a" pretty a r V.pretty col_b V.pretty a_r pretty res;
         res
       in
 
@@ -445,14 +445,14 @@ module ListMatrix: SparseMatrixFunctor =
             | [], [] -> (acclist,acc)
           in
           let resl,rest = sub_and_last_aux ([],None) c1 c2 in
-          if M.tracing then M.trace "linear_disjunct_cases" "sub_and_last: ridx: %d c1: %s, c2: %s, resultlist: %s, result_pivot: %s" ridx (V.show col1) (V.show col2) (String.concat "," (List.map (fun (i,v) -> Printf.sprintf "(%d,%s)" i (A.to_string v)) resl)) (match rest with None -> "None" | Some (i,v1,v2) -> Printf.sprintf "(%d,%s,%s)" i (A.to_string v1) (A.to_string v2));
+          if M.tracing then M.trace "linear_disjunct_cases" "sub_and_last: ridx: %d c1: %a, c2: %a, resultlist: %s, result_pivot: %s" ridx V.pretty col1 V.pretty col2 (String.concat "," (List.map (fun (i,v) -> Printf.sprintf "(%d,%s)" i (A.to_string v)) resl)) (match rest with None -> "None" | Some (i,v1,v2) -> Printf.sprintf "(%d,%s,%s)" i (A.to_string v1) (A.to_string v2)); (* TODO: avoid eager arguments *)
           V.of_sparse_list len (List.rev resl), rest
         in
         let coldiff,lastdiff = sub_and_lastterm col1 col2 in
         match lastdiff with
         | None ->
           let sameinboth=get_col_upper_triangular m1 cidx in
-          if M.tracing then M.trace "linear_disjunct_cases" "case_three: no difference found, cidx: %d, ridx: %d, coldiff: %s, sameinboth: %s" cidx ridx (V.show coldiff) (V.show sameinboth);
+          if M.tracing then M.trace "linear_disjunct_cases" "case_three: no difference found, cidx: %d, ridx: %d, coldiff: %a, sameinboth: %a" cidx ridx V.pretty coldiff V.pretty sameinboth;
           (del_col m1 cidx,  del_col m2 cidx, push_col result cidx sameinboth, ridx) (* No difference found -> (del_col m1 cidx, del_col m2 cidx, push hd to result, ridx)*)
         | Some (idx,x,y) ->
           let r1 = safe_get_row m1 idx in
@@ -469,14 +469,14 @@ module ListMatrix: SparseMatrixFunctor =
           let transformed_a = multiply_by_t (-) m1 r1 in
           let alpha = get_col_upper_triangular transformed_a cidx in
           let res = push_col transformed_res cidx alpha in
-          if M.tracing then M.trace "linear_disjunct_cases" "case_three: found difference at ridx: %d idx: %d, x: %s, y: %s, diff: %s, m1: \n%s, m2:\n%s, res:\n%s"
-              ridx idx (A.to_string x) (A.to_string y) (A.to_string diff) (show m1) (show m2) (show @@ rev_matrix res);
+          if M.tracing then M.trace "linear_disjunct_cases" "case_three: found difference at ridx: %d idx: %d, x: %s, y: %s, diff: %s, m1: \n%a, m2:\n%a, res:\n%a"
+              ridx idx (A.to_string x) (A.to_string y) (A.to_string diff) pretty m1 pretty m2 pretty (rev_matrix res); (* TODO: avoid eager A.to_string, rev_matrix *)
           safe_remove_row (transformed_a) idx, safe_remove_row (multiply_by_t (-) m2 r2) idx, safe_remove_row (res) idx, ridx - 1
       in
 
       let rec lindisjunc_aux currentrowindex currentcolindex m1 m2 result =
-        if M.tracing then M.trace "linear_disjunct" "result so far: \n%s, currentrowindex: %d, currentcolindex: %d, m1: \n%s, m2:\n%s "
-            (show @@ rev_matrix result) currentrowindex currentcolindex  (show m1) (show m2);
+        if M.tracing then M.trace "linear_disjunct" "result so far: \n%a, currentrowindex: %d, currentcolindex: %d, m1: \n%a, m2:\n%a"
+            pretty (rev_matrix result) currentrowindex currentcolindex pretty m1 pretty m2; (* TODO: avoid eager rev_matrix *)
         if currentcolindex >= maxcols then result
         else
           let col1, rc1 = col_and_rc m1 currentcolindex currentrowindex in
@@ -487,25 +487,25 @@ module ListMatrix: SparseMatrixFunctor =
                       (del_col m1 currentrowindex) (del_col m2 currentrowindex)
                       (List.mapi (fun idx row -> if idx = currentrowindex then V.push_first row currentcolindex A.one else row) result)
           | 1, 0 -> let beta = get_col_upper_triangular m2 currentcolindex in
-            if M.tracing then M.trace "linear_disjunct_cases" "case 1,0: currentrowindex: %d, currentcolindex: %d, m1: \n%s, m2:\n%s , beta %s" currentrowindex currentcolindex (show m1) (show m2) (V.show beta);
+            if M.tracing then M.trace "linear_disjunct_cases" "case 1,0: currentrowindex: %d, currentcolindex: %d, m1: \n%a, m2:\n%a , beta %a" currentrowindex currentcolindex pretty m1 pretty m2 V.pretty beta;
             lindisjunc_aux
               (currentrowindex) (currentcolindex+1)
               (safe_remove_row (case_two m1 currentrowindex col2) currentrowindex) (safe_remove_row m2 currentrowindex)
               (safe_remove_row (push_col result currentcolindex beta) currentrowindex)
           | 0, 1 -> let beta = get_col_upper_triangular m1 currentcolindex in
-            if M.tracing then M.trace "linear_disjunct_cases" "case 0,1: currentrowindex: %d, currentcolindex: %d, m1: \n%s, m2:\n%s , beta %s" currentrowindex currentcolindex (show m1) (show m2) (V.show beta);
+            if M.tracing then M.trace "linear_disjunct_cases" "case 0,1: currentrowindex: %d, currentcolindex: %d, m1: \n%a, m2:\n%a , beta %a" currentrowindex currentcolindex pretty m1 pretty m2 V.pretty beta;
             lindisjunc_aux
               (currentrowindex) (currentcolindex+1)
               (safe_remove_row m1 currentrowindex) (safe_remove_row (case_two m2 currentrowindex col1) currentrowindex)
               (safe_remove_row (push_col result currentcolindex beta) currentrowindex)
           | 0, 0 -> let m1 , m2, result, currentrowindex = case_three col1 col2 m1 m2 result currentrowindex currentcolindex in
             lindisjunc_aux currentrowindex (currentcolindex+1) m1 m2 result  (* we need to process m1, m2 and result *)
-          | a,b -> failwith ("matrix not in rref m1: " ^ (string_of_int a) ^ (string_of_int b)^(show m1) ^ " m2: " ^ (show m2))
+          | a,b -> failwith (GobPretty.sprintf "matrix not in rref m1: %d%d%a m2: %a" a b pretty m1 pretty m2)
       in
       (* create a totally empty intial result, with dimensions rows x cols *)
       let pseudoempty = BatList.make (max (num_rows m1) (num_rows m1)) (V.zero_vec (num_cols m1)) in
       let res = rev_matrix @@ lindisjunc_aux 0 0 m1 m2 pseudoempty in
-      if M.tracing then M.tracel "linear_disjunct" "linear_disjunct between \n%s and \n%s =>\n%s" (show m1)  (show m2) (show res);
+      if M.tracing then M.tracel "linear_disjunct" "linear_disjunct between \n%a and \n%a =>\n%a" pretty m1 pretty m2 pretty res;
       res
 
   end

src/cdomains/affineEquality/sparseImplementation/sparseVector.ml

@@ -91,17 +91,19 @@ module SparseVector: SparseVectorFunctor =
     let to_sparse_list v =
       v.entries
 
-    let show v =
-      let rec sparse_list_str i l =
-        if i >= v.len then "]"
+    let pretty () v =
+      let open GoblintCil.Pretty in
+      let pretty_a () a = text (A.to_string a) in
+      let rec sparse_list_str i () l: doc =
+        if i >= v.len then nil
         else
           match l with
-          | [] -> (A.to_string A.zero) ^" "^ (sparse_list_str (i + 1) l)
+          | [] -> dprintf "%a %a" pretty_a A.zero (sparse_list_str (i + 1)) l
           | (idx, value) :: xs ->
-            if i = idx then (A.to_string value) ^" "^ sparse_list_str (i + 1) xs
-            else (A.to_string A.zero) ^" "^ sparse_list_str (i + 1) l
+            if i = idx then dprintf "%a %a" pretty_a value (sparse_list_str (i + 1)) xs
+            else dprintf "%a %a" pretty_a A.zero (sparse_list_str (i + 1)) l
       in
-      "["^(sparse_list_str 0 v.entries)^"\n"
+      dprintf "[%a]" (sparse_list_str 0) v.entries
 
     let length v =
       v.len

src/cdomains/affineEquality/vector.ml

@@ -4,7 +4,7 @@ sig
   type num
   type t [@@deriving eq, ord, hash]
 
-  val show: t -> string
+  val pretty: unit -> t -> GoblintCil.Pretty.doc
 
   val copy: t -> t
 

src/cdomains/apron/affineEqualityDenseDomain.apron.ml

@@ -253,7 +253,7 @@ struct
 
   let meet t1 t2 =
     let res = meet t1 t2 in
-    if M.tracing then M.tracel "meet" "meet a: %s b: %s -> %s " (show t1) (show t2) (show res) ;
+    if M.tracing then M.tracel "meet" "meet a: %a b: %a -> %a " pretty t1 pretty t2 pretty res;
     res
 
   let meet t1 t2 = timing_wrap "meet" (meet t1) t2
@@ -279,7 +279,7 @@ struct
 
   let leq t1 t2 =
     let res = leq t1 t2 in
-    if M.tracing then M.tracel "leq" "leq a: %s b: %s -> %b " (show t1) (show t2) res ;
+    if M.tracing then M.tracel "leq" "leq a: %a b: %a -> %b" pretty t1 pretty t2 res;
     res
 
   let join a b =
@@ -348,7 +348,7 @@ struct
 
   let join a b =
     let res = join a b in
-    if M.tracing then M.tracel "join" "join a: %s b: %s -> %s " (show a) (show b) (show res) ;
+    if M.tracing then M.tracel "join" "join a: %a b: %a -> %a" pretty a pretty b pretty res;
     res
 
   let widen a b =
@@ -381,7 +381,7 @@ struct
 
   let forget_vars t vars =
     let res = forget_vars t vars in
-    if M.tracing then M.tracel "ops" "forget_vars %s -> %s" (show t) (show res);
+    if M.tracing then M.tracel "ops" "forget_vars %a -> %a" pretty t pretty res;
     res
 
   let forget_vars t vars = timing_wrap "forget_vars" (forget_vars t) vars
@@ -443,7 +443,7 @@ struct
 
   let assign_var t v v' =
     let res = assign_var t v v' in
-    if M.tracing then M.tracel "ops" "assign_var t:\n %s \n v: %a \n v': %a\n -> %s" (show t) Var.pretty v Var.pretty v' (show res);
+    if M.tracing then M.tracel "ops" "assign_var t:\n %a \n v: %a \n v': %a\n -> %a" pretty t Var.pretty v Var.pretty v' pretty res;
     res
 
   let assign_var_parallel t vv's =                                (* vv's is a list of pairs of lhs-variables and their rhs-values *)
@@ -484,7 +484,7 @@ struct
 
   let assign_var_parallel t vv's =
     let res = assign_var_parallel t vv's in
-    if M.tracing then M.tracel "ops" "assign_var parallel: %s -> %s " (show t) (show res);
+    if M.tracing then M.tracel "ops" "assign_var parallel: %a -> %a" pretty t pretty res;
     res
 
   let assign_var_parallel t vv's = timing_wrap "var_parallel" (assign_var_parallel t) vv's
@@ -514,7 +514,7 @@ struct
 
   let substitute_exp ask t var exp no_ov =
     let res = substitute_exp ask t var exp no_ov in
-    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pretty var d_exp exp (show res);
+    if M.tracing then M.tracel "ops" "Substitute_expr t: \n %a \n var: %a \n exp: %a \n -> \n %a" pretty t Var.pretty var d_exp exp pretty res;
     res
 
   let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov
@@ -569,7 +569,7 @@ struct
 
   let unify a b =
     let res = unify a b  in
-    if M.tracing then M.tracel "ops" "unify: %s %s -> %s" (show a) (show b) (show res);
+    if M.tracing then M.tracel "ops" "unify: %a %a -> %a" pretty a pretty b pretty res;
     res
 
   let assert_constraint ask d e negate no_ov =