From 9f352e76f7f6a614786e1200d0d2c35a256b359b Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Wed, 30 May 2012 17:43:02 +0200 Subject: [PATCH] handle generic conditions is for loops They are handled in essentially the same way as while loops, except that we need to take into account the loop iterator on the for loop. Because we don't know in advance if we are going to need a separate statement to evaluate the loop condition, we may need to make room for such a statement even when we turn out not to need it. This commit may therefore also affect the statement numbers in some cases. Signed-off-by: Sven Verdoolaege --- scan.cc | 76 ++++++++++++++++++++++++----- tests/dynamic_bound.scop | 33 +++++++------ tests/for_while.c | 19 ++++++++ tests/for_while.scop | 89 ++++++++++++++++++++++++++++++++++ tests/for_while_dec.c | 19 ++++++++ tests/for_while_dec.scop | 92 +++++++++++++++++++++++++++++++++++ tests/for_while_inc.c | 19 ++++++++ tests/for_while_inc.scop | 92 +++++++++++++++++++++++++++++++++++ tests/for_while_overflow.c | 17 +++++++ tests/for_while_overflow.scop | 74 ++++++++++++++++++++++++++++ tests/for_while_unsigned.c | 19 ++++++++ tests/for_while_unsigned.scop | 93 +++++++++++++++++++++++++++++++++++ tests/for_while_unsigned2.c | 20 ++++++++ tests/for_while_unsigned2.scop | 107 +++++++++++++++++++++++++++++++++++++++++ 14 files changed, 742 insertions(+), 27 deletions(-) create mode 100644 tests/for_while.c create mode 100644 tests/for_while.scop create mode 100644 tests/for_while_dec.c create mode 100644 tests/for_while_dec.scop create mode 100644 tests/for_while_inc.c create mode 100644 tests/for_while_inc.scop create mode 100644 tests/for_while_overflow.c create mode 100644 tests/for_while_overflow.scop create mode 100644 tests/for_while_unsigned.c create mode 100644 tests/for_while_unsigned.scop create mode 100644 tests/for_while_unsigned2.c create mode 100644 tests/for_while_unsigned2.scop diff --git a/scan.cc b/scan.cc index c742345..2bb07aa 100644 --- a/scan.cc +++ b/scan.cc @@ -2414,6 +2414,9 @@ static bool has_nested(__isl_keep isl_pw_aff *pa) * * The condition is allowed to contain nested accesses, provided * they are not being written to inside the body of the loop. + * Otherwise, or if the condition is otherwise non-affine, the for loop is + * essentially treated as a while loop, with iteration domain + * { [i] : i >= init }. * * We extract a pet_scop for the body and then embed it in a loop with * iteration domain and schedule @@ -2430,6 +2433,17 @@ static bool has_nested(__isl_keep isl_pw_aff *pa) * a simple upper [lower] bound and a condition that is extended * to apply to all previous iterations otherwise. * + * If the condition is non-affine, then we drop the condition from the + * iteration domain and instead create a separate statement + * for evaluating the condition. The body is then 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. + * * If the stride of the loop is not 1, then "i >= init" is replaced by * * (exists a: i = init + stride * a and a >= 0) @@ -2450,6 +2464,10 @@ static bool has_nested(__isl_keep isl_pw_aff *pa) * However, the is_simple_bound condition is not enough since it doesn't * check if there even is an upper bound. * + * If the loop condition is non-affine, then we keep the virtual + * iterator in the iteration domain and instead replace all accesses + * to the original iterator by the wrapping of the virtual iterator. + * * Wrapping on unsigned iterators can be avoided entirely if * loop condition is simple, the loop iterator is incremented * [decremented] by one and the last value before wrapping cannot @@ -2464,6 +2482,8 @@ static bool has_nested(__isl_keep isl_pw_aff *pa) * the condition on both the initial value and * the result of incrementing the iterator for each iteration of the domain * can be evaluated. + * If the loop condition is non-affine, then we only consider validity + * of the initial value. */ struct pet_scop *PetScan::extract_for(ForStmt *stmt) { @@ -2477,20 +2497,23 @@ struct pet_scop *PetScan::extract_for(ForStmt *stmt) isl_map *sched; isl_set *cond = NULL; isl_id *id; - struct pet_scop *scop; + struct pet_scop *scop, *scop_cond = NULL; assigned_value_cache cache(assigned_value); isl_int inc; bool is_one; bool is_unsigned; bool is_simple; bool is_virtual; - isl_map *wrap = NULL, *ident; + bool keep_virtual = false; + isl_map *wrap = NULL; isl_pw_aff *pa, *pa_inc, *init_val; isl_set *valid_init; isl_set *valid_cond; isl_set *valid_cond_init; isl_set *valid_cond_next; isl_set *valid_inc; + isl_map *test_access = NULL; + int stmt_id; if (!stmt->getInit() && !stmt->getCond() && !stmt->getInc()) return extract_infinite_for(stmt); @@ -2540,18 +2563,36 @@ struct pet_scop *PetScan::extract_for(ForStmt *stmt) id = isl_id_alloc(ctx, iv->getName().str().c_str(), iv); + pa = try_extract_nested_condition(stmt->getCond()); + if (allow_nested && (!pa || has_nested(pa))) + stmt_id = n_stmt++; + scop = extract(stmt->getBody()); - pa = try_extract_nested_condition(stmt->getCond()); if (pa && !is_nested_allowed(pa, scop)) { isl_pw_aff_free(pa); pa = NULL; } - if (!pa) - pa = extract_condition(stmt->getCond()); + if (!allow_nested && !pa) + pa = try_extract_affine_condition(stmt->getCond()); valid_cond = isl_pw_aff_domain(isl_pw_aff_copy(pa)); cond = isl_pw_aff_non_zero_set(pa); + if (allow_nested && !cond) { + int save_n_stmt = n_stmt; + test_access = create_test_access(ctx, n_test++); + n_stmt = stmt_id; + scop_cond = extract_non_affine_condition(stmt->getCond(), + isl_map_copy(test_access)); + n_stmt = save_n_stmt; + scop_cond = scop_add_array(scop_cond, test_access, ast_context); + scop_cond = pet_scop_prefix(scop_cond, 0); + scop = pet_scop_reset_context(scop); + scop = pet_scop_prefix(scop, 1); + keep_virtual = true; + cond = isl_set_universe(isl_space_set_alloc(ctx, 0, 0)); + } + cond = embed(cond, isl_id_copy(id)); valid_cond = isl_set_coalesce(valid_cond); valid_cond = embed(valid_cond, isl_id_copy(id)); @@ -2602,26 +2643,37 @@ struct pet_scop *PetScan::extract_for(ForStmt *stmt) valid_cond_next = valid_on_next(valid_cond, isl_set_copy(domain), inc); valid_inc = enforce_subset(isl_set_copy(domain), valid_inc); - if (is_virtual) { + if (is_virtual && !keep_virtual) { wrap = isl_map_set_dim_id(wrap, isl_dim_out, 0, isl_id_copy(id)); sched = isl_map_intersect_domain(sched, isl_set_copy(domain)); domain = isl_set_apply(domain, isl_map_copy(wrap)); sched = isl_map_apply_domain(sched, wrap); } - space = isl_set_get_space(domain); - ident = isl_map_identity(isl_space_map_from_set(space)); + if (!(is_virtual && keep_virtual)) { + space = isl_set_get_space(domain); + wrap = isl_map_identity(isl_space_map_from_set(space)); + } - scop = pet_scop_embed(scop, domain, sched, ident, id); + scop_cond = pet_scop_embed(scop_cond, isl_set_copy(domain), + isl_map_copy(sched), isl_map_copy(wrap), isl_id_copy(id)); + scop = pet_scop_embed(scop, isl_set_copy(domain), sched, wrap, id); scop = resolve_nested(scop); + if (test_access) { + scop = scop_add_while(scop_cond, scop, test_access, domain, + isl_int_sgn(inc)); + isl_set_free(valid_inc); + } else { + scop = pet_scop_restrict_context(scop, valid_inc); + scop = pet_scop_restrict_context(scop, valid_cond_next); + scop = pet_scop_restrict_context(scop, valid_cond_init); + isl_set_free(domain); + } clear_assignment(assigned_value, iv); isl_int_clear(inc); scop = pet_scop_restrict_context(scop, valid_init); - scop = pet_scop_restrict_context(scop, valid_inc); - scop = pet_scop_restrict_context(scop, valid_cond_next); - scop = pet_scop_restrict_context(scop, valid_cond_init); return scop; } diff --git a/tests/dynamic_bound.scop b/tests/dynamic_bound.scop index 24ca5b2..2698a79 100644 --- a/tests/dynamic_bound.scop +++ b/tests/dynamic_bound.scop @@ -4,13 +4,16 @@ arrays: extent: '{ N[] }' value_bounds: '{ [i0] : i0 >= 0 and i0 <= 100 }' element_type: int + element_size: 4 - context: '{ : }' extent: '{ M[] }' value_bounds: '{ [i0] : i0 >= 0 and i0 <= 100 }' element_type: int + element_size: 4 - context: '{ : }' - extent: '{ a[i0, i1] : i0 >= 0 and i1 >= 0 and i0 <= 99 and i1 <= 99 }' + extent: '{ a[i0, i1] : i1 >= 0 and i1 <= 99 and i0 >= 0 and i0 <= 99 }' element_type: int + element_size: 4 statements: - line: 13 domain: '{ S_0[] }' @@ -39,63 +42,63 @@ statements: - type: call name: g - line: 17 - domain: '{ [S_2[i, j] -> [N, M]] : N >= 1 + i and i >= 0 and j >= 0 and M >= 1 + + domain: '{ [S_4[i, j] -> [N, M]] : N >= 1 + i and j >= 0 and i >= 0 and M >= 1 + j }' - schedule: '{ S_2[i, j] -> [2, i, j] }' + schedule: '{ S_4[i, j] -> [2, i, j] }' body: type: binary operation: = arguments: - type: access - relation: '{ S_2[i, j] -> a[i, j] }' + relation: '{ S_4[i, j] -> a[i, j] }' read: 0 write: 1 - type: binary operation: + arguments: - type: access - relation: '{ S_2[i, j] -> [i] }' + relation: '{ S_4[i, j] -> [i] }' read: 1 write: 0 - type: access - relation: '{ S_2[i, j] -> [j] }' + relation: '{ S_4[i, j] -> [j] }' read: 1 write: 0 arguments: - type: access - relation: '{ S_2[i, j] -> N[] }' + relation: '{ S_4[i, j] -> N[] }' read: 1 write: 0 - type: access - relation: '{ S_2[i, j] -> M[] }' + relation: '{ S_4[i, j] -> M[] }' read: 1 write: 0 - line: 20 - domain: '{ [S_3[i, j] -> [N, M]] : i >= 0 and N >= 1 + i and j >= 0 and M >= 1 + + domain: '{ [S_7[i, j] -> [N, M]] : N >= 1 + i and j >= 0 and i >= 0 and M >= 1 + j }' - schedule: '{ S_3[i, j] -> [3, i, j] }' + schedule: '{ S_7[i, j] -> [3, i, j] }' body: type: call name: h arguments: - type: access - relation: '{ S_3[i, j] -> [i] }' + relation: '{ S_7[i, j] -> [i] }' read: 1 write: 0 - type: access - relation: '{ S_3[i, j] -> [j] }' + relation: '{ S_7[i, j] -> [j] }' read: 1 write: 0 - type: access - relation: '{ S_3[i, j] -> a[i, j] }' + relation: '{ S_7[i, j] -> a[i, j] }' read: 1 write: 0 arguments: - type: access - relation: '{ S_3[i, j] -> N[] }' + relation: '{ S_7[i, j] -> N[] }' read: 1 write: 0 - type: access - relation: '{ S_3[i, j] -> M[] }' + relation: '{ S_7[i, j] -> M[] }' read: 1 write: 0 diff --git a/tests/for_while.c b/tests/for_while.c new file mode 100644 index 0000000..ca401f3 --- /dev/null +++ b/tests/for_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 x1 = 0; x1 < n; ++x1) { +S1: s = f(); + for (int x2 = 0; P(x1, x2); ++x2) { +S2: s = g(s); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/for_while.scop b/tests/for_while.scop new file mode 100644 index 0000000..03dbc2a --- /dev/null +++ b/tests/for_while.scop @@ -0,0 +1,89 @@ +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x1, x2] : x1 >= 0 and x1 <= -1 + n and x2 >= 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[x1] : x1 >= 0 and x1 <= -1 + n }' + schedule: '[n] -> { S1[x1] -> [0, x1, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x1] -> s[] }' + read: 0 + write: 1 + - type: call + name: f +- line: 13 + domain: '[n] -> { [S_1[x1, x2] -> [1]] : x1 >= 0 and x1 <= -1 + n and x2 >= 0 }' + schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, x2, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, x2] }' + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> [x1] }' + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_1[x1, x2] -> [x2] }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : o1 >= 0 and o1 <= -1 + + x2 }' + read: 1 + write: 0 +- line: 14 + domain: '[n] -> { [S2[x1, x2] -> [1]] : x1 >= 0 and x1 <= -1 + n and x2 >= 0 }' + schedule: '[n] -> { S2[x1, x2] -> [0, x1, 1, x2, 1, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> s[] }' + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> s[] }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, o1] : o1 >= 0 and o1 <= x2 + }' + read: 1 + write: 0 +- line: 16 + domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }' + schedule: '[n] -> { R[x1] -> [0, x1, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x1] -> s[] }' + read: 1 + write: 0 diff --git a/tests/for_while_dec.c b/tests/for_while_dec.c new file mode 100644 index 0000000..1136e67 --- /dev/null +++ b/tests/for_while_dec.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 x1 = 0; x1 < n; ++x1) { +S1: s = f(); + for (int x2 = 9; P(x1, x2); x2 -= 3) { +S2: s = g(s); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/for_while_dec.scop b/tests/for_while_dec.scop new file mode 100644 index 0000000..72c5796 --- /dev/null +++ b/tests/for_while_dec.scop @@ -0,0 +1,92 @@ +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x1, x2] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1 + >= 0 and x1 <= -1 + n and x2 <= 9) }' + 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[x1] : x1 >= 0 and x1 <= -1 + n }' + schedule: '[n] -> { S1[x1] -> [0, x1, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x1] -> s[] }' + read: 0 + write: 1 + - type: call + name: f +- line: 13 + domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1 + >= 0 and x1 <= -1 + n and x2 <= 9) }' + schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, -x2, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, x2] }' + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> [x1] }' + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_1[x1, x2] -> [x2] }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]: + 3e0 = o1 and o1 <= 9 and o1 >= 3 + x2) }' + read: 1 + write: 0 +- line: 14 + domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1 >= + 0 and x1 <= -1 + n and x2 <= 9) }' + schedule: '[n] -> { S2[x1, x2] -> [0, x1, 1, -x2, 1, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> s[] }' + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> s[] }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]: + 3e0 = o1 and o1 <= 9 and o1 >= x2) }' + read: 1 + write: 0 +- line: 16 + domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }' + schedule: '[n] -> { R[x1] -> [0, x1, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x1] -> s[] }' + read: 1 + write: 0 diff --git a/tests/for_while_inc.c b/tests/for_while_inc.c new file mode 100644 index 0000000..5f1a74c --- /dev/null +++ b/tests/for_while_inc.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 x1 = 0; x1 < n; ++x1) { +S1: s = f(); + for (int x2 = 9; P(x1, x2); x2 += 2) { +S2: s = g(s); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/for_while_inc.scop b/tests/for_while_inc.scop new file mode 100644 index 0000000..4d9b82a --- /dev/null +++ b/tests/for_while_inc.scop @@ -0,0 +1,92 @@ +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x1, x2] : exists (e0 = [(-1 + x2)/2]: 2e0 = -1 + + x2 and x1 >= 0 and x1 <= -1 + n and x2 >= 9) }' + 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[x1] : x1 >= 0 and x1 <= -1 + n }' + schedule: '[n] -> { S1[x1] -> [0, x1, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x1] -> s[] }' + read: 0 + write: 1 + - type: call + name: f +- line: 13 + domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = [(-1 + x2)/2]: 2e0 = -1 + + x2 and x1 >= 0 and x1 <= -1 + n and x2 >= 9) }' + schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, x2, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, x2] }' + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> [x1] }' + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_1[x1, x2] -> [x2] }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(-1 + + o1)/2]: 2e0 = -1 + o1 and o1 <= -2 + x2 and o1 >= 9) }' + read: 1 + write: 0 +- line: 14 + domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = [(-1 + x2)/2]: 2e0 = -1 + x2 + and x1 >= 0 and x1 <= -1 + n and x2 >= 9) }' + schedule: '[n] -> { S2[x1, x2] -> [0, x1, 1, x2, 1, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> s[] }' + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> s[] }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(-1 + o1)/2]: + 2e0 = -1 + o1 and o1 <= x2 and o1 >= 9) }' + read: 1 + write: 0 +- line: 16 + domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }' + schedule: '[n] -> { R[x1] -> [0, x1, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x1] -> s[] }' + read: 1 + write: 0 diff --git a/tests/for_while_overflow.c b/tests/for_while_overflow.c new file mode 100644 index 0000000..46b1b9b --- /dev/null +++ b/tests/for_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; + for (int T = 0; t(); ++T) { + for (int i = 0; i < 2 * N; ++i) + s = s + 1; + } +#pragma endscop +} diff --git a/tests/for_while_overflow.scop b/tests/for_while_overflow.scop new file mode 100644 index 0000000..75446b7 --- /dev/null +++ b/tests/for_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 diff --git a/tests/for_while_unsigned.c b/tests/for_while_unsigned.c new file mode 100644 index 0000000..383e3cb --- /dev/null +++ b/tests/for_while_unsigned.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 x1 = 0; x1 < n; ++x1) { +S1: s = f(); + for (unsigned char x2 = 9; P(x1, x2); x2 -= 3) { +S2: s = g(s); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/for_while_unsigned.scop b/tests/for_while_unsigned.scop new file mode 100644 index 0000000..ed194ab --- /dev/null +++ b/tests/for_while_unsigned.scop @@ -0,0 +1,93 @@ +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x1, x2] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1 + >= 0 and x1 <= -1 + n and x2 <= 9) }' + 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[x1] : x1 >= 0 and x1 <= -1 + n }' + schedule: '[n] -> { S1[x1] -> [0, x1, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x1] -> s[] }' + read: 0 + write: 1 + - type: call + name: f +- line: 13 + domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1 + >= 0 and x1 <= -1 + n and x2 <= 9) }' + schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, -x2, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, x2] }' + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> [x1] }' + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_1[x1, x2] -> [o0] : exists (e0 = [(-x2 + o0)/256]: 256e0 + = -x2 + o0 and o0 <= 255 and o0 >= 0) }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]: + 3e0 = o1 and o1 <= 9 and o1 >= 3 + x2) }' + read: 1 + write: 0 +- line: 14 + domain: '[n] -> { [S2[x1, x2] -> [1]] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1 >= + 0 and x1 <= -1 + n and x2 <= 9) }' + schedule: '[n] -> { S2[x1, x2] -> [0, x1, 1, -x2, 1, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> s[] }' + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> s[] }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]: + 3e0 = o1 and o1 <= 9 and o1 >= x2) }' + read: 1 + write: 0 +- line: 16 + domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }' + schedule: '[n] -> { R[x1] -> [0, x1, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x1] -> s[] }' + read: 1 + write: 0 diff --git a/tests/for_while_unsigned2.c b/tests/for_while_unsigned2.c new file mode 100644 index 0000000..5420437 --- /dev/null +++ b/tests/for_while_unsigned2.c @@ -0,0 +1,20 @@ +int f(void); +int P(int, int); +int g(int); +void h(int); + +void foo(int n, int a[256][256]) +{ + int s; + +#pragma scop + for (int x1 = 0; x1 < n; ++x1) { +S1: s = f(); + for (unsigned char x2 = 9; P(x1, x2); x2 -= 3) { + for (int x3 = 0; x3 <= x2; ++x3) +S2: s = g(s + a[x2][255 - x2]); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/for_while_unsigned2.scop b/tests/for_while_unsigned2.scop new file mode 100644 index 0000000..740e79c --- /dev/null +++ b/tests/for_while_unsigned2.scop @@ -0,0 +1,107 @@ +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x1, x2] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1 + >= 0 and x1 <= -1 + n and x2 <= 9) }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '[n] -> { a[i0, i1] : i1 <= 255 and i0 >= 0 and i1 >= 0 }' + element_type: int + element_size: 4 +- context: '{ : }' + extent: '[n] -> { s[] }' + element_type: int + element_size: 4 +statements: +- line: 12 + domain: '[n] -> { S1[x1] : x1 >= 0 and x1 <= -1 + n }' + schedule: '[n] -> { S1[x1] -> [0, x1, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x1] -> s[] }' + read: 0 + write: 1 + - type: call + name: f +- line: 13 + domain: '[n] -> { [S_1[x1, x2] -> [1]] : exists (e0 = [(x2)/3]: 3e0 = x2 and x1 + >= 0 and x1 <= -1 + n and x2 <= 9) }' + schedule: '[n] -> { S_1[x1, x2] -> [0, x1, 1, -x2, 0] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, x2] }' + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> [x1] }' + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_1[x1, x2] -> [o0] : exists (e0 = [(-x2 + o0)/256]: 256e0 + = -x2 + o0 and o0 <= 255 and o0 >= 0) }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_1[x1, x2] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]: + 3e0 = o1 and o1 <= 9 and o1 >= 3 + x2) }' + read: 1 + write: 0 +- line: 15 + domain: '[n] -> { [S2[x1, x2, x3] -> [1]] : exists (e0 = [(255 - x2)/256], e1 = + [(x2)/3]: 3e1 = x2 and x3 >= 0 and x1 <= -1 + n and x1 >= 0 and x2 <= 9 and 256e0 + >= -x2 + x3 and 256e0 <= 255 - x2 and 256e0 >= -x2) }' + schedule: '[n] -> { S2[x1, x2, x3] -> [0, x1, 1, -x2, 1, 0, x3] }' + body: + type: binary + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x1, x2, x3] -> s[] }' + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: binary + operation: + + arguments: + - type: access + relation: '[n] -> { S2[x1, x2, x3] -> s[] }' + read: 1 + write: 0 + - type: access + relation: '[n] -> { S2[x1, x2, x3] -> a[o0, 255 - o0] : exists (e0 = [(x2)/3], + e1 = [(-253x2 - 3o0)/768]: 3e0 = x2 and 768e1 = -253x2 - 3o0 and o0 <= + 255 and o0 >= 0) }' + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x1, x2, x3] -> __pet_test_0[x1, o1] : exists (e0 = [(o1)/3]: + 3e0 = o1 and o1 <= 9 and o1 >= x2) }' + read: 1 + write: 0 +- line: 17 + domain: '[n] -> { R[x1] : x1 >= 0 and x1 <= -1 + n }' + schedule: '[n] -> { R[x1] -> [0, x1, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x1] -> s[] }' + read: 1 + write: 0 -- 2.11.4.GIT