From: root Date: Tue, 30 Jul 2019 18:56:53 +0000 (-0700) Subject: remove STL vector X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=651e9182baf50ef1e235ad7a587730b989bb44c7;hp=c8b9d01f03c5ceae9b3ad503e29f6900564cc242 remove STL vector --- diff --git a/common.mk b/common.mk index bc068dff..aca498c7 100644 --- a/common.mk +++ b/common.mk @@ -8,7 +8,7 @@ UNAME := $(shell uname) LIB_NAME := model LIB_SO := lib$(LIB_NAME).so -CPPFLAGS += -Wall -g -O3 +CPPFLAGS += -Wall -g -O0 # Mac OSX options ifeq ($(UNAME), Darwin) diff --git a/main.cc b/main.cc index 12fc3e17..53968233 100644 --- a/main.cc +++ b/main.cc @@ -199,10 +199,8 @@ int main(int argc, char **argv) parse_options(params, main_argc, main_argv); - snapshot_stack_init(); install_trace_analyses(model->get_execution()); - snapshot_record(0); model->startMainThread(); DEBUG("Exiting\n"); } diff --git a/model.cc b/model.cc index 5dd5702e..78729bd3 100644 --- a/model.cc +++ b/model.cc @@ -353,6 +353,8 @@ static void runChecker() { void ModelChecker::startChecker() { startExecution(get_system_context(), runChecker); + snapshot_stack_init(); + snapshot_record(0); } bool ModelChecker::should_terminate_execution() diff --git a/mymemory.cc b/mymemory.cc index 66a4fb97..1f8b6160 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -71,6 +71,31 @@ void *model_malloc(size_t size) #endif } +/** Non-snapshotting malloc for our use. */ +void *model_realloc(void *ptr, size_t size) +{ +#if USE_MPROTECT_SNAPSHOT + static void *(*reallocp)(void *ptr, size_t size) = NULL; + char *error; + void *newptr; + + /* get address of libc malloc */ + if (!reallocp) { + reallocp = (void * (*)(size_t))dlsym(RTLD_NEXT, "realloc"); + if ((error = dlerror()) != NULL) { + fputs(error, stderr); + exit(EXIT_FAILURE); + } + } + newptr = reallocp(ptr, size); + return newptr; +#else + if (!sStaticSpace) + sStaticSpace = create_shared_mspace(); + return mspace_realloc(sStaticSpace, ptr, size); +#endif +} + /** @brief Snapshotting malloc, for use by model-checker (not user progs) */ void * snapshot_malloc(size_t size) { diff --git a/mymemory.h b/mymemory.h index 14b945ab..567ff936 100644 --- a/mymemory.h +++ b/mymemory.h @@ -50,6 +50,7 @@ void *model_malloc(size_t size); void *model_calloc(size_t count, size_t size); void model_free(void *ptr); +void * model_realloc(void *ptr, size_t size); void * snapshot_malloc(size_t size); void * snapshot_calloc(size_t count, size_t size); diff --git a/snapshot.cc b/snapshot.cc index dab1a480..a69915eb 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -415,8 +415,8 @@ static void fork_loop() { static void fork_startExecution(ucontext_t *context, VoidFuncPtr entryPoint) { /* setup an "exiting" context */ - char stack[128]; - create_context(&exit_ctxt, stack, sizeof(stack), fork_exit); + int exit_stack_size = 256; + create_context(&exit_ctxt, snapshot_calloc(exit_stack_size, 1), exit_stack_size, fork_exit); /* setup the system context */ create_context(context, fork_snap->mStackBase, STACK_SIZE_DEFAULT, entryPoint); diff --git a/stl-model.h b/stl-model.h index 300cbd04..30a9b8c6 100644 --- a/stl-model.h +++ b/stl-model.h @@ -1,7 +1,6 @@ #ifndef __STL_MODEL_H__ #define __STL_MODEL_H__ -#include #include #include "mymemory.h" @@ -39,38 +38,217 @@ public: SNAPSHOTALLOC }; -template -class ModelVector : public std::vector<_Tp, ModelAlloc<_Tp> > -{ -public: - typedef std::vector< _Tp, ModelAlloc<_Tp> > vector; - - ModelVector() : - vector() - { } +#define VECTOR_DEFCAP 8 - ModelVector(size_t n, const _Tp& val = _Tp()) : - vector(n, val) - { } - - MEMALLOC -}; +typedef unsigned int uint; -template -class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> > -{ +template +class ModelVector { public: - typedef std::vector< _Tp, SnapshotAlloc<_Tp> > vector; - - SnapVector() : - vector() - { } + ModelVector(uint _capacity = VECTOR_DEFCAP) : + _size(0), + capacity(_capacity), + array((type *) model_malloc(sizeof(type) * _capacity)) { + } + + ModelVector(uint _capacity, type *_array) : + _size(_capacity), + capacity(_capacity), + array((type *) model_malloc(sizeof(type) * _capacity)) { + memcpy(array, _array, capacity * sizeof(type)); + } + void pop_back() { + _size--; + } + + type back() const { + return array[size - 1]; + } + + void resize(uint psize) { + if (psize <= _size) { + _size = psize; + return; + } else if (psize > capacity) { + array = (type *)model_realloc(array, (psize << 1) * sizeof(type)); + capacity = psize << 1; + } + bzero(&array[_size], (psize - _size) * sizeof(type)); + _size = psize; + } + + void push_back(type item) { + if (_size >= capacity) { + uint newcap = capacity << 1; + array = (type *)model_realloc(array, newcap * sizeof(type)); + capacity = newcap; + } + array[_size++] = item; + } + + type operator[](uint index) const { + return array[index]; + } + + type & operator[](uint index) { + return array[index]; + } + + bool empty() const { + return _size == 0; + } + + type & at(uint index) const { + return array[index]; + } + + void setExpand(uint index, type item) { + if (index >= _size) + resize(index + 1); + set(index, item); + } + + void set(uint index, type item) { + array[index] = item; + } + + void insertAt(uint index, type item) { + resize(_size + 1); + for (uint i = _size - 1;i > index;i--) { + set(i, at(i - 1)); + } + array[index] = item; + } + + void removeAt(uint index) { + for (uint i = index;(i + 1) < _size;i++) { + set(i, at(i + 1)); + } + resize(_size - 1); + } + + inline uint size() const { + return _size; + } + + ~ModelVector() { + model_free(array); + } + + void clear() { + _size = 0; + } + + MEMALLOC; +private: + uint _size; + uint capacity; + type *array; +}; - SnapVector(size_t n, const _Tp& val = _Tp()) : - vector(n, val) - { } - SNAPSHOTALLOC +template +class SnapVector { +public: + SnapVector(uint _capacity = VECTOR_DEFCAP) : + _size(0), + capacity(_capacity), + array((type *) snapshot_malloc(sizeof(type) * _capacity)) { + } + + SnapVector(uint _capacity, type *_array) : + _size(_capacity), + capacity(_capacity), + array((type *) snapshot_malloc(sizeof(type) * _capacity)) { + memcpy(array, _array, capacity * sizeof(type)); + } + void pop_back() { + _size--; + } + + type back() const { + return array[_size - 1]; + } + + void resize(uint psize) { + if (psize <= _size) { + _size = psize; + return; + } else if (psize > capacity) { + array = (type *)snapshot_realloc(array, (psize <<1 )* sizeof(type)); + capacity = psize << 1; + } + bzero(&array[_size], (psize - _size) * sizeof(type)); + _size = psize; + } + + void push_back(type item) { + if (_size >= capacity) { + uint newcap = capacity << 1; + array = (type *)snapshot_realloc(array, newcap * sizeof(type)); + capacity = newcap; + } + array[_size++] = item; + } + + type & operator[](uint index) { + return array[index]; + } + + type operator[](uint index) const { + return array[index]; + } + + bool empty() const { + return _size == 0; + } + + type & at(uint index) const { + return array[index]; + } + + void setExpand(uint index, type item) { + if (index >= _size) + resize(index + 1); + set(index, item); + } + + void set(uint index, type item) { + array[index] = item; + } + + void insertAt(uint index, type item) { + resize(_size + 1); + for (uint i = _size - 1;i > index;i--) { + set(i, at(i - 1)); + } + array[index] = item; + } + + void removeAt(uint index) { + for (uint i = index;(i + 1) < _size;i++) { + set(i, at(i + 1)); + } + resize(_size - 1); + } + + inline uint size() const { + return _size; + } + + ~SnapVector() { + snapshot_free(array); + } + + void clear() { + _size = 0; + } + + SNAPSHOTALLOC; +private: + uint _size; + uint capacity; + type *array; }; #endif /* __STL_MODEL_H__ */