From 808cbfc9ac33d6d37d614c89fbdfe05ce1cc110b Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Mon, 4 Jul 2016 15:54:44 +0200 Subject: [PATCH] isl_tab_basic_map_partial_lexopt: improve detection of equal partial solutions The partial solution stack introduced in 4fff507 (isl_tab_pip: keep cache of partial solutions, Fri Oct 16 14:46:28 2009 +0200) allows identical partial solutions to be combined on their parent domain. There are however cases where the partial solutions are not identical but still equal to each other on one of the partial domains. In this case the solution on the other partial domain is valid for both partial domains and can also be used on the parent domain. The test for such equal solutions is a bit more expensive than the one that checks for identical solutions, but it should be easier to detect opportunities for combining partial solutions at this stage than it would be to detect them afterwards. By combining partial solutions in this way, the result of isl_pw_multi_aff_from_map can be improved in some cases, as, e.g., in the new AST generation test case, derived from a feature request by Tobias Grosser. Requested-by: Tobias Grosser Signed-off-by: Sven Verdoolaege --- isl_tab_pip.c | 76 ++++++++++++++++++++++++++++++++--- test_inputs/codegen/jacobi_kernel4.c | 2 + test_inputs/codegen/jacobi_kernel4.in | 4 ++ 3 files changed, 77 insertions(+), 5 deletions(-) create mode 100644 test_inputs/codegen/jacobi_kernel4.c create mode 100644 test_inputs/codegen/jacobi_kernel4.in diff --git a/isl_tab_pip.c b/isl_tab_pip.c index d7df7a50..cdc1b203 100644 --- a/isl_tab_pip.c +++ b/isl_tab_pip.c @@ -392,6 +392,26 @@ static isl_bool same_solution(struct isl_partial_sol *s1, return isl_multi_aff_plain_is_equal(s1->ma, s2->ma); } +/* Swap the initial two partial solutions in "sol". + * + * That is, go from + * + * sol->partial = p1; p1->next = p2; p2->next = p3 + * + * to + * + * sol->partial = p2; p2->next = p1; p1->next = p3 + */ +static void swap_initial(struct isl_sol *sol) +{ + struct isl_partial_sol *partial; + + partial = sol->partial; + sol->partial = partial->next; + partial->next = partial->next->next; + sol->partial->next = partial; +} + /* Combine the initial two partial solution of "sol" into * a partial solution with the current context domain of "sol" and * the function description of the second partial solution in the list. @@ -425,11 +445,45 @@ static isl_stat combine_initial_into_second(struct isl_sol *sol) return isl_stat_ok; } +/* Are "ma1" and "ma2" equal to each other on "dom"? + * + * Combine "ma1" and "ma2" with "dom" and check if the results are the same. + * "dom" may have existentially quantified variables. Eliminate them first + * as otherwise they would have to be eliminated twice, in a more complicated + * context. + */ +static isl_bool equal_on_domain(__isl_keep isl_multi_aff *ma1, + __isl_keep isl_multi_aff *ma2, __isl_keep isl_basic_set *dom) +{ + isl_set *set; + isl_pw_multi_aff *pma1, *pma2; + isl_bool equal; + + set = isl_basic_set_compute_divs(isl_basic_set_copy(dom)); + pma1 = isl_pw_multi_aff_alloc(isl_set_copy(set), + isl_multi_aff_copy(ma1)); + pma2 = isl_pw_multi_aff_alloc(set, isl_multi_aff_copy(ma2)); + equal = isl_pw_multi_aff_is_equal(pma1, pma2); + isl_pw_multi_aff_free(pma1); + isl_pw_multi_aff_free(pma2); + + return equal; +} + /* The initial two partial solutions of "sol" are known to be at * the same level. * If they represent the same solution (on different parts of the domain), * then combine them into a single solution at the current level. * Otherwise, pop them both. + * + * Even if the two partial solution are not obviously the same, + * one may still be a simplification of the other over its own domain. + * Also check if the two sets of affine functions are equal when + * restricted to one of the domains. If so, combine the two + * using the set of affine functions on the other domain. + * That is, for two partial solutions (D1,M1) and (D2,M2), + * if M1 = M2 on D1, then the pair of partial solutions can + * be replaced by (D1+D2,M2) and similarly when M1 = M2 on D2. */ static isl_stat combine_initial_if_equal(struct isl_sol *sol) { @@ -441,14 +495,26 @@ static isl_stat combine_initial_if_equal(struct isl_sol *sol) same = same_solution(partial, partial->next); if (same < 0) return isl_stat_error; - if (!same) { - sol_pop_one(sol); - sol_pop_one(sol); - } else { - if (combine_initial_into_second(sol) < 0) + if (same) + return combine_initial_into_second(sol); + if (partial->ma && partial->next->ma) { + same = equal_on_domain(partial->ma, partial->next->ma, + partial->dom); + if (same < 0) return isl_stat_error; + if (same) + return combine_initial_into_second(sol); + same = equal_on_domain(partial->ma, partial->next->ma, + partial->next->dom); + if (same) { + swap_initial(sol); + return combine_initial_into_second(sol); + } } + sol_pop_one(sol); + sol_pop_one(sol); + return isl_stat_ok; } diff --git a/test_inputs/codegen/jacobi_kernel4.c b/test_inputs/codegen/jacobi_kernel4.c new file mode 100644 index 00000000..97b45448 --- /dev/null +++ b/test_inputs/codegen/jacobi_kernel4.c @@ -0,0 +1,2 @@ +if (8 * a + 64 * b >= t0 + 2 * t + 512 * floord(-t0 - 8 * a + 64 * b + 2 * t - 1, 512) + 512 && t0 + 512 * floord(-t0 - 8 * a + 64 * b + 2 * t - 1, 512) >= -511 && t0 + 512 * floord(-t0 - 8 * a + 64 * b + 2 * t - 1, 512) <= 1310206) + S_0(t, -((-t0 - 8 * a + 64 * b + 2 * t + 511) % 512) - 8 * a + 64 * b + 2 * t + 511); diff --git a/test_inputs/codegen/jacobi_kernel4.in b/test_inputs/codegen/jacobi_kernel4.in new file mode 100644 index 00000000..9eadc1ba --- /dev/null +++ b/test_inputs/codegen/jacobi_kernel4.in @@ -0,0 +1,4 @@ +# Check that an affine value is extracted for the final dimension +[t0,a,b,t] -> { S_0[t, i] -> [i, t0] : exists (e0 = [(t0 - i)/512]: 512e0 = t0 - i and 64b >= 2t + i - 8a and 64b <= -2t + i + 8a and 4a <= 3 + t and 4a >= t and t >= 0 and t <= 1999 and i >= 1 and i <= 1310718 and a >= 0 and a <= 500 and 8b <= 163839 + a and b <= 20480 and 8b >= 1 - a and b >= 0 and 32b <= 655359 - t + 4a and 32b >= 1 + t - 4a and t0 >= 0 and t0 <= 511) } +[t0,a,b,t] -> { : t <= -1 + 4a + 32b and t >= 0 and t <= 4a and t >= -3 + 4a and t <= 1999 and t <= 655359 + 4a - 32b and t0 >= 0 and t0 <= 511 } +[t0] -> { } -- 2.11.4.GIT