/* This file is part of cqual.
   Copyright (C) 2000-2001 The Regents of the University of California.

cqual 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 Software Foundation; either version 2, or (at your option)
any later version.

cqual is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with cqual; see the file COPYING.  If not, write to
the Free Software Foundation, 59 Temple Place - Suite 330,
Boston, MA 02111-1307, USA. */

#include <stdio.h>
#include <string.h>
#include "color.h"
#include "containers.h"
#include "quals.h"
#include "util.h"

/* #define DEBUG */      /* Enable printing of generated constraints */

#ifndef AST_H
typedef struct po_info *po_info;
#endif
typedef struct Cond_set *cond_set;

struct type_qualifier {
  enum { qk_constant, qk_variable, qk_link } kind;
  bool mark;                       /* For traversing the graph */
  qual_edge parent;                /* Parent in current spanning tree. */
  union {

    /* Constant */
    struct {
      const char *name;		     /* Name of this qualifier */
      const char *color;             /* Color information for PAM mode */
      level_qual_t level;            /* Level information for qtype */
      sign_qual_t sign;              /* Sign information for qtype */
      qual_set lbc, ubc;             /* Upper- and lower-bounds in order */
      po_info po;                    /* Partial order this qual is in */
    } elt;

    /* Variable */
    struct {
      const char *name;
      location *loc;                 /* Where did this qualifier come from */
      qual_edge_set lb, ub;          /* lower/upper bounds (generated) */
      qual_set lbc, ubc;             /* lower/upper bounds (solution) */
      cond_set cond_set;             /* conditional constraints pending
					on this variable */
      int num_equiv;                 /* # of vars unified with this one */
      bool preferred;                /* True we should try to keep the
				        name of this variable as the ecr */
      int num_errors;                /* # of error paths this variable is
					involved in */
    } var;

    /* Variable that's just been unified with another variable.  In
       this case, mark and parent don't make sense. */
    qual link;
  } u;
};

struct po_info {
  qual_set qualifiers;       /* The qualifiers in this partial order */
  bool flow_sensitive;       /* True if these qualifiers are flow-sensitive */
  bool nonprop;              /* True if these qualifiers don't propagate
				through constraints */
};

typedef enum cond_dir { c_leq_v, v_leq_c} cond_dir;

struct Cond_set {
  cond_dir dir;
  qual c, left, right;         /* constraint is
				   c <= v ==> left <= right   if dir = c_leq_v
				   v <= c ==> left <= right   if dir = v_leq_c
				  where v is the variable this constraint
				  is associated with */
  location *loc;
  struct Cond_set *next;
};

/* Some prototypes */

static int cmp_qual_byname(qual left, qual right);
void cond_set_insert(cond_set *conds, cond_dir dir, qual c, qual left,
		     qual right, location *loc);
bool cond_set_trigger(cond_set *conds, cond_dir dir, qual c);

static qual ecr_qual(qual q);
static void update_error_count(qual q);
static void increment_error_counts(qual left, qual right);

/**************************************************************************
 *                                                                        *
 * Global Variables and Initialization                                    *
 *                                                                        *
 **************************************************************************/

/* Used to prevent some catastrophic errors from occurring */
enum { state_start, state_init, state_pos_defined } state = state_start;

int flag_print_quals_graph = 0; /* Set (externally) to true if we should
				   print out the qualifier constraint
				   graph in dot form. */
static region quals_region = NULL;
static int next_qual = 0;
static int max_index = 0;
static FILE *graph_file = NULL;
qual_set all_quals;
po_set all_pos;
po_info current_po;
qual const_qual = NULL;
qual nonconst_qual = NULL;
qual volatile_qual = NULL;
qual restrict_qual = NULL;
int num_hotspots = 0;           /* Set (externally) to number of hotspots
				   to track. 0 = track no hotspots. */
qual *hotspots; /* Array of size num_hotspots */
struct Set_info po_set_info = { ptr_cmp, FALSE };
struct Set_info qual_set_info = { (set_cmp_fn) cmp_qual, FALSE };
struct Set_info qual_set_byname_info = { (set_cmp_fn) cmp_qual_byname, FALSE };
struct Set_info qual_edge_set_info = { NULL, TRUE };

/* Called before any other functions in quals.h are called. */
void init_quals(void)
{
  assert(!quals_region);
  quals_region = newregion();
  next_qual = 0;
  max_index = 0;
  all_quals = empty_qual_set();
  all_pos = empty_po_set();
  current_po = NULL;
  assert(num_hotspots >= 0);
  if (num_hotspots != 0)
    /* rarrayalloc initializes hotspots to 0 */
    {
      int i;

      hotspots = rarrayalloc(quals_region, num_hotspots, qual);
      for (i = 0; i < num_hotspots; i++)
	hotspots[i] = NULL;
    }
  else
    hotspots = NULL;
  /*  constq = add_qual("const");
      nonconstq = add_qual("$nonconst");
      volatileq = add_qual("volatile");
      add_qual_lt(nonconstq, constq); */
  if (flag_print_quals_graph)
    {
      if (graph_file)
	fclose(graph_file);
      graph_file = fopen("quals.dot", "w");
      fprintf(graph_file, "digraph G {\n");
    }
  state = state_init;
}

/* Called when no more partial orders will be defined.  You *must*
   call this function before creating any qualifier variables. */
void end_define_pos(void)
{
  assert(state == state_init);
  state = state_pos_defined;
}

/* Called when no more constraints will be generated. */
void finish_quals(void)
{
  if (flag_print_quals_graph)
    {
      fprintf(graph_file, "}\n");
      fclose(graph_file);
    }
}

/* Disposes of all memory internally allocated by functions in
   quals.c.  All qualifiers and qualifier variables become invalid
   after calling this function. */
void dispose_quals(void)
{
  assert(quals_region);
  deleteregion(quals_region);
  quals_region = 0;
  state = state_start;
}

/**************************************************************************
 *                                                                        *
 * Qualifier Constants                                                    *
 *                                                                        *
 **************************************************************************/

/* Begin and end defining a partial order.  All the qualifiers created
   between calls to begin and end are exclusively related. */
