Skip to content

Fix AMD64 lifter bugs found by instruction test suite#124

Merged
endeav0r merged 21 commits into
masterfrom
worktree-lifter-tests
Mar 13, 2026
Merged

Fix AMD64 lifter bugs found by instruction test suite#124
endeav0r merged 21 commits into
masterfrom
worktree-lifter-tests

Conversation

@endeav0r

Copy link
Copy Markdown
Member

Summary

This PR adds a comprehensive AMD64 instruction test suite (217 tests across 90 files) and begins fixing the bugs it found. The test suite asserts correct behavior per the AMD64 manual, not Falcon's current implementation — so some tests are expected to fail until the corresponding bugs are fixed.

Bug fixes included so far:

BT family (BTR/BTS dispatch swap + BTC logic error)*

  • BTR/BTS dispatch swap (translator.rs:105-106): X86_INS_BTR was dispatched to semantics.bts() and X86_INS_BTS to semantics.btr(). The semantic functions were correct, just called for the wrong instruction.
  • BTC logic error (semantics.rs:833-840): The bit-complement shifted the entire base right by offset, XOR'd with 1, then shifted back — destroying all bits below the target position. Fixed to use mask-based pattern: base ^ (1 << offset).

Test plan

  • All 8 BT/BTC/BTR/BTS tests pass
  • Remaining test failures are tracked and will be fixed in follow-up commits

🤖 Generated with Claude Code

endeavor and others added 2 commits March 12, 2026 20:08
Add per-instruction test files for every implemented x86/AMD64 handler
in the translator, organized under lib/translator/x86/tests/. Tests
assert correct behavior per the AMD64 Architecture Programmer's Manual
— 170 pass and 47 fail, revealing existing lifter bugs including the
BTR/BTS handler swap, INC/DEC CF modification, SAHF operand issues,
and various arithmetic/SSE flag computation errors.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Two bugs in the x86 bit-test instruction family:

1. BTR/BTS dispatch swap (translator.rs): X86_INS_BTR was dispatched to
   semantics.bts() and vice versa. The semantic functions themselves were
   correct, just called for the wrong instruction.

2. BTC logic error (semantics.rs): The bit-complement operation shifted the
   entire base right by offset, XOR'd with 1, then shifted back. This
   destroys all bits below the target offset position. Fixed to use the
   same mask-based pattern as BTR/BTS: base ^ (1 << offset).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Bug #1: BT* Family — BTR/BTS Dispatch Swap + BTC Logic Error

Bug 1a: BTR/BTS Dispatch Swap

In translator.rs:105-106, the dispatch table had BTR and BTS swapped:

// Before (WRONG)
X86_INS_BTR => semantics.bts(...)
X86_INS_BTS => semantics.btr(...)

The semantic functions themselves were correct — btr() computes base & ~(1 << offset) and bts() computes base | (1 << offset) — they were just called for the wrong instruction.

Bug 1b: BTC Logic Error — Destroys Bits Below Target Offset

In semantics.rs:833-840, the BTC implementation was:

temp = base >> offset          // shifts ENTIRE value right, losing lower bits
CF = truncate(temp, 1)
result = (temp ^ 1) << offset  // shift back, but lower bits are now zero

With base=0xFF00, offset=10:

  1. temp = 0xFF00 >> 10 = 0x3F — bits 8-9 (originally set) are lost
  2. result = (0x3F ^ 1) << 10 = 0x3E << 10 = 0xF800
  3. Correct per AMD64 manual: 0xFF00 ^ (1 << 10) = 0xFB00

Fixed to use the same mask-based pattern as BTR/BTS: base ^ (1 << offset), which flips only the target bit and preserves all others.

Two bugs in SAHF implementation:
1. shr operand order was reversed — shifted the constant by AX instead
   of AX by the constant
2. Read from AX bits 0/6/7 (AL) instead of AX bits 8/14/15 (AH)

SAHF loads SF, ZF, CF from the AH register per the AMD64 manual.
AH is bits [15:8] of AX, so CF=bit8, ZF=bit14, SF=bit15.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Bug #2: SAHF — Reading Flags from Wrong Byte of AX

What we're doing

Working through the AMD64 lifter bugs found by the instruction test suite, fixing them one at a time with detailed explanations.

What the bug was

SAHF (Store AH into Flags) loads SF, ZF, and CF from the AH register — bits [15:8] of AX. The implementation had two compounding errors:

1. Reversed shr operand order:

// Shifts the constant 6 right by the value of AX (nonsensical)
let zf = Expr::trun(1, Expr::shr(expr_const(6, 16), ax.clone())?)?;

2. Wrong bit positions (even if operand order were correct):

// Reads bit 0 of AX (AL bit 0) — should be bit 8 (AH bit 0)
let cf = Expr::trun(1, ax.clone())?;
// Would read AX bit 6 (AL bit 6) — should be bit 14 (AH bit 6)
let zf = Expr::trun(1, Expr::shr(ax.clone(), expr_const(6, 16))?)?;

The implementation was reading from AL (bits [7:0]) instead of AH (bits [15:8]).

How it was fixed

Shift AX right by the correct bit positions to extract AH's flag bits:

let cf = Expr::trun(1, Expr::shr(ax.clone(), expr_const(8, 16))?)?;   // AH bit 0 = AX bit 8
let zf = Expr::trun(1, Expr::shr(ax.clone(), expr_const(14, 16))?)?;  // AH bit 6 = AX bit 14
let sf = Expr::trun(1, Expr::shr(ax, expr_const(15, 16))?)?;          // AH bit 7 = AX bit 15

All 4 SAHF tests now pass.

The shared set_of helper used the subtraction overflow formula
(lhs ^ rhs) & (lhs ^ result) for ALL instructions. This is wrong
for addition — the correct addition formula is
~(lhs ^ rhs) & (lhs ^ result). Unified into a single set_of with
a subtract parameter and updated all 13 call sites. Also removed
set_cf from INC/DEC per AMD64 manual.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Fix: Systemic set_of Addition Overflow Bug

