Skip to content

Migrate from CIL's Pretty to OCaml's Format (initial pass)#1994

Draft
Copilot wants to merge 3 commits intomasterfrom
copilot/migrate-pretty-to-format
Draft

Migrate from CIL's Pretty to OCaml's Format (initial pass)#1994
Copilot wants to merge 3 commits intomasterfrom
copilot/migrate-pretty-to-format

Conversation

Copy link
Copy Markdown
Contributor

Copilot AI commented Apr 12, 2026

Begins the migration from CIL's unmaintained Pretty module to OCaml's standard Format module, which is faster (no intermediate doc construction, GADT-based internals), maintained, and compatible with ppx_deriving.show.

Core interface change

Added val pp: Format.formatter -> t -> unit to Printable.S — the de facto standard signature, also derived by ppx_deriving.show:

(* Before *)
val pretty: unit -> t -> Pretty.doc

(* After — both coexist during migration *)
val pretty: unit -> t -> Pretty.doc
val pp: Format.formatter -> t -> unit

Changes

  • Printable.S — adds val pp: Format.formatter -> t -> unit
  • printable.ml functors — all functors (SimplePretty, SimpleShow, SimpleFormat, UnitConf, HConsed, HashCached, LiftConf, Lift2Conf, ProdConf, Prod3, Liszt, Chain, LiftBot, LiftTop, Option) now derive/provide pp, so modules using them get it for free
  • Domain modules — added pp to setDomain, mapDomain, hoareDomain, baseDomain, musteqDomain, threadIdDomain, intDomTuple, valueDomain, arrayDomain, structDomain, all apron domains, and utility modules (gobFpath, gobYojson, edge)
  • VarType signature — added pp_trace: Format.formatter -> t -> unit with implementations in constrSys.ml, analyses.ml, node.ml
  • Tracing system (goblint_tracing.ml, messages.ml) — rewrites gtrace/tracel/traceli to use Format.kfprintf/Format.ifprintf instead of Pretty.gprintf/GobPretty.igprintf; trace output is now written via a Buffer+formatter, then flushed as a string with Printf.eprintf
  • 400+ trace call sites — bulk-updated to use D.pp instead of D.pretty, pp_trace instead of pretty_trace, and CilType.Exp.pp/CilType.Typ.pp/CilType.Lval.pp in place of CIL's d_exp/d_type/d_lval

Known remaining issues

A handful of call sites in td3.ml still use Pretty.docOpt (S.Var.pp_trace ()) and S.Dom.pretty_diff inside trace calls — these need Format-compatible replacements (GobFormat.pp_print_opt and a Format-based diff printer).

Messages.warn/info/debug/error still use Pretty-based format strings and are out of scope for this initial pass.

@sim642
Copy link
Copy Markdown
Member

sim642 commented Apr 12, 2026

There's little use to this without doing this in CIL first. There are old branches in both that go 95% of the way (at the time). The reason they didn't get done is that there are tricky things that Pretty can do which are slightly different from Format.

Copilot AI and others added 2 commits April 12, 2026 08:00
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>
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>
Copilot AI changed the title [WIP] Migrate from CIL's Pretty to OCaml's Format Migrate from CIL's Pretty to OCaml's Format (initial pass) Apr 12, 2026
Copilot AI requested a review from michael-schwarz April 12, 2026 08:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Migrate from CIL's Pretty to OCaml's Format

3 participants