void begin_po_qual(void)
{
  if (current_po)
    fail("begin_po_qual called without previous end_po_qual\n");
  current_po = ralloc(quals_region, struct po_info);
  current_po->qualifiers = empty_qual_set();
  current_po->flow_sensitive = FALSE;
  current_po->nonprop = FALSE;
}

void end_po_qual(void)
{
  if (!current_po)
    fail("end_po_qual called without previous begin_po_qual\n");
  po_set_insert(quals_region, &all_pos, current_po);
  current_po = NULL;
}

/* Mark the current partial order flow-sensitive */
void set_po_flow_sensitive(void)
{
  current_po->flow_sensitive = TRUE;
  current_po->nonprop = TRUE;
}

/* Mark the current partial order as non-propagating */
void set_po_nonprop(void)
{
  current_po->nonprop = TRUE;
}

/* Make a new (constant) qualifier */
qual add_qual(const char *name)
{
  /* qual_set_insert does pointer comparisons, not strcmps, so we need
     to do a special search by name first. */
  qual new_qual;

  assert(state != state_pos_defined);
  if (!current_po)
    fail("add_qual called without previous begin_po_qual\n");
  if ((new_qual = find_qual(name)))
    {
      if (new_qual->u.elt.po != current_po)
	fail("Qualifier %s in two different partial orders\n",
	     new_qual->u.elt.name);
      return new_qual;
    }
  /* We didn't find the qualifier */
  /*  printf("Adding qualifier %s\n", name);*/
  new_qual = ralloc(quals_region, struct type_qualifier);
  new_qual->kind = qk_constant;
  new_qual->mark = FALSE;
  new_qual->u.elt.name = rstrdup(quals_region, name);
  new_qual->u.elt.color = NULL;
  new_qual->u.elt.level = level_value;
  new_qual->u.elt.sign = sign_pos;
  new_qual->u.elt.lbc = empty_qual_set();
  new_qual->u.elt.ubc = empty_qual_set();
  new_qual->u.elt.po = current_po;
  qual_set_insert(quals_region, &all_quals, new_qual);
  qual_set_insert(quals_region, &current_po->qualifiers, new_qual);
  if (!strcmp(name, "const"))
    const_qual = new_qual;
  else if (!strcmp(name, "$nonconst"))
    nonconst_qual = new_qual;
  else if (!strcmp(name, "volatile"))
    volatile_qual = new_qual;
  else if (!strcmp(name, "restrict"))
    restrict_qual = new_qual;
  return new_qual;
}

/* Add assumption left < right */
void add_qual_lt(qual left, qual right)
{
  assert(left->kind == qk_constant);
  assert(right->kind == qk_constant);
  if (!qual_set_member(left->u.elt.ubc, right))
    {
      qual_set_scanner qs;
      qual q;

      /*  printf("Adding assumption ");
	  print_qual_raw(printf, left);
	  printf(" < ");
	  print_qual_raw(printf, right);
	  printf("\n");
	  */

      qual_set_insert(quals_region, &left->u.elt.ubc, right);
      qual_set_insert(quals_region, &right->u.elt.lbc, left);

      /* Add transitively-implied assumptions */
      scan_qual_set(q, qs, right->u.elt.ubc)
	add_qual_lt(left, q);

      scan_qual_set(q, qs, left->u.elt.lbc)
	add_qual_lt(q, right);
    }
}

/* Add color for qualifier */
void add_color_qual(qual q, const char *color)
{
  assert(q->kind == qk_constant);
  q->u.elt.color = rstrdup(quals_region, color);
}

/* Assert that q is a qualifier on level lev */
void add_level_qual(qual q, level_qual_t lev)
{
  assert(q->kind == qk_constant);
  assert(lev == level_value || lev == level_ref);

  q->u.elt.level = lev;
}

/* Assert that q is a qualifier on values */
void add_sign_qual(qual q, sign_qual_t sign)
{
  assert(q->kind == qk_constant);
  assert(sign == sign_pos || sign == sign_neg || sign == sign_eq);
  q->u.elt.sign = sign;
}

/* Look up a qualifier */
qual find_qual(const char *name)
{
  qual_set_scanner qs;
  qual q;

  scan_qual_set(q, qs, all_quals)
    {
      assert(q->kind == qk_constant);
      if (!strcmp(q->u.elt.name, name))
	return q;
    }
  return NULL;
}

/* Change flow-sensitive quals from nonprop to regular quals for this pass */
void reset_flow_sensitive_quals(void)
{
  po_set_scanner ss;
  po_info po;

  scan_po_set(po, ss, all_pos)
    if (po->flow_sensitive)
      po->nonprop = FALSE;
}

/**************************************************************************
 *                                                                        *
 * Qualifier Variables                                                    *
 *                                                                        *
 **************************************************************************/

/* Make a fresh qualifier variable */
qual make_qvar(const char *name, location *loc, bool preferred)
{
  qual fresh;

  assert(state == state_pos_defined);
  fresh = ralloc(quals_region, struct type_qualifier);
  fresh->kind = qk_variable;
  fresh->mark = FALSE;
  fresh->u.var.name = name;
  fresh->u.var.loc = loc;
  fresh->u.var.lb = empty_qual_edge_set();
  fresh->u.var.ub = empty_qual_edge_set();
  fresh->u.var.lbc = empty_qual_set();
  fresh->u.var.ubc = empty_qual_set();
  fresh->u.var.cond_set = NULL;
  fresh->u.var.num_equiv = 1;
  fresh->u.var.preferred = preferred;
  fresh->u.var.num_errors = 0;
  return fresh;
}

/* Make a fresh qvar, with a (somewhat) unique name. */
qual make_fresh_qvar(location *loc)
{
  const char *name;

  name = rstrcat(quals_region, "q",
		 inttostr(quals_region, next_qual++));
  return make_qvar(name, loc, FALSE);
}

/* Return the ECR for this qualifier */
static qual ecr_qual(qual q)
{
  switch (q->kind)
    {
    case qk_constant:
    case qk_variable:
      return q;
    case qk_link:
      {
	qual ecr = q, cur, temp;
	
	/* Find root */
	while (ecr->kind == qk_link)
	  ecr = ecr->u.link;
	
	/* Compress path */
	cur = q;
	while (cur->u.link != ecr)
	  {
	    temp = cur->u.link;
	    cur->u.link = ecr;
	    cur = temp;
	  }
	return ecr;
      }
      break;
    default:
      fail("Unexpected qual kind %x\n", q->kind);
    }
}

