Based on #42 but I might make this one completely independent.
This needs a lot of improvements and documentation but I already sketched something so here it is:
right now it looks like this tower of abstractions (Capability/Object/ObjectState being new and scoped to the analysis, the rest are existing SPIR-T concepts):
Values (of pointer types)
⇊ which are approximated by/map to ⇊
Capabilitys (as in CHERI, or maybe "alias sets"?)
⇊ which point to (one or more) ⇊
Objects (as in C's "memory objects", aka "allocations")
⇊ which are flow-sensitively tracked as ⇊
ObjectStates (individual "versions" or "revisions" of object contents)
⇊ which describe changes by referring to ⇊
DataInsts (regular non-control-flow instructions, here qptr.{load,store})
⇊ which interface with the data they read/write as ⇊
Values (I lied, it's not a tower, it's an ouroboros)
but because this is based on small local steps put together, the interactions with Values would all admit applying e.g. constant folding and rewrite rules etc. (as long as everything can be undone - and only loops want the true "rubberbanding", to be able to fixpoint-saturate as many effects as possible to model the loop across its iterations, without actually accidentally interpreting the loop)
Based on #42 but I might make this one completely independent.
This needs a lot of improvements and documentation but I already sketched something so here it is: