Verify the absence of overflow in checked integer arithmetic

[coord-e]

This is the first stage of the fix for the arithmetic-overflow issue found while reviewing #278.

With overflow checks on, rustc lowers integer + / - / * to AddWithOverflow / SubWithOverflow / MulWithOverflow followed by an assert on the overflow flag. Thrust hit unimplemented! on these operations, which is why every UI test is compiled with -C debug-assertions=off.

Changes

• AddWithOverflow / SubWithOverflow / MulWithOverflow now evaluate to the pair (result, overflowed):
  • result is the mathematical result, with no wrapping. rustc reads it only after the assertion that no overflow happened, so it is always in range when read.
  • overflowed is true exactly when result lies outside the operand type's range.
• The existing Assert handling then turns each overflow check into a verification condition, so a program that can overflow is rejected.
• Operand MIR types are read from Analyzer::local_decls. body.local_decls does not include the temporaries that ReborrowVisitor adds.

Tests

Both pairs are compiled with -C overflow-checks=on:

• int_overflow_checked: an i64 x + 1 guarded against i64::MAX. The fail side has the guard off by one.
• int_underflow_checked: a u32 x - 1 guarded against 0. The fail side has the guard off by one.

On main, both pairs stop at not implemented: ty=int, op=AddWithOverflow (or SubWithOverflow). cargo test fails on exactly the same set of tests as main (65 PCSat tests: the local coar:main image can't handle (Seq Int)). fmt and clippy are clean.

Not covered (next stage)

• Integer values carry no range facts yet. For example, nothing records that a u32 parameter is non-negative, so a guard is needed on both sides of a value unless the inferred precondition already bounds it.
• Wrapping arithmetic when overflow checks are off will be handled together with range facts.

🤖 Generated with Claude Code

https://claude.ai/code/session_01MvvhC4sHsobSMHAn9CgLBq

---

Generated by Claude Code