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

cfallin · 2024-02-20T19:57:47Z

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!

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 `u64`s); - 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* `Expr`s, 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 `Expr`s (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 `ValueRange`s 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!

…f `from_width`.

fitzgen

Overall LGTM, just a few questions and general suspicion flagging.

But most importantly: shouldn't there be a new clif filetest or two for the GVN behavior that warranted this fact representation change?