From bc01739130f54292c5a0c7f405f4f143b6a0f387 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Mon, 20 May 2019 17:18:35 -0400
Subject: [PATCH 60/67] FIXME: use constraint_manager class

---
 gcc/analyzer/constraint-manager.cc           | 954 ++++++++++++++-------------
 gcc/analyzer/constraint-manager.h            |  15 +-
 gcc/analyzer/region-model.cc                 | 777 ++--------------------
 gcc/analyzer/region-model.h                  |  13 +
 gcc/testsuite/gcc.dg/analyzer/abort.c        |   2 +
 gcc/testsuite/gcc.dg/analyzer/conditionals.c |   2 +
 gcc/testsuite/gcc.dg/analyzer/equivalence.c  |   2 +
 gcc/testsuite/gcc.dg/analyzer/operations.c   |   2 +
 gcc/testsuite/gcc.dg/analyzer/params-2.c     |   2 +
 gcc/testsuite/gcc.dg/analyzer/params.c       |   2 +
 gcc/testsuite/gcc.dg/analyzer/switch.c       |   2 +
 11 files changed, 596 insertions(+), 1177 deletions(-)

diff --git a/gcc/analyzer/constraint-manager.cc b/gcc/analyzer/constraint-manager.cc
index b6eb143..531d1ff 100644
--- a/gcc/analyzer/constraint-manager.cc
+++ b/gcc/analyzer/constraint-manager.cc
@@ -41,6 +41,7 @@
 #include "path-state.h"
 #include "supergraph.h"
 #include "constraint-manager.h"
+#include "tree-diagnostic.h"
 
 /* A subclass of purge_criteria: purge a specific svalue_id.  */
 
@@ -58,25 +59,6 @@ private:
   svalue_id m_victim;
 };
 
-#if 0
-/* FIXME.  */
-
-std::string
-path_var::to_str () const
-{
-  if (m_tree == NULL_TREE)
-    return "NULL";
-  if (CONSTANT_CLASS_P (m_tree))
-    return expr_to_string (m_tree);
-  else
-    return (std::string ("(")
-	    + expr_to_string (m_tree)
-	    + " @ "
-	    + std::to_string (m_stack_depth)
-	    + ")");
-}
-#endif
-
 /* FIXME.  */
 
 equiv_class::equiv_class ()
@@ -116,9 +98,7 @@ equiv_class::to_str () const
     {
       if (i > 0)
 	result += " == ";
-#if 0
       result += sid->to_str ();
-#endif
     }
   if (m_constant)
     {
@@ -170,7 +150,6 @@ equiv_class::operator== (const equiv_class &other)
   return true;
 }
 
-#if 1
 /* FIXME.  */
 
 void
@@ -181,16 +160,13 @@ equiv_class::add (svalue_id sid, const constraint_manager &cm)
       gcc_assert (m_constant == NULL_TREE);
       m_constant = cst;
     }
-  else
-    {
-      m_vars.safe_push (sid);
+  m_vars.safe_push (sid);
 
 #if 0
       if (DECL_P (v.m_tree)
 	  && is_global_var (v.m_tree))
 	m_escaped = true;
 #endif
-    }
 }
 
 /* Remove SID from this equivalence class.
@@ -219,24 +195,22 @@ equiv_class::del (svalue_id sid)
   return false;
 }
 
-#endif
-
 /* Get a representative member of this class, for handling cases
    where the IDs can change mid-traversal.  */
 
-#if 0
-path_var
+svalue_id
 equiv_class::get_representative () const
 {
+#if 0
   if (m_constant)
     return path_var (m_constant, 0);
   else
+#endif
     {
       gcc_assert (m_vars.length () > 0);
       return m_vars[0];
     }
 }
-#endif
 
 /* FIXME.  */
 
@@ -434,30 +408,85 @@ constraint_manager::operator== (const constraint_manager &other) const
 
 /* FIXME.  */
 
-std::string
-constraint_manager::to_str () const
+void
+constraint_manager::print (pretty_printer *pp) const
 {
-  std::string result ("{");
+  pp_string (pp, "{");
   int i;
   equiv_class *ec;
   FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
     {
       if (i > 0)
-	result += ", ";
-      result += equiv_class_id (i).to_str () + ": ";
-      result += ec->to_str ();
+	pp_string (pp, ", ");
+      pp_printf (pp, "%s: ", equiv_class_id (i).to_str ().c_str ());
+      pp_string (pp, ec->to_str ().c_str ());
     }
-  result += "  |  ";
+  pp_string (pp, "  |  ");
   constraint *c;
   FOR_EACH_VEC_ELT (m_constraints, i, c)
     {
       if (i > 0)
-	result += " && ";
-      result += c->to_str (*this);
+	pp_string (pp, " && ");
+      pp_string (pp, c->to_str (*this).c_str ());
     }
-  result += "}@";
-  result += std::to_string (m_stack_depth);
-  return result;
+  pp_printf (pp, "}@%i", m_stack_depth);
+}
+
+/* FIXME.  */
+
+std::string
+constraint_manager::to_str () const
+{
+  pretty_printer pp;
+  print (&pp);
+  return pp_formatted_text (&pp);
+}
+
+/* FIXME.  */
+
+void
+constraint_manager::dump_to_pp (pretty_printer *pp) const
+{
+  // TODO
+  pp_string (pp, "  equiv classes:");
+  pp_newline (pp);
+  int i;
+  equiv_class *ec;
+  FOR_EACH_VEC_ELT (m_equiv_classes, i, ec)
+    {
+      pp_printf (pp, "    %s: ", equiv_class_id (i).to_str ().c_str ());
+      pp_string (pp, ec->to_str ().c_str ());
+      pp_newline (pp);
+    }
+  pp_string (pp, "  constraints:");
+  pp_newline (pp);
+  constraint *c;
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    {
+      pp_printf (pp, "    %i: %s", i, c->to_str (*this).c_str ());
+      pp_newline (pp);
+    }
+}
+
+/* FIXME.  */
+
+void
+constraint_manager::dump (FILE *fp) const
+{
+  pretty_printer pp;
+  pp_format_decoder (&pp) = default_tree_printer;
+  pp_show_color (&pp) = pp_show_color (global_dc->printer);
+  pp.buffer->stream = fp;
+  dump_to_pp (&pp);
+  pp_flush (&pp);
+}
+
+/* FIXME.  */
+
+DEBUG_FUNCTION void
+constraint_manager::dump () const
+{
+  dump (stderr);
 }
 
 /* FIXME.  */
