X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=snapshot-interface.cc;h=57ac52ee25ba541da665b1440c5ab0e7a7bead35;hp=b702e442db887b7562de935aab261805036d4ad1;hb=1857316e6637ac144952a274ff020629abe83807;hpb=02792abf9399d1dca2fab7bc511f09e934d05f1d diff --git a/snapshot-interface.cc b/snapshot-interface.cc index b702e44..57ac52e 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -1,180 +1,168 @@ -#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 -#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 ); +#include +#include + +#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 MYBINARYNAME "model" +#define MYLIBRARYNAME "libmodel.so" +#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 +}; + +class SnapshotStack { + public: + int backTrackBeforeStep(int seq_index); + void snapshotStep(int seq_index); + + MEMALLOC + private: + std::vector > stack; +}; + +static SnapshotStack *snap_stack; + +#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 ); - } - } -} -void snapshot_utils::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 ); + /* Wait for correct part */ + while (fgets(buf, sizeof(buf), map)) { + if (strstr(buf, "==== regions for process")) + break; } - 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 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) + snapshot_add_memory_region(begin, len); + } } + pclose(map); } +#else -//class definition of snapshotTree..... -//static definitions -namespace snapshot_utils{ - snapshotTree * snapshotTree::msCurrentScope = 0; - BackTrackingParents_t snapshotTree::msRecordedParents; - SnapshotToStateMap_t snapshotTree::msSnapshottedStates; - SnapshotEdgeMap_t snapshotTree::msSnapshotEdgesMap; - unsigned int snapshotTree::msTimeCounter = 0; - void snapshotTree::EnsureRelevantRegionsSnapshotted(){ - SnapshotGlobalSegments(); - AddUserHeapToSnapshot(); - } - //declaration of constructor.... - snapshotTree::snapshotTree(){ - EnsureRelevantRegionsSnapshotted(); - } - - snapshotTree::~snapshotTree(){ - if( this == msCurrentScope ){ - msCurrentScope = 0; - } +static void get_binary_name(char *buf, size_t len) +{ + if (readlink("/proc/self/exe", buf, len) == -1) { + perror("readlink"); + exit(EXIT_FAILURE); } - - //static function definition - snapshotTree * snapshotTree::ReturnCurrentScope(){ - return msCurrentScope; +} + +/** 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); } + 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; - MyString SerializeThreadSteps( const ThreadStepMap_t & theMap ){ - MyString newStr; - char tempArray[ 2048 ] = { 0 }; - char * ptr = tempArray; - for( ThreadStepMap_t::const_iterator myIter = theMap.begin(); myIter != theMap.end(); ++myIter ){ - sprintf( ptr, "%d:%d#", myIter->first, myIter->second ); - newStr += ptr; - ptr += strlen( ptr ); - + 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) + snapshot_add_memory_region(begin, len); + DEBUG("%55s: %18p - %18p\t%c%c%c%c\n", regionname, begin, end, r, w, x, p); } - return newStr; - } - //public function definiton - /* - @funct: TakeStep( thrd_t current, thrd_t whoseNext ) - @return: bool - @Desc: this function takes a series of steps creating - new tree elements and setting the current scope. This function returns true if the step just taken leads to the parent of - an unexplored back tracking point... - */ - void snapshotTree::AddThreadStep( ThreadStepMap_t & theMap, thrd_t which ){ - if( theMap.find( which ) != theMap.end() ){ - ++theMap[ which ]; - return; - } - theMap[ which ] = 1; //implicit thread creation.... - } - bool snapshotTree::operator<( const snapshotTree & rhs ) const{ - return this->mTimeStamp < rhs.mTimeStamp; - } - bool snapshotTreeComp::operator()( const std::pair< const snapshotTree*, snapshot_id > & lhs, const std::pair< const snapshotTree*, snapshot_id > & rhs ){ - return *(lhs.first) < *(rhs.first); - } - std::pair< MyString, bool > snapshotTree::TakeStep( thrd_t which, thrd_t whoseNext ){ - assert( msCurrentScope == this ); - std::pair< MyString, bool > retVal; - ThreadStepMap_t temp = mThreadStepsTaken; - AddThreadStep( temp, which ); - MyString serialized = SerializeThreadSteps( mThreadStepsTaken ); //is it necessary to cache this with the class....? - retVal.first = serialized; - if( msSnapshotEdgesMap.find( serialized ) != msSnapshotEdgesMap.end() ){ - msCurrentScope = msSnapshotEdgesMap[ serialized ]; - } - snapshotTree * newNode = new snapshotTree(); - newNode->mThreadStepsTaken = temp; - newNode->mpParent = this; - this->mChildren.push_back( newNode ); - newNode->mNextStepTaker = whoseNext; //dont know if this will be used yet.... - newNode->mTimeStamp = msTimeCounter++; - msCurrentScope = newNode; - - //is it an actual backtracking parent.... - retVal.second = msRecordedParents.find( msCurrentScope ) != msRecordedParents.end(); - return retVal; } + fclose(map); +} +#endif - /* - @funct: BacktrackingPointSet() - @Return: NONE - @DESC: This sets up the internal states necessary in future should we take a snapshot or something... - */ - void snapshotTree::BacktrackingPointSet(){ - assert( msCurrentScope == this ); - msRecordedParents.insert( msCurrentScope->mpParent ); - } - - /* - @funct: ReturnEarliestSnapshotID( MyString key ) - @DESC: For any key, return the snapshot id which is the latest but earlier than the transition defined by the current key.... - */ - snapshot_id snapshotTree::ReturnEarliestSnapshotID( MyString key ){ - //first return a snapshotTree * - if( msSnapshotEdgesMap.find( key ) == msSnapshotEdgesMap.end() )return -1; - //snapshotTree * theNode = msSnapshotEdgesMap[ key ]; - - //do we have a greatest snapshot id that is lesser than the current id... - return -1; - - } -}; +/** 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; +} + +/** This method takes a snapshot at the given sequence number. */ +void SnapshotStack::snapshotStep(int seqindex) +{ + stack.push_back(snapshot_entry(take_snapshot(), seqindex)); +} + +void snapshot_stack_init() +{ + snap_stack = new SnapshotStack(); + SnapshotGlobalSegments(); +} + +void snapshot_record(int seq_index) +{ + snap_stack->snapshotStep(seq_index); +} + +int snapshot_backtrack_before(int seq_index) +{ + return snap_stack->backTrackBeforeStep(seq_index); +}