Proving correctness of the GCC match.pd — Part 2

The previous post talked about the background and the GCC GIMPLE IR. This post continues with a look at the format of match.pd.

The match.pd contains transformation rules for the IR, written in a "lispy" domain-specific language. Each transformation rule is specified by the simplify expression that has two operands: a template expression that is matched to the IR, and a replacement expression that replaces the matching expression in the IR. For example

/* x & ~0 -> x */
(simplify
  (bit_and @0 integer_all_onesp)
  @0)

match expressions corresponding to "x&~0" and replaces them with "x".

A template operand of the form @<number> is called a "capture" — it captures the operand so you can refer to it in other parts of the simplify expression. Using the same capture multiple times in a template means that the operands need to be identical, e.g.

/* x & x -> x */
(simplify
  (bit_and @0 @0)
  @0)

match a bit_and with two identical operands.

The predicates, such as integer_all_onesp in the first example above, are the normal predicates used in the GCC middle-end. It is possible to capture operators and predicates too, so you may write

/* x | ~0 -> ~0 */
(simplify
  (bit_ior @0 integer_all_onesp@1)
  @1)

for the rule that changes "x|~0" to "~0".

Pattern matching for commutative operators may use the :c decoration to match the operands in any order. For example

/* x | ~0 -> ~0 */
(simplify
  (bit_ior:c @0 integer_all_onesp@1)
  @1)

will match both "x|~0" and "~0|x" (although it does not matter in this case, as the GCC IR always has the constant as its second argument for commutative operations).

There are cases where you cannot express the replacement using this syntax, so it is possible to generate the replacement expression using C++ code by placing it between curly braces

/* x ^ x -> 0 */
(simplify
  (bit_xor @0 @0)
  { build_zero_cst (type); })

The type of the outermost matching expression (i.e. the type of the bit_xor) is available in the variable type.

It is often the case that additional conditions need to be fulfilled in order to permit the replacement. This can be handled with an if expression:

/* x / -1 -> -x */
(simplify
  (exact_div @0 integer_minus_onep)
  (if (!TYPE_UNSIGNED (type))
   (negate @0)))

This replaces the original expression only if the type of the outermost expression is signed. The operand to if is a C-style expression, so it is possible to create complex conditions, such as

(if (!HONOR_SNANS (element_mode (type))
     && (!HONOR_SIGNED_ZEROS (element_mode (type))
         || !COMPLEX_FLOAT_TYPE_P (type)))

Many rules are identical for several operations, and you can handle this with a for expression

/* x / -1 -> -x */
(for div (trunc_div ceil_div floor_div round_div exact_div)
 (simplify
   (div @0 integer_minus_onep)
   (if (!TYPE_UNSIGNED (type))
    (negate @0))))

The if and for can be nested arbitrarily, and you can use them to construct complex rules where multiple simplifications are done within the same for or if expression.

Finally, there are some additional functionality, such as specifying parts of templates optional, but I'll wait with that until I have made some progress with the functionality described so far...

The next blog post will look at actually proving things.