GUFA: Fix a nondeterminism bug by pre-filtering

[kripken]

The repeated "merge new content in, and filter based on the location it
arrives to" operation is non-commutative, and it turns out there was a
corner case we missed. Filtering before and after is enough to make us
return the same result with the ordering swapped.

This does make GUFA 5% slower, unfortunately. But this does result
in better code in some cases aside from fixing the nondeterminism.

Also add clearer comments about the problem here. We likely need to
just make the order of operations here deterministic (though a downside
of that is that the fuzzer wouldn't find bugs like this, and it would be
slower).

[tlively]

Abstract interpretation works deterministically no matter what order you choose to evaluate the transfer functions in on the way to the fixed point result. This property is a result of transfer functions being monotonic and the abstract domain being a lattice. I would be surprised if GUFA filtering inputs and outputs for every node does not give the same property. Are there any examples of non-monotonicity in the analysis, or some reason the domain of possible contents and their join and meet operations do not form a lattice?

[kripken]

A concrete example is in the comment starting with For example, if we start e.g. with a ref.func literal. The underlying issue, as mentioned in the PR description, is that the operation we perform is non-commutative. As a result, if the data arrives in order A, B, C (A arrives, we blend in B, then we blend in C), the result can differ if the order was instead C, B, A or anything else.

"Blend" in the last paragraph is the key point. If we just merged in data we'd be fine. But we also filter at each step. That is important for improving the quality of the result, but breaks commutativity.

Note that the operation is monotonic (after each merge+filter, we have not decreased), and we do operate on a lattice (each two values in PossibleContents have proper bounds), but lack of commutativity breaks determinism. It is easily fixable - pick a deterministic order - but that has the 2 downsides mentioned in the description (still... maybe we should do it).

[tlively]

But that ref.func literal example is fixed by filtering first, right? That's what the paragraph says later, unless I'm misunderstanding it. Is there an example that is not fixed by filtering first?

[kripken]

Yes, pre-filtering fixes that one example (and is just an improvement in general). But I am skeptical that it fixes everything. In general, such combinations of "lossy" set unions and intersections is not guaranteed to have nice properties like commutativity, as the example shows.

But you made me wonder about this a bit more. With pre-filtering, the operations we do at each step are:

1. Intersect the incoming value I with the maximal contents M, I' = I ^ M (pre-filtering)
2. The existing content E is unioned with that, E' = E u I'
3. That is intersected with the maximal contents, E = E' ^ M (post-filtering)

So overall we are repeatedly doing E = ((I ^ M) u E) ^ M. Call that E = f(E, I). Then the question is whether the f operator is commutative.

Without prefiltering we know that g(E, I) = (I u E) ^ M is not commutative, as the example shows, but perhaps f is. We do have M twice in the expression, which suggests something might simplify out. In fact, if we have the distributive property on ^, u, we could write

f(E, I) =
((I ^ M) u E) ^ M =
((I ^ M) ^ M) u (E ^ M) =  ;; distributivity
(I ^ M) u (E ^ M) =        ;; idempotence
(I u E) ^ M =              ;; distributivity
g(E, I)

But we know f != g (this PR has an example), hence ^, u is not distributive. Again, that is maybe not surprising since "lossy" set unions and intersections will not be in general.

f might still be commutative despite all that, but proving it would require checking all the combinations of all the interactions between the PossibleContents variants... unless you have some idea?

[tlively]

I don't have any other ideas, but distributivity coming up is interesting. Chapter 9 of the static program analysis text we've been using is entirely about how distributivity of transfer functions allows for much more efficient context-sensitive interprocedural analyses.

But distributivity, commutativity, and all the rest of it shouldn't matter for the final result if the transfer functions are monotone. "In a complete lattice L with finite height, every monotone function f : L → L has a unique least fixed point denoted lfp(f) defined as ..." If we're iterating to the smallest fixed point of the transfer function for the whole program, the order of CFG fragments for which we evaluate the transfer function shouldn't matter. It seems the best way to fix non-determinism bugs would be to ensure the transfer function is monotone, and with our static analysis framework, we can check that this is the case via fuzzing.

