From faa5e7a7a02e12cb95fbe6ec6bb76e21f5171a68 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Tue, 28 Apr 2020 22:08:06 -0400
Subject: [PATCH 087/237] FIXME: WIP on constraints implementation

---
 gcc/Makefile.in                     |    1 +
 gcc/analyzer/analyzer-selftests.cc  |    1 +
 gcc/analyzer/analyzer-selftests.h   |    1 +
 gcc/analyzer/analyzer.h             |    1 +
 gcc/analyzer/constraint-manager2.cc | 2306 +++++++++++++++++++++++++++
 gcc/analyzer/constraint-manager2.h  |  243 +++
 gcc/analyzer/region-model2.cc       |   39 +-
 gcc/analyzer/region-model2.h        |   13 +-
 8 files changed, 2583 insertions(+), 22 deletions(-)
 create mode 100644 gcc/analyzer/constraint-manager2.cc
 create mode 100644 gcc/analyzer/constraint-manager2.h

diff --git a/gcc/Makefile.in b/gcc/Makefile.in
index c0ea09954bc..02dbb476215 100644
--- a/gcc/Makefile.in
+++ b/gcc/Makefile.in
@@ -1225,6 +1225,7 @@ ANALYZER_OBJS = \
 	analyzer/call-string.o \
 	analyzer/checker-path.o \
 	analyzer/constraint-manager.o \
+	analyzer/constraint-manager2.o \
 	analyzer/diagnostic-manager.o \
 	analyzer/engine.o \
 	analyzer/function-set.o \
