diff --git a/src/analyses/c2poAnalysis.ml b/src/analyses/c2poAnalysis.ml
index 17d7453c82..2c5a27ce66 100644
--- a/src/analyses/c2poAnalysis.ml
+++ b/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 =
diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml b/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml
index 30b2a4ba48..03d34f02c7 100644
--- a/src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml
+++ b/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
diff --git a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml b/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml
index 59d75a0bfe..da05ca5661 100644
--- a/src/cdomains/affineEquality/arrayImplementation/arrayVector.ml
+++ b/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
diff --git a/src/cdomains/affineEquality/matrix.ml b/src/cdomains/affineEquality/matrix.ml
index 5460c2a230..7847e8e7b3 100644
--- a/src/cdomains/affineEquality/matrix.ml
+++ b/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
diff --git a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml b/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
index 3cf017f163..19e215794b 100644
--- a/src/cdomains/affineEquality/sparseImplementation/listMatrix.ml
+++ b/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
diff --git a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml b/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
index 71d4a27016..c8c78ab0d3 100644
--- a/src/cdomains/affineEquality/sparseImplementation/sparseVector.ml
+++ b/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
diff --git a/src/cdomains/affineEquality/vector.ml b/src/cdomains/affineEquality/vector.ml
index 32e78f8b5b..4206820ef6 100644
--- a/src/cdomains/affineEquality/vector.ml
+++ b/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
diff --git a/src/cdomains/apron/affineEqualityDenseDomain.apron.ml b/src/cdomains/apron/affineEqualityDenseDomain.apron.ml
index 055ff731a4..5fc398146e 100644
--- a/src/cdomains/apron/affineEqualityDenseDomain.apron.ml
+++ b/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 =
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 06e131bbec..32f9a3ac35 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.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 =
@@ -302,7 +302,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 =
@@ -331,7 +331,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
@@ -397,7 +397,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 *)
@@ -435,7 +435,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
@@ -465,7 +465,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
@@ -520,7 +520,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 =
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index e5c89d0e80..931bb88c45 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -22,18 +22,19 @@ module Rhs = struct
(None , offset, divisor ) *)
type t = ((GobZ.t * int) option * GobZ.t * GobZ.t) [@@deriving eq, ord, hash]
let var_zero i = (Some (Z.one,i), Z.zero, Z.one)
- let show_coeff c =
- if Z.equal c Z.one then ""
- else if Z.equal c Z.minus_one then "-"
- else (Z.to_string c) ^"·"
- let show_rhs_formatted formatter = let ztostring n = (if Z.(geq n zero) then "+" else "") ^ Z.to_string n in
+ let pretty_coeff () c =
+ if Z.equal c Z.one then Pretty.nil
+ else if Z.equal c Z.minus_one then Pretty.text "-"
+ else Pretty.dprintf "%a·" GobZ.pretty c
+ let pretty_rhs_formatted formatter () =
+ let zpretty () n = Pretty.dprintf "%s%a" (if Z.(geq n zero) then "+" else "") GobZ.pretty n in
function
- | (Some (coeff,v), o,_) when Z.equal o Z.zero -> Printf.sprintf "%s%s" (show_coeff coeff) (formatter v)
- | (Some (coeff,v), o,_) -> Printf.sprintf "%s%s %s" (show_coeff coeff) (formatter v) (ztostring o)
- | (None, o,_) -> Printf.sprintf "%s" (Z.to_string o)
- let show (v,o,d) =
- let rhs=show_rhs_formatted (Printf.sprintf "var_%d") (v,o,d) in
- if not (Z.equal d Z.one) then "(" ^ rhs ^ ")/" ^ (Z.to_string d) else rhs
+ | (Some (coeff,v), o,_) when Z.equal o Z.zero -> Pretty.dprintf "%a%a" pretty_coeff coeff formatter v
+ | (Some (coeff,v), o,_) -> Pretty.dprintf "%a%a %a" pretty_coeff coeff formatter v zpretty o
+ | (None, o,_) -> GobZ.pretty () o
+ let pretty () (v,o,d) =
+ let rhs () = pretty_rhs_formatted (fun () -> Pretty.dprintf "var_%d") () (v,o,d) in
+ if not (Z.equal d Z.one) then Pretty.dprintf "(%t)/%a" rhs GobZ.pretty d else rhs ()
(** factor out gcd from all terms, i.e. ax=by+c with a positive is the canonical form for adx+bdy+cd *)
let canonicalize (v,o,d) =
@@ -55,13 +56,12 @@ module EqualitiesConjunction = struct
type t = int * ( Rhs.t IntMap.t ) [@@deriving eq, ord]
- let show_formatted formatter econ =
- if IntMap.is_empty econ then "{}"
+ let pretty_formatted formatter () econ =
+ if IntMap.is_empty econ then Pretty.text "{}"
else
- let str = IntMap.fold (fun i (refmonom,off,divi) acc -> Printf.sprintf "%s%s=%s ∧ %s" (Rhs.show_coeff divi) (formatter i) (Rhs.show_rhs_formatted formatter (refmonom,off,divi)) acc) econ "" in
- "{" ^ String.sub str 0 (String.length str - 4) ^ "}"
+ Pretty.dprintf "{%a}" (Pretty.d_list " ∧ " (fun () (i, (refmonom,off,divi)) -> Pretty.dprintf "%a%a=%a" Rhs.pretty_coeff divi formatter i (Rhs.pretty_rhs_formatted formatter) (refmonom,off,divi))) (IntMap.bindings econ)
- let show econ = show_formatted (Printf.sprintf "var_%d") econ
+ let pretty = pretty_formatted (fun () -> Pretty.dprintf "var_%d")
let hash (dim,x) = dim + 13* IntMap.fold (fun k value acc -> 13 * 13 * acc + 31 * k + Rhs.hash value) x 0 (* TODO: derive *)
@@ -124,11 +124,11 @@ module EqualitiesConjunction = struct
(op dim (Array.length indexes), a)
let modify_variables_in_domain m cols op = let res = modify_variables_in_domain m cols op in if M.tracing then
- M.tracel "modify_dims" "dimarray bumping with (fun x -> x + %d) at positions [%s] in { %s } -> { %s }"
+ M.tracel "modify_dims" "dimarray bumping with (fun x -> x + %d) at positions [%s] in { %a } -> { %a }"
(op 0 1)
(Array.fold_right (fun i str -> (string_of_int i) ^ ", " ^ str) cols "")
- (show (snd m))
- (show (snd res));
+ pretty (snd m)
+ pretty (snd res);
res
(** required by AbstractRelationalDomainRepresentation, true if dimension is zero *)
@@ -166,7 +166,7 @@ module EqualitiesConjunction = struct
| [] -> d) (* empty cluster means no work for us *)
| _ -> d) (* variable is either a constant or expressed by another refvar *) in
let res = (fst res, IntMap.remove var (snd res)) in (* set d(var) to unknown, finally *)
- if M.tracing then M.tracel "forget" "forget var_%d in { %s } -> { %s }" var (show (snd d)) (show (snd res));
+ if M.tracing then M.tracel "forget" "forget var_%d in { %a } -> { %a }" var pretty (snd d) pretty (snd res);
res
let dim_add (ch: Apron.Dim.change) m =
@@ -184,10 +184,10 @@ module EqualitiesConjunction = struct
let dim_remove ch m = Timing.wrap "dim remove" (fun m -> dim_remove ch m) m
let dim_remove ch m = let res = dim_remove ch m in if M.tracing then
- M.tracel "dim_remove" "dim remove at positions [%s] in { %s } -> { %s }"
+ M.tracel "dim_remove" "dim remove at positions [%s] in { %a } -> { %a }"
(Array.fold_right (fun i str -> (string_of_int i) ^ ", " ^ str) ch.dim "")
- (show (snd m))
- (show (snd res));
+ pretty (snd m)
+ pretty (snd res);
res
exception Contradiction
@@ -238,7 +238,7 @@ module EqualitiesConjunction = struct
let (_,newh1)= inverse i (coeff1,h1,o1,divi1) in
let newh1 = Rhs.subst normalizedj j (Rhs.subst (Some(coeff,j),offs,divi) i newh1) in
subst_var ts h1 newh1)) in
- if M.tracing then M.tracel "meet_with_one_conj" "meet_with_one_conj conj: %s eq: var_%d=%s -> %s " (show (snd ts)) i (Rhs.show (var,offs,divi)) (show (snd res))
+ if M.tracing then M.tracel "meet_with_one_conj" "meet_with_one_conj conj: %a eq: var_%d=%a -> %a" pretty (snd ts) i Rhs.pretty (var,offs,divi) pretty (snd res)
; res
(** affine transform variable i allover conj with transformer (Some (coeff,i)+offs)/divi *)
@@ -328,7 +328,7 @@ struct
let simplified_monomials_from_texp (t: t) texp =
let res = simplified_monomials_from_texp t texp in
- if M.tracing then M.tracel "from_texp" "%s %a -> %s" (EConj.show @@ snd @@ BatOption.get t.d) Texpr1.Expr.pretty texp
+ if M.tracing then M.tracel "from_texp" "%a %a -> %s" EConj.pretty (snd @@ BatOption.get t.d) Texpr1.Expr.pretty texp
(BatOption.map_default (fun (l,(o,d)) -> List.fold_right (fun (a,x,b) acc -> Printf.sprintf "%s*var_%d/%s + %s" (Z.to_string a) x (Z.to_string b) acc) l ((Z.to_string o)^"/"^(Z.to_string d))) "" res);
res
@@ -406,24 +406,29 @@ struct
else (subscr (i/10)) ^ transl.(i mod 10) in
subscr i
- let show_var env i =
- let res = Var.to_string (Environment.var_of_dim env i) in
+ let pretty_var env () i =
+ let res = Var.show (Environment.var_of_dim env i) in
match String.split_on_char '#' res with
- | varname::rest::[] -> varname ^ (try to_subscript @@ int_of_string rest with _ -> "#" ^ rest)
- | _ -> res
+ | varname::rest::[] -> Pretty.dprintf "%s%s" varname (try to_subscript @@ int_of_string rest with _ -> "#" ^ res)
+ | _ -> Pretty.text res
(** prints the current variable equalities with resolved variable names *)
- let show varM =
+ let pretty () varM =
match varM.d with
- | None -> "⊥\n"
- | Some arr when EConj.is_top_con arr -> "⊤\n"
+ | None -> Pretty.text "⊥"
+ | Some arr when EConj.is_top_con arr -> Pretty.text "⊤"
| Some arr ->
if is_bot varM then
- "Bot \n"
+ Pretty.text "Bot"
else
- EConj.show_formatted (show_var varM.env) (snd arr) ^ (to_subscript @@ fst arr)
-
- let pretty () (x:t) = text (show x)
+ Pretty.dprintf "%a%s" (EConj.pretty_formatted (pretty_var varM.env)) (snd arr) (to_subscript @@ fst arr)
+
+ include Printable.SimplePretty (
+ struct
+ type nonrec t = t
+ let pretty = pretty
+ end
+ )
let printXml f x = BatPrintf.fprintf f "\n\n\n" (XmlUtil.escape (show x)) Environment.printXml x.env
let eval_interval ask = Bounds.bound_texpr
@@ -439,7 +444,7 @@ struct
let meet_with_one_conj t i e =
let res = meet_with_one_conj t i e in
- if M.tracing then M.tracel "meet" "%s with single eq %s=%s -> %s" (show t) (Z.(to_string @@ Tuple3.third e)^ show_var t.env i) (Rhs.show_rhs_formatted (show_var t.env) e) (show res);
+ if M.tracing then M.tracel "meet" "%a with single eq %a%a=%a -> %a" pretty t GobZ.pretty (Tuple3.third e) (pretty_var t.env) i (Rhs.pretty_rhs_formatted (pretty_var t.env)) e pretty res;
res
let meet t1 t2 =
@@ -453,7 +458,7 @@ struct
let meet t1 t2 =
let res = meet t1 t2 in
- if M.tracing then M.tracel "meet" "meet a: %s\n U \n b: %s \n -> %s" (show t1) (show t2) (show res) ;
+ if M.tracing then M.tracel "meet" "meet a: %a\n U \n b: %a \n -> %a" pretty t1 pretty t2 pretty res;
res
let meet t1 t2 = Timing.wrap "meet" (meet t1) t2
@@ -479,7 +484,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 =
@@ -561,7 +566,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 =
@@ -569,14 +574,14 @@ struct
let widen a b =
let res = widen a b in
- if M.tracing then M.tracel "widen" "widen a: %s b: %s -> %s" (show a) (show b) (show res) ;
+ if M.tracing then M.tracel "widen" "widen a: %a b: %a -> %a" pretty a pretty b pretty res;
res
let narrow a b = meet a b
let narrow a b =
let res = narrow a b in
- if M.tracing then M.tracel "narrow" "narrow a: %s b: %s -> %s" (show a) (show b) (show res) ;
+ if M.tracing then M.tracel "narrow" "narrow a: %a b: %a -> %a" pretty a pretty b pretty res;
res
let pretty_diff () (x, y) =
@@ -596,7 +601,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
@@ -646,7 +651,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
(** Parallel assignment of variables.
@@ -667,7 +672,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
@@ -699,7 +704,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
@@ -764,7 +769,7 @@ struct
let unify a b =
let res = unify a b in
- if M.tracing then M.tracel "ops" "unify: %s\n U\n %s -> %s" (show a) (show b) (show res);
+ if M.tracing then M.tracel "ops" "unify: %a\n U\n %a -> %a" pretty a pretty b pretty res;
res
(** Assert a constraint expression. Defined in apronDomain.apron.ml
diff --git a/src/cdomains/c2poDomain.ml b/src/cdomains/c2poDomain.ml
index 741b9c0d94..c3fc6aaa5d 100644
--- a/src/cdomains/c2poDomain.ml
+++ b/src/cdomains/c2poDomain.ml
@@ -11,11 +11,11 @@ module C2PODomain = struct
type t = CongruenceClosure.t[@@deriving ord, hash]
- let show x = show_conj (get_conjunction x)
+ let pretty () x = pretty_conj () (get_conjunction x)
let name () = "c2po"
type domain = t
- include Printable.SimpleShow (struct type t = domain let show = show end)
+ include Printable.SimplePretty (struct type t = domain let pretty = pretty end)
let equal_standard x y =
let cc1 = x.data in
@@ -36,7 +36,7 @@ module C2PODomain = struct
&& equal_diseqs cc1 cc2
&& equal_bldis cc1 cc2
in
- if M.tracing then M.trace "c2po-equal" "equal eq classes. %b\nx=\n%s\ny=\n%s" res (show_all x) (show_all y);
+ if M.tracing then M.trace "c2po-equal" "equal eq classes. %b\nx=\n%a\ny=\n%a" res pretty_all x pretty_all y;
res
let equal_normal_form x y =
@@ -48,10 +48,10 @@ module C2PODomain = struct
else
let nf1 = get_normal_form x in
let nf2 = get_normal_form y in
- if M.tracing then M.trace "c2po-min-repr" "Normal form of x = %s; Normal form of y = %s" (show_conj nf1) (show_conj nf2);
+ if M.tracing then M.trace "c2po-min-repr" "Normal form of x = %a; Normal form of y = %a" pretty_conj nf1 pretty_conj nf2;
T.props_equal nf1 nf2
in
- if M.tracing then M.trace "c2po-equal" "equal min repr. %b\nx=\n%s\ny=\n%s" res (show_all x) (show_all y);
+ if M.tracing then M.trace "c2po-equal" "equal min repr. %b\nx=\n%a\ny=\n%a" res pretty_all x pretty_all y;
res
let equal a b =
@@ -85,8 +85,7 @@ module C2PODomain = struct
if exactly_equal cc1 cc2 then
cc1
else begin
- if M.tracing then M.tracel "c2po-join" "JOIN AUTOMATON. FIRST ELEMENT: %s\nSECOND ELEMENT: %s\n"
- (show_all x) (show_all y);
+ if M.tracing then M.tracel "c2po-join" "JOIN AUTOMATON. FIRST ELEMENT: %a\nSECOND ELEMENT: %a" pretty_all x pretty_all y;
let a = cc1 in
let b = cc2 in
let cc, _ = join_cc_function a b in
@@ -98,8 +97,7 @@ module C2PODomain = struct
end
in
let res = CongruenceClosure.data_to_t res in
- if M.tracing then M.tracel "c2po-join" "JOIN. JOIN: %s\n"
- (show_all res);
+ if M.tracing then M.tracel "c2po-join" "JOIN. JOIN: %a" pretty_all res;
res
let join (a: t) (b :t) =
@@ -138,7 +136,7 @@ module C2PODomain = struct
let meet x y =
let cc1 = x.data in
let cc2 = y.data in
- if M.tracing then M.trace "c2po-meet" "Meet x= %s; y=%s" (show x) (show y);
+ if M.tracing then M.trace "c2po-meet" "Meet x= %a; y=%a" pretty x pretty y;
let res =
if exactly_equal cc1 cc2 then
cc1
@@ -150,7 +148,7 @@ module C2PODomain = struct
meet_conjs_opt a_conj cc2
in
let res = data_to_t res in
- if M.tracing then M.trace "c2po-meet" "Meet result = %s" (show res);
+ if M.tracing then M.trace "c2po-meet" "Meet result = %a" pretty res;
res
let narrow x y =
@@ -172,7 +170,7 @@ module C2PODomain = struct
meet
in
let res = data_to_t res in
- if M.tracing then M.trace "c2po-meet" "NARROW RESULT = %s" (show res);
+ if M.tracing then M.trace "c2po-meet" "NARROW RESULT = %a" pretty res;
res
let leq x y =
@@ -189,7 +187,7 @@ module C2PODomain = struct
in
let x_diff = List.filter (not_in y_conj) x_conj in
let y_diff = List.filter (not_in x_conj) y_conj in
- Pretty.dprintf ("Additional propositions of first element:\n%s\nAdditional propositions of second element:\n%s\n") (show_conj x_diff) (show_conj y_diff)
+ Pretty.dprintf ("Additional propositions of first element:\n%a\nAdditional propositions of second element:\n%a\n") pretty_conj x_diff pretty_conj y_diff
end
@@ -197,11 +195,11 @@ end
module D = struct
include Lattice.LiftBot (C2PODomain)
- let show_all = function
+ let pretty_all () = function
| `Bot ->
- show `Bot
+ pretty () `Bot
| `Lifted x ->
- show_all x
+ pretty_all () x
let meet a b =
try
@@ -218,12 +216,12 @@ module D = struct
let printXml f x = match x with
| `Lifted x ->
BatPrintf.fprintf f "\n\n\n"
- (XmlUtil.escape (Format.asprintf "%s" (show (`Lifted x))))
- (XmlUtil.escape (Format.asprintf "%s" (TUF.show_uf x.data.uf)))
- (XmlUtil.escape (Format.asprintf "%s" (SSet.show_set x.data.set)))
- (XmlUtil.escape (Format.asprintf "%s" (LMap.show_map x.data.map)))
- (XmlUtil.escape (Format.asprintf "%s" (show_normal_form x.normal_form)))
- (XmlUtil.escape (Format.asprintf "%s" (Disequalities.show_neq x.data.diseq)))
+ (XmlUtil.escape (GobPretty.sprint pretty (`Lifted x)))
+ (XmlUtil.escape (GobPretty.sprint TUF.pretty_uf x.data.uf))
+ (XmlUtil.escape (GobPretty.sprint SSet.pretty_set x.data.set))
+ (XmlUtil.escape (GobPretty.sprint LMap.pretty_map x.data.map))
+ (XmlUtil.escape (GobPretty.sprint pretty_normal_form x.normal_form))
+ (XmlUtil.escape (GobPretty.sprint Disequalities.pretty_neq x.data.diseq))
| `Bot ->
BatPrintf.fprintf f "\nbottom\n\n"
@@ -253,7 +251,7 @@ module D = struct
It removes all terms which contain one of the "vars",
while maintaining all equalities about variables that are not being removed.*)
let remove_terms_containing_variables vars cc =
- if M.tracing then M.trace "c2po" "remove_terms_containing_variables: %s\n" (List.fold_left (fun s v -> s ^"; " ^Var.show v) "" vars);
+ if M.tracing then M.trace "c2po" "remove_terms_containing_variables: %a" (Pretty.d_list "; " Var.pretty) vars;
remove_terms (T.contains_variable vars) cc
(** Remove terms from the data structure.
@@ -261,7 +259,7 @@ module D = struct
except the global vars are also kept (when vglob = true),
while maintaining all equalities about variables that are not being removed.*)
let remove_terms_not_containing_variables vars cc =
- if M.tracing then M.trace "c2po" "remove_terms_not_containing_variables: %s\n" (List.fold_left (fun s v -> s ^"; " ^Var.show v) "" vars);
+ if M.tracing then M.trace "c2po" "remove_terms_not_containing_variables: %a" (Pretty.d_list "; " Var.pretty) vars;
let not_global_and_not_contains_variable t =
let var = T.get_var t in
not (DuplicateVars.VarType.vglob var) && not (T.contains_variable vars t)
@@ -271,7 +269,7 @@ module D = struct
(** Remove terms from the data structure.
It removes all terms that may be changed after an assignment to "term".*)
let remove_may_equal_terms ask size term cc =
- if M.tracing then M.trace "c2po" "remove_may_equal_terms: %s\n" (T.show term);
+ if M.tracing then M.trace "c2po" "remove_may_equal_terms: %a" T.pretty term;
let _, cc = insert cc term in
let may_equal_term =
MayBeEqual.may_be_equal ask cc size term
diff --git a/src/cdomains/congruenceClosure.ml b/src/cdomains/congruenceClosure.ml
index 7470684b68..46a17fa25c 100644
--- a/src/cdomains/congruenceClosure.ml
+++ b/src/cdomains/congruenceClosure.ml
@@ -352,21 +352,20 @@ module Disequalities = struct
*)
(** Produces a string for the number used as offset; helper function for show* functions below.*)
- let show_number r =
+ let pretty_number () r =
if Z.equal r Z.zero then
- ""
+ Pretty.nil
else if Z.leq r Z.zero then
- Z.to_string r
+ GobZ.pretty () r
else
- " + " ^ Z.to_string r
+ Pretty.dprintf " + %a" GobZ.pretty r
- let show_neq neq =
+ let pretty_neq () neq =
let clist = bindings neq in
- let do_neq =
- (fun s (v,r,v') ->
- s ^ "\t" ^ T.show v ^ show_number r ^ " != " ^ T.show v' ^ "\n")
+ let do_neq () (v,r,v') =
+ Pretty.dprintf "\t%a%a != %a\n" T.pretty v pretty_number r T.pretty v'
in
- List.fold_left do_neq "" clist
+ Pretty.docList ~sep:Pretty.nil (do_neq ()) () clist
let get_disequalities x =
let to_disequality (t1, z, t2) =
@@ -404,11 +403,11 @@ module SSet = struct
let find_opt = TSet.find_opt
let union = TSet.union
- let show_set set =
- let show_element v s =
- s ^ "\t" ^ T.show v ^ ";\n"
+ let pretty_set () set =
+ let pretty_element () v =
+ Pretty.dprintf "\t%a;\n" T.pretty v
in
- TSet.fold show_element set "" ^ "\n"
+ Pretty.docList ~sep:Pretty.nil (pretty_element ()) () (TSet.elements set)
(** Adds all subterms of t to the SSet and the LookupMap*)
let rec subterms_of_term (set,map) t =
@@ -495,12 +494,11 @@ module MRMap = struct
let mem = TMap.mem
let empty = TMap.empty
- let show_min_rep min_representatives =
- let show_one_rep s (state, (rep, z)) =
- s ^ "\tState: " ^ T.show state ^
- "\n\tMin: (" ^ T.show rep ^ ", " ^ Z.to_string z ^ ")--\n\n"
+ let pretty_min_rep () min_representatives =
+ let pretty_one_rep () (state, (rep, z)) =
+ Pretty.dprintf "\tState: %a\n\tMin: (%a, %a)--\n\n" T.pretty state T.pretty rep GobZ.pretty z
in
- List.fold_left show_one_rep "" (bindings min_representatives)
+ Pretty.docList ~sep:Pretty.nil (pretty_one_rep ()) () (bindings min_representatives)
let rec update_min_repr (uf, set, map) min_representatives = function
| [] -> min_representatives
@@ -607,14 +605,12 @@ let get_transitions (uf, map) =
in
List.concat_map do_bindings (LMap.bindings map)
-let show_conj list =
+let pretty_conj () list =
match list with
- | [] -> "top"
+ | [] -> Pretty.text "top"
| list ->
- let show_prop s d =
- s ^ "\t" ^ T.show_prop d ^ ";\n"
- in
- List.fold_left show_prop "" list
+ let pretty_prop () d = Pretty.dprintf "\t%a;\n" T.pretty_prop d in
+ Pretty.docList ~sep:Pretty.nil (pretty_prop ()) () list
type data = {
uf: TUF.t;
@@ -675,7 +671,7 @@ let get_normal_conjunction cc get_normal_repr =
| Equal (t1,t2,z) -> failwith "No equality expected."
| BlNequal (t1,t2) -> failwith "No block disequality expected."
in
- if M.tracing then M.trace "c2po-diseq" "DISEQUALITIES: %s;\nUnion find: %s\nMap: %s\n" (show_conj disequalities) (TUF.show_uf cc.uf) (LMap.show_map cc.map);
+ if M.tracing then M.trace "c2po-diseq" "DISEQUALITIES: %a;\nUnion find: %a\nMap: %a\n" pretty_conj disequalities TUF.pretty_uf cc.uf LMap.pretty_map cc.map;
let disequalities = List.map normalize_disequality disequalities in
(* block disequalities *)
let normalize_bldis t = match t with
@@ -753,11 +749,11 @@ let get_normal_form cc =
LazyNormalFormEval.force cc.normal_form
(** Converts the normal form to string, but only if it was already computed. *)
-let show_normal_form normal_form =
+let pretty_normal_form () normal_form =
if LazyNormalFormEval.is_val normal_form then
- show_conj (LazyNormalFormEval.force normal_form)
+ pretty_conj () (LazyNormalFormEval.force normal_form)
else
- "not computed"
+ Pretty.text "not computed"
let get_conjunction_from_data data =
@@ -778,21 +774,15 @@ let data_to_t (cc : data) : t =
{data = cc;
normal_form = LazyNormalFormEval.make cc}
-let show_all (x: t) =
- "Normal form:\n" ^
- show_conj((get_conjunction x)) ^
- "Union Find partition:\n" ^
- TUF.show_uf x.data.uf
- ^ "\nSubterm set:\n"
- ^ SSet.show_set x.data.set
- ^ "\nLookup map/transitions:\n"
- ^ LMap.show_map x.data.map
- ^ "\nNeq:\n"
- ^ Disequalities.show_neq x.data.diseq
- ^ "\nBlock diseqs:\n"
- ^ show_conj (BlDis.to_conj x.data.bldis)
- ^ "\nMin repr:\n"
- ^ show_normal_form x.normal_form
+let pretty_all () (x: t) =
+ Pretty.dprintf "Normal form:\n%a\nUnion Find partition:\n%a\nSubterm set:\n%a\nLookup map/transitions:\n%a\nNeq:\n%a\nBlock diseqs:\n%a\nMin repr:\n%a"
+ pretty_conj (get_conjunction x)
+ TUF.pretty_uf x.data.uf
+ SSet.pretty_set x.data.set
+ LMap.pretty_map x.data.map
+ Disequalities.pretty_neq x.data.diseq
+ pretty_conj (BlDis.to_conj x.data.bldis)
+ pretty_normal_form x.normal_form
(** Splits the conjunction into three groups: the first one contains all equality propositions,
the second one contains all inequality propositions
@@ -832,7 +822,7 @@ let congruence_neq cc neg' =
(* take explicit dis-equalities into account *)
let uf, neq_list = Disequalities.init_list_neq uf neg in
let neq = Disequalities.propagate_neq (uf, cmap, arg, neq) cc.bldis neq_list in
- if M.tracing then M.trace "c2po-neq" "congruence_neq: %s\nUnion find: %s\n" (Disequalities.show_neq neq) (TUF.show_uf uf);
+ if M.tracing then M.trace "c2po-neq" "congruence_neq: %a\nUnion find: %a\n" Disequalities.pretty_neq neq TUF.pretty_uf uf;
{cc with uf; diseq = neq}
(**
@@ -856,7 +846,7 @@ let rec closure (uf, map, new_repr) = function
let v2, r2, uf = TUF.find uf t2 in
let sizet1, sizet2 = T.get_size t1, T.get_size t2 in
if not (Z.equal sizet1 sizet2) then (
- if M.tracing then M.trace "c2po" "ignoring equality because the sizes are not the same: %s = %s + %s" (T.show t1) (Z.to_string r) (T.show t2);
+ if M.tracing then M.trace "c2po" "ignoring equality because the sizes are not the same: %a = %a + %a" T.pretty t1 GobZ.pretty r T.pretty t2;
closure (uf, map, new_repr) rest
)
else if T.equal v1 v2 then
@@ -1046,7 +1036,7 @@ let meet_pos_conjs cc pos_conjs =
let cc = insert_set cc subterms in
closure cc pos_conjs
in
- if M.tracing then M.trace "c2po-meet" "meet_pos_conjs result: %s\n" (show_conj (get_conjunction_from_data res));
+ if M.tracing then M.trace "c2po-meet" "meet_pos_conjs result: %a\n" pretty_conj (get_conjunction_from_data res); (* TODO: avoid eager computation in argument *)
res
(** Adds propositions to the data structure.
@@ -1342,7 +1332,7 @@ let join_neq diseq1 diseq2 cc1 cc2 cc cmap1 cmap2 =
let subterms, _ = SSet.subterms_of_conj diseq in
let cc = insert_set cc subterms in
let res = congruence_neq cc diseq in
- (if M.tracing then M.trace "c2po-neq" "join_neq: %s\n\n" (Disequalities.show_neq res.diseq));
+ (if M.tracing then M.trace "c2po-neq" "join_neq: %a" Disequalities.pretty_neq res.diseq);
res
(** Joins the block disequalities bldiseq1 and bldiseq2, given a congruence closure data structure.
@@ -1369,7 +1359,7 @@ let join_bldis bldiseq1 bldiseq2 cc1 cc2 cc cmap1 cmap2 =
let cc = insert_set cc subterms in
let diseqs_ref_terms = List.filter both_root bldiseq in
let bldis = List.fold_left BlDis.add_block_diseq BlDis.empty diseqs_ref_terms in
- (if M.tracing then M.trace "c2po-neq" "join_bldis: %s\n\n" (show_conj (BlDis.to_conj bldis)));
+ (if M.tracing then M.trace "c2po-neq" "join_bldis: %a" pretty_conj (BlDis.to_conj bldis));
{cc with bldis}
(** Check for equality of two congruence closures,
@@ -1516,8 +1506,8 @@ module MayBeEqual = struct
res
in
- if M.tracing then M.trace "c2po-query" "may-point-to %a -> equal terms: %s"
- d_exp exp (List.fold_left (fun s (t,z) -> s ^ "(" ^ T.show t ^","^ Z.to_string Z.(z + offset) ^")") "" equal_terms);
+ if M.tracing then M.trace "c2po-query" "may-point-to %a -> equal terms: %a"
+ d_exp exp (Pretty.docList ~sep:Pretty.nil (fun (t,z) -> Pretty.dprintf "(%a,%a)" T.pretty t GobZ.pretty Z.(z + offset))) equal_terms;
List.fold_left intersect_query_result (AD.top ()) equal_terms
@@ -1542,8 +1532,8 @@ module MayBeEqual = struct
with IntDomain.ArithmeticOnIntegerBot _ ->
AD.bot ()
in
- M.tracel "c2po-maypointto2" "QUERY MayPointTo. \nres: %a;\nt2: %s; exp2: %a; res: %a; \nmeet: %a; result: %s\n"
- AD.pretty mpt1 (T.show t2) d_plainexp exp2 AD.pretty mpt2 AD.pretty meet (string_of_bool res);
+ M.tracel "c2po-maypointto2" "QUERY MayPointTo. \nres: %a;\nt2: %a; exp2: %a; res: %a; \nmeet: %a; result: %B"
+ AD.pretty mpt1 T.pretty t2 d_plainexp exp2 AD.pretty mpt2 AD.pretty meet res;
end;
res
@@ -1555,8 +1545,8 @@ module MayBeEqual = struct
let exp1 = T.to_cil t1 in
let mpt1 = may_point_to_all_equal_terms ask exp1 cc t1 Z.zero in
let res = may_point_to_address ask mpt1 t2 off cc in
- if M.tracing && res then M.tracel "c2po-maypointto2" "QUERY MayPointTo. \nres: %a;\nt1: %s; exp1: %a;\n"
- AD.pretty mpt1 (T.show t1) d_plainexp exp1;
+ if M.tracing && res then M.tracel "c2po-maypointto2" "QUERY MayPointTo. \nres: %a;\nt1: %a; exp1: %a;"
+ AD.pretty mpt1 T.pretty t1 d_plainexp exp1;
res
(** Returns true if `t1` and `t2` may possibly be equal or may possibly overlap. *)
@@ -1597,7 +1587,7 @@ module MayBeEqual = struct
The parameter s is the size in bits of the variable t1 we are assigning to. *)
let may_be_equal ask cc size t1 t2 =
let res = may_be_equal ask cc size t1 t2 in
- if M.tracing then M.tracel "c2po-maypointto" "May be equal: %s %s: %b\n" (T.show t1) (T.show t2) res;
+ if M.tracing then M.tracel "c2po-maypointto" "May be equal: %a %a: %b" T.pretty t1 T.pretty t2 res;
res
(**Returns true if `t2` or any subterm of `t2` may possibly point to one of the addresses in `addresses`.*)
diff --git a/src/cdomains/duplicateVars.ml b/src/cdomains/duplicateVars.ml
index ef34fa7aa1..73c1a74d3e 100644
--- a/src/cdomains/duplicateVars.ml
+++ b/src/cdomains/duplicateVars.ml
@@ -71,6 +71,8 @@ module VarType = struct
| DuplicVar v ->
duplic_var_prefix ^ v.vname ^ duplic_var_postfix
+ let pretty () v = Pretty.text (show v)
+
let get_type v = match v with
| AssignAux t
| ReturnAux t -> t
diff --git a/src/cdomains/unionFind.ml b/src/cdomains/unionFind.ml
index d16cab5818..2c624ce0ad 100644
--- a/src/cdomains/unionFind.ml
+++ b/src/cdomains/unionFind.ml
@@ -83,7 +83,7 @@ module T = struct
| SizeOfError (msg, _) ->
raise (UnsupportedCilExpression msg)
- let show_type exp =
+ let pretty_type () exp =
try
let typ = typeOf exp in
let typ_abbreviation = match Cil.unrollType typ with
@@ -99,35 +99,38 @@ module T = struct
| TBuiltin_va_list _ -> "?"
in
let bit_size = get_size_in_bits typ in
- let bit_size = Z.to_string bit_size in
- "[" ^ typ_abbreviation ^ bit_size ^ "]"
+ Pretty.dprintf "[%s%a]" typ_abbreviation GobZ.pretty bit_size
with UnsupportedCilExpression _ ->
- "[?]"
+ Pretty.text "[?]"
- let rec show : t -> string = function
+ let rec pretty (): t -> Pretty.doc =
+ let open Pretty in
+ function
| Addr v ->
- "&" ^ Var.show v
+ dprintf "&%a" Var.pretty v
| Aux (v,exp) ->
- "~" ^ Var.show v ^ show_type exp
+ dprintf "~%a%a" Var.pretty v pretty_type exp
| Deref (Addr v, z, exp) when Z.equal z Z.zero ->
- Var.show v ^ show_type exp
+ dprintf "%a%a" Var.pretty v pretty_type exp
| Deref (t, z, exp) when Z.equal z Z.zero ->
- "*" ^ show t^ show_type exp
+ dprintf "*%a%a" pretty t pretty_type exp
| Deref (t, z, exp) ->
- "*(" ^ Z.to_string z ^ "+" ^ show t ^ ")"^ show_type exp
+ dprintf "*(%a+%a)%a" GobZ.pretty z pretty t pretty_type exp
- let show_prop = function
+ let pretty_prop (): v_prop -> Pretty.doc =
+ let open Pretty in
+ function
| Equal (t1,t2,r) when Z.equal r Z.zero ->
- show t1 ^ " = " ^ show t2
+ dprintf "%a = %a" pretty t1 pretty t2
| Equal (t1,t2,r) ->
- show t1 ^ " = " ^ Z.to_string r ^ "+" ^ show t2
+ dprintf "%a = %a+%a" pretty t1 GobZ.pretty r pretty t2
| Nequal (t1,t2,r) when Z.equal r Z.zero ->
- show t1 ^ " != " ^ show t2
+ dprintf "%a != %a" pretty t1 pretty t2
| Nequal (t1,t2,r) ->
- show t1 ^ " != " ^ Z.to_string r ^ "+" ^ show t2
+ dprintf "%a != %a+%a" pretty t1 GobZ.pretty r pretty t2
| BlNequal (t1,t2) ->
- "bl(" ^ show t1 ^ ") != bl(" ^ show t2 ^ ")"
+ dprintf "bl(%a) != bl(%a)" pretty t1 pretty t2
(** Returns true if the first parameter is a subterm of the second one. *)
let rec is_subterm needle haystack =
@@ -582,7 +585,7 @@ module T = struct
| exception (UnsupportedCilExpression s) ->
M.trace "c2po-cil-conversion" "unsupported exp: %a\n%s\n" d_plainlval lval s
| t ->
- M.trace "c2po-cil-conversion" "lval: %a --> %s\n" d_plainlval lval (show t));
+ M.trace "c2po-cil-conversion" "lval: %a --> %a\n" d_plainlval lval pretty t);
res
let rec of_cil_neg ask neg e = match e with
@@ -618,8 +621,8 @@ module T = struct
in
(if M.tracing && not neg then
match res with
- | None, Some z -> M.trace "c2po-cil-conversion" "constant exp: %a --> %s\n" d_plainexp e (Z.to_string z)
- | Some t, Some z -> M.trace "c2po-cil-conversion" "exp: %a --> %s + %s\n" d_plainexp e (show t) (Z.to_string z);
+ | None, Some z -> M.trace "c2po-cil-conversion" "constant exp: %a --> %a\n" d_plainexp e GobZ.pretty z
+ | Some t, Some z -> M.trace "c2po-cil-conversion" "exp: %a --> %a + %a\n" d_plainexp e pretty t GobZ.pretty z;
| _ -> ());
res
@@ -634,7 +637,7 @@ module T = struct
if check_valid_pointer exp then
Some t, Some z
else begin
- if M.tracing then M.trace "c2po-cil-conversion" "invalid exp: %a --> %s + %s\n" d_plainexp e (show t) (Z.to_string z);
+ if M.tracing then M.trace "c2po-cil-conversion" "invalid exp: %a --> %a + %a\n" d_plainexp e pretty t GobZ.pretty z;
None, None
end
| t, z -> t, z
@@ -926,27 +929,17 @@ module UnionFind = struct
BatList.group compare bindings
(** Throws "Unknown value" if the data structure is invalid. *)
- let show_uf uf =
- let show_element acc (v, (t, size)) =
- acc ^
- "\t" ^
- (if is_root uf v then "R: " else "") ^
- "(" ^
- T.show v ^
- "; P: " ^
- T.show (fst t) ^
- "; o: " ^
- Z.to_string (snd t) ^
- "; s: " ^
- string_of_int size ^
- ")\n"
- in
- let show_eq_class acc eq_class =
- acc ^
- List.fold_left show_element "" eq_class ^
- "----\n"
+ let pretty_uf () uf =
+ let pretty_element () (v, (t, size)) =
+ Pretty.dprintf "\t%s(%a; P:%a; o:%a; s: %d)\n"
+ (if is_root uf v then "R: " else "")
+ T.pretty v
+ T.pretty (fst t)
+ GobZ.pretty (snd t)
+ size
in
- List.fold_left show_eq_class "" (get_eq_classes uf) ^ "\n"
+ let pretty_eq_class () eq_class = Pretty.d_list "\n" pretty_element () eq_class in
+ Pretty.d_list "----\n" pretty_eq_class () (get_eq_classes uf)
(** Returns a list of representative elements.*)
let get_representatives uf =
@@ -1004,27 +997,19 @@ module LookupMap = struct
in
add v zmap map
- let show_map (map:t) =
- let show_inner_binding acc (r, v) =
- acc ^
- "\t" ^
- Z.to_string r ^
- ": " ^
- T.show v ^
- "; "
+ let pretty_map () (map:t) =
+ let pretty_inner_binding () (r, v) =
+ Pretty.dprintf "\t%a: %a; " GobZ.pretty r T.pretty v
in
- let show_inner_map zmap =
+ let pretty_inner_map () zmap =
let inner_bindings = zmap_bindings zmap in
- List.fold_left show_inner_binding "" inner_bindings
+ Pretty.docList ~sep:Pretty.nil (pretty_inner_binding ()) () inner_bindings
in
- let show_binding s (v, zmap) =
- s ^
- T.show v ^
- "\t:\n" ^
- show_inner_map zmap ^ "\n"
+ let pretty_binding () (v, zmap) =
+ Pretty.dprintf "%a\t:\n%a" T.pretty v pretty_inner_map zmap
in
let bindings = bindings map in
- List.fold_left show_binding "" bindings
+ Pretty.docList ~sep:Pretty.line (pretty_binding ()) () bindings
(** The value at v' is shifted by r and then added for v.
The old entry for v' is removed. *)