		Search-engine friendly clone of the ACL2 documentation.

Fast-logext

Fast-logext32

Optimized implementation of 32-bit sign-extension.

Signature
(fast-logext32 x) → *
Arguments: x — Guard (integerp x).

Definitions and Theorems

Function: fast-logext32$inline

(defun fast-logext32$inline (x)
 (declare (xargs :guard (integerp x)))
 (let ((__function__ 'fast-logext32))
  (declare (ignorable __function__))
  (mbe
    :logic (logext 32 x)
    :exec (the (signed-byte 32)
               (- (the (unsigned-byte 32)
                       (logxor (the (unsigned-byte 32)
                                    (logand 4294967295 x))
                               (the (unsigned-byte 32) 2147483648)))
                  2147483648)))))