From feaa3b372a3596fb99c65f2463e4d2d4e2dc2d8e Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Sun, 1 Jan 2012 23:19:31 +0100 Subject: [PATCH] handle non-affine conditions in while loops We also extend the meaning of an argument to an access expression to also allow non-single valued arguments. In these cases, the constraint on the filter values is assumed to hold for all accessed filter elements. We use this to make the body of the loop depend on the while condition evaluating to true for all iterations of the loop up to and including the current iteration. The statement that computes the while condition is created in such a way that it depends on the condition evaluating to true for all previous iterations. Signed-off-by: Sven Verdoolaege --- include/pet.h | 5 +++ scan.cc | 87 ++++++++++++++++++++++++++++++++++++++++++++-- tests/while.c | 19 ++++++++++ tests/while.scop | 88 +++++++++++++++++++++++++++++++++++++++++++++++ tests/while_overflow.c | 17 +++++++++ tests/while_overflow.scop | 74 +++++++++++++++++++++++++++++++++++++++ 6 files changed, 287 insertions(+), 3 deletions(-) create mode 100644 tests/while.c create mode 100644 tests/while.scop create mode 100644 tests/while_overflow.c create mode 100644 tests/while_overflow.scop diff --git a/include/pet.h b/include/pet.h index 61ce355..b88d84e 100644 --- a/include/pet.h +++ b/include/pet.h @@ -114,6 +114,11 @@ struct pet_expr { * to the values of the arguments for which this statement * is executed. * Otherwise, it is simply the iteration domain. + * + * If one of the arguments is an access expression that accesses + * more than one element for a given iteration, then the constraints + * on the value of this argument (encoded in "domain") should be satisfied + * for all of those accessed elements. */ struct pet_stmt { int line; diff --git a/scan.cc b/scan.cc index 62fb242..d7f46cd 100644 --- a/scan.cc +++ b/scan.cc @@ -2035,18 +2035,79 @@ struct pet_scop *PetScan::extract_affine_while(__isl_take isl_pw_aff *pa, return scop; } +/* Construct a scop for a while, given the scops for the condition + * and the body, the filter access and the iteration domain of + * the while loop. + * + * In particular, the scop for the condition is filtered to depend + * on "test_access" evaluating to true for all previous iterations + * of the loop, while the scop for the body is filtered to depend + * on "test_access" evaluating to true for all iterations up to the + * current iteration. + * + * These filtered scops are then combined into a single scop. + * + * "sign" is positive if the iterator increases and negative + * if it decreases. + */ +static struct pet_scop *scop_add_while(struct pet_scop *scop_cond, + struct pet_scop *scop_body, __isl_take isl_map *test_access, + __isl_take isl_set *domain, int sign) +{ + isl_ctx *ctx = isl_set_get_ctx(domain); + isl_id *id_test; + isl_map *prev; + + id_test = isl_map_get_tuple_id(test_access, isl_dim_out); + test_access = isl_map_add_dims(test_access, isl_dim_in, 1); + test_access = isl_map_add_dims(test_access, isl_dim_out, 1); + test_access = isl_map_intersect_range(test_access, domain); + test_access = isl_map_set_tuple_id(test_access, isl_dim_out, id_test); + if (sign > 0) + prev = isl_map_lex_ge_first(isl_map_get_space(test_access), 1); + else + prev = isl_map_lex_le_first(isl_map_get_space(test_access), 1); + test_access = isl_map_intersect(test_access, prev); + scop_body = pet_scop_filter(scop_body, isl_map_copy(test_access), 1); + if (sign > 0) + prev = isl_map_lex_gt_first(isl_map_get_space(test_access), 1); + else + prev = isl_map_lex_lt_first(isl_map_get_space(test_access), 1); + test_access = isl_map_intersect(test_access, prev); + scop_cond = pet_scop_filter(scop_cond, test_access, 1); + + return pet_scop_add(ctx, scop_cond, scop_body); +} + /* Check if the while loop is of the form * * while (affine expression) * body * * If so, call extract_affine_while to construct a scop. - * Otherwise, fail. + * + * Otherwise, construct a generic while scop, with iteration domain + * { [t] : t >= 0 }. The scop consists of two parts, one for + * evaluating the condition and one for the body. + * The schedule is adjusted to reflect that the condition is evaluated + * before the body is executed and the body is filtered to depend + * on the result of the condition evaluating to true on all iterations + * up to the current iteration, while the evaluation the condition itself + * is filtered to depend on the result of the condition evaluating to true + * on all previous iterations. + * The context of the scop representing the body is dropped + * because we don't know how many times the body will be executed, + * if at all. */ struct pet_scop *PetScan::extract(WhileStmt *stmt) { Expr *cond; + isl_id *id; + isl_map *test_access; + isl_set *domain; + isl_map *sched; isl_pw_aff *pa; + struct pet_scop *scop, *scop_body; cond = stmt->getCond(); if (!cond) { @@ -2058,9 +2119,29 @@ struct pet_scop *PetScan::extract(WhileStmt *stmt) if (pa) return extract_affine_while(pa, stmt->getBody()); - unsupported(stmt); - return NULL; + if (!allow_nested) { + unsupported(stmt); + return NULL; + } + + id = isl_id_alloc(ctx, "t", NULL); + domain = infinite_domain(isl_id_copy(id)); + sched = identity_map(domain); + + test_access = create_test_access(ctx, n_test++); + scop = extract_non_affine_condition(cond, isl_map_copy(test_access)); + scop = scop_add_array(scop, test_access, ast_context); + scop = pet_scop_prefix(scop, 0); + scop = pet_scop_embed(scop, isl_set_copy(domain), isl_map_copy(sched), + isl_id_copy(id)); + scop_body = extract(stmt->getBody()); + scop_body = pet_scop_reset_context(scop_body); + scop_body = pet_scop_prefix(scop_body, 1); + scop_body = pet_scop_embed(scop_body, isl_set_copy(domain), sched, id); + scop = scop_add_while(scop, scop_body, test_access, domain, 1); + + return scop; } /* Check whether "cond" expresses a simple loop bound diff --git a/tests/while.c b/tests/while.c new file mode 100644 index 0000000..1508d65 --- /dev/null +++ b/tests/while.c @@ -0,0 +1,19 @@ +int f(void); +int P(int, int); +int g(int); +void h(int); + +void foo(int n) +{ + int s; + +#pragma scop + for (int x = 0; x < n; ++x) { +S1: s = f(); + while (P(x, s)) { +S2: s = g(s); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/while.scop b/tests/while.scop new file mode 100644 index 0000000..9455dfc --- /dev/null +++ b/tests/while.scop @@ -0,0 +1,88 @@ +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x, t] : x >= 0 and x <= -1 + n and t >= 0 }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '[n] -> { s[] }' + element_type: int + element_size: 4 +statements: +- line: 12 + domain: '[n] -> { S1[x] : x >= 0 and x <= -1 + n }' + schedule: '[n] -> { S1[x] -> [0, x, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x] -> s[] }' + read: 0 + write: 1 + - type: call + name: f +- line: 13 + domain: '[n] -> { [S_1[x, t] -> [1]] : x >= 0 and x <= -1 + n and t >= 0 }' + schedule: '[n] -> { S_1[x, t] -> [0, x, 1, t, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x, t] -> __pet_test_0[x, t] }' + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_1[x, t] -> [x] }' + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_1[x, t] -> s[] }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_1[x, t] -> __pet_test_0[x, o1] : o1 >= 0 and o1 <= -1 + + t }' + read: 1 + write: 0 +- line: 14 + domain: '[n] -> { [S2[x, t] -> [1]] : x >= 0 and x <= -1 + n and t >= 0 }' + schedule: '[n] -> { S2[x, t] -> [0, x, 1, t, 1, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x, t] -> s[] }' + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: access + relation: '[n] -> { S2[x, t] -> s[] }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x, t] -> __pet_test_0[x, o1] : o1 >= 0 and o1 <= t }' + read: 1 + write: 0 +- line: 16 + domain: '[n] -> { R[x] : x >= 0 and x <= -1 + n }' + schedule: '[n] -> { R[x] -> [0, x, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x] -> s[] }' + read: 1 + write: 0 diff --git a/tests/while_overflow.c b/tests/while_overflow.c new file mode 100644 index 0000000..4b0f840 --- /dev/null +++ b/tests/while_overflow.c @@ -0,0 +1,17 @@ +int t(void); +int f(void); +int g(int); + +void foo(int N) +{ + int s; + int v; + +#pragma scop + s = 0; + while (t()) { + for (int i = 0; i < 2 * N; ++i) + s = s + 1; + } +#pragma endscop +} diff --git a/tests/while_overflow.scop b/tests/while_overflow.scop new file mode 100644 index 0000000..1f8ca7d --- /dev/null +++ b/tests/while_overflow.scop @@ -0,0 +1,74 @@ +context: '[N] -> { : N <= 2147483647 and N >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[N] -> { __pet_test_0[t] : t >= 0 }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '[N] -> { s[] }' + element_type: int + element_size: 4 +statements: +- line: 11 + domain: '[N] -> { S_0[] }' + schedule: '{ S_0[] -> [0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[N] -> { S_0[] -> s[] }' + read: 0 + write: 1 + - type: access + relation: '[N] -> { S_0[] -> [0] }' + read: 1 + write: 0 +- line: 12 + domain: '[N] -> { [S_1[t] -> [1]] : t >= 0 }' + schedule: '{ S_1[t] -> [1, t, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[N] -> { S_1[t] -> __pet_test_0[t] }' + read: 0 + write: 1 + - type: call + name: t + arguments: + - type: access + relation: '[N] -> { S_1[t] -> __pet_test_0[o0] : o0 <= -1 + t and o0 >= 0 }' + read: 1 + write: 0 +- line: 14 + domain: '[N] -> { [S_2[t, i] -> [1]] : t >= 0 and i <= -1 + 2N and N <= 1073741823 + and i >= 0 }' + schedule: '[N] -> { S_2[t, i] -> [1, t, 1, 0, i] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[N] -> { S_2[t, i] -> s[] }' + read: 0 + write: 1 + - type: binary + operation: + + arguments: + - type: access + relation: '[N] -> { S_2[t, i] -> s[] }' + read: 1 + write: 0 + - type: access + relation: '[N] -> { S_2[t, i] -> [1] }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[N] -> { S_2[t, i] -> __pet_test_0[o0] : o0 >= 0 and o0 <= t }' + read: 1 + write: 0 -- 2.11.4.GIT