@@ -652,7 +681,9 @@ constraint_manager::apply_constraints_for_gswitch (const superedge &edge,
 /* FIXME.  */
 
 bool
-constraint_manager::add_constraint (svalue_id lhs, enum tree_code op, svalue_id rhs)
+constraint_manager::add_constraint (svalue_id lhs,
+				    enum tree_code op,
+				    svalue_id rhs)
 {
   equiv_class_id lhs_ec_id = get_or_add_equiv_class (lhs);
   equiv_class_id rhs_ec_id = get_or_add_equiv_class (rhs);
@@ -663,8 +694,8 @@ constraint_manager::add_constraint (svalue_id lhs, enum tree_code op, svalue_id
 
 bool
 constraint_manager::add_constraint (equiv_class_id lhs_ec_id,
-			    enum tree_code op,
-			    equiv_class_id rhs_ec_id)
+				    enum tree_code op,
+				    equiv_class_id rhs_ec_id)
 {
   tristate t = eval_condition (lhs_ec_id, op, rhs_ec_id);
 
@@ -695,7 +726,7 @@ constraint_manager::add_constraint (equiv_class_id lhs_ec_id,
 
 	if (rhs_ec_obj.m_constant)
 	  {
-	    gcc_assert (lhs_ec_obj.m_constant == NULL);
+	    //gcc_assert (lhs_ec_obj.m_constant == NULL);
 	    lhs_ec_obj.m_constant = rhs_ec_obj.m_constant;
 	  }
 
@@ -821,8 +852,8 @@ range::constrained_to_single_element (tree *out)
 
 void
 constraint_manager::add_constraint_internal (equiv_class_id lhs_id,
-				     enum constraint_op c_op,
-				     equiv_class_id rhs_id)
+					     enum constraint_op c_op,
+					     equiv_class_id rhs_id)
 {
   /* Add the constraint.  */
   m_constraints.safe_push (constraint (lhs_id, c_op, rhs_id));
@@ -832,10 +863,8 @@ constraint_manager::add_constraint_internal (equiv_class_id lhs_id,
       /* The following can potentially add EQ_EXPR facts, which could lead
 	 to ECs being merged, which would change the meaning of the EC IDs.
 	 Hence we need to do this via path vars.  */
-#if 0
       svalue_id lhs = lhs_id.get_obj (*this).get_representative ();
       svalue_id rhs = rhs_id.get_obj (*this).get_representative ();
-#endif
 
       /* We have LHS </<= RHS */
 
@@ -865,10 +894,8 @@ constraint_manager::add_constraint_internal (equiv_class_id lhs_id,
 	  if (other->is_ordering_p ())
 	    {
 	      /* Refresh the EC IDs, in case any mergers have happened.  */
-#if 0
 	      lhs_id = get_or_add_equiv_class (lhs);
 	      rhs_id = get_or_add_equiv_class (rhs);
-#endif
 
 	      tree lhs_const = lhs_id.get_obj (*this).m_constant;
 	      tree rhs_const = rhs_id.get_obj (*this).m_constant;
@@ -899,12 +926,11 @@ constraint_manager::add_constraint_internal (equiv_class_id lhs_id,
 		     "LHS </<= (RHS, other.lhs) </<= other.rhs"
 		     and thus this implies "LHS </<= other.rhs".  */
 
-		  // TODO:
-#if 0
 		  /* Do we have a tightly-constrained range?  */
 		  if (lhs_const
 		      && !rhs_const
-		      && INTEGRAL_TYPE_P (TREE_TYPE (rhs.m_tree))
+		      // FIXME:
+		      //&& INTEGRAL_TYPE_P (TREE_TYPE (rhs.m_tree))
 		      && other_rhs_const)
 		    {
 		      range r (bound (lhs_const, c_op == CONSTRAINT_LE),
@@ -913,13 +939,14 @@ constraint_manager::add_constraint_internal (equiv_class_id lhs_id,
 		      tree constant;
 		      if (r.constrained_to_single_element (&constant))
 			{
+			  svalue_id cst_sid = get_sid_for_constant (constant);
 			  add_constraint
 			    (rhs_id, EQ_EXPR,
-			     get_or_add_equiv_class (path_var (constant, 0)));
+			     get_or_add_equiv_class (cst_sid));
 			  return;
 			}
 		    }
-#endif
+
 		  /* Otherwise, add the constraint implied by transitivity.  */
 		  enum tree_code new_op
 		    = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
@@ -934,10 +961,10 @@ constraint_manager::add_constraint_internal (equiv_class_id lhs_id,
 
 		  /* Do we have a tightly-constrained range?  */
 		  // TODO:
-#if 0
 		  if (other_lhs_const
 		      && !lhs_const
-		      && INTEGRAL_TYPE_P (TREE_TYPE (lhs.m_tree))
+		      // FIXME:
+		      //&& INTEGRAL_TYPE_P (TREE_TYPE (lhs.m_tree))
 		      && rhs_const)
 		    {
 		      range r (bound (other_lhs_const,
@@ -947,13 +974,14 @@ constraint_manager::add_constraint_internal (equiv_class_id lhs_id,
 		      tree constant;
 		      if (r.constrained_to_single_element (&constant))
 			{
+			  svalue_id cst_sid = get_sid_for_constant (constant);
 			  add_constraint
 			    (lhs_id, EQ_EXPR,
-			     get_or_add_equiv_class (path_var (constant, 0)));
+			     get_or_add_equiv_class (cst_sid));
 			  return;
 			}
 		    }
-#endif
+
 		  /* Otherwise, add the constraint implied by transitivity.  */
 		  enum tree_code new_op
 		    = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
@@ -1135,6 +1163,18 @@ constraint_manager::eval_condition (equiv_class_id lhs_ec,
   return tristate (tristate::TS_UNKNOWN);
 }
 
+/* FIXME.  */
+
+tristate
+constraint_manager::eval_condition (svalue_id lhs,
+				    enum tree_code op,
+				    svalue_id rhs)
+{
+  return eval_condition (get_or_add_equiv_class (lhs),
+			 op,
+			 get_or_add_equiv_class (rhs));
+}
+
 /* Mark EC_ID as having escaped; walk other ECs that haven't yet been marked
    as escaped, and determine if they've now escaped, if so, mark them,
    recursively.
@@ -1372,318 +1412,320 @@ debug (const constraint_manager &cm)
 
 namespace selftest {
 
-/* Attempt to add the constraint (LHS OP RHS) to CM.
-   Verify that CM remains satisfiable.  */
+/* Various constraint_manager selftests.
+   These have to be written in terms of a region_model, since
+   the latter is responsible for managing svalue and svalue_id
+   instances.  */
 
-#define ADD_SAT_CONSTRAINT(CM, LHS, OP, RHS)				\
-  SELFTEST_BEGIN_STMT							\
-    bool sat = (CM).add_constraint (LHS, OP, RHS);			\
-    ASSERT_TRUE (sat);							\
+/* Attempt to add the constraint (LHS OP RHS) to MODEL.
+   Verify that MODEL remains satisfiable.  */
+
+#define ADD_SAT_CONSTRAINT(MODEL, LHS, OP, RHS)	\
+  SELFTEST_BEGIN_STMT					\
+    bool sat = (MODEL).add_constraint (LHS, OP, RHS);	\
+    ASSERT_TRUE (sat);					\
   SELFTEST_END_STMT
 
-/* Attempt to add the constraint (LHS OP RHS) to CM.
+/* Attempt to add the constraint (LHS OP RHS) to MODEL.
    Verify that the result is not satisfiable.  */
 
-#define ADD_UNSAT_CONSTRAINT(CM, LHS, OP, RHS)				\
-  SELFTEST_BEGIN_STMT							\
-    bool sat = (CM).add_constraint (LHS, OP, RHS);			\
-    ASSERT_FALSE (sat);							\
+#define ADD_UNSAT_CONSTRAINT(MODEL, LHS, OP, RHS)	\
+  SELFTEST_BEGIN_STMT					\
+    bool sat = (MODEL).add_constraint (LHS, OP, RHS);	\
+    ASSERT_FALSE (sat);				\
   SELFTEST_END_STMT
 
 static void
 assert_condition (const location &loc,
-		  constraint_manager &cm,
-		  svalue_id lhs, tree_code op, svalue_id rhs,
+		  region_model &model,
+		  tree lhs, tree_code op, tree rhs,
 		  tristate expected)
 {
-  equiv_class_id lhs_ec = cm.get_or_add_equiv_class (lhs);
-  equiv_class_id rhs_ec = cm.get_or_add_equiv_class (rhs);
-  tristate actual = cm.eval_condition (lhs_ec, op, rhs_ec);
+  tristate actual = model.eval_condition (lhs, op, rhs);
   ASSERT_EQ_AT (loc, actual, expected);
 }
 
-#define ASSERT_CONDITION_TRUE(CONSTRAINT_MANAGER, LHS, OP, RHS) \
+#define ASSERT_CONDITION_TRUE(PATH_STATE, LHS, OP, RHS) \
   SELFTEST_BEGIN_STMT							\
-  assert_condition (SELFTEST_LOCATION, CONSTRAINT_MANAGER, LHS, OP, RHS,	\
+  assert_condition (SELFTEST_LOCATION, PATH_STATE, LHS, OP, RHS,	\
 		    tristate (tristate::TS_TRUE));		\
   SELFTEST_END_STMT
 
-#define ASSERT_CONDITION_FALSE(CONSTRAINT_MANAGER, LHS, OP, RHS) \
+#define ASSERT_CONDITION_FALSE(PATH_STATE, LHS, OP, RHS) \
   SELFTEST_BEGIN_STMT							\
-  assert_condition (SELFTEST_LOCATION, CONSTRAINT_MANAGER, LHS, OP, RHS,	\
+  assert_condition (SELFTEST_LOCATION, PATH_STATE, LHS, OP, RHS,	\
 		    tristate (tristate::TS_FALSE));		\
   SELFTEST_END_STMT
 
-#define ASSERT_CONDITION_UNKNOWN(CONSTRAINT_MANAGER, LHS, OP, RHS) \
+#define ASSERT_CONDITION_UNKNOWN(PATH_STATE, LHS, OP, RHS) \
   SELFTEST_BEGIN_STMT							\
-  assert_condition (SELFTEST_LOCATION, CONSTRAINT_MANAGER, LHS, OP, RHS,	\
+  assert_condition (SELFTEST_LOCATION, PATH_STATE, LHS, OP, RHS,	\
 		    tristate (tristate::TS_UNKNOWN));		\
   SELFTEST_END_STMT
 
 /* FIXME.  */
 
-#if 0
 static void
 test_constraint_conditions ()
 {
-  svalue_id int_42 (build_int_cst (integer_type_node, 42), 0);
-  svalue_id int_0 (build_int_cst (integer_type_node, 0), 0);
-
-  svalue_id x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("x"),
-			  integer_type_node), 0);
-  svalue_id y (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("y"),
-			  integer_type_node), 0);
-  svalue_id z (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("z"),
-			  integer_type_node), 0);
+  tree int_42 = build_int_cst (integer_type_node, 42);
+  tree int_0 = build_int_cst (integer_type_node, 0);
+
+  tree x = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		      get_identifier ("x"),
+		      integer_type_node);
+  tree y = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("y"),
+		       integer_type_node);
+  tree z = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("z"),
+		       integer_type_node);
 
   /* Self-comparisons.  */
   {
-    constraint_manager cm;
-    ASSERT_CONDITION_TRUE (cm, x, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, x, LE_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, x, GE_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, x, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, x, LT_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, x, GT_EXPR, x);
+    region_model model;
+    ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, x, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, x);
   }
 
   /* x == y.  */
   {
-    constraint_manager cm;
-    ASSERT_CONDITION_UNKNOWN (cm, x, EQ_EXPR, y);
+    region_model model;
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
 
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
 
-    ASSERT_CONDITION_TRUE (cm, x, EQ_EXPR, y);
-    ASSERT_CONDITION_TRUE (cm, x, LE_EXPR, y);
-    ASSERT_CONDITION_TRUE (cm, x, GE_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, LT_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, GT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_TRUE (cm, y, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, y, LE_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, y, GE_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, y, LT_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, y, GT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
 
     /* Comparison with other var.  */
-    ASSERT_CONDITION_UNKNOWN (cm, x, EQ_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, LE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, NE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, LT_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GT_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z);
   }
 
   /* x == y, then y == z  */
   {
-    constraint_manager cm;
-    ASSERT_CONDITION_UNKNOWN (cm, x, EQ_EXPR, y);
-
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, y);
-    ADD_SAT_CONSTRAINT (cm, y, EQ_EXPR, z);
-
-    ASSERT_CONDITION_TRUE (cm, x, EQ_EXPR, z);
-    ASSERT_CONDITION_TRUE (cm, x, LE_EXPR, z);
-    ASSERT_CONDITION_TRUE (cm, x, GE_EXPR, z);
-    ASSERT_CONDITION_FALSE (cm, x, NE_EXPR, z);
-    ASSERT_CONDITION_FALSE (cm, x, LT_EXPR, z);
-    ASSERT_CONDITION_FALSE (cm, x, GT_EXPR, z);
+    region_model model;
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
+
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, z);
+
+    ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
+    ASSERT_CONDITION_FALSE (model, x, NE_EXPR, z);
+    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, z);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, z);
   }
 
   /* x != y.  */
   {
-    constraint_manager cm;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (cm, x, NE_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
 
-    ASSERT_CONDITION_TRUE (cm, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, EQ_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, LE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, LT_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_TRUE (cm, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, y, EQ_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, LE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, GE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, LT_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, GT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x);
 
     /* Comparison with other var.  */
-    ASSERT_CONDITION_UNKNOWN (cm, x, EQ_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, LE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, NE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, LT_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GT_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z);
   }
 
   /* x < y.  */
   {
-    constraint_manager cm;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (cm, x, LT_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, LT_EXPR, y);
 
-    ASSERT_CONDITION_TRUE (cm, x, LT_EXPR, y);
-    ASSERT_CONDITION_TRUE (cm, x, LE_EXPR, y);
-    ASSERT_CONDITION_TRUE (cm, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, GT_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, GE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (cm, y, LT_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, y, LE_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, y, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, y, GT_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, y, GE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
   }
 
   /* x <= y.  */
   {
-    constraint_manager cm;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (cm, x, LE_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
 
-    ASSERT_CONDITION_UNKNOWN (cm, x, LT_EXPR, y);
-    ASSERT_CONDITION_TRUE (cm, x, LE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, NE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, GT_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (cm, y, LT_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, LE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, NE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, EQ_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, GT_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, y, GE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
   }
 
   /* x > y.  */
   {
-    constraint_manager cm;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (cm, x, GT_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, GT_EXPR, y);
 
-    ASSERT_CONDITION_TRUE (cm, x, GT_EXPR, y);
-    ASSERT_CONDITION_TRUE (cm, x, GE_EXPR, y);
-    ASSERT_CONDITION_TRUE (cm, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, LT_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, LE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, LE_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (cm, y, GT_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, y, GE_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (cm, y, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, y, LT_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, y, LE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
   }
 
   /* x >= y.  */
   {
-    constraint_manager cm;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (cm, x, GE_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, GE_EXPR, y);
 
-    ASSERT_CONDITION_UNKNOWN (cm, x, GT_EXPR, y);
-    ASSERT_CONDITION_TRUE (cm, x, GE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, NE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, LT_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, LE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y);
 
     /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (cm, y, GT_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, GE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, NE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, EQ_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (cm, y, LT_EXPR, x);
-    ASSERT_CONDITION_TRUE (cm, y, LE_EXPR, x);
+    ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
   }
 
   // TODO: implied orderings
 
   /* Constants.  */
   {
-    constraint_manager cm;
-    ASSERT_CONDITION_FALSE (cm, int_0, EQ_EXPR, int_42);
-    ASSERT_CONDITION_TRUE (cm, int_0, NE_EXPR, int_42);
-    ASSERT_CONDITION_TRUE (cm, int_0, LT_EXPR, int_42);
-    ASSERT_CONDITION_TRUE (cm, int_0, LE_EXPR, int_42);
-    ASSERT_CONDITION_FALSE (cm, int_0, GT_EXPR, int_42);
-    ASSERT_CONDITION_FALSE (cm, int_0, GE_EXPR, int_42);
+    region_model model;
+    ASSERT_CONDITION_FALSE (model, int_0, EQ_EXPR, int_42);
+    ASSERT_CONDITION_TRUE (model, int_0, NE_EXPR, int_42);
+    ASSERT_CONDITION_TRUE (model, int_0, LT_EXPR, int_42);
+    ASSERT_CONDITION_TRUE (model, int_0, LE_EXPR, int_42);
+    ASSERT_CONDITION_FALSE (model, int_0, GT_EXPR, int_42);
+    ASSERT_CONDITION_FALSE (model, int_0, GE_EXPR, int_42);
   }
 
   /* x == 0, y == 42.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, int_0);
-    ADD_SAT_CONSTRAINT (cm, y, EQ_EXPR, int_42);
-
-    ASSERT_CONDITION_TRUE (cm, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, EQ_EXPR, y);
-    ASSERT_CONDITION_TRUE (cm, x, LE_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, GE_EXPR, y);
-    ASSERT_CONDITION_TRUE (cm, x, LT_EXPR, y);
-    ASSERT_CONDITION_FALSE (cm, x, GT_EXPR, y);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, int_42);
+
+    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
   }
 
   /* Unsatisfiable combinations.  */
 
   /* x == y && x != y.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, y);
-    ADD_UNSAT_CONSTRAINT (cm, x, NE_EXPR, y);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
+    ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, y);
   }
 
   /* x == 0 then x == 42.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, int_0);
-    ADD_UNSAT_CONSTRAINT (cm, x, EQ_EXPR, int_42);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, int_42);
   }
 
   /* x == 0 then x != 0.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, int_0);
-    ADD_UNSAT_CONSTRAINT (cm, x, NE_EXPR, int_0);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, int_0);
   }
 
   /* x == 0 then x > 0.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, int_0);
-    ADD_UNSAT_CONSTRAINT (cm, x, GT_EXPR, int_0);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, int_0);
   }
 
   /* x != y && x == y.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, x, NE_EXPR, y);
-    ADD_UNSAT_CONSTRAINT (cm, x, EQ_EXPR, y);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
+    ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, y);
   }
 
   /* x <= y && x > y.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, x, LE_EXPR, y);
-    ADD_UNSAT_CONSTRAINT (cm, x, GT_EXPR, y);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
+    ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, y);
   }
 
   // etc
@@ -1694,100 +1736,100 @@ test_constraint_conditions ()
 static void
 test_transitivity ()
 {
-  svalue_id int_42 (build_int_cst (integer_type_node, 42), 0);
-  svalue_id int_0 (build_int_cst (integer_type_node, 0), 0);
-
-  svalue_id a (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("a"),
-			  integer_type_node), 0);
-  svalue_id b (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("b"),
-			  integer_type_node), 0);
-  svalue_id c (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("c"),
-			  integer_type_node), 0);
-  svalue_id d (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("d"),
-			  integer_type_node), 0);
+  tree int_42 = build_int_cst (integer_type_node, 42);
+  tree int_0 = build_int_cst (integer_type_node, 0);
+
+  tree a = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("a"),
+		       integer_type_node);
+  tree b = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("b"),
+		       integer_type_node);
+  tree c = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("c"),
+		       integer_type_node);
+  tree d = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("d"),
+		       integer_type_node);
 
   /* a == b, then c == d, then c == b.  */
   {
-    constraint_manager cm;
-    ASSERT_CONDITION_UNKNOWN (cm, a, EQ_EXPR, b);
-    ASSERT_CONDITION_UNKNOWN (cm, b, EQ_EXPR, c);
-    ASSERT_CONDITION_UNKNOWN (cm, c, EQ_EXPR, d);
-    ASSERT_CONDITION_UNKNOWN (cm, a, EQ_EXPR, d);
-
-    ADD_SAT_CONSTRAINT (cm, a, EQ_EXPR, b);
-    ASSERT_CONDITION_TRUE (cm, a, EQ_EXPR, b);
-
-    ADD_SAT_CONSTRAINT (cm, c, EQ_EXPR, d);
-    ASSERT_CONDITION_TRUE (cm, c, EQ_EXPR, d);
-    ASSERT_CONDITION_UNKNOWN (cm, a, EQ_EXPR, d);
-
-    ADD_SAT_CONSTRAINT (cm, c, EQ_EXPR, b);
-    ASSERT_CONDITION_TRUE (cm, c, EQ_EXPR, b);
-    ASSERT_CONDITION_TRUE (cm, a, EQ_EXPR, d);
+    region_model model;
+    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, b);
+    ASSERT_CONDITION_UNKNOWN (model, b, EQ_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN (model, c, EQ_EXPR, d);
+    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d);
+
+    ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b);
+
+    ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, d);
+    ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, d);
+    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d);
+
+    ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, d);
   }
 
   /* Transitivity: "a < b", "b < c" should imply "a < c".  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, LT_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, b, LT_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (cm, a, LT_EXPR, c);
-    ASSERT_CONDITION_FALSE (cm, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
+    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a <= b", "b < c" should imply "a < c".  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, LE_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, b, LT_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (cm, a, LT_EXPR, c);
-    ASSERT_CONDITION_FALSE (cm, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
+    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a <= b", "b <= c" should imply "a <= c".  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, LE_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, b, LE_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, LE_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (cm, a, LE_EXPR, c);
-    ASSERT_CONDITION_UNKNOWN (cm, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, LE_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a > b", "b > c" should imply "a > c".  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, GT_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, b, GT_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (cm, a, GT_EXPR, c);
-    ASSERT_CONDITION_FALSE (cm, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c);
+    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a >= b", "b > c" should imply " a > c".  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, b, GT_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (cm, a, GT_EXPR, c);
-    ASSERT_CONDITION_FALSE (cm, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c);
+    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a >= b", "b >= c" should imply "a >= c".  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, b, GE_EXPR, c);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
 
-    ASSERT_CONDITION_TRUE (cm, a, GE_EXPR, c);
-    ASSERT_CONDITION_UNKNOWN (cm, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, GE_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "(a < b)", "(c < d)", "(b < c)" should
@@ -1797,51 +1839,51 @@ test_transitivity ()
      but also that:
        (a < d).  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, LT_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, c, LT_EXPR, d);
-    ADD_SAT_CONSTRAINT (cm, b, LT_EXPR, c);
-
-    ASSERT_CONDITION_TRUE (cm, a, LT_EXPR, c);
-    ASSERT_CONDITION_TRUE (cm, b, LT_EXPR, d);
-    ASSERT_CONDITION_TRUE (cm, a, LT_EXPR, d);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, c, LT_EXPR, d);
+    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
+
+    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, b, LT_EXPR, d);
+    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, d);
   }
 
   /* Transitivity: "a >= b", "b >= a" should imply that a == b.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, b, GE_EXPR, a);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, a);
 
     // TODO:
-    ASSERT_CONDITION_TRUE (cm, a, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b);
   }
 
   /* Transitivity: "a >= b", "b > a" should be impossible.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, GE_EXPR, b);
-    ADD_UNSAT_CONSTRAINT (cm, b, GT_EXPR, a);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_UNSAT_CONSTRAINT (model, b, GT_EXPR, a);
   }
 
   /* Transitivity: "a >= b", "b >= c", "c >= a" should imply
      that a == b == c.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, b, GE_EXPR, c);
-    ADD_SAT_CONSTRAINT (cm, c, GE_EXPR, a);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
+    ADD_SAT_CONSTRAINT (model, c, GE_EXPR, a);
 
-    ASSERT_CONDITION_TRUE (cm, a, EQ_EXPR, c);
+    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, c);
   }
 
   /* Transitivity: "a > b", "b > c", "c > a"
      should be impossible.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, GT_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, b, GT_EXPR, c);
-    ADD_UNSAT_CONSTRAINT (cm, c, GT_EXPR, a);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
+    ADD_UNSAT_CONSTRAINT (model, c, GT_EXPR, a);
   }
 
 }
@@ -1851,51 +1893,51 @@ test_transitivity ()
 static void
 test_constant_comparisons ()
 {
-  svalue_id int_3 (build_int_cst (integer_type_node, 3), 0);
-  svalue_id int_4 (build_int_cst (integer_type_node, 4), 0);
-  svalue_id int_5 (build_int_cst (integer_type_node, 5), 0);
+  tree int_3 = build_int_cst (integer_type_node, 3);
+  tree int_4 = build_int_cst (integer_type_node, 4);
+  tree int_5 = build_int_cst (integer_type_node, 5);
 
-  svalue_id int_1023 (build_int_cst (integer_type_node, 1023), 0);
-  svalue_id int_1024 (build_int_cst (integer_type_node, 1024), 0);
+  tree int_1023 = build_int_cst (integer_type_node, 1023);
+  tree int_1024 = build_int_cst (integer_type_node, 1024);
 
-  svalue_id a (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("a"),
-			  integer_type_node), 0);
-  svalue_id b (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("b"),
-			  integer_type_node), 0);
+  tree a = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("a"),
+		       integer_type_node);
+  tree b = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("b"),
+		       integer_type_node);
 
   /* Given a >= 1024, then a <= 1023 should be impossible.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, GE_EXPR, int_1024);
-    ADD_UNSAT_CONSTRAINT (cm, a, LE_EXPR, int_1023);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_1024);
+    ADD_UNSAT_CONSTRAINT (model, a, LE_EXPR, int_1023);
   }
 
   /* a > 4.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, GT_EXPR, int_4);
-    ASSERT_CONDITION_TRUE (cm, a, GT_EXPR, int_4);
-    ASSERT_CONDITION_TRUE (cm, a, NE_EXPR, int_3);
-    ASSERT_CONDITION_UNKNOWN (cm, a, NE_EXPR, int_5);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_4);
+    ASSERT_CONDITION_TRUE (model, a, GT_EXPR, int_4);
+    ASSERT_CONDITION_TRUE (model, a, NE_EXPR, int_3);
+    ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_5);
   }
 
   /* a <= 4.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, LE_EXPR, int_4);
-    ASSERT_CONDITION_FALSE (cm, a, GT_EXPR, int_4);
-    ASSERT_CONDITION_FALSE (cm, a, GT_EXPR, int_5);
-    ASSERT_CONDITION_UNKNOWN (cm, a, NE_EXPR, int_3);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+    ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_4);
+    ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_5);
+    ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_3);
   }
 
   /* If "a > b" and "a == 3", then "b == 4" ought to be unsatisfiable.  */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, a, GT_EXPR, b);
-    ADD_SAT_CONSTRAINT (cm, a, EQ_EXPR, int_3);
-    ADD_UNSAT_CONSTRAINT (cm, b, EQ_EXPR, int_4);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, int_3);
+    ADD_UNSAT_CONSTRAINT (model, b, EQ_EXPR, int_4);
   }
 
   /* Various tests of int ranges where there is only one possible candidate.  */
@@ -1903,52 +1945,52 @@ test_constant_comparisons ()
     /* If "a <= 4" && "a > 3", then "a == 4",
        assuming a is of integral type.  */
     {
-      constraint_manager cm;
-      ADD_SAT_CONSTRAINT (cm, a, LE_EXPR, int_4);
-      ADD_SAT_CONSTRAINT (cm, a, GT_EXPR, int_3);
-      ASSERT_CONDITION_TRUE (cm, a, EQ_EXPR, int_4);
+      region_model model;
+      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
+      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
     }
 
     /* If "a > 3" && "a <= 4", then "a == 4",
        assuming a is of integral type.  */
     {
-      constraint_manager cm;
-      ADD_SAT_CONSTRAINT (cm, a, GT_EXPR, int_3);
-      ADD_SAT_CONSTRAINT (cm, a, LE_EXPR, int_4);
-      ASSERT_CONDITION_TRUE (cm, a, EQ_EXPR, int_4);
+      region_model model;
+      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
+      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
     }
     /* If "a > 3" && "a < 5", then "a == 4",
        assuming a is of integral type.  */
     {
-      constraint_manager cm;
-      ADD_SAT_CONSTRAINT (cm, a, GT_EXPR, int_3);
-      ADD_SAT_CONSTRAINT (cm, a, LT_EXPR, int_5);
-      ASSERT_CONDITION_TRUE (cm, a, EQ_EXPR, int_4);
+      region_model model;
+      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
+      ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
+      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
     }
     /* If "a >= 4" && "a < 5", then "a == 4",
        assuming a is of integral type.  */
     {
-      constraint_manager cm;
-      ADD_SAT_CONSTRAINT (cm, a, GE_EXPR, int_4);
-      ADD_SAT_CONSTRAINT (cm, a, LT_EXPR, int_5);
-      ASSERT_CONDITION_TRUE (cm, a, EQ_EXPR, int_4);
+      region_model model;
+      ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
+      ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
+      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
     }
     /* If "a >= 4" && "a <= 4", then "a == 4".  */
     {
-      constraint_manager cm;
-      ADD_SAT_CONSTRAINT (cm, a, GE_EXPR, int_4);
-      ADD_SAT_CONSTRAINT (cm, a, LE_EXPR, int_4);
-      ASSERT_CONDITION_TRUE (cm, a, EQ_EXPR, int_4);
+      region_model model;
+      ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
+      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
     }
   }
 
 #if 0
   /* As above, but for float.   */
   {
-    constraint_manager cm;
-    ADD_SAT_CONSTRAINT (cm, f, GT_EXPR, float_3);
-    ADD_SAT_CONSTRAINT (cm, f, LE_EXPR, float_4);
-    ASSERT_CONDITION_UNKNOWN (cm, f, EQ_EXPR, int_4);
+    region_model model;
+    ADD_SAT_CONSTRAINT (model, f, GT_EXPR, float_3);
+    ADD_SAT_CONSTRAINT (model, f, LE_EXPR, float_4);
+    ASSERT_CONDITION_UNKNOWN (model, f, EQ_EXPR, int_4);
   }
 #endif
 }
@@ -1958,83 +2000,89 @@ test_constant_comparisons ()
 static void
 test_constraint_impl ()
 {
-  svalue_id int_42 (build_int_cst (integer_type_node, 42), 0);
-  svalue_id int_0 (build_int_cst (integer_type_node, 0), 0);
-
-  svalue_id x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("x"),
-			  integer_type_node), 0);
-  svalue_id y (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("y"),
-			  integer_type_node), 0);
-  svalue_id z (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("z"),
-			  integer_type_node), 0);
+  tree int_42 = build_int_cst (integer_type_node, 42);
+  tree int_0 = build_int_cst (integer_type_node, 0);
+
+  tree x = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("x"),
+		       integer_type_node);
+  tree y = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("y"),
+		       integer_type_node);
+  tree z = build_decl (UNKNOWN_LOCATION, VAR_DECL,
+		       get_identifier ("z"),
+		       integer_type_node);
 
   /* x == y.  */
   {
-    constraint_manager cm;
+    region_model model;
 
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
 
-    /* Assert various things about the insides of cm.  */
-    ASSERT_EQ (cm.m_constraints.length (), 0);
-    ASSERT_EQ (cm.m_equiv_classes.length (), 1);
+    /* Assert various things about the insides of model.  */
+    constraint_manager *cm = model.get_constraints ();
+    ASSERT_EQ (cm->m_constraints.length (), 0);
+    ASSERT_EQ (cm->m_equiv_classes.length (), 1);
   }
 
   /* y <= z; x == y.  */
   {
-    constraint_manager cm;
-    ASSERT_CONDITION_UNKNOWN (cm, x, EQ_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GE_EXPR, z);
+    region_model model;
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
 
-    ADD_SAT_CONSTRAINT (cm, y, GE_EXPR, z);
-    ASSERT_CONDITION_TRUE (cm, y, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GE_EXPR, z);
+    ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
 
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
 
-    /* Assert various things about the insides of cm.  */
-    ASSERT_EQ (cm.m_constraints.length (), 1);
-    ASSERT_EQ (cm.m_equiv_classes.length (), 2);
+    /* Assert various things about the insides of model.  */
+    constraint_manager *cm = model.get_constraints ();
+    ASSERT_EQ (cm->m_constraints.length (), 1);
+    ASSERT_EQ (cm->m_equiv_classes.length (), 2);
 
     /* Ensure that we merged the constraints.  */
-    ASSERT_CONDITION_TRUE (cm, x, GE_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
   }
 
   /* y <= z; y == x.  */
   {
-    constraint_manager cm;
-    ASSERT_CONDITION_UNKNOWN (cm, x, EQ_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GE_EXPR, z);
+    region_model model;
+    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
 
-    ADD_SAT_CONSTRAINT (cm, y, GE_EXPR, z);
-    ASSERT_CONDITION_TRUE (cm, y, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (cm, x, GE_EXPR, z);
+    ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
 
-    ADD_SAT_CONSTRAINT (cm, y, EQ_EXPR, x);
+    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, x);
 
-    /* Assert various things about the insides of cm.  */
-    ASSERT_EQ (cm.m_constraints.length (), 1);
-    ASSERT_EQ (cm.m_equiv_classes.length (), 2);
+    /* Assert various things about the insides of model.  */
+    constraint_manager *cm = model.get_constraints ();
+    ASSERT_EQ (cm->m_constraints.length (), 1);
+    ASSERT_EQ (cm->m_equiv_classes.length (), 2);
 
     /* Ensure that we merged the constraints.  */
-    ASSERT_CONDITION_TRUE (cm, x, GE_EXPR, z);
+    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
   }
 
   /* x == 0, then x != 42.  */
   {
-    constraint_manager cm;
-
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, int_0);
-    ADD_SAT_CONSTRAINT (cm, x, NE_EXPR, int_42);
-
-    /* Assert various things about the insides of cm.  */
-    ASSERT_EQ (cm.m_constraints.length (), 1);
-    ASSERT_EQ (cm.m_equiv_classes.length (), 2);
-    ASSERT_EQ (cm.m_constraints[0].m_lhs, cm.get_or_add_equiv_class (int_0));
-    ASSERT_EQ (cm.m_constraints[0].m_rhs, cm.get_or_add_equiv_class (int_42));
-    ASSERT_EQ (cm.m_constraints[0].m_op, CONSTRAINT_LT);
+    region_model model;
+
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, int_42);
+
+    /* Assert various things about the insides of model.  */
+    constraint_manager *cm = model.get_constraints ();
+    ASSERT_EQ (cm->m_constraints.length (), 1);
+    ASSERT_EQ (cm->m_equiv_classes.length (), 2);
+    ASSERT_EQ (cm->m_constraints[0].m_lhs,
+	       cm->get_or_add_equiv_class (model.get_rvalue (int_0)));
+    ASSERT_EQ (cm->m_constraints[0].m_rhs,
+	       cm->get_or_add_equiv_class (model.get_rvalue (int_42)));
+    ASSERT_EQ (cm->m_constraints[0].m_op, CONSTRAINT_LT);
   }
 
   // TODO: selftest for merging ecs "in the middle"
