		Search-engine friendly clone of the ACL2 documentation.

Fast-logext

(fast-logext n x) interprets the least significant n bits of the integer x as a signed number of width n.

This is logically identical to logext. But, for better performance we adopt a method from Sean Anderson's bit twiddling hacks page, viz:

unsigned n;                  // number of bits representing the number in x
int x;                       // sign extend this n-bit number to r
int r;                       // resulting sign-extended number
int const m = 1U << (n - 1); // mask can be pre-computed if n is fixed
x = x & ((1U << n) - 1);     // (Skip this if bits in x above position n are already zero.)
r = (x ^ m) - m;

fast-logext is actually a macro. Generally it expands into a call of fast-logext-fn, which carries out the above computation. But in the common cases where n is explicitly 8, 16, 32, or 64, it instead expands into a call of a specialized, inlined function.

Macro: fast-logext

(defmacro fast-logext (n x)
  (cond ((eql n 8)
         (cons 'fast-logext8 (cons x 'nil)))
        ((eql n 16)
         (cons 'fast-logext16 (cons x 'nil)))
        ((eql n 32)
         (cons 'fast-logext32 (cons x 'nil)))
        ((eql n 64)
         (cons 'fast-logext64 (cons x 'nil)))
        (t (cons 'fast-logext-fn
                 (cons n (cons x 'nil))))))

Subtopics

Fast-logext-exec: Executable definition of fast-logext in the general case.
Fast-logext64: Optimized implementation of 64-bit sign-extension.
Fast-logext16: Optimized implementation of 16-bit sign-extension.
Fast-logext8: Optimized implementation of 8-bit sign-extension.
Fast-logext32: Optimized implementation of 32-bit sign-extension.
Fast-logext-fn: Implementation of fast-logext in the general case.