Potential unsound inference of store capabilities due to directionality

[2over12]

In 517dd34 I added directionality to stores.

The idea here was that if we observe a store of some type variable t to a pointer p and p points to the abstract object a then p.store ⊑ a because we could have stored to p and therefore must be compatible. This kinda falls over because really we would want a must analysis here to guarantee that along some path we point to a, otherwise p.store may not have to be a subtype. Ignoring that issue for the moment: directionality made the following claim hold: If pointer z reaches p then we should also conclude z.store ⊑ a

This reasoning is fairly reasonable but has the undesirable consequence of also resulting in an overly strong consequence of p ⊑ z. Given contra-variance on store capabilities we can then derive z.store ⊑ p.store. This says that any pointer defining a stored to pointer must always store a subtype. That's undesirable because imagine some sort of situation like:

void* i;
void* z;
void* p = z;
*p=open(); 
 
z = i;
*z = 1;
}

in this case we get z.store ⊑ fd when z both stores int and fd so in an ideal world our type here is int ⊑ z.store. I need to think more about this. Im assuming the reason this was initially done was to handle how locs are generated (ie. through address computations). Something like:

u=INT_ADD rsp, 8
STORE x, u

and without flipping the direction we get

rsp_defsite.+8 ⊑ unique
unique  ⊑ t
t.store ⊑ stack.at_8_8

with that we get to conclude:

t.store ⊑ unique.store
unique.store ⊑ rsp_defsite.+8.store

but that seems fine to me