diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index ad99e26b58..cb8e8731d9 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -295,7 +295,7 @@ struct
(* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *)
(* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *)
(* Also, a local *)
- let vname = Apron.Var.to_string var in
+ let vname = GobApron.Var.show var in
let locals = fundec.sformals @ fundec.slocals in
match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
| None -> true
@@ -418,7 +418,7 @@ struct
in
let any_local_reachable = any_local_reachable fundec reachable_from_args in
let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
- if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (fun v -> Pretty.text (Apron.Var.to_string v))) arg_vars;
+ if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (GobApron.Var.pretty ())) arg_vars;
RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
let tainted = f_ask.f Queries.MayBeTainted in
let tainted_vars = TaintPartialContexts.conv_varset tainted in
diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml
index 75c12a0e63..5500ad8c3b 100644
--- a/src/cdomains/apron/affineEqualityDomain.apron.ml
+++ b/src/cdomains/apron/affineEqualityDomain.apron.ml
@@ -181,7 +181,7 @@ struct
else if Z.lt coeff Z.minus_one then Z.to_string coeff
else Format.asprintf "+%s" (Z.to_string coeff)
in
- coeff_str ^ Var.to_string var
+ coeff_str ^ Var.show var
in
let const_to_str vl =
if Z.equal vl Z.zero then
@@ -203,11 +203,10 @@ struct
| Some m when Matrix.is_empty m -> "⊤"
| Some m ->
let constraint_list = List.init (Matrix.num_rows m) (fun i -> vec_to_constraint (conv_to_ints @@ Matrix.get_row m i) t.env) in
- Format.asprintf "%s" ("[|"^ (String.concat "; " constraint_list) ^"|]")
+ "[|"^ (String.concat "; " constraint_list) ^"|]"
let pretty () (x:t) = text (show x)
- let printXml f x = BatPrintf.fprintf f "\n\n\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env)))
-
+ 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
let name () = "affeq"
@@ -430,8 +429,8 @@ struct
let assign_exp ask t var exp no_ov =
let res = assign_exp ask t var exp no_ov in
- if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %s \n exp: %a\n no_ov: %b -> \n %s"
- (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ;
+ if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %a \n exp: %a\n no_ov: %b -> \n %s"
+ (show t) Var.pretty var d_exp exp (Lazy.force no_ov) (show res);
res
let assign_var (t: VarManagement(Vc)(Mx).t) v v' =
@@ -441,7 +440,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: %s \n v': %s\n -> %s" (show t) (Var.to_string v) (Var.to_string v') (show res) ;
+ 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);
res
let assign_var_parallel t vv's =
@@ -499,7 +498,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: %s \n exp: %a \n -> \n %s" (show t) (Var.to_string var) d_exp exp (show res);
+ 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);
res
let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
index 9bf17b2f92..03ac3ed3f0 100644
--- a/src/cdomains/apron/apronDomain.apron.ml
+++ b/src/cdomains/apron/apronDomain.apron.ml
@@ -283,7 +283,7 @@ struct
let assign_exp_with ask nd v e no_ov =
match Convert.texpr1_of_cil_exp ask nd (A.env nd) e no_ov with
| texpr1 ->
- if M.tracing then M.trace "apron" "assign_exp converted: %s" (Format.asprintf "%a" Texpr1.print texpr1);
+ if M.tracing then M.trace "apron" "assign_exp converted: %a" Texpr1.pretty texpr1;
A.assign_texpr_with Man.mgr nd v texpr1 None
| exception Convert.Unsupported_CilExp _ ->
if M.tracing then M.trace "apron" "assign_exp unsupported";
@@ -442,7 +442,7 @@ struct
let invariant _ = []
let show (x:t) =
- Format.asprintf "%a (env: %a)" A.print x (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)
+ GobFormat.asprintf "%a (env: %a)" A.print x Environment.pp (A.env x)
let pretty () (x:t) = text (show x)
let equal x y =
@@ -454,7 +454,7 @@ struct
let compare (x: t) (y: t): int =
failwith "Apron.Abstract1 doesn't have total order" (* https://github.com/antoinemine/apron/issues/99 *)
- let printXml f x = BatPrintf.fprintf f "\n\n\n" (XmlUtil.escape (Format.asprintf "%a" A.print x)) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)))
+ let printXml f x = BatPrintf.fprintf f "\n\n\n" (XmlUtil.escape (GobFormat.asprint A.print x)) Environment.printXml (A.env x)
let to_yojson (x: t) =
let constraints =
@@ -463,11 +463,9 @@ struct
|> Lincons1Set.elements
|> List.map (fun lincons1 -> `String (Lincons1.show lincons1))
in
- let env = `String (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x))
- in
`Assoc [
("constraints", `List constraints);
- ("env", env);
+ ("env", Environment.to_yojson (A.env x));
]
let unify x y =
@@ -533,9 +531,9 @@ struct
| _ ->
begin match Convert.tcons1_of_cil_exp ask d (A.env d) e negate no_ov with
| tcons1 ->
- if M.tracing then M.trace "apron" "assert_constraint %a %s" d_exp e (Format.asprintf "%a" Tcons1.print tcons1);
+ if M.tracing then M.trace "apron" "assert_constraint %a %a" d_exp e Tcons1.pretty tcons1;
if M.tracing then M.trace "apron" "assert_constraint st: %a" D.pretty d;
- if M.tracing then M.trace "apron" "assert_constraint tcons1: %s" (Format.asprintf "%a" Tcons1.print tcons1);
+ if M.tracing then M.trace "apron" "assert_constraint tcons1: %a" Tcons1.pretty tcons1;
let r = meet_tcons ask d tcons1 e in
if M.tracing then M.trace "apron" "assert_constraint r: %a" D.pretty r;
r
@@ -598,7 +596,7 @@ struct
let x_cons = A.to_lincons_array Man.mgr x_j in
let y_cons = A.to_lincons_array Man.mgr y_j in
let try_add_con j con1 =
- if M.tracing then M.tracei "apron" "try_add_con %s" (Format.asprintf "%a" (Lincons1.print: Format.formatter -> Lincons1.t -> unit) con1);
+ if M.tracing then M.tracei "apron" "try_add_con %a" Lincons1.pretty con1;
let t = meet_lincons j con1 in
let t_x = A.change_environment Man.mgr t x_env false in
let t_y = A.change_environment Man.mgr t y_env false in
@@ -637,7 +635,7 @@ struct
in
let env_exists_mem_con1 env con1 =
let r = env_exists_mem_con1 env con1 in
- if M.tracing then M.trace "apron" "env_exists_mem_con1 %s %s -> %B" (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) env) (Lincons1.show con1) r;
+ if M.tracing then M.trace "apron" "env_exists_mem_con1 %a %a -> %B" Environment.pretty env Lincons1.pretty con1 r;
r
in
(* Heuristically reorder constraints to pass 36/12 with singlethreaded->multithreaded mode switching. *)
diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
index 4d473447b7..fbb1fe9ec5 100644
--- a/src/cdomains/apron/gobApron.apron.ml
+++ b/src/cdomains/apron/gobApron.apron.ml
@@ -1,6 +1,19 @@
open Batteries
include Apron
+module Scalar =
+struct
+ include Scalar
+
+ let pp = print
+ include Printable.SimpleFormat (
+ struct
+ type nonrec t = t
+ let pp = pp
+ end
+ )
+end
+
module Coeff =
struct
include Coeff
@@ -11,6 +24,15 @@ end
module Var =
struct
include Var
+
+ let pp = print
+ include Printable.SimpleFormat (
+ struct
+ type nonrec t = t
+ let pp = pp
+ end
+ )
+
let equal x y = Var.compare x y = 0
end
@@ -18,7 +40,14 @@ module Lincons1 =
struct
include Lincons1
- let show = Format.asprintf "%a" print
+ let pp = print
+ include Printable.SimpleFormat (
+ struct
+ type nonrec t = t
+ let pp = pp
+ end
+ )
+
let compare x y =
(* TODO: implement proper total Lincons1 order *)
String.compare (show x) (show y) (* HACK *)
@@ -45,12 +74,59 @@ struct
|> of_enum
end
+module Texpr1 =
+struct
+ include Texpr1
+
+ let pp = print
+ include Printable.SimpleFormat (
+ struct
+ type nonrec t = t
+ let pp = pp
+ end
+ )
+
+ module Expr =
+ struct
+ type t = expr
+
+ let pp = print_expr
+ include Printable.SimpleFormat (
+ struct
+ type nonrec t = t
+ let pp = pp
+ end
+ )
+ end
+end
+
+module Tcons1 =
+struct
+ include Tcons1
+
+ let pp = print
+ include Printable.SimpleFormat (
+ struct
+ type nonrec t = t
+ let pp = pp
+ end
+ )
+end
+
(** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain.
A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *)
module Environment =
struct
include Environment
+ let pp: Format.formatter -> Environment.t -> unit = Environment.print
+ include Printable.SimpleFormat (
+ struct
+ type nonrec t = t
+ let pp = pp
+ end
+ )
+
let compare (x: t) (y: t): int =
(* TODO: implement total Environment order in OCaml *)
failwith "Apron.Environment doesn't have total order" (* https://github.com/antoinemine/apron/issues/99 *)
diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
index 0b50815dfa..c1ca3661a5 100644
--- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
+++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -11,7 +11,7 @@ open Batteries
open GoblintCil
open Pretty
module M = Messages
-open Apron
+open GobApron
open VectorMatrix
module Mpqf = SharedFunctions.Mpqf
@@ -331,7 +331,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 %s -> %s" (EConj.show @@ snd @@ BatOption.get t.d) (Format.asprintf "%a" Texpr1.print_expr texp)
+ if M.tracing then M.tracel "from_texp" "%s %a -> %s" (EConj.show @@ 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
@@ -361,7 +361,7 @@ struct
else
match simplify_to_ref_and_offset t (Texpr1.to_expr texpr) with
| Some (None, offset, divisor) when Z.equal (Z.rem offset divisor) Z.zero -> let res = Z.div offset divisor in
- (if M.tracing then M.tracel "bounds" "min: %s max: %s" (IntOps.BigIntOps.to_string res) (IntOps.BigIntOps.to_string res);
+ (if M.tracing then M.tracel "bounds" "min: %a max: %a" GobZ.pretty res GobZ.pretty res;
Some res, Some res)
| _ -> None, None
@@ -424,7 +424,7 @@ struct
EConj.show_formatted (show_var varM.env) (snd arr) ^ (to_subscript @@ fst arr)
let pretty () (x:t) = text (show x)
- let printXml f x = BatPrintf.fprintf f "\n\n\n" (XmlUtil.escape (Format.asprintf "%s" (show x) )) (XmlUtil.escape (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (x.env)))
+ 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
let meet_with_one_conj t i (var, o, divi) =
@@ -630,8 +630,8 @@ struct
let assign_exp ask t var exp no_ov =
let res = assign_exp ask t var exp no_ov in
- if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %s \n exp: %a\n no_ov: %b -> \n %s"
- (show t) (Var.to_string var) d_exp exp (Lazy.force no_ov) (show res) ;
+ if M.tracing then M.tracel "ops" "assign_exp t:\n %s \n var: %a \n exp: %a\n no_ov: %b -> \n %s"
+ (show t) Var.pretty var d_exp exp (Lazy.force no_ov) (show res);
res
let assign_var (t: VarManagement.t) v v' =
@@ -640,7 +640,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: %s \n v': %s\n -> %s" (show t) (Var.to_string v) (Var.to_string v') (show res) ;
+ 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);
res
(** Parallel assignment of variables.
@@ -693,7 +693,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: %s \n exp: %a \n -> \n %s" (show t) (Var.to_string var) d_exp exp (show res);
+ 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);
res
let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov
diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
index 8121635e89..86b5f2770f 100644
--- a/src/cdomains/apron/sharedFunctions.apron.ml
+++ b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -40,7 +40,7 @@ let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) =
in
Z_mlgmpidl.z_of_mpzf z
| _ ->
- failwith ("int_of_scalar: unsupported: " ^ Scalar.to_string scalar)
+ failwith ("int_of_scalar: unsupported: " ^ Scalar.show scalar)
module type ConvertArg =
@@ -200,7 +200,7 @@ struct
in
let exp = Cil.constFold false exp in
let res = conv exp in
- if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %s (%b)" d_plainexp exp (Format.asprintf "%a" Texpr1.print_expr res) (Lazy.force no_ov);
+ if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" d_plainexp exp Texpr1.Expr.pretty res (Lazy.force no_ov);
res
let texpr1_of_cil_exp ask d env e no_ov =
@@ -267,7 +267,7 @@ struct
else
Const (CInt(i,ILongLong,None)), false
else
- (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %s" (Scalar.to_string c); raise Unsupported_Linexpr1)
+ (M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c; raise Unsupported_Linexpr1)
| None -> raise Unsupported_Linexpr1)
| _ -> raise Unsupported_Linexpr1
in
@@ -282,8 +282,8 @@ struct
expr := BinOp(MinusA,!expr,prod,longlong)
else
expr := BinOp(PlusA,!expr,prod,longlong)
- | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %s" (Var.to_string v); raise Unsupported_Linexpr1
- | _ -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %s" (Var.to_string v); raise Unsupported_Linexpr1
+ | None -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v; raise Unsupported_Linexpr1
+ | _ -> M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var in overflow preserving manner: %a" Var.pretty v; raise Unsupported_Linexpr1
in
Linexpr1.iter append_summand linexpr1;
!expr
diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml
index 199113a5d8..e001a2b557 100644
--- a/src/common/domains/printable.ml
+++ b/src/common/domains/printable.ml
@@ -88,6 +88,20 @@ struct
let to_yojson x = `String (show x)
end
+module type Formatable =
+sig
+ type t
+ val pp: Format.formatter -> t -> unit
+end
+
+module SimpleFormat (P: Formatable) =
+struct
+ let show x = GobFormat.asprint P.pp x
+ let pretty () x = text (show x)
+ let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape (show x))
+ let to_yojson x = `String (show x)
+end
+
module type Name = sig val name: string end
module UnitConf (N: Name) =
diff --git a/src/common/util/gobFormat.ml b/src/common/util/gobFormat.ml
index 3cda0a4758..8f26ff0087 100644
--- a/src/common/util/gobFormat.ml
+++ b/src/common/util/gobFormat.ml
@@ -19,3 +19,12 @@ let pp_set_ansi_color_tags ppf =
Format.pp_set_mark_tags ppf true
let pp_print_nothing (ppf: Format.formatter) () = ()
+
+let pp_infinity = 1000000001 (* Exact value not exposed before OCaml 5.2, but use the smallest value permitted by documentation. *)
+
+let pp_set_infinite_geometry = Format.pp_set_geometry ~max_indent:(pp_infinity - 2) ~margin:(pp_infinity - 1)
+
+let asprintf (fmt: ('a, Format.formatter, unit, string) format4): 'a =
+ Format.asprintf ("%t" ^^ fmt) pp_set_infinite_geometry
+
+let asprint pp x = asprintf "%a" pp x (* eta-expanded to bypass value restriction *)