Exception while decompiling

[pagabuc]

While decompiling certain functions, angr-management throws an exception:

Exception while running job "Decompiling":
Traceback (most recent call last):
  File "/x/angr-dev/claripy/claripy/backends/backend_z3.py", line 68, in z3_condom
    return f(*args, **kwargs)
  File "/x/angr-dev/claripy/claripy/backends/backend_z3.py", line 374, in _abstract
    return self._abstract_internal(e.ctx.ctx, e.ast)
  File "/x/angr-dev/claripy/claripy/backends/backend_z3.py", line 408, in _abstract_internal
    children = [ self._abstract_internal(ctx, z3.Z3_get_app_arg(ctx, ast, i), new_split_on) for i in range(num_args) ]
  File "/x/angr-dev/claripy/claripy/backends/backend_z3.py", line 408, in <listcomp>
    children = [ self._abstract_internal(ctx, z3.Z3_get_app_arg(ctx, ast, i), new_split_on) for i in range(num_args) ]
  File "/x/angr-dev/claripy/claripy/backends/backend_z3.py", line 408, in _abstract_internal
    children = [ self._abstract_internal(ctx, z3.Z3_get_app_arg(ctx, ast, i), new_split_on) for i in range(num_args) ]
  File "/x/angr-dev/claripy/claripy/backends/backend_z3.py", line 408, in <listcomp>
    children = [ self._abstract_internal(ctx, z3.Z3_get_app_arg(ctx, ast, i), new_split_on) for i in range(num_args) ]
  File "/x/angr-dev/claripy/claripy/backends/backend_z3.py", line 423, in _abstract_internal
    bv_num = int(z3.Z3_get_numeral_string(ctx, ast))
  File "/home/pagabuc/.virtualenvs/angr-dev/lib/python3.9/site-packages/z3/z3core.py", line 2843, in Z3_get_numeral_string
    _elems.Check(a0)
  File "/home/pagabuc/.virtualenvs/angr-dev/lib/python3.9/site-packages/z3/z3core.py", line 1414, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'invalid argument'

The above exception was the direct cause of the following exception:

Traceback (most recent call last):
  File "/x/angr-dev/angr-management/angrmanagement/data/instance.py", line 234, in _worker
    result = job.run(self)
  File "/x/angr-dev/angr-management/angrmanagement/data/jobs/decompile_function.py", line 13, in run
    inst.project.analyses.Decompiler(
  File "/x/angr-dev/angr/angr/analyses/analysis.py", line 115, in __call__
    oself.__init__(*args, **kwargs)
  File "/x/angr-dev/angr/angr/analyses/decompiler/decompiler.py", line 34, in __init__
    self._decompile()
  File "/x/angr-dev/angr/angr/analyses/decompiler/decompiler.py", line 82, in _decompile
    rs = self.project.analyses.RecursiveStructurer(ri.region, cond_proc=cond_proc, kb=self.kb)
  File "/x/angr-dev/angr/angr/analyses/analysis.py", line 115, in __call__
    oself.__init__(*args, **kwargs)
  File "/x/angr-dev/angr/angr/analyses/decompiler/structurer.py", line 39, in __init__
    self._analyze()
  File "/x/angr-dev/angr/angr/analyses/decompiler/structurer.py", line 71, in _analyze
    st = self.project.analyses.Structurer(current_region, parent_map=parent_map,
  File "/x/angr-dev/angr/angr/analyses/analysis.py", line 115, in __call__
    oself.__init__(*args, **kwargs)
  File "/x/angr-dev/angr/angr/analyses/decompiler/structurer.py", line 105, in __init__
    self._analyze()
  File "/x/angr-dev/angr/angr/analyses/decompiler/structurer.py", line 122, in _analyze
    self._analyze_acyclic()
  File "/x/angr-dev/angr/angr/analyses/decompiler/structurer.py", line 144, in _analyze_acyclic
    self.cond_proc.recover_reaching_conditions(self._region, with_successors=True)
  File "/x/angr-dev/angr/angr/analyses/decompiler/condition_processor.py", line 135, in recover_reaching_conditions
    reaching_conditions[node] = self.simplify_condition(reaching_condition)
  File "/x/angr-dev/angr/angr/analyses/decompiler/condition_processor.py", line 675, in simplify_condition
    claripy_simplified = claripy.simplify(cond)
  File "/x/angr-dev/claripy/claripy/ast/base.py", line 1126, in simplify
    s = e._first_backend('simplify')
  File "/x/angr-dev/claripy/claripy/ast/base.py", line 1061, in _first_backend
    try: return getattr(b, what)(self)
  File "/x/angr-dev/claripy/claripy/backends/backend_z3.py", line 68, in z3_condom
    return f(*args, **kwargs)
  File "/x/angr-dev/claripy/claripy/backends/backend_z3.py", line 1013, in simplify
    o = self._abstract(s)
  File "/x/angr-dev/claripy/claripy/backends/backend_z3.py", line 70, in z3_condom
    raise ClaripyZ3Error() from ze
claripy.errors.ClaripyZ3Error

I was able to reproduce the issue with several binaries (including /bin/true).

Here the versions of the packages installed with angr-dev: package_versions.txt.

Let me know if you need more information to reproduce the issue, thanks!

[rhelmot]

I am unable to reproduce this - I can decompile every function in /bin/true without issue. Can you provide a more concrete testcase?

[ltfish]

I sincerely hope this is not a Z3Py issue... I also noticed that you are using Python 3.9. I wonder if that may be the root cause.

FYI I'm using Python 3.7 on Windows and Python 3.8 on Ubuntu 20.04.

[pagabuc]

Thanks to @rhelmot we narrowed down this issue to be a problem on my side (I am still investigating what's going on). What is quite strange, is that it happens also with angr-management-onefile-ubuntu, which includes its own Python 3.8.10 interpreter..

I'll let you know!

[pagabuc]

Update: it seems to be an issue specific to debian (testing?), I was able to reproduce this exception after installing a clean system in a VM..

[rhelmot]

I just installed angr in the docker container python:3.9 which is based on debian buster, and everything worked fine...

[ltfish]

@pagabuc can you upload your VM image somewhere so that I can import and debug it?

[pagabuc]

Sure, here it is: https://drive.google.com/file/d/1pRH-03IIyWUrlxb8j0zZYoFUVEbMwYAR/view?usp=sharing

Thanks!!

[github-actions[bot]]

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions[bot]]

This issue has been closed due to inactivity.