X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=snapshot-interface.cc;h=974e436f7210acfdc1035208cb6f736a92d2c79d;hp=e350bc473c35fb48aff42ac4a42e912d4867ffb1;hb=6e5c0bb2359b9fba6160957ffa88974233ba18ac;hpb=700898cdd309acb86dcd275d8b1c34e02d67922e diff --git a/snapshot-interface.cc b/snapshot-interface.cc index e350bc47..974e436f 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -1,65 +1,148 @@ +#include +#include +#include +#include + +#include "snapshot-interface.h" +#include "snapshot.h" +#include "common.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 MYALLOCNAME "libmymemory.so" -#define PROCNAME "/proc/*/maps" -#define REPLACEPOS 6 -#define PAGESIZE 4096 -#include "snapshot-interface.h" -#include -#include -#include -#include -#include -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 ); +#define MAPFILE "/proc/self/maps" + +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; + + sprintf(execname, "vmmap -interleaved %d", pid); + map = popen(execname, "r"); + + if (!map) { + perror("popen"); + exit(EXIT_FAILURE); + } + + /* Wait for correct part */ + while (fgets(buf, sizeof(buf), map)) { + if (strstr(buf, "==== regions for process")) + break; } - return splits; + + 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); } +#else -bool checkPermissions( MyString permStr ){ - return permStr.find("w") != MyString::npos; +static void get_binary_name(char *buf, size_t len) +{ + if (readlink("/proc/self/exe", buf, len) == -1) { + perror("readlink"); + exit(EXIT_FAILURE); + } } -std::vector< std::pair< void *, size_t >, MyAlloc< std::pair< void *, size_t > > > snapshot_utils::ReturnGlobalSegmentsToSnapshot(){ - std::vector< std::pair< void *, size_t >, MyAlloc< std::pair< void *, size_t > > > theVec; - 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 ); + +/** 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 theVec; - getline( procName, line ); - std::vector< MyString, MyAlloc< MyString > > firstSplit = splitString( line, ' ' ); - if( !checkPermissions( firstSplit[ 1 ] ) ) continue; - 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; - theVec.push_back( std::make_pair( ( void * ) val1, len ) ); - } + 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) || strstr(regionname, MYLIBRARYNAME))) { + size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE; + if (len != 0) + addMemoryRegionToSnapShot(begin, len); + DEBUG("%55s: %18p - %18p\t%c%c%c%c\n", regionname, begin, end, r, w, x, p); + } } - return theVec; + fclose(map); +} +#endif + +SnapshotStack::SnapshotStack() +{ + SnapshotGlobalSegments(); + stack = NULL; +} + +SnapshotStack::~SnapshotStack() +{ +} + + +/** 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 + rollBack(stack->snapshotid); + return stack->index; + } + struct stackEntry *tmp = stack; + stack = stack->next; + model_free(tmp); + } +} + +/** This method takes a snapshot at the given sequence number. */ +void SnapshotStack::snapshotStep(int seqindex) +{ + struct stackEntry *tmp = (struct stackEntry *)model_malloc(sizeof(struct stackEntry)); + tmp->next = stack; + tmp->index = seqindex; + tmp->snapshotid = takeSnapshot(); + stack = tmp; }