• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Wp-gen
      • Dimacs-reader
      • Pfcs
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Bitcoin
      • Riscv
      • Des
      • Ethereum
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
          • Instructions
            • Two-byte-opcodes
            • One-byte-opcodes
              • X86-sal/sar/shl/shr/rcl/rcr/rol/ror
              • X86-add/adc/sub/sbb/or/and/xor/cmp-test-e-i
              • X86-far-jmp-op/en-d
              • X86-add/xadd/adc/sub/sbb/or/and/xor/cmp/test-e-g
              • X86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i
              • X86-add/adc/sub/sbb/or/and/xor/cmp-g-e
              • X86-push-segment-register
              • X86-pusha
              • X86-shld/shrd
              • X86-mov-op/en-oi
              • X86-inc/dec-4x
              • X86-cmps
              • X86-xchg
              • X86-popa
              • X86-one-byte-jcc
              • X86-movs
              • X86-push-general-register
              • X86-idiv
              • X86-div
              • X86-pop-general-register
              • X86-ret
              • X86-push-i
              • X86-pop-ev
              • X86-imul-op/en-rmi
              • X86-push-ev
              • X86-mul
              • X86-imul-op/en-m
              • X86-stos
              • X86-not/neg-f6-f7
              • X86-call-ff/2-op/en-m
              • X86-iret
              • X86-inc/dec-fe-ff
              • X86-mov-op/en-rm
              • X86-mov-op/en-mr
              • X86-near-jmp-op/en-m
              • X86-mov-op/en-mi
              • X86-loop
              • X86-out
              • X86-call-e8-op/en-m
              • X86-movsxd
              • X86-mov-op/en-fd
              • X86-cmc/clc/stc/cld/std
              • X86-near-jmp-op/en-d
              • X86-mov-op/en-td
              • X86-popf
              • X86-lea
              • X86-jrcxz
              • X86-cbw/cwd/cdqe
              • X86-pushf
              • X86-leave
              • X86-lahf
              • X86-sahf
              • X86-cwd/cdq/cqo
              • X86-rdtsc
              • X86-sti
              • X86-int3
              • X86-hlt
              • X86-cli
            • Fp-opcodes
            • Instruction-semantic-functions
            • X86-illegal-instruction
            • Implemented-opcodes
            • Opcode-maps
            • X86-general-protection
            • X86-device-not-available
            • X86-step-unimplemented
            • Privileged-opcodes
            • Three-byte-opcodes
          • Register-readers-and-writers
          • X86-modes
          • Segmentation
          • Other-non-deterministic-computations
          • Environment
          • Paging
        • Implemented-opcodes
        • To-do
        • Proof-utilities
        • Peripherals
        • Model-validation
        • Modelcalls
        • Concrete-simulation-examples
        • Utils
        • Debugging-code-proofs
      • Sha-2
      • Yul
      • Zcash
      • Proof-checker-itp13
      • Regex
      • ACL2-programming-language
      • Json
      • Jfkr
      • Equational
      • Cryptography
      • Poseidon
      • Where-do-i-place-my-book
      • Axe
      • Bigmems
      • Builtins
      • Execloader
      • Aleo
      • Solidity
      • Paco
      • Concurrent-programs
      • Bls12-377-curves
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Instructions

One-byte-opcodes

Instruction semantic functions for Intel's instructions with a one-byte opcode

Subtopics

X86-sal/sar/shl/shr/rcl/rcr/rol/ror
X86-add/adc/sub/sbb/or/and/xor/cmp-test-e-i
Operand Fetch and Execute for ADD, ADC, SUB, SBB, OR, AND, XOR, CMP, TEST: Addressing Mode = (E, I)
X86-far-jmp-op/en-d
Absolute Indirect Jump: Far
X86-add/xadd/adc/sub/sbb/or/and/xor/cmp/test-e-g
Operand Fetch and Execute for ADD, ADC, SUB, SBB, OR, AND, XOR, CMP, TEST: Addressing Mode = (E, G)
X86-add/adc/sub/sbb/or/and/xor/cmp-test-rax-i
Operand Fetch and Execute for ADD, ADC, SUB, SBB, OR, AND, XOR, CMP, TEST: Addressing Mode = (rAX, I)
X86-add/adc/sub/sbb/or/and/xor/cmp-g-e
Operand Fetch and Execute for ADD, ADC, SUB, SBB, OR, AND, XOR, CMP: Addressing Mode = (G, E)
X86-push-segment-register
PUSH Segment Register
X86-pusha
PUSHA/PUSHAD: 60
X86-shld/shrd
Double-precision shift left or right.
X86-mov-op/en-oi
X86-inc/dec-4x
X86-cmps
X86-xchg
X86-popa
POPA/POPD: 61
X86-one-byte-jcc
X86-movs
X86-push-general-register
PUSH: 50+rw/rd
X86-idiv
X86-div
X86-pop-general-register
POP: 58+rw/rd
X86-ret
X86-push-i
PUSH: 6A/68 ib/iw/id
X86-pop-ev
POP: 8F/0 r/m
X86-imul-op/en-rmi
X86-push-ev
PUSH: FF /6 r/m
X86-mul
X86-imul-op/en-m
X86-stos
X86-not/neg-f6-f7
X86-call-ff/2-op/en-m
X86-iret
X86-inc/dec-fe-ff
X86-mov-op/en-rm
X86-mov-op/en-mr
X86-near-jmp-op/en-m
X86-mov-op/en-mi
X86-loop
X86-out
X86-call-e8-op/en-m
X86-movsxd
X86-mov-op/en-fd
X86-cmc/clc/stc/cld/std
X86-near-jmp-op/en-d
X86-mov-op/en-td
X86-popf
X86-lea
X86-jrcxz
X86-cbw/cwd/cdqe
X86-pushf
X86-leave
X86-lahf
X86-sahf
X86-cwd/cdq/cqo
X86-rdtsc
X86-sti
X86-int3
X86-hlt
X86-cli