Below we will discuss binary arithmetic. This is important because the iJVM operations are on 32-bit numbers.
Given the importance of binary arithmetic, there is language support for it in ACL2. In addition, since ACL2 has been used on many industrial designs, there are publicly available "books" on binary arithmetic. We are going to use the book logops-definitions in the books/ihs/ directory of the ACL2 distribution. If you need a refresher or a reference on binary numbers, please consult the Hennessy and Patterson book.
Instead of manipulating bit-vectors directly, we are going to manipulate integers. The next few paragraphs explain how one can use integers instead of bit-vectors. First, we are going to discussed unsigned bit-vectors and then signed bit-vectors.
First, any integer can be thought of as an n-bit vector: just write the number in two's complement binary and look at the n low-order bits, e.g., 13 in binary is ...001101 and the 3 low-order bits are 101. The function (loghead n i) will return the natural number obtained by interpreting the resulting bit vector as an unsigned binary number. For example, (loghead 3 13) is 5, as the unsigned bit vector 101 corresponds to 5. Note that loghead returns numbers, not bit vectors. We can define (loghead n i) to be i (mod 2n). See logops-definitions for the details and note the following examples:
Loghead example (loghead 3 4) (loghead 3 13) (loghead 5 13) (loghead 5 -1) (loghead 5 -32) (loghead 6 -32) |
Value
4
5
13
31
0
0
|
Low order bits = natural number
100 = 4
101 = 5
01101 = 13
11111 = 31
00000 = 0
100000 = 32
|
If we want to deal with signed numbers, then the only difference is in how we interpret integers. As above, any integer can be thought of as an n-bit vector: just write the number in two's complement binary and look at the n low-order bits, but now interpret the result as a signed number. The function (logext n i) will return the integer obtained by interpreting the resulting bit vector as a signed binary number, e.g., 13 in binary ...001101 and the 3 low-order bits are 101. As a two's complement number ...11101 (101 sign extended) is -3. See logops-definitions for the details and note the following examples:
Logext example (logext 3 4) (logext 3 13) (logext 5 13) (logext 5 -1) (logext 5 -32) (logext 6 -32) |
Value
-4
-3
13
-1
0
-32
|
Low order bits = integer
100 = -4
101 = -3
01101 = 13
11111 = -1
00000 = 0
100000 = -32
|
Given the above, we can easily define functions to perform n-bit arithmetic, e.g., a function to performs 32-bit signed addition can be defined as follows:
(defun s32+ (x y)
"32 bit addition"
(logext 32 (+ x y)))
Another common operation is forming a bit vector from other bit vectors, e.g., if hi and lo are two bytes (8 bit vectors), we can construct a short (a 16 bit vector) whose first byte is hi and second byte is lo using logapp as follows (logapp 8 lo hi). (Logapp n i j) is defined in the logops-definitions books to be (loghead n i) + (j * 2n). Logior, logand, etc. are used to or, and, etc. bit vectors. See logops-definitions for details.