Enable sharing of irept's as long as no references are held to sub-parts

A PR by @reuk some time ago prevented sharing when references are held to sub-parts but didn't re-enable sharing in situations where it is actually safe to do so. This PR amends that.

This should improve performance, particularly in memory usage.

Author: NathanJPhillips

Diff for: src/util/expr.cpp

@@ -25,64 +25,40 @@ Author: Daniel Kroening, [email protected]
 
 void exprt::move_to_operands(exprt &expr)
 {
-  operandst &op=operands();
-  op.push_back(static_cast<const exprt &>(get_nil_irep()));
-  op.back().swap(expr);
+  move_to_sub(expr);
 }
 
 void exprt::move_to_operands(exprt &e1, exprt &e2)
 {
-  operandst &op=operands();
-  #ifndef USE_LIST
-  op.reserve(op.size()+2);
-  #endif
-  op.push_back(static_cast<const exprt &>(get_nil_irep()));
-  op.back().swap(e1);
-  op.push_back(static_cast<const exprt &>(get_nil_irep()));
-  op.back().swap(e2);
+  reserve_operands(get_operands_size() + 2);
+  move_to_sub(e1);
+  move_to_sub(e2);
 }
 
 void exprt::move_to_operands(exprt &e1, exprt &e2, exprt &e3)
 {
-  operandst &op=operands();
-  #ifndef USE_LIST
-  op.reserve(op.size()+3);
-  #endif
-  op.push_back(static_cast<const exprt &>(get_nil_irep()));
-  op.back().swap(e1);
-  op.push_back(static_cast<const exprt &>(get_nil_irep()));
-  op.back().swap(e2);
-  op.push_back(static_cast<const exprt &>(get_nil_irep()));
-  op.back().swap(e3);
+  reserve_operands(get_operands_size() + 3);
+  move_to_sub(e1);
+  move_to_sub(e2);
+  move_to_sub(e3);
 }
 
-void exprt::copy_to_operands(const exprt &expr)
+void exprt::copy_to_operands(exprt expr)
 {
-  operands().push_back(expr);
+  // Move the copy created by passing the argument by value to the operands
+  move_to_operands(expr);
 }
 
-void exprt::copy_to_operands(const exprt &e1, const exprt &e2)
+void exprt::copy_to_operands(exprt e1, exprt e2)
 {
-  operandst &op=operands();
-  #ifndef USE_LIST
-  op.reserve(op.size()+2);
-  #endif
-  op.push_back(e1);
-  op.push_back(e2);
+  // Move the copies created by passing the arguments by value to the operands
+  move_to_operands(e1, e2);
 }
 
-void exprt::copy_to_operands(
-  const exprt &e1,
-  const exprt &e2,
-  const exprt &e3)
+void exprt::copy_to_operands(exprt e1, exprt e2, exprt e3)
 {
-  operandst &op=operands();
-  #ifndef USE_LIST
-  op.reserve(op.size()+3);
-  #endif
-  op.push_back(e1);
-  op.push_back(e2);
-  op.push_back(e3);
+  // Move the copies created by passing the arguments by value to the operands
+  move_to_operands(e1, e2, e3);
 }
 
 void exprt::make_typecast(const typet &_type)
