X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=mymemory.cc;h=44985fa3aebc0d3fc32f97c0606b3c7ef11154a8;hp=54885ca12deb46a50eba387a66edc58fba52b5ea;hb=76e48f210747b7ef23387ffd7c33ea0009c1d922;hpb=5f85e1b11c1578a4b6fb64c18285d1d627d732df diff --git a/mymemory.cc b/mymemory.cc index 54885ca1..44985fa3 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -1,13 +1,17 @@ -#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" + #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 @@ -15,15 +19,16 @@ static mspace sStaticSpace = NULL; #endif /** Non-snapshotting calloc for our use. */ -void *model_calloc(size_t count, size_t size) { +void *model_calloc(size_t count, size_t size) +{ #if USE_MPROTECT_SNAPSHOT - static void *(*callocp)(size_t count, size_t size)=NULL; + static void *(*callocp)(size_t count, size_t size) = NULL; char *error; void *ptr; /* get address of libc malloc */ if (!callocp) { - callocp = ( void * ( * )( size_t, size_t ) )dlsym(RTLD_NEXT, "calloc"); + callocp = (void * (*)(size_t, size_t))dlsym(RTLD_NEXT, "calloc"); if ((error = dlerror()) != NULL) { fputs(error, stderr); exit(EXIT_FAILURE); @@ -32,25 +37,23 @@ void *model_calloc(size_t count, size_t size) { ptr = callocp(count, size); return ptr; #else - if( !snapshotrecord) { - createSharedMemory(); - } - if( NULL == sStaticSpace ) - sStaticSpace = create_mspace_with_base( ( void * )( snapshotrecord->mSharedMemoryBase ), SHARED_MEMORY_DEFAULT -sizeof( struct SnapShot ), 1 ); - return mspace_calloc( sStaticSpace, count, size ); + if (!sStaticSpace) + sStaticSpace = create_shared_mspace(); + return mspace_calloc(sStaticSpace, count, size); #endif } /** Non-snapshotting malloc for our use. */ -void *model_malloc(size_t size) { +void *model_malloc(size_t size) +{ #if USE_MPROTECT_SNAPSHOT - static void *(*mallocp)(size_t size)=NULL; + static void *(*mallocp)(size_t size) = NULL; char *error; void *ptr; /* get address of libc malloc */ if (!mallocp) { - mallocp = ( void * ( * )( size_t ) )dlsym(RTLD_NEXT, "malloc"); + mallocp = (void * (*)(size_t))dlsym(RTLD_NEXT, "malloc"); if ((error = dlerror()) != NULL) { fputs(error, stderr); exit(EXIT_FAILURE); @@ -59,74 +62,52 @@ void *model_malloc(size_t size) { ptr = mallocp(size); return ptr; #else - if( !snapshotrecord) { - createSharedMemory(); - } - if( NULL == sStaticSpace ) - sStaticSpace = create_mspace_with_base( ( void * )( snapshotrecord->mSharedMemoryBase ), SHARED_MEMORY_DEFAULT -sizeof( struct SnapShot ), 1 ); - return mspace_malloc( sStaticSpace, size ); + if (!sStaticSpace) + sStaticSpace = create_shared_mspace(); + return mspace_malloc(sStaticSpace, size); #endif } /** @brief Snapshotting malloc, for use by model-checker (not user progs) */ void * snapshot_malloc(size_t size) { - return malloc(size); + void *tmp = mspace_malloc(model_snapshot_space, size); + ASSERT(tmp); + return tmp; } /** @brief Snapshotting calloc, for use by model-checker (not user progs) */ void * snapshot_calloc(size_t count, size_t size) { - return calloc(count, size); + void *tmp = mspace_calloc(model_snapshot_space, count, size); + ASSERT(tmp); + return tmp; } -/** @brief Snapshotting free, for use by model-checker (not user progs) */ -void snapshot_free(void *ptr) +/** @brief Snapshotting realloc, for use by model-checker (not user progs) */ +void *snapshot_realloc(void *ptr, size_t size) { - free(ptr); -} - -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; + void *tmp = mspace_realloc(model_snapshot_space, ptr, size); + ASSERT(tmp); + return tmp; } -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); +/** @brief Snapshotting free, for use by model-checker (not user progs) */ +void snapshot_free(void *ptr) +{ + mspace_free(model_snapshot_space, ptr); } /** Non-snapshotting free for our use. */ -void model_free(void *ptr) { +void model_free(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"); + freep = (void (*)(void *))dlsym(RTLD_NEXT, "free"); if ((error = dlerror()) != NULL) { fputs(error, stderr); exit(EXIT_FAILURE); @@ -134,78 +115,82 @@ void model_free(void *ptr) { } freep(ptr); #else - mspace_free( sStaticSpace, ptr ); + mspace_free(sStaticSpace, ptr); #endif } - -/** @brief Global mspace reference for the snapshotting heap */ -mspace mySpace = NULL; - -/** Bootstrap allocation. Problem is that the dynamic linker calls - * require calloc to work and calloc requires the dynamic linker to - * work. */ +/** Bootstrap allocation. Problem is that the dynamic linker calls require + * calloc to work and calloc requires the dynamic linker to work. */ #define BOOTSTRAPBYTES 4096 char bootstrapmemory[BOOTSTRAPBYTES]; -size_t offset=0; +size_t offset = 0; -void * HandleEarlyAllocationRequest( size_t sz ){ - /*Align to 8 byte boundary*/ - sz=(sz+7)&~7; +void * HandleEarlyAllocationRequest(size_t sz) +{ + /* Align to 8 byte boundary */ + sz = (sz + 7) & ~7; if (sz > (BOOTSTRAPBYTES-offset)) { - printf("OUT OF BOOTSTRAP MEMORY\n"); + model_print("OUT OF BOOTSTRAP MEMORY\n"); exit(EXIT_FAILURE); } - void * pointer= (void *) & bootstrapmemory[offset]; - offset+=sz; + void *pointer = (void *)&bootstrapmemory[offset]; + offset += sz; return pointer; } -/** Check whether this is bootstrapped memory that we should not - free. */ +/** @brief Global mspace reference for the model-checker's snapshotting heap */ +mspace model_snapshot_space = NULL; + +#if USE_MPROTECT_SNAPSHOT -bool DontFree( void * ptr ){ - return (ptr>=(&bootstrapmemory[0])&&ptr<(&bootstrapmemory[BOOTSTRAPBYTES])); +/** @brief Global mspace reference for the user's snapshotting heap */ +mspace user_snapshot_space = NULL; + +/** Check whether this is bootstrapped memory that we should not free */ +static bool DontFree(void *ptr) +{ + return (ptr >= (&bootstrapmemory[0]) && ptr < (&bootstrapmemory[BOOTSTRAPBYTES])); } /** @brief Snapshotting malloc implementation for user programs */ -void *malloc( size_t size ) +void *malloc(size_t size) { - if (mySpace) { - void *tmp=mspace_malloc( mySpace, size ); + if (user_snapshot_space) { + void *tmp = mspace_malloc(user_snapshot_space, size); ASSERT(tmp); return tmp; } else - return HandleEarlyAllocationRequest( size ); + return HandleEarlyAllocationRequest(size); } /** @brief Snapshotting free implementation for user programs */ -void free( void * ptr ){ +void free(void * ptr) +{ if (!DontFree(ptr)) - mspace_free(mySpace, ptr); + mspace_free(user_snapshot_space, ptr); } /** @brief Snapshotting realloc implementation for user programs */ -void *realloc( void *ptr, size_t size ) +void *realloc(void *ptr, size_t size) { - void *tmp = mspace_realloc(mySpace, ptr, size); + void *tmp = mspace_realloc(user_snapshot_space, ptr, size); ASSERT(tmp); return tmp; } /** @brief Snapshotting calloc implementation for user programs */ -void * calloc( size_t num, size_t size ) +void * calloc(size_t num, size_t size) { - if (mySpace) { - void *tmp = mspace_calloc(mySpace, num, size); + if (user_snapshot_space) { + void *tmp = mspace_calloc(user_snapshot_space, num, size); ASSERT(tmp); return tmp; } else { - void *tmp=HandleEarlyAllocationRequest( size * num ); - std::memset( tmp, 0, size * num ); + void *tmp = HandleEarlyAllocationRequest(size * num); + memset(tmp, 0, size * num); return tmp; } } @@ -233,3 +218,4 @@ void operator delete[](void *p, size_t size) { free(p); } +#endif /* USE_MPROTECT_SNAPSHOT */