sRotateRight and sRotateLeft are broken on SInt 1 or SInt 2

[lsrcz]

On sbv 10.2, see the following prove calls:

ghci> prove $ \(a :: SInt 1) (b :: SInt 1) -> (sRotateRight a (xor b b)) .== a
Falsifiable. Counter-example:
  s0 = -1 :: IntN 1
  s1 =  0 :: IntN 1
ghci> prove $ \(a :: SInt 2) (b :: SInt 2) -> (sRotateRight a (xor b b)) .== a
Falsifiable. Counter-example:
  s0 = -1 :: IntN 2
  s1 =  0 :: IntN 2
ghci> prove $ \(a :: SInt 3) (b :: SInt 3) -> (sRotateRight a (xor b b)) .== a
Q.E.D.
ghci> prove $ \(a :: SInt 4) (b :: SInt 4) -> (sRotateRight a (xor b b)) .== a
Q.E.D.
ghci> prove $ \(a :: SWord 1) (b :: SWord 1) -> (sRotateRight a (xor b b)) .== a
Q.E.D.
ghci> prove $ \(a :: SWord 2) (b :: SWord 2) -> (sRotateRight a (xor b b)) .== a
Q.E.D.

xor b b should always be zero, so the lhs and rhs should always equal, however, sbv says that it is not a tautology with SInt 1 or SInt 2.

sRotateLeft has the same bug.

[LeventErkok]

The problem is in calls like svUNeg i which assumes the size represented with the given bit-size becomes non-negative in the code. Alas, this isn't true when i is too small. -(-1) == -1 : :SInt 1, -(-2) == -2 :: SInt 2. Not a problem for 3, since -(-3) == 3 :: SInt 3

Not hard to fix, but at the risk of generating ugly code for the most common case. I'm not even sure if it's worth supporting rotates with bit-vector second arguments.

Would it be a big deal for you if rotate types changed so that the second argument is SInteger? I think that would simplify a lot of the code. Same argument probably goes for shifts. Would love to hear what the end-user opinion is on this matter.

[lsrcz]

I feel that supporting bit-vector second arguments is useful, at least to me, as sometimes we may want to use SBV to verify hardware-related stuff where only bit-vectors but not mathematical numbers could be used.

We can definitely use sFromIntegral to convert bit-vectors to SInteger and then do the proposed new rotate. However, I am unsure about the implementation in your mind, so I am worried if this would cause a mixture of theories, thus

• make many solvers that do not support LIA theories, e.g., boolector, cannot be used, and
• hugely hurts solving performance.

My current workaround is to convert both arguments to SWord before doing the rotation and convert them back afterwards. This works under the assumption that the second argument is non-negative, and we add assertions for that. This is reasonable, as the Haskell standard library states that rotating with negative bits is undefined behavior.

For the fix, could we simply try to broaden the second argument to max(3, finiteBitSize) bits internally as a preprocess procedure? It seems that this works, but I cannot confirm it without inspecting the actual implementation. This will only change the generated formula when the second argument is 1 or 2 bits, and will not have a huge impact on the performance.

ghci> prove $ \(a :: SInt 1) (b :: SInt 3) -> (sRotateRight a (xor b b)) .== a
Q.E.D.
ghci> prove $ \(a :: SInt 2) (b :: SInt 3) -> (sRotateRight a (xor b b)) .== a
Q.E.D.
ghci> prove $ \(a :: SInt 1) (b :: SInt 1) -> let b' = sFromIntegral b :: SInt 3 in (sRotateRight a (xor b' b')) .== a
Q.E.D.

[LeventErkok]

@lsrcz OK; I pushed in a couple of tweaks; give it a test and see if it works for you.

This code is more complicated than I'd like; so if you can spare the cycles and figure out an easier way to code it up (especially if it still has bugs!) I'd appreciate PRs.

[lsrcz]

Thank you! I will test it and have a look at the code when I get some time.

[lsrcz]

Thank you, @LeventErkok, for the patch! The fix seems to work for me, as it survived some random testing.

I will leave the issue open to remind me to have a look at the code sometime.

[LeventErkok]

I think this is good now; so I'm going to close it. If you find further issues, please open a new ticket