/**************************************************************************
 *                                                                        *
 * Qualifier Edges                                                        *
 *                                                                        *
 **************************************************************************/

static inline qual_edge mkqual_edge(region r, qual q, location *loc)
{
  qual_edge result = ralloc(r, struct Qual_edge);
  result->loc = loc;
  result->qual = q;
  return result;
}

/**************************************************************************
 *                                                                        *
 * Predicates and Queries                                                 *
 *                                                                        *
 **************************************************************************/

/* Return the level of qualifier q */
level_qual_t level_qual(qual q)
{
  assert(q->kind == qk_constant);
  return q->u.elt.level;
}

/* Return the sign of qualifier q */
sign_qual_t sign_qual(qual q)
{
  assert(q->kind == qk_constant);
  return q->u.elt.sign;
}

/* Return TRUE iff q is flow-sensitive */
bool flow_sensitive_qual(qual q)
{
  assert(q->kind == qk_constant);
  return q->u.elt.po->flow_sensitive;
}

/* Return TRUE iff q is non-propagating */
bool nonprop_qual(qual q)
{
  assert(q->kind == qk_constant);
  return q->u.elt.po->nonprop;
}

/* Return TRUE iff q is a variable (or a link to a variable) */
bool variable_qual(qual q)
{
  q = ecr_qual(q);
  return q->kind == qk_variable;
}

/* Return TRUE iff q is a constant */
bool constant_qual(qual q)
{
  q = ecr_qual(q);
  return q->kind == qk_constant;
}

/* Return the location a qualifier variable came from */
location *location_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.loc;
}

/* Lower-bound variables of q */
qual_edge_set lb_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.lb;
}

/* Upper-bound variables of q */
qual_edge_set ub_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.ub;
}

/* Lower-bound constants of q */
qual_set lbc_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.lbc;
}

/* Upper-bound constants of q */
qual_set ubc_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.ubc;
}

/* Number of error paths q is involved in */
int error_count_qual(qual q)
{
  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  return q->u.var.num_errors;
}

/**************************************************************************
 *                                                                        *
 * Conditional Constraint Sets                                            *
 *                                                                        *
 **************************************************************************/

/* Add condition to conds.  May add duplicates. */
void cond_set_insert(cond_set *conds, cond_dir dir, qual c, qual left,
		     qual right, location *loc)
{
  cond_set new_elt;

  new_elt = ralloc(quals_region, struct Cond_set);
  new_elt->dir = dir;
  new_elt->c = c;
  new_elt->left = left;
  new_elt->right = right;
  new_elt->loc = loc;
  new_elt->next = *conds;
  *conds = new_elt;
}

/**************************************************************************
 *                                                                        *
 * Constraint Generation                                                  *
 *                                                                        *
 **************************************************************************/

int print_graph_file(const char *fmt, ...)
{
  va_list args;
  va_start(args, fmt);
  return vfprintf(graph_file, fmt, args);
}

/* left <= right.  orig is true iff this constraint was generated
   directly instead of added through transitivity. */
bool _mkleq_qual(qual left, qual right, bool orig, location *loc)
{
  if (flag_print_quals_graph && orig)
    {
      /*
      fprintf(graph_file, "%p %p\n", left, right);
      */
      print_qual_raw(print_graph_file, left);
      fprintf(graph_file, " -> ");
      print_qual_raw(print_graph_file, right);
      fprintf(graph_file, "\n");
    }
#ifdef DEBUG
  print_qual_raw(printf, left);
  printf(" %s <= ", ptr_to_ascii(left));
  print_qual_raw(printf, right);
  printf(" %s\n", ptr_to_ascii(right));
#endif
  left = ecr_qual(left);
  right = ecr_qual(right);
  if (left == right)
    /* Reflexivity */
    return FALSE;
  if (left->kind == qk_constant && right->kind == qk_constant)
    {
      /* Do comparison in lattice. */
      bool result = !leq_qual(left, right);

      if (result)
	{
	  printf("Unsatisfiable ");
	  print_qual_raw(printf, left);
	  printf(" <= ");
	  print_qual_raw(printf, right);
	  printf("\n");
	}
	
      return result;
    }
  else if (left->kind == qk_constant && right->kind == qk_variable)
    {
      bool result = FALSE;
      if (orig) /* Add no matter what */
	{
	  qual_edge_set_insert(quals_region, &right->u.var.lb,
			       mkqual_edge(quals_region, left, loc));
	  if (sign_qual(left) == sign_eq)
	    qual_edge_set_insert(quals_region, &right->u.var.ub,
				 mkqual_edge(quals_region, left, loc));
	}
      if ((!nonprop_qual(left) || orig) &&
	  !qual_set_member(right->u.var.lbc, left))
	{
	  /* Propagate if we haven't already */
	  qual q;
	  qual_set_scanner qs;
	  qual_edge qe;
	  qual_edge_set_scanner qess;

	  qual_set_insert(quals_region, &right->u.var.lbc, left);
	  scan_qual_set(q, qs, right->u.var.ubc)
	    result = _mkleq_qual(left, q, FALSE, loc) || result;
	  scan_qual_edge_set(qe, qess, right->u.var.ub)
	    result = _mkleq_qual(left, qe->qual, FALSE, loc) || result;
	  if (sign_qual(left) == sign_eq || qual_set_empty(left->u.elt.ubc))
	    /* Nonvariant qualifiers propagate in both directions.
	       Also, if left has no upper bounds then left <= right
	       ==> left = right. */
	    _mkleq_qual(right, left, FALSE, loc);
	  result = cond_set_trigger(&right->u.var.cond_set,
				    c_leq_v, left) || result;
	}
      if (orig && result)
	increment_error_counts(left, right);

      return result;
    }
  else if (left->kind == qk_variable && right->kind == qk_constant)
    {
      bool result = FALSE;
      if (orig) /* Add no matter what */
	{
	  qual_edge_set_insert(quals_region, &left->u.var.ub,
			       mkqual_edge(quals_region, right, loc));
	  if (sign_qual(right) == sign_eq)
	    qual_edge_set_insert(quals_region, &left->u.var.lb,
				 mkqual_edge(quals_region, right, loc));
	}
      if ((!nonprop_qual(right) || orig) &&
	  !qual_set_member(left->u.var.ubc, right))
	{
	  /* Propagate if we haven't already */
	  qual q;
	  qual_set_scanner qs;
	  qual_edge qe;
	  qual_edge_set_scanner qess;

	  qual_set_insert(quals_region, &left->u.var.ubc, right);
	  scan_qual_set(q, qs, left->u.var.lbc)
	    result = _mkleq_qual(q, right, FALSE, loc) || result;
	  scan_qual_edge_set(qe, qess, left->u.var.lb)
	    result = _mkleq_qual(qe->qual, right, FALSE, loc) || result;
	  if (sign_qual(right) == sign_eq || qual_set_empty(right->u.elt.lbc))
	    /* Nonvariant qualifiers propagate in both directions.
	       Also, if right has no lower bounds then left <= right
	       ==> left = right. */
	    _mkleq_qual(right, left, FALSE, loc);
	  result = cond_set_trigger(&left->u.var.cond_set,
				    v_leq_c, right) || result;
	}
      if (orig && result)
	increment_error_counts(left, right);

      return result;
    }
  else
    {
      /* Both variables -- Propagate constants in both directions */
      bool result = FALSE;
      qual q1, q2;
      qual_set_scanner qs;

      qual_edge_set_insert(quals_region, &left->u.var.ub,
			   mkqual_edge(quals_region, right, loc));
      qual_edge_set_insert(quals_region, &right->u.var.lb,
			   mkqual_edge(quals_region, left, loc));
      scan_qual_set(q1, qs, left->u.var.lbc)
	result = _mkleq_qual(q1, right, FALSE, loc) || result;
      scan_qual_set(q2, qs, right->u.var.ubc)
	result = _mkleq_qual(left, q2, FALSE, loc) || result;

      if (orig && result)
	increment_error_counts(left, right);

      return result;
    }
}

