|
|
|---|
|
|
|
|---|
Specification for the
(sal/shl-spec size dst src input-rflags) → (mv * * *)
Source: Intel Manual, Volume 2B, Instruction Set Reference (N-Z).
The shift arithmetic left (SAL) and shift logical left (SHL) instructions perform the same operation; they shift the bits in the destination operand to the left (toward more significant bit locations). For each shift count, the most significant bit of the destination operand is shifted into the CF flag, and the least significant bit is cleared. The OF flag is affected only on 1-bit shifts. For left shifts, the OF flag is set to 0 if the most-significant bit of the result is the same as the CF flag (that is, the top two bits of the original operand were the same); otherwise, it is set to 1.
Function:
(defun sal/shl-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 (sal/shl-spec-8 dst src input-rflags)) (2 (sal/shl-spec-16 dst src input-rflags)) (4 (sal/shl-spec-32 dst src input-rflags)) (8 (sal/shl-spec-64 dst src input-rflags)) (otherwise (mv 0 0 0))))
Theorem:
(defthm natp-mv-nth-0-sal/shl-spec (natp (mv-nth 0 (sal/shl-spec size dst src input-rflags))) :rule-classes :type-prescription)
Theorem:
(defthm n32p-mv-nth-1-sal/shl-spec (unsigned-byte-p 32 (mv-nth 1 (sal/shl-spec size dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 1 (sal/shl-spec size dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 1 (sal/shl-spec size dst src input-rflags))) (< (mv-nth 1 (sal/shl-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-sal/shl-spec (unsigned-byte-p 32 (mv-nth 2 (sal/shl-spec size dst src input-rflags))) :rule-classes (:rewrite (:type-prescription :corollary (natp (mv-nth 2 (sal/shl-spec size dst src input-rflags))) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p natp)))) (:linear :corollary (and (<= 0 (mv-nth 2 (sal/shl-spec size dst src input-rflags))) (< (mv-nth 2 (sal/shl-spec size dst src input-rflags)) 4294967296)) :hints (("Goal" :in-theory '(unsigned-byte-p integer-range-p (:e expt)))))))