additional bugfixes and tests

Author: stevenraphael

src/Function.cpp

@@ -659,10 +659,6 @@ void Function::define(const vector<string> &args, vector<Expr> values) {
     for (auto &value : values) {
         value = weakener(value);
     }
-    if (check.reduction_domain.defined()) {
-        check.reduction_domain.set_predicate(
-            weakener(check.reduction_domain.predicate()));
-    }
 
     ReductionDomain rdom;
     contents->init_def = Definition(init_def_args, values, rdom, true);
@@ -1109,63 +1105,24 @@ bool Function::has_pure_definition() const {
 }
 
 bool Function::is_inductive() const {
-    class RecursiveHelper : public IRVisitor {
-        using IRVisitor::visit;
-        const string &func;
-        void visit(const Call *op) override {
-            if (op->name == func) {
-                recursive = true;
-            }
-            IRVisitor::visit(op);
-        }
-
-    public:
-        bool recursive = false;
-        RecursiveHelper(const string &func)
-            : func(func) {
-        }
-    };
-
     if (!has_pure_definition()) {
         return false;
     }
 
-    RecursiveHelper r(name());
+    bool recursive = false;
     for (const Expr &e : definition().values()) {
-        e.accept(&r);
+        visit_with(e, [&](auto *self, const Call *op) {
+            if (op->name == name()) {
+                recursive = true;
+            }
+            self->visit_base(op);
+        });
     }
 
-    return r.recursive;
+    return recursive;
 }
 
 bool Function::is_inductive(const string &var) const {
-    class RecursiveHelper : public IRVisitor {
-        using IRVisitor::visit;
-        const string &func;
-        const string &var;
-        const int &pos;
-        void visit(const Call *op) override {
-            if (op->name == func) {
-                recursive = true;
-                if (const auto &v = op->args[pos].as<Variable>()) {
-                    if (v->name != var) {
-                        inductive_in_var = true;
-                    }
-                } else {
-                    inductive_in_var = true;
-                }
-            }
-            IRVisitor::visit(op);
-        }
-
-    public:
-        bool recursive = false;
-        bool inductive_in_var = false;
-        RecursiveHelper(const string &func, const string &var, const int &pos)
-            : func(func), var(var), pos(pos) {
-        }
-    };
-
     if (!has_pure_definition()) {
         return false;
     }
@@ -1178,15 +1135,30 @@ bool Function::is_inductive(const string &var) const {
             }
         }
     }
+
     if (pos == -1) {
         return false;
     }
-    RecursiveHelper r(name(), var, pos);
+
+    bool recursive = false;
+    bool inductive_in_var = false;
     for (const Expr &e : definition().values()) {
-        e.accept(&r);
+        visit_with(e, [&](auto *self, const Call *op) {
+            if (op->name == name()) {
+                recursive = true;
+                if (const auto &v = op->args[pos].as<Variable>()) {
+                    if (v->name != var) {
+                        inductive_in_var = true;
+                    }
+                } else {
+                    inductive_in_var = true;
+                }
+            }
+            self->visit_base(op);
+        });
     }
 