What we were doing

Auditing all instructions that set the overflow flag (OF) as part of fixing INC/DEC. INC and DEC were incorrectly modifying CF (carry flag), which the AMD64 manual says they should preserve. While fixing that, we discovered INC also produced wrong OF values — and traced it to a systemic bug in the shared set_of helper used by all arithmetic instructions.

What the expected behavior was

The x86 overflow flag (OF) detects signed overflow — when an arithmetic result's sign bit is wrong. The formula depends on the operation:

  • Addition overflows when same-sign operands produce a different-sign result (e.g., positive + positive = negative). Formula: ~(lhs ^ rhs) & (lhs ^ result)
  • Subtraction overflows when different-sign operands produce a result whose sign differs from lhs (e.g., negative - positive = positive). Formula: (lhs ^ rhs) & (lhs ^ result)

These differ only by a NOT on the first term.

Why it was wrong

The set_of helper (semantics.rs:87) used the subtraction formula (lhs ^ rhs) & (lhs ^ result) for ALL instructions — both addition and subtraction. This meant every addition-based instruction (ADD, ADC, INC, XADD) computed OF incorrectly.

Concrete proof with ADD 0x7FFFFFFFFFFFFFFF, 1 (should overflow: MAX_INT64 + 1):

  • Old (sub formula): (0x7F..FE) & (0xFF..FF) → MSB=0 → OF=0 ❌
  • New (add formula): ~(0x7F..FE) & (0xFF..FF) → MSB=1 → OF=1 ✅

And ADD 0xFFFFFFFFFFFFFFFF, 1 (no overflow: -1 + 1 = 0):

  • Old (sub formula): (0xFF..FE) & (0xFF..FF) → MSB=1 → OF=1 ❌
  • New (add formula): ~(0xFF..FE) & (0xFF..FF) → MSB=0 → OF=0 ✅

How we fixed it

  1. Unified set_of with a subtract: bool parameter. When subtract=false (addition), the formula NOTs the first XOR term. Removed the temporary set_of_add helper.

  2. Updated all 13 call sites:

    • false (addition): ADC, ADD, INC, XADD
    • true (subtraction): CMP, CMPSB, CMPXCHG, DEC, NEG, SBB, SCASB, SCASW, SUB
  3. Added OF edge-case tests for every instruction that sets the overflow flag — both positive-direction and negative-direction overflow where applicable:

    • ADD: negative overflow (neg+neg→pos) + near-boundary no-overflow
    • ADC: negative overflow
    • XADD: negative overflow
    • SUB: positive-direction overflow (pos−neg→neg)
    • SBB: positive-direction overflow
    • CMP: both overflow directions (had zero OF=1 coverage before)
    • CMPXCHG: signed overflow (had zero OF=1 coverage before)

Test results

All OF-related assertions pass for ADD, INC, DEC, SUB, CMP, NEG, SCASB. Remaining failures in ADC, XADD, SBB, CMPXCHG, CMPSB are pre-existing bugs unrelated to OF (CF calculation, value storage, etc.).

SBB built an expression tree sub(lhs, add(rhs, zext(CF))) and used
it directly for flag computation and operand store. When set_cf
overwrote CF (op 4), the subsequent operand_store (op 5) re-evaluated
the expression with the new CF value, producing a wrong result.
Fix: store in a temp scalar first, matching how SUB already works.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Fix: SBB Result Corruption from CF Clobbering

What we were doing

Fixing SBB (subtract with borrow), which had 3 failing tests where the stored result was wrong.

What the bug was

SBB builds an expression tree sub(lhs, add(rhs, zext(CF))) and embeds it directly into every block operation — never materializing it into a temp scalar. The block executes operations sequentially:

State: rax=0x1235, rbx=0x1234, CF=1
(Expected per AMD64 manual: rax = 0x1235 - 0x1234 - 1 = 0)

Op 1-3: ZF, SF, OF computed from expr → reads CF=1, expr evaluates to 0  ✓
Op 4:   CF := cmpltu(rax, expr) → evaluates expr with CF=1, gets 0 →
        cmpltu(0x1235, 0) = false → CF := 0      ← CF overwritten
Op 5:   rax := expr → re-evaluates with CF=0 now!
        sub(0x1235, add(0x1234, 0)) = 1           ← WRONG (should be 0)

The expression tree is re-evaluated at Op 5 with the new CF (0) instead of the input CF (1). The borrow is lost.

SUB and ADC don't have this bug because they store the result in a temp scalar first.

How we fixed it

Store the SBB result in a temp scalar before computing flags (matching how SUB already works). The expression is evaluated once with the correct CF input, and all subsequent operations reference the materialized temp value.

@endeav0r

Copy link
Copy Markdown
Member Author

Fix: SBB Result Corruption from CF Clobbering (more detail)

What we were doing

Fixing SBB (Subtract with Borrow). Per the AMD64 manual, SBB computes dest = dest - (src + CF). Three tests were failing because the stored result was wrong — off by exactly 1, as if the carry flag input was being ignored.

What the bug was

Falcon's IL works by building expression trees and adding assignment operations to a block. Operations in a block execute sequentially — each one evaluates its expression using the current state of all scalars, then writes the result.

The SBB translator built a single expression tree for the result:

expr = sub(scalar("rax"), add(scalar("rbx"), zext(64, scalar("CF"))))

This expression tree is not evaluated when it's constructed — it's a symbolic tree that references the scalar variables rax, rbx, and CF by name. It only gets evaluated later, when the executor processes each block operation. The same expression tree was embedded into every operation in the block:

Op 1: ZF := ... expr ...        // evaluates expr, reads CF from state
Op 2: SF := ... expr ...        // evaluates expr, reads CF from state
Op 3: OF := ... expr ...        // evaluates expr, reads CF from state
Op 4: CF := cmpltu(rax, expr)   // evaluates expr, reads CF from state, then WRITES to CF
Op 5: rax := expr               // evaluates expr, reads CF from state — but CF was overwritten!

