Checking assembly with Z3 | Max Bernstein

home<br>blog<br>microblog<br>favorites<br>pl resources<br>bread<br>recipes<br>rss

Checking assembly with Z3

June 1, 2026

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

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

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

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

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

dak2’s proposed patch included a branchless test for this left == FIXNUM_MIN and<br>right == -1 case, making us leave JIT code and enter the interpreter rather<br>than handle it inline. The patch encodes this branchless test as xor, xor,<br>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.<br>// Branchless (left == FIXNUM_MIN && right == -1): (left ^ MIN) | (right ^ -1) == 0.<br>let left_diff = asm.xor(left, Opnd::from(VALUE::fixnum_from_isize(RUBY_FIXNUM_MIN)));<br>let right_diff = asm.xor(right, Opnd::from(VALUE::fixnum_from_isize(-1)));<br>let combined = asm.or(left_diff, right_diff);<br>asm.test(combined, combined);<br>asm.je(jit, side_exit(jit, state, FixnumDivOverflow));

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

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

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

import z3

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

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

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

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

$ uv run prove_fixnum_min.py

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

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

Neat.

Thanks

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

They note that this is a “standard technique” and they did not<br>come up with it. ↩