		Search-engine friendly clone of the ACL2 documentation.

Bitops/fast-logrev

Fast-logrev-u64

Faster implementation of (logrev 64 x) for 64-bit unsigned values.

Signature
(fast-logrev-u64 x) → reverse-x

We could probably do better using the Reverse an N-bit quantity in parallel in 5 * lg(N) operations algorithm, but this is at least pretty fast.

(let ((x     #xfeedd00ddeadbeef)
      (times 10000000))
  ;; 21.744 seconds, 3.2 GB
  (time (loop for i fixnum from 1 to times do (logrev 64 x)))
  ;; .767 seconds, 320 MB
  (time (loop for i fixnum from 1 to times do (fast-logrev-u64 x))))

Definitions and Theorems

Function: fast-logrev-u64

(defun fast-logrev-u64 (x)
  (declare (type (unsigned-byte 64) x))
  (let ((__function__ 'fast-logrev-u64))
    (declare (ignorable __function__))
    (mbe :logic (logrev 64 x)
         :exec
         (b* (((the (unsigned-byte 32) low)
               (logand x 4294967295))
              ((the (unsigned-byte 32) high)
               (ash x -32))
              ((the (unsigned-byte 32) rlow)
               (fast-logrev-u32 low))
              ((the (unsigned-byte 32) rhigh)
               (fast-logrev-u32 high)))
           (the (unsigned-byte 64)
                (logior (the (unsigned-byte 64) (ash rlow 32))
                        rhigh))))))