diff --git a/gcc/analyzer/analyzer-selftests.cc b/gcc/analyzer/analyzer-selftests.cc
index 03426ead60d..d1f0724ec21 100644
--- a/gcc/analyzer/analyzer-selftests.cc
+++ b/gcc/analyzer/analyzer-selftests.cc
@@ -52,6 +52,7 @@ run_analyzer_selftests ()
 {
 #if ENABLE_ANALYZER
   analyzer_constraint_manager_cc_tests ();
+  analyzer_constraint_manager2_cc_tests ();
   analyzer_function_set_cc_tests ();
   analyzer_immutable_hash_map_cc_tests ();
   analyzer_program_point_cc_tests ();
diff --git a/gcc/analyzer/analyzer-selftests.h b/gcc/analyzer/analyzer-selftests.h
index a8e115c01df..c3db56caff7 100644
--- a/gcc/analyzer/analyzer-selftests.h
+++ b/gcc/analyzer/analyzer-selftests.h
@@ -35,6 +35,7 @@ extern void run_analyzer_selftests ();
    alphabetical order.  */
 extern void analyzer_checker_script_cc_tests ();
 extern void analyzer_constraint_manager_cc_tests ();
+extern void analyzer_constraint_manager2_cc_tests ();
 extern void analyzer_function_set_cc_tests ();
 extern void analyzer_immutable_hash_map_cc_tests ();
 extern void analyzer_program_point_cc_tests ();
diff --git a/gcc/analyzer/analyzer.h b/gcc/analyzer/analyzer.h
index a1141765332..0e21bc7ba49 100644
--- a/gcc/analyzer/analyzer.h
+++ b/gcc/analyzer/analyzer.h
@@ -73,6 +73,7 @@ class region_model2_manager;
 class store2_manager;
 class region_model2;
 class region_model2_context;
+class constraint_manager2;
 
 class pending_diagnostic;
 class state_change_event;
diff --git a/gcc/analyzer/constraint-manager2.cc b/gcc/analyzer/constraint-manager2.cc
new file mode 100644
index 00000000000..fd5366a573e
--- /dev/null
+++ b/gcc/analyzer/constraint-manager2.cc
@@ -0,0 +1,2306 @@
+/* Tracking equivalence classes and constraints at a point on an execution path.
+   Copyright (C) 2019-2020 Free Software Foundation, Inc.
+   Contributed by David Malcolm <dmalcolm@redhat.com>.
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it
+under the terms of the GNU General Public License as published by
+the Free Software Foundation; either version 3, or (at your option)
+any later version.
+
+GCC 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 GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+#include "config.h"
+#include "system.h"
+#include "coretypes.h"
+#include "tree.h"
+#include "function.h"
+#include "basic-block.h"
+#include "gimple.h"
+#include "gimple-iterator.h"
+#include "fold-const.h"
+#include "selftest.h"
+#include "diagnostic-core.h"
+#include "graphviz.h"
+#include "function.h"
+#include "analyzer/analyzer.h"
+#include "ordered-hash-map.h"
+#include "options.h"
+#include "cgraph.h"
+#include "cfg.h"
+#include "digraph.h"
+#include "analyzer/supergraph.h"
+#include "sbitmap.h"
+#include "bitmap.h"
+#include "tristate.h"
+#include "analyzer/region-model2.h"
+#include "analyzer/constraint-manager2.h"
+#include "analyzer/analyzer-selftests.h"
+
+/* TODO:
+   presumably best to drop equiv_class_id in favor of just equiv_class *,
+   so that there's no ordering.
+   But maybe a deeper reworking is needed?  */
+
+#if ENABLE_ANALYZER
+
+namespace ana {
+
+/* One of the end-points of a range2.  */
+
+struct bound2
+{
+  bound2 () : m_constant (NULL_TREE), m_closed (false) {}
+  bound2 (tree constant, bool closed)
+  : m_constant (constant), m_closed (closed) {}
+
+  void ensure_closed (bool is_upper);
+
+  const char * get_relation_as_str () const;
+
+  tree m_constant;
+  bool m_closed;
+};
+
+/* A range of values, used for determining if a value has been
+   constrained to just one possible constant value.  */
+
+struct range2
+{
+  range2 () : m_lower_bound (), m_upper_bound () {}
+  range2 (const bound2 &lower, const bound2 &upper)
+  : m_lower_bound (lower), m_upper_bound (upper) {}
+
+  void dump (pretty_printer *pp) const;
+
+  bool constrained_to_single_element (tree *out);
+
+  bound2 m_lower_bound;
+  bound2 m_upper_bound;
+};
+
+/* struct bound2.  */
+
+/* Ensure that this bound2 is closed by converting an open bound2 to a
+   closed one.  */
+
+void
+bound2::ensure_closed (bool is_upper)
+{
+  if (!m_closed)
+    {
+      /* Offset by 1 in the appropriate direction.
+	 For example, convert 3 < x into 4 <= x,
+	 and convert x < 5 into x <= 4.  */
+      gcc_assert (CONSTANT_CLASS_P (m_constant));
+      m_constant = fold_build2 (is_upper ? MINUS_EXPR : PLUS_EXPR,
+				TREE_TYPE (m_constant),
+				m_constant, integer_one_node);
+      gcc_assert (CONSTANT_CLASS_P (m_constant));
+      m_closed = true;
+    }
+}
+
+/* Get "<=" vs "<" for this bound2.  */
+
+const char *
+bound2::get_relation_as_str () const
+{
+  if (m_closed)
+    return "<=";
+  else
+    return "<";
+}
+
+/* struct range2.  */
+
+/* Dump this range2 to PP, which must support %E for tree.  */
+
+void
+range2::dump (pretty_printer *pp) const
+{
+  pp_printf (pp, "%qE %s x %s %qE",
+	     m_lower_bound.m_constant,
+	     m_lower_bound.get_relation_as_str (),
+	     m_upper_bound.get_relation_as_str (),
+	     m_upper_bound.m_constant);
+}
+
+/* Determine if there is only one possible value for this range2.
+   If so, return true and write the constant to *OUT.
+   Otherwise, return false.  */
+
+bool
+range2::constrained_to_single_element (tree *out)
+{
+  if (!INTEGRAL_TYPE_P (TREE_TYPE (m_lower_bound.m_constant)))
+    return false;
+  if (!INTEGRAL_TYPE_P (TREE_TYPE (m_upper_bound.m_constant)))
+    return false;
+
+  /* Convert any open bounds to closed bounds.  */
+  m_lower_bound.ensure_closed (false);
+  m_upper_bound.ensure_closed (true);
+
+  // Are they equal?
+  tree comparison = fold_binary (EQ_EXPR, boolean_type_node,
+				 m_lower_bound.m_constant,
+				 m_upper_bound.m_constant);
+  if (comparison == boolean_true_node)
+    {
+      *out = m_lower_bound.m_constant;
+      return true;
+    }
+  else
+    return false;
+}
+
+/* class equiv_class2.  */
+
+/* equiv_class2's default ctor.  */
+
+equiv_class2::equiv_class2 ()
+: m_constant (NULL_TREE), m_cst_sval (NULL), m_vars ()
+{
+}
+
+/* equiv_class2's copy ctor.  */
+
+equiv_class2::equiv_class2 (const equiv_class2 &other)
+: m_constant (other.m_constant), m_cst_sval (other.m_cst_sval),
+  m_vars (other.m_vars.length ())
+{
+  int i;
+  svalue2 *sval;
+  FOR_EACH_VEC_ELT (other.m_vars, i, sval)
+    m_vars.quick_push (sval);
+}
+
+/* Print an all-on-one-line representation of this equiv_class2 to PP,
+   which must support %E for trees.  */
+
+void
+equiv_class2::print (pretty_printer *pp) const
+{
+  pp_character (pp, '{');
+  int i;
+  svalue2 *sval;
+  FOR_EACH_VEC_ELT (m_vars, i, sval)
+    {
+      if (i > 0)
+	pp_string (pp, " == ");
+      sval->dump_to_pp (pp, true);
+    }
+  if (m_constant)
+    {
+      if (i > 0)
+	pp_string (pp, " == ");
+      pp_printf (pp, "%qE", m_constant);
+    }
+  pp_character (pp, '}');
+}
+
+/* Generate a hash value for this equiv_class2.  */
+
+hashval_t
+equiv_class2::hash () const
+{
+  inchash::hash hstate;
+  int i;
+  svalue2 *sval;
+
+  inchash::add_expr (m_constant, hstate);
+  // TODO:
+#if 0
+  FOR_EACH_VEC_ELT (m_vars, i, sval)
+    inchash::add (sval, hstate);
+#endif
+  return hstate.end ();
+}
+
+/* Equality operator for equiv_class2.  */
+
+bool
+equiv_class2::operator== (const equiv_class2 &other)
+{
+  if (m_constant != other.m_constant)
+    return false; // TODO: use tree equality here?
+
+  /* FIXME: should we compare m_cst_sval?  */
+
+  if (m_vars.length () != other.m_vars.length ())
+    return false;
+
+  int i;
+  svalue2 *sval;
+  FOR_EACH_VEC_ELT (m_vars, i, sval)
+    if (sval != other.m_vars[i])
+      return false;
+  // FIXME: ^^^ doesn't this rely on ordering
+
+  return true;
+}
+
+/* Add SID to this equiv_class2, using CM to check if it's a constant.  */
+
+void
+equiv_class2::add (svalue2 *sval)
+{
+  gcc_assert (sval);
+  if (tree cst = sval->maybe_get_constant ())
+    {
+      gcc_assert (CONSTANT_CLASS_P (cst));
+      /* FIXME: should we canonicalize which svalue2 is the constant
+	 when there are multiple equal constants?  */
+      m_constant = cst;
+      m_cst_sval = sval;
+    }
+  m_vars.safe_push (sval);
+}
+
+/* Remove SID from this equivalence class.
+   Return true if SID was the last var in the equivalence class (suggesting
+   a possible leak).  */
+
+bool
+equiv_class2::del (svalue2 *sval)
+{
+  gcc_assert (sval);
+  gcc_assert (sval != m_cst_sval);
+
+  int i;
+  svalue2 *iv;
+  FOR_EACH_VEC_ELT (m_vars, i, iv)
+    {
+      if (iv == sval)
+	{
+	  m_vars[i] = m_vars[m_vars.length () - 1];
+	  m_vars.pop ();
+	  return m_vars.length () == 0;
+	}
+    }
+
+  /* SVAL must be in the class.  */
+  gcc_unreachable ();
+  return false;
+}
+
+/* Get a representative member of this class, for handling cases
+   where the IDs can change mid-traversal.  */
+
+svalue2 *
+equiv_class2::get_representative () const
+{
+  if (m_cst_sval)
+    return m_cst_sval;
+  else
+    {
+      gcc_assert (m_vars.length () > 0);
+      return m_vars[0];
+    }
+}
+
+#if 0
+/* Comparator for use by equiv_class2::canonicalize.  */
+
+static int
+svalue2_id_cmp_by_id (const void *p1, const void *p2)
+{
+  const svalue2 *sval1 = (const svalue2_id *)p1;
+  const svalue2 *sval2 = (const svalue2_id *)p2;
+  return sid1->as_int () - sid2->as_int ();
+}
+
+/* Sort the svalue2s_ids within this equiv_class2.  */
+
+void
+equiv_class2::canonicalize ()
+{
+  m_vars.qsort (svalue2_id_cmp_by_id);
+}
+#endif
+
+/* Get a debug string for C_OP.  */
+
+const char *
+constraint_op_code2 (enum constraint_op c_op)
+{
+  switch (c_op)
+    {
+    default:
+      gcc_unreachable ();
+    case CONSTRAINT_NE: return "!=";
+    case CONSTRAINT_LT: return "<";
+    case CONSTRAINT_LE: return "<=";
+    }
+}
+
+/* Convert C_OP to an enum tree_code.  */
+
+enum tree_code
+constraint_tree_code2 (enum constraint_op c_op)
+{
+  switch (c_op)
+    {
+    default:
+      gcc_unreachable ();
+    case CONSTRAINT_NE: return NE_EXPR;
+    case CONSTRAINT_LT: return LT_EXPR;
+    case CONSTRAINT_LE: return LE_EXPR;
+    }
+}
+
+/* Given "lhs C_OP rhs", determine "lhs T_OP rhs".
+
+   For example, given "x < y", then "x > y" is false.  */
+
+static tristate
+eval_constraint_op_for_op (enum constraint_op c_op, enum tree_code t_op)
+{
+  switch (c_op)
+    {
+    default:
+      gcc_unreachable ();
+    case CONSTRAINT_NE:
+      if (t_op == EQ_EXPR)
+	return tristate (tristate::TS_FALSE);
+      if (t_op == NE_EXPR)
+	return tristate (tristate::TS_TRUE);
+      break;
+    case CONSTRAINT_LT:
+      if (t_op == LT_EXPR || t_op == LE_EXPR || t_op == NE_EXPR)
+	return tristate (tristate::TS_TRUE);
+      if (t_op == EQ_EXPR || t_op == GT_EXPR || t_op == GE_EXPR)
+	return tristate (tristate::TS_FALSE);
+      break;
+    case CONSTRAINT_LE:
+      if (t_op == LE_EXPR)
+	return tristate (tristate::TS_TRUE);
+      if (t_op == GT_EXPR)
+	return tristate (tristate::TS_FALSE);
+      break;
+    }
+  return tristate (tristate::TS_UNKNOWN);
+}
+
+/* class constraint2.  */
+
+/* Print this constraint2 to PP (which must support %E for trees),
+   using CM to look up equiv_class2 instances from ids.  */
+
+void
+constraint2::print (pretty_printer *pp, const constraint_manager2 &cm) const
+{
+  m_lhs.print (pp);
+  pp_string (pp, ": ");
+  m_lhs.get_obj (cm).print (pp);
+  pp_string (pp, " ");
+  pp_string (pp, constraint_op_code2 (m_op));
+  pp_string (pp, " ");
+  m_rhs.print (pp);
+  pp_string (pp, ": ");
+  m_rhs.get_obj (cm).print (pp);
+}
+
+/* Generate a hash value for this constraint2.  */
+
+hashval_t
+constraint2::hash () const
+{
+  inchash::hash hstate;
+  hstate.add_int (m_lhs.m_idx);
+  hstate.add_int (m_op);
+  hstate.add_int (m_rhs.m_idx);
+  return hstate.end ();
+}
+
+/* Equality operator for constraint2s.  */
+
+bool
+constraint2::operator== (const constraint2 &other) const
+{
+  if (m_lhs != other.m_lhs)
+    return false;
+  if (m_op != other.m_op)
+    return false;
+  if (m_rhs != other.m_rhs)
+    return false;
+  return true;
+}
+
+/* class equiv_class2_id.  */
+
+/* Get the underlying equiv_class2 for this ID from CM.  */
+
+const equiv_class2 &
+equiv_class2_id::get_obj (const constraint_manager2 &cm) const
+{
+  return cm.get_equiv_class2_by_index (m_idx);
+}
+
+/* Access the underlying equiv_class2 for this ID from CM.  */
+
+equiv_class2 &
+equiv_class2_id::get_obj (constraint_manager2 &cm) const
+{
+  return cm.get_equiv_class2_by_index (m_idx);
+}
+
+/* Print this equiv_class2_id to PP.  */
+
+void
+equiv_class2_id::print (pretty_printer *pp) const
+{
+  if (null_p ())
+    pp_printf (pp, "null");
+  else
+    pp_printf (pp, "ec%i", m_idx);
+}
+
+/* class constraint_manager2.  */
+
+/* constraint_manager2's copy ctor.  */
+
+constraint_manager2::constraint_manager2 (const constraint_manager2 &other)
+: m_equiv_class2es (other.m_equiv_class2es.length ()),
+  m_constraints (other.m_constraints.length ()),
+  m_mgr (other.m_mgr)
+{
+  int i;
+  equiv_class2 *ec;
+  FOR_EACH_VEC_ELT (other.m_equiv_class2es, i, ec)
+    m_equiv_class2es.quick_push (new equiv_class2 (*ec));
+  constraint2 *c;
+  FOR_EACH_VEC_ELT (other.m_constraints, i, c)
+    m_constraints.quick_push (*c);
+}
+
+/* constraint_manager2's assignment operator.  */
+
+constraint_manager2&
+constraint_manager2::operator= (const constraint_manager2 &other)
+{
+  gcc_assert (m_equiv_class2es.length () == 0);
+  gcc_assert (m_constraints.length () == 0);
+
+  int i;
+  equiv_class2 *ec;
+  m_equiv_class2es.reserve (other.m_equiv_class2es.length ());
+  FOR_EACH_VEC_ELT (other.m_equiv_class2es, i, ec)
+    m_equiv_class2es.quick_push (new equiv_class2 (*ec));
+  constraint2 *c;
+  m_constraints.reserve (other.m_constraints.length ());
+  FOR_EACH_VEC_ELT (other.m_constraints, i, c)
+    m_constraints.quick_push (*c);
+
+  return *this;
+}
+
+/* Generate a hash value for this constraint_manager2.  */
+
+hashval_t
+constraint_manager2::hash () const
+{
+  inchash::hash hstate;
+  int i;
+  equiv_class2 *ec;
+  constraint2 *c;
+
+  FOR_EACH_VEC_ELT (m_equiv_class2es, i, ec)
+    hstate.merge_hash (ec->hash ());
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    hstate.merge_hash (c->hash ());
+  return hstate.end ();
+}
+
+/* Equality operator for constraint_manager2.  */
+
+bool
+constraint_manager2::operator== (const constraint_manager2 &other) const
+{
+  if (m_equiv_class2es.length () != other.m_equiv_class2es.length ())
+    return false;
+  if (m_constraints.length () != other.m_constraints.length ())
+    return false;
+
+  int i;
+  equiv_class2 *ec;
+
+  FOR_EACH_VEC_ELT (m_equiv_class2es, i, ec)
+    if (!(*ec == *other.m_equiv_class2es[i]))
+      return false;
+
+  constraint2 *c;
+
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    if (!(*c == other.m_constraints[i]))
+      return false;
+
+  return true;
+}
+
+/* Print this constraint_manager2 to PP (which must support %E for trees).  */
+
+void
+constraint_manager2::print (pretty_printer *pp) const
+{
+  pp_string (pp, "{");
+  int i;
+  equiv_class2 *ec;
+  FOR_EACH_VEC_ELT (m_equiv_class2es, i, ec)
+    {
+      if (i > 0)
+	pp_string (pp, ", ");
+      equiv_class2_id (i).print (pp);
+      pp_string (pp, ": ");
+      ec->print (pp);
+    }
+  pp_string (pp, "  |  ");
+  constraint2 *c;
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    {
+      if (i > 0)
+	pp_string (pp, " && ");
+      c->print (pp, *this);
+    }
+  pp_printf (pp, "}");
+}
+
+/* Dump a multiline representation of this constraint_manager2 to PP
+   (which must support %E for trees).  */
+
+void
+constraint_manager2::dump_to_pp (pretty_printer *pp) const
+{
+  // TODO
+  pp_string (pp, "  equiv classes:");
+  pp_newline (pp);
+  int i;
+  equiv_class2 *ec;
+  FOR_EACH_VEC_ELT (m_equiv_class2es, i, ec)
+    {
+      pp_string (pp, "    ");
+      equiv_class2_id (i).print (pp);
+      pp_string (pp, ": ");
+      ec->print (pp);
+      pp_newline (pp);
+    }
+  pp_string (pp, "  constraints:");
+  pp_newline (pp);
+  constraint2 *c;
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    {
+      pp_printf (pp, "    %i: ", i);
+      c->print (pp, *this);
+      pp_newline (pp);
+    }
+}
+
+/* Dump a multiline representation of this constraint_manager2 to FP.  */
+
+void
+constraint_manager2::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);
+}
+
+/* Dump a multiline representation of this constraint_manager2 to stderr.  */
+
+DEBUG_FUNCTION void
+constraint_manager2::dump () const
+{
+  dump (stderr);
+}
+
+/* Dump a multiline representation of CM to stderr.  */
+
+DEBUG_FUNCTION void
+debug (const constraint_manager2 &cm)
+{
+  cm.dump ();
+}
+
+/* Attempt to add the constraint LHS OP RHS to this constraint_manager2.
+   Return true if the constraint could be added (or is already true).
+   Return false if the constraint contradicts existing knowledge.  */
+
+bool
+constraint_manager2::add_constraint (svalue2 * lhs,
+				     enum tree_code op,
+				     svalue2 * rhs)
+{
+  equiv_class2_id lhs_ec_id = get_or_add_equiv_class2 (lhs);
+  equiv_class2_id rhs_ec_id = get_or_add_equiv_class2 (rhs);
+  return add_constraint (lhs_ec_id, op,rhs_ec_id);
+}
+
+/* Attempt to add the constraint LHS_EC_ID OP RHS_EC_ID to this
+   constraint_manager2.
+   Return true if the constraint could be added (or is already true).
+   Return false if the constraint contradicts existing knowledge.  */
+
+bool
+constraint_manager2::add_constraint (equiv_class2_id lhs_ec_id,
+				    enum tree_code op,
+				    equiv_class2_id rhs_ec_id)
+{
+  tristate t = eval_condition (lhs_ec_id, op, rhs_ec_id);
+
+  /* Discard constraints that are already known.  */
+  if (t.is_true ())
+    return true;
+
+  /* Reject unsatisfiable constraints.  */
+  if (t.is_false ())
+    return false;
+
+  gcc_assert (lhs_ec_id != rhs_ec_id);
+
+  /* For now, simply accumulate constraints, without attempting any further
+     optimization.  */
+  switch (op)
+    {
+    case EQ_EXPR:
+      {
+	/* Merge rhs_ec into lhs_ec.  */
+	equiv_class2 &lhs_ec_obj = lhs_ec_id.get_obj (*this);
+	const equiv_class2 &rhs_ec_obj = rhs_ec_id.get_obj (*this);
+
+	int i;
+	svalue2 *sval;
+	FOR_EACH_VEC_ELT (rhs_ec_obj.m_vars, i, sval)
+	  lhs_ec_obj.add (sval);
+
+	if (rhs_ec_obj.m_constant)
+	  {
+	    lhs_ec_obj.m_constant = rhs_ec_obj.m_constant;
+	    lhs_ec_obj.m_cst_sval = rhs_ec_obj.m_cst_sval;
+	  }
+
+	/* Drop rhs equivalence class, overwriting it with the
+	   final ec (which might be the same one).  */
+	equiv_class2_id final_ec_id = m_equiv_class2es.length () - 1;
+	equiv_class2 *old_ec = m_equiv_class2es[rhs_ec_id.m_idx];
+	equiv_class2 *final_ec = m_equiv_class2es.pop ();
+	if (final_ec != old_ec)
+	  m_equiv_class2es[rhs_ec_id.m_idx] = final_ec;
+	delete old_ec;
+
+	/* Update the constraints.  */
+	constraint2 *c;
+	FOR_EACH_VEC_ELT (m_constraints, i, c)
+	  {
+	    /* Update references to the rhs_ec so that
+	       they refer to the lhs_ec.  */
+	    if (c->m_lhs == rhs_ec_id)
+	      c->m_lhs = lhs_ec_id;
+	    if (c->m_rhs == rhs_ec_id)
+	      c->m_rhs = lhs_ec_id;
+
+	    /* Renumber all constraints that refer to the final rhs_ec
+	       to the old rhs_ec, where the old final_ec now lives.  */
+	    if (c->m_lhs == final_ec_id)
+	      c->m_lhs = rhs_ec_id;
+	    if (c->m_rhs == final_ec_id)
+	      c->m_rhs = rhs_ec_id;
+	  }
+      }
+      break;
+    case GE_EXPR:
+      add_constraint_internal (rhs_ec_id, CONSTRAINT_LE, lhs_ec_id);
+      break;
+    case LE_EXPR:
+      add_constraint_internal (lhs_ec_id, CONSTRAINT_LE, rhs_ec_id);
+      break;
+    case NE_EXPR:
+      add_constraint_internal (lhs_ec_id, CONSTRAINT_NE, rhs_ec_id);
+      break;
+    case GT_EXPR:
+      add_constraint_internal (rhs_ec_id, CONSTRAINT_LT, lhs_ec_id);
+      break;
+    case LT_EXPR:
+      add_constraint_internal (lhs_ec_id, CONSTRAINT_LT, rhs_ec_id);
+      break;
+    default:
+      /* do nothing.  */
+      break;
+    }
+  validate ();
+  return true;
+}
+
+/* Subroutine of constraint_manager2::add_constraint, for handling all
+   operations other than equality (for which equiv classes are merged).  */
+
+void
+constraint_manager2::add_constraint_internal (equiv_class2_id lhs_id,
+					     enum constraint_op c_op,
+					     equiv_class2_id rhs_id)
+{
+  /* Add the constraint.  */
+  m_constraints.safe_push (constraint2 (lhs_id, c_op, rhs_id));
+
+  if (!flag_analyzer_transitivity)
+    return;
+
+  if (c_op != CONSTRAINT_NE)
+    {
+      /* 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 representatives.  */
+      svalue2 * lhs = lhs_id.get_obj (*this).get_representative ();
+      svalue2 * rhs = rhs_id.get_obj (*this).get_representative ();
+
+      /* We have LHS </<= RHS */
+
+      /* Handle transitivity of ordering by adding additional constraints
+	 based on what we already knew.
+
+	 So if we have already have:
+	   (a < b)
+	   (c < d)
+	 Then adding:
+	   (b < c)
+	 will also add:
+	   (a < c)
+	   (b < d)
+	 We need to recurse to ensure we also add:
+	   (a < d).
+	 We call the checked add_constraint to avoid adding constraints
+	 that are already present.  Doing so also ensures termination
+	 in the case of cycles.
+
+	 We also check for single-element ranges, adding EQ_EXPR facts
+	 where we discover them.  For example 3 < x < 5 implies
+	 that x == 4 (if x is an integer).  */
+      for (unsigned i = 0; i < m_constraints.length (); i++)
+	{
+	  const constraint2 *other = &m_constraints[i];
+	  if (other->is_ordering_p ())
+	    {
+	      /* Refresh the EC IDs, in case any mergers have happened.  */
+	      lhs_id = get_or_add_equiv_class2 (lhs);
+	      rhs_id = get_or_add_equiv_class2 (rhs);
+
+	      tree lhs_const = lhs_id.get_obj (*this).m_constant;
+	      tree rhs_const = rhs_id.get_obj (*this).m_constant;
+	      tree other_lhs_const
+		= other->m_lhs.get_obj (*this).m_constant;
+	      tree other_rhs_const
+		= other->m_rhs.get_obj (*this).m_constant;
+
+	      /* We have "LHS </<= RHS" and "other.lhs </<= other.rhs".  */
+
+	      /* If we have LHS </<= RHS and RHS </<= LHS, then we have a
+		 cycle.  */
+	      if (rhs_id == other->m_lhs
+		  && other->m_rhs == lhs_id)
+		{
+		  /* We must have equality for this to be possible.  */
+		  gcc_assert (c_op == CONSTRAINT_LE
+			      && other->m_op == CONSTRAINT_LE);
+		  add_constraint (lhs_id, EQ_EXPR, rhs_id);
+		  /* Adding an equality will merge the two ECs and potentially
+		     reorganize the constraints.  Stop iterating.  */
+		  return;
+		}
+	      /* Otherwise, check for transitivity.  */
+	      if (rhs_id == other->m_lhs)
+		{
+		  /* With RHS == other.lhs, we have:
+		     "LHS </<= (RHS, other.lhs) </<= other.rhs"
+		     and thus this implies "LHS </<= other.rhs".  */
+
+		  /* Do we have a tightly-constrained range?  */
+		  if (lhs_const
+		      && !rhs_const
+		      && other_rhs_const)
+		    {
+		      range2 r (bound2 (lhs_const, c_op == CONSTRAINT_LE),
+			       bound2 (other_rhs_const,
+				      other->m_op == CONSTRAINT_LE));
+		      tree constant;
+		      if (r.constrained_to_single_element (&constant))
+			{
+			  svalue2 * cst_sval
+			    = m_mgr->get_or_create_constant_svalue2 (constant);
+			  add_constraint
+			    (rhs_id, EQ_EXPR,
+			     get_or_add_equiv_class2 (cst_sval));
+			  return;
+			}
+		    }
+
+		  /* Otherwise, add the constraint implied by transitivity.  */
+		  enum tree_code new_op
+		    = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
+		       ? LE_EXPR : LT_EXPR);
+		  add_constraint (lhs_id, new_op, other->m_rhs);
+		}
+	      else if (other->m_rhs == lhs_id)
+		{
+		  /* With other.rhs == LHS, we have:
+		     "other.lhs </<= (other.rhs, LHS) </<= RHS"
+		     and thus this implies "other.lhs </<= RHS".  */
+
+		  /* Do we have a tightly-constrained range?  */
+		  if (other_lhs_const
+		      && !lhs_const
+		      && rhs_const)
+		    {
+		      range2 r (bound2 (other_lhs_const,
+				      other->m_op == CONSTRAINT_LE),
+			       bound2 (rhs_const,
+				      c_op == CONSTRAINT_LE));
+		      tree constant;
+		      if (r.constrained_to_single_element (&constant))
+			{
+			  svalue2 * cst_sval
+			    = m_mgr->get_or_create_constant_svalue2 (constant);
+			  add_constraint
+			    (lhs_id, EQ_EXPR,
+			     get_or_add_equiv_class2 (cst_sval));
+			  return;
+			}
+		    }
+
+		  /* Otherwise, add the constraint implied by transitivity.  */
+		  enum tree_code new_op
+		    = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
+		       ? LE_EXPR : LT_EXPR);
+		  add_constraint (other->m_lhs, new_op, rhs_id);
+		}
+	    }
+	}
+    }
+}
+
+/* Look for SVAL within the equivalence classes of this constraint_manager2;
+   if found, write the id to *OUT and return true, otherwise return false.  */
+
+bool
+constraint_manager2::get_equiv_class2_by_svalue2 (svalue2 *sval,
+						  equiv_class2_id *out) const
+{
+  /* TODO: should we have a map, rather than these searches?  */
+  int i;
+  equiv_class2 *ec;
+  FOR_EACH_VEC_ELT (m_equiv_class2es, i, ec)
+    {
+      int j;
+      svalue2 *iv;
+      FOR_EACH_VEC_ELT (ec->m_vars, j, iv)
+	if (iv == sval)
+	  {
+	    *out = equiv_class2_id (i);
+	    return true;
+	  }
+    }
+  return false;
+}
+
+/* Ensure that SVAL has an equivalence class within this constraint_manager2;
+   return the ID of the class.  */
+
+equiv_class2_id
+constraint_manager2::get_or_add_equiv_class2 (svalue2 *sval)
+{
+  equiv_class2_id result (-1);
+
+  /* Try svalue2 match.  */
+  if (get_equiv_class2_by_svalue2 (sval, &result))
+    return result;
+
+  /* Try equality of constants.  */
+  if (tree cst = sval->maybe_get_constant ())
+    {
+      int i;
+      equiv_class2 *ec;
+      FOR_EACH_VEC_ELT (m_equiv_class2es, i, ec)
+	if (ec->m_constant
+	    && types_compatible_p (TREE_TYPE (cst),
+				   TREE_TYPE (ec->m_constant)))
+	  {
+	    tree eq = fold_binary (EQ_EXPR, boolean_type_node,
+				   cst, ec->m_constant);
+	    if (eq == boolean_true_node)
+	      {
+		ec->add (sval);
+		return equiv_class2_id (i);
+	      }
+	  }
+    }
+
+
+  /* Not found.  */
+  equiv_class2 *new_ec = new equiv_class2 ();
+  new_ec->add (sval);
+  m_equiv_class2es.safe_push (new_ec);
+
+  equiv_class2_id new_id (m_equiv_class2es.length () - 1);
+
+  if (sval->maybe_get_constant ())
+    {
+      /* If we have a new EC for a constant, add constraints comparing this
+	 to other constants we may have (so that we accumulate the transitive
+	 closure of all constraints on constants as the constants are
+	 added).  */
+      for (equiv_class2_id other_id (0); other_id.m_idx < new_id.m_idx;
+	   other_id.m_idx++)
+	{
+	  const equiv_class2 &other_ec = other_id.get_obj (*this);
+	  if (other_ec.m_constant
+	      && types_compatible_p (TREE_TYPE (new_ec->m_constant),
+				     TREE_TYPE (other_ec.m_constant)))
+	    {
+	      /* If we have two ECs, both with constants, the constants must be
+		 non-equal (or they would be in the same EC).
+		 Determine the direction of the inequality, and record that
+		 fact.  */
+	      tree lt
+		= fold_binary (LT_EXPR, boolean_type_node,
+			       new_ec->m_constant, other_ec.m_constant);
+	      if (lt == boolean_true_node)
+		add_constraint_internal (new_id, CONSTRAINT_LT, other_id);
+	      else if (lt == boolean_false_node)
+		add_constraint_internal (other_id, CONSTRAINT_LT, new_id);
+	      /* Refresh new_id, in case ECs were merged.  SVAL should always
+		 be present by now, so this should never lead to a
+		 recursion.  */
+	      new_id = get_or_add_equiv_class2 (sval);
+	    }
+	}
+    }
+
+  return new_id;
+}
+
+/* Evaluate the condition LHS_EC OP RHS_EC.  */
+
+tristate
+constraint_manager2::eval_condition (equiv_class2_id lhs_ec,
+				    enum tree_code op,
+				    equiv_class2_id rhs_ec)
+{
+  if (lhs_ec == rhs_ec)
+    {
+      switch (op)
+	{
+	case EQ_EXPR:
+	case GE_EXPR:
+	case LE_EXPR:
+	  return tristate (tristate::TS_TRUE);
+
+	case NE_EXPR:
+	case GT_EXPR:
+	case LT_EXPR:
+	  return tristate (tristate::TS_FALSE);
+	default:
+	  break;
+	}
+    }
+
+  tree lhs_const = lhs_ec.get_obj (*this).get_any_constant ();
+  tree rhs_const = rhs_ec.get_obj (*this).get_any_constant ();
+  if (lhs_const && rhs_const)
+    {
+      tree comparison
+	= fold_binary (op, boolean_type_node, lhs_const, rhs_const);
+      if (comparison == boolean_true_node)
+	return tristate (tristate::TS_TRUE);
+      if (comparison == boolean_false_node)
+	return tristate (tristate::TS_FALSE);
+    }
+
+  enum tree_code swapped_op = swap_tree_comparison (op);
+
+  int i;
+  constraint2 *c;
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    {
+      if (c->m_lhs == lhs_ec
+	  && c->m_rhs == rhs_ec)
+	{
+	  tristate result_for_constraint
+	    = eval_constraint_op_for_op (c->m_op, op);
+	  if (result_for_constraint.is_known ())
+	    return result_for_constraint;
+	}
+      /* Swapped operands.  */
+      if (c->m_lhs == rhs_ec
+	  && c->m_rhs == lhs_ec)
+	{
+	  tristate result_for_constraint
+	    = eval_constraint_op_for_op (c->m_op, swapped_op);
+	  if (result_for_constraint.is_known ())
+	    return result_for_constraint;
+	}
+    }
+
+  return tristate (tristate::TS_UNKNOWN);
+}
+
+/* Evaluate the condition LHS OP RHS, creating equiv_class2 instances for
+   LHS and RHS if they aren't already in equiv_class2es.  */
+
+tristate
+constraint_manager2::eval_condition (svalue2 *lhs,
+				     enum tree_code op,
+				     svalue2 *rhs)
+{
+  return eval_condition (get_or_add_equiv_class2 (lhs),
+			 op,
+			 get_or_add_equiv_class2 (rhs));
+}
+
+/* Delete any information about svalue2_id instances identified by P.
+   Such instances are removed from equivalence classes, and any
+   redundant ECs and constraints are also removed.
+   Accumulate stats into STATS.  */
+
+void
+constraint_manager2::purge (const purge_criteria &p, purge_stats2 *stats)
+{
+  /* Delete any svalue2_ids identified by P within the various equivalence
+     classes.  */
+  for (unsigned ec_idx = 0; ec_idx < m_equiv_class2es.length (); )
+    {
+      equiv_class2 *ec = m_equiv_class2es[ec_idx];
+
+      int i;
+      svalue2 *pv;
+      bool delete_ec = false;
+      FOR_EACH_VEC_ELT (ec->m_vars, i, pv)
+	{
+	  if (pv == ec->m_cst_sval)
+	    continue;
+	  if (p.should_purge_p (pv))
+	    {
+	      if (ec->del (pv))
+		if (!ec->m_constant)
+		  delete_ec = true;
+	    }
+	}
+
+      if (delete_ec)
+	{
+	  delete ec;
+	  m_equiv_class2es.ordered_remove (ec_idx);
+	  if (stats)
+	    stats->m_num_equiv_classes++;
+
+	  /* Update the constraints, potentially removing some.  */
+	  for (unsigned con_idx = 0; con_idx < m_constraints.length (); )
+	    {
+	      constraint2 *c = &m_constraints[con_idx];
+
+	      /* Remove constraints that refer to the deleted EC.  */
+	      if (c->m_lhs == ec_idx
+		  || c->m_rhs == ec_idx)
+		{
+		  m_constraints.ordered_remove (con_idx);
+		  if (stats)
+		    stats->m_num_constraints++;
+		}
+	      else
+		{
+		  /* Renumber constraints that refer to ECs that have
+		     had their idx changed.  */
+		  c->m_lhs.update_for_removal (ec_idx);
+		  c->m_rhs.update_for_removal (ec_idx);
+
+		  con_idx++;
+		}
+	    }
+	}
+      else
+	ec_idx++;
+    }
+
+  /* Now delete any constraints that are purely between constants.  */
+  for (unsigned con_idx = 0; con_idx < m_constraints.length (); )
+    {
+      constraint2 *c = &m_constraints[con_idx];
+      if (m_equiv_class2es[c->m_lhs.m_idx]->m_vars.length () == 0
+	  && m_equiv_class2es[c->m_rhs.m_idx]->m_vars.length () == 0)
+	{
+	  m_constraints.ordered_remove (con_idx);
+	  if (stats)
+	    stats->m_num_constraints++;
+	}
+      else
+	{
+	  con_idx++;
+	}
+    }
+
+  /* Finally, delete any ECs that purely contain constants and aren't
+     referenced by any constraints.  */
+  for (unsigned ec_idx = 0; ec_idx < m_equiv_class2es.length (); )
+    {
+      equiv_class2 *ec = m_equiv_class2es[ec_idx];
+      if (ec->m_vars.length () == 0)
+	{
+	  equiv_class2_id ec_id (ec_idx);
+	  bool has_constraint = false;
+	  for (unsigned con_idx = 0; con_idx < m_constraints.length ();
+	       con_idx++)
+	    {
+	      constraint2 *c = &m_constraints[con_idx];
+	      if (c->m_lhs == ec_id
+		  || c->m_rhs == ec_id)
+		{
+		  has_constraint = true;
+		  break;
+		}
+	    }
+	  if (!has_constraint)
+	    {
+	      delete ec;
+	      m_equiv_class2es.ordered_remove (ec_idx);
+	      if (stats)
+		stats->m_num_equiv_classes++;
+
+	      /* Renumber constraints that refer to ECs that have
+		 had their idx changed.  */
+	      for (unsigned con_idx = 0; con_idx < m_constraints.length ();
+		   con_idx++)
+		{
+		  constraint2 *c = &m_constraints[con_idx];
+		  c->m_lhs.update_for_removal (ec_idx);
+		  c->m_rhs.update_for_removal (ec_idx);
+		}
+	      continue;
+	    }
+	}
+      ec_idx++;
+    }
+
+  validate ();
+}
+
+/* Comparator for use by constraint_manager2::canonicalize.
+   Sort a pair of equiv_class2 instances, using the representative
+   svalue2_id as a sort key.  */
+
+static int
+equiv_class2_cmp (const void *p1, const void *p2)
+{
+  gcc_unreachable ();
+#if 0
+  const equiv_class2 *ec1 = *(const equiv_class2 * const *)p1;
+  const equiv_class2 *ec2 = *(const equiv_class2 * const *)p2;
+
+  svalue2_id rep1 = ec1->get_representative ();
+  svalue2_id rep2 = ec2->get_representative ();
+
+  return rep1.as_int () - rep2.as_int ();
+#endif
+}
+
+/* Comparator for use by constraint_manager2::canonicalize.
+   Sort a pair of constraint instances.  */
+
+static int
+constraint_cmp (const void *p1, const void *p2)
+{
+  const constraint2 *c1 = (const constraint2 *)p1;
+  const constraint2 *c2 = (const constraint2 *)p2;
+  int lhs_cmp = c1->m_lhs.as_int () - c2->m_lhs.as_int ();
+  if (lhs_cmp)
+    return lhs_cmp;
+  int rhs_cmp = c1->m_rhs.as_int () - c2->m_rhs.as_int ();
+  if (rhs_cmp)
+    return rhs_cmp;
+  return c1->m_op - c2->m_op;
+}
+
+/* Reorder the equivalence classes and constraints within this
+   constraint_manager2 into a canonical order, to increase the
+   chances of finding equality with another instance.  */
+#if 0
+void
+constraint_manager2::canonicalize (unsigned num_svalue2_ids)
+{
+  gcc_unreachable ();
+#if 0
+  /* First, sort svalue2_ids within the ECs.  */
+  unsigned i;
+  equiv_class2 *ec;
+  FOR_EACH_VEC_ELT (m_equiv_class2es, i, ec)
+    ec->canonicalize ();
+
+  /* Next, sort the ECs into a canonical order.  */
+
+  /* We will need to remap the equiv_class2_ids in the constraints,
+     so we need to store the original index of each EC.
+     Build a lookup table, mapping from representative svalue2_id
+     to the original equiv_class2_id of that svalue2_id.  */
+  auto_vec<equiv_class2_id> original_ec_id (num_svalue2_ids);
+  for (i = 0; i < num_svalue2_ids; i++)
+    original_ec_id.quick_push (equiv_class2_id::null ());
+  FOR_EACH_VEC_ELT (m_equiv_class2es, i, ec)
+    {
+      svalue2_id rep = ec->get_representative ();
+      gcc_assert (!rep.null_p ());
+      original_ec_id[rep.as_int ()] = i;
+    }
+
+  /* Sort the equivalence classes.  */
+  m_equiv_class2es.qsort (equiv_class2_cmp);
+
+  /* Populate ec_id_map based on the old vs new EC ids.  */
+  one_way_id_map<equiv_class2_id> ec_id_map (m_equiv_class2es.length ());
+  FOR_EACH_VEC_ELT (m_equiv_class2es, i, ec)
+    {
+      svalue2_id rep = ec->get_representative ();
+      ec_id_map.put (original_ec_id[rep.as_int ()], i);
+    }
+
+  /* Update the EC ids within the constraints.  */
+  constraint2 *c;
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    {
+      ec_id_map.update (&c->m_lhs);
+      ec_id_map.update (&c->m_rhs);
+    }
+
+  /* Finally, sort the constraints. */
+  m_constraints.qsort (constraint_cmp);
+#endif
+}
+#endif
+
+/* A concrete subclass of constraint_manager2 for use when
+   merging two constraint_manager2 into a third constraint_manager2,
+   each of which has its own region_model2.
+   Calls are delegated to the constraint_manager2 for the merged model,
+   and thus affect its region_model2.  */
+#if 0
+class cleaned_constraint_manager2 : public constraint_manager2
+{
+public:
+  cleaned_constraint_manager2 (constraint_manager2 *merged)
+  : constraint_manager2 (merged->m_mgr),
+    m_merged (merged) {}
+
+#if 0
+  constraint_manager2 *clone (region_model2 *) const FINAL OVERRIDE
+  {
+    gcc_unreachable ();
+  }
+#endif
+private:
+  constraint_manager2 *m_merged;
+};
+#endif
+/* Concrete subclass of fact_visitor for use by constraint_manager2::merge.
+   For every fact in CM_A, see if it is also true in *CM_B.  Add such
+   facts to *OUT.  */
+
+class merger_fact_visitor : public fact_visitor
+{
+public:
+  merger_fact_visitor (constraint_manager2 *cm_b,
+		       constraint_manager2 *out)
+  : m_cm_b (cm_b), m_out (out)
+  {}
+
+  void on_fact (svalue2 *lhs, enum tree_code code, svalue2 *rhs)
+    FINAL OVERRIDE
+  {
+    if (m_cm_b->eval_condition (lhs, code, rhs).is_true ())
+      {
+	bool sat = m_out->add_constraint (lhs, code, rhs);
+	gcc_assert (sat);
+      }
+  }
+
+private:
+  constraint_manager2 *m_cm_b;
+  constraint_manager2 *m_out;
+};
+
+/* Use MERGER to merge CM_A and CM_B into *OUT.
+   If one thinks of a constraint_manager2 as a subset of N-dimensional
+   space, this takes the union of the points of CM_A and CM_B, and
+   expresses that into *OUT.  Alternatively, it can be thought of
+   as the intersection of the constraints.  */
+#if 0
+void
+constraint_manager2::merge (const constraint_manager2 &cm_a,
+			   const constraint_manager2 &cm_b,
+			   constraint_manager2 *out,
+			   const model_merger &merger)
+{
+  gcc_assert (merger.m_sval_mapping);
+
+  /* Map svalue2_ids in each equiv class from both sources
+     to the merged region_model2, dropping ids that don't survive merger,
+     and potentially creating svalue2s in *OUT for constants.  */
+  cleaned_constraint_manager2 cleaned_cm_a (out);
+  const one_way_svalue2_id_map &map_a_to_m
+    = merger.m_sval_mapping->m_map_from_a_to_m;
+  clean_merger_input (cm_a, map_a_to_m, &cleaned_cm_a);
+
+  cleaned_constraint_manager2 cleaned_cm_b (out);
+  const one_way_svalue2_id_map &map_b_to_m
+    = merger.m_sval_mapping->m_map_from_b_to_m;
+  clean_merger_input (cm_b, map_b_to_m, &cleaned_cm_b);
+
+  /* At this point, the two cleaned CMs have ECs and constraints referring
+     to svalue2s in the merged region model, but both of them have separate
+     ECs.  */
+
+  /* Merge the equivalence classes and constraints.
+     The easiest way to do this seems to be to enumerate all of the facts
+     in cleaned_cm_a, see which are also true in cleaned_cm_b,
+     and add those to *OUT.  */
+  merger_fact_visitor v (&cleaned_cm_b, out);
+  cleaned_cm_a.for_each_fact (&v);
+}
+#endif
+
+/* A subroutine of constraint_manager2::merge.
+   Use MAP_SVAL_TO_M to map equivalence classes and constraints from
+   SM_IN to *OUT.  Purge any non-constant svalue2 *that don't appear
+   in the result of MAP_SVAL_TO_M, purging any ECs and their constraints
+   that become empty as a result.  Potentially create svalue2s in
+   the merged region_model2 for constants that weren't already in use there.  */
+#if 0
+void
+constraint_manager2::
+clean_merger_input (const constraint_manager2 &cm_in,
+		    const one_way_svalue2_id_map &map_sval_to_m,
+		    constraint_manager2 *out)
+{
+  one_way_id_map<equiv_class2_id> map_ec_to_m
+    (cm_in.m_equiv_class2es.length ());
+  unsigned ec_idx;
+  equiv_class2 *ec;
+  FOR_EACH_VEC_ELT (cm_in.m_equiv_class2es, ec_idx, ec)
+    {
+      equiv_class2 cleaned_ec;
+      if (tree cst = ec->get_any_constant ())
+	{
+	  cleaned_ec.m_constant = cst;
+	  /* Lazily create the constant in the out region_model2.  */
+	  cleaned_ec.m_cst_sval = out->get_sval_for_constant (cst);
+	}
+      unsigned var_idx;
+      svalue2 **var_in_sval;
+      FOR_EACH_VEC_ELT (ec->m_vars, var_idx, var_in_sval)
+	{
+	  svalue2 *var_m_sval = map_sval_to_m.get_dst_for_src (*var_in_sval);
+	  if (!var_m_sval.null_p ())
+	    cleaned_ec.m_vars.safe_push (var_m_sval);
+	}
+      if (cleaned_ec.get_any_constant () || !cleaned_ec.m_vars.is_empty ())
+	{
+	  map_ec_to_m.put (ec_idx, out->m_equiv_class2es.length ());
+	  out->m_equiv_class2es.safe_push (new equiv_class2 (cleaned_ec));
+	}
+    }
+
+  /* Write out to *OUT any constraints for which both svales survived
+     cleaning, using the new EC IDs.  */
+  unsigned con_idx;
+  constraint2 *c;
+  FOR_EACH_VEC_ELT (cm_in.m_constraints, con_idx, c)
+    {
+      equiv_class2_id new_lhs = map_ec_to_m.get_dst_for_src (c->m_lhs);
+      if (new_lhs.null_p ())
+	continue;
+      equiv_class2_id new_rhs = map_ec_to_m.get_dst_for_src (c->m_rhs);
+      if (new_rhs.null_p ())
+	continue;
+      out->m_constraints.safe_push (constraint (new_lhs,
+						c->m_op,
+						new_rhs));
+    }
+}
+#endif
+/* Call VISITOR's on_fact vfunc repeatedly to express the various
+   equivalence classes and constraints.
+   This is used by constraint_manager2::merge to find the common
+   facts between two input constraint_manager2s.  */
+
+void
+constraint_manager2::for_each_fact (fact_visitor *visitor) const
+{
+  /* First, call EQ_EXPR within the various equivalence classes.  */
+  unsigned ec_idx;
+  equiv_class2 *ec;
+  FOR_EACH_VEC_ELT (m_equiv_class2es, ec_idx, ec)
+    {
+      if (ec->m_cst_sval)
+	{
+	  unsigned i;
+	  svalue2 *sval;
+	  FOR_EACH_VEC_ELT (ec->m_vars, i, sval)
+	    visitor->on_fact (ec->m_cst_sval, EQ_EXPR, sval);
+	}
+      for (unsigned i = 0; i < ec->m_vars.length (); i++)
+	for (unsigned j = i + 1; j < ec->m_vars.length (); j++)
+	  visitor->on_fact (ec->m_vars[i], EQ_EXPR, ec->m_vars[j]);
+    }
+
+  /* Now, express the various constraints.  */
+  unsigned con_idx;
+  constraint2 *c;
+  FOR_EACH_VEC_ELT (m_constraints, con_idx, c)
+    {
+      const equiv_class2 &ec_lhs = c->m_lhs.get_obj (*this);
+      const equiv_class2 &ec_rhs = c->m_rhs.get_obj (*this);
+      enum tree_code code = constraint_tree_code2 (c->m_op);
+
+      if (ec_lhs.m_cst_sval)
+	{
+	  for (unsigned j = 0; j < ec_rhs.m_vars.length (); j++)
+	    {
+	      visitor->on_fact (ec_lhs.m_cst_sval, code, ec_rhs.m_vars[j]);
+	    }
+	}
+      for (unsigned i = 0; i < ec_lhs.m_vars.length (); i++)
+	{
+	  if (ec_rhs.m_cst_sval)
+	    visitor->on_fact (ec_lhs.m_vars[i], code, ec_rhs.m_cst_sval);
+	  for (unsigned j = 0; j < ec_rhs.m_vars.length (); j++)
+	    visitor->on_fact (ec_lhs.m_vars[i], code, ec_rhs.m_vars[j]);
+	}
+    }
+}
+
+/* Assert that this object is valid.  */
+
+void
+constraint_manager2::validate () const
+{
+  /* Skip this in a release build.  */
+#if !CHECKING_P
+  return;
+#endif
+
+  int i;
+  equiv_class2 *ec;
+  FOR_EACH_VEC_ELT (m_equiv_class2es, i, ec)
+    {
+      gcc_assert (ec);
+
+      int j;
+      svalue2 *sval;
+      FOR_EACH_VEC_ELT (ec->m_vars, j, sval)
+	gcc_assert (sval);
+      if (ec->m_constant)
+	{
+	  gcc_assert (CONSTANT_CLASS_P (ec->m_constant));
+	  gcc_assert (ec->m_cst_sval);
+	}
+#if 0
+      else
+	gcc_assert (ec->m_vars.length () > 0);
+#endif
+    }
+
+  constraint2 *c;
+  FOR_EACH_VEC_ELT (m_constraints, i, c)
+    {
+      gcc_assert (!c->m_lhs.null_p ());
+      gcc_assert (c->m_lhs.as_int () <= (int)m_equiv_class2es.length ());
+      gcc_assert (!c->m_rhs.null_p ());
+      gcc_assert (c->m_rhs.as_int () <= (int)m_equiv_class2es.length ());
+    }
+}
+
+#if CHECKING_P
+
+namespace selftest {
+
+/* Various constraint_manager2 selftests.
+   These have to be written in terms of a region_model2, since
+   the latter is responsible for managing svalue2 and svalue2_id
+   instances.  */
+
+/* Verify that setting and getting simple conditions within a region_model2
+   work (thus exercising the underlying constraint_manager2).  */
+
+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_global_decl ("x", integer_type_node);
+  tree y = build_global_decl ("y", integer_type_node);
+  tree z = build_global_decl ("z", integer_type_node);
+
+  /* Self-comparisons.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ASSERT_CONDITION_TRUE2 (model, x, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, x, LE_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, x, GE_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, x, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, x, LT_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, x, GT_EXPR, x);
+  }
+
+  /* x == y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, EQ_EXPR, y);
+
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
+
+    ASSERT_CONDITION_TRUE2 (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_TRUE2 (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_TRUE2 (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, GT_EXPR, y);
+
+    /* Swapped operands.  */
+    ASSERT_CONDITION_TRUE2 (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, y, GT_EXPR, x);
+
+    /* Comparison with other var.  */
+    ASSERT_CONDITION_UNKNOWN2 (model, x, EQ_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, LE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, NE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, LT_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GT_EXPR, z);
+  }
+
+  /* x == y, then y == z  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, EQ_EXPR, y);
+
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
+    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, z);
+
+    ASSERT_CONDITION_TRUE2 (model, x, EQ_EXPR, z);
+    ASSERT_CONDITION_TRUE2 (model, x, LE_EXPR, z);
+    ASSERT_CONDITION_TRUE2 (model, x, GE_EXPR, z);
+    ASSERT_CONDITION_FALSE2 (model, x, NE_EXPR, z);
+    ASSERT_CONDITION_FALSE2 (model, x, LT_EXPR, z);
+    ASSERT_CONDITION_FALSE2 (model, x, GT_EXPR, z);
+  }
+
+  /* x != y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+
+    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
+
+    ASSERT_CONDITION_TRUE2 (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GT_EXPR, y);
+
+    /* Swapped operands.  */
+    ASSERT_CONDITION_TRUE2 (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, GT_EXPR, x);
+
+    /* Comparison with other var.  */
+    ASSERT_CONDITION_UNKNOWN2 (model, x, EQ_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, LE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, NE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, LT_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GT_EXPR, z);
+  }
+
+  /* x < y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+
+    ADD_SAT_CONSTRAINT (model, x, LT_EXPR, y);
+
+    ASSERT_CONDITION_TRUE2 (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_TRUE2 (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_TRUE2 (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, GE_EXPR, y);
+
+    /* Swapped operands.  */
+    ASSERT_CONDITION_FALSE2 (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, y, GE_EXPR, x);
+  }
+
+  /* x <= y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+
+    ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
+
+    ASSERT_CONDITION_UNKNOWN2 (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_TRUE2 (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GE_EXPR, y);
+
+    /* Swapped operands.  */
+    ASSERT_CONDITION_FALSE2 (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, LE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, y, GE_EXPR, x);
+  }
+
+  /* x > y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+
+    ADD_SAT_CONSTRAINT (model, x, GT_EXPR, y);
+
+    ASSERT_CONDITION_TRUE2 (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_TRUE2 (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_TRUE2 (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, LE_EXPR, y);
+
+    /* Swapped operands.  */
+    ASSERT_CONDITION_FALSE2 (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_FALSE2 (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, y, LE_EXPR, x);
+  }
+
+  /* x >= y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+
+    ADD_SAT_CONSTRAINT (model, x, GE_EXPR, y);
+
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GT_EXPR, y);
+    ASSERT_CONDITION_TRUE2 (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, LE_EXPR, y);
+
+    /* Swapped operands.  */
+    ASSERT_CONDITION_FALSE2 (model, y, GT_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, GE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, NE_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, EQ_EXPR, x);
+    ASSERT_CONDITION_UNKNOWN2 (model, y, LT_EXPR, x);
+    ASSERT_CONDITION_TRUE2 (model, y, LE_EXPR, x);
+  }
+
+  // TODO: implied orderings
+
+  /* Constants.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ASSERT_CONDITION_FALSE2 (model, int_0, EQ_EXPR, int_42);
+    ASSERT_CONDITION_TRUE2 (model, int_0, NE_EXPR, int_42);
+    ASSERT_CONDITION_TRUE2 (model, int_0, LT_EXPR, int_42);
+    ASSERT_CONDITION_TRUE2 (model, int_0, LE_EXPR, int_42);
+    ASSERT_CONDITION_FALSE2 (model, int_0, GT_EXPR, int_42);
+    ASSERT_CONDITION_FALSE2 (model, int_0, GE_EXPR, int_42);
+  }
+
+  /* x == 0, y == 42.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, int_42);
+
+    ASSERT_CONDITION_TRUE2 (model, x, NE_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_TRUE2 (model, x, LE_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, GE_EXPR, y);
+    ASSERT_CONDITION_TRUE2 (model, x, LT_EXPR, y);
+    ASSERT_CONDITION_FALSE2 (model, x, GT_EXPR, y);
+  }
+
+  /* Unsatisfiable combinations.  */
+
+  /* x == y && x != y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
+    ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, y);
+  }
+
+  /* x == 0 then x == 42.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, int_42);
+  }
+
+  /* x == 0 then x != 0.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_UNSAT_CONSTRAINT (model, x, NE_EXPR, int_0);
+  }
+
+  /* x == 0 then x > 0.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, int_0);
+    ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, int_0);
+  }
+
+  /* x != y && x == y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, x, NE_EXPR, y);
+    ADD_UNSAT_CONSTRAINT (model, x, EQ_EXPR, y);
+  }
+
+  /* x <= y && x > y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, x, LE_EXPR, y);
+    ADD_UNSAT_CONSTRAINT (model, x, GT_EXPR, y);
+  }
+
+  // etc
+}
+
+/* Test transitivity of conditions.  */
+
+static void
+test_transitivity ()
+{
+  tree a = build_global_decl ("a", integer_type_node);
+  tree b = build_global_decl ("b", integer_type_node);
+  tree c = build_global_decl ("c", integer_type_node);
+  tree d = build_global_decl ("d", integer_type_node);
+
+  /* a == b, then c == d, then c == b.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ASSERT_CONDITION_UNKNOWN2 (model, a, EQ_EXPR, b);
+    ASSERT_CONDITION_UNKNOWN2 (model, b, EQ_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN2 (model, c, EQ_EXPR, d);
+    ASSERT_CONDITION_UNKNOWN2 (model, a, EQ_EXPR, d);
+
+    ADD_SAT_CONSTRAINT (model, a, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE2 (model, a, EQ_EXPR, b);
+
+    ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, d);
+    ASSERT_CONDITION_TRUE2 (model, c, EQ_EXPR, d);
+    ASSERT_CONDITION_UNKNOWN2 (model, a, EQ_EXPR, d);
+
+    ADD_SAT_CONSTRAINT (model, c, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE2 (model, c, EQ_EXPR, b);
+    ASSERT_CONDITION_TRUE2 (model, a, EQ_EXPR, d);
+  }
+
+  /* Transitivity: "a < b", "b < c" should imply "a < c".  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, LT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
+
+    ASSERT_CONDITION_TRUE2 (model, a, LT_EXPR, c);
+    ASSERT_CONDITION_FALSE2 (model, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "a <= b", "b < c" should imply "a < c".  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, LT_EXPR, c);
+
+    ASSERT_CONDITION_TRUE2 (model, a, LT_EXPR, c);
+    ASSERT_CONDITION_FALSE2 (model, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "a <= b", "b <= c" should imply "a <= c".  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, LE_EXPR, c);
+
+    ASSERT_CONDITION_TRUE2 (model, a, LE_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN2 (model, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "a > b", "b > c" should imply "a > c".  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
+
+    ASSERT_CONDITION_TRUE2 (model, a, GT_EXPR, c);
+    ASSERT_CONDITION_FALSE2 (model, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "a >= b", "b > c" should imply " a > c".  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
+
+    ASSERT_CONDITION_TRUE2 (model, a, GT_EXPR, c);
+    ASSERT_CONDITION_FALSE2 (model, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "a >= b", "b >= c" should imply "a >= c".  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, c);
+
+    ASSERT_CONDITION_TRUE2 (model, a, GE_EXPR, c);
+    ASSERT_CONDITION_UNKNOWN2 (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_model2_manager mgr;
+    region_model2 model (&mgr);
+    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_TRUE2 (model, a, LT_EXPR, c);
+    ASSERT_CONDITION_TRUE2 (model, b, LT_EXPR, d);
+    ASSERT_CONDITION_TRUE2 (model, a, LT_EXPR, d);
+  }
+
+  /* Transitivity: "a >= b", "b >= a" should imply that a == b.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GE_EXPR, a);
+
+    // TODO:
+    ASSERT_CONDITION_TRUE2 (model, a, EQ_EXPR, b);
+  }
+
+  /* Transitivity: "a >= b", "b > a" should be impossible.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    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_model2_manager mgr;
+    region_model2 model (&mgr);
+    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_TRUE2 (model, a, EQ_EXPR, c);
+  }
+
+  /* Transitivity: "a > b", "b > c", "c > a"
+     should be impossible.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, b);
+    ADD_SAT_CONSTRAINT (model, b, GT_EXPR, c);
+    ADD_UNSAT_CONSTRAINT (model, c, GT_EXPR, a);
+  }
+
+}
+
+/* Test various conditionals involving constants where the results
+   ought to be implied based on the values of the constants.  */
+
+static void
+test_constant_comparisons ()
+{
+  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);
+
+  tree int_1023 = build_int_cst (integer_type_node, 1023);
+  tree int_1024 = build_int_cst (integer_type_node, 1024);
+
+  tree a = build_global_decl ("a", integer_type_node);
+  tree b = build_global_decl ("b", integer_type_node);
+
+  /* Given a >= 1024, then a <= 1023 should be impossible.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_1024);
+    ADD_UNSAT_CONSTRAINT (model, a, LE_EXPR, int_1023);
+  }
+
+  /* a > 4.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_4);
+    ASSERT_CONDITION_TRUE2 (model, a, GT_EXPR, int_4);
+    ASSERT_CONDITION_TRUE2 (model, a, NE_EXPR, int_3);
+    ASSERT_CONDITION_UNKNOWN2 (model, a, NE_EXPR, int_5);
+  }
+
+  /* a <= 4.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+    ASSERT_CONDITION_FALSE2 (model, a, GT_EXPR, int_4);
+    ASSERT_CONDITION_FALSE2 (model, a, GT_EXPR, int_5);
+    ASSERT_CONDITION_UNKNOWN2 (model, a, NE_EXPR, int_3);
+  }
+
+  /* If "a > b" and "a == 3", then "b == 4" ought to be unsatisfiable.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    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_model2_manager mgr;
+      region_model2 model (&mgr);
+      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
+      ASSERT_CONDITION_TRUE2 (model, a, EQ_EXPR, int_4);
+    }
+
+    /* If "a > 3" && "a <= 4", then "a == 4",
+       assuming a is of integral type.  */
+    {
+      region_model2_manager mgr;
+      region_model2 model (&mgr);
+      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
+      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+      ASSERT_CONDITION_TRUE2 (model, a, EQ_EXPR, int_4);
+    }
+    /* If "a > 3" && "a < 5", then "a == 4",
+       assuming a is of integral type.  */
+    {
+      region_model2_manager mgr;
+      region_model2 model (&mgr);
+      ADD_SAT_CONSTRAINT (model, a, GT_EXPR, int_3);
+      ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
+      ASSERT_CONDITION_TRUE2 (model, a, EQ_EXPR, int_4);
+    }
+    /* If "a >= 4" && "a < 5", then "a == 4",
+       assuming a is of integral type.  */
+    {
+      region_model2_manager mgr;
+      region_model2 model (&mgr);
+      ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
+      ADD_SAT_CONSTRAINT (model, a, LT_EXPR, int_5);
+      ASSERT_CONDITION_TRUE2 (model, a, EQ_EXPR, int_4);
+    }
+    /* If "a >= 4" && "a <= 4", then "a == 4".  */
+    {
+      region_model2_manager mgr;
+      region_model2 model (&mgr);
+      ADD_SAT_CONSTRAINT (model, a, GE_EXPR, int_4);
+      ADD_SAT_CONSTRAINT (model, a, LE_EXPR, int_4);
+      ASSERT_CONDITION_TRUE2 (model, a, EQ_EXPR, int_4);
+    }
+  }
+
+  /* As above, but for floating-point:
+     if "f > 3" && "f <= 4" we don't know that f == 4.  */
+  {
+    tree f = build_global_decl ("f", double_type_node);
+    tree float_3 = build_real_from_int_cst (double_type_node, int_3);
+    tree float_4 = build_real_from_int_cst (double_type_node, int_4);
+
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ADD_SAT_CONSTRAINT (model, f, GT_EXPR, float_3);
+    ADD_SAT_CONSTRAINT (model, f, LE_EXPR, float_4);
+    ASSERT_CONDITION_UNKNOWN2 (model, f, EQ_EXPR, float_4);
+    ASSERT_CONDITION_UNKNOWN2 (model, f, EQ_EXPR, int_4);
+  }
+}
+
+/* Verify various lower-level implementation details about
+   constraint_manager2.  */
+
+static void
+test_constraint_impl ()
+{
+  tree int_42 = build_int_cst (integer_type_node, 42);
+  tree int_0 = build_int_cst (integer_type_node, 0);
+
+  tree x = build_global_decl ("x", integer_type_node);
+  tree y = build_global_decl ("y", integer_type_node);
+  tree z = build_global_decl ("z", integer_type_node);
+
+  /* x == y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
+
+    /* Assert various things about the insides of model.  */
+    constraint_manager2 *cm = model.get_constraints2 ();
+    ASSERT_EQ (cm->m_constraints.length (), 0);
+    ASSERT_EQ (cm->m_equiv_class2es.length (), 1);
+  }
+
+  /* y <= z; x == y.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GE_EXPR, z);
+
+    ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_TRUE2 (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GE_EXPR, z);
+
+    ADD_SAT_CONSTRAINT (model, x, EQ_EXPR, y);
+
+    /* Assert various things about the insides of model.  */
+    constraint_manager2 *cm = model.get_constraints2 ();
+    ASSERT_EQ (cm->m_constraints.length (), 1);
+    ASSERT_EQ (cm->m_equiv_class2es.length (), 2);
+
+    /* Ensure that we merged the constraints.  */
+    ASSERT_CONDITION_TRUE2 (model, x, GE_EXPR, z);
+  }
+
+  /* y <= z; y == x.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, EQ_EXPR, y);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GE_EXPR, z);
+
+    ADD_SAT_CONSTRAINT (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_TRUE2 (model, y, GE_EXPR, z);
+    ASSERT_CONDITION_UNKNOWN2 (model, x, GE_EXPR, z);
+
+    ADD_SAT_CONSTRAINT (model, y, EQ_EXPR, x);
+
+    /* Assert various things about the insides of model.  */
+    constraint_manager2 *cm = model.get_constraints2 ();
+    ASSERT_EQ (cm->m_constraints.length (), 1);
+    ASSERT_EQ (cm->m_equiv_class2es.length (), 2);
+
+    /* Ensure that we merged the constraints.  */
+    ASSERT_CONDITION_TRUE2 (model, x, GE_EXPR, z);
+  }
+
+  /* x == 0, then x != 42.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+
+    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_manager2 *cm = model.get_constraints2 ();
+    ASSERT_EQ (cm->m_constraints.length (), 1);
+    ASSERT_EQ (cm->m_equiv_class2es.length (), 2);
+    ASSERT_EQ (cm->m_constraints[0].m_lhs,
+	       cm->get_or_add_equiv_class2 (model.get_rvalue (int_0, NULL)));
+    ASSERT_EQ (cm->m_constraints[0].m_rhs,
+	       cm->get_or_add_equiv_class2 (model.get_rvalue (int_42, NULL)));
+    ASSERT_EQ (cm->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
+}
+
+/* Check that operator== and hashing works as expected for the
+   various types.  */
+
+static void
+test_equality ()
+{
+  tree x = build_global_decl ("x", integer_type_node);
+  tree y = build_global_decl ("y", integer_type_node);
+
+  {
+    region_model2_manager mgr;
+    region_model2 model0 (&mgr);
+    region_model2 model1 (&mgr);
+
+    constraint_manager2 *cm0 = model0.get_constraints2 ();
+    constraint_manager2 *cm1 = model1.get_constraints2 ();
+
+    ASSERT_EQ (cm0->hash (), cm1->hash ());
+    ASSERT_EQ (*cm0, *cm1);
+
+#if 0
+    ASSERT_EQ (model0.hash (), model1.hash ());
+#endif
+    ASSERT_EQ (model0, model1);
+
+    ADD_SAT_CONSTRAINT (model1, x, EQ_EXPR, y);
+    ASSERT_NE (cm0->hash (), cm1->hash ());
+    ASSERT_NE (*cm0, *cm1);
+
+#if 0
+    ASSERT_NE (model0.hash (), model1.hash ());
+#endif
+    ASSERT_NE (model0, model1);
+
+    region_model2 model2 (&mgr);
+    constraint_manager2 *cm2 = model2.get_constraints2 ();
+    /* Make the same change to cm2.  */
+    ADD_SAT_CONSTRAINT (model2, x, EQ_EXPR, y);
+    ASSERT_EQ (cm1->hash (), cm2->hash ());
+    ASSERT_EQ (*cm1, *cm2);
+
+#if 0
+    ASSERT_EQ (model1.hash (), model2.hash ());
+#endif
+    ASSERT_EQ (model1, model2);
+  }
+}
+
+/* Verify tracking inequality of a variable against many constants.  */
+
+static void
+test_many_constants ()
+{
+  tree a = build_global_decl ("a", integer_type_node);
+
+  region_model2_manager mgr;
+  region_model2 model (&mgr);
+  auto_vec<tree> constants;
+  for (int i = 0; i < 20; i++)
+    {
+      tree constant = build_int_cst (integer_type_node, i);
+      constants.safe_push (constant);
+      ADD_SAT_CONSTRAINT (model, a, NE_EXPR, constant);
+
+      /* Merge, and check the result.  */
+      region_model2 other (model);
+
+#if 0
+      region_model2 merged (&mgr);
+      ASSERT_TRUE (model.can_merge_with_p (other, &merged));
+      model.canonicalize (NULL);
+      merged.canonicalize (NULL);
+      ASSERT_EQ (model, merged);
+#endif
+
+      for (int j = 0; j <= i; j++)
+	ASSERT_CONDITION_TRUE2 (model, a, NE_EXPR, constants[j]);
+    }
+}
+
+/* Run the selftests in this file, temporarily overriding
+   flag_analyzer_transitivity with TRANSITIVITY.  */
+
+static void
+run_constraint_manager2_tests (bool transitivity)
+{
+  int saved_flag_analyzer_transitivity = flag_analyzer_transitivity;
+  flag_analyzer_transitivity = transitivity;
+
+  test_constraint_conditions ();
+  if (flag_analyzer_transitivity)
+    {
+      /* These selftests assume transitivity.  */
+      test_transitivity ();
+      test_constant_comparisons ();
+    }
+  test_constraint_impl ();
+  test_equality ();
+  test_many_constants ();
+
+  flag_analyzer_transitivity = saved_flag_analyzer_transitivity;
+}
+
+/* Run all of the selftests within this file.  */
+
+void
+analyzer_constraint_manager2_cc_tests ()
+{
+  /* Run the tests twice: with and without transitivity.  */
+  run_constraint_manager2_tests (true);
+  run_constraint_manager2_tests (false);
+}
+
+} // namespace selftest
+
+#endif /* CHECKING_P */
+
+} // namespace ana
+
+#endif /* #if ENABLE_ANALYZER */
diff --git a/gcc/analyzer/constraint-manager2.h b/gcc/analyzer/constraint-manager2.h
new file mode 100644
index 00000000000..4de64fd620b
--- /dev/null
+++ b/gcc/analyzer/constraint-manager2.h
@@ -0,0 +1,243 @@
+/* Tracking equivalence classes and constraints at a point on an execution path.
+   Copyright (C) 2019-2020 Free Software Foundation, Inc.
+   Contributed by David Malcolm <dmalcolm@redhat.com>.
+
+This file is part of GCC.
+
+GCC is free software; you can redistribute it and/or modify it
+under the terms of the GNU General Public License as published by
+the Free Software Foundation; either version 3, or (at your option)
+any later version.
+
+GCC 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 GCC; see the file COPYING3.  If not see
+<http://www.gnu.org/licenses/>.  */
+
+#ifndef GCC_ANALYZER_CONSTRAINT_MANAGER2_H
+#define GCC_ANALYZER_CONSTRAINT_MANAGER2_H
+
+namespace ana {
+
+class constraint_manager2;
+
+/* Abstract base class for specifying how state should be purged.  */
+
+class purge_criteria
+{
+public:
+  virtual ~purge_criteria () {}
+  virtual bool should_purge_p (svalue2 *sval) const = 0;
+};
+
+/* An equivalence class within a constraint manager: a set of
+   svalue_ids that are known to all be equal to each other,
+   together with an optional tree constant that they are equal to.  */
+
+class equiv_class2
+{
+public:
+  equiv_class2 ();
+  equiv_class2 (const equiv_class2 &other);
+
+  hashval_t hash () const;
+  bool operator== (const equiv_class2 &other);
+
+  void add (svalue2 *sval);
+  bool del (svalue2 *sval);
+
+  tree get_any_constant () const { return m_constant; }
+
+  svalue2 *get_representative () const;
+
+  void canonicalize ();
+
+  void print (pretty_printer *pp) const;
+
+  /* An equivalence class can contain multiple constants (e.g. multiple
+     different zeroes, for different types); these are just for the last
+     constant added.  */
+  tree m_constant;
+  svalue2 *m_cst_sval;
+
+  // TODO: should this be a set rather than a vec?
+  auto_vec<svalue2 *> m_vars;
+};
+
+/* The various kinds of constraint.  */
+
+enum constraint_op
+{
+  CONSTRAINT_NE,
+  CONSTRAINT_LT,
+  CONSTRAINT_LE
+};
+
+const char *constraint_op_code (enum constraint_op c_op);
+
+/* An ID for an equiv_class2 within a constraint_manager2.  Internally, this
+   is an index into a vector of equiv_class2 * within the constraint_manager2.  */
+
+class equiv_class2_id
+{
+public:
+  static equiv_class2_id null () { return equiv_class2_id (-1); }
+
+  equiv_class2_id (unsigned idx) : m_idx (idx) {}
+  const equiv_class2 &get_obj (const constraint_manager2 &cm) const;
+  equiv_class2 &get_obj (constraint_manager2 &cm) const;
+
+  bool operator== (const equiv_class2_id &other) const
+  {
+    return m_idx == other.m_idx;
+  }
+  bool operator!= (const equiv_class2_id &other) const
+  {
+    return m_idx != other.m_idx;
+  }
+
+  bool null_p () const { return m_idx == -1; }
+
+  static equiv_class2_id from_int (int idx) { return equiv_class2_id (idx); }
+  int as_int () const { return m_idx; }
+
+  void print (pretty_printer *pp) const;
+
+  void update_for_removal (equiv_class2_id other)
+  {
+    if (m_idx > other.m_idx)
+      m_idx--;
+  }
+
+  int m_idx;
+};
+
+/* A relationship between two equivalence classes in a constraint_manager2.  */
+
+class constraint2
+{
+ public:
+  constraint2 (equiv_class2_id lhs, enum constraint_op c_op, equiv_class2_id rhs)
+  : m_lhs (lhs), m_op (c_op), m_rhs (rhs)
+  {
+    gcc_assert (!lhs.null_p ());
+    gcc_assert (!rhs.null_p ());
+  }
+
+  void print (pretty_printer *pp, const constraint_manager2 &cm) const;
+
+  hashval_t hash () const;
+  bool operator== (const constraint2 &other) const;
+
+  /* Is this an ordering, rather than a "!=".  */
+  bool is_ordering_p () const
+  {
+    return m_op != CONSTRAINT_NE;
+  }
+
+  equiv_class2_id m_lhs;
+  enum constraint_op m_op;
+  equiv_class2_id m_rhs;
+};
+
+/* An abstract base class for use with constraint_manager2::for_each_fact.  */
+
+class fact_visitor
+{
+ public:
+  virtual ~fact_visitor () {}
+  virtual void on_fact (svalue2 *lhs, enum tree_code, svalue2 *rhs) = 0;
+};
+
+/* A collection of equivalence classes and constraints on them.
+
+   Given N svalue2s, this can be thought of as representing a subset of
+   N-dimensional space.  When we call add_constraint,
+   we are effectively taking an intersection with that constraint.  */
+
+class constraint_manager2
+{
+public:
+  constraint_manager2 (region_model2_manager *mgr) : m_mgr (mgr) {}
+  constraint_manager2 (const constraint_manager2 &other);
+  virtual ~constraint_manager2 () {}
+
+#if 0
+  virtual constraint_manager2 *clone (region_model2 *) const = 0;
+#endif
+  constraint_manager2& operator= (const constraint_manager2 &other);
+
+  hashval_t hash () const;
+  bool operator== (const constraint_manager2 &other) const;
+  bool operator!= (const constraint_manager2 &other) const
+  {
+    return !(*this == other);
+  }
+
+  void print (pretty_printer *pp) const;
+  void dump_to_pp (pretty_printer *pp) const;
+  void dump (FILE *fp) const;
+  void dump () const;
+
+  const equiv_class2 &get_equiv_class2_by_index (unsigned idx) const
+  {
+    return *m_equiv_class2es[idx];
+  }
+  equiv_class2 &get_equiv_class2_by_index (unsigned idx)
+  {
+    return *m_equiv_class2es[idx];
+  }
+
+  equiv_class2 &get_equiv_class2 (svalue2 *sval)
+  {
+    equiv_class2_id ec_id = get_or_add_equiv_class2 (sval);
+    return ec_id.get_obj (*this);
+  }
+
+  bool add_constraint (svalue2 *lhs, enum tree_code op, svalue2 *rhs);
+
+  bool add_constraint (equiv_class2_id lhs_ec_id,
+		       enum tree_code op,
+		       equiv_class2_id rhs_ec_id);
+
+  bool get_equiv_class2_by_svalue2 (svalue2 *sval, equiv_class2_id *out) const;
+  equiv_class2_id get_or_add_equiv_class2 (svalue2 *sval);
+  tristate eval_condition (equiv_class2_id lhs,
+			   enum tree_code op,
+			   equiv_class2_id rhs);
+  tristate eval_condition (svalue2 *lhs,
+			   enum tree_code op,
+			   svalue2 *rhs);
+
+  void purge (const purge_criteria &p, purge_stats2 *stats);
+
+  static void merge (const constraint_manager2 &cm_a,
+		     const constraint_manager2 &cm_b,
+		     constraint_manager2 *out,
+		     const model_merger &merger);
+
+  void for_each_fact (fact_visitor *) const;
+
+  void validate () const;
+
+  auto_delete_vec<equiv_class2> m_equiv_class2es;
+  auto_vec<constraint2> m_constraints;
+
+ private:
+  static void clean_merger_input (const constraint_manager2 &cm_in,
+				  constraint_manager2 *out);
+
+  void add_constraint_internal (equiv_class2_id lhs_id,
+				enum constraint_op c_op,
+				equiv_class2_id rhs_id);
+
+  region_model2_manager *m_mgr;
+};
+
+} // namespace ana
+
+#endif /* GCC_ANALYZER_CONSTRAINT_MANAGER2_H */
diff --git a/gcc/analyzer/region-model2.cc b/gcc/analyzer/region-model2.cc
index 6e1d279e1cd..ffa3b634bfa 100644
--- a/gcc/analyzer/region-model2.cc
+++ b/gcc/analyzer/region-model2.cc
@@ -52,7 +52,7 @@ along with GCC; see the file COPYING3.  If not see
 #include "analyzer/supergraph.h"
 #include "sbitmap.h"
 #include "analyzer/region-model2.h"
