privately export pet_stmt_is_affine_assume
[pet.git] / pet_check_code.c
blob6efe0f18dba3fdd18831c4423035df3cd7fab732
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 isl_set *s1, *s2;
196 isl_id *id1, *id2;
197 int r = 0;
199 dom1 = isl_union_map_domain(isl_union_map_copy(schedule));
200 dom2 = isl_union_map_domain(isl_union_map_copy(code_schedule));
201 equal = isl_union_set_is_equal(dom1, dom2);
203 if (equal < 0)
204 r = -1;
205 else if (!equal) {
206 isl_union_set_dump(dom1);
207 isl_union_set_dump(dom2);
208 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
209 "domains not identical", r = -1);
212 isl_union_set_free(dom1);
213 isl_union_set_free(dom2);
215 return r;
218 /* Check that the relative order specified by the input schedule is respected
219 * by the schedule extracted from the code, in case the original schedule
220 * is single valued.
222 * In particular, check that there is no pair of statement instances
223 * such that the first should be scheduled _before_ the second,
224 * but is actually scheduled _after_ the second in the code.
226 static int check_order_sv(__isl_keep isl_union_map *schedule,
227 __isl_keep isl_union_map *code_schedule)
229 isl_union_map *t1;
230 isl_union_map *t2;
231 int empty;
233 t1 = isl_union_map_lex_lt_union_map(isl_union_map_copy(schedule),
234 isl_union_map_copy(schedule));
235 t2 = isl_union_map_lex_gt_union_map(isl_union_map_copy(code_schedule),
236 isl_union_map_copy(code_schedule));
237 t1 = isl_union_map_intersect(t1, t2);
238 empty = isl_union_map_is_empty(t1);
239 isl_union_map_free(t1);
241 if (empty < 0)
242 return -1;
243 if (!empty)
244 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
245 "order not respected", return -1);
247 return 0;
250 /* Check that the relative order specified by the input schedule is respected
251 * by the schedule extracted from the code, in case the original schedule
252 * is not single valued.
254 * In particular, check that the order imposed by the schedules on pairs
255 * of statement instances is the same.
257 static int check_order_not_sv(__isl_keep isl_union_map *schedule,
258 __isl_keep isl_union_map *code_schedule)
260 isl_union_map *t1;
261 isl_union_map *t2;
262 int equal;
264 t1 = isl_union_map_lex_lt_union_map(isl_union_map_copy(schedule),
265 isl_union_map_copy(schedule));
266 t2 = isl_union_map_lex_lt_union_map(isl_union_map_copy(code_schedule),
267 isl_union_map_copy(code_schedule));
268 equal = isl_union_map_is_equal(t1, t2);
269 isl_union_map_free(t1);
270 isl_union_map_free(t2);
272 if (equal < 0)
273 return -1;
274 if (!equal)
275 isl_die(isl_union_map_get_ctx(schedule), isl_error_unknown,
276 "order not respected", return -1);
278 return 0;
281 /* Check that the relative order specified by the input schedule is respected
282 * by the schedule extracted from the code.
284 * "sv" indicated whether the original schedule is single valued.
285 * If so, we use a cheaper test. Otherwise, we fall back on a more
286 * expensive test.
288 static int check_order(__isl_keep isl_union_map *schedule,
289 __isl_keep isl_union_map *code_schedule, int sv)
291 if (sv)
292 return check_order_sv(schedule, code_schedule);
293 else
294 return check_order_not_sv(schedule, code_schedule);
297 /* If the original schedule was single valued ("sv" is set),
298 * then the schedule extracted from the code should be single valued as well.
300 static int check_single_valued(__isl_keep isl_union_map *code_schedule, int sv)
302 if (!sv)
303 return 0;
305 sv = isl_union_map_is_single_valued(code_schedule);
306 if (sv < 0)
307 return -1;
309 if (!sv)
310 isl_die(isl_union_map_get_ctx(code_schedule), isl_error_unknown,
311 "schedule not single valued", return -1);
313 return 0;
316 /* Read a schedule and a context from the first argument and
317 * C code from the second argument and check that the C code
318 * corresponds to the schedule on the context.
320 * In particular, check that
321 * - the domains are identical, i.e., the calls in the C code
322 * correspond to the domain elements of the schedule
323 * - no function is called twice with the same arguments, provided
324 * the schedule is single-valued
325 * - the calls are performed in an order that is compatible
326 * with the schedule
328 * If the schedule is not single-valued then we would have to check
329 * that each function with a given set of arguments is called
330 * the same number of times as there are images in the schedule,
331 * but this is considerably more difficult.
333 int main(int argc, char **argv)
335 isl_ctx *ctx;
336 isl_set *context;
337 isl_union_map *input_schedule, *code_schedule;
338 struct pet_scop *scop;
339 struct options *options;
340 FILE *file;
341 int r;
342 int sv;
344 options = options_new_with_defaults();
345 assert(options);
346 ctx = isl_ctx_alloc_with_options(&options_args, options);
347 pet_options_set_signed_overflow(ctx, PET_OVERFLOW_IGNORE);
348 argc = options_parse(options, argc, argv, ISL_ARG_ALL);
350 file = fopen(options->schedule, "r");
351 assert(file);
352 if (options->tree) {
353 isl_schedule *schedule;
354 isl_schedule_node *node;
355 enum isl_schedule_node_type type;
357 schedule = isl_schedule_read_from_file(ctx, file);
358 node = isl_schedule_get_root(schedule);
359 isl_options_set_schedule_separate_components(ctx, 0);
360 input_schedule =
361 isl_schedule_node_get_subtree_schedule_union_map(node);
362 node = isl_schedule_node_child(node, 0);
363 type = isl_schedule_node_get_type(node);
364 if (type == isl_schedule_node_context) {
365 context = isl_schedule_node_context_get_context(node);
366 } else {
367 isl_space *space;
368 space = isl_union_map_get_space(input_schedule);
369 context = isl_set_universe(space);
371 isl_schedule_node_free(node);
372 isl_schedule_free(schedule);
373 } else {
374 input_schedule = isl_union_map_read_from_file(ctx, file);
375 context = isl_set_read_from_file(ctx, file);
377 fclose(file);
379 scop = pet_scop_extract_from_C_source(ctx, options->code, NULL);
381 input_schedule = isl_union_map_intersect_params(input_schedule,
382 isl_set_copy(context));
383 code_schedule = extract_code_schedule(scop);
384 code_schedule = isl_union_map_intersect_params(code_schedule, context);
386 sv = isl_union_map_is_single_valued(input_schedule);
387 r = sv < 0 ||
388 check_domain(input_schedule, code_schedule) ||
389 check_single_valued(code_schedule, sv) ||
390 check_order(input_schedule, code_schedule, sv);
392 pet_scop_free(scop);
393 isl_union_map_free(input_schedule);
394 isl_union_map_free(code_schedule);
395 isl_ctx_free(ctx);
397 return r;