1 |
280 |
jeremybenn |
/* 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, 2009 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_d
|
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_d
|
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_d)));
|
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 */
|