Write-canonical-address-to-memory-user-exec
- Signature
(write-canonical-address-to-memory-user-exec
lin-addr canonical-address x86)
→
(mv * x86)
Definitions and Theorems
Function: write-canonical-address-to-memory-user-exec$inline
(defun write-canonical-address-to-memory-user-exec$inline
(lin-addr canonical-address x86)
(declare (xargs :stobjs (x86)))
(declare (type (signed-byte 48) lin-addr)
(type (signed-byte 48)
canonical-address))
(declare (xargs :guard (and (canonical-address-p lin-addr)
(canonical-address-p (+ 7 lin-addr))
(app-view x86))))
(if (mbt (and (app-view x86)
(canonical-address-p (+ 7 lin-addr))))
(b* (((the (unsigned-byte 32)
canonical-address-low-nat)
(n32 canonical-address))
((the (signed-byte 32)
canonical-address-high-int)
(mbe :logic (n16-to-i16 (part-select canonical-address
:low 32
:high 47))
:exec (the (signed-byte 16)
(ash canonical-address -32))))
((mv flg0 x86)
(wml32 lin-addr canonical-address-low-nat x86))
((the (signed-byte 49) next-addr)
(+ 4 lin-addr))
((when (mbe :logic (not (canonical-address-p next-addr))
:exec (<= 140737488355328
(the (signed-byte 49) next-addr))))
(mv 'wml64-canonical-address-user-view
x86))
((mv flg1 x86)
(wiml32 next-addr
canonical-address-high-int x86))
((when (or flg0 flg1))
(mv 'wml64-canonical-address-user-view
x86)))
(mv nil x86))
(mv 'unreachable x86)))
