Gen-write-function
- Signature
(gen-write-function &key size signed?
check-alignment?-var mem-ptr?-var)
→
*- Arguments
- size — Guard (natp size).
- signed? — Guard (booleanp signed?).
- check-alignment?-var — Guard (booleanp check-alignment?-var).
- mem-ptr?-var — Guard (booleanp mem-ptr?-var).
Definitions and Theorems
Function: gen-write-function-fn
(defun gen-write-function-fn
(size signed?
check-alignment?-var mem-ptr?-var)
(declare (xargs :guard (and (natp size)
(booleanp signed?)
(booleanp check-alignment?-var)
(booleanp mem-ptr?-var))))
(let ((__function__ 'gen-write-function))
(declare (ignorable __function__))
(b*
((size-str (symbol-name (if (< size 10)
(acl2::packn (list 0 size))
(acl2::packn (list size)))))
(fn (str::cat (if signed? "WIME" "WME")
size-str))
(fn-name (intern$ fn "X86ISA"))
(fn-call
(cons
fn-name
(cons
'proc-mode
(cons
'eff-addr
(cons
'seg-reg
(cons 'val
(append (and check-alignment?-var
'(check-alignment?))
(cons 'x86
(and mem-ptr?-var
'(:mem-ptr? mem-ptr?))))))))))
(lin-mem-fn (str::cat (if signed? "WIML" "WML")
size-str))
(lin-mem-fn-name (intern$ lin-mem-fn "X86ISA"))
(short-doc-string
(str::cat "Write "
(if signed? "a signed " "an unsigned ")
(str::nat-to-dec-string size)
"-bit value to memory via an effective address."))
(long-doc-string
(str::cat
"<p>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 @(see "
lin-mem-fn
") is
called.</p>
<p>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.</p>")))
(cons
'define
(cons
fn-name
(cons
(cons
'(proc-mode :type (integer 0 4))
(cons
'(eff-addr :type (signed-byte 64))
(cons
'(seg-reg :type (integer 0 5))
(cons
(cons
'val
(cons
':type
(cons (cons (if signed? 'signed-byte 'unsigned-byte)
(cons size 'nil))
'nil)))
(append
(and check-alignment?-var
'((check-alignment? booleanp)))
(cons 'x86
(and mem-ptr?-var
'(&key ((mem-ptr? booleanp) 'nil)))))))))
(cons
':inline
(cons
't
(cons
':no-function
(cons
't
(cons
':returns
(cons
'(mv flg (x86-new x86p :hyp (x86p x86)))
(cons
':parents
(cons
'(top-level-memory)
(cons
':short
(cons
short-doc-string
(cons
':long
(cons
long-doc-string
(cons
(cons
'b*
(cons
(cons
'((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))
(cons
(cons
'(mv flg lin-addr)
(cons
(cons
'ea-to-la
(cons
'proc-mode
(cons 'eff-addr
(cons 'seg-reg
(cons (/ size 8) '(x86))))))
'nil))
(cons
'((when flg) (mv flg x86))
(and
check-alignment?-var
(cons
(cons
(cons
'unless
(cons
(cons
'or
(cons
'(not check-alignment?)
(cons
(cons
'address-aligned-p
(cons
'lin-addr
(cons
(/ size 8)
(cons
(if mem-ptr?-var 'mem-ptr? 'nil)
'nil))))
'nil)))
'nil))
'((mv
(list
:unaligned-linear-address lin-addr)
x86)))
'nil)))))
(cons
(cons lin-mem-fn-name '(lin-addr val x86))
'nil)))
(cons
'///
(cons
(cons
'defrule
(cons
(mk-name
fn "-WHEN-64-BIT-MODEP-AND-NOT-FS/GS")
(cons
(cons
'implies
(cons
(cons
'and
(cons
'(not (equal seg-reg 4))
(cons
'(not (equal seg-reg 5))
(cons
'(canonical-address-p eff-addr)
(and
check-alignment?-var
(cons
(cons
'or
(cons
'(not check-alignment?)
(cons
(cons
'address-aligned-p
(cons
'eff-addr
(cons
(/ size 8)
(cons
(if mem-ptr?-var 'mem-ptr?
'nil)
'nil))))
'nil)))
'nil))))))
(cons
(cons
'equal
(cons
(search-and-replace-once 'proc-mode
'0
fn-call)
(cons
(cons
lin-mem-fn-name '(eff-addr val x86))
'nil)))
'nil)))
'nil)))
(append
(and
check-alignment?-var
(cons
(cons
'defrule
(cons
(mk-name
fn
"-UNALIGNED-WHEN-64-BIT-MODEP-AND-NOT-FS/GS")
(cons
(cons
'implies
(cons
(cons
'and
(cons
'(not (equal seg-reg 4))
(cons
'(not (equal seg-reg 5))
(cons
(cons
'not
(cons
(cons
'or
(cons
'(not check-alignment?)
(cons
(cons
'address-aligned-p
(cons
'eff-addr
(cons
(/ size 8)
(cons
(if mem-ptr?-var 'mem-ptr?
'nil)
'nil))))
'nil)))
'nil))
'((canonical-address-p
eff-addr))))))
(cons
(cons
'equal
(cons
(search-and-replace-once 'proc-mode
'0
fn-call)
'((list
(list :unaligned-linear-address
eff-addr)
x86))))
'nil)))
'nil)))
'nil))
(cons
(cons
'defrule
(cons
(mk-name fn "-WHEN-64-BIT-MODEP-AND-FS/GS")
(cons
(cons
'implies
(cons
'(or (equal seg-reg 4)
(equal seg-reg 5))
(cons
(cons
'equal
(cons
(search-and-replace-once 'proc-mode
'0
fn-call)
(cons
(cons
'b*
(cons
(cons
'((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))))
(cons
'((when flg) (mv flg x86))
(and
check-alignment?-var
(cons
(cons
(cons
'unless
(cons
(cons
'or
(cons
'(not check-alignment?)
(cons
(cons
'address-aligned-p
(cons
'lin-addr
(cons
(/ size 8)
(cons (if mem-ptr?-var
'mem-ptr?
'nil)
'nil))))
'nil)))
'nil))
'((mv
(list
:unaligned-linear-address
lin-addr)
x86)))
'nil))))
(cons (cons lin-mem-fn-name
'(lin-addr val x86))
'nil)))
'nil)))
'nil)))
'(:hints
(("Goal"
:in-theory (e/d (ea-to-la) nil)))))))
'nil)))))))))))))))))))))))
