More advanced lattices for more precise analysis

[spacekitteh]

So, let's say I have a lattice which I know happens to be a Heyting algebra - that is, a lattice with an implication operator (every finite, distributive lattice is an example of a Heyting algebra; so are intuitionistic type theories).

There must be some way in which we can use these more advanced properties! For example, a simple constant propagation analysis might produce this fact at an if-then-else node: (b → x = 1) ∧ (!b → x = 5)

Now, this same fact might be able to be derived from interleaving in a dataflow analysis, but it would probably be much harder to automatically take advantage of more complicated facts.

[spacekitteh]

One particularly interesting method is by using so-called "Logical lattices", outlined in Combining Abstract Interpreters. A logical lattice is one where the order is implication, with the base set being the set of finite conjunctions over some theory. They further show a method to combine multiple lattices (c.f. #42 ) which results in an extremely precise lattice (more precise than the reduced product), assuming some suitable conditions (convexity, stably infinite input lattices, and disjoint theories (apart from equality)). The downside is that the join and existential operators, at least in their implementation, have O(n^2) complexity, but that looks like it can be countered by laziness.