+/* -*- Mode: C; indent-tabs-mode: t -*- */
+
#define MYBINARYNAME "model"
#define MYLIBRARYNAME "libmodel.so"
#define MYALLOCNAME "libmymemory.so"
#include <sstream>
#include <cstring>
#include <cassert>
+
+snapshotStack * snapshotObject;
+
+/*This looks like it might leak memory... Subramanian should fix this. */
+
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;
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;
+ 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 );
- }
- }
+ if( 0 != len ){
+ addMemoryRegionToSnapShot( ( void * )val1, len );
+ }
+ }
}
-void snapshot_utils::SnapshotGlobalSegments(){
+void SnapshotGlobalSegments(){
MyString fn = PROCNAME;
static char sProcessSize[ 12 ] = { 0 };
std::pair< const char *, bool > dataSect[ 3 ];
}
}
-//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();
- }
+//class definition of snapshotStack.....
+//declaration of constructor....
+snapshotStack::snapshotStack(){
+ SnapshotGlobalSegments();
+ stack=NULL;
+}
- snapshotTree::~snapshotTree(){
- if( this == msCurrentScope ){
- msCurrentScope = 0;
- }
- }
+snapshotStack::~snapshotStack(){
+}
- //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 );
-
+int snapshotStack::backTrackBeforeStep(int seqindex) {
+ while(true) {
+ if (stack->index<=seqindex) {
+ //have right entry
+ rollBack(stack->snapshotid);
+ return stack->index;
}
- 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....
+ struct stackEntry *tmp=stack;
+ free(tmp);
+ stack=stack->next;
}
- 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;
-
- }
-};
+void snapshotStack::snapshotStep(int seqindex) {
+ struct stackEntry *tmp=(struct stackEntry *)malloc(sizeof(struct stackEntry));
+ tmp->next=stack;
+ tmp->index=seqindex;
+ tmp->snapshotid=takeSnapshot();
+ stack=tmp;
+}
projects / model-checker.git / blobdiff