bool mkleq_qual(qual left, qual right, location *loc)
{
  return _mkleq_qual(left, right, TRUE, loc);
}

/* left == right */
bool mkeq_qual(qual left, qual right, location *loc)
{
  bool result;
  result = mkleq_qual(left, right, loc);
  result = mkleq_qual(right, left, loc) || result;
  return result;
}

/* left == right, plus cannot distinguish left and right anymore */
bool unify_qual(qual left, qual right, location *loc)
{
  left = ecr_qual(left);
  right = ecr_qual(right);
  if (left == right) /* Short circuit to prevent loops in ecr_qual */
    return FALSE;
#ifdef DEBUG
  print_qual_raw(printf, left);
  printf(" %s = ", ptr_to_ascii(left));
  print_qual_raw(printf, right);
  printf(" %s\n", ptr_to_ascii(right));
#endif
  if (left->kind == qk_variable && right->kind == qk_variable)
    {
      qual new_ecr, new_link, q;
      qual_set_scanner qs;
      qual_edge_set_scanner qess;
      qual_edge qe;
      bool result = FALSE;

      if (right->u.var.preferred ||
	  (left->u.var.num_equiv <= right->u.var.num_equiv))
	{
	  new_ecr = right;
	  new_link = left;
	}
      else
	{
	  new_ecr = left;
	  new_link = right;
	}

      scan_qual_edge_set(qe, qess, new_link->u.var.lb)
	result = _mkleq_qual(qe->qual, new_ecr, TRUE, qe->loc) || result;

      scan_qual_edge_set(qe, qess, new_link->u.var.ub)
	result = _mkleq_qual(new_ecr, qe->qual, TRUE, qe->loc) || result;

      scan_qual_set(q, qs, new_link->u.var.lbc)
	result = _mkleq_qual(q, new_ecr, FALSE, NULL) ||result;/*not original*/

      scan_qual_set(q, qs, new_link->u.var.ubc)
	result = _mkleq_qual(new_ecr, q, FALSE, NULL) ||result;/*not original*/

      new_ecr->u.var.num_equiv += new_link->u.var.num_equiv;
      new_ecr->u.var.num_errors += new_link->u.var.num_errors;
      update_error_count(new_ecr);
      new_link->kind = qk_link;
      new_link->u.link = new_ecr;

      return result;
    }
  else
    {
      return mkeq_qual(left, right, loc);
    }
}

/* Returns TRUE iff left <= right.  Requires that at least one of
   left, right is a constant.  By defn, returns TRUE if left and right
   are in distinct partial orders. */
bool leq_qual(qual left, qual right)
{
  left = ecr_qual(left);
  right = ecr_qual(right);

  assert(constant_qual(left) || constant_qual(right));
  if (left == right)
    return TRUE;     /* Reflexivity */

  /* XXX Fix for transitive partial order constraints */
  if (left->kind == qk_constant && right->kind == qk_constant)
    return (qual_set_member(left->u.elt.ubc, right) ||
	    !qual_set_member(left->u.elt.po->qualifiers, right));
  else if (left->kind == qk_variable)
    return (qual_set_member(left->u.var.ubc, right));
  else
    {
      assert (right->kind == qk_variable);
      return qual_set_member(right->u.var.lbc, left);
    }
}

/* Compute q such that left <= q and right <= q */
/*
bool lub_qual(qual left, qual right, qual *lub, location loc)
{
  bool result = FALSE;

  *lub = make_fresh_qvar(dummy_location);
  result = mkleq_qual(left, *lub);
  assert(!result);
  result = mkleq_qual(right, *lub) || result;
  return result;
}
*/

/* Returns TRUE iff left and right are the same.  Does not generate a
   constraint. */
bool eq_qual(qual left, qual right)
{
  return (ecr_qual(left) == ecr_qual(right));
}

/* A total ordering on qualifiers.  Returns 0 if left = right, a value
   <0 if left < right, or a value >0 if left > right */
int cmp_qual(qual left, qual right)
{
  left = ecr_qual(left);
  right = ecr_qual(right);
  return left - right;
}

