snapshot: turn C++ interface into C interface
authorBrian Norris <banorris@uci.edu>
Thu, 3 Jan 2013 19:37:51 +0000 (11:37 -0800)
committerBrian Norris <banorris@uci.edu>
Thu, 3 Jan 2013 19:37:51 +0000 (11:37 -0800)
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).

main.cc
model.cc
snapshot-interface.cc
snapshot-interface.h

diff --git a/main.cc b/main.cc
index a111572..6b9cb90 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;
 
index 84c4268..98df8f3 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 */
index 82f3e13..c33b8d4 100644 (file)
@@ -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) */
 #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);
+}
index ecc60ec..b024e5a 100644 (file)
@@ -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