Page MenuHomePhabricator

Fix Side-Conditions in SimplifyCFG for Creating Switches from InstCombine And Mask'd Comparisons

Authored by tjablin on Jun 15 2016, 3:52 PM.



This is just the correctness fix from D21397.

SimplifyCFG is able to detect the pattern:

(i == 5334 || i == 5335)


((i & -2) == 5334)

This transformation has some incorrect side conditions. Specifically, the transformation is only applied when the right-hand side constant (5334 in the example) is a power of two not equal and not equal to the negated mask. These side conditions were added in r258904 to fix PR26323. The correct side condition is that: ((Constant & Mask) == Constant)[(5334 & -2) == 5334].

It's a little bit hard to see why these transformations are correct and what the side conditions ought to be. Here is a CVC3 program to verify them for 64-bit values:

x    : BITVECTOR(64);
y    : BITVECTOR(64);
z    : BITVECTOR(64);
mask : BITVECTOR(64) = BVSHL(ONE, z);
QUERY( (y & ~mask = y) =>
       ((x & ~mask = y) <=> (x = y OR x = (y |  mask)))

Please note that each pattern must be a dual implication (<--> or iff). One directional implication can create spurious matches. If the implication is only one-way, an unsatisfiable condition on the left side can imply a satisfiable condition on the right side. Dual implication ensures that satisfiable conditions are transformed to other satisfiable conditions and unsatisfiable conditions are transformed to other unsatisfiable conditions.

Here is a concrete example of a unsatisfiable condition on the left implying a satisfiable condition on the right:
mask = (1 << z)
(x & ~mask) == y --> (x == y || x == (y | mask))

Substituting y = 3, z = 0 yields:
(x & -2) == 3 --> (x == 3 || x == 2)

The version of this code before r258904 had no side-conditions and incorrectly justified itself in comments through one-directional implication.

Diff Detail

Event Timeline

tjablin updated this revision to Diff 60924.Jun 15 2016, 3:52 PM
tjablin retitled this revision from to Fix Side-Conditions in SimplifyCFG for Creating Switches from InstCombine And Mask'd Comparisons.
tjablin updated this object.
tjablin added a subscriber: llvm-commits.
chandlerc edited edge metadata.Jun 15 2016, 4:04 PM

(i'd love for David to handle the review here, he's much more familiar with using theorem provers to document the correctness here)

majnemer accepted this revision.Jun 15 2016, 4:40 PM
majnemer edited edge metadata.



Could we use m_APInt here?

This revision is now accepted and ready to land.Jun 15 2016, 4:40 PM
tjablin added inline comments.Jun 15 2016, 6:40 PM

Yes. After this is committed, I will prepare an NFC patch with the changes you requested.

cycheng closed this revision.Jun 16 2016, 1:45 AM
cycheng edited edge metadata.

Committed r272873 (On behalf of Tom)