• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Pfcs
    • Wp-gen
    • Dimacs-reader
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Taspi
    • Riscv
      • Specification
      • Executable
        • Decoding-left-inverse
        • Decoding-executable
          • Decodex
          • Get-fields-rtype
          • Get-fields-stype
          • Get-fields-itype
          • Get-fields-btype
          • Get-imm-jtype
          • Get-imm-btype
          • Get-imm-utype
          • Get-fields-utype
          • Get-imm-stype
          • Get-imm-itype
          • Get-fields-jtype
          • Get-rs2
          • Get-rs1
          • Get-rd
          • Get-opcode
          • Get-funct7
          • Get-funct3
        • Decoding-right-inverse
        • Execution-executable
        • Decoding-correct
      • Specialized
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Decoding-executable

Decodex

Executable instruction decoder.

Signature

(decodex enc feat) → instr?

Arguments

enc — Guard (ubyte32p enc).

feat — Guard (featp feat).

Returns

instr? — Type (instr-optionp instr?).

The x in the name stands for `executable'.

The first input is a 32-bit encoding of the instruction; the second input consists of the features, which affect decoding. If decoding is successful, we return the instruction. If decoding is unsuccessful, we return nil.

The values of the encoded fields, which we write in binary notation, are taken from the instruction listings in [ISA:35].

We retrieve the opcode, and we dispatch based on it. Each dispatch first retrieves the fields, based on the format, and then checks them to see whether they are valid, and to determine which instruction is encoded, if any.

With the OP-IMM opcode, shift instructions are encoded in a specialization of the I-type format, where the low 5 or 6 bits of the immediate are the shift amount, while the high 7 or 6 bits need to have specific values. Whether the immediate is split into 5 low bits and 7 high bits, or into 6 low bits and 6 high bits, depends on whether we are in RV32I or RV64I mode, so we use the features passed as input to this function. We generate slightly different shift instructions, in the two cases.

With the OP-IMM-32 opcode, shift instructions are encoded in a specialization of the I-type format, where the low 5 bits of the immediate are the shift amount, while the high 7 bits need to have specific values.

Definitions and Theorems

Function: decodex

(defun decodex (enc feat)
 (declare (xargs :guard (and (ubyte32p enc) (featp feat))))
 (let ((__function__ 'decodex))
  (declare (ignorable __function__))
  (b* ((enc (ubyte32-fix enc)))
   (case (get-opcode enc)
    (3 (b* (((mv funct3 rd rs1 imm)
             (get-fields-itype enc))
            ((unless (or (not (feat-embedp feat))
                         (and (ubyte4p rd) (ubyte4p rs1))))
             nil)
            (funct (case funct3
                     (0 (load-funct-lb))
                     (1 (load-funct-lh))
                     (2 (load-funct-lw))
                     (3 (if (feat-64p feat)
                            (load-funct-ld)
                          nil))
                     (4 (load-funct-lbu))
                     (5 (load-funct-lhu))
                     (6 (if (feat-64p feat)
                            (load-funct-lwu)
                          nil))
                     (7 nil)))
            ((unless funct) nil))
         (instr-load funct rd rs1 imm)))
    (19 (b* (((mv funct3 rd rs1 imm)
              (get-fields-itype enc))
             ((unless (or (not (feat-embedp feat))
                          (and (ubyte4p rd) (ubyte4p rs1))))
              nil)
             (funct (case funct3
                      (0 (op-imm-funct-addi))
                      (1 nil)
                      (2 (op-imm-funct-slti))
                      (3 (op-imm-funct-sltiu))
                      (4 (op-imm-funct-xori))
                      (5 nil)
                      (6 (op-imm-funct-ori))
                      (7 (op-imm-funct-andi))))
             ((when funct)
              (instr-op-imm funct rd rs1 imm)))
          (if (feat-64p feat)
              (b* ((loimm (part-select imm :low 0 :high 5))
                   (hiimm (part-select imm :low 6 :high 11))
                   ((when (= funct3 1))
                    (if (= hiimm 0)
                        (instr-op-imms64 (op-imms-funct-slli)
                                         rd rs1 loimm)
                      nil)))
                (case hiimm
                  (0 (instr-op-imms64 (op-imms-funct-srli)
                                      rd rs1 loimm))
                  (16 (instr-op-imms64 (op-imms-funct-srai)
                                       rd rs1 loimm))
                  (t nil)))
            (b* ((loimm (part-select imm :low 0 :high 4))
                 (hiimm (part-select imm :low 5 :high 11))
                 ((when (= funct3 1))
                  (if (= hiimm 0)
                      (instr-op-imms32 (op-imms-funct-slli)
                                       rd rs1 loimm)
                    nil)))
              (case hiimm
                (0 (instr-op-imms32 (op-imms-funct-srli)
                                    rd rs1 loimm))
                (32 (instr-op-imms32 (op-imms-funct-srai)
                                     rd rs1 loimm))
                (t nil))))))
    (23 (b* (((mv rd imm) (get-fields-utype enc))
             ((unless (or (not (feat-embedp feat))
                          (ubyte4p rd)))
              nil))
          (instr-auipc rd imm)))
    (27 (b* (((unless (feat-64p feat)) nil)
             ((mv funct3 rd rs1 imm)
              (get-fields-itype enc))
             ((unless (or (not (feat-embedp feat))
                          (and (ubyte4p rd) (ubyte4p rs1))))
              nil)
             ((when (= funct3 0))
              (instr-op-imm-32 (op-imm-32-funct-addiw)
                               rd rs1 imm))
             (loimm (part-select imm :low 0 :high 4))
             (hiimm (part-select imm :low 5 :high 11))
             ((when (= funct3 1))
              (if (= hiimm 0)
                  (instr-op-imms-32 (op-imms-32-funct-slliw)
                                    rd rs1 loimm)
                nil))
             ((when (= funct3 5))
              (case hiimm
                (0 (instr-op-imms-32 (op-imms-32-funct-srliw)
                                     rd rs1 loimm))
                (32 (instr-op-imms-32 (op-imms-32-funct-sraiw)
                                      rd rs1 loimm))
                (t nil))))
          nil))
    (35 (b* (((mv funct3 rs1 rs2 imm)
              (get-fields-stype enc))
             ((unless (or (not (feat-embedp feat))
                          (and (ubyte4p rs1) (ubyte4p rs2))))
              nil)
             (funct (case funct3
                      (0 (store-funct-sb))
                      (1 (store-funct-sh))
                      (2 (store-funct-sw))
                      (3 (if (feat-64p feat)
                             (store-funct-sd)
                           nil))
                      (t nil)))
             ((unless funct) nil))
          (instr-store funct rs1 rs2 imm)))
    (51
      (b* (((mv funct3 funct7 rd rs1 rs2)
            (get-fields-rtype enc))
           ((unless (or (not (feat-embedp feat))
                        (and (ubyte4p rd)
                             (ubyte4p rs1)
                             (ubyte4p rs2))))
            nil)
           (funct (case funct3
                    (0 (case funct7
                         (0 (op-funct-add))
                         (1 (if (feat-mp feat) (op-funct-mul) nil))
                         (32 (op-funct-sub))
                         (t nil)))
                    (1 (case funct7
                         (0 (op-funct-sll))
                         (1 (if (feat-mp feat) (op-funct-mulh) nil))
                         (t nil)))
                    (2 (case funct7
                         (0 (op-funct-slt))
                         (1 (if (feat-mp feat)
                                (op-funct-mulhsu)
                              nil))
                         (t nil)))
                    (3 (case funct7
                         (0 (op-funct-sltu))
                         (1 (if (feat-mp feat)
                                (op-funct-mulhu)
                              nil))
                         (t nil)))
                    (4 (case funct7
                         (0 (op-funct-xor))
                         (1 (if (feat-mp feat) (op-funct-div) nil))
                         (t nil)))
                    (5 (case funct7
                         (0 (op-funct-srl))
                         (1 (if (feat-mp feat) (op-funct-divu) nil))
                         (32 (op-funct-sra))
                         (t nil)))
                    (6 (case funct7
                         (0 (op-funct-or))
                         (1 (if (feat-mp feat) (op-funct-rem) nil))
                         (t nil)))
                    (7 (case funct7
                         (0 (op-funct-and))
                         (1 (if (feat-mp feat) (op-funct-remu) nil))
                         (t nil)))))
           ((unless funct) nil))
        (instr-op funct rd rs1 rs2)))
    (55 (b* (((mv rd imm) (get-fields-utype enc))
             ((unless (or (not (feat-embedp feat))
                          (ubyte4p rd)))
              nil))
          (instr-lui rd imm)))
    (59 (b* (((unless (feat-64p feat)) nil)
             ((mv funct3 funct7 rd rs1 rs2)
              (get-fields-rtype enc))
             ((unless (or (not (feat-embedp feat))
                          (and (ubyte4p rd)
                               (ubyte4p rs1)
                               (ubyte4p rs2))))
              nil)
             (funct (case funct3
                      (0 (case funct7
                           (0 (op-32-funct-addw))
                           (1 (if (feat-mp feat)
                                  (op-32-funct-mulw)
                                nil))
                           (32 (op-32-funct-subw))
                           (t nil)))
                      (1 (case funct7
                           (0 (op-32-funct-sllw))
                           (t nil)))
                      (2 nil)
                      (3 nil)
                      (4 (case funct7
                           (1 (if (feat-mp feat)
                                  (op-32-funct-divw)
                                nil))
                           (t nil)))
                      (5 (case funct7
                           (0 (op-32-funct-srlw))
                           (1 (if (feat-mp feat)
                                  (op-32-funct-divuw)
                                nil))
                           (32 (op-32-funct-sraw))
                           (t nil)))
                      (6 (case funct7
                           (1 (if (feat-mp feat)
                                  (op-32-funct-remw)
                                nil))
                           (t nil)))
                      (7 (case funct7
                           (1 (if (feat-mp feat)
                                  (op-32-funct-remuw)
                                nil))
                           (t nil)))))
             ((unless funct) nil))
          (instr-op-32 funct rd rs1 rs2)))
    (99 (b* (((mv funct3 rs1 rs2 imm)
              (get-fields-btype enc))
             ((unless (or (not (feat-embedp feat))
                          (and (ubyte4p rs1) (ubyte4p rs2))))
              nil)
             (funct (case funct3
                      (0 (branch-funct-beq))
                      (1 (branch-funct-bne))
                      (2 nil)
                      (3 nil)
                      (4 (branch-funct-blt))
                      (5 (branch-funct-bge))
                      (6 (branch-funct-bltu))
                      (7 (branch-funct-bgeu))))
             ((unless funct) nil))
          (instr-branch funct rs1 rs2 imm)))
    (103 (b* (((mv funct3 rd rs1 imm)
               (get-fields-itype enc))
              ((unless (or (not (feat-embedp feat))
                           (and (ubyte4p rd) (ubyte4p rs1))))
               nil)
              ((unless (= funct3 0)) nil))
           (instr-jalr rd rs1 imm)))
    (111 (b* (((mv rd imm) (get-fields-jtype enc))
              ((unless (or (not (feat-embedp feat))
                           (ubyte4p rd)))
               nil))
           (instr-jal rd imm)))
    (t nil)))))

Theorem: instr-optionp-of-decodex

(defthm instr-optionp-of-decodex
  (b* ((instr? (decodex enc feat)))
    (instr-optionp instr?))
  :rule-classes :rewrite)

Theorem: instr-validp-of-decodex

(defthm instr-validp-of-decodex
  (b* ((?instr? (decodex enc feat)))
    (implies instr? (instr-validp instr? feat))))

Theorem: decodex-of-ubyte32-fix-enc

(defthm decodex-of-ubyte32-fix-enc
  (equal (decodex (ubyte32-fix enc) feat)
         (decodex enc feat)))

Theorem: decodex-ubyte32-equiv-congruence-on-enc

(defthm decodex-ubyte32-equiv-congruence-on-enc
  (implies (acl2::ubyte32-equiv enc enc-equiv)
           (equal (decodex enc feat)
                  (decodex enc-equiv feat)))
  :rule-classes :congruence)

Theorem: decodex-of-feat-fix-feat

(defthm decodex-of-feat-fix-feat
  (equal (decodex enc (feat-fix feat))
         (decodex enc feat)))

Theorem: decodex-feat-equiv-congruence-on-feat

(defthm decodex-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (decodex enc feat)
                  (decodex enc feat-equiv)))
  :rule-classes :congruence)