Check-nop-output
- Signature
(check-nop-output halt-address x86) → *
- Arguments
- x86 — Output x86 State.
Definitions and Theorems
Function: check-nop-output
(defun check-nop-output (halt-address x86)
(declare (xargs :stobjs (x86)))
(declare (type (signed-byte 48) halt-address))
(let ((__function__ 'check-nop-output))
(declare (ignorable __function__))
(cond
((or
(fault x86)
(not (equal (ms x86)
(cons (cons 'x86-fetch-decode-execute-halt
(cons ':rip (cons halt-address 'nil)))
'nil))))
(cw "~|(ms x86) = ~x0 (fault x86) = ~x1~%"
(ms x86)
(fault x86)))
(t (if (and (equal (rgfi *rax* x86) 0)
(equal (rgfi *rbx* x86) 0)
(equal (rgfi *rcx* x86) 0)
(equal (rgfi *rdx* x86) 0)
(equal (rgfi *rsi* x86) 0)
(equal (rgfi *rdi* x86) 0)
(equal (rgfi *rsp* x86) 0)
(equal (rgfi *r8* x86) 0)
(equal (rgfi *r9* x86) 0)
(equal (rgfi *r10* x86) 0)
(equal (rgfi *r11* x86) 0)
(equal (rgfi *r12* x86) 0)
(equal (rgfi *r13* x86) 0)
(equal (rgfi *r14* x86) 0)
(equal (rgfi *r15* x86) 0)
(equal (rflags x86) 2))
(prog2$ (cw "~|NOP sequences behave as expected.~%")
t)
(cw "~|NOP sequences DO NOT behave as expected!~%"))))))