/* Return TRUE iff q has bound as an originally-specified lower-bound */
bool has_lb_qual(qual q, qual bound)
{
  qual_edge_set_scanner qess;
  qual_edge qe;

  scan_qual_edge_set(qe, qess, lb_qual(q))
    if (eq_qual(bound, qe->qual))
      return TRUE;
  return FALSE;
}

/* Return TRUE iff q has bound as an originally-specified upper-bound */
bool has_ub_qual(qual q, qual bound)
{
  qual_edge_set_scanner qess;
  qual_edge qe;

  scan_qual_edge_set(qe, qess, ub_qual(q))
    if (eq_qual(bound, qe->qual))
      return TRUE;
  return FALSE;
}

/* Return TRUE iff q has bound as an originally-specified bound */
bool has_qual(qual q, qual bound)
{
  return has_lb_qual(q, bound) || has_ub_qual(q, bound);
}

/* Adds the conditional constraint l1<=r1 ==> l2<=r2.  This constraint
   is allowed only if at least one of {l1,r1} is a constant. */
bool cond_mkleq_qual(qual l1, qual r1, qual l2, qual r2, location *loc)
{
  assert(constant_qual(l1) || constant_qual(r1));
#ifdef DEBUG
  print_qual_raw(printf, l1);
  printf(" %s <= ", ptr_to_ascii(l1));
  print_qual_raw(printf, r1);
  printf(" %s  ==>  ", ptr_to_ascii(r1));
  print_qual_raw(printf, l2);
  printf(" %s <= ", ptr_to_ascii(l2));
  print_qual_raw(printf, r2);
  printf(" %s\n", ptr_to_ascii(r2));
#endif

  l1 = ecr_qual(l1);
  r1 = ecr_qual(r1);
  l2 = ecr_qual(l2);
  r2 = ecr_qual(r2);
  if (leq_qual(l1, r1))
    /* Condition is true */
    return mkleq_qual(l2, r2, loc);
  else if (constant_qual(l1) && constant_qual(r1))
    /* Conditional will never be true -- ignore constraint */
    return FALSE;
  else
    {
      /* Condition is not true yet; add constraint to pending set */
      qual v, c;
      cond_dir dir;

      if (constant_qual(l1))
	{ c = l1; v = ecr_qual(r1); dir = c_leq_v; }
      else
	{ c = r1; v = ecr_qual(l1); dir = v_leq_c; }
      assert (constant_qual(c) && variable_qual(v));
      cond_set_insert(&v->u.var.cond_set, dir, c, l2, r2, loc);
      return FALSE;
    }
}

/* If there are any conditions in conds triggered by dir and c, add them
   and remove the conditions from conds. */
bool cond_set_trigger(cond_set *conds, cond_dir dir, qual c)
{
  cond_set cur, prev;
  bool result = FALSE;

  prev = NULL;
  cur = *conds;
  while (cur)
    {
      /* XXX Also check transitivity in partial order */
      if (cur->dir == dir && cur->c == c)
	{
	  /* We found a match.  Remove from list... */
	  if (prev)
	    /* make prev's next skip over cur */
	    prev->next = cur->next;
	  else
	    /* no prev -- make conds (head of list) skip over cur */
	    *conds = cur->next;

	  /* ...and add constraint */
	  result = mkleq_qual(cur->left, cur->right, cur->loc) || result;
	}
      else
	/* Advance prev */
	prev = cur;

      /* Advance cur in any case */
      cur = cur->next;
    }
  return result;
}

/**************************************************************************
 *                                                                        *
 * Print/View Qualifiers                                                  *
 *                                                                        *
 **************************************************************************/

/* Apply f to all possible values of q.  f is applied to NULL in
   the error case. */
void scan_bounds(qual q, void (*f)(qual, void *), void *arg)
{
  qual_set_scanner qs;
  qual p;

  scan_qual_set(p, qs, q->u.var.lbc)
    if ((sign_qual(p) == sign_pos) ||
	(sign_qual(p) == sign_eq))
      f(p, arg);

  scan_qual_set(p, qs, q->u.var.ubc)
    if (sign_qual(p) == sign_neg)    /* eq handled above */
      f(p, arg);
}

/* Compare constant qualifiers by name */
static int cmp_qual_byname(qual left, qual right)
{
  assert(left->kind == qk_constant && right->kind == qk_constant);
  return strcmp(left->u.elt.name, right->u.elt.name);
}

/* Apply f to all possible values of q in sorted order. */
void scan_bounds_sorted(qual q, void (*f)(qual, void *), void *arg)
{
  region scratch_region;
  qual_set_byname bounds;
  qual_set_byname_scanner qsbn;
  qual_set_scanner qs;
  qual p;

  scratch_region = newregion();
  bounds = empty_qual_set_byname();

  scan_qual_set(p, qs, q->u.var.lbc)
    if ((sign_qual(p) == sign_pos) || (sign_qual(p) == sign_eq))
      qual_set_byname_insert(scratch_region, &bounds, p);
  scan_qual_set(p, qs, q->u.var.ubc)
    if (sign_qual(p) == sign_neg)
      qual_set_byname_insert(scratch_region, &bounds, p);

  qual_set_byname_sort(bounds);
  scan_qual_set_byname(p, qsbn, bounds)
    f(p, arg);
  deleteregion(scratch_region);
}

typedef struct print_info {
  printf_func pf;
  bool first;
  int size;
} *print_info;

void print_qual_fn(qual q, void *arg)
{
  print_info pi = (print_info) arg;

  assert(q->kind == qk_constant);
  if (!pi->first)
    pi->size += pi->pf(" ");
  pi->size += pi->pf("%s", q->u.elt.name);
  pi->first = FALSE;
}

/* Print the qualifiers, nicely */
int print_qual(printf_func pf, qual q)
{
  q = ecr_qual(q);
  switch(q->kind)
    {
    case qk_constant:
      {
	return pf("%s", q->u.elt.name);
      }
    case qk_variable:
      {
	struct print_info pi = {0, TRUE, 0};
	pi.pf = pf;

	scan_bounds_sorted(q, print_qual_fn, &pi);
	return pi.size;
      };
      break;
    default:
      fail("Unexpected kind %d for qualifiers\n", q->kind);
    }
}

