X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=mymemory.cc;h=efc36e98c8be4b607bb0927936beed7e6769712f;hp=88018e269093c531a67bde16d27de8a95d6d6305;hb=251ac4b4bf3a9f2d3cfacc1e6618200ca1c431ac;hpb=339c89039e14e4f2433d4af0b0d2ae6e6c41e028 diff --git a/mymemory.cc b/mymemory.cc index 88018e26..efc36e98 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -1,186 +1,118 @@ -#include "mymemory.h" -#include "snapshot.h" -#include "snapshotimp.h" + +#include #include #include #include -#include +#include +#include + +#include "mymemory.h" +#include "snapshot.h" +#include "common.h" +#include "threads-model.h" +#include "model.h" +#include "datarace.h" + #define REQUESTS_BEFORE_ALLOC 1024 -size_t allocatedReqs[ REQUESTS_BEFORE_ALLOC ] = { 0 }; + +size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 }; int nextRequest = 0; int howManyFreed = 0; -#if !USE_MPROTECT_SNAPSHOT static mspace sStaticSpace = NULL; -#endif - -/** Non-snapshotting malloc for our use. */ -void *MYMALLOC(size_t size) { -#if USE_MPROTECT_SNAPSHOT - static void *(*mallocp)(size_t size); - char *error; - void *ptr; - - /* get address of libc malloc */ - if (!mallocp) { - mallocp = ( void * ( * )( size_t ) )dlsym(RTLD_NEXT, "malloc"); - if ((error = dlerror()) != NULL) { - fputs(error, stderr); - exit(EXIT_FAILURE); - } - } - ptr = mallocp(size); - return ptr; -#else - if( !sTheRecord ){ - createSharedLibrary(); - } - if( NULL == sStaticSpace ) - sStaticSpace = create_mspace_with_base( ( void * )( sTheRecord->mSharedMemoryBase ), SHARED_MEMORY_DEFAULT -sizeof( struct Snapshot ), 1 ); - return mspace_malloc( sStaticSpace, size ); -#endif +/** Non-snapshotting calloc for our use. */ +void *model_calloc(size_t count, size_t size) +{ + if (!sStaticSpace) + sStaticSpace = create_shared_mspace(); + return mspace_calloc(sStaticSpace, count, size); } -void *system_malloc( size_t size ){ - static void *(*mallocp)(size_t size); - char *error; - void *ptr; - - /* get address of libc malloc */ - if (!mallocp) { - mallocp = ( void * ( * )( size_t ) )dlsym(RTLD_NEXT, "malloc"); - if ((error = dlerror()) != NULL) { - fputs(error, stderr); - exit(EXIT_FAILURE); - } - } - ptr = mallocp(size); - return ptr; +/** Non-snapshotting malloc for our use. */ +void *model_malloc(size_t size) +{ + if (!sStaticSpace) + sStaticSpace = create_shared_mspace(); + return mspace_malloc(sStaticSpace, size); } -void system_free( void * ptr ){ - static void (*freep)(void *); - char *error; - - /* get address of libc free */ - if (!freep) { - freep = ( void ( * )( void * ) )dlsym(RTLD_NEXT, "free"); - if ((error = dlerror()) != NULL) { - fputs(error, stderr); - exit(EXIT_FAILURE); - } - } - freep(ptr); +/** Non-snapshotting malloc for our use. */ +void *model_realloc(void *ptr, size_t size) +{ + if (!sStaticSpace) + sStaticSpace = create_shared_mspace(); + return mspace_realloc(sStaticSpace, ptr, size); } -/** Non-snapshotting free for our use. */ -void MYFREE(void *ptr) { -#if USE_MPROTECT_SNAPSHOT - static void (*freep)(void *); - char *error; - - /* get address of libc free */ - if (!freep) { - freep = ( void ( * )( void * ) )dlsym(RTLD_NEXT, "free"); - if ((error = dlerror()) != NULL) { - fputs(error, stderr); - exit(EXIT_FAILURE); - } - } - freep(ptr); -#else - mspace_free( sStaticSpace, ptr ); -#endif +/** @brief Snapshotting malloc, for use by model-checker (not user progs) */ +void * snapshot_malloc(size_t size) +{ + void *tmp = mspace_malloc(model_snapshot_space, size); + ASSERT(tmp); + return tmp; } - -/** This global references the mspace for the snapshotting heap */ -mspace mySpace = NULL; - -/** This global references the unaligned memory address that was malloced for the snapshotting heap */ -void * basemySpace = NULL; - -/** Adding the fix for not able to allocate through a reimplemented calloc at the beginning before instantiating our allocator -A bit circumspect about adding an sbrk. linux docs say to avoid using it... */ - -void * HandleEarlyAllocationRequest( size_t sz ){ - if( 0 == mySpace ){ - void * returnAddress = sbrk( sz ); - if( nextRequest >= REQUESTS_BEFORE_ALLOC ){ - exit( EXIT_FAILURE ); - } - allocatedReqs[ nextRequest++ ] = ( size_t )returnAddress; - return returnAddress; - } - return NULL; +/** @brief Snapshotting calloc, for use by model-checker (not user progs) */ +void * snapshot_calloc(size_t count, size_t size) +{ + void *tmp = mspace_calloc(model_snapshot_space, count, size); + ASSERT(tmp); + return tmp; } -/** The fact that I am not expecting more than a handful requests is implicit in my not using a binary search here*/ - -bool DontFree( void * ptr ){ - if( howManyFreed == nextRequest ) return false; //a minor optimization to reduce the number of instructions executed on each free call.... - if( NULL == ptr ) return true; - for( int i = nextRequest - 1; i >= 0; --i ){ - if( allocatedReqs[ i ] == ( size_t )ptr ) { - ++howManyFreed; - return true; - } - } - return false; +/** @brief Snapshotting realloc, for use by model-checker (not user progs) */ +void *snapshot_realloc(void *ptr, size_t size) +{ + void *tmp = mspace_realloc(model_snapshot_space, ptr, size); + ASSERT(tmp); + return tmp; } -/** Snapshotting malloc implementation for user programs. */ - -void *malloc( size_t size ) { - void * earlyReq = HandleEarlyAllocationRequest( size ); - if( earlyReq ) return earlyReq; - return mspace_malloc( mySpace, size ); +/** @brief Snapshotting free, for use by model-checker (not user progs) */ +void snapshot_free(void *ptr) +{ + mspace_free(model_snapshot_space, ptr); } -/** Snapshotting free implementation for user programs. */ - -void free( void * ptr ){ - if( DontFree( ptr ) ) return; - mspace_free( mySpace, ptr ); +/** Non-snapshotting free for our use. */ +void model_free(void *ptr) +{ + mspace_free(sStaticSpace, ptr); } -/** Snapshotting realloc implementation for user programs. */ +/** Bootstrap allocation. Problem is that the dynamic linker calls require + * calloc to work and calloc requires the dynamic linker to work. */ -void *realloc( void *ptr, size_t size ){ - return mspace_realloc( mySpace, ptr, size ); -} +#define BOOTSTRAPBYTES 131072 +char bootstrapmemory[BOOTSTRAPBYTES]; +size_t offset = 0; -/** Snapshotting calloc implementation for user programs. */ +void * HandleEarlyAllocationRequest(size_t sz) +{ + /* Align to 8 byte boundary */ + sz = (sz + 7) & ~7; -void * calloc( size_t num, size_t size ){ - void * earlyReq = HandleEarlyAllocationRequest( size * num ); - if( earlyReq ) { - std::memset( earlyReq, 0, size * num ); - return earlyReq; + if (sz > (BOOTSTRAPBYTES-offset)) { + model_print("OUT OF BOOTSTRAP MEMORY. Increase the size of BOOTSTRAPBYTES in mymemory.cc\n"); + exit(EXIT_FAILURE); } - return mspace_calloc( mySpace, num, size ); -} - -/** Snapshotting new operator for user programs. */ -void * operator new(size_t size) throw(std::bad_alloc) { - return malloc(size); + void *pointer = (void *)&bootstrapmemory[offset]; + offset += sz; + return pointer; } -/** Snapshotting delete operator for user programs. */ +/** @brief Global mspace reference for the model-checker's snapshotting heap */ +mspace model_snapshot_space = NULL; -void operator delete(void *p) throw() { - free(p); +/** @brief Snapshotting allocation function for use by the Thread class only */ +void * Thread_malloc(size_t size) +{ + return snapshot_malloc(size); } -/** Snapshotting new[] operator for user programs. */ - -void * operator new[](size_t size) throw(std::bad_alloc) { - return malloc(size); -} - -/** Snapshotting delete[] operator for user programs. */ - -void operator delete[](void *p, size_t size) { - free(p); +/** @brief Snapshotting free function for use by the Thread class only */ +void Thread_free(void *ptr) +{ + snapshot_free(ptr); }