From b5000a06086de6ea8799168d463f018cab785830 Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Mon, 8 Oct 2012 13:26:07 -0700 Subject: [PATCH 1/1] mymemory: add basic model_snapshot_space I will begin to utilize the 'model_snapshot_space' as the model-checker's private snapshotting heap. --- mymemory.cc | 3 +++ mymemory.h | 2 ++ snapshot.cc | 24 +++++++++++++++++------- 3 files changed, 22 insertions(+), 7 deletions(-) diff --git a/mymemory.cc b/mymemory.cc index f296048..387d6de 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -132,6 +132,9 @@ void * HandleEarlyAllocationRequest(size_t sz) return pointer; } +/** @brief Global mspace reference for the model-checker's snapshotting heap */ +mspace model_snapshot_space = NULL; + #if USE_MPROTECT_SNAPSHOT /** @brief Global mspace reference for the user's snapshotting heap diff --git a/mymemory.h b/mymemory.h index 0788e69..b224206 100644 --- a/mymemory.h +++ b/mymemory.h @@ -156,6 +156,8 @@ extern mspace create_mspace(size_t capacity, int locked); extern mspace user_snapshot_space; #endif +extern mspace model_snapshot_space; + #ifdef __cplusplus }; /* end of extern "C" */ #endif diff --git a/snapshot.cc b/snapshot.cc index 59aad72..e006189 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -30,6 +30,13 @@ /* extern declaration definition */ struct SnapShot * snapshotrecord = NULL; +/** PageAlignedAdressUpdate return a page aligned address for the + * address being added as a side effect the numBytes are also changed. + */ +static void * PageAlignAddressUpward(void * addr) { + return (void *)((((uintptr_t)addr)+PAGESIZE-1)&~(PAGESIZE-1)); +} + #if !USE_MPROTECT_SNAPSHOT /** @statics * These variables are necessary because the stack is shared region and @@ -48,13 +55,6 @@ static snapshot_id snapshotid = 0; #else /* USE_MPROTECT_SNAPSHOT */ -/** PageAlignedAdressUpdate return a page aligned address for the - * address being added as a side effect the numBytes are also changed. - */ -static void * PageAlignAddressUpward(void * addr) { - return (void *)((((uintptr_t)addr)+PAGESIZE-1)&~(PAGESIZE-1)); -} - /** ReturnPageAlignedAddress returns a page aligned address for the * address being added as a side effect the numBytes are also changed. */ @@ -174,6 +174,12 @@ void initSnapshotLibrary(unsigned int numbackingpages, void * pagealignedbase=PageAlignAddressUpward(basemySpace); user_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1); addMemoryRegionToSnapShot(pagealignedbase, numheappages); + + void *base_model_snapshot_space = model_malloc((numheappages + 1) * PAGESIZE); + pagealignedbase = PageAlignAddressUpward(base_model_snapshot_space); + model_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1); + addMemoryRegionToSnapShot(pagealignedbase, numheappages); + entryPoint(); } #else @@ -183,6 +189,10 @@ void initSnapshotLibrary(unsigned int numbackingpages, if (!snapshotrecord) createSharedMemory(); + void *base_model_snapshot_space = malloc((numheappages + 1) * PAGESIZE); + void *pagealignedbase = PageAlignAddressUpward(base_model_snapshot_space); + model_snapshot_space = create_mspace_with_base(pagealignedbase, numheappages * PAGESIZE, 1); + //step 2 setup the stack context. ucontext_t newContext; getcontext( &newContext ); -- 2.34.1