add functions for manipulating the domain of a pet_context
[pet.git] / pet_check_code.c
blob3360577d6cb7e15b554b92c0cf6e85f4f8e5ddd7
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 #include "aff.h"
47 struct options {
48 struct isl_options *isl;
49 struct pet_options *pet;
50 char *schedule;
51 char *code;
54 ISL_ARGS_START(struct options, options_args)
55 ISL_ARG_CHILD(struct options, isl, "isl", &isl_options_args, "isl options")
56 ISL_ARG_CHILD(struct options, pet, NULL, &pet_options_args, "pet options")
57 ISL_ARG_ARG(struct options, schedule, "schedule", NULL)
58 ISL_ARG_ARG(struct options, code, "code", NULL)
59 ISL_ARGS_END
61 ISL_ARG_DEF(options, struct options, options_args)
63 static __isl_give isl_pw_aff *expr_extract_pw_aff(__isl_keep pet_expr *expr,
64 __isl_keep isl_space *space);
66 /* Extract an affine expression from the call to floord in "expr".
68 * "space" is the iteration space of the statement containing the expression.
70 static __isl_give isl_pw_aff *expr_extract_floord(__isl_keep pet_expr *expr,
71 __isl_keep isl_space *space)
73 isl_pw_aff *lhs, *rhs;
74 pet_expr *arg;
76 arg = pet_expr_get_arg(expr, 0);
77 lhs = expr_extract_pw_aff(arg, space);
78 pet_expr_free(arg);
79 arg = pet_expr_get_arg(expr, 1);
80 rhs = expr_extract_pw_aff(arg, space);
81 pet_expr_free(arg);
82 return isl_pw_aff_floor(isl_pw_aff_div(lhs, rhs));
85 /* Extract an affine expression from the call in "expr".
87 * "space" is the iteration space of the statement containing the expression.
89 * We only support calls to the "floord" function for now.
91 static __isl_give isl_pw_aff *call_expr_extract_pw_aff(
92 __isl_keep pet_expr *expr, __isl_keep isl_space *space)
94 const char *name;
96 name = pet_expr_call_get_name(expr);
97 if (!name)
98 return NULL;
99 if (!strcmp(name, "floord"))
100 return expr_extract_floord(expr, space);
102 isl_die(isl_space_get_ctx(space), isl_error_unsupported,
103 "unsupported expression", return NULL);
106 /* Extract an affine expression from the access to a named space in "index".
108 * We assume we are accessing a 0D space and
109 * we turn that into an expression equal to a parameter of the same name.
111 static __isl_give isl_pw_aff *resolve_access(__isl_take isl_multi_pw_aff *index)
113 isl_id *id;
114 isl_set *dom;
115 isl_aff *aff;
116 isl_local_space *ls;
117 isl_pw_aff *pa;
119 id = isl_multi_pw_aff_get_tuple_id(index, isl_dim_out);
120 dom = isl_multi_pw_aff_domain(index);
121 dom = isl_set_insert_dims(dom, isl_dim_param, 0, 1);
122 dom = isl_set_set_dim_id(dom, isl_dim_param, 0, id);
123 ls = isl_local_space_from_space(isl_set_get_space(dom));
124 aff = isl_aff_var_on_domain(ls, isl_dim_param, 0);
125 pa = isl_pw_aff_alloc(dom, aff);
127 return pa;
130 /* Extract an affine expression from the access expression "expr".
132 * If we are accessing a (1D) anonymous space, then we are actually
133 * computing an affine expression and we simply return that expression.
134 * Otherwise, we try and convert the access to an affine expression in
135 * resolve_access().
137 static __isl_give isl_pw_aff *access_expr_extract_pw_aff(
138 __isl_keep pet_expr *expr)
140 isl_pw_aff *pa;
141 isl_multi_pw_aff *index;
143 index = pet_expr_access_get_index(expr);
144 if (isl_multi_pw_aff_has_tuple_id(index, isl_dim_out)) {
145 pa = resolve_access(index);
146 } else {
147 pa = isl_multi_pw_aff_get_pw_aff(index, 0);
148 isl_multi_pw_aff_free(index);
150 return pa;
153 /* Extract an affine expression defined over iteration space "space"
154 * from the integer expression "expr".
156 static __isl_give isl_pw_aff *int_expr_extract_pw_aff(
157 __isl_keep pet_expr *expr, __isl_keep isl_space *space)
159 isl_local_space *ls;
160 isl_aff *aff;
162 ls = isl_local_space_from_space(isl_space_copy(space));
163 aff = isl_aff_zero_on_domain(ls);
164 aff = isl_aff_add_constant_val(aff, pet_expr_int_get_val(expr));
165 return isl_pw_aff_from_aff(aff);
168 /* Extract an affine expression from the operation in "expr".
170 * "space" is the iteration space of the statement containing the expression.
172 * We only handle the kinds of expressions that we would expect
173 * as arguments to a function call in code generated by isl.
175 static __isl_give isl_pw_aff *op_expr_extract_pw_aff(__isl_keep pet_expr *expr,
176 __isl_keep isl_space *space)
178 isl_pw_aff *pa, *pa1, *pa2;
179 pet_expr *arg;
180 enum pet_op_type type;
182 switch (pet_expr_get_n_arg(expr)) {
183 case 1:
184 if (pet_expr_op_get_type(expr) == pet_op_minus) {
185 arg = pet_expr_get_arg(expr, 0);
186 pa = expr_extract_pw_aff(arg, space);
187 pet_expr_free(arg);
188 return isl_pw_aff_neg(pa);
190 assert(0);
191 case 2:
192 arg = pet_expr_get_arg(expr, 0);
193 pa1 = expr_extract_pw_aff(arg, space);
194 pet_expr_free(arg);
195 arg = pet_expr_get_arg(expr, 1);
196 pa2 = expr_extract_pw_aff(arg, space);
197 pet_expr_free(arg);
198 type = pet_expr_op_get_type(expr);
199 switch (type) {
200 case pet_op_mul:
201 pa = isl_pw_aff_mul(pa1, pa2);
202 break;
203 case pet_op_add:
204 pa = isl_pw_aff_add(pa1, pa2);
205 break;
206 case pet_op_sub:
207 pa = isl_pw_aff_sub(pa1, pa2);
208 break;
209 case pet_op_div:
210 pa = isl_pw_aff_tdiv_q(pa1, pa2);
211 break;
212 case pet_op_mod:
213 pa = isl_pw_aff_tdiv_r(pa1, pa2);
214 break;
215 case pet_op_eq:
216 case pet_op_ne:
217 case pet_op_le:
218 case pet_op_ge:
219 case pet_op_lt:
220 case pet_op_gt:
221 pa = pet_comparison(type, pa1, pa2);
222 break;
223 case pet_op_land:
224 case pet_op_lor:
225 pa = pet_boolean(type, pa1, pa2);
226 break;
227 default:
228 assert(0);
230 return pa;
231 case 3:
232 arg = pet_expr_get_arg(expr, 0);
233 pa = expr_extract_pw_aff(arg, space);
234 pet_expr_free(arg);
235 arg = pet_expr_get_arg(expr, 1);
236 pa1 = expr_extract_pw_aff(arg, space);
237 pet_expr_free(arg);
238 arg = pet_expr_get_arg(expr, 2);
239 pa2 = expr_extract_pw_aff(arg, space);
240 pet_expr_free(arg);
241 return isl_pw_aff_cond(pa, pa1, pa2);
242 default:
243 assert(0);
247 /* Extract an affine expression from "expr" in the form of an isl_pw_aff.
249 * "space" is the iteration space of the statement containing the expression.
251 * We only handle the kinds of expressions that we would expect
252 * as arguments to a function call in code generated by isl.
254 static __isl_give isl_pw_aff *expr_extract_pw_aff(__isl_keep pet_expr *expr,
255 __isl_keep isl_space *space)
257 switch (pet_expr_get_type(expr)) {
258 case pet_expr_int:
259 return int_expr_extract_pw_aff(expr, space);
260 case pet_expr_access:
261 return access_expr_extract_pw_aff(expr);
262 case pet_expr_op:
263 return op_expr_extract_pw_aff(expr, space);
264 case pet_expr_call:
265 return call_expr_extract_pw_aff(expr, space);
266 case pet_expr_cast:
267 case pet_expr_double:
268 case pet_expr_error:
269 assert(0);
273 /* Extract an affine expression from "expr" in the form of an isl_map.
275 * "space" is the iteration space of the statement containing the expression.
277 static __isl_give isl_map *expr_extract_map(__isl_keep pet_expr *expr,
278 __isl_keep isl_space *space)
280 isl_pw_aff *pa;
282 pa = expr_extract_pw_aff(expr, space);
283 return isl_map_from_pw_aff(pa);
286 /* Extract a call from "stmt".
288 * The returned map is of the form
290 * { domain -> function[arguments] }
292 static __isl_give isl_map *stmt_extract_call(struct pet_stmt *stmt)
294 int i, n;
295 isl_set *domain;
296 isl_map *call;
297 const char *name;
299 domain = isl_set_copy(stmt->domain);
300 call = isl_map_from_domain(domain);
302 assert(pet_expr_get_type(stmt->body) == pet_expr_call);
304 n = pet_expr_get_n_arg(stmt->body);
305 for (i = 0; i < n; ++i) {
306 isl_map *map_i;
307 isl_space *space;
308 pet_expr *arg;
310 arg = pet_expr_get_arg(stmt->body, i);
311 space = pet_stmt_get_space(stmt);
312 map_i = expr_extract_map(arg, space);
313 isl_space_free(space);
314 pet_expr_free(arg);
315 call = isl_map_flat_range_product(call, map_i);
318 name = pet_expr_call_get_name(stmt->body);
319 call = isl_map_set_tuple_name(call, isl_dim_out, name);
321 return call;
324 /* Extract a mapping from the iterations domains of "scop" to
325 * the calls in the corresponding statements.
327 * We skip assignment and kill statements.
328 * Other than assignments and kill statements, all statements are assumed
329 * to be function calls.
331 static __isl_give isl_union_map *scop_collect_calls(struct pet_scop *scop)
333 int i;
334 isl_ctx *ctx;
335 isl_map *call_i;
336 isl_union_map *call;
338 if (!scop)
339 return NULL;
341 call = isl_union_map_empty(isl_set_get_space(scop->context));
342 ctx = isl_set_get_ctx(scop->context);
344 for (i = 0; i < scop->n_stmt; ++i) {
345 struct pet_stmt *stmt;
347 stmt = scop->stmts[i];
348 if (pet_stmt_is_assign(stmt))
349 continue;
350 if (pet_stmt_is_kill(stmt))
351 continue;
352 call_i = stmt_extract_call(scop->stmts[i]);
353 call = isl_union_map_add_map(call, call_i);
356 return call;
359 /* Extract a schedule on the original domains from "scop".
360 * The original domain elements appear as calls in "scop".
362 * We first extract a schedule on the code iteration domains
363 * and a mapping from the code iteration domains to the calls
364 * (i.e., the original domain) and then combine the two.
366 static __isl_give isl_union_map *extract_code_schedule(struct pet_scop *scop)
368 isl_union_map *schedule;
369 isl_union_map *calls;
371 schedule = pet_scop_collect_schedule(scop);
373 calls = scop_collect_calls(scop);
375 schedule = isl_union_map_apply_domain(schedule, calls);
377 return schedule;
380 /* Check that schedule and code_schedule have the same domain,
381 * i.e., that they execute the same statement instances.
383 static int check_domain(__isl_keep isl_union_map *schedule,
384 __isl_keep isl_union_map *code_schedule)
386 isl_union_set *dom1, *dom2;
387 int equal;
388 isl_set *s1, *s2;;
389 isl_id *id1, *id2;
390 int r = 0;
392 dom1 = isl_union_map_domain(isl_union_map_copy(schedule));
393 dom2 = isl_union_map_domain(isl_union_map_copy(code_schedule));
394 equal = isl_union_set_is_equal(dom1, dom2);
396 if (equal < 0)
397 r = -1;
398 else if (!equal) {
399 isl_union_set_dump(dom1);
400 isl_union_set_dump(dom2);
401 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
402 "domains not identical", r = -1);
405 isl_union_set_free(dom1);
406 isl_union_set_free(dom2);
408 return r;
411 /* Check that the relative order specified by the input schedule is respected
412 * by the schedule extracted from the code, in case the original schedule
413 * is single valued.
415 * In particular, check that there is no pair of statement instances
416 * such that the first should be scheduled _before_ the second,
417 * but is actually scheduled _after_ the second in the code.
419 static int check_order_sv(__isl_keep isl_union_map *schedule,
420 __isl_keep isl_union_map *code_schedule)
422 isl_union_map *t1;
423 isl_union_map *t2;
424 int empty;
426 t1 = isl_union_map_lex_lt_union_map(isl_union_map_copy(schedule),
427 isl_union_map_copy(schedule));
428 t2 = isl_union_map_lex_gt_union_map(isl_union_map_copy(code_schedule),
429 isl_union_map_copy(code_schedule));
430 t1 = isl_union_map_intersect(t1, t2);
431 empty = isl_union_map_is_empty(t1);
432 isl_union_map_free(t1);
434 if (empty < 0)
435 return -1;
436 if (!empty)
437 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
438 "order not respected", return -1);
440 return 0;
443 /* Check that the relative order specified by the input schedule is respected
444 * by the schedule extracted from the code, in case the original schedule
445 * is not single valued.
447 * In particular, check that the order imposed by the schedules on pairs
448 * of statement instances is the same.
450 static int check_order_not_sv(__isl_keep isl_union_map *schedule,
451 __isl_keep isl_union_map *code_schedule)
453 isl_union_map *t1;
454 isl_union_map *t2;
455 int equal;
457 t1 = isl_union_map_lex_lt_union_map(isl_union_map_copy(schedule),
458 isl_union_map_copy(schedule));
459 t2 = isl_union_map_lex_lt_union_map(isl_union_map_copy(code_schedule),
460 isl_union_map_copy(code_schedule));
461 equal = isl_union_map_is_equal(t1, t2);
462 isl_union_map_free(t1);
463 isl_union_map_free(t2);
465 if (equal < 0)
466 return -1;
467 if (!equal)
468 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
469 "order not respected", return -1);
471 return 0;
474 /* Check that the relative order specified by the input schedule is respected
475 * by the schedule extracted from the code.
477 * "sv" indicated whether the original schedule is single valued.
478 * If so, we use a cheaper test. Otherwise, we fall back on a more
479 * expensive test.
481 static int check_order(__isl_keep isl_union_map *schedule,
482 __isl_keep isl_union_map *code_schedule, int sv)
484 if (sv)
485 return check_order_sv(schedule, code_schedule);
486 else
487 return check_order_not_sv(schedule, code_schedule);
490 /* If the original schedule was single valued ("sv" is set),
491 * then the schedule extracted from the code should be single valued as well.
493 static int check_single_valued(__isl_keep isl_union_map *code_schedule, int sv)
495 if (!sv)
496 return 0;
498 sv = isl_union_map_is_single_valued(code_schedule);
499 if (sv < 0)
500 return -1;
502 if (!sv)
503 isl_die(isl_union_map_get_ctx(code_schedule), isl_error_unknown,
504 "schedule not single valued", return -1);
506 return 0;
509 /* Read a schedule and a context from the first argument and
510 * C code from the second argument and check that the C code
511 * corresponds to the schedule on the context.
513 * In particular, check that
514 * - the domains are identical, i.e., the calls in the C code
515 * correspond to the domain elements of the schedule
516 * - no function is called twice with the same arguments, provided
517 * the schedule is single-valued
518 * - the calls are performed in an order that is compatible
519 * with the schedule
521 * If the schedule is not single-valued then we would have to check
522 * that each function with a given set of arguments is called
523 * the same number of times as there are images in the schedule,
524 * but this is considerably more difficult.
526 int main(int argc, char **argv)
528 isl_ctx *ctx;
529 isl_set *context;
530 isl_union_map *schedule, *code_schedule;
531 struct pet_scop *scop;
532 struct options *options;
533 FILE *file;
534 int r;
535 int sv;
537 options = options_new_with_defaults();
538 assert(options);
539 ctx = isl_ctx_alloc_with_options(&options_args, options);
540 pet_options_set_signed_overflow(ctx, PET_OVERFLOW_IGNORE);
541 argc = options_parse(options, argc, argv, ISL_ARG_ALL);
543 file = fopen(options->schedule, "r");
544 assert(file);
545 schedule = isl_union_map_read_from_file(ctx, file);
546 context = isl_set_read_from_file(ctx, file);
547 fclose(file);
549 scop = pet_scop_extract_from_C_source(ctx, options->code, NULL);
551 schedule = isl_union_map_intersect_params(schedule,
552 isl_set_copy(context));
553 code_schedule = extract_code_schedule(scop);
554 code_schedule = isl_union_map_intersect_params(code_schedule, context);
556 sv = isl_union_map_is_single_valued(schedule);
557 r = sv < 0 ||
558 check_domain(schedule, code_schedule) ||
559 check_single_valued(code_schedule, sv) ||
560 check_order(schedule, code_schedule, sv);
562 pet_scop_free(scop);
563 isl_union_map_free(schedule);
564 isl_union_map_free(code_schedule);
565 isl_ctx_free(ctx);
567 return r;