		Search-engine friendly clone of the ACL2 documentation.

Instruction

Instructionp

Recognizer for instruction structures.

Signature
(instructionp x) → *

Definitions and Theorems

Function: instructionp

(defun instructionp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'instructionp))
    (declare (ignorable __function__))
    (and (consp x)
         (cond ((or (atom x) (eq (car x) :unary))
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 3)
                     (b* ((op (std::da-nth 0 (cdr x)))
                          (arg (std::da-nth 1 (cdr x)))
                          (into (std::da-nth 2 (cdr x))))
                       (and (unary-opp op)
                            (operandp arg)
                            (registerp into)))))
               ((eq (car x) :binary)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((op (std::da-nth 0 (cdr x)))
                          (arg1 (std::da-nth 1 (cdr x)))
                          (arg2 (std::da-nth 2 (cdr x)))
                          (into (std::da-nth 3 (cdr x))))
                       (and (binary-opp op)
                            (operandp arg1)
                            (operandp arg2)
                            (registerp into)))))
               ((eq (car x) :ternary)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 5)
                     (b* ((op (std::da-nth 0 (cdr x)))
                          (arg1 (std::da-nth 1 (cdr x)))
                          (arg2 (std::da-nth 2 (cdr x)))
                          (arg3 (std::da-nth 3 (cdr x)))
                          (into (std::da-nth 4 (cdr x))))
                       (and (ternary-opp op)
                            (operandp arg1)
                            (operandp arg2)
                            (operandp arg3)
                            (registerp into)))))
               ((eq (car x) :equal)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((op (std::da-nth 0 (cdr x)))
                          (arg1 (std::da-nth 1 (cdr x)))
                          (arg2 (std::da-nth 2 (cdr x)))
                          (into (std::da-nth 3 (cdr x))))
                       (and (equal-opp op)
                            (operandp arg1)
                            (operandp arg2)
                            (registerp into)))))
               ((eq (car x) :assert)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 3)
                     (b* ((op (std::da-nth 0 (cdr x)))
                          (arg1 (std::da-nth 1 (cdr x)))
                          (arg2 (std::da-nth 2 (cdr x))))
                       (and (assert-opp op)
                            (operandp arg1)
                            (operandp arg2)))))
               ((eq (car x) :commit)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((op (std::da-nth 0 (cdr x)))
                          (arg1 (std::da-nth 1 (cdr x)))
                          (arg2 (std::da-nth 2 (cdr x)))
                          (into (std::da-nth 3 (cdr x))))
                       (and (commit-opp op)
                            (operandp arg1)
                            (operandp arg2)
                            (registerp into)))))
               ((eq (car x) :hash)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 3)
                     (b* ((op (std::da-nth 0 (cdr x)))
                          (arg (std::da-nth 1 (cdr x)))
                          (into (std::da-nth 2 (cdr x))))
                       (and (hash-opp op)
                            (operandp arg)
                            (registerp into)))))
               ((eq (car x) :cast)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 3)
                     (b* ((args (std::da-nth 0 (cdr x)))
                          (into (std::da-nth 1 (cdr x)))
                          (as (std::da-nth 2 (cdr x))))
                       (and (operand-listp args)
                            (registerp into)
                            (register-typep as)))))
               (t (and (eq (car x) :call)
                       (and (true-listp (cdr x))
                            (eql (len (cdr x)) 3))
                       (b* ((ref (std::da-nth 0 (cdr x)))
                            (args (std::da-nth 1 (cdr x)))
                            (into (std::da-nth 2 (cdr x))))
                         (and (referencep ref)
                              (operand-listp args)
                              (registerp into)))))))))

Theorem: consp-when-instructionp

(defthm consp-when-instructionp
  (implies (instructionp x) (consp x))
  :rule-classes :compound-recognizer)