@@ -2043,6 +2091,7 @@ test_constraint_impl ()
   // TODO: selftest where there are pre-existing constraints
 }
 
+#if 0
 /* FIXME.  */
 
 static void
@@ -2064,38 +2113,9 @@ test_assignment ()
   ASSERT_CONDITION_TRUE (cm, y, EQ_EXPR, int_0);
   ASSERT_CONDITION_TRUE (cm, y, EQ_EXPR, x);
 }
+#endif
 
-/* FIXME.  */
-
-static void
-test_stack_frames ()
-{
-  svalue_id int_42 (build_int_cst (integer_type_node, 42), 0);
-  svalue_id int_0 (build_int_cst (integer_type_node, 0), 0);
-
-  /* "a" in the parent frame.  */
-  svalue_id a (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("a"),
-			  integer_type_node), 0);
-  /* "x" in a child frame.  */
-  svalue_id x (build_decl (UNKNOWN_LOCATION, PARM_DECL,
-			  get_identifier ("x"),
-			  integer_type_node), 1);
-
-  {
-    constraint_manager cm;
-    cm.m_stack_depth = 1;
-
-    /* x == a.  */
-    ADD_SAT_CONSTRAINT (cm, x, EQ_EXPR, a);
-    ASSERT_CONDITION_TRUE (cm, x, EQ_EXPR, a);
-
-    /* Pop the stack.  */
-    cm.pop_stack_frame ();
-    ASSERT_CONDITION_UNKNOWN (cm, x, EQ_EXPR, a);
-  }
-}
-
+#if 0
 /* Check that operator== and hashing works as expected for the
    various types.  */
 
