Skip to content

majit: add a StaticLength arm to the RangeTo slice-index fold - #1124

Merged
youknowone merged 1 commit into
mainfrom
residual
Aug 9, 2026
Merged

majit: add a StaticLength arm to the RangeTo slice-index fold#1124
youknowone merged 1 commit into
mainfrom
residual

Conversation

@youknowone

@youknowone youknowone commented Aug 9, 2026

Copy link
Copy Markdown
Owner

What this changes

Adds a StaticLength arm to the RangeTo slice-index fold, beside the existing MinusOne arm. A residual &receiver[..end] is rewritten only when the receiver's length is fixed by __array_repeat's ConstInt count, a comparison dominating the site proves the bound on the proving edge, and end matches the comparison operand as the same ArrayLen value.

Census result

Three-stream census A/B at the PR head c78b1c6ecd4 (arm = HEAD, base = HEAD~1 for the two touched files), both arms real builds, per-arm LLBC extraction, HEAD stable across both:

stream base arm newly good
phaseA 1677 1677 0
phaseB 11 10 1 — pyre_interpreter::display::<Impl>::push_onto
skip 1678 1678 0

(unique subjects, not raw lines) — NEWLY BAD 0/0/0, VERDICT CLEAN.

Determinism control: the same code was censused twice back to back; the subject sets were identical across all three streams (0 movement). So the single-subject delta is a real effect of this change, not run-to-run variation.

Please still calibrate expectations: this clears one rtyper subject. It is not a broad coverage win.

The one real corpus site declines, and that is deliberate

call_function_impl_result in pyre/pyre-interpreter/src/call.rs is not rewritten. That site genuinely is in bounds — its args: &[PyObjectRef] is a shared reference and so cannot change length between the two ArrayLen reads — but the frontend has no shared-reference/immutability notion with which to prove it, so the fold correctly refuses. The anchor test is named call_function_impl_result_declines_residual_array_index and its doc comment says exactly this.

Why the rule is shaped the way it is

An earlier revision of this fold rewrote that site. A three-lens adversarial review then proved by execution that it did so only through two unsound admissions:

  1. The stability scan window ran [proving_edge .. site_op), but the interval that must be free of length-changing operations is [earlier ArrayLen .. later ArrayLen]. In any acyclic diamond the comparison block is reachable backward from the site but never forward from the proving edge, so a mutation between the compared length read and the branch was never scanned. Moving a byte-identical mutating call from the site block into the entry block flipped decline → admit.
  2. may_reference_base returned early for any operation that did not syntactically name the base, so a mutation reached through a second handle — an owner object, or a base published by an allowlisted ArrayWrite and reloaded — was invisible even inside the window.

Both emit getslice(buf, 0, 9) on a length-8 array, and ll_listslice_startstop clamps rather than panicking, so the failure mode is a silent wrong-length slice rather than a crash.

This PR fixes both. The window now spans the two ArrayLen definitions ordered by dominance (unorderable reads decline); inside it, a call outside the read-only allowlist declines regardless of its operands; and the base declines if it was published into a FieldWrite/ArrayWrite value slot or passed to a non-allowlisted call before the later read.

A latent miscompile fix to code already on main

range_feeds_only_index now requires exactly one end FieldWrite on the range value before either arm may substitute the captured operand.

This tightens the MinusOne arm already on main, whose guard is

let is_construction_write =
    matches!(&op.kind, OpKind::FieldWrite { base, .. } if base == range_result);

— keyed only on the base, with no field-name check and no uniqueness count. A later range.end = m therefore passes the consumer gate while the ctor-time value is the one planted, and the write becomes dead. Census-invisible, because it is a guard rather than a coverage lever, but real.

Verification

  • cargo test --release -p majit-translate --lib — 3167 passed, 0 failed, 33 ignored
  • front::slice_index module — 31 passed, 0 failed
  • anchor (--ignored call_function_impl_result) — 2 passed, 0 failed
  • cargo check -p majit-translate --all-targets, cargo fmt --check — clean

Each of the four new negative regressions was verified by mutation: the guard was reverted, the test observed to fail, and the guard restored.

🤖 Generated with Claude Code

The fold now also proves a RangeTo bound from a receiver whose length is
fixed by __array_repeat's ConstInt count, a comparison dominating the site
on the proving edge, and an `end` matched to the comparison operand as the
same ArrayLen value.

