Unable to abstract StringS from Z3
Closed this issue · 4 comments
zwimer commented
Description
Claripy cannot properly abstract string symbols from Z3
Steps to reproduce the bug
import claripy
s = claripy.StringS("abc", 64)
claripy.backend_manager.backends.z3.simplify(s)
Yields
Traceback (most recent call last):
File "<stdin>", line 1, in <module>
File "/Users/zwimer/Desktop/Work/claripy2/claripy/backends/backend_z3.py", line 93, in z3_condom
return f(*args, **kwargs)
File "/Users/zwimer/Desktop/Work/claripy2/claripy/backends/backend_z3.py", line 990, in simplify
o = self._abstract(s)
File "/Users/zwimer/Desktop/Work/claripy2/claripy/backends/backend_z3.py", line 93, in z3_condom
return f(*args, **kwargs)
File "/Users/zwimer/Desktop/Work/claripy2/claripy/backends/backend_z3.py", line 398, in _abstract
return self._abstract_internal(e.ctx.ctx, e.ast)
File "/Users/zwimer/Desktop/Work/claripy2/claripy/backends/backend_z3.py", line 492, in _abstract_internal
raise BackendError("Unknown z3 term type %d...?" % symbol_ty)
claripy.errors.BackendError: Unknown z3 term type 11...?
Environment
Master: 728cc9d
Additional context
No response
zwimer commented
I have a PR in the works, but more Z3 info gathering is required via: Z3Prover/z3#6443
zwimer commented
Proposed solution @ltfish :
StringS
length is always fixed tomax_length
in claripy; unbounded in Z3StringS
length is encoded in Z3 names, but unbounded in Z3- forStringS
who do not have it encoded in their name when abstracting to claripy, we set it tomax_length
- Do not support
StringS
in z3
zwimer commented
@ltfish I think we should just do 3 since other things read Z3 names like our unsat core stuff and fixing the length after abstraction feels like a correctness issue. So I think just disallowing z3 support is fine, since we already don't support it via the fact that the code will error.
zwimer commented
I disallowed StringS
abstraction in the z3 backend in the linked PR since it doesn't work anyway. I added a warning for StringS
conversion. Functionally this just cleans up exceptions and adds an logging warning.