Replace eager `show` with lazy `pretty` during analysis by sim642 · Pull Request #1797 · goblint/analyzer

sim642 · 2025-07-30T19:00:36Z

Closes #1795.

This probably isn't all of it, but hopefully is most that I quickly found with some simple searches.

Copilot

Pull request overview

This pull request replaces eager show functions with lazy pretty functions throughout the codebase to improve performance during analysis. The change converts string-based formatting to Pretty document-based formatting, which allows for lazy evaluation and avoids unnecessary computation when tracing is disabled.

Key Changes

Converts show functions to pretty functions that return Pretty.doc instead of string
Updates all trace/tracel calls to use format specifier %a with pretty-printers instead of %s with string conversion
Replaces Printable.SimpleShow with Printable.SimplePretty in domain definitions

Reviewed changes

Copilot reviewed 14 out of 14 changed files in this pull request and generated 10 comments.

Show a summary per file

File	Description
src/cdomains/unionFind.ml	Converts `show` functions to `pretty` functions for terms, propositions, union-find structures, and lookup maps
src/cdomains/duplicateVars.ml	Adds `pretty` function for VarType module
src/cdomains/congruenceClosure.ml	Converts all `show` functions to `pretty` for disequalities, sets, maps, conjunctions, and traces; contains bugs in function signatures
src/cdomains/c2poDomain.ml	Updates C2PODomain to use `pretty` instead of `show`, changes from SimpleShow to SimplePretty, updates XML printing
src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml	Converts RHS and EqualitiesConjunction pretty-printing; contains function signature bugs and leftover `show` call
src/cdomains/apron/affineEqualityDomain.apron.ml	Updates trace calls to use `pretty` instead of `show`
src/cdomains/apron/affineEqualityDenseDomain.apron.ml	Updates trace calls to use `pretty` instead of `show`
src/cdomains/affineEquality/vector.ml	Changes interface from `show` to `pretty`
src/cdomains/affineEquality/sparseImplementation/sparseVector.ml	Implements `pretty` function for sparse vectors
src/cdomains/affineEquality/sparseImplementation/listMatrix.ml	Implements `pretty` function for list matrices; contains eager computation in traces with TODO comments
src/cdomains/affineEquality/matrix.ml	Changes interface from `show` to `pretty`
src/cdomains/affineEquality/arrayImplementation/arrayVector.ml	Implements `pretty` function for array vectors
src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml	Implements `pretty` function for array matrices; contains eager `of_array` conversion
src/analyses/c2poAnalysis.ml	Updates all trace calls to use `pretty` functions instead of `show`

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2025-12-09T05:46:42Z

src/cdomains/congruenceClosure.ml

-    if M.tracing then M.trace "c2po-query" "may-point-to %a -> equal terms: %s"
-        d_exp exp (List.fold_left (fun s (t,z) -> s ^ "(" ^ T.show t ^","^ Z.to_string Z.(z + offset) ^")") "" equal_terms);
+    if M.tracing then M.trace "c2po-query" "may-point-to %a -> equal terms: %a"
+        d_exp exp (Pretty.docList ~sep:Pretty.nil (fun (t,z) -> Pretty.dprintf "(%a,%a)" T.pretty t GobZ.pretty Z.(z + offset))) equal_terms;


The function signature is missing the unit parameter. The anonymous function should be (fun () (t,z) -> ...) to match the Pretty.docList pattern where the first parameter is unit for lazy evaluation.

Suggested change

d_exp exp (Pretty.docList ~sep:Pretty.nil (fun (t,z) -> Pretty.dprintf "(%a,%a)" T.pretty t GobZ.pretty Z.(z + offset))) equal_terms;

d_exp exp (Pretty.docList ~sep:Pretty.nil (fun () (t,z) -> Pretty.dprintf "(%a,%a)" T.pretty t GobZ.pretty Z.(z + offset))) equal_terms;

Copilot · 2025-12-09T05:46:42Z

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

+      Pretty.dprintf "{%a}" (Pretty.d_list " ∧ " (fun () (i, (refmonom,off,divi)) -> Pretty.dprintf "%a%a=%a" Rhs.pretty_coeff divi formatter i (Rhs.pretty_rhs_formatted formatter) (refmonom,off,divi))) (IntMap.bindings econ)

