|
|
|---|
|
|
|
|---|
(x86-leave proc-mode start-rip temp-rip
prefixes rex-byte opcode modr/m sib x86)
→
x86Function:
(defun x86-leave (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-leave)) (declare (ignorable __function__)) (b* ((?ctx 'x86-leave)) (b* (((the (integer 2 8) operand-size) (select-operand-size proc-mode nil rex-byte nil prefixes t t nil x86)) (rbp/ebp/bp (rgfi-size operand-size *rbp* 0 x86)) (inst-ac? (alignment-checking-enabled-p x86)) ((mv flg val x86) (rme-size-opt proc-mode operand-size (the (signed-byte 64) (i64 rbp/ebp/bp)) 2 :r inst-ac? x86 :mem-ptr? nil :check-canonicity t)) ((when flg) (!!fault-fresh :ss 0 :pop-error flg)) ((mv flg (the (signed-byte 64) new-rsp)) (add-to-*sp proc-mode (i64 rbp/ebp/bp) operand-size x86)) ((when flg) (!!ms-fresh :invalid-rsp new-rsp)) (x86 (!rgfi-size operand-size *rbp* val rex-byte x86)) (x86 (write-*sp proc-mode new-rsp x86)) (x86 (write-*ip proc-mode temp-rip x86))) x86))))
Theorem:
(defthm x86p-of-x86-leave (implies (x86p x86) (b* ((x86 (x86-leave proc-mode start-rip temp-rip prefixes rex-byte opcode modr/m sib x86))) (x86p x86))) :rule-classes :rewrite)