The problem: Op 4 evaluates the expression (which reads the input CF), computes the new carry flag, and writes it back to the CF scalar. Then Op 5 evaluates the same expression tree — but when it reads scalar("CF"), it now gets the output CF from Op 4 instead of the input CF. Whenever the output CF differs from the input CF, the result stored in rax is wrong.

Concrete trace: SBB rax, rbx with rax=0x1235, rbx=0x1234, CF=1

Expected per AMD64 manual: rax = 0x1235 - (0x1234 + 1) = 0

Initial state: rax=0x1235, rbx=0x1234, CF=1

Op 1: ZF := ...
      Evaluates expr: sub(0x1235, add(0x1234, zext(64, 1)))
                     = sub(0x1235, 0x1235) = 0
      ZF := 1 ✓

Op 2-3: SF, OF computed similarly. All correct (CF is still 1).

Op 4: CF := cmpltu(rax, expr)
      Evaluates expr: sub(0x1235, add(0x1234, zext(64, 1))) = 0
      cmpltu(0x1235, 0) → false
      CF := 0                    ← CF scalar is now 0, was 1

Op 5: rax := expr
      Evaluates expr: sub(0x1235, add(0x1234, zext(64, CF)))
      But CF is now 0!
      = sub(0x1235, add(0x1234, 0))
      = sub(0x1235, 0x1234)
      = 1                        ← WRONG, should be 0
      rax := 1

The result is 1 instead of 0 because the expression tree re-read CF after it was overwritten.

Why SUB doesn't have this bug

SUB stores the subtraction result in a temp scalar as the first operation:

Op 1: temp0 := sub(rax, rbx)    // evaluated once, stored in temp0
Op 2: ZF := ... temp0 ...       // reads temp0 (a concrete value, no CF reference)
Op 3: SF := ... temp0 ...
Op 4: OF := ... temp0 ...
Op 5: CF := cmpltu(rax, temp0)  // overwrites CF, but nobody reads CF after this
Op 6: rax := temp0              // reads temp0, not an expression tree — immune to CF changes

Because temp0 is a scalar holding the already-computed value, it doesn't matter that CF gets overwritten in Op 5 — nothing re-evaluates an expression containing CF after that point.

How we fixed it

Changed SBB to match SUB's pattern: store the result in a temp scalar (self.temp(0, lhs.bits())) as the first block operation, then use that temp for all flag computations and the final store. The expression tree containing CF is evaluated exactly once, with the correct input CF value.

CF bug: after shl(lhs, count-1) the last-shifted-out bit sits at the
MSB, but trun(1) extracted the LSB. Added shr(cf, bits-1) to bring
the MSB down before truncating.

OF bug: used cmpeq(cf, MSB(result)) which gives OF=1 when equal.
Per AMD64 manual, OF = MSB(result) XOR CF, so OF=1 when they differ.
Changed cmpeq to xor.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Fix: SHL CF and OF Flag Computation

What we were doing

Fixing SHL (shift left), which had 2 failing tests: wrong CF in shl_to_zero and wrong OF in shl_by_one.

What the bug was

Two separate bugs in flag computation:

Bug 1 — CF extracts the wrong bit. Per the AMD64 manual, CF receives the last bit shifted out. For SHL dest, count, that's the original bit at position bits - count (i.e., the bit that ends up at the MSB after shifting left by count - 1).

The code correctly shifts lhs left by count - 1 to move the target bit to the MSB position. But then it calls trun(1, ...) to extract it — which takes bit 0 (the LSB), not bit 63 (the MSB).

SHL rax, 1 with rax = 0x8000000000000000
Expected: CF = bit 63 of original = 1

Code:  cf = shl(0x8000000000000000, 0) = 0x8000000000000000
       cf = trun(1, 0x8000000000000000)
          = bit 0 = 0                    ← WRONG (should be bit 63 = 1)

Bug 2 — OF uses equality instead of XOR. Per the AMD64 manual, for shift count == 1: OF = MSB(result) XOR CF. The code used cmpeq(cf, MSB(result)), which gives OF=1 when they're equal — the opposite of XOR.

SHL rax, 1 with rax = 0xC000000000000001
Result = 0x8000000000000002, CF = 1, MSB(result) = 1
Expected: OF = 1 XOR 1 = 0

Code:  of = cmpeq(1, 1) = 1             ← WRONG (XOR gives 0)

How we fixed it

  1. CF: Added shr(cf, bits - 1) after the left-shift to bring the MSB down to bit 0 before truncating. Now trun(1, shr(shl(lhs, count-1), 63)) correctly extracts the MSB.

  2. OF: Changed cmpeq to xor, matching the AMD64 manual formula OF = MSB(result) XOR CF.

SHLD: trun(64) extracted the low 64 bits of the 128-bit shifted value,
but the answer lives in the high 64 bits. Added shr(shifted, 64) before
truncating. Also fixed CF MSB-vs-LSB extraction (same bug as SHL).

SHRD: result extraction was correct (low 64 bits), but set_zf/set_sf
were called on the 128-bit value. SF checked bit 127 instead of bit 63
of the 64-bit result. Fixed by truncating to 64 bits before computing
flags.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Fix: SHLD/SHRD Result Extraction and Flag Computation

What we were doing

Fixing SHLD (double precision shift left) and SHRD (double precision shift right). Both instructions concatenate dest and src into a 128-bit temporary, shift it, then extract a 64-bit result. SHLD had completely wrong results; SHRD had correct results but wrong SF/ZF flags.

What the bug was

SHLD — extracting the wrong half of the 128-bit result.

SHLD concatenates [dest | src] into a 128-bit value (dest in high, src in low) and shifts left by count. The SHLD result is the upper 64 bits of the shifted value. But the code used trun(64, result) which extracts the lower 64 bits.

