From 410f2f63218a98ee44e7c179b69308a3d0b3fca8 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Mon, 31 Oct 2016 16:06:14 +0100 Subject: [PATCH] pet_scop_from_pet_tree: take into account assumptions The assumptions provided by the user in __pencil_assume/__builtin_assume statements are collected in the context, but they were not otherwise exploited. Exploit them during the extraction process as well. In particular, use the assumptions to simplify expressions. This simplification can in some cases eliminate some redundant pieces and therefore also speed up the extraction process. Tested-by: Samuel Thibault Signed-off-by: Sven Verdoolaege --- tests/assume.scop | 2 +- tests/assume3.c | 9 +++++++ tests/assume3.scop | 43 +++++++++++++++++++++++++++++++++ tests/assume4.c | 11 +++++++++ tests/assume4.scop | 44 ++++++++++++++++++++++++++++++++++ tests/assume5.c | 10 ++++++++ tests/assume5.scop | 70 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ tree2scop.c | 39 ++++++++++++++++++++++++++++++ 8 files changed, 227 insertions(+), 1 deletion(-) create mode 100644 tests/assume3.c create mode 100644 tests/assume3.scop create mode 100644 tests/assume4.c create mode 100644 tests/assume4.scop create mode 100644 tests/assume5.c create mode 100644 tests/assume5.scop diff --git a/tests/assume.scop b/tests/assume.scop index 5658526..b25f21f 100644 --- a/tests/assume.scop +++ b/tests/assume.scop @@ -5,7 +5,7 @@ context: '[S, n, m] -> { : 0 <= S <= 2147483647 and n >= -2147483648 and n < m 2147483648 - n and m <= 2147483647 }' schedule: '{ domain: "[S, n, m] -> { S_0[]; S_1[i] : 0 <= i < n }", child: { sequence: [ { filter: "[n] -> { S_0[] }" }, { filter: "[n] -> { S_1[i] }", child: { schedule: - "[n] -> L_0[{ S_1[i] -> [(i)] }]" } } ] } }' + "[m, n] -> L_0[{ S_1[i] -> [(i)] }]" } } ] } }' arrays: - context: '[S] -> { : S >= 0 }' extent: '[S, n, m] -> { D[i0] : 0 <= i0 < S }' diff --git a/tests/assume3.c b/tests/assume3.c new file mode 100644 index 0000000..b161e65 --- /dev/null +++ b/tests/assume3.c @@ -0,0 +1,9 @@ +int f(int k) +{ + int a; +#pragma scop + __pencil_assume(k >= 0); + a = k % 16; +#pragma endscop + return a; +} diff --git a/tests/assume3.scop b/tests/assume3.scop new file mode 100644 index 0000000..1d9e4d5 --- /dev/null +++ b/tests/assume3.scop @@ -0,0 +1,43 @@ +start: 23 +end: 91 +indent: "\t" +context: '[k] -> { : 0 <= k <= 2147483647 }' +schedule: '{ domain: "[k] -> { S_1[]; S_0[] }", child: { sequence: [ { filter: "[k] + -> { S_0[] }" }, { filter: "[k] -> { S_1[] }" } ] } }' +arrays: +- context: '{ : }' + extent: '[k] -> { a[] }' + element_type: int + element_size: 4 +statements: +- line: 5 + domain: '[k] -> { S_0[] }' + body: + type: expression + expr: + type: op + operation: assume + arguments: + - type: access + index: '[k] -> { S_0[] -> [(1)] }' + reference: __pet_ref_0 + read: 1 + write: 0 +- line: 6 + domain: '[k] -> { S_1[] }' + body: + type: expression + expr: + type: op + operation: = + arguments: + - type: access + index: '[k] -> { S_1[] -> a[] }' + reference: __pet_ref_1 + read: 0 + write: 1 + - type: access + index: '[k] -> { S_1[] -> [(k - 16*floor((k)/16))] }' + reference: __pet_ref_2 + read: 1 + write: 0 diff --git a/tests/assume4.c b/tests/assume4.c new file mode 100644 index 0000000..c6d3ba5 --- /dev/null +++ b/tests/assume4.c @@ -0,0 +1,11 @@ +int f(int k) +{ + int a[10]; +#pragma scop + for (int i = 0; i < 10; ++i) { + __pencil_assume(k >= 0); + a[i] = k % 16; + } +#pragma endscop + return a[0]; +} diff --git a/tests/assume4.scop b/tests/assume4.scop new file mode 100644 index 0000000..f8a6c81 --- /dev/null +++ b/tests/assume4.scop @@ -0,0 +1,44 @@ +start: 27 +end: 135 +indent: "\t" +context: '[k] -> { : 0 <= k <= 2147483647 }' +schedule: '{ domain: "[k] -> { S_1[i] : 0 <= i <= 9; S_0[i] : 0 <= i <= 9 }", child: + { schedule: "[k] -> L_0[{ S_1[i] -> [(i)]; S_0[i] -> [(i)] }]", child: { sequence: + [ { filter: "[k] -> { S_0[i] }" }, { filter: "[k] -> { S_1[i] }" } ] } } }' +arrays: +- context: '{ : }' + extent: '[k] -> { a[i0] : 0 <= i0 <= 9 }' + element_type: int + element_size: 4 +statements: +- line: 6 + domain: '[k] -> { S_0[i] : 0 <= i <= 9 }' + body: + type: expression + expr: + type: op + operation: assume + arguments: + - type: access + index: '[k] -> { S_0[i] -> [(1)] }' + reference: __pet_ref_0 + read: 1 + write: 0 +- line: 7 + domain: '[k] -> { S_1[i] : 0 <= i <= 9 }' + body: + type: expression + expr: + type: op + operation: = + arguments: + - type: access + index: '[k] -> { S_1[i] -> a[(i)] }' + reference: __pet_ref_1 + read: 0 + write: 1 + - type: access + index: '[k] -> { S_1[i] -> [(k - 16*floor((k)/16))] }' + reference: __pet_ref_2 + read: 1 + write: 0 diff --git a/tests/assume5.c b/tests/assume5.c new file mode 100644 index 0000000..fd126e3 --- /dev/null +++ b/tests/assume5.c @@ -0,0 +1,10 @@ +int f(int k) +{ + int a; +#pragma scop + __pencil_assume(k >= 0); + k = -1; + a = k % 16; +#pragma endscop + return a; +} diff --git a/tests/assume5.scop b/tests/assume5.scop new file mode 100644 index 0000000..bc4d994 --- /dev/null +++ b/tests/assume5.scop @@ -0,0 +1,70 @@ +start: 23 +end: 100 +indent: "\t" +context: '{ : }' +schedule: '{ domain: "{ S_0[]; S_2[]; S_1[] }", child: { sequence: [ { filter: "{ + S_0[] }" }, { filter: "{ S_1[] }" }, { filter: "{ S_2[] }" } ] } }' +arrays: +- context: '{ : }' + extent: '{ a[] }' + element_type: int + element_size: 4 +- context: '{ : }' + extent: '{ k[] }' + element_type: int + element_size: 4 +statements: +- line: 5 + domain: '{ S_0[] }' + body: + type: expression + expr: + type: op + operation: assume + arguments: + - type: op + operation: '>=' + arguments: + - type: access + index: '{ S_0[] -> k[] }' + reference: __pet_ref_0 + read: 1 + write: 0 + - type: int + value: 0 +- line: 6 + domain: '{ S_1[] }' + body: + type: expression + expr: + type: op + operation: = + arguments: + - type: access + index: '{ S_1[] -> k[] }' + reference: __pet_ref_1 + read: 0 + write: 1 + - type: op + operation: '-' + arguments: + - type: int + value: 1 +- line: 7 + domain: '{ S_2[] }' + body: + type: expression + expr: + type: op + operation: = + arguments: + - type: access + index: '{ S_2[] -> a[] }' + reference: __pet_ref_2 + read: 0 + write: 1 + - type: access + index: '{ S_2[] -> [(-1)] }' + reference: __pet_ref_3 + read: 1 + write: 0 diff --git a/tree2scop.c b/tree2scop.c index 23cdd3c..4d7d992 100644 --- a/tree2scop.c +++ b/tree2scop.c @@ -47,6 +47,42 @@ #include "state.h" #include "tree2scop.h" +/* If "stmt" is an affine assumption, then record the assumption in "pc". + */ +static __isl_give pet_context *add_affine_assumption(struct pet_stmt *stmt, + __isl_take pet_context *pc) +{ + isl_bool affine; + isl_set *cond; + + affine = pet_stmt_is_affine_assume(stmt); + if (affine < 0) + return pet_context_free(pc); + if (!affine) + return pc; + cond = pet_stmt_assume_get_affine_condition(stmt); + cond = isl_set_reset_tuple_id(cond); + pc = pet_context_intersect_domain(pc, cond); + return pc; +} + +/* Given a scop "scop" derived from an assumption statement, + * record the assumption in "pc", if it is affine. + * Note that "scop" should consist of exactly one statement. + */ +static __isl_give pet_context *scop_add_affine_assumption( + __isl_keep pet_scop *scop, __isl_take pet_context *pc) +{ + int i; + + if (!scop) + return pet_context_free(pc); + for (i = 0; i < scop->n_stmt; ++i) + pc = add_affine_assumption(scop->stmts[i], pc); + + return pc; +} + /* Update "pc" by taking into account the writes in "stmt". * That is, clear any previously assigned values to variables * that are written by "stmt". @@ -2419,6 +2455,7 @@ static struct pet_scop *mark_exposed(struct pet_scop *scop) * After extracting a statement, we update "pc" * based on the top-level assignments in the statement * so that we can exploit them in subsequent statements in the same block. + * Top-level affine assumptions are also recorded in the context. * * If there are any breaks or continues in the individual statements, * then we may have to compute a new skip condition. @@ -2465,6 +2502,8 @@ static struct pet_scop *scop_from_block(__isl_keep pet_tree *tree, if (pet_scop_has_affine_skip(scop, pet_skip_now)) pc = apply_affine_continue(pc, scop); scop_i = scop_from_tree(tree->u.b.child[i], pc, state); + if (pet_tree_is_assume(tree->u.b.child[i])) + pc = scop_add_affine_assumption(scop_i, pc); pc = scop_handle_writes(scop_i, pc); if (is_assignment(tree->u.b.child[i])) pc = handle_assignment(pc, tree->u.b.child[i]); -- 2.11.4.GIT