		Search-engine friendly clone of the ACL2 documentation.

Create-inst-doc

Signature
(create-inst-doc inst &key (fn-ok? 't) (arg-ok? 'nil)) → inst-doc-string
Arguments: inst — Guard (inst-p inst).; fn-ok? — Include information about the semantic function in the documentation or not.
Guard (booleanp fn-ok?).; arg-ok? — Include information about the operands (inst.operands field) in the documentation or not.
Guard (booleanp arg-ok?).
Returns: inst-doc-string — Type (stringp inst-doc-string).

Definitions and Theorems

Function: symbol-list-to-string

(defun symbol-list-to-string (lst)
  (declare (xargs :guard (symbol-listp lst)))
  (let ((__function__ 'symbol-list-to-string))
    (declare (ignorable __function__))
    (if (atom lst)
        ""
      (if (eql (len lst) 1)
          (str::cat ":" (symbol-name (car lst)))
        (str::cat ":" (symbol-name (car lst))
                  " "
                  (symbol-list-to-string (cdr lst)))))))

Theorem: stringp-of-symbol-list-to-string

(defthm stringp-of-symbol-list-to-string
  (implies (and (symbol-listp lst))
           (b* ((newstr (symbol-list-to-string lst)))
             (stringp newstr)))
  :rule-classes :rewrite)

Function: create-extra-info-doc-string

(defun create-extra-info-doc-string (info text)
 (declare (xargs :guard (stringp text)))
 (let ((__function__ 'create-extra-info-doc-string))
  (declare (ignorable __function__))
  (if info
   (let*
    ((info-string
      (cond
           ((symbolp info)
            (str::cat ":" (symbol-name info)))
           ((symbol-listp info)
            (symbol-list-to-string info))
           (t (str::pretty info
                           :config *x86isa-printconfig-base-10*)))))
    (str::cat "<tr><td> @('"
              text "') </td>" "<td> @('"
              info-string "') </td> </tr>"))
   "")))

Theorem: stringp-of-create-extra-info-doc-string

(defthm stringp-of-create-extra-info-doc-string
  (implies (and (stringp text))
           (b* ((doc (create-extra-info-doc-string info text)))
             (stringp doc)))
  :rule-classes :rewrite)

Function: create-extra-info-doc

(defun create-extra-info-doc (opcode)
 (declare (xargs :guard (strict-opcode-p opcode)))
 (let ((__function__ 'create-extra-info-doc))
   (declare (ignorable __function__))
   (b*
     (((opcode opcode))
      (feat-doc (create-extra-info-doc-string opcode.feat ":FEAT "))
      (vex-doc (create-extra-info-doc-string opcode.vex ":VEX "))
      (evex-doc (create-extra-info-doc-string opcode.evex ":EVEX "))
      (pfx-doc (create-extra-info-doc-string opcode.pfx ":PFX "))
      (mode-doc (create-extra-info-doc-string opcode.mode ":MODE "))
      (reg-doc (create-extra-info-doc-string opcode.reg ":REG "))
      (mod-doc (create-extra-info-doc-string opcode.mod ":MOD "))
      (r/m-doc (create-extra-info-doc-string opcode.r/m ":R/M "))
      (rex-doc (create-extra-info-doc-string opcode.rex ":REX "))
      (extra-info (str::cat "<table>" mode-doc
                            pfx-doc reg-doc mod-doc r/m-doc rex-doc
                            vex-doc evex-doc feat-doc "</table>")))
     extra-info)))

Theorem: stringp-of-create-extra-info-doc

(defthm stringp-of-create-extra-info-doc
  (implies (and (strict-opcode-p opcode))
           (b* ((doc (create-extra-info-doc opcode)))
             (stringp doc)))
  :rule-classes :rewrite)

Function: get-addressing-method-doc

(defun get-addressing-method-doc (code)
  (declare (xargs :guard (addressing-method-code-p code)))
  (let ((__function__ 'get-addressing-method-doc))
    (declare (ignorable __function__))
    (b* ((alst (cdr (assoc-equal code *z-addressing-method-info*)))
         (doc (cdr (assoc-equal :doc alst)))
         ((unless doc) ""))
      doc)))

Theorem: stringp-of-get-addressing-method-doc

(defthm stringp-of-get-addressing-method-doc
  (b* ((str (get-addressing-method-doc code)))
    (stringp str))
  :rule-classes :rewrite)

Function: gen-addressing-method-code-doc

(defun gen-addressing-method-code-doc (z-info)
 (declare (xargs :guard (alistp z-info)))
 (let ((__function__ 'gen-addressing-method-code-doc))
  (declare (ignorable __function__))
  (if (endp z-info)
      nil
    (b*
     ((code (caar z-info))
      ((unless (addressing-method-code-p code))
       (er hard? __function__
           "~% Bad code ~x0 encountered! ~%" code))
      (codestr (str::pretty code
                            :config *x86isa-printconfig-base-10*))
      (docstr (str::cat "@(' " codestr "'): "
                        (get-addressing-method-doc code)))
      (topic-name (intern$ (str::cat codestr "-Z-ADDRESSING-METHOD")
                           "X86ISA"))
      (form (cons (cons 'defxdoc
                        (cons topic-name
                              (cons ':long (cons docstr 'nil))))
                  'nil))
      (rest (gen-addressing-method-code-doc (cdr z-info))))
     (append form rest)))))

Function: get-operand-type-code-doc

(defun get-operand-type-code-doc (code)
  (declare (xargs :guard (operand-type-code-p code)))
  (let ((__function__ 'get-operand-type-code-doc))
    (declare (ignorable __function__))
    (b* ((alst (cdr (assoc-equal code *operand-type-code-info*)))
         (doc (cdr (assoc-equal :doc alst)))
         ((unless doc) ""))
      doc)))

Theorem: stringp-of-get-operand-type-code-doc

(defthm stringp-of-get-operand-type-code-doc
  (b* ((str (get-operand-type-code-doc code)))
    (stringp str))
  :rule-classes :rewrite)

Function: gen-operand-type-code-doc

(defun gen-operand-type-code-doc (info)
 (declare (xargs :guard (alistp info)))
 (let ((__function__ 'gen-operand-type-code-doc))
  (declare (ignorable __function__))
  (if (endp info)
      nil
   (b*
    ((code (caar info))
     ((unless (operand-type-code-p code))
      (er hard? __function__
          "~% Bad code ~x0 encountered! ~%" code))
     (codestr
       (str::pretty code
                    :config *x86isa-printconfig-base-10-lowercase*))
     (docstr (str::cat "@(' " codestr "'): "
                       (get-operand-type-code-doc code)))
     (topic-name
      (intern$
        (str::upcase-string (str::cat codestr "-OPERAND-TYPE-CODE"))
        "X86ISA"))
     (form (cons (cons 'defxdoc
                       (cons topic-name
                             (cons ':long (cons docstr 'nil))))
                 'nil))
     (rest (gen-operand-type-code-doc (cdr info))))
    (append form rest)))))

Function: create-arg-doc

(defun create-arg-doc (x)
 (declare (xargs :guard (operand-type-p x)))
 (let ((__function__ 'create-arg-doc))
  (declare (ignorable __function__))
  (cond
   ((atom x) " ")
   ((eql (len x) 1)
    (b*
      ((possible-code (nth 0 x))
       (codestr (str::pretty possible-code
                             :config *x86isa-printconfig-base-10*))
       (topic-name (str::cat codestr "-Z-ADDRESSING-METHOD")))
      (if (addressing-method-code-p possible-code)
          (str::cat "[<a href=\"index.html?topic=X86ISA____"
                    topic-name "\">" codestr "</a>] ")
        (str::cat "[@('" codestr "')] "))))
   ((eql (len x) 2)
    (b*
     ((addressing-mode (nth 0 x))
      (addressing-mode-str
           (str::pretty addressing-mode
                        :config *x86isa-printconfig-base-10*))
      (addressing-mode-topic-name (str::cat addressing-mode-str
                                            "-Z-ADDRESSING-METHOD"))
      (operand-code (nth 1 x))
      (operand-code-str
       (str::pretty operand-code
                    :config *x86isa-printconfig-base-10-lowercase*))
      (operand-code-topic-name
           (str::upcase-string (str::cat operand-code-str
                                         "-OPERAND-TYPE-CODE"))))
     (str::cat "[<a href=\"index.html?topic=X86ISA____"
               addressing-mode-topic-name
               "\">" addressing-mode-str
               "</a> - <a href=\"index.html?topic=X86ISA____"
               operand-code-topic-name
               "\">" operand-code-str "</a>] ")))
   (t " "))))

Theorem: stringp-of-create-arg-doc

(defthm stringp-of-create-arg-doc
  (b* ((xstr (create-arg-doc x)))
    (stringp xstr))
  :rule-classes :rewrite)

Function: create-args-doc

(defun create-args-doc (operands)
  (declare (xargs :guard (maybe-operands-p operands)))
  (let ((__function__ 'create-args-doc))
    (declare (ignorable __function__))
    (b* (((unless operands) "<td> </td>")
         ((operands operands))
         (op1 (create-arg-doc operands.op1))
         ((if (eql operands.op2 nil))
          (str::cat "<td> " op1 " </td>"))
         (op2 (create-arg-doc operands.op2))
         ((if (eql operands.op3 nil))
          (str::cat "<td> " op1 ", " op2 " </td>"))
         (op3 (create-arg-doc operands.op3))
         ((if (eql operands.op4 nil))
          (str::cat "<td> " op1 ", " op2 ", " op3 " </td>"))
         (op4 (create-arg-doc operands.op4)))
      (str::cat "<td> " op1
                ", " op2 ", " op3 ", " op4 " </td>"))))

Theorem: stringp-of-create-args-doc

(defthm stringp-of-create-args-doc
  (b* ((docstr (create-args-doc operands)))
    (stringp docstr))
  :rule-classes :rewrite)

Theorem: inst-p-implies-mnemonic-p

(defthm inst-p-implies-mnemonic-p
  (implies (inst-p x)
           (mnemonic-p (inst->mnemonic x)))
  :rule-classes :forward-chaining)

Theorem: inst-p-implies-mnemonic-p-alt

(defthm inst-p-implies-mnemonic-p-alt
  (implies (and (inst-p x)
                (not (stringp (inst->mnemonic x))))
           (symbolp (inst->mnemonic x))))

Theorem: inst-p-implies-consp-fn

(defthm inst-p-implies-consp-fn
  (implies (and (inst-p x) (inst->fn x))
           (consp (inst->fn x))))

Function: create-inst-doc-fn

(defun create-inst-doc-fn (inst fn-ok? arg-ok?)
 (declare (xargs :guard (and (inst-p inst)
                             (booleanp fn-ok?)
                             (booleanp arg-ok?))))
 (let ((__function__ 'create-inst-doc))
  (declare (ignorable __function__))
  (b*
   (((inst inst))
    (opcode inst.opcode)
    ((opcode opcode))
    (opcode-byte (loghead 8 opcode.op))
    (mnemonic (if (stringp inst.mnemonic)
                  inst.mnemonic
                (symbol-name inst.mnemonic)))
    (fn-info
     (if
      (and fn-ok? inst.fn)
      (if (eql (car inst.fn) :no-instruction)
          "@('NO INSTRUCTION')"
       (concatenate
         'string
         "@(tsee "
         (str::pretty (car inst.fn)
                      :config *x86isa-printconfig*)
         ") "
         (if (cdr inst.fn)
             (concatenate 'string
                          "-- <br/><tt>"
                          (str::pretty (cdr inst.fn)
                                       :config *x86isa-printconfig*)
                          "</tt>")
           "")))
      ""))
    (fn-info (if fn-ok? (concatenate 'string
                                     " <td> " fn-info " </td> ")
               ""))
    (extra-info (create-extra-info-doc opcode))
    (arg-str (if arg-ok? (create-args-doc inst.operands)
               ""))
    (doc-string
         (concatenate 'string
                      "<tr> " " <td> "
                      (subseq (str::hexify-width opcode-byte 2)
                              3 nil)
                      " </td> " " <td> "
                      mnemonic " </td> " " <td> " extra-info
                      " </td> " arg-str fn-info "</tr>")))
   doc-string)))

Theorem: stringp-of-create-inst-doc

(defthm stringp-of-create-inst-doc
  (b* ((inst-doc-string (create-inst-doc-fn inst fn-ok? arg-ok?)))
    (stringp inst-doc-string))
  :rule-classes :rewrite)