-  let show econ = show_formatted (Printf.sprintf "var_%d") econ
+  let pretty = pretty_formatted (fun () -> Pretty.dprintf "var_%d")


Inconsistent function signature usage. On line 62, formatter i is called without unit parameter, but on line 64, formatter is defined as (fun () -> Pretty.dprintf "var_%d") which expects to be called with unit. Either change line 62 to formatter () i or change line 64 to (fun i -> Pretty.dprintf "var_%d" i).

Suggested change

let pretty = pretty_formatted (fun () -> Pretty.dprintf "var_%d")

let pretty = pretty_formatted (fun i -> Pretty.dprintf "var_%d" i)

Copilot · 2025-12-09T05:46:43Z

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

+    | (Some (coeff,v), o,_) when Z.equal o Z.zero -> Pretty.dprintf "%a%a" pretty_coeff coeff formatter v
+    | (Some (coeff,v), o,_) -> Pretty.dprintf "%a%a %a" pretty_coeff coeff formatter v zpretty o


The function signature for pretty_rhs_formatted is incorrect. The formatter parameter should be formatter () to match how it's being called on line 36 with (fun () -> Pretty.dprintf "var_%d"). The function is expecting a unit parameter but receiving a function that takes unit.

Suggested change

| (Some (coeff,v), o,_) when Z.equal o Z.zero -> Pretty.dprintf "%a%a" pretty_coeff coeff formatter v

| (Some (coeff,v), o,_) -> Pretty.dprintf "%a%a %a" pretty_coeff coeff formatter v zpretty o

| (Some (coeff,v), o,_) when Z.equal o Z.zero -> Pretty.dprintf "%a%a" pretty_coeff coeff (formatter () v)

| (Some (coeff,v), o,_) -> Pretty.dprintf "%a%a %a" pretty_coeff coeff (formatter () v) zpretty o

Copilot · 2025-12-09T05:46:43Z

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

+      let pretty = pretty
+    end
+    )
  let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (show x)) Environment.printXml x.env


The printXml function still uses the deprecated show function which should have been replaced. This will cause a compilation error since show is no longer defined. Use GobPretty.sprint pretty x instead of show x.

Suggested change

let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (show x)) Environment.printXml x.env

let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (GobPretty.sprint pretty x)) Environment.printXml x.env

Copilot · 2025-12-09T05:46:43Z

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

          in
          let resl,rest = sub_and_last_aux ([],None) c1 c2 in
-          if M.tracing then M.trace "linear_disjunct_cases" "sub_and_last: ridx: %d c1: %s, c2: %s, resultlist: %s, result_pivot: %s" ridx (V.show col1) (V.show col2) (String.concat "," (List.map (fun (i,v) -> Printf.sprintf "(%d,%s)" i (A.to_string v)) resl)) (match rest with None -> "None" | Some (i,v1,v2) -> Printf.sprintf "(%d,%s,%s)" i (A.to_string v1) (A.to_string v2));
+          if M.tracing then M.trace "linear_disjunct_cases" "sub_and_last: ridx: %d c1: %a, c2: %a, resultlist: %s, result_pivot: %s" ridx V.pretty col1 V.pretty col2 (String.concat "," (List.map (fun (i,v) -> Printf.sprintf "(%d,%s)" i (A.to_string v)) resl)) (match rest with None -> "None" | Some (i,v1,v2) -> Printf.sprintf "(%d,%s,%s)" i (A.to_string v1) (A.to_string v2)); (* TODO: avoid eager arguments *)


This trace call has eager computation in its arguments. The String.concat with List.map, Printf.sprintf, and A.to_string operations will be executed even when tracing is disabled. As noted in the TODO comment, these eager arguments should be avoided to improve performance when tracing is disabled.

Suggested change

if M.tracing then M.trace "linear_disjunct_cases" "sub_and_last: ridx: %d c1: %a, c2: %a, resultlist: %s, result_pivot: %s" ridx V.pretty col1 V.pretty col2 (String.concat "," (List.map (fun (i,v) -> Printf.sprintf "(%d,%s)" i (A.to_string v)) resl)) (match rest with None -> "None" | Some (i,v1,v2) -> Printf.sprintf "(%d,%s,%s)" i (A.to_string v1) (A.to_string v2)); (* TODO: avoid eager arguments *)

