		Search-engine friendly clone of the ACL2 documentation.

Opcode

Make-opcode

Basic constructor macro for opcode structures.

Syntax

(make-opcode [: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 the usual way to construct opcode structures. It simply conses together a structure with the specified fields.

This macro generates a new opcode structure from scratch. See also change-opcode, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-opcode

(defmacro make-opcode (&rest args)
  (std::make-aggregate 'opcode
                       args
                       '((:op quote 0)
                         (:mode quote nil)
                         (:reg quote nil)
                         (:mod quote nil)
                         (:r/m quote nil)
                         (:pfx quote nil)
                         (:rex quote nil)
                         (:vex quote nil)
                         (:evex quote nil)
                         (:feat quote nil)
                         (:superscripts quote nil)
                         (:group quote nil))
                       'make-opcode
                       nil))

Function: opcode

(defun opcode (op mode reg mod r/m pfx
                  rex vex evex feat superscripts group)
 (declare (xargs :guard (and (24bits-p op)
                             (op-mode-p mode)
                             (maybe-3bits-p reg)
                             (mod-p mod)
                             (maybe-3bits-p r/m)
                             (op-pfx-p pfx)
                             (rex-p rex)
                             (maybe-vex-p vex)
                             (maybe-evex-p evex)
                             (symbol-listp feat)
                             (superscripts-p superscripts)
                             (opcode-extension-group-p group))))
 (declare (xargs :guard t))
 (let ((__function__ 'opcode))
  (declare (ignorable __function__))
  (b* ((op (mbe :logic (24bits-fix op) :exec op))
       (mode (mbe :logic (op-mode-fix mode)
                  :exec mode))
       (reg (mbe :logic (maybe-3bits-fix reg)
                 :exec reg))
       (mod (mbe :logic (mod-fix mod) :exec mod))
       (r/m (mbe :logic (maybe-3bits-fix r/m)
                 :exec r/m))
       (pfx (mbe :logic (op-pfx-fix pfx) :exec pfx))
       (rex (mbe :logic (rex-fix rex) :exec rex))
       (vex (mbe :logic (maybe-vex-fix vex)
                 :exec vex))
       (evex (mbe :logic (maybe-evex-fix evex)
                  :exec evex))
       (feat (mbe :logic (acl2::symbol-list-fix feat)
                  :exec feat))
       (superscripts (mbe :logic (superscripts-fix superscripts)
                          :exec superscripts))
       (group (mbe :logic (opcode-extension-group-fix group)
                   :exec group)))
   (std::prod-cons
      (std::prod-cons (std::prod-cons op (std::prod-cons mode reg))
                      (std::prod-cons mod (std::prod-cons r/m pfx)))
      (std::prod-cons
           (std::prod-cons rex (std::prod-cons vex evex))
           (std::prod-cons feat
                           (std::prod-cons superscripts group)))))))