		Search-engine friendly clone of the ACL2 documentation.

Decoding-and-spec-utils

Select-segment-register

Segment register to use for an instruction operand in memory.

Signature
(select-segment-register proc-mode p2 p4? mod r/m sib x86) → seg-reg
Arguments: p2 — Guard (unsigned-byte-p 8 p2).; p4? — Guard (booleanp p4?).; mod — Guard (unsigned-byte-p 2 mod).; r/m — Guard (unsigned-byte-p 3 r/m).; sib — Guard (unsigned-byte-p 8 sib).; x86 — Guard (x86p x86).
Returns: seg-reg — Type (integer-range-p 0 *segment-register-names-len* seg-reg).

If there is a segment register override prefix, the prefix determines the segment register, according to Intel manual, Mar'17, Volume 2, Section 2.1.1.

Otherwise, we use the default segment selection rules in Intel manual, May'18, Volume 1, Table 3-5. Since we only call this function for instruction operands, the CS rule does not apply. The ES rule applies to string instructions, but our model does not use this function to determine the ES segment for string instructions (which cannot be overridden, at least for the string instructions we currently support), so this function does not take the ES rule into account either. So the result is either SS or DS, based on whether the base register is one of rSP and rBP or not: this determination is made based on Intel manual, May'18, Volume 2, Table 2-1 if the address size is 16 bits, and Intel manual, May'18, Volume 2, Table 2-2 otherwise. However, when Mod is not 11b and R/M is 100b, the notation [--][--] in Table 2-2 indicates the use of a SIB byte: according to Intel manual, May'18, Volume 2, Table 2-3, when the Base field of the SIB byte is 100b, the base register is rSP, and thus in this case the default segment register is SS.

Note that here we may recalculate the address size even if that has already been calculated as part of the decoding of the instruction whose operand we are accessing. Thus, it may be possible to optimize the overall code.

Definitions and Theorems

Function: select-segment-register$inline

(defun select-segment-register$inline
       (proc-mode p2 p4? mod r/m sib x86)
  (declare (xargs :stobjs (x86)))
  (declare (type (integer 0 4) proc-mode))
  (declare (xargs :guard (and (unsigned-byte-p 8 p2)
                              (booleanp p4?)
                              (unsigned-byte-p 2 mod)
                              (unsigned-byte-p 3 r/m)
                              (unsigned-byte-p 8 sib)
                              (x86p x86))))
  (case p2
    (46 1)
    (54 2)
    (62 3)
    (38 0)
    (100 4)
    (101 5)
    (t (b* ((addr-size (select-address-size proc-mode p4? x86)))
         (if (= addr-size 2)
             (if (and (not (= mod 3))
                      (or (= r/m 2) (= r/m 3)))
                 2
               3)
           (if (or (and (or (= mod 1) (= mod 2)) (= r/m 5))
                   (and (not (= mod 3))
                        (= r/m 4)
                        (= (sib->base sib) 4)))
               2
             3))))))

Theorem: return-type-of-select-segment-register

(defthm return-type-of-select-segment-register
  (b* ((seg-reg (select-segment-register$inline
                     proc-mode p2 p4? mod r/m sib x86)))
    (integer-range-p 0 *segment-register-names-len* seg-reg))
  :rule-classes :rewrite)

Theorem: range-of-select-segment-register

(defthm range-of-select-segment-register
  (b* ((?seg-reg (select-segment-register$inline
                      proc-mode p2 p4? mod r/m sib x86)))
    (and (<= 0 seg-reg) (< seg-reg 6)))
  :rule-classes :linear)