From 9cba0a91f795bc858ab3482ba674a2d293157d8d Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Sun, 21 Jun 2015 14:19:20 +0200 Subject: [PATCH] isl_basic_map_gist: do not introduce context divs in input The divs of the input and the context are currently aligned, which introduces the context divs in the input. This may seem harmless because there should not be any constraints involving those context divs in the result such that those divs will get eliminated again, but this only happens after the div constraints have been added and they may get simplified in between. This may lead to spurious constraints in the output that may even involve variables that did not appear in the input. Do not add the context divs to the input, but add completely unconstrained dimensions instead. Signed-off-by: Sven Verdoolaege --- isl_map_simplify.c | 12 ++++++++---- isl_test.c | 18 ++++++++++++++++++ test_inputs/codegen/roman.c | 2 +- test_inputs/codegen/separate2.c | 2 +- 4 files changed, 28 insertions(+), 6 deletions(-) diff --git a/isl_map_simplify.c b/isl_map_simplify.c index 83b9a16f..0e749073 100644 --- a/isl_map_simplify.c +++ b/isl_map_simplify.c @@ -2725,7 +2725,7 @@ struct isl_basic_map *isl_basic_map_gist(struct isl_basic_map *bmap, { isl_basic_set *bset, *eq; isl_basic_map *eq_bmap; - unsigned n_div, n_eq, n_ineq; + unsigned total, n_div, extra, n_eq, n_ineq; if (!bmap || !context) goto error; @@ -2751,11 +2751,15 @@ struct isl_basic_map *isl_basic_map_gist(struct isl_basic_map *bmap, goto error; context = isl_basic_map_align_divs(context, bmap); - bmap = isl_basic_map_align_divs(bmap, context); - n_div = isl_basic_map_dim(bmap, isl_dim_div); + n_div = isl_basic_map_dim(context, isl_dim_div); + total = isl_basic_map_dim(bmap, isl_dim_all); + extra = n_div - isl_basic_map_dim(bmap, isl_dim_div); - bset = uset_gist(isl_basic_map_underlying_set(isl_basic_map_copy(bmap)), + bset = isl_basic_map_underlying_set(isl_basic_map_copy(bmap)); + bset = isl_basic_set_add_dims(bset, isl_dim_set, extra); + bset = uset_gist(bset, isl_basic_map_underlying_set(isl_basic_map_copy(context))); + bset = isl_basic_set_project_out(bset, isl_dim_set, total, extra); if (!bset || bset->n_eq == 0 || n_div == 0 || isl_basic_set_plain_is_empty(bset)) { diff --git a/isl_test.c b/isl_test.c index f7e6791d..abd0cc13 100644 --- a/isl_test.c +++ b/isl_test.c @@ -1291,6 +1291,24 @@ struct { "[t1] -> { [i4, i6] : exists (e0 = floor((1530 - 4t1 - 5i4)/20): " "i4 <= 1 and 5e0 <= 381 - t1 and 20e0 <= 1530 - 4t1 - 5i4 and " "20e0 >= 1511 - 4t1 - 5i4) }" }, + /* Check that no constraints on i6 are introduced in the gist */ + { "[t1, t2] -> { [i4, i5, i6] : exists (e0 = floor((1 + i4)/2), " + "e1 = floor((1530 - 4t1 - 5i4)/20), " + "e2 = floor((-4t1 - 5i4 + 10*floor((1 + i4)/2))/20), " + "e3 = floor((-1 + i4)/2): t2 = 0 and 2e3 = -1 + i4 and " + "20e2 >= -19 - 4t1 - 5i4 + 10e0 and 5e2 <= 1 - t1 and " + "2e0 <= 1 + i4 and 2e0 >= i4 and " + "20e1 <= 1530 - 4t1 - 5i4 and " + "20e1 >= 1511 - 4t1 - 5i4 and i4 <= 1 and " + "5e1 <= 381 - t1 and 20e2 <= -4t1 - 5i4 + 10e0) }", + "[t1, t2] -> { [i4, i5, i6] : exists (e0 = floor((-17 + i4)/2), " + "e1 = floor((-t1 + i6)/5): 5e1 = -t1 + i6 and " + "2e0 <= -17 + i4 and 2e0 >= -18 + i4 and " + "10e0 <= -91 + 5i4 + 4i6 and " + "10e0 >= -105 + 5i4 + 4i6) }", + "[t1, t2] -> { [i4, i5, i6] : exists (e0 = floor((381 - t1)/5), " + "e1 = floor((-1 + i4)/2): t2 = 0 and 2e1 = -1 + i4 and " + "i4 <= 1 and 5e0 <= 381 - t1 and 20e0 >= 1511 - 4t1 - 5i4) }" }, }; static int test_gist(struct isl_ctx *ctx) diff --git a/test_inputs/codegen/roman.c b/test_inputs/codegen/roman.c index 1dd43c52..d7e4077e 100644 --- a/test_inputs/codegen/roman.c +++ b/test_inputs/codegen/roman.c @@ -17,7 +17,7 @@ S_24(c1, c3); S_19(c1, c3); } - if (np1 >= i && i + c1 <= 21) { + if (i + c1 <= 21) { S_15(c1, i + c1 - 2); for (int c5 = 0; c5 < i + c1 - 2; c5 += 1) { S_16(c1, i + c1 - 2, c5); diff --git a/test_inputs/codegen/separate2.c b/test_inputs/codegen/separate2.c index 0fba4f1f..469c894a 100644 --- a/test_inputs/codegen/separate2.c +++ b/test_inputs/codegen/separate2.c @@ -4,6 +4,6 @@ if ((length - 1) % 16 <= 14) for (int c6 = max(0, 2 * ((length - 1) % 16) + 2 * c5 - 60); c6 <= 30; c6 += 1) { if (2 * length + c6 >= 2 * ((length - 1) % 16) + 4 && 2 * ((length - 1) % 16) >= c6 && 2 * ((length - 1) % 16) + 2 * c5 >= c6 && c6 + 62 >= 2 * ((length - 1) % 16) + 2 * c5 && 2 * ((length - 1) % 16) + 2 * c5 == 2 * ((length - 1) % 32) + c6 && (2 * c5 - c6) % 32 == 0) S_3(c0, 0, (c6 / 2) - ((length - 1) % 16) + length - 1); - if (length <= 16 && length >= c5 + 1 && c6 >= 1 && length >= c6) + if (length <= 15 && length >= c5 + 1 && c6 >= 1 && length >= c6) S_0(c0, c5, c6 - 1); } -- 2.11.4.GIT