Checking assembly with Z3

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>…