		Search-engine friendly clone of the ACL2 documentation.

Instruction-semantic-functions

Shlx-spec

Specification for the SHLX instruction.

Signature
(shlx-spec size src cnt) → *
Arguments: cnt — Guard (unsigned-byte-p 6 cnt).

Since this instruction does not affect the flags, this function does not take or return flags.

Definitions and Theorems

Function: shlx-spec$inline

(defun shlx-spec$inline (size src cnt)
  (declare (type (member 4 8) size))
  (declare (xargs :guard (unsigned-byte-p 6 cnt)))
  (declare (xargs :guard
                  (case size
                    (4 (n32p src))
                    (8 (n64p src))
                    (otherwise nil))))
  (case size
    (4 (shlx-spec-32 src cnt))
    (8 (shlx-spec-64 src cnt))
    (otherwise 0)))

Theorem: natp-shlx-spec

(defthm natp-shlx-spec
  (natp (shlx-spec size src cnt))
  :rule-classes :type-prescription)

Subtopics

Shlx-spec-64
Shlx-spec-32