update isl for isl_space_domain_factor_domain
[pet.git] / pet_check_code.c
blob3320944d0b50a389a66e19b6336c9932b878c2cf
1 /*
2 * Copyright 2012-2014 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/options.h>
40 #include <isl/set.h>
41 #include <isl/union_map.h>
42 #include <isl/id_to_pw_aff.h>
43 #include <pet.h>
45 struct options {
46 struct isl_options *isl;
47 struct pet_options *pet;
48 char *schedule;
49 char *code;
52 ISL_ARGS_START(struct options, options_args)
53 ISL_ARG_CHILD(struct options, isl, "isl", &isl_options_args, "isl options")
54 ISL_ARG_CHILD(struct options, pet, NULL, &pet_options_args, "pet options")
55 ISL_ARG_ARG(struct options, schedule, "schedule", NULL)
56 ISL_ARG_ARG(struct options, code, "code", NULL)
57 ISL_ARGS_END
59 ISL_ARG_DEF(options, struct options, options_args)
61 static __isl_give isl_pw_aff *expr_extract_pw_aff(struct pet_expr *expr,
62 __isl_keep isl_space *space, __isl_keep isl_id_to_pw_aff *assignments);
64 /* Extract an affine expression from the call to floord in "expr",
65 * possibly exploiting "assignments".
67 * "space" is the iteration space of the statement containing the expression.
69 static __isl_give isl_pw_aff *expr_extract_floord(struct pet_expr *expr,
70 __isl_keep isl_space *space, __isl_keep isl_id_to_pw_aff *assignments)
72 isl_pw_aff *lhs, *rhs;
74 lhs = expr_extract_pw_aff(expr->args[0], space, assignments);
75 rhs = expr_extract_pw_aff(expr->args[1], space, assignments);
76 return isl_pw_aff_floor(isl_pw_aff_div(lhs, rhs));
79 /* Extract an affine expression from the call in "expr",
80 * possibly exploiting "assignments".
82 * "space" is the iteration space of the statement containing the expression.
84 * We only support calls to the "floord" function for now.
86 static __isl_give isl_pw_aff *call_expr_extract_pw_aff(struct pet_expr *expr,
87 __isl_keep isl_space *space, __isl_keep isl_id_to_pw_aff *assignments)
89 assert(!strcmp(expr->name, "floord"));
91 return expr_extract_floord(expr, space, assignments);
94 /* Is the variable accessed by "index" assigned in "assignments"?
96 * The assignments map variable identifiers to functions of the form
98 * { domain -> value }
100 static int is_assigned(__isl_keep isl_multi_pw_aff *index,
101 __isl_keep isl_id_to_pw_aff *assignments)
103 isl_id *var;
104 int assigned;
106 var = isl_multi_pw_aff_get_tuple_id(index, isl_dim_out);
107 assigned = isl_id_to_pw_aff_has(assignments, var);
108 isl_id_free(var);
110 return assigned;
113 /* Apply the appropriate assignment in "assignments"
114 * to the index expression "index".
116 * "index" is of the form
118 * { access_domain -> variable }
120 * "assignments" maps variable identifiers to functions of the form
122 * { assignment_domain -> value }
124 * We assume the assignment precedes the access in the code.
125 * In particular, we assume that the loops around the assignment
126 * are the same as the first loops around the access.
128 * We compute
130 * { access_domain -> assignment_domain }
132 * equating the iterators of assignment_domain to the corresponding iterators
133 * in access_domain and then plug that into the assigned value, obtaining
135 * { access_domain -> value }
137 static __isl_give isl_pw_aff *apply_assignment(
138 __isl_take isl_multi_pw_aff *index,
139 __isl_keep isl_id_to_pw_aff *assignments)
141 isl_id *id;
142 isl_set *dom;
143 isl_pw_aff *val;
144 isl_multi_aff *ma;
145 isl_space *space, *dom_space;
146 isl_local_space *ls;
147 int i, n;
149 id = isl_multi_pw_aff_get_tuple_id(index, isl_dim_out);
150 dom = isl_multi_pw_aff_domain(index);
151 val = isl_id_to_pw_aff_get(assignments, id);
152 space = isl_pw_aff_get_domain_space(val);
153 dom_space = isl_set_get_space(dom);
154 space = isl_space_map_from_domain_and_range(dom_space, space);
155 ma = isl_multi_aff_zero(space);
156 ls = isl_local_space_from_space(isl_set_get_space(dom));
157 n = isl_multi_aff_dim(ma, isl_dim_out);
158 for (i = 0; i < n; ++i) {
159 isl_aff *aff;
161 aff = isl_aff_var_on_domain(isl_local_space_copy(ls),
162 isl_dim_set, i);
163 ma = isl_multi_aff_set_aff(ma, i, aff);
165 isl_local_space_free(ls);
167 val = isl_pw_aff_pullback_multi_aff(val, ma);
168 val = isl_pw_aff_intersect_domain(val, dom);
170 return val;
173 /* Extract an affine expression from the access to a named space in "index",
174 * possibly exploiting "assignments".
176 * If the variable has been assigned a value, we return the corresponding
177 * assignment. Otherwise, we assume we are accessing a 0D space and
178 * we turn that into an expression equal to a parameter of the same name.
180 static __isl_give isl_pw_aff *resolve_access(__isl_take isl_multi_pw_aff *index,
181 __isl_keep isl_id_to_pw_aff *assignments)
183 isl_id *id;
184 isl_set *dom;
185 isl_aff *aff;
186 isl_local_space *ls;
187 isl_pw_aff *pa;
189 if (is_assigned(index, assignments))
190 return apply_assignment(index, assignments);
192 id = isl_multi_pw_aff_get_tuple_id(index, isl_dim_out);
193 dom = isl_multi_pw_aff_domain(index);
194 dom = isl_set_insert_dims(dom, isl_dim_param, 0, 1);
195 dom = isl_set_set_dim_id(dom, isl_dim_param, 0, id);
196 ls = isl_local_space_from_space(isl_set_get_space(dom));
197 aff = isl_aff_var_on_domain(ls, isl_dim_param, 0);
198 pa = isl_pw_aff_alloc(dom, aff);
200 return pa;
203 /* Extract an affine expression from the access expression "expr",
204 * possibly exploiting "assignments".
206 * If we are accessing a (1D) anonymous space, then we are actually
207 * computing an affine expression and we simply return that expression.
208 * Otherwise, we try and convert the access to an affine expression in
209 * resolve_access().
211 static __isl_give isl_pw_aff *access_expr_extract_pw_aff(struct pet_expr *expr,
212 __isl_keep isl_id_to_pw_aff *assignments)
214 isl_pw_aff *pa;
216 if (isl_multi_pw_aff_has_tuple_id(expr->acc.index, isl_dim_out)) {
217 isl_multi_pw_aff *index;
218 index = isl_multi_pw_aff_copy(expr->acc.index);
219 pa = resolve_access(index, assignments);
220 } else
221 pa = isl_multi_pw_aff_get_pw_aff(expr->acc.index, 0);
222 return pa;
225 /* Extract an affine expression defined over iteration space "space"
226 * from the integer expression "expr".
228 static __isl_give isl_pw_aff *int_expr_extract_pw_aff(struct pet_expr *expr,
229 __isl_keep isl_space *space)
231 isl_local_space *ls;
232 isl_aff *aff;
234 ls = isl_local_space_from_space(isl_space_copy(space));
235 aff = isl_aff_zero_on_domain(ls);
236 aff = isl_aff_add_constant_val(aff, isl_val_copy(expr->i));
237 return isl_pw_aff_from_aff(aff);
240 /* Extract an affine expression from the operation in "expr",
241 * possibly exploiting "assignments".
243 * "space" is the iteration space of the statement containing the expression.
245 * We only handle the kinds of expressions that we would expect
246 * as arguments to a function call in code generated by isl.
248 static __isl_give isl_pw_aff *op_expr_extract_pw_aff(struct pet_expr *expr,
249 __isl_keep isl_space *space, __isl_keep isl_id_to_pw_aff *assignments)
251 isl_pw_aff *pa, *pa1, *pa2;
253 switch (expr->n_arg) {
254 case 1:
255 if (expr->op == pet_op_minus) {
256 pa = expr_extract_pw_aff(expr->args[0], space,
257 assignments);
258 return isl_pw_aff_neg(pa);
260 assert(0);
261 case 2:
262 pa1 = expr_extract_pw_aff(expr->args[0], space, assignments);
263 pa2 = expr_extract_pw_aff(expr->args[1], space, assignments);
264 switch (expr->op) {
265 case pet_op_mul:
266 pa = isl_pw_aff_mul(pa1, pa2);
267 break;
268 case pet_op_add:
269 pa = isl_pw_aff_add(pa1, pa2);
270 break;
271 case pet_op_sub:
272 pa = isl_pw_aff_sub(pa1, pa2);
273 break;
274 case pet_op_div:
275 pa = isl_pw_aff_tdiv_q(pa1, pa2);
276 break;
277 case pet_op_mod:
278 pa = isl_pw_aff_tdiv_r(pa1, pa2);
279 break;
280 default:
281 assert(0);
283 return pa;
284 case 3:
285 pa = expr_extract_pw_aff(expr->args[0], space, assignments);
286 pa1 = expr_extract_pw_aff(expr->args[1], space, assignments);
287 pa2 = expr_extract_pw_aff(expr->args[2], space, assignments);
288 return isl_pw_aff_cond(pa, pa1, pa2);
289 default:
290 assert(0);
294 /* Extract an affine expression from "expr", possibly exploiting "assignments",
295 * in the form of an isl_pw_aff.
297 * "space" is the iteration space of the statement containing the expression.
299 * We only handle the kinds of expressions that we would expect
300 * as arguments to a function call in code generated by isl.
302 static __isl_give isl_pw_aff *expr_extract_pw_aff(struct pet_expr *expr,
303 __isl_keep isl_space *space, __isl_keep isl_id_to_pw_aff *assignments)
305 switch (expr->type) {
306 case pet_expr_int:
307 return int_expr_extract_pw_aff(expr, space);
308 case pet_expr_access:
309 return access_expr_extract_pw_aff(expr, assignments);
310 case pet_expr_op:
311 return op_expr_extract_pw_aff(expr, space, assignments);
312 case pet_expr_call:
313 return call_expr_extract_pw_aff(expr, space, assignments);
314 case pet_expr_cast:
315 case pet_expr_double:
316 assert(0);
320 /* Extract an affine expression from "expr", possibly exploiting "assignments",
321 * in the form of an isl_map.
323 * "space" is the iteration space of the statement containing the expression.
325 static __isl_give isl_map *expr_extract_map(struct pet_expr *expr,
326 __isl_keep isl_space *space, __isl_keep isl_id_to_pw_aff *assignments)
328 isl_pw_aff *pa;
330 pa = expr_extract_pw_aff(expr, space, assignments);
331 return isl_map_from_pw_aff(pa);
334 /* Extract a call from "stmt", possibly exploiting "assignments".
336 * The returned map is of the form
338 * { domain -> function[arguments] }
340 static __isl_give isl_map *stmt_extract_call(struct pet_stmt *stmt,
341 __isl_keep isl_id_to_pw_aff *assignments)
343 int i;
344 isl_set *domain;
345 isl_map *call;
347 domain = isl_set_copy(stmt->domain);
348 call = isl_map_from_domain(domain);
350 assert(stmt->body->type == pet_expr_call);
352 for (i = 0; i < stmt->body->n_arg; ++i) {
353 isl_map *arg;
354 isl_space *space;
356 space = pet_stmt_get_space(stmt);
357 arg = expr_extract_map(stmt->body->args[i], space, assignments);
358 isl_space_free(space);
359 call = isl_map_flat_range_product(call, arg);
362 call = isl_map_set_tuple_name(call, isl_dim_out, stmt->body->name);
364 return call;
367 /* Add the assignment in "stmt" to "assignments".
369 * We extract the accessed variable identifier "var"
370 * and the assigned value
372 * { domain -> value }
374 * and map "var" to this value in "assignments", replacing
375 * any possible previously assigned value to the same variable.
377 static __isl_give isl_id_to_pw_aff *add_assignment(
378 __isl_take isl_id_to_pw_aff *assignments, struct pet_stmt *stmt)
380 isl_id *var;
381 isl_space *space;
382 isl_pw_aff *val;
384 assert(stmt->body->op == pet_op_assign);
385 assert(stmt->body->args[0]->type == pet_expr_access);
386 var = isl_map_get_tuple_id(stmt->body->args[0]->acc.access,
387 isl_dim_out);
388 space = pet_stmt_get_space(stmt);
389 val = expr_extract_pw_aff(stmt->body->args[1], space, assignments);
390 isl_space_free(space);
392 assignments = isl_id_to_pw_aff_set(assignments, var, val);
394 return assignments;
397 /* Extract a mapping from the iterations domains of "scop" to
398 * the calls in the corresponding statements.
400 * While scanning "scop", we keep track of assignments to variables
401 * so that we can plug them in in the arguments of the calls.
402 * Note that we do not perform any dependence analysis on the assigned
403 * variables. In code generated by isl, such assignments should only
404 * appear immediately before they are used.
406 * The assignments are kept as an associative array between
407 * variable identifiers and assignments of the form
409 * { domain -> value }
411 * We skip kill statements.
412 * Other than assignments and kill statements, all statements are assumed
413 * to be function calls.
415 static __isl_give isl_union_map *scop_collect_calls(struct pet_scop *scop)
417 int i;
418 isl_ctx *ctx;
419 isl_map *call_i;
420 isl_id_to_pw_aff *assignments;
421 isl_union_map *call;
423 if (!scop)
424 return NULL;
426 call = isl_union_map_empty(isl_set_get_space(scop->context));
427 ctx = isl_set_get_ctx(scop->context);
428 assignments = isl_id_to_pw_aff_alloc(ctx, 0);
430 for (i = 0; i < scop->n_stmt; ++i) {
431 struct pet_stmt *stmt;
433 stmt = scop->stmts[i];
434 if (pet_stmt_is_assign(stmt)) {
435 assignments = add_assignment(assignments, stmt);
436 continue;
438 if (pet_stmt_is_kill(stmt))
439 continue;
440 call_i = stmt_extract_call(scop->stmts[i], assignments);
441 call = isl_union_map_add_map(call, call_i);
444 isl_id_to_pw_aff_free(assignments);
446 return call;
449 /* Extract a schedule on the original domains from "scop".
450 * The original domain elements appear as calls in "scop".
452 * We first extract a schedule on the code iteration domains
453 * and a mapping from the code iteration domains to the calls
454 * (i.e., the original domain) and then combine the two.
456 static __isl_give isl_union_map *extract_code_schedule(struct pet_scop *scop)
458 isl_union_map *schedule;
459 isl_union_map *calls;
461 schedule = pet_scop_collect_schedule(scop);
463 calls = scop_collect_calls(scop);
465 schedule = isl_union_map_apply_domain(schedule, calls);
467 return schedule;
470 /* Check that schedule and code_schedule have the same domain,
471 * i.e., that they execute the same statement instances.
473 static int check_domain(__isl_keep isl_union_map *schedule,
474 __isl_keep isl_union_map *code_schedule)
476 isl_union_set *dom1, *dom2;
477 int equal;
478 isl_set *s1, *s2;;
479 isl_id *id1, *id2;
480 int r = 0;
482 dom1 = isl_union_map_domain(isl_union_map_copy(schedule));
483 dom2 = isl_union_map_domain(isl_union_map_copy(code_schedule));
484 equal = isl_union_set_is_equal(dom1, dom2);
486 if (equal < 0)
487 r = -1;
488 else if (!equal) {
489 isl_union_set_dump(dom1);
490 isl_union_set_dump(dom2);
491 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
492 "domains not identical", r = -1);
495 isl_union_set_free(dom1);
496 isl_union_set_free(dom2);
498 return r;
501 /* Check that the relative order specified by the input schedule is respected
502 * by the schedule extracted from the code, in case the original schedule
503 * is single valued.
505 * In particular, check that there is no pair of statement instances
506 * such that the first should be scheduled _before_ the second,
507 * but is actually scheduled _after_ the second in the code.
509 static int check_order_sv(__isl_keep isl_union_map *schedule,
510 __isl_keep isl_union_map *code_schedule)
512 isl_union_map *t1;
513 isl_union_map *t2;
514 int empty;
516 t1 = isl_union_map_lex_lt_union_map(isl_union_map_copy(schedule),
517 isl_union_map_copy(schedule));
518 t2 = isl_union_map_lex_gt_union_map(isl_union_map_copy(code_schedule),
519 isl_union_map_copy(code_schedule));
520 t1 = isl_union_map_intersect(t1, t2);
521 empty = isl_union_map_is_empty(t1);
522 isl_union_map_free(t1);
524 if (empty < 0)
525 return -1;
526 if (!empty)
527 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
528 "order not respected", return -1);
530 return 0;
533 /* Check that the relative order specified by the input schedule is respected
534 * by the schedule extracted from the code, in case the original schedule
535 * is not single valued.
537 * In particular, check that the order imposed by the schedules on pairs
538 * of statement instances is the same.
540 static int check_order_not_sv(__isl_keep isl_union_map *schedule,
541 __isl_keep isl_union_map *code_schedule)
543 isl_union_map *t1;
544 isl_union_map *t2;
545 int equal;
547 t1 = isl_union_map_lex_lt_union_map(isl_union_map_copy(schedule),
548 isl_union_map_copy(schedule));
549 t2 = isl_union_map_lex_lt_union_map(isl_union_map_copy(code_schedule),
550 isl_union_map_copy(code_schedule));
551 equal = isl_union_map_is_equal(t1, t2);
552 isl_union_map_free(t1);
553 isl_union_map_free(t2);
555 if (equal < 0)
556 return -1;
557 if (!equal)
558 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
559 "order not respected", return -1);
561 return 0;
564 /* Check that the relative order specified by the input schedule is respected
565 * by the schedule extracted from the code.
567 * "sv" indicated whether the original schedule is single valued.
568 * If so, we use a cheaper test. Otherwise, we fall back on a more
569 * expensive test.
571 static int check_order(__isl_keep isl_union_map *schedule,
572 __isl_keep isl_union_map *code_schedule, int sv)
574 if (sv)
575 return check_order_sv(schedule, code_schedule);
576 else
577 return check_order_not_sv(schedule, code_schedule);
580 /* If the original schedule was single valued ("sv" is set),
581 * then the schedule extracted from the code should be single valued as well.
583 static int check_single_valued(__isl_keep isl_union_map *code_schedule, int sv)
585 if (!sv)
586 return 0;
588 sv = isl_union_map_is_single_valued(code_schedule);
589 if (sv < 0)
590 return -1;
592 if (!sv)
593 isl_die(isl_union_map_get_ctx(code_schedule), isl_error_unknown,
594 "schedule not single valued", return -1);
596 return 0;
599 /* Read a schedule and a context from the first argument and
600 * C code from the second argument and check that the C code
601 * corresponds to the schedule on the context.
603 * In particular, check that
604 * - the domains are identical, i.e., the calls in the C code
605 * correspond to the domain elements of the schedule
606 * - no function is called twice with the same arguments, provided
607 * the schedule is single-valued
608 * - the calls are performed in an order that is compatible
609 * with the schedule
611 * If the schedule is not single-valued then we would have to check
612 * that each function with a given set of arguments is called
613 * the same number of times as there are images in the schedule,
614 * but this is considerably more difficult.
616 int main(int argc, char **argv)
618 isl_ctx *ctx;
619 isl_set *context;
620 isl_union_map *schedule, *code_schedule;
621 struct pet_scop *scop;
622 struct options *options;
623 FILE *file;
624 int r;
625 int sv;
627 options = options_new_with_defaults();
628 assert(options);
629 ctx = isl_ctx_alloc_with_options(&options_args, options);
630 pet_options_set_signed_overflow(ctx, PET_OVERFLOW_IGNORE);
631 argc = options_parse(options, argc, argv, ISL_ARG_ALL);
633 file = fopen(options->schedule, "r");
634 assert(file);
635 schedule = isl_union_map_read_from_file(ctx, file);
636 context = isl_set_read_from_file(ctx, file);
637 fclose(file);
639 scop = pet_scop_extract_from_C_source(ctx, options->code, NULL);
641 schedule = isl_union_map_intersect_params(schedule,
642 isl_set_copy(context));
643 code_schedule = extract_code_schedule(scop);
644 code_schedule = isl_union_map_intersect_params(code_schedule, context);
646 sv = isl_union_map_is_single_valued(schedule);
647 r = sv < 0 ||
648 check_domain(schedule, code_schedule) ||
649 check_single_valued(code_schedule, sv) ||
650 check_order(schedule, code_schedule, sv);
652 pet_scop_free(scop);
653 isl_union_map_free(schedule);
654 isl_union_map_free(code_schedule);
655 isl_ctx_free(ctx);
657 return r;