JML Tutorial - Reasoning about bit-wise operations
Last Modified:
In Java programs (and other languages), integer-like variables of various bit-widths are sometimes used as limited range numbers and sometimes as a collection of bits. For example, the variable may represent a collection of boolean options, each one as a bit, and all together collected into an 8- or 16- or 32- or 64-bit variable. Java has some bit-wise operations for this purpose: bit-wise and, or and exclusive or, and bit-shift left and right.
This would be transparent to verification except for some limitations of solvers.
- Current solvers can treat variables as either numbers or bit-vectors but they cannot convert between them.
- Current solvers do not have general bit operations on numbers, only on bit-vectors. Some limited operations can be emulated: for example shifting by a fixed, known amount can be accomplished by multiplication or division. Solvers do implement numeric operations (addition, etc.) for bit-vectors.
- In general, solving logic problems over bit-vectors takes far longer than solving the equivalent problem over numbers, especially on 64-bit longs. Note that this is the reverse of the situation for implementation code: in Java code, bit-vector operations are sometimes used because they are faster than the corresponding numeric operations (e.g., right shifts are faster than divides).
- OpenJML has the additional current limitation that it translates a whole method either as bit-vectors or as numbers, and not a mixture.
Because of the above considerations, a choice has to be made: should the int-like values in a given proof attempt be translated as bit-vectors or as numbers. Because performance is usually better, OpenJML by default will attempt to verify a method using numbers for the int-like variables, and only use bit-vectors if there are bit-vector operations that cannot be performed on numbers.
The choice between using bit-vectors or not is performed automatically, but the user can force the
choice using the command-line option --esc-bv=true
to use bit-vectors and --esc-bv=false
to use numbers
(the default is --esc-bv=auto
).
The following example verifies successfully, but takes 8-10 times longer (on my machine using Z3 4.3.1) using bitvectors vs not.
// openjml --esc --esc-bv=true T_BVMult.java
public class T_BVMult {
//@ code_java_math
public void test(long i) {
long square = i*i;
//@ assert -16000 < i < 16000 ==> square < Integer.MAX_VALUE;
}
}
The important point for writing specifications is that in situations where using bit-vectors is a performance problem, one wants to keep as much of the program as possible using numbers. To do that, use the following trick: even if the implementation of method A uses bit-vector operations, write the specification so it does not. Then any method B that calls the method A only sees numeric operations in A’s specification (and not the bit-vector operations in A’s implementation), so method B does not need to be verified using bit-vectors. The bit-vector proof is limited to method A.
The following method rounds a number up to the next highest multiple of 16. The implementation uses a non-obvious bit-twiddling trick to do so. The specification expresses the desired outcome more clearly and uses only numeric operations. The successful verification shows that the bit-twiddling trick correctly implements the desired result.
// openjml --esc T_BVRoundUp.java
public class T_BVRoundUp {
//@ requires n <= 0x7ffffff0;
//@ ensures n <= \result <= n+15;
//@ ensures (\result%16) == 0;
//@ pure
//@ code_java_math
public int m1(int n) {
return n + ((-n) & 0x0f);
}
}