The stability scan spans the two ArrayLen definitions, ordered by dominance
and operation index; reads that cannot be ordered decline. Inside that
interval a call outside the read-only allowlist declines regardless of its
operands, and the base declines if it was published into a FieldWrite or
ArrayWrite value slot, or passed to a call outside the allowlist, before
the later read.

range_feeds_only_index now requires exactly one `end` FieldWrite on the
range value before either the MinusOne or the StaticLength arm substitutes
the captured operand.

call_function_impl_result declines: its `args` is a shared reference, which
the frontend has no way to express.

Three-stream census at eba36d1 is unchanged by this commit
(phaseA 1648, phaseB 6, skip 1653; no newly-failing subject).

Assisted-by: Claude
@coderabbitai

coderabbitai Bot commented Aug 9, 2026

Copy link
Copy Markdown

Review Change Stack

Walkthrough

The slice-index pass now recognizes statically proven RangeTo bounds and emits __getslice_rangeto. It adds conservative alias, control-flow, mutation, and range-consumer checks. Tests cover successful rewrites, rejected proofs, and residual indexing.

Changes

RangeTo rewrite extension

Layer / File(s) Summary
RangeTo bound contract and rewrite dispatch
majit/majit-translate/src/front/slice_index.rs
The pass adds StaticLength bounds, validates end values and writes, and dispatches to the appropriate getslice helper.
Static-length proof analysis
majit/majit-translate/src/front/slice_index.rs
The pass resolves aliases, detects static repeat lengths, checks dominance and comparisons, and rejects unsafe mutations.
Rewrite regression coverage
majit/majit-translate/src/front/slice_index.rs, majit/majit-translate/src/front/mir.rs
Tests cover proof cases, rejection cases, helper signatures, and intentional residual array indexing.

Estimated code review effort: 4 (Complex) | ~45 minutes

Sequence Diagram(s)

sequenceDiagram
  participant Frontend
  participant StaticLengthProof
  participant RangeConsumerValidation
  participant SliceIndexRewriter
  Frontend->>StaticLengthProof: analyze RangeTo bound
  StaticLengthProof->>RangeConsumerValidation: provide proven end
  RangeConsumerValidation->>SliceIndexRewriter: approve valid consumer
  SliceIndexRewriter->>Frontend: emit getslice helper or retain residual operation
Loading

Possibly related PRs

  • youknowone/pyre#932: Extends the slice-index and getslice rewrite infrastructure in the same frontend file.
  • youknowone/pyre#1029: Introduces the RangeTo rewrite behavior extended by this change.

Poem

I hop through bounds where static lengths shine,
And guard every alias in line.
If proof is clear, slices bloom anew;
If not, residual indexing stays true.
Binky, the rabbit, approves the queue!

🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check ✅ Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check ✅ Passed Check skipped because no linked issues were found for this pull request.
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title clearly and concisely describes the primary change: adding a StaticLength arm to the RangeTo slice-index fold.
✨ Finishing Touches
📝 Generate docstrings
  • Create stacked PR
  • Commit on current branch
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch residual

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

@github-actions

github-actions Bot commented Aug 9, 2026

Copy link
Copy Markdown

🤖 Codex parity review

Static analysis of this diff vs the local RPython/PyPy sources (commit c78b1c6).
Updated: 2026-08-09T12:10:47.911Z

Files in the reviewed diff
majit/majit-translate/src/front/mir.rs
majit/majit-translate/src/front/slice_index.rs

1. Regressions to PyPy parity introduced by this patch

  • majit/majit-translate/src/front/slice_index.rs:233 ↔ rpython/rtyper/rtyper.py:778 — the new require_end_write gate rejects a previously rewritable RangeTo/len - 1 site unless it finds exactly one field literally named "end" (end_writes == 1). MIR can fall back to __pos_0 for unresolved aggregate field schemas, so this newly loses the existing rewrite solely due to representation metadata; upstream passes the positional stop operand directly to getslice.

2. Other mismatches introduced by this patch

  • majit/majit-translate/src/front/slice_index.rs:413 ↔ rpython/rtyper/rtyper.py:774resolve_block_alias discards non-variable incoming link arguments via LinkArg::as_variable(). Thus a phi receiving both a variable and a constant is incorrectly treated as the variable alone. That can falsely identify a receiver as __array_repeat, prove the wrong static length, and replace Rust indexing with getslice; upstream consumes the actual positional slice operand and does not erase alternate incoming values.

  • majit/majit-translate/src/front/slice_index.rs:582 ↔ rpython/rtyper/rtyper.py:755 — the patch introduces HashMap<BlockId, HashSet<BlockId>> dominator engines (duplicated again at line 779) with no corresponding RPython data structure or phase. Upstream’s slice lowering is the direct decompose_slice_args() contract, not a separate CFG/value-numbering proof pass. This is a non-line-by-line structural divergence, contrary to the required port shape.

