From 1314871a1ff07b5baf01f8171a54f8f7ebe68aff Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Fri, 3 Jul 2015 19:05:08 +0200 Subject: [PATCH] AST generation: remove redundant constraints before determining loop bounds The constraints that determine the part of the schedule space for which a (possibly degenerate) loop is generated are first checked to see if they assign a single value in isl_ast_build_set_loop_bounds. This function also keeps track of the subset of constraints that do not involve the loop iterator in the "pending" constraints such that they can be added in the guard on the loop after it has been generated. The other constraints are stored in the "generated" constraints. During the actual construction of the for loop, i.e., its initial value and its condition, the constraints not involving the loop iterator are ignored because they are handled by the pending constraints. However, the pending constraints are simplified with respect to the generated constraints (including the current constraints involving the loop iterator), while the redundant constraints in the complete set of constraints are also eliminated as a side effect of a gist operation. This means in particular that if there are two mutually redundant constraints, one involving the loop iterator and one not involving the loop iterator, that then _both_ constraints may end up getting eliminated. For example, for the newly added test case, the set of constraints at some loop level is [b0] -> { [[] -> [i0, i1, i2, i3]] : b0 <= 2 and i2 <= 2 and i2 >= 1 and i2 >= -1 + 2i1 and i2 >= 1 - 2i1 and i2 >= 8 - 8b0 and i1 >= 1 - 4i0 and i0 <= 2 and b0 >= 1 and i1 <= 1 } The constraint "b0 >= 1" gets eliminated with respect to the generated constraints (which includes "i2 >= 8 - 8b0"), while the "i2 >= 8 - 8b0" constraint gets eliminated from the above set when redundant constraints are removed. Perform the removal of redundant constraints before the constraints are split up into pending and generated constraints to avoid this situation. Reported-by: Tobias Grosser Signed-off-by: Sven Verdoolaege --- isl_ast_codegen.c | 1 + test_inputs/codegen/omega/lefur04-0.c | 2 +- test_inputs/codegen/redundant.c | 19 +++++++++++++++++++ test_inputs/codegen/redundant.st | 6 ++++++ 4 files changed, 27 insertions(+), 1 deletion(-) create mode 100644 test_inputs/codegen/redundant.c create mode 100644 test_inputs/codegen/redundant.st diff --git a/isl_ast_codegen.c b/isl_ast_codegen.c index fc8e2d7b..0316ea23 100644 --- a/isl_ast_codegen.c +++ b/isl_ast_codegen.c @@ -1449,6 +1449,7 @@ static __isl_give isl_ast_graft *create_node_scaled( depth = isl_ast_build_get_depth(build); sub_build = isl_ast_build_copy(build); + bounds = isl_basic_set_remove_redundancies(bounds); sub_build = isl_ast_build_set_loop_bounds(sub_build, isl_basic_set_copy(bounds)); degenerate = isl_ast_build_has_value(sub_build); diff --git a/test_inputs/codegen/omega/lefur04-0.c b/test_inputs/codegen/omega/lefur04-0.c index 124d0f15..72ecbe49 100644 --- a/test_inputs/codegen/omega/lefur04-0.c +++ b/test_inputs/codegen/omega/lefur04-0.c @@ -2,7 +2,7 @@ for (int c0 = 0; c0 <= 3; c0 += 1) for (int c1 = max(2 * c0 - 3, c0 / 2); c1 <= min(3, c0 + 1); c1 += 1) for (int c2 = c0; c2 <= min(min(3, 2 * c0 - c1 + 1), 3 * c1 + 2); c2 += 1) for (int c3 = max(max(max(c1 - (-c1 + 3) / 3, c0 - (-c2 + 3) / 3), c2 - (c2 + 2) / 3), c2 + floord(3 * c1 - c2 - 1, 6)); c3 <= min(3, c0 + c2 / 3 + 1); c3 += 1) - for (int c5 = max(max(max(max(0, 2 * c3 - 4), c1 - (-c1 + 3) / 3), c2 - (c2 + 3) / 3), c3 - (c3 + 3) / 3); c5 <= min(min(c1 + 1, c3), -c2 + 2 * c3 - (c2 + 3) / 3 + 2); c5 += 1) + for (int c5 = max(max(max(max(0, 2 * c3 - 4), c2 - (c2 + 3) / 3), c3 - (c3 + 3) / 3), c1 - (c1 - 2 * c3 + 5) / 5); c5 <= min(min(c1 + 1, c3), -c2 + 2 * c3 - (c2 + 3) / 3 + 2); c5 += 1) for (int c6 = max(max(max(max(max(-200 * c1 + 400 * c3 - 199, 250 * c3 + 1), 1000 * c0 - 500 * c5 - 501), 667 * c0 - 333 * c1 - (c0 + c1 + 3) / 3 - 332), 333 * c1 + c1 / 3), 333 * c2 + (c2 + 1) / 3); c6 <= min(min(min(min(min(min(1000, 500 * c0 + 499), -200 * c1 + 400 * c3 + 400), 500 * c5 + 501), 1000 * c0 - 500 * c5 + 997), 333 * c2 - (-c2 + 3) / 3 + 333), 333 * c3 - (-c3 + 3) / 3 + 334); c6 += 1) for (int c7 = max(max(max(max(500 * c5 + 2, c6), 1000 * c0 - c6), 1000 * c3 - 2 * c6 + 2), 500 * c1 + (c6 + 1) / 2); c7 <= min(min(min(min(500 * c5 + 501, 2 * c6 + 1), 1000 * c0 - c6 + 999), 1000 * c3 - 2 * c6 + 1001), 500 * c1 + (c6 + 1) / 2 + 499); c7 += 1) s0(c0, c1, c2, c3, c2 / 3, c5, c6, c7); diff --git a/test_inputs/codegen/redundant.c b/test_inputs/codegen/redundant.c new file mode 100644 index 00000000..6ac7d2dd --- /dev/null +++ b/test_inputs/codegen/redundant.c @@ -0,0 +1,19 @@ +for (int c0 = 0; c0 <= 2; c0 += 1) + for (int c1 = max(0, -2 * c0 + b0 / 2); c1 <= 1; c1 += 1) { + if (b0 >= 1 && 4 * c0 + c1 >= 1) + for (int c2 = 1; c2 <= 2; c2 += 1) { + if (c2 == 2) { + for (int c3 = 1; c3 <= 14; c3 += 1) + write(c0, c1, 8 * b0 - 3, c3); + } else if (c1 == 1) { + for (int c3 = 1; c3 <= 14; c3 += 1) + write(c0, 1, 8 * b0 - 4, c3); + } else + for (int c3 = 1; c3 <= 14; c3 += 1) + write(c0, 0, 8 * b0 - 4, c3); + } + for (int c2 = max(max(3, -8 * b0 + 6), 8 * c0 - 12); c2 <= min(min(7, -8 * b0 + 17), 8 * c0 + 6); c2 += 1) + if (c1 >= -2 * ((8 * c0 - 2 * c1 - c2 + 8) / 4) + 1 && -2 * ((8 * c0 - 2 * c1 - c2 + 8) / 4) + 9 >= c1 && (8 * c0 - 2 * c1 - c2 + 8) % 4 <= 2 && ((8 * c0 - 2 * c1 - c2 + 8) % 4) + 2 * c2 <= 14) + for (int c3 = 1; c3 <= 14; c3 += 1) + write(c0, c1, 8 * b0 + c2 - 5, c3); + } diff --git a/test_inputs/codegen/redundant.st b/test_inputs/codegen/redundant.st new file mode 100644 index 00000000..e766f740 --- /dev/null +++ b/test_inputs/codegen/redundant.st @@ -0,0 +1,6 @@ +# Check that b1 >= 1 is not dropped by mistake in 4 * c0 + c1 >= 1 part +domain: "[b0] -> { write[i0, o1, o2, o3] : ((exists (e0 = floor((4 + o2)/8), e1 = floor((5 + o2)/8), e2 = floor((4 + o2)/262144), e3, e4: o1 <= 1 and o1 >= 0 and o2 <= 12 and o2 >= 1 and o3 <= 14 and o3 >= 1 and 8e0 <= 4 + o2 and 8e1 <= 5 + o2 and 262144e2 <= 4 - 8b0 + o2 and 262144e2 >= -262139 + o2 and 262144e2 <= 4 + o2 and 262144e2 >= -3 - 8b0 + o2 and 4e4 <= 1 - 8i0 + 2o1 - o2 + 8e0 and 4e4 <= 4 - 8i0 + 2o1 + o2 - 8e0 and 4e4 >= 2o1 + o2 - 8e1 - 8e3 and 4e4 >= -3 + 2o1 + o2 - 8e0 - 8e3 and 4e4 >= -6 + 2o1 - o2 + 8e0 - 8e3 and 2e4 >= -9 + o1 and 2e4 <= -1 + o1 and 4e4 <= -6 + 2o1 - o2 + 8e1 - 8e3 and 4e4 >= -3 - 8i0 + 2o1 + o2 - 8e0 and 4e4 >= -6 - 8i0 + 2o1 - o2 + 8e0)) or (exists (e0 = floor((4 + o2)/8), e1 = floor((5 + o2)/8), e2 = floor((4 + o2)/262144), e3, e4: o1 <= 1 and o1 >= 0 and o2 <= 12 and o2 >= 1 and o3 <= 14 and o3 >= 1 and 8e0 <= 4 + o2 and 8e1 >= -2 + o2 and 262144e2 <= 4 - 8b0 + o2 and 262144e2 >= -262139 + o2 and 262144e2 <= 4 + o2 and 262144e2 >= -3 - 8b0 + o2 and 4e4 <= 1 - 8i0 + 2o1 - o2 + 8e0 and 4e4 <= 4 - 8i0 + 2o1 + o2 - 8e0 and 4e4 >= -3 + 2o1 + o2 - 8e0 - 8e3 and 4e4 >= -6 + 2o1 - o2 + 8e0 - 8e3 and 2e4 >= -9 + o1 and 2e4 <= -1 + o1 and 4e4 <= 1 + 2o1 - o2 + 8e0 - 8e3 and 4e4 <= 4 + 2o1 + o2 - 8e0 - 8e3 and 4e4 <= -1 + 2o1 + o2 - 8e1 - 8e3 and 4e4 >= -3 - 8i0 + 2o1 + o2 - 8e0 and 4e4 >= -6 - 8i0 + 2o1 - o2 + 8e0)) or (exists (e0 = floor((2 + o2)/8), e1 = floor((4 + o2)/8), e2 = floor((4 + o2)/262144), e3, e4: o1 <= 1 and o1 >= 0 and o2 <= 13 and o2 >= 3 and o3 <= 14 and o3 >= 1 and 8e0 >= -5 + o2 and 8e1 <= 4 + o2 and 262144e2 <= 4 - 8b0 + o2 and 262144e2 >= -262139 + o2 and 262144e2 <= 4 + o2 and 262144e2 >= -3 - 8b0 + o2 and 4e4 <= 1 - 8i0 + 2o1 - o2 + 8e1 and 4e4 <= 4 - 8i0 + 2o1 + o2 - 8e1 and 4e4 >= -3 + 2o1 + o2 - 8e1 - 8e3 and 4e4 >= -6 + 2o1 - o2 + 8e1 - 8e3 and 2e4 >= -9 + o1 and 2e4 <= -1 + o1 and 4e4 <= 1 + 2o1 - o2 + 8e1 - 8e3 and 4e4 <= -4 + 2o1 + o2 - 8e0 - 8e3 and 4e4 <= 4 + 2o1 + o2 - 8e1 - 8e3 and 4e4 >= -3 - 8i0 + 2o1 + o2 - 8e1 and 4e4 >= -6 - 8i0 + 2o1 - o2 + 8e1))) and b0 >= 0 and i0 <= 2 and i0 >= 0 and b0 <= 2 }" +child: + context: "[b0] -> { [] : b0 <= 2 and b0 >= 0 }" + child: + schedule: "[b0] -> [{ write[i0, o1, o2, o3] -> [i0] }, { write[i0, i1, i2, i3] -> [(i1)] }, { write[i0, i1, i2, i3] -> [(5 - 8b0 + i2)] }, { write[i0,i1, i2, i3] -> [(i3)] }]" -- 2.11.4.GIT