Pr/83 by cds-amal · Pull Request #111 · runtimeverification/stable-mir-json

cds-amal · 2025-11-30T19:34:59Z

Summary

This PR enhances the MIR graph visualization with richer allocation information and adds D2 as an alternative output format.

Key changes:

Index-first architecture: Build AllocIndex, TypeIndex, and GraphContext upfront before graph traversal, enabling context-aware rendering throughout
ALLOCS legend: New yellow info node showing all GlobalAlloc entries with decoded values (strings as ASCII, small integers as numeric values)
Enhanced constant labels: Constants now show provenance references like const [alloc0: Int(I32) = 42] instead of opaque const ?_i32
D2 output format (--d2 flag): Alternative to DOT with modern diagramming, viewable in browser at https://play.d2lang.com

Addresses

#83

Example

Before:

const ?_i32

After:

const [alloc0: Int(I32) = 42]

New CLI usage

cargo run -- --dot file.rs   # Graphviz DOT (existing)
cargo run -- --d2 file.rs    # D2 format (new)

New Make targets

make dot    # Generate all dot files
make svg    # Generate all svg files
make png    # Generate all png files
make d2      # Generate all D2 files

Test plan

Run --dot on test programs, verify ALLOCS legend appears
Run --d2 on test programs, verify output renders in D2 playground
Verify make integration-test passes

dkcumming · 2025-12-01T02:10:33Z

Hey @cds-amal looks great, I am excited to give this a go later on. Our CI is currently stuck on Code Quality, this can be fixed by running cargo clippy and cargo fmt and resolving the errors. I will be in touch on this soon, thank you!

dkcumming

Awesome stuff, I'm loving the whole thing. Some minor fix ups, and I would personally like to add the fast fail if dot is not installed with an informative message.

Do you think you could rebase and consider the suggestions?

Also what do you think about the ut8? I think we leave it for another issue right now so we get this in faster (sorry for my delay in getting this reviewed)

dkcumming · 2026-01-11T10:54:11Z

Makefile

+clean-graphs:
+	@rm -rf $(OUTDIR_DOT) $(OUTDIR_SVG) $(OUTDIR_PNG) $(OUTDIR_D2)
+


Suggested change

clean-graphs:

@rm -rf $(OUTDIR_DOT) $(OUTDIR_SVG) $(OUTDIR_PNG) $(OUTDIR_D2)

clean-graphs:

@rm -rf $(OUTDIR_DOT) $(OUTDIR_SVG) $(OUTDIR_PNG) $(OUTDIR_D2)

check-graphviz:

@command -v dot >/dev/null 2>&1 || { echo "Error: graphviz not installed. Install with: apt install graphviz"; exit 1; }

dkcumming · 2026-01-11T10:54:34Z

Makefile

 	fi
 	bash tests/ui/run_ui_tests.sh "$$RUST_DIR_ROOT" "${VERBOSE}"
+
+.PHONY: dot svg png d2 clean-graphs


Suggested change

.PHONY: dot svg png d2 clean-graphs

.PHONY: dot svg png d2 clean-graphs check-graphviz

dkcumming · 2026-01-11T10:55:10Z

Makefile

+		mv $$name.smir.dot $(OUTDIR_DOT)/ 2>/dev/null || true; \
+	done
+
+svg: dot


Suggested change

svg: dot

svg: check-graphviz dot

dkcumming · 2026-01-11T10:55:25Z

Makefile

+		dot -Tsvg $$dotfile -o $(OUTDIR_SVG)/$$name.svg; \
+	done
+
+png: dot


Suggested change

png: dot

png: check-graphviz dot

dkcumming · 2026-01-11T10:58:07Z

src/mk_graph/output/d2.rs

+    let legend_lines = ctx.allocs_legend_lines();
+    if legend_lines.is_empty() {
+        return;
+    }


Since ctx.allocs_legend_lines(); will always add "ALLOCS" to the output I believe this early return is never possible to be taken right?

dkcumming · 2026-01-11T11:02:07Z

src/mk_graph/index.rs

