Bug in clearBit

[jvilar]

The clearBit function does not work correctly. It currently uses the default implementation from Data.Bits and the result is that all the bits above the one selected are also cleared. A possible solution is to define it explicitly using:

clearBit bv = complement . setBit (complement bv) 

Best regards,

Juan Miguel

[IagoAbal]

Hi @jvilar and thanks for reporting this bug. I think the bug is not in clearBit but in .&..

Current implementation of (.&.) is:

(BV n1 a) .&. (BV n2 b) =
  BV n $ a .&. b
  where
    n = max n1 n2

and I think it should instead be:

u@(BV n1 _) .&. v@(BV n2 _) =
  BV n $ a .&. b
  where
    n = max n1 n2
    BV _ a = signExtend n u
    BV _ b = signExtend n v

(Edited to fix typo in code snippet.)

That is, for .&. (and for .|.!) the bit-vectors must be interpreted as signed, whereas right now they are interpreted as unsigned.

I need to properly test the change and if everything is OK I'll commit it, or you may open a pull request if you are in a hurry.

[jvilar]

Thank you for your prompt answer. However, I think that .&. is fine as it is. I don't understand the in in your code, so I tested with

u@(BV n1 _) .&. v@(BV n2 _) =
  BV n $ a .&. b
  where
    n = max n1 n2
    BV _ a = signExtend (n-n1) u
    BV _ b = signExtend (n-n2) v

But sign extending the operands risks having too many ones. Consider

let a = bitVec 2 3
    b = bitVec 4 15
print $ a .&. b

which outputs [4]15 with the sign extensions.

On the other hand, if you worry about the repeated use of complement, an alternate definition for clearBit could be

clearBit u@(BV n _) i = u .&. v
  where v = bitVec n $ 2 ^ n - 2 ^ i - 1

Best regards,

Juan Miguel

[IagoAbal]

Hi,

The extra ins were just a typo, sorry about the confusion, I have edited my previous comment.

The main reason why I don't think clearBit is to blame it's precisely because it is using the default implementation, and the default implementation is based on properties that are supposed to hold. Quoting the documentation:

x clearBit i is the same as x .&. complement (bit i)

We could redefine clearBit but, still, it should satisfy that "law" and right now it would not.

Forgot to mention that one also needs to fix bit:

bit i = BV (i+2) (2^i)

so that complement (bit i) works as expected.

Regarding your example:

let a = bitVec 2 3
    b = bitVec 4 15
print $ a .&. b

This does work correctly, because bitVec 2 3 is 0b11 and it can be interpreted as a -1. If you mean to represent +2 you can use bitVec 3 3 (or just fromInteger 3 :: BV).

Note that when you use bitVec 2 3 it doesn't mean "represent +3 using 2 bits", here 3 is just representing a bunch of bits. Note that you can also type bitVec 2 7 to obtain the same bit-vector. If you want to create a bit-vector representing +3 using the minimum number of bits, then you must use fromInteger 3 :: BV, and this will automatically allocate an extra bit for the sign.

I believe it makes sense that .&. interpretes bit-vectors as signed. Note that 15 .&. -1 == 15 also in Haskell. But I would need to test it properly and think more about it. And, of course, this would require a major version since it may break existing code. That's a pity, but in principle I think it's important to respect the laws assumed by Data.Bits. We could always add a new +&+ operator that does not perform sign-extension.

[jvilar]

As I see it, there are two different issues here. First is whether the given equivalence is a law or a default implementation. From my point of view, it is an implementation since the meaning of clearBit should be to set to zero a given bit, which I agree that usually can be accomplished by the given equivalence, but there is a problem with it when the values involved have different bit lengths, which is exactly the case with BV.

The other issue is that according to the documentation of Data.BitVector:

Bit-vectors are interpreted as unsigned integers (i.e. natural numbers) except for some specific signed operations.

And I fell that bit, complement and much less .&. enter in the category of signed operations, therefore they should not be using signExtend and I think that it also imples that bitVec 2 3 is a perfectly correct expression. On the other hand your proposal for bit and .&. leans towards interpreting the values as signed integers, which could be OK but against the philosophy of Data.BitVector.

Best,

Juan Miguel

[IagoAbal]

Bit-vectors are interpreted as unsigned integers (i.e. natural numbers) except for some specific signed operations.

And I fell that bit, complement and much less .&. enter in the category of signed operations, therefore they should not be using signExtend

That is true, that is why I said that this would break backwards compatibility and would require a major version bump. The documentation would need to change too of course. I'm not saying that I have decided on this particular fix, but the fact that x .&. complement (bit i) doesn't do what one would expect does disturb me a little bit.

For your use of Data.Bitvector, does it make a lot of difference? One basically needs to take care of the sign bit.

I think that it also imples that bitVec 2 3 is a perfectly correct expression.

It is of course a correct expression, as it is bitVec 2 7 which yields the same result. What I'm saying is that if you want to obtain the BV representation of a given integer, the right function for that is fromInteger. The bitVec function is somehow lower-level, and bitVec 2 7 is a correct expression but it is certainly not representing the integer 7.

We can start by patching 0.5 with your latest proposal:

{-# INLINE clearBit #-}
clearBit u@(BV n _) i = u .&. v
  where v = bitVec n $ 2 ^ n - 2 ^ i - 1

This can go into v0.5.1. But I am still considering to change .&. and .|. in a future release. But as I said, I have not even tested my proposed fix properly yet, I don't know if it would break any of the important properties that currently do hold.

[IagoAbal]

We can start by patching 0.5 with your latest proposal:

Let me know if you can submit a pull request with that change, plus one or more QuickCheck properties about clearBit.

[jvilar]

For your use of Data.Bitvector, does it make a lot of difference? One basically needs to take care of the sign bit.

It will indeed because the change in bit will imply that operations like setting a bit would change the size of the BV, which would be inconvenient. I use a BV like an space-efficient array of Bool, the sign bit does not make much sense to me, while keeping the size constant is important.

Regarding the question of bitVec 2 3, just use ones 2 and you get the same results in a not so low level way.

Let me know if you can submit a pull request with that change, plus one or more QuickCheck properties about clearBit.

Just done it.

Best,

Juan Miguel

[IagoAbal]

Fixed by 0aff564.