if M.tracing then (

let resultlist_str = String.concat "," (List.map (fun (i,v) -> Printf.sprintf "(%d,%s)" i (A.to_string v)) resl) in

let result_pivot_str = match rest with

| None -> "None"

| Some (i,v1,v2) -> Printf.sprintf "(%d,%s,%s)" i (A.to_string v1) (A.to_string v2)

in

M.trace "linear_disjunct_cases" "sub_and_last: ridx: %d c1: %a, c2: %a, resultlist: %s, result_pivot: %s"

ridx V.pretty col1 V.pretty col2 resultlist_str result_pivot_str

); (* TODO: avoid eager arguments *)

Copilot · 2025-12-09T05:46:44Z

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

+          if M.tracing then M.trace "linear_disjunct_cases" "case_three: found difference at ridx: %d idx: %d, x: %s, y: %s, diff: %s, m1: \n%a, m2:\n%a, res:\n%a"
+              ridx idx (A.to_string x) (A.to_string y) (A.to_string diff) pretty m1 pretty m2 pretty (rev_matrix res); (* TODO: avoid eager A.to_string, rev_matrix *)


This trace call has eager computation in its arguments. The A.to_string calls and rev_matrix res computation will be executed even when tracing is disabled. As noted in the TODO comment, these eager arguments should be avoided to improve performance when tracing is disabled.

Copilot · 2025-12-09T05:46:44Z

src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml

+    if M.tracing then M.tracel "from_texp" "%a %a -> %s" EConj.pretty (snd @@ BatOption.get t.d) Texpr1.Expr.pretty texp
        (BatOption.map_default (fun (l,(o,d)) -> List.fold_right (fun (a,x,b) acc -> Printf.sprintf "%s*var_%d/%s + %s" (Z.to_string a) x (Z.to_string b) acc) l ((Z.to_string o)^"/"^(Z.to_string d))) "" res);


This trace call has eager computation of its arguments. The complex string formatting operations (BatOption.map_default with Printf.sprintf and Z.to_string calls) will be executed even when tracing is disabled. This defeats the purpose of replacing show with lazy pretty. Consider restructuring to avoid eager computation.

Suggested change

if M.tracing then M.tracel "from_texp" "%a %a -> %s" EConj.pretty (snd @@ BatOption.get t.d) Texpr1.Expr.pretty texp

(BatOption.map_default (fun (l,(o,d)) -> List.fold_right (fun (a,x,b) acc -> Printf.sprintf "%s*var_%d/%s + %s" (Z.to_string a) x (Z.to_string b) acc) l ((Z.to_string o)^"/"^(Z.to_string d))) "" res);

if M.tracing then (

let formatted =

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

in

M.tracel "from_texp" "%a %a -> %s"

EConj.pretty (snd @@ BatOption.get t.d)

Texpr1.Expr.pretty texp

formatted

);

Copilot · 2025-12-09T05:46:44Z

src/cdomains/affineEquality/sparseImplementation/listMatrix.ml

+        if M.tracing then M.trace "linear_disjunct" "result so far: \n%a, currentrowindex: %d, currentcolindex: %d, m1: \n%a, m2:\n%a"
+            pretty (rev_matrix result) currentrowindex currentcolindex pretty m1 pretty m2; (* TODO: avoid eager rev_matrix *)


This trace call has eager computation in its arguments. The rev_matrix result computation will be executed even when tracing is disabled. As noted in the TODO comment, this eager argument should be avoided to improve performance when tracing is disabled.

Suggested change

if M.tracing then M.trace "linear_disjunct" "result so far: \n%a, currentrowindex: %d, currentcolindex: %d, m1: \n%a, m2:\n%a"

pretty (rev_matrix result) currentrowindex currentcolindex pretty m1 pretty m2; (* TODO: avoid eager rev_matrix *)

if M.tracing then (

let rev_res = rev_matrix result in

M.trace "linear_disjunct" "result so far: \n%a, currentrowindex: %d, currentcolindex: %d, m1: \n%a, m2:\n%a"

pretty rev_res currentrowindex currentcolindex pretty m1 pretty m2

);

