From 0d38ab7bcba2f12ef5c3e349d24c3b325eaa9466 Mon Sep 17 00:00:00 2001 From: Sven Verdoolaege Date: Mon, 24 Mar 2014 12:21:40 +0100 Subject: [PATCH] derive access relations of call expressions from function summary In previous commits, we have added the infrastructure to store and extract function summaries from function bodies. In this commit, we exploit this information to derive access relations from the function summaries whenever they are available. This allows for an extraction of more accurate access relations than those based on the default heuristic that the entire array slice passed to the function is either read or written, which may not only be wildly inaccurate, but it may also be wrong. Signed-off-by: Sven Verdoolaege --- context.c | 590 ++++++++++++++++++++++++++++++++++++++++++++++++- tests/call1.c | 14 ++ tests/call1.scop | 49 ++++ tests/call2.c | 17 ++ tests/call2.scop | 40 ++++ tests/call3.c | 14 ++ tests/call3.scop | 46 ++++ tests/call4.c | 17 ++ tests/call4.scop | 46 ++++ tests/call5.c | 13 ++ tests/call5.scop | 44 ++++ tests/call_struct.c | 35 +++ tests/call_struct.scop | 101 +++++++++ 13 files changed, 1023 insertions(+), 3 deletions(-) create mode 100644 tests/call1.c create mode 100644 tests/call1.scop create mode 100644 tests/call2.c create mode 100644 tests/call2.scop create mode 100644 tests/call3.c create mode 100644 tests/call3.scop create mode 100644 tests/call4.c create mode 100644 tests/call4.scop create mode 100644 tests/call5.c create mode 100644 tests/call5.scop create mode 100644 tests/call_struct.c create mode 100644 tests/call_struct.scop diff --git a/context.c b/context.c index 515c7a5..6ad85d4 100644 --- a/context.c +++ b/context.c @@ -35,6 +35,7 @@ #include #include "aff.h" +#include "array.h" #include "context.h" #include "expr.h" #include "expr_arg.h" @@ -509,19 +510,602 @@ static __isl_give pet_expr *plug_in_affine_read(__isl_take pet_expr *expr, return pet_expr_map_access(expr, &access_plug_in_affine_read, pc); } +/* Add an extra affine expression to "mpa" that is equal to + * an extra dimension in the range of the wrapped relation in the domain + * of "mpa". "n_arg" is the original number of dimensions in this range. + * + * That is, if "n_arg" is 0, then the input has the form + * + * D(i) -> [f(i)] + * + * and the output has the form + * + * [D(i) -> [y]] -> [f(i), y] + * + * If "n_arg" is different from 0, then the input has the form + * + * [D(i) -> [x]] -> [f(i,x)] + * + * with x consisting of "n_arg" dimensions, and the output has the form + * + * [D(i) -> [x,y]] -> [f(i,x), y] + * + * + * We first adjust the domain of "mpa" and then add the extra + * affine expression (y). + */ +static __isl_give isl_multi_pw_aff *add_arg(__isl_take isl_multi_pw_aff *mpa, + int n_arg) +{ + int dim; + isl_space *space; + isl_multi_aff *ma; + isl_multi_pw_aff *mpa2; + + if (n_arg == 0) { + space = isl_space_domain(isl_multi_pw_aff_get_space(mpa)); + dim = isl_space_dim(space, isl_dim_set); + space = isl_space_from_domain(space); + space = isl_space_add_dims(space, isl_dim_set, 1); + ma = isl_multi_aff_domain_map(space); + } else { + isl_multi_aff *ma2;; + isl_space *dom, *ran; + + space = isl_space_domain(isl_multi_pw_aff_get_space(mpa)); + space = isl_space_unwrap(space); + dom = isl_space_domain(isl_space_copy(space)); + dim = isl_space_dim(dom, isl_dim_set); + ran = isl_space_range(space); + ran = isl_space_add_dims(ran, isl_dim_set, 1); + space = isl_space_map_from_set(dom); + ma = isl_multi_aff_identity(space); + ma2 = isl_multi_aff_project_out_map(ran, isl_dim_set, n_arg, 1); + ma = isl_multi_aff_product(ma, ma2); + } + + mpa = isl_multi_pw_aff_pullback_multi_aff(mpa, ma); + space = isl_space_domain(isl_multi_pw_aff_get_space(mpa)); + ma = isl_multi_aff_project_out_map(space, isl_dim_set, 0, dim + n_arg); + mpa2 = isl_multi_pw_aff_from_multi_aff(ma); + mpa = isl_multi_pw_aff_flat_range_product(mpa, mpa2); + + return mpa; +} + +/* Add the integer value from "arg" to "mpa". + */ +static __isl_give isl_multi_pw_aff *add_int(__isl_take isl_multi_pw_aff *mpa, + __isl_take pet_expr *arg) +{ + isl_space *space; + isl_val *v; + isl_aff *aff; + isl_multi_pw_aff *mpa_arg; + + v = pet_expr_int_get_val(arg); + pet_expr_free(arg); + + space = isl_space_domain(isl_multi_pw_aff_get_space(mpa)); + aff = isl_aff_val_on_domain(isl_local_space_from_space(space), v); + mpa_arg = isl_multi_pw_aff_from_pw_aff(isl_pw_aff_from_aff(aff)); + + mpa = isl_multi_pw_aff_flat_range_product(mpa, mpa_arg); + + return mpa; +} + +/* Add the affine expression from "arg" to "mpa". + * "n_arg" is the number of dimensions in the range of the wrapped + * relation in the domain of "mpa". + */ +static __isl_give isl_multi_pw_aff *add_aff(__isl_take isl_multi_pw_aff *mpa, + int n_arg, __isl_take pet_expr *arg) +{ + isl_multi_pw_aff *mpa_arg; + + mpa_arg = pet_expr_access_get_index(arg); + pet_expr_free(arg); + + if (n_arg > 0) { + isl_space *space; + isl_multi_aff *ma; + + space = isl_space_domain(isl_multi_pw_aff_get_space(mpa)); + space = isl_space_unwrap(space); + ma = isl_multi_aff_domain_map(space); + mpa_arg = isl_multi_pw_aff_pullback_multi_aff(mpa_arg, ma); + } + + mpa = isl_multi_pw_aff_flat_range_product(mpa, mpa_arg); + + return mpa; +} + +/* Given the data space "space1" of an index expression passed + * to a function and the data space "space2" of the corresponding + * array accessed in the function, construct and return the complete + * data space from the perspective of the function call. + * If add is set, then it is not the index expression with space "space1" itself + * that is passed to the function, but its address. + * + * In the simplest case, no member accesses are involved and "add" is not set. + * Let "space1" be of the form A[x] and "space2" of the form B[y]. + * Then the returned space is A[x,y]. + * That is, the dimension is the sum of the dimensions and the name + * is that of "space1". + * If "add" is set, then the final dimension of "space1" is the same + * as the initial dimension of "space2" and the dimension of the result + * is one less that the sum. This also applies when the dimension + * of "space1" is zero. The dimension of "space2" can never be zero + * when "add" is set since a pointer value is passed to the function, + * which is treated as an array of dimension at least 1. + * + * If "space1" involves any member accesses, then it is the innermost + * array space of "space1" that needs to be extended with "space2". + * This innermost array space appears in the range of the wrapped + * relation in "space1". + * + * If "space2" involves any member accesses, then it is the outermost + * array space of "space2" that needs to be combined with innermost + * array space of "space1". This outermost array space appears + * in the deepest nesting of the domains and is therefore handled + * recursively. + * + * For example, if "space1" is of the form + * + * s_a[s[x] -> a[y]] + * + * and "space2" is of the form + * + * d_b_c[d_b[d[z] -> b[u]] -> c[v]] + * + * then the resulting space is + * + * s_a_b_c[s_a_b[s_a[s[x] -> a[y,z]] -> b[u]] -> c[v]] + */ +static __isl_give isl_space *patch_space(__isl_take isl_space *space1, + __isl_take isl_space *space2, int add) +{ + int dim; + isl_id *id; + + if (!space1 || !space2) + goto error; + + if (isl_space_is_wrapping(space2)) { + isl_ctx *ctx; + isl_space *dom; + const char *name1, *name2; + char *name; + + ctx = isl_space_get_ctx(space1); + space2 = isl_space_unwrap(space2); + dom = isl_space_domain(isl_space_copy(space2)); + space1 = patch_space(space1, dom, add); + space2 = isl_space_range(space2); + name1 = isl_space_get_tuple_name(space1, isl_dim_set); + name2 = isl_space_get_tuple_name(space2, isl_dim_set); + name = pet_array_member_access_name(ctx, name1, name2); + space1 = isl_space_product(space1, space2); + space1 = isl_space_set_tuple_name(space1, isl_dim_set, name); + free(name); + return space1; + } + + dim = isl_space_dim(space2, isl_dim_set) - add; + id = isl_space_get_tuple_id(space1, isl_dim_set); + if (isl_space_is_wrapping(space1)) { + isl_id *id; + + space1 = isl_space_unwrap(space1); + id = isl_space_get_tuple_id(space1, isl_dim_out); + space1 = isl_space_add_dims(space1, isl_dim_out, dim); + space1 = isl_space_set_tuple_id(space1, isl_dim_out, id); + space1 = isl_space_wrap(space1); + } else { + space1 = isl_space_add_dims(space1, isl_dim_out, dim); + } + space1 = isl_space_set_tuple_id(space1, isl_dim_set, id); + + isl_space_free(space2); + return space1; +error: + isl_space_free(space1); + isl_space_free(space2); + return NULL; +} + +/* Drop the initial dimension of "map", assuming that it is equal to zero. + * If it turns out not to be equal to zero, then drop the initial dimension + * of "map" after setting the value to zero and print a warning. + */ +static __isl_give isl_map *drop_initial_zero(__isl_take isl_map *map, + __isl_keep isl_map *prefix) +{ + isl_map *zeroed; + + zeroed = isl_map_copy(map); + zeroed = isl_map_fix_si(zeroed, isl_dim_out, 0, 0); + map = isl_map_subtract(map, isl_map_copy(zeroed)); + if (!isl_map_is_empty(map)) { + fprintf(stderr, "possible out-of-bounds accesses\n"); + isl_map_dump(map); + fprintf(stderr, "when passing\n"); + isl_map_dump(prefix); + } + isl_map_free(map); + map = zeroed; + map = isl_map_project_out(map, isl_dim_out, 0, 1); + return map; +} + +/* Given an identity mapping "id" that adds structure to + * the range of "map" with dimensions "pos" and "pos + 1" replaced + * by their sum, adjust "id" to apply to the range of "map" directly. + * That is, plug in + * + * [i_0, ..., i_pos, i_{pos+1}, i_{pos+2}, ...] -> + * [i_0, ..., i_pos + i_{pos+1}, i_{pos+2}, ...] + * + * in "id", where the domain of this mapping corresponds to the range + * of "map" and the range of this mapping corresponds to the original + * domain of "id". + */ +static __isl_give isl_map *patch_map_add(__isl_take isl_map *id, + __isl_keep isl_map *map, int pos) +{ + isl_space *space; + isl_multi_aff *ma; + isl_aff *aff1, *aff2; + + space = isl_space_range(isl_map_get_space(map)); + ma = isl_multi_aff_identity(isl_space_map_from_set(space)); + aff1 = isl_multi_aff_get_aff(ma, pos); + aff2 = isl_multi_aff_get_aff(ma, pos + 1); + aff1 = isl_aff_add(aff1, aff2); + ma = isl_multi_aff_set_aff(ma, pos, aff1); + ma = isl_multi_aff_drop_dims(ma, isl_dim_out, pos + 1, 1); + id = isl_map_preimage_domain_multi_aff(id, ma); + + return id; +} + +/* Return the dimension of the innermost array in the data space "space". + * If "space" is not a wrapping space, the it does not involve any + * member accesses and the innermost array is simply the accessed + * array itself. + * Otherwise, the innermost array is encoded in the range of the + * wrapped space. + */ +static int innermost_dim(__isl_keep isl_space *space) +{ + int dim; + + if (!isl_space_is_wrapping(space)) + return isl_space_dim(space, isl_dim_set); + + space = isl_space_copy(space); + space = isl_space_unwrap(space); + dim = isl_space_dim(space, isl_dim_out); + isl_space_free(space); + + return dim; +} + +/* Internal data structure for patch_map. + * + * "prefix" is the index expression passed to the function + * "add" is set if it is the address of "prefix" that is passed to the function. + * "res" collects the results. + */ +struct pet_patch_map_data { + isl_map *prefix; + int add; + + isl_union_map *res; +}; + +/* Combine the index expression data->prefix with the subaccess relation "map". + * If data->add is set, then it is not the index expression data->prefix itself + * that is passed to the function, but its address. + * + * If data->add is not set, then we essentially need to concatenate + * data->prefix with map, except that we need to make sure that + * the target space is set correctly. This target space is computed + * by the function patch_space. We then simply compute the flat + * range product and subsequently reset the target space. + * + * If data->add is set then the outer dimension of "map" is an offset + * with respect to the inner dimension of data->prefix and we therefore + * need to add these two dimensions rather than simply concatenating them. + * This computation is performed in patch_map_add. + * If however, the innermost accessed array of data->prefix is + * zero-dimensional, then there is no innermost dimension of data->prefix + * to add to the outermost dimension of "map", Instead, we are passing + * a pointer to a scalar member, meaning that the outermost dimension + * of "map" needs to be zero and that this zero needs to be removed + * from the concatenation. This computation is performed in drop_initial_zero. + */ +static int patch_map(__isl_take isl_map *map, void *user) +{ + struct pet_patch_map_data *data = user; + isl_space *space; + isl_map *id; + int pos, dim; + + space = isl_space_range(isl_map_get_space(data->prefix)); + dim = innermost_dim(space); + pos = isl_space_dim(space, isl_dim_set) - dim; + space = patch_space(space, isl_space_range(isl_map_get_space(map)), + data->add); + if (data->add && dim == 0) + map = drop_initial_zero(map, data->prefix); + map = isl_map_flat_range_product(isl_map_copy(data->prefix), map); + space = isl_space_map_from_set(space); + space = isl_space_add_dims(space, isl_dim_in, 0); + id = isl_map_identity(space); + if (data->add && dim != 0) + id = patch_map_add(id, map, pos + dim - 1); + map = isl_map_apply_range(map, id); + data->res = isl_union_map_add_map(data->res, map); + + return 0; +} + +/* Combine the index expression of "expr" with the subaccess relation "access". + * If "add" is set, then it is not the index expression of "expr" itself + * that is passed to the function, but its address. + * + * We call patch_map on each map in "access" and return the combined results. + */ +static __isl_give isl_union_map *patch(__isl_take isl_union_map *access, + __isl_keep pet_expr *expr, int add) +{ + struct pet_patch_map_data data; + isl_map *map; + + map = isl_map_from_multi_pw_aff(pet_expr_access_get_index(expr)); + data.prefix = map; + data.add = add; + data.res = isl_union_map_empty(isl_union_map_get_space(access)); + if (isl_union_map_foreach_map(access, &patch_map, &data) < 0) + data.res = isl_union_map_free(data.res); + isl_union_map_free(access); + isl_map_free(data.prefix); + + return data.res; +} + +/* Set the access relations of "expr", which appears in the argument + * at position "pos" in a call expression by composing the access + * relations in "summary" with the expression "int_arg" of the integer + * arguments in terms of the domain and expression arguments of "expr" and + * combining the result with the index expression passed to the function. + * If "add" is set, then it is not "expr" itself that is passed + * to the function, but the address of "expr". + * + * We reset the read an write flag of "expr" and rely on + * pet_expr_access_set_access setting the flags based on + * the access relations. + * + * After relating each access relation of the called function + * to the domain and expression arguments at the call site, + * the result is combined with the index expression by the function patch + * and then stored in the access expression. + */ +static __isl_give pet_expr *set_access_relations(__isl_take pet_expr *expr, + __isl_keep pet_function_summary *summary, int pos, + __isl_take isl_multi_pw_aff *int_arg, int add) +{ + enum pet_expr_access_type type; + + expr = pet_expr_access_set_read(expr, 0); + expr = pet_expr_access_set_write(expr, 0); + for (type = pet_expr_access_begin; type < pet_expr_access_end; ++type) { + isl_union_map *access; + + access = pet_function_summary_arg_get_access(summary, + pos, type); + access = isl_union_map_preimage_domain_multi_pw_aff(access, + isl_multi_pw_aff_copy(int_arg)); + access = patch(access, expr, add); + expr = pet_expr_access_set_access(expr, type, access); + } + isl_multi_pw_aff_free(int_arg); + + return expr; +} + +/* Set the access relations of "arg", which appears in the argument + * at position "pos" in the call expression "call" based on the + * information in "summary". + * If "add" is set, then it is not "arg" itself that is passed + * to the function, but the address of "arg". + * + * We create an affine function "int_arg" that expresses + * the integer function call arguments in terms of the domain of "arg" + * (i.e., the outer loop iterators) and the expression arguments. + * If the actual argument is not an affine expression or if it itself + * has expression arguments, then it is added as an argument to "arg" and + * "int_arg" is made to reference this additional expression argument. + * + * Finally, we call set_access_relations to plug in the actual arguments + * (expressed in "int_arg") into the access relations in "summary" and + * to add the resulting access relations to "arg". + */ +static __isl_give pet_expr *access_plug_in_summary(__isl_take pet_expr *arg, + __isl_keep pet_expr *call, __isl_keep pet_function_summary *summary, + int pos, int add) +{ + int j, n; + isl_space *space; + isl_multi_pw_aff *int_arg; + int arg_n_arg; + + space = pet_expr_access_get_augmented_domain_space(arg); + space = isl_space_from_domain(space); + arg_n_arg = pet_expr_get_n_arg(arg); + int_arg = isl_multi_pw_aff_zero(space); + n = pet_function_summary_get_n_arg(summary); + for (j = 0; j < n; ++j) { + pet_expr *arg_j; + int arg_j_n_arg; + + if (!pet_function_summary_arg_is_int(summary, j)) + continue; + + arg_j = pet_expr_get_arg(call, j); + arg_j_n_arg = pet_expr_get_n_arg(arg_j); + if (pet_expr_get_type(arg_j) == pet_expr_int) { + int_arg = add_int(int_arg, arg_j); + } else if (arg_j_n_arg != 0 || !pet_expr_is_affine(arg_j)) { + arg = pet_expr_insert_arg(arg, arg_n_arg, + arg_j); + int_arg = add_arg(int_arg, arg_n_arg); + arg_n_arg++; + } else { + int_arg = add_aff(int_arg, arg_n_arg, arg_j); + } + } + arg = set_access_relations(arg, summary, pos, int_arg, add); + + return arg; +} + +/* Given the argument "arg" at position "pos" of "call", + * check if it is either an access expression or the address + * of an access expression. If so, use the information in "summary" + * to set the access relations of the access expression. + */ +static __isl_give pet_expr *arg_plug_in_summary(__isl_take pet_expr *arg, + __isl_keep pet_expr *call, __isl_keep pet_function_summary *summary, + int pos) +{ + enum pet_expr_type type; + pet_expr *arg2; + + type = pet_expr_get_type(arg); + if (type == pet_expr_access) + return access_plug_in_summary(arg, call, summary, pos, 0); + if (type != pet_expr_op) + return arg; + if (pet_expr_op_get_type(arg) != pet_op_address_of) + return arg; + + arg2 = pet_expr_get_arg(arg, 0); + if (pet_expr_get_type(arg2) == pet_expr_access) + arg2 = access_plug_in_summary(arg2, call, summary, pos, 1); + arg = pet_expr_set_arg(arg, 0, arg2); + + return arg; +} + +/* Given a call expression, check if the integer arguments can + * be represented by affine expressions in the context "pc" + * (assuming they are not already affine expressions). + * If so, replace these arguments by the corresponding affine expressions. + */ +static __isl_give pet_expr *call_plug_in_affine_args(__isl_take pet_expr *call, + __isl_keep pet_context *pc) +{ + int i, n; + + n = pet_expr_get_n_arg(call); + for (i = 0; i < n; ++i) { + pet_expr *arg; + isl_pw_aff *pa; + + arg = pet_expr_get_arg(call, i); + if (!arg) + return pet_expr_free(call); + if (pet_expr_get_type_size(arg) == 0 || + pet_expr_is_affine(arg)) { + pet_expr_free(arg); + continue; + } + + pa = pet_expr_extract_affine(arg, pc); + pet_expr_free(arg); + if (!pa) + return pet_expr_free(call); + if (isl_pw_aff_involves_nan(pa)) { + isl_pw_aff_free(pa); + continue; + } + + arg = pet_expr_from_index(isl_multi_pw_aff_from_pw_aff(pa)); + call = pet_expr_set_arg(call, i, arg); + } + + return call; +} + +/* If "call" has an associated function summary, then use it + * to set the access relations of the array arguments of the function call. + * + * We first plug in affine expressions for the integer arguments + * whenever possible as these arguments will be plugged in + * in the access relations of the array arguments. + */ +static __isl_give pet_expr *call_plug_in_summary(__isl_take pet_expr *call, + void *user) +{ + pet_context *pc = user; + pet_function_summary *summary; + int i, n; + + if (!pet_expr_call_has_summary(call)) + return call; + + call = call_plug_in_affine_args(call, pc); + + summary = pet_expr_call_get_summary(call); + if (!summary) + return pet_expr_free(call); + + n = pet_expr_get_n_arg(call); + for (i = 0; i < n; ++i) { + pet_expr *arg_i; + + if (!pet_function_summary_arg_is_array(summary, i)) + continue; + + arg_i = pet_expr_get_arg(call, i); + arg_i = arg_plug_in_summary(arg_i, call, summary, i); + call = pet_expr_set_arg(call, i, arg_i); + } + + pet_function_summary_free(summary); + return call; +} + +/* For each call subexpression of "expr", plug in the access relations + * from the associated function summary (if any). + */ +static __isl_give pet_expr *plug_in_summaries(__isl_take pet_expr *expr, + __isl_keep pet_context *pc) +{ + return pet_expr_map_call(expr, &call_plug_in_summary, pc); +} + /* Evaluate "expr" in the context of "pc". * * In particular, we first make sure that all the access expressions * inside "expr" have the same domain as "pc". - * Then, we plug in affine expressions for scalar reads and - * plug in the arguments of all access expressions in "expr". + * Then, we plug in affine expressions for scalar reads, + * plug in the arguments of all access expressions in "expr" and + * plug in the access relations from the summary functions associated + * to call expressions. */ __isl_give pet_expr *pet_context_evaluate_expr(__isl_keep pet_context *pc, __isl_take pet_expr *expr) { expr = pet_expr_insert_domain(expr, pet_context_get_space(pc)); expr = plug_in_affine_read(expr, pc); - return pet_expr_plug_in_args(expr, pc); + expr = pet_expr_plug_in_args(expr, pc); + expr = plug_in_summaries(expr, pc); + return expr; } /* Wrapper around pet_context_evaluate_expr diff --git a/tests/call1.c b/tests/call1.c new file mode 100644 index 0000000..e90a669 --- /dev/null +++ b/tests/call1.c @@ -0,0 +1,14 @@ +void foo(int pos, int C[const static pos + 4]) +{ + for (int i = 0; i < 4; ++i) + C[pos + i] += i; +} + +void bar(int n, int A[const static n]) +{ +#pragma scop + __pencil_assume(n % 4 == 0); + for (int i = 0; i < n; i += 4) + foo(i, A); +#pragma endscop +} diff --git a/tests/call1.scop b/tests/call1.scop new file mode 100644 index 0000000..00c369f --- /dev/null +++ b/tests/call1.scop @@ -0,0 +1,49 @@ +start: 141 +end: 245 +indent: "\t" +context: '[n] -> { : exists (e0 = floor((n)/4): 4e0 = n and n >= 0 and n <= 2147483647) + }' +arrays: +- context: '[n] -> { : n >= 0 }' + extent: '[n] -> { A[i0] : i0 <= -1 + n and i0 >= 0 }' + element_type: int + element_size: 4 +statements: +- line: 10 + domain: '[n] -> { S_0[] }' + schedule: '{ S_0[] -> [0] }' + body: + type: expression + expr: + type: op + operation: assume + arguments: + - type: access + index: '[n] -> { S_0[] -> [(1)] }' + reference: __pet_ref_0 + read: 1 + write: 0 +- line: 12 + domain: '[n] -> { S_1[i] : exists (e0 = floor((i)/4): 4e0 = i and i <= -4 + n and + i >= 0) }' + schedule: '[n] -> { S_1[i] -> [1, i] }' + body: + type: expression + expr: + type: call + name: foo + arguments: + - type: access + index: '[n] -> { S_1[i] -> [(i)] }' + reference: __pet_ref_1 + read: 1 + write: 0 + - type: access + may_read: '[n] -> { S_1[i] -> A[o0] : o0 >= i and o0 <= 3 + i }' + may_write: '[n] -> { S_1[i] -> A[o0] : o0 >= i and o0 <= 3 + i }' + must_write: '[n] -> { S_1[i] -> A[o0] : o0 >= i and o0 <= 3 + i }' + index: '[n] -> { S_1[i] -> A[] }' + depth: 1 + reference: __pet_ref_2 + read: 1 + write: 1 diff --git a/tests/call2.c b/tests/call2.c new file mode 100644 index 0000000..1cc25ea --- /dev/null +++ b/tests/call2.c @@ -0,0 +1,17 @@ +int f(int, int); + +void foo(int i, int n, int A[const static n]) +{ + A[i - 1] = 0; + if (i < n) + if (f(i, n)) + A[i] += 1; +} + +void bar(int n, int B[const static n][n]) +{ +#pragma scop + for (int i = 0; i < n; ++i) + foo(i + 1, n, B[i]); +#pragma endscop +} diff --git a/tests/call2.scop b/tests/call2.scop new file mode 100644 index 0000000..6c256b1 --- /dev/null +++ b/tests/call2.scop @@ -0,0 +1,40 @@ +start: 169 +end: 250 +indent: "\t" +context: '[n] -> { : n <= 2147483647 and n >= 0 }' +arrays: +- context: '[n] -> { : n >= 0 }' + extent: '[n] -> { B[i0, i1] : i0 >= 0 and i0 <= -1 + n and i1 <= -1 + n and i1 >= + 0 }' + element_type: int + element_size: 4 +statements: +- line: 15 + domain: '[n] -> { S_0[i] : i <= -1 + n and i >= 0 }' + schedule: '[n] -> { S_0[i] -> [0, i] }' + body: + type: expression + expr: + type: call + name: foo + arguments: + - type: access + index: '[n] -> { S_0[i] -> [(1 + i)] }' + reference: __pet_ref_0 + read: 1 + write: 0 + - type: access + index: '[n] -> { S_0[i] -> [(n)] }' + reference: __pet_ref_1 + read: 1 + write: 0 + - type: access + may_read: '[n] -> { S_0[i] -> B[i, 1 + i] : i <= -2 + n }' + may_write: '[n] -> { S_0[i] -> B[i, 1 + i] : i <= -2 + n; S_0[i] -> B[i, i] + }' + must_write: '[n] -> { S_0[i] -> B[i, i] }' + index: '[n] -> { S_0[i] -> B[(i)] }' + depth: 2 + reference: __pet_ref_2 + read: 1 + write: 1 diff --git a/tests/call3.c b/tests/call3.c new file mode 100644 index 0000000..cfd5b53 --- /dev/null +++ b/tests/call3.c @@ -0,0 +1,14 @@ +void foo(int C[const static 4]) +{ + for (int i = 0; i < 4; ++i) + C[i] += i; +} + +void bar(int n, int A[const static n]) +{ +#pragma scop + __pencil_assume(n % 4 == 0); + for (int i = 0; i < n; i += 4) + foo(&A[i]); +#pragma endscop +} diff --git a/tests/call3.scop b/tests/call3.scop new file mode 100644 index 0000000..7296844 --- /dev/null +++ b/tests/call3.scop @@ -0,0 +1,46 @@ +start: 120 +end: 225 +indent: "\t" +context: '[n] -> { : exists (e0 = floor((n)/4): 4e0 = n and n >= 0 and n <= 2147483647) + }' +arrays: +- context: '[n] -> { : n >= 0 }' + extent: '[n] -> { A[i0] : i0 <= -1 + n and i0 >= 0 }' + element_type: int + element_size: 4 +statements: +- line: 10 + domain: '[n] -> { S_0[] }' + schedule: '{ S_0[] -> [0] }' + body: + type: expression + expr: + type: op + operation: assume + arguments: + - type: access + index: '[n] -> { S_0[] -> [(1)] }' + reference: __pet_ref_0 + read: 1 + write: 0 +- line: 12 + domain: '[n] -> { S_1[i] : exists (e0 = floor((i)/4): 4e0 = i and i <= -4 + n and + i >= 0) }' + schedule: '[n] -> { S_1[i] -> [1, i] }' + body: + type: expression + expr: + type: call + name: foo + arguments: + - type: op + operation: '&' + arguments: + - type: access + may_read: '[n] -> { S_1[i] -> A[o0] : o0 >= i and o0 <= 3 + i }' + may_write: '[n] -> { S_1[i] -> A[o0] : o0 >= i and o0 <= 3 + i }' + must_write: '[n] -> { S_1[i] -> A[o0] : o0 >= i and o0 <= 3 + i }' + index: '[n] -> { S_1[i] -> A[(i)] }' + reference: __pet_ref_1 + read: 1 + write: 1 diff --git a/tests/call4.c b/tests/call4.c new file mode 100644 index 0000000..aadad4b --- /dev/null +++ b/tests/call4.c @@ -0,0 +1,17 @@ +int f(int); + +void foo(int a[static 1]) +{ + int t = a[0]; + + if (f(t)) + a[0] = t + 1; +} + +void bar() +{ +#pragma scop + int s; + foo(&s); +#pragma endscop +} diff --git a/tests/call4.scop b/tests/call4.scop new file mode 100644 index 0000000..893f9e8 --- /dev/null +++ b/tests/call4.scop @@ -0,0 +1,46 @@ +start: 100 +end: 147 +indent: "\t" +context: '{ : }' +arrays: +- context: '{ : }' + extent: '{ s[] }' + element_type: int + element_size: 4 + declared: 1 + exposed: 1 +statements: +- line: 14 + domain: '{ S_0[] }' + schedule: '{ S_0[] -> [0] }' + body: + type: expression + expr: + type: op + operation: kill + arguments: + - type: access + killed: '{ S_0[] -> s[] }' + index: '{ S_0[] -> s[] }' + reference: __pet_ref_0 + kill: 1 +- line: 15 + domain: '{ S_1[] }' + schedule: '{ S_1[] -> [1] }' + body: + type: expression + expr: + type: call + name: foo + arguments: + - type: op + operation: '&' + arguments: + - type: access + may_read: '{ S_1[] -> s[] }' + may_write: '{ S_1[] -> s[] }' + must_write: '{ }' + index: '{ S_1[] -> s[] }' + reference: __pet_ref_1 + read: 1 + write: 1 diff --git a/tests/call5.c b/tests/call5.c new file mode 100644 index 0000000..ea91cc1 --- /dev/null +++ b/tests/call5.c @@ -0,0 +1,13 @@ +void foo(int pos, int C[const static pos + 4]) +{ + for (int i = 0; i < 4; ++i) + C[pos + i] += i; +} + +void bar(int n, int A[const static n]) +{ +#pragma scop + __pencil_assume(n >= 4); + foo(0, A); +#pragma endscop +} diff --git a/tests/call5.scop b/tests/call5.scop new file mode 100644 index 0000000..eb970ef --- /dev/null +++ b/tests/call5.scop @@ -0,0 +1,44 @@ +start: 141 +end: 208 +indent: "\t" +context: '[n] -> { : n >= 4 and n <= 2147483647 }' +arrays: +- context: '[n] -> { : n >= 0 }' + extent: '[n] -> { A[i0] : i0 <= -1 + n and i0 >= 0 }' + element_type: int + element_size: 4 +statements: +- line: 10 + domain: '[n] -> { S_0[] }' + schedule: '{ S_0[] -> [0] }' + body: + type: expression + expr: + type: op + operation: assume + arguments: + - type: access + index: '[n] -> { S_0[] -> [(1)] }' + reference: __pet_ref_0 + read: 1 + write: 0 +- line: 11 + domain: '[n] -> { S_1[] }' + schedule: '{ S_1[] -> [1] }' + body: + type: expression + expr: + type: call + name: foo + arguments: + - type: int + value: 0 + - type: access + may_read: '[n] -> { S_1[] -> A[o0] : o0 <= 3 and o0 >= 0 }' + may_write: '[n] -> { S_1[] -> A[o0] : o0 <= 3 and o0 >= 0 }' + must_write: '[n] -> { S_1[] -> A[o0] : o0 <= 3 and o0 >= 0 }' + index: '[n] -> { S_1[] -> A[] }' + depth: 1 + reference: __pet_ref_1 + read: 1 + write: 1 diff --git a/tests/call_struct.c b/tests/call_struct.c new file mode 100644 index 0000000..4cf7fb4 --- /dev/null +++ b/tests/call_struct.c @@ -0,0 +1,35 @@ +struct s0 { + struct { + int a[10]; + } f[10]; + int b; +}; + +struct s { + struct s0 c[10]; +}; + +void bar(struct s0 t[static 5]) +{ + for (int i = 0; i < 10; ++i) + for (int j = 0; j < 10; ++j) + t[2].f[i].a[j] = i * j; + t[3].b = 1; +} + +void quux(int a[1]) +{ + a[0] = 5; +} + +void foo() +{ + struct s s[10]; + +#pragma scop + bar(s[0].c); + for (int i = 1; i < 4; ++i) + bar(&s[1].c[i]); + quux(&s[2].c[9].b); +#pragma endscop +} diff --git a/tests/call_struct.scop b/tests/call_struct.scop new file mode 100644 index 0000000..1f7497e --- /dev/null +++ b/tests/call_struct.scop @@ -0,0 +1,101 @@ +start: 295 +end: 407 +indent: "\t" +context: '{ : }' +types: +- name: s + definition: "struct s {\n struct s0 c[10];\n}" +- name: s0 + definition: "struct s0 {\n struct {\n int a[10];\n } f[10];\n int + b;\n}" +arrays: +- context: '{ : }' + extent: '{ s[i0] : i0 >= 0 and i0 <= 9 }' + element_type: struct s + element_size: 4040 + element_is_record: 1 +- context: '{ : }' + extent: '{ s_c[s[i0] -> c[i1]] : i0 >= 0 and i0 <= 9 and i1 >= 0 and i1 <= 9 }' + element_type: struct s0 + element_size: 404 + element_is_record: 1 +- context: '{ : }' + extent: '{ s_c_b[s_c[s[i0] -> c[i1]] -> b[]] : i0 >= 0 and i0 <= 9 and i1 >= 0 and + i1 <= 9 }' + element_type: int + element_size: 4 +- context: '{ : }' + extent: '{ s_c_f[s_c[s[i0] -> c[i1]] -> f[i2]] : i0 >= 0 and i0 <= 9 and i1 >= 0 + and i1 <= 9 and i2 >= 0 and i2 <= 9 }' + element_type: + element_size: 40 + element_is_record: 1 +- context: '{ : }' + extent: '{ s_c_f_a[s_c_f[s_c[s[i0] -> c[i1]] -> f[i2]] -> a[i3]] : i0 >= 0 and i0 + <= 9 and i1 >= 0 and i1 <= 9 and i2 >= 0 and i2 <= 9 and i3 >= 0 and i3 <= 9 }' + element_type: int + element_size: 4 +statements: +- line: 30 + domain: '{ S_0[] }' + schedule: '{ S_0[] -> [0] }' + body: + type: expression + expr: + type: call + name: bar + arguments: + - type: access + may_write: '{ S_0[] -> s_c_b[s_c[s[0] -> c[3]] -> b[]]; S_0[] -> s_c_f_a[s_c_f[s_c[s[0] + -> c[2]] -> f[o2]] -> a[o3]] : o2 >= 0 and o3 >= 0 and o3 <= 9 and o2 <= + 9 }' + must_write: '{ S_0[] -> s_c_b[s_c[s[0] -> c[3]] -> b[]]; S_0[] -> s_c_f_a[s_c_f[s_c[s[0] + -> c[2]] -> f[o2]] -> a[o3]] : o2 >= 0 and o3 >= 0 and o3 <= 9 and o2 <= + 9 }' + index: '{ S_0[] -> s_c[s[(0)] -> c[]] }' + depth: 2 + reference: __pet_ref_0 + read: 0 + write: 1 +- line: 32 + domain: '{ S_1[i] : i >= 1 and i <= 3 }' + schedule: '{ S_1[i] -> [1, i] }' + body: + type: expression + expr: + type: call + name: bar + arguments: + - type: op + operation: '&' + arguments: + - type: access + may_write: '{ S_1[i] -> s_c_f_a[s_c_f[s_c[s[1] -> c[2 + i]] -> f[o2]] -> + a[o3]] : o3 >= 0 and o3 <= 9 and o2 <= 9 and o2 >= 0; S_1[i] -> s_c_b[s_c[s[1] + -> c[3 + i]] -> b[]] }' + must_write: '{ S_1[i] -> s_c_f_a[s_c_f[s_c[s[1] -> c[2 + i]] -> f[o2]] -> + a[o3]] : o3 >= 0 and o3 <= 9 and o2 <= 9 and o2 >= 0; S_1[i] -> s_c_b[s_c[s[1] + -> c[3 + i]] -> b[]] }' + index: '{ S_1[i] -> s_c[s[(1)] -> c[(i)]] }' + reference: __pet_ref_1 + read: 0 + write: 1 +- line: 33 + domain: '{ S_2[] }' + schedule: '{ S_2[] -> [2] }' + body: + type: expression + expr: + type: call + name: quux + arguments: + - type: op + operation: '&' + arguments: + - type: access + may_write: '{ S_2[] -> s_c_b[s_c[s[2] -> c[9]] -> b[]] }' + must_write: '{ S_2[] -> s_c_b[s_c[s[2] -> c[9]] -> b[]] }' + index: '{ S_2[] -> s_c_b[s_c[s[(2)] -> c[(9)]] -> b[]] }' + reference: __pet_ref_2 + read: 0 + write: 1 -- 2.11.4.GIT