3. Pre-existing mismatches (already present before this patch)

  • majit/majit-translate/src/front/slice_index.rs:270 ↔ rpython/rtyper/rtyper.py:765RangeFrom rewrites still require a literal non-negative ConstInt; upstream accepts any SomeInteger proven nonneg, including runtime values. This restriction predates the patch.

  • majit/majit-translate/src/front/slice_index.rs:181 ↔ rpython/rtyper/rtyper.py:775 — before this patch, all RangeTo cases except len - 1 were declined, although upstream lowers a non-negative stop through ordinary startstop slicing. The patch adds one narrow static-array case but does not remove the pre-existing general gap.

4. Structural adaptations

  • majit/majit-translate/src/front/slice_index.rs:341 ↔ rpython/rtyper/rtyper.py:755 — mapping Rust RangeTo indexing to synthetic __getslice_rangeto and then RPython getslice(slice, 0, end) is a Rust/CPython-compiler adaptation: Rust indexing panics on an out-of-range range bound, while RPython’s start/stop list helper clamps stop to the list length.

  • majit/majit-translate/src/front/mir.rs:24249 ↔ pypy/interpreter/baseobjspace.py:1549 — the retained residual result for call_function_impl_result reflects the frontend’s inability to represent Rust shared-reference immutability. PyPy explicitly sequences slice unpacking and length acquisition because either can affect the other; Rust’s aliasing/borrow semantics require a different proof representation.

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: c78b1c6ecd

ℹ️ 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".

