		Search-engine friendly clone of the ACL2 documentation.

Floating-point-converts

Sse-cvt-int-to-fp

Signature
(sse-cvt-int-to-fp op mxcsr exp-width frac-width) → (mv * * *)
Arguments: op — Guard (integerp op).; exp-width — Guard (posp exp-width).; frac-width — Guard (posp frac-width).

Definitions and Theorems

Function: sse-cvt-int-to-fp

(defun sse-cvt-int-to-fp (op mxcsr exp-width frac-width)
 (declare (type (unsigned-byte 32) mxcsr))
 (declare (xargs :guard (and (integerp op)
                             (posp exp-width)
                             (posp frac-width))))
 (let ((__function__ 'sse-cvt-int-to-fp))
  (declare (ignorable __function__))
  (b*
   ((mxcsr (mbe :logic (loghead 32 mxcsr)
                :exec mxcsr))
    (rc (mbe :logic (part-select mxcsr
                                 :low 13
                                 :high (1+ 13))
             :exec (logand 3 (ash mxcsr (- 13)))))
    (bias
     (nfix
        (ec-call (rtl::bias (list nil (1+ frac-width) exp-width)))))
    (int-to-rat (rat-round op rc bias exp-width frac-width))
    (sign (cond ((> int-to-rat 0) 0)
                ((< int-to-rat 0) 1)
                (t (if (int= rc 1) 1 0))))
    (pe (not (= op int-to-rat)))
    (mxcsr (if pe (!mxcsrbits->pe 1 mxcsr) mxcsr))
    (pm (equal (mxcsrbits->pm mxcsr) 1))
    ((when (and pe (not pm)))
     (mv 'precision-exception-is-not-masked
         0 mxcsr))
    (fp-result (rat-to-fp int-to-rat sign
                          nil nil nil rc exp-width frac-width)))
   (mv nil fp-result mxcsr))))

Theorem: integerp-result-sse-cvt-int-to-fp

(defthm integerp-result-sse-cvt-int-to-fp
  (integerp
       (mv-nth 1
               (sse-cvt-int-to-fp op mxcsr exp-width frac-width)))
  :rule-classes :type-prescription)

Theorem: n32p-mxcsr-sse-cvt-int-to-fp

(defthm n32p-mxcsr-sse-cvt-int-to-fp
 (unsigned-byte-p
      32
      (mv-nth 2
              (sse-cvt-int-to-fp op mxcsr exp-width frac-width)))
 :rule-classes
 (:rewrite
  (:type-prescription
   :corollary
   (natp (mv-nth 2
                 (sse-cvt-int-to-fp op mxcsr exp-width frac-width)))
   :hints
   (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp))))
  (:linear
   :corollary
   (and
     (<= 0
         (mv-nth 2
                 (sse-cvt-int-to-fp op mxcsr exp-width frac-width)))
     (< (mv-nth 2
                (sse-cvt-int-to-fp op mxcsr exp-width frac-width))
        4294967296))
   :hints
   (("Goal"
        :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))