From b8bf69376ab74b4ae25845de51b90cf4896a33cd Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Apr 2026 07:17:38 +0000 Subject: [PATCH 1/3] Initial plan From ed977a3d0125a1a24b5b8965eb3ea275701a4850 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Apr 2026 08:00:13 +0000 Subject: [PATCH 2/3] Add pp implementations to modules implementing Printable.S Add pp to modules that implement Printable.S without SimplePretty/SimpleShow/SimpleFormat: - FlagHelper: derive pp from show - partitionDomain: Make and SetSet get pp from show - ResultType2: derive pp from overridden show - creationLockset A: derive pp from show - mCPRegistry DomListPrintable/DomVariantPrintable: derive pp from show - basetype Variables/RawStrings/CilStmt: derive pp from show - controlSpecC: derive pp from show Add pp_trace to VarType signature and implementations: - constrSys VarType: add val pp_trace - constrSys Var2: implement pp_trace via GobPretty.sprint - analyses VarF: implement pp_trace via GobPretty.sprint - analyses GVarF/GVarFC: pp_trace = pp - node: add pp_trace using show Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- src/analyses/creationLockset.ml | 1 + src/analyses/mCPRegistry.ml | 4 ++++ src/common/cdomains/basetype.ml | 3 +++ src/common/domains/printable.ml | 33 ++++++++++++++++++++++++++++ src/common/framework/controlSpecC.ml | 1 + src/common/framework/node.ml | 2 ++ src/common/util/gobFormat.ml | 4 ++++ src/constraint/constrSys.ml | 3 +++ src/domain/flagHelper.ml | 1 + src/domain/hoareDomain.ml | 5 +++++ src/domain/mapDomain.ml | 33 ++++++++++++++++++++++++++++ src/domain/partitionDomain.ml | 2 ++ src/domain/setDomain.ml | 14 ++++++++++++ src/framework/analyses.ml | 4 ++++ src/framework/analysisResult.ml | 1 + src/util/std/gobFpath.ml | 2 ++ 16 files changed, 113 insertions(+) diff --git a/src/analyses/creationLockset.ml b/src/analyses/creationLockset.ml index 61fc797585..905614ca81 100644 --- a/src/analyses/creationLockset.ml +++ b/src/analyses/creationLockset.ml @@ -140,6 +140,7 @@ module Spec = struct (* TID and Lockset components are directly queried from other analyses and already are printed by them *) let pretty () (_, _, cl) = G.pretty () cl let show (_, _, cl) = G.show cl + let pp ppf x = Format.pp_print_string ppf (show x) let to_yojson (_, _, cl) = G.to_yojson cl let printXml f (_, _, cl) = G.printXml f cl diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml index 05519dbb62..09975b5027 100644 --- a/src/analyses/mCPRegistry.ml +++ b/src/analyses/mCPRegistry.ml @@ -169,6 +169,8 @@ struct in IO.to_string (List.print ~first:"[" ~last:"]" ~sep:", " String.print) (rev xs) + let pp ppf x = Format.pp_print_string ppf (show x) + let to_yojson xs = let f a n (module S : Printable.S) x = let name = find_spec_name n in @@ -246,6 +248,8 @@ struct analysis_name ^ ":" ^ S.show (Obj.obj x) ) + let pp ppf x = Format.pp_print_string ppf (show x) + let to_yojson x = `Assoc [ unop_map (fun n (module S: Printable.S) x -> diff --git a/src/common/cdomains/basetype.ml b/src/common/cdomains/basetype.ml index 5ec9b22b44..fa86fbc50e 100644 --- a/src/common/cdomains/basetype.ml +++ b/src/common/cdomains/basetype.ml @@ -11,6 +11,7 @@ struct let description = RichVarinfo.BiVarinfoMap.Collection.describe_varinfo x in "(" ^ x.vname ^ ", " ^ description ^ ")" else x.vname + let pp ppf x = Format.pp_print_string ppf (show x) let pretty () x = Pretty.text (show x) type group = Global | Local | Parameter | Temp [@@deriving ord, show { with_path = false }] let to_group = function @@ -28,6 +29,7 @@ struct open Pretty type t = string [@@deriving eq, ord, hash, to_yojson] let show x = "\"" ^ x ^ "\"" + let pp ppf x = Format.pp_print_string ppf (show x) let pretty () x = text (show x) let name () = "raw strings" let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape (show x)) @@ -125,6 +127,7 @@ module CilStmt: Printable.S with type t = stmt = struct include CilType.Stmt let show x = "" + let pp ppf x = Format.pp_print_string ppf (show x) let pretty = Cilfacade.stmt_pretty_short let name () = "expressions" diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index 45a66ea336..3d5bfe4eeb 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -12,6 +12,7 @@ sig val compare: t -> t -> int val show: t -> string val pretty: unit -> t -> doc + val pp: Format.formatter -> t -> unit (* These two lets us reuse the short function, and allows some overriding * possibilities. *) val printXml : 'a BatInnerIO.output -> t -> unit @@ -35,6 +36,7 @@ struct type t = | [@@deriving eq, ord, hash] let show (x: t) = match x with _ -> . let pretty () (x: t) = match x with _ -> . + let pp _ (x: t) = match x with _ -> . let printXml _ (x: t) = match x with _ -> . let name () = "empty" let to_yojson (x: t) = match x with _ -> . @@ -71,6 +73,7 @@ end module SimpleShow (P: Showable) = struct let pretty () x = text (P.show x) + let pp ppf x = Format.pp_print_string ppf (P.show x) let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape (P.show x)) let to_yojson x = `String (P.show x) end @@ -84,6 +87,7 @@ end module SimplePretty (P: Prettyable) = struct let show x = GobPretty.sprint P.pretty x + let pp ppf x = Format.pp_print_string ppf (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 @@ -96,6 +100,7 @@ end module SimpleFormat (P: Formatable) = struct + let pp = P.pp 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)) @@ -109,6 +114,7 @@ struct type t = unit [@@deriving eq, ord, hash] include StdLeaf let pretty () _ = text N.name + let pp ppf _ = Format.pp_print_string ppf N.name let show _ = N.name let name () = "Unit" let printXml f () = BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape N.name) @@ -132,6 +138,7 @@ struct let show = lift_f Base.show let pretty () = lift_f (Base.pretty ()) + let pp ppf = lift_f (Base.pp ppf) (* Debug printing with tags *) (* let pretty () x = Pretty.dprintf "%a[%d,%d]" Base.pretty x.BatHashcons.obj x.BatHashcons.tag x.BatHashcons.hcode @@ -189,6 +196,7 @@ struct let show = lift_f Base.show let pretty () = lift_f (Base.pretty ()) + let pp ppf = lift_f (Base.pp ppf) let printXml f = lift_f (Base.printXml f) let to_yojson = lift_f (Base.to_yojson) @@ -220,6 +228,8 @@ struct else Base.show x + let pp ppf x = Format.pp_print_string ppf (show x) + let printXml f x = if Conf.expand then BatPrintf.fprintf f "\n\n%s\n\n%a\n\n" (Base.name ()) Base.printXml x @@ -268,6 +278,8 @@ struct | `Bot -> bot_name | `Top -> top_name + let pp ppf x = Format.pp_print_string ppf (show x) + let pretty () (state:t) = match state with | `Lifted n -> Base.pretty () n @@ -329,6 +341,8 @@ struct | `Left n -> Base1.show n | `Right n -> Base2.show n + let pp ppf x = Format.pp_print_string ppf (show x) + let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name () let printXml f = function | `Left x -> Base1.printXml f x @@ -374,6 +388,8 @@ struct | `Middle n -> Base2.show n | `Right n -> Base3.show n + let pp ppf x = Format.pp_print_string ppf (show x) + let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name () ^ " or " ^ Base3.name () let printXml f = function | `Left x -> Base1.printXml f x @@ -408,6 +424,8 @@ struct | None -> N.name | Some n -> Base.show n + let pp ppf x = Format.pp_print_string ppf (show x) + let name () = Base.name () ^ " option" let printXml f = function | None -> BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape N.name) @@ -451,6 +469,8 @@ struct | `Bot -> bot_name | `Top -> top_name + let pp ppf x = Format.pp_print_string ppf (show x) + let relift x = match x with | `Lifted1 n -> `Lifted1 (Base1.relift n) | `Lifted2 n -> `Lifted2 (Base2.relift n) @@ -512,6 +532,8 @@ struct else text (show (x,y)) + let pp ppf x = Format.pp_print_string ppf (show x) + let printXml f (x,y) = BatPrintf.fprintf f "\n\n\n%s\n\n%a\n%s\n\n%a\n\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x (XmlUtil.escape (Base2.name ())) Base2.printXml y @@ -560,6 +582,8 @@ struct ++ unalign ++ text ")" + let pp ppf x = Format.pp_print_string ppf (show x) + let printXml f (x,y,z) = BatPrintf.fprintf f "\n\n\n%s\n\n%a\n%s\n\n%a\n%s\n\n%a\n\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x (XmlUtil.escape (Base2.name ())) Base2.printXml y (XmlUtil.escape (Base3.name ())) Base3.printXml z @@ -579,6 +603,7 @@ struct let show x = "[" ^ (BatDeque.fold_right (fun a acc -> Base.show a ^ ", " ^ acc) x "]") let pretty () x = text (show x) + let pp ppf x = Format.pp_print_string ppf (show x) let name () = Base.name () ^ "queue" let relift x = BatDeque.map Base.relift x @@ -618,6 +643,7 @@ struct "[" ^ (String.concat ", " elems) ^ "]" let pretty () x = text (show x) + let pp ppf x = Format.pp_print_string ppf (show x) let relift x = List.map Base.relift x @@ -647,6 +673,7 @@ struct let show x = P.names x let pretty () x = text (show x) + let pp ppf x = Format.pp_print_string ppf (show x) let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (P.names x) let to_yojson x = `String (P.names x) @@ -665,6 +692,8 @@ struct | `Lifted n -> Base.show n | `Bot -> "bot of " ^ (Base.name ()) + let pp ppf x = Format.pp_print_string ppf (show x) + let pretty () (state:t) = match state with | `Lifted n -> Base.pretty () n @@ -696,6 +725,8 @@ struct | `Lifted n -> Base.show n | `Top -> "top of " ^ (Base.name ()) + let pp ppf x = Format.pp_print_string ppf (show x) + let pretty () (state:t) = match state with | `Lifted n -> Base.pretty () n @@ -733,6 +764,7 @@ struct type t = string [@@deriving eq, ord, hash, to_yojson] include StdLeaf let pretty () n = text n + let pp ppf n = Format.pp_print_string ppf n let show n = n let name () = "String" let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" x @@ -756,6 +788,7 @@ struct let show _ = failwith Message.message let pretty _ _ = failwith Message.message + let pp _ _ = failwith Message.message let printXml _ _ = failwith Message.message let to_yojson _ = failwith Message.message diff --git a/src/common/framework/controlSpecC.ml b/src/common/framework/controlSpecC.ml index eaec77f6c5..d83db16f8d 100644 --- a/src/common/framework/controlSpecC.ml +++ b/src/common/framework/controlSpecC.ml @@ -31,6 +31,7 @@ let tag x = let show x = let module C = (val !control_spec_c) in C.show (Obj.obj x) +let pp ppf x = Format.pp_print_string ppf (show x) let pretty () x = let module C = (val !control_spec_c) in C.pretty () (Obj.obj x) diff --git a/src/common/framework/node.ml b/src/common/framework/node.ml index 906f9e1d77..fcd580d059 100644 --- a/src/common/framework/node.ml +++ b/src/common/framework/node.ml @@ -40,6 +40,8 @@ include Printable.SimplePretty ( ) (* TODO: deriving to_yojson gets overridden by SimplePretty *) +let pp_trace ppf x = Format.pp_print_string ppf (show x) + (** Show node ID for CFG and results output. *) let show_id = function | Statement stmt -> string_of_int stmt.sid diff --git a/src/common/util/gobFormat.ml b/src/common/util/gobFormat.ml index 8f26ff0087..a194708b5f 100644 --- a/src/common/util/gobFormat.ml +++ b/src/common/util/gobFormat.ml @@ -28,3 +28,7 @@ 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 *) + +let pp_print_opt ?(none="?") pp ppf = function + | None -> Format.pp_print_string ppf none + | Some x -> pp ppf x diff --git a/src/constraint/constrSys.ml b/src/constraint/constrSys.ml index 7857d5a543..9e4fbdbd59 100644 --- a/src/constraint/constrSys.ml +++ b/src/constraint/constrSys.ml @@ -13,6 +13,7 @@ sig include Hashtbl.HashedType include SysVar with type t := t val pretty_trace: unit -> t -> GoblintCil.Pretty.doc + val pp_trace: Format.formatter -> t -> unit val compare : t -> t -> int val printXml : 'a BatInnerIO.output -> t -> unit @@ -37,6 +38,8 @@ struct | `L a -> GoblintCil.Pretty.dprintf "L:%a" LV.pretty_trace a | `G a -> GoblintCil.Pretty.dprintf "G:%a" GV.pretty_trace a + let pp_trace ppf x = Format.pp_print_string ppf (GobPretty.sprint pretty_trace x) + let printXml f = function | `L a -> LV.printXml f a | `G a -> GV.printXml f a diff --git a/src/domain/flagHelper.ml b/src/domain/flagHelper.ml index c3bcb584b2..fe1eb2d18e 100644 --- a/src/domain/flagHelper.ml +++ b/src/domain/flagHelper.ml @@ -31,6 +31,7 @@ struct | _ -> failwith Msg.msg let show = unop L.show R.show + let pp ppf x = Format.pp_print_string ppf (show x) let pretty () = unop (L.pretty ()) (R.pretty ()) let printXml f = unop (L.printXml f) (R.printXml f) let to_yojson = unop L.to_yojson R.to_yojson diff --git a/src/domain/hoareDomain.ml b/src/domain/hoareDomain.ml index 1bd56c0d1d..f7edc1a632 100644 --- a/src/domain/hoareDomain.ml +++ b/src/domain/hoareDomain.ml @@ -162,6 +162,11 @@ struct let content = List.fold_left (++) nil separated in (text "{") ++ content ++ (text "}") + let pp ppf x = + let pp_sep ppf () = Format.fprintf ppf ", " in + Format.fprintf ppf "{%a}" + (Format.pp_print_list ~pp_sep E.pp) (elements x) + let pretty_diff () ((x:t),(y:t)): Pretty.doc = Pretty.dprintf "HoarePO: %a not leq %a" pretty x pretty y let printXml f x = diff --git a/src/domain/mapDomain.ml b/src/domain/mapDomain.ml index cf563dab44..0963c05cb1 100644 --- a/src/domain/mapDomain.ml +++ b/src/domain/mapDomain.ml @@ -79,6 +79,17 @@ struct let show map = GobPretty.sprint pretty map + let pp ppf map = + let first = ref true in + Format.fprintf ppf "@[{"; + M.iter (fun k v -> + if !first then (first := false; Format.fprintf ppf "@[@,") + else Format.fprintf ppf "@,"; + Format.fprintf ppf "@[%a ->@ @[%a@]@]" D.pp k R.pp v + ) map; + if !first then Format.fprintf ppf "}" + else Format.fprintf ppf "@]}@]" + let printXml f map = BatPrintf.fprintf f "\n\n"; M.iter (fun k v -> @@ -132,6 +143,28 @@ struct let show map = GobPretty.sprint pretty map + let pp ppf mapping = + let groups = + M.fold (fun k v acc -> + GroupMap.update (D.to_group k) (fun kvs -> + let kvs = Option.value kvs ~default:[] in + Some ((k, v) :: kvs) + ) acc + ) mapping GroupMap.empty + in + Format.fprintf ppf "@[{"; + let first_group = ref true in + GroupMap.iter (fun group kvs -> + if !first_group then (first_group := false; Format.fprintf ppf "@[@,") + else Format.fprintf ppf "@,"; + Format.fprintf ppf "@[%s {@ @[%a@]}@]" (D.show_group group) + (Format.pp_print_list (fun ppf (k, v) -> + Format.fprintf ppf "@[%a ->@ @[%a@]@]" D.pp k R.pp v)) + (List.rev kvs) + ) groups; + if !first_group then Format.fprintf ppf "}" + else Format.fprintf ppf "@]}@]" + (* TODO: groups in XML, JSON? *) end diff --git a/src/domain/partitionDomain.ml b/src/domain/partitionDomain.ml index e97946e463..70322ba238 100644 --- a/src/domain/partitionDomain.ml +++ b/src/domain/partitionDomain.ml @@ -54,6 +54,7 @@ struct type elem = S.elt let show _ = "Partitions" + let pp ppf x = Format.pp_print_string ppf (show x) let leq x y = for_all (fun p -> exists (S.leq p) y) x @@ -105,6 +106,7 @@ struct type partition = t let show _ = "Partitions" + let pp ppf x = Format.pp_print_string ppf (show x) (* Top and bottom are reversed: Bottom will be All (equations), i.e. contradiction, diff --git a/src/domain/setDomain.ml b/src/domain/setDomain.ml index e11c8182de..dde816035a 100644 --- a/src/domain/setDomain.ml +++ b/src/domain/setDomain.ml @@ -152,6 +152,11 @@ struct let all_elems : string list = List.map E.show (S.elements x) in Printable.get_short_list "{" "}" all_elems + let pp ppf x = + let pp_sep ppf () = Format.fprintf ppf ",@ " in + Format.fprintf ppf "@[{%a}@]" + (Format.pp_print_list ~pp_sep E.pp) (S.elements x) + let to_yojson x = [%to_yojson: E.t list] (S.elements x) let printXml f xs = @@ -361,6 +366,11 @@ struct | `Top -> N.topname | `Lifted t -> S.show t + let pp ppf x = + match x with + | `Top -> Format.pp_print_string ppf N.topname + | `Lifted t -> S.pp ppf t + (* Lattice implementation *) (* Lift separately because lattice order might be different from subset order, e.g. after Reverse *) @@ -430,6 +440,10 @@ struct let content = List.fold_left (++) nil separated in content + let pp ppf x = + let pp_sep ppf () = Format.fprintf ppf ", " in + Format.pp_print_list ~pp_sep Base.pp ppf (elements x) + let pretty_diff () ((x:t),(y:t)): Pretty.doc = Pretty.dprintf "%s: %a not leq %a" (name ()) pretty x pretty y let printXml f xs = diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index f655d89316..187fe7f500 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -35,6 +35,8 @@ struct (* if get_bool "dbg.trace.context" then dprintf "(%a, %d) on %a" Node.pretty_trace n (LD.tag c) CilType.Location.pretty (getLocation x) *) else dprintf "%a on %a" Node.pretty_trace n CilType.Location.pretty (getLocation x) + let pp_trace ppf x = Format.pp_print_string ppf (GobPretty.sprint pretty_trace x) + let printXml f (n,c) = Var.printXml f n; BatPrintf.fprintf f "\n"; @@ -63,6 +65,7 @@ struct let var_id = show let node _ = MyCFG.Function Cil.dummyFunDec let pretty_trace = pretty + let pp_trace = pp let is_write_only = function | `Left x -> V.is_write_only x | `Right _ -> true @@ -79,6 +82,7 @@ struct let var_id = show let node _ = MyCFG.Function Cil.dummyFunDec let pretty_trace = pretty + let pp_trace = pp let is_write_only = function | `Left x -> V.is_write_only x | `Right _ -> true diff --git a/src/framework/analysisResult.ml b/src/framework/analysisResult.ml index 2d9fe623c7..f894248b17 100644 --- a/src/framework/analysisResult.ml +++ b/src/framework/analysisResult.ml @@ -53,6 +53,7 @@ struct open S include Printable.Prod3 (C) (D) (CilType.Fundec) let show (es,x,f:t) = D.show x + let pp ppf x = Format.pp_print_string ppf (show x) let pretty () (_,x,_) = D.pretty () x let printXml f (c,d,fd) = BatPrintf.fprintf f "\n%a\n%a" C.printXml c D.printXml d diff --git a/src/util/std/gobFpath.ml b/src/util/std/gobFpath.ml index 9b6523030c..93b62e3ab8 100644 --- a/src/util/std/gobFpath.ml +++ b/src/util/std/gobFpath.ml @@ -4,6 +4,8 @@ let hash p = Hashtbl.hash (Fpath.to_string p) let pretty () p = GoblintCil.Pretty.text (Fpath.to_string p) +let pp ppf p = Format.pp_print_string ppf (Fpath.to_string p) + let to_yojson p = `String (Fpath.to_string p) let of_yojson = function From 635fa367ab681e738a999472c874ef50e062b988 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Apr 2026 08:16:11 +0000 Subject: [PATCH 3/3] Migrate tracing system from Pretty to Format, add pp to domain files Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/fc978a58-7acb-4657-923a-8cd4ecb79445 Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com> --- src/analyses/accessAnalysis.ml | 4 +- src/analyses/apron/relationAnalysis.apron.ml | 44 +++---- src/analyses/apron/relationPriv.apron.ml | 106 ++++++++-------- src/analyses/base.ml | 118 +++++++++--------- src/analyses/baseInvariant.ml | 52 ++++---- src/analyses/basePriv.ml | 110 ++++++++-------- src/analyses/c2poAnalysis.ml | 18 +-- src/analyses/condVars.ml | 2 +- src/analyses/mCP.ml | 10 +- src/analyses/startStateAnalysis.ml | 2 +- src/analyses/symbLocks.ml | 8 +- src/analyses/taintPartialContexts.ml | 4 +- src/analyses/threadEscape.ml | 6 +- src/analyses/tmpSpecial.ml | 6 +- src/analyses/varEq.ml | 14 +-- src/arg/argConstraints.ml | 6 +- src/cdomain/value/cdomains/arrayDomain.ml | 6 +- src/cdomain/value/cdomains/int/intDomTuple.ml | 1 + src/cdomain/value/cdomains/intDomain0.ml | 5 +- src/cdomain/value/cdomains/offset.ml | 2 +- src/cdomain/value/cdomains/structDomain.ml | 17 +-- src/cdomain/value/cdomains/threadIdDomain.ml | 3 + src/cdomain/value/cdomains/valueDomain.ml | 12 +- .../apron/affineEqualityDenseDomain.apron.ml | 9 +- .../apron/affineEqualityDomain.apron.ml | 9 +- src/cdomains/apron/apronDomain.apron.ml | 19 +-- .../apron/linearTwoVarEqualityDomain.apron.ml | 11 +- src/cdomains/apron/relationDomain.apron.ml | 2 + src/cdomains/apron/sharedFunctions.apron.ml | 10 +- src/cdomains/baseDomain.ml | 2 + src/cdomains/c2poDomain.ml | 2 +- src/cdomains/duplicateVars.ml | 2 +- src/cdomains/musteqDomain.ml | 2 + src/cdomains/symbLocksDomain.ml | 2 +- src/cdomains/unionFind.ml | 14 +-- src/common/framework/cfgTools.ml | 10 +- src/common/framework/edge.ml | 3 + src/common/util/messages.ml | 14 +-- src/config/gobConfig.ml | 6 +- src/domains/access.ml | 14 +-- src/framework/constraints.ml | 8 +- src/framework/control.ml | 12 +- src/incremental/compareAST.ml | 4 +- src/lifters/longjmpLifter.ml | 10 +- src/lifters/specLifters.ml | 8 +- src/solver/generic.ml | 10 +- src/solver/postSolver.ml | 6 +- src/solver/sLR.ml | 12 +- src/solver/sLRphased.ml | 18 +-- src/solver/sLRterm.ml | 20 +-- src/solver/sideWPointSelect.ml | 2 +- src/solver/td3.ml | 88 ++++++------- src/solver/td3UpdateRule.ml | 10 +- src/solver/td_simplified.ml | 38 +++--- src/solver/td_simplified_ref.ml | 38 +++--- src/solver/topDown.ml | 32 ++--- src/solver/topDown_deprecated.ml | 26 ++-- src/solver/topDown_space_cache_term.ml | 32 ++--- src/solver/topDown_term.ml | 26 ++-- src/util/loopUnrolling.ml | 2 +- src/util/std/gobYojson.ml | 2 + src/util/tracing/goblint_tracing.ml | 23 ++-- 62 files changed, 574 insertions(+), 540 deletions(-) diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index 64c61a8d93..a30e4de345 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -32,7 +32,7 @@ struct emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *) let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) = - if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach; + if M.tracing then M.trace "access" "do_access %a %a %B" CilType.Exp.pp e AccessKind.pp kind reach; let reach_or_mpt: _ Queries.t = if reach then ReachableFrom e else MayPointTo e in let ad = man.ask reach_or_mpt in man.emit (Access {exp=e; ad; kind; reach}) @@ -42,7 +42,7 @@ struct + [deref=true], [reach=false] - Access [exp] by dereferencing once (may-point-to), used for lval writes and shallow special accesses. + [deref=true], [reach=true] - Access [exp] by dereferencing transitively (reachable), used for deep special accesses. *) let access_one_top ?(force=false) ?(deref=false) man (kind: AccessKind.t) reach exp = - if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)" CilType.Exp.pretty exp AccessKind.pretty kind reach deref; + if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)" CilType.Exp.pp exp AccessKind.pp kind reach deref; if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man) then ( if deref && Cil.isPointerType (Cilfacade.typeOf exp) then (* avoid dereferencing integers to unknown pointers, which cause many spurious type-based accesses *) do_access man kind reach exp; diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 5d66659b43..789304f0ae 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -89,7 +89,7 @@ struct let e' = visitCilExpr visitor e in let rel = RD.add_vars st.rel (List.map RV.local (VH.to_seq_values v_ins |> List.of_seq)) in (* add temporary g#in-s *) let rel' = VH.fold (fun v v_in rel -> - if M.tracing then M.trace "relation" "read_global %a %a" CilType.Varinfo.pretty v CilType.Varinfo.pretty v_in; + if M.tracing then M.trace "relation" "read_global %a %a" CilType.Varinfo.pp v CilType.Varinfo.pp v_in; read_global ask getg {st with rel} v v_in (* g#in = g; *) ) v_ins rel in @@ -124,7 +124,7 @@ struct let assign_from_globals_wrapper ask getg st e f = let (rel', e', v_ins) = read_globals_to_locals ask getg st e in - if M.tracing then M.trace "relation" "assign_from_globals_wrapper %a" d_exp e'; + if M.tracing then M.trace "relation" "assign_from_globals_wrapper %a" CilType.Exp.pp e'; let rel' = f rel' e' in (* x = e; *) let rel'' = RD.remove_vars rel' (List.map RV.local (VH.to_seq_values v_ins |> List.of_seq)) in (* remove temporary g#in-s *) rel'' @@ -155,7 +155,7 @@ struct v_out.vattr <- v.vattr; (*copy the attributes because the tracking may depend on them. Otherwise an assertion fails *) let st = {st with rel = RD.add_vars st.rel [RV.local v_out]} in (* add temporary g#out *) let st' = {st with rel = f st v_out} in (* g#out = e; *) - if M.tracing then M.trace "relation" "write_global %a %a" CilType.Varinfo.pretty v CilType.Varinfo.pretty v_out; + if M.tracing then M.trace "relation" "write_global %a %a" CilType.Varinfo.pp v CilType.Varinfo.pp v_out; let st' = write_global ask getg sideg st' v v_out in (* g = g#out; *) let rel'' = RD.remove_vars st'.rel [RV.local v_out] in (* remove temporary g#out *) {st' with rel = rel''} @@ -192,7 +192,7 @@ struct let no_overflow man exp = lazy ( let res = no_overflow man exp in - if M.tracing then M.tracel "no_ov" "no_ov %b exp: %a" res d_exp exp; + if M.tracing then M.tracel "no_ov" "no_ov %b exp: %a" res CilType.Exp.pp exp; res ) @@ -249,20 +249,20 @@ struct let assign man (lv:lval) e = let st = man.local in let simplified_e = replace_deref_exps man.ask e in - if M.tracing then M.traceli "relation" "assign %a = %a (simplified to %a)" d_lval lv d_exp e d_exp simplified_e; + if M.tracing then M.traceli "relation" "assign %a = %a (simplified to %a)" CilType.Lval.pp lv CilType.Exp.pp e CilType.Exp.pp simplified_e; let ask = Analyses.ask_of_man man in let r = assign_to_global_wrapper ask man.global man.sideg st lv (fun st v -> assign_from_globals_wrapper ask man.global st simplified_e (fun apr' e' -> - if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pretty v d_exp e' d_plainexp e'; - if M.tracing then M.trace "relation" "st: %a" RD.pretty apr'; + if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pp v CilType.Exp.pp e' CilType.Exp.pp e'; + if M.tracing then M.trace "relation" "st: %a" RD.pp apr'; let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in let r' = assert_type_bounds ask r v in - if M.tracing then M.traceu "relation" "-> %a" RD.pretty r'; + if M.tracing then M.traceu "relation" "-> %a" RD.pp r'; r' ) ) in - if M.tracing then M.traceu "relation" "-> %a" D.pretty r; + if M.tracing then M.traceu "relation" "-> %a" D.pp r; r let branch man e b = @@ -331,7 +331,7 @@ struct | Some (Arg _) when not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *) | _ -> false (* keep everything else (just added args, globals, global privs) *) ); - if M.tracing then M.tracel "combine" "relation enter newd: %a" RD.pretty new_rel; + if M.tracing then M.tracel "combine" "relation enter newd: %a" RD.pp new_rel; new_rel let enter man r f args = @@ -386,11 +386,11 @@ struct let st = man.local in let reachable_from_args = reachable_from_args man args in let fundec = Node.find_fundec man.node in - if M.tracing then M.tracel "combine-rel" "relation f: %a" CilType.Varinfo.pretty f.svar; - if M.tracing then M.tracel "combine-rel" "relation formals: %a" (d_list "," CilType.Varinfo.pretty) f.sformals; - if M.tracing then M.tracel "combine-rel" "relation args: %a" (d_list "," d_exp) args; - if M.tracing then M.tracel "combine-rel" "relation st: %a" D.pretty st; - if M.tracing then M.tracel "combine-rel" "relation fun_st: %a" D.pretty fun_st; + if M.tracing then M.tracel "combine-rel" "relation f: %a" CilType.Varinfo.pp f.svar; + if M.tracing then M.tracel "combine-rel" "relation formals: %a" (d_list "," CilType.Varinfo.pp) f.sformals; + if M.tracing then M.tracel "combine-rel" "relation args: %a" (d_list "," CilType.Exp.pp) args; + if M.tracing then M.tracel "combine-rel" "relation st: %a" D.pp st; + if M.tracing then M.tracel "combine-rel" "relation fun_st: %a" D.pp fun_st; let new_fun_rel = RD.add_vars fun_st.rel (RD.vars st.rel) in let arg_substitutes = let filter_actuals (x,e) = @@ -416,7 +416,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 (GobApron.Var.pretty ())) arg_vars; + if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (GobApron.Var.pp ())) 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 @@ -430,7 +430,7 @@ struct ) in let unify_rel = RD.unify new_rel new_fun_rel in (* TODO: unify_with *) - if M.tracing then M.tracel "combine-rel" "relation unifying %a %a = %a" RD.pretty new_rel RD.pretty new_fun_rel RD.pretty unify_rel; + if M.tracing then M.tracel "combine-rel" "relation unifying %a %a = %a" RD.pp new_rel RD.pp new_fun_rel RD.pp unify_rel; {fun_st with rel = unify_rel} let combine_assign man r fe f args fc fun_st (f_ask : Queries.ask) = @@ -640,10 +640,10 @@ struct in match q with | EvalInt e -> - if M.tracing then M.traceli "evalint" "relation query %a (%a)" d_exp e d_plainexp e; - if M.tracing then M.trace "evalint" "relation st: %a" D.pretty man.local; + if M.tracing then M.traceli "evalint" "relation query %a (%a)" CilType.Exp.pp e CilType.Exp.pp e; + if M.tracing then M.trace "evalint" "relation st: %a" D.pp man.local; let r = eval_int e (no_overflow (Analyses.ask_of_man man) e) in - if M.tracing then M.traceu "evalint" "relation query %a -> %a" d_exp e ID.pretty r; + if M.tracing then M.traceu "evalint" "relation query %a -> %a" CilType.Exp.pp e ID.pp r; r | Queries.IterSysVars (vq, vf) -> let vf' x = vf (Obj.repr x) in @@ -720,9 +720,9 @@ struct in match q with | EvalInt e -> - if M.tracing then M.traceli "relation" "evalint query %a (%a), man %a" d_exp e d_plainexp e D.pretty man.local; + if M.tracing then M.traceli "relation" "evalint query %a (%a), man %a" CilType.Exp.pp e CilType.Exp.pp e D.pp man.local; let r = eval_int e (no_overflow (dummyask) e) in - if M.tracing then M.trace "relation" "evalint response %a -> %a" d_exp e ValueDomainQueries.ID.pretty r; + if M.tracing then M.trace "relation" "evalint response %a -> %a" CilType.Exp.pp e ValueDomainQueries.ID.pp r; r |_ -> Queries.Result.top q in diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index cba9084ad7..1b18a7c599 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -893,20 +893,20 @@ struct let lock_get_m oct local_m get_m = let joined = LRD.join local_m get_m in - if M.tracing then M.traceli "relationpriv" "lock_get_m:\n get=%a\n joined=%a" LRD.pretty get_m LRD.pretty joined; + if M.tracing then M.traceli "relationpriv" "lock_get_m:\n get=%a\n joined=%a" LRD.pp get_m LRD.pp joined; let r = LRD.fold (fun _ -> RD.meet) joined (RD.top ()) in - if M.tracing then M.trace "relationpriv" "meet=%a" RD.pretty r; + if M.tracing then M.trace "relationpriv" "meet=%a" RD.pp r; let r = RD.meet oct r in - if M.tracing then M.traceu "relationpriv" "-> %a" RD.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RD.pp r; r let lock oct local_m get_m = - if M.tracing then M.traceli "relationpriv" "cluster lock: local=%a" LRD.pretty local_m; + if M.tracing then M.traceli "relationpriv" "cluster lock: local=%a" LRD.pp local_m; let r = lock_get_m oct local_m get_m in (* is_bot check commented out because it's unnecessarily expensive *) (* if RD.is_bot_env r then failwith "DownwardClosedCluster.lock: not downward closed?"; *) - if M.tracing then M.traceu "relationpriv" "-> %a" RD.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RD.pp r; r let unlock w oct_side = @@ -989,7 +989,7 @@ struct (lad, lad_weak) let lock oct (local_m, _) (get_m, get_m') = - if M.tracing then M.traceli "relationpriv" "cluster lock: local=%a" LRD1.pretty local_m; + if M.tracing then M.traceli "relationpriv" "cluster lock: local=%a" LRD1.pp local_m; let r = let locked = DCCluster.lock_get_m oct local_m get_m in if RD.is_bot_env locked then ( @@ -1002,7 +1002,7 @@ struct else locked in - if M.tracing then M.traceu "relationpriv" "-> %a" RD.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RD.pp r; r let unlock w oct_side = @@ -1044,15 +1044,15 @@ struct let get_m_with_mutex_inits inits ask getg m = let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in - if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n get=%a" LockDomain.MustLock.pretty m LRD.pretty get_m; + if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n get=%a" LockDomain.MustLock.pp m LRD.pp get_m; let r = let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in let get_mutex_inits' = Cluster.keep_only_protected_globals ask m get_mutex_inits in let get_mutex_inits' = Cluster.filter_clusters inits get_mutex_inits' in - if M.tracing then M.trace "relationpriv" "inits=%a\n inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits'; + if M.tracing then M.trace "relationpriv" "inits=%a\n inits'=%a" LRD.pp get_mutex_inits LRD.pp get_mutex_inits'; LRD.join get_m get_mutex_inits' in - if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pp r; r let atomic_mutex = LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var @@ -1067,15 +1067,15 @@ struct else get_relevant_writes_nofilter ask @@ G.mutex @@ getg (V.global g) in - if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n get=%a" CilType.Varinfo.pretty g LRD.pretty get_mutex_global_g; + if M.tracing then M.traceli "relationpriv" "get_mutex_global_g_with_mutex_inits %a\n get=%a" CilType.Varinfo.pp g LRD.pp get_mutex_global_g; let r = let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in let get_mutex_inits' = Cluster.keep_global g get_mutex_inits in let get_mutex_inits' = Cluster.filter_clusters inits get_mutex_inits' in - if M.tracing then M.trace "relationpriv" "inits=%a\n inits'=%a" LRD.pretty get_mutex_inits LRD.pretty get_mutex_inits'; + if M.tracing then M.trace "relationpriv" "inits=%a\n inits'=%a" LRD.pp get_mutex_inits LRD.pp get_mutex_inits'; LRD.join get_mutex_global_g get_mutex_inits' in - if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pp r; r let get_mutex_global_g_with_mutex_inits_atomic inits ask getg = @@ -1349,147 +1349,147 @@ struct module RelComponents = RelationDomain.RelComponents (RD) (D) let read_global ask getg st g x = - if M.tracing then M.traceli "relationpriv" "read_global %a %a" CilType.Varinfo.pretty g CilType.Varinfo.pretty x; - if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; + if M.tracing then M.traceli "relationpriv" "read_global %a %a" CilType.Varinfo.pp g CilType.Varinfo.pp x; + if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r; r in let r = Priv.read_global ask getg st g x in - if M.tracing then M.traceu "relationpriv" "-> %a" RD.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RD.pp r; r let write_global ?invariant ask getg sideg st g x = - if M.tracing then M.traceli "relationpriv" "write_global %a %a" CilType.Varinfo.pretty g CilType.Varinfo.pretty x; - if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; + if M.tracing then M.traceli "relationpriv" "write_global %a %a" CilType.Varinfo.pp g CilType.Varinfo.pp x; + if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r; r in let sideg x v = - if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v; + if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v; sideg x v in let r = write_global ?invariant ask getg sideg st g x in - if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r; r let lock ask getg st m = - if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.MustLock.pretty m; - if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; + if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.MustLock.pp m; + if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r; r in let r = lock ask getg st m in - if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r; r let unlock ask getg sideg st m = - if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.MustLock.pretty m; - if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; + if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.MustLock.pp m; + if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r; r in let sideg x v = - if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v; + if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v; sideg x v in let r = unlock ask getg sideg st m in - if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r; r let enter_multithreaded ask getg sideg st = if M.tracing then M.traceli "relationpriv" "enter_multithreaded"; - if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; + if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r; r in let sideg x v = - if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v; + if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v; sideg x v in let r = enter_multithreaded ask getg sideg st in - if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r; r let threadenter ask getg st = if M.tracing then M.traceli "relationpriv" "threadenter"; - if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; + if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r; r in let r = threadenter ask getg st in - if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r; r let sync ask getg sideg st reason = if M.tracing then M.traceli "relationpriv" "sync"; - if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; + if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r; r in let sideg x v = - if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v; + if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v; sideg x v in let r = sync ask getg sideg st reason in - if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r; r let escape node ask getg sideg st vs = if M.tracing then M.traceli "relationpriv" "escape"; - if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; + if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r; r in let sideg x v = - if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v; + if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v; sideg x v in let r = escape node ask getg sideg st vs in - if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r; r let thread_join ?force ask getg e st = if M.tracing then M.traceli "relationpriv" "thread_join"; - if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; + if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r; r in let r = thread_join ?force ask getg e st in - if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r; r let thread_return ask getg sideg tid st = if M.tracing then M.traceli "relationpriv" "thread_return"; - if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st; + if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "relationpriv" "getg %a -> %a" V.pp x G.pp r; r in let sideg x v = - if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pretty x G.pretty v; + if M.tracing then M.trace "relationpriv" "sideg %a %a" V.pp x G.pp v; sideg x v in let r = thread_return ask getg sideg tid st in - if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pretty r; + if M.tracing then M.traceu "relationpriv" "-> %a" RelComponents.pp r; r end diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 3cde51b49b..132c7eabe9 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -293,7 +293,7 @@ struct (* Evaluate binop for two abstract values: *) let evalbinop_base ~man (op: binop) (t1:typ) (a1:value) (t2:typ) (a2:value) (t:typ) :value = - if M.tracing then M.tracel "eval" "evalbinop %a %a %a" d_binop op VD.pretty a1 VD.pretty a2; + if M.tracing then M.tracel "eval" "evalbinop %a %a %a" d_binop op VD.pp a1 VD.pp a2; (* We define a conversion function for the easy cases when we can just use * the integer domain operations. *) let bool_top ik = ID.(join (of_int ik Z.zero) (of_int ik Z.one)) in @@ -417,7 +417,7 @@ struct let ay = AD.choose y in let handle_address_is_multiple addr = begin match Addr.to_var addr with | Some v when man.ask (Q.IsMultiple v) -> - if M.tracing then M.tracel "addr" "IsMultiple %a" CilType.Varinfo.pretty v; + if M.tracing then M.tracel "addr" "IsMultiple %a" CilType.Varinfo.pp v; None | _ -> Some true @@ -425,7 +425,7 @@ struct in match Addr.semantic_equal ax ay with | Some true -> - if M.tracing then M.tracel "addr" "semantic_equal %a %a" AD.pretty x AD.pretty y; + if M.tracing then M.tracel "addr" "semantic_equal %a %a" AD.pp x AD.pp y; handle_address_is_multiple ax | Some false -> Some false | None -> None @@ -527,7 +527,7 @@ struct (* get hold of the variable value, either from local or global state *) let var = get_var ~man st x in let v = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (fun x -> get ~man st x exp) var offs exp (Some (Var x, Offs.to_cil_offset offs)) x.vtype in - if M.tracing then M.tracec "get" "var = %a, %a = %a" VD.pretty var AD.pretty (AD.of_mval (x, offs)) VD.pretty v; + if M.tracing then M.tracec "get" "var = %a, %a = %a" VD.pp var AD.pp (AD.of_mval (x, offs)) VD.pp v; if full then var else match v with | Blob (c,s,_) -> c | x -> x @@ -549,7 +549,7 @@ struct * For the exp argument it is always ok to put None. This means not using precise information about * which part of an array is involved. *) and get ~man ?top ?full (st: store) (addrs:address) (exp:exp option) : value = - if M.tracing then M.traceli "get" "Address: %a\nState: %a" AD.pretty addrs CPA.pretty st.cpa; + if M.tracing then M.traceli "get" "Address: %a\nState: %a" AD.pp addrs CPA.pp st.cpa; (* Finding a single varinfo*offset pair *) let res = (* We form the collecting function by joining *) @@ -565,7 +565,7 @@ struct let f x a = VD.join (c @@ get_addr ~man ?top ?full st x exp) a in (* Finally we join over all the addresses in the set. *) AD.fold f addrs (VD.bot ()) in - if M.tracing then M.traceu "get" "Result: %a" VD.pretty res; + if M.tracing then M.traceu "get" "Result: %a" VD.pp res; res @@ -590,7 +590,7 @@ struct let rec reachable_from_value ask (value: value) (t: typ) (description: string) = let empty = AD.empty () in - if M.tracing then M.trace "reachability" "Checking value %a" VD.pretty value; + if M.tracing then M.trace "reachability" "Checking value %a" VD.pp value; match value with | Top -> if not (VD.is_immediate_type t) then M.info ~category:Unsound "Unknown value in %s could be an escaped pointer address!" description; empty @@ -617,9 +617,9 @@ struct * all pointers within a structure should be considered, but we don't follow * pointers. We return a flattend representation, thus simply an address (set). *) let reachable_from_addr ~man st (addr: Addr.t): address = - if M.tracing then M.tracei "reachability" "Checking for %a" Addr.pretty addr; + if M.tracing then M.tracei "reachability" "Checking for %a" Addr.pp addr; let res = reachable_from_value (Analyses.ask_of_man man) (get_addr ~man st addr None) (Addr.type_of addr) (Addr.show addr) in - if M.tracing then M.traceu "reachability" "Reachable addresses: %a" AD.pretty res; + if M.tracing then M.traceu "reachability" "Reachable addresses: %a" AD.pp res; res (* The code for getting the variables reachable from the list of parameters. @@ -627,7 +627,7 @@ struct * addresses, as both AD elements abstracting individual (ambiguous) addresses * and the workset of visited addresses. *) let reachable_vars ~man (st: store) (args: address): address = - if M.tracing then M.traceli "reachability" "Checking reachable arguments from %a!" AD.pretty args; + if M.tracing then M.traceli "reachability" "Checking reachable arguments from %a!" AD.pp args; let empty = AD.empty () in (* We begin looking at the parameters: *) let workset = ref args in @@ -643,7 +643,7 @@ struct workset := AD.diff collected !visited done; (* Return the list of elements that have been visited. *) - if M.tracing then M.traceu "reachability" "All reachable vars: %a" AD.pretty !visited; + if M.tracing then M.traceu "reachability" "All reachable vars: %a" AD.pp !visited; !visited let reachable_vars ~man st args = Timing.wrap "reachability" (reachable_vars ~man st) args @@ -757,7 +757,7 @@ struct (* The evaluation function as mutually recursive eval_lv & eval_rv *) let rec eval_rv ~(man: _ man) (st: store) (exp:exp): value = - if M.tracing then M.traceli "evalint" "base eval_rv %a" d_exp exp; + if M.tracing then M.traceli "evalint" "base eval_rv %a" CilType.Exp.pp exp; let r = (* we have a special expression that should evaluate to top ... *) if exp = MyCFG.unknown_exp then @@ -765,7 +765,7 @@ struct else eval_rv_ask_evalint ~man st exp in - if M.tracing then M.traceu "evalint" "base eval_rv %a -> %a" d_exp exp VD.pretty r; + if M.tracing then M.traceu "evalint" "base eval_rv %a -> %a" CilType.Exp.pp exp VD.pp r; r (** Evaluate expression using EvalInt query. @@ -774,13 +774,13 @@ struct Non-integer expression just delegate to next eval_rv function. *) and eval_rv_ask_evalint ~man st exp = let eval_next () = eval_rv_no_ask_evalint ~man st exp in - if M.tracing then M.traceli "evalint" "base eval_rv_ask_evalint %a" d_exp exp; + if M.tracing then M.traceli "evalint" "base eval_rv_ask_evalint %a" CilType.Exp.pp exp; let r:value = match Cilfacade.typeOf exp with | typ when Cil.isIntegralType typ && not (Cil.isConstant exp) -> (* don't EvalInt integer constants, base can do them precisely itself *) - if M.tracing then M.traceli "evalint" "base ask EvalInt %a" d_exp exp; + if M.tracing then M.traceli "evalint" "base ask EvalInt %a" CilType.Exp.pp exp; let a = man.ask (Q.EvalInt exp) in (* through queries includes eval_next, so no (exponential) branching is necessary *) - if M.tracing then M.traceu "evalint" "base ask EvalInt %a -> %a" d_exp exp Queries.ID.pretty a; + if M.tracing then M.traceu "evalint" "base ask EvalInt %a -> %a" CilType.Exp.pp exp Queries.ID.pp a; begin match a with | `Bot -> eval_next () (* Base EvalInt returns bot on incorrect type (e.g. pthread_t); ignore and continue. *) (* | x -> Some (Int x) *) @@ -790,7 +790,7 @@ struct | exception Cilfacade.TypeOfError _ (* Bug: typeOffset: Field on a non-compound *) | _ -> eval_next () in - if M.tracing then M.traceu "evalint" "base eval_rv_ask_evalint %a -> %a" d_exp exp VD.pretty r; + if M.tracing then M.traceu "evalint" "base eval_rv_ask_evalint %a -> %a" CilType.Exp.pp exp VD.pp r; r (** Evaluate expression without EvalInt query on outermost expression. @@ -815,13 +815,13 @@ struct Subexpressions delegate to [eval_rv], which may use queries on them. *) and eval_rv_base ~man (st: store) (exp:exp): value = let eval_rv = eval_rv_back_up in - if M.tracing then M.traceli "evalint" "base eval_rv_base %a" d_exp exp; + if M.tracing then M.traceli "evalint" "base eval_rv_base %a" CilType.Exp.pp exp; let binop_remove_same_casts ~extra_is_safe ~e1 ~e2 ~t1 ~t2 ~c1 ~c2 = let te1 = Cilfacade.typeOf e1 in let te2 = Cilfacade.typeOf e2 in let both_arith_type = isArithmeticType te1 && isArithmeticType te2 in let is_safe = (extra_is_safe || VD.is_statically_safe_cast t1 te1 && VD.is_statically_safe_cast t2 te2) && not both_arith_type in - if M.tracing then M.tracel "cast" "remove cast on both sides for %a? -> %b" d_exp exp is_safe; + if M.tracing then M.tracel "cast" "remove cast on both sides for %a? -> %b" CilType.Exp.pp exp is_safe; if is_safe then ( (* we can ignore the casts if the casts can't change the value *) let e1 = if isArithmeticType te1 then c1 else e1 in let e2 = if isArithmeticType te2 then c2 else e2 in @@ -969,7 +969,7 @@ struct | AddrOfLabel _ -> VD.top () in - if M.tracing then M.traceu "evalint" "base eval_rv_base %a -> %a" d_exp exp VD.pretty r; + if M.tracing then M.traceu "evalint" "base eval_rv_base %a -> %a" CilType.Exp.pp exp VD.pp r; r and eval_rv_base_lval ~eval_lv ~man (st: store) (exp: exp) (lv: lval): value = @@ -995,7 +995,7 @@ struct | Addr (x, o) -> begin let at = Addr.Mval.type_of (x, o) in - if M.tracing then M.tracel "evalint" "cast_ok %a %a %a" Addr.pretty (Addr (x, o)) CilType.Typ.pretty (Cil.unrollType x.vtype) CilType.Typ.pretty at; + if M.tracing then M.tracel "evalint" "cast_ok %a %a %a" Addr.pp (Addr (x, o)) CilType.Typ.pp (Cil.unrollType x.vtype) CilType.Typ.pp at; if at = TVoid [] then (* HACK: cast from alloc variable is always fine *) true else @@ -1023,7 +1023,7 @@ struct VD.top () (* upcasts not! *) in let v' = VD.cast ~kind:Internal t v in (* cast to the expected type (the abstract type might be something other than t since we don't change addresses upon casts!) *) (* TODO: proper castkind *) - if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!" VD.pretty v d_type t VD.pretty v'; + if M.tracing then M.tracel "cast" "Ptr-Deref: cast %a to %a = %a!" VD.pp v CilType.Typ.pp t VD.pp v'; let v' = VD.eval_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) (fun x -> get ~man st x (Some exp)) v' (convert_offset ~man st ofs) (Some exp) None t in (* handle offset *) v' in @@ -1047,7 +1047,7 @@ struct (* Fallback to MustBeEqual query, could get extra precision from exprelation/var_eq. *) let must_be_equal () = let r = Q.must_be_equal (Analyses.ask_of_man man) e1 e2 in - if M.tracing then M.tracel "query" "MustBeEqual (%a, %a) = %b" d_exp e1 d_exp e2 r; + if M.tracing then M.tracel "query" "MustBeEqual (%a, %a) = %b" CilType.Exp.pp e1 CilType.Exp.pp e2 r; r in match op with @@ -1156,13 +1156,13 @@ struct let eval_rv ~man (st: store) (exp:exp): value = try let r = eval_rv ~man st exp in - if M.tracing then M.tracel "eval" "eval_rv %a = %a" d_exp exp VD.pretty r; + if M.tracing then M.tracel "eval" "eval_rv %a = %a" CilType.Exp.pp exp VD.pp r; if VD.is_bot r then VD.top_value (Cilfacade.typeOf exp) else r with IntDomain.ArithmeticOnIntegerBot _ -> ValueDomain.Compound.top_value (Cilfacade.typeOf exp) let query_evalint ~man st e = - if M.tracing then M.traceli "evalint" "base query_evalint %a" d_exp e; + if M.tracing then M.traceli "evalint" "base query_evalint %a" CilType.Exp.pp e; let r = match eval_rv_no_ask_evalint ~man st e with | Int i -> `Lifted i (* cast should be unnecessary, eval_rv should guarantee right ikind already *) | Bot -> Queries.ID.top () (* out-of-scope variables cause bot, but query result should then be unknown *) @@ -1170,7 +1170,7 @@ struct | v -> M.debug ~category:Analyzer "Base EvalInt %a query answering bot instead of %a" d_exp e VD.pretty v; Queries.ID.bot () | exception (IntDomain.ArithmeticOnIntegerBot _) when not !AnalysisState.should_warn -> Queries.ID.bot () in - if M.tracing then M.traceu "evalint" "base query_evalint %a -> %a" d_exp e Queries.ID.pretty r; + if M.tracing then M.traceu "evalint" "base query_evalint %a -> %a" CilType.Exp.pp e Queries.ID.pp r; r (* Evaluate an expression containing only locals. This is needed for smart joining the partitioned arrays where man is not accessible. *) @@ -1451,7 +1451,7 @@ struct | AddrOf lval | StartOf lval -> lval_may_signed_overflow man lval in - if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp exp res; res + if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" CilType.Exp.pp exp res; res and lval_may_signed_overflow man (lval : lval) = let (host, offset) = lval in let host_may_signed_overflow = function @@ -1636,7 +1636,7 @@ struct let g: V.t = Obj.obj g in query_invariant_global man g | Q.MaySignedOverflow e -> (let res = exp_may_signed_overflow man e in - if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" d_plainexp e res; res + if M.tracing then M.trace "signed_overflow" "base exp_may_signed_overflow %a. Result = %b" CilType.Exp.pp e res; res ) | _ -> Q.Result.top q @@ -1666,9 +1666,9 @@ struct | _ -> st let update_variable x t y z = - if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a" x.vname VD.pretty y CPA.pretty z; + if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a" x.vname VD.pp y CPA.pp z; let r = update_variable x t y z in (* refers to definition above *) - if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\nresults in\n%a" x.vname VD.pretty y CPA.pretty z CPA.pretty r; + if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\nresults in\n%a" x.vname VD.pp y CPA.pp z CPA.pp r; r (* Updating a single varinfo*offset pair. NB! This function's type does @@ -1708,9 +1708,9 @@ struct else new_value in - if M.tracing then M.tracel "set" "update_one_addr: start with '%a' (type '%a') \nstate:%a" AD.pretty (AD.of_mval (x,offs)) d_type x.vtype D.pretty st; + if M.tracing then M.tracel "set" "update_one_addr: start with '%a' (type '%a') \nstate:%a" AD.pp (AD.of_mval (x,offs)) CilType.Typ.pp x.vtype D.pp st; if isFunctionType x.vtype then begin - if M.tracing then M.tracel "set" "update_one_addr: returning: '%a' is a function type " d_type x.vtype; + if M.tracing then M.tracel "set" "update_one_addr: returning: '%a' is a function type " CilType.Typ.pp x.vtype; st end else if get_bool "exp.globs_are_top" then begin @@ -1731,9 +1731,9 @@ struct Priv.read_global ask priv_getg st x in let new_value = update_offset old_value in - if M.tracing then M.tracel "set" "update_offset %a -> %a" VD.pretty old_value VD.pretty new_value; + if M.tracing then M.tracel "set" "update_offset %a -> %a" VD.pp old_value VD.pp new_value; let r = Priv.write_global ~invariant ask priv_getg (priv_sideg man.sideg) st x new_value in - if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: updated a global var '%s' \nstate:%a" x.vname D.pretty r; + if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: updated a global var '%s' \nstate:%a" x.vname D.pp r; r end else begin if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: update a local var '%s' ..." x.vname; @@ -1823,18 +1823,18 @@ struct * precise information about arrays. *) let set ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store = let lval_raw = (Option.map (fun x -> Lval x) lval_raw) in - if M.tracing then M.tracel "set" "lval: %a\nvalue: %a\nstate: %a" AD.pretty lval VD.pretty value CPA.pretty st.cpa; + if M.tracing then M.tracel "set" "lval: %a\nvalue: %a\nstate: %a" AD.pp lval VD.pp value CPA.pp st.cpa; let update_one x store = set_addr ~man ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override store x lval_type value in try (* We start from the current state and an empty list of global deltas, * and we assign to all the different possible places: *) let nst = AD.fold update_one lval st in - (* if M.tracing then M.tracel "set" "new state1 %a" CPA.pretty nst; *) + (* if M.tracing then M.tracel "set" "new state1 %a" CPA.pp nst; *) (* If the address was definite, then we just return it. If the address * was ambiguous, we have to join it with the initial state. *) let nst = if AD.cardinal lval > 1 then D.join st nst else nst in - (* if M.tracing then M.tracel "set" "new state2 %a" CPA.pretty nst; *) + (* if M.tracing then M.tracel "set" "new state2 %a" CPA.pp nst; *) nst with (* If any of the addresses are unknown, we ignore it!?! *) @@ -1917,7 +1917,7 @@ struct let set_savetop ~man ?lval_raw ?rval_raw st adr lval_t v : store = - if M.tracing then M.tracel "set" "savetop %a %a %a" AD.pretty adr d_type lval_t VD.pretty v; + if M.tracing then M.tracel "set" "savetop %a %a %a" AD.pp adr CilType.Typ.pp lval_t VD.pp v; match v with | Top -> set ~man st adr lval_t (VD.top_value (AD.type_of adr)) ?lval_raw ?rval_raw | v -> set ~man st adr lval_t v ?lval_raw ?rval_raw @@ -2001,7 +2001,7 @@ struct | [(x,offs)] -> let t = v.vtype in let iv = VD.bot_value ~varAttr:v.vattr t in (* correct bottom value for top level variable *) - if M.tracing then M.tracel "set" "init bot value (%a): %a" d_plaintype t VD.pretty iv; + if M.tracing then M.tracel "set" "init bot value (%a): %a" d_plaintype t VD.pp iv; let nv = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) iv offs rval_val (Some (Lval lval)) lval t in (* do desired update to value *) set_savetop ~man man.local (AD.of_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *) | _ -> @@ -2018,8 +2018,8 @@ struct let valu = eval_rv ~man man.local exp in let refine () = let res = invariant man man.local exp tv in - if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a" d_exp exp Queries.ES.pretty (man.ask (Queries.EqualSet exp)); - if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a" d_exp exp Queries.ES.pretty (man.ask (Queries.CondVars exp)); + if M.tracing then M.tracec "branch" "EqualSet result for expression %a is %a" CilType.Exp.pp exp Queries.ES.pp (man.ask (Queries.EqualSet exp)); + if M.tracing then M.tracec "branch" "CondVars result for expression %a is %a" CilType.Exp.pp exp Queries.ES.pp (man.ask (Queries.CondVars exp)); if M.tracing then M.traceu "branch" "Invariant enforced!"; match man.ask (Queries.CondVars exp) with | s when Queries.ES.cardinal s = 1 -> @@ -2027,12 +2027,12 @@ struct invariant man res e tv | _ -> res in - if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a" d_exp exp VD.pretty valu; + if M.tracing then M.traceli "branch" ~subsys:["invariant"] "Evaluating branch for expression %a with value %a" CilType.Exp.pp exp VD.pp valu; (* First we want to see, if we can determine a dead branch: *) match valu with (* For a boolean value: *) | Int value -> - if M.tracing then M.traceu "branch" "Expression %a evaluated to %a" d_exp exp ID.pretty value; + if M.tracing then M.traceu "branch" "Expression %a evaluated to %a" CilType.Exp.pp exp ID.pp value; Option.map_default_delayed (fun v -> (* Eliminate the dead branch and just propagate to the true branch *) if v = tv then @@ -2069,7 +2069,7 @@ struct let st: store = man.local in match fundec.svar.vname with | "__goblint_dummy_init" -> - if M.tracing then M.trace "init" "dummy init: %a" D.pretty st; + if M.tracing then M.trace "init" "dummy init: %a" D.pp st; publish_all man `Init; (* otherfun uses __goblint_dummy_init, where we can properly side effect global initialization *) (* TODO: move into sync `Init *) @@ -2128,7 +2128,7 @@ struct ) let invalidate ~(must: bool) ?(deep=true) ~man (st:store) (exps: exp list): store = - if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]" (d_list ", " d_plainexp) exps; + if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]" (d_list ", " CilType.Exp.pp) exps; if exps <> [] then M.info ~category:Imprecise "Invalidating expressions: %a" (d_list ", " d_exp) exps; (* To invalidate a single address, we create a pair with its corresponding * top value. *) @@ -2150,7 +2150,7 @@ struct if M.tracing && exps <> [] then ( let addrs = List.map (Tuple3.first) invalids' in let vs = List.map (Tuple3.third) invalids' in - M.tracel "invalidate" "Setting addresses [%a] to values [%a]" (d_list ", " Addr.pretty) addrs (d_list ", " VD.pretty) vs + M.tracel "invalidate" "Setting addresses [%a] to values [%a]" (d_list ", " Addr.pp) addrs (d_list ", " VD.pp) vs ); (* copied from set_many *) let f (acc: store) ((lval:Addr.t),(typ:Cil.typ),(value:value)): store = @@ -2389,7 +2389,7 @@ struct (addr, AD.type_of addr) in let forks = forkfun man lv f args in - if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a" f.vname (d_list "," CilType.Varinfo.pretty) (List.map BatTuple.Tuple4.second forks); + if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a" f.vname (d_list "," CilType.Varinfo.pp) (List.map BatTuple.Tuple4.second forks); List.iter (fun (lval, f, args, multiple) -> man.spawn ~multiple lval f args) forks; let st: store = man.local in let desc = LF.find f in @@ -2817,7 +2817,7 @@ struct | Address jmp_buf -> let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (man.prev_node, man.control_context ())), false) in let r = set ~man st jmp_buf (Cilfacade.typeOf env) value in - if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a" d_exp env D.pretty st D.pretty r; + if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a" CilType.Exp.pp env D.pp st D.pp r; r | _ -> failwith "problem?!" in @@ -2870,7 +2870,7 @@ struct | Addr.Addr ((v,o) as mval) when CPA.mem v fun_st.cpa -> begin let lval_type = Addr.type_of addr in - if M.tracing then M.trace "taintPC" "updating %a; type: %a" Addr.Mval.pretty (v,o) d_type lval_type; + if M.tracing then M.trace "taintPC" "updating %a; type: %a" Addr.Mval.pp (v,o) CilType.Typ.pp lval_type; match CPA.find_opt v (fun_st.cpa) with | None -> st (* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *) @@ -2880,7 +2880,7 @@ struct | _ -> let address = AD.singleton addr in let new_val = get_mval ~man fun_st mval None in - if M.tracing then M.trace "taintPC" "update val: %a" VD.pretty new_val; + if M.tracing then M.trace "taintPC" "update val: %a" VD.pp new_val; let st' = set_savetop ~man st address lval_type new_val in (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *) Option.map_default (fun deps -> @@ -2896,7 +2896,7 @@ struct let combine_env man lval fexp f args fc au (f_ask: Queries.ask) = let combine_one (st: D.t) (fun_st: D.t) = - if M.tracing then M.tracel "combine" "%a\n%a" CPA.pretty st.cpa CPA.pretty fun_st.cpa; + if M.tracing then M.tracel "combine" "%a\n%a" CPA.pp st.cpa CPA.pp fun_st.cpa; (* This function does miscellaneous things, but the main task was to give the * handle to the global state to the state return from the function, but now * the function tries to add all the context variables back to the callee. @@ -2907,29 +2907,29 @@ struct let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in let ask = Analyses.ask_of_man man in let tainted = f_ask.f Q.MayBeTainted in - if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a" f.svar.vname AD.pretty tainted; - if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a" CPA.pretty st.cpa CPA.pretty fun_st.cpa; + if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a" f.svar.vname AD.pp tainted; + if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a" CPA.pp st.cpa CPA.pp fun_st.cpa; if AD.is_top tainted then let cpa_local = CPA.filter (fun x _ -> not (is_global ask x)) st.cpa in let cpa' = CPA.fold CPA.add cpa_noreturn cpa_local in (* add cpa_noreturn to cpa_local *) - if M.tracing then M.trace "taintPC" "combined: %a" CPA.pretty cpa'; + if M.tracing then M.trace "taintPC" "combined: %a" CPA.pp cpa'; { fun_st with cpa = cpa' } else (* remove variables from caller cpa, that are global and not in the callee cpa *) let cpa_caller = CPA.filter (fun x _ -> (not (is_global ask x)) || CPA.mem x fun_st.cpa) st.cpa in - if M.tracing then M.trace "taintPC" "cpa_caller: %a" CPA.pretty cpa_caller; + if M.tracing then M.trace "taintPC" "cpa_caller: %a" CPA.pp cpa_caller; (* add variables from callee that are not in caller yet *) let cpa_new = CPA.filter (fun x _ -> not (CPA.mem x cpa_caller)) cpa_noreturn in - if M.tracing then M.trace "taintPC" "cpa_new: %a" CPA.pretty cpa_new; + if M.tracing then M.trace "taintPC" "cpa_new: %a" CPA.pp cpa_new; let cpa_caller' = CPA.fold CPA.add cpa_new cpa_caller in - if M.tracing then M.trace "taintPC" "cpa_caller': %a" CPA.pretty cpa_caller'; + if M.tracing then M.trace "taintPC" "cpa_caller': %a" CPA.pp cpa_caller'; (* remove lvals from the tainted set that correspond to variables for which we just added a new mapping from the callee*) let tainted = AD.filter (function | Addr.Addr (v,_) -> not (CPA.mem v cpa_new) | _ -> false ) tainted in let st_combined = combine_st man {st with cpa = cpa_caller'} fun_st tainted in - if M.tracing then M.trace "taintPC" "combined: %a" CPA.pretty st_combined.cpa; + if M.tracing then M.trace "taintPC" "combined: %a" CPA.pp st_combined.cpa; { fun_st with cpa = st_combined.cpa } in let nst = add_globals st fun_st in @@ -3130,7 +3130,7 @@ struct let st: store = man.local in match e with | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *) - if M.tracing then M.tracel "priv" "LOCK EVENT %a" LockDomain.Addr.pretty addr; + if M.tracing then M.tracel "priv" "LOCK EVENT %a" LockDomain.Addr.pp addr; CommonPriv.lift_lock ask (fun st m -> Priv.lock ask (priv_getg man.global) st m ) st addr diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 1386df31aa..f751fddcd8 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -56,7 +56,7 @@ struct with Lattice.Uncomparable -> old_val let refine_lv_fallback man st lval value tv = - if M.tracing then M.tracec "invariant" "Restricting %a with %a" d_lval lval VD.pretty value; + if M.tracing then M.tracec "invariant" "Restricting %a with %a" CilType.Lval.pp lval VD.pp value; let addr = eval_lv ~man st lval in if (AD.is_top addr) then st else @@ -65,7 +65,7 @@ struct let old_val = map_oldval old_val t_lval in let old_val = if is_some_bot old_val then ( - if M.tracing then M.tracec "invariant" "%a is bot! This should not happen. Will continue with top!" d_lval lval; + if M.tracing then M.tracec "invariant" "%a is bot! This should not happen. Will continue with top!" CilType.Lval.pp lval; VD.top () ) else @@ -74,7 +74,7 @@ struct let state_with_excluded = set st addr t_lval value ~man in let value = get ~man state_with_excluded addr None in let new_val = apply_invariant ~old_val ~new_val:value in - if M.tracing then M.traceu "invariant" "New value is %a" VD.pretty new_val; + if M.tracing then M.traceu "invariant" "New value is %a" VD.pp new_val; (* make that address meet the invariant, i.e exclusion sets will be joined *) if is_some_bot new_val then ( if M.tracing then M.tracel "branch" "C The branch %B is dead!" tv; @@ -93,7 +93,7 @@ struct let v = apply_invariant ~old_val ~new_val:c' in if is_some_bot v then contra st else ( - if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; + if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" CilType.Lval.pp x VD.pp old_val VD.pp v pretty c VD.pp c'; set' x v st ) in @@ -107,9 +107,9 @@ struct let v = apply_invariant ~old_val ~new_val in if is_some_bot v then contra st else ( - if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)" CilType.Varinfo.pretty var VD.pretty old_val VD.pretty v pretty c VD.pretty c'; + if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)" CilType.Varinfo.pp var VD.pp old_val VD.pp v pretty c VD.pp c'; let r = set' (Cil.var var) v st in - if M.tracing then M.tracel "inv" "st from %a to %a" D.pretty st D.pretty r; + if M.tracing then M.tracel "inv" "st from %a to %a" D.pp st D.pp r; r ) | Mem (Lval lv), off when GobConfig.get_bool "ana.base.branch.refine-pointer-by-pointee" -> @@ -122,7 +122,7 @@ struct match base_a with | Addr base_mval -> let (lval_a:VD.t) = Address (AD.singleton base_a) in - if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" d_lval lv VD.pretty lval_a; + if M.tracing then M.tracel "inv" "Consider case of lval %a = %a" CilType.Lval.pp lv VD.pp lval_a; let st = set' lv lval_a st in let orig = PreValueDomain.Addr.Mval.add_offset base_mval original_offset in let old_val = get_mval ~man st orig None in @@ -134,7 +134,7 @@ struct if is_some_bot v then Some (D.join acc (try contra st with Analyses.Deadcode -> D.bot ())) else ( - if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c'; + if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)" CilType.Lval.pp x VD.pp old_val VD.pp v pretty c VD.pp c'; Some (D.join acc (set' x v st)) ) | _ -> None @@ -154,7 +154,7 @@ struct match (op, lval, value, tv) with (* The true-branch where x == value: *) | Eq, x, value, true -> - if M.tracing then M.tracec "invariant" "Yes, %a equals %a" d_lval x VD.pretty value; + if M.tracing then M.tracec "invariant" "Yes, %a equals %a" CilType.Lval.pp x VD.pp value; (match value with | Int n -> let ikind = Cilfacade.get_ikind_exp (Lval lval) in @@ -167,20 +167,20 @@ struct match ID.to_int n with | Some n -> (* When x != n, we can return a singleton exclusion set *) - if M.tracing then M.tracec "invariant" "Yes, %a is not %a" d_lval x GobZ.pretty n; + if M.tracing then M.tracec "invariant" "Yes, %a is not %a" CilType.Lval.pp x GobZ.pp n; let ikind = Cilfacade.get_ikind_exp (Lval lval) in `Refine (x, Int (ID.of_excl_list ikind [n])) | None -> `NotUnderstood end | Address n -> begin - if M.tracing then M.tracec "invariant" "Yes, %a is not %a" d_lval x AD.pretty n; + if M.tracing then M.tracec "invariant" "Yes, %a is not %a" CilType.Lval.pp x AD.pp n; match eval_rv_address ~man st (Lval x) with | Address a when AD.is_definite n -> `Refine (x, Address (AD.diff a n)) | Top when AD.is_null n -> `Refine (x, Address AD.not_null) | v -> - if M.tracing then M.tracec "invariant" "No address invariant for: %a != %a" VD.pretty v AD.pretty n; + if M.tracing then M.tracec "invariant" "No address invariant for: %a != %a" VD.pp v AD.pp n; `NotUnderstood end (* | Address a -> `Refine (x, value) *) @@ -200,7 +200,7 @@ struct let limit_from = if tv then ID.maximal else ID.minimal in match limit_from n with | Some n -> - if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a" d_lval x GobZ.pretty n; + if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a" CilType.Lval.pp x GobZ.pp n; `Refine (x, Int (range_from n)) | None -> `NotUnderstood end @@ -215,7 +215,7 @@ struct let limit_from = if tv then ID.maximal else ID.minimal in match limit_from n with | Some n -> - if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a" d_lval x GobZ.pretty n; + if M.tracing then M.tracec "invariant" "Yes, success! %a is not %a" CilType.Lval.pp x GobZ.pp n; `Refine (x, Int (range_from n)) | None -> `NotUnderstood end @@ -227,7 +227,7 @@ struct if M.tracing then M.trace "invariant" "Failed! (operation not supported)"; `NotUnderstood in - if M.tracing then M.traceli "invariant" "assume expression %a is %B" d_exp exp tv; + if M.tracing then M.traceli "invariant" "assume expression %a is %B" CilType.Exp.pp exp tv; let null_val (typ:typ):VD.t = match Cil.unrollType typ with | TPtr _ -> Address AD.null_ptr @@ -269,7 +269,7 @@ struct helper Ne x (null_val (Cilfacade.typeOf exp)) tv | UnOp (LNot,uexp,typ) -> derived_invariant uexp (not tv) | _ -> - if M.tracing then M.tracec "invariant" "Failed! (expression %a not understood)" d_plainexp exp; + if M.tracing then M.tracec "invariant" "Failed! (expression %a not understood)" CilType.Exp.pp exp; `NotUnderstood in match derived_invariant exp tv with @@ -285,7 +285,7 @@ struct let invariant man st exp tv: D.t = let fallback reason st = - if M.tracing then M.tracel "inv" "Can't handle %a.\n%t" d_plainexp exp reason; + if M.tracing then M.tracel "inv" "Can't handle %a.\n%t" CilType.Exp.pp exp reason; invariant_fallback man st exp tv in (* inverse values for binary operation a `op` b == c *) @@ -415,7 +415,7 @@ struct in let a' = excl b a in let b' = excl a b in - if M.tracing then M.tracel "inv" "inv_bin_int: unequal: %a and %a; ikind: %a; a': %a, b': %a" ID.pretty a ID.pretty b d_ikind ikind ID.pretty a' ID.pretty b'; + if M.tracing then M.tracel "inv" "inv_bin_int: unequal: %a and %a; ikind: %a; a': %a, b': %a" ID.pp a ID.pp b d_ikind ikind ID.pp a' ID.pp b'; meet_bin a' b' | _, _ -> a, b end @@ -578,7 +578,7 @@ struct else b | _ -> b) in - if M.tracing then M.trace "inv_float" "Div: (%a,%a) = %a yields (%a,%a)" FD.pretty a FD.pretty b FD.pretty c FD.pretty a' FD.pretty b'; + if M.tracing then M.trace "inv_float" "Div: (%a,%a) = %a yields (%a,%a)" FD.pp a FD.pp b FD.pp c FD.pp a' FD.pp b'; meet_bin a' b' | Eq | Ne as op -> let both x = x, x in @@ -737,20 +737,20 @@ struct | (BinOp (op, e1, e2, _) as e, Float _) | (BinOp (op, e1, e2, _) as e, Int _) -> let invert_binary_op c pretty c_int c_float = - if M.tracing then M.tracel "inv" "binop %a with %a %a %a == %a" d_exp e VD.pretty (eval e1 st) d_binop op VD.pretty (eval e2 st) pretty c; + if M.tracing then M.tracel "inv" "binop %a with %a %a %a == %a" CilType.Exp.pp e VD.pp (eval e1 st) d_binop op VD.pp (eval e2 st) pretty c; (match eval e1 st, eval e2 st with | Int a, Int b -> let ikind = Cilfacade.get_ikind_exp e1 in (* both operands have the same type (except for Shiftlt, Shiftrt)! *) let ikres = Cilfacade.get_ikind_exp e in (* might be different from argument types, e.g. for LT, GT, EQ, ... *) let a', b' = inv_bin_int (a, b) ikind (c_int ikres) op in - if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a" d_exp e ID.pretty (c_int ikind) ID.pretty a' ID.pretty b'; + if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a" CilType.Exp.pp e ID.pp (c_int ikind) ID.pp a' ID.pp b'; let st' = inv_exp (Int a') e1 st in let st'' = inv_exp (Int b') e2 st' in st'' | Float a, Float b -> let fkind = Cilfacade.get_fkind_exp e1 in (* both operands have the same type *) let a', b' = inv_bin_float (a, b) (c_float fkind) op in - if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a" d_exp e FD.pretty (c_float fkind) FD.pretty a' FD.pretty b'; + if M.tracing then M.tracel "inv" "binop: %a, c: %a, a': %a, b': %a" CilType.Exp.pp e FD.pp (c_float fkind) FD.pp a' FD.pp b'; let st' = inv_exp (Float a') e1 st in let st'' = inv_exp (Float b') e2 st' in st'' @@ -766,7 +766,7 @@ struct | Lval x, (Int _ | Float _ | Address _) -> (* meet x with c *) let update_lval c x c' pretty = refine_lv man st c x c' pretty exp in let t = Cil.unrollType (Cilfacade.typeOfLval x) in (* unroll type to deal with TNamed *) - if M.tracing then M.trace "invSpecial" "invariant with Lval %a, c_typed %a, type %a" d_lval x VD.pretty c_typed d_type t; + if M.tracing then M.trace "invSpecial" "invariant with Lval %a, c_typed %a, type %a" CilType.Lval.pp x VD.pp c_typed CilType.Typ.pp t; begin match c_typed with | Int c -> let c' = match t with @@ -781,7 +781,7 @@ struct begin match x, t with | (Var v, offs), TInt (ik, _) -> let tmpSpecial = man.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) in - if M.tracing then M.trace "invSpecial" "qry Result: %a" Queries.ML.pretty tmpSpecial; + if M.tracing then M.trace "invSpecial" "qry Result: %a" Queries.ML.pp tmpSpecial; begin match tmpSpecial with | `Lifted (Abs (ik, xInt)) -> let c' = ID.cast_to ~kind:Internal ik c in (* different ik! *) (* TODO: proper castkind *) @@ -816,7 +816,7 @@ struct begin match x, t with | (Var v, offs), TFloat (fk, _) -> let tmpSpecial = man.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) in - if M.tracing then M.trace "invSpecial" "qry Result: %a" Queries.ML.pretty tmpSpecial; + if M.tracing then M.trace "invSpecial" "qry Result: %a" Queries.ML.pp tmpSpecial; begin match tmpSpecial with | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st @@ -859,7 +859,7 @@ struct (* Suppressing overflow warnings as this is not a computation that comes from the program *) let res_range = (ID.cast_to ~suppress_ovwarn:true ~kind:Internal ik (ID.top_of ik_e)) in (* TODO: proper castkind *) let c' = ID.cast_to ~kind:Internal ik_e (ID.meet c res_range) in (* TODO: cast without overflow, is this right for normal invariant? *) (* TODO: proper castkind *) - if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" d_exp e d_ikind ik_e d_ikind ik ID.pretty i ID.pretty c d_ikind ik_e ID.pretty c'; + if M.tracing then M.tracel "inv" "cast: %a from %a to %a: i = %a; cast c = %a to %a = %a" CilType.Exp.pp e d_ikind ik_e d_ikind ik ID.pp i ID.pp c d_ikind ik_e ID.pp c'; inv_exp (Int c') e st else fallback (fun () -> Pretty.dprintf "CastE: %a evaluates to %a which is bigger than the type it is cast to which is %a" d_plainexp e ID.pretty i CilType.Typ.pretty t) st diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 20826195db..86b4f05def 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -216,7 +216,7 @@ struct let get_mutex_inits = getg V.mutex_inits in let is_in_Gm x _ = is_protected_by ask m x in let get_mutex_inits' = CPA.filter is_in_Gm get_mutex_inits in - if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n get_m: %a\n get_mutex_inits: %a\n get_mutex_inits': %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty get_mutex_inits CPA.pretty get_mutex_inits'; + if M.tracing then M.tracel "priv" "get_m_with_mutex_inits %a:\n get_m: %a\n get_mutex_inits: %a\n get_mutex_inits': %a" LockDomain.MustLock.pp m CPA.pp get_m CPA.pp get_mutex_inits CPA.pp get_mutex_inits'; CPA.join get_m get_mutex_inits' (** [get_m_with_mutex_inits] optimized for implementation-specialized [read_global]. *) @@ -240,7 +240,7 @@ struct let cpa' = CPA.fold (fun x v acc -> if EscapeDomain.EscapedVars.mem x escaped (* && is_unprotected ask x *) then ( - if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v; + if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a" CilType.Varinfo.pp x VD.pp v; sideg (V.global x) (CPA.singleton x v); CPA.remove x acc ) @@ -256,8 +256,8 @@ struct let cpa' = CPA.fold (fun x v acc -> if is_global ask x (* && is_unprotected ask x *) then ( - if M.tracing then M.tracel "priv" "enter_multithreaded remove %a" CilType.Varinfo.pretty x; - if M.tracing then M.tracel "priv" "ENTER MULTITHREADED SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v; + if M.tracing then M.tracel "priv" "enter_multithreaded remove %a" CilType.Varinfo.pp x; + if M.tracing then M.tracel "priv" "ENTER MULTITHREADED SIDE %a = %a" CilType.Varinfo.pp x VD.pp v; sideg (V.global x) (CPA.singleton x v); CPA.remove x acc ) @@ -317,7 +317,7 @@ struct No other privatization uses is_unprotected, so this hack is only needed here. *) let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in let cpa' = CPA.filter is_in_V get_m in - if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.MustLock.pretty m CPA.pretty cpa'; + if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a" LockDomain.MustLock.pp m CPA.pp cpa'; {st with cpa = CPA.fold CPA.add cpa' st.cpa} ) else @@ -326,7 +326,7 @@ struct let unlock ask getg sideg (st: BaseComponents (D).t) m = let is_in_Gm x _ = is_protected_by ask m x in let side_m_cpa = CPA.filter is_in_Gm st.cpa in - if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.MustLock.pretty m CPA.pretty side_m_cpa; + if M.tracing then M.tracel "priv" "PerMutexOplusPriv.unlock m=%a side_m_cpa=%a" LockDomain.MustLock.pp m CPA.pp side_m_cpa; sideg (V.mutex m) side_m_cpa; st @@ -413,7 +413,7 @@ struct CPA.find x st.cpa let read_global ask getg st x = let v = read_global ask getg st x in - if M.tracing then M.tracel "priv" "READ GLOBAL %a %B %a = %a" CilType.Varinfo.pretty x (is_unprotected ask x) CPA.pretty st.cpa VD.pretty v; + if M.tracing then M.tracel "priv" "READ GLOBAL %a %B %a = %a" CilType.Varinfo.pp x (is_unprotected ask x) CPA.pp st.cpa VD.pp v; v let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v = let cpa' = @@ -423,7 +423,7 @@ struct CPA.add x v st.cpa in if not invariant then ( - if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v; + if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pp x VD.pp v; let side_cpa = CPA.singleton x v in sideg (V.global x) side_cpa; if !earlyglobs && not (ThreadFlag.is_currently_multi ask) then @@ -444,7 +444,7 @@ struct let get_m = CPA.filter is_in_Gm get_m in let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in let meet = long_meet st.cpa get_m in - if M.tracing then M.tracel "priv" "LOCK %a:\n get_m: %a\n meet: %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty meet; + if M.tracing then M.tracel "priv" "LOCK %a:\n get_m: %a\n meet: %a" LockDomain.MustLock.pp m CPA.pp get_m CPA.pp meet; {st with cpa = meet} ) else @@ -471,12 +471,12 @@ struct let cpa' = CPA.fold (fun x v cpa -> if is_global ask x && is_unprotected ask x (* && not (VD.is_top v) *) then ( - if M.tracing then M.tracel "priv" "SYNC SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v; + if M.tracing then M.tracel "priv" "SYNC SIDE %a = %a" CilType.Varinfo.pp x VD.pp v; sideg (V.global x) (CPA.singleton x v); CPA.remove x cpa ) else ( - if M.tracing then M.tracel "priv" "SYNC NOSIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v; + if M.tracing then M.tracel "priv" "SYNC NOSIDE %a = %a" CilType.Varinfo.pp x VD.pp v; cpa ) ) st.cpa st.cpa @@ -563,7 +563,7 @@ struct let read_global ask getg st x = let v = read_global ask getg st x in - if M.tracing then M.tracel "priv" "READ GLOBAL %a %B %a = %a" CilType.Varinfo.pretty x (is_unprotected ~protection:Weak ask x) CPA.pretty st.cpa VD.pretty v; + if M.tracing then M.tracel "priv" "READ GLOBAL %a %B %a = %a" CilType.Varinfo.pp x (is_unprotected ~protection:Weak ask x) CPA.pp st.cpa VD.pp v; v let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v = @@ -575,7 +575,7 @@ struct else CPA.add x v st.cpa in - if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v; + if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a" CilType.Varinfo.pp x VD.pp v; let digest = Digest.current ask in let sidev = GMutex.singleton digest (CPA.singleton x v) in let l' = L.add lm (CPA.singleton x v) l in @@ -675,7 +675,7 @@ struct sideg V.mutex_inits (G.create_mutex sidev); let cpa' = CPA.fold (fun x v acc -> if EscapeDomain.EscapedVars.mem x escaped (* && is_unprotected ask x *) then ( - if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a" CilType.Varinfo.pretty x VD.pretty v; + if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a" CilType.Varinfo.pp x VD.pp v; let sidev = GMutex.singleton digest (CPA.singleton x v) in sideg (V.global x) (G.create_global sidev); CPA.remove x acc @@ -1533,10 +1533,10 @@ struct else GWeak.find lockset_init weaks in - if M.tracing then M.trace "priv" "d_cpa: %a" VD.pretty d_cpa; - if M.tracing then M.trace "priv" "d_sync: %a" VD.pretty d_sync; - if M.tracing then M.trace "priv" "d_weak: %a" VD.pretty d_weak; - if M.tracing then M.trace "priv" "d_init: %a" VD.pretty d_init; + if M.tracing then M.trace "priv" "d_cpa: %a" VD.pp d_cpa; + if M.tracing then M.trace "priv" "d_sync: %a" VD.pp d_sync; + if M.tracing then M.trace "priv" "d_weak: %a" VD.pp d_weak; + if M.tracing then M.trace "priv" "d_init: %a" VD.pp d_init; let d_weak = VD.join d_weak d_init in let d = VD.join d_cpa (VD.join d_sync d_weak) in d @@ -1708,9 +1708,9 @@ struct acc ) weaks (VD.bot ()) in - if M.tracing then M.trace "priv" "d_cpa: %a" VD.pretty d_cpa; - if M.tracing then M.trace "priv" "d_sync: %a" VD.pretty d_sync; - if M.tracing then M.trace "priv" "d_weak: %a" VD.pretty d_weak; + if M.tracing then M.trace "priv" "d_cpa: %a" VD.pp d_cpa; + if M.tracing then M.trace "priv" "d_sync: %a" VD.pp d_sync; + if M.tracing then M.trace "priv" "d_weak: %a" VD.pp d_weak; let d = VD.join d_cpa (VD.join d_sync d_weak) in d @@ -1742,11 +1742,11 @@ struct let s = MustLockset.remove m (current_lockset ask) in let (w, p) = st.priv in let p' = P.map (fun s' -> MinLocksets.add s s') p in - if M.tracing then M.traceli "priv" "unlock %a %a" LockDomain.MustLock.pretty m CPA.pretty st.cpa; + if M.tracing then M.traceli "priv" "unlock %a %a" LockDomain.MustLock.pp m CPA.pp st.cpa; let side_gsyncw = CPA.fold (fun x v acc -> if is_global ask x then ( let w_x = W.find x w in - if M.tracing then M.trace "priv" "gsyncw %a %a %a" CilType.Varinfo.pretty x VD.pretty v MinLocksets.pretty w_x; + if M.tracing then M.trace "priv" "gsyncw %a %a %a" CilType.Varinfo.pp x VD.pp v MinLocksets.pp w_x; MinLocksets.fold (fun w acc -> let v = distr_init getg x v in GSyncW.add w (CPA.add x v (GSyncW.find w acc)) acc @@ -1755,7 +1755,7 @@ struct acc ) st.cpa (GSyncW.bot ()) in - if M.tracing then M.traceu "priv" "unlock %a %a" LockDomain.MustLock.pretty m GSyncW.pretty side_gsyncw; + if M.tracing then M.traceu "priv" "unlock %a %a" LockDomain.MustLock.pp m GSyncW.pp side_gsyncw; sideg (V.mutex m) (UnwrappedG.create_sync (GSync.singleton s side_gsyncw)); {st with priv = (w, p')} @@ -2050,109 +2050,109 @@ struct module BaseComponents = BaseComponents (D) let read_global ask getg st x = - if M.tracing then M.traceli "priv" "read_global %a" CilType.Varinfo.pretty x; - if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st; + if M.tracing then M.traceli "priv" "read_global %a" CilType.Varinfo.pp x; + if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r; r in let v = Priv.read_global ask getg st x in - if M.tracing then M.traceu "priv" "-> %a" VD.pretty v; + if M.tracing then M.traceu "priv" "-> %a" VD.pp v; v let write_global ?invariant ask getg sideg st x v = - if M.tracing then M.traceli "priv" "write_global %a %a" CilType.Varinfo.pretty x VD.pretty v; - if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st; + if M.tracing then M.traceli "priv" "write_global %a %a" CilType.Varinfo.pp x VD.pp v; + if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r; r in let sideg x v = - if M.tracing then M.trace "priv" "sideg %a %a" V.pretty x G.pretty v; + if M.tracing then M.trace "priv" "sideg %a %a" V.pp x G.pp v; sideg x v in let r = write_global ?invariant ask getg sideg st x v in - if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r; + if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r; r let lock ask getg st m = - if M.tracing then M.traceli "priv" "lock %a" LockDomain.MustLock.pretty m; - if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st; + if M.tracing then M.traceli "priv" "lock %a" LockDomain.MustLock.pp m; + if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r; r in let r = lock ask getg st m in - if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r; + if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r; r let unlock ask getg sideg st m = - if M.tracing then M.traceli "priv" "unlock %a" LockDomain.MustLock.pretty m; - if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st; + if M.tracing then M.traceli "priv" "unlock %a" LockDomain.MustLock.pp m; + if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r; r in let sideg x v = - if M.tracing then M.trace "priv" "sideg %a %a" V.pretty x G.pretty v; + if M.tracing then M.trace "priv" "sideg %a %a" V.pp x G.pp v; sideg x v in let r = unlock ask getg sideg st m in - if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r; + if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r; r let enter_multithreaded ask getg sideg st = if M.tracing then M.traceli "priv" "enter_multithreaded"; - if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st; + if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r; r in let sideg x v = - if M.tracing then M.trace "priv" "sideg %a %a" V.pretty x G.pretty v; + if M.tracing then M.trace "priv" "sideg %a %a" V.pp x G.pp v; sideg x v in let r = enter_multithreaded ask getg sideg st in - if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r; + if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r; r let threadenter ask st = if M.tracing then M.traceli "priv" "threadenter"; - if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st; + if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st; let r = threadenter ask st in - if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r; + if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r; r let sync ask getg sideg st reason = if M.tracing then M.traceli "priv" "sync"; - if M.tracing then M.trace "priv" "st: %a" BaseComponents.pretty st; + if M.tracing then M.trace "priv" "st: %a" BaseComponents.pp st; let getg x = let r = getg x in - if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r; r in let sideg x v = - if M.tracing then M.trace "priv" "sideg %a %a" V.pretty x G.pretty v; + if M.tracing then M.trace "priv" "sideg %a %a" V.pp x G.pp v; sideg x v in let r = sync ask getg sideg st reason in - if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pretty r; + if M.tracing then M.traceu "priv" "-> %a" BaseComponents.pp r; r let invariant_global ask getg g = - if M.tracing then M.traceli "priv" "invariant_global %a" V.pretty g; + if M.tracing then M.traceli "priv" "invariant_global %a" V.pp g; let getg x = let r = getg x in - if M.tracing then M.trace "priv" "getg %a -> %a" V.pretty x G.pretty r; + if M.tracing then M.trace "priv" "getg %a -> %a" V.pp x G.pp r; r in let r = invariant_global ask getg g in - if M.tracing then M.traceu "priv" "-> %a" Invariant.pretty r; + if M.tracing then M.traceu "priv" "-> %a" Invariant.pp r; r end diff --git a/src/analyses/c2poAnalysis.ml b/src/analyses/c2poAnalysis.ml index b5bff3431a..0a18675206 100644 --- a/src/analyses/c2poAnalysis.ml +++ b/src/analyses/c2poAnalysis.ml @@ -61,7 +61,7 @@ struct let f a prop = try let exp = T.prop_to_cil prop in (* May raise UnsupportedCilExpression *) - if M.tracing then M.trace "c2po-invariant" "Adding invariant: %a" d_exp exp; + if M.tracing then M.trace "c2po-invariant" "Adding invariant: %a" CilType.Exp.pp exp; Invariant.(a && of_exp exp) with T.UnsupportedCilExpression _ -> a @@ -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: %s; expr: %s + %s. \nTo_cil: lval: %a; expr: %a\n" (T.show lterm) (T.show rterm) (Z.to_string roffset) CilType.Exp.pp (T.to_cil lterm) CilType.Exp.pp (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 @@ -126,7 +126,7 @@ struct We have to forget all the information we had. This should almost never happen. Except if the left hand side is a complicated expression like myStruct.field1[i]->field2[z+k], and Goblint can't infer the offset.*) - if M.tracing then M.trace "c2po-invalidate" "Invalidate lval: %a" d_lval lval; + if M.tracing then M.trace "c2po-invalidate" "Invalidate lval: %a" CilType.Lval.pp lval; C2PODomain.top () let assign ctx lval expr = @@ -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: %s.\n" CilType.Lval.pp lval CilType.Exp.pp expr (D.show 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: %s; is_bot: %b\n" CilType.Exp.pp e pos (show_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: %s; result: %s\n" CilType.Exp.pp (BatOption.default (MayBeEqual.dummy_lval_print (TVoid [])) exp_opt) (D.show ctx.local) (D.show 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 = Cil.var (Var.dummy_varinfo (TVoid [])) 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: %s; state_with_ghosts: %s\n" CilType.Lval.pp lval (D.show ctx.local) (C2PODomain.show state_with_ghosts); end; (* remove callee vars that are not reachable and not global *) let reachable_variables = @@ -285,7 +285,7 @@ struct (*remove all variables that were tainted by the function*) let tainted = f_ask.f (MayBeTainted) in - if M.tracing then M.trace "c2po-tainted" "combine_env1: %a\n" MayBeEqual.AD.pretty tainted; + if M.tracing then M.trace "c2po-tainted" "combine_env1: %a\n" MayBeEqual.AD.pp tainted; let local = D.remove_tainted_terms caller_ask tainted state_with_assignments.data in let local = data_to_t local in @@ -297,7 +297,7 @@ struct if M.tracing then begin let dummy_lval = Cil.var (Var.dummy_varinfo (TVoid[])) 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: %s; f_state: %s; meeting everything: %s\n" CilType.Lval.pp lval (D.show ctx.local) (D.show f_d) (C2PODomain.show d) end; `Lifted d diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml index b504750a85..f6e4e3e7ac 100644 --- a/src/analyses/condVars.ml +++ b/src/analyses/condVars.ml @@ -108,7 +108,7 @@ struct let save_expr lval expr = match mustPointTo man (AddrOf lval) with | Some clval -> - if M.tracing then M.tracel "condvars" "CondVars: saving %a = %a" Mval.Exp.pretty clval d_exp expr; + if M.tracing then M.tracel "condvars" "CondVars: saving %a = %a" Mval.Exp.pp clval CilType.Exp.pp expr; D.add clval (D.V.singleton expr) d (* if lval must point to clval, add expr *) | None -> d in diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index b972195bad..a4a637fa64 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -213,9 +213,9 @@ struct let oman' : (S.D.t, S.G.t, S.C.t, S.V.t) man = inner_man "do_emits" ~splits ~post_all oman'' n od in n, Obj.repr @@ S.event man' e oman' in - if M.tracing then M.traceli "event" "%a\n before: %a" Events.pretty e D.pretty man.local; + if M.tracing then M.traceli "event" "%a\n before: %a" Events.pp e D.pp man.local; let d, q = map_deadcode f @@ spec_list2 man.local oman.local in - if M.tracing then M.traceu "event" "%a\n after:%a" Events.pretty e D.pretty d; + if M.tracing then M.traceu "event" "%a\n after:%a" Events.pp e D.pp d; do_sideg man !sides; do_spawns man !spawns; do_splits man d !splits !emits; @@ -265,7 +265,7 @@ struct (* Explicitly polymorphic type required here for recursive GADT call in ask. *) and query': type a. querycache:Obj.t Queries.Hashtbl.t -> Queries.Set.t -> (D.t, G.t, C.t, V.t) man -> a Queries.t -> a Queries.result = fun ~querycache asked man q -> let anyq = Queries.Any q in - if M.tracing then M.traceli "query" "query %a" Queries.Any.pretty anyq; + if M.tracing then M.traceli "query" "query %a" Queries.Any.pp anyq; let r = match Queries.Hashtbl.find_option querycache anyq with | Some r -> if M.tracing then M.trace "query" "cached"; @@ -291,7 +291,7 @@ struct in (* meet results so that precision from all analyses is combined *) let res = S.query man' q in - if M.tracing then M.trace "queryanswers" "analysis %s query %a -> answer %a" (S.name ()) Queries.Any.pretty anyq Result.pretty res; + if M.tracing then M.trace "queryanswers" "analysis %s query %a -> answer %a" (S.name ()) Queries.Any.pp anyq Result.pp res; Result.meet a @@ res in match q with @@ -337,7 +337,7 @@ struct in if M.tracing then ( let module Result = (val Queries.Result.lattice q) in - M.traceu "query" "-> %a" Result.pretty r + M.traceu "query" "-> %a" Result.pp r ); r diff --git a/src/analyses/startStateAnalysis.ml b/src/analyses/startStateAnalysis.ml index ac649d59ea..7e8cf62c89 100644 --- a/src/analyses/startStateAnalysis.ml +++ b/src/analyses/startStateAnalysis.ml @@ -55,7 +55,7 @@ struct let lval = Lval (Var var, NoOffset) in let value = get_value (ask_of_man ctx) lval in let duplicated_var = to_varinfo (DuplicVar var) in - if M.tracing then M.trace "startState" "added value: var: %a; value: %a" CilType.Varinfo.pretty duplicated_var AD.pretty value; + if M.tracing then M.trace "startState" "added value: var: %a; value: %a" CilType.Varinfo.pp duplicated_var AD.pp value; D.add duplicated_var value st in (* assign function parameters *) diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml index 02a0477016..0b33878250 100644 --- a/src/analyses/symbLocks.ml +++ b/src/analyses/symbLocks.ml @@ -63,11 +63,11 @@ struct | a when not (Queries.ES.is_bot a) -> Queries.ES.add e a | _ -> Queries.ES.singleton e in - if M.tracing then M.tracel "symb_locks" "get_all_locks exps %a = %a" d_plainexp e Queries.ES.pretty exps; - if M.tracing then M.tracel "symb_locks" "get_all_locks st = %a" D.pretty st; + if M.tracing then M.tracel "symb_locks" "get_all_locks exps %a = %a" CilType.Exp.pp e Queries.ES.pp exps; + if M.tracing then M.tracel "symb_locks" "get_all_locks st = %a" D.pp st; let add_locks x xs = PS.union (get_locks x st) xs in let r = Queries.ES.fold add_locks exps (PS.empty ()) in - if M.tracing then M.tracel "symb_locks" "get_all_locks %a = %a" d_plainexp e PS.pretty r; + if M.tracing then M.tracel "symb_locks" "get_all_locks %a = %a" CilType.Exp.pp e PS.pp r; r let same_unknown_index (ask: Queries.ask) exp slocks = @@ -136,7 +136,7 @@ struct *) let one_perelem (e,a,l) xs = (* ignore (printf "one_perelem (%a,%a,%a)\n" Exp.pretty e Exp.pretty a Exp.pretty l); *) - if M.tracing then M.tracel "symb_locks" "one_perelem (%a,%a,%a)" Exp.pretty e Exp.pretty a Exp.pretty l; + if M.tracing then M.tracel "symb_locks" "one_perelem (%a,%a,%a)" Exp.pp e Exp.pp a Exp.pp l; match Exp.fold_offs (Exp.replace_base (dummyFunDec.svar,`NoOffset) e l) with | Some (v, o) -> (* ignore (printf "adding lock %s\n" l); *) diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml index 52f772ac47..07eff6d502 100644 --- a/src/analyses/taintPartialContexts.ml +++ b/src/analyses/taintPartialContexts.ml @@ -36,7 +36,7 @@ struct | _ -> false ) d in - if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a" f.svar.vname D.pretty d D.pretty d_return; + if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a" f.svar.vname D.pp d D.pp d_return; d_return @@ -45,7 +45,7 @@ struct [man.local, (D.bot ())] let combine_env man lval fexp f args fc au f_ask = - if M.tracing then M.trace "taintPC" "combine for %s in TaintPC: tainted: in function: %a before call: %a" f.svar.vname D.pretty au D.pretty man.local; + if M.tracing then M.trace "taintPC" "combine for %s in TaintPC: tainted: in function: %a before call: %a" f.svar.vname D.pp au D.pp man.local; D.union man.local au let combine_assign man (lvalOpt:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t = diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 2bf67f4bb9..e39f8bd7ec 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -36,7 +36,7 @@ struct Queries.AD.fold to_extra ad (D.empty ()) (* Ignore soundness warnings, as invalidation proper will raise them. *) | ad -> - if M.tracing then M.tracel "escape" "reachable %a: %a" d_exp e Queries.AD.pretty ad; + if M.tracing then M.tracel "escape" "reachable %a: %a" CilType.Exp.pp e Queries.AD.pp ad; D.empty () let mpt (ask: Queries.ask) e: D.t = @@ -50,7 +50,7 @@ struct AD.fold to_extra (AD.remove UnknownPtr ad) (D.empty ()) (* Ignore soundness warnings, as invalidation proper will raise them. *) | ad -> - if M.tracing then M.tracel "escape" "mpt %a: %a" d_exp e AD.pretty ad; + if M.tracing then M.tracel "escape" "mpt %a: %a" CilType.Exp.pp e AD.pp ad; D.empty () let thread_id man = @@ -174,7 +174,7 @@ struct (* not reusing fman.local to avoid unnecessarily early join of extra *) let escaped = reachable (Analyses.ask_of_man man) ptc_arg in let escaped = D.filter (fun v -> not v.vglob) escaped in - if M.tracing then M.tracel "escape" "%a: %a" d_exp ptc_arg D.pretty escaped; + if M.tracing then M.tracel "escape" "%a: %a" CilType.Exp.pp ptc_arg D.pp escaped; let thread_id = thread_id man in emit_escape_event man escaped; side_effect_escape man escaped thread_id; diff --git a/src/analyses/tmpSpecial.ml b/src/analyses/tmpSpecial.ml index fd2b6f71e3..fe2025d730 100644 --- a/src/analyses/tmpSpecial.ml +++ b/src/analyses/tmpSpecial.ml @@ -22,7 +22,7 @@ struct (* transfer functions *) let assign man (lval:lval) (rval:exp) : D.t = - if M.tracing then M.tracel "tmpSpecial" "assignment of %a" d_lval lval; + if M.tracing then M.tracel "tmpSpecial" "assignment of %a" CilType.Lval.pp lval; (* Invalidate all entrys from the map that are possibly written by the assignment *) invalidate (Analyses.ask_of_man man) (mkAddrOf lval) man.local @@ -41,7 +41,7 @@ struct (* Just dbg prints *) (if M.tracing then match lval with - | Some lv -> if M.tracing then M.tracel "tmpSpecial" "Special: %s with lval %a" f.vname d_lval lv + | Some lv -> if M.tracing then M.tracel "tmpSpecial" "Special: %s with lval %a" f.vname CilType.Lval.pp lv | _ -> if M.tracing then M.tracel "tmpSpecial" "Special: %s" f.vname); @@ -73,7 +73,7 @@ struct in - if M.tracing then M.tracel "tmpSpecial" "Result: %a" D.pretty d; + if M.tracing then M.tracel "tmpSpecial" "Result: %a" D.pp d; d diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 0c51cbaf60..bbb9f70dea 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -316,7 +316,7 @@ struct else (Messages.warn ~category:Analyzer ~msg:("Keep " ^sprint 80 (Exp.pretty () a)^" because of "^sprint 80 (Exp.pretty () b)) (); r) Messages.warn ~category:Analyzer ~msg:(sprint 80 (Exp.pretty () b) ^" changed lvalues: "^sprint 80 (Queries.LS.pretty () bls)) (); *) - if M.tracing then M.tracel "var_eq" "may_change %a %a = %B" CilType.Exp.pretty b CilType.Exp.pretty a r; + if M.tracing then M.tracel "var_eq" "may_change %a %a = %B" CilType.Exp.pp b CilType.Exp.pp a r; r (* Remove elements, that would change if the given lval would change.*) @@ -372,8 +372,8 @@ struct let lvt = unrollType @@ Cilfacade.typeOfLval lv in if M.tracing then ( M.tracel "var_eq" "add_eq is_global_var %a = %B" d_plainlval lv (is_global_var ask (Lval lv) = Some false); - M.tracel "var_eq" "add_eq interesting %a = %B" d_plainexp rv (interesting rv); - M.tracel "var_eq" "add_eq is_global_var %a = %B" d_plainexp rv (is_global_var ask rv = Some false); + M.tracel "var_eq" "add_eq interesting %a = %B" CilType.Exp.pp rv (interesting rv); + M.tracel "var_eq" "add_eq is_global_var %a = %B" CilType.Exp.pp rv (is_global_var ask rv = Some false); M.tracel "var_eq" "add_eq type %a = %B" d_plainlval lv (isIntegralType lvt || isPointerType lvt); ); if is_global_var ask (Lval lv) = Some false @@ -493,7 +493,7 @@ struct let remove_reachable ~deep ask es st = let rs = reachables ~deep ask es in - if M.tracing then M.tracel "var_eq" "remove_reachable %a: %a" (Pretty.d_list ", " d_exp) es AD.pretty rs; + if M.tracing then M.tracel "var_eq" "remove_reachable %a: %a" (Pretty.d_list ", " CilType.Exp.pp) es AD.pp rs; (* Prior to https://github.com/goblint/analyzer/pull/694 checks were done "in the other direction": each expression in st was checked for reachability from es/rs using very conservative but also unsound reachable_from. It is unknown, why that was necessary. *) @@ -550,7 +550,7 @@ struct D.B.fold add es (Queries.ES.empty ()) let rec eq_set_clos e s = - if M.tracing then M.traceli "var_eq" "eq_set_clos %a" d_plainexp e; + if M.tracing then M.traceli "var_eq" "eq_set_clos %a" CilType.Exp.pp e; let r = match e with | AddrOf (Mem (BinOp (IndexPI, a, i, _)), os) -> (* convert IndexPI to Index offset *) @@ -586,7 +586,7 @@ struct | CastE (k,t,e) -> Queries.ES.map (fun e -> CastE (k,t,e)) (eq_set_clos e s) in - if M.tracing then M.traceu "var_eq" "eq_set_clos %a = %a" d_plainexp e Queries.ES.pretty r; + if M.tracing then M.traceu "var_eq" "eq_set_clos %a = %a" CilType.Exp.pp e Queries.ES.pp r; r @@ -596,7 +596,7 @@ struct Queries.ID.of_bool (Cilfacade.get_ikind t) true | Queries.EqualSet e -> let r = eq_set_clos e man.local in - if M.tracing then M.tracel "var_eq" "equalset %a = %a" d_plainexp e Queries.ES.pretty r; + if M.tracing then M.tracel "var_eq" "equalset %a = %a" CilType.Exp.pp e Queries.ES.pp r; r | Queries.Invariant context when GobConfig.get_bool "ana.var_eq.invariant.enabled" && GobConfig.get_bool "witness.invariant.exact" -> (* only exact equalities here *) let scope = Node.find_fundec man.node in diff --git a/src/arg/argConstraints.ml b/src/arg/argConstraints.ml index 8ff2367607..a602c39b7f 100644 --- a/src/arg/argConstraints.ml +++ b/src/arg/argConstraints.ml @@ -226,11 +226,11 @@ struct | Queries.IterPrevVars f -> if M.tracing then M.tracei "witness" "IterPrevVars"; Dom.iter (fun x r -> - if M.tracing then M.tracei "witness" "x = %a" Spec.D.pretty x; + if M.tracing then M.tracei "witness" "x = %a" Spec.D.pp x; R.iter (function ((n, c, j), e) -> if M.tracing then M.tracec "witness" "n = %a" Node.pretty_plain n; - if M.tracing then M.tracec "witness" "c = %a" Spec.C.pretty c; - if M.tracing then M.tracec "witness" "j = %a" Spec.D.pretty j; + if M.tracing then M.tracec "witness" "c = %a" Spec.C.pp c; + if M.tracing then M.tracec "witness" "j = %a" Spec.D.pp j; f (I.to_int x) (n, Obj.repr c, I.to_int j) e ) r; if M.tracing then M.traceu "witness" "" (* unindent! *) diff --git a/src/cdomain/value/cdomains/arrayDomain.ml b/src/cdomain/value/cdomains/arrayDomain.ml index 1b096a88f3..0bd08653dc 100644 --- a/src/cdomain/value/cdomains/arrayDomain.ml +++ b/src/cdomain/value/cdomains/arrayDomain.ml @@ -136,6 +136,7 @@ struct let show x = "Array: " ^ Val.show x let pretty () x = text "Array: " ++ pretty () x + let pp ppf x = Format.pp_print_string ppf (show x) let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y let get ?(checkBounds=true) (ask: VDQ.t) a i = a let set (ask: VDQ.t) a (ie, i) v = @@ -201,6 +202,7 @@ struct "Array (unrolled to " ^ (Stdlib.string_of_int (factor ())) ^ "): " ^ (show_list xl) ^ Val.show xr ^ ")" let pretty () x = text "Array: " ++ text (show x) + let pp ppf x = Format.pp_print_string ppf (show x) let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y let get ?(checkBounds=true) (ask: VDQ.t) (xl, xr) (_,i) = let search_unrolled_values min_i max_i = @@ -376,6 +378,7 @@ struct Val.show xr ^ ")" let pretty () x = text "Array: " ++ text (show x) + let pp ppf x = Format.pp_print_string ppf (show x) let pretty_diff () (x,y) = dprintf "%s: %a not leq %a" (name ()) pretty x pretty y let printXml f = function @@ -523,7 +526,7 @@ struct let move_if_affected ?replace_with_const = move_if_affected_with_length ?replace_with_const None let set_with_length length (ask:VDQ.t) x (i,_) a = - if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pretty a; + if M.tracing then M.trace "update_offset" "part array set_with_length %a %s %a" pretty x (BatOption.map_default Basetype.CilExp.show "None" i) Val.pp a; match i with | Some i when Offset.Index.Exp.is_all i -> (* TODO: Doesn't seem to work for unassume. *) @@ -1848,6 +1851,7 @@ struct let printXml f x = delegate_if_no_nullbytes x (printXml f) (A.printXml f) let to_yojson x = delegate_if_no_nullbytes x to_yojson A.to_yojson let pretty () x = delegate_if_no_nullbytes x (pretty ()) (A.pretty ()) + let pp ppf x = Format.pp_print_string ppf (show x) let construct a n = if get_bool "ana.base.arrays.nullbytes" then diff --git a/src/cdomain/value/cdomains/int/intDomTuple.ml b/src/cdomain/value/cdomains/int/intDomTuple.ml index 4f117bc8a2..ee76da5699 100644 --- a/src/cdomain/value/cdomains/int/intDomTuple.ml +++ b/src/cdomain/value/cdomains/int/intDomTuple.ml @@ -382,6 +382,7 @@ module IntDomTupleImpl = struct | _ -> mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.name () ^ ":" ^ (I.show x) } x |> to_list |> String.concat "; " + let pp ppf x = Format.pp_print_string ppf (show x) let to_yojson = [%to_yojson: Yojson.Safe.t list] % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.to_yojson x } (* `map/opt_map` are used by `project` *) diff --git a/src/cdomain/value/cdomains/intDomain0.ml b/src/cdomain/value/cdomains/intDomain0.ml index 296cbe5dd5..2b07754d7d 100644 --- a/src/cdomain/value/cdomains/intDomain0.ml +++ b/src/cdomain/value/cdomains/intDomain0.ml @@ -201,6 +201,7 @@ struct "⊤" else I.show x.v (* TODO add ikind to output *) + let pp ppf x = Format.pp_print_string ppf (show x) let pretty () x = if not (GobConfig.get_bool "dbg.full-output") && I.is_top_of x.ikind x.v then Pretty.text "⊤" @@ -306,7 +307,7 @@ module Size = struct (* size in bits as int, range as int64 *) let is_cast_injective ~from_type ~to_type = let (from_min, from_max) = range (Cilfacade.get_ikind from_type) in let (to_min, to_max) = range (Cilfacade.get_ikind to_type) in - if M.tracing then M.trace "int" "is_cast_injective %a (%a, %a) -> %a (%a, %a)" CilType.Typ.pretty from_type GobZ.pretty from_min GobZ.pretty from_max CilType.Typ.pretty to_type GobZ.pretty to_min GobZ.pretty to_max; + if M.tracing then M.trace "int" "is_cast_injective %a (%a, %a) -> %a (%a, %a)" CilType.Typ.pp from_type GobZ.pp from_min GobZ.pp from_max CilType.Typ.pp to_type GobZ.pp to_min GobZ.pp to_max; Z.compare to_min from_min <= 0 && Z.compare from_max to_max <= 0 let cast t x = (* TODO: overflow is implementation-dependent! *) @@ -321,7 +322,7 @@ module Size = struct (* size in bits as int, range as int64 *) else if Z.lt y a then Z.add y c else y in - if M.tracing then M.tracel "cast" "Cast %a to range [%a, %a] (%a) = %a (%s in int64)" GobZ.pretty x GobZ.pretty a GobZ.pretty b GobZ.pretty c GobZ.pretty y (if is_int64_big_int y then "fits" else "does not fit"); + if M.tracing then M.tracel "cast" "Cast %a to range [%a, %a] (%a) = %a (%s in int64)" GobZ.pp x GobZ.pp a GobZ.pp b GobZ.pp c GobZ.pp y (if is_int64_big_int y then "fits" else "does not fit"); y (** @return Bit range always includes 0. *) diff --git a/src/cdomain/value/cdomains/offset.ml b/src/cdomain/value/cdomains/offset.ml index 7954a3a6ff..8e1ca0f506 100644 --- a/src/cdomain/value/cdomains/offset.ml +++ b/src/cdomain/value/cdomains/offset.ml @@ -248,7 +248,7 @@ struct let semantic_equal ~typ1 xoffs ~typ2 yoffs = let x_index = to_index ~typ:typ1 xoffs in let y_index = to_index ~typ:typ2 yoffs in - if M.tracing then M.tracel "addr" "xoffs=%a typ1=%a xindex=%a yoffs=%a typ2=%a yindex=%a" pretty xoffs d_plaintype typ1 Idx.pretty x_index pretty yoffs d_plaintype typ2 Idx.pretty y_index; + if M.tracing then M.tracel "addr" "xoffs=%a typ1=%a xindex=%a yoffs=%a typ2=%a yindex=%a" pretty xoffs d_plaintype typ1 Idx.pp x_index pretty yoffs d_plaintype typ2 Idx.pp y_index; Idx.eq x_index y_index include Lattice.NoBotTop diff --git a/src/cdomain/value/cdomains/structDomain.ml b/src/cdomain/value/cdomains/structDomain.ml index 29277b0dab..ab230a38f1 100644 --- a/src/cdomain/value/cdomains/structDomain.ml +++ b/src/cdomain/value/cdomains/structDomain.ml @@ -49,6 +49,7 @@ struct Printable.get_short_list "<" ">" whole_str_list let pretty () = M.pretty () + let pp ppf x = Format.pp_print_string ppf (show x) let replace s field value = M.add field value s let get s field = match M.find_opt field s with @@ -150,7 +151,7 @@ struct let create = hs_create let replace s field value = - if Messages.tracing then Messages.tracel "simplesets" "Normalize top Replace - s:\n%a\nfield:%a\nvalue: %a\n---------" HS.pretty s Basetype.CilField.pretty field Val.pretty value; + if Messages.tracing then Messages.tracel "simplesets" "Normalize top Replace - s:\n%a\nfield:%a\nvalue: %a\n---------" HS.pp s Basetype.CilField.pp field Val.pp value; HS.map (fun s -> SS.replace s field value) s let get = hs_get @@ -219,7 +220,7 @@ struct let (overlapping, rem_uniq) = List.partition (fun ss -> SS.leq h ss || SS.leq ss h ) unique in let joined = List.fold_left (fun el acc -> let res = join_f acc el in - if Messages.tracing then Messages.tracel "simplesets-fct" "Join-fct joining others!\nacc: %a\nel: %a\nres: %a" SS.pretty acc SS.pretty el SS.pretty res; + if Messages.tracing then Messages.tracel "simplesets-fct" "Join-fct joining others!\nacc: %a\nel: %a\nres: %a" SS.pp acc SS.pp el SS.pp res; res ) h overlapping in aux (joined::rem_uniq) t @@ -253,6 +254,8 @@ struct | Some k -> (HS.pretty () s) ++ (text " with key ") ++ (F.pretty () k) | None -> (HS.pretty () s) ++ (text " without key") + let pp ppf x = Format.pp_print_string ppf (show x) + let top () = (hs_top (), None) let is_top (s, _) = hs_is_top s let bot () = (hs_bot (), None) @@ -312,14 +315,14 @@ struct aux (joined::rem_uniq) t in let res = aux [] (HS.elements s) in - if Messages.tracing then Messages.tracel "reduce-key" "Reduced - s:\n%a\nto:\n%a\n---------" HS.pretty s HS.pretty res; + if Messages.tracing then Messages.tracel "reduce-key" "Reduced - s:\n%a\nto:\n%a\n---------" HS.pp s HS.pp res; (res, Some key) let reduce_key (x: t): t = reduce_key_with_fct (SS.join) x let replace (s,k) field value : t = let join_set s =if HS.is_bot s then s else HS.singleton (join_ss s) in - if Messages.tracing then Messages.tracel "keyedsets" "Replace - s:\n%a\nfield:%a\nvalue: %a\n---------" HS.pretty s Basetype.CilField.pretty field Val.pretty value ; + if Messages.tracing then Messages.tracel "keyedsets" "Replace - s:\n%a\nfield:%a\nvalue: %a\n---------" HS.pp s Basetype.CilField.pp field Val.pp value ; let replaced = HS.map (fun s -> SS.replace s field value) s in let result_key = match find_key_field (s,k) with @@ -411,7 +414,7 @@ struct let join_with_fct f (x, k) (y, _) = let appended = List.append (HS.elements x) (HS.elements y) in - if Messages.tracing then Messages.tracel "bettersets" "Join-fct start!\nx: %a\ny: %a" HS.pretty x HS.pretty y; + if Messages.tracing then Messages.tracel "bettersets" "Join-fct start!\nx: %a\ny: %a" HS.pp x HS.pp y; let reduce_list_key_with_fct join_f (xs: variant list) (x: t) = match find_key_field x with | None -> x @@ -427,14 +430,14 @@ struct ) unique in let joined = List.fold_left (fun el acc -> let res = join_f acc el in - if Messages.tracing then Messages.tracel "bettersets" "Join-fct joining others!\nacc: %a\nel: %a\nres: %a" SS.pretty acc SS.pretty el SS.pretty res; + if Messages.tracing then Messages.tracel "bettersets" "Join-fct joining others!\nacc: %a\nel: %a\nres: %a" SS.pp acc SS.pp el SS.pp res; res ) h overlapping in aux (joined::rem_uniq) t in (aux [] xs, Some key) in let res = reduce_list_key_with_fct (SS.join_with_fct f) appended (x,k) in - if Messages.tracing then Messages.tracel "bettersets" "Join-fct result!\nx: %a\ny: %a\nconverted: %a\nres: %a" HS.pretty x HS.pretty y HS.pretty (HS.of_list appended) pretty res; + if Messages.tracing then Messages.tracel "bettersets" "Join-fct result!\nx: %a\ny: %a\nconverted: %a\nres: %a" HS.pp x HS.pp y HS.pp (HS.of_list appended) pretty res; res let join = join_with_fct Val.join diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index 5ac8f02d9c..5fcec1d3e0 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -127,6 +127,7 @@ struct Pretty.dprintf "%a, %a" P.pretty p S.pretty s let show x = GobPretty.sprint pretty x + let pp ppf x = Format.pp_print_string ppf (show x) module D = Lattice.Prod (struct include S @@ -326,6 +327,8 @@ struct | Thread tid -> FlagConfiguredTID.show tid | UnknownThread -> "Unknown thread id" + let pp ppf t = Format.pp_print_string ppf (show t) + let printXml f t = match t with | Thread tid -> FlagConfiguredTID.printXml f tid diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 401da647a2..eab15249a3 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -337,6 +337,8 @@ struct | Bot -> bot_name | Top -> top_name + let pp ppf x = Format.pp_print_string ppf (show x) + let pretty_diff () (x,y) = match (x,y) with | (Int x, Int y) -> ID.pretty_diff () (x,y) @@ -471,7 +473,7 @@ struct | x -> x (* TODO we should also keep track of the type here *) in let a' = AD.map one_addr a in - if M.tracing then M.tracel "cast" "cast_addr %a to %a is %a!" AD.pretty a d_type t AD.pretty a'; + if M.tracing then M.tracel "cast" "cast_addr %a to %a is %a!" AD.pp a CilType.Typ.pp t AD.pp a'; a' (* this is called for: @@ -488,7 +490,7 @@ struct | JmpBuf _ -> v | _ -> - let log_top (_,l,_,_) = if Messages.tracing then Messages.tracel "cast" "log_top at %d: %a to %a is top!" l pretty v d_type t in + let log_top (_,l,_,_) = if Messages.tracing then Messages.tracel "cast" "log_top at %d: %a to %a is top!" l pretty v CilType.Typ.pp t in let t = unrollType t in let v' = match t with | TInt (ik,_) -> @@ -564,7 +566,7 @@ struct log_top __POS__; Top | _ -> log_top __POS__; assert false in - if Messages.tracing then Messages.tracel "cast" "cast %a to %a is %a!" pretty v d_type t pretty v'; + if Messages.tracing then Messages.tracel "cast" "cast %a to %a is %a!" pretty v CilType.Typ.pp t pretty v'; v' @@ -903,7 +905,7 @@ struct (* Funny, this does not compile without the final type annotation! *) let rec eval_offset (ask: VDQ.t) f (x: t) (offs:offs) (exp:exp option) (v:lval option) (t:typ): t = let rec do_eval_offset (x:t) (offs:offs) (l:lval option) (o:offset option): t = - if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp; + if M.tracing then M.traceli "eval_offset" "do_eval_offset %a %a (%a)" pretty x Offs.pp offs (Pretty.docOpt (CilType.Exp.pp ())) exp; let r = match x, offs with | Blob((va, _, zeroinit) as c), `Index (_, ox) -> @@ -979,7 +981,7 @@ struct let update_offset ?(blob_destructive=false) (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t = let rec do_update_offset ?(bitfield:int option=None) (x:t) (offs:offs) (l:lval option) (o:offset option) (t:typ):t = (* TODO: why does inner t argument change here, but not in eval_offset? *) - if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value; + if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a" pretty x Offs.pp offs (Pretty.docOpt (CilType.Exp.pp ())) exp pretty value; let mu = function Blob (Blob (y, s', zeroinit), s, _) -> Blob (y, ID.join s s', zeroinit) | x -> x in let r = match x, offs with diff --git a/src/cdomains/apron/affineEqualityDenseDomain.apron.ml b/src/cdomains/apron/affineEqualityDenseDomain.apron.ml index 1db52f15a2..f00e0c0ca0 100644 --- a/src/cdomains/apron/affineEqualityDenseDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDenseDomain.apron.ml @@ -136,7 +136,7 @@ struct let res = bound_texpr d texpr1 in (if M.tracing then match res with - | Some min, Some max -> M.tracel "bounds" "min: %a max: %a" GobZ.pretty min GobZ.pretty max + | Some min, Some max -> M.tracel "bounds" "min: %a max: %a" GobZ.pp min GobZ.pp max | _ -> () ); res @@ -210,6 +210,7 @@ struct "[|"^ (String.concat "; " constraint_list) ^"|]" let pretty () (x:t) = text (show x) + let pp ppf x = Format.pp_print_string ppf (show x) let printXml f x = BatPrintf.fprintf f "\n\n\nmatrix\n\n\n%s\n\nenv\n\n\n%a\n\n\n" (XmlUtil.escape (show x)) Environment.printXml x.env let eval_interval ask = Bounds.bound_texpr @@ -443,7 +444,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 %s \n v: %a \n v': %a\n -> %s" (show t) Var.pp v Var.pp v' (show res); res let assign_var_parallel t vv's = (* vv's is a list of pairs of lhs-variables and their rhs-values *) @@ -514,7 +515,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 %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pp var CilType.Exp.pp exp (show res); res let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov @@ -573,7 +574,7 @@ struct res let assert_constraint ask d e negate no_ov = - if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" d_exp e (Lazy.force no_ov); + if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" CilType.Exp.pp e (Lazy.force no_ov); match Convert.tcons1_of_cil_exp ask d d.env e negate no_ov with | tcons1 -> meet_tcons ask d tcons1 e | exception Convert.Unsupported_CilExp _ -> d diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 06e131bbec..8f47c7926b 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -137,7 +137,7 @@ struct let res = bound_texpr d texpr1 in (if M.tracing then match res with - | Some min, Some max -> M.tracel "bounds" "min: %a max: %a" GobZ.pretty min GobZ.pretty max + | Some min, Some max -> M.tracel "bounds" "min: %a max: %a" GobZ.pp min GobZ.pp max | _ -> () ); res @@ -212,6 +212,7 @@ struct "[|"^ (String.concat "; " constraint_list) ^"|]" let pretty () (x:t) = text (show x) + let pp ppf x = Format.pp_print_string ppf (show x) let printXml f x = BatPrintf.fprintf f "\n\n\nmatrix\n\n\n%s\n\nenv\n\n\n%a\n\n\n" (XmlUtil.escape (show x)) Environment.printXml x.env let eval_interval ask = Bounds.bound_texpr @@ -397,7 +398,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 %s \n v: %a \n v': %a\n -> %s" (show t) Var.pp v Var.pp v' (show res); res let assign_var_parallel t vv's = (* vv's is a list of pairs of lhs-variables and their rhs-values *) @@ -465,7 +466,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 %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pp var CilType.Exp.pp exp (show res); res let substitute_exp ask t var exp no_ov = timing_wrap "substitution" (substitute_exp ask t var exp) no_ov @@ -524,7 +525,7 @@ struct res let assert_constraint ask d e negate no_ov = - if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" d_exp e (Lazy.force no_ov); + if M.tracing then M.tracel "assert_constraint" "assert_constraint with expr: %a %b" CilType.Exp.pp e (Lazy.force no_ov); match Convert.tcons1_of_cil_exp ask d d.env e negate no_ov with | tcons1 -> meet_tcons ask d tcons1 e | exception Convert.Unsupported_CilExp _ -> d diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 2273ec5306..292967657f 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: %a" Texpr1.pretty texpr1; + if M.tracing then M.trace "apron" "assign_exp converted: %a" Texpr1.pp 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"; @@ -446,6 +446,7 @@ struct let show (x:t) = GobFormat.asprintf "%a (env: %a)" A.print x Environment.pp (A.env x) let pretty () (x:t) = text (show x) + let pp ppf x = Format.pp_print_string ppf (show x) let equal x y = Environment.equal (A.env x) (A.env y) && A.is_eq Man.mgr x y @@ -501,7 +502,7 @@ struct LAnd, LOr, LNot are directly supported by Apron domain in order to confirm logic-containing Apron invariants from witness while deep-query is disabled *) let rec assert_constraint ask d e negate (no_ov: bool Lazy.t) = - if M.tracing then M.trace "assert_constraint_apron" "%a ;;; %a" d_exp e d_plainexp e; + if M.tracing then M.trace "assert_constraint_apron" "%a ;;; %a" CilType.Exp.pp e CilType.Exp.pp e; match e with (* Apron doesn't properly meet with DISEQ constraints: https://github.com/antoinemine/apron/issues/37. Join Gt and Lt versions instead. *) @@ -533,14 +534,14 @@ 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 %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: %a" Tcons1.pretty tcons1; + if M.tracing then M.trace "apron" "assert_constraint %a %a" CilType.Exp.pp e Tcons1.pp tcons1; + if M.tracing then M.trace "apron" "assert_constraint st: %a" D.pp d; + if M.tracing then M.trace "apron" "assert_constraint tcons1: %a" Tcons1.pp tcons1; let r = meet_tcons ask d tcons1 e in - if M.tracing then M.trace "apron" "assert_constraint r: %a" D.pretty r; + if M.tracing then M.trace "apron" "assert_constraint r: %a" D.pp r; r | exception Convert.Unsupported_CilExp reason -> - if M.tracing then M.trace "apron" "assert_constraint %a unsupported: %s" d_exp e (SharedFunctions.show_unsupported_cilExp reason); + if M.tracing then M.trace "apron" "assert_constraint %a unsupported: %s" CilType.Exp.pp e (SharedFunctions.show_unsupported_cilExp reason); d end @@ -618,7 +619,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 %a" Lincons1.pretty con1; + if M.tracing then M.tracei "apron" "try_add_con %a" Lincons1.pp 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 @@ -657,7 +658,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 %a %a -> %B" Environment.pretty env Lincons1.pretty con1 r; + if M.tracing then M.trace "apron" "env_exists_mem_con1 %a %a -> %B" Environment.pp env Lincons1.pp con1 r; r in (* Heuristically reorder constraints to pass 36/12 with singlethreaded->multithreaded mode switching. *) diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml index e5c89d0e80..81db898057 100644 --- a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml +++ b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml @@ -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" "%s %a -> %s" (EConj.show @@ snd @@ BatOption.get t.d) Texpr1.Expr.pp 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 @@ -358,7 +358,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: %a max: %a" GobZ.pretty res GobZ.pretty res; + (if M.tracing then M.tracel "bounds" "min: %a max: %a" GobZ.pp res GobZ.pp res; Some res, Some res) | _ -> None, None @@ -424,6 +424,7 @@ struct EConj.show_formatted (show_var varM.env) (snd arr) ^ (to_subscript @@ fst arr) let pretty () (x:t) = text (show x) + let pp ppf x = Format.pp_print_string ppf (show x) let printXml f x = BatPrintf.fprintf f "\n\n\nequalities\n\n\n%s\n\nenv\n\n\n%a\n\n\n" (XmlUtil.escape (show x)) Environment.printXml x.env let eval_interval ask = Bounds.bound_texpr @@ -646,7 +647,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 %s \n v: %a \n v': %a\n -> %s" (show t) Var.pp v Var.pp v' (show res); res (** Parallel assignment of variables. @@ -699,7 +700,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 %s \n var: %a \n exp: %a \n -> \n %s" (show t) Var.pp var CilType.Exp.pp exp (show res); res let substitute_exp ask t var exp no_ov = Timing.wrap "substitution" (substitute_exp ask t var exp) no_ov @@ -754,7 +755,7 @@ struct | _ -> t (* For equalities of more then 2 vars we just return t *)) let meet_tcons ask t tcons original_expr no_ov = - if M.tracing then M.tracel "meet_tcons" "meet_tcons with expr: %a no_ov:%b" d_exp original_expr (Lazy.force no_ov); + if M.tracing then M.tracel "meet_tcons" "meet_tcons with expr: %a no_ov:%b" CilType.Exp.pp original_expr (Lazy.force no_ov); meet_tcons ask t tcons original_expr no_ov let meet_tcons t tcons expr = Timing.wrap "meet_tcons" (meet_tcons t tcons) expr diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml index 5d266cf474..1d713f7d47 100644 --- a/src/cdomains/apron/relationDomain.apron.ml +++ b/src/cdomains/apron/relationDomain.apron.ml @@ -161,6 +161,8 @@ struct let third = PrivD.show r.priv in "(" ^ first ^ ", " ^ third ^ ")" + let pp ppf r = Format.pp_print_string ppf (show r) + let pretty () r = text "(" ++ RD.pretty () r.rel diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 53c8db8099..1b9c97964c 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -110,7 +110,7 @@ struct | Some min, Some max when Z.compare type_min min <= 0 && Z.compare max type_max <= 0 -> () | min_opt, max_opt -> - if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)" CilType.Exp.pretty exp (Pretty.docOpt (IntOps.BigIntOps.pretty ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pretty ())) max_opt; + if M.tracing then M.trace "apron" "may overflow: %a (%a, %a)" CilType.Exp.pp exp (Pretty.docOpt (IntOps.BigIntOps.pp ())) min_opt (Pretty.docOpt (IntOps.BigIntOps.pp ())) max_opt; raise (Unsupported_CilExp Overflow) ) @@ -122,7 +122,7 @@ struct | `Bot (* This happens when called on a pointer type; -> we can safely return top *) | `Top -> IntDomain.IntDomTuple.top_of ik | `Lifted x -> x (* Cast should be unnecessary because it should be taken care of by EvalInt. *) in - if M.tracing then M.trace "relation-query" "texpr1_expr_of_cil_exp/query: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty res; + if M.tracing then M.trace "relation-query" "texpr1_expr_of_cil_exp/query: %a -> %a" CilType.Exp.pp e IntDomain.IntDomTuple.pp res; res in (* recurse without env and ask arguments *) @@ -161,7 +161,7 @@ struct let ikind = try (Cilfacade.get_ikind_exp e) with Invalid_argument a -> raise (Unsupported_CilExp (Ikind_non_integer a)) in let simp = query e ikind in let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to ~kind:Internal ikind simp in (* TODO: proper castkind *) - if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a" d_plainexp e IntDomain.IntDomTuple.pretty simp; + if M.tracing then M.trace "relation" "texpr1_expr_of_cil_exp/simplify: %a -> %a" CilType.Exp.pp e IntDomain.IntDomTuple.pp simp; BatOption.map_default (fun c -> Const (CInt (c, ikind, None))) e const in let texpr1 e = texpr1_expr_of_cil_exp (simplify e) in @@ -222,7 +222,7 @@ struct M.tracel "rel-texpr-cil-conv" "unsuccessfull: %s" (show_unsupported_cilExp ex); raise (Unsupported_CilExp ex) | res -> - M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" d_plainexp exp Texpr1.Expr.pretty res (Lazy.force no_ov); + M.trace "relation" "texpr1_expr_of_cil_exp: %a -> %a (%b)" CilType.Exp.pp exp Texpr1.Expr.pp res (Lazy.force no_ov); M.tracel "rel-texpr-cil-conv" "successfull: Good"; res else conv exp @@ -584,7 +584,7 @@ struct | exception Invalid_argument _ -> ID.top () (* real top, not a top of any ikind because we don't even know the ikind *) | ik -> - if M.tracing then M.trace "relation" "eval_int: exp_is_constraint %a = %B" d_plainexp e (Cilfacade.exp_is_boolean e); + if M.tracing then M.trace "relation" "eval_int: exp_is_constraint %a = %B" CilType.Exp.pp e (Cilfacade.exp_is_boolean e); if Cilfacade.exp_is_boolean e then match check_assert ask d e no_ov with | `True -> ID.of_bool ik true diff --git a/src/cdomains/baseDomain.ml b/src/cdomains/baseDomain.ml index 64b5a174e8..24553fef47 100644 --- a/src/cdomains/baseDomain.ml +++ b/src/cdomains/baseDomain.ml @@ -70,6 +70,8 @@ struct PrivD.pretty () r.priv ++ text ")" + let pp ppf r = Format.pp_print_string ppf (show r) + let printXml f r = let e = XmlUtil.escape in BatPrintf.fprintf f "\n\n\n%s\n\n%a\n%s\n\n%a\n%s\n\n%a\n\n%s\n\n%a\n\n" diff --git a/src/cdomains/c2poDomain.ml b/src/cdomains/c2poDomain.ml index edb42f64c7..5af518937c 100644 --- a/src/cdomains/c2poDomain.ml +++ b/src/cdomains/c2poDomain.ml @@ -281,7 +281,7 @@ module D = struct (** Remove terms from the data structure. It removes all terms that may point to one of the tainted addresses.*) let remove_tainted_terms ask address cc = - if M.tracing then M.tracel "c2po-tainted" "remove_tainted_terms: %a\n" MayBeEqual.AD.pretty address; + if M.tracing then M.tracel "c2po-tainted" "remove_tainted_terms: %a\n" MayBeEqual.AD.pp address; let may_be_tainted = MayBeEqual.may_point_to_one_of_these_addresses ask address cc in diff --git a/src/cdomains/duplicateVars.ml b/src/cdomains/duplicateVars.ml index fdeb99428b..c1aa8c0bd6 100644 --- a/src/cdomains/duplicateVars.ml +++ b/src/cdomains/duplicateVars.ml @@ -118,7 +118,7 @@ struct let to_varinfo v = let res = VarVarinfoMap.to_varinfo v in - if M.tracing then M.trace "c2po-varinfo" "to_varinfo: %a -> %a" d_type (get_type v) d_type res.vtype; + if M.tracing then M.trace "c2po-varinfo" "to_varinfo: %a -> %a" CilType.Typ.pp (get_type v) CilType.Typ.pp res.vtype; res end diff --git a/src/cdomains/musteqDomain.ml b/src/cdomains/musteqDomain.ml index c7a1cbc176..04c63da872 100644 --- a/src/cdomains/musteqDomain.ml +++ b/src/cdomains/musteqDomain.ml @@ -100,6 +100,8 @@ struct let content () = fold f mapping nil in dprintf "@[%s {\n @[%t@]}@]" (show mapping) content + let pp ppf x = Format.pp_print_string ppf (show x) + let add_old = add let rec add (x,y) fd d = if V.equal x y || mem (x,y) d then d else diff --git a/src/cdomains/symbLocksDomain.ml b/src/cdomains/symbLocksDomain.ml index 020ac9120e..6ce07940c1 100644 --- a/src/cdomains/symbLocksDomain.ml +++ b/src/cdomains/symbLocksDomain.ml @@ -237,7 +237,7 @@ struct | _ , _ -> raise (Invalid_argument "") let from_exps a l : t option = - if M.tracing then M.tracel "symb_locks" "from_exps %a (%s) %a (%s)" d_plainexp a (ees_to_str (toEl a)) d_plainexp l (ees_to_str (toEl l)); + if M.tracing then M.tracel "symb_locks" "from_exps %a (%s) %a (%s)" CilType.Exp.pp a (ees_to_str (toEl a)) CilType.Exp.pp l (ees_to_str (toEl l)); let a, l = toEl a, toEl l in (* ignore (printf "from_exps:\n %s\n %s\n" (ees_to_str a) (ees_to_str l)); *) (*let rec fold_left2 f a xs ys = diff --git a/src/cdomains/unionFind.ml b/src/cdomains/unionFind.ml index 585ea117ca..4ccbb8d0c1 100644 --- a/src/cdomains/unionFind.ml +++ b/src/cdomains/unionFind.ml @@ -357,7 +357,7 @@ module T = struct let const = to_cil_constant off (Some typ) in BinOp (PlusPI, cil_t, const, typ) in - if M.tracing then M.trace "c2po-2cil" "exp: %a; offset: %s; res: %a" d_exp cil_t (Z.to_string off) d_exp res; + if M.tracing then M.trace "c2po-2cil" "exp: %a; offset: %s; res: %a" CilType.Exp.pp cil_t (Z.to_string off) CilType.Exp.pp res; res let is_field = function @@ -413,7 +413,7 @@ module T = struct (** Get a Cil expression that is equivalent to *(exp + offset), by taking into account type correctness.*) let dereference_exp exp offset = - if M.tracing then M.trace "c2po-deref" "exp: %a, offset: %s" d_exp exp (Z.to_string offset); + if M.tracing then M.trace "c2po-deref" "exp: %a, offset: %s" CilType.Exp.pp exp (Z.to_string offset); let res = let find_field cinfo = try @@ -461,7 +461,7 @@ module T = struct else raise (UnsupportedCilExpression "not a pointer variable") in - if M.tracing then M.trace "c2po-deref" "deref result: %a" d_exp res; + if M.tracing then M.trace "c2po-deref" "deref result: %a" CilType.Exp.pp res; res let get_size t = get_size_in_bits @@ type_of_term t @@ -603,14 +603,14 @@ module T = struct | false -> let res = match of_cil_neg ask neg (Cil.constFold false e) with | exception (UnsupportedCilExpression s) -> - if M.tracing then M.trace "c2po-cil-conversion" "unsupported exp: %a\n%s\n" d_plainexp e s; + if M.tracing then M.trace "c2po-cil-conversion" "unsupported exp: %a\n%s\n" CilType.Exp.pp e s; None, None | t, z -> t, Some z 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 --> %s\n" CilType.Exp.pp e (Z.to_string z) + | Some t, Some z -> M.trace "c2po-cil-conversion" "exp: %a --> %s + %s\n" CilType.Exp.pp e (show t) (Z.to_string z); | _ -> ()); res @@ -625,7 +625,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 --> %s + %s\n" CilType.Exp.pp e (show t) (Z.to_string z); None, None end | t, z -> t, z diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index d2d1a92f8c..17a918e658 100644 --- a/src/common/framework/cfgTools.ml +++ b/src/common/framework/cfgTools.ml @@ -122,6 +122,10 @@ let rec pretty_edges () = function | [_,x] -> Edge.pretty_plain () x | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs +let pp_edges ppf edges = + let pp_sep ppf () = Format.pp_print_string ppf "; " in + Format.pp_print_list ~pp_sep (fun ppf (_,e) -> Edge.pp ppf e) ppf edges + let node_scc_global = NH.create 113 exception Not_connect of fundec @@ -149,9 +153,9 @@ let createCFG (file: file) = let addEdges ?(skippedStatements = []) fromNode edges toNode = if Messages.tracing then Messages.trace "cfg" "Adding edges [%a] from\n\t%a\nto\n\t%a ... " - pretty_edges edges - Node.pretty_trace fromNode - Node.pretty_trace toNode; + pp_edges edges + Node.pp_trace fromNode + Node.pp_trace toNode; NH.replace fd_nodes fromNode (); NH.replace fd_nodes toNode (); H.modify_def [] toNode (List.cons (edges,fromNode)) cfgB; diff --git a/src/common/framework/edge.ml b/src/common/framework/edge.ml index e6f214a4c8..da47e79142 100644 --- a/src/common/framework/edge.ml +++ b/src/common/framework/edge.ml @@ -47,6 +47,9 @@ let pretty () = function | Skip -> Pretty.text "skip" | VDecl v -> Cil.defaultCilPrinter#pVDecl () v +let show x = GobPretty.sprint pretty x +let pp ppf x = Format.pp_print_string ppf (show x) + let pretty_plain () = function | Assign (lv,rv) -> dprintf "Assign '%a = %a' " d_lval lv d_exp rv | Proc (None ,f,ars) -> dprintf "Proc '%a(%a)'" d_exp f (d_list ", " d_exp) ars diff --git a/src/common/util/messages.ml b/src/common/util/messages.ml index 7fe00a6708..8b8d7620ff 100644 --- a/src/common/util/messages.ml +++ b/src/common/util/messages.ml @@ -344,20 +344,18 @@ let msg_final severity ?(tags=[]) ?(category=Category.Unknown) fmt = include Goblint_tracing -open Pretty - let tracel sys ?var fmt = let loc = !current_loc in - let docloc sys doc = - printtrace sys (dprintf "(%a)@?" CilType.Location.pretty loc ++ indent 2 doc); + let strloc sys s = + printtrace sys (Format.asprintf "(%a) %s" CilType.Location.pp loc s) in - gtrace true docloc sys var ~loc ignore fmt + gtrace true strloc sys var ~loc ignore fmt let traceli sys ?var ?(subsys=[]) fmt = let loc = !current_loc in let g () = activate sys subsys in - let docloc sys doc: unit = - printtrace sys (dprintf "(%a)" CilType.Location.pretty loc ++ indent 2 doc); + let strloc sys s = + printtrace sys (Format.asprintf "(%a) %s" CilType.Location.pp loc s); traceIndent () in - gtrace true docloc sys var ~loc g fmt + gtrace true strloc sys var ~loc g fmt diff --git a/src/config/gobConfig.ml b/src/config/gobConfig.ml index 92012108c3..4ed108b746 100644 --- a/src/config/gobConfig.ml +++ b/src/config/gobConfig.ml @@ -304,7 +304,7 @@ struct try let st = String.trim st in let x = get_value !json_conf (parse_path st) in - if Goblint_tracing.tracing then Goblint_tracing.trace "conf-reads" "Reading '%s', it is %a." st GobYojson.pretty x; + if Goblint_tracing.tracing then Goblint_tracing.trace "conf-reads" "Reading '%s', it is %a." st GobYojson.pp x; try f x with Yojson.Safe.Util.Type_error (s, _) -> Logs.error "The value for '%s' has the wrong type: %s" st s; @@ -362,7 +362,7 @@ struct @raise Invalid_argument @raise Json_encoding.Cannot_destruct *) let set_path_string st v = - if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a." st GobYojson.pretty v; + if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a." st GobYojson.pp v; set_value v json_conf (parse_path st) let set_json st j = @@ -417,7 +417,7 @@ struct | Some fn -> let v = In_channel.with_open_text (Fpath.to_string fn) Yojson.Safe.from_channel in merge v; - if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Merging with '%a', resulting\n%a." GobFpath.pretty fn GobYojson.pretty !json_conf + if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Merging with '%a', resulting\n%a." GobFpath.pp fn GobYojson.pp !json_conf | None -> raise (Sys_error (Printf.sprintf "%s: No such file or directory" (Fpath.to_string fn))) end diff --git a/src/domains/access.ml b/src/domains/access.ml index 823e1cd589..044ddf5f7c 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -276,7 +276,7 @@ let get_val_type e: acc_typ = (** Add access to {!Memo} after distributing. *) let add_one ~side memo: unit = let ignorable = is_ignorable_memo memo in - if M.tracing then M.trace "access" "add_one %a (ignorable = %B)" Memo.pretty memo ignorable; + if M.tracing then M.trace "access" "add_one %a (ignorable = %B)" Memo.pp memo ignorable; if not ignorable then side memo @@ -284,7 +284,7 @@ let add_one ~side memo: unit = Empty access sets are needed for prefix-type_suffix race checking. *) let rec add_distribute_outer ~side ~side_empty (ts: typsig) (o: Offset.Unit.t) = let memo = (`Type ts, o) in - if M.tracing then M.tracei "access" "add_distribute_outer %a" Memo.pretty memo; + if M.tracing then M.tracei "access" "add_distribute_outer %a" Memo.pp memo; add_one ~side memo; (* Add actual access for non-recursive call, or empty access for recursive call when side is side_empty. *) (* distribute to variables of the type *) @@ -307,11 +307,11 @@ let rec add_distribute_outer ~side ~side_empty (ts: typsig) (o: Offset.Unit.t) = let add ~side ~side_empty e voffs = begin match voffs with | Some (v, o) -> (* known variable *) - if M.tracing then M.traceli "access" "add var %a%a" CilType.Varinfo.pretty v CilType.Offset.pretty o; + if M.tracing then M.traceli "access" "add var %a%a" CilType.Varinfo.pp v CilType.Offset.pp o; let memo = (`Var v, Offset.Unit.of_cil o) in add_one ~side memo | None -> (* unknown variable *) - if M.tracing then M.traceli "access" "add type %a" CilType.Exp.pretty e; + if M.tracing then M.traceli "access" "add type %a" CilType.Exp.pp e; let ty = get_val_type e in (* extract old acc_typ from expression *) let (t, o) = match ty with (* convert acc_typ to type-based Memo (components) *) | `Struct (c, o) -> (TComp (c, []), o) @@ -485,7 +485,7 @@ struct end let group_may_race (warn_accs:WarnAccs.t) = - if M.tracing then M.tracei "access" "group_may_race %a" WarnAccs.pretty warn_accs; + if M.tracing then M.tracei "access" "group_may_race %a" WarnAccs.pp warn_accs; (* BFS to traverse one component with may_race edges *) let rec bfs' warn_accs ~todo ~visited = let todo_all = WarnAccs.union_all todo in @@ -542,7 +542,7 @@ let group_may_race (warn_accs:WarnAccs.t) = ) in let (comps, warn_accs) = components [] warn_accs in - if M.tracing then M.trace "access" "components %a" WarnAccs.pretty warn_accs; + if M.tracing then M.trace "access" "components %a" WarnAccs.pp warn_accs; (* repeat BFS to find all prefix-type_suffix-only components starting from prefix accesses (symmetric) *) let rec components_cross comps ~prefix ~type_suffix = if AS.is_empty prefix then @@ -550,7 +550,7 @@ let group_may_race (warn_accs:WarnAccs.t) = else ( let prefix_acc = AS.choose prefix in let (warn_accs', comp) = bfs {(WarnAccs.empty ()) with prefix; type_suffix} {(WarnAccs.empty ()) with prefix=AS.singleton prefix_acc} in - if M.tracing then M.trace "access" "components_cross %a" WarnAccs.pretty warn_accs'; + if M.tracing then M.trace "access" "components_cross %a" WarnAccs.pp warn_accs'; let comps' = if AS.cardinal comp > 1 then comp :: comps diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index bb77519cbf..098a7592ba 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -188,8 +188,8 @@ struct let tf_normal_call man lv e (f:fundec) args getl sidel demandl getg sideg = let combine (cd, fc, fd) = - if M.tracing then M.traceli "combine" "local: %a" S.D.pretty cd; - if M.tracing then M.trace "combine" "function: %a" S.D.pretty fd; + if M.tracing then M.traceli "combine" "local: %a" S.D.pp cd; + if M.tracing then M.trace "combine" "function: %a" S.D.pp fd; let rec cd_man = { man with ask = (fun (type a) (q: a Queries.t) -> S.query cd_man q); @@ -236,7 +236,7 @@ struct S.D.join acc (S.combine_assign combine_assign_man lv e f args fc fd1_man.local (Analyses.ask_of_man fd1_man)) ) (S.D.bot ()) (S.paths_as_set fd_man) in - if M.tracing then M.traceu "combine" "combined local: %a" S.D.pretty r; + if M.tracing then M.traceu "combine" "combined local: %a" S.D.pp r; r in let paths = S.enter man lv f args in @@ -249,7 +249,7 @@ struct if M.tracing then M.traceli "combine" "combining"; let paths = List.map combine paths in let r = List.fold_left D.join (D.bot ()) paths in - if M.tracing then M.traceu "combine" "combined: %a" S.D.pretty r; + if M.tracing then M.traceu "combine" "combined: %a" S.D.pp r; r diff --git a/src/framework/control.ml b/src/framework/control.ml index f2bfffde2d..07aeef3624 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -291,7 +291,7 @@ struct let gh = GHT.create 13 in let getg v = GHT.find_default gh v (EQSys.G.bot ()) in let sideg v d = - if M.tracing then M.trace "global_inits" "sideg %a = %a" EQSys.GVar.pretty v EQSys.G.pretty d; + if M.tracing then M.trace "global_inits" "sideg %a = %a" EQSys.GVar.pp v EQSys.G.pp d; GHT.replace gh v (EQSys.G.join (getg v) d) in (* Old-style global function for context. @@ -320,15 +320,15 @@ struct let funs = ref [] in (*let count = ref 0 in*) let transfer_func (st : Spec.D.t) (loc, edge) : Spec.D.t = - if M.tracing then M.trace "con" "Initializer %a" CilType.Location.pretty loc; + if M.tracing then M.trace "con" "Initializer %a" CilType.Location.pp loc; (*incr count; if (get_bool "dbg.verbose")&& (!count mod 1000 = 0) then Printf.printf "%d %!" !count; *) match edge with | MyCFG.Entry func -> - if M.tracing then M.trace "global_inits" "Entry %a" d_lval (var func.svar); + if M.tracing then M.trace "global_inits" "Entry %a" CilType.Lval.pp (var func.svar); Spec.body {man with local = st} func | MyCFG.Assign (lval,exp) -> - if M.tracing then M.trace "global_inits" "Assign %a = %a" d_lval lval d_exp exp; + if M.tracing then M.trace "global_inits" "Assign %a = %a" CilType.Lval.pp lval CilType.Exp.pp exp; begin match lval, exp with | (Var v,o), (AddrOf (Var f,NoOffset)) when v.vstorage <> Static && isFunctionType f.vtype -> @@ -338,7 +338,7 @@ struct let res = Spec.assign {man with local = st} lval exp in (* Needed for privatizations (e.g. None) that do not side immediately *) let res' = Spec.sync {man with local = res} `Normal in - if M.tracing then M.trace "global_inits" "\t\t -> state:%a" Spec.D.pretty res; + if M.tracing then M.trace "global_inits" "\t\t -> state:%a" Spec.D.pp res; res' | _ -> failwith "Unsupported global initializer edge" in @@ -355,7 +355,7 @@ struct let with_externs = do_extern_inits man file in (*if (get_bool "dbg.verbose") then Printf.printf "Number of init. edges : %d\nWorking:" (List.length edges); *) let result : Spec.D.t = List.fold_left transfer_func with_externs edges in - if M.tracing then M.trace "global_inits" "startstate: %a" Spec.D.pretty result; + if M.tracing then M.trace "global_inits" "startstate: %a" Spec.D.pp result; result, !funs in diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml index 4d01d7e166..568baef828 100644 --- a/src/incremental/compareAST.ml +++ b/src/incremental/compareAST.ml @@ -129,7 +129,7 @@ and eq_typ_acc ?(fun_parameter_name_comparison_enabled: bool = true) (a: typ) (b a, b, c, (updatedCompinfoRenames, updatedEnumRenames) in - if Messages.tracing then Messages.tracei "compareast" "eq_typ_acc %a vs %a (%a, %a)" d_type a d_type b pretty_length acc pretty_length !global_typ_acc; (* %a makes List.length calls lazy if compareast isn't being traced *) + if Messages.tracing then Messages.tracei "compareast" "eq_typ_acc %a vs %a (%a, %a)" CilType.Typ.pp a CilType.Typ.pp b pretty_length acc pretty_length !global_typ_acc; (* %a makes List.length calls lazy if compareast isn't being traced *) let r, updated_rename_mapping = match a, b with | TPtr (typ1, attr1), TPtr (typ2, attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 | TArray (typ1, (Some lenExp1), attr1), TArray (typ2, (Some lenExp2), attr2) -> eq_typ_acc typ1 typ2 ~rename_mapping ~acc &&>> eq_exp lenExp1 lenExp2 ~acc &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 @@ -175,7 +175,7 @@ and eq_typ_acc ?(fun_parameter_name_comparison_enabled: bool = true) (a: typ) (b | TFloat (fk1, attr1), TFloat (fk2, attr2) -> (fk1 = fk2, rename_mapping) &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 | _, _ -> false, rename_mapping in - if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a" d_type a d_type b; + if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a" CilType.Typ.pp a CilType.Typ.pp b; (r, updated_rename_mapping) and eq_eitems (a: string * attributes * exp * location) (b: string * attributes * exp * location) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with diff --git a/src/lifters/longjmpLifter.ml b/src/lifters/longjmpLifter.ml index c392499ef6..035617d0ea 100644 --- a/src/lifters/longjmpLifter.ml +++ b/src/lifters/longjmpLifter.ml @@ -146,7 +146,7 @@ struct | Target (target_node, target_context) -> let target_fundec = Node.find_fundec target_node in if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (man.control_context ()) then ( - if M.tracing then Messages.tracel "longjmp" "Fun: Potentially from same context, side-effect to %a" Node.pretty target_node; + if M.tracing then Messages.tracel "longjmp" "Fun: Potentially from same context, side-effect to %a" Node.pp target_node; man.sideg (V.longjmpto (target_node, man.context ())) (G.create_local (Lazy.force combined)) (* No need to propagate this outwards here, the set of valid longjumps is part of the context, we can never have the same context setting the longjmp multiple times *) ) @@ -160,9 +160,9 @@ struct in JmpBufDomain.JmpBufSet.iter handle_target active_targets in - if M.tracing then M.tracel "longjmp" "longfd getg %a" CilType.Fundec.pretty f; + if M.tracing then M.tracel "longjmp" "longfd getg %a" CilType.Fundec.pp f; let longfd = G.local (man.global (V.longjmpret (f, Option.get fc))) in - if M.tracing then M.tracel "longjmp" "longfd %a" D.pretty longfd; + if M.tracing then M.tracel "longjmp" "longfd %a" D.pp longfd; if not (D.is_bot longfd) then handle_longjmp (man.local, fc, longfd); S.combine_env (conv_man) lv e f args fc fd f_ask @@ -215,7 +215,7 @@ struct (* Eval `env` again to avoid having to construct bespoke man to ask *) let targets = path_man.ask (EvalJumpBuf env) in let valid_targets = path_man.ask ValidLongJmp in - if M.tracing then Messages.tracel "longjmp" "Jumping to %a" JmpBufDomain.JmpBufSet.pretty targets; + if M.tracing then Messages.tracel "longjmp" "Jumping to %a" JmpBufDomain.JmpBufSet.pp targets; let handle_target target = match target with | JmpBufDomain.BufferEntryOrTop.AllTargets -> M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env; @@ -223,7 +223,7 @@ struct | Target (target_node, target_context) -> let target_fundec = Node.find_fundec target_node in if CilType.Fundec.equal target_fundec current_fundec && ControlSpecC.equal target_context (man.control_context ()) then ( - if M.tracing then Messages.tracel "longjmp" "Potentially from same context, side-effect to %a" Node.pretty target_node; + if M.tracing then Messages.tracel "longjmp" "Potentially from same context, side-effect to %a" Node.pp target_node; man.sideg (V.longjmpto (target_node, man.context ())) (G.create_local (Lazy.force specialed)) ) else if JmpBufDomain.JmpBufSet.mem target valid_targets then ( diff --git a/src/lifters/specLifters.ml b/src/lifters/specLifters.ml index b3fd321c15..73930cab48 100644 --- a/src/lifters/specLifters.ml +++ b/src/lifters/specLifters.ml @@ -722,10 +722,10 @@ struct assert (D.cardinal man.local = 1); let cd = D.choose man.local in let k x y = - if M.tracing then M.traceli "combine" "function: %a" Spec.D.pretty x; + if M.tracing then M.traceli "combine" "function: %a" Spec.D.pp x; try let r = Spec.combine_env (conv man cd) l fe f a fc x f_ask in - if M.tracing then M.traceu "combine" "combined function: %a" Spec.D.pretty r; + if M.tracing then M.traceu "combine" "combined function: %a" Spec.D.pp r; D.add r y with Deadcode -> if M.tracing then M.traceu "combine" "combined function: dead"; @@ -738,10 +738,10 @@ struct assert (D.cardinal man.local = 1); let cd = D.choose man.local in let k x y = - if M.tracing then M.traceli "combine" "function: %a" Spec.D.pretty x; + if M.tracing then M.traceli "combine" "function: %a" Spec.D.pp x; try let r = Spec.combine_assign (conv man cd) l fe f a fc x f_ask in - if M.tracing then M.traceu "combine" "combined function: %a" Spec.D.pretty r; + if M.tracing then M.traceu "combine" "combined function: %a" Spec.D.pp r; D.add r y with Deadcode -> if M.tracing then M.traceu "combine" "combined function: dead"; diff --git a/src/solver/generic.ml b/src/solver/generic.ml index a8bf588182..6f300604f6 100644 --- a/src/solver/generic.ml +++ b/src/solver/generic.ml @@ -46,7 +46,7 @@ struct let increase (v:Var.t) = let set v c = if not full_trace && (c > start_c && c > !max_c && not (GobOption.exists (Var.equal v) !max_var)) then begin - if tracing then trace "sol" "Switched tracing to %a" Var.pretty_trace v; + if tracing then trace "sol" "Switched tracing to %a" Var.pp_trace v; max_c := c; max_var := Some v end @@ -64,20 +64,20 @@ struct let new_var_event x = incr SolverStats.vars; - if tracing then trace "sol" "New %a" Var.pretty_trace x + if tracing then trace "sol" "New %a" Var.pp_trace x let get_var_event x = - if tracing && full_trace then trace "sol" "Querying %a" Var.pretty_trace x + if tracing && full_trace then trace "sol" "Querying %a" Var.pp_trace x let eval_rhs_event x = - if tracing && full_trace then trace "sol" "(Re-)evaluating %a" Var.pretty_trace x; + if tracing && full_trace then trace "sol" "(Re-)evaluating %a" Var.pp_trace x; incr SolverStats.evals; if (get_bool "dbg.solver-progress") then (incr stack_d; Logs.debug "%d" !stack_d) let update_var_event x o n = if tracing then increase x; if full_trace || (not (Dom.is_bot o) && GobOption.exists (Var.equal x) !max_var) then begin - if tracing then tracei "sol_max" "(%d) Update to %a" !max_c Var.pretty_trace x; + if tracing then tracei "sol_max" "(%d) Update to %a" !max_c Var.pp_trace x; if tracing then traceu "sol_max" "%a" Dom.pretty_diff (n, o) end diff --git a/src/solver/postSolver.ml b/src/solver/postSolver.ml index 449e4e5bdd..902276806c 100644 --- a/src/solver/postSolver.ml +++ b/src/solver/postSolver.ml @@ -192,7 +192,7 @@ struct let reachable = PS.init_reachable ~vh in let rec one_var x = - if M.tracing then M.trace "postsolver" "one_var %a reachable=%B system=%B" S.Var.pretty_trace x (VH.mem reachable x) (Option.is_some (S.system x)); + if M.tracing then M.trace "postsolver" "one_var %a reachable=%B system=%B" S.Var.pp_trace x (VH.mem reachable x) (Option.is_some (S.system x)); if not (VH.mem reachable x) then ( VH.replace reachable x (); Option.may (one_constraint x) (S.system x) @@ -203,13 +203,13 @@ struct try VH.find vh y with Not_found -> S.Dom.bot () in let set y d = - if M.tracing then M.trace "postsolver" "one_side %a %a %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty d; + if M.tracing then M.trace "postsolver" "one_side %a %a %a" S.Var.pp_trace x S.Var.pp_trace y S.Dom.pp d; PS.one_side ~vh ~x ~y ~d; (* check before recursing *) one_var y in let rhs = f get set in - if M.tracing then M.trace "postsolver" "one_constraint %a %a" S.Var.pretty_trace x S.Dom.pretty rhs; + if M.tracing then M.trace "postsolver" "one_constraint %a %a" S.Var.pp_trace x S.Dom.pp rhs; PS.one_constraint ~vh ~x ~rhs in (Timing.wrap "postsolver_iter" (List.iter one_var)) vs; diff --git a/src/solver/sLR.ml b/src/solver/sLR.ml index 968ca6879f..cab31f6b4f 100644 --- a/src/solver/sLR.ml +++ b/src/solver/sLR.ml @@ -62,8 +62,8 @@ module SLR3 = let old = HM.find rho x in let tmp = eq x (eval x) (side x) in let tmp = S.Dom.join tmp (sides x) in - if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ; - if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp; + if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ; + if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp; let tmp = if wpx then if HM.mem globals x then S.Dom.widen old (S.Dom.join old tmp) @@ -72,7 +72,7 @@ module SLR3 = in if not (S.Dom.equal old tmp) then begin update_var_event x old tmp; - if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp; + if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp; HM.replace rho x tmp; let w = try HM.find infl x with Not_found -> VS.empty in let w = if wpx then VS.add x w else w in @@ -401,11 +401,11 @@ module Make0 = let use_box = (not (V.ver>1)) || HM.mem wpoint x in let restart_mode_x = h_find_default restart_mode x (2*GobConfig.get_int "solvers.slr4.restart_count") in let rstrt = use_box && (V.ver>3) && D.leq tmp old && restart_mode_x <> 0 in - if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ; - if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp; + if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ; + if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp; let tmp = if use_box then box old tmp else tmp in if not (D.eq tmp old) then begin - if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp; + if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp; let _ = X.set_value x tmp in if V.ver>3 && restart_mode_x mod 2 = 1 && not (D.leq tmp old) then HM.replace restart_mode x (restart_mode_x - 1); diff --git a/src/solver/sLRphased.ml b/src/solver/sLRphased.ml index feff5514f3..5863efa89d 100644 --- a/src/solver/sLRphased.ml +++ b/src/solver/sLRphased.ml @@ -72,7 +72,7 @@ module Make = let effects = ref Set.empty in let side y d = assert (not (S.Dom.is_bot d)); - if tracing then trace "sol" "SIDE: Var: %a\nVal: %a" S.Var.pretty_trace y S.Dom.pretty d; + if tracing then trace "sol" "SIDE: Var: %a\nVal: %a" S.Var.pp_trace y S.Dom.pp d; let first = not (Set.mem y !effects) in effects := Set.add y !effects; if first then ( @@ -83,7 +83,7 @@ module Make = if not (HM.mem rho y) then ( if b then solve1 (HM.find key x - 1) ~side:true y else solve0 ~side:true y ) else ( - (* trace "sol" "SIDE: Var: %a already exists with Prio: %i and Val: %a" S.Var.pretty_trace y (HM.find key y) S.Dom.pretty d; *) + (* trace "sol" "SIDE: Var: %a already exists with Prio: %i and Val: %a" S.Var.pp_trace y (HM.find key y) S.Dom.pp d; *) if HM.find key y < 0 then HM.replace key y (Ref.post_decr count_side) ); q := H.add y !q @@ -101,28 +101,28 @@ module Make = let tmp = eq x eval side in let tmp = S.Dom.join tmp (sides x) in (* if (b && not (S.Dom.leq old tmp)) then ( *) - (* trace "sol" "Var: %a\nOld: %a\nTmp: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp; *) + (* trace "sol" "Var: %a\nOld: %a\nTmp: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp; *) (* assert false *) (* ); *) let val_new = if wpx then if b then let nar = narrow old tmp in - if tracing then trace "sol" "NARROW: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar; + if tracing then trace "sol" "NARROW: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp S.Dom.pp nar; nar else let wid = S.Dom.widen old (S.Dom.join old tmp) in - if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid; + if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp S.Dom.pp wid; wid else tmp in - if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ; - if tracing then trace "sol" "Contrib:%a" S.Dom.pretty val_new; + if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ; + if tracing then trace "sol" "Contrib:%a" S.Dom.pp val_new; if S.Dom.equal old val_new then () else begin update_var_event x old val_new; - if tracing then trace "sol" "New Value:%a" S.Dom.pretty val_new; + if tracing then trace "sol" "New Value:%a" S.Dom.pp val_new; HM.replace rho x val_new; let w = try HM.find infl x with Not_found -> VS.empty in (* let w = if wpx then VS.add x w else w in *) @@ -162,7 +162,7 @@ module Make = and sides x = let w = try HM.find set x with Not_found -> VS.empty in let v = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ()) - in if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pretty_trace x S.Dom.pretty v; v + in if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pp_trace x S.Dom.pp v; v and eq x get set = eval_rhs_event x; match S.system x with diff --git a/src/solver/sLRterm.ml b/src/solver/sLRterm.ml index 7cde3e10ae..8838b3f02b 100644 --- a/src/solver/sLRterm.ml +++ b/src/solver/sLRterm.ml @@ -63,14 +63,14 @@ module SLR3term = HM.replace rho x (S.Dom.bot ()); HM.replace infl x (VS.add x VS.empty); let c = if side then count_side else count in - if tracing then trace "sol" "INIT: Var: %a with prio %d" S.Var.pretty_trace x !c; + if tracing then trace "sol" "INIT: Var: %a with prio %d" S.Var.pp_trace x !c; HM.replace key x !c; decr c end in let sides x = let w = try HM.find set x with Not_found -> VS.empty in let v = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ()) in - if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pretty_trace x S.Dom.pretty v; v + if tracing then trace "sol" "SIDES: Var: %a\nVal: %a" S.Var.pp_trace x S.Dom.pp v; v in let rec iterate b_old prio = if H.size !q = 0 || min_key q > prio then () @@ -121,7 +121,7 @@ module SLR3term = ) *) (* if S.Dom.is_bot d then print_endline "BOT" else *) - if tracing then trace "sol" "SIDE: Var: %a\nVal: %a" S.Var.pretty_trace y S.Dom.pretty d; + if tracing then trace "sol" "SIDE: Var: %a\nVal: %a" S.Var.pp_trace y S.Dom.pp d; let first = not (Set.mem y !effects) in effects := Set.add y !effects; if first then ( @@ -132,7 +132,7 @@ module SLR3term = ignore @@ do_var false y (* solve ~side:true y *) ) else ( - (* trace "sol" "SIDE: Var: %a already exists with Prio: %i and Val: %a" S.Var.pretty_trace y (HM.find key y) S.Dom.pretty d; *) + (* trace "sol" "SIDE: Var: %a already exists with Prio: %i and Val: %a" S.Var.pp_trace y (HM.find key y) S.Dom.pp d; *) if HM.find key y < 0 then ( HM.replace key y (Ref.post_decr count_side); q := rebuild !q @@ -155,28 +155,28 @@ module SLR3term = if wpx then if S.Dom.leq tmp old then ( let nar = narrow old tmp in - if tracing then trace "sol" "NARROW1: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar; + if tracing then trace "sol" "NARROW1: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp S.Dom.pp nar; nar, true ) else if b_old then ( let nar = narrow old tmp in - if tracing then trace "sol" "NARROW2: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty nar; + if tracing then trace "sol" "NARROW2: Var: %a\nOld: %a\nNew: %a\nNarrow: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp S.Dom.pp nar; nar, true ) else ( let wid = S.Dom.widen old (S.Dom.join old tmp) in - if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty wid; + if tracing then trace "sol" "WIDEN: Var: %a\nOld: %a\nNew: %a\nWiden: %a" S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp S.Dom.pp wid; wid, false ) else tmp, b_old in - if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ; - if tracing then trace "sol" "Contrib:%a" S.Dom.pretty val_new; + if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ; + if tracing then trace "sol" "Contrib:%a" S.Dom.pp val_new; if S.Dom.equal old val_new then () else begin update_var_event x old val_new; - if tracing then trace "sol" "New Value:%a" S.Dom.pretty val_new; + if tracing then trace "sol" "New Value:%a" S.Dom.pp val_new; HM.replace rho x val_new; let w = try HM.find infl x with Not_found -> VS.empty in (* let w = if wpx then VS.add x w else w in *) diff --git a/src/solver/sideWPointSelect.ml b/src/solver/sideWPointSelect.ml index fc0fd17fa8..6f6d01a55d 100644 --- a/src/solver/sideWPointSelect.ml +++ b/src/solver/sideWPointSelect.ml @@ -202,7 +202,7 @@ module Cycle : S = let should_mark_wpoint state called old_sides x y cycle = match cycle with | Some cycle -> - if tracing && cycle then trace "side_widen" "cycle: should mark wpoint %a" S.Var.pretty_trace y; + if tracing && cycle then trace "side_widen" "cycle: should mark wpoint %a" S.Var.pp_trace y; cycle | None -> failwith "destabilize_vs information not provided to side_widen cycle strategy"; diff --git a/src/solver/td3.ml b/src/solver/td3.ml index a3ecd439e9..8d64e6d7b1 100644 --- a/src/solver/td3.ml +++ b/src/solver/td3.ml @@ -304,7 +304,7 @@ module Base = let cache_sizes = ref [] in let add_infl y x = - if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x; + if tracing then trace "sol2" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x; HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty)); if collect_dep then HM.replace dep x (VS.add y (HM.find_default dep x VS.empty)); @@ -326,7 +326,7 @@ module Base = | Some old_gas -> let decremented_gas = old_gas - 1 in if decremented_gas >= 0 then ( - if tracing then trace "widengas" "reducing gas of %a: %d -> %d" S.Var.pretty_trace x old_gas decremented_gas; + if tracing then trace "widengas" "reducing gas of %a: %d -> %d" S.Var.pp_trace x old_gas decremented_gas; HM.replace wpoint_gas x decremented_gas ) | None -> ((* Not a widening point *)) in @@ -335,7 +335,7 @@ module Base = (* Same as destabilize, but returns true if it destabilized a called var, or a var in vs which was stable. *) let rec destabilize_vs x = (* TODO remove? Only used for side_widen cycle. *) - if tracing then trace "sol2" "destabilize_vs %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "destabilize_vs %a" S.Var.pp_trace x; let w = HM.find_default infl x VS.empty in HM.replace infl x VS.empty; VS.fold (fun y b -> @@ -350,11 +350,11 @@ module Base = ) w false (* nosemgrep: fold-exists *) (* does side effects *) and eq_wrapper x eqx = ((UpdateRule.get_wrapper ~solve_widen:(fun x-> solve x Widen) ~init ~stable ~data:update_rule_data ~sides ~add_sides ~rho ~destabilize ~side ~assert_can_receive_side):UpdateRule.eq_wrapper) x eqx and solve ?reuse_eq x phase = - if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %a" S.Var.pretty_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) pretty_wpoint x; + if tracing then trace "sol2" "solve %a, phase: %s, called: %b, stable: %b, wpoint: %a" S.Var.pp_trace x (show_phase phase) (HM.mem called x) (HM.mem stable x) pretty_wpoint x; init x; assert (Hooks.system x <> None); if not (HM.mem called x || HM.mem stable x) then ( - if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "stable add %a" S.Var.pp_trace x; HM.replace stable x (); HM.replace called x (); (* Here we cache should_widen x before eq. If during eq eval makes x wpoint (with config widen_gas = 0), then be still don't apply widening the first time, but just overwrite. @@ -368,7 +368,7 @@ module Base = match reuse_eq with | Some d when narrow_reuse -> (* Do not reset deps for reuse of eq *) - if tracing then trace "sol2" "eq reused %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "eq reused %a" S.Var.pp_trace x; incr SolverStats.narrow_reuses; d | _ -> @@ -395,15 +395,15 @@ module Base = else box old eqd in - if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nEqd: %a\nNew value: %a" S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty eqd S.Dom.pretty wpd; + if tracing then trace "sol" "Var: %a (wp: %b)\nOld value: %a\nEqd: %a\nNew value: %a" S.Var.pp_trace x wp S.Dom.pp old S.Dom.pp eqd S.Dom.pp wpd; if cache then ( - if tracing then trace "cache" "cache size %d for %a" (HM.length l) S.Var.pretty_trace x; + if tracing then trace "cache" "cache size %d for %a" (HM.length l) S.Var.pp_trace x; cache_sizes := HM.length l :: !cache_sizes; ); if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( (* value changed *) if tracing then trace "sol" "Changed"; - (* if tracing && not (S.Dom.is_bot old) && wp then trace "solchange" "%a (wpx: %a): %a -> %a" S.Var.pretty_trace x pretty_wpoint x S.Dom.pretty old S.Dom.pretty wpd; *) - if tracing && not (S.Dom.is_bot old) && wp then trace "solchange" "%a (wpx: %a): %a" S.Var.pretty_trace x pretty_wpoint x S.Dom.pretty_diff (wpd, old); + (* if tracing && not (S.Dom.is_bot old) && wp then trace "solchange" "%a (wpx: %a): %a -> %a" S.Var.pp_trace x pretty_wpoint x S.Dom.pp old S.Dom.pp wpd; *) + if tracing && not (S.Dom.is_bot old) && wp then trace "solchange" "%a (wpx: %a): %a" S.Var.pp_trace x pretty_wpoint x S.Dom.pretty_diff (wpd, old); update_var_event x old wpd; HM.replace rho x wpd; destabilize x; @@ -411,30 +411,30 @@ module Base = ) else ( (* TODO: why non-equal and non-stable checks in switched order compared to TD3 paper? *) if not (HM.mem stable x) then ( (* value unchanged, but not stable, i.e. destabilized itself during rhs *) - if tracing then trace "sol2" "solve still unstable %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "solve still unstable %a" S.Var.pp_trace x; (solve[@tailcall]) x Widen ) else ( if term && phase = Widen && HM.mem wpoint_gas x then ( (* TODO: or use wp? *) - if tracing then trace "sol2" "solve switching to narrow %a" S.Var.pretty_trace x; - if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "solve switching to narrow %a" S.Var.pp_trace x; + if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace x; HM.remove stable x; HM.remove superstable x; Hooks.stable_remove x; (solve[@tailcall]) ~reuse_eq:eqd x Narrow ) else if remove_wpoint && not space && (not term || phase = Narrow) then ( (* this makes e.g. nested loops precise, ex. tests/regression/34-localization/01-nested.c - if we do not remove wpoint, the inner loop head will stay a wpoint and widen the outer loop variable. *) - if tracing then trace "sol2" "solve removing wpoint %a (%a)" S.Var.pretty_trace x pretty_wpoint x; + if tracing then trace "sol2" "solve removing wpoint %a (%a)" S.Var.pp_trace x pretty_wpoint x; HM.remove wpoint_gas x; ) ) ) ) and eq x get set demand = - if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "eq %a" S.Var.pp_trace x; match Hooks.system x with | None -> S.Dom.bot () | Some f -> f get set demand and simple_solve l x y = - if tracing then trace "sol2" "simple_solve %a (rhs: %b)" S.Var.pretty_trace y (Hooks.system y <> None); + if tracing then trace "sol2" "simple_solve %a (rhs: %b)" S.Var.pp_trace y (Hooks.system y <> None); if Hooks.system y = None then (init y; HM.replace stable y (); HM.find rho y) else (* TODO: should td_space store information for widening points with remaining gas? *) if not space || HM.mem wpoint_gas y then (solve y Widen; HM.find rho y) else @@ -453,7 +453,7 @@ module Base = else (if cache then HM.replace l y eqd; eqd) ) and eval l x y = - if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y; + if tracing then trace "sol2" "eval %a ## %a" S.Var.pp_trace x S.Var.pp_trace y; get_var_event y; if HM.mem called y then ( if restart_wpoint && not (HM.mem wpoint_gas y) then ( @@ -461,30 +461,30 @@ module Base = The loop body might then side effect the old value, see tests/incremental/06-local-wpoint-read. Here we avoid this, by setting it to bottom for the loop body eval. *) if not (restart_once && HM.mem restarted_wpoint y) then ( - if tracing then trace "sol2" "wpoint restart %a ## %a" S.Var.pretty_trace y S.Dom.pretty (HM.find_default rho y (S.Dom.bot ())); + if tracing then trace "sol2" "wpoint restart %a ## %a" S.Var.pp_trace y S.Dom.pp (HM.find_default rho y (S.Dom.bot ())); HM.replace rho y (S.Dom.bot ()); if restart_once then (* avoid populating hashtable unnecessarily *) HM.replace restarted_wpoint y (); ) ); - if tracing then trace "sol2" "eval adding wpoint %a from %a" S.Var.pretty_trace y S.Var.pretty_trace x; + if tracing then trace "sol2" "eval adding wpoint %a from %a" S.Var.pp_trace y S.Var.pp_trace x; mark_wpoint y default_widen_gas; ); let tmp = simple_solve l x y in if HM.mem rho y then add_infl y x; - if tracing then trace "sol2" "eval %a ## %a -> %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty tmp; + if tracing then trace "sol2" "eval %a ## %a -> %a" S.Var.pp_trace x S.Var.pp_trace y S.Dom.pp tmp; tmp and side ?x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *) - if tracing then trace "sol2" "side to %a (wpx: %a) from %a ## value: %a" S.Var.pretty_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty d; + if tracing then trace "sol2" "side to %a (wpx: %a) from %a ## value: %a" S.Var.pp_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pp_trace ())) x S.Dom.pp d; assert_can_receive_side y; init y; WPS.notify_side wps_data x y; let widen a b = - if M.tracing then M.traceli "sol2" "side widen %a %a" S.Dom.pretty a S.Dom.pretty b; + if M.tracing then M.traceli "sol2" "side widen %a %a" S.Dom.pp a S.Dom.pp b; let r = S.Dom.widen a (S.Dom.join a b) in - if M.tracing then M.traceu "sol2" "-> %a" S.Dom.pretty r; + if M.tracing then M.traceu "sol2" "-> %a" S.Dom.pp r; r in let old_sides = HM.find_default sides y VS.empty in @@ -494,11 +494,11 @@ module Base = in let old = HM.find rho y in let tmp = op old d in - if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y; + if tracing then trace "sol2" "stable add %a" S.Var.pp_trace y; HM.replace stable y (); if not (S.Dom.leq tmp old) then ( - if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %a) from %a: %a -> %a" S.Var.pretty_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty old S.Dom.pretty tmp; - if tracing && not (S.Dom.is_bot old) then trace "solchange" "side to %a (wpx: %a) from %a: %a" S.Var.pretty_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pretty_trace ())) x S.Dom.pretty_diff (tmp, old); + if tracing && not (S.Dom.is_bot old) then trace "solside" "side to %a (wpx: %a) from %a: %a -> %a" S.Var.pp_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pp_trace ())) x S.Dom.pp old S.Dom.pp tmp; + if tracing && not (S.Dom.is_bot old) then trace "solchange" "side to %a (wpx: %a) from %a: %a" S.Var.pp_trace y pretty_wpoint y (Pretty.docOpt (S.Var.pp_trace ())) x S.Dom.pretty_diff (tmp, old); (match x with | Some x -> @@ -515,7 +515,7 @@ module Base = (* make y a widening point if ... This will only matter for the next side _ y. *) if WPS.should_mark_wpoint wps_data called old_sides x y destabilized_vs then ( - if tracing then trace "sol2" "side adding wpoint %a from %a" S.Var.pretty_trace y (Pretty.docOpt (S.Var.pretty_trace ())) x; + if tracing then trace "sol2" "side adding wpoint %a from %a" S.Var.pp_trace y (Pretty.docOpt (S.Var.pp_trace ())) x; mark_wpoint y default_side_widen_gas ); @@ -523,7 +523,7 @@ module Base = if not vetoed_widen then reduce_gas y; ) and demand l x y = - if tracing then trace "sol2" "demand weak dep %a from %a" S.Var.pretty_trace y S.Var.pretty_trace x; + if tracing then trace "sol2" "demand weak dep %a from %a" S.Var.pp_trace y S.Var.pp_trace x; match weak_deps_handling with | "none" -> ignore (eval l x y) | "eager" -> @@ -533,7 +533,7 @@ module Base = HM.replace weak_dep x (VS.add y (try HM.find weak_dep x with Not_found -> VS.empty)) | _ -> assert false and init x = - if tracing then trace "sol2" "init %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "init %a" S.Var.pp_trace x; if not (HM.mem rho x) then ( new_var_event x; HM.replace rho x (S.Dom.bot ()) @@ -541,7 +541,7 @@ module Base = in let set_start (x,d) = - if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d; + if tracing then trace "sol2" "set_start %a ## %a" S.Var.pp_trace x S.Dom.pp d; init x; UpdateRule.register_start update_rule_data x d; HM.replace rho x d; @@ -550,11 +550,11 @@ module Base = in let rec destabilize_normal x = - if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace x; let w = HM.find_default infl x VS.empty in HM.replace infl x VS.empty; VS.iter (fun y -> - if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace y; + if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace y; HM.remove stable y; HM.remove superstable y; Hooks.stable_remove y; @@ -572,7 +572,7 @@ module Base = if GobConfig.get_bool "incremental.load" then ( let restart_leaf x = - if tracing then trace "sol2" "Restarting to bot %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "Restarting to bot %a" S.Var.pp_trace x; Logs.debug "Restarting to bot %a" S.Var.pretty_trace x; HM.replace rho x (S.Dom.bot ()); (* HM.remove rho x; *) @@ -592,7 +592,7 @@ module Base = (* destabilize which restarts side-effected vars *) (* side_fuel specifies how many times (in recursion depth) to destabilize side_infl, None means infinite *) let rec destabilize_with_side ~side_fuel x = - if tracing then trace "sol2" "destabilize_with_side %a %a" S.Var.pretty_trace x (Pretty.docOpt (Pretty.dprintf "%d")) side_fuel; + if tracing then trace "sol2" "destabilize_with_side %a %a" S.Var.pp_trace x (Pretty.docOpt (Pretty.dprintf "%d")) side_fuel; (* retrieve and remove (side-effect) dependencies/influences *) let w_side_dep = HM.find_default side_dep x VS.empty in @@ -620,8 +620,8 @@ module Base = (* destabilize side dep to redo side effects *) VS.iter (fun y -> - if tracing then trace "sol2" "destabilize_with_side %a side_dep %a" S.Var.pretty_trace x S.Var.pretty_trace y; - if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace y; + if tracing then trace "sol2" "destabilize_with_side %a side_dep %a" S.Var.pp_trace x S.Var.pp_trace y; + if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace y; HM.remove stable y; HM.remove superstable y; Hooks.stable_remove y; @@ -631,8 +631,8 @@ module Base = (* destabilize eval infl *) VS.iter (fun y -> - if tracing then trace "sol2" "destabilize_with_side %a infl %a" S.Var.pretty_trace x S.Var.pretty_trace y; - if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace y; + if tracing then trace "sol2" "destabilize_with_side %a infl %a" S.Var.pp_trace x S.Var.pp_trace y; + if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace y; HM.remove stable y; HM.remove superstable y; Hooks.stable_remove y; @@ -649,8 +649,8 @@ module Base = in (* TODO: should this also be conditional on restart_only_globals? right now goes through function entry side effects, but just doesn't restart them *) VS.iter (fun y -> - if tracing then trace "sol2" "destabilize_with_side %a side_infl %a" S.Var.pretty_trace x S.Var.pretty_trace y; - if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace y; + if tracing then trace "sol2" "destabilize_with_side %a side_infl %a" S.Var.pp_trace x S.Var.pp_trace y; + if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace y; HM.remove stable y; HM.remove superstable y; Hooks.stable_remove y; @@ -722,8 +722,8 @@ module Base = HM.remove side_dep x; (* destabilize side dep to redo side effects *) VS.iter (fun y -> - if tracing then trace "sol2" "destabilize_leaf %a side_dep %a" S.Var.pretty_trace x S.Var.pretty_trace y; - if tracing then trace "sol2" "stable remove %a" S.Var.pretty_trace y; + if tracing then trace "sol2" "destabilize_leaf %a side_dep %a" S.Var.pp_trace x S.Var.pp_trace y; + if tracing then trace "sol2" "stable remove %a" S.Var.pp_trace y; HM.remove stable y; HM.remove superstable y; Hooks.stable_remove y; @@ -900,7 +900,7 @@ module Base = let restore () = let get x = let d = get ~check:true x in - if tracing then trace "sol2" "restored var %a ## %a" S.Var.pretty_trace x S.Dom.pretty d + if tracing then trace "sol2" "restored var %a ## %a" S.Var.pp_trace x S.Dom.pp d in List.iter get vs; HM.filteri_inplace (fun x _ -> HM.mem visited x) rho @@ -1183,7 +1183,7 @@ module DepVals(UpdateRule: Td3UpdateRule.S): DemandEqIncrSolver = in match all_deps_unchanged with | Some oldv -> - if M.tracing then M.trace "sol2" "All deps unchanged for %a, not evaluating RHS" S.Var.pretty_trace x; + if M.tracing then M.trace "sol2" "All deps unchanged for %a, not evaluating RHS" S.Var.pp_trace x; oldv | None -> (* This needs to be done here as a local wrapper around get to avoid polluting dep_vals during earlier checks *) diff --git a/src/solver/td3UpdateRule.ml b/src/solver/td3UpdateRule.ml index 873026660c..7ae7910a49 100644 --- a/src/solver/td3UpdateRule.ml +++ b/src/solver/td3UpdateRule.ml @@ -124,11 +124,11 @@ module Narrow:S = ) ) new_acc; and divided_side (phase:divided_side_mode) x y d: bool = - if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d; - if tracing then trace "sol2" "divided side to %a from %a ## value: %a" S.Var.pretty_trace y S.Var.pretty_trace x S.Dom.pretty d; + if tracing then trace "side" "divided side to %a from %a ## value: %a" S.Var.pp_trace y S.Var.pp_trace x S.Dom.pp d; + if tracing then trace "sol2" "divided side to %a from %a ## value: %a" S.Var.pp_trace y S.Var.pp_trace x S.Dom.pp d; assert_can_receive_side y; init y; - if tracing then trace "sol2" "stable add %a" S.Var.pretty_trace y; + if tracing then trace "sol2" "stable add %a" S.Var.pp_trace y; HM.replace stable y (); let sided = GobOption.exists (VS.mem x) (HM.find_option sides y) in @@ -169,7 +169,7 @@ module Narrow:S = in if not (S.Dom.equal old_side new_side) then ( - if tracing then trace "side" "divided side to %a from %a changed (phase: %s) Old value: %a ## New value: %a" S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_mode phase) S.Dom.pretty old_side S.Dom.pretty new_side; + if tracing then trace "side" "divided side to %a from %a changed (phase: %s) Old value: %a ## New value: %a" S.Var.pp_trace y S.Var.pp_trace x (show_divided_side_mode phase) S.Dom.pp old_side S.Dom.pp new_side; if S.Dom.is_bot new_side && narrow_gas = None then HM.remove y_sides x @@ -192,7 +192,7 @@ module Narrow:S = in if not (S.Dom.equal y_newval y_oldval) then ( if tracing then trace "side" "value of %a changed by side from %a (phase: %s) Old value: %a ## New value: %a" - S.Var.pretty_trace y S.Var.pretty_trace x (show_divided_side_mode phase) S.Dom.pretty y_oldval S.Dom.pretty y_newval; + S.Var.pp_trace y S.Var.pp_trace x (show_divided_side_mode phase) S.Dom.pp y_oldval S.Dom.pp y_newval; HM.replace rho y y_newval; destabilize y; ); diff --git a/src/solver/td_simplified.ml b/src/solver/td_simplified.ml index d2e8c93241..6a07915887 100644 --- a/src/solver/td_simplified.ml +++ b/src/solver/td_simplified.ml @@ -34,38 +34,38 @@ module Base : GenericEqSolver = ); let add_infl y x = - if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x; + if tracing then trace "infl" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x; HM.replace infl y (VS.add x (HM.find_default infl y VS.empty)); in let init x = if not (HM.mem rho x) then ( new_var_event x; - if tracing then trace "init" "init %a" S.Var.pretty_trace x; + if tracing then trace "init" "init %a" S.Var.pp_trace x; HM.replace rho x (S.Dom.bot ()) ) in let eq x get set = - if tracing then trace "eq" "eq %a" S.Var.pretty_trace x; + if tracing then trace "eq" "eq %a" S.Var.pp_trace x; match S.system x with | None -> S.Dom.bot () | Some f -> f get set in let rec destabilize x = - if tracing then trace "destab" "destabilize %a" S.Var.pretty_trace x; + if tracing then trace "destab" "destabilize %a" S.Var.pp_trace x; let w = HM.find_default infl x VS.empty in HM.replace infl x VS.empty; VS.iter (fun y -> - if tracing then trace "destab" "stable remove %a" S.Var.pretty_trace y; + if tracing then trace "destab" "stable remove %a" S.Var.pp_trace y; HM.remove stable y; destabilize y ) w in let rec query x y = (* ~eval in td3 *) - if tracing then trace "solver_query" "entering query for %a; stable %b; called %b" S.Var.pretty_trace y (HM.mem stable y) (HM.mem called y); + if tracing then trace "solver_query" "entering query for %a; stable %b; called %b" S.Var.pp_trace y (HM.mem stable y) (HM.mem called y); get_var_event y; if not (HM.mem called y) then ( if S.system y = None then ( @@ -77,20 +77,20 @@ module Base : GenericEqSolver = iterate y; HM.remove called y) ) else ( - if tracing && not (HM.mem wpoint y) then trace "wpoint" "query adding wpoint %a" S.Var.pretty_trace y; + if tracing && not (HM.mem wpoint y) then trace "wpoint" "query adding wpoint %a" S.Var.pp_trace y; HM.replace wpoint y (); ); let tmp = HM.find rho y in add_infl y x; - if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pretty_trace y S.Dom.pretty tmp; + if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pp_trace y S.Dom.pp tmp; tmp and side x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *) - if tracing then trace "side" "side to %a (wpx: %b) from %a; value: %a" S.Var.pretty_trace y (HM.mem wpoint y) S.Var.pretty_trace x S.Dom.pretty d; + if tracing then trace "side" "side to %a (wpx: %b) from %a; value: %a" S.Var.pp_trace y (HM.mem wpoint y) S.Var.pp_trace x S.Dom.pp d; assert (S.system y = None); init y; let widen a b = - if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pretty_trace y; + if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pp_trace y; S.Dom.widen a (S.Dom.join a b) in let op a b = if HM.mem wpoint y then widen a b else S.Dom.join a b @@ -99,16 +99,16 @@ module Base : GenericEqSolver = let tmp = op old d in HM.replace stable y (); if not (S.Dom.leq tmp old) then ( - if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a new: %a" S.Var.pretty_trace y (HM.mem wpoint y) S.Var.pretty_trace x S.Dom.pretty tmp; + if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a new: %a" S.Var.pp_trace y (HM.mem wpoint y) S.Var.pp_trace x S.Dom.pp tmp; HM.replace rho y tmp; destabilize y; (* make y a widening point. This will only matter for the next side _ y. *) - if tracing && not (HM.mem wpoint y) then trace "wpoint" "side adding wpoint %a" S.Var.pretty_trace y; + if tracing && not (HM.mem wpoint y) then trace "wpoint" "side adding wpoint %a" S.Var.pp_trace y; HM.replace wpoint y () ) and iterate x = (* ~(inner) solve in td3*) - if tracing then trace "iter" "begin iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x); + if tracing then trace "iter" "begin iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pp_trace x (HM.mem called x) (HM.mem stable x) (HM.mem wpoint x); init x; assert (S.system x <> None); if not (HM.mem stable x) then ( @@ -119,26 +119,26 @@ module Base : GenericEqSolver = let wpd = (* d after widen/narrow (if wp) *) if not wp then eqd else ( - if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x; + if M.tracing then M.trace "wpoint" "widen %a" S.Var.pp_trace x; box old eqd) in if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( (* old != wpd *) - if tracing && not (S.Dom.is_bot old) then trace "update" "%a (wpx: %b): %a" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old); + if tracing && not (S.Dom.is_bot old) then trace "update" "%a (wpx: %b): %a" S.Var.pp_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old); update_var_event x old wpd; HM.replace rho x wpd; destabilize x; - if tracing then trace "iter" "iterate changed %a" S.Var.pretty_trace x; + if tracing then trace "iter" "iterate changed %a" S.Var.pp_trace x; (iterate[@tailcall]) x ) else ( (* old == wpd *) if not (HM.mem stable x) then ( (* value unchanged, but not stable, i.e. destabilized itself during rhs *) - if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x; + if tracing then trace "iter" "iterate still unstable %a" S.Var.pp_trace x; (iterate[@tailcall]) x ) else ( (* this makes e.g. nested loops precise, ex. tests/regression/34-localization/01-nested.c - if we do not remove wpoint, the inner loop head will stay a wpoint and widen the outer loop variable. *) - if tracing && (HM.mem wpoint x) then trace "wpoint" "iterate removing wpoint %a" S.Var.pretty_trace x; + if tracing && (HM.mem wpoint x) then trace "wpoint" "iterate removing wpoint %a" S.Var.pp_trace x; HM.remove wpoint x ) ) @@ -171,7 +171,7 @@ module Base : GenericEqSolver = flush_all (); ); List.iter (fun x -> HM.replace called x (); - if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x; + if tracing then trace "multivar" "solving for %a" S.Var.pp_trace x; iterate x; HM.remove called x ) unstable_vs; diff --git a/src/solver/td_simplified_ref.ml b/src/solver/td_simplified_ref.ml index 2968dc1b84..57ebe9b637 100644 --- a/src/solver/td_simplified_ref.ml +++ b/src/solver/td_simplified_ref.ml @@ -33,7 +33,7 @@ module Base : GenericEqSolver = ); let add_infl y x = - if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x; + if tracing then trace "infl" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x; let y_ref = HM.find data y in y_ref := { !y_ref with infl = VS.add x !y_ref.infl } in @@ -45,7 +45,7 @@ module Base : GenericEqSolver = | None -> begin new_var_event x; - if tracing then trace "init" "init %a" S.Var.pretty_trace x; + if tracing then trace "init" "init %a" S.Var.pp_trace x; let data_x = ref { infl = VS.empty; value = S.Dom.bot (); @@ -59,19 +59,19 @@ module Base : GenericEqSolver = in let eq x get set = - if tracing then trace "eq" "eq %a" S.Var.pretty_trace x; + if tracing then trace "eq" "eq %a" S.Var.pp_trace x; match S.system x with | None -> S.Dom.bot () | Some f -> f get set in let rec destabilize x = - if tracing then trace "destab" "destabilize %a" S.Var.pretty_trace x; + if tracing then trace "destab" "destabilize %a" S.Var.pp_trace x; let x_ref = HM.find data x in let w = !x_ref.infl in x_ref := { !x_ref with infl = VS.empty }; VS.iter (fun y -> - if tracing then trace "destab" "stable remove %a" S.Var.pretty_trace y; + if tracing then trace "destab" "stable remove %a" S.Var.pp_trace y; let y_ref = HM.find data y in y_ref := { !y_ref with stable = false }; destabilize y @@ -80,7 +80,7 @@ module Base : GenericEqSolver = let rec query x y = let y_ref = init y in - if tracing then trace "sol_query" "entering query for %a; stable %b; called %b" S.Var.pretty_trace y (!y_ref.stable) (!y_ref.called); + if tracing then trace "sol_query" "entering query for %a; stable %b; called %b" S.Var.pp_trace y (!y_ref.stable) (!y_ref.called); get_var_event y; if not (!y_ref.called) then ( if S.system y = None then ( @@ -91,20 +91,20 @@ module Base : GenericEqSolver = iterate y; y_ref := { !y_ref with called = false };) ) else ( - if tracing && not (!y_ref.wpoint) then trace "wpoint" "query adding wpoint %a" S.Var.pretty_trace y; + if tracing && not (!y_ref.wpoint) then trace "wpoint" "query adding wpoint %a" S.Var.pp_trace y; y_ref := { !y_ref with wpoint = true }; ); let tmp = !y_ref.value in add_infl y x; - if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pretty_trace y S.Dom.pretty tmp; + if tracing then trace "answer" "exiting query for %a\nanswer: %a" S.Var.pp_trace y S.Dom.pp tmp; tmp and side x y d = (* side from x to y; only to variables y w/o rhs; x only used for trace *) assert (S.system y = None); let y_ref = init y in - if tracing then trace "side" "side to %a (wpx: %b) from %a ## value: %a" S.Var.pretty_trace y (!y_ref.wpoint) S.Var.pretty_trace x S.Dom.pretty d; + if tracing then trace "side" "side to %a (wpx: %b) from %a ## value: %a" S.Var.pp_trace y (!y_ref.wpoint) S.Var.pp_trace x S.Dom.pp d; let widen a b = - if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pretty_trace y; + if M.tracing then M.trace "wpoint" "side widen %a" S.Var.pp_trace y; S.Dom.widen a (S.Dom.join a b) in let op a b = if !y_ref.wpoint then widen a b else S.Dom.join a b @@ -113,11 +113,11 @@ module Base : GenericEqSolver = let tmp = op old d in y_ref := { !y_ref with stable = true }; if not (S.Dom.leq tmp old) then ( - if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a: %a -> %a" S.Var.pretty_trace y (!y_ref.wpoint) S.Var.pretty_trace x S.Dom.pretty old S.Dom.pretty tmp; + if tracing && not (S.Dom.is_bot old) then trace "update" "side to %a (wpx: %b) from %a: %a -> %a" S.Var.pp_trace y (!y_ref.wpoint) S.Var.pp_trace x S.Dom.pp old S.Dom.pp tmp; y_ref := { !y_ref with value = tmp }; destabilize y; (* make y a widening point. This will only matter for the next side _ y. *) - if tracing && not (!y_ref.wpoint) then trace "wpoint" "side adding wpoint %a" S.Var.pretty_trace y; + if tracing && not (!y_ref.wpoint) then trace "wpoint" "side adding wpoint %a" S.Var.pp_trace y; y_ref := { !y_ref with wpoint = true }; ) @@ -125,7 +125,7 @@ module Base : GenericEqSolver = (* beginning of iterate*) let x_ref = init x in - if tracing then trace "iter" "iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pretty_trace x (!x_ref.called) (!x_ref.stable) (!x_ref.wpoint); + if tracing then trace "iter" "iterate %a, called: %b, stable: %b, wpoint: %b" S.Var.pp_trace x (!x_ref.called) (!x_ref.stable) (!x_ref.wpoint); assert (S.system x <> None); if not (!x_ref.stable) then ( x_ref := { !x_ref with stable = true }; @@ -135,26 +135,26 @@ module Base : GenericEqSolver = let wpd = (* d after widen/narrow (if wp) *) if not wp then eqd else ( - if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x; + if M.tracing then M.trace "wpoint" "widen %a" S.Var.pp_trace x; box old eqd) in if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then ( (* old != wpd *) - if tracing && not (S.Dom.is_bot old) && !x_ref.wpoint then trace "solchange" "%a (wpx: %b): %a" S.Var.pretty_trace x (!x_ref.wpoint) S.Dom.pretty_diff (wpd, old); + if tracing && not (S.Dom.is_bot old) && !x_ref.wpoint then trace "solchange" "%a (wpx: %b): %a" S.Var.pp_trace x (!x_ref.wpoint) S.Dom.pretty_diff (wpd, old); update_var_event x old wpd; x_ref := { !x_ref with value = wpd }; destabilize x; - if tracing then trace "iter" "iterate changed %a" S.Var.pretty_trace x; + if tracing then trace "iter" "iterate changed %a" S.Var.pp_trace x; (iterate[@tailcall]) x ) else ( (* old == wpd *) if not (!x_ref.stable) then ( (* value unchanged, but not stable, i.e. destabilized itself during rhs *) - if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x; + if tracing then trace "iter" "iterate still unstable %a" S.Var.pp_trace x; (iterate[@tailcall]) x ) else ( (* this makes e.g. nested loops precise, ex. tests/regression/34-localization/01-nested.c - if we do not remove wpoint, the inner loop head will stay a wpoint and widen the outer loop variable. *) - if tracing && (!x_ref.wpoint) then trace "wpoint" "iterate removing wpoint %a" S.Var.pretty_trace x; + if tracing && (!x_ref.wpoint) then trace "wpoint" "iterate removing wpoint %a" S.Var.pp_trace x; x_ref := { !x_ref with wpoint = false }; ) ) @@ -188,7 +188,7 @@ module Base : GenericEqSolver = List.iter (fun x -> let x_ref = HM.find data x in x_ref := { !x_ref with called = true }; - if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x; + if tracing then trace "multivar" "solving for %a" S.Var.pp_trace x; iterate x; x_ref := { !x_ref with called = false } ) unstable_vs; diff --git a/src/solver/topDown.ml b/src/solver/topDown.ml index f71481ff40..00da73ae34 100644 --- a/src/solver/topDown.ml +++ b/src/solver/topDown.ml @@ -32,7 +32,7 @@ module WP = let wpoint = HM.create 10 in let add_infl y x = - if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x; + if tracing then trace "sol2" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x; HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty)) in let add_set x y d = @@ -42,15 +42,15 @@ module WP = in let is_side x = HM.mem set x in let rec destabilize x = - (* if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x; *) + (* if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace x; *) let w = HM.find_default infl x VS.empty in HM.replace infl x VS.empty; VS.iter (fun y -> HM.remove stable y; - if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace y; + if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace y; if not (HM.mem called y) then destabilize y) w and solve x = - if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x); + if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pp_trace x (HM.mem called x) (HM.mem stable x); if not (HM.mem called x || HM.mem stable x) then ( HM.replace stable x (); HM.replace called x (); @@ -59,22 +59,22 @@ module WP = let old = HM.find rho x in let tmp' = eq x (eval x) (side x) in let tmp = S.Dom.join tmp' (sides x) in - if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ; - if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp; + if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ; + if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp; let tmp = if is_side x then S.Dom.widen old (S.Dom.join old tmp) else if wpx then box old tmp else tmp in HM.remove called x; if not (S.Dom.equal old tmp) then ( - if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty (S.Dom.widen old (S.Dom.join old tmp)); + if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pp old S.Dom.pp tmp S.Dom.pp (S.Dom.widen old (S.Dom.join old tmp)); update_var_event x old tmp; - if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp; - if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pretty_trace x (HM.mem rho x) (is_side x) S.Dom.pretty tmp S.Dom.pretty old; + if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp; + if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pp_trace x (HM.mem rho x) (is_side x) S.Dom.pp tmp S.Dom.pp old; HM.replace rho x tmp; destabilize x; ); (solve[@tailcall]) x ) and eq x get set = - if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "eq %a" S.Var.pp_trace x; eval_rhs_event x; match S.system x with | None -> S.Dom.bot () @@ -89,7 +89,7 @@ module WP = in f get sidef and eval x y = - if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y; + if tracing then trace "sol2" "eval %a ## %a" S.Var.pp_trace x S.Var.pp_trace y; get_var_event y; if HM.mem called y || S.system y = None then HM.replace wpoint y (); solve y; @@ -97,11 +97,11 @@ module WP = HM.find rho y and sides x = let w = try HM.find set x with Not_found -> VS.empty in - let d = VS.fold (fun y d -> let r = try S.Dom.join d (HPM.find rho' (y,x)) with Not_found -> d in if tracing then trace "sol2" "sides: side %a from %a: %a" S.Var.pretty_trace x S.Var.pretty_trace y S.Dom.pretty r; r) w (S.Dom.bot ()) in - if tracing then trace "sol2" "sides %a ## %a" S.Var.pretty_trace x S.Dom.pretty d; + let d = VS.fold (fun y d -> let r = try S.Dom.join d (HPM.find rho' (y,x)) with Not_found -> d in if tracing then trace "sol2" "sides: side %a from %a: %a" S.Var.pp_trace x S.Var.pp_trace y S.Dom.pp r; r) w (S.Dom.bot ()) in + if tracing then trace "sol2" "sides %a ## %a" S.Var.pp_trace x S.Dom.pp d; d and side x y d = - if tracing then trace "sol2" "side %a ## %a (wpx: %b) ## %a" S.Var.pretty_trace x S.Var.pretty_trace y (HM.mem rho y) S.Dom.pretty d; + if tracing then trace "sol2" "side %a ## %a (wpx: %b) ## %a" S.Var.pp_trace x S.Var.pp_trace y (HM.mem rho y) S.Dom.pp d; let old = try HPM.find rho' (x,y) with Not_found -> S.Dom.bot () in if not (S.Dom.equal old d) then ( add_set x y (S.Dom.join old d); @@ -109,7 +109,7 @@ module WP = solve y; ) and init x = - if tracing then trace "sol2" "init %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "init %a" S.Var.pp_trace x; if not (HM.mem rho x) then ( new_var_event x; HM.replace rho x (S.Dom.bot ()) @@ -117,7 +117,7 @@ module WP = in let set_start (x,d) = - if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d; + if tracing then trace "sol2" "set_start %a ## %a" S.Var.pp_trace x S.Dom.pp d; init x; add_set x x d; solve x diff --git a/src/solver/topDown_deprecated.ml b/src/solver/topDown_deprecated.ml index 8d7ad781b2..61f270959c 100644 --- a/src/solver/topDown_deprecated.ml +++ b/src/solver/topDown_deprecated.ml @@ -36,16 +36,16 @@ module TD3 = let add_set x y d = HM.replace set y (VS.add x (try HM.find set y with Not_found -> VS.empty)); HPM.add rho' (x,y) d; HM.add sidevs y () in let is_side x = HM.mem set x in let make_wpoint x = - if tracing then trace "sol2" "make_wpoint %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "make_wpoint %a" S.Var.pp_trace x; HM.replace wpoint x () in let rec destabilize x = - if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace x; let t = HM.find_default infl x VS.empty in HM.replace infl x VS.empty; VS.iter (fun y -> HM.remove stable y; if not (HM.mem called y) then destabilize y) t and solve x = - if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x); + if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pp_trace x (HM.mem called x) (HM.mem stable x); if not (HM.mem called x || HM.mem stable x) then begin HM.replace called x (); let wpx = HM.mem wpoint x in @@ -54,21 +54,21 @@ module TD3 = let old = HM.find rho x in let tmp = eq x (eval x) (side x) in let tmp = S.Dom.join tmp (sides x) in - if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ; - if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp; + if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ; + if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp; let tmp = if is_side x then S.Dom.widen old (S.Dom.join old tmp) else if wpx then box old tmp else tmp in HM.remove called x; if not (S.Dom.equal old tmp) then begin update_var_event x old tmp; - if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp; - if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pretty_trace x wpx (is_side x) S.Dom.pretty tmp S.Dom.pretty old; + if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp; + if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pp_trace x wpx (is_side x) S.Dom.pp tmp S.Dom.pp old; HM.replace rho x tmp; destabilize x; (solve[@tailcall]) x; end; end; and eq x get set = - if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "eq %a" S.Var.pp_trace x; eval_rhs_event x; match S.system x with | None -> S.Dom.bot () @@ -83,7 +83,7 @@ module TD3 = in f get sidef and eval x y = - if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y; + if tracing then trace "sol2" "eval %a ## %a" S.Var.pp_trace x S.Var.pp_trace y; get_var_event y; if not (HM.mem rho y) then init y; if HM.mem called y then make_wpoint y else if neg is_side y then solve y; @@ -92,11 +92,11 @@ module TD3 = and sides x = let w = try HM.find set x with Not_found -> VS.empty in let d = VS.fold (fun z d -> try S.Dom.join d (HPM.find rho' (z,x)) with Not_found -> d) w (S.Dom.bot ()) in - if tracing then trace "sol2" "sides %a ## %a" S.Var.pretty_trace x S.Dom.pretty d; + if tracing then trace "sol2" "sides %a ## %a" S.Var.pp_trace x S.Dom.pp d; d and side x y d = if S.Dom.is_bot d then () else - if tracing then trace "sol2" "side %a ## %a (wpx: %b) ## %a" S.Var.pretty_trace x S.Var.pretty_trace y (HM.mem wpoint y) S.Dom.pretty d; + if tracing then trace "sol2" "side %a ## %a (wpx: %b) ## %a" S.Var.pp_trace x S.Var.pp_trace y (HM.mem wpoint y) S.Dom.pp d; if not (HM.mem rho y) then begin init y; add_set x y d; @@ -113,7 +113,7 @@ module TD3 = end end and init x = - if tracing then trace "sol2" "init %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "init %a" S.Var.pp_trace x; if not (HM.mem rho x) then begin new_var_event x; HM.replace rho x (S.Dom.bot ()); @@ -122,7 +122,7 @@ module TD3 = in let set_start (x,d) = - if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d; + if tracing then trace "sol2" "set_start %a ## %a" S.Var.pp_trace x S.Dom.pp d; init x; add_set x x d; solve x diff --git a/src/solver/topDown_space_cache_term.ml b/src/solver/topDown_space_cache_term.ml index 56f089156c..313519ad7f 100644 --- a/src/solver/topDown_space_cache_term.ml +++ b/src/solver/topDown_space_cache_term.ml @@ -29,16 +29,16 @@ module WP = let cache_sizes = ref [] in let add_infl y x = - if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x; + if tracing then trace "sol2" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x; HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty)) in let rec destabilize x = - if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace x; let w = HM.find_default infl x VS.empty in HM.replace infl x VS.empty; VS.iter (fun y -> HM.remove stable y; if not (HM.mem called y) then destabilize y) w and solve x phase = - if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x); + if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pp_trace x (HM.mem called x) (HM.mem stable x); if not (HM.mem called x || HM.mem stable x) then ( HM.replace stable x (); HM.replace called x (); @@ -46,17 +46,17 @@ module WP = let l = HM.create 10 in let tmp = eq x (eval l x) (side l) in let tmp = S.Dom.join tmp (try HM.find rho' x with Not_found -> S.Dom.bot ()) in - if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ; - if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp; + if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ; + if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp; HM.remove called x; let tmp = match phase with Widen -> S.Dom.widen old (S.Dom.join old tmp) | Narrow -> S.Dom.narrow old tmp in - if tracing then trace "cache" "cache size %d for %a" (HM.length l) S.Var.pretty_trace x; + if tracing then trace "cache" "cache size %d for %a" (HM.length l) S.Var.pp_trace x; cache_sizes := HM.length l :: !cache_sizes; if not (S.Dom.equal old tmp) then ( - (* if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty (S.Dom.widen old (S.Dom.join old tmp)); *) + (* if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pp old S.Dom.pp tmp S.Dom.pp (S.Dom.widen old (S.Dom.join old tmp)); *) update_var_event x old tmp; - if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp; - (* if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pretty_trace x (HM.mem rho x) (is_side x) S.Dom.pretty tmp S.Dom.pretty old; *) + if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp; + (* if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pp_trace x (HM.mem rho x) (is_side x) S.Dom.pp tmp S.Dom.pp old; *) HM.replace rho x tmp; destabilize x; (solve[@tailcall]) x phase; @@ -68,13 +68,13 @@ module WP = ); ) and eq x get set = - if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "eq %a" S.Var.pp_trace x; eval_rhs_event x; match S.system x with | None -> S.Dom.bot () | Some f -> f get set and simple_solve l x y = - if tracing then trace "sol2" "simple_solve %a (rhs: %b)" S.Var.pretty_trace y (S.system y <> None); + if tracing then trace "sol2" "simple_solve %a (rhs: %b)" S.Var.pp_trace y (S.system y <> None); if S.system y = None then init y; if HM.mem rho y then (solve y Widen; HM.find rho y) else if HM.mem called y then (init y; HM.remove l y; HM.find rho y) else @@ -87,13 +87,13 @@ module WP = else (HM.replace l y tmp; tmp) ) and eval l x y = - if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y; + if tracing then trace "sol2" "eval %a ## %a" S.Var.pp_trace x S.Var.pp_trace y; get_var_event y; let tmp = simple_solve l x y in if HM.mem rho y then add_infl y x; tmp and side l y d = - if tracing then trace "sol2" "side to %a (wpx: %b) ## value: %a" S.Var.pretty_trace y (HM.mem rho y) S.Dom.pretty d; + if tracing then trace "sol2" "side to %a (wpx: %b) ## value: %a" S.Var.pp_trace y (HM.mem rho y) S.Dom.pp d; let old = try HM.find rho' y with Not_found -> S.Dom.bot () in if not (S.Dom.leq d old) then ( HM.replace rho' y (S.Dom.join old d); @@ -103,7 +103,7 @@ module WP = solve y Widen; ) and init x = - if tracing then trace "sol2" "init %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "init %a" S.Var.pp_trace x; if not (HM.mem rho x) then ( new_var_event x; HM.replace rho x (S.Dom.bot ()) @@ -111,7 +111,7 @@ module WP = in let set_start (x,d) = - if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d; + if tracing then trace "sol2" "set_start %a ## %a" S.Var.pp_trace x S.Dom.pp d; init x; HM.replace rho x d; HM.replace rho' x d; @@ -175,7 +175,7 @@ module WP = let restore () = let get x = let d = get x in - if tracing then trace "sol2" "restored var %a ## %a" S.Var.pretty_trace x S.Dom.pretty d + if tracing then trace "sol2" "restored var %a ## %a" S.Var.pp_trace x S.Dom.pp d in List.iter get vs in diff --git a/src/solver/topDown_term.ml b/src/solver/topDown_term.ml index 3a67cda982..82b87dfd3e 100644 --- a/src/solver/topDown_term.ml +++ b/src/solver/topDown_term.ml @@ -29,19 +29,19 @@ module WP = let wpoint = HM.create 10 in let add_infl y x = - if tracing then trace "sol2" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x; + if tracing then trace "sol2" "add_infl %a %a" S.Var.pp_trace y S.Var.pp_trace x; HM.replace infl y (VS.add x (try HM.find infl y with Not_found -> VS.empty)) in let rec destabilize x = - if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace x; let w = HM.find_default infl x VS.empty in HM.replace infl x VS.empty; VS.iter (fun y -> HM.remove stable y; - (* if tracing then trace "sol2" "destabilize %a" S.Var.pretty_trace y; *) + (* if tracing then trace "sol2" "destabilize %a" S.Var.pp_trace y; *) if not (HM.mem called y) then destabilize y) w and solve x phase = - if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pretty_trace x (HM.mem called x) (HM.mem stable x); + if tracing then trace "sol2" "solve %a, called: %b, stable: %b" S.Var.pp_trace x (HM.mem called x) (HM.mem stable x); if not (HM.mem called x || HM.mem stable x) then ( HM.replace stable x (); HM.replace called x (); @@ -50,15 +50,15 @@ module WP = let old = HM.find rho x in let tmp = eq x (eval x) side in let tmp = S.Dom.join tmp (try HM.find rho' x with Not_found -> S.Dom.bot ()) in - if tracing then trace "sol" "Var: %a" S.Var.pretty_trace x ; - if tracing then trace "sol" "Contrib:%a" S.Dom.pretty tmp; + if tracing then trace "sol" "Var: %a" S.Var.pp_trace x ; + if tracing then trace "sol" "Contrib:%a" S.Dom.pp tmp; HM.remove called x; let tmp = if wpx then match phase with Widen -> S.Dom.widen old (S.Dom.join old tmp) | Narrow -> S.Dom.narrow old tmp else tmp in if not (S.Dom.equal old tmp) then ( - (* if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pretty old S.Dom.pretty tmp S.Dom.pretty (S.Dom.widen old (S.Dom.join old tmp)); *) + (* if tracing then if is_side x then trace "sol2" "solve side: old = %a, tmp = %a, widen = %a" S.Dom.pp old S.Dom.pp tmp S.Dom.pp (S.Dom.widen old (S.Dom.join old tmp)); *) update_var_event x old tmp; - if tracing then trace "sol" "New Value:%a" S.Dom.pretty tmp; - (* if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pretty_trace x (HM.mem rho x) (is_side x) S.Dom.pretty tmp S.Dom.pretty old; *) + if tracing then trace "sol" "New Value:%a" S.Dom.pp tmp; + (* if tracing then trace "sol2" "new value for %a (wpx: %b, is_side: %b) is %a. Old value was %a" S.Var.pp_trace x (HM.mem rho x) (is_side x) S.Dom.pp tmp S.Dom.pp old; *) HM.replace rho x tmp; destabilize x; (solve[@tailcall]) x phase; @@ -70,13 +70,13 @@ module WP = ); ) and eq x get set = - if tracing then trace "sol2" "eq %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "eq %a" S.Var.pp_trace x; eval_rhs_event x; match S.system x with | None -> S.Dom.bot () | Some f -> f get set and eval x y = - if tracing then trace "sol2" "eval %a ## %a" S.Var.pretty_trace x S.Var.pretty_trace y; + if tracing then trace "sol2" "eval %a ## %a" S.Var.pp_trace x S.Var.pp_trace y; get_var_event y; if HM.mem called y then HM.replace wpoint y (); solve y Widen; @@ -91,7 +91,7 @@ module WP = solve y Widen; ) and init x = - if tracing then trace "sol2" "init %a" S.Var.pretty_trace x; + if tracing then trace "sol2" "init %a" S.Var.pp_trace x; if not (HM.mem rho x) then ( new_var_event x; HM.replace rho x (S.Dom.bot ()) @@ -99,7 +99,7 @@ module WP = in let set_start (x,d) = - if tracing then trace "sol2" "set_start %a ## %a" S.Var.pretty_trace x S.Dom.pretty d; + if tracing then trace "sol2" "set_start %a ## %a" S.Var.pp_trace x S.Dom.pp d; init x; HM.replace rho' x d; solve x Widen diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 4dee3a62c8..86f807eb8a 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -408,7 +408,7 @@ class copyandPatchLabelsVisitor(loopEnd, currentIterationEnd, gotos) = object (* this makes new physical copy*) let new_s = {sn with labels = new_labels} in CopyOfHashTable.replace copyof new_s s; - if M.tracing then M.trace "cfg" "Marking %a as copy of %a" CilType.Stmt.pretty new_s CilType.Stmt.pretty s; + if M.tracing then M.trace "cfg" "Marking %a as copy of %a" CilType.Stmt.pp new_s CilType.Stmt.pp s; if new_s.labels <> [] then (* Use original s, ns might be temporay e.g. if the type of statement changed *) (* record that goto s; appearing in the current fragment should later be patched to goto new_s *) diff --git a/src/util/std/gobYojson.ml b/src/util/std/gobYojson.ml index 72d5f0b0e2..2def7dd61c 100644 --- a/src/util/std/gobYojson.ml +++ b/src/util/std/gobYojson.ml @@ -30,3 +30,5 @@ let print (ch: 'a BatIO.output) json = let pretty () json = GoblintCil.Pretty.text (Yojson.Safe.to_string json) + +let pp ppf json = Format.pp_print_string ppf (Yojson.Safe.to_string json) diff --git a/src/util/tracing/goblint_tracing.ml b/src/util/tracing/goblint_tracing.ml index f62ec3ee38..52c4ba6b75 100644 --- a/src/util/tracing/goblint_tracing.ml +++ b/src/util/tracing/goblint_tracing.ml @@ -7,7 +7,6 @@ open Goblint_std open Goblint_parallel open GoblintCil -open Pretty module Strs = Set.Make (String) @@ -35,16 +34,15 @@ let indent_level = ref 0 let traceIndent () = indent_level := !indent_level + 2 let traceOutdent () = indent_level := !indent_level - 2 -let traceTag (sys : string) : Pretty.doc = +let traceTag (sys : string) : string = let rec ind (i : int) : string = if (i <= 0) then "" else " " ^ (ind (i-1)) in - (text ((ind !indent_level) ^ "%%% " ^ sys ^ ": ")) + (ind !indent_level) ^ "%%% " ^ sys ^ ": " let trace_mutex = GobMutex.create () -let printtrace sys d: unit = +let printtrace sys (s: string): unit = GobMutex.lock trace_mutex; - fprint stderr ~width:max_int ((traceTag sys) ++ d ++ line); - flush stderr; + Printf.eprintf "%s%s\n%!" (traceTag sys) s; GobMutex.unlock trace_mutex let gtrace always f sys var ?loc do_subsys fmt = @@ -60,9 +58,14 @@ let gtrace always f sys var ?loc do_subsys fmt = in if cond then begin do_subsys (); - gprintf (f sys) fmt + let buf = Buffer.create 64 in + let ppf = Format.formatter_of_buffer buf in + Format.kfprintf (fun ppf -> + Format.pp_print_flush ppf (); + f sys (Buffer.contents buf) + ) ppf fmt end else - GobPretty.igprintf () fmt + Format.ifprintf Format.err_formatter fmt let trace sys ?var fmt = gtrace true printtrace sys var ignore fmt @@ -74,13 +77,13 @@ let trace sys ?var fmt = gtrace true printtrace sys var ignore fmt *) let tracei (sys:string) ?var ?(subsys=[]) fmt = - let f sys d = printtrace sys d; traceIndent () in + let f sys s = printtrace sys s; traceIndent () in let g () = activate sys subsys in gtrace true f sys var g fmt let tracec sys fmt = gtrace false printtrace sys None ignore fmt let traceu sys fmt = - let f sys d = printtrace sys d; traceOutdent () in + let f sys s = printtrace sys s; traceOutdent () in let g () = deactivate sys in gtrace true f sys None g fmt