Support integer-to-integer casts - #278
Conversation
Rvalue::Cast(IntToInt) fell through to the catch-all unimplemented!, so
code such as `impl Idx for u32 { fn new(idx: usize) -> u32 { idx as u32 } }`
could not be verified without #[thrust::trusted].
An `as` cast between integer types never panics; it silently truncates or
reinterprets the value. The cast is therefore identity only when the
source type's range lies inside the target's; otherwise the result is the
value wrapped into the target's range with SMT-LIB `mod`. Casts involving
bool or char, which MIR also represents as IntToInt, still reach
unimplemented!.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MvvhC4sHsobSMHAn9CgLBq
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
The recursive large-power and negative-dividend wrapping paths lack the repository-required paired UI coverage.
Get a fresh assessment by requesting another Copilot review.
Review effort: Balanced
Findings: 1
Open (1)
What changed in this PR
Adds refinement support for integer-to-integer casts, including truncation and signed reinterpretation.
Changes:
- Models integer casts using identity or modular wrapping.
- Adds SMT
modand large power-of-two terms. - Adds paired UI tests for identity, truncating, and signed casts.
| File | Description |
|---|---|
src/analyze/basic_block.rs |
Implements integer-cast refinement. |
src/chc.rs |
Adds modulo and power-of-two terms. |
tests/ui/pass/int_cast.rs |
Tests valid Idx casts. |
tests/ui/fail/int_cast.rs |
Tests rejection of an invalid cast assertion. |
tests/ui/pass/int_cast_truncate.rs |
Tests valid truncation. |
tests/ui/fail/int_cast_truncate.rs |
Tests incorrect truncation output. |
tests/ui/pass/int_cast_signed.rs |
Tests valid signed reinterpretation. |
tests/ui/fail/int_cast_signed.rs |
Tests incorrect signed output. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01MvvhC4sHsobSMHAn9CgLBq
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 47040781bd
ℹ️ 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 int_ty_includes(self.tcx, ty, op_ty) { | ||
| op_pty |
There was a problem hiding this comment.
When the operand comes from overflowing integer arithmetic with debug assertions disabled, its logical term can be outside the source type's range because BinaryOp::Add is modeled as unbounded integer addition. Returning it unchanged makes verification unsound: fn f(x: u32) -> u64 { (x + 1) as u64 } followed by assert!(f(u32::MAX) == 4294967296) is accepted by the generated constraints, although Rust wraps the addition and returns 0. Normalize the term to the source type's range before deciding that a widening cast is an identity.
Useful? React with 👍 / 👎.
…casts) into forall-sort Brings in coord-e#114 (Rust expressions as thrust::predicate bodies, instantiated per generic arguments), coord-e#275 (newer PCSat in CI), coord-e#276, coord-e#277 and coord-e#278 on top of forall-sort. Resolution: - A predicate call whose instance resolves goes through Analyzer::predicate_with_args, so a Rust-body predicate is defined once per instantiation and a raw SMT-LIB2 predicate keeps its single definition. A call that does not resolve (it still depends on the owner's type parameters) keeps the forall predicate. - predicate_with_args takes the calling function as owner, since forall-sort translates type parameters relative to it; an instance whose arguments mention type parameters is keyed by that owner too. - UserDefinedPredDef keeps both the new body enum and the ForallPred dependency set. A formula body contributes its ForallPred atoms directly and its calls to other user-defined predicates as edges of the dependency graph; a raw body is still scanned by name. - The refinement clause builder records the value-variable origin only when the value term is a variable, as the singleton case substitutes a default term. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Rvalue::Cast(IntToInt)fell through to the catch-allunimplemented!("rvalue=..."). So code likeimpl Idx for u32 { fn new(idx: usize) -> u32 { idx as u32 } fn index(self) -> usize { self as usize } }could only be handled with#[thrust::trusted].Changes
ascast never panics. Instead it truncates or reinterprets the value without warning, and the refinement now models that:u32 → usize,usize → u128,u32 → i64), the value passes through unchanged.N-bit target:x mod 2^NN-bit target:(x + 2^(N-1)) mod 2^N - 2^(N-1)Function::MOD/Term::mod_andTerm::pow2tochc.Term::Intholds ani64, sopow2builds2^64and larger as a product of smaller powers.boolorcharare alsoIntToIntin MIR. They still reachunimplemented!.Tests
int_cast: theIdxexample above, without#[thrust::trusted]int_cast_truncate:(2^32 + 5) as u32 == 5, viau64 → u32int_cast_signed:4294967295 as i32 == -1, viau32 → i32If every cast is forced to identity, the
passsides ofint_cast_truncateandint_cast_signedboth fail.Known limitations
i8/u8/i16/u16/i128/u128have noModelimpl instd.rs, so functions taking or returning them still panic in template building.-C debug-assertions=offis not modeled. A value can therefore fall outside its type's range, and a cast that passes the value through unchanged inherits that gap.🤖 Generated with Claude Code
https://claude.ai/code/session_01MvvhC4sHsobSMHAn9CgLBq
Generated by Claude Code