Checking Assembly with Z3

6 hours ago

A new contributor, dak2, submitted a PR to fix an overflow bug in ZJIT related to fixnum division.
The issue occurs when dividing FIXNUM_MIN by -1, where the result overflows to a bignum, not a fixnum.
In CRuby, this case is handled by a special condition in the function rb_fix_divmod_fix.
dak2's patch uses a branchless test (via xor, or, test, je in LIR) to detect the overflow case and exit to the interpreter.
The author verified the equivalence of the branchless test to the original condition using the Z3 SMT solver.
Z3 confirmed the correctness of the patch by not finding counter-examples when the condition was negated and checked.
The author also tested a modified version with a changed constant to see a failure, confirming Z3's validation process.
Acknowledgements were given to CF Bolz-Tereick for feedback and noting that this is a standard technique.

Hasty Briefsbeta