• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • 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
            • Get-prefixes
            • Vex-0f3a-execute
            • Vex-0f38-execute
            • Vex-0f-execute
            • Two-byte-opcode-execute
            • Second-three-byte-opcode-execute
            • One-byte-opcode-execute
            • First-three-byte-opcode-execute
            • Evex-0f3a-execute
            • Evex-0f38-execute
            • Evex-0f-execute
            • X86-fetch-decode-execute
            • Vex-decode-and-execute
            • Evex-decode-and-execute
            • X86-run
            • Implemented-opcodes
            • Three-byte-opcode-decode-and-execute
            • X86-run-halt-count
            • Two-byte-opcode-decode-and-execute
            • X86-run-steps
            • Opcode-maps
              • Cpuid
              • Opcode-maps-structures
                • Opcode
                  • Opcode-fix
                  • Make-opcode
                  • Opcode-p
                  • Opcode-equiv
                  • Change-opcode
                    • Opcode->superscripts
                    • Opcode->group
                    • Opcode->vex
                    • Opcode->r/m
                    • Opcode->reg
                    • Opcode->pfx
                    • Opcode->mode
                    • Opcode->feat
                    • Opcode->evex
                    • Opcode->rex
                    • Opcode->op
                    • Opcode->mod
                  • Inst
                  • Op/en-p
                  • Operands
                  • Inst-list-p
                  • Operand-type-p
                  • Strict-opcode-p
                  • Opcode-extension-group-p
                  • Superscripts-p
                  • Maybe-operands-p
                  • Exception-desc-p
                  • Count-avx-pfx-cases
                  • Mnemonic-p
                  • Maybe-3bits-p
                  • Op-pfx-p
                  • Maybe-vex-p
                  • Maybe-evex-p
                  • Fn-desc-p
                  • Op-mode-p
                  • Rex-p
                  • Mod-p
                  • Avx-pfx-well-formed-p
                  • Any-present-in
                  • Superscripts-fix
                  • Strict-opcode-fix
                  • Operand-type-fix
                  • Opcode-extension-group-fix
                  • Maybe-operands-fix
                  • Maybe-evex-fix
                  • Maybe-3bits-fix
                  • Keyword-list-fix
                  • Exception-desc-fix
                  • Rex-fix
                  • Op-pfx-fix
                  • Op-mode-fix
                  • Mod-fix
                  • Mnemonic-fix
                  • Maybe-vex-fix
                  • Fn-desc-fix
                  • Vex-p
                  • Evex-p
                • Implemented-opcodes
                • Chk-exc-fn
                • Filtering-instructions
                • Addressing-method-code-p
                • Operand-type-code-p
                • Eval-pre-map
              • X86-run-halt
              • X86-fetch-decode-execute-halt
              • X86-run-steps1
            • Physical-memory
            • Decoding-and-spec-utils
            • Instructions
            • 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
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Opcode

    Change-opcode

    Modifying constructor for opcode structures.

    Syntax
    (change-opcode x 
                   [:op <op>] 
                   [:mode <mode>] 
                   [:reg <reg>] 
                   [:mod <mod>] 
                   [:r/m <r/m>] 
                   [:pfx <pfx>] 
                   [:rex <rex>] 
                   [:vex <vex>] 
                   [:evex <evex>] 
                   [:feat <feat>] 
                   [:superscripts <superscripts>] 
                   [:group <group>]) 
    

    This is an often useful alternative to make-opcode.

    We construct a new opcode structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

    Definition

    This is an ordinary change- macro introduced by defprod.

    Macro: change-opcode

    (defmacro change-opcode (x &rest args)
      (std::change-aggregate 'opcode
                             x args
                             '((:op . opcode->op)
                               (:mode . opcode->mode)
                               (:reg . opcode->reg)
                               (:mod . opcode->mod)
                               (:r/m . opcode->r/m)
                               (:pfx . opcode->pfx)
                               (:rex . opcode->rex)
                               (:vex . opcode->vex)
                               (:evex . opcode->evex)
                               (:feat . opcode->feat)
                               (:superscripts . opcode->superscripts)
                               (:group . opcode->group))
                             'change-opcode
                             'remake-opcode))