minor fixes to lcov build target, better contextobj testing

1 files changed, 153 insertions, 14 deletions

diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h
index 37c94aaad..46d01946b 100644
--- a/test/unit/context/context_black.h
+++ b/test/unit/context/context_black.h
@@ -26,6 +26,69 @@ using namespace std;
 using namespace CVC4;
 using namespace CVC4::context;
 
+struct MyContextNotifyObj : public ContextNotifyObj {
+  int nCalls;
+
+  MyContextNotifyObj(Context* context, bool pre) :
+    ContextNotifyObj(context, pre),
+    nCalls(0) {
+  }
+
+  void notify() {
+    ++nCalls;
+  }
+};
+
+class MyContextObj : public ContextObj {
+  MyContextNotifyObj& notify;
+
+public:
+  int nCalls;
+  int nSaves;
+
+private:
+  MyContextObj(const MyContextObj& other) :
+    ContextObj(other),
+    notify(other.notify),
+    nCalls(0),
+    nSaves(0) {
+  }
+
+public:
+
+  MyContextObj(Context* context, MyContextNotifyObj& n) :
+    ContextObj(context),
+    notify(n),
+    nCalls(0),
+    nSaves(0) {
+  }
+
+  MyContextObj(bool topScope, Context* context, MyContextNotifyObj& n) :
+    ContextObj(topScope, context),
+    notify(n),
+    nCalls(0),
+    nSaves(0) {
+  }
+
+  ~MyContextObj() {
+    destroy();
+  }
+
+  ContextObj* save(ContextMemoryManager* pcmm) {
+    ++nSaves;
+    return new(pcmm) MyContextObj(*this);
+  }
+
+  void restore(ContextObj* contextObj) {
+    nCalls = notify.nCalls;
+  }
+
+  void makeCurrent() {
+    ContextObj::makeCurrent();
+  }
+};
+
+
 class ContextBlack : public CxxTest::TestSuite {
 private:
 
@@ -61,21 +124,14 @@ public:
     i = 5;
   }
 
-  void testPreNotify() {
-    struct MyContextNotifyObj : ContextNotifyObj {
-      int nCalls;
-
-      MyContextNotifyObj(Context* context, bool pre) :
-        ContextNotifyObj(context, pre),
-        nCalls(0) {
-      }
+  void testPrePostNotify() {
+    // This is tricky; we want to detect if pre- and post-notifies are
+    // done correctly.  For that, we have to use a special ContextObj,
+    // since that's the only thing that runs between pre- and post-.
 
-      void notify() {
-        ++nCalls;
-      }
-    } a(d_context, true), b(d_context, false);
+    MyContextNotifyObj a(d_context, true), b(d_context, false);
 
-    {
+    try {
       MyContextNotifyObj c(d_context, true), d(d_context, false);
 
       TS_ASSERT_EQUALS(a.nCalls, 0);
@@ -83,14 +139,45 @@ public:
       TS_ASSERT_EQUALS(c.nCalls, 0);
       TS_ASSERT_EQUALS(d.nCalls, 0);
 
+      MyContextObj w(d_context, a);
+      MyContextObj x(d_context, b);
+      MyContextObj y(d_context, c);
+      MyContextObj z(d_context, d);
+
       d_context->push();
+
+      w.makeCurrent();
+      x.makeCurrent();
+      y.makeCurrent();
+      z.makeCurrent();
+
+      TS_ASSERT_EQUALS(a.nCalls, 0);
+      TS_ASSERT_EQUALS(b.nCalls, 0);
+      TS_ASSERT_EQUALS(c.nCalls, 0);
+      TS_ASSERT_EQUALS(d.nCalls, 0);
+
+      TS_ASSERT_EQUALS(w.nCalls, 0);
+      TS_ASSERT_EQUALS(x.nCalls, 0);
+      TS_ASSERT_EQUALS(y.nCalls, 0);
+      TS_ASSERT_EQUALS(z.nCalls, 0);
+
       d_context->push();
 
+      w.makeCurrent();
+      x.makeCurrent();
+      y.makeCurrent();
+      z.makeCurrent();
+
       TS_ASSERT_EQUALS(a.nCalls, 0);
       TS_ASSERT_EQUALS(b.nCalls, 0);
       TS_ASSERT_EQUALS(c.nCalls, 0);
       TS_ASSERT_EQUALS(d.nCalls, 0);
 
+      TS_ASSERT_EQUALS(w.nCalls, 0);
+      TS_ASSERT_EQUALS(x.nCalls, 0);
+      TS_ASSERT_EQUALS(y.nCalls, 0);
+      TS_ASSERT_EQUALS(z.nCalls, 0);
+
       d_context->pop();
 
       TS_ASSERT_EQUALS(a.nCalls, 1);
@@ -98,17 +185,69 @@ public:
       TS_ASSERT_EQUALS(c.nCalls, 1);
       TS_ASSERT_EQUALS(d.nCalls, 1);
 
+      TS_ASSERT_EQUALS(w.nCalls, 1);
+      TS_ASSERT_EQUALS(x.nCalls, 0);
+      TS_ASSERT_EQUALS(y.nCalls, 1);
+      TS_ASSERT_EQUALS(z.nCalls, 0);
+
       d_context->pop();
 
       TS_ASSERT_EQUALS(a.nCalls, 2);
       TS_ASSERT_EQUALS(b.nCalls, 2);
       TS_ASSERT_EQUALS(c.nCalls, 2);
       TS_ASSERT_EQUALS(d.nCalls, 2);
+
+      TS_ASSERT_EQUALS(w.nCalls, 2);
+      TS_ASSERT_EQUALS(x.nCalls, 1);
+      TS_ASSERT_EQUALS(y.nCalls, 2);
+      TS_ASSERT_EQUALS(z.nCalls, 1);
+    } catch(Exception& e) {
+      cerr << e.toString() << endl;
+      TS_FAIL("Exception thrown from test");
     }
 
-    // we do this to get full code coverage of destruction paths
+    // we do this (together with the { } block above) to get full code
+    // coverage of destruction paths; a and b haven't been destructed
+    // yet, here.
     delete d_context;
 
     d_context = NULL;
   }
+
+  void testTopScopeContextObj() {
+    // this test's implementation is based on the fact that a
+    // ContextObj allocated primordially "in the top scope" (first arg
+    // to ctor is "true"), doesn't get updated if you immediately call
+    // makeCurrent().
+
+    MyContextNotifyObj n(d_context, true);
+
+    d_context->push();
+
+    MyContextObj x(true, d_context, n);
+    MyContextObj y(false, d_context, n);
+
+    TS_ASSERT_EQUALS(x.nSaves, 0);
+    TS_ASSERT_EQUALS(y.nSaves, 0);
+
+    x.makeCurrent();
+    y.makeCurrent();
+
+    TS_ASSERT_EQUALS(x.nSaves, 0);
+    TS_ASSERT_EQUALS(y.nSaves, 1);
+
+    d_context->push();
+
+    x.makeCurrent();
+    y.makeCurrent();
+
+    TS_ASSERT_EQUALS(x.nSaves, 1);
+    TS_ASSERT_EQUALS(y.nSaves, 2);
+
+    d_context->pop();
+    d_context->pop();
+
+    TS_ASSERT_EQUALS(x.nSaves, 1);
+    TS_ASSERT_EQUALS(y.nSaves, 2);
+  }
 };