X86isa-one-fact-cosim
- Signature
(x86isa-one-fact-cosim input start-address
halt-address xrun-limit sys-view? x86)
→
(mv * x86)- Arguments
- sys-view? — Guard (booleanp sys-view?).
Definitions and Theorems
Function: x86isa-one-fact-cosim
(defun x86isa-one-fact-cosim
(input start-address
halt-address xrun-limit sys-view? x86)
(declare (xargs :stobjs (x86)))
(declare (type (unsigned-byte 50) input)
(type (signed-byte 48) start-address)
(type (signed-byte 48) halt-address)
(type (unsigned-byte 50) xrun-limit))
(declare (xargs :guard (booleanp sys-view?)))
(let ((__function__ 'x86isa-one-fact-cosim))
(declare (ignorable __function__))
(b*
((ctx __function__)
(x86 (if sys-view? (init-sys-view 4202496 x86)
x86))
((mv flg x86)
(init-x86-state-64 nil start-address
(acons 7 input (acons 4 35184372088832 nil))
nil nil nil
nil nil nil 2 *factorial-binary* x86))
((when flg)
(let ((x86 (!!ms-fresh :init-x86-state-64-error flg)))
(mv nil x86)))
(x86 (time$ (x86-run-halt halt-address xrun-limit x86)))
(ok? (check-fact-output input halt-address x86))
((unless ok?) (mv nil x86)))
(mv t x86))))
