-#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 <iostream>
-#include <fstream>
+#include <stdlib.h>
#include <unistd.h>
-#include <sys/types.h>
-#include <sstream>
#include <cstring>
-#include <cassert>
-
-/*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;
- MyStringStream ss( input );
- MyString item;
- while( std::getline( ss, item, delim ) ){
- splits.push_back( item );
- }
- return splits;
-}
+#include <inttypes.h>
+
+#include "snapshot-interface.h"
+#include "snapshot.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");
-bool checkPermissions( MyString permStr ){
- return permStr.find("w") != MyString::npos;
+ if (!map) {
+ perror("popen");
+ exit(EXIT_FAILURE);
+ }
+
+ /* Wait for correct part */
+ while (fgets(buf, sizeof(buf), map)) {
+ if (strstr(buf, "==== regions for process"))
+ break;
+ }
+
+ 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);
}
-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 );
- }
- }
+#else
+
+static void get_binary_name(char *buf, size_t len)
+{
+ if (readlink("/proc/self/exe", buf, len) == -1) {
+ perror("readlink");
+ exit(EXIT_FAILURE);
+ }
}
-void 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 );
- }
- 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 );
- }
- }
+
+/** 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;
+
+ 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);
+ }
+ }
+ fclose(map);
}
+#endif
-//class definition of snapshotStack.....
-//declaration of constructor....
-snapshotStack::snapshotStack(){
- SnapshotGlobalSegments();
- AddUserHeapToSnapshot();
- stack=NULL;
+SnapshotStack::SnapshotStack()
+{
+ SnapshotGlobalSegments();
+ stack = NULL;
}
-
-snapshotStack::~snapshotStack(){
+
+SnapshotStack::~SnapshotStack()
+{
}
-
-int snapshotStack::backTrackBeforeStep(int seqindex) {
- while(true) {
- if (stack->index<=seqindex) {
- //have right entry
- rollBack(stack->snapshotid);
- return stack->index;
- }
- struct stackEntry *tmp=stack;
- free(tmp);
- stack=stack->next;
- }
+
+
+/** 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);
+ }
}
-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;
+/** 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