Bug in some shift/rotates

[robdockins]

Consider the following:

xs : [32]
xs = 0xdeadbeef

f : [32] -> [32]
f zs = zs <<< ( [True,False,False]:[3] )

q0 = f xs
q1 = f (rnf (xs @@ [0..31]))
q2 = f      (xs @@ [0..31])

I expect q0, q1 and q2 to all compute the same answer. However, in current master, q2 computes the wrong value. The other shift and rotate operations are also broken in similar ways. Probably, the culprit is the code path that computes results when both arguments of a shift or rotate are unpacked bit vectors, as the example starts working correctly when either argument is packed.

[brianhuffman]

I just added some putStrLns to the barrelShifter function to get some tracing output. It appears that the n parameter to the go inner function does not take the values 3, 2, 1 as you'd expect for a 3-bit shift amount, but rather it takes the values 32, 31, 30. If you change the type of xs in the example from [32] to [48] (for example) then n takes the values 48, 47, 46.

So it appears that the "number of bits in shift amount" parameter to barrelShifter is simply being passed the width of the number being shifted instead of the width of the shift amount.

I believe the bug is on this line:

cryptol/src/Cryptol/Backend/WordValue.hs

Line 580 in 282613d

bitmapWordVal sym n =<< barrelShifter sym (iteBit sym) shiftOp (Nat n) bs0 n idx_segs

The second-to-last argument, n is actually the width of the shifted array, when it should instead be the width of the index.

[robdockins]

Yep, that looks like the likely culprit. I guess I should go through and audit all the uses of barrelShifter to make sure this mistake doesn't occur elsewhere too.

EDIT: fixing that line does indeed seem like it fixes the bug, and other uses of the barrel shifter are correctly using the number of index bits for that argument. I'll put together a patch, and take the opportunity to add some documentation to these functions while I'm in there.