arithmetic right shift behavior on overshift

[robdockins]

Consider the following GHCi interaction:

Prelude Data.SBV> (-1 :: SBV Int8) `sShiftRight` (1 :: SBV Word8)
-1 :: SInt8
Prelude Data.SBV> (-1 :: SBV Int8) `sShiftRight` (7 :: SBV Word8)
-1 :: SInt8
Prelude Data.SBV> (-1 :: SBV Int8) `sShiftRight` (8 :: SBV Word8)
0 :: SInt8
Prelude Data.SBV> (-1 :: Int8) `shiftR` 8
-1
Prelude Data.SBV> (-1 :: SBV Int8) `shiftR` 8
-1 :: SInt8

The sShiftRight operation is giving incorrect answers for shift values that exceed the number of bits in the word to be shifted. This appears to be due to the use of svSelect in its implementation with a zero default.

Is there a particular reason to implement right and left shifts using table lookups instead of relying on underlying primitives (bvshl, bvlshr and bvashr in SMTLib)?

[LeventErkok]

You're right on the use of zero. We need to be more careful there. But I also agree that we should simply use the underlying SMTLib functions.

I think there was a point in time where either SMTLib or one of the implementations I used (most likely Yices or CVC4) didn't support symbolic second arguments for shifts, and thus I had to do the expansion. But looks like they do now.

Basically, it would involve changing the following two lines:

https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Core/Symbolic.hs#L139-L140

by removing the Int arguments; and then following thru the implications of that. Would be great if you can do that and submit a patch! If not, let me know and I might tackle it sometime.

Also would be good to check about rotates; I couldn't find anything in the SMTLib if they support rotates these days; it can probably use the same trick.

[robdockins]

OK, I'll take a stab at making a patch.

As for rotates, I don't think they are supported directly in SMTLib, or by the solvers. However, they can probably be encoded using shifts and bitwise or, I think. I don't know if that's better than table lookups or not.

[LeventErkok]

Thanks! Much appreciated.

[LeventErkok]

@robdockins There seems to be more to this story. See this:

https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Core/Model.hs#L834-L862

It appears I was thinking about arithmetic/logic shifts, but perhaps got the semantics wrong. Can you take a look at those comments to see what the appropriate semantics should be?

[LeventErkok]

@robdockins I believe I've fixed this issue, and cleaned-up the code base a bit along the way.

Can you do some testing on the Cryptol side to see all is well?

[robdockins]

On the Cryptol side, we're now running into issues where SBV is generating code which applies bvlshr and friends at different bitwidths, which is causing failures in the solver. This is probably only possible when using the dynamic interface; previously we didn't need them to be the same width. The solution, presumably, is to coerce the arguments into the same bitwidth. I don't know if it's better to handle that on the SBV side, or from within Cryptol.

Do you have an opinion?

P.S. Thanks for getting a patch together so quickly!

[LeventErkok]

It's on purpose that the shifted value and the shiftee can have different bitwidths. This is also true for Cryptol, right?

Cryptol> (2:[8]) << (3:[2])
0x10

So, I'd say it's completely legit to apply it to different widths. And that's precisely why we have the type:

sShiftRight  :: (SIntegral b, SIntegral a) => SBV a -> SBV b -> SBV a

Note the separate a and b there.

Before figuring out who should fix what, we should first figure out what's going on. Is that a Cryptol issue, or something on the SBV side (either Dynamic or otherwise) that's giving you problems?

[robdockins]

In that case it's definitely an SBV issue.

Prelude Data.SBV> prove (\x -> sShiftRight (0xFF :: SBV Word8) (x :: SBV Word32) .== 0xFF)
*** Exception: 
*** Data.SBV: Unexpected non-success response from Z3:
***
***    Sent      : (define-fun s2 () (_ BitVec 8) (bvlshr s1 s0))
***    Expected  : success
***    Received  : (error "line 11 column 44: Argument s0 at position 1 does not match declaration (declare-fun bvlshr ((_ BitVec 8) (_ BitVec 8)) (_ BitVec 8))")
***    Exit code : ExitFailure (-15)
***
***    Executable: /usr/local/bin/z3
***    Options   : -nw -in -smt2
***
*** Failed to establish solver context. Running in debug mode might provide
*** more information. Please report this as an issue!

CallStack (from HasCallStack):
  error, called at ./Data/SBV/SMT/SMT.hs:722:61 in sbv-7.2-inplace:Data.SBV.SMT.SMT

Yes, Cryptol also allows the bitwidths to be different.

[LeventErkok]

yep, that's a bug on SBV alright.. Will look at it later tonight.

[LeventErkok]

yeah, SMTLib doesn't allow mixed-bitwidth shifts.. This wasn't a problem before since we had only constants and we did the "right" thing, but now we are using symbolic values, we have to adjust for the types. What should be the semantics though? Let's say we want:

   shift : [8] -> [32] -> [8]