Comment on lines +413 to +417
.filter_map(|link| {
link.args
.get(arg_index)
.and_then(LinkArg::as_variable)
.cloned()

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Reject constant predecessors in alias resolution

When a block input has both a variable predecessor and a LinkArg::Const predecessor, this filter_map silently discards the constant edge and can therefore report that the input aliases the sole remaining variable. For example, a comparison phi receiving end on one edge and constant 0 on another can be treated as identical to end; the constant edge may satisfy phi <= N while an oversized end reaches the slice site, causing the rewrite to replace Rust's bounds failure with the clamping getslice behavior. Treat any non-variable incoming argument as disagreement rather than omitting it.

AGENTS.md reference: AGENTS.md:L16-L18

Useful? React with 👍 / 👎.

@coderabbitai coderabbitai Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actionable comments posted: 5

🤖 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/front/slice_index.rs`:
- Around line 582-617: Extract the duplicated dominator-map construction into a
shared dominators helper, and compute it once in
rangeto_static_length_bound_matches. Pass the resulting map through
comparison_operand_matches_end and array_len_base_is_stable instead of
rebuilding it per candidate; also precompute each block’s predecessor list
before the fixpoint loop and reuse it during iteration.
- Around line 487-498: Update comparison_for_switch’s recursive bool-unwrapping
path to track recursion state, using a depth counter or HashSet<Variable>
propagated through each nested call. Return None when the same variable is
revisited (or the depth limit is reached), while preserving the existing
comparison extraction for non-cyclic operands.
- Around line 1142-1176: Update the conditional branch setup in the
bound-handling block so the false edge passed to set_branch is the actual
false_block, not other_block. Preserve the site_block/other_block selection used
for downstream control flow, but ensure site_on_true_edge = false gives
false_block a predecessor and allows the edge-dominance check to execute.
- Around line 400-431: Update visit to collect all blocks whose inputargs
contain var rather than selecting the first match; proceed only when exactly one
matching block exists, return None when multiple blocks bind the same variable,
and preserve the existing fallback for no matches.
- Around line 820-844: The StaticLength rewrite in
rangeto_static_length_bound_matches must require proof that the stop operand is
non-negative before producing __getslice_rangeto. Reuse the existing stop-side
non-negative guard used for MinusOne, such as ValueType::Unsigned or an ArrayLen
proof, and reject bounded signed-negative stops so they do not reach
decompose_slice_args.
🪄 Autofix

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 Plus

Run ID: a6a203a4-bb9e-4983-9660-cbe1c84d060f

📥 Commits

Reviewing files that changed from the base of the PR and between 0c3c477 and c78b1c6.

📒 Files selected for processing (2)
  • majit/majit-translate/src/front/mir.rs
  • majit/majit-translate/src/front/slice_index.rs

Comment on lines +400 to +431
let Some((block_id, arg_index)) = graph.blocks.iter().find_map(|b| {
b.inputargs
.iter()
.position(|arg| arg == var)
.map(|i| (b.id, i))
}) else {
return Some(var.clone());
};
let incoming: Vec<Variable> = graph
.blocks
.iter()
.flat_map(|b| &b.exits)
.filter(|link| link.target == block_id)
.filter_map(|link| {
link.args
.get(arg_index)
.and_then(LinkArg::as_variable)
.cloned()
})
.collect();
let incoming: Vec<Variable> = incoming
.into_iter()
.filter(|candidate| candidate != var)
.collect();
let first = incoming.first()?.clone();
if incoming.iter().any(|candidate| candidate != &first) {
return None;
}
visit(graph, &first, seen)
}
visit(graph, var, &mut std::collections::HashSet::new())
}

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🎯 Functional Correctness | 🟡 Minor | ⚡ Quick win

Reject a Variable that is an inputarg of more than one block.

visit selects only the first block whose inputargs contain var. The comment at Lines 388-391 states MIR is not strict SSA and one Variable name can be threaded through several blocks. If the same name is an inputarg of two blocks and no operation defines it, the walk reads only the first block's incoming edges. The returned root can then represent a different value than the one at the use site. comparison_operand_matches_end compares roots by identity at Line 518, so a wrong root turns an unproven bound into an accepted proof.

Use filter and require exactly one match, then decline when several blocks bind the name.

🛡️ Proposed conservative guard
-        let Some((block_id, arg_index)) = graph.blocks.iter().find_map(|b| {
-            b.inputargs
-                .iter()
-                .position(|arg| arg == var)
-                .map(|i| (b.id, i))
-        }) else {
-            return Some(var.clone());
-        };
+        let bindings: Vec<_> = graph
+            .blocks
+            .iter()
+            .filter_map(|b| {
+                b.inputargs
+                    .iter()
+                    .position(|arg| arg == var)
+                    .map(|i| (b.id, i))
+            })
+            .collect();
+        let (block_id, arg_index) = match bindings.as_slice() {
+            [] => return Some(var.clone()),
+            [single] => *single,
+            // The same name binds in several blocks; the incoming set is
+            // ambiguous, so do not guess a root identity.
+            _ => return None,
+        };
📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change
let Some((block_id, arg_index)) = graph.blocks.iter().find_map(|b| {
b.inputargs
.iter()
.position(|arg| arg == var)
.map(|i| (b.id, i))
}) else {
return Some(var.clone());
};
let incoming: Vec<Variable> = graph
.blocks
.iter()
.flat_map(|b| &b.exits)
.filter(|link| link.target == block_id)
.filter_map(|link| {
link.args
.get(arg_index)
.and_then(LinkArg::as_variable)
.cloned()
})
.collect();
let incoming: Vec<Variable> = incoming
.into_iter()
.filter(|candidate| candidate != var)
.collect();
let first = incoming.first()?.clone();
if incoming.iter().any(|candidate| candidate != &first) {
return None;
}
visit(graph, &first, seen)
}
visit(graph, var, &mut std::collections::HashSet::new())
}
let bindings: Vec<_> = graph
.blocks
.iter()
.filter_map(|b| {
b.inputargs
.iter()
.position(|arg| arg == var)
.map(|i| (b.id, i))
})
.collect();
let (block_id, arg_index) = match bindings.as_slice() {
[] => return Some(var.clone()),
[single] => *single,
// The same name binds in several blocks; the incoming set is
// ambiguous, so do not guess a root identity.
_ => return None,
};
let incoming: Vec<Variable> = graph
.blocks
.iter()
.flat_map(|b| &b.exits)
.filter(|link| link.target == block_id)
.filter_map(|link| {
link.args
.get(arg_index)
.and_then(LinkArg::as_variable)
.cloned()
})
.collect();
let incoming: Vec<Variable> = incoming
.into_iter()
.filter(|candidate| candidate != var)
.collect();
let first = incoming.first()?.clone();
if incoming.iter().any(|candidate| candidate != &first) {
return None;
}
visit(graph, &first, seen)
}
visit(graph, var, &mut std::collections::HashSet::new())
}
🤖 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/front/slice_index.rs` around lines 400 - 431,
Update visit to collect all blocks whose inputargs contain var rather than
selecting the first match; proceed only when exactly one matching block exists,
return None when multiple blocks bind the same variable, and preserve the
existing fallback for no matches.

Comment on lines +487 to +498
OpKind::UnaryOp { op, operand, .. } if op == "bool" => {
Some(("bool".to_string(), operand.clone(), switch.clone()))
}
_ => None,
}
})?;
if operand.0 == "bool" {
let nested = comparison_for_switch(graph, &operand.1)?;
return Some(nested);
}
Some((operand.0, operand.1, const_int_value(graph, &operand.2)?))
}

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🩺 Stability & Availability | 🟡 Minor | ⚡ Quick win

