From: Brian Norris <banorris@uci.edu>
Date: Thu, 3 Jan 2013 19:37:51 +0000 (-0800)
Subject: snapshot: turn C++ interface into C interface
X-Git-Tag: oopsla2013~384
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=260b391c9292c9eb48da1033bf4ac1c32ea49f87

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 a111572..6b9cb90 100644
--- 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 84c4268..98df8f3 100644
--- 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 82f3e13..c33b8d4 100644
--- 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 ecc60ec..b024e5a 100644
--- 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