• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
          • Rflag-specifications
          • Characterizing-undefined-behavior
          • Top-level-memory
          • App-view
          • X86-decoder
          • Physical-memory
          • Decoding-and-spec-utils
            • Read-operands-and-write-results
            • Effective-address-computations
            • Select-operand-size
            • Instruction-pointer-operations
            • Stack-pointer-operations
            • Select-segment-register
            • Prefix-modrm-sib-decoding
            • Select-address-size
            • Rex-byte-from-vex-prefixes
            • Check-instruction-length
            • Error-objects
            • Rip-guard-okp
            • Sib-decoding
              • Sib-structures
                • X86-decode-sib-p
            • Instructions
            • Register-readers-and-writers
            • X86-modes
            • Segmentation
            • Other-non-deterministic-computations
            • Environment
            • Paging
          • Implemented-opcodes
          • To-do
          • Proof-utilities
          • Peripherals
          • Model-validation
          • Modelcalls
          • Concrete-simulation-examples
          • Utils
          • Debugging-code-proofs
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Sib-decoding
    • Structures

    Sib-structures

    Bitstruct definitions to store a SIB byte and its fields.

    Definitions and Theorems

    Function: sib-p$inline

    (defun sib-p$inline (x)
      (declare (xargs :guard t))
      (mbe :logic (unsigned-byte-p 8 x)
           :exec (and (natp x) (< x 256))))

    Theorem: sib-p-when-unsigned-byte-p

    (defthm sib-p-when-unsigned-byte-p
      (implies (unsigned-byte-p 8 x)
               (sib-p x)))

    Theorem: unsigned-byte-p-when-sib-p

    (defthm unsigned-byte-p-when-sib-p
      (implies (sib-p x)
               (unsigned-byte-p 8 x)))

    Theorem: sib-p-compound-recognizer

    (defthm sib-p-compound-recognizer
      (implies (sib-p x) (natp x))
      :rule-classes :compound-recognizer)

    Function: sib-fix$inline

    (defun sib-fix$inline (x)
      (declare (xargs :guard (sib-p x)))
      (mbe :logic (loghead 8 x) :exec x))

    Theorem: sib-p-of-sib-fix

    (defthm sib-p-of-sib-fix
      (b* ((fty::fixed (sib-fix$inline x)))
        (sib-p fty::fixed))
      :rule-classes :rewrite)

    Theorem: sib-fix-when-sib-p

    (defthm sib-fix-when-sib-p
      (implies (sib-p x)
               (equal (sib-fix x) x)))

    Function: sib-equiv$inline

    (defun sib-equiv$inline (x y)
      (declare (xargs :guard (and (sib-p x) (sib-p y))))
      (equal (sib-fix x) (sib-fix y)))

    Theorem: sib-equiv-is-an-equivalence

    (defthm sib-equiv-is-an-equivalence
      (and (booleanp (sib-equiv x y))
           (sib-equiv x x)
           (implies (sib-equiv x y)
                    (sib-equiv y x))
           (implies (and (sib-equiv x y) (sib-equiv y z))
                    (sib-equiv x z)))
      :rule-classes (:equivalence))

    Theorem: sib-equiv-implies-equal-sib-fix-1

    (defthm sib-equiv-implies-equal-sib-fix-1
      (implies (sib-equiv x x-equiv)
               (equal (sib-fix x) (sib-fix x-equiv)))
      :rule-classes (:congruence))

    Theorem: sib-fix-under-sib-equiv

    (defthm sib-fix-under-sib-equiv
      (sib-equiv (sib-fix x) x)
      :rule-classes (:rewrite :rewrite-quoted-constant))

    Function: sib$inline

    (defun sib$inline (base index scale)
      (declare (xargs :guard (and (3bits-p base)
                                  (3bits-p index)
                                  (2bits-p scale))))
      (b* ((base (mbe :logic (3bits-fix base)
                      :exec base))
           (index (mbe :logic (3bits-fix index)
                       :exec index))
           (scale (mbe :logic (2bits-fix scale)
                       :exec scale)))
        (logapp 3 base (logapp 3 index scale))))

    Theorem: sib-p-of-sib

    (defthm sib-p-of-sib
      (b* ((sib (sib$inline base index scale)))
        (sib-p sib))
      :rule-classes :rewrite)

    Theorem: sib$inline-of-3bits-fix-base

    (defthm sib$inline-of-3bits-fix-base
      (equal (sib$inline (3bits-fix base)
                         index scale)
             (sib$inline base index scale)))

    Theorem: sib$inline-3bits-equiv-congruence-on-base

    (defthm sib$inline-3bits-equiv-congruence-on-base
      (implies (3bits-equiv base base-equiv)
               (equal (sib$inline base index scale)
                      (sib$inline base-equiv index scale)))
      :rule-classes :congruence)

    Theorem: sib$inline-of-3bits-fix-index

    (defthm sib$inline-of-3bits-fix-index
      (equal (sib$inline base (3bits-fix index)
                         scale)
             (sib$inline base index scale)))

    Theorem: sib$inline-3bits-equiv-congruence-on-index

    (defthm sib$inline-3bits-equiv-congruence-on-index
      (implies (3bits-equiv index index-equiv)
               (equal (sib$inline base index scale)
                      (sib$inline base index-equiv scale)))
      :rule-classes :congruence)

    Theorem: sib$inline-of-2bits-fix-scale

    (defthm sib$inline-of-2bits-fix-scale
      (equal (sib$inline base index (2bits-fix scale))
             (sib$inline base index scale)))

    Theorem: sib$inline-2bits-equiv-congruence-on-scale

    (defthm sib$inline-2bits-equiv-congruence-on-scale
      (implies (2bits-equiv scale scale-equiv)
               (equal (sib$inline base index scale)
                      (sib$inline base index scale-equiv)))
      :rule-classes :congruence)

    Function: sib-equiv-under-mask$inline

    (defun sib-equiv-under-mask$inline (x x1 mask)
      (declare (xargs :guard (and (sib-p x)
                                  (sib-p x1)
                                  (integerp mask))))
      (fty::int-equiv-under-mask (sib-fix x)
                                 (sib-fix x1)
                                 mask))

    Function: sib->base$inline

    (defun sib->base$inline (x)
      (declare (xargs :guard (sib-p x)))
      (mbe :logic
           (let ((x (sib-fix x)))
             (part-select x :low 0 :width 3))
           :exec (the (unsigned-byte 3)
                      (logand (the (unsigned-byte 3) 7)
                              (the (unsigned-byte 8) x)))))

    Theorem: 3bits-p-of-sib->base

    (defthm 3bits-p-of-sib->base
      (b* ((base (sib->base$inline x)))
        (3bits-p base))
      :rule-classes :rewrite)

    Theorem: sib->base$inline-of-sib-fix-x

    (defthm sib->base$inline-of-sib-fix-x
      (equal (sib->base$inline (sib-fix x))
             (sib->base$inline x)))

    Theorem: sib->base$inline-sib-equiv-congruence-on-x

    (defthm sib->base$inline-sib-equiv-congruence-on-x
      (implies (sib-equiv x x-equiv)
               (equal (sib->base$inline x)
                      (sib->base$inline x-equiv)))
      :rule-classes :congruence)

    Theorem: sib->base-of-sib

    (defthm sib->base-of-sib
      (equal (sib->base (sib base index scale))
             (3bits-fix base)))

    Theorem: sib->base-of-write-with-mask

    (defthm sib->base-of-write-with-mask
     (implies
       (and (fty::bitstruct-read-over-write-hyps x sib-equiv-under-mask)
            (sib-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 7) 0))
       (equal (sib->base x) (sib->base y))))

    Function: sib->index$inline

    (defun sib->index$inline (x)
     (declare (xargs :guard (sib-p x)))
     (mbe
         :logic
         (let ((x (sib-fix x)))
           (part-select x :low 3 :width 3))
         :exec (the (unsigned-byte 3)
                    (logand (the (unsigned-byte 3) 7)
                            (the (unsigned-byte 5)
                                 (ash (the (unsigned-byte 8) x) -3))))))

    Theorem: 3bits-p-of-sib->index

    (defthm 3bits-p-of-sib->index
      (b* ((index (sib->index$inline x)))
        (3bits-p index))
      :rule-classes :rewrite)

    Theorem: sib->index$inline-of-sib-fix-x

    (defthm sib->index$inline-of-sib-fix-x
      (equal (sib->index$inline (sib-fix x))
             (sib->index$inline x)))

    Theorem: sib->index$inline-sib-equiv-congruence-on-x

    (defthm sib->index$inline-sib-equiv-congruence-on-x
      (implies (sib-equiv x x-equiv)
               (equal (sib->index$inline x)
                      (sib->index$inline x-equiv)))
      :rule-classes :congruence)

    Theorem: sib->index-of-sib

    (defthm sib->index-of-sib
      (equal (sib->index (sib base index scale))
             (3bits-fix index)))

    Theorem: sib->index-of-write-with-mask

    (defthm sib->index-of-write-with-mask
     (implies
       (and (fty::bitstruct-read-over-write-hyps x sib-equiv-under-mask)
            (sib-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 56)
                   0))
       (equal (sib->index x) (sib->index y))))

    Function: sib->scale$inline

    (defun sib->scale$inline (x)
     (declare (xargs :guard (sib-p x)))
     (mbe
         :logic
         (let ((x (sib-fix x)))
           (part-select x :low 6 :width 2))
         :exec (the (unsigned-byte 2)
                    (logand (the (unsigned-byte 2) 3)
                            (the (unsigned-byte 2)
                                 (ash (the (unsigned-byte 8) x) -6))))))

    Theorem: 2bits-p-of-sib->scale

    (defthm 2bits-p-of-sib->scale
      (b* ((scale (sib->scale$inline x)))
        (2bits-p scale))
      :rule-classes :rewrite)

    Theorem: sib->scale$inline-of-sib-fix-x

    (defthm sib->scale$inline-of-sib-fix-x
      (equal (sib->scale$inline (sib-fix x))
             (sib->scale$inline x)))

    Theorem: sib->scale$inline-sib-equiv-congruence-on-x

    (defthm sib->scale$inline-sib-equiv-congruence-on-x
      (implies (sib-equiv x x-equiv)
               (equal (sib->scale$inline x)
                      (sib->scale$inline x-equiv)))
      :rule-classes :congruence)

    Theorem: sib->scale-of-sib

    (defthm sib->scale-of-sib
      (equal (sib->scale (sib base index scale))
             (2bits-fix scale)))

    Theorem: sib->scale-of-write-with-mask

    (defthm sib->scale-of-write-with-mask
     (implies
       (and (fty::bitstruct-read-over-write-hyps x sib-equiv-under-mask)
            (sib-equiv-under-mask x y fty::mask)
            (equal (logand (lognot fty::mask) 192)
                   0))
       (equal (sib->scale x) (sib->scale y))))

    Theorem: sib-fix-in-terms-of-sib

    (defthm sib-fix-in-terms-of-sib
      (equal (sib-fix x) (change-sib x)))

    Function: !sib->base$inline

    (defun !sib->base$inline (base x)
      (declare (xargs :guard (and (3bits-p base) (sib-p x))))
      (mbe :logic
           (b* ((base (mbe :logic (3bits-fix base)
                           :exec base))
                (x (sib-fix x)))
             (part-install base x :width 3 :low 0))
           :exec (the (unsigned-byte 8)
                      (logior (the (unsigned-byte 8)
                                   (logand (the (unsigned-byte 8) x)
                                           (the (signed-byte 4) -8)))
                              (the (unsigned-byte 3) base)))))

    Theorem: sib-p-of-!sib->base

    (defthm sib-p-of-!sib->base
      (b* ((new-x (!sib->base$inline base x)))
        (sib-p new-x))
      :rule-classes :rewrite)

    Theorem: !sib->base$inline-of-3bits-fix-base

    (defthm !sib->base$inline-of-3bits-fix-base
      (equal (!sib->base$inline (3bits-fix base) x)
             (!sib->base$inline base x)))

    Theorem: !sib->base$inline-3bits-equiv-congruence-on-base

    (defthm !sib->base$inline-3bits-equiv-congruence-on-base
      (implies (3bits-equiv base base-equiv)
               (equal (!sib->base$inline base x)
                      (!sib->base$inline base-equiv x)))
      :rule-classes :congruence)

    Theorem: !sib->base$inline-of-sib-fix-x

    (defthm !sib->base$inline-of-sib-fix-x
      (equal (!sib->base$inline base (sib-fix x))
             (!sib->base$inline base x)))

    Theorem: !sib->base$inline-sib-equiv-congruence-on-x

    (defthm !sib->base$inline-sib-equiv-congruence-on-x
      (implies (sib-equiv x x-equiv)
               (equal (!sib->base$inline base x)
                      (!sib->base$inline base x-equiv)))
      :rule-classes :congruence)

    Theorem: !sib->base-is-sib

    (defthm !sib->base-is-sib
      (equal (!sib->base base x)
             (change-sib x :base base)))

    Theorem: sib->base-of-!sib->base

    (defthm sib->base-of-!sib->base
      (b* ((?new-x (!sib->base$inline base x)))
        (equal (sib->base new-x)
               (3bits-fix base))))

    Theorem: !sib->base-equiv-under-mask

    (defthm !sib->base-equiv-under-mask
      (b* ((?new-x (!sib->base$inline base x)))
        (sib-equiv-under-mask new-x x -8)))

    Function: !sib->index$inline

    (defun !sib->index$inline (index x)
      (declare (xargs :guard (and (3bits-p index) (sib-p x))))
      (mbe :logic
           (b* ((index (mbe :logic (3bits-fix index)
                            :exec index))
                (x (sib-fix x)))
             (part-install index x :width 3 :low 3))
           :exec (the (unsigned-byte 8)
                      (logior (the (unsigned-byte 8)
                                   (logand (the (unsigned-byte 8) x)
                                           (the (signed-byte 7) -57)))
                              (the (unsigned-byte 6)
                                   (ash (the (unsigned-byte 3) index)
                                        3))))))

    Theorem: sib-p-of-!sib->index

    (defthm sib-p-of-!sib->index
      (b* ((new-x (!sib->index$inline index x)))
        (sib-p new-x))
      :rule-classes :rewrite)

    Theorem: !sib->index$inline-of-3bits-fix-index

    (defthm !sib->index$inline-of-3bits-fix-index
      (equal (!sib->index$inline (3bits-fix index) x)
             (!sib->index$inline index x)))

    Theorem: !sib->index$inline-3bits-equiv-congruence-on-index

    (defthm !sib->index$inline-3bits-equiv-congruence-on-index
      (implies (3bits-equiv index index-equiv)
               (equal (!sib->index$inline index x)
                      (!sib->index$inline index-equiv x)))
      :rule-classes :congruence)

    Theorem: !sib->index$inline-of-sib-fix-x

    (defthm !sib->index$inline-of-sib-fix-x
      (equal (!sib->index$inline index (sib-fix x))
             (!sib->index$inline index x)))

    Theorem: !sib->index$inline-sib-equiv-congruence-on-x

    (defthm !sib->index$inline-sib-equiv-congruence-on-x
      (implies (sib-equiv x x-equiv)
               (equal (!sib->index$inline index x)
                      (!sib->index$inline index x-equiv)))
      :rule-classes :congruence)

    Theorem: !sib->index-is-sib

    (defthm !sib->index-is-sib
      (equal (!sib->index index x)
             (change-sib x :index index)))

    Theorem: sib->index-of-!sib->index

    (defthm sib->index-of-!sib->index
      (b* ((?new-x (!sib->index$inline index x)))
        (equal (sib->index new-x)
               (3bits-fix index))))

    Theorem: !sib->index-equiv-under-mask

    (defthm !sib->index-equiv-under-mask
      (b* ((?new-x (!sib->index$inline index x)))
        (sib-equiv-under-mask new-x x -57)))

    Function: !sib->scale$inline

    (defun !sib->scale$inline (scale x)
      (declare (xargs :guard (and (2bits-p scale) (sib-p x))))
      (mbe :logic
           (b* ((scale (mbe :logic (2bits-fix scale)
                            :exec scale))
                (x (sib-fix x)))
             (part-install scale x :width 2 :low 6))
           :exec (the (unsigned-byte 8)
                      (logior (the (unsigned-byte 8)
                                   (logand (the (unsigned-byte 8) x)
                                           (the (signed-byte 9) -193)))
                              (the (unsigned-byte 8)
                                   (ash (the (unsigned-byte 2) scale)
                                        6))))))

    Theorem: sib-p-of-!sib->scale

    (defthm sib-p-of-!sib->scale
      (b* ((new-x (!sib->scale$inline scale x)))
        (sib-p new-x))
      :rule-classes :rewrite)

    Theorem: !sib->scale$inline-of-2bits-fix-scale

    (defthm !sib->scale$inline-of-2bits-fix-scale
      (equal (!sib->scale$inline (2bits-fix scale) x)
             (!sib->scale$inline scale x)))

    Theorem: !sib->scale$inline-2bits-equiv-congruence-on-scale

    (defthm !sib->scale$inline-2bits-equiv-congruence-on-scale
      (implies (2bits-equiv scale scale-equiv)
               (equal (!sib->scale$inline scale x)
                      (!sib->scale$inline scale-equiv x)))
      :rule-classes :congruence)

    Theorem: !sib->scale$inline-of-sib-fix-x

    (defthm !sib->scale$inline-of-sib-fix-x
      (equal (!sib->scale$inline scale (sib-fix x))
             (!sib->scale$inline scale x)))

    Theorem: !sib->scale$inline-sib-equiv-congruence-on-x

    (defthm !sib->scale$inline-sib-equiv-congruence-on-x
      (implies (sib-equiv x x-equiv)
               (equal (!sib->scale$inline scale x)
                      (!sib->scale$inline scale x-equiv)))
      :rule-classes :congruence)

    Theorem: !sib->scale-is-sib

    (defthm !sib->scale-is-sib
      (equal (!sib->scale scale x)
             (change-sib x :scale scale)))

    Theorem: sib->scale-of-!sib->scale

    (defthm sib->scale-of-!sib->scale
      (b* ((?new-x (!sib->scale$inline scale x)))
        (equal (sib->scale new-x)
               (2bits-fix scale))))

    Theorem: !sib->scale-equiv-under-mask

    (defthm !sib->scale-equiv-under-mask
      (b* ((?new-x (!sib->scale$inline scale x)))
        (sib-equiv-under-mask new-x x 63)))

    Function: sib-debug$inline

    (defun sib-debug$inline (x)
      (declare (xargs :guard (sib-p x)))
      (b* (((sib x)))
        (cons (cons 'base x.base)
              (cons (cons 'index x.index)
                    (cons (cons 'scale x.scale) nil)))))

    Theorem: return-type-of-sib->base-linear

    (defthm return-type-of-sib->base-linear
      (< (sib->base sib) 8)
      :rule-classes :linear)

    Theorem: return-type-of-sib->index-linear

    (defthm return-type-of-sib->index-linear
      (< (sib->index sib) 8)
      :rule-classes :linear)

    Theorem: return-type-of-sib->scale-linear

    (defthm return-type-of-sib->scale-linear
      (< (sib->scale sib) 4)
      :rule-classes :linear)