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 { ... }