yapall
yapall copied to clipboard
Offset-based memory model
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 allocationa[*]
which represents loads/stores at an unknown offset - "Sub-allocations"
a[n]
for concrete offsetsn
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]
anda[*]
This would be a significant undertaking, and would require #37.