libLISA - Automated CPU Instruction Discovery and Analysis

libLISA's automatically-inferred semantics can be used to verify the correctness of other implementations. In our 2024 paper, we verified the correctness of Dasgupta et al.'s semantics implemented in the K framework. In the table below, you will find an overview of all bugs that we have found.

ToolBug description
Dasgupta et al.Incorrect bit offset for BT/BTS/BTR/BTC with memory operand

Incorrect bit offset for BT/BTS/BTR/BTC with memory operand

In all bit test variants (BT/BTS/BTR/BTC) on memory with a register bit offset, the bit offset is computed incorrectly. The bit offset is converted to a byte offset by shifting right by 3, then zero-extending the result to 64 bits. It should be sign-extended, to preserve the sign bits of negative offsets.

Dasgupta et al.CMPS performs comparison incorrectly

CMPS performs comparison incorrectly

The CMPS variants perform a comparison by setting flags according to Mem2 - Mem1, but they should be set according to Mem1 - Mem2.

Dasgupta et al.OF incorrect for RCLB/RCRB

OF incorrect for RCLB/RCRB

The overflow flag (OF) of RCLB/RCRB is undefined when the masked rotate count is not 0 or 1. However, Dasgupta et al. specifies the OF as undefined when the masked rotate count modulo the operand size + 1 is not 0 or 1.

Dasgupta et al.vmpsadbw_xmm_xmm_m128_imm8 writes to wrong destination

vmpsadbw_xmm_xmm_m128_imm8 writes to wrong destination

The VMPSADBW instruction incorrectly writes to the source operand (R3) instead of destination operand (R4).

Dasgupta et al.Crash when MULX is executed with identical destination registers

Crash when MULX is executed with identical destination registers

The MULX instructions write a result to two destination operands. The destination operands can be equal. Dasgupta et al.'s semantics have not taken this possibility into account, causing the K prover to crash when MULX with equal destination operands is executed.

Dasgupta et al.XCHGL is disassembled incorrectly

XCHGL is disassembled incorrectly

The instruction XCHGL EAX, EAX can be encoded as both 87C0 and 90. The second encoding has the semantics of NOP (do nothing), while the first has the semantics of XCHGL (set the upper 32 bits of RAX to zero). objdump, the disassembler used by Dasgupta et al. incorrectly disassembles 90 with a REX prefix as XCHGL instead of NOP."

This bug has since been fixed in binutils. Please note that older versions of Ubuntu ship old versions of binutils that still contain this bug. You will need a version newer than Ubuntu 22.04.