X86isa-one-fib-cosim
- Signature
(x86isa-one-fib-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-fib-cosim
(defun
x86isa-one-fib-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-fib-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 0 input (acons 4 35184372088832 nil))
nil nil nil
nil nil nil 2 *fibonacci-binary* x86))
((when flg)
(let ((x86 (!!ms-fresh :init-x86-state-64-error flg)))
(mv nil 0 x86)))
((mv steps x86)
(time$ (x86-run-halt-count halt-address
xrun-limit x86 xrun-limit)))
(ok? (check-fib-output input halt-address x86))
((unless ok?) (mv nil steps x86)))
(mv t steps x86))))
