|
|
|---|
|
|
|
|---|
(x86-pushf proc-mode start-rip temp-rip
prefixes rex-byte opcode modr/m sib x86)
→
x86Function:
(defun x86-pushf (proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86) (declare (xargs :stobjs (x86))) (declare (type (integer 0 4) proc-mode) (type (signed-byte 48) start-rip) (type (signed-byte 48) temp-rip) (type (unsigned-byte 52) prefixes) (type (unsigned-byte 8) rex-byte) (type (unsigned-byte 8) opcode) (type (unsigned-byte 8) modr/m) (type (unsigned-byte 8) sib)) (declare (ignorable proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib)) (declare (xargs :guard (and (prefixes-p prefixes) (modr/m-p modr/m) (sib-p sib) (rip-guard-okp proc-mode temp-rip)))) (let ((__function__ 'x86-pushf)) (declare (ignorable __function__)) (b* ((?ctx 'x86-pushf)) (b* (((the (integer 1 8) operand-size) (select-operand-size proc-mode nil rex-byte nil prefixes t t nil x86)) (rsp (read-*sp proc-mode x86)) ((mv flg new-rsp) (add-to-*sp proc-mode rsp (- operand-size) x86)) ((when flg) (!!fault-fresh :ss 0 :push flg)) ((the (unsigned-byte 32) eflags) (rflags x86)) ((the (unsigned-byte 32) eflags) (case operand-size (2 (logand 65535 eflags)) (otherwise (logand 3997695 eflags)))) ((mv flg x86) (wme-size-opt proc-mode operand-size (the (signed-byte 48) new-rsp) 2 eflags (alignment-checking-enabled-p x86) x86 :mem-ptr? nil)) ((when flg) (!!ms-fresh :wme-size-opt flg)) (x86 (write-*sp proc-mode new-rsp x86)) (x86 (write-*ip proc-mode temp-rip x86))) x86))))
Theorem:
(defthm x86p-of-x86-pushf (implies (x86p x86) (b* ((x86 (x86-pushf proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)