@@ -2240,11 +2260,11 @@ test_purging ()
 void
 analyzer_constraint_manager_cc_tests ()
 {
-#if 0
   test_constraint_conditions ();
   test_transitivity ();
   test_constant_comparisons ();
   test_constraint_impl ();
+#if 0
   test_assignment ();
   test_stack_frames ();
   test_equality ();
diff --git a/gcc/analyzer/constraint-manager.h b/gcc/analyzer/constraint-manager.h
index 2d885b3..3c75075 100644
--- a/gcc/analyzer/constraint-manager.h
+++ b/gcc/analyzer/constraint-manager.h
@@ -164,7 +164,11 @@ class constraint_manager
 public:
   constraint_manager () {}
   constraint_manager (const constraint_manager &other);
-  ~constraint_manager ();
+  virtual ~constraint_manager ();
+
+  virtual constraint_manager *clone (region_model *) const = 0;
+  virtual tree maybe_get_constant (svalue_id sid) const = 0;
+  virtual svalue_id get_sid_for_constant (tree cst) const = 0;
 
   constraint_manager& operator= (const constraint_manager &other);
 
@@ -176,6 +180,10 @@ public:
   }
 
   std::string to_str () const;
+  void print (pretty_printer *pp) const;
+  void dump_to_pp (pretty_printer *pp) const;
+  void dump (FILE *fp) const;
+  void dump () const;
 
   const equiv_class &get_equiv_class_by_index (unsigned idx) const
   {
@@ -192,8 +200,6 @@ public:
     return ec_id.get_obj (*this);
   }
 