Copilot · 2025-12-09T05:46:44Z

src/cdomains/affineEquality/arrayImplementation/arrayMatrix.ml

+    let pretty =
+      GoblintCil.Pretty.(docArray ~sep:nil (fun _ x -> V.pretty () (V.of_array x))) (* TODO: avoid of_array *)


The V.of_array call is eagerly executed for each element even when the pretty-printing may not be needed. As noted in the TODO comment, this conversion should be avoided. Consider restructuring to delay the conversion or use a more efficient approach.

Copilot · 2025-12-09T05:46:45Z

src/cdomains/congruenceClosure.ml

    closure cc pos_conjs
  in
-  if M.tracing then M.trace "c2po-meet" "meet_pos_conjs result: %s\n" (show_conj (get_conjunction_from_data res));
+  if M.tracing then M.trace "c2po-meet" "meet_pos_conjs result: %a\n" pretty_conj (get_conjunction_from_data res); (* TODO: avoid eager computation in argument *)


This trace call still has eager computation in its arguments. The get_conjunction_from_data res is computed eagerly even when tracing is disabled. Consider wrapping this in a function to make it lazy: (fun () -> pretty_conj (get_conjunction_from_data res)).

Suggested change

if M.tracing then M.trace "c2po-meet" "meet_pos_conjs result: %a\n" pretty_conj (get_conjunction_from_data res); (* TODO: avoid eager computation in argument *)

if M.tracing then M.trace "c2po-meet" "meet_pos_conjs result: %a\n" (fun () -> pretty_conj (get_conjunction_from_data res)); (* TODO: avoid eager computation in argument *)

sim642 added 2 commits July 30, 2025 21:31

