From 34889fe5217a620638b28a1b0902280a1d61495d Mon Sep 17 00:00:00 2001
From: David Malcolm <dmalcolm@redhat.com>
Date: Tue, 14 Apr 2020 10:27:51 -0400
Subject: [PATCH 32/44] FIXME: more WIP on bindings

---
 gcc/analyzer/analyzer.h       |   1 +
 gcc/analyzer/region-model2.cc | 227 +++++++++++++++++++++++++++-------
 gcc/analyzer/region-model2.h  | 187 +++++++++++++++++++---------
 3 files changed, 314 insertions(+), 101 deletions(-)

diff --git a/gcc/analyzer/analyzer.h b/gcc/analyzer/analyzer.h
index 6087e0474b2..16bec81a4a9 100644
--- a/gcc/analyzer/analyzer.h
+++ b/gcc/analyzer/analyzer.h
@@ -64,6 +64,7 @@ class region2;
   class map_region2;
   class symbolic_region2;
   class field_region2;
+class region_model2_manager;
 class region_model2;
 class region_model2_context;
 
diff --git a/gcc/analyzer/region-model2.cc b/gcc/analyzer/region-model2.cc
index 6c96abcd6c7..a4fd6a75b39 100644
--- a/gcc/analyzer/region-model2.cc
+++ b/gcc/analyzer/region-model2.cc
@@ -694,6 +694,14 @@ region2::kind_to_str (enum kind kind)
     }
 }
 
+/* FIXME.  */
+
+int
+region2::cmp_indices (const region2 *reg1, const region2 *reg2)
+{
+  return (long)reg1->get_idx () - (long)reg2->get_idx ();
+}
+
 /* class region2.  */
 
 /* Equality operator for region2.
@@ -1319,26 +1327,12 @@ region2::get_view (tree type, region_model2 *model) const
 
 /* region2's ctor.  */
 
-region2::region2 (region2 *parent, tree type)
-: m_parent (parent), m_type (type)
+region2::region2 (unsigned idx, region2 *parent, tree type)
+: m_idx (idx), m_parent (parent), m_type (type)
 {
   gcc_assert (type == NULL_TREE || TYPE_P (type));
 }
 
-/* region2's copy ctor.  */
-#if 0
-region2::region2 (const region2 &other)
-: m_parent_reg (other.m_parent_reg), m_sval_id (other.m_sval_id),
-  m_type (other.m_type), m_view_regs (other.m_view_regs.length ()),
-  m_is_view (other.m_is_view), m_active_view_reg (other.m_active_view_reg)
-{
-  int i;
-  region2_id *rid;
-  FOR_EACH_VEC_ELT (other.m_view_regs, i, rid)
-    m_view_regs.quick_push (*rid);
-}
-#endif
-
 /* Base implementation of region2::add_to_hash vfunc; subclasses should
    chain up to this.  */
 
@@ -1371,6 +1365,17 @@ region2::print_fields (const region_model2 &model ATTRIBUTE_UNUSED,
 }
 #endif
 
+/* FIXME.  */
+
+int
+region2::cmp_ptrs (const void *p1, const void *p2)
+{
+  const region2 * const *reg1 = (const region2 * const *)p1;
+  const region2 * const *reg2 = (const region2 * const *)p2;
+
+  return cmp_indices (*reg1, *reg2);
+}
+
 /* Determine if a pointer to this region2 must be non-NULL.
 
    Generally, pointers to region2s must be non-NULL, but pointers
@@ -2261,8 +2266,8 @@ heap_region2::compare_fields (const heap_region2 &) const
 
 /* root_region2's default ctor.  */
 
-root_region2::root_region2 ()
-: region2 (NULL, NULL_TREE)
+root_region2::root_region2 (unsigned idx)
+: region2 (idx, NULL, NULL_TREE)
 {
 }
 
@@ -2751,11 +2756,93 @@ field_region2::dump_to_pp (pretty_printer *pp, bool simple) const
     }
 }
 