Add a recursion guard to the bool unwrap.

comparison_for_switch recurses on the inner operand of a bool UnaryOp with no visited set. resolve_block_alias guards its own cycles, but this call chain does not. A self-referential or mutually referential bool chain makes the function recurse without end and overflows the stack. Pass a depth counter or a HashSet<Variable> through the recursion and return None on repetition.

🤖 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/front/slice_index.rs` around lines 487 - 498,
Update comparison_for_switch’s recursive bool-unwrapping path to track recursion
state, using a depth counter or HashSet<Variable> propagated through each nested
call. Return None when the same variable is revisited (or the depth limit is
reached), while preserving the existing comparison extraction for non-cyclic
operands.

Comment on lines +582 to +617
let mut dominators: std::collections::HashMap<
crate::model::BlockId,
std::collections::HashSet<crate::model::BlockId>,
> = graph
.blocks
.iter()
.map(|block| {
(
block.id,
graph.blocks.iter().map(|other| other.id).collect(),
)
})
.collect();
dominators.insert(graph.startblock, [graph.startblock].into_iter().collect());
let mut changed = true;
while changed {
changed = false;
for block in &graph.blocks {
if block.id == graph.startblock {
continue;
}
let predecessors = graph.predecessors(block.id);
if predecessors.is_empty() {
continue;
}
let mut next = dominators[&predecessors[0]].clone();
for predecessor in &predecessors[1..] {
next.retain(|id| dominators[predecessor].contains(id));
}
next.insert(block.id);
if next != dominators[&block.id] {
dominators.insert(block.id, next);
changed = true;
}
}
}

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🚀 Performance & Scalability | 🟠 Major | ⚡ Quick win

Compute the dominator sets once and pass them in.

This block builds the full dominator map. rangeto_static_length_bound_matches builds the identical map again at Lines 779-809. The two copies are literal duplicates, so a fix to one will not reach the other.

The cost also compounds: rangeto_static_length_bound_matches calls comparison_operand_matches_end inside its for candidate in &graph.blocks loop, and that call reaches this function, so the fixpoint runs once per candidate block. Each iteration of the fixpoint calls graph.predecessors(block.id), which itself scans every block and its successors. The total work is therefore roughly O(B^3) per rewrite site on graphs with many blocks.

Extract one fn dominators(graph: &FunctionGraph) -> HashMap<BlockId, HashSet<BlockId>> helper, compute it once in rangeto_static_length_bound_matches, and pass the result to comparison_operand_matches_end and array_len_base_is_stable. Also hoist the per-block predecessor lists out of the fixpoint loop.

🤖 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/front/slice_index.rs` around lines 582 - 617,
Extract the duplicated dominator-map construction into a shared dominators
helper, and compute it once in rangeto_static_length_bound_matches. Pass the
resulting map through comparison_operand_matches_end and
array_len_base_is_stable instead of rebuilding it per candidate; also precompute
each block’s predecessor list before the fixpoint loop and reuse it during
iteration.

Comment on lines +820 to +844
let Some(success) = (match op.as_str() {
"le" if bound == n => Some(true),
"lt" if n.checked_add(1) == Some(bound) => Some(true),
"gt" if bound == n => Some(false),
"ge" if n.checked_add(1) == Some(bound) => Some(false),
_ => None,
}) else {
continue;
};
let mut true_target = None;
let mut false_target = None;
for link in &candidate.exits {
match link.exitcase {
Some(crate::model::ExitCase::Bool(true)) => true_target = Some(link.target),
Some(crate::model::ExitCase::Bool(false)) => false_target = Some(link.target),
_ => {}
}
}
let (Some(true_target), Some(false_target)) = (true_target, false_target) else {
continue;
};
let proving_edge_target = if success { true_target } else { false_target };
if !comparison_operand_matches_end(graph, end, &lhs) {
continue;
}

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🎯 Functional Correctness | 🟠 Major | ⚡ Quick win

🧩 Analysis chain

🏁 Script executed:

