Merge states

[lks9]

I was able to replay busybox echo hello. However, it took quite a long time, especially in the end where there were 32 active states and it took 42 min.

Proposal: Merge all found states after each iteration to speed up symbolic execution. In the echo hello exampe, the execution at the end could be up to 32 times faster, since only one symbolic execution successor needs to be computed for each step.

[lks9]

Solving #12 did not do the trick.

With busybox echo hello I still have 16 active states. I checked the first tow of the state splits. It was after a syscall setgid.

So I keep this open as it would be still very helpful to get the state merging done.

[lks9]

This is easier than expected just use simgr.merge(stash='found'). However, testing this takes some time.

[lks9]

Not sure if this is related to the state merging: replay_claripy_recursion_error.txt

...
  File "/home/lukas/Software/angr-dev/claripy/claripy/backends/backend_z3.py", line 450, 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 "/home/lukas/Software/angr-dev/claripy/claripy/backends/backend_z3.py", line 450, 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 "/home/lukas/.virtualenvs/angr/lib/python3.8/site-packages/z3/z3core.py", line 2951, in Z3_get_app_arg
    r = _elems.f(a0, a1, a2)
ctypes.ArgumentError: argument 3: <class 'RecursionError'>: maximum recursion depth exceeded while calling a Python object

[lks9]

Well, in the meantime, I implemented a --merge option. However, the problem still persists. With --merge it goes faster, but I can no longer replay some traces.

Example: merge_state_example.zip

With --merge:

$ retrace.py maxintbuggy_retrace 2023-05-10-014011-25dff25d-maxintbuggy.c.trace --assertions max3of4 max0of1 max0of4 max3res max0res --merge
DEBUG    | 2023-05-11 00:01:52,259 | src_tracer.retrace | Starting with function "main"
DEBUG    | 2023-05-11 00:01:52,327 | src_tracer.retrace | F4 main --count 0
DEBUG    | 2023-05-11 00:01:52,381 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:01:53,553 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:01:54,155 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:01:54,754 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:01:55,459 | src_tracer.retrace | N
DEBUG    | 2023-05-11 00:01:55,474 | src_tracer.retrace | F3 max --count 2
DEBUG    | 2023-05-11 00:01:55,492 | src_tracer.retrace | Proposition "max3of4" with index 0
DEBUG    | 2023-05-11 00:02:17,403 | src_tracer.retrace | Merging 4 states in 'ghost_end'
DEBUG    | 2023-05-11 00:02:29,047 | src_tracer.retrace | Proposition "max0of1" with index 1
DEBUG    | 2023-05-11 00:02:36,603 | src_tracer.retrace | Proposition "max0of4" with index 2
DEBUG    | 2023-05-11 00:03:06,792 | src_tracer.retrace | Merging 3 states in 'ghost_end'
DEBUG    | 2023-05-11 00:04:08,017 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:04:15,083 | src_tracer.retrace | N
DEBUG    | 2023-05-11 00:04:23,655 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:04:38,614 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:04:43,948 | src_tracer.retrace | T
WARNING  | 2023-05-11 00:04:53,187 | src_tracer.retrace | Could not find T at all in simgr <SimulationManager with 1 avoid>

And without --merge it goes through:

$ retrace.py maxintbuggy_retrace 2023-05-10-014011-25dff25d-maxintbuggy.c.trace --assertions max3of4 max0of1 max0of4 max3res max0res
DEBUG    | 2023-05-11 00:05:44,513 | src_tracer.retrace | Starting with function "main"
DEBUG    | 2023-05-11 00:05:44,583 | src_tracer.retrace | F4 main --count 0
DEBUG    | 2023-05-11 00:05:44,637 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:05:45,822 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:05:46,437 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:05:47,155 | src_tracer.retrace | T
DEBUG    | 2023-05-11 00:05:48,008 | src_tracer.retrace | N
DEBUG    | 2023-05-11 00:05:48,026 | src_tracer.retrace | F3 max --count 2
DEBUG    | 2023-05-11 00:05:48,045 | src_tracer.retrace | Proposition "max3of4" with index 0
DEBUG    | 2023-05-11 00:06:20,897 | src_tracer.retrace | Proposition "max0of1" with index 1
DEBUG    | 2023-05-11 00:06:20,899 | src_tracer.retrace | Proposition "max0of1" with index 1
DEBUG    | 2023-05-11 00:06:20,900 | src_tracer.retrace | Proposition "max0of1" with index 1
DEBUG    | 2023-05-11 00:06:20,902 | src_tracer.retrace | Proposition "max0of1" with index 1
DEBUG    | 2023-05-11 00:06:21,101 | src_tracer.retrace | Proposition "max0of4" with index 2
DEBUG    | 2023-05-11 00:06:21,102 | src_tracer.retrace | Proposition "max0of4" with index 2
DEBUG    | 2023-05-11 00:06:21,104 | src_tracer.retrace | Proposition "max0of4" with index 2
DEBUG    | 2023-05-11 00:06:21,105 | src_tracer.retrace | Proposition "max0of4" with index 2
DEBUG    | 2023-05-11 00:07:49,913 | src_tracer.retrace | T (found 10)
DEBUG    | 2023-05-11 00:08:49,083 | src_tracer.retrace | N (found 10)
DEBUG    | 2023-05-11 00:08:49,322 | src_tracer.retrace | T (found 10)
DEBUG    | 2023-05-11 00:09:56,945 | src_tracer.retrace | T (found 4)
DEBUG    | 2023-05-11 00:09:57,902 | src_tracer.retrace | T (found 4)
DEBUG    | 2023-05-11 00:10:29,336 | src_tracer.retrace | T (found 2)
DEBUG    | 2023-05-11 00:10:30,108 | src_tracer.retrace | N (found 2)
DEBUG    | 2023-05-11 00:10:30,144 | src_tracer.retrace | Proposition "max3res" with index 3
DEBUG    | 2023-05-11 00:10:30,146 | src_tracer.retrace | Proposition "max3res" with index 3
DEBUG    | 2023-05-11 00:10:30,234 | src_tracer.retrace | Proposition "max0res" with index 4
DEBUG    | 2023-05-11 00:10:30,236 | src_tracer.retrace | Proposition "max0res" with index 4
DEBUG    | 2023-05-11 00:10:44,576 | src_tracer.retrace | R --count 5 (found 2)
DEBUG    | 2023-05-11 00:10:44,834 | src_tracer.retrace | R --count 6 (found 2)