/* Source code for an implementation of the Omega test, an integer
|
/* Source code for an implementation of the Omega test, an integer
|
programming algorithm for dependence analysis, by William Pugh,
|
programming algorithm for dependence analysis, by William Pugh,
|
appeared in Supercomputing '91 and CACM Aug 92.
|
appeared in Supercomputing '91 and CACM Aug 92.
|
|
|
This code has no license restrictions, and is considered public
|
This code has no license restrictions, and is considered public
|
domain.
|
domain.
|
|
|
Changes copyright (C) 2005, 2006, 2007, 2009 Free Software Foundation, Inc.
|
Changes copyright (C) 2005, 2006, 2007, 2009 Free Software Foundation, Inc.
|
Contributed by Sebastian Pop <sebastian.pop@inria.fr>
|
Contributed by Sebastian Pop <sebastian.pop@inria.fr>
|
|
|
This file is part of GCC.
|
This file is part of GCC.
|
|
|
GCC is free software; you can redistribute it and/or modify it under
|
GCC is free software; you can redistribute it and/or modify it under
|
the terms of the GNU General Public License as published by the Free
|
the terms of the GNU General Public License as published by the Free
|
Software Foundation; either version 3, or (at your option) any later
|
Software Foundation; either version 3, or (at your option) any later
|
version.
|
version.
|
|
|
GCC is distributed in the hope that it will be useful, but WITHOUT ANY
|
GCC is distributed in the hope that it will be useful, but WITHOUT ANY
|
WARRANTY; without even the implied warranty of MERCHANTABILITY or
|
WARRANTY; without even the implied warranty of MERCHANTABILITY or
|
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
|
for more details.
|
for more details.
|
|
|
You should have received a copy of the GNU General Public License
|
You should have received a copy of the GNU General Public License
|
along with GCC; see the file COPYING3. If not see
|
along with GCC; see the file COPYING3. If not see
|
<http://www.gnu.org/licenses/>. */
|
<http://www.gnu.org/licenses/>. */
|
|
|
#include "config.h"
|
#include "config.h"
|
#include "params.h"
|
#include "params.h"
|
|
|
#ifndef GCC_OMEGA_H
|
#ifndef GCC_OMEGA_H
|
#define GCC_OMEGA_H
|
#define GCC_OMEGA_H
|
|
|
#define OMEGA_MAX_VARS PARAM_VALUE (PARAM_OMEGA_MAX_VARS)
|
#define OMEGA_MAX_VARS PARAM_VALUE (PARAM_OMEGA_MAX_VARS)
|
#define OMEGA_MAX_GEQS PARAM_VALUE (PARAM_OMEGA_MAX_GEQS)
|
#define OMEGA_MAX_GEQS PARAM_VALUE (PARAM_OMEGA_MAX_GEQS)
|
#define OMEGA_MAX_EQS PARAM_VALUE (PARAM_OMEGA_MAX_EQS)
|
#define OMEGA_MAX_EQS PARAM_VALUE (PARAM_OMEGA_MAX_EQS)
|
|
|
#define pos_infinity (0x7ffffff)
|
#define pos_infinity (0x7ffffff)
|
#define neg_infinity (-0x7ffffff)
|
#define neg_infinity (-0x7ffffff)
|
|
|
/* Results of the Omega solver. */
|
/* Results of the Omega solver. */
|
enum omega_result {
|
enum omega_result {
|
omega_false = 0,
|
omega_false = 0,
|
omega_true = 1,
|
omega_true = 1,
|
|
|
/* Value returned when the solver is unable to determine an
|
/* Value returned when the solver is unable to determine an
|
answer. */
|
answer. */
|
omega_unknown = 2,
|
omega_unknown = 2,
|
|
|
/* Value used for asking the solver to simplify the system. */
|
/* Value used for asking the solver to simplify the system. */
|
omega_simplify = 3
|
omega_simplify = 3
|
};
|
};
|
|
|
/* Values used for labeling equations. Private (not used outside the
|
/* Values used for labeling equations. Private (not used outside the
|
solver). */
|
solver). */
|
enum omega_eqn_color {
|
enum omega_eqn_color {
|
omega_black = 0,
|
omega_black = 0,
|
omega_red = 1
|
omega_red = 1
|
};
|
};
|
|
|
/* Structure for equations. */
|
/* Structure for equations. */
|
typedef struct eqn_d
|
typedef struct eqn_d
|
{
|
{
|
int key;
|
int key;
|
int touched;
|
int touched;
|
enum omega_eqn_color color;
|
enum omega_eqn_color color;
|
|
|
/* Array of coefficients for the equation. The layout of the data
|
/* Array of coefficients for the equation. The layout of the data
|
is as follows: coef[0] is the constant, coef[i] for 1 <= i <=
|
is as follows: coef[0] is the constant, coef[i] for 1 <= i <=
|
OMEGA_MAX_VARS, are the coefficients for each dimension. Examples:
|
OMEGA_MAX_VARS, are the coefficients for each dimension. Examples:
|
the equation 0 = 9 + x + 0y + 5z is encoded as [9 1 0 5], the
|
the equation 0 = 9 + x + 0y + 5z is encoded as [9 1 0 5], the
|
inequality 0 <= -8 + x + 2y + 3z is encoded as [-8 1 2 3]. */
|
inequality 0 <= -8 + x + 2y + 3z is encoded as [-8 1 2 3]. */
|
int *coef;
|
int *coef;
|
} *eqn;
|
} *eqn;
|
|
|
typedef struct omega_pb_d
|
typedef struct omega_pb_d
|
{
|
{
|
/* The number of variables in the system of equations. */
|
/* The number of variables in the system of equations. */
|
int num_vars;
|
int num_vars;
|
|
|
/* Safe variables are not eliminated during the Fourier-Motzkin
|
/* Safe variables are not eliminated during the Fourier-Motzkin
|
simplification of the system. Safe variables are all those
|
simplification of the system. Safe variables are all those
|
variables that are placed at the beginning of the array of
|
variables that are placed at the beginning of the array of
|
variables: PB->var[1, ..., SAFE_VARS]. PB->var[0] is not used,
|
variables: PB->var[1, ..., SAFE_VARS]. PB->var[0] is not used,
|
as PB->eqs[x]->coef[0] represents the constant of the equation. */
|
as PB->eqs[x]->coef[0] represents the constant of the equation. */
|
int safe_vars;
|
int safe_vars;
|
|
|
/* Number of elements in eqs[]. */
|
/* Number of elements in eqs[]. */
|
int num_eqs;
|
int num_eqs;
|
/* Number of elements in geqs[]. */
|
/* Number of elements in geqs[]. */
|
int num_geqs;
|
int num_geqs;
|
/* Number of elements in subs[]. */
|
/* Number of elements in subs[]. */
|
int num_subs;
|
int num_subs;
|
|
|
int hash_version;
|
int hash_version;
|
bool variables_initialized;
|
bool variables_initialized;
|
bool variables_freed;
|
bool variables_freed;
|
|
|
/* Index or name of variables. Negative integers are reserved for
|
/* Index or name of variables. Negative integers are reserved for
|
wildcard variables. Maps the index of variables in the original
|
wildcard variables. Maps the index of variables in the original
|
problem to the new index of the variable. The index for a
|
problem to the new index of the variable. The index for a
|
variable in the coef array of an equation can change as some
|
variable in the coef array of an equation can change as some
|
variables are eliminated. */
|
variables are eliminated. */
|
int *var;
|
int *var;
|
|
|
int *forwarding_address;
|
int *forwarding_address;
|
|
|
/* Inequalities in the system of constraints. */
|
/* Inequalities in the system of constraints. */
|
eqn geqs;
|
eqn geqs;
|
|
|
/* Equations in the system of constraints. */
|
/* Equations in the system of constraints. */
|
eqn eqs;
|
eqn eqs;
|
|
|
/* A map of substituted variables. */
|
/* A map of substituted variables. */
|
eqn subs;
|
eqn subs;
|
} *omega_pb;
|
} *omega_pb;
|
|
|
extern void omega_initialize (void);
|
extern void omega_initialize (void);
|
extern omega_pb omega_alloc_problem (int, int);
|
extern omega_pb omega_alloc_problem (int, int);
|
extern enum omega_result omega_solve_problem (omega_pb, enum omega_result);
|
extern enum omega_result omega_solve_problem (omega_pb, enum omega_result);
|
extern enum omega_result omega_simplify_problem (omega_pb);
|
extern enum omega_result omega_simplify_problem (omega_pb);
|
extern enum omega_result omega_simplify_approximate (omega_pb);
|
extern enum omega_result omega_simplify_approximate (omega_pb);
|
extern enum omega_result omega_constrain_variable_sign (omega_pb,
|
extern enum omega_result omega_constrain_variable_sign (omega_pb,
|
enum omega_eqn_color,
|
enum omega_eqn_color,
|
int, int);
|
int, int);
|
extern void debug_omega_problem (omega_pb);
|
extern void debug_omega_problem (omega_pb);
|
extern void omega_print_problem (FILE *, omega_pb);
|
extern void omega_print_problem (FILE *, omega_pb);
|
extern void omega_print_red_equations (FILE *, omega_pb);
|
extern void omega_print_red_equations (FILE *, omega_pb);
|
extern int omega_count_red_equations (omega_pb);
|
extern int omega_count_red_equations (omega_pb);
|
extern void omega_pretty_print_problem (FILE *, omega_pb);
|
extern void omega_pretty_print_problem (FILE *, omega_pb);
|
extern void omega_unprotect_variable (omega_pb, int var);
|
extern void omega_unprotect_variable (omega_pb, int var);
|
extern void omega_negate_geq (omega_pb, int);
|
extern void omega_negate_geq (omega_pb, int);
|
extern void omega_convert_eq_to_geqs (omega_pb, int eq);
|
extern void omega_convert_eq_to_geqs (omega_pb, int eq);
|
extern void omega_print_eqn (FILE *, omega_pb, eqn, bool, int);
|
extern void omega_print_eqn (FILE *, omega_pb, eqn, bool, int);
|
extern bool omega_problem_has_red_equations (omega_pb);
|
extern bool omega_problem_has_red_equations (omega_pb);
|
extern enum omega_result omega_eliminate_redundant (omega_pb, bool);
|
extern enum omega_result omega_eliminate_redundant (omega_pb, bool);
|
extern void omega_eliminate_red (omega_pb, bool);
|
extern void omega_eliminate_red (omega_pb, bool);
|
extern void omega_constrain_variable_value (omega_pb, enum omega_eqn_color,
|
extern void omega_constrain_variable_value (omega_pb, enum omega_eqn_color,
|
int, int);
|
int, int);
|
extern bool omega_query_variable (omega_pb, int, int *, int *);
|
extern bool omega_query_variable (omega_pb, int, int *, int *);
|
extern int omega_query_variable_signs (omega_pb, int, int, int, int,
|
extern int omega_query_variable_signs (omega_pb, int, int, int, int,
|
int, int, bool *, int *);
|
int, int, bool *, int *);
|
extern bool omega_query_variable_bounds (omega_pb, int, int *, int *);
|
extern bool omega_query_variable_bounds (omega_pb, int, int *, int *);
|
extern void (*omega_when_reduced) (omega_pb);
|
extern void (*omega_when_reduced) (omega_pb);
|
extern void omega_no_procedure (omega_pb);
|
extern void omega_no_procedure (omega_pb);
|
|
|
/* Return true when variable I in problem PB is a wildcard. */
|
/* Return true when variable I in problem PB is a wildcard. */
|
|
|
static inline bool
|
static inline bool
|
omega_wildcard_p (omega_pb pb, int i)
|
omega_wildcard_p (omega_pb pb, int i)
|
{
|
{
|
return (pb->var[i] < 0);
|
return (pb->var[i] < 0);
|
}
|
}
|
|
|
/* Return true when variable I in problem PB is a safe variable. */
|
/* Return true when variable I in problem PB is a safe variable. */
|
|
|
static inline bool
|
static inline bool
|
omega_safe_var_p (omega_pb pb, int i)
|
omega_safe_var_p (omega_pb pb, int i)
|
{
|
{
|
/* The constant of an equation is not a variable. */
|
/* The constant of an equation is not a variable. */
|
gcc_assert (0 < i);
|
gcc_assert (0 < i);
|
return (i <= pb->safe_vars);
|
return (i <= pb->safe_vars);
|
}
|
}
|
|
|
/* Print to FILE equality E from PB. */
|
/* Print to FILE equality E from PB. */
|
|
|
static inline void
|
static inline void
|
omega_print_eq (FILE *file, omega_pb pb, eqn e)
|
omega_print_eq (FILE *file, omega_pb pb, eqn e)
|
{
|
{
|
omega_print_eqn (file, pb, e, false, 0);
|
omega_print_eqn (file, pb, e, false, 0);
|
}
|
}
|
|
|
/* Print to FILE inequality E from PB. */
|
/* Print to FILE inequality E from PB. */
|
|
|
static inline void
|
static inline void
|
omega_print_geq (FILE *file, omega_pb pb, eqn e)
|
omega_print_geq (FILE *file, omega_pb pb, eqn e)
|
{
|
{
|
omega_print_eqn (file, pb, e, true, 0);
|
omega_print_eqn (file, pb, e, true, 0);
|
}
|
}
|
|
|
/* Print to FILE inequality E from PB. */
|
/* Print to FILE inequality E from PB. */
|
|
|
static inline void
|
static inline void
|
omega_print_geq_extra (FILE *file, omega_pb pb, eqn e)
|
omega_print_geq_extra (FILE *file, omega_pb pb, eqn e)
|
{
|
{
|
omega_print_eqn (file, pb, e, true, 1);
|
omega_print_eqn (file, pb, e, true, 1);
|
}
|
}
|
|
|
/* E1 = E2, make a copy of E2 into E1. Equations contain S variables. */
|
/* E1 = E2, make a copy of E2 into E1. Equations contain S variables. */
|
|
|
static inline void
|
static inline void
|
omega_copy_eqn (eqn e1, eqn e2, int s)
|
omega_copy_eqn (eqn e1, eqn e2, int s)
|
{
|
{
|
e1->key = e2->key;
|
e1->key = e2->key;
|
e1->touched = e2->touched;
|
e1->touched = e2->touched;
|
e1->color = e2->color;
|
e1->color = e2->color;
|
|
|
memcpy (e1->coef, e2->coef, (s + 1) * sizeof (int));
|
memcpy (e1->coef, e2->coef, (s + 1) * sizeof (int));
|
}
|
}
|
|
|
/* Initialize E = 0. Equation E contains S variables. */
|
/* Initialize E = 0. Equation E contains S variables. */
|
|
|
static inline void
|
static inline void
|
omega_init_eqn_zero (eqn e, int s)
|
omega_init_eqn_zero (eqn e, int s)
|
{
|
{
|
e->key = 0;
|
e->key = 0;
|
e->touched = 0;
|
e->touched = 0;
|
e->color = omega_black;
|
e->color = omega_black;
|
|
|
memset (e->coef, 0, (s + 1) * sizeof (int));
|
memset (e->coef, 0, (s + 1) * sizeof (int));
|
}
|
}
|
|
|
/* Allocate N equations with S variables. */
|
/* Allocate N equations with S variables. */
|
|
|
static inline eqn
|
static inline eqn
|
omega_alloc_eqns (int s, int n)
|
omega_alloc_eqns (int s, int n)
|
{
|
{
|
int i;
|
int i;
|
eqn res = (eqn) (xcalloc (n, sizeof (struct eqn_d)));
|
eqn res = (eqn) (xcalloc (n, sizeof (struct eqn_d)));
|
|
|
for (i = n - 1; i >= 0; i--)
|
for (i = n - 1; i >= 0; i--)
|
{
|
{
|
res[i].coef = (int *) (xcalloc (OMEGA_MAX_VARS + 1, sizeof (int)));
|
res[i].coef = (int *) (xcalloc (OMEGA_MAX_VARS + 1, sizeof (int)));
|
omega_init_eqn_zero (&res[i], s);
|
omega_init_eqn_zero (&res[i], s);
|
}
|
}
|
|
|
return res;
|
return res;
|
}
|
}
|
|
|
/* Free N equations from array EQ. */
|
/* Free N equations from array EQ. */
|
|
|
static inline void
|
static inline void
|
omega_free_eqns (eqn eq, int n)
|
omega_free_eqns (eqn eq, int n)
|
{
|
{
|
int i;
|
int i;
|
|
|
for (i = n - 1; i >= 0; i--)
|
for (i = n - 1; i >= 0; i--)
|
free (eq[i].coef);
|
free (eq[i].coef);
|
|
|
free (eq);
|
free (eq);
|
}
|
}
|
|
|
/* Returns true when E is an inequality with a single variable. */
|
/* Returns true when E is an inequality with a single variable. */
|
|
|
static inline bool
|
static inline bool
|
single_var_geq (eqn e, int nv ATTRIBUTE_UNUSED)
|
single_var_geq (eqn e, int nv ATTRIBUTE_UNUSED)
|
{
|
{
|
return (e->key != 0
|
return (e->key != 0
|
&& -OMEGA_MAX_VARS <= e->key && e->key <= OMEGA_MAX_VARS);
|
&& -OMEGA_MAX_VARS <= e->key && e->key <= OMEGA_MAX_VARS);
|
}
|
}
|
|
|
/* Allocate a new equality with all coefficients 0, and tagged with
|
/* Allocate a new equality with all coefficients 0, and tagged with
|
COLOR. Return the index of this equality in problem PB. */
|
COLOR. Return the index of this equality in problem PB. */
|
|
|
static inline int
|
static inline int
|
omega_add_zero_eq (omega_pb pb, enum omega_eqn_color color)
|
omega_add_zero_eq (omega_pb pb, enum omega_eqn_color color)
|
{
|
{
|
int idx = pb->num_eqs++;
|
int idx = pb->num_eqs++;
|
|
|
gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
|
gcc_assert (pb->num_eqs <= OMEGA_MAX_EQS);
|
omega_init_eqn_zero (&pb->eqs[idx], pb->num_vars);
|
omega_init_eqn_zero (&pb->eqs[idx], pb->num_vars);
|
pb->eqs[idx].color = color;
|
pb->eqs[idx].color = color;
|
return idx;
|
return idx;
|
}
|
}
|
|
|
/* Allocate a new inequality with all coefficients 0, and tagged with
|
/* Allocate a new inequality with all coefficients 0, and tagged with
|
COLOR. Return the index of this inequality in problem PB. */
|
COLOR. Return the index of this inequality in problem PB. */
|
|
|
static inline int
|
static inline int
|
omega_add_zero_geq (omega_pb pb, enum omega_eqn_color color)
|
omega_add_zero_geq (omega_pb pb, enum omega_eqn_color color)
|
{
|
{
|
int idx = pb->num_geqs;
|
int idx = pb->num_geqs;
|
|
|
pb->num_geqs++;
|
pb->num_geqs++;
|
gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
|
gcc_assert (pb->num_geqs <= OMEGA_MAX_GEQS);
|
omega_init_eqn_zero (&pb->geqs[idx], pb->num_vars);
|
omega_init_eqn_zero (&pb->geqs[idx], pb->num_vars);
|
pb->geqs[idx].touched = 1;
|
pb->geqs[idx].touched = 1;
|
pb->geqs[idx].color = color;
|
pb->geqs[idx].color = color;
|
return idx;
|
return idx;
|
}
|
}
|
|
|
/* Initialize variables for problem PB. */
|
/* Initialize variables for problem PB. */
|
|
|
static inline void
|
static inline void
|
omega_initialize_variables (omega_pb pb)
|
omega_initialize_variables (omega_pb pb)
|
{
|
{
|
int i;
|
int i;
|
|
|
for (i = pb->num_vars; i >= 0; i--)
|
for (i = pb->num_vars; i >= 0; i--)
|
pb->forwarding_address[i] = pb->var[i] = i;
|
pb->forwarding_address[i] = pb->var[i] = i;
|
|
|
pb->variables_initialized = true;
|
pb->variables_initialized = true;
|
}
|
}
|
|
|
/* Free problem PB. */
|
/* Free problem PB. */
|
|
|
static inline void
|
static inline void
|
omega_free_problem (omega_pb pb)
|
omega_free_problem (omega_pb pb)
|
{
|
{
|
free (pb->var);
|
free (pb->var);
|
free (pb->forwarding_address);
|
free (pb->forwarding_address);
|
omega_free_eqns (pb->geqs, OMEGA_MAX_GEQS);
|
omega_free_eqns (pb->geqs, OMEGA_MAX_GEQS);
|
omega_free_eqns (pb->eqs, OMEGA_MAX_EQS);
|
omega_free_eqns (pb->eqs, OMEGA_MAX_EQS);
|
omega_free_eqns (pb->subs, OMEGA_MAX_VARS + 1);
|
omega_free_eqns (pb->subs, OMEGA_MAX_VARS + 1);
|
free (pb);
|
free (pb);
|
}
|
}
|
|
|
/* Copy omega problems: P1 = P2. */
|
/* Copy omega problems: P1 = P2. */
|
|
|
static inline void
|
static inline void
|
omega_copy_problem (omega_pb p1, omega_pb p2)
|
omega_copy_problem (omega_pb p1, omega_pb p2)
|
{
|
{
|
int e, i;
|
int e, i;
|
|
|
p1->num_vars = p2->num_vars;
|
p1->num_vars = p2->num_vars;
|
p1->hash_version = p2->hash_version;
|
p1->hash_version = p2->hash_version;
|
p1->variables_initialized = p2->variables_initialized;
|
p1->variables_initialized = p2->variables_initialized;
|
p1->variables_freed = p2->variables_freed;
|
p1->variables_freed = p2->variables_freed;
|
p1->safe_vars = p2->safe_vars;
|
p1->safe_vars = p2->safe_vars;
|
p1->num_eqs = p2->num_eqs;
|
p1->num_eqs = p2->num_eqs;
|
p1->num_subs = p2->num_subs;
|
p1->num_subs = p2->num_subs;
|
p1->num_geqs = p2->num_geqs;
|
p1->num_geqs = p2->num_geqs;
|
|
|
for (e = p2->num_eqs - 1; e >= 0; e--)
|
for (e = p2->num_eqs - 1; e >= 0; e--)
|
omega_copy_eqn (&(p1->eqs[e]), &(p2->eqs[e]), p2->num_vars);
|
omega_copy_eqn (&(p1->eqs[e]), &(p2->eqs[e]), p2->num_vars);
|
|
|
for (e = p2->num_geqs - 1; e >= 0; e--)
|
for (e = p2->num_geqs - 1; e >= 0; e--)
|
omega_copy_eqn (&(p1->geqs[e]), &(p2->geqs[e]), p2->num_vars);
|
omega_copy_eqn (&(p1->geqs[e]), &(p2->geqs[e]), p2->num_vars);
|
|
|
for (e = p2->num_subs - 1; e >= 0; e--)
|
for (e = p2->num_subs - 1; e >= 0; e--)
|
omega_copy_eqn (&(p1->subs[e]), &(p2->subs[e]), p2->num_vars);
|
omega_copy_eqn (&(p1->subs[e]), &(p2->subs[e]), p2->num_vars);
|
|
|
for (i = p2->num_vars; i >= 0; i--)
|
for (i = p2->num_vars; i >= 0; i--)
|
p1->var[i] = p2->var[i];
|
p1->var[i] = p2->var[i];
|
|
|
for (i = OMEGA_MAX_VARS; i >= 0; i--)
|
for (i = OMEGA_MAX_VARS; i >= 0; i--)
|
p1->forwarding_address[i] = p2->forwarding_address[i];
|
p1->forwarding_address[i] = p2->forwarding_address[i];
|
}
|
}
|
|
|
#endif /* GCC_OMEGA_H */
|
#endif /* GCC_OMEGA_H */
|
|
|