Use pretty instead of show in relational domains (issue #1795)

46f80fc

Use pretty instead of show in vector and matrix (issue #1795)

1e89a9b

sim642 added this to the v2.7.0 Bamboozled Buffalo milestone Jul 30, 2025

sim642 added cleanup Refactoring, clean-up bug performance Analysis time, memory usage relational Relational analyses (Apron, affeq, lin2var) labels Jul 30, 2025

DrMichaelPetter self-requested a review August 6, 2025 19:44

sim642 added 3 commits September 4, 2025 12:05

Use pretty instead of show in C-2PO domains (issue #1795)

31b2e1c

Use pretty instead of show in C-2PO analysis (issue #1795)

c2a588f

Use pretty instead of show in lin2vareq domain (issue #1795)

fd4bd85

sim642 marked this pull request as ready for review September 4, 2025 09:35

sim642 modified the milestones: v2.7.0 Bamboozled Buffalo, v2.8.0 Nov 25, 2025

michael-schwarz requested a review from Copilot December 9, 2025 05:40

Copilot started reviewing on behalf of michael-schwarz December 9, 2025 05:41 View session

Copilot AI reviewed Dec 9, 2025

View reviewed changes

sim642 mentioned this pull request Feb 6, 2026

Non-deterministic non-termination of ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--device_handler--scsi_dh_rdac.ko-entry_point.cil.out.i #1942

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Replace eager `show` with lazy `pretty` during analysis#1797

Replace eager `show` with lazy `pretty` during analysis#1797
sim642 wants to merge 5 commits intomasterfrom
no-show

sim642 commented Jul 30, 2025 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Dec 9, 2025

Uh oh!

Copilot AI Dec 9, 2025

Uh oh!

Copilot AI Dec 9, 2025

Uh oh!

Copilot AI Dec 9, 2025

Uh oh!

Copilot AI Dec 9, 2025

Uh oh!

Copilot AI Dec 9, 2025

Uh oh!

Copilot AI Dec 9, 2025

Uh oh!

Copilot AI Dec 9, 2025

Uh oh!

Copilot AI Dec 9, 2025

Uh oh!

Copilot AI Dec 9, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

	d_exp exp (Pretty.docList ~sep:Pretty.nil (fun (t,z) -> Pretty.dprintf "(%a,%a)" T.pretty t GobZ.pretty Z.(z + offset))) equal_terms;
	d_exp exp (Pretty.docList ~sep:Pretty.nil (fun () (t,z) -> Pretty.dprintf "(%a,%a)" T.pretty t GobZ.pretty Z.(z + offset))) equal_terms;

	let pretty = pretty_formatted (fun () -> Pretty.dprintf "var_%d")
	let pretty = pretty_formatted (fun i -> Pretty.dprintf "var_%d" i)

		\| (Some (coeff,v), o,_) when Z.equal o Z.zero -> Pretty.dprintf "%a%a" pretty_coeff coeff formatter v
		\| (Some (coeff,v), o,_) -> Pretty.dprintf "%a%a %a" pretty_coeff coeff formatter v zpretty o

	let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (show x)) Environment.printXml x.env
	let printXml f x = BatPrintf.fprintf f "<value>\n<map>\n<key>\nequalities\n</key>\n<value>\n%s</value>\n<key>\nenv\n</key>\n<value>\n%a</value>\n</map>\n</value>\n" (XmlUtil.escape (GobPretty.sprint pretty x)) Environment.printXml x.env

-          if M.tracing then M.trace "linear_disjunct_cases" "sub_and_last: ridx: %d c1: %a, c2: %a, resultlist: %s, result_pivot: %s" ridx V.pretty col1 V.pretty col2 (String.concat "," (List.map (fun (i,v) -> Printf.sprintf "(%d,%s)" i (A.to_string v)) resl)) (match rest with None -> "None" | Some (i,v1,v2) -> Printf.sprintf "(%d,%s,%s)" i (A.to_string v1) (A.to_string v2)); (* TODO: avoid eager arguments *)
+          if M.tracing then (
+            let resultlist_str = String.concat "," (List.map (fun (i,v) -> Printf.sprintf "(%d,%s)" i (A.to_string v)) resl) in
+            let result_pivot_str = match rest with
+              | None -> "None"
+              | Some (i,v1,v2) -> Printf.sprintf "(%d,%s,%s)" i (A.to_string v1) (A.to_string v2)
+            in
+            M.trace "linear_disjunct_cases" "sub_and_last: ridx: %d c1: %a, c2: %a, resultlist: %s, result_pivot: %s"
+              ridx V.pretty col1 V.pretty col2 resultlist_str result_pivot_str
+          ); (* TODO: avoid eager arguments *)

		if M.tracing then M.trace "linear_disjunct_cases" "case_three: found difference at ridx: %d idx: %d, x: %s, y: %s, diff: %s, m1: \n%a, m2:\n%a, res:\n%a"
		ridx idx (A.to_string x) (A.to_string y) (A.to_string diff) pretty m1 pretty m2 pretty (rev_matrix res); (* TODO: avoid eager A.to_string, rev_matrix *)

		if M.tracing then M.tracel "from_texp" "%a %a -> %s" EConj.pretty (snd @@ BatOption.get t.d) Texpr1.Expr.pretty texp
		(BatOption.map_default (fun (l,(o,d)) -> List.fold_right (fun (a,x,b) acc -> Printf.sprintf "%s*var_%d/%s + %s" (Z.to_string a) x (Z.to_string b) acc) l ((Z.to_string o)^"/"^(Z.to_string d))) "" res);

		if M.tracing then M.trace "linear_disjunct" "result so far: \n%a, currentrowindex: %d, currentcolindex: %d, m1: \n%a, m2:\n%a"
		pretty (rev_matrix result) currentrowindex currentcolindex pretty m1 pretty m2; (* TODO: avoid eager rev_matrix *)

		let pretty =
		GoblintCil.Pretty.(docArray ~sep:nil (fun _ x -> V.pretty () (V.of_array x))) (* TODO: avoid of_array *)

	if M.tracing then M.trace "c2po-meet" "meet_pos_conjs result: %a\n" pretty_conj (get_conjunction_from_data res); (* TODO: avoid eager computation in argument *)
	if M.tracing then M.trace "c2po-meet" "meet_pos_conjs result: %a\n" (fun () -> pretty_conj (get_conjunction_from_data res)); (* TODO: avoid eager computation in argument *)

Conversation

sim642 commented Jul 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Key Changes

Reviewed changes

Uh oh!

Copilot AI Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 9, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

sim642 commented Jul 30, 2025 •

edited

Loading