Integer division (`/`) and remainder (`%`) abort with `unimplemented!`, and bypass div-by-zero / `MIN / -1` panic checking

[coord-e]

Bug

Thrust aborts (unimplemented!) whenever a function performs integer division or remainder. These are common operations on supported Int-modeled types, so any program using a / b or a % b cannot be analyzed at all.

Repro

#[thrust::callable]
fn half(a: i32) {
    let _ = a / 2;
}

fn main() {}

Running thrust-rustc on this aborts with an unimplemented! panic rather than producing a verification result.

Root cause

Division/remainder are unsupported at two layers:

1. MIR translation (src/analyze/basic_block.rs)

Rvalue::BinaryOp only matches Add, Sub, Mul, and the comparison operators. BinOp::Div and BinOp::Rem fall through to the catch-all:

// src/analyze/basic_block.rs, in rvalue_type / Rvalue::BinaryOp
match (&lhs_ty, op) {
    (rty::Type::Int, mir::BinOp::Add) => { ... }
    (rty::Type::Int, mir::BinOp::Sub) => { ... }
    (rty::Type::Int, mir::BinOp::Mul) => { ... }
    (rty::Type::Int | rty::Type::Bool, mir::BinOp::Ge) => { ... }
    // ... Gt / Le / Lt / Eq / Ne ...
    _ => unimplemented!("ty={}, op={:?}", lhs_ty.display(), op),   // ← Div / Rem land here
}

2. CHC term layer (src/chc.rs)

There is no division/modulo Function at all — Function defines ADD, SUB, MUL, NEG, the comparisons, AND/OR/NOT, and STORE/SELECT, but nothing for div/mod. So even a one-line addition to the MIR match has nothing to lower to.

Why this is non-trivial (not just a missing match arm)

A correct implementation has to deal with core-logic subtleties that a naive Div => App(DIV, …) would get wrong:

1. Truncated vs. Euclidean semantics. Rust's / truncates toward zero and % takes the sign of the dividend (-7 / 2 == -3, -7 % 2 == -1). SMT-LIB2's div/mod (theory of ints) are Euclidean: mod is always non-negative ((div (- 7) 2) is -4, (mod (- 7) 2) is 1). Lowering Rust //% directly to SMT div/mod is therefore unsound for negative operands. The translation needs to either encode truncated division explicitly or adjust the Euclidean result by the sign of the operands.

2. New panic conditions to verify. Unlike +/-/*, division introduces panics that Thrust — as a panic-absence verifier — should be checking, independent of the -C debug-assertions setting:

   • Division by zero (a / 0, a % 0): rustc always inserts an Assert(Ne(divisor, 0)) before the Div/Rem (it is not gated on debug-assertions). That assertion is analyzed today, but since the following Div/Rem is unimplemented, analysis aborts before a result is produced, so the div-by-zero obligation is never actually discharged end-to-end.
   • INT::MIN / -1 overflow (and the analogous %): also a panic in Rust.

   For nonlinear divisors these obligations are also non-trivial for the backend solver, which is worth noting when designing the encoding.

Suggested direction

• Add Div/Rem arms to the Rvalue::BinaryOp match in rvalue_type.
• Add corresponding Functions in src/chc.rs and their SMT-LIB2 emission, using an encoding that matches Rust's truncated semantics rather than SMT's Euclidean div/mod.
• Decide how the div-by-zero and MIN / -1 obligations should surface (they should be verifiable, like other panics).

Happy to take a crack at this if it's wanted — flagging first because the semantic-mismatch and panic-checking aspects are design decisions rather than a mechanical addition.