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-2015 Free Software Foundation, Inc. 9 Contributed by Sebastian Pop <sebastian.pop@inria.fr> 10 11This file is part of GCC. 12 13GCC is free software; you can redistribute it and/or modify it under 14the terms of the GNU General Public License as published by the Free 15Software Foundation; either version 3, or (at your option) any later 16version. 17 18GCC is distributed in the hope that it will be useful, but WITHOUT ANY 19WARRANTY; without even the implied warranty of MERCHANTABILITY or 20FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 21for more details. 22 23You should have received a copy of the GNU General Public License 24along 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. */ 41enum 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). */ 55enum omega_eqn_color { 56 omega_black = 0, 57 omega_red = 1 58}; 59 60/* Structure for equations. */ 61typedef 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 75typedef 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 117extern void omega_initialize (void); 118extern omega_pb omega_alloc_problem (int, int); 119extern enum omega_result omega_solve_problem (omega_pb, enum omega_result); 120extern enum omega_result omega_simplify_problem (omega_pb); 121extern enum omega_result omega_simplify_approximate (omega_pb); 122extern enum omega_result omega_constrain_variable_sign (omega_pb, 123 enum omega_eqn_color, 124 int, int); 125extern void debug (omega_pb_d &ref); 126extern void debug (omega_pb_d *ptr); 127extern void debug_omega_problem (omega_pb); 128extern void omega_print_problem (FILE *, omega_pb); 129extern void omega_print_red_equations (FILE *, omega_pb); 130extern int omega_count_red_equations (omega_pb); 131extern void omega_pretty_print_problem (FILE *, omega_pb); 132extern void omega_unprotect_variable (omega_pb, int var); 133extern void omega_negate_geq (omega_pb, int); 134extern void omega_convert_eq_to_geqs (omega_pb, int eq); 135extern void omega_print_eqn (FILE *, omega_pb, eqn, bool, int); 136extern bool omega_problem_has_red_equations (omega_pb); 137extern enum omega_result omega_eliminate_redundant (omega_pb, bool); 138extern void omega_eliminate_red (omega_pb, bool); 139extern void omega_constrain_variable_value (omega_pb, enum omega_eqn_color, 140 int, int); 141extern bool omega_query_variable (omega_pb, int, int *, int *); 142extern int omega_query_variable_signs (omega_pb, int, int, int, int, 143 int, int, bool *, int *); 144extern bool omega_query_variable_bounds (omega_pb, int, int *, int *); 145extern void (*omega_when_reduced) (omega_pb); 146extern void omega_no_procedure (omega_pb); 147 148/* Return true when variable I in problem PB is a wildcard. */ 149 150static inline bool 151omega_wildcard_p (omega_pb pb, int i) 152{ 153 return (pb->var[i] < 0); 154} 155 156/* Return true when variable I in problem PB is a safe variable. */ 157 158static inline bool 159omega_safe_var_p (omega_pb pb, int i) 160{ 161 /* The constant of an equation is not a variable. */ 162 gcc_assert (0 < i); 163 return (i <= pb->safe_vars); 164} 165 166/* Print to FILE equality E from PB. */ 167 168static inline void 169omega_print_eq (FILE *file, omega_pb pb, eqn e) 170{ 171 omega_print_eqn (file, pb, e, false, 0); 172} 173 174/* Print to FILE inequality E from PB. */ 175 176static inline void 177omega_print_geq (FILE *file, omega_pb pb, eqn e) 178{ 179 omega_print_eqn (file, pb, e, true, 0); 180} 181 182/* Print to FILE inequality E from PB. */ 183 184static inline void 185omega_print_geq_extra (FILE *file, omega_pb pb, eqn e) 186{ 187 omega_print_eqn (file, pb, e, true, 1); 188} 189 190/* E1 = E2, make a copy of E2 into E1. Equations contain S variables. */ 191 192static inline void 193omega_copy_eqn (eqn e1, eqn e2, int s) 194{ 195 e1->key = e2->key; 196 e1->touched = e2->touched; 197 e1->color = e2->color; 198 199 memcpy (e1->coef, e2->coef, (s + 1) * sizeof (int)); 200} 201 202/* Initialize E = 0. Equation E contains S variables. */ 203 204static inline void 205omega_init_eqn_zero (eqn e, int s) 206{ 207 e->key = 0; 208 e->touched = 0; 209 e->color = omega_black; 210 211 memset (e->coef, 0, (s + 1) * sizeof (int)); 212} 213 214/* Allocate N equations with S variables. */ 215 216static inline eqn 217omega_alloc_eqns (int s, int n) 218{ 219 int i; 220 eqn res = (eqn) (xcalloc (n, sizeof (struct eqn_d))); 221 222 for (i = n - 1; i >= 0; i--) 223 { 224 res[i].coef = (int *) (xcalloc (OMEGA_MAX_VARS + 1, sizeof (int))); 225 omega_init_eqn_zero (&res[i], s); 226 } 227 228 return res; 229} 230 231/* Free N equations from array EQ. */ 232 233static inline void 234omega_free_eqns (eqn eq, int n) 235{ 236 int i; 237 238 for (i = n - 1; i >= 0; i--) 239 free (eq[i].coef); 240 241 free (eq); 242} 243 244/* Returns true when E is an inequality with a single variable. */ 245 246static inline bool 247single_var_geq (eqn e, int nv ATTRIBUTE_UNUSED) 248{ 249 return (e->key != 0 250 && -OMEGA_MAX_VARS <= e->key && e->key <= OMEGA_MAX_VARS); 251} 252 253/* Allocate a new equality with all coefficients 0, and tagged with 254 COLOR. Return the index of this equality in problem PB. */ 255 256static inline int 257omega_add_zero_eq (omega_pb pb, enum omega_eqn_color color) 258{ 259 int idx = pb->num_eqs++; 260 261 gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS); 262 omega_init_eqn_zero (&pb->eqs[idx], pb->num_vars); 263 pb->eqs[idx].color = color; 264 return idx; 265} 266 267/* Allocate a new inequality with all coefficients 0, and tagged with 268 COLOR. Return the index of this inequality in problem PB. */ 269 270static inline int 271omega_add_zero_geq (omega_pb pb, enum omega_eqn_color color) 272{ 273 int idx = pb->num_geqs; 274 275 pb->num_geqs++; 276 gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS); 277 omega_init_eqn_zero (&pb->geqs[idx], pb->num_vars); 278 pb->geqs[idx].touched = 1; 279 pb->geqs[idx].color = color; 280 return idx; 281} 282 283/* Initialize variables for problem PB. */ 284 285static inline void 286omega_initialize_variables (omega_pb pb) 287{ 288 int i; 289 290 for (i = pb->num_vars; i >= 0; i--) 291 pb->forwarding_address[i] = pb->var[i] = i; 292 293 pb->variables_initialized = true; 294} 295 296/* Free problem PB. */ 297 298static inline void 299omega_free_problem (omega_pb pb) 300{ 301 free (pb->var); 302 free (pb->forwarding_address); 303 omega_free_eqns (pb->geqs, OMEGA_MAX_GEQS); 304 omega_free_eqns (pb->eqs, OMEGA_MAX_EQS); 305 omega_free_eqns (pb->subs, OMEGA_MAX_VARS + 1); 306 free (pb); 307} 308 309/* Copy omega problems: P1 = P2. */ 310 311static inline void 312omega_copy_problem (omega_pb p1, omega_pb p2) 313{ 314 int e, i; 315 316 p1->num_vars = p2->num_vars; 317 p1->hash_version = p2->hash_version; 318 p1->variables_initialized = p2->variables_initialized; 319 p1->variables_freed = p2->variables_freed; 320 p1->safe_vars = p2->safe_vars; 321 p1->num_eqs = p2->num_eqs; 322 p1->num_subs = p2->num_subs; 323 p1->num_geqs = p2->num_geqs; 324 325 for (e = p2->num_eqs - 1; e >= 0; e--) 326 omega_copy_eqn (&(p1->eqs[e]), &(p2->eqs[e]), p2->num_vars); 327 328 for (e = p2->num_geqs - 1; e >= 0; e--) 329 omega_copy_eqn (&(p1->geqs[e]), &(p2->geqs[e]), p2->num_vars); 330 331 for (e = p2->num_subs - 1; e >= 0; e--) 332 omega_copy_eqn (&(p1->subs[e]), &(p2->subs[e]), p2->num_vars); 333 334 for (i = p2->num_vars; i >= 0; i--) 335 p1->var[i] = p2->var[i]; 336 337 for (i = OMEGA_MAX_VARS; i >= 0; i--) 338 p1->forwarding_address[i] = p2->forwarding_address[i]; 339} 340 341#endif /* GCC_OMEGA_H */ 342