Upstream simplifier rule verification tool

apps/CMakeLists.txt

@@ -74,6 +74,7 @@ add_app(nl_means)
 add_app(onnx)
 add_app(resize)
 add_app(resnet_50)
+add_app(simplifier_rule_verifier)
 add_app(stencil_chain)
 add_app(unsharp)
 add_app(wavelet)

apps/simplifier_rule_verifier/.gitignore

@@ -0,0 +1,2 @@
+bin
+*.inc

apps/simplifier_rule_verifier/CMakeLists.txt

@@ -0,0 +1,118 @@
+cmake_minimum_required(VERSION 3.28)
+project(simplifier_rule_verifier)
+
+enable_testing()
+
+# Set up language settings
+set(CMAKE_CXX_STANDARD 17)
+set(CMAKE_CXX_STANDARD_REQUIRED YES)
+set(CMAKE_CXX_EXTENSIONS NO)
+
+# Find Halide
+find_package(Halide REQUIRED)
+
+add_library(
+    rule_verifier_support STATIC
+    expr_util.cpp
+    parser.cpp
+    reduction_order.cpp
+    super_simplify.cpp
+    z3.cpp
+)
+target_link_libraries(rule_verifier_support PUBLIC Halide::Halide Halide::Tools)
+target_include_directories(rule_verifier_support PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
+
+add_executable(filter_rewrite_rules filter_rewrite_rules.cpp)
+target_link_libraries(filter_rewrite_rules PRIVATE rule_verifier_support)
+
+add_executable(super_simplify super_simplify_tool.cpp)
+target_link_libraries(super_simplify PRIVATE rule_verifier_support)
+
+# Both tools shell out to z3, so there's nothing to test without it.
+find_program(Z3_EXECUTABLE z3)
+if (NOT Z3_EXECUTABLE)
+    message(STATUS "z3 not found; skipping the apps/simplifier_rule_verifier tests")
+    return()
+endif ()
+
+add_test(
+    NAME rule_verifier_good_rules
+    COMMAND filter_rewrite_rules ${CMAKE_CURRENT_SOURCE_DIR}/test/good_rules.txt
+)
+set_tests_properties(
+    rule_verifier_good_rules
+    PROPERTIES
+    ENVIRONMENT "HL_Z3=${Z3_EXECUTABLE}"
+    LABELS simplifier_rule_verifier
+    PASS_REGULAR_EXPRESSION
+        "0 rule\\(s\\) were disproved by z3\n0 rule\\(s\\) could not be verified by z3\n0 rule\\(s\\) did not obey the reduction order\nSuccess!"
+)
+
+# These rules are supposed to be rejected, so the tool is expected to fail. Pin
+# down the number of each sort of failure, so that a rule slipping through
+# unnoticed is a test failure too.
+add_test(
+    NAME rule_verifier_bad_rules
+    COMMAND filter_rewrite_rules ${CMAKE_CURRENT_SOURCE_DIR}/test/bad_rules.txt
+)
+set_tests_properties(
+    rule_verifier_bad_rules
+    PROPERTIES
+    ENVIRONMENT "HL_Z3=${Z3_EXECUTABLE}"
+    LABELS simplifier_rule_verifier
+    PASS_REGULAR_EXPRESSION
+        "2 rule\\(s\\) were disproved by z3\n0 rule\\(s\\) could not be verified by z3\n8 rule\\(s\\) did not obey the reduction order\nFailure!"
+)
+
+# Every rule here is only true if the parser reads it with the intended
+# precedence and associativity, so a regression in the grammar shows up as a
+# rule z3 can disprove.
+add_test(
+    NAME rule_verifier_parser_rules
+    COMMAND filter_rewrite_rules ${CMAKE_CURRENT_SOURCE_DIR}/test/parser_rules.txt
+)
+set_tests_properties(
+    rule_verifier_parser_rules
+    PROPERTIES
+    ENVIRONMENT "HL_Z3=${Z3_EXECUTABLE}"
+    LABELS simplifier_rule_verifier
+    PASS_REGULAR_EXPRESSION
+        "0 rule\\(s\\) were disproved by z3\n0 rule\\(s\\) could not be verified by z3\n0 rule\\(s\\) did not obey the reduction order\nSuccess!"
+)
+
+add_test(
+    NAME rule_verifier_narrow_int_rules
+    COMMAND filter_rewrite_rules ${CMAKE_CURRENT_SOURCE_DIR}/test/narrow_int_rules.txt
+)
+set_tests_properties(
+    rule_verifier_narrow_int_rules
+    PROPERTIES
+    ENVIRONMENT "HL_Z3=${Z3_EXECUTABLE}"
+    LABELS simplifier_rule_verifier
+    PASS_REGULAR_EXPRESSION
+        "0 rule\\(s\\) were disproved by z3\n0 rule\\(s\\) could not be verified by z3\n0 rule\\(s\\) did not obey the reduction order\nSuccess!"
+)
+
+add_test(
+    NAME rule_verifier_synthesize_predicates
+    COMMAND filter_rewrite_rules ${CMAKE_CURRENT_SOURCE_DIR}/test/rules_needing_predicates.txt
+)
+set_tests_properties(
+    rule_verifier_synthesize_predicates
+    PROPERTIES
+    ENVIRONMENT "HL_Z3=${Z3_EXECUTABLE}"
+    LABELS simplifier_rule_verifier
+    PASS_REGULAR_EXPRESSION "rewrite\\(min\\(x\\*c0, y\\*c0\\), min\\(x, y\\)\\*c0, 0 <= c0\\)"
+)
+
+add_test(
+    NAME rule_verifier_super_simplify
+    COMMAND super_simplify ${CMAKE_CURRENT_SOURCE_DIR}/test/exprs.txt 4
+)
+set_tests_properties(
+    rule_verifier_super_simplify
+    PROPERTIES
+    ENVIRONMENT "HL_Z3=${Z3_EXECUTABLE}"
+    LABELS simplifier_rule_verifier
+    PASS_REGULAR_EXPRESSION "select\\(x < y, x, y\\) -> min\\(x, y\\)"
+)

apps/simplifier_rule_verifier/Makefile

@@ -0,0 +1,31 @@
+include ../support/Makefile.inc
+
+CXXFLAGS += -O2 -g
+
+OBJECTS = $(BIN)/expr_util.o $(BIN)/parser.o $(BIN)/reduction_order.o \
+          $(BIN)/super_simplify.o $(BIN)/z3.o
+
+all: $(BIN)/filter_rewrite_rules $(BIN)/super_simplify
+
+$(BIN)/%.o: %.cpp %.h
+	@mkdir -p $(@D)
+	$(CXX) $(CXXFLAGS) -c $< -o $@
+
+$(BIN)/filter_rewrite_rules: filter_rewrite_rules.cpp $(OBJECTS) $(LIB_HALIDE)
+	@mkdir -p $(@D)
+	$(CXX) $(CXXFLAGS) $< $(OBJECTS) -o $@ $(LIBHALIDE_LDFLAGS)
+
+$(BIN)/super_simplify: super_simplify_tool.cpp $(OBJECTS) $(LIB_HALIDE)
+	@mkdir -p $(@D)
+	$(CXX) $(CXXFLAGS) $< $(OBJECTS) -o $@ $(LIBHALIDE_LDFLAGS)
+
+test: $(BIN)/filter_rewrite_rules $(BIN)/super_simplify
+	$(BIN)/filter_rewrite_rules test/good_rules.txt
+	! $(BIN)/filter_rewrite_rules test/bad_rules.txt
+	$(BIN)/filter_rewrite_rules test/parser_rules.txt
+	$(BIN)/filter_rewrite_rules test/narrow_int_rules.txt
+	$(BIN)/filter_rewrite_rules test/rules_needing_predicates.txt
+	$(BIN)/super_simplify test/exprs.txt 4
+
+clean:
+	rm -rf $(BIN)

apps/simplifier_rule_verifier/README.md

@@ -0,0 +1,108 @@
+# simplifier_rule_verifier
+
+Tools for checking and generating rewrite rules for Halide's simplifier
+(`src/Simplify_*.cpp`). They were written for the paper "Verifying and Improving
+Halide's Term Rewriting System with Program Synthesis" (Newcomb et al., OOPSLA
+2021).
+
+Both tools shell out to [z3](https://github.com/Z3Prover/z3), so it needs to be
+on your `PATH`, or named by the `HL_Z3` environment variable. Set
+`HL_DEBUG_RULE_VERIFIER` to 1 or 2 for progress and z3 queries on stderr, and
+`HL_Z3_TIMEOUT` to raise the per-query limit in seconds from the default 60,
+which some rules with several symbolic constants under a div or mod need.
+
+## filter_rewrite_rules
+
+```
+filter_rewrite_rules rules.txt [output_dir]
+```
+
+Takes a file of proposed simplifier rules, one per line, in the same syntax used
+in `src/Simplify_*.cpp`:
+
+```
+rewrite(min(x, y) + max(x, y), x + y)
+rewrite((x + c0) + c1, x + fold(c0 + c1))
+rewrite(x*c0 + y*c0, (x + y)*c0)
+```
+
+Variables named `c0`, `c1`, ... are constant wildcards, and anything else is a
+general wildcard, as in the simplifier itself. A rule may carry a third argument
+giving a predicate under which it applies.
+
+For each rule it checks that:
+
+- The rule is true, by asking z3 to find a counterexample.
+- The rule obeys the reduction order in `reduction_order.cpp`, which is what
+  stops the simplifier from rewriting in circles forever. Roughly, the right
+  hand side must be strictly smaller than the left hand side under an ordering
+  that accounts for both expression size and the specific operations used, so
+  that repeated rewriting must terminate.
+- No other rule in the file subsumes it.
+
+Rules that fail are reported and dropped. The surviving rules are printed
+grouped by the IR node type they apply to, ready to be pasted into the
+corresponding `src/Simplify_*.cpp`. If an output directory is given, each group
+is also written to `Simplify_<node type>.inc` in it.
+
+The tool exits with a non-zero status if any rule was disproved or violated the
+reduction order.
+
+A rule may also be written with a predicate of `false`:
+
+```
+rewrite(min(x*c0, y*c0), min(x, y)*c0, false)
+```
+
+which asks the tool to synthesize the weakest predicate it can find under which
+the rule holds. Above, it finds `0 <= c0`. If it can't prove the predicate it
+synthesized is sufficient, it wraps it in `prove_me(...)` to flag that a human
+needs to finish the job.
+
+### What the checks assume
+
+Signed integers of 32 bits and wider are modelled as unbounded SMT integers, so
+overflow is assumed not to happen - the same assumption the simplifier itself
+makes under `no_overflow_int`. Narrower types are modelled as bit-vectors, which
+do wrap. Division and modulo follow Halide's Euclidean definition at every
+width: `0 <= a%b < |b|`, and both return zero when `b` is zero.
+
+Casts between widths aren't modelled, so a rule that mixes types is reported as
+unverifiable rather than being checked. So is a rule using an intrinsic the SMT
+conversion doesn't know; run with `HL_DEBUG_RULE_VERIFIER=1` to see which.
+
+The reduction order is purely syntactic, so it rejects rules that terminate only
+because a constant strictly decreases on each application, such as
+
+```
+rewrite((x + c0) % c1, (x + fold(c0 % c1)) % c1, c1 > 0 && (c0 >= c1 || c0 < 0))
+```
+
+Rules like that are in the simplifier and are fine; they just can't be justified
+by this tool.
+
+## super_simplify
+
+```
+super_simplify exprs.txt max_size
+```
+
+Takes a file of Halide `Expr`s, one per line, and uses counterexample-guided
+inductive synthesis to search for the smallest equivalent expression of at most
+`max_size` leaves. This is how candidate rules for `filter_rewrite_rules` were
+found in the first place.
+
+## Building
+
+```
+make
+make test
+```
+
+or, from a CMake build of Halide:
+
+```
+cmake -G Ninja -S apps -B apps-build
+cmake --build apps-build --target filter_rewrite_rules super_simplify
+ctest --test-dir apps-build -L simplifier_rule_verifier
+```

apps/simplifier_rule_verifier/debug.h

@@ -0,0 +1,36 @@
+#ifndef SIMPLIFIER_RULE_VERIFIER_DEBUG_H
+#define SIMPLIFIER_RULE_VERIFIER_DEBUG_H
+
+#include <cstdlib>
+#include <iostream>
+#include <utility>
+
+// A stand-in for Halide's internal debug stream, which isn't part of the
+// public API. Messages at a level above the value of the HL_DEBUG_RULE_VERIFIER
+// environment variable are dropped.
+class debug {
+    const bool enabled;
+
+    static int verbosity() {
+        static const int level = []() {
+            const char *s = getenv("HL_DEBUG_RULE_VERIFIER");
+            return s ? atoi(s) : 0;
+        }();
+        return level;
+    }
+
+public:
+    explicit debug(int level)
+        : enabled(level <= verbosity()) {
+    }
+
+    template<typename T>
+    debug &operator<<(T &&x) {
+        if (enabled) {
+            std::cerr << std::forward<T>(x);
+        }
+        return *this;
+    }
+};
+
+#endif