Tests to demonstrate irept sharing is broken

Author: NathanJPhillips

Diff for: unit/util/irep_sharing.cpp

@@ -0,0 +1,61 @@
+// Copyright 2018 DiffBlue Limited. All Rights Reserved.
+
+/// \file Tests that irep sharing works correctly
+
+#include <testing-utils/catch.hpp>
+#include <util/expr.h>
+
+SCENARIO("irept_sharing", "[!mayfail][core][utils][irept]")
+{
+  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());
+    }
+    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());
+    }
+  }
+}