#!/bin/bash
# Description: Inspect the getslice stop-argument nonneg requirement in the rtyper.
set -euo pipefail

fd -t f 'rtyper.rs' | while IFS= read -r f; do
  rg -n -C 12 'decompose_slice_args|must be proved non-negative|nonneg' "$f"
done

# The frontend's own non-negativity gate for the RangeFrom arm, for comparison.
fd -t f 'slice_index.rs' --exec rg -n -C 6 'bound_is_const_nonneg|ValueType::Unsigned'

Repository: youknowone/pyre

Length of output: 12372


🏁 Script executed:

#!/bin/bash
set -euo pipefail

# Locate and inspect the relevant slice_index.rs sections.
target="majit/majit-translate/src/front/slice_index.rs"
if [ -f "$target" ]; then
  wc -l "$target"
  printf '\n--- lines 230-300 ---\n'
  sed -n '230,300p' "$target" | cat -n
  printf '\n--- lines 480-530 ---\n'
  sed -n '480,530p' "$target" | cat -n
  printf '\n--- lines 730-870 ---\n'
  sed -n '730,870p' "$target" | cat -n
else
  echo "missing $target"
fi

printf '\n--- flowspace_adapter slice lowering region ---\n'
rg -n -C 8 '__getslice_rangeto|getslice\(slice, 0, end\)|RangeTo' majit/majit-translate/src/translator/majit/majit-translate/src/translator/rtyper/flowspace_adapter.rs || true

Repository: youknowone/pyre

Length of output: 12677


🏁 Script executed:

#!/bin/bash
set -euo pipefail

printf '%s\n' '--- files matching flowspace_adapter.rs ---'
fd -t f 'flowspace_adapter.rs' . || true

printf '%s\n' '--- flowspace_adapter slice-related terms ---'
rg -n -C 8 '__getslice_rangeto|getslice\(slice, 0, end\)|RangeTo|decompose_slice_args|SliceKind::StartStop' majit/majit-translate/src || true

printf '%s\n' '--- graph ops around range index / getslice lowering in front slice_index.rs ---'
rg -n -C 8 '__getslice_rangeto|getslice|getslice_rangeto|RangeTo|SliceIndexBounds::StaticLength' majit/majit-translate/src/front/slice_index.rs || true

printf '%s\n' '--- AnyWhere rtyper slice adapter terms ---'
rg -n -C 8 '__getslice_rangeto|getslice\(slice, 0, end\)|RangeTo|decompose_slice_args|SliceKind::StartStop' majit/majit-translate/src/translator || true

Repository: youknowone/pyre

Length of output: 50374


🏁 Script executed:

#!/bin/bash
set -euo pipefail

file="majit/majit-translate/src/translator/rtyper/flowspace_adapter.rs"
rg -n -C 12 'decompose_slice_args|SliceKind::StartStop|__getslice_rangeto|getslice\(slice, 0, end\)' "$file" || true
sed -n '1580,1645p' "$file" | cat -n

Repository: youknowone/pyre

Length of output: 10145


Require a non-negative stop before rewriting StaticLength bounds.

StaticLength only proves end <= n, then rewrites to __getslice_rangeto(slice, end), which lowers to getslice(slice, 0, end). decompose_slice_args rejects runtime SomeInteger stop operands unless nonneg is true, so this can cause rtyping failure and fall through to a bare unwired getslice. Add the same stop-side non-negative guard used for MinusOne (for example ValueType::Unsigned or an ArrayLen proof) in rangeto_static_length_bound_matches, and add a rejection case for a bounded signed negative stop.

