Infinite deepcopy recursion leads to crash

[igorganich]

Describe the bug
It is possible to get a crash due to infinite deepcopy recursion of some internal z3 objects

To Reproduce

1. Checkout on this commit igorganich/damn-vulnerable-defi-halmos@e3d6f07
2. Run halmos --solver-timeout-assertion 0 --function check_naiveReceiver --debug

...
File "/usr/lib/python3.12/copy.py", line 162, in deepcopy
y = _reconstruct(x, memo, *rv)
^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/usr/lib/python3.12/copy.py", line 259, in _reconstruct
state = deepcopy(state, memo)
^^^^^^^^^^^^^^^^^^^^^
File "/usr/lib/python3.12/copy.py", line 136, in deepcopy
y = copier(x, memo)
^^^^^^^^^^^^^^^
File "/usr/lib/python3.12/copy.py", line 221, in _deepcopy_dict
y[deepcopy(key, memo)] = deepcopy(value, memo)
^^^^^^^^^^^^^^^^^^^^^
File "/usr/lib/python3.12/copy.py", line 143, in deepcopy
y = copier(memo)
^^^^^^^^^^^^
File "/home/ihor/halmos_env/lib/python3.12/site-packages/z3/z3.py", line 356, in __deepcopy__
return _to_ast_ref(self.ast, self.ctx)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/ihor/halmos_env/lib/python3.12/site-packages/z3/z3.py", line 540, in _to_ast_ref
k = _ast_kind(ctx, a)
^^^^^^^^^^^^^^^^^
File "/home/ihor/halmos_env/lib/python3.12/site-packages/z3/z3.py", line 494, in _ast_kind
return Z3_get_ast_kind(ctx.ref(), a)
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
File "/home/ihor/halmos_env/lib/python3.12/site-packages/z3/z3core.py", line 3084, in Z3_get_ast_kind
r = _elems.f(a0, a1)
^^^^^^^^^^^^^^^^
ctypes.ArgumentError: argument 1: RecursionError: maximum recursion depth exceeded

Environment:

• OS: Linux 5.15.167.4-microsoft-standard-WSL2 Cleanup #1 SMP Tue Nov 5 00:21:55 UTC 2024 x86_64 x86_64 x86_64 GNU/Linux
• Python version: Python 3.12.7
• Halmos version: halmos 0.2.1.dev19+g4e82a90

[igorganich]

I think, the problem is in bad handling the case, when we create calldata via svm.createCalldata() and we have some logic like

return address(bytes20(msg.data[msg.data.length - 20:])); 

because when I switched to svm.createBytes(), the problem disappeared

[daejunpark]

The issue is due to a large call context with the max call depth of 1024. A call context includes trace info, which is a list of other call contexts. This recursive structure, combined with the behavior of z3 objects' deepcopy (which doesn't seem to memoize objects recursively referenced), seems to cause this issue.

The full call context can be found in: log.txt

--

@karmacoma-eth could we consider using a data structure for traces that doesn't need deepcopy()? For example, since trace items are never removed, we could use a backward-growing linked list to store them in reverse order. This way, instead of deepcopying the entire trace list, we can just copy the trace header pointer, as adding a new trace item doesn't affect the original trace.

For example, two traces, trace1 = [ item1, item2 ] and trace2 = [ item1, item2, item3 ], can be represented using a single copy of the following linked list, where trace1 points to item2 and, and trace2 points to item3:

item3 -> item2 -> item1 -> null

wdyt?