-    return r.inductive_in_var;
+    return inductive_in_var;
 }
 
 bool Function::can_be_inlined() const {

src/Inductive.cpp

@@ -16,6 +16,8 @@ namespace Internal {
 using std::string;
 using std::vector;
 
+namespace {
+
 class BaseCaseSolver : public IRVisitor {
     using IRVisitor::visit;
     const vector<string> &vars;
@@ -31,16 +33,24 @@ class BaseCaseSolver : public IRVisitor {
 
     void visit(const Call *op) override {
         if (op->is_intrinsic(Call::if_then_else)) {
+            if (nested_select == 0) {
+                visit_with(op->args[0], [&](auto *self, const Call *inner_op) {
+                    user_assert(inner_op->name != func) << "Function " << func << " contains an inductive function reference outside of a select operation value.\n";
+                    self->visit_base(inner_op);
+                });
+            }
+
             nested_select += 1;
             vector<Interval> old_intervals = condition_intervals;
             for (size_t i = 0; i < vars.size(); i++) {
-                condition_intervals[i] = Interval::make_intersection(old_intervals[i], solve_for_outer_interval(simplify(op->args[0]), vars[i]));
+                Interval inter = Interval::make_intersection(old_intervals[i], solve_for_outer_interval(simplify(op->args[0]), vars[i]));
+                condition_intervals[i] = Interval(inter.min, Interval::pos_inf());
                 bounds.push(vars[i], condition_intervals[i]);
             }
-
             op->args[1].accept(this);
             for (size_t i = 0; i < vars.size(); i++) {
-                condition_intervals[i] = Interval::make_intersection(old_intervals[i], solve_for_outer_interval(simplify(!op->args[0]), vars[i]));
+                Interval inter = Interval::make_intersection(old_intervals[i], solve_for_outer_interval(simplify(!op->args[0]), vars[i]));
+                condition_intervals[i] = Interval(inter.min, Interval::pos_inf());
                 bounds.pop(vars[i]);
                 bounds.push(vars[i], condition_intervals[i]);
             }
@@ -51,7 +61,7 @@ class BaseCaseSolver : public IRVisitor {
             }
             nested_select -= 1;
         } else if (op->name == func) {
-            user_assert(nested_select > 0) << "Function " << func << " contains an inductive function reference outside of a select operation.\n";
+            user_assert(nested_select > 0) << "Function " << func << " contains an inductive function reference outside of a select operation value.\n";
             user_assert(nested_select == 1) << "Function " << func << " contains an inductive function reference inside a nested select operation.\n";
             bool found_inductive = false;
             for (size_t position = 0; position < vars.size(); position++) {
@@ -67,7 +77,9 @@ class BaseCaseSolver : public IRVisitor {
                     found_inductive = true;
                     new_interval = Interval(Interval::neg_inf(), start_box[position].max);
                 } else {
-                    new_interval = Interval::everything();
+                    std::ostringstream err;
+                    err << "Inductive variable " << vars[position] << " in inductive function " << func << " is not provably monotonically decreasing outside of the base case.";
+                    user_error << err.str() << "\n";
                 }
                 new_interval = Interval::make_intersection(new_interval, condition_intervals[position]);
                 Scope<Interval> i_scope;
@@ -93,7 +105,7 @@ class BaseCaseSolver : public IRVisitor {
     }
 };
 
-// anonymous namespace
+}  // anonymous namespace
 
 Box expand_to_include_base_case(const vector<string> &vars, const Expr &RHS, const string &func, const Box &box_required) {
     Expr substed = substitute_in_all_lets(RHS);
@@ -109,18 +121,5 @@ Box expand_to_include_base_case(const vector<string> &vars, const Expr &RHS, con
     return box2;
 }
 
-Box expand_to_include_base_case(const Function &fn, const Box &box_required, const int &pos) {
-    return expand_to_include_base_case(fn.args(), fn.values()[pos], fn.name(), box_required);
-}
-
-Box expand_to_include_base_case(const Function &fn, const Box &box_required) {
-    Box b = expand_to_include_base_case(fn.args(), fn.values()[0], fn.name(), box_required);
-    for (size_t pos = 1; pos < fn.values().size(); pos++) {
-        Box b2 = expand_to_include_base_case(fn.args(), fn.values()[pos], fn.name(), box_required);
-        merge_boxes(b, b2);
-    }
-    return b;
-}
-
 }  // namespace Internal
 }  // namespace Halide

src/Inductive.h

@@ -50,8 +50,6 @@ namespace Internal {
 /** Given an initial box for an inductively defined function,
     returns an expanded box that includes the function's non-inductive base case. */
 Box expand_to_include_base_case(const std::vector<std::string> &vars, const Expr &RHS, const std::string &func, const Box &box_required);
-Box expand_to_include_base_case(const Function &fn, const Box &box_required, const int &pos = 0);
-Box expand_to_include_base_case(const Function &fn, const Box &box_required);
 
 }  // namespace Internal
 }  // namespace Halide

test/error/CMakeLists.txt

@@ -74,7 +74,10 @@ tests(
     implicit_args.cpp
     impossible_constraints.cpp
     incomplete_target.cpp
-    inductive_loop.cpp
+    inductive_2d_arbitrary.cpp
+    inductive_cond_nested.cpp
+    inductive_cond_self_reference.cpp
+    inductive_loop_1.cpp
     inductive_loop_2.cpp
     inductive_loop_3.cpp
     inductive_nested_select.cpp

test/error/inductive_2d_arbitrary.cpp

@@ -0,0 +1,18 @@
+#include "Halide.h"
+#include <stdio.h>
+
+using namespace Halide;
+
+int main(int argc, char **argv) {
+    Func f("f"), g("g");
+
+    Var x("x"), y("y");
+
+    f(x, y) = select(x < 2 || y < 2 || y > 6, 0, f(x - 1, y + 1)) + select(x < 2 || x > 6 || y < 2, 0, f(x + 1, y - 1));
+    g(x, y) = f(x, y) * 2;
+
+    g.realize({10, 10});
+
+    printf("Success!\n");
+    return 0;
+}

test/error/inductive_cond_nested.cpp

@@ -0,0 +1,18 @@
+#include "Halide.h"
+#include <stdio.h>
+
+using namespace Halide;
+
+int main(int argc, char **argv) {
+    Func f("f"), g("g");
+
+    Var x("x");
+
+    f(x) = select(x < max(2, abs(select(x < 0, f(x - 1), 5))), 0, f(x - 1) + x);
+    g(x) = f(x) * 2;
+
+    g.realize({10});
+
+    printf("Success!\n");
+    return 0;
+}

test/error/inductive_cond_self_reference.cpp

@@ -0,0 +1,18 @@
+#include "Halide.h"
+#include <stdio.h>
+
+using namespace Halide;
+
+int main(int argc, char **argv) {
+    Func f("f"), g("g");
+
+    Var x("x");
+
+    f(x) = select(x < f(x - 1), 0, f(x - 1) + x);
+    g(x) = f(x) * 2;
+
+    g.realize({10});
+
+    printf("Success!\n");
+    return 0;
+}