|
|
|---|
|
|
|
|---|
Specification for the
(sar-spec size dst src input-rflags) → (mv * * *)
Source: Intel Manual, Volume 2B, Instruction Set Reference (N-Z).
The shift arithmetic right (SAR) and shift logical right (SHR) instructions shift the bits of the destination operand to the right (toward less significant bit locations). For each shift count, the least significant bit of the destination operand is shifted into the CF flag, and the most significant bit is either set or cleared depending on the instruction type. The SAR instruction sets or clears the most significant bit to correspond to the sign (most significant bit) of the original value in the destination operand. In effect, the SAR instruction fills the empty bit position s shifted value with the sign of the unshifted value. ... The OF flag is affected only on 1-bit shifts. For the SAR instruction, the OF flag is cleared for all 1-bit shifts. For the SHR instruction, the OF flag is set to the most-significant bit of the original operand.
Function:
(defun sar-spec$inline (size dst src input-rflags) (declare (type (member 1 2 4 8) size) (type (unsigned-byte 32) input-rflags)) (declare (xargs :guard (and (n06p src) (case size (1 (n08p dst)) (2 (n16p dst)) (4 (n32p dst)) (8 (n64p dst)) (otherwise nil))))) (case size (1 (sar-spec-8 dst src input-rflags)) (2 (sar-spec-16 dst src input-rflags)) (4 (sar-spec-32 dst src input-rflags)) (8 (sar-spec-64 dst src input-rflags)) (otherwise (mv 0 0 0))))
Theorem:
(defthm natp-mv-nth-0-sar-spec (natp (mv-nth 0 (sar-spec size dst src input-rflags))) :rule-classes :type-prescription)
Theorem:
(defthm n32p-mv-nth-1-sar-spec (unsigned-byte-p 32 (mv-nth 1 (sar-spec size dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (sar-spec size dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (sar-spec size dst src input-rflags))) (< (mv-nth 1 (sar-spec size dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))
Theorem:
(defthm n32p-mv-nth-2-sar-spec (unsigned-byte-p 32 (mv-nth 2 (sar-spec size dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (sar-spec size dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (sar-spec size dst src input-rflags))) (< (mv-nth 2 (sar-spec size dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))