GNATprove Tips and Tricks: Bitwise Operations
by Clément Fumex –
The ProofInUse joint laboratory is currently improving the way SPARK deals with modular types and bitwise operators. Until now the SPARK tool was trying its best to translate those into equivalent operations on integers. It is now using native theory of smt-solvers when available resulting in much better support, and guaranteeing state of the art handling of bitwise operations.
The following small examples were not provable until now, and are now handled without any difficulty.
The first example, is a procedure that takes a value in 16bits and gives back its first and second halfs in two 8-bits values. The code uses masks and is straightforward. SPARK proves that the value can be reconstructed from its first and second halfs in the expected way:
procedure Write16 (Val : in Unsigned_16; FstHalf, SndHalf : out Unsigned_8) with
Post => (Val = (Unsigned_16(FstHalf) or Shift_Left(Unsigned_16(SndHalf), 8 )))
is
begin
FstHalf := Unsigned_8 (Val and 16#00FF#);
SndHalf := Unsigned_8 (Shift_Right(Val, 8) and 16#00FF#);
end Write16;Now let's look at a quite well known example: a procedure that swaps its arguments using a succession of xor. SPARK is now able to prove that the three xor did not do anything unexpected and that the arguments were indeed swapped.
procedure swap (a, b : in out Unsigned_32) with
Post => a'Old = b and b'Old = a
is
begin
a := a xor b;
b := a xor b;
a := a xor b;
end swap;How does it work? xor with a given parameter is an involution, i.e., "a xor (a xor b) = b". Hence if we rewrite the three calls to xor to
a' := a xor b;
b' := a' xor b;
a'' := a' xor b';Replacing a' by its value gives us
b' := (a xor b) xor bequal to "a" by involution. And replacing both a' and b' by their values gives us
a'' := (a xor b) xor aequal to "a xor (a xor b)", hence "b".
The last example, that you can find in the well known book "Hacker's Delight", is an expression function that computes the average of two modulars that can not cause overflow. While the body only deals with bitwise operations SPARK can prove that the result is indeed the average:
function Average (a, b : Unsigned_32) return Unsigned_32 is
((a and b) + Shift_Right(a xor b, 1))
with
Post => Average'Result = Unsigned_32( (Unsigned_64(a) + Unsigned_64(b)) / 2 );How does it work?
The main idea behind the algorithm uses the following equalities:
x + y = (x and y) + (x or y) = (x xor y) + 2*(x and y)The first equality is due to the fact that "(x and y)" is the intersection of x's 1-bits and y's 1-bits and that "(x or y)" is their union, hence if you do these two sums by hand, placing "x" above "y" and "(x and y)" above "(x or y)", as in:
x = 1011_0110 x and y = 0010_0010
y = 0010_0011 x or y = 1011_0111
----------------- ---------------------
x+y = 1101_1001 x + y = 1101_1001Switching from the addition to the left to the addition to the right amounts to add some gravity to the formula, indeed, the 1-bits in "x" that were above a 0-bit in "y", "fall down" to the union while the ones that were standing above a 1-bit in "y" stay in the intersection. The main point being that this second sum is obtained by rearranging the bits in the two operands without any changes on the actual computation.
The second equality "(x and y) + (x or y) = (x xor y) + 2*(x and y)" comes from the equality :
x or y = (x xor y) + (x and y)Indeed, the 1-bits in "(x xor y)" are the ones that are in the union but not the intersection. Hence:
(x and y) + (x or y) = (x and y) + (x xor y) + (x and y)
= (x xor y) + 2*(x and y)We then can derive that the average equals to:
(x + y) / 2 = ((x xor y) + 2*(x and y)) / 2
= (x xor y)/2 + (x and y)Now, we use a last trick: unsigned division by two is done by a logical shift right by one, letting us conclude:
(x + y) / 2 = Shift_Right(x xor y, 1) + (x and y)Note that GNATprove can check all these intermediary equalities for you! In particular the correctness of the average function, that is what took me 40 lines to explain, is now proved in less than 1second.