z3.Array support

[bannsec]

When dealing with very large table lookups, z3.Array is a huge improvement in performance. It would be great if symbolic memory read strategy could be updated to use it, but even simply having the ability to use those primitives with claripy objects (for instance, inside custom user hooks) would be quite beneficial.

Information on Arrays can be found here: https://rise4fun.com/z3/tutorialcontent/guide

Mainly, it comes down to stuff like

table = z3.Array(<args>)
table = z3.Store(table, 0, 1)
#etc

# Lookup becomes
table[sym_var] 

[rhelmot]

iirc there isn't a good z3 theory that we can use which combines bitvector arithmetic and arrays, which makes this highly problematic to integrate into symbolic execution. I agree it would be nice to have in claripy, though. Unfortunately, there isn't really any manpower available for such a project at the moment. If anyone wanted to take this issue, they would probably want to model it after the relevant parts of the PR which added string support.

[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.