X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=snapshot-interface.cc;h=57ac52ee25ba541da665b1440c5ab0e7a7bead35;hb=76bf58915289cb923cc95e237b64151bf799167c;hp=c33b8d44549aa29de3d1dbdbb71bbf5f7628d8fd;hpb=260b391c9292c9eb48da1033bf4ac1c32ea49f87;p=c11tester.git diff --git a/snapshot-interface.cc b/snapshot-interface.cc index c33b8d44..57ac52ee 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -2,6 +2,7 @@ #include #include #include +#include #include "snapshot-interface.h" #include "snapshot.h" @@ -14,25 +15,24 @@ #define MYLIBRARYNAME "libmodel.so" #define MAPFILE "/proc/self/maps" -struct stackEntry { - struct stackEntry *next; +struct snapshot_entry { + snapshot_entry(snapshot_id id, int idx) : snapshotid(id), index(idx) { } snapshot_id snapshotid; int index; + MEMALLOC }; class SnapshotStack { public: - SnapshotStack(); - ~SnapshotStack(); int backTrackBeforeStep(int seq_index); void snapshotStep(int seq_index); MEMALLOC private: - struct stackEntry *stack; + std::vector > stack; }; -static SnapshotStack *snapshotObject; +static SnapshotStack *snap_stack; #ifdef MAC /** The SnapshotGlobalSegments function computes the memory regions @@ -125,16 +125,6 @@ static void SnapshotGlobalSegments() } #endif -SnapshotStack::SnapshotStack() -{ - SnapshotGlobalSegments(); - stack = NULL; -} - -SnapshotStack::~SnapshotStack() -{ -} - /** This method returns to the last snapshot before the inputted * sequence number. This function must be called from the model * checking thread and not from a snapshotted stack. @@ -143,40 +133,36 @@ SnapshotStack::~SnapshotStack() */ int SnapshotStack::backTrackBeforeStep(int seqindex) { - while (true) { - if (stack->index <= seqindex) { - //have right entry - snapshot_roll_back(stack->snapshotid); - return stack->index; - } - struct stackEntry *tmp = stack; - stack = stack->next; - model_free(tmp); - } + int i; + for (i = (int)stack.size() - 1; i >= 0; i++) + if (stack[i].index <= seqindex) + break; + else + stack.pop_back(); + + ASSERT(i >= 0); + snapshot_roll_back(stack[i].snapshotid); + return stack[i].index; } /** This method takes a snapshot at the given sequence number. */ void SnapshotStack::snapshotStep(int seqindex) { - struct stackEntry *tmp = (struct stackEntry *)model_malloc(sizeof(struct stackEntry)); - tmp->next = stack; - tmp->index = seqindex; - tmp->snapshotid = take_snapshot(); - stack = tmp; + stack.push_back(snapshot_entry(take_snapshot(), seqindex)); } - void snapshot_stack_init() { - snapshotObject = new SnapshotStack(); + snap_stack = new SnapshotStack(); + SnapshotGlobalSegments(); } void snapshot_record(int seq_index) { - snapshotObject->snapshotStep(seq_index); + snap_stack->snapshotStep(seq_index); } int snapshot_backtrack_before(int seq_index) { - return snapshotObject->backTrackBeforeStep(seq_index); + return snap_stack->backTrackBeforeStep(seq_index); }