nodestack.cc

   1 #define __STDC_FORMAT_MACROS
   2 #include <inttypes.h>
   3 #include <cstdlib>
   4
   5 #include <string.h>
   6
   7 #include "nodestack.h"
   8 #include "action.h"
   9 #include "common.h"
  10 #include "threads-model.h"
  11 #include "modeltypes.h"
  12 #include "execution.h"
  13 #include "params.h"
  14
  15 /**
  16  * @brief Node constructor
  17  *
  18  * Constructs a single Node for use in a NodeStack. Each Node is associated
  19  * with exactly one ModelAction (exception: the first Node should be created
  20  * as an empty stub, to represent the first thread "choice") and up to one
  21  * parent.
  22  *
  23  * @param params The model-checker parameters
  24  * @param act The ModelAction to associate with this Node. May be NULL.
  25  * @param par The parent Node in the NodeStack. May be NULL if there is no
  26  * parent.
  27  * @param nthreads The number of threads which exist at this point in the
  28  * execution trace.
  29  */
  30 Node::Node(const struct model_params *params, ModelAction *act, Node *par,
  31                 int nthreads) :
  32         action(act),
  33         params(params),
  34         uninit_action(NULL),
  35         parent(par),
  36         num_threads(nthreads)
  37 {
  38         ASSERT(act);
  39         act->set_node(this);
  40 }
  41
  42 /** @brief Node desctructor */
  43 Node::~Node()
  44 {
  45         delete action;
  46         if (uninit_action)
  47                 delete uninit_action;
  48 }
  49
  50 /** Prints debugging info for the ModelAction associated with this Node */
  51 void Node::print() const
  52 {
  53         action->print();
  54 }
  55
  56 NodeStack::NodeStack() :
  57         node_list(),
  58         head_idx(-1),
  59         total_nodes(0)
  60 {
  61         total_nodes++;
  62 }
  63
  64 NodeStack::~NodeStack()
  65 {
  66         for (unsigned int i = 0; i < node_list.size(); i++)
  67                 delete node_list[i];
  68 }
  69
  70 /**
  71  * @brief Register the model-checker object with this NodeStack
  72  * @param exec The execution structure for the ModelChecker
  73  */
  74 void NodeStack::register_engine(const ModelExecution *exec)
  75 {
  76         this->execution = exec;
  77 }
  78
  79 const struct model_params * NodeStack::get_params() const
  80 {
  81         return execution->get_params();
  82 }
  83
  84 void NodeStack::print() const
  85 {
  86         model_print("............................................\n");
  87         model_print("NodeStack printing node_list:\n");
  88         for (unsigned int it = 0; it < node_list.size(); it++) {
  89                 if ((int)it == this->head_idx)
  90                         model_print("vvv following action is the current iterator vvv\n");
  91                 node_list[it]->print();
  92         }
  93         model_print("............................................\n");
  94 }
  95
  96 /** Note: The is_enabled set contains what actions were enabled when
  97  *  act was chosen. */
  98 ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_enabled)
  99 {
 100         DBG();
 101
 102         /* Record action */
 103         Node *head = get_head();
 104
 105         int next_threads = execution->get_num_threads();
 106         if (act->get_type() == THREAD_CREATE || act->get_type() == PTHREAD_CREATE ) // may need to be changed
 107                 next_threads++;
 108         node_list.push_back(new Node(get_params(), act, head, next_threads));
 109         total_nodes++;
 110         head_idx++;
 111         return NULL;
 112 }
 113
 114
 115 /** Reset the node stack. */
 116 void NodeStack::full_reset()
 117 {
 118         for (unsigned int i = 0; i < node_list.size(); i++)
 119                 delete node_list[i];
 120         node_list.clear();
 121         reset_execution();
 122         total_nodes = 1;
 123 }
 124
 125 Node * NodeStack::get_head() const
 126 {
 127         if (node_list.empty() || head_idx < 0)
 128                 return NULL;
 129         return node_list[head_idx];
 130 }
 131
 132 Node * NodeStack::get_next() const
 133 {
 134         if (node_list.empty()) {
 135                 DEBUG("Empty\n");
 136                 return NULL;
 137         }
 138         unsigned int it = head_idx + 1;
 139         if (it == node_list.size()) {
 140                 DEBUG("At end\n");
 141                 return NULL;
 142         }
 143         return node_list[it];
 144 }
 145
 146 void NodeStack::reset_execution()
 147 {
 148         head_idx = -1;
 149 }