+/* class binding_key.  */
+
+/* FIXME.  */
+
+int
+binding_key::cmp_ptrs (const void *p1, const void *p2)
+{
+  const binding_key * const *pk1 = (const binding_key * const *)p1;
+  const binding_key * const *pk2 = (const binding_key * const *)p2;
+  return cmp (*pk1, *pk2);
+}
+
+/* FIXME.  */
+
+int
+binding_key::cmp (const binding_key *k1, const binding_key *k2)
+{
+  if (int reg_cmp = region2::cmp_indices (k1->m_region, k2->m_region))
+    return reg_cmp;
+
+  enum kind kind1 = k1->get_kind ();
+  enum kind kind2 = k2->get_kind ();
+  if (kind1 != kind2)
+    return (int)kind1 - (int)kind2;
+
+  int concrete1 = k1->concrete_p ();
+  int concrete2 = k2->concrete_p ();
+  if (int concrete_cmp = concrete1 - concrete2)
+    return concrete_cmp;
+  if (concrete1)
+    {
+      // TODO
+      gcc_unreachable ();
+    }
+  else
+    {
+      // TODO
+      gcc_unreachable ();
+    }
+}
+
+/* class binding_cluster.  */
+
+void
+binding_cluster::dump_to_pp (pretty_printer *pp, bool simple) const
+{
+  auto_vec <const binding_key *> binding_keys;
+  for (map_t::iterator iter = m_map.begin ();
+       iter != m_map.end (); ++iter)
+    {
+      const binding_key *key = (*iter).first;
+      binding_keys.safe_push (key);
+    }
+
+  binding_keys.qsort (binding_key::cmp_ptrs);
+
+  const binding_key *key;
+  unsigned i;
+  FOR_EACH_VEC_ELT (binding_keys, i, key)
+    {
+      if (i > 0)
+	pp_string (pp, ", ");
+      svalue2 *value = *const_cast <map_t &> (m_map).get (key);
+      pp_string (pp, "binding key: {");
+      key->dump_to_pp (pp, simple);
+      pp_string (pp, "}, value: {");
+      value->dump_to_pp (pp, simple);
+      pp_string (pp, "}");
+    }
+}
+
+void
+binding_cluster::bind (region_model2_manager *mgr,
+		       region2 *reg, svalue2 *val)
+{
+  // FIXME: what if symbolic vs concrete?
+  const binding_key *binding
+    = mgr->get_concrete_binding (reg, binding_key::BK_direct, 0);
+  m_map.put (binding, val);
+}
+
 /* class region_model2_manager.  */
 
 region_model2_manager::region_model2_manager ()
