Function:
(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:
(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:
(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 (e/d* (unsigned-byte-p) nil))))))