irept: Use singly-linked lists with SUB_IS_LIST

This reduces the memory footprint by two pointers for both named_sub and
comments. The cost is that computing the size of lists and add/remove require
additional iterator increments.

Author: tautschnig

src/util/irep.cpp

@@ -151,11 +151,21 @@ void irept::nonrecursive_destructor(dt *old_data)
     INVARIANT(d->ref_count!=0, "All contents of the stack must be in use");
     d->ref_count--;
 
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(d->named_sub.begin(), d->named_sub.end());
+  const std::size_t comments_size =
+    std::distance(d->comments.begin(), d->comments.end());
+#else
+  const std::size_t named_sub_size = d->named_sub.size();
+  const std::size_t comments_size = d->comments.size();
+#endif
+
     if(d->ref_count==0)
     {
       stack.reserve(stack.size()+
-                    d->named_sub.size()+
-                    d->comments.size()+
+                    named_sub_size +
+                    comments_size +
                     d->sub.size());
 
       for(named_subt::iterator
@@ -276,7 +286,11 @@ void irept::remove(const irep_namet &name)
   named_subt::iterator it=named_subt_lower_bound(s, name);
 
   if(it!=s.end() && it->first==name)
-    s.erase(it);
+  {
+    named_subt::iterator before = s.before_begin();
+    while(std::next(before) != it) ++before;
+    s.erase_after(before);
+  }
   #else
   s.erase(name);
   #endif
@@ -313,7 +327,11 @@ irept &irept::add(const irep_namet &name)
 
   if(it==s.end() ||
      it->first!=name)
-    it=s.insert(it, std::make_pair(name, irept()));
+  {
+    named_subt::iterator before = s.before_begin();
+    while(std::next(before) != it) ++before;
+    it = s.emplace_after(before, name, irept());
+  }
 
   return it->second;
   #else
@@ -331,7 +349,11 @@ irept &irept::add(const irep_namet &name, const irept &irep)
 
   if(it==s.end() ||
      it->first!=name)
-    it=s.insert(it, std::make_pair(name, irep));
+  {
+    named_subt::iterator before = s.before_begin();
+    while(std::next(before) != it) ++before;
+    it = s.emplace_after(before, name, irep);
+  }
   else
     it->second=irep;
 
@@ -394,10 +416,20 @@ bool irept::full_eq(const irept &other) const
   const irept::named_subt &i1_comments=get_comments();
   const irept::named_subt &i2_comments=other.get_comments();
 
+#ifdef SUB_IS_LIST
+  if(
+    i1_sub.size() != i2_sub.size() ||
+    std::distance(i1_named_sub.begin(), i1_named_sub.end()) !=
+    std::distance(i2_named_sub.begin(), i2_named_sub.end()) ||
+    std::distance(i1_comments.begin(), i1_comments.end()) !=
+    std::distance(i2_comments.begin(), i2_comments.end()))
+    return false;
+#else
   if(i1_sub.size()!=i2_sub.size() ||
      i1_named_sub.size()!=i2_named_sub.size() ||
      i1_comments.size()!=i2_comments.size())
     return false;
+#endif
 
   for(std::size_t i=0; i<i1_sub.size(); i++)
     if(!i1_sub[i].full_eq(i2_sub[i]))
@@ -528,8 +560,15 @@ int irept::compare(const irept &i) const
               "Unequal lengths will return before this");
   }
 
+#ifdef SUB_IS_LIST
+  const named_subt::size_type n_size =
+    std::distance(get_named_sub().begin(), get_named_sub().end());
+  const named_subt::size_type i_n_size =
+    std::distance(i.get_named_sub().begin(), i.get_named_sub().end());
+#else
   const named_subt::size_type n_size=get_named_sub().size(),
         i_n_size=i.get_named_sub().size();
+#endif
   if(n_size<i_n_size)
     return -1;
   if(n_size>i_n_size)
