diff --git a/apps/CMakeLists.txt b/apps/CMakeLists.txt index 8e27436dfb57..afc90b173081 100644 --- a/apps/CMakeLists.txt +++ b/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) diff --git a/apps/simplifier_rule_verifier/.gitignore b/apps/simplifier_rule_verifier/.gitignore new file mode 100644 index 000000000000..811562b5e88c --- /dev/null +++ b/apps/simplifier_rule_verifier/.gitignore @@ -0,0 +1,2 @@ +bin +*.inc diff --git a/apps/simplifier_rule_verifier/CMakeLists.txt b/apps/simplifier_rule_verifier/CMakeLists.txt new file mode 100644 index 000000000000..7534899a24d2 --- /dev/null +++ b/apps/simplifier_rule_verifier/CMakeLists.txt @@ -0,0 +1,130 @@ +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_float_literals + COMMAND super_simplify ${CMAKE_CURRENT_SOURCE_DIR}/test/float_exprs.txt 1 +) +set_tests_properties( + rule_verifier_float_literals + PROPERTIES + ENVIRONMENT "HL_Z3=${Z3_EXECUTABLE}" + LABELS simplifier_rule_verifier + PASS_REGULAR_EXPRESSION "super_simplify\\(2500\\.000000f\\)" +) + +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\\)" +) diff --git a/apps/simplifier_rule_verifier/Makefile b/apps/simplifier_rule_verifier/Makefile new file mode 100644 index 000000000000..3f5337022db9 --- /dev/null +++ b/apps/simplifier_rule_verifier/Makefile @@ -0,0 +1,32 @@ +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 + $(BIN)/super_simplify test/float_exprs.txt 1 | grep -q "super_simplify(2500.000000f)" + +clean: + rm -rf $(BIN) diff --git a/apps/simplifier_rule_verifier/README.md b/apps/simplifier_rule_verifier/README.md new file mode 100644 index 000000000000..67c113453689 --- /dev/null +++ b/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_.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 +``` diff --git a/apps/simplifier_rule_verifier/debug.h b/apps/simplifier_rule_verifier/debug.h new file mode 100644 index 000000000000..a958ee569606 --- /dev/null +++ b/apps/simplifier_rule_verifier/debug.h @@ -0,0 +1,36 @@ +#ifndef SIMPLIFIER_RULE_VERIFIER_DEBUG_H +#define SIMPLIFIER_RULE_VERIFIER_DEBUG_H + +#include +#include +#include + +// 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 + debug &operator<<(T &&x) { + if (enabled) { + std::cerr << std::forward(x); + } + return *this; + } +}; + +#endif diff --git a/apps/simplifier_rule_verifier/expr_util.cpp b/apps/simplifier_rule_verifier/expr_util.cpp new file mode 100644 index 000000000000..ceea1fb152ed --- /dev/null +++ b/apps/simplifier_rule_verifier/expr_util.cpp @@ -0,0 +1,537 @@ +#include "expr_util.h" + +#include "Halide.h" + +using namespace Halide; +using namespace Halide::Internal; + +using std::map; +using std::string; +using std::vector; + +class FindVars : public IRVisitor { + Scope<> lets; + + void visit(const Variable *op) override { + if (!lets.contains(op->name)) { + auto &v = vars[op->name]; + v.second++; + v.first = op; + } + } + + void visit(const Let *op) override { + op->value.accept(this); + { + ScopedBinding<> bind(lets, op->name); + op->body.accept(this); + } + } + +public: + map> vars; +}; + +map> find_vars(const Expr &e) { + FindVars f; + e.accept(&f); + return f.vars; +} + +template +bool more_general_than(const Expr &a, const Op *b, map &bindings, bool entered_a) { + if (!entered_a) { + map backup = bindings; + if (more_general_than(a, b->a, bindings)) { + return true; + } + bindings = backup; + + if (more_general_than(a, b->b, bindings)) { + return true; + } + bindings = backup; + } + + if (const Op *op_a = a.as()) { + return (more_general_than(op_a->a, b->a, bindings, true) && + more_general_than(op_a->b, b->b, bindings, true)); + } + return false; +} + +bool more_general_than(const Expr &a, const Expr &b, map &bindings, bool entered_a) { + if (const Variable *var = a.as()) { + const Variable *var_b = b.as(); + auto it = bindings.find(var->name); + if (it != bindings.end()) { + return equal(it->second, b); + } else { + bool const_wild = var->name[0] == 'c'; + bool b_const_wild = var_b && (var_b->name[0] == 'c'); + bool b_const = is_const(b); + bool may_bind = !const_wild || (const_wild && (b_const_wild || b_const)); + if (may_bind) { + bindings[var->name] = b; + return true; + } else { + return false; + } + } + } + + if (is_const(a) && is_const(b)) { + return equal(a, b); + } + + if (const And *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const Or *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const Min *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const Max *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const Add *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const Sub *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const Mul *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const Div *op = b.as
()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const Mod *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const LE *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const LT *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const EQ *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const NE *op = b.as()) { + return more_general_than(a, op, bindings, entered_a); + } + + if (const Not *op = b.as()) { + if (!entered_a) { + map backup = bindings; + if (more_general_than(a, op->a, bindings, entered_a)) { + return true; + } + bindings = backup; + } + + const Not *op_a = a.as(); + return (op_a && + more_general_than(op_a->a, op->a, bindings, true)); + } + + if (const Select *op = b.as(); + return (op_a && + more_general_than(op_a->condition, op->condition, bindings, true) && + more_general_than(op_a->true_value, op->true_value, bindings, true) && + more_general_than(op_a->false_value, op->false_value, bindings, true)); + } + + return false; +} + +class FindCommutativeOps : public IRVisitor { + template + void visit_commutative_op(const Op *op) { + const Variable *var_a = op->a.template as(); + const Variable *var_b = op->b.template as(); + const Call *call_b = op->b.template as(); + if ((var_b && var_b->name[0] == 'c') || + is_const(op->b) || + (call_b && call_b->name == "fold")) { + op->a.accept(this); + return; + } + if (var_a || var_b) { + commutative_ops.push_back(Expr(op)); + } + IRVisitor::visit(op); + } + + void visit(const Add *op) override { + visit_commutative_op(op); + } + void visit(const Mul *op) override { + visit_commutative_op(op); + } + void visit(const Min *op) override { + visit_commutative_op(op); + } + void visit(const Max *op) override { + visit_commutative_op(op); + } + void visit(const EQ *op) override { + visit_commutative_op(op); + } + void visit(const NE *op) override { + visit_commutative_op(op); + } + void visit(const And *op) override { + visit_commutative_op(op); + } + void visit(const Or *op) override { + visit_commutative_op(op); + } + +public: + vector commutative_ops; +}; + +class Commute : public IRMutator { + template + Expr visit_commutative_op(const Op *op) { + if (to_commute.same_as(op)) { + return Op::make(op->b, op->a); + } else { + return IRMutator::visit(op); + } + } + + Expr visit(const Add *op) override { + return visit_commutative_op(op); + } + Expr visit(const Mul *op) override { + return visit_commutative_op(op); + } + Expr visit(const Min *op) override { + return visit_commutative_op(op); + } + Expr visit(const Max *op) override { + return visit_commutative_op(op); + } + Expr visit(const EQ *op) override { + return visit_commutative_op(op); + } + Expr visit(const NE *op) override { + return visit_commutative_op(op); + } + Expr visit(const And *op) override { + return visit_commutative_op(op); + } + Expr visit(const Or *op) override { + return visit_commutative_op(op); + } + + Expr to_commute; + +public: + using IRMutator::mutate; + + Commute(Expr c) + : to_commute(std::move(c)) { + } +}; + +vector generate_commuted_variants(const Expr &expr) { + FindCommutativeOps finder; + expr.accept(&finder); + + vector exprs; + exprs.push_back(expr); + + for (const Expr &e : finder.commutative_ops) { + Commute commuter(e); + vector new_exprs = exprs; + for (const Expr &l : exprs) { + new_exprs.push_back(commuter.mutate(l)); + } + exprs.swap(new_exprs); + } + return exprs; +} + +vector generate_reassociated_variants(const Expr &e); + +struct LinearTerm { + bool positive; + Expr e; +}; + +// This function is very very exponential +void all_possible_exprs_that_compute_sum(const vector &terms, vector *result) { + // The number of results is at least n factorial times the (n-1)th catalan + // number. Let's throw an error rather than trying to produce too + // much stuff. + if (terms.size() >= 8) { + std::cerr << "Too many terms passed to all_possible_exprs_that_compute_sum. " + << "Would OOM. Just generating one and not recursing on leaves.\n"; + Expr pos, neg; + for (const auto &t : terms) { + if (t.positive) { + if (pos.defined()) { + pos += t.e; + } else { + pos = t.e; + } + } else { + if (neg.defined()) { + neg += t.e; + } else { + neg = t.e; + } + } + } + if (!pos.defined()) { + pos = 0; + } + if (neg.defined()) { + pos -= neg; + } + result->push_back(pos); + return; + } + + if (terms.size() == 1) { + if (terms[0].positive) { + vector variants = generate_reassociated_variants(terms[0].e); + result->insert(result->end(), variants.begin(), variants.end()); + } + return; + } + + for (size_t i = 1; i < (size_t)((1 << terms.size()) - 1); i++) { + vector left, right; + for (size_t j = 0; j < terms.size(); j++) { + if (i & (1 << j)) { + left.push_back(terms[j]); + } else { + right.push_back(terms[j]); + } + } + vector left_exprs, right_exprs, right_exprs_negated; + all_possible_exprs_that_compute_sum(left, &left_exprs); + all_possible_exprs_that_compute_sum(right, &right_exprs); + for (auto &t : right) { + t.positive = !t.positive; + } + all_possible_exprs_that_compute_sum(right, &right_exprs_negated); + + for (auto &l : left_exprs) { + for (auto &r : right_exprs) { + result->push_back(l + r); + } + for (auto &r : right_exprs_negated) { + result->push_back(l - r); + } + } + } +} + +Expr make_binop(IRNodeType t, Expr l, Expr r) { + if (t == IRNodeType::Min) { + return min(l, r); + } else if (t == IRNodeType::Max) { + return max(l, r); + } else { + std::cerr << "Unsupported binop in make_binop: " << t << "\n"; + abort(); + } +} + +template +void all_possible_exprs_that_compute_associative_op_helper(const Expr &e, + vector *result) { + if (!e.as()) { + vector variants = generate_reassociated_variants(e); + result->insert(result->end(), variants.begin(), variants.end()); + return; + } + + vector terms = unpack_binary_op(e); + // The number of results is doubly exponential in the number of terms, so + // as in all_possible_exprs_that_compute_sum, refuse rather than OOM. + if (terms.size() >= 8) { + std::cerr << "Too many terms passed to " + << "all_possible_exprs_that_compute_associative_op. " + << "Would OOM. Just generating one and not recursing on leaves.\n"; + result->push_back(e); + return; + } + + for (size_t i = 1; i < (size_t)((1 << terms.size()) - 1); i++) { + vector left, right; + for (size_t j = 0; j < terms.size(); j++) { + if (i & (1 << j)) { + left.push_back(terms[j]); + } else { + right.push_back(terms[j]); + } + } + assert(left.size() < terms.size()); + assert(right.size() < terms.size()); + vector left_exprs, right_exprs; + all_possible_exprs_that_compute_associative_op_helper(pack_binary_op(left), &left_exprs); + all_possible_exprs_that_compute_associative_op_helper(pack_binary_op(right), &right_exprs); + for (auto &l : left_exprs) { + for (auto &r : right_exprs) { + // Skip non-canonical ones + if (!l.as() && + !r.as() && + r.node_type() > l.node_type()) { + continue; + } + result->push_back(Op::make(l, r)); + } + } + } +} + +template +void all_possible_exprs_that_compute_associative_op(const Op *op, + vector *result) { + all_possible_exprs_that_compute_associative_op_helper(Expr(op), result); +} + +template +void all_possible_exprs_that_compute_non_associative_op(const Op *op, + vector *result) { + for (const Expr &e1 : generate_reassociated_variants(op->a)) { + for (const Expr &e2 : generate_reassociated_variants(op->b)) { + result->emplace_back(Op::make(e1, e2)); + } + } +} + +vector generate_reassociated_variants(const Expr &e) { + if (e.as() || e.as()) { + vector terms, pending; + pending.emplace_back(LinearTerm{true, e}); + while (!pending.empty()) { + auto next = pending.back(); + pending.pop_back(); + if (const Add *add = next.e.as()) { + pending.emplace_back(LinearTerm{next.positive, add->a}); + pending.emplace_back(LinearTerm{next.positive, add->b}); + } else if (const Sub *sub = next.e.as()) { + pending.emplace_back(LinearTerm{next.positive, sub->a}); + pending.emplace_back(LinearTerm{!next.positive, sub->b}); + } else { + terms.push_back(next); + } + } + + // We now have a linear combination of terms and need to + // generate all possible trees that compute it. We'll generate + // all possible partitions, then generate all reassociated + // variants of the left and right, then combine them. + vector result; + all_possible_exprs_that_compute_sum(terms, &result); + return result; + } else if (const Min *op = e.as()) { + vector result; + all_possible_exprs_that_compute_associative_op(op, &result); + return result; + } else if (const Max *op = e.as()) { + vector result; + all_possible_exprs_that_compute_associative_op(op, &result); + return result; + } else if (const And *op = e.as()) { + vector result; + all_possible_exprs_that_compute_associative_op(op, &result); + return result; + } else if (const Or *op = e.as()) { + vector result; + all_possible_exprs_that_compute_associative_op(op, &result); + return result; + } else if (const Mul *op = e.as()) { + vector result; + all_possible_exprs_that_compute_associative_op(op, &result); + return result; + } else if (const LT *op = e.as()) { + vector result; + all_possible_exprs_that_compute_non_associative_op(op, &result); + return result; + } else if (const LE *op = e.as()) { + vector result; + all_possible_exprs_that_compute_non_associative_op(op, &result); + return result; + } else if (const EQ *op = e.as()) { + vector result; + all_possible_exprs_that_compute_non_associative_op(op, &result); + return result; + } else if (const NE *op = e.as()) { + vector result; + all_possible_exprs_that_compute_non_associative_op(op, &result); + return result; + } else if (const Div *op = e.as
()) { + vector result; + all_possible_exprs_that_compute_non_associative_op(op, &result); + return result; + } else if (const Mod *op = e.as()) { + vector result; + all_possible_exprs_that_compute_non_associative_op(op, &result); + return result; + } else if (const Select *op = e.as()) { + return Select::make(sel->condition, + reparse_as_bool(sel->true_value), + reparse_as_bool(sel->false_value)); + } else if (is_const_zero(e)) { + return const_false(); + } else if (is_const_one(e)) { + return const_true(); + } else { + std::cerr << "Expected bool Expr: " << e << "\n"; + exit(1); + } + } + + // The binary operators, and how tightly each binds. A token that is a + // prefix of another must come after it, so that "<=" is never read as "<". + struct BinOp { + const char *token; + int precedence; + Expr (*make)(Parser *, const Expr &, const Expr &); + }; + + static const vector &binops() { + static const vector ops = { + {"||", 1, [](Parser *p, const Expr &a, const Expr &b) { return p->reparse_as_bool(a) || p->reparse_as_bool(b); }}, + {"&&", 2, [](Parser *p, const Expr &a, const Expr &b) { return p->reparse_as_bool(a) && p->reparse_as_bool(b); }}, + {"<=", 3, [](Parser *, const Expr &a, const Expr &b) { return a <= b; }}, + {">=", 3, [](Parser *, const Expr &a, const Expr &b) { return a >= b; }}, + {"==", 3, [](Parser *, const Expr &a, const Expr &b) { return a == b; }}, + {"!=", 3, [](Parser *, const Expr &a, const Expr &b) { return a != b; }}, + {"<", 3, [](Parser *, const Expr &a, const Expr &b) { return a < b; }}, + {">", 3, [](Parser *, const Expr &a, const Expr &b) { return a > b; }}, + {"+", 4, [](Parser *, const Expr &a, const Expr &b) { return a + b; }}, + {"-", 4, [](Parser *, const Expr &a, const Expr &b) { return a - b; }}, + {"*", 5, [](Parser *, const Expr &a, const Expr &b) { return a * b; }}, + {"/", 5, [](Parser *, const Expr &a, const Expr &b) { return a / b; }}, + {"%", 5, [](Parser *, const Expr &a, const Expr &b) { return a % b; }}, + }; + return ops; + } + + // Anything that binds tighter than a binary operator: a literal, a + // variable, a call, a parenthesized expression, or a unary operator + // applied to one of those. + Expr parse_primary() { + struct TypePattern { + const char *cast_prefix = nullptr; + const char *constant_prefix = nullptr; + Type type; + string cast_prefix_storage, constant_prefix_storage; + TypePattern(Type t) { + ostringstream cast_prefix_stream, constant_prefix_stream; + cast_prefix_stream << t << '('; + cast_prefix_storage = cast_prefix_stream.str(); + cast_prefix = cast_prefix_storage.c_str(); + + constant_prefix_stream << '(' << t << ')'; + constant_prefix_storage = constant_prefix_stream.str(); + constant_prefix = constant_prefix_storage.c_str(); + type = t; + } + }; + static vector> typenames = + []() { + Type scalar_types[] = {UInt(1), + Int(8), + UInt(8), + Int(16), + UInt(16), + Int(32), + UInt(32), + Int(64), + UInt(64), + Float(64), + Float(32)}; + vector> vec; + for (int v : {1, 2, 4, 8, 16, 32, 64, 128}) { + for (Type t : scalar_types) { + vec.emplace_back(new TypePattern(t.with_lanes(v))); + } + } + return vec; + }(); + + consume_whitespace(); + + consume_whitespace(); + + // type-cast + for (const auto &t : typenames) { + if (consume(t->cast_prefix)) { + Expr a = cast(t->type, parse_expr()); + expect(")"); + return a; + } + } + + // Let binding. Always has parens + if (consume("(let ")) { + string name = consume_token(); + consume_whitespace(); + expect("="); + consume_whitespace(); + + Expr value = parse_expr(); + + consume_whitespace(); + expect("in"); + consume_whitespace(); + + var_types[name] = value.type(); + + Expr body = parse_expr(); + + Expr a = Let::make(name, value, body); + expect(")"); + return a; + } + if (consume("min(")) { + Expr a = parse_expr(); + expect(","); + Expr b = parse_expr(); + consume_whitespace(); + expect(")"); + return min(a, b); + } + if (consume("max(")) { + Expr a = parse_expr(); + expect(","); + Expr b = parse_expr(); + consume_whitespace(); + expect(")"); + return max(a, b); + } + if (consume("select(")) { + Expr a = parse_expr(); + a = reparse_as_bool(a); + expect(","); + Expr b = parse_expr(); + expect(","); + Expr c = parse_expr(); + consume_whitespace(); + expect(")"); + if (b.type().is_bool() && !c.type().is_bool()) { + c = reparse_as_bool(c); + } else if (!b.type().is_bool() && c.type().is_bool()) { + b = reparse_as_bool(b); + } + + return select(a, b, c); + } + Call::IntrinsicOp binary_intrinsics[] = {Call::bitwise_and, + Call::bitwise_or, + Call::shift_left, + Call::shift_right}; + for (const auto &intrin : binary_intrinsics) { + if (consume(Call::get_intrinsic_name(intrin))) { + expect("("); + Expr a = parse_expr(); + expect(","); + Expr b = parse_expr(); + consume_whitespace(); + expect(")"); + return Call::make(a.type(), intrin, {a, b}, Call::PureIntrinsic); + } + } + + if (consume("fold(")) { + Expr e = parse_expr(); + e = Call::make(e.type(), "fold", {e}, Call::PureIntrinsic); + expect(")"); + return e; + } + + if (consume("!")) { + Expr e = parse_primary(); + e = reparse_as_bool(e); + return !e; + } + + // Parse entire rewrite rules as exprs + if (consume("rewrite(")) { + Expr lhs = parse_expr(); + expect(","); + Expr rhs = parse_expr(); + if (lhs.type().is_bool()) { + rhs = reparse_as_bool(rhs); + } + if (rhs.type().is_bool()) { + lhs = reparse_as_bool(lhs); + } + Expr predicate = const_true(); + consume_whitespace(); + if (consume(",")) { + predicate = parse_expr(); + predicate = reparse_as_bool(predicate); + } + expect(")"); + return Call::make(Bool(), "rewrite", {lhs, rhs, predicate}, Call::Extern); + } + + if (consume("round_f32(")) { + Expr a = parse_expr(); + expect(")"); + return round(a); + } + if (consume("ceil_f32(")) { + Expr a = parse_expr(); + expect(")"); + return ceil(a); + } + if (consume("floor_f32(")) { + Expr a = parse_expr(); + expect(")"); + return floor(a); + } + if (consume("likely(")) { + Expr a = parse_expr(); + expect(")"); + return likely(a); + } + if (consume("likely_if_innermost(")) { + Expr a = parse_expr(); + expect(")"); + return likely_if_innermost(a); + } + + Type expected_type = Int(32); + for (const auto &t : typenames) { + // A type annotation for the token that follows + if (consume(t->constant_prefix)) { + expected_type = t->type; + } + } + + // An expression in parens + if (consume("(")) { + Expr e = parse_expr(); + expect(")"); + return e; + } + + // Negation of something that isn't a constant + if (peek() == '-' && !(cursor[1] >= '0' && cursor[1] <= '9')) { + expect("-"); + return -parse_primary(); + } + + // Constants + if ((peek() >= '0' && peek() <= '9') || peek() == '-') { + const char *tmp = cursor; + Expr e = make_const(Int(32), consume_int()); + if (peek() == '.') { + // Rewind and parse as float instead + cursor = tmp; + e = consume_float(); + } + return e; + } + if (consume("true")) { + return const_true(); + } + if (consume("false")) { + return const_false(); + } + + // Variables, loads, and calls + if ((peek() >= 'a' && peek() <= 'z') || + (peek() >= 'A' && peek() <= 'Z') || + peek() == '$' || + peek() == '_' || + peek() == '.') { + string name = consume_token(); + if (consume("[")) { + Expr index = parse_expr(); + // eat an alignment specifier + consume_whitespace(); + if (consume("aligned(")) { + consume_int(); + expect(", "); + consume_int(); + expect(")"); + } + expect("]"); + if (expected_type == Type{}) { + expected_type = Int(32); + } + return Load::make(expected_type, name, index); + } else if (consume("(")) { + vector args; + while (1) { + consume_whitespace(); + if (consume(")")) { + break; + } + args.push_back(parse_expr()); + consume_whitespace(); + consume(","); + } + return Call::make(expected_type, name, args, Call::PureExtern); + } else { + auto it = var_types.find(name); + if (it != var_types.end()) { + expected_type = it->second; + } + if (expected_type == Type{}) { + expected_type = Int(32); + } + return Variable::make(expected_type, name); + } + } + + std::cerr << "Failed to parse starting at: " << cursor << "\n"; + exit(1); + } + +public: + // Precedence climbing: parse a primary, then keep absorbing binary + // operators that bind at least as tightly as min_precedence. All of them + // are left-associative, as in C++. + Expr parse_expr(int min_precedence = 1) { + Expr a = parse_primary(); + while (true) { + consume_whitespace(); + const BinOp *op = nullptr; + for (const BinOp &candidate : binops()) { + if (candidate.precedence >= min_precedence && consume(candidate.token)) { + op = &candidate; + break; + } + } + if (!op) { + return a; + } + a = op->make(this, a, parse_expr(op->precedence + 1)); + } + } + + Parser(const char *c, const char *e) + : cursor(c), end(e) { + } +}; + +Expr parse_halide_expr(const char *cursor, const char *end, Type expected_type) { + Parser parser(cursor, end); + Expr result = parser.parse_expr(); + if (expected_type.is_bool()) { + result = parser.reparse_as_bool(result); + } + return result; +} + +vector parse_halide_exprs_from_file(const string &filename) { + vector exprs; + std::ifstream input; + input.open(filename); + if (input.fail()) { + debug(0) << "parse_halide_exprs_from_file: Unable to open " << filename; + assert(false); + } + for (string line; std::getline(input, line);) { + if (line.empty()) { + continue; + } + + // Lines can be commented out for debugging, in python style (#) or + // C++ style (// or */). + if (line[0] == '#' || line[0] == '/' || line[0] == '*') { + continue; + } + + // There are some extraneous newlines in some of the files. Balance parentheses... + size_t open, close; + while (1) { + open = std::count(line.begin(), line.end(), '('); + close = std::count(line.begin(), line.end(), ')'); + if (open <= close) { + break; + } + string next; + debug(0) << "Unbalanced parens in :\n\n" + << line << "\n\n"; + assert(std::getline(input, next)); + line += next; + } + const char *start = &line[0]; + const char *end = &line[line.size()]; + debug(1) << "Parsing: " << line << "\n"; + exprs.push_back(parse_halide_expr(start, end, Type{})); + } + + return exprs; +} diff --git a/apps/simplifier_rule_verifier/parser.h b/apps/simplifier_rule_verifier/parser.h new file mode 100644 index 000000000000..b6e47aa8f165 --- /dev/null +++ b/apps/simplifier_rule_verifier/parser.h @@ -0,0 +1,37 @@ +#ifndef PARSER_COMMON_H +#define PARSER_COMMON_H + +#include + +#include "Halide.h" + +// Helper routines for writing a parser and routines for parsing +// Halide Exprs. + +// Move the input cursor past any whitespace, but not beyond the end +// pointer. +void consume_whitespace(const char **cursor, const char *end); + +// If the input cursor starts with the expected string, update it to +// point to the end of the string and return true. Otherwise, return +// false and don't modify the input cursor. +bool consume(const char **cursor, const char *end, const char *expected); + +// Calls consume and asserts that it succeeded. +void expect(const char **cursor, const char *end, const char *pattern); + +// Consume and return a legal Halide identifier. +std::string consume_token(const char **cursor, const char *end); + +// Consume and return a constant integer. +int64_t consume_int(const char **cursor, const char *end); + +// Consume and return a constant float as a constant Halide Expr of +// the appropriate type. +Halide::Expr consume_float(const char **cursor, const char *end); + +// Parse a full Halide Expr, as produced by a Halide IRPrinter elsewhere. +Halide::Expr parse_halide_expr(const char *cursor, const char *end, Halide::Type expected_type); + +std::vector parse_halide_exprs_from_file(const std::string &filename); +#endif diff --git a/apps/simplifier_rule_verifier/reduction_order.cpp b/apps/simplifier_rule_verifier/reduction_order.cpp new file mode 100644 index 000000000000..94dbe1ceb4fc --- /dev/null +++ b/apps/simplifier_rule_verifier/reduction_order.cpp @@ -0,0 +1,494 @@ +#include "Halide.h" +#include "debug.h" +#include "expr_util.h" + +using namespace Halide; +using namespace Halide::Internal; + +using std::map; +using std::ostringstream; +using std::set; +using std::string; + +IRNodeType node_ordering[18] = {IRNodeType::Ramp, IRNodeType::Broadcast, IRNodeType::Select, IRNodeType::Div, IRNodeType::Mul, IRNodeType::Mod, IRNodeType::Sub, IRNodeType::Add, IRNodeType::Min, IRNodeType::Not, IRNodeType::Or, IRNodeType::And, IRNodeType::GE, IRNodeType::GT, IRNodeType::LE, IRNodeType::LT, IRNodeType::NE, IRNodeType::EQ}; + +map nto = { + {IRNodeType::Ramp, 23}, + {IRNodeType::Broadcast, 22}, + {IRNodeType::Select, 21}, + {IRNodeType::Div, 20}, + {IRNodeType::Mul, 19}, + {IRNodeType::Mod, 18}, + {IRNodeType::Sub, 17}, + {IRNodeType::Add, 16}, + {IRNodeType::Max, 14}, // max and min have same weight + {IRNodeType::Min, 14}, + {IRNodeType::Not, 13}, + {IRNodeType::Or, 12}, + {IRNodeType::And, 11}, + {IRNodeType::GE, 10}, + {IRNodeType::GT, 9}, + {IRNodeType::LE, 8}, + {IRNodeType::LT, 7}, + {IRNodeType::NE, 6}, + {IRNodeType::EQ, 5}, + {IRNodeType::Cast, 4}, + {IRNodeType::FloatImm, 2}, + {IRNodeType::UIntImm, 1}, + {IRNodeType::IntImm, 0}}; + +class DivisorSet : public IRVisitor { + Scope<> lets; + + void visit(const Div *op) override { + ostringstream term; + term << op->b; + divisors.insert(term.str()); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const Mod *op) override { + ostringstream term; + term << op->b; + divisors.insert(term.str()); + op->a.accept(this); + op->b.accept(this); + } + +public: + set divisors; +}; + +set find_divisors(const Expr &e) { + DivisorSet d; + e.accept(&d); + return d.divisors; +} + +class VectorOpCount : public IRVisitor { + void visit(const Ramp *op) override { + counter += 1; + } + void visit(const Broadcast *op) override { + counter += 1; + } + +public: + int counter = 0; +}; + +int get_vector_count(const Expr &e) { + VectorOpCount rcounter; + e.accept(&rcounter); + return rcounter.counter; +} + +bool check_divisors(const Expr &LHS, const Expr &RHS) { + // check that all divisors on RHS appear as divisors on LHS + set lhs_divisors = find_divisors(LHS); + set rhs_divisors = find_divisors(RHS); + for (auto const &rhs_term : rhs_divisors) { + if (lhs_divisors.count(rhs_term) == 0) { + return false; + } + } + return true; +} + +class NonlinearOpsCount : public IRVisitor { + void visit(const Div *op) override { + counter += 1; + op->a.accept(this); + op->b.accept(this); + } + void visit(const Mod *op) override { + counter += 1; + op->a.accept(this); + op->b.accept(this); + } + void visit(const Mul *op) override { + counter += 1; + op->a.accept(this); + op->b.accept(this); + } + void visit(const Call *op) override { + if (op->name == "fold") { + return; + } else { + IRVisitor::visit(op); + } + } + +public: + int counter = 0; +}; + +int get_nonlinear_op_count(const Expr &e) { + NonlinearOpsCount nl; + e.accept(&nl); + return nl.counter; +} + +bool is_expr_constant(const Expr &e) { + const Variable *var_a = e.as(); + const Call *call_a = e.as(); + return is_const(e) || (var_a && var_a->name[0] == 'c') || (call_a && call_a->name == "fold"); +} + +bool is_expr_addsub(const Expr &e) { + return e.as() || e.as(); +} + +Expr get_right_child(const Expr &e) { + if (const Add *op = e.as()) { + return op->b; + } else if (const Sub *op = e.as()) { + return op->b; + } else if (const Mod *op = e.as()) { + return op->b; + } else if (const Div *op = e.as
()) { + return op->b; + } else if (const Mul *op = e.as()) { + return op->b; + } else if (const Min *op = e.as()) { + return op->b; + } else if (const Max *op = e.as()) { + return op->b; + } else if (const EQ *op = e.as()) { + return op->b; + } else if (const NE *op = e.as()) { + return op->b; + } else if (const LT *op = e.as()) { + return op->b; + } else if (const LE *op = e.as()) { + return op->b; + } else if (const And *op = e.as()) { + return op->b; + } else if (const Or *op = e.as()) { + return op->b; + } else { + debug(0) << "Warning: don't know about the right child of: " << e << "\n"; + return Expr(); + } +} + +bool is_right_child_constant(const Expr &e) { + Expr r = get_right_child(e); + return r.defined() && is_expr_constant(r); +} + +class NodeHistogram : public IRVisitor { + Scope<> lets; + + void visit(const Call *op) override { + if (op->name == "fold") { + return; + } + IRVisitor::visit(op); + } + + void visit(const Select *op) override { + increment_histo(IRNodeType::Select); + op->condition.accept(this); + op->true_value.accept(this); + op->false_value.accept(this); + } + + void visit(const Ramp *op) override { + increment_histo(IRNodeType::Ramp); + op->base.accept(this); + op->stride.accept(this); + } + + void visit(const Broadcast *op) override { + increment_histo(IRNodeType::Broadcast); + op->value.accept(this); + } + + void visit(const Add *op) override { + increment_histo(IRNodeType::Add); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const Sub *op) override { + increment_histo(IRNodeType::Add); // Put Sub counts in the Add bucket + op->a.accept(this); + op->b.accept(this); + } + + void visit(const Mul *op) override { + increment_histo(IRNodeType::Mul); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const Div *op) override { + increment_histo(IRNodeType::Div); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const Mod *op) override { + increment_histo(IRNodeType::Mod); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const LT *op) override { + increment_histo(IRNodeType::LT); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const LE *op) override { + increment_histo(IRNodeType::LE); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const GT *op) override { + increment_histo(IRNodeType::GT); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const GE *op) override { + increment_histo(IRNodeType::GE); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const EQ *op) override { + increment_histo(IRNodeType::EQ); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const Min *op) override { + increment_histo(IRNodeType::Min); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const Max *op) override { + increment_histo(IRNodeType::Min); // put max counts into min bucket so we count them the same + op->a.accept(this); + op->b.accept(this); + } + + void visit(const Not *op) override { + increment_histo(IRNodeType::Not); + op->a.accept(this); + } + + void visit(const And *op) override { + increment_histo(IRNodeType::And); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const Or *op) override { + increment_histo(IRNodeType::Or); + op->a.accept(this); + op->b.accept(this); + } + + void visit(const Let *op) override { + op->value.accept(this); + { + ScopedBinding<> bind(lets, op->name); + op->body.accept(this); + } + } + +public: + map histogram; + void increment_histo(IRNodeType node_type) { + if (histogram.count(node_type) == 0) { + histogram[node_type] = 1; + } else { + histogram[node_type] = histogram[node_type] + 1; + } + } +}; + +map build_histogram(const Expr &e) { + NodeHistogram histo; + e.accept(&histo); + return histo.histogram; +} + +int get_total_leaf_count(const Expr &e) { + class CountLeaves : public IRVisitor { + using IRVisitor::visit; + void visit(const IntImm *op) override { + count++; + } + void visit(const UIntImm *op) override { + count++; + } + void visit(const FloatImm *op) override { + count++; + } + void visit(const Variable *op) override { + count++; + } + void visit(const Call *op) override { + if (op->name == "fold") { + count++; + } else { + IRVisitor::visit(op); + } + } + + public: + int count = 0; + } counter; + e.accept(&counter); + return counter.count; +} + +int get_total_op_count(const Expr &e) { + map histo = build_histogram(e); + int counter = 0; + for (auto const &node : histo) { + counter += node.second; + } + return counter; +} + +// return 1 if correctly ordered, -1 if incorrectly ordered, 0 if tied +int compare_histograms(const Expr &LHS, const Expr &RHS) { + map lhs_histo = build_histogram(LHS); + map rhs_histo = build_histogram(RHS); + int lhs_node_count, rhs_node_count; + for (auto const &node : node_ordering) { + lhs_node_count = 0; + rhs_node_count = 0; + if (lhs_histo.count(node) == 1) { + lhs_node_count = lhs_histo[node]; + } + if (rhs_histo.count(node) == 1) { + rhs_node_count = rhs_histo[node]; + } + + debug(1) << node << " LHS count " << lhs_node_count << " RHS count " << rhs_node_count << "\n"; + // RHS side has more of some op than LHS + if (lhs_node_count < rhs_node_count) { + return -1; + // LHS side has strictly more of some op than RHS + } else if (lhs_node_count > rhs_node_count) { + return 1; + } + } + return 0; +} + +bool valid_reduction_order(const Expr &LHS, const Expr &RHS) { + + // first, check that RHS has fewer ramp ops + // wildcard variables can only match scalars, so we don't need to check variable occurrence counts + if (get_vector_count(LHS) > get_vector_count(RHS)) { + return true; + } else if (get_vector_count(LHS) < get_vector_count(RHS)) { + debug(1) << __LINE__ << "\n"; + return false; + } + + // check that occurrences of variables on RHS is equal or lesser to those in LHS + // if any variable has more occurrences in RHS than it does on LHS, then the next several orders are invalid + auto lhs_vars = find_vars(LHS); + auto rhs_vars = find_vars(RHS); + for (auto const &varcount : rhs_vars) { + // constant wildcards don't count bc they can't match terms so can't cause reduction order failures + if (varcount.first.front() != 'c' && + (lhs_vars.count(varcount.first) == 0 || + varcount.second.second > lhs_vars[varcount.first].second)) { + debug(1) << __LINE__ << "\n"; + return false; + } + } + + // accept rule if LHS has strictly more occurrences of at least 1 variable + for (auto const &lhsv : lhs_vars) { + if ((lhsv.first.front() != 'c') && + ((rhs_vars.count(lhsv.first) == 0) || (lhsv.second.second > rhs_vars[lhsv.first].second))) { + return true; + } + } + + // LHS should have more div, mod, mul operations than RHS (if var occurrences are >=) + if (get_nonlinear_op_count(LHS) > get_nonlinear_op_count(RHS)) { + return true; + } else if (get_nonlinear_op_count(LHS) < get_nonlinear_op_count(RHS)) { + debug(1) << __LINE__ << "\n"; + return false; + } + + // LHS should have more total ops than RHS (if var occurrences are >=) + if (get_total_leaf_count(LHS) > get_total_leaf_count(RHS)) { + return true; + } else if (get_total_leaf_count(LHS) < get_total_leaf_count(RHS)) { + debug(1) << __LINE__ << "\n"; + return false; + } + + // LHS should have more total ops than RHS (if var occurrences are >=) + if (get_total_op_count(LHS) > get_total_op_count(RHS)) { + return true; + } else if (get_total_op_count(LHS) < get_total_op_count(RHS)) { + debug(1) << __LINE__ << "\n"; + return false; + } + + // check that histogram of operations obeys ordering (if var occurrences are >=) + int rule_histogram_ordering = compare_histograms(LHS, RHS); + if (rule_histogram_ordering == 1) { + return true; + } else if (rule_histogram_ordering == -1) { + debug(1) << __LINE__ << "\n"; + return false; + } + + // ordered if LHS is not add or sub and RHS is add or sub + // invalid order if LHS is add or sub and RSH is NOT add or sub + bool is_LHS_add_sub = is_expr_addsub(LHS); + bool is_RHS_add_sub = is_expr_addsub(RHS); + + if (!(is_LHS_add_sub) && is_RHS_add_sub) { + return true; + } + if (is_LHS_add_sub && !(is_RHS_add_sub)) { + debug(1) << __LINE__ << "\n"; + return false; + } + + // ordered if the right child of the LHS is not a constant and the right child of the RHS is a constant + // invalid order if the right child of the LHS is a constant and the right child of the RHS is not a constant + // this checks if right child is IntImm, UIntImm, or Variable whose first char is c + if (!(is_right_child_constant(LHS)) && is_right_child_constant(RHS)) { + return true; + } + if (is_right_child_constant(LHS) && !(is_right_child_constant(RHS))) { + debug(1) << __LINE__ << "\n"; + return false; + } + + // check that root symbol obeys ordering + IRNodeType lhs_root_type = LHS.node_type(); + IRNodeType rhs_root_type = RHS.node_type(); + + if (nto[lhs_root_type] < nto[rhs_root_type]) { + return true; + } + if (nto[lhs_root_type] > nto[rhs_root_type]) { + debug(1) << __LINE__ << "\n"; + return false; + } + + // It's a tie. No good. + debug(1) << __LINE__ << "\n"; + return false; +} diff --git a/apps/simplifier_rule_verifier/reduction_order.h b/apps/simplifier_rule_verifier/reduction_order.h new file mode 100644 index 000000000000..2b610e93cd2b --- /dev/null +++ b/apps/simplifier_rule_verifier/reduction_order.h @@ -0,0 +1,9 @@ +#ifndef REDUCTION_ORDER_H +#define REDUCTION_ORDER_H + +#include "Halide.h" + +bool check_divisors(const Halide::Expr &LHS, const Halide::Expr &RHS); +bool valid_reduction_order(const Halide::Expr &LHS, const Halide::Expr &RHS); + +#endif diff --git a/apps/simplifier_rule_verifier/super_simplify.cpp b/apps/simplifier_rule_verifier/super_simplify.cpp new file mode 100644 index 000000000000..cb5c7d1d9c34 --- /dev/null +++ b/apps/simplifier_rule_verifier/super_simplify.cpp @@ -0,0 +1,404 @@ +#include "super_simplify.h" +#include "debug.h" +#include "expr_util.h" +#include "z3.h" +#include + +using namespace Halide; +using namespace Halide::Internal; +using std::map; +using std::pair; +using std::set; +using std::string; +using std::vector; + +// Make an expression which can act as any other small integer +// expression in the given leaf terms, depending on the values of the +// integer opcodes. Not all possible programs are valid (e.g. due to +// type errors), so also returns an Expr on the inputs opcodes that +// encodes whether or not the program is well-formed. +pair interpreter_expr(vector terms, vector use_counts, vector opcodes, Type desired_type, Type int_type, int max_leaves) { + // Each opcode is an enum identifying the op, followed by the indices of the three args. + assert(opcodes.size() % 4 == 0); + assert(terms.size() == use_counts.size()); + + Expr program_is_valid = const_true(); + + // Type type of each term. Encode int as 0, bool as 1. + vector terms_int, terms_bool; + for (auto &t : terms) { + if (t.type() == int_type) { + terms_int.push_back(t); + terms_bool.push_back(const_false()); + } else if (t.type() == Bool()) { + terms_int.push_back(0); + terms_bool.push_back(t); + } else { + std::cerr << t << " " << int_type << "\n"; + assert(false && "Unhandled wildcard type"); + } + } + + // TODO: bound constants to be within the ranges of the constants in the input + + Expr leaves_used = cast(int_type, 0); + + int initial_terms = (int)terms.size(); + + for (size_t i = 0; i < opcodes.size(); i += 4) { + Expr op = opcodes[i]; + Expr arg1_idx = opcodes[i + 1]; + Expr arg2_idx = opcodes[i + 2]; + Expr arg3_idx = opcodes[i + 3]; + + // Get the args using a select tree. args are either the index of an existing value, or some constant. + + int s = (int)std::max(terms_int.size(), terms_bool.size()); + + // int opcodes outside the valid range are constants. + Expr arg1_int = select(arg1_idx >= s, arg1_idx - s, arg1_idx); + Expr arg2_int = select(arg2_idx >= s, arg2_idx - s, arg2_idx); + Expr arg3_int = select(arg3_idx >= s, arg3_idx - s, arg3_idx); + + for (size_t j = 0; j < terms_int.size(); j++) { + arg1_int = select(arg1_idx == (int)j, terms_int[j], arg1_int); + arg2_int = select(arg2_idx == (int)j, terms_int[j], arg2_int); + arg3_int = select(arg3_idx == (int)j, terms_int[j], arg3_int); + } + + // Bool opcodes beyond the end of the valid range are true. Negative ones are false + Expr arg1_bool = (arg1_idx >= s); + Expr arg2_bool = (arg2_idx >= s); + Expr arg3_bool = (arg3_idx >= s); + + for (size_t j = 0; j < terms_bool.size(); j++) { + arg1_bool = select(arg1_idx == (int)j, terms_bool[j], arg1_bool); + arg2_bool = select(arg2_idx == (int)j, terms_bool[j], arg2_bool); + arg3_bool = select(arg3_idx == (int)j, terms_bool[j], arg3_bool); + } + + // Perform the op. + Expr result_int = cast(int_type, 0); + Expr result_bool = const_false(); + + Expr arg1_used = const_true(); + Expr arg2_used = op != 0 && op != 10 && op != 11 && op != 15 && op != 16; + Expr arg3_used = op == 12; + + Expr arg1_leaf = arg1_idx < initial_terms || arg1_idx >= s; + Expr arg2_leaf = arg2_idx < initial_terms || arg2_idx >= s; + Expr arg3_leaf = arg3_idx < initial_terms || arg3_idx >= s; + + for (int j = 0; j < (int)use_counts.size(); j++) { + // We've potentially soaked up one allowed use of each original term + use_counts[j] -= select(arg1_idx == j && arg1_used, cast(int_type, 1), cast(int_type, 0)); + use_counts[j] -= select(arg2_idx == j && arg2_used, cast(int_type, 1), cast(int_type, 0)); + use_counts[j] -= select(arg3_idx == j && arg3_used, cast(int_type, 1), cast(int_type, 0)); + } + + leaves_used += select(arg1_leaf && arg1_used, cast(int_type, 1), cast(int_type, 0)); + leaves_used += select(arg2_leaf && arg2_used, cast(int_type, 1), cast(int_type, 0)); + leaves_used += select(arg3_leaf && arg3_used, cast(int_type, 1), cast(int_type, 0)); + + result_int = select(op == 0, arg1_int, result_int); + result_bool = select(op == 0, arg1_bool, result_bool); + result_int = select(op == 1, arg1_int + arg2_int, result_int); + result_int = select(op == 2, arg1_int - arg2_int, result_int); + result_int = select(op == 3, arg1_int * arg2_int, result_int); + result_int = select(op == 4, min(arg1_int, arg2_int), result_int); + result_int = select(op == 5, max(arg1_int, arg2_int), result_int); + result_bool = select(op == 6, arg1_int < arg2_int, result_bool); + result_bool = select(op == 7, arg1_int <= arg2_int, result_bool); + result_bool = select(op == 8, arg1_int == arg2_int, result_bool); + result_bool = select(op == 9, arg1_int != arg2_int, result_bool); + + // TODO: switch 2 to any constant divisor already found in the input + result_int = select(op == 10, arg1_int / 2, result_int); + result_int = select(op == 11, arg1_int % 2, result_int); + + // Meaningful if arg1 is a bool + result_int = select(op == 12, select(arg1_bool, arg2_int, arg3_int), result_int); + result_bool = select(op == 13, arg1_bool && arg2_bool, result_bool); + result_bool = select(op == 14, arg1_bool || arg2_bool, result_bool); + result_bool = select(op == 15, !arg1_bool, result_bool); + result_bool = select(op == 16, arg1_bool, result_bool); + + // Type-check it + program_is_valid = program_is_valid && (op <= 16 && op >= 0); + + terms_int.push_back(result_int); + terms_bool.push_back(result_bool); + } + + for (const auto &u : use_counts) { + program_is_valid = program_is_valid && (u >= 0); + } + // Require that: + // We don't duplicate any wildcards and we strictly reduce the number of leaf nodes. + // More precise filtering will be done later. + program_is_valid = program_is_valid && (leaves_used < max_leaves); + + Expr result = (desired_type.is_bool()) ? terms_bool.back() : terms_int.back(); + + return {result, program_is_valid}; +} + +class CountLeaves : public IRVisitor { + using IRVisitor::visit; + + void visit(const Variable *op) override { + result++; + } + + void visit(const IntImm *op) override { + result++; + } + + void visit(const UIntImm *op) override { + result++; + } + + void visit(const FloatImm *op) override { + result++; + } + +public: + int result = 0; +}; + +// Use CEGIS to construct an equivalent expression to the input of the given size. +Expr super_simplify(Expr e, int size) { + // debug(0) << "\n-------------------------------------------\n"; + std::cerr << "super_simplify(" << e << ")" << "\n"; + + string z3_comment; + { + std::ostringstream sstr; + sstr << e << " at size " << size; + z3_comment = sstr.str(); + } + + // We may assume there's no undefined behavior in the existing + // left-hand-side. + class CheckForUB : public IRVisitor { + using IRVisitor::visit; + void visit(const Mod *op) override { + safe = safe && (op->b != 0); + } + void visit(const Div *op) override { + safe = safe && (op->b != 0); + } + void visit(const Let *op) override { + assert(false && "CheckForUB not written to handle Lets"); + } + + public: + Expr safe = const_true(); + } ub_checker; + e.accept(&ub_checker); + + CountLeaves leaf_counter; + e.accept(&leaf_counter); + + auto vars = find_vars(e); + + // The interpreter below only represents Int(32) and Bool leaves, so + // there's nothing to search for if the expression has any others. + for (const auto &v : vars) { + Type t = v.second.first.type(); + if (t != Int(32) && !t.is_bool()) { + debug(1) << "Can't synthesize an equivalent to " << e + << ": wildcard " << v.first << " has type " << t << "\n"; + return Expr(); + } + } + + vector leaves, leaves8, use_counts, use_counts8; + for (const auto &v : vars) { + leaves.push_back(v.second.first); + leaves8.push_back(Variable::make(Int(8), v.first + "_8")); + use_counts.push_back(v.second.second); + use_counts8.push_back(cast(v.second.second)); + } + + vector> counterexamples; + + map current_program; + + vector symbolic_opcodes, symbolic_opcodes8; + for (int i = 0; i < size * 4; i++) { + string name = "op" + std::to_string(i); + symbolic_opcodes.push_back(Variable::make(Int(32), name)); + symbolic_opcodes8.push_back(Variable::make(Int(8), name)); + + // The initial program is some garbage + current_program[name] = 0; + } + + map all_vars_zero; + for (const auto &v : vars) { + all_vars_zero[v.first] = make_zero(v.second.first.type()); + } + + Expr program, program_works; + { + auto p = interpreter_expr(leaves, use_counts, symbolic_opcodes, e.type(), Int(32), leaf_counter.result); + program = p.first; + program_works = (e == program) && p.second; + program = simplify(common_subexpression_elimination(program)); + program_works = simplify(common_subexpression_elimination(program_works)); + } + + // Make an 8-bit version of the interpreter too so that we can use SAT solvers. + Expr program8, program8_works; + { + auto p = interpreter_expr(leaves8, use_counts8, symbolic_opcodes8, e.type(), Int(8), leaf_counter.result); + program8 = p.first; + if (e.type().is_bool()) { + program8_works = (e == program8) && p.second; + } else { + program8_works = (cast(e) == program8) && p.second; + } + program8 = simplify(common_subexpression_elimination(program8)); + program8_works = simplify(common_subexpression_elimination(program8_works)); + } + + std::mt19937 rng(0); + std::uniform_int_distribution random_int(-3, 3); + + while (1) { + if (counterexamples.size() > 100) { + debug(0) << "TOO MANY COUNTEREXAMPLES, bailing for size=" << size << "\ne=" << e << "\n"; + return Expr(); + } + + // First synthesize a counterexample to the current program. + Expr current_program_works = substitute(current_program, program_works); + map counterexample = all_vars_zero; + + debug(2) << "Candidate RHS:\n" + << simplify(simplify(substitute_in_all_lets(substitute(current_program, program)))) << "\n"; + + // Start with just random fuzzing. If that fails, we'll ask Z3 for a counterexample. + int counterexamples_found_with_fuzzing = 0; + for (int i = 0; i < 5; i++) { + map rand_binding = all_vars_zero; + for (auto &it : rand_binding) { + if (it.second.type() == Bool()) { + it.second = (random_int(rng) & 1) ? const_true() : const_false(); + } else { + it.second = random_int(rng); + } + } + auto interpreted = simplify(substitute(rand_binding, ub_checker.safe && !current_program_works)); + if (is_const_one(interpreted)) { + counterexamples.push_back(rand_binding); + // We probably only want to add a couple + // counterexamples at a time + counterexamples_found_with_fuzzing++; + if (counterexamples_found_with_fuzzing >= 2) { + break; + } + } + } + + if (counterexamples_found_with_fuzzing == 0) { + auto result = satisfy(ub_checker.safe && !current_program_works, &counterexample, + "finding counterexamples for " + z3_comment); + if (result == Z3Result::Unsat) { + // Woo! + Expr e = simplify(substitute_in_all_lets(common_subexpression_elimination(substitute(current_program, program)))); + // TODO: Figure out why I need to simplify twice + // here. There are still exprs for which the + // simplifier requires repeated applications, and + // it's not supposed to. + e = simplify(e); + + return e; + } else if (result == Z3Result::Sat) { + counterexamples.push_back(counterexample); + } else { + return Expr(); + } + } + + // Now synthesize a program that fits all the counterexamples + Expr works_on_counterexamples = const_true(); + for (auto &c : counterexamples) { + works_on_counterexamples = works_on_counterexamples && substitute(c, program_works); + } + + // First try for an 8-bit program + bool have_8_bit_program = false; + if (false) { // Just seems to slow things down, sadly + Expr works_on_counterexamples8 = const_true(); + for (const auto &c : counterexamples) { + map c8; + for (const auto &p : c) { + c8[p.first + "_8"] = simplify(cast(p.second)); + } + works_on_counterexamples8 = (works_on_counterexamples8 && + substitute(c8, substitute(c, program8_works))); + } + have_8_bit_program = satisfy(works_on_counterexamples8, ¤t_program, + "finding 8-bit program for " + z3_comment) == Z3Result::Sat; + + if (have_8_bit_program) { + // Map program opcodes back to the integers and check it + for (auto &p : current_program) { + p.second = cast(p.second); + } + // debug(0) << "Candidate 8-bit program: " << simplify(substitute(current_program, program)) << "\n"; + Expr check = substitute(current_program, works_on_counterexamples); + if (!can_prove(check)) { + // debug(0) << "8-bit program doesn't work on integers in full space\n"; + have_8_bit_program = false; + } else { + // debug(0) << "8-bit program also works in the integers for current counterexamples (" << counterexamples.size() << ")\n"; + } + } + } + + if (!have_8_bit_program) { + // debug(0) << "Failed to solve for 8-bit program. Trying to find a program in the integers\n"; + if (satisfy(works_on_counterexamples, ¤t_program, + "finding program for " + z3_comment) != Z3Result::Sat) { + // Failed to synthesize a program + // debug(0) << "Failed to find a program in the integers\n"; + return Expr(); + } + // debug(0) << "Found a program in the integers: " << simplify(substitute(current_program, program)) << "\n"; + } else { + // debug(0) << "Found a working 8-bit program.\n"; + } + // We have a new program + + // If we start to have many many counterexamples, we should + // double-check things are working as intended. + if (counterexamples.size() > 30) { + Expr sanity_check = simplify(substitute(current_program, works_on_counterexamples)); + // Might fail to be the constant true due to overflow, so just make sure it's not the constant false + if (is_const_zero(sanity_check)) { + Expr p = simplify(common_subexpression_elimination(substitute(current_program, program))); + std::cout << "Synthesized program doesn't actually work on counterexamples!\n" + << "Original expr: " << e << "\n" + << "Program: " << p << "\n" + << "Check: " << sanity_check << "\n"; + std::cout << "Opcodes: \n"; + for (const auto &p : current_program) { + std::cout << p.first << " = " << p.second << "\n"; + } + std::cout << "Counterexamples: \n"; + for (const auto &c : counterexamples) { + const char *prefix = ""; + for (const auto &it : c) { + std::cout << prefix << it.first << " = " << it.second; + prefix = ", "; + } + std::cout << "\n"; + } + return Expr(); + } + } + } +} diff --git a/apps/simplifier_rule_verifier/super_simplify.h b/apps/simplifier_rule_verifier/super_simplify.h new file mode 100644 index 000000000000..5ebf906f50e2 --- /dev/null +++ b/apps/simplifier_rule_verifier/super_simplify.h @@ -0,0 +1,12 @@ +#ifndef SUPER_SIMPLIFY_H +#define SUPER_SIMPLIFY_H + +#include "Halide.h" + +std::pair interpreter_expr(std::vector terms, std::vector use_counts, + std::vector opcodes, Halide::Type desired_type, Halide::Type int_type, int max_leaves); + +// Use CEGIS to construct an equivalent expression to the input of the given size. +Halide::Expr super_simplify(Halide::Expr e, int size); + +#endif diff --git a/apps/simplifier_rule_verifier/super_simplify_tool.cpp b/apps/simplifier_rule_verifier/super_simplify_tool.cpp new file mode 100644 index 000000000000..a238a45c7499 --- /dev/null +++ b/apps/simplifier_rule_verifier/super_simplify_tool.cpp @@ -0,0 +1,22 @@ +#include "Halide.h" +#include "parser.h" +#include "super_simplify.h" + +using namespace Halide; + +int main(int argc, char **argv) { + if (argc < 3) { + std::cout << "Usage: ./super_simplify halide_exprs.txt max_size\n"; + return 0; + } + + std::vector exprs = parse_halide_exprs_from_file(argv[1]); + const int max_size = std::atoi(argv[2]); + + for (const auto &e : exprs) { + Expr simpler = super_simplify(e, max_size); + std::cout << e << " -> " << simpler << "\n"; + } + + return 0; +} diff --git a/apps/simplifier_rule_verifier/test/bad_rules.txt b/apps/simplifier_rule_verifier/test/bad_rules.txt new file mode 100644 index 000000000000..3016ebb1c12c --- /dev/null +++ b/apps/simplifier_rule_verifier/test/bad_rules.txt @@ -0,0 +1,9 @@ +# Rules that are false. z3 should find a counterexample for each. +rewrite((x/2)*2, x) +rewrite(min(x, y) + max(x, y), x + y + 1) + +# Rules that are true, but that don't obey the reduction order, so +# they would make the simplifier loop forever. +rewrite(x + y, y + x) +rewrite(min(x, y), min(y, x)) +rewrite(min(x, y) - max(x, y), min(x - y, y - x)) diff --git a/apps/simplifier_rule_verifier/test/exprs.txt b/apps/simplifier_rule_verifier/test/exprs.txt new file mode 100644 index 000000000000..b3b7f05d48d6 --- /dev/null +++ b/apps/simplifier_rule_verifier/test/exprs.txt @@ -0,0 +1,2 @@ +min(x, y) + max(x, y) +select(x < y, x, y) diff --git a/apps/simplifier_rule_verifier/test/float_exprs.txt b/apps/simplifier_rule_verifier/test/float_exprs.txt new file mode 100644 index 000000000000..0b918befde26 --- /dev/null +++ b/apps/simplifier_rule_verifier/test/float_exprs.txt @@ -0,0 +1,5 @@ +# Halide's printer emits float literals in scientific notation when they're +# small enough, so the parser has to accept an exponent. Parsing 2.5e3 +# correctly turns it back into 2500. +2.500000e+03f +1.000000e-16f diff --git a/apps/simplifier_rule_verifier/test/good_rules.txt b/apps/simplifier_rule_verifier/test/good_rules.txt new file mode 100644 index 000000000000..24bbe37bc71a --- /dev/null +++ b/apps/simplifier_rule_verifier/test/good_rules.txt @@ -0,0 +1,10 @@ +# Rules that are true, obey the reduction order, and so should all survive. +rewrite(x + 0, x) +rewrite(min(x, x), x) +rewrite(max(x, min(x, y)), x) +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) +rewrite(select(x, y, y), y) +rewrite(min(x, y) < x, y < x) +rewrite(max(x, y)*2 - x - y, max(x - y, y - x)) diff --git a/apps/simplifier_rule_verifier/test/narrow_int_rules.txt b/apps/simplifier_rule_verifier/test/narrow_int_rules.txt new file mode 100644 index 000000000000..e9dc55dec5b2 --- /dev/null +++ b/apps/simplifier_rule_verifier/test/narrow_int_rules.txt @@ -0,0 +1,6 @@ +# Halide's integer division and modulo are Euclidean at every width, so the +# remainder is never negative even when the denominator is. SMT-LIB's +# bit-vector ops don't work that way, so this pins down the encoding the tool +# uses for types narrower than 32 bits. +rewrite((int8)x % (int8)c0 < 0, false, c0 != 0) +rewrite((int16)x % (int16)c0 < 0, false, c0 != 0) diff --git a/apps/simplifier_rule_verifier/test/parser_rules.txt b/apps/simplifier_rule_verifier/test/parser_rules.txt new file mode 100644 index 000000000000..eeb52b94dcda --- /dev/null +++ b/apps/simplifier_rule_verifier/test/parser_rules.txt @@ -0,0 +1,23 @@ +# These rules are only true if the parser gets precedence and associativity +# right, so they pin down the expression grammar. + +# Multiplicative binds tighter than additive +rewrite(1 + 2*3, 7) +rewrite((1 + 2)*3, 9) + +# Additive and multiplicative are left-associative +rewrite(1 - 2 - 3, -4) +rewrite(12 / 3 / 2, 2) +rewrite(2 * 3 % 4, 2) + +# Comparisons bind looser than arithmetic +rewrite(1 + 2 < 4, true) +rewrite(2 * 3 == 6, true) + +# && binds tighter than || +rewrite(x < y && y < z || x < z, x < z) + +# Unary operators bind tighter than any binary one +rewrite(-x + y, y - x) +rewrite(-x * 2, x * -2) +rewrite(!(x < y), y <= x) diff --git a/apps/simplifier_rule_verifier/test/rules_needing_predicates.txt b/apps/simplifier_rule_verifier/test/rules_needing_predicates.txt new file mode 100644 index 000000000000..449bd3d8960d --- /dev/null +++ b/apps/simplifier_rule_verifier/test/rules_needing_predicates.txt @@ -0,0 +1,2 @@ +# A predicate of false is a request for the tool to synthesize one. +rewrite(min(x*c0, y*c0), min(x, y)*c0, false) diff --git a/apps/simplifier_rule_verifier/z3.cpp b/apps/simplifier_rule_verifier/z3.cpp new file mode 100644 index 000000000000..ec0da55c6e7b --- /dev/null +++ b/apps/simplifier_rule_verifier/z3.cpp @@ -0,0 +1,573 @@ +#include "z3.h" +#include "debug.h" +#include "expr_util.h" +#include "parser.h" + +#include + +using namespace Halide; +using namespace Halide::Internal; + +using std::map; +using std::string; + +// Record a binding, if the name is one of the variables we asked about. z3 +// invents names of its own for let-bound subexpressions, which we skip. +void record(const map &var_types, const string &name, int64_t value, + map *bindings) { + auto it = var_types.find(name); + if (it != var_types.end()) { + (*bindings)[name] = make_const(it->second, value); + } +} + +bool parse_model(const char **cursor, const char *end, const map &var_types, + map *bindings) { + consume_whitespace(cursor, end); + // Older versions of z3 tag the model with the token "model" + if (!consume(cursor, end, "(")) { + return false; + } + consume_whitespace(cursor, end); + consume(cursor, end, "model"); + consume_whitespace(cursor, end); + while (consume(cursor, end, "(define-fun")) { + consume_whitespace(cursor, end); + string name = consume_token(cursor, end); + consume_whitespace(cursor, end); + if (!consume(cursor, end, "()")) { + return false; + } + consume_whitespace(cursor, end); + if (consume(cursor, end, "Bool")) { + consume_whitespace(cursor, end); + if (consume(cursor, end, "true)")) { + record(var_types, name, 1, bindings); + } else if (consume(cursor, end, "false)")) { + record(var_types, name, 0, bindings); + } else { + return false; + } + } else if (consume(cursor, end, "Int")) { + consume_whitespace(cursor, end); + if (consume(cursor, end, "(- ")) { + record(var_types, name, -std::atoll(consume_token(cursor, end).c_str()), bindings); + consume(cursor, end, ")"); + } else { + record(var_types, name, std::atoll(consume_token(cursor, end).c_str()), bindings); + } + consume_whitespace(cursor, end); + consume(cursor, end, ")"); + } else if (consume(cursor, end, "(_ BitVec ")) { + int64_t bits = consume_int(cursor, end); + if (!consume(cursor, end, ")")) { + return false; + } + consume_whitespace(cursor, end); + if (!consume(cursor, end, "#x")) { + return false; + } + // Accumulate the bit pattern unsigned. Shifting into the sign bit + // of an int64_t, or by 64, would be undefined. + uint64_t bit_pattern = 0; + for (int i = 0; i < bits; i += 4) { + bit_pattern *= 16; + char next = (**cursor); + if (next >= '0' && next <= '9') { + bit_pattern += next - '0'; + } else if (next >= 'a' && next <= 'f') { + bit_pattern += 10 + next - 'a'; + } else { + std::cerr << "Bad hex literal char: '" << next << "'\n"; + abort(); + } + (*cursor)++; + } + // Reinterpret as signed if that's what the variable is + int64_t value = (int64_t)bit_pattern; + auto it = var_types.find(name); + if (it != var_types.end() && it->second.is_int() && bits < 64 && + bit_pattern >= (uint64_t)1 << (bits - 1)) { + value -= (int64_t)1 << bits; + } + record(var_types, name, value, bindings); + consume(cursor, end, ")"); + } else { + return false; + } + consume_whitespace(cursor, end); + } + consume_whitespace(cursor, end); + if (!consume(cursor, end, ")")) { + return false; + } + return true; +} + +// Convert from a Halide Expr to SMT2 to pass to z3. Returns false if the Expr +// uses something the conversion doesn't model, in which case the caller must +// treat the query as undecidable. +bool expr_to_smt2(const Expr &e, string *result) { + class ExprToSMT2 : public IRVisitor { + public: + std::ostringstream formula; + Expr unhandled; + + void give_up(const Expr &e) { + if (!unhandled.defined()) { + unhandled = e; + } + formula << ""; + } + + protected: + bool use_bitvector(Type t) { + return (t.is_int() && t.bits() < 32) || t.is_uint(); + } + + void visit(const IntImm *imm) override { + if (imm->type.bits() >= 32) { + formula << imm->value; + } else { + formula << "#b"; + for (int i = imm->type.bits() - 1; i >= 0; i--) { + formula << (int((imm->value >> i) & 1)); + } + } + } + + void visit(const UIntImm *imm) override { + if (imm->type.is_bool()) { + if (imm->value) { + formula << "true"; + } else { + formula << "false"; + } + } else { + formula << "#b"; + for (int i = imm->type.bits() - 1; i >= 0; i--) { + formula << (int(imm->value >> i) & 1); + } + } + } + + void visit(const FloatImm *imm) override { + formula << imm->value; + } + + void visit(const StringImm *imm) override { + formula << imm->value; + } + + void visit(const Variable *var) override { + formula << var->name; + } + + void visit(const Add *op) override { + if (use_bitvector(op->type)) { + formula << "(bvadd "; + } else { + formula << "(+ "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const Sub *op) override { + if (use_bitvector(op->type)) { + formula << "(bvsub "; + } else { + formula << "(- "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const Mul *op) override { + if (use_bitvector(op->type)) { + formula << "(bvmul "; + } else { + formula << "(* "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const Div *op) override { + if (op->type.is_int() && op->type.bits() < 32) { + formula << "(my_bvsdiv "; + } else if (op->type.is_uint()) { + formula << "(my_bvudiv "; + } else { + formula << "(my_div "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const Mod *op) override { + if (op->type.is_int() && op->type.bits() < 32) { + formula << "(my_bvsmod "; + } else if (op->type.is_uint()) { + formula << "(my_bvumod "; + } else { + formula << "(my_mod "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const Min *op) override { + if (op->type.is_int() && op->type.bits() < 32) { + formula << "(my_bvsmin "; + } else if (op->type.is_uint()) { + formula << "(my_bvumin "; + } else { + formula << "(my_min "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const Max *op) override { + if (op->type.is_int() && op->type.bits() < 32) { + formula << "(my_bvsmax "; + } else if (op->type.is_uint()) { + formula << "(my_bvumax "; + } else { + formula << "(my_max "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const EQ *op) override { + formula << "(= "; + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const NE *op) override { + formula << "(not (= "; + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << "))"; + } + + void visit(const LT *op) override { + if (op->a.type().is_int() && op->a.type().bits() < 32) { + formula << "(bvslt "; + } else if (op->a.type().is_uint()) { + formula << "(bvult "; + } else { + formula << "(< "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const LE *op) override { + if (op->a.type().is_int() && op->a.type().bits() < 32) { + formula << "(bvsle "; + } else if (op->a.type().is_uint()) { + formula << "(bvule "; + } else { + formula << "(<= "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const GT *op) override { + if (op->a.type().is_int() && op->a.type().bits() < 32) { + formula << "(bvsgt "; + } else if (op->a.type().is_uint()) { + formula << "(bvugt "; + } else { + formula << "(> "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const GE *op) override { + if (op->a.type().is_int() && op->a.type().bits() < 32) { + formula << "(bvsge "; + } else if (op->a.type().is_uint()) { + formula << "(bvuge "; + } else { + formula << "(>= "; + } + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const And *op) override { + formula << "(and "; + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const Or *op) override { + formula << "(or "; + op->a.accept(this); + formula << " "; + op->b.accept(this); + formula << ")"; + } + + void visit(const Not *op) override { + formula << "(not "; + op->a.accept(this); + formula << ")"; + } + + void visit(const Select *op) override { + formula << "(ite "; + op->condition.accept(this); + formula << " "; + op->true_value.accept(this); + formula << " "; + op->false_value.accept(this); + formula << ")"; + } + + void visit(const Cast *op) override { + const Call *call = op->value.as(); + if (call && op->type == Int(32) && call->name == "abs") { + Expr equiv = select(op->value < 0, 0 - op->value, op->value); + equiv.accept(this); + } else if (op->value.type().is_bool()) { + Expr equiv = select(op->value, cast(op->type, 1), cast(op->type, 0)); + equiv.accept(this); + } else { + give_up(op); + } + } + + void visit(const Call *op) override { + if (op->is_intrinsic(Call::signed_integer_overflow)) { + // Hrm. Just generate invalid SMT2 so we can fail in peace. + formula << ""; + } else if (op->name == "fold" || op->name == "prove_me") { + // Markers used by rewrite rules. They don't change the value. + op->args[0].accept(this); + } else { + give_up(op); + } + } + + void visit(const Ramp *op) override { + give_up(op); + } + + void visit(const Let *op) override { + formula << "(let ((" << op->name << " "; + op->value.accept(this); + formula << ")) "; + op->body.accept(this); + formula << ")"; + } + + void visit(const Broadcast *op) override { + op->value.accept(this); + } + } to_smt2; + + e.accept(&to_smt2); + if (to_smt2.unhandled.defined()) { + debug(1) << "Unhandled IR node for SMT2: " << to_smt2.unhandled << "\n"; + return false; + } + *result = to_smt2.formula.str(); + return true; +} + +// The z3 binary to run. Override it with the HL_Z3 environment variable if it +// isn't on the PATH. +string z3_executable() { + const char *s = getenv("HL_Z3"); + return s ? s : "z3"; +} + +// Rules with several symbolic constants under a div or mod can take z3 a long +// while. HL_Z3_TIMEOUT raises the per-query limit, in seconds. +int z3_timeout(int suggested) { + const char *s = getenv("HL_Z3_TIMEOUT"); + return s ? atoi(s) : suggested; +} + +Z3Result +satisfy(Expr e, map *bindings, const string &comment, int timeout) { + + // Branch hints don't affect the value, and z3 has no notion of them + e = simplify(common_subexpression_elimination(remove_likelies(e))); + + if (is_const_one(e)) { + return Z3Result::Sat; + } + if (is_const_zero(e)) { + return Z3Result::Unsat; + } + if (!e.type().is_bool()) { + std::cout << "Cannot satisfy non-boolean expression " << e << "\n"; + abort(); + } + + std::ostringstream z3_source; + + z3_source << "; " << comment << "\n"; + + map var_types; + for (const auto &v : find_vars(e)) { + Type t = v.second.first.type(); + var_types[v.first] = t; + if (t.is_bool()) { + z3_source << "(declare-const " << v.first << " Bool)\n"; + } else if (t.is_int() && t.bits() >= 32) { + // Matches expr_to_smt2, which uses unbounded Int arithmetic for + // signed types of 32 bits and wider + z3_source << "(declare-const " << v.first << " Int)\n"; + } else { + z3_source << "(declare-const " << v.first << " (_ BitVec " << v.second.first.type().bits() << "))\n"; + } + } + + z3_source << "(define-fun my_min ((x Int) (y Int)) Int (ite (< x y) x y))\n" + << "(define-fun my_max ((x Int) (y Int)) Int (ite (< x y) y x))\n" + << "(define-fun my_div ((x Int) (y Int)) Int (ite (= y 0) 0 (div x y)))\n" + << "(define-fun my_mod ((x Int) (y Int)) Int (ite (= y 0) 0 (mod x y)))\n"; + + // Halide's integer division and modulo are Euclidean: 0 <= a%b < |b|, and + // (a/b)*b + a%b == a. Both return zero when b is zero. SMT-LIB's Int div + // and mod are Euclidean too, but its bit-vector ops are not: bvsdiv + // truncates towards zero and bvsrem takes the sign of the dividend, so the + // fixed-width versions correct the quotient and remainder when bvsrem + // comes out negative. + for (int i = 8; i <= 32; i *= 2) { + std::ostringstream ty, zero, args; + ty << "(_ BitVec " << i << ")"; + zero << "(_ bv0 " << i << ")"; + args << "((x " << ty.str() << ") (y " << ty.str() << ")) " << ty.str(); + const string z = zero.str(); + z3_source << "(define-fun my_bvsmin " << args.str() << " (ite (bvslt x y) x y))\n" + << "(define-fun my_bvsmax " << args.str() << " (ite (bvslt x y) y x))\n" + << "(define-fun my_bvumin " << args.str() << " (ite (bvult x y) x y))\n" + << "(define-fun my_bvumax " << args.str() << " (ite (bvult x y) y x))\n" + << "(define-fun my_bvsmod " << args.str() + << " (ite (= y " << z << ") " << z + << " (let ((r (bvsrem x y)))" + << " (ite (bvslt r " << z << ")" + << " (bvadd r (ite (bvslt y " << z << ") (bvneg y) y)) r))))\n" + << "(define-fun my_bvsdiv " << args.str() + << " (ite (= y " << z << ") " << z + << " (let ((q (bvsdiv x y)))" + << " (ite (bvslt (bvsrem x y) " << z << ")" + << " (ite (bvsgt y " << z << ") (bvsub q (_ bv1 " << i << ")) (bvadd q (_ bv1 " << i << ")))" + << " q))))\n" + << "(define-fun my_bvumod " << args.str() + << " (ite (= y " << z << ") " << z << " (bvurem x y)))\n" + << "(define-fun my_bvudiv " << args.str() + << " (ite (= y " << z << ") " << z << " (bvudiv x y)))\n"; + } + + Expr orig = e; + while (const Let *l = e.as()) { + if (l->value.type().is_int() && l->value.type().bits() >= 32) { + z3_source << "(declare-const " << l->name << " Int)\n"; + } else if (l->value.type().is_bool()) { + z3_source << "(declare-const " << l->name << " Bool)\n"; + } else { + break; + } + string value; + if (!expr_to_smt2(l->value, &value)) { + return Z3Result::Unknown; + } + z3_source << "(assert (= " << l->name << " " << value << "))\n"; + e = l->body; + } + + string formula; + if (!expr_to_smt2(e, &formula)) { + return Z3Result::Unknown; + } + + z3_source << "(assert " << formula << ")\n" + << "(check-sat)\n" + << "(get-model)\n"; + + string src = z3_source.str(); + + debug(2) << "z3 query:\n" + << src << "\n"; + + TemporaryFile z3_file("query", "z3"); + TemporaryFile z3_output("output", "txt"); + write_entire_file(z3_file.pathname(), &src[0], src.size()); + + // No shell involved, so nothing here needs quoting or escaping + int ret = run_process({z3_executable(), + "-T:" + std::to_string(z3_timeout(timeout)), + z3_file.pathname()}, + z3_output.pathname(), ""); + + auto result_vec = read_entire_file(z3_output.pathname()); + string result(result_vec.begin(), result_vec.end()); + + debug(2) << "z3 produced: " << result << "\n"; + + if (starts_with(result, "unknown") || starts_with(result, "timeout")) { + return Z3Result::Unknown; + } + + if (ret && !starts_with(result, "unsat")) { + std::cout << "** z3 query failed with exit code " << ret << "\n" + << "** query was:\n" + << src << "\n" + << "** output was:\n" + << result << "\n" + << "** Expr was:\n" + << orig << "\n"; + return Z3Result::Unknown; + } + + if (starts_with(result, "unsat")) { + return Z3Result::Unsat; + } else { + const char *cursor = &(result[0]); + const char *end = &(result[result.size()]); + if (!consume(&cursor, end, "sat")) { + return Z3Result::Unknown; + } + parse_model(&cursor, end, var_types, bindings); + return Z3Result::Sat; + } +} diff --git a/apps/simplifier_rule_verifier/z3.h b/apps/simplifier_rule_verifier/z3.h new file mode 100644 index 000000000000..886a6467056c --- /dev/null +++ b/apps/simplifier_rule_verifier/z3.h @@ -0,0 +1,30 @@ +#ifndef Z3_H +#define Z3_H + +#include "Halide.h" + +// Wrapper to use Z3 to do satisfiability queries on Halide Exprs + +enum class Z3Result { + Sat, + Unsat, + Unknown +}; + +inline std::ostream &operator<<(std::ostream &s, Z3Result r) { + switch (r) { + case Z3Result::Sat: + s << "Sat"; + break; + case Z3Result::Unsat: + s << "Unsat"; + break; + case Z3Result::Unknown: + s << "Unknown"; + } + return s; +} + +Z3Result satisfy(Halide::Expr constraint, std::map *result, const std::string &comment = "", int timeout = 60); + +#endif diff --git a/src/Simplify_EQ.cpp b/src/Simplify_EQ.cpp index e676e9fb34aa..9f802166d1b7 100644 --- a/src/Simplify_EQ.cpp +++ b/src/Simplify_EQ.cpp @@ -308,7 +308,8 @@ Expr Simplify::visit(const EQ *op, ExprInfo *info) { false)) || (no_overflow_int(a.type()) && - (rewrite((x + c0) % c1 == c2, x % c1 == fold((c2 - c0) % c1)) || + (rewrite((x + c0) % c1 == c2, x % c1 == fold((c2 - c0) % c1), + 0 <= c2 && c2 < max(c1, -c1)) || rewrite(x == x % c0, x / c0 == 0, c0 != 0) || rewrite(x % c0 == x, x / c0 == 0, c0 != 0) || rewrite(x == (x / c0) * c0, x % c0 == 0, c0 != 0) || diff --git a/test/correctness/simplify.cpp b/test/correctness/simplify.cpp index e9202f6a1d0a..a03b37d531fb 100644 --- a/test/correctness/simplify.cpp +++ b/test/correctness/simplify.cpp @@ -440,6 +440,12 @@ void check_algebra() { check((x * 8 - y) % 4, (-y) % 4); check((x + 31) % 32 == 31, x % 32 == 0); check((x - 1) % 32 == 31, x % 32 == 0); + // A remainder lies in [0, |c|), for negative divisors too + check((x + 3) % 14 == 1, x % 14 == 12); + check((x + 3) % -14 == 1, x % -14 == 12); + check((x + 3) % 14 == -1, f); + check((x + 3) % 14 == 20, f); + check((x + 3) % -14 == -1, f); // Check an optimization important for fusing dimensions check((x / 3) * 3 + x % 3, x);