Why does Z3 say this equation is not feasible when I have an input that is correct?
For a simple shift-and-XOR operation, where "enter" 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
Putting our solution into equation Z3, we see that we can satisfy it.
input = 0xbec6672a
[4294967295 &
((input ^ 134520112) << 8 | (input ^ 134520112) >> 24) ^
3405691582 ==
134520840]
# True
Why can't Z3 find this solution?
source to share
It turns out that in Z3, shift operators are arithmetic shifts, not logical shifts.
This means that the right shift >>
is padded with the sign bit rather than padded with zeros.
For normal behavior, you should use the logical right shift ( LShR
) function .
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 rotary. The Z3 has a mechanism for direct rotation (in this case it would be RotateLeft(shiftreg, 8)
.
source to share
I believe that "(shiftreg -> 24)" is interpreted as arithmetic right shift 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 shift to the right. First, give it a chance to recode this to 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 verify that this actually sits using your favorite QFBV solver (z3, cvc4, etc.). He sits and he sits with "(= entry # xbec6672a)". Now change "(bvlshr shiftreg0 # x00000018)" to "(bvashr shiftreg0 # x00000018)". It is unstable. Change the offset back. Then let's check if the upper bit of shiftreg0 should be 1. Adding the following statement really makes the problem unstable.
(assert (not (= ((_ extract 31 31) shiftreg0) #b1)))
So we know that "(bvashr shiftreg0 # x00000018)" will be forced to shift 1s for the upper 24 bits. Thus, we know that bvlshr and bvashr should behave differently in this example.
As for the final True score, I only have guesses. (I suspect z3 has problems displaying the widths of all constant operators in the python interface, and there is a 0 internally hanging in a 33+ bit constant in shift. Can Z3 developer comment on this?)
source to share