/* Print the raw qualifiers */
int print_qual_raw(printf_func pf, qual q)
{
  if (!q)
    fail("Null qualifier in print_qual_raw\n");
  switch(q->kind)
    {
    case qk_constant: return pf("%s", q->u.elt.name);
    case qk_variable: return pf("%s", q->u.var.name);
    case qk_link:
      {
	int result = pf("[");
	result += print_qual_raw(pf, q->u.link);
	result += pf("]");
	return result;
      }
    default: fail("Unexpected kind %d for qualifier\n", q->kind);
    }
}

/* Returns color we should use for lub of colors 1 and 2 */
const char *combine_colors_pam(const char *color1, const char *color2)
{
  if (!color1) return color2;
  if (!color2) return color1;
  if (strcmp(color1, color2) == 0)
    return color1;
  return pam_color_multiqual;
}

void color_qual_fn(qual q, void *arg)
{
  const char **color = (const char **) arg;

  *color = combine_colors_pam(*color, color_qual(q));
}

/* Return the color of qualifier q.  q may be a constant or a variable */
const char *color_qual(qual q)
{
  q = ecr_qual(q);
  switch (q->kind)
    {
    case qk_constant:
      return q->u.elt.color;
    case qk_variable:
      {
	const char *color = NULL;

	scan_bounds(q, color_qual_fn, &color);
	return color;
    }
      break;
    default:
      fail("Unexpected kind %d for qualifier\n", q->kind);
    }
}

/* Return the name of qualifier q.  q may be a constant or a variable. */
const char *name_qual(qual q)
{
  q = ecr_qual(q);
  switch (q->kind)
    {
    case qk_constant: return q->u.elt.name;
    case qk_variable: return q->u.var.name;
    default:
      fail("Unexpected kind %d for qualifier\n", q->kind);
    }
}

/**************************************************************************
 *                                                                        *
 * Constraint Graph Traversal                                             *
 *                                                                        *
 **************************************************************************/

typedef enum direction {dir_lower, dir_upper, dir_both} dir;

/* Erase all the marks marked as TRUE reachable via TRUE marked nodes
   from q. */
static void traverse_clear_marks(qual q)
{
  qual_edge qe;
  qual_edge_set_scanner qess;

  q = ecr_qual(q);
  if (!q->mark)
    return;
  q->mark = FALSE;

  if (q->kind == qk_variable)
    {
      scan_qual_edge_set(qe, qess, q->u.var.lb)
	traverse_clear_marks(qe->qual);
      
      scan_qual_edge_set(qe, qess, q->u.var.ub)
	traverse_clear_marks(qe->qual);
    }
  else
    assert(q->kind == qk_constant);
}

/* Traverse the constraint graph starting from qualifier variable q,
   looking for constant qualifier c in direction d.  If such a path
   exists, set the parent pointers and return c.  Otherwise return
   NULL.  If c is NULL, look for any path to a constant qualifier, and
   return that qualifier. */
qual find_shortest_path(region r, qual q, qual c, dir d)
{
  dd_list queue;
  qual path_end;

  q = ecr_qual(q);
  assert(q->kind == qk_variable && (!c || constant_qual(c)));
  queue = dd_new_list(r);
  dd_add_last(r, queue, q);
  q->parent = NULL;                /* Mark as root */
  assert(!c || c->parent == NULL); /* Should be */
  path_end = NULL;

  while (!dd_is_empty(queue))
    {
      qual q;

      q = DD_GET(qual, dd_first(queue));
      dd_remove(dd_first(queue));
      q = ecr_qual(q);
      if (q->mark)
	continue;

      q->mark = TRUE;
      if (q == c || (!c && constant_qual(q)))
	{
	  path_end = q;
	  break;
	}
      else
	{
	  qual_edge_set_scanner qess;
	  qual_edge qe;

	  if (d == dir_lower &&
	      ((!c && !qual_set_empty(q->u.var.lbc)) ||
	       qual_set_member(q->u.var.lbc, c)))
	    {
	      scan_qual_edge_set(qe, qess, q->u.var.lb)
		{
		  qual b;

		  b = ecr_qual(qe->qual);
		  if (!b->mark)
		    {
		      b->parent = mkqual_edge(r, q, qe->loc);
		      dd_add_last(r, queue, b);
		    }
		}
	    }
	  if (d == dir_upper &&
	      ((!c && !qual_set_empty(q->u.var.ubc)) ||
	       qual_set_member(q->u.var.ubc, c)))
	    {
	      scan_qual_edge_set(qe, qess, q->u.var.ub)
		{
		  qual b;

		  b = ecr_qual(qe->qual);
		  if (!b->mark)
		    {
		      b->parent = mkqual_edge(r, q, qe->loc);
		      dd_add_last(r, queue, b);
		    }
		}
	    }
	}
    }

  traverse_clear_marks(q);
  return path_end;
}

/* Traverse parent pointer chain from q */
static void traverse_parent_edges(qual q, qual_traverse_edge_func f, void *arg)
{
  qual b;

  q = ecr_qual(q);
  for (b = q; b->parent != NULL; b = ecr_qual(b->parent->qual))
    f(b, b->parent->qual, b->parent->loc, arg);
}

/* Traverse parent pointer chain from q in reverse */
void traverse_parent_edges_reverse(qual q, qual_traverse_edge_func f,
				   void *arg) {
  if (q->parent != NULL)
    {
      traverse_parent_edges_reverse(q->parent->qual, f, arg);
      f(q->parent->qual, q, q->parent->loc, arg);
    }
}

/* Call f(q1, q2, arg) for every edge q1->q2 on a shortest
   unidirectional path from qualifier variable q to constant qualifier
   c.  If c == NULL, finds shortest path to any constant qualifier.
   If there are paths in both directions, traverses both. */
void traverse_shortest_path_edges(qual q, qual c, qual_traverse_edge_func f,
				  void *arg)
{
  region scratch_region;
  qual left_end, right_end;

  scratch_region = newregion();
  if ((left_end = find_shortest_path(scratch_region, q, c, dir_lower)))
    traverse_parent_edges(left_end, f, arg);

  if ((right_end = find_shortest_path(scratch_region, q, c, dir_upper)))
    traverse_parent_edges_reverse(right_end, f, arg);
  deleteregion(scratch_region);
}