-: m_root_region (),
-  m_globals_region (&m_root_region),
+: m_next_region_idx (0),
+  m_root_region (alloc_region_idx ()),
+  m_globals_region (alloc_region_idx (), &m_root_region),
   m_globals_map ()
 {
   // TODO
@@ -2791,7 +2878,7 @@ region_model2_manager::get_region_for_global (tree expr,
   if (slot)
     return *slot;
   decl_region2 *reg
-    = new decl_region2 (&m_globals_region, expr);
+    = new decl_region2 (alloc_region_idx (), &m_globals_region, expr);
   m_globals_map.put (expr, reg);
   return reg;
 }
@@ -2800,10 +2887,30 @@ region2 *
 region_model2_manager::get_field_region (region2 *parent, tree field,
 					 region_model2_context *ctxt)
 {
-  region2 *field_reg = new field_region2 (parent, field);
+  // FIXME: should only alloc_region_idx if consolidation fails
+  region2 *field_reg = new field_region2 (alloc_region_idx (), parent, field);
   return const_cast <region2 *> (m_fields.consolidate (field_reg));
 }
 
+const concrete_binding *
+region_model2_manager::get_concrete_binding (region2 *region,
+					     enum binding_key::kind kind,
+					     concrete_binding::offset_t offset)
+{
+  concrete_binding *b = new concrete_binding (region, kind, offset);
+  return m_concrete_binding_key_mgr.consolidate (b);
+}
+
+const symbolic_binding *
+region_model2_manager::get_symbolic_binding (region2 *region,
+					     enum binding_key::kind kind,
+					     region2 *concrete_offset_region)
+{
+  symbolic_binding *b
+    = new symbolic_binding (region, kind, concrete_offset_region);
+  return m_symbolic_binding_key_mgr.consolidate (b);
+}
+
 /* class region_model2.  */
 
 /* region_model2's default ctor.  */
@@ -3040,7 +3147,32 @@ region_model2::dump_dot (const char *path) const
 void
 region_model2::dump_to_pp (pretty_printer *pp, bool summarize) const
 {
-  // TODO: sort into some deterministic order
+#if 1
+  /* Sort into some deterministic order.  */
+  auto_vec<const region2 *> base_regions;
+  for (cluster_map_t::iterator iter = m_cluster_map.begin ();
+       iter != m_cluster_map.end (); ++iter)
+    {
+      const region2 *base_reg = (*iter).first;
+      base_regions.safe_push (base_reg);
+    }
+  base_regions.qsort (region2::cmp_ptrs);
+
+  const region2 *base_reg;
+  unsigned i;
+  FOR_EACH_VEC_ELT (base_regions, i, base_reg)
+    {
+      if (i > 0)
+	pp_string (pp, ", ");
+      binding_cluster *cluster
+	= *const_cast<cluster_map_t &> (m_cluster_map).get (base_reg);
+      pp_string (pp, "base region: {");
+      base_reg->dump_to_pp (pp, summarize);
+      pp_string (pp, "} has cluster: {");
+      cluster->dump_to_pp (pp, summarize);
+      pp_string (pp, "}");
+    }
+#else
   for (store_map_t::iterator iter = m_store_map.begin ();
        iter != m_store_map.end (); ++iter)
     {
@@ -3052,6 +3184,7 @@ region_model2::dump_to_pp (pretty_printer *pp, bool summarize) const
       pp_string (pp, ": ");
       sval->dump_to_pp (pp, summarize);
     }
+#endif
 #if 0
   if (summarize)
     {
@@ -4142,7 +4275,7 @@ region_model2::handle_phi (region_model2_manager *mgr,
 #endif
     }
   else
-    set_value (get_lvalue (mgr, lhs, ctxt), rhs_sval, ctxt);
+    set_value (mgr, get_lvalue (mgr, lhs, ctxt), rhs_sval, ctxt);
 
   if (ctxt)
     ctxt->on_phi (phi, rhs);
@@ -4775,14 +4908,29 @@ region_model2::deref_rvalue (tree ptr, region_model2_context *ctxt)
    by RHS_SVAL.  */
 
 void
-region_model2::set_value (region2 *lhs_reg, svalue2 *rhs_sval,
+region_model2::set_value (region_model2_manager *mgr,
+			  region2 *lhs_reg, svalue2 *rhs_sval,
 			  region_model2_context *ctxt)
 {
   gcc_assert (lhs_reg);
   gcc_assert (rhs_sval);
 
+#if 1
+  const region2 *base_reg = lhs_reg->get_base_region ();
+  binding_cluster *cluster = NULL;
+  binding_cluster **slot = m_cluster_map.get (base_reg);
+  if (slot)
+    cluster = *slot;
+  else
+    {
+      cluster = new binding_cluster ();
+      m_cluster_map.put (base_reg, cluster);
+    }
+  cluster->bind (mgr, lhs_reg, rhs_sval);
+#else
   m_store_map.put (lhs_reg, rhs_sval);
   // TODO: various kinds of invalidation etc
+#endif
 }
 
 /* Set the value of the region2 given by LHS to the value given
@@ -4796,7 +4944,7 @@ region_model2::set_value (region_model2_manager *mgr,
   svalue2 *rhs_sval = get_rvalue (mgr, rhs, ctxt);
   gcc_assert (lhs_reg);
   gcc_assert (rhs_sval);
-  set_value (lhs_reg, rhs_sval, ctxt);
+  set_value (mgr, lhs_reg, rhs_sval, ctxt);
 }
 
 /* Determine what is known about the condition "LHS_SVAL OP RHS_SVAL" within
@@ -6597,8 +6745,6 @@ assert_dump_eq (const location &loc,
   pretty_printer pp;
   pp_format_decoder (&pp) = default_tree_printer;
 
-  return; // FIXME
-
   model.dump_to_pp (&pp, summarize);
   ASSERT_STREQ_AT (loc, pp_formatted_text (&pp), expected);
 }
@@ -6699,27 +6845,18 @@ test_dump_2 ()
      and a more sophisticated region binding/cluster implementation.  */
 
   /* Simplified dump.  */
-  ASSERT_DUMP_EQ (model, true, "c.x: 17, c.y: -3");
+  ASSERT_DUMP_EQ (model, true,
+		  "base region: {c} has cluster: {"
+		  "binding key: {region: c.x, kind: direct, offset: 0},"
+		  " value: {17},"
+		  " binding key: {region: c.y, kind: direct, offset: 0},"
+		  " value: {-3}"
+		  "}");
 
   /* Full dump.  */
   ASSERT_DUMP_EQ
     (model, false,
-     "r0: {kind: `root', parent: null, sval: null}\n"
-     "`-globals: r1: {kind: `globals', parent: r0, sval: null, map: {`c': r2}}\n"
-     "  `-`c': r2: {kind: `struct', parent: r1, sval: null, type: `struct coord', map: {`x': r3, `y': r4}}\n"
-     "    |: type: `struct coord'\n"
-     "    |-`x': r3: {kind: `primitive', parent: r2, sval: sv0, type: `int'}\n"
-     "    |  |: sval: sv0: {type: `int', `17'}\n"
-     "    |  |: type: `int'\n"
-     "    `-`y': r4: {kind: `primitive', parent: r2, sval: sv1, type: `int'}\n"
-     "      |: sval: sv1: {type: `int', `-3'}\n"
-     "      |: type: `int'\n"
-     "svalue2s:\n"
-     "  sv0: {type: `int', `17'}\n"
-     "  sv1: {type: `int', `-3'}\n"
-     "constraint manager:\n"
-     "  equiv classes:\n"
-     "  constraints:\n");
+     "base region: {decl_region2(globals, `struct coord', `c')} has cluster: {binding key: {region: field_region2(decl_region2(globals, `struct coord', `c'), `int', `x'), kind: direct, offset: 0}, value: {constant_svalue2(`int', 17)}, binding key: {region: field_region2(decl_region2(globals, `struct coord', `c'), `int', `y'), kind: direct, offset: 0}, value: {constant_svalue2(`int', -3)}}");
 }
 
 #if 0
diff --git a/gcc/analyzer/region-model2.h b/gcc/analyzer/region-model2.h
index db5e66f8678..18b9bfde7e5 100644
--- a/gcc/analyzer/region-model2.h
+++ b/gcc/analyzer/region-model2.h
@@ -554,6 +554,9 @@ public:
   virtual region2 *clone () const = 0;
 #endif
 
+  unsigned get_idx () const { return m_idx; }
+  static int cmp_indices (const region2 *reg1, const region2 *reg2);
+
   virtual enum kind get_kind () const = 0;
   virtual map_region2 *dyn_cast_map_region2 () { return NULL; }
   virtual symbolic_region2 *dyn_cast_symbolic_region2 () { return NULL; }
@@ -610,17 +613,17 @@ public:
 
   bool non_null_p (const region_model2 &model) const;
 
+  static int cmp_ptrs (const void *, const void *);
+
  protected:
-  region2 (region2 *parent, tree type);
-#if 0
-  region2 (const region2 &other);
-#endif
+  region2 (unsigned idx, region2 *parent, tree type);
 
   virtual void add_to_hash (inchash::hash &hstate) const;
 #if 0
   virtual void print_fields (const region_model2 &model,
 			     pretty_printer *pp) const;
 #endif
+
  private:
 #if 0
   void become_active_view (region_model2 &model, region_id this_rid);
@@ -628,6 +631,7 @@ public:
   void deactivate_view (region_model2 &model, region_id this_view_rid);
 #endif
 
+  unsigned m_idx; // purely for deterministic sorting at this stage, for dumps
   region2 *m_parent;
   tree m_type;
 };
@@ -654,8 +658,8 @@ public:
   typedef ordered_hash_map<tree, region2 *> map_t;
   typedef map_t::iterator iterator_t;
 
-  map_region2 (region2 *parent, tree type)
-  : region2 (parent, type)
+  map_region2 (unsigned idx, region2 *parent, tree type)
+  : region2 (idx, parent, type)
   {}
   map_region2 (const map_region2 &other);
 
@@ -736,15 +740,10 @@ class scope_region2 : public map_region2
  public:
 
  protected:
-  scope_region2 (region2 *parent)
-  : map_region2 (parent, NULL_TREE)
+  scope_region2 (unsigned idx, region2 *parent)
+    : map_region2 (idx, parent, NULL_TREE)
   {}
 
-  scope_region2 (const scope_region2 &other)
-  : map_region2 (other)
-  {
-  }
-
   bool compare_fields (const scope_region2 &other) const;
 };
 
