x87 Instructions
Function:
(defun fcw-rc (fcw) (declare (xargs :guard (natp fcw))) (case (bits fcw 11 10) (0 'rne) (1 'rdn) (2 'rup) (3 'rtz)))
Function:
(defun fcw-pc (fcw) (declare (xargs :guard (natp fcw))) (case (bits fcw 9 8) ((0 1) 24) (2 53) (3 64)))
Function:
(defun es nil (declare (xargs :guard t)) 7)
Function:
(defun bb nil (declare (xargs :guard t)) 15)
Function:
(defun c1 nil (declare (xargs :guard t)) 9)
Function:
(defun set-es (fsw) (declare (xargs :guard (natp fsw))) (set-flag (bb) (set-flag (es) fsw)))
Function:
(defun clear-c1 (fsw) (declare (xargs :guard (natp fsw))) (logand fsw 65023))
Function:
(defun x87-binary-pre-comp-excp (op a af b bf) (declare (xargs :guard (and (member op '(add sub mul div)) (encodingp a af) (encodingp b bf)))) (if (or (snanp a af) (unsupp a af) (snanp b bf) (unsupp b bf)) (set-flag (ibit) 0) (if (or (qnanp a af) (qnanp b bf)) 0 (if (binary-undefined-p op a af b bf) (set-flag (ibit) 0) (if (and (eql op 'div) (zerp b bf) (not (infp a af))) (set-flag (zbit) 0) (if (or (denormp a af) (pseudop a af) (denormp b bf) (pseudop b bf)) (set-flag (dbit) 0) 0))))))
Function:
(defun convert-nan-to-ep (x f) (declare (xargs :guard (and (encodingp x f) (<= (prec f) 64)))) (cat (sgnf x f) 1 (1- (expt 2 15)) 15 1 1 (manf x f) (1- (prec f)) 0 (- 64 (prec f))))
Function:
(defun x87-binary-pre-comp-val (op a af b bf) (declare (xargs :guard (and (member op '(add sub mul div)) (encodingp a af) (encodingp b bf) (<= (prec af) 64) (<= (prec bf) 64)))) (let ((aep (convert-nan-to-ep a af)) (bep (convert-nan-to-ep b bf))) (if (nanp a af) (if (nanp b bf) (if (> (sigf aep (ep)) (sigf bep (ep))) (qnanize aep (ep)) (if (< (sigf aep (ep)) (sigf bep (ep))) (qnanize bep (ep)) (if (= (sgnf aep (ep)) 0) (qnanize (convert-nan-to-ep a af) (ep)) (qnanize (convert-nan-to-ep b bf) (ep))))) (qnanize aep (ep))) (if (nanp b bf) (qnanize bep (ep)) (if (binary-undefined-p op a af b bf) (indef (ep)) nil)))))
Function:
(defun x87-binary-pre-comp (op a af b bf) (declare (xargs :guard (and (member op '(add sub mul div)) (encodingp a af) (encodingp b bf) (<= (prec af) 64) (<= (prec bf) 64)))) (mv (x87-binary-pre-comp-val op a af b bf) (x87-binary-pre-comp-excp op a af b bf)))
Function:
(defun x87-post-comp (u fcw) (declare (xargs :guard (and (real/rationalp u) (not (= u 0)) (natp fcw)))) (let* ((rmode (fcw-rc fcw)) (r (rnd u rmode (fcw-pc fcw))) (rsgn (if (< r 0) 1 0)) (flags (if (= r u) 0 (set-flag (pbit) 0)))) (if (> (abs r) (lpn (ep))) (let ((flags (set-flag (obit) flags))) (if (= (bitn fcw (obit)) 1) (let ((flags (set-flag (pbit) flags))) (if (or (and (eql rmode 'rdn) (> r 0)) (and (eql rmode 'rup) (< r 0)) (eql rmode 'rtz)) (mv (nencode (* (sgn r) (lpn (ep))) (ep)) flags) (mv (iencode rsgn (ep)) (set-flag (c1) flags)))) (let ((s (* r (expt 2 (- (* 3 (expt 2 13))))))) (if (> (abs s) (lpn (ep))) (mv (iencode rsgn (ep)) (set-flag (c1) (set-flag (pbit) flags))) (mv (nencode s (ep)) (if (> (abs r) (abs u)) (set-flag (c1) flags) flags)))))) (if (< (abs r) (spn (ep))) (if (= (bitn fcw (ubit)) 1) (let ((d (drnd u rmode (ep)))) (if (= d u) (mv (dencode d (ep)) flags) (let ((flags (set-flag (pbit) (set-flag (ubit) flags)))) (if (= d 0) (mv (zencode rsgn (ep)) flags) (if (= (abs d) (spn (ep))) (mv (nencode d (ep)) (set-flag (c1) flags)) (mv (dencode d (ep)) (if (> (abs d) (abs u)) (set-flag (c1) flags) flags))))))) (let ((flags (set-flag (ubit) flags)) (s (* r (expt 2 (* 3 (expt 2 13)))))) (if (< (abs s) (spn (ep))) (mv (zencode rsgn (ep)) (set-flag (pbit) flags)) (mv (nencode s (ep)) (if (> (abs r) (abs u)) (set-flag (c1) flags) flags))))) (mv (nencode r (ep)) (if (> (abs r) (abs u)) (set-flag (c1) flags) flags))))))
Function:
(defun x87-binary-comp (op a af b bf fcw) (declare (xargs :guard (and (member op '(add sub mul div)) (encodingp a af) (encodingp b bf) (natp fcw)))) (if (or (infp a af) (if (eql op 'div) (zerp b bf) (infp b bf))) (mv (iencode (binary-inf-sgn op a af b bf) (ep)) 0) (let* ((asgn (sgnf a af)) (bsgn (sgnf b bf)) (aval (decode a af)) (bval (decode b bf)) (u (binary-eval op aval bval))) (if (or (and (eql op 'div) (infp b bf)) (= u 0)) (mv (zencode (binary-zero-sgn op asgn bsgn (fcw-rc fcw)) (ep)) 0) (x87-post-comp u fcw)))))
Function:
(defun x87-binary-spec (op a af b bf fcw fsw) (declare (xargs :guard (and (member op '(add sub mul div)) (encodingp a af) (encodingp b bf) (<= (prec af) 64) (<= (prec bf) 64) (natp fcw) (natp fsw)))) (let ((fsw (clear-c1 fsw))) (mv-let (result pre-flags) (x87-binary-pre-comp op a af b bf) (if (unmasked-excp-p pre-flags fcw) (mv nil (set-es (logior fsw pre-flags))) (if result (mv result (logior fsw pre-flags)) (mv-let (result post-flags) (x87-binary-comp op a af b bf fcw) (mv result (if (unmasked-excp-p post-flags fcw) (set-es (logior (logior fsw pre-flags) post-flags)) (logior (logior fsw pre-flags) post-flags)))))))))
Function:
(defun x87-sqrt-pre-comp-excp (a f) (declare (xargs :guard (encodingp a f))) (if (or (unsupp a f) (snanp a f)) (set-flag (ibit) 0) (if (qnanp a f) 0 (if (and (not (zerp a f)) (= (sgnf a f) 1)) (set-flag (ibit) 0) (if (or (denormp a f) (pseudop a f)) (set-flag (dbit) 0) 0)))))
Function:
(defun x87-sqrt-pre-comp-val (a f) (declare (xargs :guard (and (encodingp a f) (<= (prec f) 64)))) (if (nanp a f) (qnanize (convert-nan-to-ep a f) (ep)) (if (and (not (zerp a f)) (= (sgnf a f) 1)) (indef (ep)) nil)))
Function:
(defun x87-sqrt-pre-comp (a f) (declare (xargs :guard (and (encodingp a f) (<= (prec f) 64)))) (mv (x87-sqrt-pre-comp-val a f) (x87-sqrt-pre-comp-excp a f)))
Function:
(defun x87-sqrt-comp (a f fcw) (declare (xargs :guard (and (encodingp a f) (or (zerp a f) (= (sgnf a f) 0)) (<= (prec f) 64) (natp fcw)))) (if (or (infp a f) (zerp a f)) (mv a 0) (x87-post-comp (qsqrt (decode a f) 66) fcw)))
Function:
(defun x87-sqrt-spec (a f fcw fsw) (declare (xargs :guard (and (encodingp a f) (<= (prec f) 64) (natp fcw) (natp fsw)))) (let ((fsw (clear-c1 fsw))) (mv-let (result pre-flags) (x87-sqrt-pre-comp a f) (if (unmasked-excp-p pre-flags fcw) (mv nil (set-es (logior fsw pre-flags))) (if result (mv result (logior fsw pre-flags)) (mv-let (result post-flags) (x87-sqrt-comp a f fcw) (mv result (if (unmasked-excp-p post-flags fcw) (set-es (logior (logior fsw pre-flags) post-flags)) (logior (logior fsw pre-flags) post-flags)))))))))