From d6c8ddd76655ba12756f4eaa6158bfff625e9a43 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Sun, 29 Dec 2013 10:34:10 +0100 Subject: [PATCH] treat fors with non-affine initialization or non-constant increment as whiles Signed-off-by: Sven Verdoolaege --- scan.cc | 176 ++++++++++++++++------- scan.h | 9 +- tests/break6.c | 18 +++ tests/break6.scop | 343 +++++++++++++++++++++++++++++++++++++++++++++ tests/for_while_inc2.c | 19 +++ tests/for_while_inc2.scop | 183 ++++++++++++++++++++++++ tests/for_while_inc3.c | 19 +++ tests/for_while_inc3.scop | 183 ++++++++++++++++++++++++ tests/for_while_inc4.c | 20 +++ tests/for_while_inc4.scop | 156 +++++++++++++++++++++ tests/for_while_init.c | 19 +++ tests/for_while_init.scop | 183 ++++++++++++++++++++++++ tests/for_while_init2.c | 19 +++ tests/for_while_init2.scop | 187 ++++++++++++++++++++++++ tests/for_while_init3.c | 11 ++ tests/for_while_init3.scop | 161 +++++++++++++++++++++ tests/inc5.c | 11 ++ tests/inc5.scop | 150 ++++++++++++++++++++ tests/loop7.c | 13 ++ tests/loop7.scop | 131 +++++++++++++++++ 20 files changed, 1958 insertions(+), 53 deletions(-) create mode 100644 tests/break6.c create mode 100644 tests/break6.scop create mode 100644 tests/for_while_inc2.c create mode 100644 tests/for_while_inc2.scop create mode 100644 tests/for_while_inc3.c create mode 100644 tests/for_while_inc3.scop create mode 100644 tests/for_while_inc4.c create mode 100644 tests/for_while_inc4.scop create mode 100644 tests/for_while_init.c create mode 100644 tests/for_while_init.scop create mode 100644 tests/for_while_init2.c create mode 100644 tests/for_while_init2.scop create mode 100644 tests/for_while_init3.c create mode 100644 tests/for_while_init3.scop create mode 100644 tests/inc5.c create mode 100644 tests/inc5.scop create mode 100644 tests/loop7.c create mode 100644 tests/loop7.scop diff --git a/scan.cc b/scan.cc index 80c82a5..e4f50ae 100644 --- a/scan.cc +++ b/scan.cc @@ -434,37 +434,6 @@ void PetScan::report_missing_increment(Stmt *stmt) report(stmt, id); } -/* Report an increment that is not constan, unless autodetect is set. - */ -void PetScan::report_non_constant_increment(Stmt *stmt) -{ - DiagnosticsEngine &diag = PP.getDiagnostics(); - unsigned id = diag.getCustomDiagID(DiagnosticsEngine::Warning, - "non-constant increment"); - report(stmt, id); -} - -/* Report an increment that is not static affine, unless autodetect is set. - */ -void PetScan::report_non_static_affine_increment(Stmt *stmt) -{ - DiagnosticsEngine &diag = PP.getDiagnostics(); - unsigned id = diag.getCustomDiagID(DiagnosticsEngine::Warning, - "non static-affine increment"); - report(stmt, id); -} - -/* Report a loop initialization that is not static affine, - * unless autodetect is set. - */ -void PetScan::report_non_static_affine_initialization(Stmt *stmt) -{ - DiagnosticsEngine &diag = PP.getDiagnostics(); - unsigned id = diag.getCustomDiagID(DiagnosticsEngine::Warning, - "non static-affine initialization"); - report(stmt, id); -} - /* Extract an integer from "expr". */ __isl_give isl_val *PetScan::extract_int(isl_ctx *ctx, IntegerLiteral *expr) @@ -2566,7 +2535,7 @@ struct pet_scop *PetScan::extract(WhileStmt *stmt) if (partial) return scop_body; - return extract_while(cond, test_nr, stmt_nr, scop_body); + return extract_while(cond, test_nr, stmt_nr, scop_body, NULL); } /* Construct a generic while scop, with iteration domain @@ -2575,6 +2544,10 @@ struct pet_scop *PetScan::extract(WhileStmt *stmt) * "test_nr" is the sequence number of the virtual test variable that contains * the result of the condition and "stmt_nr" is the sequence number * of the statement that evaluates the condition. + * If "scop_inc" is not NULL, then it is added at the end of the body, + * after replacing any skip conditions resulting from continue statements + * by the skip conditions resulting from break statements (if any). + * * 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 @@ -2590,7 +2563,7 @@ struct pet_scop *PetScan::extract(WhileStmt *stmt) * or in scop_add_break (if the skip condition is not affine). */ struct pet_scop *PetScan::extract_while(Expr *cond, int test_nr, int stmt_nr, - struct pet_scop *scop_body) + struct pet_scop *scop_body, struct pet_scop *scop_inc) { isl_id *id, *id_test, *id_break_test; isl_set *domain; @@ -2619,6 +2592,17 @@ struct pet_scop *PetScan::extract_while(Expr *cond, int test_nr, int stmt_nr, isl_aff_copy(ident), isl_id_copy(id)); scop_body = pet_scop_reset_context(scop_body); scop_body = pet_scop_prefix(scop_body, 1); + if (scop_inc) { + scop_inc = pet_scop_prefix(scop_inc, 2); + if (pet_scop_has_skip(scop_body, pet_skip_later)) { + isl_multi_pw_aff *skip; + skip = pet_scop_get_skip(scop_body, pet_skip_later); + scop_body = pet_scop_set_skip(scop_body, + pet_skip_now, skip); + } else + pet_scop_reset_skip(scop_body, pet_skip_now); + scop_body = pet_scop_add_seq(ctx, scop_body, scop_inc); + } scop_body = pet_scop_embed(scop_body, isl_set_copy(domain), isl_aff_copy(ident), ident, id); @@ -2836,18 +2820,115 @@ static __isl_give isl_set *valid_on_next(__isl_take isl_set *cond, return enforce_subset(dom, cond); } -/* Construct a pet_scop for a for statement. - * The for loop is required to be of the form +/* Extract the for loop "stmt" as a while loop. + * "iv" is the loop iterator. "init" is the initialization. + * "inc" is the increment. * - * for (i = init; condition; ++i) + * That is, the for loop has the form * - * or + * for (iv = init; cond; iv += inc) + * body; + * + * and is treated as + * + * iv = init; + * while (cond) { + * body; + * iv += inc; + * } + * + * except that the skips resulting from any continue statements + * in body do not apply to the increment, but are replaced by the skips + * resulting from break statements. + * + * If "iv" is declared in the for loop, then it is killed before + * and after the loop. + */ +struct pet_scop *PetScan::extract_non_affine_for(ForStmt *stmt, ValueDecl *iv, + __isl_take pet_expr *init, __isl_take pet_expr *inc) +{ + int declared; + int test_nr, stmt_nr; + pet_expr *expr_iv; + struct pet_scop *scop_init, *scop_inc, *scop, *scop_body; + int type_size; + struct pet_array *array; + struct pet_scop *scop_kill; + + if (!allow_nested) { + unsupported(stmt); + return NULL; + } + + clear_assignment(assigned_value, iv); + + declared = !initialization_assignment(stmt->getInit()); + + expr_iv = extract_access_expr(iv); + expr_iv = mark_write(expr_iv); + type_size = pet_expr_get_type_size(expr_iv); + init = pet_expr_new_binary(type_size, pet_op_assign, expr_iv, init); + scop_init = extract(init, stmt->getInit()->getSourceRange(), false); + scop_init = pet_scop_prefix(scop_init, declared); + + test_nr = n_test++; + stmt_nr = n_stmt++; + scop_body = extract(stmt->getBody()); + if (partial) { + pet_scop_free(scop_init); + return scop_body; + } + + expr_iv = extract_access_expr(iv); + expr_iv = mark_write(expr_iv); + type_size = pet_expr_get_type_size(expr_iv); + inc = pet_expr_new_binary(type_size, pet_op_add_assign, expr_iv, inc); + scop_inc = extract(inc, stmt->getInc()->getSourceRange(), false); + if (!scop_inc) { + pet_scop_free(scop_init); + pet_scop_free(scop_body); + return NULL; + } + + scop = extract_while(stmt->getCond(), test_nr, stmt_nr, scop_body, + scop_inc); + + scop = pet_scop_prefix(scop, declared + 1); + scop = pet_scop_add_seq(ctx, scop_init, scop); + + if (!declared) + return scop; + + array = extract_array(ctx, iv, NULL); + if (array) + array->declared = 1; + scop_kill = kill(stmt, array); + scop_kill = pet_scop_prefix(scop_kill, 0); + scop = pet_scop_add_seq(ctx, scop_kill, scop); + scop_kill = kill(stmt, array); + scop_kill = pet_scop_add_array(scop_kill, array); + scop_kill = pet_scop_prefix(scop_kill, 3); + scop = pet_scop_add_seq(ctx, scop, scop_kill); + + return scop; +} + +/* Construct a pet_scop for a for statement. + * The for loop is required to be of one of the following forms * + * for (i = init; condition; ++i) * for (i = init; condition; --i) + * for (i = init; condition; i += constant) + * for (i = init; condition; i -= constant) * * The initialization of the for loop should either be an assignment - * to an integer variable, or a declaration of such a variable with - * initialization. + * of a static affine value to an integer variable, or a declaration + * of such a variable with initialization. + * + * If the initialization or the increment do not satisfy the above + * conditions, i.e., if the initialization is not static affine + * or the increment is not constant, then the for loop is extracted + * as a while loop instead. * * The condition is allowed to contain nested accesses, provided * they are not being written to inside the body of the loop. @@ -2996,26 +3077,23 @@ struct pet_scop *PetScan::extract_for(ForStmt *stmt) pet_context_free(pc_init_val); pa_inc = pet_expr_extract_affine(pe_inc, pc); pet_context_free(pc); - pet_expr_free(pe_inc); - pet_expr_free(pe_init); inc = pet_extract_cst(pa_inc); if (!pe_init || !pe_inc || !inc || isl_val_is_nan(inc) || isl_pw_aff_involves_nan(pa_inc) || isl_pw_aff_involves_nan(init_val)) { - if (!pe_init || !pe_inc || (pa_inc && !inc)) - ; - else if (isl_pw_aff_involves_nan(pa_inc)) - report_non_static_affine_increment(stmt->getInc()); - else if (isl_pw_aff_involves_nan(init_val)) - report_non_static_affine_initialization(rhs); - else - report_non_constant_increment(stmt->getInc()); isl_id_free(id); isl_val_free(inc); isl_pw_aff_free(pa_inc); isl_pw_aff_free(init_val); + if (pe_init && pe_inc && !(pa_inc && !inc)) + return extract_non_affine_for(stmt, iv, + pe_init, pe_inc); + pet_expr_free(pe_init); + pet_expr_free(pe_inc); return NULL; } + pet_expr_free(pe_init); + pet_expr_free(pe_inc); pa = try_extract_nested_condition(stmt->getCond()); if (allow_nested && (!pa || pet_nested_any_in_pw_aff(pa))) diff --git a/scan.h b/scan.h index f8ed0a8..44af951 100644 --- a/scan.h +++ b/scan.h @@ -159,12 +159,16 @@ private: __isl_give pet_expr *extract_increment(clang::ForStmt *stmt, clang::ValueDecl *iv); struct pet_scop *extract_for(clang::ForStmt *stmt); + struct pet_scop *extract_non_affine_for(clang::ForStmt *stmt, + clang::ValueDecl *iv, + __isl_take pet_expr *init, __isl_take pet_expr *inc); struct pet_scop *extract_infinite_loop(clang::Stmt *body); struct pet_scop *extract_infinite_for(clang::ForStmt *stmt); struct pet_scop *extract_affine_while(__isl_take isl_pw_aff *pa, clang::Stmt *body); struct pet_scop *extract_while(clang::Expr *cond, int test_nr, - int stmt_nr, struct pet_scop *scop_body); + int stmt_nr, struct pet_scop *scop_body, + struct pet_scop *scop_inc); __isl_give pet_expr *mark_write(__isl_take pet_expr *access); __isl_give pet_expr *extract_assume(clang::Expr *expr); @@ -245,7 +249,4 @@ private: void unsupported(clang::Stmt *stmt); void report_prototype_required(clang::Stmt *stmt); void report_missing_increment(clang::Stmt *stmt); - void report_non_constant_increment(clang::Stmt *stmt); - void report_non_static_affine_increment(clang::Stmt *stmt); - void report_non_static_affine_initialization(clang::Stmt *stmt); }; diff --git a/tests/break6.c b/tests/break6.c new file mode 100644 index 0000000..8c2e2ed --- /dev/null +++ b/tests/break6.c @@ -0,0 +1,18 @@ +int f(); + +void foo() +{ + int i, a[100]; + +#pragma scop + for (i = f(); i < 100; ++i) { + a[i] = 0; + if (f()) + break; + a[i] = 1; + if (f()) + continue; + a[i] = 2; + } +#pragma endscop +} diff --git a/tests/break6.scop b/tests/break6.scop new file mode 100644 index 0000000..d1bb3c8 --- /dev/null +++ b/tests/break6.scop @@ -0,0 +1,343 @@ +start: 40 +end: 184 +context: '{ : }' +arrays: +- context: '{ : }' + extent: '{ __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: '{ __pet_test_1[t] : t >= 0 }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '{ __pet_test_2[t] : t >= 0 }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '{ __pet_test_3[t] : t >= 0 }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '{ a[i0] : i0 >= 0 and i0 <= 99 }' + element_type: int + element_size: 4 +- context: '{ : }' + extent: '{ i[] }' + element_type: int + element_size: 4 +statements: +- line: 8 + domain: '{ S_0[] }' + schedule: '{ S_0[] -> [0, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ S_0[] -> i[] }' + index: '{ S_0[] -> i[] }' + reference: __pet_ref_0 + read: 0 + write: 1 + - type: call + name: f +- line: 8 + domain: '{ [S_1[t] -> [1, 0]] : t >= 0 }' + schedule: '{ S_1[t] -> [0, 1, t, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ S_1[t] -> __pet_test_0[t] }' + index: '{ S_1[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_3 + read: 0 + write: 1 + - type: op + operation: < + arguments: + - type: access + relation: '{ S_1[t] -> i[] }' + index: '{ S_1[t] -> i[] }' + reference: __pet_ref_4 + read: 1 + write: 0 + - type: int + value: 100 + arguments: + - type: access + relation: '{ S_1[t] -> __pet_test_0[-1 + t] : t >= 1 }' + index: '{ S_1[t] -> __pet_test_0[((-1 + t) : t >= 1)] }' + reference: __pet_ref_1 + read: 1 + write: 0 + - type: access + relation: '{ S_1[t] -> __pet_test_1[-1 + t] : t >= 1 }' + index: '{ S_1[t] -> __pet_test_1[((-1 + t) : t >= 1)] }' + reference: __pet_ref_2 + read: 1 + write: 0 +- line: 9 + domain: '{ [S_2[t] -> [1, 0]] : t >= 0 }' + schedule: '{ S_2[t] -> [0, 1, t, 1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ [S_2[t] -> [i1]] -> a[i1] : i1 >= 0 }' + index: '{ [S_2[t] -> [i1]] -> a[((i1) : i1 >= 0)] }' + reference: __pet_ref_8 + read: 0 + write: 1 + arguments: + - type: access + relation: '{ S_2[t] -> i[] }' + index: '{ S_2[t] -> i[] }' + reference: __pet_ref_7 + read: 1 + write: 0 + - type: int + value: 0 + arguments: + - type: access + relation: '{ S_2[t] -> __pet_test_0[t] }' + index: '{ S_2[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_5 + read: 1 + write: 0 + - type: access + relation: '{ S_2[t] -> __pet_test_1[-1 + t] : t >= 1 }' + index: '{ S_2[t] -> __pet_test_1[((-1 + t) : t >= 1)] }' + reference: __pet_ref_6 + read: 1 + write: 0 +- line: 10 + domain: '{ [S_3[t] -> [1, 0]] : t >= 0 }' + schedule: '{ S_3[t] -> [0, 1, t, 1, 1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ S_3[t] -> __pet_test_1[t] }' + index: '{ S_3[t] -> __pet_test_1[(t)] }' + reference: __pet_ref_11 + read: 0 + write: 1 + - type: call + name: f + arguments: + - type: access + relation: '{ S_3[t] -> __pet_test_0[t] }' + index: '{ S_3[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_9 + read: 1 + write: 0 + - type: access + relation: '{ S_3[t] -> __pet_test_1[-1 + t] : t >= 1 }' + index: '{ S_3[t] -> __pet_test_1[((-1 + t) : t >= 1)] }' + reference: __pet_ref_10 + read: 1 + write: 0 +- line: 12 + domain: '{ [S_4[t] -> [1, 0]] : t >= 0 }' + schedule: '{ S_4[t] -> [0, 1, t, 1, 2] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ [S_4[t] -> [i1]] -> a[i1] : i1 >= 0 }' + index: '{ [S_4[t] -> [i1]] -> a[((i1) : i1 >= 0)] }' + reference: __pet_ref_15 + read: 0 + write: 1 + arguments: + - type: access + relation: '{ S_4[t] -> i[] }' + index: '{ S_4[t] -> i[] }' + reference: __pet_ref_14 + read: 1 + write: 0 + - type: int + value: 1 + arguments: + - type: access + relation: '{ S_4[t] -> __pet_test_0[t] }' + index: '{ S_4[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_12 + read: 1 + write: 0 + - type: access + relation: '{ S_4[t] -> __pet_test_1[t] }' + index: '{ S_4[t] -> __pet_test_1[(t)] }' + reference: __pet_ref_13 + read: 1 + write: 0 +- line: 13 + domain: '{ [S_5[t] -> [1, 0]] : t >= 0 }' + schedule: '{ S_5[t] -> [0, 1, t, 1, 3, 0, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ S_5[t] -> __pet_test_2[t] }' + index: '{ S_5[t] -> __pet_test_2[(t)] }' + reference: __pet_ref_18 + read: 0 + write: 1 + - type: call + name: f + arguments: + - type: access + relation: '{ S_5[t] -> __pet_test_0[t] }' + index: '{ S_5[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_16 + read: 1 + write: 0 + - type: access + relation: '{ S_5[t] -> __pet_test_1[t] }' + index: '{ S_5[t] -> __pet_test_1[(t)] }' + reference: __pet_ref_17 + read: 1 + write: 0 +- line: -1 + domain: '{ [S_6[t] -> [1, 0]] : t >= 0 }' + schedule: '{ S_6[t] -> [0, 1, t, 1, 3, 1] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ S_6[t] -> __pet_test_3[t] }' + index: '{ S_6[t] -> __pet_test_3[(t)] }' + reference: __pet_ref_21 + read: 0 + write: 1 + - type: op + operation: '?:' + arguments: + - type: access + relation: '{ S_6[t] -> __pet_test_1[t] }' + index: '{ S_6[t] -> __pet_test_1[(t)] }' + reference: __pet_ref_22 + read: 1 + write: 0 + - type: access + relation: '{ S_6[t] -> [1] }' + index: '{ S_6[t] -> [(1)] }' + reference: __pet_ref_23 + read: 1 + write: 0 + - type: access + relation: '{ [S_6[t] -> [0]] -> __pet_test_2[t] }' + index: '{ [S_6[t] -> [__pet_test_1]] -> __pet_test_2[(t)] }' + reference: __pet_ref_25 + read: 1 + write: 0 + arguments: + - type: access + relation: '{ S_6[t] -> __pet_test_1[t] }' + index: '{ S_6[t] -> __pet_test_1[(t)] }' + reference: __pet_ref_24 + read: 1 + write: 0 + arguments: + - type: access + relation: '{ S_6[t] -> __pet_test_0[t] }' + index: '{ S_6[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_19 + read: 1 + write: 0 + - type: access + relation: '{ S_6[t] -> __pet_test_1[-1 + t] : t >= 1 }' + index: '{ S_6[t] -> __pet_test_1[((-1 + t) : t >= 1)] }' + reference: __pet_ref_20 + read: 1 + write: 0 +- line: 15 + domain: '{ [S_7[t] -> [1, 0, 0]] : t >= 0 }' + schedule: '{ S_7[t] -> [0, 1, t, 1, 4] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ [S_7[t] -> [i1]] -> a[i1] : i1 >= 0 }' + index: '{ [S_7[t] -> [i1]] -> a[((i1) : i1 >= 0)] }' + reference: __pet_ref_30 + read: 0 + write: 1 + arguments: + - type: access + relation: '{ S_7[t] -> i[] }' + index: '{ S_7[t] -> i[] }' + reference: __pet_ref_29 + read: 1 + write: 0 + - type: int + value: 2 + arguments: + - type: access + relation: '{ S_7[t] -> __pet_test_0[t] }' + index: '{ S_7[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_26 + read: 1 + write: 0 + - type: access + relation: '{ S_7[t] -> __pet_test_1[-1 + t] : t >= 1 }' + index: '{ S_7[t] -> __pet_test_1[((-1 + t) : t >= 1)] }' + reference: __pet_ref_27 + read: 1 + write: 0 + - type: access + relation: '{ S_7[t] -> __pet_test_3[t] }' + index: '{ S_7[t] -> __pet_test_3[(t)] }' + reference: __pet_ref_28 + read: 1 + write: 0 +- line: 8 + domain: '{ [S_8[t] -> [1, 0]] : t >= 0 }' + schedule: '{ S_8[t] -> [0, 1, t, 2] }' + body: + type: op + operation: += + arguments: + - type: access + relation: '{ S_8[t] -> i[] }' + index: '{ S_8[t] -> i[] }' + reference: __pet_ref_33 + read: 0 + write: 1 + - type: int + value: 1 + arguments: + - type: access + relation: '{ S_8[t] -> __pet_test_0[t] }' + index: '{ S_8[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_31 + read: 1 + write: 0 + - type: access + relation: '{ S_8[t] -> __pet_test_1[t] }' + index: '{ S_8[t] -> __pet_test_1[(t)] }' + reference: __pet_ref_32 + read: 1 + write: 0 +implications: +- satisfied: 0 + extension: '{ __pet_test_1[t] -> __pet_test_1[t''] : t'' <= t and t'' >= 0 }' +- satisfied: 1 + extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }' diff --git a/tests/for_while_inc2.c b/tests/for_while_inc2.c new file mode 100644 index 0000000..6d37929 --- /dev/null +++ b/tests/for_while_inc2.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 += s) { +S2: s = g(s); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/for_while_inc2.scop b/tests/for_while_inc2.scop new file mode 100644 index 0000000..70af95a --- /dev/null +++ b/tests/for_while_inc2.scop @@ -0,0 +1,183 @@ +start: 83 +end: 234 +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x1, t] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '[n] -> { x2[] }' + element_type: int + element_size: 4 + declared: 1 +- context: '{ : }' + extent: '[n] -> { s[] }' + element_type: int + element_size: 4 +statements: +- line: 12 + domain: '[n] -> { S1[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S1[x1] -> [0, x1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x1] -> s[] }' + index: '[n] -> { S1[x1] -> s[] }' + reference: __pet_ref_0 + read: 0 + write: 1 + - type: call + name: f +- line: 13 + domain: '[n] -> { S_5[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_5[x1] -> [0, x1, 1, 0] }' + body: + type: op + operation: kill + arguments: + - type: access + relation: '[n] -> { S_5[x1] -> x2[] }' + index: '[n] -> { S_5[x1] -> x2[] }' + reference: __pet_ref_1 + read: 0 + write: 0 +- line: 13 + domain: '[n] -> { S_1[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_1[x1] -> [0, x1, 1, 1] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x1] -> x2[] }' + index: '[n] -> { S_1[x1] -> x2[] }' + reference: __pet_ref_2 + read: 0 + write: 1 + - type: int + value: 0 +- line: 13 + domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S_2[x1, t] -> [0, x1, 1, 2, t, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_4 + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> [x1] }' + index: '[n] -> { S_2[x1, t] -> [(x1)] }' + reference: __pet_ref_5 + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_2[x1, t] -> x2[] }' + index: '[n] -> { S_2[x1, t] -> x2[] }' + reference: __pet_ref_6 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, -1 + t] : t >= 1 }' + index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }' + reference: __pet_ref_3 + read: 1 + write: 0 +- line: 14 + domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 2, t, 1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> s[] }' + index: '[n] -> { S2[x1, t] -> s[] }' + reference: __pet_ref_8 + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> s[] }' + index: '[n] -> { S2[x1, t] -> s[] }' + reference: __pet_ref_9 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_7 + read: 1 + write: 0 +- line: 13 + domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 2, t, 2] }' + body: + type: op + operation: += + arguments: + - type: access + relation: '[n] -> { S_4[x1, t] -> x2[] }' + index: '[n] -> { S_4[x1, t] -> x2[] }' + reference: __pet_ref_11 + read: 0 + write: 1 + - type: access + relation: '[n] -> { S_4[x1, t] -> s[] }' + index: '[n] -> { S_4[x1, t] -> s[] }' + reference: __pet_ref_12 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_4[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_10 + read: 1 + write: 0 +- line: 13 + domain: '[n] -> { S_6[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_6[x1] -> [0, x1, 1, 3] }' + body: + type: op + operation: kill + arguments: + - type: access + relation: '[n] -> { S_6[x1] -> x2[] }' + index: '[n] -> { S_6[x1] -> x2[] }' + reference: __pet_ref_13 + read: 0 + write: 0 +- line: 16 + domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { R[x1] -> [0, x1, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x1] -> s[] }' + index: '[n] -> { R[x1] -> s[] }' + reference: __pet_ref_14 + read: 1 + write: 0 +implications: +- satisfied: 1 + extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : x1 >= 0 and + x1 <= -1 + n and t'' <= t and t'' >= 0 }' diff --git a/tests/for_while_inc3.c b/tests/for_while_inc3.c new file mode 100644 index 0000000..1199a67 --- /dev/null +++ b/tests/for_while_inc3.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 += n) { +S2: s = g(s); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/for_while_inc3.scop b/tests/for_while_inc3.scop new file mode 100644 index 0000000..310e101 --- /dev/null +++ b/tests/for_while_inc3.scop @@ -0,0 +1,183 @@ +start: 83 +end: 234 +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x1, t] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '[n] -> { x2[] }' + element_type: int + element_size: 4 + declared: 1 +- context: '{ : }' + extent: '[n] -> { s[] }' + element_type: int + element_size: 4 +statements: +- line: 12 + domain: '[n] -> { S1[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S1[x1] -> [0, x1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x1] -> s[] }' + index: '[n] -> { S1[x1] -> s[] }' + reference: __pet_ref_0 + read: 0 + write: 1 + - type: call + name: f +- line: 13 + domain: '[n] -> { S_5[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_5[x1] -> [0, x1, 1, 0] }' + body: + type: op + operation: kill + arguments: + - type: access + relation: '[n] -> { S_5[x1] -> x2[] }' + index: '[n] -> { S_5[x1] -> x2[] }' + reference: __pet_ref_1 + read: 0 + write: 0 +- line: 13 + domain: '[n] -> { S_1[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_1[x1] -> [0, x1, 1, 1] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x1] -> x2[] }' + index: '[n] -> { S_1[x1] -> x2[] }' + reference: __pet_ref_2 + read: 0 + write: 1 + - type: int + value: 0 +- line: 13 + domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S_2[x1, t] -> [0, x1, 1, 2, t, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_4 + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> [x1] }' + index: '[n] -> { S_2[x1, t] -> [(x1)] }' + reference: __pet_ref_5 + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_2[x1, t] -> x2[] }' + index: '[n] -> { S_2[x1, t] -> x2[] }' + reference: __pet_ref_6 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, -1 + t] : t >= 1 }' + index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }' + reference: __pet_ref_3 + read: 1 + write: 0 +- line: 14 + domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 2, t, 1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> s[] }' + index: '[n] -> { S2[x1, t] -> s[] }' + reference: __pet_ref_8 + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> s[] }' + index: '[n] -> { S2[x1, t] -> s[] }' + reference: __pet_ref_9 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_7 + read: 1 + write: 0 +- line: 13 + domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 2, t, 2] }' + body: + type: op + operation: += + arguments: + - type: access + relation: '[n] -> { S_4[x1, t] -> x2[] }' + index: '[n] -> { S_4[x1, t] -> x2[] }' + reference: __pet_ref_11 + read: 0 + write: 1 + - type: access + relation: '[n] -> { S_4[x1, t] -> [n] }' + index: '[n] -> { S_4[x1, t] -> [(n)] }' + reference: __pet_ref_12 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_4[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_10 + read: 1 + write: 0 +- line: 13 + domain: '[n] -> { S_6[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_6[x1] -> [0, x1, 1, 3] }' + body: + type: op + operation: kill + arguments: + - type: access + relation: '[n] -> { S_6[x1] -> x2[] }' + index: '[n] -> { S_6[x1] -> x2[] }' + reference: __pet_ref_13 + read: 0 + write: 0 +- line: 16 + domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { R[x1] -> [0, x1, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x1] -> s[] }' + index: '[n] -> { R[x1] -> s[] }' + reference: __pet_ref_14 + read: 1 + write: 0 +implications: +- satisfied: 1 + extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : x1 >= 0 and + x1 <= -1 + n and t'' <= t and t'' >= 0 }' diff --git a/tests/for_while_inc4.c b/tests/for_while_inc4.c new file mode 100644 index 0000000..9592fdb --- /dev/null +++ b/tests/for_while_inc4.c @@ -0,0 +1,20 @@ +int f(void); +int P(int, int); +int g(int); +void h(int); + +void foo(int n) +{ + int s; + int x2; + +#pragma scop + for (int x1 = 0; x1 < n; ++x1) { +S1: s = f(); + for (x2 = 0; P(x1, x2); x2 += n) { +S2: s = g(s); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/for_while_inc4.scop b/tests/for_while_inc4.scop new file mode 100644 index 0000000..d4cfd17 --- /dev/null +++ b/tests/for_while_inc4.scop @@ -0,0 +1,156 @@ +start: 92 +end: 239 +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x1, t] : x1 <= -1 + n and x1 >= 0 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 +- context: '{ : }' + extent: '[n] -> { x2[] }' + element_type: int + element_size: 4 +statements: +- line: 13 + domain: '[n] -> { S1[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S1[x1] -> [0, x1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x1] -> s[] }' + index: '[n] -> { S1[x1] -> s[] }' + reference: __pet_ref_0 + read: 0 + write: 1 + - type: call + name: f +- line: 14 + domain: '[n] -> { S_1[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_1[x1] -> [0, x1, 1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x1] -> x2[] }' + index: '[n] -> { S_1[x1] -> x2[] }' + reference: __pet_ref_1 + read: 0 + write: 1 + - type: int + value: 0 +- line: 14 + domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S_2[x1, t] -> [0, x1, 1, 1, t, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_3 + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> [x1] }' + index: '[n] -> { S_2[x1, t] -> [(x1)] }' + reference: __pet_ref_4 + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_2[x1, t] -> x2[] }' + index: '[n] -> { S_2[x1, t] -> x2[] }' + reference: __pet_ref_5 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, -1 + t] : t >= 1 }' + index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }' + reference: __pet_ref_2 + read: 1 + write: 0 +- line: 15 + domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 1, t, 1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> s[] }' + index: '[n] -> { S2[x1, t] -> s[] }' + reference: __pet_ref_7 + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> s[] }' + index: '[n] -> { S2[x1, t] -> s[] }' + reference: __pet_ref_8 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_6 + read: 1 + write: 0 +- line: 14 + domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 1, t, 2] }' + body: + type: op + operation: += + arguments: + - type: access + relation: '[n] -> { S_4[x1, t] -> x2[] }' + index: '[n] -> { S_4[x1, t] -> x2[] }' + reference: __pet_ref_10 + read: 0 + write: 1 + - type: access + relation: '[n] -> { S_4[x1, t] -> [n] }' + index: '[n] -> { S_4[x1, t] -> [(n)] }' + reference: __pet_ref_11 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_4[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_9 + read: 1 + write: 0 +- line: 17 + domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { R[x1] -> [0, x1, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x1] -> s[] }' + index: '[n] -> { R[x1] -> s[] }' + reference: __pet_ref_12 + read: 1 + write: 0 +implications: +- satisfied: 1 + extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : x1 >= 0 and + x1 <= -1 + n and t'' <= t and t'' >= 0 }' diff --git a/tests/for_while_init.c b/tests/for_while_init.c new file mode 100644 index 0000000..33c496d --- /dev/null +++ b/tests/for_while_init.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 = s; P(x1, x2); ++x2) { +S2: s = g(s); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/for_while_init.scop b/tests/for_while_init.scop new file mode 100644 index 0000000..77bc7d6 --- /dev/null +++ b/tests/for_while_init.scop @@ -0,0 +1,183 @@ +start: 83 +end: 231 +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x1, t] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '[n] -> { x2[] }' + element_type: int + element_size: 4 + declared: 1 +- context: '{ : }' + extent: '[n] -> { s[] }' + element_type: int + element_size: 4 +statements: +- line: 12 + domain: '[n] -> { S1[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S1[x1] -> [0, x1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x1] -> s[] }' + index: '[n] -> { S1[x1] -> s[] }' + reference: __pet_ref_0 + read: 0 + write: 1 + - type: call + name: f +- line: 13 + domain: '[n] -> { S_5[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_5[x1] -> [0, x1, 1, 0] }' + body: + type: op + operation: kill + arguments: + - type: access + relation: '[n] -> { S_5[x1] -> x2[] }' + index: '[n] -> { S_5[x1] -> x2[] }' + reference: __pet_ref_1 + read: 0 + write: 0 +- line: 13 + domain: '[n] -> { S_1[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_1[x1] -> [0, x1, 1, 1] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x1] -> x2[] }' + index: '[n] -> { S_1[x1] -> x2[] }' + reference: __pet_ref_2 + read: 0 + write: 1 + - type: access + relation: '[n] -> { S_1[x1] -> s[] }' + index: '[n] -> { S_1[x1] -> s[] }' + reference: __pet_ref_3 + read: 1 + write: 0 +- line: 13 + domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S_2[x1, t] -> [0, x1, 1, 2, t, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_5 + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> [x1] }' + index: '[n] -> { S_2[x1, t] -> [(x1)] }' + reference: __pet_ref_6 + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_2[x1, t] -> x2[] }' + index: '[n] -> { S_2[x1, t] -> x2[] }' + reference: __pet_ref_7 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, -1 + t] : t >= 1 }' + index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }' + reference: __pet_ref_4 + read: 1 + write: 0 +- line: 14 + domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 2, t, 1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> s[] }' + index: '[n] -> { S2[x1, t] -> s[] }' + reference: __pet_ref_9 + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> s[] }' + index: '[n] -> { S2[x1, t] -> s[] }' + reference: __pet_ref_10 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_8 + read: 1 + write: 0 +- line: 13 + domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 2, t, 2] }' + body: + type: op + operation: += + arguments: + - type: access + relation: '[n] -> { S_4[x1, t] -> x2[] }' + index: '[n] -> { S_4[x1, t] -> x2[] }' + reference: __pet_ref_12 + read: 0 + write: 1 + - type: int + value: 1 + arguments: + - type: access + relation: '[n] -> { S_4[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_11 + read: 1 + write: 0 +- line: 13 + domain: '[n] -> { S_6[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_6[x1] -> [0, x1, 1, 3] }' + body: + type: op + operation: kill + arguments: + - type: access + relation: '[n] -> { S_6[x1] -> x2[] }' + index: '[n] -> { S_6[x1] -> x2[] }' + reference: __pet_ref_13 + read: 0 + write: 0 +- line: 16 + domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { R[x1] -> [0, x1, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x1] -> s[] }' + index: '[n] -> { R[x1] -> s[] }' + reference: __pet_ref_14 + read: 1 + write: 0 +implications: +- satisfied: 1 + extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : x1 >= 0 and + x1 <= -1 + n and t'' <= t and t'' >= 0 }' diff --git a/tests/for_while_init2.c b/tests/for_while_init2.c new file mode 100644 index 0000000..b69c01d --- /dev/null +++ b/tests/for_while_init2.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 = s; P(x1, x2); x2 += s) { +S2: s = g(s); + } +R: h(s); + } +#pragma endscop +} diff --git a/tests/for_while_init2.scop b/tests/for_while_init2.scop new file mode 100644 index 0000000..6f2f8d2 --- /dev/null +++ b/tests/for_while_init2.scop @@ -0,0 +1,187 @@ +start: 83 +end: 234 +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[x1, t] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '[n] -> { x2[] }' + element_type: int + element_size: 4 + declared: 1 +- context: '{ : }' + extent: '[n] -> { s[] }' + element_type: int + element_size: 4 +statements: +- line: 12 + domain: '[n] -> { S1[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S1[x1] -> [0, x1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S1[x1] -> s[] }' + index: '[n] -> { S1[x1] -> s[] }' + reference: __pet_ref_0 + read: 0 + write: 1 + - type: call + name: f +- line: 13 + domain: '[n] -> { S_5[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_5[x1] -> [0, x1, 1, 0] }' + body: + type: op + operation: kill + arguments: + - type: access + relation: '[n] -> { S_5[x1] -> x2[] }' + index: '[n] -> { S_5[x1] -> x2[] }' + reference: __pet_ref_1 + read: 0 + write: 0 +- line: 13 + domain: '[n] -> { S_1[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_1[x1] -> [0, x1, 1, 1] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[x1] -> x2[] }' + index: '[n] -> { S_1[x1] -> x2[] }' + reference: __pet_ref_2 + read: 0 + write: 1 + - type: access + relation: '[n] -> { S_1[x1] -> s[] }' + index: '[n] -> { S_1[x1] -> s[] }' + reference: __pet_ref_3 + read: 1 + write: 0 +- line: 13 + domain: '[n] -> { [S_2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S_2[x1, t] -> [0, x1, 1, 2, t, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_5 + read: 0 + write: 1 + - type: call + name: P + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> [x1] }' + index: '[n] -> { S_2[x1, t] -> [(x1)] }' + reference: __pet_ref_6 + read: 1 + write: 0 + - type: access + relation: '[n] -> { S_2[x1, t] -> x2[] }' + index: '[n] -> { S_2[x1, t] -> x2[] }' + reference: __pet_ref_7 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_2[x1, t] -> __pet_test_0[x1, -1 + t] : t >= 1 }' + index: '[n] -> { S_2[x1, t] -> __pet_test_0[(x1), ((-1 + t) : t >= 1)] }' + reference: __pet_ref_4 + read: 1 + write: 0 +- line: 14 + domain: '[n] -> { [S2[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S2[x1, t] -> [0, x1, 1, 2, t, 1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> s[] }' + index: '[n] -> { S2[x1, t] -> s[] }' + reference: __pet_ref_9 + read: 0 + write: 1 + - type: call + name: g + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> s[] }' + index: '[n] -> { S2[x1, t] -> s[] }' + reference: __pet_ref_10 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S2[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S2[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_8 + read: 1 + write: 0 +- line: 13 + domain: '[n] -> { [S_4[x1, t] -> [1]] : x1 <= -1 + n and x1 >= 0 and t >= 0 }' + schedule: '[n] -> { S_4[x1, t] -> [0, x1, 1, 2, t, 2] }' + body: + type: op + operation: += + arguments: + - type: access + relation: '[n] -> { S_4[x1, t] -> x2[] }' + index: '[n] -> { S_4[x1, t] -> x2[] }' + reference: __pet_ref_12 + read: 0 + write: 1 + - type: access + relation: '[n] -> { S_4[x1, t] -> s[] }' + index: '[n] -> { S_4[x1, t] -> s[] }' + reference: __pet_ref_13 + read: 1 + write: 0 + arguments: + - type: access + relation: '[n] -> { S_4[x1, t] -> __pet_test_0[x1, t] }' + index: '[n] -> { S_4[x1, t] -> __pet_test_0[(x1), (t)] }' + reference: __pet_ref_11 + read: 1 + write: 0 +- line: 13 + domain: '[n] -> { S_6[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { S_6[x1] -> [0, x1, 1, 3] }' + body: + type: op + operation: kill + arguments: + - type: access + relation: '[n] -> { S_6[x1] -> x2[] }' + index: '[n] -> { S_6[x1] -> x2[] }' + reference: __pet_ref_14 + read: 0 + write: 0 +- line: 16 + domain: '[n] -> { R[x1] : x1 <= -1 + n and x1 >= 0 }' + schedule: '[n] -> { R[x1] -> [0, x1, 2] }' + body: + type: call + name: h + arguments: + - type: access + relation: '[n] -> { R[x1] -> s[] }' + index: '[n] -> { R[x1] -> s[] }' + reference: __pet_ref_15 + read: 1 + write: 0 +implications: +- satisfied: 1 + extension: '[n] -> { __pet_test_0[x1, t] -> __pet_test_0[x1, t''] : x1 >= 0 and + x1 <= -1 + n and t'' <= t and t'' >= 0 }' diff --git a/tests/for_while_init3.c b/tests/for_while_init3.c new file mode 100644 index 0000000..21f47af --- /dev/null +++ b/tests/for_while_init3.c @@ -0,0 +1,11 @@ +void foo(int n, int A[n]) +{ + int s; + +#pragma scop + s = 0; + for (int i = 0; i < n; ++i) + for (int j = A[i]; j < 10; ++j) + s++; +#pragma endscop +} diff --git a/tests/for_while_init3.scop b/tests/for_while_init3.scop new file mode 100644 index 0000000..316d16b --- /dev/null +++ b/tests/for_while_init3.scop @@ -0,0 +1,161 @@ +start: 37 +end: 145 +context: '[n] -> { : n <= 2147483647 and n >= -2147483648 }' +arrays: +- context: '{ : }' + extent: '[n] -> { __pet_test_0[i, t] : i <= -1 + n and i >= 0 and t >= 0 }' + value_bounds: '{ [i0] : i0 >= 0 and i0 <= 1 }' + element_type: int + element_size: 4 + uniquely_defined: 1 +- context: '{ : }' + extent: '[n] -> { j[] }' + element_type: int + element_size: 4 + declared: 1 +- context: '{ : }' + extent: '[n] -> { A[i0] : i0 >= 0 }' + element_type: int + element_size: 4 +- context: '{ : }' + extent: '[n] -> { s[] }' + element_type: int + element_size: 4 +statements: +- line: 6 + domain: '[n] -> { S_0[] }' + schedule: '{ S_0[] -> [0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_0[] -> s[] }' + index: '[n] -> { S_0[] -> s[] }' + reference: __pet_ref_0 + read: 0 + write: 1 + - type: int + value: 0 +- line: 8 + domain: '[n] -> { S_5[i] : i <= -1 + n and i >= 0 }' + schedule: '[n] -> { S_5[i] -> [1, i, 0] }' + body: + type: op + operation: kill + arguments: + - type: access + relation: '[n] -> { S_5[i] -> j[] }' + index: '[n] -> { S_5[i] -> j[] }' + reference: __pet_ref_1 + read: 0 + write: 0 +- line: 8 + domain: '[n] -> { S_1[i] : i <= -1 + n and i >= 0 }' + schedule: '[n] -> { S_1[i] -> [1, i, 1] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_1[i] -> j[] }' + index: '[n] -> { S_1[i] -> j[] }' + reference: __pet_ref_2 + read: 0 + write: 1 + - type: access + relation: '[n] -> { S_1[i] -> A[i] }' + index: '[n] -> { S_1[i] -> A[(i)] }' + reference: __pet_ref_3 + read: 1 + write: 0 +- line: 8 + domain: '[n] -> { [S_2[i, t] -> [1]] : i <= -1 + n and i >= 0 and t >= 0 }' + schedule: '[n] -> { S_2[i, t] -> [1, i, 2, t, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[n] -> { S_2[i, t] -> __pet_test_0[i, t] }' + index: '[n] -> { S_2[i, t] -> __pet_test_0[(i), (t)] }' + reference: __pet_ref_5 + read: 0 + write: 1 + - type: op + operation: < + arguments: + - type: access + relation: '[n] -> { S_2[i, t] -> j[] }' + index: '[n] -> { S_2[i, t] -> j[] }' + reference: __pet_ref_6 + read: 1 + write: 0 + - type: int + value: 10 + arguments: + - type: access + relation: '[n] -> { S_2[i, t] -> __pet_test_0[i, -1 + t] : t >= 1 }' + index: '[n] -> { S_2[i, t] -> __pet_test_0[(i), ((-1 + t) : t >= 1)] }' + reference: __pet_ref_4 + read: 1 + write: 0 +- line: 9 + domain: '[n] -> { [S_3[i, t] -> [1]] : i <= -1 + n and i >= 0 and t >= 0 }' + schedule: '[n] -> { S_3[i, t] -> [1, i, 2, t, 1] }' + body: + type: op + operation: ++ + arguments: + - type: access + relation: '[n] -> { S_3[i, t] -> s[] }' + index: '[n] -> { S_3[i, t] -> s[] }' + reference: __pet_ref_8 + read: 1 + write: 1 + arguments: + - type: access + relation: '[n] -> { S_3[i, t] -> __pet_test_0[i, t] }' + index: '[n] -> { S_3[i, t] -> __pet_test_0[(i), (t)] }' + reference: __pet_ref_7 + read: 1 + write: 0 +- line: 8 + domain: '[n] -> { [S_4[i, t] -> [1]] : i <= -1 + n and i >= 0 and t >= 0 }' + schedule: '[n] -> { S_4[i, t] -> [1, i, 2, t, 2] }' + body: + type: op + operation: += + arguments: + - type: access + relation: '[n] -> { S_4[i, t] -> j[] }' + index: '[n] -> { S_4[i, t] -> j[] }' + reference: __pet_ref_10 + read: 0 + write: 1 + - type: int + value: 1 + arguments: + - type: access + relation: '[n] -> { S_4[i, t] -> __pet_test_0[i, t] }' + index: '[n] -> { S_4[i, t] -> __pet_test_0[(i), (t)] }' + reference: __pet_ref_9 + read: 1 + write: 0 +- line: 8 + domain: '[n] -> { S_6[i] : i <= -1 + n and i >= 0 }' + schedule: '[n] -> { S_6[i] -> [1, i, 3] }' + body: + type: op + operation: kill + arguments: + - type: access + relation: '[n] -> { S_6[i] -> j[] }' + index: '[n] -> { S_6[i] -> j[] }' + reference: __pet_ref_11 + read: 0 + write: 0 +implications: +- satisfied: 1 + extension: '[n] -> { __pet_test_0[i, t] -> __pet_test_0[i, t''] : i >= 0 and i <= + -1 + n and t'' <= t and t'' >= 0 }' diff --git a/tests/inc5.c b/tests/inc5.c new file mode 100644 index 0000000..dcf7bb0 --- /dev/null +++ b/tests/inc5.c @@ -0,0 +1,11 @@ +void foo(int N) +{ + int i; + int a[N]; + +#pragma scop + i = 0; + for (i = 0; i < N; i += i) + a[i] = i; +#pragma endscop +} diff --git a/tests/inc5.scop b/tests/inc5.scop new file mode 100644 index 0000000..d995df9 --- /dev/null +++ b/tests/inc5.scop @@ -0,0 +1,150 @@ +start: 38 +end: 115 +context: '[N] -> { : N >= 0 and N <= 2147483647 }' +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] -> { N[] }' + element_type: int + element_size: 4 +- context: '[N] -> { : N >= 0 }' + extent: '[N] -> { a[i0] : i0 <= -1 + N and i0 >= 0 }' + element_type: int + element_size: 4 +- context: '{ : }' + extent: '[N] -> { i[] }' + element_type: int + element_size: 4 +statements: +- line: 7 + domain: '[N] -> { S_0[] }' + schedule: '{ S_0[] -> [0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[N] -> { S_0[] -> i[] }' + index: '[N] -> { S_0[] -> i[] }' + reference: __pet_ref_0 + read: 0 + write: 1 + - type: int + value: 0 +- line: 8 + domain: '[N] -> { S_1[] }' + schedule: '{ S_1[] -> [1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[N] -> { S_1[] -> i[] }' + index: '[N] -> { S_1[] -> i[] }' + reference: __pet_ref_1 + read: 0 + write: 1 + - type: int + value: 0 +- line: 8 + domain: '[N] -> { [S_2[t] -> [1]] : t >= 0 }' + schedule: '{ S_2[t] -> [1, 1, t, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[N] -> { S_2[t] -> __pet_test_0[t] }' + index: '[N] -> { S_2[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_3 + read: 0 + write: 1 + - type: op + operation: < + arguments: + - type: access + relation: '[N] -> { S_2[t] -> i[] }' + index: '[N] -> { S_2[t] -> i[] }' + reference: __pet_ref_4 + read: 1 + write: 0 + - type: access + relation: '[N] -> { S_2[t] -> N[] }' + index: '[N] -> { S_2[t] -> N[] }' + reference: __pet_ref_5 + read: 1 + write: 0 + arguments: + - type: access + relation: '[N] -> { S_2[t] -> __pet_test_0[-1 + t] : t >= 1 }' + index: '[N] -> { S_2[t] -> __pet_test_0[((-1 + t) : t >= 1)] }' + reference: __pet_ref_2 + read: 1 + write: 0 +- line: 9 + domain: '[N] -> { [S_3[t] -> [1]] : t >= 0 }' + schedule: '{ S_3[t] -> [1, 1, t, 1] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '[N] -> { [S_3[t] -> [i1]] -> a[i1] : i1 >= 0 }' + index: '[N] -> { [S_3[t] -> [i1]] -> a[((i1) : i1 >= 0)] }' + reference: __pet_ref_8 + read: 0 + write: 1 + arguments: + - type: access + relation: '[N] -> { S_3[t] -> i[] }' + index: '[N] -> { S_3[t] -> i[] }' + reference: __pet_ref_7 + read: 1 + write: 0 + - type: access + relation: '[N] -> { S_3[t] -> i[] }' + index: '[N] -> { S_3[t] -> i[] }' + reference: __pet_ref_9 + read: 1 + write: 0 + arguments: + - type: access + relation: '[N] -> { S_3[t] -> __pet_test_0[t] }' + index: '[N] -> { S_3[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_6 + read: 1 + write: 0 +- line: 8 + domain: '[N] -> { [S_4[t] -> [1]] : t >= 0 }' + schedule: '{ S_4[t] -> [1, 1, t, 2] }' + body: + type: op + operation: += + arguments: + - type: access + relation: '[N] -> { S_4[t] -> i[] }' + index: '[N] -> { S_4[t] -> i[] }' + reference: __pet_ref_11 + read: 0 + write: 1 + - type: access + relation: '[N] -> { S_4[t] -> i[] }' + index: '[N] -> { S_4[t] -> i[] }' + reference: __pet_ref_12 + read: 1 + write: 0 + arguments: + - type: access + relation: '[N] -> { S_4[t] -> __pet_test_0[t] }' + index: '[N] -> { S_4[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_10 + read: 1 + write: 0 +implications: +- satisfied: 1 + extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }' diff --git a/tests/loop7.c b/tests/loop7.c new file mode 100644 index 0000000..32d641b --- /dev/null +++ b/tests/loop7.c @@ -0,0 +1,13 @@ +int f(); + +void foo() +{ + int i; + int a; + +#pragma scop + i = f(); + for (i = i; i < 10; ++i) + a = 5; +#pragma endscop +} diff --git a/tests/loop7.scop b/tests/loop7.scop new file mode 100644 index 0000000..04b2f1c --- /dev/null +++ b/tests/loop7.scop @@ -0,0 +1,131 @@ +start: 40 +end: 114 +context: '{ : }' +arrays: +- context: '{ : }' + extent: '{ __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: '{ a[] }' + element_type: int + element_size: 4 +- context: '{ : }' + extent: '{ i[] }' + element_type: int + element_size: 4 +statements: +- line: 9 + domain: '{ S_0[] }' + schedule: '{ S_0[] -> [0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ S_0[] -> i[] }' + index: '{ S_0[] -> i[] }' + reference: __pet_ref_0 + read: 0 + write: 1 + - type: call + name: f +- line: 10 + domain: '{ S_1[] }' + schedule: '{ S_1[] -> [1, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ S_1[] -> i[] }' + index: '{ S_1[] -> i[] }' + reference: __pet_ref_1 + read: 0 + write: 1 + - type: access + relation: '{ S_1[] -> i[] }' + index: '{ S_1[] -> i[] }' + reference: __pet_ref_2 + read: 1 + write: 0 +- line: 10 + domain: '{ [S_2[t] -> [1]] : t >= 0 }' + schedule: '{ S_2[t] -> [1, 1, t, 0] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ S_2[t] -> __pet_test_0[t] }' + index: '{ S_2[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_4 + read: 0 + write: 1 + - type: op + operation: < + arguments: + - type: access + relation: '{ S_2[t] -> i[] }' + index: '{ S_2[t] -> i[] }' + reference: __pet_ref_5 + read: 1 + write: 0 + - type: int + value: 10 + arguments: + - type: access + relation: '{ S_2[t] -> __pet_test_0[-1 + t] : t >= 1 }' + index: '{ S_2[t] -> __pet_test_0[((-1 + t) : t >= 1)] }' + reference: __pet_ref_3 + read: 1 + write: 0 +- line: 11 + domain: '{ [S_3[t] -> [1]] : t >= 0 }' + schedule: '{ S_3[t] -> [1, 1, t, 1] }' + body: + type: op + operation: = + arguments: + - type: access + relation: '{ S_3[t] -> a[] }' + index: '{ S_3[t] -> a[] }' + reference: __pet_ref_7 + read: 0 + write: 1 + - type: int + value: 5 + arguments: + - type: access + relation: '{ S_3[t] -> __pet_test_0[t] }' + index: '{ S_3[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_6 + read: 1 + write: 0 +- line: 10 + domain: '{ [S_4[t] -> [1]] : t >= 0 }' + schedule: '{ S_4[t] -> [1, 1, t, 2] }' + body: + type: op + operation: += + arguments: + - type: access + relation: '{ S_4[t] -> i[] }' + index: '{ S_4[t] -> i[] }' + reference: __pet_ref_9 + read: 0 + write: 1 + - type: int + value: 1 + arguments: + - type: access + relation: '{ S_4[t] -> __pet_test_0[t] }' + index: '{ S_4[t] -> __pet_test_0[(t)] }' + reference: __pet_ref_8 + read: 1 + write: 0 +implications: +- satisfied: 1 + extension: '{ __pet_test_0[t] -> __pet_test_0[t''] : t'' <= t and t'' >= 0 }' -- 2.11.4.GIT