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

NathanJPhillips · NathanJPhillips · commit dd5ab8fa39ca · 2018-03-29T09:24:14.000+01:00
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.
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
@@ -21,64 +21,40 @@ Author: Daniel Kroening, kroening@kroening.com
 
 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)
@@ -105,7 +81,7 @@ void exprt::make_not()
 
   if(id()==ID_not && operands().size()==1)
   {
-    new_expr.swap(operands().front());
+    new_expr.swap(op0());
   }
   else
   {
diff --git a/src/util/expr.h b/src/util/expr.h
@@ -93,17 +93,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 --git a/src/util/irep.cpp b/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 --git a/src/util/irep.h b/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 --git a/unit/util/irep_sharing.cpp b/unit/util/irep_sharing.cpp
@@ -7,7 +7,7 @@
 
 #ifdef SHARING
 
-SCENARIO("irept_sharing_trade_offs", "[!mayfail][core][utils][irept]")
+SCENARIO("irept_sharing", "[core][utils][irept]")
 {
   GIVEN("An irept created with move_to_sub")
   {
@@ -21,35 +21,6 @@ SCENARIO("irept_sharing_trade_offs", "[!mayfail][core][utils][irept]")
       irept irep = test_irep;
       REQUIRE(&irep.read() == &test_irep.read());
     }
-    THEN("Changing subs in the original using a reference taken before "
-      "copying should not change them in the copy")
-    {
-      irept &sub = test_irep.get_sub()[0];
-      irept irep = test_irep;
-      sub.id(ID_0);
-      REQUIRE(test_irep.get_sub()[0].id() == ID_0);
-      REQUIRE(irep.get_sub()[0].id() == ID_1);
-    }
-    THEN("Holding a reference to a sub should not prevent sharing")
-    {
-      irept &sub = test_irep.get_sub()[0];
-      irept irep = test_irep;
-      REQUIRE(&irep.read() == &test_irep.read());
-      sub = irept(ID_0);
-      REQUIRE(irep.get_sub()[0].id() == test_irep.get_sub()[0].id());
-    }
-  }
-}
-
-SCENARIO("irept_sharing", "[core][utils][irept]")
-{
-  GIVEN("An irept created with move_to_sub")
-  {
-    irept test_irep(ID_1);
-    irept test_subirep(ID_1);
-    irept test_subsubirep(ID_1);
-    test_subirep.move_to_sub(test_subsubirep);
-    test_irep.move_to_sub(test_subirep);
     THEN("Copies of a copy should return object with the same address")
     {
       irept irep1 = test_irep;
@@ -69,6 +40,15 @@ SCENARIO("irept_sharing", "[core][utils][irept]")
       REQUIRE(test_irep.get_sub()[0].id() == ID_1);
       REQUIRE(irep.get_sub()[0].id() == ID_0);
     }
+    THEN("Changing subs in the original using a reference taken before "
+      "copying should not change them in the copy")
+    {
+      irept &sub = test_irep.get_sub()[0];
+      irept irep = test_irep;
+      sub.id(ID_0);
+      REQUIRE(test_irep.get_sub()[0].id() == ID_0);
+      REQUIRE(irep.get_sub()[0].id() == ID_1);
+    }
     THEN("Getting a reference to a sub in a copy should break sharing")
     {
       irept irep = test_irep;
@@ -104,7 +84,7 @@ SCENARIO("irept_sharing", "[core][utils][irept]")
 
 #include <util/expr.h>
 
-SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]")
+SCENARIO("exprt_sharing", "[core][utils][exprt]")
 {
   GIVEN("An expression created with move_to_operands")
   {
@@ -118,35 +98,6 @@ SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]")
       exprt expr = test_expr;
       REQUIRE(&expr.read() == &test_expr.read());
     }
-    THEN("Changing operands in the original using a reference taken before "
-      "copying should not change them in the copy")
-    {
-      exprt &operand = test_expr.op0();
-      exprt expr = test_expr;
-      operand.id(ID_0);
-      REQUIRE(test_expr.op0().id() == ID_0);
-      REQUIRE(expr.op0().id() == ID_1);
-    }
-    THEN("Holding a reference to an operand should not prevent sharing")
-    {
-      exprt &operand = test_expr.op0();
-      exprt expr = test_expr;
-      REQUIRE(&expr.read() == &test_expr.read());
-      operand = exprt(ID_0);
-      REQUIRE(expr.op0().id() == test_expr.op0().id());
-    }
-  }
-}
-
-SCENARIO("exprt_sharing", "[core][utils][exprt]")
-{
-  GIVEN("An expression created with move_to_operands")
-  {
-    exprt test_expr(ID_1);
-    exprt test_subexpr(ID_1);
-    exprt test_subsubexpr(ID_1);
-    test_subexpr.move_to_operands(test_subsubexpr);
-    test_expr.move_to_operands(test_subexpr);
     THEN("Copies of a copy should return object with the same address")
     {
       exprt expr1 = test_expr;
@@ -166,6 +117,15 @@ SCENARIO("exprt_sharing", "[core][utils][exprt]")
       REQUIRE(test_expr.op0().id() == ID_1);
       REQUIRE(expr.op0().id() == ID_0);
     }
+    THEN("Changing operands in the original using a reference taken before "
+      "copying should not change them in the copy")
+    {
+      exprt &operand = test_expr.op0();
+      exprt expr = test_expr;
+      operand.id(ID_0);
+      REQUIRE(test_expr.op0().id() == ID_0);
+      REQUIRE(expr.op0().id() == ID_1);
+    }
     THEN("Getting a reference to an operand in a copy should break sharing")
     {
       exprt expr = test_expr;
