		Search-engine friendly clone of the ACL2 documentation.

Top-level-memory

Wime32

Write a signed 32-bit value to memory via an effective address.

Signature
(wime32 proc-mode eff-addr seg-reg val check-alignment? x86 &key (mem-ptr? 'nil)) → (mv flg x86-new)
Arguments: check-alignment? — Guard (booleanp check-alignment?).; mem-ptr? — Guard (booleanp mem-ptr?).
Returns: x86-new — Type (x86p x86-new), given (x86p x86).

The effective address eff-addr is translated to a canonical linear address. If this translation is successful and no other error occurs (like alignment errors), then wiml32 is called.

Prior to the effective address translation, we check whether write access is allowed. In 32-bit mode, write access is allowed in data segments (DS, ES, FS, GS, and SS) if the W bit in the segment descriptor is 1; write access is disallowed in code segments (this is not explicitly mentioned in Intel manual, May'18, Volume 3, Section 3.4.5.1, but it seems reasonable). In 64-bit mode, the W bit is ignored (see Atmel manual, Dec'17, Volume 2, Section 4.8.1); by analogy, we allow write access to the code segment as well. These checks may be slightly optimized using the invariant that SS.W must be 1 when SS is loaded.

Definitions and Theorems

Function: wime32$inline

(defun wime32$inline (proc-mode eff-addr seg-reg
                                val check-alignment? x86 mem-ptr?)
 (declare (xargs :stobjs (x86)))
 (declare (type (integer 0 4) proc-mode)
          (type (signed-byte 64) eff-addr)
          (type (integer 0 5) seg-reg)
          (type (signed-byte 32) val))
 (declare (xargs :guard (and (booleanp check-alignment?)
                             (booleanp mem-ptr?))))
 (b*
  (((when
     (and
      (/= proc-mode 0)
      (or (= seg-reg 1)
          (b* ((attr (loghead 16 (seg-hidden-attri seg-reg x86)))
               (w (data-segment-descriptor-attributesbits->w attr)))
            (= w 0)))))
    (mv (list :non-writable-segment eff-addr seg-reg)
        x86))
   ((mv flg lin-addr)
    (ea-to-la proc-mode eff-addr seg-reg 4 x86))
   ((when flg) (mv flg x86))
   ((unless (or (not check-alignment?)
                (address-aligned-p lin-addr 4 mem-ptr?)))
    (mv (list :unaligned-linear-address lin-addr)
        x86)))
  (wiml32 lin-addr val x86)))

Theorem: x86p-of-wime32.x86-new

(defthm x86p-of-wime32.x86-new
  (implies (x86p x86)
           (b* (((mv ?flg ?x86-new)
                 (wime32$inline proc-mode eff-addr seg-reg
                                val check-alignment? x86 mem-ptr?)))
             (x86p x86-new)))
  :rule-classes :rewrite)

Theorem: wime32-when-64-bit-modep-and-not-fs/gs

(defthm wime32-when-64-bit-modep-and-not-fs/gs
  (implies (and (not (equal seg-reg 4))
                (not (equal seg-reg 5))
                (canonical-address-p eff-addr)
                (or (not check-alignment?)
                    (address-aligned-p eff-addr 4 mem-ptr?)))
           (equal (wime32 0 eff-addr
                          seg-reg val check-alignment? x86
                          :mem-ptr? mem-ptr?)
                  (wiml32 eff-addr val x86))))

Theorem: wime32-unaligned-when-64-bit-modep-and-not-fs/gs

(defthm wime32-unaligned-when-64-bit-modep-and-not-fs/gs
  (implies (and (not (equal seg-reg 4))
                (not (equal seg-reg 5))
                (not (or (not check-alignment?)
                         (address-aligned-p eff-addr 4 mem-ptr?)))
                (canonical-address-p eff-addr))
           (equal (wime32 0 eff-addr
                          seg-reg val check-alignment? x86
                          :mem-ptr? mem-ptr?)
                  (list (list :unaligned-linear-address eff-addr)
                        x86))))

Theorem: wime32-when-64-bit-modep-and-fs/gs

(defthm wime32-when-64-bit-modep-and-fs/gs
 (implies
  (or (equal seg-reg 4) (equal seg-reg 5))
  (equal (wime32 0 eff-addr
                 seg-reg val check-alignment? x86
                 :mem-ptr? mem-ptr?)
         (b* (((mv flg lin-addr)
               (b* (((mv base & &)
                     (segment-base-and-bounds 0 seg-reg x86))
                    (lin-addr (i64 (+ base (n64 eff-addr)))))
                 (if (canonical-address-p lin-addr)
                     (mv nil lin-addr)
                   (mv (list :non-canonical-address lin-addr)
                       0))))
              ((when flg) (mv flg x86))
              ((unless (or (not check-alignment?)
                           (address-aligned-p lin-addr 4 mem-ptr?)))
               (mv (list :unaligned-linear-address lin-addr)
                   x86)))
           (wiml32 lin-addr val x86)))))