Charon MIR front-end follow-up: #121 parity fixes, 0.1.201 cast/tuple/dispatch regressions, and syn-metadata retirement - #144
Conversation
|
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Run ID: ⛔ Files ignored due to path filters (1)
📒 Files selected for processing (3)
💤 Files with no reviewable changes (1)
WalkthroughExpands LLBC handling to include pyre-jit, introduces front/typestr and migrates callsites, and refactors MIR lowering to thread HostStaticAddrs, compute liveness, thread edge arguments, derive struct metadata, and improve cast/place lowering; CI, scripts, tests, docs, and minor runtime fixes updated accordingly. ChangesLLBC Artifact Infrastructure Expansion
String Parsing Utilities Refactoring
MIR Frontend Liveness and Metadata Enhancement
Hint Harvesting and Function Path Matching
Pipeline Integration and Documentation
Estimated code review effort🎯 4 (Complex) | ⏱️ ~75 minutes Possibly related PRs
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
|
dc21015 to
dab4280
Compare
633aa2f to
cb9cafe
Compare
Continue the comment cleanup over the remaining seven files. Replace internal-roadmap and past-state comment references with present-tense descriptions, and repoint diagnostic messages in flowspace_adapter.rs that still named the deleted `front/ast.rs` path to `front::mir`. Remove the `stacker` dependency from majit-translate: its only consumer was `front::ast::lower_expr`, which was deleted with the AST front-end; no source file in the crate references `stacker::maybe_grow`. Assisted-by: Claude
…ee utils Delete six syn_metadata helpers that have no remaining callers (the import-aware type-string machinery that served the removed AST `Expr::Path` resolver): full_type_string, qualified_full_type_string_with_imports, collect_trait_names, extract_dyn_trait_root (+ _with_context), qualify_known_trait_name, trait_object_root_name_qualified. Move the syn-free type-id string classifiers (transparent_result_ok_type, first_top_level_generic_arg, nolength_from_array_type_id) into a new front::typestr module, and move the unit-variant ctor allowlist (is_synthetic_unit_variant_path) into translator::rtyper::unit_variant_fold next to its fold. Narrow trait_object_root_name to pub(crate); its only caller is type_root_ident. front::syn_metadata now holds only the four syn-tree harvesters the MIR path still sources from interpreter source: collect_struct_origins, classify_fn_arg_ty, type_root_ident, trait_object_root_name. Assisted-by: Claude
derive_program_metadata keyed the FORCE_ATTRIBUTES_INTO_CLASSES shadow
rows by the crate-stripped module path (segs[1..].join("::")), but the
syn pre-pass (pre_register_struct_fields_from_file, invoked with an empty
module prefix) and the _init_classdef read both key by the bare leaf, so
the module-path key never matched. Key by the bare leaf instead.
Assisted-by: Claude
Charon 0.1.201 emits `as` casts as Rvalue::UnaryOp({"Cast"}). The arm
mapped int<->ptr / int<->float crossings to OpKind::UnaryOp cast opnames
(cast_int_to_ptr etc.), which normalize_unary_op_name rejects: the rtyper
retired every typed cast name from the unary-op path. Lower a
bank-crossing cast to simple_call(<host_callable>, v) instead -
lltype.cast_int_to_ptr / lltype.cast_ptr_to_int for int<->ptr, the float
/ int builtins for int<->float - whose rtyper hooks emit the low-level
cast op. The bank decision reads the operand place type and destination
type, so it is independent of the CastKind tag; same-bank casts still
alias the operand. build_rvalue gains the destination type so the cast
arm can read the destination bank.
Assisted-by: Claude
A `tuple.N` projection whose base is an opaque Ref tuple - function-return tuples and enum-variant payloads read through an Option/Result downcast, which the lowering does not build inline - was aliased to the whole tuple Variable, so a later merge with an Int-typed sibling tripped the assembler's per-bank kind cross-check. Emit a typed FieldRead __pos_<N> carrying the element type when the base place is a non-unit tuple. The *Checked (value, bool) shape is excluded: it lowers to a scalar BinOp, so binop_result_locals tracks those locals and their .0 collapses to that scalar instead of extracting a tuple element. Assisted-by: Claude
…ing link extract_opcode_dispatch_arms_from_mir passed only the startblock parameter map to build_arm_body_graph, so an arm whose handler forwards an arm-local inputarg - an executor reborrow threaded as a block parameter rather than referencing the startblock Input directly - referenced an unknown Variable and was rejected. arm_input_names extends the parameter map with each switch-target block's own inputargs, resolved through the dispatch link that renames them (Link renames args[i] into the target block's inputargs[i]), restoring the parameter name the wrapper builder forwards. Assisted-by: Claude
can_thread_variable_to_block, its inner recursion can_thread_variable_to_block_inner, and its sole caller thread_loop_link_args have zero callers across the workspace. #97 named can_thread_variable_to_block for removal once explicit MIR CFG processing made it obsolete; being pub kept the dead_code lint quiet. Remove all three. ensure_variable_at_block and variable_defined_in_block retain other callers and stay. Assisted-by: Claude
…t_field_attrs The pyre-jit-trace build-script analyze (build.rs:184) sources the eval_loop_jit portal from build/llbc/pyre-jit.ullbc. That file is absent on a clean tree, and during pyre-jit's own extraction it is the artefact being produced, so requiring it created a bootstrap cycle where extracting pyre-jit.ullbc needs pyre-jit.ullbc. - majit-translate/src/lib.rs: auto_discover_workspace_llbc_paths treats only pyre-object.ullbc and pyre-interpreter.ullbc as mandatory and appends pyre-jit.ullbc when present. When pyre-jit.ullbc is absent the discovery degrades to the 2-crate front-end (execute_opcode_step portal) instead of returning None, which had panicked the build script with "no LLBC source resolved". - .github/workflows/pyre-ci.yml: add pyre-jit to the extract-llbc.sh invocations in the cargo-test and pyre-check jobs (lines 67/102) so the analyze reads pyre-jit.ullbc on a populated tree. - majit-translate/src/front/mir.rs: key derived struct_field_attrs by the crate-stripped def-path. Assisted-by: Claude
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 9c4ac668a0
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if let ProjectionElem::Tagged(v) = &elem | ||
| && self.place_is_tuple(&inner) | ||
| && !self.place_is_binop_scalar(&inner) | ||
| && let Some(field_payload) = v.as_object().and_then(|m| m.get("Field")) | ||
| && let Some(idx) = self.positional_field_index(field_payload) |
There was a problem hiding this comment.
Do not collapse every checked-op field
When a MIR *Checked/overflowing binary op is followed by a projection of its overflow flag (field .1), this guard treats the whole tuple-typed local as a scalar and suppresses the new tuple FieldRead; the fallback below then aliases .1 to the numeric result variable. That makes code that actually uses the overflow boolean (rather than only an eliminated assert on it) branch on the arithmetic value instead of the flag, so this exception needs to apply only to the value field (.0) or otherwise model the overflow field separately.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Actionable comments posted: 1
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@majit/majit-translate/src/jit_codewriter/assembler.rs`:
- Around line 3231-3233: Update the explanatory comment that currently ties the
`bitand`/`bitor`/`bitxor` spelling to `syn::BinOp`; instead describe these as
Rust operator-trait spellings (e.g., "Rust operator-trait spellings
(`bitand`/`bitor`/`bitxor`)") that are recognized and rewritten at the
JIT/blackhole emission boundary (see `jtransform.rs` / `assembler.rs`), and keep
the reference to the `OpKind::BinOp.op` renaming behavior; simply reword the
comment to remove any implication that `syn::BinOp` types/variants are involved
in the op-name generation path.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro
Run ID: 55ddc5d6-0682-47fc-aea6-ada44a897b69
📒 Files selected for processing (34)
.github/workflows/pyre-ci.ymlmajit/charon-corpus/README.mdmajit/charon-corpus/src/lib.rsmajit/majit-backend-dynasm/src/aarch64/assembler.rsmajit/majit-charon-reader/tests/corpus.rsmajit/majit-translate/Cargo.tomlmajit/majit-translate/src/annotator/classdesc.rsmajit/majit-translate/src/flowspace/model.rsmajit/majit-translate/src/front/llbc_hints.rsmajit/majit-translate/src/front/mir.rsmajit/majit-translate/src/front/mir_dispatch.rsmajit/majit-translate/src/front/mod.rsmajit/majit-translate/src/front/semantic.rsmajit/majit-translate/src/front/syn_metadata.rsmajit/majit-translate/src/front/typestr.rsmajit/majit-translate/src/jit_codewriter/assembler.rsmajit/majit-translate/src/jit_codewriter/call.rsmajit/majit-translate/src/jit_codewriter/jtransform.rsmajit/majit-translate/src/lib.rsmajit/majit-translate/src/model.rsmajit/majit-translate/src/translator/rtyper/cutover.rsmajit/majit-translate/src/translator/rtyper/flowspace_adapter.rsmajit/majit-translate/src/translator/rtyper/lltypesystem/lltype.rsmajit/majit-translate/src/translator/rtyper/unit_variant_fold.rsmajit/majit-translate/tests/test_make_jitcodes_produces_graph_keyed_output.rsmajit/majit-translate/tests/test_mir_frontend.rspyre/check.pypyre/pyre-interpreter/src/pyframe.rspyre/pyre-interpreter/src/pyopcode.rspyre/pyre-jit-trace/build.rsscripts/extract-llbc.shscripts/install-charon.shtools/ubuntu24-amd64-repro/Dockerfiletools/ubuntu24-amd64-repro/README.md
💤 Files with no reviewable changes (2)
- majit/majit-translate/Cargo.toml
- majit/majit-translate/src/model.rs
| // `int_and` / `int_or` / `int_xor`. When an `OpKind::BinOp.op` | ||
| // arrives spelled with Rust's `syn::BinOp` trait names | ||
| // (`bitand`/`bitor`/`bitxor`) for source faithfulness, rename them |
There was a problem hiding this comment.
🧩 Analysis chain
🏁 Script executed:
#!/bin/bash
# Verify MIR frontend operator naming and syn involvement
rg -nP --type=rust -C3 '\b(bitand|bitor|bitxor)\b' majit/majit-translate/src/front/mir.rs majit/majit-translate/src/front/
# Check if syn is still referenced in MIR/frontend modules after retirement
rg -nP --type=rust -C2 '\bsyn::' majit/majit-translate/src/front/mir*.rs majit/majit-translate/src/front/semantic.rsRepository: youknowone/pyre
Length of output: 41
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# 1) Inspect the exact comment and surrounding code
sed -n '3210,3260p' majit/majit-translate/src/jit_codewriter/assembler.rs | nl -ba | sed -n '1,120p'
# 2) Find all occurrences of bitand/bitor/bitxor in translate (front + codewriter) to locate source of naming
rg -n --type=rust '\b(bitand|bitor|bitxor)\b' majit/majit-translate/src | head -n 50
# 3) Check for syn:: usage in the front directory (beyond just mir*.rs)
rg -n --type=rust '\bsyn::' majit/majit-translate/src/front | head -n 50
# 4) Also check whether any module references syn metadata retirement (`#121`) via comments/identifiers
rg -n --type=rust 'syn-metadata|Charon-MIR|front::mir|syn-AST' majit/majit-translate/src | head -n 50Repository: youknowone/pyre
Length of output: 102
🏁 Script executed:
#!/bin/bash
set -euo pipefail
sed -n '3200,3270p' majit/majit-translate/src/jit_codewriter/assembler.rs | nl -ba
rg -n --type=rust '\b(bitand|bitor|bitxor)\b' majit/majit-translate/src | head -n 80
rg -n --type=rust '\bsyn::' majit/majit-translate/src/front | head -n 80
rg -n --type=rust 'syn-metadata|Charon-MIR|front::mir|syn-AST' majit/majit-translate/src | head -n 80Repository: youknowone/pyre
Length of output: 102
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Inspect surrounding comment + code
sed -n '3210,3260p' majit/majit-translate/src/jit_codewriter/assembler.rs | nl -ba
# Locate occurrences of the operator names in translate
rg -n --type=rust '\b(bitand|bitor|bitxor)\b' majit/majit-translate/src | head -n 80
# Check for syn:: usage in the frontend
rg -n --type=rust '\bsyn::' majit/majit-translate/src/front | head -n 80
# Look for any references to the syn→MIR migration context
rg -n --type=rust 'syn-metadata|Charon-MIR|front::mir|syn-AST' majit/majit-translate/src | head -n 80Repository: youknowone/pyre
Length of output: 102
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Inspect surrounding comment + code
sed -n '3210,3260p' majit/majit-translate/src/jit_codewriter/assembler.rs | nl -ba
# Locate occurrences of the operator names in translate
rg -n --type=rust '\b(bitand|bitor|bitxor)\b' majit/majit-translate/src | head -n 80
# Check for syn:: usage in the frontend
rg -n --type=rust '\bsyn::' majit/majit-translate/src/front | head -n 80
# Look for any references to the syn→MIR migration context
rg -n --type=rust 'syn-metadata|Charon-MIR|front::mir|syn-AST' majit/majit-translate/src | head -n 80Repository: youknowone/pyre
Length of output: 102
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Inspect surrounding comment + code
sed -n '3210,3260p' majit/majit-translate/src/jit_codewriter/assembler.rs | nl -ba
# Locate occurrences of the operator names in translate
rg -n --type=rust '\b(bitand|bitor|bitxor)\b' majit/majit-translate/src | head -n 80
# Check for syn:: usage in the frontend
rg -n --type=rust '\bsyn::' majit/majit-translate/src/front | head -n 80
# Look for any references to the syn→MIR migration context
rg -n --type=rust 'syn-metadata|Charon-MIR|front::mir|syn-AST' majit/majit-translate/src | head -n 80Repository: youknowone/pyre
Length of output: 102
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# 1) Show the exact updated comment context (no `nl` needed)
sed -n '3225,3245p' majit/majit-translate/src/jit_codewriter/assembler.rs
# 2) Determine whether these operator spellings exist anywhere in translate source
rg -n --type=rust '\b(bitand|bitor|bitxor)\b' majit/majit-translate/src | head -n 50
# 3) Check for syn usage in the MIR/frontend pipeline
rg -n --type=rust '\bsyn::' majit/majit-translate/src/front | head -n 50
rg -n --type=rust 'syn::BinOp' majit/majit-translate/src/front | head -n 50
# 4) Check whether the only occurrences are in this comment area
rg -n --type=rust '\b(bitand|bitor|bitxor)\b' majit/majit-translate/src/jit_codewriter/assembler.rsRepository: youknowone/pyre
Length of output: 7597
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Find explicit syn BinOp usage
rg -n --type=rust 'syn::BinOp' majit/majit-translate/src | head -n 50
rg -n --type=rust '\bBinOp\b' majit/majit-translate/src/front majit/majit-translate/src/translator majit/majit-translate/src/jit_codewriter | head -n 80
# Find where binop_name is set to "bitand"/"bitor"/"bitxor"
rg -n --type=rust '\bbinop_name\b' majit/majit-translate/src/jit_codewriter/jtransform.rs
sed -n '700,820p' majit/majit-translate/src/jit_codewriter/jtransform.rs
# Also check for direct mappings from syn BinOp variants/tokens to these strings
rg -n --type=rust '"bitand"|\"bitor\"|\"bitxor\"' majit/majit-translate/src/front majit/majit-translate/src/translator | head -n 80Repository: youknowone/pyre
Length of output: 16584
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# 1) Find where bitand/bitor/bitxor are used in the frontend pipeline that would set OpKind::BinOp.op
rg -n --type=rust '"(bitand|bitor|bitxor)"' majit/majit-translate/src/front | head -n 80
# 2) Find where OpKind::BinOp is constructed with these op strings (op: "...") in front/
rg -n --type=rust 'OpKind::BinOp\s*\{[^}]*op:\s*"(bitand|bitor|bitxor)"' majit/majit-translate/src/front | head -n 80
# 3) Also search the translator front-end boundary outside front/ (where it crosses from MIR to graph ops)
rg -n --type=rust 'OpKind::BinOp\s*\{[^}]*op:\s*"(bitand|bitor|bitxor)"' majit/majit-translate/src/translator | head -n 80
# 4) Inspect around construction in front/mir.rs if we find any; otherwise inspect the BinOp label mapping comment area.
rg -n --type=rust 'Rvalue::BinaryOp|BinaryOp.*OpKind::BinOp|op:\s*.*' majit/majit-translate/src/front/mir.rs | head -n 80Repository: youknowone/pyre
Length of output: 41
🏁 Script executed:
#!/bin/bash
set -euo pipefail
# Where do these spellings originate within the "front" layer?
rg -n --type=rust '"(bitand|bitor|bitxor)"' majit/majit-translate/src/front | head -n 80
# Look for syn BinOp variant usage
rg -n --type=rust 'syn::BinOp::' majit/majit-translate/src/front | head -n 80
rg -n --type=rust '\bBitAnd\b|\bBitOr\b|\bBitXor\b' majit/majit-translate/src/front | head -n 80
rg -n --type=rust '\bBinOp\b' majit/majit-translate/src/front | head -n 80
# Also search outside front/ in case the syn BinOp lowering is in translator/cutover/adapters
rg -n --type=rust 'syn::BinOp::' majit/majit-translate/src | head -n 80
rg -n --type=rust '\bBitAnd\b|\bBitOr\b|\bBitXor\b' majit/majit-translate/src | head -n 80Repository: youknowone/pyre
Length of output: 41
Clarify the comment: avoid implying syn::BinOp is part of current op-name generation
"bitand"/"bitor"/"bitxor" are still recognized and rewritten at the JIT/blackhole emission boundary (jtransform.rs / assembler.rs), but the operator-spelling path doesn’t reference syn::BinOp types/variants—syn appears to be used for frontend metadata elsewhere (e.g. front/syn_metadata.rs). Reword to describe the naming convention without tying it to syn::BinOp (e.g., “Rust operator-trait spellings (bitand/bitor/bitxor)”).
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@majit/majit-translate/src/jit_codewriter/assembler.rs` around lines 3231 -
3233, Update the explanatory comment that currently ties the
`bitand`/`bitor`/`bitxor` spelling to `syn::BinOp`; instead describe these as
Rust operator-trait spellings (e.g., "Rust operator-trait spellings
(`bitand`/`bitor`/`bitxor`)") that are recognized and rewritten at the
JIT/blackhole emission boundary (see `jtransform.rs` / `assembler.rs`), and keep
the reference to the `OpKind::BinOp.op` renaming behavior; simply reword the
comment to remove any implication that `syn::BinOp` types/variants are involved
in the op-name generation path.
resolve_place collapsed both `.0` and `.1` of a `*Checked (value, bool)` binop-result local to the same scalar base, so a live read of the overflow bit `.1` aliased to the arithmetic value. The binop-scalar collapse is now field-aware: `.0` still collapses to the scalar (the JIT IR models the checked op as a plain BinOp and the paired overflow Assert is dropped), while a read of field 1 or higher of a binop-scalar local returns LowerError::Unsupported — the overflow bit is not modeled. A genuine Ref tuple `.N` still emits the typed FieldRead. No analyzed body reads a checked-binop `.1` as a live value, so the generated jit_trace_gen.rs is byte-identical; the fail-loud arm guards a future live use against silently aliasing the overflow bool. Assisted-by: Claude
Commit the resolved lockfile and drop its .gitignore entry. pyre is an application, so a committed lockfile pins the dependency graph for reproducible builds, and it is the only complete input for the pyre-ci ullbc cache key: the charon extraction monomorphizes crates.io dependency MIR into the .ullbc artefacts, so a registry version drift within a semver range must invalidate the cache — an untracked Cargo.lock is absent at the cache's hashFiles() evaluation and would let a stale ullbc be reused. Assisted-by: Claude
Both heavy jobs (cargo-test, pyre-check) redirect PYRE_SHARED_BUILD into the workspace and add two actions/cache layers, so re-runs and unchanged- source pushes skip the Charon install and ullbc extraction: - Charon binary: cache .pyre-build/charon (+ charon-src for the Windows from-source build) keyed on runner.os/arch + CHARON_VERSION. On a hit install-charon.sh self-skips, removing the ~5-6 min Windows from-source charon build from every job. - ullbc: cache build/llbc as one atomic entry (so the three .ullbc never restore partially and degrade auto-discovery), and gate the Extract LLBC step on the cache hit since extract-llbc.sh never self-skips. The key hashes Cargo.lock, every member manifest, the pyre/ and majit/ source trees (majit-translate is monomorphized into pyre-jit.ullbc) and the extraction scripts; it carries no restore-keys so a stale ullbc is never reused. CHARON_VERSION is a job env mirroring CHARON_VERSION_DEFAULT in scripts/install-charon.sh, so one value drives both the cache key and the script's .installed-version stamp. Locally PYRE_SHARED_BUILD stays unset and the scripts keep using the shared ../.pyre-build. Also add scripts/charon-msvc-env.sh to the path triggers. Assisted-by: Claude
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 5637f393f0
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| fn mark_place_write(place: &Place, uses: &mut [bool], defs: &mut [bool]) { | ||
| match &place.kind { | ||
| PlaceKind::Local(i) => mark_local_def(*i as usize, defs), | ||
| PlaceKind::Projection(inner, _) => mark_place_use(inner, uses, defs), |
There was a problem hiding this comment.
Mark projection indices live before lowering writes
When an Assign writes through an Index projection and the offset local was defined in a predecessor block, this liveness pass only marks the projection base as live and drops the projection element. emit_projection_write later resolves that offset via index_offset_var, but edge_args never threaded it into the target block, so cross-block array/slice writes such as loop-carried a[i] = v can fail with an uninitialized MIR local during lowering.
Useful? React with 👍 / 👎.
…lowering #144 recorded three ingredients differing at once between the arm that degrades (`state.regs[program[pc+1] as usize] += 1`) and the written-out arm that lowers: the compound operator, the computed index, and the same-slot read-modify-write. This fixture varies them one at a time. Measured recorded-degraded set: OP_COMPOUND_COMPUTEDIDX, OP_COMPOUND_LETIDX. arm ingredients result OP_CTRL_ADD control lowers OP_PLAIN_COMPUTEDIDX computed index in lvalue lowers OP_RMW_LETIDX same-slot read-modify-write lowers OP_COMPOUND_LETIDX `+=`, let-bound index degrades OP_COMPOUND_COMPUTEDIDX all three degrades The blocker is the compound-assignment operator alone. Neither the computed index nor the read-modify-write is implicated, so #144's title attributes it to the wrong ingredient. Cause, consistent with the measurement: `<op>=` is recognized only by `lower_state_field_update` (majit-macros/src/jit_interp/jitcode_lower/lower_vable.rs:249), which matches `binary.left` against `Expr::Field` and then looks the member up in `config.state_scalars`. An array-element place is `Expr::Index`, so it returns None at :257 — before the scalar lookup, and for any array whether or not the index is computed. `state.arr[i] = expr` lowers because it is a separate recognizer that routes `[int; virt]` arrays to the vable array path. No fix here: teaching the recognizer array places must lower the index exactly once, and both the read and the write-back go through the vable path rather than the scalar `store_state_field` this function emits. Assisted-by: Claude
Compound assignment was recognized only by `lower_state_field_update`, whose place must be an `Expr::Field` naming a scalar state field. An array element is an `Expr::Index`, so it reached neither that nor `lower_vable_array_write`, which matches `Expr::Assign` only — the arm degraded to a BC_ABORT stub while the written-out `a[i] = a[i] + v` lowered (#144). `lower_vable_array_update` handles `frame.arr[index] <op>= expr` for declared virtualizable arrays with int items: live marker, getarrayitem, BinopI, live marker, setarrayitem. The index is lowered once and its register feeds both the read and the write-back. Desugaring to `a[i] = a[i] + v` at the syntax level would lower the index expression twice — wrong for an impure index, and a second getarrayitem_gc_i on the hot path regardless. Both operands are lowered before any op is emitted so a late decline cannot leave a half-built read behind. Float and ref elements keep degrading: `opcode_for_assign_binop` names the Int binop family, so emitting it against another bank would be wrong. That decline is now the positive control for #140's channel. Test coupling, as #144 required. `OP_BUMP` was the positive case of `degraded_arm_is_named_at_install` and now lowers, so the assertion was substituted rather than dropped: `OP_FBUMP` (a float-element compound assign) takes the positive role, and `OP_BUMP` moves to the silent list so the fix cannot regress unnoticed. `the_named_arms_are_exactly_the_abort_stubs_in_the_ir` independently cross-checks the registry against the IR and still finds exactly one stub. `jit_interp_compound_assign_lowering.rs` flips to asserting every spelling lowers, plus a control proving the recorder is live in that binary — an empty degraded set would otherwise be satisfied by a dead channel. Assisted-by: Claude
Follow-up to #97 (the syn-AST → Charon-MIR JIT front-end swap itself landed in #121). Fixes #72.
Summary
Post-#121 consolidation of the Charon-extracted MIR JIT front-end. Four change classes:
f255e42b16): MIR-level liveness analysis and edge-argument threading through branch/switch links (front::mircompute_mir_liveness,edge_args/target_input_locals); a dynasm AArch64 branch-alignment debug assertion; aload_fast_pairbounds-check fix inpyopcode; and sourcing theeval_loop_jitportal frompyre-jit.ullbc(adds it to the required LLBC set).ascasts asRvalue::UnaryOp(Cast)— lower bank-crossing casts viasimple_callhost callables; emit typedFieldReadfor genuineRef-tuple element reads; key derivedstruct_field_attrsby bare leaf; resolve switch-target inputargs through the feeding link infront::mir_dispatch.syn_metadatahelpers (−545) and the deadcan_thread_variable_to_block/thread_loop_link_argscluster (−111 inmodel.rs); drop the unusedstackerdependency; relocate syn-free utilities intofront::typestr.install-charon.sh/extract-llbc.sh.pyre-buildshared cache + an Ubuntu-24.04 repro Dockerfile); extractpyre-jit.ullbcin thecargo testandpyre/check.pyCI jobs.Local gate:
pyre/check.pydynasm 41/41 + cranelift 41/41 (both backends),cargo test -p majit-translategreen, over freshly re-extracted ULLBC.Self-review
Prompt & Model
Model:
Prompt:
Answer
Summary by CodeRabbit
New Features
Bug Fixes
Chores