-  virtual tree maybe_get_constant (svalue_id sid) const = 0;
-
   void on_assignment (svalue_id lhs, svalue_id rhs);
 
   bool apply_constraints_for_edge (const superedge &edge,
@@ -221,6 +227,9 @@ public:
   tristate eval_condition (equiv_class_id lhs,
 			   enum tree_code op,
 			   equiv_class_id rhs);
+  tristate eval_condition (svalue_id lhs,
+			   enum tree_code op,
+			   svalue_id rhs);
 
   /* For implementing "__analyzer_eval".  */
   tristate dump_condition (tree lhs, enum tree_code op, tree rhs);
diff --git a/gcc/analyzer/region-model.cc b/gcc/analyzer/region-model.cc
index 979cc27..9849f73 100644
--- a/gcc/analyzer/region-model.cc
+++ b/gcc/analyzer/region-model.cc
@@ -43,6 +43,48 @@
 #include "region-model.h"
 #include "tree-diagnostic.h"
 #include "diagnostic-color.h"
+#include "constraint-manager.h"
+
+////////////////////////////////////////////////////////////////////////////
+
+class impl_constraint_manager : public constraint_manager
+{
+ public:
+  impl_constraint_manager (region_model *model)
+  : constraint_manager (),
+    m_model (model)
+  {}
+
+  impl_constraint_manager (const impl_constraint_manager &other,
+			   region_model *model)
+  : constraint_manager (other),
+    m_model (model)
+  {}
+
+  constraint_manager *clone (region_model *model) const
+  {
+    return new impl_constraint_manager (*this, model);
+  }
+
+  tree maybe_get_constant (svalue_id sid) const FINAL OVERRIDE
+  {
+    svalue *svalue = m_model->get_svalue (sid);
+    if (constant_svalue *cst_svalue = svalue->dyn_cast_constant_svalue ())
+      {
+	return cst_svalue->get_constant ();
+      }
+    return NULL_TREE;
+  }
+
+  svalue_id get_sid_for_constant (tree cst) const FINAL OVERRIDE
+  {
+    gcc_assert (CONSTANT_CLASS_P (cst));
+    return m_model->get_rvalue (cst);
+  }
+
+ private:
+  region_model *m_model;
+};
 
 ////////////////////////////////////////////////////////////////////////////
 
@@ -62,6 +104,16 @@ svalue_id::dump_node_name_to_pp (pretty_printer *pp) const
   pp_printf (pp, "svalue_%i", m_idx);
 }
 