-//#include "analyzer/constraint-manager.h"
+#include "analyzer/constraint-manager2.h"
 #include "diagnostic-event-id.h"
 #include "analyzer/sm.h"
 #include "diagnostic-event-id.h"
@@ -3012,7 +3012,7 @@ region_model2::region_model2 (region_model2_manager *mgr)
 : m_mgr (mgr), m_store (), m_current_frame (NULL)
 {
   //m_root_reg = add_region2 (new root_region2 ());
-  //m_constraints = new impl_constraint_manager (this);
+  m_constraints2 = new constraint_manager2 (mgr);
   // TODO
 }
 
@@ -3020,6 +3020,7 @@ region_model2::region_model2 (region_model2_manager *mgr)
 
 region_model2::region_model2 (const region_model2 &other)
 : m_mgr (other.m_mgr), m_store (other.m_store),
+  m_constraints2 (new constraint_manager2 (*other.m_constraints2)),
   m_current_frame (other.m_current_frame)
 {
 }
@@ -3029,6 +3030,7 @@ region_model2::region_model2 (const region_model2 &other)
 region_model2::~region_model2 ()
 {
   // empty?
+  delete m_constraints2;
 }
 
 /* region_model2's assignment operator.  */
@@ -3085,10 +3087,8 @@ region_model2::operator== (const region_model2 &other) const
   if (m_store != other.m_store)
     return false;
 
