Read unsigned integer constants as unsigned - #277
Conversation
const_value_ty read Uint constants with to_int, which sign-extends, so a constant with the high bit set such as 255u8 became -1. Read them with to_uint instead. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WZXwt16ZiUmjT6hDYraDtb
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. |
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WZXwt16ZiUmjT6hDYraDtb
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
The unsigned high-bit regression needs the required paired UI tests.
Get a fresh assessment by requesting another Copilot review.
Review effort: Balanced
Findings: 1
What changed in this PR
Corrects unsigned MIR constants so high-bit values are not sign-extended.
Changes:
- Handles signed and unsigned constants separately.
- Uses
ScalarInt::to_uintfor unsigned values.
| File | Description |
|---|---|
src/analyze/basic_block.rs |
Corrects unsigned constant conversion. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
![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: 0a5b0970c1
ℹ️ 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".
| let val = val.to_uint(val.size()); | ||
| PlaceType::with_ty_and_term( | ||
| rty::Type::int(), | ||
| chc::Term::int(val.try_into().unwrap()), |
There was a problem hiding this comment.
For u64, usize on 64-bit targets, or u128 constants above i64::MAX, to_uint produces a u128 that this conversion cannot narrow to the i64 accepted by Term::int, so the unwrap() panics before verification. For example, analyzing let x: u64 = u64::MAX; assert!(x > 200); aborts here with TryFromIntError; represent the full unsigned value in the CHC term or report unsupported widths without panicking.
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>
const_value_tyreadUintconstants withScalarInt::to_int, which sign-extends. So a constant with the high bit set, such as255u8, became-1. As a result,let x: u8 = 255; assert!(x > 200);was reported as Unsat, andassert!(x < 200)verified.This splits the arm so that
Uintconstants are read withto_uint.🤖 Generated with Claude Code
https://claude.ai/code/session_01WZXwt16ZiUmjT6hDYraDtb