PetScan::extract_non_affine_condition: remove redundant resolve_nested
[pet.git] / pet_check_code.c
blob9eb0988bb943d9454aff7b0ffc375cc73fde032e
1 /*
2 * Copyright 2012 Ecole Normale Superieure. All rights reserved.
4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions
6 * are met:
8 * 1. Redistributions of source code must retain the above copyright
9 * notice, this list of conditions and the following disclaimer.
11 * 2. Redistributions in binary form must reproduce the above
12 * copyright notice, this list of conditions and the following
13 * disclaimer in the documentation and/or other materials provided
14 * with the distribution.
16 * THIS SOFTWARE IS PROVIDED BY ECOLE NORMALE SUPERIEURE ''AS IS'' AND ANY
17 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
18 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
19 * PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL ECOLE NORMALE SUPERIEURE OR
20 * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
21 * EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
22 * PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA,
23 * OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
24 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
25 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
26 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
28 * The views and conclusions contained in the software and documentation
29 * are those of the authors and should not be interpreted as
30 * representing official policies, either expressed or implied, of
31 * Ecole Normale Superieure.
34 #include <assert.h>
35 #include <stdio.h>
36 #include <string.h>
37 #include <isl/arg.h>
38 #include <isl/aff.h>
39 #include <isl/set.h>
40 #include <isl/union_map.h>
41 #include <isl/id_to_pw_aff.h>
42 #include <pet.h>
44 struct options {
45 struct pet_options *pet;
46 char *schedule;
47 char *code;
50 ISL_ARGS_START(struct options, options_args)
51 ISL_ARG_CHILD(struct options, pet, NULL, &pet_options_args, "pet options")
52 ISL_ARG_ARG(struct options, schedule, "schedule", NULL)
53 ISL_ARG_ARG(struct options, code, "code", NULL)
54 ISL_ARGS_END
56 ISL_ARG_DEF(options, struct options, options_args)
58 static __isl_give isl_pw_aff *expr_extract_pw_aff(struct pet_expr *expr,
59 __isl_keep isl_id_to_pw_aff *assignments);
61 /* Extract an affine expression from the call to floord in "expr",
62 * possibly exploiting "assignments".
64 static __isl_give isl_pw_aff *expr_extract_floord(struct pet_expr *expr,
65 __isl_keep isl_id_to_pw_aff *assignments)
67 isl_pw_aff *lhs, *rhs;
69 lhs = expr_extract_pw_aff(expr->args[0], assignments);
70 rhs = expr_extract_pw_aff(expr->args[1], assignments);
71 return isl_pw_aff_floor(isl_pw_aff_div(lhs, rhs));
74 /* Extract an affine expression from the call in "expr",
75 * possibly exploiting "assignments".
77 * We only support calls to the "floord" function for now.
79 static __isl_give isl_pw_aff *call_expr_extract_pw_aff(struct pet_expr *expr,
80 __isl_keep isl_id_to_pw_aff *assignments)
82 assert(!strcmp(expr->name, "floord"));
84 return expr_extract_floord(expr, assignments);
87 /* Is the variable accessed by "index" assigned in "assignments"?
89 * The assignments map variable identifiers to functions of the form
91 * { domain -> value }
93 static int is_assigned(__isl_keep isl_multi_pw_aff *index,
94 __isl_keep isl_id_to_pw_aff *assignments)
96 isl_id *var;
97 int assigned;
99 var = isl_multi_pw_aff_get_tuple_id(index, isl_dim_out);
100 assigned = isl_id_to_pw_aff_has(assignments, var);
101 isl_id_free(var);
103 return assigned;
106 /* Apply the appropriate assignment in "assignments"
107 * to the index expression "index".
109 * "index" is of the form
111 * { access_domain -> variable }
113 * "assignments" maps variable identifiers to functions of the form
115 * { assignment_domain -> value }
117 * We assume the assignment precedes the access in the code.
118 * In particular, we assume that the loops around the assignment
119 * are the same as the first loops around the access.
121 * We compute
123 * { access_domain -> assignment_domain }
125 * equating the iterators of assignment_domain to the corresponding iterators
126 * in access_domain and then plug that into the assigned value, obtaining
128 * { access_domain -> value }
130 static __isl_give isl_pw_aff *apply_assignment(
131 __isl_take isl_multi_pw_aff *index,
132 __isl_keep isl_id_to_pw_aff *assignments)
134 isl_id *id;
135 isl_set *dom;
136 isl_pw_aff *val;
137 isl_multi_aff *ma;
138 isl_space *space, *dom_space;
139 isl_local_space *ls;
140 int i, n;
142 id = isl_multi_pw_aff_get_tuple_id(index, isl_dim_out);
143 dom = isl_multi_pw_aff_domain(index);
144 val = isl_id_to_pw_aff_get(assignments, id);
145 space = isl_pw_aff_get_domain_space(val);
146 dom_space = isl_set_get_space(dom);
147 space = isl_space_map_from_domain_and_range(dom_space, space);
148 ma = isl_multi_aff_zero(space);
149 ls = isl_local_space_from_space(isl_set_get_space(dom));
150 n = isl_multi_aff_dim(ma, isl_dim_out);
151 for (i = 0; i < n; ++i) {
152 isl_aff *aff;
154 aff = isl_aff_var_on_domain(isl_local_space_copy(ls),
155 isl_dim_set, i);
156 ma = isl_multi_aff_set_aff(ma, i, aff);
158 isl_local_space_free(ls);
160 val = isl_pw_aff_pullback_multi_aff(val, ma);
161 val = isl_pw_aff_intersect_domain(val, dom);
163 return val;
166 /* Extract an affine expression from the access to a named space in "index",
167 * possibly exploiting "assignments".
169 * If the variable has been assigned a value, we return the corresponding
170 * assignment. Otherwise, we assume we are accessing a 0D space and
171 * we turn that into an expression equal to a parameter of the same name.
173 static __isl_give isl_pw_aff *resolve_access(__isl_take isl_multi_pw_aff *index,
174 __isl_keep isl_id_to_pw_aff *assignments)
176 isl_id *id;
177 isl_set *dom;
178 isl_aff *aff;
179 isl_local_space *ls;
180 isl_pw_aff *pa;
182 if (is_assigned(index, assignments))
183 return apply_assignment(index, assignments);
185 id = isl_multi_pw_aff_get_tuple_id(index, isl_dim_out);
186 dom = isl_multi_pw_aff_domain(index);
187 dom = isl_set_insert_dims(dom, isl_dim_param, 0, 1);
188 dom = isl_set_set_dim_id(dom, isl_dim_param, 0, id);
189 ls = isl_local_space_from_space(isl_set_get_space(dom));
190 aff = isl_aff_var_on_domain(ls, isl_dim_param, 0);
191 pa = isl_pw_aff_alloc(dom, aff);
193 return pa;
196 /* Extract an affine expression from the access expression "expr",
197 * possibly exploiting "assignments".
199 * If we are accessing a (1D) anonymous space, then we are actually
200 * computing an affine expression and we simply return that expression.
201 * Otherwise, we try and convert the access to an affine expression in
202 * resolve_access().
204 static __isl_give isl_pw_aff *access_expr_extract_pw_aff(struct pet_expr *expr,
205 __isl_keep isl_id_to_pw_aff *assignments)
207 isl_pw_aff *pa;
209 if (isl_multi_pw_aff_has_tuple_id(expr->acc.index, isl_dim_out)) {
210 isl_multi_pw_aff *index;
211 index = isl_multi_pw_aff_copy(expr->acc.index);
212 pa = resolve_access(index, assignments);
213 } else
214 pa = isl_multi_pw_aff_get_pw_aff(expr->acc.index, 0);
215 return pa;
218 /* Extract an affine expression from "expr", possibly exploiting "assignments",
219 * in the form of an isl_pw_aff.
221 * We only handle the kinds of expressions that we would expect
222 * as arguments to a function call in code generated by isl.
224 static __isl_give isl_pw_aff *expr_extract_pw_aff(struct pet_expr *expr,
225 __isl_keep isl_id_to_pw_aff *assignments)
227 isl_pw_aff *pa, *pa1, *pa2;
229 switch (expr->type) {
230 case pet_expr_access:
231 return access_expr_extract_pw_aff(expr, assignments);
232 case pet_expr_unary:
233 if (expr->op == pet_op_minus) {
234 pa = expr_extract_pw_aff(expr->args[0], assignments);
235 return isl_pw_aff_neg(pa);
237 assert(0);
238 case pet_expr_binary:
239 pa1 = expr_extract_pw_aff(expr->args[0], assignments);
240 pa2 = expr_extract_pw_aff(expr->args[1], assignments);
241 switch (expr->op) {
242 case pet_op_mul:
243 pa = isl_pw_aff_mul(pa1, pa2);
244 break;
245 case pet_op_add:
246 pa = isl_pw_aff_add(pa1, pa2);
247 break;
248 case pet_op_sub:
249 pa = isl_pw_aff_sub(pa1, pa2);
250 break;
251 case pet_op_div:
252 pa = isl_pw_aff_tdiv_q(pa1, pa2);
253 break;
254 case pet_op_mod:
255 pa = isl_pw_aff_tdiv_r(pa1, pa2);
256 break;
257 default:
258 assert(0);
260 return pa;
261 case pet_expr_call:
262 return call_expr_extract_pw_aff(expr, assignments);
263 case pet_expr_ternary:
264 pa = expr_extract_pw_aff(expr->args[0], assignments);
265 pa1 = expr_extract_pw_aff(expr->args[1], assignments);
266 pa2 = expr_extract_pw_aff(expr->args[2], assignments);
267 return isl_pw_aff_cond(pa, pa1, pa2);
268 case pet_expr_cast:
269 case pet_expr_double:
270 assert(0);
274 /* Extract an affine expression from "expr", possibly exploiting "assignments",
275 * in the form of an isl_map.
277 static __isl_give isl_map *expr_extract_map(struct pet_expr *expr,
278 __isl_keep isl_id_to_pw_aff *assignments)
280 return isl_map_from_pw_aff(expr_extract_pw_aff(expr, assignments));
283 /* Extract a call from "stmt", possibly exploiting "assignments".
285 * The returned map is of the form
287 * { domain -> function[arguments] }
289 static __isl_give isl_map *stmt_extract_call(struct pet_stmt *stmt,
290 __isl_keep isl_id_to_pw_aff *assignments)
292 int i;
293 isl_set *domain;
294 isl_map *call;
296 domain = isl_set_copy(stmt->domain);
297 call = isl_map_from_domain(domain);
299 assert(stmt->body->type == pet_expr_call);
301 for (i = 0; i < stmt->body->n_arg; ++i) {
302 isl_map *arg;
304 arg = expr_extract_map(stmt->body->args[i], assignments);
305 call = isl_map_flat_range_product(call, arg);
308 call = isl_map_set_tuple_name(call, isl_dim_out, stmt->body->name);
310 return call;
313 /* Add the assignment in "stmt" to "assignments".
315 * We extract the accessed variable identifier "var"
316 * and the assigned value
318 * { domain -> value }
320 * and map "var" to this value in "assignments", replacing
321 * any possible previously assigned value to the same variable.
323 static __isl_give isl_id_to_pw_aff *add_assignment(
324 __isl_take isl_id_to_pw_aff *assignments, struct pet_stmt *stmt)
326 isl_id *var;
327 isl_pw_aff *val;
329 assert(stmt->body->op == pet_op_assign);
330 assert(stmt->body->args[0]->type == pet_expr_access);
331 var = isl_map_get_tuple_id(stmt->body->args[0]->acc.access,
332 isl_dim_out);
333 val = expr_extract_pw_aff(stmt->body->args[1], assignments);
335 assignments = isl_id_to_pw_aff_set(assignments, var, val);
337 return assignments;
340 /* Is "stmt" a kill statement?
342 static int is_kill(struct pet_stmt *stmt)
344 if (stmt->body->type != pet_expr_unary)
345 return 0;
346 return stmt->body->op == pet_op_kill;
349 /* Extract a mapping from the iterations domains of "scop" to
350 * the calls in the corresponding statements.
352 * While scanning "scop", we keep track of assignments to variables
353 * so that we can plug them in in the arguments of the calls.
354 * Note that we do not perform any dependence analysis on the assigned
355 * variables. In code generated by isl, such assignments should only
356 * appear immediately before they are used.
358 * The assignments are kept as an associative array between
359 * variable identifiers and assignments of the form
361 * { domain -> value }
363 * We skip kill statements.
364 * Other than assignments and kill statements, all statements are assumed
365 * to be function calls.
367 static __isl_give isl_union_map *scop_collect_calls(struct pet_scop *scop)
369 int i;
370 isl_ctx *ctx;
371 isl_map *call_i;
372 isl_id_to_pw_aff *assignments;
373 isl_union_map *call;
375 if (!scop)
376 return NULL;
378 call = isl_union_map_empty(isl_set_get_space(scop->context));
379 ctx = isl_set_get_ctx(scop->context);
380 assignments = isl_id_to_pw_aff_alloc(ctx, 0);
382 for (i = 0; i < scop->n_stmt; ++i) {
383 struct pet_stmt *stmt;
385 stmt = scop->stmts[i];
386 if (stmt->body->type == pet_expr_binary) {
387 assignments = add_assignment(assignments, stmt);
388 continue;
390 if (is_kill(stmt))
391 continue;
392 call_i = stmt_extract_call(scop->stmts[i], assignments);
393 call = isl_union_map_add_map(call, call_i);
396 isl_id_to_pw_aff_free(assignments);
398 return call;
401 /* Extract a schedule on the original domains from "scop".
402 * The original domain elements appear as calls in "scop".
404 * We first extract a schedule on the code iteration domains
405 * and a mapping from the code iteration domains to the calls
406 * (i.e., the original domain) and then combine the two.
408 static __isl_give isl_union_map *extract_code_schedule(struct pet_scop *scop)
410 isl_union_map *schedule;
411 isl_union_map *calls;
413 schedule = pet_scop_collect_schedule(scop);
415 calls = scop_collect_calls(scop);
417 schedule = isl_union_map_apply_domain(schedule, calls);
419 return schedule;
422 /* Check that schedule and code_schedule have the same domain,
423 * i.e., that they execute the same statement instances.
425 static int check_domain(__isl_keep isl_union_map *schedule,
426 __isl_keep isl_union_map *code_schedule)
428 isl_union_set *dom1, *dom2;
429 int equal;
430 isl_set *s1, *s2;;
431 isl_id *id1, *id2;
433 dom1 = isl_union_map_domain(isl_union_map_copy(schedule));
434 dom2 = isl_union_map_domain(isl_union_map_copy(code_schedule));
435 equal = isl_union_set_is_equal(dom1, dom2);
436 isl_union_set_free(dom1);
437 isl_union_set_free(dom2);
439 if (equal < 0)
440 return -1;
441 if (!equal)
442 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
443 "domains not identical", return -1);
445 return 0;
448 /* Check that the relative order specified by the input schedule is respected
449 * by the schedule extracted from the code, in case the original schedule
450 * is single valued.
452 * In particular, check that there is no pair of statement instances
453 * such that the first should be scheduled _before_ the second,
454 * but is actually scheduled _after_ the second in the code.
456 static int check_order_sv(__isl_keep isl_union_map *schedule,
457 __isl_keep isl_union_map *code_schedule)
459 isl_union_map *t1;
460 isl_union_map *t2;
461 int empty;
463 t1 = isl_union_map_lex_lt_union_map(isl_union_map_copy(schedule),
464 isl_union_map_copy(schedule));
465 t2 = isl_union_map_lex_gt_union_map(isl_union_map_copy(code_schedule),
466 isl_union_map_copy(code_schedule));
467 t1 = isl_union_map_intersect(t1, t2);
468 empty = isl_union_map_is_empty(t1);
469 isl_union_map_free(t1);
471 if (empty < 0)
472 return -1;
473 if (!empty)
474 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
475 "order not respected", return -1);
477 return 0;
480 /* Check that the relative order specified by the input schedule is respected
481 * by the schedule extracted from the code, in case the original schedule
482 * is not single valued.
484 * In particular, check that the order imposed by the schedules on pairs
485 * of statement instances is the same.
487 static int check_order_not_sv(__isl_keep isl_union_map *schedule,
488 __isl_keep isl_union_map *code_schedule)
490 isl_union_map *t1;
491 isl_union_map *t2;
492 int equal;
494 t1 = isl_union_map_lex_lt_union_map(isl_union_map_copy(schedule),
495 isl_union_map_copy(schedule));
496 t2 = isl_union_map_lex_lt_union_map(isl_union_map_copy(code_schedule),
497 isl_union_map_copy(code_schedule));
498 equal = isl_union_map_is_equal(t1, t2);
499 isl_union_map_free(t1);
500 isl_union_map_free(t2);
502 if (equal < 0)
503 return -1;
504 if (!equal)
505 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
506 "order not respected", return -1);
508 return 0;
511 /* Check that the relative order specified by the input schedule is respected
512 * by the schedule extracted from the code.
514 * "sv" indicated whether the original schedule is single valued.
515 * If so, we use a cheaper test. Otherwise, we fall back on a more
516 * expensive test.
518 static int check_order(__isl_keep isl_union_map *schedule,
519 __isl_keep isl_union_map *code_schedule, int sv)
521 if (sv)
522 return check_order_sv(schedule, code_schedule);
523 else
524 return check_order_not_sv(schedule, code_schedule);
527 /* If the original schedule was single valued ("sv" is set),
528 * then the schedule extracted from the code should be single valued as well.
530 static int check_single_valued(__isl_keep isl_union_map *code_schedule, int sv)
532 if (!sv)
533 return 0;
535 sv = isl_union_map_is_single_valued(code_schedule);
536 if (sv < 0)
537 return -1;
539 if (!sv)
540 isl_die(isl_union_map_get_ctx(code_schedule), isl_error_unknown,
541 "schedule not single valued", return -1);
543 return 0;
546 /* Read a schedule and a context from the first argument and
547 * C code from the second argument and check that the C code
548 * corresponds to the schedule on the context.
550 * In particular, check that
551 * - the domains are identical, i.e., the calls in the C code
552 * correspond to the domain elements of the schedule
553 * - no function is called twice with the same arguments, provided
554 * the schedule is single-valued
555 * - the calls are performed in an order that is compatible
556 * with the schedule
558 * If the schedule is not single-valued then we would have to check
559 * that each function with a given set of arguments is called
560 * the same number of times as there are images in the schedule,
561 * but this is considerably more difficult.
563 int main(int argc, char **argv)
565 isl_ctx *ctx;
566 isl_set *context;
567 isl_union_map *schedule, *code_schedule;
568 struct pet_scop *scop;
569 struct options *options;
570 FILE *file;
571 int r;
572 int sv;
574 options = options_new_with_defaults();
575 assert(options);
576 ctx = isl_ctx_alloc_with_options(&options_args, options);
577 pet_options_set_signed_overflow(ctx, PET_OVERFLOW_IGNORE);
578 argc = options_parse(options, argc, argv, ISL_ARG_ALL);
580 file = fopen(options->schedule, "r");
581 assert(file);
582 schedule = isl_union_map_read_from_file(ctx, file);
583 context = isl_set_read_from_file(ctx, file);
584 fclose(file);
586 scop = pet_scop_extract_from_C_source(ctx, options->code, NULL);
588 schedule = isl_union_map_intersect_params(schedule,
589 isl_set_copy(context));
590 code_schedule = extract_code_schedule(scop);
591 code_schedule = isl_union_map_intersect_params(code_schedule, context);
593 sv = isl_union_map_is_single_valued(schedule);
594 r = sv < 0 ||
595 check_domain(schedule, code_schedule) ||
596 check_single_valued(code_schedule, sv) ||
597 check_order(schedule, code_schedule, sv);
599 pet_scop_free(scop);
600 isl_union_map_free(schedule);
601 isl_union_map_free(code_schedule);
602 isl_ctx_free(ctx);
604 return r;