🤖 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/front/slice_index.rs` around lines 820 - 844, The
StaticLength rewrite in rangeto_static_length_bound_matches must require proof
that the stop operand is non-negative before producing __getslice_rangeto. Reuse
the existing stop-side non-negative guard used for MinusOne, such as
ValueType::Unsigned or an ArrayLen proof, and reject bounded signed-negative
stops so they do not reach decompose_slice_args.

Comment on lines +1142 to +1176
let (site_block, other_block, true_block) = if bound.is_some() {
let (true_block, _) = g.create_block_with_arg_vars(0);
let (false_block, _) = g.create_block_with_arg_vars(0);
(
if site_on_true_edge {
true_block
} else {
false_block
},
if site_on_true_edge {
false_block
} else {
true_block
},
true_block,
)
} else {
(entry, entry, entry)
};
if let Some(bound) = bound {
let bound_var = g.push_op_var(entry, OpKind::ConstInt(bound), true).unwrap();
let cond = g
.push_op_var(
entry,
OpKind::BinOp {
op: "le".into(),
lhs: end.clone(),
rhs: bound_var,
result_ty: ValueType::Bool,
},
true,
)
.unwrap();
g.set_branch(entry, cond, true_block, vec![], other_block, vec![]);
}

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

🎯 Functional Correctness | 🟠 Major | ⚡ Quick win

The site_on_true_edge = false graph never reaches the site block.

true_block always holds the real true target. other_block is the complement of site_block, so other_block == false_block only when site_on_true_edge is true. When site_on_true_edge is false, other_block == true_block, and Line 1175 sends both edges to true_block. site_block is then false_block, which has no predecessor.

rangeto_static_length_wrong_edge_declines at Lines 2122-2127 therefore passes because the index site is unreachable, not because the site sits on the failing edge. The edge-dominance check at Lines 845-852 stays uncovered for that case.

Pass the real false target to set_branch.

🐛 Proposed fix
-        let (site_block, other_block, true_block) = if bound.is_some() {
+        let (site_block, other_block, true_block, false_block) = if bound.is_some() {
             let (true_block, _) = g.create_block_with_arg_vars(0);
             let (false_block, _) = g.create_block_with_arg_vars(0);
             (
                 if site_on_true_edge {
                     true_block
                 } else {
                     false_block
                 },
                 if site_on_true_edge {
                     false_block
                 } else {
                     true_block
                 },
                 true_block,
+                false_block,
             )
         } else {
-            (entry, entry, entry)
+            (entry, entry, entry, entry)
         };
@@
-            g.set_branch(entry, cond, true_block, vec![], other_block, vec![]);
+            g.set_branch(entry, cond, true_block, vec![], false_block, vec![]);
📝 Committable suggestion

‼️ IMPORTANT
Carefully review the code before committing. Ensure that it accurately replaces the highlighted code, contains no missing lines, and has no issues with indentation. Thoroughly test & benchmark the code to ensure it meets the requirements.

Suggested change
let (site_block, other_block, true_block) = if bound.is_some() {
let (true_block, _) = g.create_block_with_arg_vars(0);
let (false_block, _) = g.create_block_with_arg_vars(0);
(
if site_on_true_edge {
true_block
} else {
false_block
},
if site_on_true_edge {
false_block
} else {
true_block
},
true_block,
)
} else {
(entry, entry, entry)
};
if let Some(bound) = bound {
let bound_var = g.push_op_var(entry, OpKind::ConstInt(bound), true).unwrap();
let cond = g
.push_op_var(
entry,
OpKind::BinOp {
op: "le".into(),
lhs: end.clone(),
rhs: bound_var,
result_ty: ValueType::Bool,
},
true,
)
.unwrap();
g.set_branch(entry, cond, true_block, vec![], other_block, vec![]);
}
let (site_block, other_block, true_block, false_block) = if bound.is_some() {
let (true_block, _) = g.create_block_with_arg_vars(0);
let (false_block, _) = g.create_block_with_arg_vars(0);
(
if site_on_true_edge {
true_block
} else {
false_block
},
if site_on_true_edge {
false_block
} else {
true_block
},
true_block,
false_block,
)
} else {
(entry, entry, entry, entry)
};
if let Some(bound) = bound {
let bound_var = g.push_op_var(entry, OpKind::ConstInt(bound), true).unwrap();
let cond = g
.push_op_var(
entry,
OpKind::BinOp {
op: "le".into(),
lhs: end.clone(),
rhs: bound_var,
result_ty: ValueType::Bool,
},
true,
)
.unwrap();
g.set_branch(entry, cond, true_block, vec![], false_block, vec![]);
}
🤖 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/front/slice_index.rs` around lines 1142 - 1176,
Update the conditional branch setup in the bound-handling block so the false
edge passed to set_branch is the actual false_block, not other_block. Preserve
the site_block/other_block selection used for downstream control flow, but
ensure site_on_true_edge = false gives false_block a predecessor and allows the
edge-dominance check to execute.

@youknowone

Copy link
Copy Markdown
Owner Author

Correction to the original PR description.

The description as first posted stated the census yield of this PR was zero. That figure was measured at eba36d13ed9 and was correct there, but it is not correct for the code as it will land. The branch was subsequently rebased onto commits that touch majit-translate (including front/mir.rs), and re-measuring at the PR head gives a different answer:

stream base arm newly good
phaseA 1677 1677 0
phaseB 11 10 1 — pyre_interpreter::display::<Impl>::push_onto
skip 1678 1678 0

