#include <unistd.h>
#include <sys/types.h>
#include <sstream>
+#include <cstring>
+#include <cassert>
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;
bool checkPermissions( MyString permStr ){
return permStr.find("w") != MyString::npos;
}
-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;
+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 ];
}
if( i >= 3 || dataSect[ i ].second == true ) continue;
dataSect[ i ].second = true;
- if( !procName.good() )return theVec;
+ if( !procName.good() )return;
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 ) );
+ takeSegmentSnapshot( line );
}
}
- return theVec;
}
+
+//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 function definition
+ snapshotTree * snapshotTree::ReturnCurrentScope(){
+ return msCurrentScope;
+ }
+
+ 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 );
+
+ }
+ 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;
+ }
+
+ /*
+ @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;
+
+ }
+};
projects / model-checker.git / blobdiff