		Search-engine friendly clone of the ACL2 documentation.

Instr

Instr-kind

Get the kind (tag) of a instr structure.

Signature
(instr-kind x) → kind
Arguments: x — Guard (instrp x).

Definitions and Theorems

Function: instr-kind$inline

(defun instr-kind$inline (x)
  (declare (xargs :guard (instrp x)))
  (let ((__function__ 'instr-kind))
    (declare (ignorable __function__))
    (mbe :logic (cond ((or (atom x) (eq (car x) :op-imm))
                       :op-imm)
                      ((eq (car x) :op-imms32) :op-imms32)
                      ((eq (car x) :op-imms64) :op-imms64)
                      ((eq (car x) :op-imm-32) :op-imm-32)
                      ((eq (car x) :op-imms-32) :op-imms-32)
                      ((eq (car x) :lui) :lui)
                      ((eq (car x) :auipc) :auipc)
                      ((eq (car x) :op) :op)
                      ((eq (car x) :op-32) :op-32)
                      ((eq (car x) :jal) :jal)
                      ((eq (car x) :jalr) :jalr)
                      ((eq (car x) :branch) :branch)
                      ((eq (car x) :load) :load)
                      (t :store))
         :exec (car x))))

Theorem: instr-kind-possibilities

(defthm instr-kind-possibilities
  (or (equal (instr-kind x) :op-imm)
      (equal (instr-kind x) :op-imms32)
      (equal (instr-kind x) :op-imms64)
      (equal (instr-kind x) :op-imm-32)
      (equal (instr-kind x) :op-imms-32)
      (equal (instr-kind x) :lui)
      (equal (instr-kind x) :auipc)
      (equal (instr-kind x) :op)
      (equal (instr-kind x) :op-32)
      (equal (instr-kind x) :jal)
      (equal (instr-kind x) :jalr)
      (equal (instr-kind x) :branch)
      (equal (instr-kind x) :load)
      (equal (instr-kind x) :store))
  :rule-classes
  ((:forward-chaining :trigger-terms ((instr-kind x)))))