		Search-engine friendly clone of the ACL2 documentation.

Floating-point-converts

Sse-cvt-fp-to-int

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

Definitions and Theorems

Function: sse-cvt-fp-to-int

(defun sse-cvt-fp-to-int
       (nbytes op mxcsr trunc exp-width frac-width)
 (declare (type (unsigned-byte 32) mxcsr))
 (declare (xargs :guard (and (natp nbytes)
                             (natp op)
                             (booleanp trunc)
                             (posp exp-width)
                             (posp frac-width))))
 (let ((__function__ 'sse-cvt-fp-to-int))
  (declare (ignorable __function__))
  (b* ((mxcsr (mbe :logic (loghead 32 mxcsr)
                   :exec mxcsr))
       ((mv kind sign exp ?implicit frac)
        (fp-decode op exp-width frac-width))
       (daz (logbitp 6 mxcsr))
       ((mv kind exp frac)
        (sse-daz kind exp frac daz))
       ((mv special-ok result invalid)
        (sse-cvt-fp-to-int-special kind nbytes))
       (mxcsr (if invalid (!mxcsrbits->ie 1 mxcsr)
                mxcsr))
       (im (equal (mxcsrbits->im mxcsr) 1))
       ((when (and invalid (not im)))
        (mv 'invalid-operand-exception-is-not-masked
            0 mxcsr)))
   (if special-ok (mv nil result mxcsr)
    (b*
     ((bias
       (nfix
        (ec-call (rtl::bias (list nil (1+ frac-width) exp-width)))))
      (rat (fp-to-rat sign
                      exp frac bias exp-width frac-width))
      (rc (mbe :logic (part-select mxcsr
                                   :low 13
                                   :high (1+ 13))
               :exec (logand 3 (ash mxcsr (- 13)))))
      (rc (if trunc 3 rc))
      (rat-to-int (rat-round-to-int rat rc))
      (nbits (ash nbytes 3))
      (min-signed-int (- (expt 2 (1- nbits))))
      (max-signed-int (1- (expt 2 (1- nbits))))
      (out-of-range (or (< rat-to-int min-signed-int)
                        (> rat-to-int max-signed-int)))
      (mxcsr (if out-of-range (!mxcsrbits->ie 1 mxcsr)
               mxcsr))
      ((when (and out-of-range (not im)))
       (mv 'invalid-operand-exception-is-not-masked
           0 mxcsr))
      ((when out-of-range)
       (mv nil (ash 1 (1- nbits)) mxcsr))
      (pe (not (= rat-to-int 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)))
     (mv nil rat-to-int mxcsr))))))

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

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

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

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