		Search-engine friendly clone of the ACL2 documentation.

Peripherals

X86-exec-peripherals

Execute the peripherals

Signature
(x86-exec-peripherals x86) → x86
Returns: x86 — Type (x86p x86), given (x86p x86).

Definitions and Theorems

Function: x86-exec-peripherals

(defun x86-exec-peripherals (x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard t))
 (let ((__function__ 'x86-exec-peripherals))
  (declare (ignorable __function__))
  (b*
   (((when (app-view x86)) x86)
    (time-stamp-counter (n64 (1+ (time-stamp-counter x86))))
    (x86 (!time-stamp-counter time-stamp-counter x86))
    (x86 (if (app-view x86)
             x86
           (wm-low-64 256 time-stamp-counter x86)))
    (last-clock-event (last-clock-event x86))
    (x86 (if (and (> last-clock-event 100000)
                  (equal (rflagsbits->intf (rflags x86))
                         1)
                  (not (inhibit-interrupts-one-instruction x86))
                  (not (equal (memi 264 x86) 0))
                  (not (fault x86)))
             (b* ((x86 (!last-clock-event 0 x86))
                  (x86 (!fault (cons '(:interrupt 32) (fault x86))
                               x86)))
               x86)
           (!last-clock-event (1+ last-clock-event)
                              x86)))
    (x86 (b* ((tty-byte-valid (not (equal (memi 1017 x86) 0)))
              ((when (not tty-byte-valid)) x86)
              (tty-output-byte (memi 1016 x86))
              (x86 (!memi 1017 0 x86))
              (x86 (write-tty tty-output-byte x86)))
           x86))
    (x86 (b* ((tty-write-byte-valid (not (equal (memi 1019 x86) 0)))
              ((when tty-write-byte-valid) x86)
              ((mv tty-input x86) (read-tty x86))
              ((when (equal tty-input nil)) x86)
              (x86 (!memi 1018 tty-input x86))
              (x86 (!memi 1019 1 x86)))
           x86)))
   x86)))

Theorem: x86p-of-x86-exec-peripherals

(defthm x86p-of-x86-exec-peripherals
  (implies (x86p x86)
           (b* ((x86 (x86-exec-peripherals x86)))
             (x86p x86)))
  :rule-classes :rewrite)