From 644f5fcbc3a95a02db9ace6386f782c9d1e6f94d Mon Sep 17 00:00:00 2001 From: weiyu Date: Wed, 2 Oct 2019 16:23:56 -0700 Subject: [PATCH] Do not unset FuncInst locations when new executions start; check if execution numbers match instead --- funcinst.cc | 4 +++- funcinst.h | 5 ++++- funcnode.cc | 14 +++++++------- 3 files changed, 14 insertions(+), 9 deletions(-) diff --git a/funcinst.cc b/funcinst.cc index 7f031d17..c89284a7 100644 --- a/funcinst.cc +++ b/funcinst.cc @@ -1,7 +1,9 @@ #include "funcinst.h" +#include "model.h" FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) : - single_location(true) + single_location(true), + execution_number(model->get_execution_number()) { ASSERT(act); ASSERT(func_node); diff --git a/funcinst.h b/funcinst.h index 6bbed2c8..ae3aa093 100644 --- a/funcinst.h +++ b/funcinst.h @@ -17,7 +17,6 @@ public: void * get_location() const { return location; } void set_location(void * loc) { location = loc; } - void unset_location() { location = NULL; } action_type get_type() const { return type; } memory_order get_mo() const { return order; } @@ -37,6 +36,9 @@ public: bool is_single_location() { return single_location; } void not_single_location() { single_location = false; } + void set_execution_number(int new_number) { execution_number = new_number; } + int get_execution_number() { return execution_number; } + void print(); MEMALLOC @@ -57,6 +59,7 @@ private: FuncNode * func_node; bool single_location; + int execution_number; /* Currently not in use. May remove this field later * diff --git a/funcnode.cc b/funcnode.cc index e05e84f7..a402ecb4 100644 --- a/funcnode.cc +++ b/funcnode.cc @@ -5,6 +5,8 @@ #include "predicate.h" #include "concretepredicate.h" +#include "model.h" + FuncNode::FuncNode(ModelHistory * history) : history(history), exit_count(0), @@ -31,11 +33,6 @@ FuncNode::FuncNode(ModelHistory * history) : /* Reallocate snapshotted memories when new executions start */ void FuncNode::set_new_exec_flag() { - for (mllnode * it = inst_list.begin(); it != NULL; it = it->getNext()) { - FuncInst * inst = it->getVal(); - inst->unset_location(); - } - action_list_buffer = new SnapList(); read_locations = new loc_set_t(); write_locations = new loc_set_t(); @@ -66,10 +63,13 @@ void FuncNode::add_inst(ModelAction *act) FuncInst * inst = func_inst_map.get(position); ASSERT(inst->get_type() == act->get_type()); + int curr_execution_number = model->get_execution_number(); - // locations are set to NULL when new executions start - if (inst->get_location() == NULL) + /* Reset locations when new executions start */ + if (inst->get_execution_number() != curr_execution_number) { inst->set_location(act->get_location()); + inst->set_execution_number(curr_execution_number); + } if (inst->get_location() != act->get_location()) inst->not_single_location(); -- 2.34.1