NEWLY BAD 0/0/0, VERDICT CLEAN. Unique subjects, not raw lines.

I re-ran the same code twice as a determinism control before believing the delta: the subject sets were identical across all three streams, so this is a real effect of the change rather than run-to-run variation.

The description has been updated. The earlier zero was a stale measurement on my part, not a property of the change.

commented by Claude

@youknowone

Copy link
Copy Markdown
Owner Author

CI triage — none of the three red checks is caused by this PR

Control used throughout is the parent-sha run (0c3c4777ba9, run 31303981088), not the merge base.

check parent 0c3c4777ba9 this PR c78b1c6ecd4 verdict
CPython suite (gate) fail fail pre-existing
pyre/check.py (macos-latest) fail fail pre-existing
pyre/check.py (ubuntu-24.04) pass fail false red — see below

CPython suite (gate) and check.py (macOS)

Byte-for-byte the same failures on both commits:

test.test_pickletools: PASS -> FAIL  rc=1  FAILED (errors=1,   skipped=13)  ERROR: test_ints
test.test_re:          PASS -> FAIL  rc=1  FAILED (errors=303, skipped=13)

macOS check.py additionally reports dynasm 1 failed, 410 passed on both. Identical error and skip counts on parent and head.

check.py (ubuntu) — a perf gate whose denominator halved

This one did flip from pass to fail, so it deserved a real look. The failing rows are a single fixture out of 410, on both backends at once:

FAIL dynasm    synth/mapdict_frozen_unboxing_fold  exec 1.30s > pypy 0.02s  ratio 64.9x > gate 63x
FAIL cranelift synth/mapdict_frozen_unboxing_fold  exec 1.52s > pypy 0.02s  ratio 70.8x > gate 63x

Comparing the absolute columns against the parent run:

cpython pypy dynasm cranelift third
parent (passed) 0.24s 0.06s 1.38s → 28.5x 1.57s → 32.5x 2.35s → 50.4x
this PR (failed) 0.22s 0.03s 1.37s → 68.8x 1.60s → 80.6x 2.26s → 117.3x

pyre's own execution times did not regress — dynasm 1.38s → 1.37s, the third column 2.35s → 2.26s, cranelift 1.57s → 1.60s (+1.9%, within noise). What moved is the pypy denominator, 0.06s → 0.03s, and all three ratios rose by the same ~2.2× factor as a result.

Three ratios moving together by an identical factor while the numerators stay flat is a denominator move, not a codegen change — a codegen regression cannot lift every backend's ratio by the same multiple while leaving every backend's absolute time unchanged. At 0.02–0.03s the pypy measurement is at its resolution floor, where a few milliseconds swings the ratio past a 63x gate that this row was already sitting under by a small margin.

This is the known denominator-collapse class in the synth perf gate, not a property of this change.

commented by Claude

@youknowone
youknowone merged commit 241a97f into main Aug 9, 2026
14 of 17 checks passed
@youknowone
youknowone deleted the residual branch August 9, 2026 13:26
@youknowone

Copy link
Copy Markdown
Owner Author

Follow-up on the parity review: #1133.

§2 (resolve_block_alias dropped non-variable incoming arguments) — real, and fixed there. filter_map discarded a non-variable incoming argument instead of treating it as a disagreement, so [Variable(v), Constant(7)] resolved to v's root. Collecting into Option<Vec<Variable>> short-circuits on the first one. Links out of blocks unreachable from startblock cannot execute and are excluded from the walk rather than allowed to veto a resolution.

§1 (the end write is matched as field.name == "end") — the code reading is right, but this PR did not narrow a rewrite the older code performed. is_construction_write has never keyed on the field name and still does not; the end_writes gate only requires the write to be unique and named. This PR also added resolve_block_alias, which widened which sites are recognised at all — so accepting __pos_0 would admit sites only the new alias resolution makes visible, not restore an earlier rewrite. It was implemented and measured, cleared no additional prepass subject, and is not included; a test records the decline with that reasoning.

§3 (dominance/reachability sets vs. the decompose_slice_args() contract) — not addressed; it is an objection to the fold's design rather than to these two defects.

One measurement note for anyone reading the census numbers in this PR's history: pyre_interpreter::display::<Impl>::push_onto is not stable in the three-stream prepass census — on a byte-identical tree it scored phaseB 15 once and 14 eight times across independent runs. Single-observation 1-subject deltas on that row are not evidence in either direction.

commented by Claude

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.

1 participant