• 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
      • Booting-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
            • X86-effective-addr-32/64
            • X86-effective-addr-from-sib
            • X86-effective-addr-16
            • X86-effective-addr-16-disp
            • X86-effective-addr
          • 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
        • 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

• Effective-address-computations

X86-effective-addr-16

Effective address calculation with 16-bit addressing.

Signature

(x86-effective-addr-16 proc-mode temp-rip r/m mod x86) 
  → 
(mv flg address increment-rip-by x86)

Arguments

r/m — r/m field of ModR/M byte.

mod — mod field of ModR/M byte.

Returns

address — Type (n16p address).

increment-rip-by — Type (natp increment-rip-by).

x86 — Type (x86p x86), given (x86p x86).

This is according to Intel manual, Mar'17, Vol. 2, Table 2-1.

We assume that the additions in the table are modular, even though the documentation is not clear in that respect. So we simply apply n16 to the exact integer result. This is in analogy to the use of n32 for effective address calculation in 64-bit mode when there is an address size override prefix: see x86-effective-addr-32/64.

Definitions and Theorems

Function: x86-effective-addr-16

(defun x86-effective-addr-16 (proc-mode temp-rip r/m mod x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (signed-byte 48) temp-rip)
          (type (unsigned-byte 3) r/m)
          (type (unsigned-byte 2) mod))
 (declare (xargs :guard (and (2bits-p mod) (3bits-p r/m))))
 (let ((__function__ 'x86-effective-addr-16))
  (declare (ignorable __function__))
  (case r/m
   (0 (b* ((bx (rr16 3 x86))
           (si (rr16 6 x86))
           ((mv flg disp increment-rip-by x86)
            (x86-effective-addr-16-disp proc-mode temp-rip mod x86))
           ((when flg) (mv flg 0 0 x86)))
        (mv nil (n16 (+ bx si disp))
            increment-rip-by x86)))
   (1 (b* ((bx (rr16 3 x86))
           (di (rr16 7 x86))
           ((mv flg disp increment-rip-by x86)
            (x86-effective-addr-16-disp proc-mode temp-rip mod x86))
           ((when flg) (mv flg 0 0 x86)))
        (mv nil (n16 (+ bx di disp))
            increment-rip-by x86)))
   (2 (b* ((bp (rr16 5 x86))
           (si (rr16 6 x86))
           ((mv flg disp increment-rip-by x86)
            (x86-effective-addr-16-disp proc-mode temp-rip mod x86))
           ((when flg) (mv flg 0 0 x86)))
        (mv nil (n16 (+ bp si disp))
            increment-rip-by x86)))
   (3 (b* ((bp (rr16 5 x86))
           (di (rr16 7 x86))
           ((mv flg disp increment-rip-by x86)
            (x86-effective-addr-16-disp proc-mode temp-rip mod x86))
           ((when flg) (mv flg 0 0 x86)))
        (mv nil (n16 (+ bp di disp))
            increment-rip-by x86)))
   (4 (b* ((si (rr16 6 x86))
           ((mv flg disp increment-rip-by x86)
            (x86-effective-addr-16-disp proc-mode temp-rip mod x86))
           ((when flg) (mv flg 0 0 x86)))
        (mv nil (n16 (+ si disp))
            increment-rip-by x86)))
   (5 (b* ((di (rr16 7 x86))
           ((mv flg disp increment-rip-by x86)
            (x86-effective-addr-16-disp proc-mode temp-rip mod x86))
           ((when flg) (mv flg 0 0 x86)))
        (mv nil (n16 (+ di disp))
            increment-rip-by x86)))
   (6
    (case mod
     (0 (b* (((mv flg disp x86)
              (rime-size-opt proc-mode 2 temp-rip 1 :x nil x86
                             :mem-ptr? nil))
             ((when flg) (mv flg 0 0 x86)))
          (mv nil (n16 disp) 2 x86)))
     (otherwise
      (b* ((bp (rr16 5 x86))
           ((mv flg disp increment-rip-by x86)
            (x86-effective-addr-16-disp proc-mode temp-rip mod x86))
           ((when flg) (mv flg 0 0 x86)))
        (mv nil (n16 (+ bp disp))
            increment-rip-by x86)))))
   (7 (b* ((bx (rr16 3 x86))
           ((mv flg disp increment-rip-by x86)
            (x86-effective-addr-16-disp proc-mode temp-rip mod x86))
           ((when flg) (mv flg 0 0 x86)))
        (mv nil (n16 (+ bx disp))
            increment-rip-by x86)))
   (otherwise (mv :r/m-out-of-range 0 0 x86)))))

Theorem: n16p-of-x86-effective-addr-16.address

(defthm n16p-of-x86-effective-addr-16.address
  (b* (((mv ?flg ?address ?increment-rip-by ?x86)
        (x86-effective-addr-16 proc-mode temp-rip r/m mod x86)))
    (n16p address))
  :rule-classes :rewrite)

Theorem: natp-of-x86-effective-addr-16.increment-rip-by

(defthm natp-of-x86-effective-addr-16.increment-rip-by
  (b* (((mv ?flg ?address ?increment-rip-by ?x86)
        (x86-effective-addr-16 proc-mode temp-rip r/m mod x86)))
    (natp increment-rip-by))
  :rule-classes :rewrite)

Theorem: x86p-of-x86-effective-addr-16.x86

(defthm x86p-of-x86-effective-addr-16.x86
 (implies
      (x86p x86)
      (b* (((mv ?flg ?address ?increment-rip-by ?x86)
            (x86-effective-addr-16 proc-mode temp-rip r/m mod x86)))
        (x86p x86)))
 :rule-classes :rewrite)

Theorem: i64p-mv-nth-1-x86-effective-addr-16

(defthm i64p-mv-nth-1-x86-effective-addr-16
 (signed-byte-p
    64
    (mv-nth 1
            (x86-effective-addr-16 proc-mode temp-rip r/m mod x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary
   (integerp
    (mv-nth 1
            (x86-effective-addr-16 proc-mode temp-rip r/m mod x86)))
   :hints (("Goal" :in-theory '(signed-byte-p integer-range-p))))
  (:linear
   :corollary
   (and
    (<=
       -9223372036854775808
       (mv-nth
            1
            (x86-effective-addr-16 proc-mode temp-rip r/m mod x86)))
    (<
     (mv-nth 1
             (x86-effective-addr-16 proc-mode temp-rip r/m mod x86))
     9223372036854775808))
   :hints
   (("Goal"
         :in-theory '(signed-byte-p integer-range-p (:e expt)))))))

Theorem: natp-mv-nth-2-x86-effective-addr-16

(defthm natp-mv-nth-2-x86-effective-addr-16
 (natp
    (mv-nth 2
            (x86-effective-addr-16 proc-mode temp-rip r/m mod x86)))
 :rule-classes :type-prescription)

Theorem: mv-nth-2-x86-effective-addr-16-<=-4

(defthm mv-nth-2-x86-effective-addr-16-<=-4
 (<= (mv-nth 2
             (x86-effective-addr-16 proc-mode temp-rip r/m mod x86))
     4)
 :rule-classes :linear)