		Search-engine friendly clone of the ACL2 documentation.

Logops-definitions

Logext

(logext size i) sign-extends i to a size-bit signed integer.

Signature
(logext size i) → int
Arguments: size — Guard (and (integerp size) (< 0 size)).; i — Guard (integerp i).
Returns: int — Type (integerp int).

logext interprets the least significant size bits of i as a signed, 2's complement integer.

Basic examples:

(logext 4 7)  --> 7        Bottom four bits are 0111
                           Sign bit is 0
                           Sign extension creates {0000......0}111
                           2's complement interpretation: 7.

(logext 3 7)  --> -1       Bottom 3 bits are 111
                           Sign bit is 1
                           Sign extension creates {1111.....1}111
                           2's complement interpretation: -1.

(logext 4 8)  --> -8       Bottom 4 bits are 1000
                           Sign bit is 1
                           Sign extension creates {1111.....1}1000
                           2's complement interpretation: -8.

This function returns a (possibly negative) integer. For consistency with signed-byte-p, size must be strictly greater than 0. In contrast, the related function logextu carries out a sign-extension but only returns the low size bits, i.e., it always returns a natural number.

We specify logext in terms of the size of the result instead of as a bit position because we normally specify integer subranges by the number of significant (including sign) bits.

See also bitops::bitops/fast-logext for a logically identical function that is optimized for better performance.

Definitions and Theorems

Function: logext

(defun logext (size i)
  (declare (type unsigned-byte size))
  (declare (xargs :guard (and (and (integerp size) (< 0 size))
                              (integerp i))))
  (declare (xargs :split-types t))
  (let ((__function__ 'logext))
    (declare (ignorable __function__))
    (let* ((size-1 (- size 1)))
      (declare (type unsigned-byte size-1))
      (logapp size-1
              i (if (logbitp size-1 i) -1 0)))))

Theorem: logext-type

(defthm logext-type
  (b* ((int (logext size i)))
    (integerp int))
  :rule-classes :type-prescription)

Subtopics

Fast-logext: (fast-logext n x) interprets the least significant n bits of the integer x as a signed number of width n.
Ihs/logext-lemmas: Lemmas about logext from the logops-lemmas book.
Logext-basics
Logext*: Recursive definition of logext.