Add a ConstraintAnalysis pass

[kripken]

This simply parses IR into constraints, flows them around, and sees
if we can prove things.

This is a minimal version, without conditional propagation etc.

[tlively]

Comments on code so far. Will look at tests next.

[tlively]

Can we prove this will actually converge? Can we create a pathological case where the analysis alternates between two different constraint sets forever?

[kripken]

It must converge now because we simply drop extra things in approximateAnd. If we did something more complex, we'd need to be careful and define a total order, I think.

[tlively]

I'm worried that a sequence of ORs (control flow merges) and ANDs (from the contents of blocks) could change the order of constraints so that the one that is dropped is not stable.

[tlively]

Why not keep the beginning constraints instead? Then when we can get to the end of a block, we can merge the current constraints (and eventually any additional constraints due to the specific control flow edge) into the beginning constraints of each successor block and only process that successor block again if its starting constraints are different.

In contrast, the current approach may reprocess successor blocks even if they don't learn anything new from the single predecessor that was updated.

Storing the beginning constraints would also let us avoid re-merging all the predecessors for each block in the optimization phase.

This would also help prove convergence. If we can show that the merge operation on constraint sets is monotonic on some partial order on constraint sets and converges after a bounded number of steps, then we will know the analysis will converge. In contrast, it's hard to say anything about how the end constraints will change over time because they are the result of non-monotonic meet operations over the course of the block.

[kripken]

Interesting, yeah, storing the start might have benefits. It does mean adding a bottom element though, so we can merge incrementally like that.

However, about the very last point: storing the beginning or the end is NFC, so I don't see how it helps with convergence?

[kripken]

Instead of a bottom element it might be cleaner to use std::optional in the pass. That is, there is no logical (as in mathematical logic) meaning to the bottom element - it is not a logical constraint - so a "null" can be handled by the users, rather than inside constraint.h.

However - thinking more on this, I'm not sure it's right. We can't simply keep merging in content as it flows around. The input to a block is, effectively, X || Y || Z, and it matters which of those we update. If we update X three times with a == 10 that is very different than if we update X, Y, Z to that constraint - only then we can apply something.

So I think it is best to do this as it is written: merge the inputs in a loop, seeing them all at once.

[tlively]

Instead of a bottom element it might be cleaner to use std::optional in the pass. That is, there is no logical (as in mathematical logic) meaning to the bottom element - it is not a logical constraint - so a "null" can be handled by the users, rather than inside constraint.h.

Sure, bottom is not literally a bounded set of constraints like other values would be, but it is certainly a meaningful point in the space of possible known constraints. Representing it in constraint.h keeps the analysis code simpler while ensuring that we can never "forget" that we have observed a contradiction. It also lets us write unit tests for it.

If we update X three times with a == 10 that is very different than if we update X, Y, Z to that constraint - only then we can apply something.

I'm not sure what you mean here.

[kripken]

If we receive data from blocks X, Y, and Z, then we only have a valid state after seeing all of X, Y, and Z. That is, if our state starts at some null/bottom, and X arrives, we cannot flow X onward.

Concretely, if X has a == 10 but we haven't seen Y or Z yet, then we don't know if a == 10 is true in this block, and it would be invalid to apply a == 10 in the block and/or to flow it onward.

We only find the valid state of inputs to the block after merging X, Y, and Z. Doing so at once is the simplest way to get the valid state.

[tlively]

When an analysis uses a proper join-semilattice, it's fine to start out with incomplete information because we know that eventually we will reach a sound fixed point where we know everything we need to know.

If you're right that it's not sound to start with incomplete information for one block, then it seems that worklist algorithm for flowing information around would not be sound, since it necessarily starts with incomplete information at loop heads.

But I think it should be fine to start with incomplete information. We don't have a join-semilattice because the OR operation does not go to a unique least upper bound, but it is at least monotonic. We know that the analysis will only ever learn more possibilities (i.e. loosen or drop constraints) as information flows around. So if we start out knowing X has a == 10 and propagate some constraints based on that information, but then later we process Y or Z and learn that a might have some other value, then we will recalculate what we can infer (which will be fewer/looser constraints in general) and then propagate those looser constraints to the successors.

[kripken]

When an analysis uses a proper join-semilattice, it's fine to start out with incomplete information because we know that eventually we will reach a sound fixed point where we know everything we need to know.

Let me put it this way: if we see this as an abstract interpretation situation, then we must calculate the entire transfer function at each node. And the entire transfer function is f(X, Y, Z) = X || Y || Z in this example: we cannot receive only X and propagate that onwards.

Or, here is the actual problem: again, if one predecessor X supplies a == 10, and we are in a block with if (a == 10), then if we just use a == 10 at the start of the block and start to apply it, we'd optimize that if condition. But we can't. Again, we must calculate the entire transfer function at the start of the block before doing anything with that data, so that we have something valid.

Now, we could define the transfer function so that f(X, null, null) == null - effectively blocking propagation until we get info from all sides - but I think it is far more natural to just do the expected thing from the point of view of mathematical logic: we are computing X || Y || Z, so just compute that at the top of each block.

That is, what does null mean from the point of view of logic? I am trying to keep the math pure here 😄

[tlively]

If we had a bottom value to initialize constraints to, then we wouldn't have to distinguish the first constraints like this.

[kripken]

True, yeah. Maybe worth adding, though this might be the only place it helps?