[Unit Tests] Reenable `top_scope_context_obj` (#6892)

Fixes #6047. The test was disabled because ASan found a use-after-free
due to an object allocated in the top scope being destroyed after the
scope (see #2607 for a detailed explanation). At first, the plan was to
add support for this use case. However, we have decided that we
currently don't need support for this feature and added a guard against
it (#6082). This commit reenables the test but changes it to destroy the
object allocated in the top level scope before the corresponding level
is popped. It additionally adds a test of the guard from #6082.

diff --git a/test/unit/context/context_black.cpp b/test/unit/context/context_black.cpp
index 316aa7d460f211dda709d10bba55995e5fb1bdec..28bd1438c1638c130e91bcf00ccef096a74f116a 100644 (file)
--- a/test/unit/context/context_black.cpp
+++ b/test/unit/context/context_black.cpp
@@ -198,8 +198,6 @@ TEST_F(TestContextBlack, pre_post_notify)
   d_context.reset(nullptr);
 }
 
-// TODO: reenable after #2607 is merged in (issue 6047)
-#if 0
 TEST_F(TestContextBlack, top_scope_context_obj)
 {
   // this test's implementation is based on the fact that a
@@ -211,33 +209,60 @@ TEST_F(TestContextBlack, top_scope_context_obj)
 
   d_context->push();
 
-  MyContextObj x(true, d_context.get(), n);
-  MyContextObj y(false, d_context.get(), n);
+  MyContextObj x(false, d_context.get(), n);
+  {
+    MyContextObj y(true, d_context.get(), n);
 
-  ASSERT_EQ(x.d_nsaves, 0);
-  ASSERT_EQ(y.d_nsaves, 0);
+    ASSERT_EQ(x.d_nsaves, 0);
+    ASSERT_EQ(y.d_nsaves, 0);
 
-  x.makeCurrent();
-  y.makeCurrent();
+    x.makeCurrent();
+    y.makeCurrent();
 
-  ASSERT_EQ(x.d_nsaves, 0);
-  ASSERT_EQ(y.d_nsaves, 1);
+    ASSERT_EQ(x.d_nsaves, 1);
+    ASSERT_EQ(y.d_nsaves, 0);
 
-  d_context->push();
+    d_context->push();
 
-  x.makeCurrent();
-  y.makeCurrent();
+    x.makeCurrent();
+    y.makeCurrent();
 
-  ASSERT_EQ(x.d_nsaves, 1);
-  ASSERT_EQ(y.d_nsaves, 2);
+    ASSERT_EQ(x.d_nsaves, 2);
+    ASSERT_EQ(y.d_nsaves, 1);
+
+    d_context->pop();
+
+    // `y` is invalid below the first level because it was allocated in the top
+    // scope. We have to make sure to destroy it before the next pop.
+  }
 
   d_context->pop();
-  d_context->pop();
 
-  ASSERT_EQ(x.d_nsaves, 1);
-  ASSERT_EQ(y.d_nsaves, 2);
+  ASSERT_EQ(x.d_nsaves, 2);
+}
+
+TEST_F(TestContextBlack, detect_invalid_obj)
+{
+  MyContextNotifyObj n(d_context.get(), true);
+
+  {
+    // Objects allocated at the bottom scope are allowed to outlive the scope
+    // that they have been allocated in.
+    d_context->push();
+    MyContextObj x(false, d_context.get(), n);
+    d_context->pop();
+  }
+
+  ASSERT_DEATH(
+      {
+        // Objects allocated at the top scope are not allowed to outlive the
+        // scope that they have been allocated in.
+        d_context->push();
+        MyContextObj y(true, d_context.get(), n);
+        d_context->pop();
+      },
+      "d_pScope != nullptr");
 }
-#endif
 
 }  // namespace test
 }  // namespace cvc5