Instruction-semantic-functions
Instruction Semantic Functions
The instruction semantic functions have dual roles:
- They fetch the instruction's operands, as dictated by the decoded
components of the instruction (like the prefixes, SIB byte, etc.)
provided as input; these decoded components are provided by our x86
decoder function x86-fetch-decode-execute.
- They contain or act as the functional specification of the
instructions. For example, the functional specification function of
the ADD instruction returns two values: the appropriately truncated
sum of the operands and the modified flags. We do not deal with the
x86 state in these specifications.
Each semantic function takes, among other arguments, the value
start-rip of the instruction pointer at the beginning of the
instruction, and the value temp-rip of the instruction pointer
after the decoding of the prefixes, REX byte, opcode, ModR/M byte, and
SIB byte (some of these bytes may not be present). The semantic
function may further increment the instruction pointer beyond
temp-rip to read the ending bytes of the instruction, e.g. to
read a displacement or an immediate. The semantic function eventually
writes the final value of the instruction pointer into RIP.
Subtopics
- Sar-spec
- Specification for the SAR instruction
- Shr-spec
- Specification for the SHR instruction
- Sal/shl-spec
- Specification for the SAL/SHL instruction
- Rol-spec
- Specification for the ROL instruction
- Ror-spec
- Specification for the ROR instruction
- Rcl-spec
- Specification for the RCL instruction
- Rcr-spec
- Specification for the RCR instruction
- Simd-sub-spec
- Specification for the SIMD subtraction instructions.
- Simd-add-spec
- Specification for the SIMD addition instructions.
- Imul-spec
- Specification for the IMUL (unsigned imultiply) instruction
- Mul-spec
- Specification for the MUL (unsigned multiply) instruction
- Idiv-spec
- Specification for the IDIV (unsigned idivide) instruction
- Div-spec
- Specification for the DIV (unsigned divide) instruction
- Shrd-spec
- Specification for the SHRD instruction.
- Shld-spec
- Specification for the SHLD instruction.
- Gpr-arith/logic-spec
- Semantics of general-purpose arithmetic and logical instructions
- Shrx-spec
- Specification for the SHRX instruction.
- Shlx-spec
- Specification for the SHLX instruction.
- Sarx-spec
- Specification for the SARX instruction.
- Floating-point-specifications
- Misc. utilities for the specification of floating-point operations