[kripken]

But distributivity, commutativity, and all the rest of it shouldn't matter for the final result if the transfer functions are monotone.

Wait, aren't those properties necessary? The theorem is:

"In a complete lattice L with finite height, every monotone function f : L → L has a unique least fixed point denoted lfp(f) defined as ..."

Monotonicity is not enough, it also needs to be on a lattice, which has commutativity etc.

It seems the best way to fix non-determinism bugs would be to ensure the transfer function is monotone

Again, GUFA is monotone [0]. Every update E = ((I ^ M) u E) ^ M (or, before pre-filtering, E = (I u E) ^ M) is at least as much as the value before.

Or, putting it another way: Assume we have items arriving, A, B, C, D, and they lead to the monotonically increasing amounts 10, 20, 30, 40. That is, A gives 10; A u B gives 20, A u B u C gives 30 and ..u D gives 40. It is possible to have another order, D, C, B, A in which the amounts end up 15, 25, 35, 45. Commutativity etc. would prevent that, but without it, it matters the order in which they arrive.

[0] At least AFAIK. I believe we have an assertion on it that has never fired. But we do not have a proof.

[tlively]

But possible-contents is a lattice, and the set of possible-contents for every value of the program is another, bigger lattice. Is there something wrong with our union and intersection operators that prevent the implementation from being a lattice?

Assume we have items arriving, A, B, C, D, and they lead to the monotonically increasing amounts 10, 20, 30, 40. That is, A gives 10; A u B gives 20, A u B u C gives 30 and ..u D gives 40. It is possible to have another order, D, C, B, A in which the amounts end up 15, 25, 35, 45. Commutativity etc. would prevent that, but without it, it matters the order in which they arrive.

Sure, the intermediate values on the way to final solution can be different, but if we have a monotone function on a lattice and we are iterating to a fixed point, then we can't ever arrive at any solution other than the least fixed point.

[kripken]

Oh, I think I see where we are missing each other:

1. PossibleContents is a lattice with the operations u and ^. Those are commutative etc.
2. But we don't just use u in each iteration of GUFA, we use this operation: f_M(E, I) = (I u E) ^ M. That is a different operation, and not commutative (though it is monotonic).

[kripken]

We figured the issue out offline, summary:

• Abstract interpretation of a node with two inputs: f(left u right), where f is the transfer function of the node (say, an i32.xor).
• GUFA on two inputs: g(new u g(old)) (or in reverse order), where g is the refining operation that applies the type information at each node, that is, g_e(v) = v ^ type(e) (intersect/meet with the type of the node).

That is, GUFA is a simple flow operation of data, with a history: each iteration we take the new input, merge with the old, and then refine the result. We will end up with a final result at that node of many g operations. If g is something simple like set intersection that does not matter, but with the limited shapes PossibleContents allows, that makes the order end up mattering in rare cases like this PR fixes. And, in particular, we don't have the ability to use symmetry etc. like abstract interpretation does on left u right (which makes the order not matter).

It may be interesting to make GUFA more like abstract interpretation: fetch all the predecessor nodes and join them, as opposed to joining a single arrival at a time with the old state. That might be slower in some cases, not clear. It would avoid the loss of precision of repeated application of g, which would be nice (though it isn't clear how much loss of precision we have after this PR).

[tlively]

Using a more traditional transfer function would also remove the need for separate pre- and post-filtering. Instead, the filtering would happen just once, in the transfer function itself. This uses distributivity of ^ and u: U_i (I_i ^ M) = (U_i I_i) ^ M.

[tlively]

Ideally we could point out an example of non-monotonicity to explain why we have nondeterminism bugs, but LGTM to land regardless.