SHLD rax, rbx, 4
rax = 0x123456789ABCDEF0, rbx = 0xFEDCBA9876543210

tmp (128-bit) = 0x123456789ABCDEF0_FEDCBA9876543210
shifted = tmp << 4 = 0x23456789ABCDEF0F_EDCBA98765432100
                      ^^^^^^^^^^^^^^^^  ← answer (high 64)

trun(64, shifted) = 0xEDCBA98765432100  ← WRONG (took low 64)
Expected:           0x23456789ABCDEF0F  ← the high 64 bits

SHLD — CF extracts the wrong bit. Same MSB-vs-LSB bug as SHL: after shifting the 128-bit temp left by count-1, the last-shifted-out bit is at bit 127 (MSB), but trun(1, ...) extracted bit 0 (LSB).

SHRD — flags computed on 128-bit value instead of 64-bit result.

SHRD's result extraction was correct (trun(64) gives the right low 64 bits for a right shift). But set_zf and set_sf were called on the 128-bit shifted value. SF checked bit 127 (always 0 for a right shift) instead of bit 63 of the 64-bit result.

SHRD rax, rbx, 8
Result (128-bit) = 0x0000000000000000_AB00000000000000
                    bit 127 = 0         bit 63 = 1

set_sf on 128-bit → SF = 0     ← WRONG
set_sf on  64-bit → SF = 1     ← CORRECT

How we fixed it

  1. SHLD result: Added shr(shifted, 64) before trun(64, ...) to extract the high 64 bits.
  2. SHLD CF: Added shr(cf_shifted, 127) before trun(1, ...) to extract the MSB instead of LSB.
  3. Both SHLD and SHRD: Truncate to 64 bits first, then call set_zf/set_sf on the correctly-sized result.

The MUL instruction was using cmpeq(upper_half, 0) to set CF/OF, which
produces 1 when the upper half IS zero (no overflow) — the opposite of
correct. Per AMD64 manual, CF=OF=1 when the upper half of the result is
non-zero. Changed to cmpneq for all four widths (8/16/32/64-bit).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Fix: MUL CF/OF flags inverted

What we were doing: Testing the MUL (unsigned multiply) instruction with both small results (fitting in lower half) and overflow results (spilling into upper half RDX).

