`claripy._backend_z3._abstract()` failed

[hwu71]

When I was trying to convert a FuncDecl z3 expression Func_0x401149(ZeroExt(32, Extract(31, 0, var_load(<BV64 rdi>))), 100) to claripy using claripy._backend_z3._abstract(). I got such error:

Call return value: Func_0x401149(ZeroExt(32,
                      Extract(31, 0, var_load(<BV64 rdi>))),
              100)
ERROR   | 2021-09-03 15:11:55,414 | claripy.backends.backend_z3 | Mystery operation Func_0x401149 in BackendZ3._abstract_internal. Please report this.
ERROR   | 2021-09-03 15:11:55,414 | claripy.backends.backend_z3 | Unknown Z3 error in abstraction (result_ty == 'UNINTERPRETED'). Update your version of Z3, and, if the problem persists, open a claripy issue.
Traceback (most recent call last):
  File "/home/hongwei/Desktop/Codes/AMP_pipeline/repos/claripy/claripy/backends/backend_z3.py", line 68, in z3_condom
    return f(*args, **kwargs)
  File "/home/hongwei/Desktop/Codes/AMP_pipeline/repos/claripy/claripy/backends/backend_z3.py", line 374, in _abstract
    return self._abstract_internal(e.ctx.ctx, e.ast)
  File "/home/hongwei/Desktop/Codes/AMP_pipeline/repos/claripy/claripy/backends/backend_z3.py", line 506, in _abstract_internal
    raise BackendError(err)
claripy.errors.BackendError: Unknown Z3 error in abstraction (result_ty == 'UNINTERPRETED'). Update your version of Z3, and, if the problem persists, open a claripy issue.

Z3-solver version: 4.8.12 (the latest one)

I can create some scripts to help reproduce this issue if needed.

[rhelmot]

Claripy doesn't have support for uninterpreted functions right now. Did you construct that z3 AST manually?

[hwu71]

Scripts to reproduce it:

import claripy
import z3

def cal_func(func_name, args, ret):
    args_z3 = claripy._backend_z3.convert_list(args)
    ret_z3 = claripy._backend_z3.convert(ret)
    args_z3_sorts = list(map(lambda x: x.sort(), args_z3))
    ret_z3_sort = ret_z3.sort()
    func_sig = []
    if args_z3_sorts:
        func_sig = args_z3_sorts
    func_sig.append(ret_z3_sort)
    func = z3.Function(func_name, *func_sig)
    ret_val = func(*args_z3)
    ret_val_claripy = claripy._backend_z3._abstract(ret_val)
    print("Ret val in Z3:", ret_val)
    print("Ret val in Claripy:", ret_val_claripy)


rdi = claripy.BV('rdi', 64, explicit_name=True)
var_load = to_ret = claripy.BVS('var_load' + str(rdi), 64, explicit_name=True)

arg_1 = claripy.ZeroExt(32, claripy.Extract(31, 0, var_load))
arg_2 = claripy.BVV(100, 64)
args = [arg_1, arg_2]
ret = claripy.BVS('ret_val', 64, explicit_name=True)
cal_func('0x401149', args, ret)

Did you construct that z3 AST manually?

I construct the function arguments using some Claripy operations, but the ret_val is calculated by z3.Function

[rhelmot]

Yeah we explicitly do not support z3.Function right now. It's not a fundamental limitation, it's just something we've never needed and haven't found the time to put in. I'll gladly accept a pull request to add it.

[hwu71]

Thanks for your explanation. I will try it out.

[github-actions]

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]

This issue has been closed due to inactivity.