		Search-engine friendly clone of the ACL2 documentation.

Fibonacci32-cosim

X86isa-one-fib32-cosim

Signature
(x86isa-one-fib32-cosim input start-address halt-address xrun-limit x86) → (mv * * x86)

Definitions and Theorems

Function: x86isa-one-fib32-cosim

(defun
 x86isa-one-fib32-cosim
 (input start-address
        halt-address xrun-limit x86)
 (declare (xargs :stobjs (x86)))
 (declare (type (unsigned-byte 8) input)
          (type (signed-byte 48) start-address)
          (type (signed-byte 48) halt-address)
          (type (unsigned-byte 50) xrun-limit))
 (let
  ((__function__ 'x86isa-one-fib32-cosim))
  (declare (ignorable __function__))
  (b*
   ((ctx __function__)
    ((mv flg x86)
     (init-x86-state
      nil start-address
      (cons (cons '0 input)
            (cons '(3 . 3221223764)
                  (cons '(1 . 4294967295)
                        (cons (cons '2 input)
                              (cons '(7 . 7901)
                                    (cons (cons '6 input)
                                          '((5 . 3221223576)
                                            (4 . 3221223552))))))))
      nil nil '((1 . 27) (2 . 35) (3 . 35))
      (acons 1 0 (acons 2 0 (acons 3 0 nil)))
      (acons 1 65535
             (acons 2 4294967295 (acons 3 4294967295 nil)))
      (acons 1
             (!code-segment-descriptor-attributesbits->d 1 0)
             (acons 2
                    (!data-segment-descriptor-attributesbits->w 1 0)
                    nil))
      642
      (acons 3221223552 input *fibonacci32-binary*)
      x86))
    ((when flg)
     (let ((x86 (!!ms-fresh :init-x86-state-error flg)))
          (mv nil 0 x86)))
    ((mv steps x86)
     (time$ (x86-run-halt-count halt-address
                                xrun-limit x86 xrun-limit)))
    (ok? (check-fib32-output input halt-address x86))
    ((unless ok?) (mv nil 0 x86)))
   (mv t steps x86))))