CODEWITHSUNDEEP
pythonpython-2.7evalz3z3py
Sharad
Sharad

Reputation: 553

Python eval printing an extra \n for a z3 expression

I have narrowed down my problem in the following code. I am trying to convert a string into equivalent z3 expression. The problem is that when the variable name is big, the 'eval' puts extra \n in between the expression but if I use a smaller variable name the extra \n is not there. I need to have a bigger variable name because that is not under my control. Please suggest how can I make the code working correctly with bigger variable names

EXTRA \n PRODUCING CODE

from z3 import BitVec, Solver #@UnresolvedImport

z3sig_dict = {}
z3sig_dict['v__DOT__process_1_reg3'] = {"z3name":BitVec('v__DOT__process_1_reg3', 32), "bits":32}
z3sig_dict['v__DOT__process_1_reg3_1'] = {"z3name":BitVec('v__DOT__process_1_reg3_1', 32), "bits":32}
string = "(z3sig_dict['v__DOT__process_1_reg3']['z3name'] == (8 + (z3sig_dict['v__DOT__process_1_reg3_1']['z3name'] % 0x20000000)))"
s = Solver()
print(string)
clause = eval(string)
print(str(clause))
s.add(clause)

The output of this code is

(z3sig_dict['v__DOT__process_1_reg3']['z3name'] == (8 + (z3sig_dict['v__DOT__process_1_reg3_1']['z3name'] % 0x20000000)))
v__DOT__process_1_reg3 ==
8 + v__DOT__process_1_reg3_1%536870912

CORRECTLY WORKING CODE

from z3 import BitVec, Solver #@UnresolvedImport

z3sig_dict = {}
z3sig_dict['reg3'] = {"z3name":BitVec('reg3', 32), "bits":32}
z3sig_dict['reg3_1'] = {"z3name":BitVec('reg3_1', 32), "bits":32}
string = "(z3sig_dict['reg3']['z3name'] == (8 + (z3sig_dict['reg3_1']['z3name'] % 0x20000000)))"
s = Solver()
print(string)
clause = eval(string)
print(str(clause))
s.add(clause)

The output of this code is

(z3sig_dict['reg3']['z3name'] == (8 + (z3sig_dict['reg3_1']['z3name'] % 0x20000000)))
reg3 == 8 + reg3_1%536870912

SOME OBSERVATIONS

If I reduce the % 0x20000000 to % 0x2000, then also the code works correctly, but incorrectly if I add one more zero i.e 0x20000

Upvotes: 2

Views: 586

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

Z3 adds the \n because it thinks the output is too wide for the shell to print. By default, it assumes that only 80 characters fit into one line, but it's easy to tell Z3 to use more space:

from z3 import *

set_param(max_lines=1, max_width=1000000)
print(str(clause))

Upvotes: 2

Related Questions