-#include "snapshot-interface.h"
-#include <iostream>
-#include <fstream>
+#include <stdlib.h>
#include <unistd.h>
-#include <sys/types.h>
-#include <sstream>
#include <cstring>
-#include <string>
-#include <cassert>
-#include <vector>
-#include <utility>
+#include <inttypes.h>
+
+#include "snapshot-interface.h"
+#include "snapshot.h"
+#include "common.h"
+#include "mymemory.h"
+#include "stl-model.h"
+/* MYBINARYNAME only works because our pathname usually includes 'model' (e.g.,
+ * /.../model-checker/test/userprog.o) */
#define MYBINARYNAME "model"
-#define MYLIBRARYNAME "libmodel.so"
-#define PROCNAME "/proc/*/maps"
-#define REPLACEPOS 6
-#define PAGESIZE 4096
+#define MAPFILE "/proc/self/maps"
+
+struct snapshot_entry {
+ snapshot_entry(snapshot_id id, int idx) : snapshotid(id), index(idx) { }
+ snapshot_id snapshotid;
+ int index;
+ MEMALLOC
+};
-typedef std::basic_string<char, std::char_traits<char>, MyAlloc<char> > MyString;
+class SnapshotStack {
+ public:
+ int backTrackBeforeStep(int seq_index);
+ void snapshotStep(int seq_index);
-SnapshotStack * snapshotObject;
+ MEMALLOC
+ private:
+ ModelVector<struct snapshot_entry> stack;
+};
-/*This looks like it might leak memory... Subramanian should fix this. */
+static SnapshotStack *snap_stack;
-typedef std::basic_stringstream< char, std::char_traits< char >, MyAlloc< char > > MyStringStream;
-std::vector< MyString, MyAlloc< MyString> > splitString( MyString input, char delim ){
- std::vector< MyString, MyAlloc< MyString > > splits;
- MyStringStream ss( input );
- MyString item;
- while( std::getline( ss, item, delim ) ){
- splits.push_back( item );
+#ifdef MAC
+/** The SnapshotGlobalSegments function computes the memory regions
+ * that may contain globals and then configures the snapshotting
+ * library to snapshot them.
+ */
+static void SnapshotGlobalSegments()
+{
+ int pid = getpid();
+ char buf[9000], execname[100];
+ FILE *map;
+
+ sprintf(execname, "vmmap -interleaved %d", pid);
+ map = popen(execname, "r");
+
+ if (!map) {
+ perror("popen");
+ exit(EXIT_FAILURE);
}
- return splits;
-}
-bool checkPermissions( MyString permStr ){
- return permStr.find("w") != MyString::npos;
-}
-static void takeSegmentSnapshot( const MyString & lineText ){
- std::vector< MyString, MyAlloc< MyString > > firstSplit = splitString( lineText, ' ' );
- if( checkPermissions( firstSplit[ 1 ] ) ){
- std::vector< MyString, MyAlloc< MyString > > secondSplit = splitString( firstSplit[ 0 ], '-' );
- size_t val1 = 0, val2 = 0;
- sscanf( secondSplit[ 0 ].c_str(), "%zx", &val1 );
- sscanf( secondSplit[ 1 ].c_str(), "%zx", &val2 );
- size_t len = ( val2 - val1 ) / PAGESIZE;
- if( 0 != len ){
- addMemoryRegionToSnapShot( ( void * )val1, len );
+ /* Wait for correct part */
+ while (fgets(buf, sizeof(buf), map)) {
+ if (strstr(buf, "==== regions for process"))
+ break;
+ }
+
+ while (fgets(buf, sizeof(buf), map)) {
+ char regionname[200] = "";
+ char type[23];
+ char smstr[23];
+ char r, w, x;
+ char mr, mw, mx;
+ void *begin, *end;
+
+ //Skip out at the end of the section
+ if (buf[0] == '\n')
+ break;
+
+ sscanf(buf, "%22s %p-%p", type, &begin, &end);
+
+ char * secondpart = strstr(buf, "]");
+
+ sscanf(&secondpart[2], "%c%c%c/%c%c%c SM=%3s %200s\n", &r, &w, &x, &mr, &mw, &mx, smstr, regionname);
+ if (w == 'w' && strstr(regionname, MYBINARYNAME)) {
+ size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
+ if (len != 0)
+ snapshot_add_memory_region(begin, len);
}
}
+ pclose(map);
+}
+#else
+
+static void get_binary_name(char *buf, size_t len)
+{
+ ssize_t size = readlink("/proc/self/exe", buf, len);
+ if (size < 0) {
+ perror("readlink");
+ exit(EXIT_FAILURE);
+ }
+
+ /* Terminate string */
+ if ((size_t)size > len)
+ size = len;
+ buf[size] = '\0';
}
-void SnapshotGlobalSegments(){
- MyString fn = PROCNAME;
- static char sProcessSize[ 12 ] = { 0 };
- std::pair< const char *, bool > dataSect[ 2 ];
- dataSect[ 0 ] = std::make_pair( MYBINARYNAME, false );
- dataSect[ 1 ] = std::make_pair( MYLIBRARYNAME, false );
- static pid_t sProcID = 0;
- if( 0 == sProcID ) {
- sProcID = getpid();
- sprintf( sProcessSize, "%d", sProcID );
+
+/** The SnapshotGlobalSegments function computes the memory regions
+ * that may contain globals and then configures the snapshotting
+ * library to snapshot them.
+ */
+static void SnapshotGlobalSegments()
+{
+ char buf[9000];
+ char binary_name[800];
+ FILE *map;
+
+ map = fopen(MAPFILE, "r");
+ if (!map) {
+ perror("fopen");
+ exit(EXIT_FAILURE);
}
- fn.replace( REPLACEPOS, 1, sProcessSize );
- std::ifstream procName( fn.c_str() );
- if( procName.is_open() ){
- MyString line;
- while( procName.good() ){
- getline( procName, line );
- int i = 0;
- for( i = 0; i < 3; ++i ){
- if( MyString::npos != line.find( dataSect[ i ].first ) ) break;
- }
- if( i >= 3 || dataSect[ i ].second == true ) continue;
- dataSect[ i ].second = true;
- if( !procName.good() )return;
- getline( procName, line );
- takeSegmentSnapshot( line );
- }
+ get_binary_name(binary_name, sizeof(binary_name));
+ while (fgets(buf, sizeof(buf), map)) {
+ char regionname[200] = "";
+ char r, w, x, p;
+ void *begin, *end;
+
+ sscanf(buf, "%p-%p %c%c%c%c %*x %*x:%*x %*u %200s\n", &begin, &end, &r, &w, &x, &p, regionname);
+ if (w == 'w' && strstr(regionname, binary_name)) {
+ size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
+ if (len != 0)
+ snapshot_add_memory_region(begin, len);
+ DEBUG("%55s: %18p - %18p\t%c%c%c%c\n", regionname, begin, end, r, w, x, p);
+ }
}
+ fclose(map);
}
+#endif
-//class definition of SnapshotStack.....
-//declaration of constructor....
-SnapshotStack::SnapshotStack(){
- SnapshotGlobalSegments();
- stack=NULL;
+/** This method returns to the last snapshot before the inputted
+ * sequence number. This function must be called from the model
+ * checking thread and not from a snapshotted stack.
+ * @param seqindex is the sequence number to rollback before.
+ * @return is the sequence number we actually rolled back to.
+ */
+int SnapshotStack::backTrackBeforeStep(int seqindex)
+{
+ int i;
+ for (i = (int)stack.size() - 1; i >= 0; i++)
+ if (stack[i].index <= seqindex)
+ break;
+ else
+ stack.pop_back();
+
+ ASSERT(i >= 0);
+ snapshot_roll_back(stack[i].snapshotid);
+ return stack[i].index;
}
-
-SnapshotStack::~SnapshotStack(){
+
+/** This method takes a snapshot at the given sequence number. */
+void SnapshotStack::snapshotStep(int seqindex)
+{
+ stack.push_back(snapshot_entry(take_snapshot(), seqindex));
}
-
-int SnapshotStack::backTrackBeforeStep(int seqindex) {
- while(true) {
- if (stack->index<=seqindex) {
- //have right entry
- rollBack(stack->snapshotid);
- return stack->index;
- }
- struct stackEntry *tmp=stack;
- MYFREE(tmp);
- stack=stack->next;
- }
+
+void snapshot_stack_init()
+{
+ snap_stack = new SnapshotStack();
+ SnapshotGlobalSegments();
+}
+
+void snapshot_record(int seq_index)
+{
+ snap_stack->snapshotStep(seq_index);
}
-void SnapshotStack::snapshotStep(int seqindex) {
- struct stackEntry *tmp=(struct stackEntry *)MYMALLOC(sizeof(struct stackEntry));
- tmp->next=stack;
- tmp->index=seqindex;
- tmp->snapshotid=takeSnapshot();
- stack=tmp;
+int snapshot_backtrack_before(int seq_index)
+{
+ return snap_stack->backTrackBeforeStep(seq_index);
}
projects / model-checker.git / blobdiff