-#if 0
-  if (*m_constraints != *other.m_constraints)
+  if (*m_constraints2 != *other.m_constraints2)
     return false;
-#endif
 
   if (m_current_frame != other.m_current_frame)
     return false;
@@ -3246,6 +3246,11 @@ region_model2::dump_to_pp (pretty_printer *pp, bool summarize) const
   /* Dump store.  */
   m_store.dump_to_pp (pp, summarize, true); // FIXME
 
+  /* Dump constraints.  */
+  pp_string (pp, "constraint_manager2:");
+  pp_newline (pp);
+  m_constraints2->dump_to_pp (pp);
+
 #else
   for (store_map_t::iterator iter = m_store_map.begin ();
        iter != m_store_map.end (); ++iter)
@@ -3545,6 +3550,7 @@ region_model2::on_stmt (const supernode *snode,
       /* TODO: GIMPLE_GOTO needs to be handled by the engine, not the
 	 region_model2, but I don't think this is a regression relative to
 	 the old implementation.  */
+    case GIMPLE_SWITCH:
     case GIMPLE_LABEL:
       /* No-op.  */
       return true;
@@ -5127,12 +5133,8 @@ region_model2::eval_condition (svalue2 *lhs,
   if (ts.is_known ())
     return ts;
 
-#if 0
   /* Otherwise, try constraints.  */
-  return m_constraints->eval_condition (lhs_sval, op, rhs_sval);
-#endif
-  return tristate::unknown (); // TODO
-
+  return m_constraints2->eval_condition (lhs, op, rhs);
 }
 
 /* Determine what is known about the condition "LHS_SVAL OP RHS_SVAL" within
@@ -5258,11 +5260,10 @@ region_model2::add_constraint (tree lhs, enum tree_code op, tree rhs,
   if (t_cond.is_false ())
     return false;
 
-  gcc_unreachable ();
-#if 0
   /* Store the constraint.  */
-  m_constraints->add_constraint (lhs_sval, op, rhs_sval);
+  m_constraints2->add_constraint (lhs_sval, op, rhs_sval);
 
+#if 0
   add_any_constraints_from_ssa_def_stmt (lhs, op, rhs, ctxt);
 
   /* If we now know a symbolic_region2 is non-NULL, clear its
@@ -7090,8 +7091,16 @@ test_dump ()
   region_model2_manager mgr;
   region_model2 model (&mgr);
 
-  ASSERT_DUMP_EQ (model, false, "stack depth: 0\n");
-  ASSERT_DUMP_EQ (model, true, "stack depth: 0\n");
+  ASSERT_DUMP_EQ (model, false,
+		  "stack depth: 0\n"
+		  "constraint_manager2:\n"
+		  "  equiv classes:\n"
+		  "  constraints:\n");
+  ASSERT_DUMP_EQ (model, true,
+		  "stack depth: 0\n"
+		  "constraint_manager2:\n"
+		  "  equiv classes:\n"
+		  "  constraints:\n");
 }
 
 /* Helper function for selftests.  Create a struct or union type named NAME,
diff --git a/gcc/analyzer/region-model2.h b/gcc/analyzer/region-model2.h
index b30b8bc6714..b7e5ea2e256 100644
--- a/gcc/analyzer/region-model2.h
+++ b/gcc/analyzer/region-model2.h
@@ -1789,13 +1789,13 @@ class region_model2
 
   unsigned get_num_svalue2s () const { return m_svalue2s.length (); }
   unsigned get_num_region2s () const { return m_region2s.length (); }
-
+#endif
   /* For selftests.  */
-  constraint_manager *get_constraints ()
+  constraint_manager2 *get_constraints2 ()
   {
-    return m_constraints;
+    return m_constraints2;
   }
-
+#if 0
   void get_descendents (region2_id rid, region2_id_set *out,
 			region2_id exclude_rid) const;
 
@@ -1889,9 +1889,8 @@ class region_model2
 
   store2 m_store;
 
-#if 0
-  constraint_manager *m_constraints; // TODO: embed, rather than dynalloc?
-#endif
+  constraint_manager2 *m_constraints2; // TODO: embed, rather than dynalloc?
+
   frame_region2 *m_current_frame;
 };
 
-- 
2.26.2

