Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Check overflow with Z3

Tags:

z3

z3py

I'm new to Z3 and I was checking the online python tutorial.

Then I thought I could check overflow behavior in BitVecs.

I wrote this code:

x = BitVec('x', 3)
y = Int('y')

solve(BV2Int(x) == y, Not(BV2Int(x + 1) == (y + 1)))

and I was expecting [y = 7, x = 7] (i.e. when values are equal but successors are not because x + 1 will be 0 and y + 1 will be 8)

But Z3 answers [y = 0, x = 0].

What am I doing wrong?

like image 508
Braulio Horta Avatar asked Jul 23 '13 21:07

Braulio Horta


2 Answers

I don't think you're doing anything wrong, looks like BV2Int is buggy:

 x = BitVec('x', 3)
 prove(x <= 3)
 prove(BV2Int(x) <= 3)

Z3py proves the first one, but gives the counter-example x=0 for the second. That doesn't sound right. (The only explanation might be some weird Python thing, but I don't see how.)

Also note that the model you get will depend on whether + treats the bit-vector as a signed number in the Python bindings, which I believe is the case. However, BV2Int might not do so, treating it as an unsigned value. This would further complicate the matters.

In any case, looks like BV2Int is not quite kosher; I'd stay away from it until there's an official answer from the Z3 folks.

like image 164
alias Avatar answered Sep 20 '22 17:09

alias


For others who are concerned by this, this appears to have been solved at some point. I just re-ran this example with the latest version of z3 (a few years after initial post), and it does return 7,7.

like image 29
Owl Owl Avatar answered Sep 20 '22 17:09

Owl Owl