Add a mathematical constraint system

[kripken]

This allows defining constraints like { x >= 0 && x <= 100 } and to then check if they
imply something else is true or false, like { x >= 0 && x <= 100 } => { x < 9999 }
(example of a valid inference).

This is the minimal first part of such a system, focusing on ==, !=, and very simple
solving. Putting up for design feedback before I work in depth on the rest.

Next steps are to add >=, < etc., and to add a pass that uses this in a control-flow
aware way, that is, the goal is to optimize things like

if (x > 10) {
   assert(x > 0); // this can be removed
}

This is important to remove userspace bounds checks for Kotlin (and likely Java).

inplace_vector part here is from #8814 (will rebase once it lands).

[tlively]

I highly recommend explicitly framing the constraint space as a lattice:

1. Both and_ and fuzzyOr are effectively merging constraints. You want both (but especially fuzzyOr) to have all the properties of a lattice join operator: monotonicity, associativity, commutativity, idempotency, etc. You also want fuzzyOr to be as precise as possible; it has to lose some precision sometimes, but you only want it to lose as much precision as necessary given the representation of constraints. So you want it to be a least upper bound, i.e. a join.
2. Making the constraint space a lattice will give you all the nice properties you want for using it in a program analysis: order-independence, guaranteed convergence, etc. It also reduces all the novelty and complexity to just generating the constraints in the first place; getting to the fixed point after that is just the classic worklist + graph traversal pattern.
3. Making the constraint space a lattice will let you test it in the lattice fuzzer, which can do a better job than just unit tests alone of making sure it has all the properties we want, including that we do not unnecessarily lose precision in the merge operation.

[tlively]

I did have that POC for pulling in Z3. In the limit I guess that's what we'd want. 5c2bbb7

[tlively]

Perhaps proves or implies?

[kripken]

Hmm, yeah. Another option is eval as @MaxGraey suggests?

[MaxGraey]

That's awesome!

Have you considered more academic and conventional naming for lattice-like stuff?

Value -> Term
Result -> KnownTruth
ConstraintSet -> Conjunction

check(conj) -> eval(conj)
and_(conj) -> meet(conj) / meetWith(conj)
fuzzyOr(conj) -> join(conj) / joinWith(conj)

or something like this?

[kripken]

@tlively Definitely making this a lattice would have benefits, but it would add overhead and complexity, I worry. Specifically, having a limited capacity (number of constraints in a set), as in the current design, is really nice for efficiency, but makes it not a lattice. Here is a concrete example. For a lattice we need this absorption law: (a ^ b) v b == b. Take

a = { x >= 10 && x <= 20 }  ;; span of numbers: 10, 11, .., to 20
b = { x & 1 }               ;; all odd numbers

a ^ b should be the set of odd numbers in that range, i.e., 11, 13, .., 19. However, that can't be written if the capacity is 2. So a ^ b loses something. That doesn't mean it isn't useful! We can define a ^ b to contain any 2 of the 3 constraints being combined (this can prove fewer things, but more than nothing). E.g. a ^ b = a (just ignore b). But then

(a ^ b) v b == a v b != b

which breaks the absorption rule.

(This is sort of parallel to the issue with multiple constants in possible-constants - we only support one constant, not an arbitrary number. An arbitrary number is necessary for all the nice mathematical properties we want, but the overhead isn't worth it in GUFA.)

[kripken]

@MaxGraey

Value -> Term

Good idea, I think that makes sense.

Result -> KnownTruth

I think this is clear enough already, and shorter?

ConstraintSet -> Conjunction

I left this intentionally vague as this may expand in the future. A set of constraints is, atm, a conjunction, but if we find a nice way to allow OR and not just AND, we should add it. The idea is, conceptually, a set of constraints that can prove things.

[MaxGraey]

Btw binaryen already has some basic semi and full lattices: https://github.com/WebAssembly/binaryen/blob/main/src/analysis/lattice.h and https://github.com/WebAssembly/binaryen/blob/main/src/analysis/lattices/abstraction.h infra. So how about this?

class LowerBound : Lattice { ... }
class UpperBound : FullLattice { ... }
class RangeBound : FullLattice { ... }

[tlively]

Specifically, having a limited capacity (number of constraints in a set), as in the current design, is really nice for efficiency, but makes it not a lattice.

Certainly you cannot have all three of these properties:

1. The constraint system is a lattice.
2. The constraints have bounded representation.
3. The join and meet operators are logical or and logical and with full precision.

We both agree that we must give up on (3). I'm just saying that we should design the system such that we can still have (1) and (2) instead of just (2). Designing the system to be a lattice will require some care and perhaps some additional compromises on precision, but I strongly believe the benefits would be worth it.

One option would be to come up with all the constraints we're interested in, then figure out how to structure them properly to make sure they form a lattice.

Another way to keep things simple would be to use the product of multiple simpler lattices for the analysis. For example, we could simultaneously do a range analysis, sign analysis, and bit analysis, each of which is very simple to understand. Each individual component of the larger lattice could be developed independently.

Otherwise we should just pull in Z3 rather than reinventing the wheel for an arbitrary constraint solver.

[kripken]

One option would be to come up with all the constraints we're interested in, then figure out how to structure them properly to make sure they form a lattice.

Here are the ones we know we want, from direct user feedback:

• Ranges, things like x >= 10 && x <= 20, for bounds check removal
• Equality/inequality, like x != null for null check removal
• Subtyping checks, like isSubType(x, T) for cast check removal

And possibly other things that are common in branch conditions (the above three are all derived from that). E.g. if if (x & 1) { .. } is common then we want x & 1 - we could gather data here to be more precise.

The product of lattices for each of those things grows large quickly, so I worry about overhead there.

Z3 is definitely an option in the long term, but (1) we need only a tiny subset of it, and (2) we really want a wasm constraint solver, and implementing wasm-isms in Z3 (like subtyping etc.) may be difficult/inefficient.

To be clear about the scope: This rather small PR adds !=, ==. Later PRs can add <=, >, isSubType and will not grow this code by much. The final step is a generic pass that uses this in a control-flow-aware way - that is code we need even if we use Z3.

So all this will remain quite small and focused: this is not a big project!

[tlively]

The most trivial way to turn the current constraint system into a lattice is to define a total order on Constraint:

• join (i.e. fuzzyOr) would do what the current codes does where it sees if the new constraints are subsumed by or subsume the current constraints. If not, the result would be top (which is similar to what the current code does, except that the empty constraint set does double duty as top and bottom in the current code).
• meet (i.e. and_) would similarly check whether the new constraints are subsumed by or subsume the current constraints. Any extra new constraints (i.e. those not related to existing constraints) would be added if there is space for them, and otherwise only the top 3 constraints according to the arbitrary total order on constraints would be kept.

This logic can be abstracted out into a generic BoundedConjunction<L, N> lattice, then Constraint can be its own lattice where checks (or proves or whatever) is the < operator for the lattice, then the analysis here could just use Conjunction<Constraint, 3>.

(Note that BoundedConjunction would be a join semilattice, not a full lattice. But that's sufficient for our purposes. We probably should choose a name other than meet to avoid confusion.)