James Routley

Short post today. New ZJIT contributor dak2 submitted a PR to fix an overflow bug in fixnum division in ZJIT. We did the division fine, but lied about the type of the result in the case of dividing FIXNUM_MIN by -1. You can see how this is special-cased in CRuby:

static inline void
rb_fix_divmod_fix(VALUE a, VALUE b, VALUE *divp, VALUE *modp)
{
    // ...
    if (x == FIXNUM_MIN && y == -1) {
        if (divp) *divp = LONG2NUM(-FIXNUM_MIN);
        if (modp) *modp = LONG2FIX(0);
        return;
    }
    // ...
}

Since -FIXNUM_MIN (note the negative) does not fit in a fixnum, it gets promoted to a bignum. It’s one of two special cases in fixnum division that does not produce a fixnum, the other being dividing by zero (which produces an error).

$ irb
irb(main):001> LONG_MAX = 2**63 - 1
=> 9223372036854775807
irb(main):002> FIXNUM_MAX = LONG_MAX / 2
=> 4611686018427387903
irb(main):003> LONG_MIN = -LONG_MAX - 1
=> -9223372036854775808
irb(main):004> FIXNUM_MIN = LONG_MIN / 2
=> -4611686018427387904
irb(main):005> (-FIXNUM_MIN) < FIXNUM_MAX
=> false
irb(main):006>
$

This is due to the numbers being two’s complement and therefore having more negative numbers than positive numbers (because of zero).

dak2’s proposed patch included a branchless test for this left == FIXNUM_MIN and right == -1 case, making us leave JIT code and enter the interpreter rather than handle it inline. The patch encodes this branchless test as xor, xor, or, test, je in our platform-independent low-level IR (LIR):

// Side exit on FIXNUM_MIN / -1, which overflows to a Bignum, not a Fixnum.
// Branchless (left == FIXNUM_MIN && right == -1): (left ^ MIN) | (right ^ -1) == 0.
let left_diff = asm.xor(left, Opnd::from(VALUE::fixnum_from_isize(RUBY_FIXNUM_MIN)));
let right_diff = asm.xor(right, Opnd::from(VALUE::fixnum_from_isize(-1)));
let combined = asm.or(left_diff, right_diff);
asm.test(combined, combined);
asm.je(jit, side_exit(jit, state, FixnumDivOverflow));

I didn’t understand why those were equivalent. Rather than try and bang my head against it, I thought I’d let Z3 try. After all, I’ve been watching CF have fun with it for a couple years now.

Z3 is an SMT solver. The core trick to use Z3 as a “proof engine” that I learned from CF¹ is to make Z3 search for counter-examples by negating the condition:

#!/usr/bin/env python3
# /// script
# requires-python = ">=3.13"
# dependencies = [
#     "z3-solver",
# ]
# ///

import z3

WORD_SIZE = 64
LONG_MAX   = z3.BitVecVal(2**63 - 1, WORD_SIZE)
LONG_MIN   = -LONG_MAX - 1
FIXNUM_MIN = LONG_MIN / 2

def prove(cond):
    solver = z3.Solver()
    assert solver.check(z3.Not(cond)) == z3.unsat, solver.model()

left = z3.BitVec("left", WORD_SIZE)
right = z3.BitVec("right", WORD_SIZE)
# The original C condition
lhs = z3.And(left == FIXNUM_MIN, right == -1)
# The new branchless LIR
rhs = ((left ^ FIXNUM_MIN) | (right ^ -1)) == 0
prove(lhs == rhs)

This negation is required because the core model of Z3 is a machine that finds example values. This means that there is an implicit “exists” in front of your condition. To disprove this, Z3 needs to search all inputs. However, if you negate the condition, it becomes a “for all”. This means that in order to disprove the “for all”, Z3 only needs to find a single counterexample.

$ uv run prove_fixnum_min.py
$

Z3 did not complain, so the new code must be fine. Just as a quick check, in case assert is turned off or something, I like to see tests fail. So after modifying one of the constants from -1 to 0:

$ uv run prove_fixnum_min.py
Traceback (most recent call last):
  File "/path/prove_fixnum_min.py", line 26, in <module>
    prove(lhs == rhs)
    ~~~~~^^^^^^^^^^^^
  File "/path/prove_fixnum_min.py", line 18, in prove
    assert solver.check(z3.Not(cond)) == z3.unsat, solver.model()
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
AssertionError: [right = 18446744073709551615, left = 13835058055282163712]
$

Neat.

Thanks

Thanks to CF Bolz-Tereick for reading and giving feedback on this post.

Checking assembly with Z3

Thanks