-#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 "snapshot.h"
#include <iostream>
#include <fstream>
#include <unistd.h>
-#include <sys/types.h>
#include <sstream>
#include <cstring>
+#include <string>
#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;
- MyStringStream ss( input );
- MyString item;
- while( std::getline( ss, item, delim ) ){
- splits.push_back( item );
+#include <vector>
+#include <utility>
+#include <inttypes.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 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);
}
- 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)
+ addMemoryRegionToSnapShot(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)
+ addMemoryRegionToSnapShot(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;
-
+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;
+}
projects / c11tester.git / blobdiff