• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • Syscalls
        • Cpuid
        • X86isa-state
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • X86-modes
        • Segmentation
          • Ea-to-la
          • Segment-base-and-bounds
          • Ia32e-segmentation
          • Eas-to-las
          • Ia32-segmentation
        • Register-readers-and-writers
        • Other-non-deterministic-computations
        • Environment
        • Paging
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Execloader
    • Axe
  • Testing-utilities
  • Math

• Segmentation

Segment-base-and-bounds

Return a segment's base linear address, lower bound, and upper bound.

Signature

(segment-base-and-bounds proc-mode seg-reg x86) 
  → 
(mv base lower-bound upper-bound)

Returns

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

lower-bound — Type (n33p lower-bound).

upper-bound — Type (n32p upper-bound).

The segment is the one in the given segment register.

Base addresses coming from segment descriptors are always 32 bits: see Intel manual, Mar'17, Vol. 3A, Sec. 3.4.5 and AMD manual, Apr'16, Vol. 2, Sec. 4.7 and 4.8. However, in 64-bit mode, segment bases for FS and GS are 64 bits: see Intel manual, Mar'17, Vol. 3A, Sec. 3.4.4 and AMD manual, Apr'16, Vol. 2, Sec 4.5.3. As an optimization, in 64-bit mode, since segment bases for CS, DS, SS, and ES are ignored, this function just returns 0 as the base result under these conditions. In 64-bit mode, when the segment register is FS or GS, we read the base address from the MSRs mentioned in Intel manual, Mar'17, Vol. 3A, Sec. 3.4.4 and AMD manual, Apr'16, Vol. 2, Sec 4.5.3; these are physically mapped to the relevant hidden portions of FS and GS, so it should be a state invariant that they are equal to the relevant hidden portions of FS and GS. In 32-bit mode, since the high 32 bits are ignored (see Intel manual, Mar'17, Vol. 3A, Sec. 3.4.4 and AMD manual, Apr'16, Vol. 2, Sec 4.5.3), we only return the low 32 bits of the base address read from the hidden portion of the segment register.

*hidden-segment-register-layout* uses 32 bits for the segment limit, which is consistent with the 20 bits in segment descriptors when the G (granularity) bit is 1: see Intel manual, Mar'17, Vol. 3A, Sec. 3.4.5 and AMD manual, Apr'16, Vol. 2, Sec. 4-7 and 4-8. Thus, the limit is an unsigned 32-bit integer.

The lower bound is 0 for code segments, i.e. for the CS register. For data (including stack) segments, i.e. for the SS, DS, ES, FS, and GS registers, the lower bound depends on the E bit: if E is 0, the lower bound is 0; if E is 1, the segment is an expand-down data segment and the lower bound is one plus the segment limit. See Intel manual, Mar'17, Vol. 3A, Sec. 3.4.5 and AMD manual, Apr'16, Vol. 2, Sec. 4.7 and 4-8. Since the limit is an unsigned 32-bit (see above), adding 1 may produce an unsigned 33-bit result. Even though this should not actually happen with well-formed segments, this function returns an unsigned 33-bit integer as the lower bound result. As an optimization, in 64-bit mode, since segment limits and bounds are ignored, this function returns 0 as the lower bound; the caller must ignore this result in 64-bit mode.

The upper bound is the segment limit for code segments, i.e. for the CS register. For data (including stack) segments, i.e. for the SS, DS, ES, FS, and GS registers, the upper bound depends on the E and D/B bits: if E is 0, the upper bound is the segment limit; if E is 1, the segment is an expand-down data segment and the upper bound is 2^32-1 if D/B is 1, 2^16-1 if D/B is 0. See Intel manual, Mar'17, Vol. 3A, Sec. 3.4.5 and AMD manual, Apr'16, Vol. 2, Sec. 4.7 and 4-8. Since the limit is an unsigned 32-bit (see above), this function returns an unsigned 32-bit integer as the upper bound result. As an optimization, in 64-bit mode, since segment limits and bounds are ignored, this function returns 0 as the upper bound; the caller must ignore this result in 64-bit mode.

Definitions and Theorems

Function: segment-base-and-bounds$inline

