Z3 StringV abstraction broken
zwimer opened this issue · 0 comments
zwimer commented
Description
claripy
is unable to abstract StringV
from z3.
A traceback from: claripy.backend_manager.backends.z3.simplify(claripy.StringV("abc"))
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 92, in z3_condom
return f(*args, **kwargs)
File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 1016, in simplify
o = self._abstract(s)
File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 92, in z3_condom
return f(*args, **kwargs)
File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 414, in _abstract
return self._abstract_internal(e.ctx.ctx, e.ast)
File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 536, in _abstract_internal
a = self._string_constant_from_ast(ctx, ast, decl)
File "/home/zwimer/.virtualenvs/test/lib/python3.10/site-packages/claripy/backends/backend_z3.py", line 718, in _string_constant_from_ast
raise BackendError("Weird Z3 model")
claripy.errors.BackendError: Weird Z3 model
Steps to reproduce the bug
import claripy
a = claripy.StringV("abc")
claripy.backend_manager.backends.z3.simplify(a)
Environment
> mkvirtualenv test
> pip install claripy
Additional context
Before fixing this (and having it work fully), these issues need to be addressed: