[PATCH] D21397: Teach SimplifyCFG to Create Switches from InstCombine Or Mask'd Comparisons

[Thomas Jablin via llvm-commits]

tjablin created this revision.
tjablin added reviewers: chandlerc, halfdan, majnemer, cycheng.
tjablin added a subscriber: llvm-commits.

I am following Chandler's suggestion by teaching SimplifyCFG to recognize the Or-Mask trick that InstCombine uses to reduce the number of comparisons. Specifically, InstCombine can turn:
  (i == 5334 || i == 5335)
into:
  ((i | 1) == 5335)

SimplifyCFG was already able to detect the pattern:
  (i == 5334 || i == 5335)
to:
  ((i & -2) == 5334)

In the process of making this change, I discovered that the And version of the transformation had some incorrect side conditions. Specifically, the transformation was only applied when right-hand side constant (5334 in the example) was 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:

  ONE  : BITVECTOR(64) = BVZEROEXTEND(0bin1, 63);
  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)))
  );
  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.

This patch supersedes D21315 and resolves PR27555 (https://llvm.org/bugs/show_bug.cgi?id=27555).

http://reviews.llvm.org/D21397

Files:
  lib/Transforms/Utils/SimplifyCFG.cpp
  test/Transforms/SimplifyCFG/switch_create.ll

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D21397.60882.patch
Type: text/x-patch
Size: 5807 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20160615/f497a893/attachment.bin>