/* Call f(q', arg) for every node q' on all paths from qualifier q to
   constant qualifier c.  Does nothing if there is no such path. */
void __traverse_qual_graph_nodes(qual q, qual c, qual_traverse_node_func f,
			       void *arg)
{
  q = ecr_qual(q);
  assert(constant_qual(c));

  if (q->mark)
    return;
  q->mark = TRUE;

  if (q->kind == qk_variable)
    {
      bool traverse_upper, traverse_lower;
      qual_edge_set_scanner qess;
      qual_edge qe;

      traverse_upper = has_ub_qual(q, c);
      traverse_lower = has_lb_qual(q, c);

      if (traverse_upper || traverse_lower)
	f(q, arg);

      if (traverse_upper)
	scan_qual_edge_set(qe, qess, q->u.var.ub)
	  __traverse_qual_graph_nodes(qe->qual, c, f, arg);

      if (traverse_lower)
	scan_qual_edge_set(qe, qess, q->u.var.lb)
	  __traverse_qual_graph_nodes(qe->qual, c, f, arg);
    }
  else
    {
      assert(q->kind == qk_constant);
      f(q, arg);
    }
}

/* Apply qtf to every *node* in the quals graph reachable in direction
   dir from q. */
static void _traverse_qual_graph_nodes(qual q, enum direction dir,
				       qual_traverse_node_func qtf,
				       void *arg)
{
  q = ecr_qual(q);

  if (q->mark)
    return;
  q->mark = TRUE;
  qtf(q, arg);
  if (q->kind == qk_variable)
    {
      qual_edge_set_scanner qess;
      qual_edge qe;

      bool
	traverse_lower = (dir == dir_lower || dir == dir_both),
	traverse_upper = (dir == dir_upper || dir == dir_both);

      if (traverse_lower)
	scan_qual_edge_set(qe, qess, q->u.var.lb)
	  _traverse_qual_graph_nodes(qe->qual, dir, qtf, arg);
      if (traverse_upper)
	scan_qual_edge_set(qe, qess, q->u.var.ub)
	  _traverse_qual_graph_nodes(qe->qual, dir, qtf, arg);
    }
  else
    assert(q->kind == qk_constant);
}

/* Traverse the edges in the qualifier graph.  po_bounds_only as above.
   arg is passed to f. */
struct traverse_node_data {
  qual_traverse_node_func f;
  void *arg;
  bool po_bounds_only;
};

void traverse_qual_graph_nodes_lower(qual q, void *arg)
{
  struct traverse_node_data *data = (struct traverse_node_data *) arg;
  if (q->kind == qk_constant || !data->po_bounds_only ||
      !(qual_set_empty(q->u.var.lbc)))
    data->f(q, data->arg);
}

void traverse_qual_graph_nodes_upper(qual q, void *arg)
{
  struct traverse_node_data *data = (struct traverse_node_data *) arg;
  if (q->kind == qk_constant || !data->po_bounds_only ||
      !(qual_set_empty(q->u.var.ubc)))
    data->f(q, data->arg);
}

void traverse_qual_graph_nodes_both(qual q, void *arg)
{
  struct traverse_node_data *data = (struct traverse_node_data *) arg;
  if (q->kind == qk_constant ||
      !data->po_bounds_only ||
      !(qual_set_empty(q->u.var.lbc)) ||
      !(qual_set_empty(q->u.var.ubc)))
    data->f(q, data->arg);
}

void traverse_qual_graph_nodes(qual q, bool po_bounds_only,
			       qual_traverse_node_func f, void *arg)
{
  struct traverse_node_data data;
  bool traverse_both = FALSE;
  qual qual_bound;
  qual_set_scanner qs;

  data.f = f;
  data.po_bounds_only = po_bounds_only;
  data.arg = arg;

  q = ecr_qual(q);
  assert(q->kind == qk_variable);

  if (po_bounds_only)
    {
      scan_qual_set(qual_bound, qs, q->u.var.ubc)
	if (sign_qual(qual_bound) == sign_eq)
	  traverse_both = TRUE;
      scan_qual_set(qual_bound, qs, q->u.var.lbc)
	if (sign_qual(qual_bound) == sign_eq)
	  traverse_both = TRUE;
    }
  if (traverse_both)
      {
	_traverse_qual_graph_nodes(q, dir_both, traverse_qual_graph_nodes_both,
				   &data);
	traverse_clear_marks(q);
      }
  else
    {
      _traverse_qual_graph_nodes(q, dir_lower, traverse_qual_graph_nodes_lower,
				 &data);
      traverse_clear_marks(q);
      _traverse_qual_graph_nodes(q, dir_upper, traverse_qual_graph_nodes_upper,
				 &data);
      traverse_clear_marks(q);
    }

}

/* Apply qtf to every *non-transitive edge* in the quals graph
   reachable in direction dir from q. */
static void _traverse_qual_graph_edges(qual q, enum direction dir,
				       qual_traverse_edge_func qtf,
				       void *arg)
{
  qual_edge_set_scanner qess;
  qual_edge qe;

  q = ecr_qual(q);

  if (q->kind == qk_constant)
    return;
  if (q->mark)
    return;
  q->mark = TRUE;
  switch (dir)
    {
    case dir_lower:
      scan_qual_edge_set(qe, qess, q->u.var.lb)
	{
	  qtf(qe->qual, q, qe->loc, arg);
	  _traverse_qual_graph_edges(qe->qual, dir, qtf, arg);
	}
      break;
    case dir_upper:
      scan_qual_edge_set(qe, qess, q->u.var.ub)
	{
	  qtf(q, qe->qual, qe->loc, arg);
	  _traverse_qual_graph_edges(qe->qual, dir, qtf, arg);
	}
      break;
    case dir_both:
      scan_qual_edge_set(qe, qess, q->u.var.lb)
	{
	  qtf(qe->qual, q, qe->loc, arg);
	  _traverse_qual_graph_edges(qe->qual, dir, qtf, arg);
	}
      scan_qual_edge_set(qe, qess, q->u.var.ub)
	{
	  qtf(q, qe->qual, qe->loc, arg);
	  _traverse_qual_graph_edges(qe->qual, dir, qtf, arg);
	}
      break;
    }
}

