The question here is how to handle writes to an abstract location that are unbounded. Currently, for an abstract object named RSI we do RSI <= thing.load.@0sigma_size. This approach doesnt work well if some writes are bounded. then we will get RSI@0sigma_size <= thing.load.@0sigma_size. If the program is type safe wrt to our model these two types must be equal. But that's going to result in a reflexive edge with a field to the abstract object.
Ideas of how to handle this:
If we have an unbounded write/read to an abstract object, every reference to that object should be unified.
The question here is how to handle writes to an abstract location that are unbounded. Currently, for an abstract object named RSI we do
RSI <= thing.load.@0sigma_size
. This approach doesnt work well if some writes are bounded. then we will getRSI@0sigma_size <= thing.load.@0sigma_size
. If the program is type safe wrt to our model these two types must be equal. But that's going to result in a reflexive edge with a field to the abstract object.Ideas of how to handle this: