Sign-extend SwitchInt targets of signed discriminants

[coord-e]

Fixes #132.

mir::SwitchTargets::iter() yields each case as the discriminant type's bit pattern zero-extended into a u128, and type_switch_int converted it with val.try_into::<i64>().unwrap(). For a signed discriminant a negative case therefore arrived as a large positive number — the -1 arm of an i32 match was pinned to 4294967295. The discriminant operand itself is modeled as its true value, so such an arm was verified under a path assumption nothing satisfies (silently accepting programs that panic), while a comparison against a negative literal was rejected as unreachable. An i64 discriminant hit the try_into().unwrap() instead.

The Int case now takes the width and signedness from the discriminant's MIR type (Ty::int_size_and_signed) and sign-extends the bit pattern (Size::sign_extend) before building the literal.

Behavior

program	before	after
match x { -1 => assert!(x > 0), _ => {} } (panics at runtime)	accepted as safe (unsound)	Unsat
let x: i32 = -1; assert!(x == -1)	Unsat	accepted
a.signum(), a < 0 => s == -1	Unsat	accepted
negative literal against an i64	TryFromIntError panic	accepted
match x { 1 => assert!(x > 1), _ => {} } (positive control)	Unsat	Unsat

Tests

tests/ui/{pass,fail}/switch_int_negative.rs. Before the change the pass file is reported Unsat and the fail file is accepted; after it, the reverse — so the pair pins both faces of the bug. Full cargo test (330 UI tests) passes, as do cargo fmt --check and cargo clippy --all-targets.

[Copilot]

🟡 Changes recommended

The distinct negative i64 regression remains untested despite the width-sensitive fix.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

Corrects SwitchInt path assumptions for negative signed discriminants.

Changes:

• Sign-extends integer targets using MIR width and signedness.
• Adds pass/fail regression tests for negative i32 targets.

File summaries

File	Description
src/analyze/basic_block.rs	Corrects signed target conversion.
tests/ui/pass/switch_int_negative.rs	Adds valid negative-match coverage.
tests/ui/fail/switch_int_negative.rs	Adds unsound-branch rejection coverage.

Review details

• Files reviewed: 3/3 changed files
• Comments generated: 1
• Review effort level: Balanced

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.