Logops-byte-functions
A portable implementation and extension of Common Lisp byte
functions.
The proposed Common Lisp standard [X3J13 Draft 14.10] defines a
number of functions that operate on subfields of integers. These subfields are
specified by (BYTE size position), which "indicates a byte of width size
and whose bits have weights 2^{position+size-1} through 2^{pos}, and
whose representation is implementation dependent". Unfortunately, the
standard does not specify what BYTE returns, only that whatever is returned is
understood by the byte manipulation functions LDB, DPB, etc.
This lack of complete specification makes it impossible for ACL2 to specify
the byte manipulation functions of Common Lisp in a portable way. For example
AKCL uses (cons size position) as a byte specifier, whereas another
implementation might use a special data structure to represent (byte size
position). Since any theorem about the ACL2 built-ins is meant to be a
theorem for all Common Lisp implementations, ACL2 cannot define BYTE.
Therefore, we have provided a portable implementation of the byte operations
specified by the draft standard. This behavior of this implementation should
be consistent with every Common Lisp that provides the standard byte
operations. Our byte specifier (bsp size pos) is analogous to CLTL's
(byte size pos), where size and pos are nonnegative integers. Note that
the standard indicates that reading a byte of size 0 returns 0, and writing a
byte of size 0 leaves the destination unchanged.
This table indicates the correspondance between the Common Lisp byte
operations and our portable implementation:
Common Lisp This Implementation
------ ---- ---- --------------
(BYTE size position) (BSP size position)
(BYTE-SIZE bytespec) (BSP-SIZE bsp)
(BYTE-POSITION bytespec) (BSP-POSITION bsp)
(LDB bytespec integer) (RDB bsp integer)
(DPB newbyte bytespec integer) (WRB newbyte bsp integer)
(LDB-TEST bytespec integer) (RDB-TEST bsp integer)
(MASK-FIELD bytespec integer) (RDB-FIELD bsp integer)
(DEPOSIT-FIELD newbyte bytespec integer) (WRB-FIELD newbyte bsp integer)
For more information, see the documentation for the functions listed above.
If you are concerned about the efficiency of this implementation, see the file
ihs/logops-efficiency-hack.lsp for some notes.
Subtopics
- Wrb
- (wrb i bsp j) writes the (bsp-size bsp) low-order bits of i
into the byte of j specified by bsp.
- Rdb
- (rdb bsp i) returns the byte of i specified by bsp.
- Bsp
- (bsp size pos) returns a byte-specifier.
- Bspp
- (bspp bsp) recognizes objects produced by bsp.
- Wrb-field
- (wrb-field i bsp j) is analogous to Common Lisp's (deposit-field
newbyte bytespec integer).
- Bsp-size
- (bsp-size (bsp size pos)) = size
- Bsp-position
- (bsp-position (bsp size pos)) = pos
- Rdb-test
- (rdb-test bsp i) is true iff the field of i specified by
bsp is nonzero.
- Rdb-field
- (rdb-field bsp i) is analogous to Common Lisp's (mask-field bytespec integer).
- Wrb-guard
- (wrb-guard i bsp j) is a macro form of the guards for wrb and wrb-field.
- Rdb-guard
- (rdb-guard bsp i) is a macro form of the guards for rdb, rdb-test, and rdb-field.