/* Traverse the edges in the qualifier graph.  po_bounds_only as above.
   arg is passed to f. */
struct traverse_edge_data {
  qual_traverse_edge_func f;
  void *arg;
  bool po_bounds_only;
};

void traverse_qual_graph_edges_lower(qual left, qual right, 
				     location *loc, void *arg)
{
  struct traverse_edge_data *data = (struct traverse_edge_data *) arg;
  if (left->kind == qk_constant || !data->po_bounds_only ||
      !(qual_set_empty(left->u.var.lbc)))
    data->f(left, right, loc, data->arg);
}

void traverse_qual_graph_edges_upper(qual left, qual right,
				     location *loc, void *arg)
{
  struct traverse_edge_data *data = (struct traverse_edge_data *) arg;
  if (right->kind == qk_constant || !data->po_bounds_only ||
      !(qual_set_empty(right->u.var.ubc)))
    data->f(left, right, loc, data->arg);
}

void traverse_qual_graph_edges_both(qual left, qual right,
				    location *loc, void *arg)
{
  struct traverse_edge_data *data = (struct traverse_edge_data *) arg;
  if (left->kind == qk_constant || right->kind == qk_constant ||
      !data->po_bounds_only ||
      !(qual_set_empty(left->u.var.lbc)) ||
      !(qual_set_empty(left->u.var.ubc)) ||
      !(qual_set_empty(right->u.var.lbc)) ||
      !(qual_set_empty(right->u.var.ubc)))
    data->f(left, right, loc, data->arg);
}

void traverse_qual_graph_edges(qual q, bool po_bounds_only,
			       qual_traverse_edge_func f, void *arg)
{
  struct traverse_edge_data data;
  bool traverse_both = FALSE;
  qual qual_bound;
  qual_set_scanner qs;

  data.f = f;
  data.po_bounds_only = po_bounds_only;
  data.arg = arg;

  q = ecr_qual(q);
  assert(q->kind == qk_variable);

  if (po_bounds_only)
    {
      scan_qual_set(qual_bound, qs, q->u.var.ubc)
	if (sign_qual(qual_bound) == sign_eq)
	  traverse_both = TRUE;
      scan_qual_set(qual_bound, qs, q->u.var.lbc)
	if (sign_qual(qual_bound) == sign_eq)
	  traverse_both = TRUE;
    }
  if (traverse_both)
      {
	_traverse_qual_graph_edges(q, dir_both, traverse_qual_graph_edges_both,
				   &data);
	traverse_clear_marks(q);
      }
  else
    {
      _traverse_qual_graph_edges(q, dir_lower, traverse_qual_graph_edges_lower,
				 &data);
      traverse_clear_marks(q);
      _traverse_qual_graph_edges(q, dir_upper, traverse_qual_graph_edges_upper,
				 &data);
      traverse_clear_marks(q);
    }
}

/* Print the graph of qualifiers for q to file.  If po_bounds_only is
   true, then only print the graph showing how partial order elements
   affect q; otherwise print all qualifiers reachable from q. */
void print_qual_graph_edge(qual left, qual right, location *loc, void *arg)
{
  FILE *graph_file = (FILE *) arg;
  fprintf(graph_file, "%s -> %s\n", name_qual(left), name_qual(right));
}

void print_qual_graph(qual q, const char *file, bool po_bounds_only)
{
  FILE *graph_file;

  if (!(graph_file = fopen(file, "w")))
    {
      perror(file);
      return;
    }
  fprintf(graph_file, "digraph G {\n");
  traverse_qual_graph_edges(q, po_bounds_only, print_qual_graph_edge,
			    graph_file);
  fprintf(graph_file, "}\n");
  fclose(graph_file);
}

/**************************************************************************
 *                                                                        *
 * Hotspots                                                               *
 *                                                                        *
 **************************************************************************/

/* Called when q's error count has changed. */
static void update_error_count(qual q)
{
  int i;

  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  if (q->u.var.num_errors == 0)
    return;

  /* See if q is in hotspots list */
  for (i = 0; i < num_hotspots && hotspots[i]; i++)
    if (eq_qual(hotspots[i], q))
      break;

  if (i == num_hotspots)
    {
      /* List is full, but q is not in the list */
      int j;

      /* Find smallest element with greater count than q */
      for (j = num_hotspots - 1; j >= 0; j--)
	if (error_count_qual(hotspots[j]) > error_count_qual(q))
	  break;

      if (j != num_hotspots)
	{
	  /* Move q to position j */
	  int k;

	  for (k = num_hotspots - 1; k > j; k--)
	    hotspots[k] = hotspots[k-1];
	  hotspots[j] = q;
	}
    }
  else if (hotspots[i] != NULL && i != 0)
    {
      /* In the list at position i, and it may need to be moved up
         the list. */
      int j;

      for (j = i; j > 0; j--)
	if (error_count_qual(hotspots[j-1]) < error_count_qual(hotspots[j]))
	  {
	    qual tmp;
	    
	    tmp = hotspots[j-1];
	    hotspots[j-1] = q;
	    hotspots[j] = tmp;
	  }
    }
  else
    /* Empty space on the hotspots list -- just add */
    hotspots[i] = q;
}

/* Increment q's error count and update the hotspots list */
static void increment_error_count(qual q)
{

  if (!hotspots)
    return;

  q = ecr_qual(q);
  assert(q->kind == qk_variable);
  q->u.var.num_errors++;

  update_error_count(q);
}

/* Called during graph traversal of increment_error_counts */
static void increment_error_count_func(qual q, void *arg)
{
  q = ecr_qual(q);
  if (q->kind == qk_variable)
    increment_error_count(q);
}

/* Called when an error occurs for the constraint left <= right */
static void increment_error_counts(qual left, qual right)
{
  left = ecr_qual(left);
  right = ecr_qual(right);

  if (left->kind == qk_constant && right->kind == qk_constant)
    ;
  else if (left->kind == qk_variable)
    traverse_qual_graph_nodes(left, TRUE, increment_error_count_func, NULL);
  else
    {
      assert(right->kind == qk_variable);
      traverse_qual_graph_nodes(right, TRUE, increment_error_count_func, NULL);
    }
}
