Codegen, take 3#369
Draft
nikomatsakis wants to merge 8 commits into
Draft
Conversation
nikomatsakis
force-pushed
the
codegen-3
branch
5 times, most recently
from
471b132 to
7b10752
Compare
Contributor
|
do you mind splitting the codegen work from the toolchain fixes and merge those in first? |
Update minirust-rs crate to latest. Minor formality-core changes for tuple UpcastFrom and debug impl generation.
…re_crate Infrastructure needed for the codegen module: - Add Drop trait to core crate (FIXME: model the drop method) - Add Stmt::Print for println!() support in codegen tests - Add LtData::Erased for lifetime-erased codegen - Extract with_core_crate() helper from check_all_crates - Make borrow_check_expr public for use from codegen - Add Drop impl checking rules - Update test expectations for Drop trait change
Judgment-based codegen that compiles the high-level expression grammar into MiniRust basic blocks, then executes them via the MiniRust interpreter. Key design: - SemeRegion: single-entry, multi-exit CFG builder with anonymous blocks (names allocated lazily on terminate) and named blocks (preserved by append) - CodegenGlobal: cross-function state (fn_map for monomorphization worklist) - CodegenFn: per-function state (locals, bb counters, typeck env) - CodegenScope: variable→local mapping, label stack, flow state Judgments: codegen_function, codegen_block, codegen_stmt, codegen_expr_into, resolve_call, resolve_place, resolve_rigid, type_expr Supports: literals, variables, assignment, function calls (with monomorphization), if/else, loops with break/continue, references, derefs, structs, labeled blocks.
- Document SemeRegion lifecycle, append semantics, and compound helpers - Add walkthroughs for literal, call, if/else, and loop codegen - Render judgment signatures with one argument per line in mdbook
Collaborator
|
☔ The latest upstream changes (possibly #375) made this pull request unmergeable. Please resolve the merge conflicts. |
tiif
reviewed
Jun 3, 2026
Comment on lines
+302
to
+313
| ( | ||
| // Print statement: type-check the expression (result discarded) | ||
| (borrow_check_expr( | ||
| env, | ||
| assumptions, | ||
| state, | ||
| expr, | ||
| places_live_on_exit | ||
| ) => (_expr_ty, state)) | ||
| ------------------------------------------------------------ ("print") | ||
| (borrow_check_statement(env, assumptions, state, Stmt::Print { expr }, places_live_on_exit) => (env, state)) | ||
| ) |
Member
There was a problem hiding this comment.
what is the motivation to support print statement? (it's good to have of course, but i am just curious how is it related to codegen).
Member
There was a problem hiding this comment.
is drop impl something related to minirust codegen specifically?
Member
There was a problem hiding this comment.
heh are we cloning the the minirust codebase here? other than running the script, is there a better way to do this?(maybe josh would help?)
Comment on lines
+55
to
+59
| // Everything outlives 'erased | ||
| ( | ||
| ----------------------------- ("anything outlives erased") | ||
| (prove_outlives(_decls, _env, _assumptions, _a, LtData::Erased) => Constraints::none(env)) | ||
| ) |
Member
There was a problem hiding this comment.
mm why everything outlives 'erased?
FormalityTest.ok() now type-checks AND executes (codegen + MiniRust)
by default. Tests without a main function must call .skip_execute().
Tests can assert stdout with .expect_output("...").
- Move codegen tests from crates/formality-rust/src/codegen/test.rs
to tests/codegen.rs using the unified harness
- Fix reference tests to use exists<'a> instead of 'static
(required now that type-checking runs before codegen)
- Add minirust-rs and libspecr as root crate dependencies
- Add .skip_execute() to all existing integration tests (no main)
Rename throughout the codegen module and book chapter: - SemeRegion → CodeBlock - seme_region.rs → code_block.rs - fresh_region → fresh_code_block - region variables → code
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What does this PR do?
Next draft of codegen. Rebased.
How does it work, what questions do you have?
It includes a chapter in the mdbook that explains the key ideas. The most important one is a
SemeRegion(single-entry, multi-exit) that contains a fragment of a CFG. Thecodegen_xxxjudgments convert bits of formality's Expr IR intoSemeRegionoutput, these regions can then be combined. This is a nice setup in that you can convert expressions and things in a "standalone" fashion.We do still thread a global state through everything to let us make globally unique identifiers; I don't love that, might be nice to switch away from it.
AI disclosure