Offset-based memory model

[langston-barrett]

Right now, a pointer stored to a single, concrete field of a struct or index in an array will be retrieved in a load from any field or index. We should instead adopt a memory model that separates these. This would involve:

• For each GEP expression and instruction with all concrete indices, calculating the offset added to the base pointer
• For each (basic) allocation a, a new allocation a[*] which represents loads/stores at an unknown offset
• "Sub-allocations" a[n] for concrete offsets n that have been calculated via GEPs - though care must be taken such that there is only a bounded number of such suballocations.
• Rules relating loads and stores from the a[n] and a[*]

This would be a significant undertaking, and would require #37.