remove STL vector
authorroot <root@dw-6.eecs.uci.edu>
Tue, 30 Jul 2019 18:56:53 +0000 (11:56 -0700)
committerroot <root@dw-6.eecs.uci.edu>
Tue, 30 Jul 2019 18:56:53 +0000 (11:56 -0700)
common.mk
main.cc
model.cc
mymemory.cc
mymemory.h
snapshot.cc
stl-model.h

index bc068df..aca498c 100644 (file)
--- 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 12fc3e1..5396823 100644 (file)
--- 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");
 }
index 5dd5702..78729bd 100644 (file)
--- 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()
index 66a4fb9..1f8b616 100644 (file)
@@ -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)
 {
index 14b945a..567ff93 100644 (file)
@@ -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);
index dab1a48..a69915e 100644 (file)
@@ -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);
index 300cbd0..30a9b8c 100644 (file)
@@ -1,7 +1,6 @@
 #ifndef __STL_MODEL_H__
 #define __STL_MODEL_H__
 
-#include <vector>
 #include <list>
 #include "mymemory.h"
 
@@ -39,38 +38,217 @@ public:
        SNAPSHOTALLOC
 };
 
-template<typename _Tp>
-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<typename _Tp>
-class SnapVector : public std::vector<_Tp, SnapshotAlloc<_Tp> >
-{
+template<typename type>
+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<typename type>
+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__ */