|
0
|
1 /* Source code for an implementation of the Omega test, an integer
|
|
|
2 programming algorithm for dependence analysis, by William Pugh,
|
|
|
3 appeared in Supercomputing '91 and CACM Aug 92.
|
|
|
4
|
|
|
5 This code has no license restrictions, and is considered public
|
|
|
6 domain.
|
|
|
7
|
|
|
8 Changes copyright (C) 2005, 2006, 2007 Free Software Foundation, Inc.
|
|
|
9 Contributed by Sebastian Pop <sebastian.pop@inria.fr>
|
|
|
10
|
|
|
11 This file is part of GCC.
|
|
|
12
|
|
|
13 GCC is free software; you can redistribute it and/or modify it under
|
|
|
14 the terms of the GNU General Public License as published by the Free
|
|
|
15 Software Foundation; either version 3, or (at your option) any later
|
|
|
16 version.
|
|
|
17
|
|
|
18 GCC is distributed in the hope that it will be useful, but WITHOUT ANY
|
|
|
19 WARRANTY; without even the implied warranty of MERCHANTABILITY or
|
|
|
20 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
|
|
21 for more details.
|
|
|
22
|
|
|
23 You should have received a copy of the GNU General Public License
|
|
|
24 along with GCC; see the file COPYING3. If not see
|
|
|
25 <http://www.gnu.org/licenses/>. */
|
|
|
26
|
|
|
27 #include "config.h"
|
|
|
28 #include "params.h"
|
|
|
29
|
|
|
30 #ifndef GCC_OMEGA_H
|
|
|
31 #define GCC_OMEGA_H
|
|
|
32
|
|
|
33 #define OMEGA_MAX_VARS PARAM_VALUE (PARAM_OMEGA_MAX_VARS)
|
|
|
34 #define OMEGA_MAX_GEQS PARAM_VALUE (PARAM_OMEGA_MAX_GEQS)
|
|
|
35 #define OMEGA_MAX_EQS PARAM_VALUE (PARAM_OMEGA_MAX_EQS)
|
|
|
36
|
|
|
37 #define pos_infinity (0x7ffffff)
|
|
|
38 #define neg_infinity (-0x7ffffff)
|
|
|
39
|
|
|
40 /* Results of the Omega solver. */
|
|
|
41 enum omega_result {
|
|
|
42 omega_false = 0,
|
|
|
43 omega_true = 1,
|
|
|
44
|
|
|
45 /* Value returned when the solver is unable to determine an
|
|
|
46 answer. */
|
|
|
47 omega_unknown = 2,
|
|
|
48
|
|
|
49 /* Value used for asking the solver to simplify the system. */
|
|
|
50 omega_simplify = 3
|
|
|
51 };
|
|
|
52
|
|
|
53 /* Values used for labeling equations. Private (not used outside the
|
|
|
54 solver). */
|
|
|
55 enum omega_eqn_color {
|
|
|
56 omega_black = 0,
|
|
|
57 omega_red = 1
|
|
|
58 };
|
|
|
59
|
|
|
60 /* Structure for equations. */
|
|
|
61 typedef struct eqn
|
|
|
62 {
|
|
|
63 int key;
|
|
|
64 int touched;
|
|
|
65 enum omega_eqn_color color;
|
|
|
66
|
|
|
67 /* Array of coefficients for the equation. The layout of the data
|
|
|
68 is as follows: coef[0] is the constant, coef[i] for 1 <= i <=
|
|
|
69 OMEGA_MAX_VARS, are the coefficients for each dimension. Examples:
|
|
|
70 the equation 0 = 9 + x + 0y + 5z is encoded as [9 1 0 5], the
|
|
|
71 inequality 0 <= -8 + x + 2y + 3z is encoded as [-8 1 2 3]. */
|
|
|
72 int *coef;
|
|
|
73 } *eqn;
|
|
|
74
|
|
|
75 typedef struct omega_pb
|
|
|
76 {
|
|
|
77 /* The number of variables in the system of equations. */
|
|
|
78 int num_vars;
|
|
|
79
|
|
|
80 /* Safe variables are not eliminated during the Fourier-Motzkin
|
|
|
81 simplification of the system. Safe variables are all those
|
|
|
82 variables that are placed at the beginning of the array of
|
|
|
83 variables: PB->var[1, ..., SAFE_VARS]. PB->var[0] is not used,
|
|
|
84 as PB->eqs[x]->coef[0] represents the constant of the equation. */
|
|
|
85 int safe_vars;
|
|
|
86
|
|
|
87 /* Number of elements in eqs[]. */
|
|
|
88 int num_eqs;
|
|
|
89 /* Number of elements in geqs[]. */
|
|
|
90 int num_geqs;
|
|
|
91 /* Number of elements in subs[]. */
|
|
|
92 int num_subs;
|
|
|
93
|
|
|
94 int hash_version;
|
|
|
95 bool variables_initialized;
|
|
|
96 bool variables_freed;
|
|
|
97
|
|
|
98 /* Index or name of variables. Negative integers are reserved for
|
|
|
99 wildcard variables. Maps the index of variables in the original
|
|
|
100 problem to the new index of the variable. The index for a
|
|
|
101 variable in the coef array of an equation can change as some
|
|
|
102 variables are eliminated. */
|
|
|
103 int *var;
|
|
|
104
|
|
|
105 int *forwarding_address;
|
|
|
106
|
|
|
107 /* Inequalities in the system of constraints. */
|
|
|
108 eqn geqs;
|
|
|
109
|
|
|
110 /* Equations in the system of constraints. */
|
|
|
111 eqn eqs;
|
|
|
112
|
|
|
113 /* A map of substituted variables. */
|
|
|
114 eqn subs;
|
|
|
115 } *omega_pb;
|
|
|
116
|
|
|
117 extern void omega_initialize (void);
|
|
|
118 extern omega_pb omega_alloc_problem (int, int);
|
|
|
119 extern enum omega_result omega_solve_problem (omega_pb, enum omega_result);
|
|
|
120 extern enum omega_result omega_simplify_problem (omega_pb);
|
|
|
121 extern enum omega_result omega_simplify_approximate (omega_pb);
|
|
|
122 extern enum omega_result omega_constrain_variable_sign (omega_pb,
|
|
|
123 enum omega_eqn_color,
|
|
|
124 int, int);
|
|
|
125 extern void debug_omega_problem (omega_pb);
|
|
|
126 extern void omega_print_problem (FILE *, omega_pb);
|
|
|
127 extern void omega_print_red_equations (FILE *, omega_pb);
|
|
|
128 extern int omega_count_red_equations (omega_pb);
|
|
|
129 extern void omega_pretty_print_problem (FILE *, omega_pb);
|
|
|
130 extern void omega_unprotect_variable (omega_pb, int var);
|
|
|
131 extern void omega_negate_geq (omega_pb, int);
|
|
|
132 extern void omega_convert_eq_to_geqs (omega_pb, int eq);
|
|
|
133 extern void omega_print_eqn (FILE *, omega_pb, eqn, bool, int);
|
|
|
134 extern bool omega_problem_has_red_equations (omega_pb);
|
|
|
135 extern enum omega_result omega_eliminate_redundant (omega_pb, bool);
|
|
|
136 extern void omega_eliminate_red (omega_pb, bool);
|
|
|
137 extern void omega_constrain_variable_value (omega_pb, enum omega_eqn_color,
|
|
|
138 int, int);
|
|
|
139 extern bool omega_query_variable (omega_pb, int, int *, int *);
|
|
|
140 extern int omega_query_variable_signs (omega_pb, int, int, int, int,
|
|
|
141 int, int, bool *, int *);
|
|
|
142 extern bool omega_query_variable_bounds (omega_pb, int, int *, int *);
|
|
|
143 extern void (*omega_when_reduced) (omega_pb);
|
|
|
144 extern void omega_no_procedure (omega_pb);
|
|
|
145
|
|
|
146 /* Return true when variable I in problem PB is a wildcard. */
|
|
|
147
|
|
|
148 static inline bool
|
|
|
149 omega_wildcard_p (omega_pb pb, int i)
|
|
|
150 {
|
|
|
151 return (pb->var[i] < 0);
|
|
|
152 }
|
|
|
153
|
|
|
154 /* Return true when variable I in problem PB is a safe variable. */
|
|
|
155
|
|
|
156 static inline bool
|
|
|
157 omega_safe_var_p (omega_pb pb, int i)
|
|
|
158 {
|
|
|
159 /* The constant of an equation is not a variable. */
|
|
|
160 gcc_assert (0 < i);
|
|
|
161 return (i <= pb->safe_vars);
|
|
|
162 }
|
|
|
163
|
|
|
164 /* Print to FILE equality E from PB. */
|
|
|
165
|
|
|
166 static inline void
|
|
|
167 omega_print_eq (FILE *file, omega_pb pb, eqn e)
|
|
|
168 {
|
|
|
169 omega_print_eqn (file, pb, e, false, 0);
|
|
|
170 }
|
|
|
171
|
|
|
172 /* Print to FILE inequality E from PB. */
|
|
|
173
|
|
|
174 static inline void
|
|
|
175 omega_print_geq (FILE *file, omega_pb pb, eqn e)
|
|
|
176 {
|
|
|
177 omega_print_eqn (file, pb, e, true, 0);
|
|
|
178 }
|
|
|
179
|
|
|
180 /* Print to FILE inequality E from PB. */
|
|
|
181
|
|
|
182 static inline void
|
|
|
183 omega_print_geq_extra (FILE *file, omega_pb pb, eqn e)
|
|
|
184 {
|
|
|
185 omega_print_eqn (file, pb, e, true, 1);
|
|
|
186 }
|
|
|
187
|
|
|
188 /* E1 = E2, make a copy of E2 into E1. Equations contain S variables. */
|
|
|
189
|
|
|
190 static inline void
|
|
|
191 omega_copy_eqn (eqn e1, eqn e2, int s)
|
|
|
192 {
|
|
|
193 e1->key = e2->key;
|
|
|
194 e1->touched = e2->touched;
|
|
|
195 e1->color = e2->color;
|
|
|
196
|
|
|
197 memcpy (e1->coef, e2->coef, (s + 1) * sizeof (int));
|
|
|
198 }
|
|
|
199
|
|
|
200 /* Initialize E = 0. Equation E contains S variables. */
|
|
|
201
|
|
|
202 static inline void
|
|
|
203 omega_init_eqn_zero (eqn e, int s)
|
|
|
204 {
|
|
|
205 e->key = 0;
|
|
|
206 e->touched = 0;
|
|
|
207 e->color = omega_black;
|
|
|
208
|
|
|
209 memset (e->coef, 0, (s + 1) * sizeof (int));
|
|
|
210 }
|
|
|
211
|
|
|
212 /* Allocate N equations with S variables. */
|
|
|
213
|
|
|
214 static inline eqn
|
|
|
215 omega_alloc_eqns (int s, int n)
|
|
|
216 {
|
|
|
217 int i;
|
|
|
218 eqn res = (eqn) (xcalloc (n, sizeof (struct eqn)));
|
|
|
219
|
|
|
220 for (i = n - 1; i >= 0; i--)
|
|
|
221 {
|
|
|
222 res[i].coef = (int *) (xcalloc (OMEGA_MAX_VARS + 1, sizeof (int)));
|
|
|
223 omega_init_eqn_zero (&res[i], s);
|
|
|
224 }
|
|
|
225
|
|
|
226 return res;
|
|
|
227 }
|
|
|
228
|
|
|
229 /* Free N equations from array EQ. */
|
|
|
230
|
|
|
231 static inline void
|
|
|
232 omega_free_eqns (eqn eq, int n)
|
|
|
233 {
|
|
|
234 int i;
|
|
|
235
|
|
|
236 for (i = n - 1; i >= 0; i--)
|
|
|
237 free (eq[i].coef);
|
|
|
238
|
|
|
239 free (eq);
|
|
|
240 }
|
|
|
241
|
|
|
242 /* Returns true when E is an inequality with a single variable. */
|
|
|
243
|
|
|
244 static inline bool
|
|
|
245 single_var_geq (eqn e, int nv ATTRIBUTE_UNUSED)
|
|
|
246 {
|
|
|
247 return (e->key != 0
|
|
|
248 && -OMEGA_MAX_VARS <= e->key && e->key <= OMEGA_MAX_VARS);
|
|
|
249 }
|
|
|
250
|
|
|
251 /* Allocate a new equality with all coefficients 0, and tagged with
|
|
|
252 COLOR. Return the index of this equality in problem PB. */
|
|
|
253
|
|
|
254 static inline int
|
|
|
255 omega_add_zero_eq (omega_pb pb, enum omega_eqn_color color)
|
|
|
256 {
|
|
|
257 int idx = pb->num_eqs++;
|
|
|
258
|
|
|
259 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
|
|
|
260 omega_init_eqn_zero (&pb->eqs[idx], pb->num_vars);
|
|
|
261 pb->eqs[idx].color = color;
|
|
|
262 return idx;
|
|
|
263 }
|
|
|
264
|
|
|
265 /* Allocate a new inequality with all coefficients 0, and tagged with
|
|
|
266 COLOR. Return the index of this inequality in problem PB. */
|
|
|
267
|
|
|
268 static inline int
|
|
|
269 omega_add_zero_geq (omega_pb pb, enum omega_eqn_color color)
|
|
|
270 {
|
|
|
271 int idx = pb->num_geqs;
|
|
|
272
|
|
|
273 pb->num_geqs++;
|
|
|
274 gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
|
|
|
275 omega_init_eqn_zero (&pb->geqs[idx], pb->num_vars);
|
|
|
276 pb->geqs[idx].touched = 1;
|
|
|
277 pb->geqs[idx].color = color;
|
|
|
278 return idx;
|
|
|
279 }
|
|
|
280
|
|
|
281 /* Initialize variables for problem PB. */
|
|
|
282
|
|
|
283 static inline void
|
|
|
284 omega_initialize_variables (omega_pb pb)
|
|
|
285 {
|
|
|
286 int i;
|
|
|
287
|
|
|
288 for (i = pb->num_vars; i >= 0; i--)
|
|
|
289 pb->forwarding_address[i] = pb->var[i] = i;
|
|
|
290
|
|
|
291 pb->variables_initialized = true;
|
|
|
292 }
|
|
|
293
|
|
|
294 /* Free problem PB. */
|
|
|
295
|
|
|
296 static inline void
|
|
|
297 omega_free_problem (omega_pb pb)
|
|
|
298 {
|
|
|
299 free (pb->var);
|
|
|
300 free (pb->forwarding_address);
|
|
|
301 omega_free_eqns (pb->geqs, OMEGA_MAX_GEQS);
|
|
|
302 omega_free_eqns (pb->eqs, OMEGA_MAX_EQS);
|
|
|
303 omega_free_eqns (pb->subs, OMEGA_MAX_VARS + 1);
|
|
|
304 free (pb);
|
|
|
305 }
|
|
|
306
|
|
|
307 /* Copy omega problems: P1 = P2. */
|
|
|
308
|
|
|
309 static inline void
|
|
|
310 omega_copy_problem (omega_pb p1, omega_pb p2)
|
|
|
311 {
|
|
|
312 int e, i;
|
|
|
313
|
|
|
314 p1->num_vars = p2->num_vars;
|
|
|
315 p1->hash_version = p2->hash_version;
|
|
|
316 p1->variables_initialized = p2->variables_initialized;
|
|
|
317 p1->variables_freed = p2->variables_freed;
|
|
|
318 p1->safe_vars = p2->safe_vars;
|
|
|
319 p1->num_eqs = p2->num_eqs;
|
|
|
320 p1->num_subs = p2->num_subs;
|
|
|
321 p1->num_geqs = p2->num_geqs;
|
|
|
322
|
|
|
323 for (e = p2->num_eqs - 1; e >= 0; e--)
|
|
|
324 omega_copy_eqn (&(p1->eqs[e]), &(p2->eqs[e]), p2->num_vars);
|
|
|
325
|
|
|
326 for (e = p2->num_geqs - 1; e >= 0; e--)
|
|
|
327 omega_copy_eqn (&(p1->geqs[e]), &(p2->geqs[e]), p2->num_vars);
|
|
|
328
|
|
|
329 for (e = p2->num_subs - 1; e >= 0; e--)
|
|
|
330 omega_copy_eqn (&(p1->subs[e]), &(p2->subs[e]), p2->num_vars);
|
|
|
331
|
|
|
332 for (i = p2->num_vars; i >= 0; i--)
|
|
|
333 p1->var[i] = p2->var[i];
|
|
|
334
|
|
|
335 for (i = OMEGA_MAX_VARS; i >= 0; i--)
|
|
|
336 p1->forwarding_address[i] = p2->forwarding_address[i];
|
|
|
337 }
|
|
|
338
|
|
|
339 #endif /* GCC_OMEGA_H */
|
