CODEWITHSUNDEEP
mathz3xorsolversmt
Zach Riggle
Zach Riggle

Reputation: 3095

Why does Z3 say that this equation is not satisfiable, when I have input that is correct?

Given a simple shift-and-XOR operation, where 'input' is symbolic:

input    = BitVec('input',32)
feedback = 0x8049d30
shiftreg = input ^ feedback
shiftreg = 0xffffffff & ((shiftreg << 8) | (shiftreg >> 24))
shiftreg = shiftreg ^ 0xcafebabe

s = Solver()
s.add(shiftreg == 0x804a008)
s.check()
# unsat

We are told that this equation is not solvable. If printed, s contains:

[4294967295 &
 ((input ^ 134520112) << 8 | (input ^ 134520112) >> 24) ^
 3405691582 ==
 134520840]

However, I can trivially create an example that solves this equation for 'input'.

want = 0x804a008
want ^= 0xcafebabe
want = 0xffffffff & ((want >> 8) | (want << 24))
want ^= 0x8049d30
print hex(want)
# 0xbec6672a

Entering our solution into Z3's equation, we see that we can satisfy it.

input = 0xbec6672a
[4294967295 &
 ((input ^ 134520112) << 8 | (input ^ 134520112) >> 24) ^
 3405691582 ==
 134520840]
# True

Why can Z3 not find this solution?

Upvotes: 3

Views: 3438

Answers (2)

Zach Riggle
Zach Riggle

Reputation: 3095

It turns out that in Z3, the shift operators are arithmetic shifts rather than logical shifts.

This means that a right shift >> is filled with the sign bit, rather than filled with zeroes.

You must use the Logical Shift Right (LShR) function in order to get normal behavior.

input    = BitVec('input',32)
feedback = 0x8049d30
shiftreg = input ^ feedback
shiftreg = (shiftreg << 8) | LShR(shiftreg, 24)
shiftreg = shiftreg ^ 0xcafebabe

s = Solver()
s.add(shiftreg == 0x804a008)
s.check()
hex(s.model()[input].as_long())
# 0xbec6672a

In this particular example, the shift operation is actually a rotate. Z3 has a mechanism for doing the rotate directly (in this case, it would be RotateLeft(shiftreg, 8).

Upvotes: 6

Tim
Tim

Reputation: 1098

I believe that "(shiftreg >> 24)" is interpreted as an arithmetic shift right in the z3 python API: http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html (see rshift). I think you are expecting a logical right shift. First, let's reencode this into smt2.

(declare-fun input () (_ BitVec 32))
(define-fun feedback () (_ BitVec 32) #x08049d30)
(define-fun shiftreg0 () (_ BitVec 32)
  (bvxor feedback input))
(define-fun shiftreg1 () (_ BitVec 32)
  (bvand #xffffffff
         (bvor (bvshl shiftreg0 #x00000008)
               (bvlshr shiftreg0 #x00000018))))
(define-fun shiftreg2 () (_ BitVec 32)
  (bvxor shiftreg1  #xcafebabe))

(assert (= shiftreg2 #x0804a008))
(check-sat)

We can check that this is indeed sat using your favourite QFBV solver (z3, cvc4, etc.). It is sat, and it is sat with "(= input #xbec6672a)" asserted. Now change "(bvlshr shiftreg0 #x00000018)" to "(bvashr shiftreg0 #x00000018)". This is unsat. Change the shift back. Next, let's check if the top bit of shiftreg0 is entailed to be 1. Adding the following assertion does indeed make the problem unsat.

(assert (not (= ((_ extract 31 31) shiftreg0) #b1)))

Thus we know that "(bvashr shiftreg0 #x00000018)" would be forced to shift in 1s for the top 24 bits. Thus we know that bvlshr and bvashr must behave differently on this example.

As for why the final evaluation is True, I have only guesses. (I suspect that z3 has trouble inferring the width of all constant operators in the python interface, and internally there is a 0 hanging out in a 33+ bit wide constant in the shift. Can a Z3 developer can comment on this?)

Upvotes: 2

Related Questions