do we extend the first argument to 32 bits; do the shift, and chop it back? Or maybe reduce the second argument to 8 bits and do the shift? Something else? What if the shifted amount is larger than the shiftee? (Which I presume is actually more common.)

I'd appreciate thoughts on this.

[robdockins]

I think the output size should match the size of the shifted input, and the index size should be coerced to match. If the index size is smaller it should be extended; if it is larger, it should be truncated, with the caveat that if any of the truncated bits are set, the result should be the appropriate saturated result (0 or -1 depending). I'm pretty sure this preserves the "perform n 1-bit shifts" semantics.

[LeventErkok]

Another alternative could be that we require shifted-amnt and shiftee to have the exact same bit-width, and let the caller of the library deal with adjusting them appropriately. I like the simplicity of that approach as it directly maps to SMT-Lib, and is also how we implement the shift method of the Data.Bits class where the Int argument is interpreted as wide as the shifted amount.

If we did that, would that cause trouble on your end?

[robdockins]

Cryptol allows different sizes for the arguments, so we'll have to deal with that at some point, either inside SBV or outside.

I feel like it is slightly nicer to do it inside the SBV abstraction boundary, especially as the SMTLib restriction to same-size arguments feels very arbitrary to me.

[LeventErkok]

Indeed; that restriction over there seems arbitrary. Maybe we can have a compromise and say that the shift-amount is at-most as big as the shifted value; otherwise we reject it? (And if it's smaller, we pad it with zeros.) Is that reasonable?

…

On Mon, Aug 7, 2017 at 6:32 PM, robdockins ***@***.***> wrote: Cryptol allows different sizes for the arguments, so we'll have to deal with that at some point, either inside SBV or outside. I feel like it is slightly nicer to do it inside the SBV abstraction boundary, especially as the SMTLib restriction to same-size arguments feels very arbitrary to me. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#323 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAhiSRogF3nXKanCORt5JpjU5ESk9d7rks5sV7qtgaJpZM4Os7-e> .

[robdockins]

That could work... I'll still have to handle the other case on my end, but that's OK.

However, I don't see how it makes your job any easier... do you have a typeclass already that statically compares the sizes of Word/Int types?

[LeventErkok]

No not really; I was planning to dynamically reject it. But now that I think about it, I don't really like the idea. Both operands having the same type might be a better choice here. Let me give it some more thought; I'm not quite sure what the right thing to do is yet.

…

On Mon, Aug 7, 2017 at 6:41 PM, robdockins ***@***.***> wrote: That could work... I'll still have to handle the other case on my end, but that's OK. However, I don't see how it makes your job any easier... do you have a typeclass already that statically compares the sizes of Word/Int types? — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#323 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAhiSTPbAhfhjC3GMFB7Q9bEi0LSIQIxks5sV7ywgaJpZM4Os7-e> .

[robdockins]

I remain concerned about the case where you are simply truncating the top bits of the index value. The semantics you have written down here will differ from the concrete execution semantics for cases where the top bits are set.

Maybe the easiest way to handle this is to use an if statement to saturate the index amount? Something
like: amt = if x >= n then (n-1) else (extract n x)

[LeventErkok]

@robdockins Good point! Why n-1, I think it should be n, right?

I made those changes in the code base; can you review and give it a shot?

[robdockins]

Yes, you're right, n is the correct number, and not n-1.

The code looks sensible, I'll test it as soon as I get a chance.

[LeventErkok]

@robdockins I redid the implementation after that fix, which should be more robust/simpler. Do you mind doing a fresh pull and running your tests again? Thanks!

[robdockins]

The cryptol test suite is showing some failures that I think are related to these most recent changes, but I haven't tracked down the root cause yet.

[LeventErkok]

I just pushed in another commit: 675c401 to address the svLessThan comment. Though I doubt it'd have to do with those failures..

My test-suite is passing, can you do a fresh pull and let's see what's wrong..

[robdockins]

Fresh pull results in a failing case; reverting to d4b8472 fixes the immediate problem.

I'm still not sure what the problem is yet.

[LeventErkok]

one difference is that negative shifts are no longer well defined when you explicitly call shiftL/shiftR. (I found that "reverse"-direction in Haskell is only defined for shift, and the behavior is undefined for shiftL/shiftR.)

Though I don't see why that should be an issue for Cryptol.. Curious.

[LeventErkok]

@robdockins any news on what the culprit might be?

[robdockins]

Sorry, not yet; I haven't had a chance to look into it more deeply yet. For reference, the Cryptol program demonstrating the problem is:

average33 : [32] -> [32] -> [32]
average33 x y = drop`{1}(z'/2)
    where
          z' : [33]
          z' = (0b0 # x) + (0b0 # y)

average4 : [32] -> [32] -> [32]
average4 x y =    (x >> 1) + (y >> 1) + (x && y && 1)

property av4 x y = average33 x y == average4 x y

Using SBV prior to d4b8472 causes this property to QED when I attempt to :prove, but new SBV gives a spurious counterexample.

When I look at the output SMTLib, it's clear that something is wrong (it doesn't mention a shift at all!), but I don't know why. Here is the SMT file created by new SBV for this proof:

; Automatically created by SBV on 2017-08-10 12:13:32.724451 PDT
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_BV)
; --- uninterpreted sorts ---
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
(define-fun s2 () (_ BitVec 1) #b0)
(define-fun s9 () (_ BitVec 32) #x00000001)
(define-fun s6 () (_ BitVec 33) #b000000000000000000000000000000010)
; --- skolem constants ---
(declare-fun s0 () (_ BitVec 32))
(declare-fun s1 () (_ BitVec 32))
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(define-fun s3 () (_ BitVec 33) (concat s2 s0))
(define-fun s4 () (_ BitVec 33) (concat s2 s1))
(define-fun s5 () (_ BitVec 33) (bvadd s3 s4))
(define-fun s7 () (_ BitVec 33) (bvudiv s5 s6))
(define-fun s8 () (_ BitVec 32) ((_ extract 31 0) s7))
(define-fun s10 () (_ BitVec 32) (bvand s1 s9))
(define-fun s11 () (_ BitVec 32) (bvand s0 s10))
(define-fun s12 () Bool (= s8 s11))
(assert (not s12))
(check-sat)

And here it is prior to the most recent changes:

; Automatically created by SBV on 2017-08-10 12:22:40.970828 PDT
(set-option :smtlib2_compliant true)
(set-option :diagnostic-output-channel "stdout")
(set-option :produce-models true)
(set-logic QF_BV)
; --- uninterpreted sorts ---
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
(define-fun s2 () (_ BitVec 1) #b0)
(define-fun s9 () (_ BitVec 1) #b1)
(define-fun s13 () (_ BitVec 32) #x00000001)
(define-fun s6 () (_ BitVec 33) #b000000000000000000000000000000010)
; --- skolem constants ---
(declare-fun s0 () (_ BitVec 32))
(declare-fun s1 () (_ BitVec 32))
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(define-fun s3 () (_ BitVec 33) (concat s2 s0))
(define-fun s4 () (_ BitVec 33) (concat s2 s1))
(define-fun s5 () (_ BitVec 33) (bvadd s3 s4))
(define-fun s7 () (_ BitVec 33) (bvudiv s5 s6))
(define-fun s8 () (_ BitVec 32) ((_ extract 31 0) s7))
(define-fun s10 () (_ BitVec 32) (bvlshr s0 ((_ zero_extend 31) s9)))
(define-fun s11 () (_ BitVec 32) (bvlshr s1 ((_ zero_extend 31) s9)))
(define-fun s12 () (_ BitVec 32) (bvadd s10 s11))
(define-fun s14 () (_ BitVec 32) (bvand s1 s13))
(define-fun s15 () (_ BitVec 32) (bvand s0 s14))
(define-fun s16 () (_ BitVec 32) (bvadd s12 s15))
(define-fun s17 () Bool (= s8 s16))
(assert (not s17))
(check-sat)

[LeventErkok]

Looks like the entire definition of avg4 got reduced to:

x & y & 1

there's neither a shift, nor the addition; which suggests x >> 1 and y >> 1 somehow both got turned into 0; causing the constant-folder to skip the addition as well.

The first step would be to replicate this purely using SBV, with no Cryptol involvement; I tried a few things but wasn't able to do so. I'll see if I can get something later tonight.

[LeventErkok]

@robdockins I see what the problem is. It's this line here:

https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Core/Operations.hs#L644

It's stuffing the bit-size of x into a bit-vector of the size of i; in Cryptol's case, the number 32 inside a 1-bit vector; which of course overflows and screws the comparison up.

I didn't notice this in SBV because the "smallest" you have the shift is 8-bits, which is more than enough to put in the bit-width of the largest bit-vector of 64; and we never have this problem.

I'll see if I can come up with a solution shortly..

[LeventErkok]

@robdockins Fix is in, give it a shot!

[robdockins]

That seems to fix the problem! Thanks!

[LeventErkok]

Cool. Do you need a release, or can this wait till we accumulate more changes. (I'm happy either way.)

[robdockins]

I think this can wait a bit.

[LeventErkok]

Great; closing this ticket then. Feel free to open a new ticket if anything else comes up.

[LeventErkok]

@robdockins sbv 7.2 is now released on Hackage which contains the fix for this issue.