+                let desc = if is_str && concrete_bytes.iter().all(|b| b.is_ascii()) {
+                    let s: String = concrete_bytes
+                        .iter()
+                        .take(20)
+                        .map(|&b| b as char)
+                        .collect::<String>()
+                        .escape_default()
+                        .to_string();


I think this could be changed to work for utf8. Although the code would need to change from take(20) because you are not guaranteed that a char will fit 1 byte so 20 might be in the middle of a char. I don't know if this is needed for this PR though, I would be happy to make an issue for it to handle utf8

One does not casually reason about the wide and skinny bytes in a PR; when implementing this, I wanted to avoid the issue and should have called it out. Would appreciate if we could raise an issue, so a fix is more focused, that would be a good-first-contrib category.

src/mk_graph/index.rs

Restructure the graph generation to build indices upfront rather than resolving relationships at traversal time. This improves maintainability and enables richer constant/allocation information in the output. Add new data structures for graph context: - AllocIndex: maps AllocId to processed AllocEntry with descriptions - AllocEntry: contains alloc metadata and human-readable description - AllocKind: categorizes allocs as Memory/Static/VTable/Function - TypeIndex: maps type IDs to display names - GraphContext: holds all indices and provides rendering methods Add ALLOCS legend node to graphs: - Display all GlobalAlloc entries in a yellow info node - Show allocation ID, type, and decoded value where possible - Decode string literals as escaped ASCII - Decode small integers as numeric values Enhance constant operand labels: - Show provenance references: `const [alloc0: Int(I32) = 42]` - Display inline constant values with types: `const 42_Uint(Usize)` - Show function names for ZeroSized function constants Add context-aware rendering functions: - render_stmt_ctx: renders statements with alloc context - render_rvalue_ctx: renders rvalues with operand context - render_intrinsic_ctx: renders intrinsics with operand context Update to_dot_file to use new architecture: - Build GraphContext before consuming SmirJson - Pass context to statement/operand rendering - Use context for call edge argument labels Add accessor methods to AllocInfo in printer.rs: - alloc_id(): returns the allocation ID - ty(): returns the type - global_alloc(): returns reference to GlobalAlloc

Add alternative graph output format using D2 language alongside existing DOT format. D2 offers modern diagramming with better text rendering and can be viewed in browser via d2lang.com playground. Changes: - Add --d2 command-line flag for D2 output - Add to_d2_file() method to SmirJson for D2 rendering - Add emit_d2file() entry point - Add render_terminator_ctx() and terminator_targets() helpers - Add resolve_call_target() method to GraphContext - Add escape_d2() to handle $ and other special characters in labels Output includes: - ALLOCS legend with allocation descriptions - Function containers with basic blocks - Block-to-block control flow edges - Call edges to external functions

- Change &String to &str in short_name() and block_name() signatures - Extract bytes_to_u64_le() helper for repeated byte-to-int conversion - Fix expect() messages to properly interpolate path using unwrap_or_else

Extract D2 rendering into focused helper functions: - render_d2_allocs_legend - render_d2_function - render_d2_blocks - render_d2_block_edges - render_d2_call_edges - render_d2_asm - render_d2_static

Break up rather large mk_graph.rs into focused teeny tiny-er modules: - mk_graph/mod.rs: Entry points (emit_dotfile, emit_d2file) - mk_graph/index.rs: AllocIndex, TypeIndex, AllocEntry structures - mk_graph/context.rs: GraphContext with rendering methods - mk_graph/util.rs: GraphLabelString trait and helper functions - mk_graph/output/dot.rs: DOT (Graphviz) rendering - mk_graph/output/d2.rs: D2 diagram rendering This improves maintainability and makes it easier to add new output formats in the future.

- dot: Generate .dot files in output-dot/ - svg: Convert dot files to SVG (requires graphviz) - png: Convert dot files to PNG (requires graphviz) - d2: Generate .d2 files in output-d2/ Update README with usage instructions.

Leverage the LayoutShape and field type information recently added to TypeMetadata (commits 74a4261, 18f452d) to provide actual useful data instead of leaving it to gather dust in the JSON output. Introduce TypeEntry, LayoutInfo, and associated structures to index.rs, replacing the rather spartan string-only type index with something that knows about field offsets, sizes, alignments, and discriminants. One might argue this is what a type index ought to have done from the start. Add rendering methods to GraphContext for displaying types with their memory layouts. The DOT output now includes a TYPES legend (in a fetching shade of lavender) and locals are annotated with size and alignment. This allows tooling to answer questions like "how large is this struct" and "at what offset does field 3 live" without resorting to prayer or manual calculation.

Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>

@dkcumming

## Summary Follow up from a review comment on PR #111. Removes an unreachable early return in D2 legend rendering. ## Problem In `src/mk_graph/output/d2.rs`: ``` let legend_lines = ctx.allocs_legend_lines(); if legend_lines.is_empty() { return; } ``` As pointed out by @dkcumming, `allocs_legend_lines()` always inserts the `"ALLOCS"` header, so this condition can never be true. ## Change Remove the dead branch and rely on the invariant guaranteed by `allocs_legend_lines()`. ## Diff ```diff fn render_d2_allocs_legend(ctx: &GraphContext, out: &mut String) { let legend_lines = ctx.allocs_legend_lines(); - if legend_lines.is_empty() { - return; - } out.push_str("ALLOCS: {\n"); out.push_str(" style.fill: \"#ffffcc\"\n"); ``` ## Review context #111 (comment)

## Summary This is a small follow up to review comments from PR #111 where adding a fast-fail check for Graphviz (dot) was suggested but not included before merge. ## Changes - Add check-graphviz target - Wire it into svg and png - Add to .PHONY - Provide OS agnostic error message ## Before running: ``` make svg ``` produces many repeated shell errors after generating all .dot files: ``` Converting assert_eq.smir.dot -> assert_eq.smir.svg /bin/sh: line 4: dot: command not found ... make: *** [Makefile:94: svg] Error 127 ``` ## After ``` $ make svg Error: Graphviz is not installed or 'dot' is not in PATH. Please install Graphviz for your system and ensure 'dot' is available. See: https://graphviz.org/download/ ``` ## How to test 1. Temporarily uninstall Graphviz or remove dot from PATH 2. Run: make svg 3. Observe immediate fast-fail message 4. Reinstall Graphviz 5. Run again. Graphs generate normally ## Context Reviewer suggestion here: #111 (comment) #111 (comment) #111 (comment) #111 (comment) Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>

cds-amal marked this pull request as ready for review December 2, 2025 01:45

dkcumming reviewed Jan 11, 2026

View reviewed changes

cds-amal force-pushed the pr/83 branch from 9098513 to 1c8f03b Compare January 12, 2026 15:26

cds-amal and others added 9 commits January 12, 2026 23:55

refactor: improve code quality

1c167da

- Change &String to &str in short_name() and block_name() signatures - Extract bytes_to_u64_le() helper for repeated byte-to-int conversion - Fix expect() messages to properly interpolate path using unwrap_or_else

refactor: flatten nested logic in to_d2_file

daf4c82

Extract D2 rendering into focused helper functions: - render_d2_allocs_legend - render_d2_function - render_d2_blocks - render_d2_block_edges - render_d2_call_edges - render_d2_asm - render_d2_static

cargo clippy && cargo fmt

d6fd395

Add make targets for graph visualization

be7a54a

- dot: Generate .dot files in output-dot/ - svg: Convert dot files to SVG (requires graphviz) - png: Convert dot files to PNG (requires graphviz) - d2: Generate .d2 files in output-d2/ Update README with usage instructions.

Update src/mk_graph/index.rs

0ab9564

Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>

cds-amal force-pushed the pr/83 branch from 1c8f03b to 0ab9564 Compare January 13, 2026 04:55

dkcumming added the automerge label Jan 13, 2026

dkcumming approved these changes Jan 13, 2026

View reviewed changes

automergerpr-permission-manager bot merged commit e9395d9 into runtimeverification:master Jan 13, 2026
5 checks passed

This was referenced Feb 2, 2026

make: prevent svg/png generation when dot is unavailable #117

Merged

d2: remove unreachable early return in legend rendering #118

Merged

cds-amal deleted the pr/83 branch February 3, 2026 21:36

dkcumming mentioned this pull request Feb 4, 2026

Graph Improvements: Rendering Constant Values #107

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Pr/83#111

Pr/83#111
automergerpr-permission-manager[bot] merged 9 commits intoruntimeverification:masterfrom
cds-rs:pr/83

cds-amal commented Nov 30, 2025 •

edited

Loading

Uh oh!

dkcumming commented Dec 1, 2025

Uh oh!

dkcumming left a comment

Uh oh!

dkcumming Jan 11, 2026

Uh oh!

dkcumming Jan 11, 2026

Uh oh!

dkcumming Jan 11, 2026

Uh oh!

dkcumming Jan 11, 2026

Uh oh!

dkcumming Jan 11, 2026

Uh oh!

dkcumming Jan 11, 2026

Uh oh!

cds-amal Jan 11, 2026

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		clean-graphs:
		@rm -rf $(OUTDIR_DOT) $(OUTDIR_SVG) $(OUTDIR_PNG) $(OUTDIR_D2)

	.PHONY: dot svg png d2 clean-graphs
	.PHONY: dot svg png d2 clean-graphs check-graphviz

Conversation

cds-amal commented Nov 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Addresses

Example

New CLI usage

New Make targets

Test plan

Uh oh!

dkcumming commented Dec 1, 2025

Uh oh!

dkcumming left a comment

Choose a reason for hiding this comment

Uh oh!

dkcumming Jan 11, 2026

Choose a reason for hiding this comment

Uh oh!

dkcumming Jan 11, 2026

Choose a reason for hiding this comment

Uh oh!

dkcumming Jan 11, 2026

Choose a reason for hiding this comment

Uh oh!

dkcumming Jan 11, 2026

Choose a reason for hiding this comment

Uh oh!

dkcumming Jan 11, 2026

Choose a reason for hiding this comment

Uh oh!

dkcumming Jan 11, 2026

Choose a reason for hiding this comment

Uh oh!

cds-amal Jan 11, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

cds-amal commented Nov 30, 2025 •

edited

Loading