Passes using multiple types of facts (aka snooping) about hoopl HOT 1 OPEN

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 (cf #41). They further show a method to combine multiple lattices 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.

from hoopl.