What the bug was: The MUL instruction sets CF=OF=1 when the upper half of the result is non-zero (indicating the result doesn't fit in the destination register alone). The implementation used cmpeq(upper_half, 0), which evaluates to 1 when the upper half IS zero — the exact opposite of correct behavior. This meant CF=OF=1 for small multiplies (no overflow) and CF=OF=0 for overflowing multiplies.

How we fixed it: Changed cmpeq to cmpneq for all four operand widths (8/16/32/64-bit). Now CF=OF=1 only when the upper half is non-zero, matching the AMD64 manual specification.

Tests fixed: mul_r64_small, mul_r64_overflow

@endeav0r

Copy link
Copy Markdown
Member Author

Fix: MUL CF/OF flags inverted (detailed)

What we were doing

Testing the MUL (unsigned multiply) instruction. Per the AMD64 Architecture Programmer's Manual Vol. 3, §3.3 (MUL):

"MUL performs an unsigned multiplication of the operand and the accumulator (rAX). If the upper half of the product is non-zero, CF and OF are set to 1; otherwise they are cleared to 0."

We tested two cases:

  1. Small multiply (mul_r64_small): RAX=5, RBX=3 → 128-bit product = 15. Fits entirely in RAX (RDX=0). Expected: CF=0, OF=0.
  2. Overflow multiply (mul_r64_overflow): RAX=0xFFFFFFFFFFFFFFFF, RBX=2 → 128-bit product = 0x1_FFFFFFFFFFFFFFFE. Upper half spills into RDX=1. Expected: CF=1, OF=1.

What the bug was

The implementation used Expr::cmpeq(rdx.get()?, expr_const(0, 64)) (and equivalently for 8/16/32-bit widths). This compares the upper half to zero and returns 1 when they are equal (i.e., when there is NO overflow). But CF/OF should be 1 when there IS overflow (upper half non-zero). The condition was logically inverted.

Concrete walkthrough for 64-bit case (line 2419 before fix):

OF = cmpeq(RDX, 0)
CF = OF
  • Small multiply (RAX=5 × RBX=3 = 15): RDX=0. cmpeq(0, 0) = 1 → CF=1, OF=1. But expected CF=0, OF=0. ❌
  • Overflow multiply (RAX=0xFFFF...FF × RBX=2): RDX=1. cmpeq(1, 0) = 0 → CF=0, OF=0. But expected CF=1, OF=1. ❌

The same inverted logic existed in all four operand-width cases (8-bit checks AH, 16-bit checks DX, 32-bit checks EDX, 64-bit checks RDX).

How we fixed it

Changed Expr::cmpeq to Expr::cmpneq in all four width cases. Now:

OF = cmpneq(RDX, 0)
CF = OF
  • Small multiply: RDX=0. cmpneq(0, 0) = 0 → CF=0, OF=0. ✅
  • Overflow multiply: RDX=1. cmpneq(1, 0) = 1 → CF=1, OF=1. ✅

Tests fixed: mul_r64_small, mul_r64_overflow

Two bugs: (1) Operands were zero-extended before multiplication instead
of sign-extended, producing wrong results for negative inputs. (2) OF/CF
checked if upper half != 0, but for signed multiply they should be set
when the full result != sign-extension of the lower half.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Fix: IMUL signed multiply — wrong extension and wrong flag computation

What we were doing

Testing the IMUL (signed multiply) instruction in one-operand form. Per the AMD64 Architecture Programmer's Manual Vol. 3, §3.3 (IMUL):

"IMUL performs a signed multiplication of the operand and the accumulator. [...] For one-operand form, the result is stored in rDX:rAX. If the upper half of the product is not the sign-extension of the lower half, CF and OF are set to 1; otherwise they are cleared."

We tested three cases:

  1. Small positive (imul_r64_one_operand_small_positive): RAX=7, RBX=3 → signed product = 21. Fits in RAX, RDX=0 (sign-extension of positive). Expected: CF=0, OF=0.
  2. Negative result (imul_r64_one_operand_negative_result): RAX=-3 (0xFFFFFFFFFFFFFFFD), RBX=4 → signed product = -12. In 128-bit signed: RDX=0xFFFFFFFFFFFFFFFF, RAX=0xFFFFFFFFFFFFFFF4. The upper half is the sign-extension of the lower half's sign bit, so the result fits in 64 bits. Expected: CF=0, OF=0.
  3. Two-operand simple (imul_r64_two_operand_simple): RAX=10, RBX=20 → RAX=200. Expected: no overflow.

What the bugs were

Bug 1: Zero-extension instead of sign-extension (line ~1718)

The code did:

Expr::mul(
    Expr::zext(bit_width, multiplicand)?,
    Expr::zext(bit_width, multiplier)?,
)?

IMUL is a signed multiply. Operands must be sign-extended to the double-width before multiplication, not zero-extended. With zero-extension, a negative 64-bit value like -3 (0xFFFFFFFFFFFFFFFD) becomes the large positive 128-bit value 0x0000000000000000FFFFFFFFFFFFFFFD, producing a completely wrong product.

Concrete example: RAX = -3 (0xFFFFFFFFFFFFFFFD), RBX = 4.

  • With zext: 128-bit operands are 0x0000_0000_0000_0000_FFFF_FFFF_FFFF_FFFD × 0x0000_0000_0000_0000_0000_0000_0000_0004 = 0x0000_0000_0000_0003_FFFF_FFFF_FFFF_FFF4. RDX = 0x3, RAX = 0xFFFFFFFFFFFFFFF4.
  • With sext (correct): 128-bit operands are 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFD × 0x0000_0000_0000_0000_0000_0000_0000_0004 = 0xFFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFFF_FFF4. RDX = 0xFFFFFFFFFFFFFFFF, RAX = 0xFFFFFFFFFFFFFFF4.

The test expected RDX=0xFFFFFFFFFFFFFFFF but got RDX=0x3.

Bug 2: Wrong OF/CF flag check (line ~1764)

The code checked:

OF = cmpneq(upper_half, 0)

This checks whether the upper half is non-zero. But for signed multiply, CF=OF=1 when the result doesn't fit in the lower half as a signed value. A negative result that fits (like -12) has an all-ones upper half — non-zero, but that's the correct sign-extension, NOT overflow.

Per the AMD64 manual, the correct check is whether the full double-width result equals the sign-extension of the lower half:

OF = cmpneq(full_result, sext(double_width, lower_half))

Concrete example: signed product = -12.

  • Full 128-bit result: 0xFFFFFFFFFFFFFFFF_FFFFFFFFFFFFFFF4
  • Lower 64 bits: 0xFFFFFFFFFFFFFFF4 (sign bit = 1)
  • Sign-extension of lower 64 bits to 128: 0xFFFFFFFFFFFFFFFF_FFFFFFFFFFFFFFF4
  • These are equal → OF=0, CF=0. ✅ (Result fits in 64-bit signed.)

With the old check: upper half = 0xFFFFFFFFFFFFFFFF ≠ 0 → OF=1. ❌

How we fixed it

  1. Changed Expr::zext to Expr::sext for both multiplicand and multiplier before the double-width multiplication.
  2. Changed the OF flag to cmpneq(full_result, sext(bit_width, trun(bit_width/2, full_result))) — comparing the full result against the sign-extension of its lower half.

Tests fixed: imul_r64_one_operand_small_positive, imul_r64_one_operand_negative_result, imul_r64_two_operand_simple

(1) Divisor zero-extended instead of sign-extended to 128-bit, wrong
for negative divisors. (2) Dividend low half read from EAX (32-bit)
instead of RAX (64-bit), corrupting the 128-bit dividend. (3) Result
truncated to 32 bits instead of 64 when storing quotient/remainder
back to RAX/RDX.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Fix: IDIV — three bugs in 64-bit signed division

What we were doing

Testing the IDIV (signed divide) instruction with a negative dividend. Per the AMD64 Architecture Programmer's Manual Vol. 3, §3.3 (IDIV):

"IDIV performs a signed division of the dividend by the divisor and stores the results in rAX (quotient) and rDX (remainder). The sign of the remainder is always the same as the sign of the dividend."

Test case (idiv_r64_negative_dividend):

  • RDX:RAX = -100 as 128-bit signed: RDX=0xFFFFFFFFFFFFFFFF, RAX=0xFFFFFFFFFFFFFF9C
  • RBX = 7
  • Expected: RAX = -14 (0xFFFFFFFFFFFFFFF2), RDX = -2 (0xFFFFFFFFFFFFFFFE)
  • Got: RAX = 0x92492484 (garbage)

What the bugs were

Bug 1: Divisor zero-extended instead of sign-extended (line 1578)

let divisor = Expr::zext(divisor.bits() * 2, divisor)?;  // BUG

IDIV performs signed division. The IL's divs operation interprets both operands as signed values of their bit width. If we zero-extend a negative 64-bit divisor to 128 bits, the MSB is 0, so divs treats it as a large positive number instead of the intended negative value.

Example: divisor = -7 (0xFFFFFFFFFFFFFFF9)

  • zext to 128: 0x00000000000000000000000000000000_FFFFFFFFFFFFFFF9 → interpreted as +18446744073709551609 by divs. Wrong.
  • sext to 128: 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF_FFFFFFFFFFFFFFF9 → interpreted as -7 by divs. Correct.

(This bug didn't affect our specific test since the divisor was 7 (positive), but it would produce wrong results for any negative divisor.)

Bug 2: Dividend assembled from EAX instead of RAX (line 1604)

Expr::zext(128, self.get_register(x86_reg::X86_REG_EAX)?.get()?)?  // BUG: EAX is 32-bit

For 64-bit IDIV, the 128-bit dividend is assembled as (RDX << 64) | RAX. But the code read EAX (the lower 32 bits of RAX) instead of RAX, so only 32 bits of the low half were included.

Concrete trace with RAX=0xFFFFFFFFFFFFFF9C, RDX=0xFFFFFFFFFFFFFFFF:

  • High half: zext(128, RDX) << 64 = 0xFFFFFFFFFFFFFFFF_0000000000000000
  • Low half (buggy): zext(128, EAX) = zext(128, 0xFFFFFF9C) = 0x00000000FFFFFF9C
  • Assembled dividend: 0xFFFFFFFFFFFFFFFF_00000000FFFFFF9C ← wrong, missing upper 32 bits of RAX

Should be:

  • Low half: zext(128, RAX) = zext(128, 0xFFFFFFFFFFFFFF9C) = 0x0000000000000000FFFFFFFFFFFFFF9C
  • Assembled dividend: 0xFFFFFFFFFFFFFFFF_FFFFFFFFFFFFFF9C = -100 ✅

Bug 3: Result truncated to 32 bits instead of 64 (lines 1641-1642)

128 => {
    rax.set(block, Expr::trun(32, quotient.into())?)?;  // BUG: should be 64
    rdx.set(block, Expr::trun(32, remainder.into())?)?;  // BUG: should be 64
}

Copy-paste from the 64-bit case (which stores to 32-bit EAX/EDX). The 128-bit case stores to 64-bit RAX/RDX, so the quotient and remainder must be truncated to 64 bits. With trun(32), any quotient with bits above 31 would be silently discarded.

How we fixed it

  1. Changed Expr::zext to Expr::sext for the divisor (line 1578)
  2. Changed X86_REG_EAX to X86_REG_RAX in the 128-bit dividend assembly (line 1604)
  3. Changed Expr::trun(32, ...) to Expr::trun(64, ...) for both quotient and remainder in the 128-bit result case (lines 1641-1642)

Tests fixed: idiv_r64_negative_dividend
No regressions: idiv_r64_positive, div_r64_simple, div_r64_with_upper_bits all still pass.

Two bugs: (1) src operand received its own original value instead of the
original dest value (exchange was not happening). Also required saving
original dest to a temp to avoid expression re-evaluation after dest is
overwritten. (2) CF used set_cf (subtraction formula) instead of the
addition carry formula cmpltu(result, lhs).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Fix: XADD — src gets wrong value + CF uses subtraction formula

What we were doing

Testing the XADD (Exchange and Add) instruction. Per the AMD64 Architecture Programmer's Manual Vol. 3, §3.3 (XADD):

"XADD exchanges the contents of the destination (first) and source (second) operands, then loads the sum of the two original values into the destination operand. The flags are set according to the result of the addition."

Semantically: temp = dest + src; src = original_dest; dest = temp.

Test case (xadd_rax_rbx_normal): RAX=0x10, RBX=0x20.

  • Expected: RAX = 0x30 (sum), RBX = 0x10 (original RAX)
  • Got: RAX = 0x30, RBX = 0x30

What the bugs were

Bug 1: src operand received the wrong value (line 4131)

The code stored rhs (the source operand's own original value) back into the source operand:

self.operand_store(block, &detail.operands[0], result.into())?;  // dest = sum ✅
self.operand_store(block, &detail.operands[1], rhs)?;            // src = rhs ❌

Per the manual, src should receive the original dest value (lhs), not its own value. But simply changing rhs to lhs isn't enough due to Falcon's expression re-evaluation semantics: lhs is an expression referencing the rax scalar, and by the time the second operand_store executes, the first store has already overwritten rax with the sum.

Concrete trace with RAX=0x10, RBX=0x20:

  1. operand_store(operands[0], result) → sets RAX = 0x30 (the sum)
  2. operand_store(operands[1], lhs)lhs is the expression rax → evaluates to 0x30 (already overwritten!) → sets RBX = 0x30

The fix saves the original dest to a temp scalar before any stores:

let original_dest = self.temp(1, lhs.bits());
block.assign(original_dest.clone(), lhs.clone());
// ... later ...
self.operand_store(block, &detail.operands[1], original_dest.into())?;

Now original_dest is a dedicated temp scalar that holds 0x10 and isn't affected when rax is overwritten.

Bug 2: CF used the subtraction formula (line 4127)

The code called self.set_cf(block, result, lhs), which computes cmpltu(lhs, result) — the borrow detection formula for subtraction. But XADD performs addition, so CF should use the addition carry formula cmpltu(result, lhs) (result wrapped below lhs).

Example: RAX=0x10, RBX=0x20, sum=0x30.

  • Subtraction formula: cmpltu(0x10, 0x30) = true → CF=1. Wrong (no carry in 0x10+0x20).
  • Addition formula: cmpltu(0x30, 0x10) = false → CF=0. Correct.

Changed to inline Expression::cmpltu(result, lhs) matching how ADD computes CF.

How we fixed it

  1. Save original dest value to self.temp(1, ...) before any operand stores
  2. Store original_dest (not rhs or lhs) into the source operand
  3. Replace self.set_cf(block, result, lhs) with Expression::cmpltu(result, lhs) for addition CF

Tests fixed: xadd_rax_rbx_normal, xadd_rax_rbx_signed_overflow, xadd_rax_rbx_negative_overflow
No regressions: xadd_rax_rbx_zero_result still passes.

Flags were computed from operand[0] - operand[1] instead of
accumulator - operand[0] per AMD64 manual. Also saves comparison
operands to temps in head block before conditional paths can modify
them (expression re-evaluation bug).

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Fix: CMPXCHG — flags computed from wrong operands

What we were doing

Testing the CMPXCHG (Compare and Exchange) instruction. Per the AMD64 Architecture Programmer's Manual Vol. 3, §3.3 (CMPXCHG):

"Compares the value in the rAX register with the first operand (destination operand). If the two values are equal, the second operand (source operand) is loaded into the destination operand. Otherwise, the destination operand is loaded into the rAX register. The status flags are set according to the result of the compare operation (the subtraction of the first operand from rAX)."

The key phrase: flags come from rAX - first_operand.

Test case (cmpxchg_not_equal): cmpxchg rbx, rcx with RAX=1, RBX=5, RCX=0xAAAA...

  • CMP is: RAX - RBX = 1 - 5 = 0xFFFFFFFFFFFFFFFC
  • Expected: ZF=0 (not equal), SF=1 (MSB set), CF=1 (unsigned borrow: 1 < 5)
  • Got: SF=0, CF=0

What the bugs were

Bug 1: Flags computed from the wrong subtraction (line 1393)

The tail block computed:

let result = Expr::sub(lhs.clone(), rhs.clone())?;  // operand[0] - operand[1]

Where lhs = operand[0] (RBX, the destination) and rhs = operand[1] (RCX, the source). This computes RBX - RCX = 5 - 0xAAAA..., which produces completely different flags than the correct RAX - RBX = 1 - 5.

Concrete walkthrough:

  • Buggy: RBX - RCX = 5 - 0xAAAAAAAAAAAAAAAA = 0x5555555555555555_5B. Result MSB=0 → SF=0. 5 < 0xAAAA → CF should be 1 but set_cf(result, lhs=RBX) computes cmpltu(RBX, result) = cmpltu(5, 0x5555...5B) = true → CF=1. Hmm, actually CF=1 here by accident, but with different values the whole computation is wrong.
  • Correct: RAX - RBX = 1 - 5 = 0xFFFFFFFFFFFFFFFC. MSB=1 → SF=1. cmpltu(RAX, result) = cmpltu(1, 0xFFFF...FC) = true → CF=1.

Bug 2: Expression re-evaluation after conditional paths (lines 1390-1396)

Even if we fixed the subtraction to use dest.get()? - lhs (RAX - operand[0]), it would still be wrong due to Falcon's expression re-evaluation semantics. The tail block executes after the conditional paths which modify registers:

  • Taken path (RAX == RBX): operand[0] (RBX) gets overwritten with RCX. So lhs (which references the rbx scalar) now evaluates to RCX's value.
  • Not-taken path (RAX != RBX): RAX gets overwritten with RBX. So dest.get()? now evaluates to RBX's value (not the original RAX).

In either case, by the time the tail block computes the subtraction, the register values have changed.

How we fixed it

Saved the comparison operands to temp scalars in the head block before branching:

// In head block:
let cmp_lhs = self.temp(0, lhs.bits());  // will hold original RAX
let cmp_rhs = self.temp(1, lhs.bits());  // will hold original operand[0]
block.assign(cmp_lhs.clone(), dest.get()?);
block.assign(cmp_rhs.clone(), lhs.clone());

// In tail block:
let result = Expr::sub(cmp_lhs.clone().into(), cmp_rhs.clone().into())?;
self.set_sf(block, result.clone())?;
self.set_of(block, result.clone(), cmp_lhs.clone().into(), cmp_rhs.into(), true)?;
self.set_cf(block, result, cmp_lhs.into())?;

Temp scalars are dedicated storage that isn't affected by the register modifications in the conditional paths, so the flags are computed from the correct original values.

Tests fixed: cmpxchg_not_equal (SF, CF), cmpxchg_signed_overflow (CF)
No regressions: cmpxchg_equal still passes.

…alar

operand_load creates Scalar::temp(instruction.address, operand.size * 8) for
memory operands. For CMPSB, both operands are 8-bit memory loads at the same
instruction address, so both calls produce an identical scalar name. The second
load overwrites the first, making sub(temp, temp) always 0 and ZF always 1.

Fix: save the first operand_load result to a distinct self.temp(0, ...) scalar
before calling operand_load for the second operand.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Bug 10: CMPSB — shared temp scalar in operand_load

Root cause: operand_load (mode.rs:141-144) creates Scalar::temp(instruction.address, operand.size * 8) for memory operands. For CMPSB, both operands are 8-bit memory loads at the same instruction address, so both calls produce an identical scalar name. The second load overwrites the first, and the subtraction sub(temp, temp) always evaluates to 0, making ZF always 1.

Fix: Save the first operand_load result to a distinct self.temp(0, ...) scalar before calling operand_load for the second operand. self.temp(N, bits) produces names like "temp_0x{addr}_{N}" which don't collide with operand_load's "temp_0x{addr}".

Tests fixed (4): cmpsb_equal, cmpsb_src_greater, cmpsb_src_less, cmpsb_df_set

Commit: 2767d1c

LODSD loads a dword (4 bytes), so RSI should be adjusted by 4 per the
AMD64 manual. The code was using expr_const(1, ...) in both the increment
and decrement blocks, matching LODSB's byte-sized adjustment instead of
LODSD's dword-sized adjustment.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Bug 11: LODSD — RSI adjusted by 1 instead of 4

Root cause: lodsd (semantics.rs:2052,2063) uses expr_const(1, ...) for both the increment and decrement of RSI. LODSD loads a dword (4 bytes), so RSI should be adjusted by 4 per the AMD64 manual. The code was copy-pasted from lodsb where the byte-sized adjustment of 1 is correct.

Fix: Change expr_const(1, self.mode().bits()) to expr_const(4, self.mode().bits()) in both the inc and dec blocks.

Tests fixed (2): lodsd_df_clear, lodsd_df_set
(2 other tests already passed: lodsd_zero_extends_rax, lodsd_memory_unchanged)

Commit: c5890ee

set_cf computes CF = cmpltu(lhs, result) for subtraction. SCASW computes
AX - [RDI], so lhs is AX. The code was passing temp ([RDI] value) instead
of ax.get()?, causing CF to be computed from the wrong operand. The sibling
scasb function correctly passes al.get()?.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Bug 12: SCASW — set_cf passed RHS instead of LHS

Root cause: scasw (semantics.rs:3596) passes temp.into() (the memory operand, i.e. [RDI]) to set_cf as the lhs argument. But set_cf computes CF = cmpltu(lhs, result) for subtraction borrow detection, and the LHS of AX - [RDI] is AX, not [RDI]. The sibling scasb correctly passes al.get()?.

Fix: Change self.set_cf(block, expr, temp.into())? to self.set_cf(block, expr, ax.get()?)?.

Tests fixed (1): scasw_signed_overflow
(4 other tests already passed: scasw_match, scasw_no_match, scasw_df_set, scasw_rax_unchanged)

Commit: 067be7e

The CF computation used cmpltu(result, lhs), which detects carry from
lhs+rhs but misses carry from the subsequent +CF step. For example,
0 + 0xFFFFFFFFFFFFFFFF + 1 = 0: lhs+rhs=0xFFFFFFFFFFFFFFFF (no carry),
then +1 wraps to 0 (carry). The single check sees cmpltu(0, 0) = false.

Fix: compute the intermediate sum (lhs+rhs) in a temp, then detect carry
from each step independently: carry1 = cmpltu(lhs+rhs, lhs),
carry2 = cmpltu(result, lhs+rhs), CF = carry1 | carry2.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Bug 13: ADC — single cmpltu misses carry when both addition steps wrap

Root cause: adc (semantics.rs:459-462) computes CF = cmpltu(result, lhs). This detects carry from lhs + rhs but misses carry from the subsequent + CF step. For example, 0 + 0xFFFFFFFFFFFFFFFF + 1 = 0 (mod 2^64): the first addition lhs+rhs = 0xFFFFFFFFFFFFFFFF doesn't carry, but adding CF=1 wraps to 0, which should set CF=1. The single check sees cmpltu(0, 0) = false and incorrectly reports CF=0.

Fix: Compute the intermediate sum lhs+rhs in a temp scalar, then detect carry from each step independently:

  • carry1 = cmpltu(lhs+rhs, lhs) — carry from first addition
  • carry2 = cmpltu(result, lhs+rhs) — carry from adding CF
  • CF = carry1 | carry2

Tests fixed (1): adc_zero_result_with_carry_in
(3 other tests already passed: adc_normal_cf_clear, adc_signed_overflow_via_carry, adc_negative_overflow)

Commit: b4f2e69

endeavor and others added 4 commits March 12, 2026 23:25
The 128-bit codepath for both PADDQ and PSUBQ had three bugs:
1. shr/shl operand order was reversed (e.g. shr(64, lhs) instead of shr(lhs, 64))
2. Upper qword addition/subtraction used lhs for both operands instead of lhs and rhs
3. PSUBQ used sub(mask, ...) instead of and(mask, ...) to isolate the lower qword

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
The loop computing per-byte subtractions used self.temp(0, 8) for every
iteration, so each assignment overwrote the previous. The reconstruction
loop then read the same scalar 16 times, producing a result where every
byte equaled the last byte's subtraction.

Fix: use self.temp(i + 2, 8) to give each byte lane its own temp scalar.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Each block.assign overwrote the temp scalar with just the shifted dword,
discarding previously placed dwords. Only the last dword (result3 << 96)
survived.

Fix: OR each shifted dword with the accumulated temp value.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
PSLLDQ and PSRLDQ take a byte count as the immediate operand, but the
code passed this directly to shl/shr which operate on bits. This caused
e.g. "shift left by 4 bytes" to shift by only 4 bits instead of 32 bits.

Fix: multiply the byte count by 8 (shl by 3) before passing to the
bit-level shift operation. Also removed a duplicate zext check in PSLLDQ.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r

Copy link
Copy Markdown
Member Author

Bugs 14-17: SSE instruction fixes

Bug 14: PADDQ/PSUBQ — swapped operands and wrong register in 128-bit path

Root cause: The 128-bit codepath for both PADDQ and PSUBQ had three bugs:

  1. shr/shl operand order was reversed (e.g. shr(64, lhs) instead of shr(lhs, 64))
  2. Upper qword addition/subtraction used lhs for both operands instead of lhs and rhs
  3. PSUBQ used sub(mask, ...) instead of and(mask, ...) to isolate the lower qword

Tests fixed (4): paddq_basic, paddq_wrapping, psubq_basic, psubq_wrapping

Commit: 3cc1cb1


Bug 15: PSUBB — all byte lanes share the same temp scalar

Root cause: The loop computing per-byte subtractions used self.temp(0, 8) for every iteration. Each assignment overwrote the previous, so the reconstruction loop read the same (last byte's) value 16 times.

Fix: Use self.temp(i + 2, 8) to give each byte lane its own temp scalar.

Tests fixed (1): psubb_basic
(1 other test already passed: psubb_wrapping)

Commit: bbfa704


Bug 16: PSHUFD — dword results overwritten instead of ORed together

Root cause: Each block.assign(temp, shl(resultN, ...)) overwrote temp with just the shifted dword, discarding previously placed dwords. Only the last dword survived.

Fix: OR each shifted dword with the accumulated temp value.

Tests fixed (2): pshufd_reverse, pshufd_broadcast_low

Commit: 4440c8f


Bug 17: PSLLDQ/PSRLDQ — shift amount is bytes, not bits

Root cause: PSLLDQ and PSRLDQ take a byte count as the immediate, but the code passed it directly to shl/shr which operate on bits. "Shift left by 4 bytes" shifted by 4 bits instead of 32.

Fix: Multiply the byte count by 8 (shl by 3) before passing to the bit-level shift.

Tests fixed (4): pslldq_shift_4_bytes, pslldq_shift_8_bytes, psrldq_shift_4_bytes, psrldq_shift_8_bytes

Commit: 9651b09

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@endeav0r
endeav0r merged commit 11d115b into master Mar 13, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant