From fe00e30944ebfe46f8638002e78a3649be0a1564 Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Wed, 29 Apr 2020 11:43:43 -0400
Subject: [PATCH 089/377] FIXME: WIP on sm-state for revamped model

---
 gcc/analyzer/analyzer.h             |   1 +
 gcc/analyzer/constraint-manager2.cc |  76 +--
 gcc/analyzer/constraint-manager2.h  |  30 +-
 gcc/analyzer/program-state.cc       | 814 +++++++++++++++++++++++++++-
 gcc/analyzer/program-state.h        | 104 ++++
 5 files changed, 970 insertions(+), 55 deletions(-)

diff --git a/gcc/analyzer/analyzer.h b/gcc/analyzer/analyzer.h
index 0e21bc7ba49..8df49a0b631 100644
--- a/gcc/analyzer/analyzer.h
+++ b/gcc/analyzer/analyzer.h
@@ -74,6 +74,7 @@ class store2_manager;
 class region_model2;
 class region_model2_context;
 class constraint_manager2;
+class equiv_class2;
 
 class pending_diagnostic;
 class state_change_event;
diff --git a/gcc/analyzer/constraint-manager2.cc b/gcc/analyzer/constraint-manager2.cc
index fd5366a573e..87c7fe92593 100644
--- a/gcc/analyzer/constraint-manager2.cc
+++ b/gcc/analyzer/constraint-manager2.cc
@@ -331,30 +331,30 @@ equiv_class2::canonicalize ()
 /* Get a debug string for C_OP.  */
 
 const char *
-constraint_op_code2 (enum constraint_op c_op)
+constraint2_op_code (enum constraint2_op c_op)
 {
   switch (c_op)
     {
     default:
       gcc_unreachable ();
-    case CONSTRAINT_NE: return "!=";
-    case CONSTRAINT_LT: return "<";
-    case CONSTRAINT_LE: return "<=";
+    case CONSTRAINT2_NE: return "!=";
+    case CONSTRAINT2_LT: return "<";
+    case CONSTRAINT2_LE: return "<=";
     }
 }
 
 /* Convert C_OP to an enum tree_code.  */
 
 enum tree_code
-constraint_tree_code2 (enum constraint_op c_op)
+constraint2_tree_code (enum constraint2_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;
+    case CONSTRAINT2_NE: return NE_EXPR;
+    case CONSTRAINT2_LT: return LT_EXPR;
+    case CONSTRAINT2_LE: return LE_EXPR;
     }
 }
 
@@ -363,25 +363,25 @@ constraint_tree_code2 (enum constraint_op c_op)
    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)
