snapshot: turn C++ interface into C interface

We don't need all this 'class' structure exposed as an interface; we
only use 3 simple functions (one of which probably can be removed).

diff --git a/main.cc b/main.cc
index a1115721436706f2007d23cd7fc4c4733f09c28f..6b9cb9054e7819496c9a9c6f8d652a45d6754abd 100644 (file)
--- a/main.cc
+++ b/main.cc
@@ -123,11 +123,10 @@ static void model_main()
        //Initialize race detector
        initRaceDetector();
 
-       //Create the singleton SnapshotStack object
-       snapshotObject = new SnapshotStack();
+       snapshot_stack_init();
 
        model = new ModelChecker(params);
-       snapshotObject->snapshotStep(0);
+       snapshot_record(0);
        model->run();
        delete model;
 

diff --git a/model.cc b/model.cc
index 84c42689425f257d594c969df0b758038001ab83..98df8f316106a5f4cce404f4cada60ee35c5898a 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -159,7 +159,7 @@ void ModelChecker::reset_to_initial_state()
        /* Print all model-checker output before rollback */
        fflush(model_out);
 
-       snapshotObject->backTrackBeforeStep(0);
+       snapshot_backtrack_before(0);
 }
 
 /** @return a thread ID for a new Thread */

diff --git a/snapshot-interface.cc b/snapshot-interface.cc
index 82f3e1300b253dfaa06ea8988a19640ae9eaffa2..c33b8d44549aa29de3d1dbdbb71bbf5f7628d8fd 100644 (file)
--- a/snapshot-interface.cc
+++ b/snapshot-interface.cc
@@ -6,6 +6,7 @@
 #include "snapshot-interface.h"
 #include "snapshot.h"
 #include "common.h"
+#include "mymemory.h"
 
 /* MYBINARYNAME only works because our pathname usually includes 'model' (e.g.,
  * /.../model-checker/test/userprog.o) */
@@ -13,7 +14,25 @@
 #define MYLIBRARYNAME "libmodel.so"
 #define MAPFILE "/proc/self/maps"
 
-SnapshotStack *snapshotObject;
+struct stackEntry {
+       struct stackEntry *next;
+       snapshot_id snapshotid;
+       int index;
+};
+
+class SnapshotStack {
+ public:
+       SnapshotStack();
+       ~SnapshotStack();
+       int backTrackBeforeStep(int seq_index);
+       void snapshotStep(int seq_index);
+
+       MEMALLOC
+ private:
+       struct stackEntry *stack;
+};
+
+static SnapshotStack *snapshotObject;
 
 #ifdef MAC
 /** The SnapshotGlobalSegments function computes the memory regions
@@ -145,3 +164,19 @@ void SnapshotStack::snapshotStep(int seqindex)
        tmp->snapshotid = take_snapshot();
        stack = tmp;
 }
+
+
+void snapshot_stack_init()
+{
+       snapshotObject = new SnapshotStack();
+}
+
+void snapshot_record(int seq_index)
+{
+       snapshotObject->snapshotStep(seq_index);
+}
+
+int snapshot_backtrack_before(int seq_index)
+{
+       return snapshotObject->backTrackBeforeStep(seq_index);
+}

diff --git a/snapshot-interface.h b/snapshot-interface.h
index ecc60ec6453a9ca4991c92e27d248622a201b7c5..b024e5a83a06300eb0e7a95aeee4f9f326765995 100644 (file)
--- a/snapshot-interface.h
+++ b/snapshot-interface.h
@@ -2,10 +2,8 @@
  *  @brief C++ layer on top of snapshotting system.
  */
 
-
 #ifndef __SNAPINTERFACE_H
 #define __SNAPINTERFACE_H
-#include "mymemory.h"
 
 typedef unsigned int snapshot_id;
 
@@ -14,26 +12,8 @@ void initSnapshotLibrary(unsigned int numbackingpages,
                unsigned int numsnapshots, unsigned int nummemoryregions,
                unsigned int numheappages, VoidFuncPtr entryPoint);
 
-struct stackEntry {
-       struct stackEntry *next;
-       snapshot_id snapshotid;
-       int index;
-};
-
-class SnapshotStack {
- public:
-       SnapshotStack();
-       ~SnapshotStack();
-       int backTrackBeforeStep(int seq_index);
-       void snapshotStep(int seq_index);
-
-       MEMALLOC
- private:
-       struct stackEntry *stack;
-};
-
-/* Not sure what it even means to have more than one snapshot object,
-   so let's just make a global reference to it.*/
+void snapshot_stack_init();
+void snapshot_record(int seq_index);
+int snapshot_backtrack_before(int seq_index);
 
-extern SnapshotStack *snapshotObject;
 #endif