Proof-carrying code: change range facts to be more general.

[cfallin]

Previously, the proof-carrying code (PCC) mechanism optionally described each value in the program with at most one fact of the form:

• A static range (min, max are u64s);
• A dynamic range (min, max are symbolic expressions: sums of global values or SSA values and offsets)

This worked well enough in filetests that exercised PCC for static and dynamic Wasm memory cases: the fact language was expressive enough to describe all the invariants.

However, as soon as the optimizer started to combine different accesses together -- for example, by sharing one select_spectre_guard across multiple accesses -- it quickly became apparent that we might need to describe both a static and dynamic range for one value. The existing system fails to check, producing Conflict facts, on the new test in pcc_memory.rs here.

To make the fact language more expressive, I worked through a series of more expressive variants until finding one that seems to work:

• First, a variant with combined static and dynamic ranges: e.g., range(0, 0xffff, 0, gv1) means that a value is within the given static range and also less than or equal to gv1. This allows the intersection of dynamic and static facts to work, but has a lot of weird edge-cases because it's like two analyses glued together in a product type; we really want to cross-compare against the two sometimes, e.g. if we know static range facts about the symbolic expressions and want to apply those elsewhere. It also led to weird logic due to redundancy: the expressions could also be constants (no "base value") and so we handled the constant-value case twice. It seemed that actually the two worlds should be merged completely.

• Next, a variant with only Exprs, and two cases for a range: Exact (with one or more expressions that are known to be equivalent to the value) and Inclusive, with min and max lists. In both cases we want lists because we may know that a value is, for example, less than both v1 and gv2; both are needed to prove different things, and the relative order of the two is not known so it cannot be simplified.

  This was almost right; it fell apart only when working out apply_inequality where it became apparent that we need to sometimes state that a value is exactly equal to some expressions and less than others (e.g., exactly v1 and also in a 32-bit range).

  Aside from that it was also a bit awkward to have a four-case (or three-case for commutative) breakdown in all ops: exact+exact, exact+inclusive, inclusive+inclusive.

• Finally, the variant in this PR: every range is described by three lists, the min, equal and max sets of expressions.

The way this works is: for any value for which we have a fact, we collect lower and upper bounds, and also expressions we know it's equivalent to. Like an egraph, we don't drop facts or "simplify" along the way, because any of the bits may be useful later. However we don't explode in memory or analysis time because this is bounded by the stated facts: we locally derive the "maximum fact" for the result of an addition, then check if it implies the stated fact on the actual result, then keep only that stated fact.

The value described by these sets is within the interval that is the intersection of all combinations of min/max values; this makes intersect quite simple (union the sets of bounds, and the equalities, because it must be both). Some of the other ops and tests -- union, and especially "is this value in the range" or "does this range imply this other range" -- are a little intricate, but I think correct. To pick a random example: an expression is within a range if we can prove that it is greater than or equal to all lower bounds, and vice-versa for upper bounds; OR if it is exactly equal to one of the equality bounds. Equality is structural on Exprs (i.e., the default derived Eq is valid) because they are not redundant: there is only one way to express v1+1, and we can never prove that v1 == v2 within the context of one expression.

I will likely write up a bunch more in the top doc-comment and throughout the code; this is meant to get the working system in first. (I'm also happy to do this as part of this PR if preferred.)

There are also some ideas for performance improvement if needed, e.g. by interning ValueRanges and then memoizing the operations (intersect(range2, range5) = range7 in a lookup table). I haven't measured perf yet.

I also haven't fuzzed this yet but will do so and then submit any required bugfixes separately. Hopefully we can get this turned on soon!

[cfallin]

With some more testing I've found the equality mechanism to be a little fragile (specifically around constants, as well as the above-mentioned quadratic representation for multiple merged SSA vals), and I need to go have a think; so I'm gonna switch this to "draft" mode.

[cfallin]

After a little more thought around both the specific last issues seen here, and the efficiency in general of the larger facts, I had the above-mentioned think, and now I have a thought on a new approach that I'd like to document here before (unfortunately) having to context-switch away for a bit.

To recap, the current state is:

• main today has PCC that works fine for static checks (memory with sufficiently large guard regions); the range facts are compact Copy structs that describe statically-known integer bounds.

• The difficulties arise when modeling symbolic expressions and comparisons between them that arise with dynamic checks -- specifically, tying together a compare with a conditional-select -- when this interacts either with optimizations merging things together or with constant values.

In my view, these difficulties are symptoms of trying to represent a "slice" of the overall worldview (partial order relation between program values) in facts on individual values. That is, from the perspective of an individual value, we have to carry around its inequalities with a bunch of other values in case we need them. Furthermore, because facts are attached to values, when constants are involved, we can lose track of things: a constant value can be rematerialized or incorporated in a bunch of different places and does not have a stable identity like an SSA value v1 does.

So, IMHO a reasonable solution might be to build a "whole worldview" data structure, and share it across the function. One can see this as taking this PR a bit further: this PR lets a fact on a single value talk about multiple relations (so single facts go from atomic tidbits to slices of the whole world); instead let's build "the whole world" and then point into it.

To be more concrete, I envision a "partial order relation DAG" with nodes that represent sets of equal values, either symbolic (SSA values, global values) or concrete (integer constants), and edges that represent less-than-or-equal relations. Edge labels represent known "distance" (e.g. 5 on edge from x to y means x + 5 <= y), and edges can also be labeled with predicates that make them true (value v1, the result of an icmp, implies v2 <= v3).

The idea is that we can point to any given node in this DAG from a fact on a value in the IR; these DAG nodes don't actually need to track the set of equal values (that's implicit in the set of all nodes that point to them); and we can do a union-find-like thing to efficiently answer less-than queries. Basically we can implement le(node1, node2, Option<pred>) -> Option<distance> where we get a Some(min_distance) if there is some path from one node to another (enabling edges labeled under pred if present), where min_distance is the sum of edge labels. Then we can compress the path by adding a direct edge (transitivity!) to make further queries more efficient. I suspect this will lead to a fairly efficient overall check of a function body, because the same comparisons will be done over and over. (E.g., different offsets from a base pointer into a struct, all less than the guard-region size.)

As mentioned I need to context-switch away for a bit but I'll try to get back to this at some point!