+std::string
+svalue_id::to_str () const
+{
+  pretty_printer pp;
+  print (&pp);
+  return pp_formatted_text (&pp);
+}
+
+////////////////////////////////////////////////////////////////////////////
+
 void
 region_id::print (pretty_printer *pp) const
 {
@@ -1071,6 +1123,7 @@ svalue_constraint::operator== (const svalue_constraint &other) const
 region_model::region_model ()
 {
   m_root_rid = add_region (new root_region ());
+  m_constraints = new impl_constraint_manager (this);
   // TODO
 }
 
@@ -1090,9 +1143,7 @@ region_model::region_model (const region_model &other)
   FOR_EACH_VEC_ELT (other.m_regions, i, region)
     m_regions.safe_push (region->clone ());
 
-  svalue_constraint *c;
-  FOR_EACH_VEC_ELT (other.m_constraints, i, c)
-    m_constraints.safe_push (*c);
+  m_constraints = other.m_constraints->clone (this);
 }
 
 /* FIXME.  */
@@ -1109,7 +1160,7 @@ region_model::operator== (const region_model &other) const
   if (m_svalues.length () != other.m_svalues.length ())
     return false;
 
-  if (m_constraints.length () != other.m_constraints.length ())
+  if (!(m_constraints == other.m_constraints))
     return false;
 
   unsigned i;
@@ -1123,11 +1174,6 @@ region_model::operator== (const region_model &other) const
     if (!(*m_regions[i] == *other.m_regions[i]))
       return false;
 
-  svalue_constraint *c;
-  FOR_EACH_VEC_ELT (other.m_constraints, i, c)
-    if (!(m_constraints[i] == other.m_constraints[i]))
-      return false;
-
   return true;
 }
 
@@ -1180,17 +1226,9 @@ region_model::print (pretty_printer *pp) const
       region->print (*this, region_id::from_int (i), pp);
     }
 
-  pp_string (pp, "], constraints: [");
-
-  svalue_constraint *c;
-  FOR_EACH_VEC_ELT (m_constraints, i, c)
-    {
-      if (i > 0)
-	pp_string (pp, ", ");
-      c->print (*this, pp);
-    }
+  pp_string (pp, "], constraints: ");
 
-  pp_string (pp, "]");
+  m_constraints->print (pp);
 }
 
 /* FIXME.  */
@@ -1288,15 +1326,9 @@ region_model::dump_to_pp (pretty_printer *pp) const
       pp_newline (pp);
     }
 
-  pp_string (pp, "constraints:");
+  pp_string (pp, "constraint manager:");
   pp_newline (pp);
-  svalue_constraint *c;
-  FOR_EACH_VEC_ELT (m_constraints, i, c)
-    {
-      pp_string (pp, "  ");
-      c->print (*this, pp);
-      pp_newline (pp);
-    }
+  m_constraints->dump_to_pp (pp);
 }
 
 /* FIXME.  */
@@ -1931,6 +1963,8 @@ region_model::eval_condition (svalue_id lhs_sid,
   /* FIXME: this is a very simplistic implementation.  */
 
 #if 1
+  return m_constraints->eval_condition (lhs_sid, op, rhs_sid);
+#else
   unsigned i;
   svalue_constraint *c;
   FOR_EACH_VEC_ELT (m_constraints, i, c)
@@ -1975,8 +2009,14 @@ region_model::add_constraint (tree lhs, enum tree_code op, tree rhs)
   /* Store the constraint.  */
 
 #if 1
+
+#if 1
+  m_constraints->add_constraint (lhs_sid, op, rhs_sid);
+#else
   /* For now, a trivial implementation.  */
   m_constraints.safe_push (svalue_constraint (lhs_sid, op, rhs_sid));
+#endif
+
 #else
   svalue *lhs_sval = get_svalue (lhs_sid);
   svalue *rhs_sval = get_svalue (rhs_sid);
@@ -2360,7 +2400,9 @@ test_dump ()
 		"svalues:\n"
 		"  sv0: {poisoned: uninit}\n"
 		"  sv1: {poisoned: uninit}\n"
-		"constraints:\n");
+		"constraint manager:\n"
+		"  equiv classes:\n"
+		"  constraints:\n");
 }
 
 static void
@@ -2374,687 +2416,12 @@ test_unique_constants ()
   ASSERT_NE (model.get_rvalue (int_0), model.get_rvalue (int_42));
 }
 