@@ -112,7 +88,7 @@ void exprt::make_not()
 
   if(id()==ID_not && operands().size()==1)
   {
-    new_expr.swap(operands().front());
+    new_expr.swap(op0());
   }
   else
   {

Diff for: src/util/expr.h

@@ -94,17 +94,23 @@ class exprt:public irept
   const exprt &op3() const
   { return operands()[3]; }
 
+  operandst::size_type get_operands_size() const
+  {
+    return get_sub_size();
+  }
   void reserve_operands(operandst::size_type n)
-  { operands().reserve(n) ; }
+  {
+    reserve_sub(n);
+  }
 
   // destroys expr, e1, e2, e3
   void move_to_operands(exprt &expr);
   void move_to_operands(exprt &e1, exprt &e2);
   void move_to_operands(exprt &e1, exprt &e2, exprt &e3);
   // does not destroy expr, e1, e2, e3
-  void copy_to_operands(const exprt &expr);
-  void copy_to_operands(const exprt &e1, const exprt &e2);
-  void copy_to_operands(const exprt &e1, const exprt &e2, const exprt &e3);
+  void copy_to_operands(exprt expr);
+  void copy_to_operands(exprt e1, exprt e2);
+  void copy_to_operands(exprt e1, exprt e2, exprt e3);
 
   // the following are deprecated -- use constructors instead
   void make_typecast(const typet &_type);

Diff for: src/util/irep.cpp

@@ -57,14 +57,14 @@ const irept &get_nil_irep()
 
 void irept::move_to_named_sub(const irep_namet &name, irept &irep)
 {
-  add(name).swap(irep);
+  add(name, std::move(irep));
   irep.clear();
 }
 
 void irept::move_to_sub(irept &irep)
 {
-  get_sub().push_back(get_nil_irep());
-  get_sub().back().swap(irep);
+  write(true).sub.push_back(std::move(irep));
+  irep.clear();
 }
 
 const irep_idt &irept::get(const irep_namet &name) const
@@ -121,13 +121,13 @@ long long irept::get_long_long(const irep_namet &name) const
 
 void irept::set(const irep_namet &name, const long long value)
 {
-  add(name).id(std::to_string(value));
+  set(name, std::to_string(value));
 }
 
 void irept::remove(const irep_namet &name)
 {
-  named_subt &s=
-    is_comment(name)?get_comments():get_named_sub();
+  named_subt &s =
+    is_comment(name) ? write(true).comments : write(true).named_sub;
 
   #ifdef SUB_IS_LIST
   named_subt::iterator it=named_subt_lower_bound(s, name);
@@ -160,47 +160,23 @@ const irept &irept::find(const irep_namet &name) const
   return it->second;
 }
 
-irept &irept::add(const irep_namet &name)
+irept &irept::add(const irep_namet &name, bool mark_sharable)
 {
-  named_subt &s=
-    is_comment(name)?get_comments():get_named_sub();
+  named_subt &s =
+    is_comment(name)
+      ? write(mark_sharable).comments : write(mark_sharable).named_sub;
 
   #ifdef SUB_IS_LIST
-  named_subt::iterator it=named_subt_lower_bound(s, name);
-
-  if(it==s.end() ||
-     it->first!=name)
-    it=s.insert(it, std::make_pair(name, irept()));
 
-  return it->second;
-  #else
-  return s[name];
-  #endif
-}
-
-irept &irept::add(const irep_namet &name, const irept &irep)
-{
-  named_subt &s=
-    is_comment(name)?get_comments():get_named_sub();
-
-  #ifdef SUB_IS_LIST
   named_subt::iterator it=named_subt_lower_bound(s, name);
-
-  if(it==s.end() ||
-     it->first!=name)
-    it=s.insert(it, std::make_pair(name, irep));
-  else
-    it->second=irep;
-
+  if(it == s.end() || it->first != name)
+    it = s.emplace(it, name, irept());
   return it->second;
+
   #else
-  std::pair<named_subt::iterator, bool> entry=
-    s.insert(std::make_pair(name, irep));
 
-  if(!entry.second)
-    entry.first->second=irep;
+  return s[name];
 
-  return entry.first->second;
   #endif
 }
 

Diff for: src/util/irep.h

@@ -125,8 +125,14 @@ class irept
   }
 
   const irept &find(const irep_namet &name) const;
-  irept &add(const irep_namet &name);
-  irept &add(const irep_namet &name, const irept &irep);
+  irept &add(const irep_namet &name)
+  {
+    return add(name, false);
+  }
+  void add(const irep_namet &name, irept irep)
+  {
+    add(name, true) = std::move(irep);
+  }
 
   const std::string &get_string(const irep_namet &name) const
   {
@@ -141,7 +147,9 @@ class irept
   long long get_long_long(const irep_namet &name) const;
 
   void set(const irep_namet &name, const irep_idt &value)
-  { add(name).id(value); }
+  {
+    add(name, true).id(value);
+  }
   void set(const irep_namet &name, const irept &irep)
   { add(name, irep); }
   void set(const irep_namet &name, const long long value);
@@ -176,6 +184,16 @@ class irept
     return write(false).sub;
   }
   const subt &get_sub() const { return read().sub; }
+  subt::size_type get_sub_size() const
+  {
+    return read().sub.size();
+  }
+  void reserve_sub(subt::size_type n)
+  {
+#ifndef USE_LIST
+    write(true).sub.reserve(n);
+#endif
+  }
   named_subt &get_named_sub()
   {
     return write(false).named_sub;
@@ -199,6 +217,20 @@ class irept
   { return !name.empty() && name[0]=='#'; }
 
 private:
+  /// Adds a new irept to the comments or named_sub collection with the given
+  /// name or retrieves the existing irept with the matching name
+  /// \remarks
+  /// If name starts with a hash symbol ('#') then the comments collection is
+  /// used, otherwise the named_sub collection is used
+  /// If the reference returned by this call is potentially held long enough
+  /// that a copy of this irept could be made before it is disposed of then you
+  /// must pass false for mark_sharable to ensure safe behaviour.
+  /// \param name: The name of the irept to add/retrieve
+  /// \param mark_sharable: If false then future copies of this irept will
+  /// not use sharing
+  /// \returns The added or retrieved irept
+  irept &add(const irep_namet &name, bool mark_sharable);
+
   class dt
 #ifdef SHARING
     : public copy_on_write_pointeet<unsigned>

Diff for: unit/util/irep_sharing.cpp

@@ -5,7 +5,7 @@
 #include <testing-utils/catch.hpp>
 #include <util/expr.h>
 
-SCENARIO("irept_sharing", "[!mayfail][core][utils][irept]")
+SCENARIO("irept_sharing", "[core][utils][irept]")
 {
   GIVEN("A sample expression created with move_to_operands and a copy")
   {