z3 symbolic read using z3.Functions

[Tim-Nosco]

@ltfish To accomplish this effort, we will need to

1. demonstrate whether or not the development investment is a time payoff for average use-cases (static memory vs dynamic memory)
2. implement a new claripy node for the z3.Function
3. write into the z3 backend how to convert the node into z3 objects
4. long-term goal: auto-detect the usecases where this functionality is most effective

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