-/* Attempt to add the constraint (LHS OP RHS) to MODEL.
-   Verify that MODEL remains satisfiable.  */
-
-#define ADD_SAT_CONSTRAINT(MODEL, LHS, OP, RHS)	\
-  SELFTEST_BEGIN_STMT					\
-    bool sat = (MODEL).add_constraint (LHS, OP, RHS);	\
-    ASSERT_TRUE (sat);					\
-  SELFTEST_END_STMT
-
-/* Attempt to add the constraint (LHS OP RHS) to MODEL.
-   Verify that the result is not satisfiable.  */
-
-#define ADD_UNSAT_CONSTRAINT(MODEL, LHS, OP, RHS)	\
-  SELFTEST_BEGIN_STMT					\
-    bool sat = (MODEL).add_constraint (LHS, OP, RHS);	\
-    ASSERT_FALSE (sat);				\
-  SELFTEST_END_STMT
-
-static void
-assert_condition (const location &loc,
-		  region_model &model,
-		  tree lhs, tree_code op, tree rhs,
-		  tristate expected)
-{
-  tristate actual = model.eval_condition (lhs, op, rhs);
-  ASSERT_EQ_AT (loc, actual, expected);
-}
-
-#define ASSERT_CONDITION_TRUE(PATH_STATE, LHS, OP, RHS) \
-  SELFTEST_BEGIN_STMT							\
-  assert_condition (SELFTEST_LOCATION, PATH_STATE, LHS, OP, RHS,	\
-		    tristate (tristate::TS_TRUE));		\
-  SELFTEST_END_STMT
-
-#define ASSERT_CONDITION_FALSE(PATH_STATE, LHS, OP, RHS) \
-  SELFTEST_BEGIN_STMT							\
-  assert_condition (SELFTEST_LOCATION, PATH_STATE, LHS, OP, RHS,	\
-		    tristate (tristate::TS_FALSE));		\
-  SELFTEST_END_STMT
-
-#define ASSERT_CONDITION_UNKNOWN(PATH_STATE, LHS, OP, RHS) \
-  SELFTEST_BEGIN_STMT							\
-  assert_condition (SELFTEST_LOCATION, PATH_STATE, LHS, OP, RHS,	\
-		    tristate (tristate::TS_UNKNOWN));		\
-  SELFTEST_END_STMT
-
-/* FIXME.  */
-
-static void
-test_constraint_conditions ()
-{
-  tree int_42 = build_int_cst (integer_type_node, 42);
-  tree int_0 = build_int_cst (integer_type_node, 0);
-
-  tree x = build_decl (UNKNOWN_LOCATION, VAR_DECL,
-		      get_identifier ("x"),
-		      integer_type_node);
-  tree y = build_decl (UNKNOWN_LOCATION, VAR_DECL,
-		       get_identifier ("y"),
-		       integer_type_node);
-  tree z = build_decl (UNKNOWN_LOCATION, VAR_DECL,
-		       get_identifier ("z"),
-		       integer_type_node);
-
-  /* Self-comparisons.  */
-  {
-    region_model model;
-    ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, x, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, x);
-  }
-
-  /* x == y.  */
-  {
-    region_model model;
-    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
-
-    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
-
-    ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, y);
-#if 0
-    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
-    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
-#endif
-    ASSERT_CONDITION_FALSE (model, x, NE_EXPR, y);
-#if 0
-    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
-
-    /* Swapped operands.  */
-    ASSERT_CONDITION_TRUE (model, y, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
-
-    /* Comparison with other var.  */
-    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z);
-#endif
-  }
-
-#if 0
-
-  /* x == y, then y == z  */
-  {
-    region_model model;
-    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
-
-    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
-    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, z);
-
-    ASSERT_CONDITION_TRUE (model, x, EQ_EXPR, z);
-    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, z);
-    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
-    ASSERT_CONDITION_FALSE (model, x, NE_EXPR, z);
-    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, z);
-    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, z);
-  }
-
-  /* x != y.  */
-  {
-    region_model model;
-
-    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
-
-    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y);
-
-    /* Swapped operands.  */
-    ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x);
-
-    /* Comparison with other var.  */
-    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, z);
-  }
-
-  /* x < y.  */
-  {
-    region_model model;
-
-    ADD_SAT_CONSTRAINT (model, x, LT_EXPR, y);
-
-    ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y);
-    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
-    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y);
-
-    /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, y, LE_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, y, GT_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
-  }
-
-  /* x <= y.  */
-  {
-    region_model model;
-
-    ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
-
-    ASSERT_CONDITION_UNKNOWN (model, x, LT_EXPR, y);
-    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, y);
-
-    /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (model, y, LT_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, LE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, GT_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, x);
-  }
-
-  /* x > y.  */
-  {
-    region_model model;
-
-    ADD_SAT_CONSTRAINT (model, x, GT_EXPR, y);
-
-    ASSERT_CONDITION_TRUE (model, x, GT_EXPR, y);
-    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
-    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, LE_EXPR, y);
-
-    /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, y, GE_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, y, NE_EXPR, x);
-    ASSERT_CONDITION_FALSE (model, y, EQ_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, y, LT_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
-  }
-
-  /* x >= y.  */
-  {
-    region_model model;
-
-    ADD_SAT_CONSTRAINT (model, x, GE_EXPR, y);
-
-    ASSERT_CONDITION_UNKNOWN (model, x, GT_EXPR, y);
-    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, NE_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, LT_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, LE_EXPR, y);
-
-    /* Swapped operands.  */
-    ASSERT_CONDITION_FALSE (model, y, GT_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, GE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, NE_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, EQ_EXPR, x);
-    ASSERT_CONDITION_UNKNOWN (model, y, LT_EXPR, x);
-    ASSERT_CONDITION_TRUE (model, y, LE_EXPR, x);
-  }
-
-  // TODO: implied orderings
-
-  /* Constants.  */
-  {
-    region_model model;
-    ASSERT_CONDITION_FALSE (model, int_0, EQ_EXPR, int_42);
-    ASSERT_CONDITION_TRUE (model, int_0, NE_EXPR, int_42);
-    ASSERT_CONDITION_TRUE (model, int_0, LT_EXPR, int_42);
-    ASSERT_CONDITION_TRUE (model, int_0, LE_EXPR, int_42);
-    ASSERT_CONDITION_FALSE (model, int_0, GT_EXPR, int_42);
-    ASSERT_CONDITION_FALSE (model, int_0, GE_EXPR, int_42);
-  }
-
-  /* x == 0, y == 42.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
-    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, int_42);
-
-    ASSERT_CONDITION_TRUE (model, x, NE_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, EQ_EXPR, y);
-    ASSERT_CONDITION_TRUE (model, x, LE_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, GE_EXPR, y);
-    ASSERT_CONDITION_TRUE (model, x, LT_EXPR, y);
-    ASSERT_CONDITION_FALSE (model, x, GT_EXPR, y);
-  }
-
-  /* Unsatisfiable combinations.  */
-
-  /* x == y && x != y.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
-    ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, y);
-  }
-
-  /* x == 0 then x == 42.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
-    ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, int_42);
-  }
-
-  /* x == 0 then x != 0.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
-    ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, int_0);
-  }
-
-  /* x == 0 then x > 0.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
-    ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, int_0);
-  }
-
-  /* x != y && x == y.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
-    ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, y);
-  }
-
-  /* x <= y && x > y.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
-    ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, y);
-  }
-
-#endif
-
-  // etc
-}
 
 #if 0
 
 /* FIXME.  */
 
 static void
