update isl to version 0.23
[pet.git] / pet_check_code.c
blob547065e1260c633e3357c5aad12b716c27ee7b12
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_set.h>
42 #include <isl/union_map.h>
43 #include <isl/id_to_pw_aff.h>
44 #include <isl/schedule_node.h>
45 #include <pet.h>
47 struct options {
48 struct isl_options *isl;
49 struct pet_options *pet;
50 char *schedule;
51 char *code;
52 unsigned tree;
55 ISL_ARGS_START(struct options, options_args)
56 ISL_ARG_CHILD(struct options, isl, "isl", &isl_options_args, "isl options")
57 ISL_ARG_CHILD(struct options, pet, NULL, &pet_options_args, "pet options")
58 ISL_ARG_ARG(struct options, schedule, "schedule", NULL)
59 ISL_ARG_ARG(struct options, code, "code", NULL)
60 ISL_ARG_BOOL(struct options, tree, 0, "tree", 0,
61 "input schedule is specified as schedule tree")
62 ISL_ARGS_END
64 ISL_ARG_DEF(options, struct options, options_args)
66 /* Extract an affine expression from "expr" in the form of an isl_map.
68 * The domain of the created expression is that of "pc".
70 static __isl_give isl_map *expr_extract_map(__isl_keep pet_expr *expr,
71 __isl_keep pet_context *pc)
73 isl_pw_aff *pa;
75 pa = pet_expr_extract_affine(expr, pc);
76 return isl_map_from_pw_aff(pa);
79 /* Extract a call from "stmt".
81 * The returned map is of the form
83 * { domain -> function[arguments] }
85 static __isl_give isl_map *stmt_extract_call(struct pet_stmt *stmt)
87 int i, n;
88 isl_set *domain;
89 isl_map *call;
90 const char *name;
91 pet_context *pc;
92 pet_expr *expr;
94 expr = pet_tree_expr_get_expr(stmt->body);
95 if (!expr)
96 return NULL;
97 if (pet_expr_get_type(expr) != pet_expr_call)
98 isl_die(pet_expr_get_ctx(expr),
99 isl_error_invalid, "expecting call statement",
100 goto error);
102 domain = isl_set_copy(stmt->domain);
103 call = isl_map_from_domain(domain);
105 pc = pet_context_alloc(isl_set_copy(stmt->domain));
106 n = pet_expr_get_n_arg(expr);
107 for (i = 0; i < n; ++i) {
108 isl_map *map_i;
109 pet_expr *arg;
111 arg = pet_expr_get_arg(expr, i);
112 map_i = expr_extract_map(arg, pc);
113 pet_expr_free(arg);
114 call = isl_map_flat_range_product(call, map_i);
116 pet_context_free(pc);
118 name = pet_expr_call_get_name(expr);
119 call = isl_map_set_tuple_name(call, isl_dim_out, name);
121 pet_expr_free(expr);
122 return call;
123 error:
124 pet_expr_free(expr);
125 return NULL;
128 /* Extract a mapping from the iterations domains of "scop" to
129 * the calls in the corresponding statements.
131 * We skip assignment and kill statements.
132 * Other than assignments and kill statements, all statements are assumed
133 * to be function calls.
135 static __isl_give isl_union_map *scop_collect_calls(struct pet_scop *scop)
137 int i;
138 isl_ctx *ctx;
139 isl_map *call_i;
140 isl_union_map *call;
142 if (!scop)
143 return NULL;
145 call = isl_union_map_empty(isl_set_get_space(scop->context));
146 ctx = isl_set_get_ctx(scop->context);
148 for (i = 0; i < scop->n_stmt; ++i) {
149 struct pet_stmt *stmt;
151 stmt = scop->stmts[i];
152 if (pet_stmt_is_assign(stmt))
153 continue;
154 if (pet_stmt_is_kill(stmt))
155 continue;
156 call_i = stmt_extract_call(scop->stmts[i]);
157 call = isl_union_map_add_map(call, call_i);
160 return call;
163 /* Extract a schedule on the original domains from "scop".
164 * The original domain elements appear as calls in "scop".
166 * We first extract a schedule on the code iteration domains
167 * and a mapping from the code iteration domains to the calls
168 * (i.e., the original domain) and then combine the two.
170 static __isl_give isl_union_map *extract_code_schedule(struct pet_scop *scop)
172 isl_schedule *schedule;
173 isl_union_map *schedule_map;
174 isl_union_map *calls;
176 schedule = pet_scop_get_schedule(scop);
177 schedule_map = isl_schedule_get_map(schedule);
178 isl_schedule_free(schedule);
180 calls = scop_collect_calls(scop);
182 schedule_map = isl_union_map_apply_domain(schedule_map, calls);
184 return schedule_map;
187 /* Check that schedule and code_schedule have the same domain,
188 * i.e., that they execute the same statement instances.
190 static int check_domain(__isl_keep isl_union_map *schedule,
191 __isl_keep isl_union_map *code_schedule)
193 isl_union_set *dom1, *dom2;
194 int equal;
195 int r = 0;
197 dom1 = isl_union_map_domain(isl_union_map_copy(schedule));
198 dom2 = isl_union_map_domain(isl_union_map_copy(code_schedule));
199 equal = isl_union_set_is_equal(dom1, dom2);
201 if (equal < 0)
202 r = -1;
203 else if (!equal) {
204 isl_union_set_dump(dom1);
205 isl_union_set_dump(dom2);
206 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
207 "domains not identical", r = -1);
210 isl_union_set_free(dom1);
211 isl_union_set_free(dom2);
213 return r;
216 /* Check that the relative order specified by the input schedule is respected
217 * by the schedule extracted from the code, in case the original schedule
218 * is single valued.
220 * In particular, check that there is no pair of statement instances
221 * such that the first should be scheduled _before_ the second,
222 * but is actually scheduled _after_ the second in the code.
224 static int check_order_sv(__isl_keep isl_union_map *schedule,
225 __isl_keep isl_union_map *code_schedule)
227 isl_union_map *t1;
228 isl_union_map *t2;
229 int empty;
231 t1 = isl_union_map_lex_lt_union_map(isl_union_map_copy(schedule),
232 isl_union_map_copy(schedule));
233 t2 = isl_union_map_lex_gt_union_map(isl_union_map_copy(code_schedule),
234 isl_union_map_copy(code_schedule));
235 t1 = isl_union_map_intersect(t1, t2);
236 empty = isl_union_map_is_empty(t1);
237 isl_union_map_free(t1);
239 if (empty < 0)
240 return -1;
241 if (!empty)
242 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
243 "order not respected", return -1);
245 return 0;
248 /* Check that the relative order specified by the input schedule is respected
249 * by the schedule extracted from the code, in case the original schedule
250 * is not single valued.
252 * In particular, check that the order imposed by the schedules on pairs
253 * of statement instances is the same.
255 static int check_order_not_sv(__isl_keep isl_union_map *schedule,
256 __isl_keep isl_union_map *code_schedule)
258 isl_union_map *t1;
259 isl_union_map *t2;
260 int equal;
262 t1 = isl_union_map_lex_lt_union_map(isl_union_map_copy(schedule),
263 isl_union_map_copy(schedule));
264 t2 = isl_union_map_lex_lt_union_map(isl_union_map_copy(code_schedule),
265 isl_union_map_copy(code_schedule));
266 equal = isl_union_map_is_equal(t1, t2);
267 isl_union_map_free(t1);
268 isl_union_map_free(t2);
270 if (equal < 0)
271 return -1;
272 if (!equal)
273 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
274 "order not respected", return -1);
276 return 0;
279 /* Check that the relative order specified by the input schedule is respected
280 * by the schedule extracted from the code.
282 * "sv" indicated whether the original schedule is single valued.
283 * If so, we use a cheaper test. Otherwise, we fall back on a more
284 * expensive test.
286 static int check_order(__isl_keep isl_union_map *schedule,
287 __isl_keep isl_union_map *code_schedule, int sv)
289 if (sv)
290 return check_order_sv(schedule, code_schedule);
291 else
292 return check_order_not_sv(schedule, code_schedule);
295 /* If the original schedule was single valued ("sv" is set),
296 * then the schedule extracted from the code should be single valued as well.
298 static int check_single_valued(__isl_keep isl_union_map *code_schedule, int sv)
300 if (!sv)
301 return 0;
303 sv = isl_union_map_is_single_valued(code_schedule);
304 if (sv < 0)
305 return -1;
307 if (!sv)
308 isl_die(isl_union_map_get_ctx(code_schedule), isl_error_unknown,
309 "schedule not single valued", return -1);
311 return 0;
314 /* Read a schedule and a context from the first argument and
315 * C code from the second argument and check that the C code
316 * corresponds to the schedule on the context.
318 * In particular, check that
319 * - the domains are identical, i.e., the calls in the C code
320 * correspond to the domain elements of the schedule
321 * - no function is called twice with the same arguments, provided
322 * the schedule is single-valued
323 * - the calls are performed in an order that is compatible
324 * with the schedule
326 * If the schedule is not single-valued then we would have to check
327 * that each function with a given set of arguments is called
328 * the same number of times as there are images in the schedule,
329 * but this is considerably more difficult.
331 int main(int argc, char **argv)
333 isl_ctx *ctx;
334 isl_set *context;
335 isl_union_map *input_schedule, *code_schedule;
336 struct pet_scop *scop;
337 struct options *options;
338 FILE *file;
339 int r;
340 int sv;
342 options = options_new_with_defaults();
343 assert(options);
344 ctx = isl_ctx_alloc_with_options(&options_args, options);
345 pet_options_set_signed_overflow(ctx, PET_OVERFLOW_IGNORE);
346 argc = options_parse(options, argc, argv, ISL_ARG_ALL);
348 file = fopen(options->schedule, "r");
349 assert(file);
350 if (options->tree) {
351 isl_schedule *schedule;
352 isl_schedule_node *node;
353 enum isl_schedule_node_type type;
355 schedule = isl_schedule_read_from_file(ctx, file);
356 node = isl_schedule_get_root(schedule);
357 isl_options_set_schedule_separate_components(ctx, 0);
358 input_schedule =
359 isl_schedule_node_get_subtree_schedule_union_map(node);
360 node = isl_schedule_node_child(node, 0);
361 type = isl_schedule_node_get_type(node);
362 if (type == isl_schedule_node_context) {
363 context = isl_schedule_node_context_get_context(node);
364 } else {
365 isl_space *space;
366 space = isl_union_map_get_space(input_schedule);
367 context = isl_set_universe(space);
369 isl_schedule_node_free(node);
370 isl_schedule_free(schedule);
371 } else {
372 input_schedule = isl_union_map_read_from_file(ctx, file);
373 context = isl_set_read_from_file(ctx, file);
375 fclose(file);
377 scop = pet_scop_extract_from_C_source(ctx, options->code, NULL);
379 input_schedule = isl_union_map_intersect_params(input_schedule,
380 isl_set_copy(context));
381 code_schedule = extract_code_schedule(scop);
382 code_schedule = isl_union_map_intersect_params(code_schedule, context);
384 sv = isl_union_map_is_single_valued(input_schedule);
385 r = sv < 0 ||
386 check_domain(input_schedule, code_schedule) ||
387 check_single_valued(code_schedule, sv) ||
388 check_order(input_schedule, code_schedule, sv);
390 pet_scop_free(scop);
391 isl_union_map_free(input_schedule);
392 isl_union_map_free(code_schedule);
393 isl_ctx_free(ctx);
395 return r;