		Search-engine friendly clone of the ACL2 documentation.

Fast-logext

Fast-logext8

Optimized implementation of 8-bit sign-extension.

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

Definitions and Theorems

Function: fast-logext8$inline

(defun fast-logext8$inline (x)
 (declare (xargs :guard (integerp x)))
 (let ((__function__ 'fast-logext8))
  (declare (ignorable __function__))
  (mbe
   :logic (logext 8 x)
   :exec (the (signed-byte 8)
              (- (the (unsigned-byte 8)
                      (logxor (the (unsigned-byte 8) (logand 255 x))
                              (the (unsigned-byte 8) 128)))
                 128)))))