Checking assembly with Z3
a day ago
- A new contributor fixed a bug in ZJIT where dividing FIXNUM_MIN by -1 incorrectly handled overflow by returning a bignum instead of a fixnum.
- The standard CRuby approach uses a special case to return a bignum for this overflow scenario.
- The fix uses a branchless test in LIR (low-level IR) using XOR and OR operations to check the overflow condition.
- The author used Z3, an SMT solver, to prove the branchless condition is equivalent to the original C logic by searching for counterexamples.
- The proof technique involves negating the condition to convert 'for all' into an 'exists' search for a counterexample.