Unit test to check that irept implements sharing

Separately test irept and exprt, where the latter are expected to have the very
same behaviour.

Author: NathanJPhillips

unit/Makefile

@@ -39,6 +39,7 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_refinement/union_find_replace.cpp \
        util/expr_cast/expr_cast.cpp \
        util/expr_iterator.cpp \
+       util/irep_sharing.cpp \
        util/message.cpp \
        util/parameter_indices.cpp \
        util/simplify_expr.cpp \

unit/util/irep_sharing.cpp

@@ -0,0 +1,124 @@
+// Copyright 2018 DiffBlue Limited. All Rights Reserved.
+
+/// \file Tests that irep sharing works correctly
+
+#include <testing-utils/catch.hpp>
+#include <util/expr.h>
+
+#ifdef SHARING
+
+SCENARIO("irept_sharing", "[core][utils][irept]")
+{
+  GIVEN("An irept created with move_to_sub and a copy")
+  {
+    irept test_irep;
+    irept test_subirep;
+    irept test_subsubirep(ID_1);
+    test_subirep.move_to_sub(test_subsubirep);
+    test_irep.move_to_sub(test_subirep);
+    THEN("Calling read() on a copy should return object with the same address")
+    {
+      irept irep = test_irep;
+      REQUIRE(&irep.read() == &test_irep.read());
+    }
+    THEN("Getting a reference to an operand in a copy should break sharing")
+    {
+      irept irep = test_irep;
+      irept &operand = irep.get_sub()[0];
+      REQUIRE(&irep.read() != &test_irep.read());
+      operand = irept(ID_0);
+      REQUIRE(irep.get_sub()[0].id() != test_irep.get_sub()[0].id());
+    }
+    THEN(
+      "Getting a reference to an operand in the original should break sharing")
+    {
+      irept irep = test_irep;
+      irept &operand = test_irep.get_sub()[0];
+      REQUIRE(&irep.read() != &test_irep.read());
+      operand = irept(ID_0);
+      REQUIRE(irep.get_sub()[0].id() != test_irep.get_sub()[0].id());
+    }
+    THEN("Changing an id in the original should break sharing")
+    {
+      irept irep = test_irep;
+      test_irep.id(ID_1);
+      REQUIRE(&irep.read() != &test_irep.read());
+      REQUIRE(irep.id() != test_irep.id());
+    }
+    // the following would be desirable for irept to be safe, but we know it
+    // presently does not hold; see #1855 for a proposed solution
+    // THEN("Holding a reference to an operand should prevent sharing")
+    // {
+    //   irept &operand = test_irep.get_sub()[0];
+    //   irept irep = test_irep;
+    //   REQUIRE(&irep.read() != &test_irep.read());
+    //   operand = irept(ID_0);
+    //   REQUIRE(irep.get_sub()[0].id() != test_irep.get_sub()[0].id());
+    // }
+    THEN("Changing an id should not prevent sharing")
+    {
+      test_irep.id(ID_1);
+      irept irep = test_irep;
+      REQUIRE(&irep.read() == &test_irep.read());
+    }
+  }
+}
+
+SCENARIO("exprt_sharing", "[core][utils][exprt]")
+{
+  GIVEN("A sample expression created with move_to_operands and a copy")
+  {
+    exprt test_expr;
+    exprt test_subexpr;
+    exprt test_subsubexpr(ID_1);
+    test_subexpr.move_to_operands(test_subsubexpr);
+    test_expr.move_to_operands(test_subexpr);
+    THEN("Calling read() on a copy should return object with the same address")
+    {
+      exprt expr = test_expr;
+      REQUIRE(&expr.read() == &test_expr.read());
+    }
+    THEN("Getting a reference to an operand in a copy should break sharing")
+    {
+      exprt expr = test_expr;
+      exprt &operand = expr.op0();
+      REQUIRE(&expr.read() != &test_expr.read());
+      operand = exprt(ID_0);
+      REQUIRE(expr.op0().id() != test_expr.op0().id());
+    }
+    THEN(
+      "Getting a reference to an operand in the original should break sharing")
+    {
+      exprt expr = test_expr;
+      exprt &operand = test_expr.op0();
+      REQUIRE(&expr.read() != &test_expr.read());
+      operand = exprt(ID_0);
+      REQUIRE(expr.op0().id() != test_expr.op0().id());
+    }
+    THEN("Changing an id in the original should break sharing")
+    {
+      exprt expr = test_expr;
+      test_expr.id(ID_1);
+      REQUIRE(&expr.read() != &test_expr.read());
+      REQUIRE(expr.id() != test_expr.id());
+    }
+    // the following would be desirable for irept to be safe, but we know it
+    // presently does not hold; see #1855 for a proposed solution
+    // THEN("Holding a reference to an operand should 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());
+    // }
+    THEN("Changing an id should not prevent sharing")
+    {
+      test_expr.id(ID_1);
+      exprt expr = test_expr;
+      REQUIRE(&expr.read() == &test_expr.read());
+    }
+  }
+}
+
+#endif