@@ -754,15 +753,10 @@ class scope_region2 : public map_region2
 class frame_region2 : public scope_region2
 {
 public:
-  frame_region2 (region2 *parent, function *fun, int depth)
-  : scope_region2 (parent), m_fun (fun), m_depth (depth)
+  frame_region2 (unsigned idx, region2 *parent, function *fun, int depth)
+  : scope_region2 (idx, parent), m_fun (fun), m_depth (depth)
   {}
 
-  frame_region2 (const frame_region2 &other)
-  : scope_region2 (other), m_fun (other.m_fun), m_depth (other.m_depth)
-  {
-  }
-
   /* region2 vfuncs.  */
 #if 0
   region2 *clone () const FINAL OVERRIDE;
@@ -805,15 +799,10 @@ namespace ana {
 class globals_region2 : public scope_region2
 {
  public:
-  globals_region2 (region2 *parent)
-  : scope_region2 (parent)
+  globals_region2 (unsigned idx, region2 *parent)
+  : scope_region2 (idx, parent)
   {}
 
-  globals_region2 (const globals_region2 &other)
-  : scope_region2 (other)
-  {
-  }
-
   /* region2 vfuncs.  */
 #if 0
   region2 *clone () const FINAL OVERRIDE;
@@ -845,11 +834,8 @@ namespace ana {
 class code_region2 : public map_region2
 {
 public:
-  code_region2 (region2 *parent)
-  : map_region2 (parent, NULL_TREE)
-  {}
-  code_region2 (const code_region2 &other)
-  : map_region2 (other)
+  code_region2 (unsigned idx, region2 *parent)
+  : map_region2 (idx, parent, NULL_TREE)
   {}
 
   /* region2 vfuncs.  */
@@ -886,8 +872,8 @@ namespace ana {
 class function_region2 : public map_region2
 {
 public:
-  function_region2 (region2 *parent, tree type)
-  : map_region2 (parent, type)
+  function_region2 (unsigned idx, region2 *parent, tree type)
+  : map_region2 (idx, parent, type)
   {
     gcc_assert (FUNC_OR_METHOD_TYPE_P (type));
   }
@@ -1043,8 +1029,7 @@ namespace ana {
 class root_region2 : public region2
 {
 public:
-  root_region2 ();
-  root_region2 (const root_region2 &other);
+  root_region2 (unsigned idx);
 
   bool compare_fields (const root_region2 &other) const;
 
@@ -1131,7 +1116,7 @@ namespace ana {
 class symbolic_region2 : public region2
 {
 public:
-  symbolic_region2 (region2 *parent, tree type, bool possibly_null)
+  symbolic_region2 (unsigned idx, region2 *parent, tree type, bool possibly_null)
   : region2 (parent, type),
     m_possibly_null (possibly_null)
   {}
@@ -1165,8 +1150,8 @@ public:
 class decl_region2 : public region2
 {
 public:
-  decl_region2 (region2 *parent, tree decl)
-  : region2 (parent, TREE_TYPE (decl)), m_decl (decl)
+  decl_region2 (unsigned idx, region2 *parent, tree decl)
+  : region2 (idx, parent, TREE_TYPE (decl)), m_decl (decl)
   {}
 
 #if 0
@@ -1191,8 +1176,8 @@ private:
 class field_region2 : public region2
 {
 public:
-  field_region2 (region2 *parent, tree field)
-  : region2 (parent, TREE_TYPE (field)), m_field (field)
+  field_region2 (unsigned idx, region2 *parent, tree field)
+  : region2 (idx, parent, TREE_TYPE (field)), m_field (field)
   {}
 
 #if 0
@@ -1216,18 +1201,50 @@ private:
 
 class binding_key
 {
+public:
+  virtual ~binding_key() {}
+  virtual bool concrete_p () const = 0;
+
+  enum kind
+  {
+   BK_direct,
+   BK_default
+  };
+  static const char *kind_to_string (enum kind kind)
+  {
+    return kind == BK_direct ? "direct" : "default";
+  }
+
+  virtual void dump_to_pp (pretty_printer *pp, bool simple) const
+  {
+    pp_string (pp, "region: ");
+    m_region->dump_to_pp (pp, simple);
+    pp_printf (pp, ", kind: %s", kind_to_string (m_kind));
+  }
+
+  static int cmp_ptrs (const void *, const void *);
+  static int cmp (const binding_key *, const binding_key *);
+
 protected:
-  binding_key (region2 *region, bool direct)
-  : m_region (region), m_direct (direct) {}
+  binding_key (region2 *region, enum kind kind)
+  : m_region (region), m_kind (kind) {}
 
   region2 *get_region () const { return m_region; }
 
-  bool direct_p () const { return m_direct; }
-  bool default_p () const { return !m_direct; }
+  enum kind get_kind () const { return m_kind; }
+
+  hashval_t impl_hash () const
+  {
+    return (long)m_region ^ m_kind;
+  }
+  bool impl_eq (const binding_key &other)
+  {
+    return m_region == other.m_region && m_kind == other.m_kind;
+  }
 
 private:
   region2 *m_region;
-  bool m_direct; /* vs default.  */
+  enum kind m_kind;
 };
 
 class concrete_binding : public binding_key
@@ -1235,9 +1252,27 @@ class concrete_binding : public binding_key
 public:
   typedef unsigned offset_t;
 
-  concrete_binding (region2 *region, bool direct, offset_t offset)
-  : binding_key (region, direct), m_offset (offset)
+  concrete_binding (region2 *region, enum kind kind, offset_t offset)
+  : binding_key (region, kind), m_offset (offset)
   {}
+  bool concrete_p () const FINAL OVERRIDE { return true; }
+
+  hashval_t hash () const
+  {
+    return binding_key::impl_hash () ^ m_offset;
+  }
+  bool operator== (const concrete_binding &other)
+  {
+    if (!binding_key::impl_eq (other))
+      return false;
+    return m_offset == other.m_offset;
+  }
+
+  void dump_to_pp (pretty_printer *pp, bool simple) const FINAL OVERRIDE
+  {
+    binding_key::dump_to_pp (pp, simple);
+    pp_printf (pp, ", offset: %i", m_offset);
+  }
 
 private:
   offset_t m_offset;
@@ -1246,11 +1281,31 @@ private:
 class symbolic_binding : public binding_key
 {
 public:
-  symbolic_binding (region2 *region, bool direct,
+  symbolic_binding (region2 *region, enum kind kind,
 		    region2 *concrete_offset_region)
-  : binding_key (region, direct),
+  : binding_key (region, kind),
     m_concrete_offset_region (concrete_offset_region)
   {}
+  bool concrete_p () const FINAL OVERRIDE { return false; }
+
+  hashval_t hash () const
+  {
+    return binding_key::impl_hash () ^ (long)m_concrete_offset_region;
+  }
+  bool operator== (const symbolic_binding &other)
+  {
+    if (!binding_key::impl_eq (other))
+      return false;
+    return m_concrete_offset_region == other.m_concrete_offset_region;
+  }
+
+  void dump_to_pp (pretty_printer *pp, bool simple) const FINAL OVERRIDE
+  {
+    binding_key::dump_to_pp (pp, simple);
+    pp_string (pp, ", concrete offset region: ");
+    m_concrete_offset_region->dump_to_pp (pp, simple);
+  }
+
 private:
   region2 *m_concrete_offset_region;
 };
@@ -1261,7 +1316,7 @@ private:
 class binding_cluster
 {
 public:
-  typedef hash_map <const binding_key *, const svalue *> map_t;
+  typedef hash_map <const binding_key *, svalue2 *> map_t;
   //typedef typename map_t::iterator iterator_t;
 
 #if 0
@@ -1269,8 +1324,15 @@ public:
   binding_cluster (const binding_cluster &other);
 #endif
 
+  void dump_to_pp (pretty_printer *pp, bool simple) const;
+
+#if 1
+  void bind (region_model2_manager *mgr,
+	     region2 *, svalue2 *);
+#else
   const binding_cluster *bind (const extrinsic_state &ext_state,
-			       const region2 *, const svalue *) const;
+			       const region2 *, const svalue2 *) const;
+#endif
 
 private:
   map_t m_map;
@@ -1296,14 +1358,18 @@ public:
 
   const concrete_binding *
   get_concrete_binding (region2 *region,
-			bool direct,
+			enum binding_key::kind kind,
 			concrete_binding::offset_t offset);
 
   const symbolic_binding *
-  get_symbolic_binding (region2 *region, bool direct,
+  get_symbolic_binding (region2 *region,
+			enum binding_key::kind kind,
 			region2 *concrete_offset_region);
 
+  unsigned alloc_region_idx () { return m_next_region_idx++; }
+
 private:
+  unsigned m_next_region_idx;
   root_region2 m_root_region;
 
   typedef hash_map<tree, constant_svalue2 *> constants_map_t;
@@ -1321,7 +1387,8 @@ private:
   fields_map_t m_fields_map;
 #endif
 
-  uniq_manager<binding_key> m_binding_key_mgr;
+  uniq_manager<concrete_binding> m_concrete_binding_key_mgr;
+  uniq_manager<symbolic_binding> m_symbolic_binding_key_mgr;
 };
 
 /* A region_model2 encapsulates a representation of the state of memory, with
@@ -1443,7 +1510,8 @@ class region_model2
   region2_id deref_rvalue (tree ptr, region_model2_context *ctxt);
 
 #endif
-  void set_value (region2 *lhs_reg, svalue2 *rhs_sval,
+  void set_value (region_model2_manager *mgr,
+		  region2 *lhs_reg, svalue2 *rhs_sval,
 		  region_model2_context *ctxt);
   void set_value (region_model2_manager *mgr,
 		  tree lhs, tree rhs, region_model2_context *ctxt);
@@ -1580,8 +1648,15 @@ class region_model2
 				      bool *is_first);
 #endif
 
+
+#if 1
+  typedef hash_map <const region2 *, binding_cluster *> cluster_map_t;
+  cluster_map_t m_cluster_map; // TODO: deep copy of this!
+#else
   typedef hash_map <region2 *, svalue2 *> store_map_t;
   store_map_t m_store_map;
+#endif
+
 #if 0
   constraint_manager *m_constraints; // TODO: embed, rather than dynalloc?
 #endif
-- 
2.21.0