+eval_constraint_op_for_op (enum constraint2_op c_op, enum tree_code t_op)
 {
   switch (c_op)
     {
     default:
       gcc_unreachable ();
-    case CONSTRAINT_NE:
+    case CONSTRAINT2_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:
+    case CONSTRAINT2_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:
+    case CONSTRAINT2_LE:
       if (t_op == LE_EXPR)
 	return tristate (tristate::TS_TRUE);
       if (t_op == GT_EXPR)
@@ -403,7 +403,7 @@ constraint2::print (pretty_printer *pp, const constraint_manager2 &cm) const
   pp_string (pp, ": ");
   m_lhs.get_obj (cm).print (pp);
   pp_string (pp, " ");
-  pp_string (pp, constraint_op_code2 (m_op));
+  pp_string (pp, constraint2_op_code (m_op));
   pp_string (pp, " ");
   m_rhs.print (pp);
   pp_string (pp, ": ");
@@ -720,19 +720,19 @@ constraint_manager2::add_constraint (equiv_class2_id lhs_ec_id,
       }
       break;
     case GE_EXPR:
-      add_constraint_internal (rhs_ec_id, CONSTRAINT_LE, lhs_ec_id);
+      add_constraint_internal (rhs_ec_id, CONSTRAINT2_LE, lhs_ec_id);
       break;
     case LE_EXPR:
-      add_constraint_internal (lhs_ec_id, CONSTRAINT_LE, rhs_ec_id);
+      add_constraint_internal (lhs_ec_id, CONSTRAINT2_LE, rhs_ec_id);
       break;
     case NE_EXPR:
-      add_constraint_internal (lhs_ec_id, CONSTRAINT_NE, rhs_ec_id);
+      add_constraint_internal (lhs_ec_id, CONSTRAINT2_NE, rhs_ec_id);
       break;
     case GT_EXPR:
-      add_constraint_internal (rhs_ec_id, CONSTRAINT_LT, lhs_ec_id);
+      add_constraint_internal (rhs_ec_id, CONSTRAINT2_LT, lhs_ec_id);
       break;
     case LT_EXPR:
-      add_constraint_internal (lhs_ec_id, CONSTRAINT_LT, rhs_ec_id);
+      add_constraint_internal (lhs_ec_id, CONSTRAINT2_LT, rhs_ec_id);
       break;
     default:
       /* do nothing.  */
@@ -747,8 +747,8 @@ constraint_manager2::add_constraint (equiv_class2_id lhs_ec_id,
 
 void
 constraint_manager2::add_constraint_internal (equiv_class2_id lhs_id,
-					     enum constraint_op c_op,
-					     equiv_class2_id rhs_id)
+					      enum constraint2_op c_op,
+					      equiv_class2_id rhs_id)
 {
   /* Add the constraint.  */
   m_constraints.safe_push (constraint2 (lhs_id, c_op, rhs_id));
@@ -756,7 +756,7 @@ constraint_manager2::add_constraint_internal (equiv_class2_id lhs_id,
   if (!flag_analyzer_transitivity)
     return;
 
-  if (c_op != CONSTRAINT_NE)
+  if (c_op != CONSTRAINT2_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.
@@ -810,8 +810,8 @@ constraint_manager2::add_constraint_internal (equiv_class2_id lhs_id,
 		  && 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);
+		  gcc_assert (c_op == CONSTRAINT2_LE
+			      && other->m_op == CONSTRAINT2_LE);
 		  add_constraint (lhs_id, EQ_EXPR, rhs_id);
 		  /* Adding an equality will merge the two ECs and potentially
 		     reorganize the constraints.  Stop iterating.  */
@@ -829,9 +829,9 @@ constraint_manager2::add_constraint_internal (equiv_class2_id lhs_id,
 		      && !rhs_const
 		      && other_rhs_const)
 		    {
-		      range2 r (bound2 (lhs_const, c_op == CONSTRAINT_LE),
+		      range2 r (bound2 (lhs_const, c_op == CONSTRAINT2_LE),
 			       bound2 (other_rhs_const,
-				      other->m_op == CONSTRAINT_LE));
+				      other->m_op == CONSTRAINT2_LE));
 		      tree constant;
 		      if (r.constrained_to_single_element (&constant))
 			{
@@ -846,7 +846,7 @@ constraint_manager2::add_constraint_internal (equiv_class2_id lhs_id,
 
 		  /* Otherwise, add the constraint implied by transitivity.  */
 		  enum tree_code new_op
-		    = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
+		    = ((c_op == CONSTRAINT2_LE && other->m_op == CONSTRAINT2_LE)
 		       ? LE_EXPR : LT_EXPR);
 		  add_constraint (lhs_id, new_op, other->m_rhs);
 		}
@@ -862,9 +862,9 @@ constraint_manager2::add_constraint_internal (equiv_class2_id lhs_id,
 		      && rhs_const)
 		    {
 		      range2 r (bound2 (other_lhs_const,
-				      other->m_op == CONSTRAINT_LE),
+				      other->m_op == CONSTRAINT2_LE),
 			       bound2 (rhs_const,
-				      c_op == CONSTRAINT_LE));
+				      c_op == CONSTRAINT2_LE));
 		      tree constant;
 		      if (r.constrained_to_single_element (&constant))
 			{
@@ -879,7 +879,7 @@ constraint_manager2::add_constraint_internal (equiv_class2_id lhs_id,
 
 		  /* Otherwise, add the constraint implied by transitivity.  */
 		  enum tree_code new_op
-		    = ((c_op == CONSTRAINT_LE && other->m_op == CONSTRAINT_LE)
+		    = ((c_op == CONSTRAINT2_LE && other->m_op == CONSTRAINT2_LE)
 		       ? LE_EXPR : LT_EXPR);
 		  add_constraint (other->m_lhs, new_op, rhs_id);
 		}
@@ -974,9 +974,9 @@ constraint_manager2::get_or_add_equiv_class2 (svalue2 *sval)
 		= 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);
+		add_constraint_internal (new_id, CONSTRAINT2_LT, other_id);
 	      else if (lt == boolean_false_node)
-		add_constraint_internal (other_id, CONSTRAINT_LT, new_id);
+		add_constraint_internal (other_id, CONSTRAINT2_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.  */
@@ -1072,7 +1072,7 @@ constraint_manager2::eval_condition (svalue2 *lhs,
    Accumulate stats into STATS.  */
 
 void
-constraint_manager2::purge (const purge_criteria &p, purge_stats2 *stats)
+constraint_manager2::purge (const purge_criteria2 &p, purge_stats2 *stats)
 {
   /* Delete any svalue2_ids identified by P within the various equivalence
      classes.  */
@@ -1311,11 +1311,11 @@ private:
    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
+class merger2_fact_visitor : public fact2_visitor
 {
 public:
-  merger_fact_visitor (constraint_manager2 *cm_b,
-		       constraint_manager2 *out)
+  merger2_fact_visitor (constraint_manager2 *cm_b,
+			constraint_manager2 *out)
   : m_cm_b (cm_b), m_out (out)
   {}
 
@@ -1439,7 +1439,7 @@ clean_merger_input (const constraint_manager2 &cm_in,
    facts between two input constraint_manager2s.  */
 
 void
-constraint_manager2::for_each_fact (fact_visitor *visitor) const
+constraint_manager2::for_each_fact (fact2_visitor *visitor) const
 {
   /* First, call EQ_EXPR within the various equivalence classes.  */
   unsigned ec_idx;
@@ -1465,7 +1465,7 @@ constraint_manager2::for_each_fact (fact_visitor *visitor) const
     {
       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);
+      enum tree_code code = constraint2_tree_code (c->m_op);
 
       if (ec_lhs.m_cst_sval)
 	{
@@ -2175,7 +2175,7 @@ test_constraint_impl ()
 	       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);
+    ASSERT_EQ (cm->m_constraints[0].m_op, CONSTRAINT2_LT);
   }
 
   // TODO: selftest for merging ecs "in the middle"
diff --git a/gcc/analyzer/constraint-manager2.h b/gcc/analyzer/constraint-manager2.h
index 4de64fd620b..0b849e1876c 100644
--- a/gcc/analyzer/constraint-manager2.h
+++ b/gcc/analyzer/constraint-manager2.h
@@ -27,10 +27,10 @@ class constraint_manager2;
 
 /* Abstract base class for specifying how state should be purged.  */
 
-class purge_criteria
+class purge_criteria2
 {
 public:
-  virtual ~purge_criteria () {}
+  virtual ~purge_criteria2 () {}
   virtual bool should_purge_p (svalue2 *sval) const = 0;
 };
 
@@ -70,14 +70,14 @@ public:
 
 /* The various kinds of constraint.  */
 
-enum constraint_op
+enum constraint2_op
 {
-  CONSTRAINT_NE,
-  CONSTRAINT_LT,
-  CONSTRAINT_LE
+  CONSTRAINT2_NE,
+  CONSTRAINT2_LT,
+  CONSTRAINT2_LE
 };
 
-const char *constraint_op_code (enum constraint_op c_op);
+const char *constraint_op_code (enum constraint2_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.  */
@@ -121,7 +121,7 @@ public:
 class constraint2
 {
  public:
-  constraint2 (equiv_class2_id lhs, enum constraint_op c_op, equiv_class2_id rhs)
+  constraint2 (equiv_class2_id lhs, enum constraint2_op c_op, equiv_class2_id rhs)
   : m_lhs (lhs), m_op (c_op), m_rhs (rhs)
   {
     gcc_assert (!lhs.null_p ());
@@ -136,20 +136,20 @@ class constraint2
   /* Is this an ordering, rather than a "!=".  */
   bool is_ordering_p () const
   {
-    return m_op != CONSTRAINT_NE;
+    return m_op != CONSTRAINT2_NE;
   }
 
   equiv_class2_id m_lhs;
-  enum constraint_op m_op;
+  enum constraint2_op m_op;
   equiv_class2_id m_rhs;
 };
 
 /* An abstract base class for use with constraint_manager2::for_each_fact.  */
 
-class fact_visitor
+class fact2_visitor
 {
  public:
-  virtual ~fact_visitor () {}
+  virtual ~fact2_visitor () {}
   virtual void on_fact (svalue2 *lhs, enum tree_code, svalue2 *rhs) = 0;
 };
 
@@ -213,14 +213,14 @@ public:
 			   enum tree_code op,
 			   svalue2 *rhs);
 
-  void purge (const purge_criteria &p, purge_stats2 *stats);
+  void purge (const purge_criteria2 &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 for_each_fact (fact2_visitor *) const;
 
   void validate () const;
 
@@ -232,7 +232,7 @@ public:
 				  constraint_manager2 *out);
 
   void add_constraint_internal (equiv_class2_id lhs_id,
-				enum constraint_op c_op,
+				enum constraint2_op c_op,
 				equiv_class2_id rhs_id);
 
   region_model2_manager *m_mgr;
diff --git a/gcc/analyzer/program-state.cc b/gcc/analyzer/program-state.cc
index 2592ebd5e1b..445989b298d 100644
--- a/gcc/analyzer/program-state.cc
+++ b/gcc/analyzer/program-state.cc
@@ -37,6 +37,7 @@ along with GCC; see the file COPYING3.  If not see
 #include "analyzer/region-model2.h"
 #include "analyzer/program-state.h"
 #include "analyzer/constraint-manager.h"
+#include "analyzer/constraint-manager2.h"
 #include "alloc-pool.h"
 #include "fibonacci_heap.h"
 #include "shortest-paths.h"
@@ -591,6 +592,441 @@ sm_state_map::validate (const state_machine &sm,
     }
 }
 
+/* class sm_state_map2.  */
+
+/* sm_state_map2's ctor.  */
+
+sm_state_map2::sm_state_map2 ()
+: m_map (), m_global_state (0)
+{
+}
+
+/* Clone the sm_state_map2.  */
+
+sm_state_map2 *
+sm_state_map2::clone () const
+{
+  return new sm_state_map2 (*this);
+}
+
+/* Print this sm_state_map2 (for SM) to PP.
+   If MODEL is non-NULL, print representative tree values where
+   available.  */
+
+void
+sm_state_map2::print (const state_machine &sm, const region_model2 *model,
+		     pretty_printer *pp) const
+{
+  bool first = true;
+  pp_string (pp, "{");
+  if (m_global_state != 0)
+    {
+      pp_printf (pp, "global: %s", sm.get_state_name (m_global_state));
+      first = false;
+    }
+  for (map_t::iterator iter = m_map.begin ();
+       iter != m_map.end ();
+       ++iter)
+    {
+      if (!first)
+	pp_string (pp, ", ");
+      first = false;
+      svalue2 *sval = (*iter).first;
+      sval->dump_to_pp (pp, false);
+
+      entry_t e = (*iter).second;
+      pp_printf (pp, ": %s", sm.get_state_name (e.m_state));
+#if 0
+      if (model)
+	if (tree rep = model->get_representative_tree (sid))
+	  {
+	    pp_string (pp, " (");
+	    dump_quoted_tree (pp, rep);
+	    pp_character (pp, ')');
+	  }
+#endif
+      if (e.m_origin)
+	{
+	  pp_string (pp, " (origin: ");
+	  e.m_origin->dump_to_pp (pp, false);
+#if 0
+	  if (model)
+	    if (tree rep = model->get_representative_tree (e.m_origin))
+	      {
+		pp_string (pp, " (");
+		dump_quoted_tree (pp, rep);
+		pp_character (pp, ')');
+	      }
+#endif
+	  pp_string (pp, ")");
+	}
+    }
+  pp_string (pp, "}");
+}
+
+/* Dump this object (for SM) to stderr.  */
+
+DEBUG_FUNCTION void
+sm_state_map2::dump (const state_machine &sm) const
+{
+  pretty_printer pp;
+  pp_show_color (&pp) = pp_show_color (global_dc->printer);
+  pp.buffer->stream = stderr;
+  print (sm, NULL, &pp);
+  pp_newline (&pp);
+  pp_flush (&pp);
+}
+
+/* Return true if no states have been set within this map
+   (all expressions are for the start state).  */
+
+bool
+sm_state_map2::is_empty_p () const
+{
+  return m_map.elements () == 0 && m_global_state == 0;
+}
+
+/* Generate a hash value for this sm_state_map2.  */
+
+hashval_t
+sm_state_map2::hash () const
+{
+  hashval_t result = 0;
+
+  /* Accumulate the result by xoring a hash for each slot, so that the
+     result doesn't depend on the ordering of the slots in the map.  */
+
+  for (map_t::iterator iter = m_map.begin ();
+       iter != m_map.end ();
+       ++iter)
+    {
+      inchash::hash hstate;
+      hstate.add_ptr ((*iter).first);
+      entry_t e = (*iter).second;
+      hstate.add_int (e.m_state);
+      hstate.add_ptr (e.m_origin);
+      result ^= hstate.end ();
+    }
+  result ^= m_global_state;
+
+  return result;
+}
+
+/* Equality operator for sm_state_map2.  */
+
+bool
+sm_state_map2::operator== (const sm_state_map2 &other) const
+{
+  if (m_global_state != other.m_global_state)
+    return false;
+
+  if (m_map.elements () != other.m_map.elements ())
+    return false;
+
+  for (map_t::iterator iter = m_map.begin ();
+       iter != m_map.end ();
+       ++iter)
+    {
+      svalue2 *sval = (*iter).first;
+      entry_t e = (*iter).second;
+      entry_t *other_slot = const_cast <map_t &> (other.m_map).get (sval);
+      if (other_slot == NULL)
+	return false;
+      if (e != *other_slot)
+	return false;
+    }
+
+  gcc_checking_assert (hash () == other.hash ());
+
+  return true;
+}
+
+/* Get the state of SVAL within this object.
+   States default to the start state.  */
+
+state_machine::state_t
+sm_state_map2::get_state (svalue2 *sval) const
+{
+  gcc_assert (sval);
+
+  if (entry_t *slot
+      = const_cast <map_t &> (m_map).get (sval))
+    return slot->m_state;
+  else
+    return 0;
+}
+
+/* Get the "origin" svalue2 for any state of SVAL.  */
+
+svalue2 *
+sm_state_map2::get_origin (svalue2 *sval) const
+{
+  gcc_assert (sval);
+
+  entry_t *slot
+    = const_cast <map_t &> (m_map).get (sval);
+  if (slot)
+    return slot->m_origin;
+  else
+    return NULL;
+}
+
+/* Set the state of SID within MODEL to STATE, recording that
+   the state came from ORIGIN.  */
+
+void
+sm_state_map2::set_state (region_model2 *model,
+			  svalue2 *sval,
+			  state_machine::state_t state,
+			  svalue2 *origin)
+{
+  if (model == NULL)
+    return;
+  equiv_class2 &ec = model->get_constraints2 ()->get_equiv_class2 (sval);
+  if (!set_state (ec, state, origin))
+    return;
+
+  // TODO:
+#if 0
+  /* Also do it for all svalues that are equal via non-cm, so that
+     e.g. (void *)&r and (foo *)&r transition together.  */
+  for (unsigned i = 0; i < model->get_num_svalues (); i++)
+    {
+      svalue_id other_sid = svalue_id::from_int (i);
+      if (other_sid == sid)
+	continue;
+
+      tristate eq = model->eval_condition_without_cm (sid, EQ_EXPR, other_sid);
+      if (eq.is_true ())
+	impl_set_state (other_sid, state, origin);
+    }
+#endif
+}
+
+/* Set the state of EC to STATE, recording that the state came from
+   ORIGIN.
+   Return true if any states of svalue_ids within EC changed.  */
+
+bool
+sm_state_map2::set_state (const equiv_class2 &ec,
+			  state_machine::state_t state,
+			  svalue2 *origin)
+{
+  int i;
+  svalue2 *sval;
+  bool any_changed = false;
+  FOR_EACH_VEC_ELT (ec.m_vars, i, sval)
+    any_changed |= impl_set_state (sval, state, origin);
+  return any_changed;
+}
+
+/* Set state of SVAL to STATE, bypassing equivalence classes.
+   Return true if the state changed.  */
+
+bool
+sm_state_map2::impl_set_state (svalue2 *sval, state_machine::state_t state,
+			       svalue2 *origin)
+{
+  if (get_state (sval) == state)
+    return false;
+
+  /* Special-case state 0 as the default value.  */
+  if (state == 0)
+    {
+      if (m_map.get (sval))
+	m_map.remove (sval);
+      return true;
+    }
+  gcc_assert (sval);
+  m_map.put (sval, entry_t (state, origin));
+  return true;
+}
+
+/* Set the "global" state within this state map to STATE.  */
+
+void
+sm_state_map2::set_global_state (state_machine::state_t state)
+{
+  m_global_state = state;
+}
+
+/* Get the "global" state within this state map.  */
+
+state_machine::state_t
+sm_state_map2::get_global_state () const
+{
+  return m_global_state;
+}
+
+/* Handle CALL to unknown FNDECL with an unknown function body, which
+   could do anything to the states passed to it.
+   Clear any state for SM for the params and any LHS.
+   Note that the function might be known to other state machines, but
+   not to this one.  */
+
+void
+sm_state_map2::purge_for_unknown_fncall (const exploded_graph &eg,
+					const state_machine &sm,
+					const gcall *call,
+					tree fndecl,
+					region_model *new_model,
+					region_model_context *ctxt)
+{
+  gcc_unreachable ();
+#if 0
+  logger * const logger = eg.get_logger ();
+  if (logger)
+    {
+      if (fndecl)
+	logger->log ("function %qE is unknown to checker %qs",
+		     fndecl, sm.get_name ());
+      else
+	logger->log ("unknown function pointer for checker %qs",
+		     sm.get_name ());
+    }
+
+  /* Purge any state for parms.  */
+  tree iter_param_types = NULL_TREE;
+  if (fndecl)
+    iter_param_types = TYPE_ARG_TYPES (TREE_TYPE (fndecl));
+  for (unsigned arg_idx = 0; arg_idx < gimple_call_num_args (call); arg_idx++)
+    {
+      /* Track expected param type, where available.  */
+      if (iter_param_types)
+	{
+	  tree param_type = TREE_VALUE (iter_param_types);
+	  gcc_assert (param_type);
+	  iter_param_types = TREE_CHAIN (iter_param_types);
+
+	  /* Don't purge state if it was passed as a const pointer
+	     e.g. for things like strlen (PTR).  */
+	  if (TREE_CODE (param_type) == POINTER_TYPE)
+	    if (TYPE_READONLY (TREE_TYPE (param_type)))
+	      continue;
+	}
+      tree parm = gimple_call_arg (call, arg_idx);
+      svalue_id parm_sid = new_model->get_rvalue (parm, ctxt);
+      set_state (new_model, parm_sid, 0, NULL);
+
+      /* Also clear sm-state from svalue_ids that are passed via a
+	 pointer.  */
+      if (TREE_CODE (parm) == ADDR_EXPR)
+	{
+	  tree pointee = TREE_OPERAND (parm, 0);
+	  svalue_id parm_sid = new_model->get_rvalue (pointee, ctxt);
+	  set_state (new_model, parm_sid, 0, svalue_id::null ());
+	}
+    }
+
+  /* Purge any state for any LHS.  */
+  if (tree lhs = gimple_call_lhs (call))
+    {
+      svalue_id lhs_sid = new_model->get_rvalue (lhs, ctxt);
+      set_state (new_model, lhs_sid, 0, svalue_id::null ());
+    }
+#endif
+}
+
+#if 0
+/* Purge any state for svalue_ids >= FIRST_UNUSED_SID.
+   If !SM::can_purge_p, then report the state as leaking,
+   using SM_IDX, CTXT, and MAP.
+   Return the number of states that were purged.  */
+
+int
+sm_state_map2::on_svalue_purge (const state_machine &sm,
+			       int sm_idx,
+			       svalue_id first_unused_sid,
+			       const svalue_id_map &map,
+			       impl_region_model_context *ctxt)
+{
+  /* TODO: ideally remove the slot directly; for now
+     do it in two stages.  */
+  auto_vec<svalue_id> to_remove;
+  for (map_t::iterator iter = m_map.begin ();
+       iter != m_map.end ();
+       ++iter)
+    {
+      svalue_id dst_sid ((*iter).first);
+      if (dst_sid.as_int () >= first_unused_sid.as_int ())
+	{
+	  /* Complain about leaks here.  */
+	  entry_t e = (*iter).second;
+
+	  if (!sm.can_purge_p (e.m_state))
+	    ctxt->on_state_leak (sm, sm_idx, dst_sid, first_unused_sid,
+				 map, e.m_state);
+
+	  to_remove.safe_push (dst_sid);
+	}
+      else if ((*iter).second.m_origin.as_int () >= first_unused_sid.as_int ())
+	{
+	  /* If the origin svalue is being purged, then reset it to null.  */
+	  (*iter).second.m_origin = svalue_id::null ();
+	}
+    }
+
+  int i;
+  svalue_id *dst_sid;
+  FOR_EACH_VEC_ELT (to_remove, i, dst_sid)
+    m_map.remove (*dst_sid);
+
+  return to_remove.length ();
+}
+
+/* Set the state of CHILD_SID to that of PARENT_SID.  */
+
+void
+sm_state_map2::on_inherited_svalue (svalue_id parent_sid,
+				   svalue_id child_sid)
+{
+  state_machine::state_t state = get_state (parent_sid);
+  impl_set_state (child_sid, state, parent_sid);
+}
+
+/* Set the state of DST_SID to that of SRC_SID.  */
+
+void
+sm_state_map2::on_cast (svalue_id src_sid,
+		       svalue_id dst_sid)
+{
+  state_machine::state_t state = get_state (src_sid);
+  impl_set_state (dst_sid, state, get_origin (src_sid));
+}
+#endif
+
+/* Purge state from SID (in response to a call to an unknown function).  */
+
+void
+sm_state_map2::on_unknown_change (svalue2 *sval)
+{
+  impl_set_state (sval, (state_machine::state_t)0, NULL);
+}
+
+/* Assert that this object is sane.  */
+#if 0
+void
+sm_state_map2::validate (const state_machine &sm,
+			int num_svalues) const
+{
+  /* Skip this in a release build.  */
+#if !CHECKING_P
+  return;
+#endif
+
+  for (map_t::iterator iter = m_map.begin ();
+       iter != m_map.end ();
+       ++iter)
+    {
+      svalue_id sid = (*iter).first;
+      entry_t e = (*iter).second;
+
+      gcc_assert (sid.as_int () < num_svalues);
+      sm.validate (e.m_state);
+      gcc_assert (e.m_origin.as_int () < num_svalues);
+    }
+}
+#endif
 /* class program_state.  */
 
 /* program_state's ctor.  */
@@ -600,6 +1036,7 @@ program_state::program_state (const extrinsic_state &ext_state)
   m_region_model2 (NULL),
   m_region_model (NULL),
   m_checker_states (ext_state.get_num_checkers ()),
+  m_checker_states2 (),
   m_valid (true)
 {
   if (ext_state.get_engine ())
@@ -615,6 +1052,9 @@ program_state::program_state (const extrinsic_state &ext_state)
   int num_states = ext_state.get_num_checkers ();
   for (int i = 0; i < num_states; i++)
     m_checker_states.quick_push (new sm_state_map ());
+  if (ext_state.get_engine2 ())
+    for (int i = 0; i < num_states; i++)
+      m_checker_states2.safe_push (new sm_state_map2 ());
 }
 
 /* program_state's copy ctor.  */
@@ -624,6 +1064,7 @@ program_state::program_state (const program_state &other)
   m_region_model2 (NULL),
   m_region_model (NULL),
   m_checker_states (other.m_checker_states.length ()),
+  m_checker_states2 (other.m_checker_states2.length ()),
   m_valid (true)
 {
   if (other.m_region_model2)
@@ -634,6 +1075,9 @@ program_state::program_state (const program_state &other)
   sm_state_map *smap;
   FOR_EACH_VEC_ELT (other.m_checker_states, i, smap)
     m_checker_states.quick_push (smap->clone ());
+  sm_state_map2 *smap2;
+  FOR_EACH_VEC_ELT (other.m_checker_states2, i, smap2)
+    m_checker_states2.quick_push (smap2->clone ());
 }
 
 /* program_state's assignment operator.  */
@@ -659,6 +1103,15 @@ program_state::operator= (const program_state &other)
   FOR_EACH_VEC_ELT (other.m_checker_states, i, smap)
     m_checker_states.quick_push (smap->clone ());
 
+  sm_state_map2 *smap2;
+  FOR_EACH_VEC_ELT (m_checker_states2, i, smap2)
+    delete smap2;
+  m_checker_states2.truncate (0);
+  gcc_assert (m_checker_states2.space (other.m_checker_states2.length ()));
+
+  FOR_EACH_VEC_ELT (other.m_checker_states2, i, smap2)
+    m_checker_states2.quick_push (smap2->clone ());
+
   m_valid = other.m_valid;
 
   return *this;
@@ -681,6 +1134,11 @@ program_state::program_state (program_state &&other)
     m_checker_states.quick_push (smap);
   other.m_checker_states.truncate (0);
 
+  sm_state_map2 *smap2;
+  FOR_EACH_VEC_ELT (other.m_checker_states2, i, smap2)
+    m_checker_states2.quick_push (smap2);
+  other.m_checker_states2.truncate (0);
+
   m_valid = other.m_valid;
 }
 #endif
@@ -713,6 +1171,10 @@ program_state::hash () const
   sm_state_map *smap;
   FOR_EACH_VEC_ELT (m_checker_states, i, smap)
     result ^= smap->hash ();
+  sm_state_map2 *smap2;
+  FOR_EACH_VEC_ELT (m_checker_states2, i, smap2)
+    result ^= smap2->hash ();
+
   return result;
 }
 
@@ -736,6 +1198,11 @@ program_state::operator== (const program_state &other) const
     if (!(*smap == *other.m_checker_states[i]))
       return false;
 
+  sm_state_map2 *smap2;
+  FOR_EACH_VEC_ELT (m_checker_states2, i, smap2)
+    if (!(*smap2 == *other.m_checker_states2[i]))
+      return false;
+
   gcc_checking_assert (hash () == other.hash ());
 
   return true;
@@ -762,6 +1229,16 @@ program_state::print (const extrinsic_state &ext_state,
 	  pp_newline (pp);
 	}
     }
+  sm_state_map2 *smap2;
+  FOR_EACH_VEC_ELT (m_checker_states2, i, smap2)
+    {
+      if (!smap2->is_empty_p ())
+	{
+	  pp_printf (pp, "%s: ", ext_state.get_name (i));
+	  smap2->print (ext_state.get_sm (i), m_region_model2, pp);
+	  pp_newline (pp);
+	}
+    }
   if (!m_valid)
     {
       pp_printf (pp, "invalid state");
@@ -787,12 +1264,25 @@ program_state::dump_to_pp (const extrinsic_state &ext_state,
   sm_state_map *smap;
   FOR_EACH_VEC_ELT (m_checker_states, i, smap)
     {
-      if (!smap->is_empty_p ())
+      if (!smap->is_empty_p ())
+	{
+	  if (summarize)
+	    pp_space (pp);
+	  pp_printf (pp, "%s: ", ext_state.get_name (i));
+	  smap->print (ext_state.get_sm (i), m_region_model, pp);
+	  if (!summarize)
+	    pp_newline (pp);
+	}
+    }
+  sm_state_map2 *smap2;
+  FOR_EACH_VEC_ELT (m_checker_states2, i, smap2)
+    {
+      if (!smap2->is_empty_p ())
 	{
 	  if (summarize)
 	    pp_space (pp);
 	  pp_printf (pp, "%s: ", ext_state.get_name (i));
-	  smap->print (ext_state.get_sm (i), m_region_model, pp);
+	  smap2->print (ext_state.get_sm (i), m_region_model2, pp);
 	  if (!summarize)
 	    pp_newline (pp);
 	}
@@ -1154,6 +1644,8 @@ program_state::can_merge_with_p (const program_state &other,
 	}
     }
 
+  // TODO: m_checker_states2  
+
   impl_region_model_context ctxt (out, NULL, ext_state);
   out->m_region_model->canonicalize (&ctxt);
 
@@ -1702,6 +2194,318 @@ test_program_state_merging_2 ()
   ASSERT_FALSE (s0.can_merge_with_p (s1, ext_state, &merged));
 }
 
+/* Tests for sm_state_map2.  */
+
+static void
+test_sm_state_map2 ()
+{
+  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);
+
+  /* Test setting states on svalue_id instances directly.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    svalue2 *x_sval = model.get_rvalue (x, NULL);
+    svalue2 *y_sval = model.get_rvalue (y, NULL);
+    svalue2 *z_sval = model.get_rvalue (z, NULL);
+
+    sm_state_map2 map;
+    ASSERT_TRUE (map.is_empty_p ());
+    ASSERT_EQ (map.get_state (x_sval), 0);
+
+    map.impl_set_state (x_sval, 42, z_sval);
+    ASSERT_EQ (map.get_state (x_sval), 42);
+    ASSERT_EQ (map.get_origin (x_sval), z_sval);
+    ASSERT_EQ (map.get_state (y_sval), 0);
+    ASSERT_FALSE (map.is_empty_p ());
+
+    map.impl_set_state (y_sval, 0, z_sval);
+    ASSERT_EQ (map.get_state (y_sval), 0);
+
+    map.impl_set_state (x_sval, 0, z_sval);
+    ASSERT_EQ (map.get_state (x_sval), 0);
+    ASSERT_TRUE (map.is_empty_p ());
+  }
+
+  /* Test setting states via equivalence classes.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    svalue2 *x_sval = model.get_rvalue (x, NULL);
+    svalue2 *y_sval = model.get_rvalue (y, NULL);
+    svalue2 *z_sval = model.get_rvalue (z, NULL);
+
+    sm_state_map2 map;
+    ASSERT_TRUE (map.is_empty_p ());
+    ASSERT_EQ (map.get_state (x_sval), 0);
+    ASSERT_EQ (map.get_state (y_sval), 0);
+
+    model.add_constraint (x, EQ_EXPR, y, NULL);
+
+    /* Setting x to a state should also update y, as they
+       are in the same equivalence class.  */
+    map.set_state (&model, x_sval, 5, z_sval);
+    ASSERT_EQ (map.get_state (x_sval), 5);
+    ASSERT_EQ (map.get_state (y_sval), 5);
+    ASSERT_EQ (map.get_origin (x_sval), z_sval);
+    ASSERT_EQ (map.get_origin (y_sval), z_sval);
+  }
+
+  /* Test equality and hashing.  */
+  {
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    svalue2 *y_sval = model.get_rvalue (y, NULL);
+    svalue2 *z_sval = model.get_rvalue (z, NULL);
+
+    sm_state_map2 map0;
+    sm_state_map2 map1;
+    sm_state_map2 map2;
+
+    ASSERT_EQ (map0.hash (), map1.hash ());
+    ASSERT_EQ (map0, map1);
+
+    map1.impl_set_state (y_sval, 5, z_sval);
+    ASSERT_NE (map0.hash (), map1.hash ());
+    ASSERT_NE (map0, map1);
+
+    /* Make the same change to map2.  */
+    map2.impl_set_state (y_sval, 5, z_sval);
+    ASSERT_EQ (map1.hash (), map2.hash ());
+    ASSERT_EQ (map1, map2);
+  }
+
+  /* Equality and hashing shouldn't depend on ordering.  */
+  {
+    sm_state_map2 map0;
+    sm_state_map2 map1;
+    sm_state_map2 map2;
+
+    ASSERT_EQ (map0.hash (), map1.hash ());
+    ASSERT_EQ (map0, map1);
+
+    region_model2_manager mgr;
+    region_model2 model (&mgr);
+    svalue2 *x_sval = model.get_rvalue (x, NULL);
+    svalue2 *y_sval = model.get_rvalue (y, NULL);
+    svalue2 *z_sval = model.get_rvalue (z, NULL);
+
+    map1.impl_set_state (x_sval, 2, NULL);
+    map1.impl_set_state (y_sval, 3, NULL);
+    map1.impl_set_state (z_sval, 2, NULL);
+
+    map2.impl_set_state (z_sval, 2, NULL);
+    map2.impl_set_state (y_sval, 3, NULL);
+    map2.impl_set_state (x_sval, 2, NULL);
+
+    ASSERT_EQ (map1.hash (), map2.hash ());
+    ASSERT_EQ (map1, map2);
+  }
+
+  // TODO: coverage for purging
+}
+
+/* Verify that program_state::dump_to_pp works as expected.  */
+
+static void
+test_program_state2_dumping ()
+{
+#if 0
+  /* Create a program_state for a global ptr "p" that has
+     malloc sm-state, pointing to a region on the heap.  */
+  tree p = build_global_decl ("p", ptr_type_node);
+
+  state_machine *sm = make_malloc_state_machine (NULL);
+  const state_machine::state_t UNCHECKED_STATE
+    = sm->get_state_by_name ("unchecked");
+  auto_delete_vec <state_machine> checkers;
+  checkers.safe_push (sm);
+  extrinsic_state ext_state (checkers);
+
+  program_state s (ext_state);
+  region_model2 *model = s.m_region_model;
+  region_id new_rid = model->add_new_malloc_region ();
+  svalue_id ptr_sid
+      = model->get_or_create_ptr_svalue (ptr_type_node, new_rid);
+  model->set_value (model->get_lvalue (p, NULL),
+		    ptr_sid, NULL);
+  sm_state_map2 *smap = s.m_checker_states2[0];
+
+  smap->impl_set_state (ptr_sid, UNCHECKED_STATE, svalue_id::null ());
+  ASSERT_EQ (smap->get_state (ptr_sid), UNCHECKED_STATE);
+
+  ASSERT_DUMP_EQ
+    (s, ext_state, false,
+     "rmodel: r0: {kind: `root', parent: null, sval: null}\n"
+     "|-heap: r1: {kind: `heap', parent: r0, sval: sv0}\n"
+     "|  |: sval: sv0: {poisoned: uninit}\n"
+     "|  `-r2: {kind: `symbolic', parent: r1, sval: null, possibly_null: true}\n"
+     "`-globals: r3: {kind: `globals', parent: r0, sval: null, map: {`p': r4}}\n"
+     "  `-`p': r4: {kind: `primitive', parent: r3, sval: sv1, type: `void *'}\n"
+     "    |: sval: sv1: {type: `void *', &r2}\n"
+     "    |: type: `void *'\n"
+     "svalues:\n"
+     "  sv0: {poisoned: uninit}\n"
+     "  sv1: {type: `void *', &r2}\n"
+     "constraint manager:\n"
+     "  equiv classes:\n"
+     "  constraints:\n"
+     "malloc: {sv1: unchecked (`p')}\n");
+
+  ASSERT_DUMP_EQ (s, ext_state, true,
+		  "rmodel: p: &r2 malloc: {sv1: unchecked (`p')}");
+#endif
+}
+
+/* Verify that program_state::dump_to_pp works for string literals.  */
+
+static void
+test_program_state2_dumping_2 ()
+{
+#if 0
+  /* Create a program_state for a global ptr "p" that points to
+     a string constant.  */
+  tree p = build_global_decl ("p", ptr_type_node);
+
+  tree string_cst_ptr = build_string_literal (4, "foo");
+
+  auto_delete_vec <state_machine> checkers;
+  extrinsic_state ext_state (checkers);
+
+  program_state s (ext_state);
+  region_model *model = s.m_region_model;
+  region_id p_rid = model->get_lvalue (p, NULL);
+  svalue_id str_sid = model->get_rvalue (string_cst_ptr, NULL);
+  model->set_value (p_rid, str_sid, NULL);
+
+  ASSERT_DUMP_EQ
+    (s, ext_state, false,
+     "rmodel: r0: {kind: `root', parent: null, sval: null}\n"
+     "|-globals: r1: {kind: `globals', parent: r0, sval: null, map: {`p': r2}}\n"
+     "|  `-`p': r2: {kind: `primitive', parent: r1, sval: sv3, type: `void *'}\n"
+     "|    |: sval: sv3: {type: `void *', &r4}\n"
+     "|    |: type: `void *'\n"
+     "`-r3: {kind: `array', parent: r0, sval: sv0, type: `const char[4]', array: {[0]: r4}}\n"
+     "  |: sval: sv0: {type: `const char[4]', `\"foo\"'}\n"
+     "  |: type: `const char[4]'\n"
+     "  `-[0]: r4: {kind: `primitive', parent: r3, sval: null, type: `const char'}\n"
+     "    |: type: `const char'\n"
+     "svalues:\n"
+     "  sv0: {type: `const char[4]', `\"foo\"'}\n"
+     "  sv1: {type: `int', `0'}\n"
+     "  sv2: {type: `const char *', &r4}\n"
+     "  sv3: {type: `void *', &r4}\n"
+     "constraint manager:\n"
+     "  equiv classes:\n"
+     "  constraints:\n");
+
+  ASSERT_DUMP_EQ (s, ext_state, true,
+		  "rmodel: p: &\"foo\"[0]");
+#endif
+}
+
+/* Verify that program_states with identical sm-state can be merged,
+   and that the merged program_state preserves the sm-state.  */
+
+static void
+test_program_state2_merging ()
+{
+#if 0
+  /* Create a program_state for a global ptr "p" that has
+     malloc sm-state, pointing to a region on the heap.  */
+  tree p = build_global_decl ("p", ptr_type_node);
+
+  auto_delete_vec <state_machine> checkers;
+  checkers.safe_push (make_malloc_state_machine (NULL));
+  extrinsic_state ext_state (checkers);
+
+  program_state s0 (ext_state);
+  impl_region_model_context ctxt (&s0, NULL, ext_state);
+
+  region_model *model0 = s0.m_region_model;
+  region_id new_rid = model0->add_new_malloc_region ();
+  svalue_id ptr_sid
+      = model0->get_or_create_ptr_svalue (ptr_type_node, new_rid);
+  model0->set_value (model0->get_lvalue (p, &ctxt),
+		     ptr_sid, &ctxt);
+  sm_state_map2 *smap = s0.m_checker_states[0];
+  const state_machine::state_t TEST_STATE = 3;
+  smap->impl_set_state (ptr_sid, TEST_STATE, svalue_id::null ());
+  ASSERT_EQ (smap->get_state (ptr_sid), TEST_STATE);
+
+  model0->canonicalize (&ctxt);
+
+  /* Verify that canonicalization preserves sm-state.  */
+  ASSERT_EQ (smap->get_state (model0->get_rvalue (p, NULL)), TEST_STATE);
+
+  /* Make a copy of the program_state.  */
+  program_state s1 (s0);
+  ASSERT_EQ (s0, s1);
+
+  /* We have two identical states with "p" pointing to a heap region
+     with the given sm-state.
+     They ought to be mergeable, preserving the sm-state.  */
+  program_state merged (ext_state);
+  ASSERT_TRUE (s0.can_merge_with_p (s1, ext_state, &merged));
+  merged.validate (ext_state);
+
+  /* Verify that the merged state has the sm-state for "p".  */
+  region_model *merged_model = merged.m_region_model;
+  sm_state_map2 *merged_smap = merged.m_checker_states[0];
+  ASSERT_EQ (merged_smap->get_state (merged_model->get_rvalue (p, NULL)),
+	     TEST_STATE);
+
+  /* Try canonicalizing.  */
+  impl_region_model_context merged_ctxt (&merged, NULL, ext_state);
+  merged.m_region_model->canonicalize (&merged_ctxt);
+  merged.validate (ext_state);
+
+  /* Verify that the merged state still has the sm-state for "p".  */
+  ASSERT_EQ (merged_smap->get_state (merged_model->get_rvalue (p, NULL)),
+	     TEST_STATE);
+
+  /* After canonicalization, we ought to have equality with the inputs.  */
+  ASSERT_EQ (s0, merged);
+#endif
+}
+
+/* Verify that program_states with different global-state in an sm-state
+   can't be merged.  */
+
+static void
+test_program_state2_merging_2 ()
+{
+#if 0
+  auto_delete_vec <state_machine> checkers;
+  checkers.safe_push (make_signal_state_machine (NULL));
+  extrinsic_state ext_state (checkers);
+
+  program_state s0 (ext_state);
+  {
+    sm_state_map2 *smap0 = s0.m_checker_states[0];
+    const state_machine::state_t TEST_STATE_0 = 0;
+    smap0->set_global_state (TEST_STATE_0);
+    ASSERT_EQ (smap0->get_global_state (), TEST_STATE_0);
+  }
+
+  program_state s1 (ext_state);
+  {
+    sm_state_map2 *smap1 = s1.m_checker_states[0];
+    const state_machine::state_t TEST_STATE_1 = 1;
+    smap1->set_global_state (TEST_STATE_1);
+    ASSERT_EQ (smap1->get_global_state (), TEST_STATE_1);
+  }
+
+  ASSERT_NE (s0, s1);
+
+  /* They ought to not be mergeable.  */
+  program_state merged (ext_state);
+  ASSERT_FALSE (s0.can_merge_with_p (s1, ext_state, &merged));
+#endif
+}
+
 /* Run all of the selftests within this file.  */
 
 void
@@ -1712,6 +2516,12 @@ analyzer_program_state_cc_tests ()
   test_program_state_dumping_2 ();
   test_program_state_merging ();
   test_program_state_merging_2 ();
+
+  test_sm_state_map2 ();
+  test_program_state2_dumping ();
+  test_program_state2_dumping_2 ();
+  test_program_state2_merging ();
+  test_program_state2_merging_2 ();
 }
 
 } // namespace selftest
diff --git a/gcc/analyzer/program-state.h b/gcc/analyzer/program-state.h
index b1a3b7a5652..b759f3bcbb1 100644
--- a/gcc/analyzer/program-state.h
+++ b/gcc/analyzer/program-state.h
@@ -223,6 +223,109 @@ private:
   state_machine::state_t m_global_state;
 };
 
+/* Map from svalue2 * to state machine state, also capturing the origin of
+   each state.  */
+
+class sm_state_map2
+{
+public:
+  /* An entry in the hash_map.  */
+  struct entry_t
+  {
+    /* Default ctor needed by hash_map::empty.  */
+    entry_t ()
+    : m_state (0), m_origin (NULL)
+    {
+    }
+
+    entry_t (state_machine::state_t state,
+	     svalue2 *origin)
+    : m_state (state), m_origin (origin)
+    {}
+
+    bool operator== (const entry_t &other) const
+    {
+      return (m_state == other.m_state
+	      && m_origin == other.m_origin);
+    }
+    bool operator!= (const entry_t &other) const
+    {
+      return !(*this == other);
+    }
+
+    state_machine::state_t m_state;
+    svalue2 *m_origin;
+  };
+  typedef hash_map <svalue2 *, entry_t> map_t;
+  typedef map_t::iterator iterator_t;
+
+  sm_state_map2 ();
+
+  sm_state_map2 *clone () const;
+
+  void print (const state_machine &sm, const region_model2 *model,
+	      pretty_printer *pp) const;
+  void dump (const state_machine &sm) const;
+
+  bool is_empty_p () const;
+
+  hashval_t hash () const;
+
+  bool operator== (const sm_state_map2 &other) const;
+  bool operator!= (const sm_state_map2 &other) const
+  {
+    return !(*this == other);
+  }
+
+  state_machine::state_t get_state (svalue2 *sval) const;
+  svalue2 *get_origin (svalue2 *sval) const;
+
+  void set_state (region_model2 *model,
+		  svalue2 *sval,
+		  state_machine::state_t state,
+		  svalue2 *origin);
+  bool set_state (const equiv_class2 &ec,
+		  state_machine::state_t state,
+		  svalue2 *origin);
+  bool impl_set_state (svalue2 *sval,
+		       state_machine::state_t state,
+		       svalue2 *origin);
+
+  void set_global_state (state_machine::state_t state);
+  state_machine::state_t get_global_state () const;
+
+  void purge_for_unknown_fncall (const exploded_graph &eg,
+				 const state_machine &sm,
+				 const gcall *call, tree fndecl,
+				 region_model *new_model,
+				 region_model_context *ctxt);
+
+#if 0
+  int on_svalue_purge (const state_machine &sm,
+		       int sm_idx,
+		       svalue_id first_unused_sid,
+		       const svalue_id_map &map,
+		       impl_region_model_context *ctxt);
+  void on_inherited_svalue (svalue_id parent_sid,
+			    svalue_id child_sid);
+
+  void on_cast (svalue_id src_sid,
+		svalue_id dst_sid);
+#endif
+
+  void on_unknown_change (svalue2 *sval);
+
+#if 0
+  void validate (const state_machine &sm, int num_svalues) const;
+#endif
+  iterator_t begin () const { return m_map.begin (); }
+  iterator_t end () const { return m_map.end (); }
+
+private:
+  map_t m_map;
+  state_machine::state_t m_global_state;
+};
+
 /* A class for representing the state of interest at a given path of
    analysis.
 
@@ -307,6 +410,7 @@ public:
   /* TODO: lose the pointer here (const-correctness issues?).  */
   region_model *m_region_model;
   auto_delete_vec<sm_state_map> m_checker_states;
+  auto_delete_vec<sm_state_map2> m_checker_states2;
 
   /* If false, then don't attempt to explore further states along this path.
      For use in "handling" lvalues for tree codes we haven't yet
-- 
2.26.2

