remove STL vector

diff --git a/common.mk b/common.mk
index bc068dff1fb1e559b4aafb9b01881028c28b615a..aca498c7dffc8ab426fea26f84abc3b76e9f3e4f 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 12fc3e17c717cdc04c300bb19d111bb8a3627f7e..5396823334df9a0b47f3077f3c352cc6774e7e1b 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");
 }

diff --git a/model.cc b/model.cc
index 5dd5702ebbc824dfaae6453b2fbe7e51aa3d80ca..78729bd38ac4d9da05d25527450f6668f38be997 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()

diff --git a/mymemory.cc b/mymemory.cc
index 66a4fb973066621e3531b3963f045eafb63977f7..1f8b616020e481e795fd36f74bfa1d2ab56722cc 100644 (file)
--- 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 14b945ab755f1c9f038dd741ca7990a9ade118ea..567ff936e97d32d0d7c62074b01541234a898531 100644 (file)
--- 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 dab1a480d5910d84ed97ec2782e6fa73d7e50a85..a69915ebe41c6e8c7bff79f8362531735c1f2905 100644 (file)
--- 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 300cbd045ad6bc7c6b808d1b83ccc77a47511f26..30a9b8c69872f9122e7494bcf28a5962ab2d4ab1 100644 (file)
--- a/stl-model.h
+++ b/stl-model.h
@@ -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__ */