From 894baf65d820dd109facf8bfbd800928f0779dd6 Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Thu, 13 Aug 2026 10:53:16 -0700 Subject: [PATCH 01/10] Add apps/simplifier_rule_verifier A port of apps/super_simplify from the super_simplify_v3 branch, where it had been left to bit-rot since 2021. filter_rewrite_rules takes a file of proposed simplifier rules in Simplify_*.cpp syntax and checks each one with z3 for correctness, against a reduction order for termination, and against the other rules for subsumption. super_simplify searches for the smallest expression equivalent to a given one by CEGIS. Dropped synthesize_predicate.cpp and the tools that depended on it. Both of its entry points were only reachable from disabled branches, and it was built on internal Simplify APIs that would have forced the app to build against src/ rather than an installed Halide. The predicate synthesis that filter_rewrite_rules actually uses is implemented inline and is unaffected. Also fixed, in the course of getting it running again: - z3 no longer tags models with "model", so every counterexample came back empty. - fold() in a rule aborted the SMT conversion. - Rules z3 disproved were still emitted as good rules. - bvumod is not an SMT-LIB operator, so unsigned mod produced invalid SMT2. - Integer division and modulo are Euclidean at every width in Halide, but the narrow-integer encoding used raw bvsmod and a floor-division bvsdiv, and handled neither division by zero. Verified against div_imp/mod_imp on all 65536 int8 operand pairs. - An unmodelled intrinsic in one rule aborted the whole run. - The parser had no unary minus, and could not reparse a Select as boolean. The parser's precedence ladder is now a precedence-climbing loop over a table of operators, which drops the pushback stack it used to thread between levels. Verified by reparsing every rule in src/Simplify_*.cpp and diffing: the only change is that && and || are left-associative, as in C++. Tested by ctest under the label simplifier_rule_verifier, and by make test. Both skip when z3 isn't installed, so the macOS CI job that builds apps now installs it. Co-Authored-By: Claude Opus 5 --- .github/workflows/testing-macos.yml | 4 + apps/CMakeLists.txt | 1 + apps/simplifier_rule_verifier/.gitignore | 2 + apps/simplifier_rule_verifier/CMakeLists.txt | 118 ++ apps/simplifier_rule_verifier/Makefile | 31 + apps/simplifier_rule_verifier/README.md | 108 ++ apps/simplifier_rule_verifier/debug.h | 36 + apps/simplifier_rule_verifier/expr_util.cpp | 527 ++++++++ apps/simplifier_rule_verifier/expr_util.h | 61 + .../filter_rewrite_rules.cpp | 1076 +++++++++++++++++ apps/simplifier_rule_verifier/parser.cpp | 539 +++++++++ apps/simplifier_rule_verifier/parser.h | 37 + .../reduction_order.cpp | 494 ++++++++ .../reduction_order.h | 9 + .../super_simplify.cpp | 392 ++++++ .../simplifier_rule_verifier/super_simplify.h | 12 + .../super_simplify_tool.cpp | 22 + .../test/bad_rules.txt | 9 + apps/simplifier_rule_verifier/test/exprs.txt | 2 + .../test/good_rules.txt | 10 + .../test/narrow_int_rules.txt | 6 + .../test/parser_rules.txt | 23 + .../test/rules_needing_predicates.txt | 2 + apps/simplifier_rule_verifier/z3.cpp | 561 +++++++++ apps/simplifier_rule_verifier/z3.h | 30 + 25 files changed, 4112 insertions(+) create mode 100644 apps/simplifier_rule_verifier/.gitignore create mode 100644 apps/simplifier_rule_verifier/CMakeLists.txt create mode 100644 apps/simplifier_rule_verifier/Makefile create mode 100644 apps/simplifier_rule_verifier/README.md create mode 100644 apps/simplifier_rule_verifier/debug.h create mode 100644 apps/simplifier_rule_verifier/expr_util.cpp create mode 100644 apps/simplifier_rule_verifier/expr_util.h create mode 100644 apps/simplifier_rule_verifier/filter_rewrite_rules.cpp create mode 100644 apps/simplifier_rule_verifier/parser.cpp create mode 100644 apps/simplifier_rule_verifier/parser.h create mode 100644 apps/simplifier_rule_verifier/reduction_order.cpp create mode 100644 apps/simplifier_rule_verifier/reduction_order.h create mode 100644 apps/simplifier_rule_verifier/super_simplify.cpp create mode 100644 apps/simplifier_rule_verifier/super_simplify.h create mode 100644 apps/simplifier_rule_verifier/super_simplify_tool.cpp create mode 100644 apps/simplifier_rule_verifier/test/bad_rules.txt create mode 100644 apps/simplifier_rule_verifier/test/exprs.txt create mode 100644 apps/simplifier_rule_verifier/test/good_rules.txt create mode 100644 apps/simplifier_rule_verifier/test/narrow_int_rules.txt create mode 100644 apps/simplifier_rule_verifier/test/parser_rules.txt create mode 100644 apps/simplifier_rule_verifier/test/rules_needing_predicates.txt create mode 100644 apps/simplifier_rule_verifier/z3.cpp create mode 100644 apps/simplifier_rule_verifier/z3.h diff --git a/.github/workflows/testing-macos.yml b/.github/workflows/testing-macos.yml index a67ef4dc77eb..4546ad94cc93 100644 --- a/.github/workflows/testing-macos.yml +++ b/.github/workflows/testing-macos.yml @@ -85,6 +85,10 @@ jobs: - name: Install wasm toolchain run: brew install emscripten + # Used by apps/simplifier_rule_verifier, which skips its tests without it. + - name: Install z3 + run: brew install z3 + # AppleClang on Intel unconditionally injects /usr/local/include and # /usr/local/lib into every compile/link, below CMake's control. # Homebrew's jpeg-turbo (built with -DWITH_JPEG8=1, i.e. reports 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..52481a49009d --- /dev/null +++ b/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) +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\\)" +) diff --git a/apps/simplifier_rule_verifier/Makefile b/apps/simplifier_rule_verifier/Makefile new file mode 100644 index 000000000000..d75d83ea18cc --- /dev/null +++ b/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) 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..eedd7ab2b9a7 --- /dev/null +++ b/apps/simplifier_rule_verifier/expr_util.cpp @@ -0,0 +1,527 @@ +#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); + 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(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..e9dd909f4baf --- /dev/null +++ b/apps/simplifier_rule_verifier/super_simplify.cpp @@ -0,0 +1,392 @@ +#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); + 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/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..fadd8789be27 --- /dev/null +++ b/apps/simplifier_rule_verifier/z3.cpp @@ -0,0 +1,561 @@ +#include "z3.h" +#include "debug.h" +#include "expr_util.h" +#include "parser.h" + +using namespace Halide; +using namespace Halide::Internal; + +using std::map; +using std::string; + +bool parse_model(const char **cursor, const char *end, 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); + bool interesting = !starts_with(name, "z3name!") && name[0] != 't'; + if (consume(cursor, end, "true)")) { + if (interesting) { + (*bindings)[name] = const_true(); + } + } else if (consume(cursor, end, "false)")) { + if (interesting) { + (*bindings)[name] = const_false(); + } + } else { + return false; + } + } else if (consume(cursor, end, "Int")) { + consume_whitespace(cursor, end); + if (consume(cursor, end, "(- ")) { + string val = consume_token(cursor, end); + if (!starts_with(name, "z3name!") && name[0] != 't') { + (*bindings)[name] = -std::atoi(val.c_str()); + } + consume(cursor, end, ")"); + } else { + string val = consume_token(cursor, end); + if (!starts_with(name, "z3name!") && name[0] != 't') { + (*bindings)[name] = std::atoi(val.c_str()); + } + } + 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; + } + int64_t result = 0; + for (int i = 0; i < bits; i += 4) { + result *= 16; + char next = (**cursor); + if (next >= '0' && next <= '9') { + result += next - '0'; + } else if (next >= 'a' && next <= 'f') { + result += 10 + next - 'a'; + } else { + std::cerr << "Bad hex literal char: '" << next << "'\n"; + abort(); + } + (*cursor)++; + } + // We only deal in signed + if (result >= (1 << (bits - 1))) { + result -= (1 << bits); + } + if (!starts_with(name, "z3name!") && name[0] != 't') { + (*bindings)[name] = (int)result; + } + 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) { + + e = simplify(common_subexpression_elimination(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"; + + for (const auto &v : find_vars(e)) { + if (v.second.first.type().is_bool()) { + z3_source << "(declare-const " << v.first << " Bool)\n"; + } else if (v.second.first.type() == Int(32)) { + 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()); + + string cmd = (z3_executable() + " -T:" + std::to_string(z3_timeout(timeout)) + + " " + z3_file.pathname() + " > " + z3_output.pathname()); + + int ret = pclose(popen(cmd.c_str(), "r")); + + 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, 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 From c2870e56d4dafcb6beab9e1dd079d8820bfde7ea Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Thu, 13 Aug 2026 10:53:24 -0700 Subject: [PATCH 02/10] Make the (x + c0) % c1 == c2 rewrite rule correct in isolation A remainder always lies in [0, |c1|), so for c2 outside that range the left hand side is false while the right hand side need not be. The rule relied on the bounds analysis in Simplify_EQ having already folded such comparisons away, which it does, so this changes no behaviour. It makes the rule stand on its own rather than on the order of the passes around it. Found by apps/simplifier_rule_verifier, which checks rules in isolation. Co-Authored-By: Claude Opus 5 --- src/Simplify_EQ.cpp | 3 ++- test/correctness/simplify.cpp | 6 ++++++ 2 files changed, 8 insertions(+), 1 deletion(-) 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); From 338dfabca806c53cc1fec42622011f1af16a7a15 Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Thu, 13 Aug 2026 11:10:41 -0700 Subject: [PATCH 03/10] Fix bugs in apps/simplifier_rule_verifier found by code review All but one predate the port. The search for a free wildcard name, used when demoting a constant wildcard that appears in neither a fold nor a predicate, tested against a copy of the rule taken before any substitution. Every constant wildcard therefore picked the same name and they collapsed into one variable, so the rule written out was not the rule that had been checked. Given rewrite(select(u, x + c0, x + c1), x + select(u, c0, c1)) it emitted select(x, y + z, z + y) -> select(x, y, y) + z, which is false. Parsing a bit-vector out of a z3 model shifted by up to 64 to find the sign bit, which is undefined and in practice took the sign-extend branch every time, so any counterexample mentioning a variable of 32 bits or wider was reported wrong. It also built every binding as an Int(32) regardless of the variable's real type. Both now come from the types the query was built with, which also lets z3's names for let-bound subexpressions be filtered by lookup rather than by guessing that anything starting with 't' is one. Variables of type Int(64) were declared as bit-vectors while their operators were emitted as unbounded-Int ones, so z3 rejected the query and the rule was silently classed unverifiable. likely and likely_if_innermost were not understood by the SMT conversion, so rules mentioning them were emitted without ever being checked. They only carry a branch hint, so the conversion now sees through them, as it does for fold. The parser was also turning likely_if_innermost into likely, quietly changing such rules on round-trip. all_possible_exprs_that_compute_associative_op_helper was missing the bail-out that its sibling has, so a long enough chain of terms would shift past the width of an int and exhaust memory well before that. consume() read a byte before checking it was in bounds. The binding map threaded through predicate synthesis was left over from the dropped synthesize_predicate, and was shadowed by the inner declarations that replaced it, so the code substituting it back into the rule did nothing. Co-Authored-By: Claude Opus 5 --- apps/simplifier_rule_verifier/expr_util.cpp | 10 +++ .../filter_rewrite_rules.cpp | 31 ++++---- apps/simplifier_rule_verifier/parser.cpp | 4 +- apps/simplifier_rule_verifier/z3.cpp | 73 +++++++++++-------- 4 files changed, 67 insertions(+), 51 deletions(-) diff --git a/apps/simplifier_rule_verifier/expr_util.cpp b/apps/simplifier_rule_verifier/expr_util.cpp index eedd7ab2b9a7..ceea1fb152ed 100644 --- a/apps/simplifier_rule_verifier/expr_util.cpp +++ b/apps/simplifier_rule_verifier/expr_util.cpp @@ -387,6 +387,16 @@ void all_possible_exprs_that_compute_associative_op_helper(const Expr &e, } 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++) { diff --git a/apps/simplifier_rule_verifier/filter_rewrite_rules.cpp b/apps/simplifier_rule_verifier/filter_rewrite_rules.cpp index 6ab1aea56fb1..491ff6d84c3f 100644 --- a/apps/simplifier_rule_verifier/filter_rewrite_rules.cpp +++ b/apps/simplifier_rule_verifier/filter_rewrite_rules.cpp @@ -460,7 +460,6 @@ void check_rule(Rule &r) { } } - map binding; if (is_const_zero(r.predicate)) { out << "Synthesizing a predicate for " << r.orig << "\n"; Expr new_predicate = const_true(); @@ -661,12 +660,6 @@ void check_rule(Rule &r) { out << "Rewrote predicate: " << r.predicate << " -> " << new_predicate << "\n"; r.predicate = new_predicate; } - r.lhs = substitute(binding, r.lhs); - - for (auto &it : binding) { - it.second = Call::make(it.second.type(), "fold", {it.second}, Call::PureExtern); - } - r.rhs = substitute(binding, r.rhs); } } @@ -802,19 +795,21 @@ int main(int argc, char **argv) { e.accept(&finder); for (const auto &v : finder.all) { - if (finder.used_in_fold.count(v)) { + if (finder.used_in_fold.count(v) || v[0] != 'c') { continue; } - if (v[0] == 'c') { - // Find a free wildcard var to replace it with - const char *names[] = {"x", "y", "z", "w", "u", "v"}; - for (const char *n : names) { - if (!expr_uses_var(e, n)) { - Expr var = Variable::make(Int(32), n); - r.lhs = substitute(v, var, r.lhs); - r.rhs = substitute(v, var, r.rhs); - break; - } + // Find a wildcard name that isn't taken. The rule is rewritten as + // we go, so check it rather than the copy taken above, otherwise + // every constant wildcard picks the same name and they collapse + // into one. + for (const char *n : {"x", "y", "z", "w", "u", "v"}) { + if (!expr_uses_var(r.lhs, n) && + !expr_uses_var(r.rhs, n) && + !expr_uses_var(r.predicate, n)) { + Expr var = Variable::make(Int(32), n); + r.lhs = substitute(v, var, r.lhs); + r.rhs = substitute(v, var, r.rhs); + break; } } } diff --git a/apps/simplifier_rule_verifier/parser.cpp b/apps/simplifier_rule_verifier/parser.cpp index 3b0a29553ff6..6ee0b28a2231 100644 --- a/apps/simplifier_rule_verifier/parser.cpp +++ b/apps/simplifier_rule_verifier/parser.cpp @@ -25,7 +25,7 @@ void consume_whitespace(const char **cursor, const char *end) { bool consume(const char **cursor, const char *end, const char *expected) { const char *tmp = *cursor; - while (*tmp == *expected && tmp < end && *expected) { + while (tmp < end && *expected && *tmp == *expected) { tmp++; expected++; } @@ -368,7 +368,7 @@ class Parser { if (consume("likely_if_innermost(")) { Expr a = parse_expr(); expect(")"); - return likely(a); + return likely_if_innermost(a); } Type expected_type = Int(32); diff --git a/apps/simplifier_rule_verifier/z3.cpp b/apps/simplifier_rule_verifier/z3.cpp index fadd8789be27..6e5763904632 100644 --- a/apps/simplifier_rule_verifier/z3.cpp +++ b/apps/simplifier_rule_verifier/z3.cpp @@ -9,7 +9,18 @@ using namespace Halide::Internal; using std::map; using std::string; -bool parse_model(const char **cursor, const char *end, map *bindings) { +// 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, "(")) { @@ -28,31 +39,20 @@ bool parse_model(const char **cursor, const char *end, map *bindin consume_whitespace(cursor, end); if (consume(cursor, end, "Bool")) { consume_whitespace(cursor, end); - bool interesting = !starts_with(name, "z3name!") && name[0] != 't'; if (consume(cursor, end, "true)")) { - if (interesting) { - (*bindings)[name] = const_true(); - } + record(var_types, name, 1, bindings); } else if (consume(cursor, end, "false)")) { - if (interesting) { - (*bindings)[name] = const_false(); - } + record(var_types, name, 0, bindings); } else { return false; } } else if (consume(cursor, end, "Int")) { consume_whitespace(cursor, end); if (consume(cursor, end, "(- ")) { - string val = consume_token(cursor, end); - if (!starts_with(name, "z3name!") && name[0] != 't') { - (*bindings)[name] = -std::atoi(val.c_str()); - } + record(var_types, name, -std::atoll(consume_token(cursor, end).c_str()), bindings); consume(cursor, end, ")"); } else { - string val = consume_token(cursor, end); - if (!starts_with(name, "z3name!") && name[0] != 't') { - (*bindings)[name] = std::atoi(val.c_str()); - } + record(var_types, name, std::atoll(consume_token(cursor, end).c_str()), bindings); } consume_whitespace(cursor, end); consume(cursor, end, ")"); @@ -65,27 +65,30 @@ bool parse_model(const char **cursor, const char *end, map *bindin if (!consume(cursor, end, "#x")) { return false; } - int64_t result = 0; + // 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) { - result *= 16; + bit_pattern *= 16; char next = (**cursor); if (next >= '0' && next <= '9') { - result += next - '0'; + bit_pattern += next - '0'; } else if (next >= 'a' && next <= 'f') { - result += 10 + next - 'a'; + bit_pattern += 10 + next - 'a'; } else { std::cerr << "Bad hex literal char: '" << next << "'\n"; abort(); } (*cursor)++; } - // We only deal in signed - if (result >= (1 << (bits - 1))) { - result -= (1 << bits); - } - if (!starts_with(name, "z3name!") && name[0] != 't') { - (*bindings)[name] = (int)result; + // 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; @@ -371,8 +374,11 @@ bool expr_to_smt2(const Expr &e, string *result) { 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. + } else if (op->is_intrinsic(Call::likely) || + op->is_intrinsic(Call::likely_if_innermost) || + op->name == "fold" || op->name == "prove_me") { + // Branch hints, and markers used by rewrite rules. None of + // them change the value they wrap. op->args[0].accept(this); } else { give_up(op); @@ -439,10 +445,15 @@ satisfy(Expr e, map *bindings, const string &comment, int timeout) z3_source << "; " << comment << "\n"; + map var_types; for (const auto &v : find_vars(e)) { - if (v.second.first.type().is_bool()) { + 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 (v.second.first.type() == Int(32)) { + } 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"; @@ -555,7 +566,7 @@ satisfy(Expr e, map *bindings, const string &comment, int timeout) if (!consume(&cursor, end, "sat")) { return Z3Result::Unknown; } - parse_model(&cursor, end, bindings); + parse_model(&cursor, end, var_types, bindings); return Z3Result::Sat; } } From 4075f8e70911e1cf469b9492e76161e5fb06dbfd Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Thu, 13 Aug 2026 11:16:26 -0700 Subject: [PATCH 04/10] Don't install z3 in the macOS CI job The Linux buildbots already build and test every app, so the rule verifier gets its coverage there. Installing z3 on the macOS runner only added load to a machine that's already oversubscribed, for a second set of the same results. Without z3 the tests aren't registered at all, so the macOS apps build is unaffected. Co-Authored-By: Claude Opus 5 --- .github/workflows/testing-macos.yml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.github/workflows/testing-macos.yml b/.github/workflows/testing-macos.yml index 4546ad94cc93..a67ef4dc77eb 100644 --- a/.github/workflows/testing-macos.yml +++ b/.github/workflows/testing-macos.yml @@ -85,10 +85,6 @@ jobs: - name: Install wasm toolchain run: brew install emscripten - # Used by apps/simplifier_rule_verifier, which skips its tests without it. - - name: Install z3 - run: brew install z3 - # AppleClang on Intel unconditionally injects /usr/local/include and # /usr/local/lib into every compile/link, below CMake's control. # Homebrew's jpeg-turbo (built with -DWITH_JPEG8=1, i.e. reports From 429dd1050684c07496b8393562b6005777f6cf3a Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Thu, 13 Aug 2026 11:22:54 -0700 Subject: [PATCH 05/10] Strip branch hints with remove_likelies rather than by hand satisfy() has to see through likely and likely_if_innermost, since they don't change the value and z3 has no notion of them. IROperator.h already has a helper for exactly that, so use it on the whole expression instead of special-casing the two intrinsics in the SMT conversion's Call visitor. Co-Authored-By: Claude Opus 5 --- apps/simplifier_rule_verifier/z3.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/apps/simplifier_rule_verifier/z3.cpp b/apps/simplifier_rule_verifier/z3.cpp index 6e5763904632..77be9937f5b4 100644 --- a/apps/simplifier_rule_verifier/z3.cpp +++ b/apps/simplifier_rule_verifier/z3.cpp @@ -374,11 +374,8 @@ bool expr_to_smt2(const Expr &e, string *result) { if (op->is_intrinsic(Call::signed_integer_overflow)) { // Hrm. Just generate invalid SMT2 so we can fail in peace. formula << ""; - } else if (op->is_intrinsic(Call::likely) || - op->is_intrinsic(Call::likely_if_innermost) || - op->name == "fold" || op->name == "prove_me") { - // Branch hints, and markers used by rewrite rules. None of - // them change the value they wrap. + } 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); @@ -428,7 +425,8 @@ int z3_timeout(int suggested) { Z3Result satisfy(Expr e, map *bindings, const string &comment, int timeout) { - e = simplify(common_subexpression_elimination(e)); + // 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; From 6c117b6e32b8cded930619c22fbc494621e5ea1a Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Thu, 13 Aug 2026 11:25:51 -0700 Subject: [PATCH 06/10] Use Halide::Tools::ThreadPool instead of a hand-rolled work queue The original app used the ThreadPool in src/, which isn't part of the public API, so the port replaced it with a small index-based work queue. There's an equivalent in tools/halide_thread_pool.h with the same async() interface, which apps can reach through Halide::Tools, so use that instead. Co-Authored-By: Claude Opus 5 --- apps/simplifier_rule_verifier/CMakeLists.txt | 2 +- .../filter_rewrite_rules.cpp | 34 +++++++------------ 2 files changed, 14 insertions(+), 22 deletions(-) diff --git a/apps/simplifier_rule_verifier/CMakeLists.txt b/apps/simplifier_rule_verifier/CMakeLists.txt index 52481a49009d..23ff0409f231 100644 --- a/apps/simplifier_rule_verifier/CMakeLists.txt +++ b/apps/simplifier_rule_verifier/CMakeLists.txt @@ -19,7 +19,7 @@ add_library( super_simplify.cpp z3.cpp ) -target_link_libraries(rule_verifier_support PUBLIC Halide::Halide) +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) diff --git a/apps/simplifier_rule_verifier/filter_rewrite_rules.cpp b/apps/simplifier_rule_verifier/filter_rewrite_rules.cpp index 491ff6d84c3f..c11d4831cff0 100644 --- a/apps/simplifier_rule_verifier/filter_rewrite_rules.cpp +++ b/apps/simplifier_rule_verifier/filter_rewrite_rules.cpp @@ -1,18 +1,20 @@ #include "Halide.h" #include "debug.h" #include "expr_util.h" +#include "halide_thread_pool.h" #include "parser.h" #include "reduction_order.h" #include "z3.h" #include #include +#include #include #include -#include using namespace Halide; using namespace Halide::Internal; +using Halide::Tools::ThreadPool; // Take a list of rewrite rules and classify them by root IR node, and // what problems they might have that require further investigation. @@ -403,25 +405,6 @@ struct ScopedFlush { } }; -// Run f on every element of v, using one thread per core. -template -void parallel_for_each(vector &v, F f) { - std::atomic next{0}; - vector threads; - size_t num_threads = std::max(1u, std::thread::hardware_concurrency()); - num_threads = std::min(num_threads, v.size()); - for (size_t i = 0; i < num_threads; i++) { - threads.emplace_back([&]() { - for (size_t j = next++; j < v.size(); j = next++) { - f(v[j]); - } - }); - } - for (auto &t : threads) { - t.join(); - } -} - void check_rule(Rule &r) { std::ostringstream out; ScopedFlush flush_out(out); @@ -700,7 +683,16 @@ int main(int argc, char **argv) { // Check the rules, and synthesize predicates for any that ask for one. Each // check shells out to z3, so run a few at a time. - parallel_for_each(rules, check_rule); + { + ThreadPool pool; + vector> futures; + for (Rule &r : rules) { + futures.emplace_back(pool.async([&r]() { check_rule(r); })); + } + for (auto &f : futures) { + f.get(); + } + } std::cout << "Done checking rules\n"; From d9015ee98d442811d138b59964a0a2f9292e1292 Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Fri, 14 Aug 2026 09:06:31 -0700 Subject: [PATCH 07/10] Run z3 with system() rather than popen(), for Windows popen and pclose are POSIX-only, so the Windows bots couldn't build the app. The pipe was never read: z3's output is redirected to a file and read back from there, and only the exit status is used. system() gives us that and is standard C++, so there's nothing to shim. Also quote the two temporary file paths, which on Windows land under a temp directory that may contain spaces. Co-Authored-By: Claude Opus 5 --- apps/simplifier_rule_verifier/z3.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/apps/simplifier_rule_verifier/z3.cpp b/apps/simplifier_rule_verifier/z3.cpp index 77be9937f5b4..8f261868f900 100644 --- a/apps/simplifier_rule_verifier/z3.cpp +++ b/apps/simplifier_rule_verifier/z3.cpp @@ -3,6 +3,8 @@ #include "expr_util.h" #include "parser.h" +#include + using namespace Halide; using namespace Halide::Internal; @@ -532,9 +534,11 @@ satisfy(Expr e, map *bindings, const string &comment, int timeout) write_entire_file(z3_file.pathname(), &src[0], src.size()); string cmd = (z3_executable() + " -T:" + std::to_string(z3_timeout(timeout)) + - " " + z3_file.pathname() + " > " + z3_output.pathname()); + " \"" + z3_file.pathname() + "\" > \"" + z3_output.pathname() + "\""); - int ret = pclose(popen(cmd.c_str(), "r")); + // z3's output is redirected to a file, so all we need back is the exit + // status. popen would leave us a pipe we never read, and isn't portable. + int ret = std::system(cmd.c_str()); auto result_vec = read_entire_file(z3_output.pathname()); string result(result_vec.begin(), result_vec.end()); @@ -546,7 +550,7 @@ satisfy(Expr e, map *bindings, const string &comment, int timeout) } if (ret && !starts_with(result, "unsat")) { - std::cout << "** z3 query failed with exit code " << ret << "\n" + std::cout << "** z3 query failed, status " << ret << "\n" << "** query was:\n" << src << "\n" << "** output was:\n" From 49ed803b4636e1b3e69f884dfa9aa3e8f76c341e Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Fri, 14 Aug 2026 09:37:58 -0700 Subject: [PATCH 08/10] Run z3 with run_process rather than system() Util.h has run_process, which spawns the child directly instead of going through a shell, and the merged branch adds an overload that redirects its stdout to a file. That's exactly what this needs, so no shell command has to be built at all: the temporary file paths become plain arguments, and the quoting added for Windows temp directories is no longer necessary. The return value is now the child's exit code rather than a shell wait status, so the diagnostic for a failed query reports a usable number. Co-Authored-By: Claude Opus 5 --- apps/simplifier_rule_verifier/z3.cpp | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/apps/simplifier_rule_verifier/z3.cpp b/apps/simplifier_rule_verifier/z3.cpp index 8f261868f900..ec0da55c6e7b 100644 --- a/apps/simplifier_rule_verifier/z3.cpp +++ b/apps/simplifier_rule_verifier/z3.cpp @@ -533,12 +533,11 @@ satisfy(Expr e, map *bindings, const string &comment, int timeout) TemporaryFile z3_output("output", "txt"); write_entire_file(z3_file.pathname(), &src[0], src.size()); - string cmd = (z3_executable() + " -T:" + std::to_string(z3_timeout(timeout)) + - " \"" + z3_file.pathname() + "\" > \"" + z3_output.pathname() + "\""); - - // z3's output is redirected to a file, so all we need back is the exit - // status. popen would leave us a pipe we never read, and isn't portable. - int ret = std::system(cmd.c_str()); + // 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()); @@ -550,7 +549,7 @@ satisfy(Expr e, map *bindings, const string &comment, int timeout) } if (ret && !starts_with(result, "unsat")) { - std::cout << "** z3 query failed, status " << ret << "\n" + std::cout << "** z3 query failed with exit code " << ret << "\n" << "** query was:\n" << src << "\n" << "** output was:\n" From 9b8f0fae3bd7899153d46522908af792f12ddffb Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Fri, 14 Aug 2026 17:42:06 -0700 Subject: [PATCH 09/10] Parse float literals in scientific notation Halide's printer emits small floats as e.g. 1.000000e-16f, but the parser stopped at the 'e' and then failed on the leftover exponent. Found by feeding it a corpus of Exprs collected from a real build, where 16 of the 844 were unparseable for this reason. Co-Authored-By: Claude Opus 5 --- apps/simplifier_rule_verifier/CMakeLists.txt | 12 ++++++++++++ apps/simplifier_rule_verifier/Makefile | 1 + apps/simplifier_rule_verifier/parser.cpp | 10 ++++++++++ apps/simplifier_rule_verifier/test/float_exprs.txt | 5 +++++ 4 files changed, 28 insertions(+) create mode 100644 apps/simplifier_rule_verifier/test/float_exprs.txt diff --git a/apps/simplifier_rule_verifier/CMakeLists.txt b/apps/simplifier_rule_verifier/CMakeLists.txt index 23ff0409f231..7534899a24d2 100644 --- a/apps/simplifier_rule_verifier/CMakeLists.txt +++ b/apps/simplifier_rule_verifier/CMakeLists.txt @@ -105,6 +105,18 @@ set_tests_properties( 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 diff --git a/apps/simplifier_rule_verifier/Makefile b/apps/simplifier_rule_verifier/Makefile index d75d83ea18cc..3f5337022db9 100644 --- a/apps/simplifier_rule_verifier/Makefile +++ b/apps/simplifier_rule_verifier/Makefile @@ -26,6 +26,7 @@ test: $(BIN)/filter_rewrite_rules $(BIN)/super_simplify $(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/parser.cpp b/apps/simplifier_rule_verifier/parser.cpp index 6ee0b28a2231..4e7ed50cd165 100644 --- a/apps/simplifier_rule_verifier/parser.cpp +++ b/apps/simplifier_rule_verifier/parser.cpp @@ -2,6 +2,7 @@ #include "debug.h" +#include #include #include #include @@ -89,6 +90,15 @@ Expr consume_float(const char **cursor, const char *end) { } } double d = integer_part + double(fractional_part) / denom; + // An exponent, as in 1.000000e-16f + if (consume(cursor, end, "e") || consume(cursor, end, "E")) { + bool exponent_negative = consume(cursor, end, "-"); + if (!exponent_negative) { + consume(cursor, end, "+"); + } + int64_t exponent = consume_int(cursor, end); + d *= std::pow(10.0, (double)(exponent_negative ? -exponent : exponent)); + } if (negative) { d = -d; } 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 From 97dc27aab62a49da2ad1abeac7d27a1732734293 Mon Sep 17 00:00:00 2001 From: Andrew Adams Date: Fri, 14 Aug 2026 17:48:57 -0700 Subject: [PATCH 10/10] Decline unsupported wildcard types in super_simplify instead of aborting The CEGIS interpreter only represents Int(32) and Bool leaves, and asserted on anything else. Feeding it a corpus of Exprs collected from a real build, most of which mention uint32, uint64 or float variables, that assert killed the process rather than reporting that there was nothing to search. Check the leaf types up front and return an undefined Expr, which is what callers already expect when no equivalent is found. Co-Authored-By: Claude Opus 5 --- apps/simplifier_rule_verifier/super_simplify.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/apps/simplifier_rule_verifier/super_simplify.cpp b/apps/simplifier_rule_verifier/super_simplify.cpp index e9dd909f4baf..cb5c7d1d9c34 100644 --- a/apps/simplifier_rule_verifier/super_simplify.cpp +++ b/apps/simplifier_rule_verifier/super_simplify.cpp @@ -201,6 +201,18 @@ Expr super_simplify(Expr e, int size) { 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);