X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=snapshot-interface.cc;h=072c1f959ac07c256129248174665a33fb5e7b30;hp=10bd809779d7651f642e4b7918ebc7a260bd1d9b;hb=305c314f6e2e34396053c3974e3be3796a16e4e1;hpb=72e4ac7e09dac04744d8e1b4d8166a23fd197786 diff --git a/snapshot-interface.cc b/snapshot-interface.cc index 10bd809..072c1f9 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -1,91 +1,121 @@ -#define MYBINARYNAME "model" -#define MYLIBRARYNAME "libmodel.so" -#define MYALLOCNAME "libmymemory.so" -#define PROCNAME "/proc/*/maps" -#define REPLACEPOS 6 -#define PAGESIZE 4096 #include "snapshot-interface.h" +#include "snapshot.h" #include #include #include #include #include #include +#include #include +#include +#include +#include +#include "common.h" + + +#define MYBINARYNAME "model" +#define MYLIBRARYNAME "libmodel.so" +#define MAPFILE_FORMAT "/proc/%d/maps" + +SnapshotStack * snapshotObject; -snapshotStack * snapshotObject; +#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; -/*This looks like it might leak memory... Subramanian should fix this. */ + sprintf(execname, "vmmap -interleaved %d", pid); + map=popen(execname, "r"); -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 ); + 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; + int size; + void *begin, *end; + + //Skip out at the end of the section + if (buf[0]=='\n') + break; + + sscanf(buf, "%22s %p-%p [%5dK] %c%c%c/%c%c%c SM=%3s %200s\n", type, &begin, &end, &size, &r, &w, &x, &mr, &mw, &mx, smstr, regionname); + + if (w == 'w' && (strstr(regionname, MYBINARYNAME) || strstr(regionname, MYLIBRARYNAME))) { + size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE; + if (len != 0) + addMemoryRegionToSnapShot(begin, len); } } + pclose(map); } -void SnapshotGlobalSegments(){ - MyString fn = PROCNAME; - static char sProcessSize[ 12 ] = { 0 }; - std::pair< const char *, bool > dataSect[ 3 ]; - dataSect[ 0 ] = std::make_pair( MYBINARYNAME, false ); - dataSect[ 1 ] = std::make_pair( MYLIBRARYNAME, false ); - dataSect[ 2 ] = std::make_pair( MYALLOCNAME, false ); - static pid_t sProcID = 0; - if( 0 == sProcID ) { - sProcID = getpid(); - sprintf( sProcessSize, "%d", sProcID ); +#else +/** 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], filename[100]; + FILE *map; + + sprintf(filename, MAPFILE_FORMAT, pid); + map = fopen(filename, "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 ); - } + 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, MYBINARYNAME) || strstr(regionname, MYLIBRARYNAME))) { + size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE; + if (len != 0) + addMemoryRegionToSnapShot(begin, len); + DEBUG("%45s: %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(){ +SnapshotStack::SnapshotStack(){ SnapshotGlobalSegments(); stack=NULL; } - -snapshotStack::~snapshotStack(){ + +SnapshotStack::~SnapshotStack(){ } - -int snapshotStack::backTrackBeforeStep(int seqindex) { + + +/** 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) { while(true) { if (stack->index<=seqindex) { //have right entry @@ -93,13 +123,14 @@ int snapshotStack::backTrackBeforeStep(int seqindex) { return stack->index; } struct stackEntry *tmp=stack; - free(tmp); stack=stack->next; + MYFREE(tmp); } } -void snapshotStack::snapshotStep(int seqindex) { - struct stackEntry *tmp=(struct stackEntry *)malloc(sizeof(struct stackEntry)); +/** This method takes a snapshot at the given sequence number. */ +void SnapshotStack::snapshotStep(int seqindex) { + struct stackEntry *tmp=(struct stackEntry *)MYMALLOC(sizeof(struct stackEntry)); tmp->next=stack; tmp->index=seqindex; tmp->snapshotid=takeSnapshot();