How to add information to BitVec variable and get that variable back with get_vars()?

user_11250393 0
Viewed 111

In the code below I tried to add some extra information to BitVec variable, then created some condition, and then use get_vars to get back the x variable but it is always different because the output of this little snippet is False. I expected to be the same object but it seems that when x > 3 is executed, BoolRef is created and x is lost. Also, I expected that x.ast would be the same as var.ast but the instances are different.

from z3 import BitVec
from z3.z3util import get_vars

x = BitVec('x', 256)
x.foo = 1

some_cond = x > 3

for var in get_vars(some_cond):
    print(var is x)
    print(hasattr(var, 'foo'))

I thought to wrap z3.BitVec function in a class that extends z3.BitVecRef but it will be a pain since I need to wrap all the other functions such as z3.If, z3.And, z3.Or, etc.

I can include information in the name of the z3.BitVec but it will be slower since I need to parse that string later.

So, my question is if there is any other way to add information to z3.BitVec and get that information later with or without get_vars?

Thanks!

z3py
1 Answers

The problem here is that as z3 processes these variables it "internalizes" them and converts them to BitVecRef's; which no-longer produce true with the originals you had when you use the is construct.

Unfortunately, this is quite hard-coded in the way z3 and z3py works, so you cannot really work-around it. However, if you are willing to create and keep track of a list of variables yourself, then you can effectively simulate it like this:

from z3 import BitVec, Or
from z3.z3util import get_vars

x = BitVec('x', 256)
x.foo = 1

y = BitVec('y', 256)
y.foo = 2

z = BitVec('z', 256)

some_cond = Or([x > 3, y < 1, z > 12])

def my_get_attribute(var, attrib, allMyVariables):
    for known in allMyVariables:
        if var == known:
           if hasattr(known, attrib):
              return getattr(known, attrib)
           else:
              raise Exception("Can't find attribute '{}' on variable '{}'".format(attrib, var))
    raise Exception("Can't find variable '{}', make sure allMyVariables is kept up-to-date.".format(var))

for var in get_vars(some_cond):
    print("var: {}, foo: {}".format(var, my_get_attribute(var, 'foo', [x, y, z])))

When I run this, I get:

var: x, foo: 1
var: y, foo: 2
Traceback (most recent call last):
  File "a.py", line 24, in <module>
    print("var: {}, foo: {}".format(var, my_get_attribute(var, 'foo', [x, y, z])))
  File "a.py", line 20, in my_get_attribute
    raise Exception("Can't find attribute '{}' on variable '{}'".format(attrib, var))
Exception: Can't find attribute 'foo' on variable 'z'

This isn't ideal as it requires you to keep track of your variables obviously; but I suspect you might already have that lying around if you are putting in attributes to start with. Hope this helps!

user_9363100
Related