@@ -592,7 +631,13 @@ std::size_t irept::hash() const
     result=hash_combine(result, it->second.hash());
   }
 
-  result=hash_finalize(result, named_sub.size()+sub.size());
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(named_sub.begin(), named_sub.end());
+#else
+  const std::size_t named_sub_size = named_sub.size();
+#endif
+  result = hash_finalize(result, named_sub_size + sub.size());
 
   #ifdef HASH_CODE
   read().hash_code=result;
@@ -625,9 +670,16 @@ std::size_t irept::full_hash() const
     result=hash_combine(result, it->second.full_hash());
   }
 
-  result=hash_finalize(
-    result,
-    named_sub.size()+sub.size()+comments.size());
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(named_sub.begin(), named_sub.end());
+  const std::size_t comments_size =
+    std::distance(comments.begin(), comments.end());
+#else
+  const std::size_t named_sub_size = named_sub.size();
+  const std::size_t comments_size = comments.size();
+#endif
+  result = hash_finalize(result, named_sub_size + sub.size() + comments_size);
 
   return result;
 }

src/util/irep.h

@@ -23,7 +23,7 @@ Author: Daniel Kroening, [email protected]
 // #define SUB_IS_LIST
 
 #ifdef SUB_IS_LIST
-#include <list>
+#include <forward_list>
 #else
 #include <map>
 #endif
@@ -95,7 +95,7 @@ class irept
   // memory and increase efficiency.
 
   #ifdef SUB_IS_LIST
-  typedef std::list<std::pair<irep_namet, irept> > named_subt;
+  typedef std::forward_list<std::pair<irep_namet, irept> > named_subt;
   #else
   typedef std::map<irep_namet, irept> named_subt;
   #endif

src/util/irep_hash_container.cpp

