		Search-engine friendly clone of the ACL2 documentation.

Instr

Instrp

Recognizer for instr structures.

Signature
(instrp x) → *

Definitions and Theorems

Function: instrp

(defun instrp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'instrp))
    (declare (ignorable __function__))
    (and (consp x)
         (cond ((or (atom x) (eq (car x) :op-imm))
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((funct (std::da-nth 0 (cdr x)))
                          (rd (std::da-nth 1 (cdr x)))
                          (rs1 (std::da-nth 2 (cdr x)))
                          (imm (std::da-nth 3 (cdr x))))
                       (and (op-imm-funct-p funct)
                            (ubyte5p rd)
                            (ubyte5p rs1)
                            (ubyte12p imm)))))
               ((eq (car x) :op-imms32)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((funct (std::da-nth 0 (cdr x)))
                          (rd (std::da-nth 1 (cdr x)))
                          (rs1 (std::da-nth 2 (cdr x)))
                          (imm (std::da-nth 3 (cdr x))))
                       (and (op-imms-funct-p funct)
                            (ubyte5p rd)
                            (ubyte5p rs1)
                            (ubyte5p imm)))))
               ((eq (car x) :op-imms64)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((funct (std::da-nth 0 (cdr x)))
                          (rd (std::da-nth 1 (cdr x)))
                          (rs1 (std::da-nth 2 (cdr x)))
                          (imm (std::da-nth 3 (cdr x))))
                       (and (op-imms-funct-p funct)
                            (ubyte5p rd)
                            (ubyte5p rs1)
                            (ubyte6p imm)))))
               ((eq (car x) :op-imm-32)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((funct (std::da-nth 0 (cdr x)))
                          (rd (std::da-nth 1 (cdr x)))
                          (rs1 (std::da-nth 2 (cdr x)))
                          (imm (std::da-nth 3 (cdr x))))
                       (and (op-imm-32-funct-p funct)
                            (ubyte5p rd)
                            (ubyte5p rs1)
                            (ubyte12p imm)))))
               ((eq (car x) :op-imms-32)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((funct (std::da-nth 0 (cdr x)))
                          (rd (std::da-nth 1 (cdr x)))
                          (rs1 (std::da-nth 2 (cdr x)))
                          (imm (std::da-nth 3 (cdr x))))
                       (and (op-imms-32-funct-p funct)
                            (ubyte5p rd)
                            (ubyte5p rs1)
                            (ubyte5p imm)))))
               ((eq (car x) :lui)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 2)
                     (b* ((rd (std::da-nth 0 (cdr x)))
                          (imm (std::da-nth 1 (cdr x))))
                       (and (ubyte5p rd) (ubyte20p imm)))))
               ((eq (car x) :auipc)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 2)
                     (b* ((rd (std::da-nth 0 (cdr x)))
                          (imm (std::da-nth 1 (cdr x))))
                       (and (ubyte5p rd) (ubyte20p imm)))))
               ((eq (car x) :op)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((funct (std::da-nth 0 (cdr x)))
                          (rd (std::da-nth 1 (cdr x)))
                          (rs1 (std::da-nth 2 (cdr x)))
                          (rs2 (std::da-nth 3 (cdr x))))
                       (and (op-funct-p funct)
                            (ubyte5p rd)
                            (ubyte5p rs1)
                            (ubyte5p rs2)))))
               ((eq (car x) :op-32)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((funct (std::da-nth 0 (cdr x)))
                          (rd (std::da-nth 1 (cdr x)))
                          (rs1 (std::da-nth 2 (cdr x)))
                          (rs2 (std::da-nth 3 (cdr x))))
                       (and (op-32-funct-p funct)
                            (ubyte5p rd)
                            (ubyte5p rs1)
                            (ubyte5p rs2)))))
               ((eq (car x) :jal)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 2)
                     (b* ((rd (std::da-nth 0 (cdr x)))
                          (imm (std::da-nth 1 (cdr x))))
                       (and (ubyte5p rd) (ubyte20p imm)))))
               ((eq (car x) :jalr)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 3)
                     (b* ((rd (std::da-nth 0 (cdr x)))
                          (rs1 (std::da-nth 1 (cdr x)))
                          (imm (std::da-nth 2 (cdr x))))
                       (and (ubyte5p rd)
                            (ubyte5p rs1)
                            (ubyte12p imm)))))
               ((eq (car x) :branch)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((funct (std::da-nth 0 (cdr x)))
                          (rs1 (std::da-nth 1 (cdr x)))
                          (rs2 (std::da-nth 2 (cdr x)))
                          (imm (std::da-nth 3 (cdr x))))
                       (and (branch-funct-p funct)
                            (ubyte5p rs1)
                            (ubyte5p rs2)
                            (ubyte12p imm)))))
               ((eq (car x) :load)
                (and (true-listp (cdr x))
                     (eql (len (cdr x)) 4)
                     (b* ((funct (std::da-nth 0 (cdr x)))
                          (rd (std::da-nth 1 (cdr x)))
                          (rs1 (std::da-nth 2 (cdr x)))
                          (imm (std::da-nth 3 (cdr x))))
                       (and (load-funct-p funct)
                            (ubyte5p rd)
                            (ubyte5p rs1)
                            (ubyte12p imm)))))
               (t (and (eq (car x) :store)
                       (and (true-listp (cdr x))
                            (eql (len (cdr x)) 4))
                       (b* ((funct (std::da-nth 0 (cdr x)))
                            (rs1 (std::da-nth 1 (cdr x)))
                            (rs2 (std::da-nth 2 (cdr x)))
                            (imm (std::da-nth 3 (cdr x))))
                         (and (store-funct-p funct)
                              (ubyte5p rs1)
                              (ubyte5p rs2)
                              (ubyte12p imm)))))))))

Theorem: consp-when-instrp

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