Unable to abstract StringS from Z3

zwimer commented 1 year ago

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: https://github.com/angr/claripy/commit/728cc9d1bedc7c19aa1a6a318262e83e69be0a00

Additional context

No response

zwimer commented 1 year ago

I have a PR in the works, but more Z3 info gathering is required via: https://github.com/Z3Prover/z3/discussions/6443

zwimer commented 1 year ago

Proposed solution @ltfish :

StringS length is always fixed to max_length in claripy; unbounded in Z3
StringS length is encoded in Z3 names, but unbounded in Z3- for StringS who do not have it encoded in their name when abstracting to claripy, we set it to max_length
Do not support StringS in z3

zwimer commented 1 year ago

@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 1 year ago

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.

angr / claripy