@@ -49,17 +49,24 @@ void irep_hash_container_baset::pack(
   const irept::named_subt &named_sub=irep.get_named_sub();
   const irept::named_subt &comments=irep.get_comments();
 
-  packed.reserve(
-    1+1+sub.size()+named_sub.size()*2+
-    (full?comments.size()*2:0));
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(named_sub.begin(), named_sub.end());
+  const std::size_t comments_size = full ?
+    std::distance(comments.begin(), comments.end()) : 0;
+#else
+  const std::size_t named_sub_size = named_sub.size();
+  const std::size_t comments_size = full ? comments.size() : 0;
+#endif
+  packed.reserve(1 + 1 + sub.size() + named_sub_size * 2 + comments_size * 2);
 
   packed.push_back(irep_id_hash()(irep.id()));
 
   packed.push_back(sub.size());
   forall_irep(it, sub)
     packed.push_back(number(*it));
 
-  packed.push_back(named_sub.size());
+  packed.push_back(named_sub_size);
   forall_named_irep(it, named_sub)
   {
     packed.push_back(irep_id_hash()(it->first)); // id
@@ -68,7 +75,7 @@ void irep_hash_container_baset::pack(
 
   if(full)
   {
-    packed.push_back(comments.size());
+    packed.push_back(comments_size);
     forall_named_irep(it, comments)
     {
       packed.push_back(irep_id_hash()(it->first)); // id

src/util/lispirep.cpp

@@ -46,9 +46,17 @@ void irep2lisp(const irept &src, lispexprt &dest)
   dest.value="";
   dest.type=lispexprt::List;
 
-  dest.reserve(2+2*src.get_sub().size()
-                +2*src.get_named_sub().size()
-                +2*src.get_comments().size());
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(src.get_named_sub().begin(), src.get_named_sub().end());
+  const std::size_t comments_size =
+    std::distance(src.get_comments().begin(), src.get_comments().end());
+#else
+  const std::size_t named_sub_size = src.get_named_sub().size();
+  const std::size_t comments_size = src.get_comments().size();
+#endif
+  dest.reserve(
+    2 + 2 * src.get_sub().size() + 2 * named_sub_size + 2 * comments_size);
 
   lispexprt id;
   id.type=lispexprt::String;

src/util/merge_irep.cpp

@@ -28,7 +28,13 @@ std::size_t to_be_merged_irept::hash() const
         result, static_cast<const merged_irept &>(it->second).hash());
   }
 
-  result=hash_finalize(result, named_sub.size()+sub.size());
+#ifdef SUB_IS_LIST
+  const std::size_t named_sub_size =
+    std::distance(named_sub.begin(), named_sub.end());
+#else
+  const std::size_t named_sub_size = named_sub.size();
+#endif
+  result = hash_finalize(result, named_sub_size + sub.size());
 
   return result;
 }
@@ -44,9 +50,16 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const
   const irept::named_subt &o_named_sub=other.get_named_sub();
 
   if(sub.size()!=o_sub.size())
-    return true;
+    return false;
+#ifdef SUB_IS_LIST
+  if(
+    std::distance(named_sub.begin(), named_sub.end()) !=
+    std::distance(o_named_sub.begin(), o_named_sub.end()))
+    return false;
+#else
   if(named_sub.size()!=o_named_sub.size())
-    return true;
+    return false;
+#endif
 
   {
     irept::subt::const_iterator s_it=sub.begin();
@@ -95,13 +108,19 @@ const merged_irept &merged_irepst::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
+#ifdef SUB_IS_LIST
+  irept::named_subt::iterator before = dest_named_sub.before_begin();
+#endif
   forall_named_irep(it, src_named_sub)
+  {
     #ifdef SUB_IS_LIST
-    dest_named_sub.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
+    dest_named_sub.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
     #else
     dest_named_sub[it->first]=merged(it->second); // recursive call
     #endif
+  }
 
   std::pair<to_be_merged_irep_storet::const_iterator, bool> result=
     to_be_merged_irep_store.insert(to_be_merged_irept(new_irep));
@@ -140,24 +159,36 @@ const irept &merge_irept::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
+#ifdef SUB_IS_LIST
+  irept::named_subt::iterator before = dest_named_sub.before_begin();
+#endif
   forall_named_irep(it, src_named_sub)
+  {
     #ifdef SUB_IS_LIST
-    dest_named_sub.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
+    dest_named_sub.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
     #else
     dest_named_sub[it->first]=merged(it->second); // recursive call
     #endif
+  }
 
   const irept::named_subt &src_comments=irep.get_comments();
   irept::named_subt &dest_comments=new_irep.get_comments();
 
+#ifdef SUB_IS_LIST
+  before = dest_comments.before_begin();
+#endif
   forall_named_irep(it, src_comments)
+  {
     #ifdef SUB_IS_LIST
-    dest_comments.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
+    dest_comments.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
     #else
     dest_comments[it->first]=merged(it->second); // recursive call
     #endif
+  }
 
   return *irep_store.insert(new_irep).first;
 }
@@ -188,24 +219,36 @@ const irept &merge_full_irept::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
+#ifdef SUB_IS_LIST
+  irept::named_subt::iterator before = dest_named_sub.before_begin();
+#endif
   forall_named_irep(it, src_named_sub)
+  {
     #ifdef SUB_IS_LIST
-    dest_named_sub.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
+    dest_named_sub.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
     #else
     dest_named_sub[it->first]=merged(it->second); // recursive call
     #endif
+  }
 
   const irept::named_subt &src_comments=irep.get_comments();
   irept::named_subt &dest_comments=new_irep.get_comments();
 
+#ifdef SUB_IS_LIST
+  before = dest_comments.before_begin();
+#endif
   forall_named_irep(it, src_comments)
+  {
     #ifdef SUB_IS_LIST
-    dest_comments.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
+    dest_comments.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
     #else
     dest_comments[it->first]=merged(it->second); // recursive call
     #endif
+  }
 
   return *irep_store.insert(new_irep).first;
 }