(defun
 segment-base-and-bounds$inline
 (proc-mode seg-reg x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (integer 0 5) seg-reg))
 (case
  proc-mode
  (0 (cond ((eql seg-reg 4) (mv (msri 1 x86) 0 0))
           ((eql seg-reg 5) (mv (msri 2 x86) 0 0))
           (t (mv 0 0 0))))
  (1
   (mbe
    :logic
    (b*
      ((base (loghead 64 (seg-hidden-basei seg-reg x86)))
       (limit (loghead 32 (seg-hidden-limiti seg-reg x86)))
       (attr (loghead 16 (seg-hidden-attri seg-reg x86)))
       (d/b (if (= seg-reg 1)
                (code-segment-descriptor-attributesbits->d attr)
                (data-segment-descriptor-attributesbits->d/b attr)))
       (e (if (= seg-reg 1)
              0
              (data-segment-descriptor-attributesbits->e attr)))
       (lower (if (= e 1) (1+ limit) 0))
       (upper (if (= e 1)
                  (if (= d/b 1) 4294967295 65535)
                  limit)))
      (mv (n32 base) lower upper))
    :exec
    (b*
      (((the (unsigned-byte 64) base)
        (seg-hidden-basei seg-reg x86))
       ((the (unsigned-byte 32) base)
        (bitsets::bignum-extract base 0))
       ((the (unsigned-byte 32) limit)
        (seg-hidden-limiti seg-reg x86))
       ((the (unsigned-byte 16) attr)
        (seg-hidden-attri seg-reg x86))
       (d/b (if (= seg-reg 1)
                (code-segment-descriptor-attributesbits->d attr)
                (data-segment-descriptor-attributesbits->d/b attr)))
       (e (if (= seg-reg 1)
              0
              (data-segment-descriptor-attributesbits->e attr)))
       (lower (if (= e 1) (1+ limit) 0))
       (upper (if (= e 1)
                  (if (= d/b 1) 4294967295 65535)
                  limit)))
      (mv base lower upper))))
  (otherwise (mv 0 0 0))))

Theorem: n64p-of-segment-base-and-bounds.base

(defthm
 n64p-of-segment-base-and-bounds.base
 (implies
      (x86p x86)
      (b* (((mv ?base ?lower-bound ?upper-bound)
            (segment-base-and-bounds$inline proc-mode seg-reg x86)))
          (n64p base)))
 :rule-classes :rewrite)

Theorem: n33p-of-segment-base-and-bounds.lower-bound

(defthm
     n33p-of-segment-base-and-bounds.lower-bound
     (b* (((mv ?base ?lower-bound ?upper-bound)
           (segment-base-and-bounds$inline proc-mode seg-reg x86)))
         (n33p lower-bound))
     :rule-classes :rewrite)

Theorem: n32p-of-segment-base-and-bounds.upper-bound

(defthm
     n32p-of-segment-base-and-bounds.upper-bound
     (b* (((mv ?base ?lower-bound ?upper-bound)
           (segment-base-and-bounds$inline proc-mode seg-reg x86)))
         (n32p upper-bound))
     :rule-classes :rewrite)

Theorem: segment-base-is-n64p

(defthm
 segment-base-is-n64p
 (implies
     (x86p x86)
     (unsigned-byte-p
          64
          (mv-nth 0
                  (segment-base-and-bounds proc-mode seg-reg x86))))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary
   (implies
    (x86p x86)
    (natp (mv-nth 0
                  (segment-base-and-bounds proc-mode seg-reg x86))))
   :hints
   (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (implies
    (x86p x86)
    (and
       (<= 0
           (mv-nth 0
                   (segment-base-and-bounds proc-mode seg-reg x86)))
       (< (mv-nth 0
                  (segment-base-and-bounds proc-mode seg-reg x86))
          18446744073709551616)))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: segment-lower-bound-is-n33p

(defthm
 segment-lower-bound-is-n33p
 (unsigned-byte-p
      33
      (mv-nth 1
              (segment-base-and-bounds proc-mode seg-reg x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
     :corollary
     (natp (mv-nth 1
                   (segment-base-and-bounds proc-mode seg-reg x86)))
     :hints
     (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and
       (<= 0
           (mv-nth 1
                   (segment-base-and-bounds proc-mode seg-reg x86)))
       (< (mv-nth 1
                  (segment-base-and-bounds proc-mode seg-reg x86))
          8589934592))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: segment-upper-bound-is-n32p

(defthm
 segment-upper-bound-is-n32p
 (unsigned-byte-p
      32
      (mv-nth 2
              (segment-base-and-bounds proc-mode seg-reg x86)))
 :rule-classes
 (:rewrite
  (:type-prescription
     :corollary
     (natp (mv-nth 2
                   (segment-base-and-bounds proc-mode seg-reg x86)))
     :hints
     (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and
       (<= 0
           (mv-nth 2
                   (segment-base-and-bounds proc-mode seg-reg x86)))
       (< (mv-nth 2
                  (segment-base-and-bounds proc-mode seg-reg x86))
          4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))

Theorem: segment-base-and-bound-of-xw

(defthm
 segment-base-and-bound-of-xw
 (implies
   (and (not (equal fld :msr))
        (not (equal fld :seg-hidden-base))
        (not (equal fld :seg-hidden-limit))
        (not (equal fld :seg-hidden-attr)))
   (equal (segment-base-and-bounds proc-mode
                                   seg-reg (xw fld index value x86))
          (segment-base-and-bounds proc-mode seg-reg x86))))