-test_transitivity ()
-{
-  tree int_42 (build_int_cst (integer_type_node, 42), 0);
-  tree int_0 (build_int_cst (integer_type_node, 0), 0);
-
-  tree a (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("a"),
-			  integer_type_node);
-  tree b (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("b"),
-			  integer_type_node);
-  tree c (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("c"),
-			  integer_type_node);
-  tree d (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("d"),
-			  integer_type_node);
-
-  /* a == b, then c == d, then c == b.  */
-  {
-    region_model model;
-    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, b);
-    ASSERT_CONDITION_UNKNOWN (model, b, EQ_EXPR, c);
-    ASSERT_CONDITION_UNKNOWN (model, c, EQ_EXPR, d);
-    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d);
-
-    ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, b);
-    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b);
-
-    ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, d);
-    ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, d);
-    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, d);
-
-    ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, b);
-    ASSERT_CONDITION_TRUE (model, c, EQ_EXPR, b);
-    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, d);
-  }
-
-  /* Transitivity: "a < b", "b < c" should imply "a < c".  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
-
-    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
-    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
-  }
-
-  /* Transitivity: "a <= b", "b < c" should imply "a < c".  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
-
-    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
-    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
-  }
-
-  /* Transitivity: "a <= b", "b <= c" should imply "a <= c".  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, b, LE_EXPR, c);
-
-    ASSERT_CONDITION_TRUE (model, a, LE_EXPR, c);
-    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c);
-  }
-
-  /* Transitivity: "a > b", "b > c" should imply "a > c".  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
-
-    ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c);
-    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
-  }
-
-  /* Transitivity: "a >= b", "b > c" should imply " a > c".  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
-
-    ASSERT_CONDITION_TRUE (model, a, GT_EXPR, c);
-    ASSERT_CONDITION_FALSE (model, a, EQ_EXPR, c);
-  }
-
-  /* Transitivity: "a >= b", "b >= c" should imply "a >= c".  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
-
-    ASSERT_CONDITION_TRUE (model, a, GE_EXPR, c);
-    ASSERT_CONDITION_UNKNOWN (model, a, EQ_EXPR, c);
-  }
-
-  /* Transitivity: "(a < b)", "(c < d)", "(b < c)" should
-     imply the easy cases:
-       (a < c)
-       (b < d)
-     but also that:
-       (a < d).  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, c, LT_EXPR, d);
-    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
-
-    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, c);
-    ASSERT_CONDITION_TRUE (model, b, LT_EXPR, d);
-    ASSERT_CONDITION_TRUE (model, a, LT_EXPR, d);
-  }
-
-  /* Transitivity: "a >= b", "b >= a" should imply that a == b.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, a);
-
-    // TODO:
-    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, b);
-  }
-
-  /* Transitivity: "a >= b", "b > a" should be impossible.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
-    ADD_UNSAT_CONSTRAINT (model, b, GT_EXPR, a);
-  }
-
-  /* Transitivity: "a >= b", "b >= c", "c >= a" should imply
-     that a == b == c.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
-    ADD_SAT_CONSTRAINT (model, c, GE_EXPR, a);
-
-    ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, c);
-  }
-
-  /* Transitivity: "a > b", "b > c", "c > a"
-     should be impossible.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
-    ADD_UNSAT_CONSTRAINT (model, c, GT_EXPR, a);
-  }
-
-}
-
-/* FIXME.  */
-
-static void
-test_constant_comparisons ()
-{
-  tree int_3 (build_int_cst (integer_type_node, 3), 0);
-  tree int_4 (build_int_cst (integer_type_node, 4), 0);
-  tree int_5 (build_int_cst (integer_type_node, 5), 0);
-
-  tree int_1023 (build_int_cst (integer_type_node, 1023), 0);
-  tree int_1024 (build_int_cst (integer_type_node, 1024), 0);
-
-  tree a (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("a"),
-			  integer_type_node);
-  tree b (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("b"),
-			  integer_type_node);
-
-  /* Given a >= 1024, then a <= 1023 should be impossible.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_1024);
-    ADD_UNSAT_CONSTRAINT (model, a, LE_EXPR, int_1023);
-  }
-
-  /* a > 4.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_4);
-    ASSERT_CONDITION_TRUE (model, a, GT_EXPR, int_4);
-    ASSERT_CONDITION_TRUE (model, a, NE_EXPR, int_3);
-    ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_5);
-  }
-
-  /* a <= 4.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
-    ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_4);
-    ASSERT_CONDITION_FALSE (model, a, GT_EXPR, int_5);
-    ASSERT_CONDITION_UNKNOWN (model, a, NE_EXPR, int_3);
-  }
-
-  /* If "a > b" and "a == 3", then "b == 4" ought to be unsatisfiable.  */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
-    ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, int_3);
-    ADD_UNSAT_CONSTRAINT (model, b, EQ_EXPR, int_4);
-  }
-
-  /* Various tests of int ranges where there is only one possible candidate.  */
-  {
-    /* If "a <= 4" && "a > 3", then "a == 4",
-       assuming a is of integral type.  */
-    {
-      region_model model;
-      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
-      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
-      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
-    }
-
-    /* If "a > 3" && "a <= 4", then "a == 4",
-       assuming a is of integral type.  */
-    {
-      region_model model;
-      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
-      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
-      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
-    }
-    /* If "a > 3" && "a < 5", then "a == 4",
-       assuming a is of integral type.  */
-    {
-      region_model model;
-      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
-      ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
-      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
-    }
-    /* If "a >= 4" && "a < 5", then "a == 4",
-       assuming a is of integral type.  */
-    {
-      region_model model;
-      ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
-      ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
-      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
-    }
-    /* If "a >= 4" && "a <= 4", then "a == 4".  */
-    {
-      region_model model;
-      ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
-      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
-      ASSERT_CONDITION_TRUE (model, a, EQ_EXPR, int_4);
-    }
-  }
-
-#if 0
-  /* As above, but for float.   */
-  {
-    region_model model;
-    ADD_SAT_CONSTRAINT (model, f, GT_EXPR, float_3);
-    ADD_SAT_CONSTRAINT (model, f, LE_EXPR, float_4);
-    ASSERT_CONDITION_UNKNOWN (model, f, EQ_EXPR, int_4);
-  }
-#endif
-}
-
-/* FIXME.  */
-
-static void
-test_constraint_impl ()
-{
-  tree int_42 (build_int_cst (integer_type_node, 42), 0);
-  tree int_0 (build_int_cst (integer_type_node, 0), 0);
-
-  tree x (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("x"),
-			  integer_type_node);
-  tree y (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("y"),
-			  integer_type_node);
-  tree z (build_decl (UNKNOWN_LOCATION, VAR_DECL,
-			  get_identifier ("z"),
-			  integer_type_node);
-
-  /* x == y.  */
-  {
-    region_model model;
-
-    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
-
-    /* Assert various things about the insides of model.  */
-    ASSERT_EQ (model.m_constraints.length (), 0);
-    ASSERT_EQ (model.m_equiv_classes.length (), 1);
-  }
-
-  /* y <= z; x == y.  */
-  {
-    region_model model;
-    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
-
-    ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
-    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
-
-    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
-
-    /* Assert various things about the insides of model.  */
-    ASSERT_EQ (model.m_constraints.length (), 1);
-    ASSERT_EQ (model.m_equiv_classes.length (), 2);
-
-    /* Ensure that we merged the constraints.  */
-    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
-  }
-
-  /* y <= z; y == x.  */
-  {
-    region_model model;
-    ASSERT_CONDITION_UNKNOWN (model, x, EQ_EXPR, y);
-    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
-
-    ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
-    ASSERT_CONDITION_TRUE (model, y, GE_EXPR, z);
-    ASSERT_CONDITION_UNKNOWN (model, x, GE_EXPR, z);
-
-    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, x);
-
-    /* Assert various things about the insides of model.  */
-    ASSERT_EQ (model.m_constraints.length (), 1);
-    ASSERT_EQ (model.m_equiv_classes.length (), 2);
-
-    /* Ensure that we merged the constraints.  */
-    ASSERT_CONDITION_TRUE (model, x, GE_EXPR, z);
-  }
-
-  /* x == 0, then x != 42.  */
-  {
-    region_model model;
-
-    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
-    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, int_42);
-
-    /* Assert various things about the insides of model.  */
-    ASSERT_EQ (model.m_constraints.length (), 1);
-    ASSERT_EQ (model.m_equiv_classes.length (), 2);
-    ASSERT_EQ (model.m_constraints[0].m_lhs, model.get_or_add_equiv_class (int_0));
-    ASSERT_EQ (model.m_constraints[0].m_rhs, model.get_or_add_equiv_class (int_42));
-    ASSERT_EQ (model.m_constraints[0].m_op, CONSTRAINT_LT);
-  }
-
-  // TODO: selftest for merging ecs "in the middle"
-  // where a non-final one gets overwritten
-
-  // TODO: selftest where there are pre-existing constraints
-}
-
-/* FIXME.  */
-
-static void
 test_assignment ()
 {
   tree int_0 (build_int_cst (integer_type_node, 0), 0);
@@ -3251,11 +2618,7 @@ analyzer_region_model_cc_tests ()
 {
   test_dump ();
   test_unique_constants ();
-  test_constraint_conditions ();
 #if 0
-  test_transitivity ();
-  test_constant_comparisons ();
-  test_constraint_impl ();
   test_assignment ();
   test_stack_frames ();
   test_equality ();
diff --git a/gcc/analyzer/region-model.h b/gcc/analyzer/region-model.h
index 64fe380..491bccf 100644
--- a/gcc/analyzer/region-model.h
+++ b/gcc/analyzer/region-model.h
@@ -36,6 +36,8 @@ class svalue;
 class region;
 class region_model;
 
+class constraint_manager;
+
 /* A region_model is effectively a graph of regions and symbolic values.
    We store per-model IDs rather than pointers to make it easier to clone
    and to compare graphs.  */
@@ -67,6 +69,7 @@ public:
 
   void print (pretty_printer *pp) const;
   void dump_node_name_to_pp (pretty_printer *pp) const;
+  std::string to_str () const;
 
 private:
   svalue_id (int idx) : m_idx (idx) {}
@@ -664,6 +667,12 @@ class region_model
 
   tree maybe_get_constant (svalue_id sid);
 
+  /* For selftests.  */
+  constraint_manager *get_constraints ()
+  {
+    return m_constraints;
+  }
+
  private:
   void update_for_call_superedge (const call_superedge &call_edge);
   void update_for_return_superedge (const return_superedge &return_edge);
@@ -677,7 +686,11 @@ class region_model
   auto_delete_vec<region> m_regions;
   region_id m_root_rid;
  private:
+#if 1
+  constraint_manager *m_constraints; // FIXME: embed, rather than dynalloc?
+#else
   auto_vec<svalue_constraint> m_constraints; // TODO hash, copy-ctor, etc
+#endif
 };
 
 namespace inchash
diff --git a/gcc/testsuite/gcc.dg/analyzer/abort.c b/gcc/testsuite/gcc.dg/analyzer/abort.c
index cfbf74c..285a4c7 100644
--- a/gcc/testsuite/gcc.dg/analyzer/abort.c
+++ b/gcc/testsuite/gcc.dg/analyzer/abort.c
@@ -1,3 +1,5 @@
+/* { dg-additional-options "-fanalyzer-region-model" } */
+
 #include <assert.h>
 #include <stdio.h>
 #include <stdlib.h>
diff --git a/gcc/testsuite/gcc.dg/analyzer/conditionals.c b/gcc/testsuite/gcc.dg/analyzer/conditionals.c
index 578a9b8..28f6978 100644
--- a/gcc/testsuite/gcc.dg/analyzer/conditionals.c
+++ b/gcc/testsuite/gcc.dg/analyzer/conditionals.c
@@ -1,3 +1,5 @@
+/* { dg-additional-options "-fanalyzer-region-model" } */
+
 void test (int i, int j)
 {
   if (i > 4)
diff --git a/gcc/testsuite/gcc.dg/analyzer/equivalence.c b/gcc/testsuite/gcc.dg/analyzer/equivalence.c
index fb28660..3986967 100644
--- a/gcc/testsuite/gcc.dg/analyzer/equivalence.c
+++ b/gcc/testsuite/gcc.dg/analyzer/equivalence.c
@@ -1,3 +1,5 @@
+/* { dg-additional-options "-fanalyzer-region-model" } */
+
 void test (int p, int q, int r)
 {
   if (p == 42)
diff --git a/gcc/testsuite/gcc.dg/analyzer/operations.c b/gcc/testsuite/gcc.dg/analyzer/operations.c
index 9ea2327..a5e0997 100644
--- a/gcc/testsuite/gcc.dg/analyzer/operations.c
+++ b/gcc/testsuite/gcc.dg/analyzer/operations.c
@@ -1,3 +1,5 @@
+/* { dg-additional-options "-fanalyzer-region-model" } */
+
 void test (int i, int j)
 {
   int k, m;
diff --git a/gcc/testsuite/gcc.dg/analyzer/params-2.c b/gcc/testsuite/gcc.dg/analyzer/params-2.c
index 1584ebd..ede14f1 100644
--- a/gcc/testsuite/gcc.dg/analyzer/params-2.c
+++ b/gcc/testsuite/gcc.dg/analyzer/params-2.c
@@ -1,3 +1,5 @@
+/* { dg-additional-options "-fanalyzer-region-model" } */
+
 #include <stdlib.h>
 
 static void ensure_equal (int a, int b)
diff --git a/gcc/testsuite/gcc.dg/analyzer/params.c b/gcc/testsuite/gcc.dg/analyzer/params.c
index ff405f2..d9bd530 100644
--- a/gcc/testsuite/gcc.dg/analyzer/params.c
+++ b/gcc/testsuite/gcc.dg/analyzer/params.c
@@ -1,3 +1,5 @@
+/* { dg-additional-options "-fanalyzer-region-model" } */
+
 static int called_function(int j)
 {
   int k;
diff --git a/gcc/testsuite/gcc.dg/analyzer/switch.c b/gcc/testsuite/gcc.dg/analyzer/switch.c
index a55ba2b..02e2ec0 100644
--- a/gcc/testsuite/gcc.dg/analyzer/switch.c
+++ b/gcc/testsuite/gcc.dg/analyzer/switch.c
@@ -1,3 +1,5 @@
+/* { dg-additional-options "-fanalyzer-region-model" } */
+
 void test (int i)
 {
   switch (i)
-- 
1.8.5.3

