X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=snapshot-interface.cc;h=b702e442db887b7562de935aab261805036d4ad1;hb=02792abf9399d1dca2fab7bc511f09e934d05f1d;hp=e350bc473c35fb48aff42ac4a42e912d4867ffb1;hpb=7f626cb1b37a65340c9d82a124aa59797f8083ce;p=model-checker.git

diff --git a/snapshot-interface.cc b/snapshot-interface.cc
index e350bc4..b702e44 100644
--- a/snapshot-interface.cc
+++ b/snapshot-interface.cc
@@ -10,6 +10,8 @@
 #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;
@@ -24,8 +26,20 @@ std::vector< MyString, MyAlloc< MyString> > splitString( MyString input, char de
 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 ];
@@ -49,17 +63,118 @@ std::vector< std::pair< void *, size_t >, MyAlloc< std::pair< void *, size_t > >
 			}
 			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;
+		
+	}
+};