[LVI] Introduce an intersect operation on lattice values


[LVI] Introduce an intersect operation on lattice values

LVI has several separate sources of facts - edge local conditions, recursive queries, assumes, and control independent value facts - which all apply to the same value at the same location. The existing implementation was very conservative about exploiting all of these facts at once.

This change introduces an "intersect" function specifically to abstract the action of picking a good set of facts from all of the separate facts given. At the moment, this function is relatively simple (i.e. mostly just reuses the bits which were already there), but even the minor additions reveal the inherent power. For example, JumpThreading is now capable of doing an inductive proof that a particular value is always positive and removing a half range check.

I'm currently only using the new intersect function in one place. If folks are happy with the direction of the work, I plan on making a series of small changes without review to replace mergeIn with intersect at all the appropriate places.

Differential Revision: http://reviews.llvm.org/D14476


reamesFeb 1 2016, 7:15 PM
Differential Revision
D14476: [LVI] Introduce an intersect operation on lattice values
rL259460: Add comments.