Consider pointees separately for refinement

[michael-schwarz]

Closes #1658

[michael-schwarz]

Does something special need to be done for the unknown pointer?

[sim642]

Why is it necessary to limit this to NoOffset? Seems like it shouldn't really matter whether the pointer in in a struct field or something.

[sim642]

This now swallows all deadcode, but this might not be entirely right. In particular, if the invariant doesn't hold for any pointees, this will join together a bunch of bots, but not raise Deadcode, which I think it would've done before.
We might have to have some extra logic here that if all cases were dead, then Deadcode is also raised after the fold. I think MCP does something similar (but other way around, for any instead of all).

[sim642]

I started thinking about this more in relation to double dereferences, etc and realized this should be some kind of recursive process because pointers can be refined at every level.
For example

p → {&q, &r}
q → {&x, &y}
r → {&z, &w}
x → {1}
y → {2}
z → {1}
w → {3}

Assuming **p == 2 should refine p → {&q} and q → {&y}.
Seems like Mem should just recurse (while refining the pointer) and Var would be the base case.

[sim642]

Or perhaps not be so ambitious and handle nested dereferences... It's surprisingly tricky to get right even in very simple theoretical setting (the unassume paper appendix on pointers). We spent over an hour with Vesal trying to get it right in a semi-general case (where lvalues are sequences of derefs ending with a variable, so no arbitrary expressions in dereference, nor offsets). The formal definition is also very inefficient in subtle ways because the AST of such lvalues is in the wrong direction compared to the order of dereferencing pointers (which happens from inside out).
It's worth revisiting separately to not block this PR.