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