src/ASTAnalyses/Order/ordergraph.cc

   1 #include "ordergraph.h"
   2 #include "ordernode.h"
   3 #include "boolean.h"
   4 #include "orderedge.h"
   5 #include "ordergraph.h"
   6 #include "order.h"
   7
   8 OrderGraph::OrderGraph(Order *_order) :
   9         order(_order) {
  10 }
  11
  12 OrderGraph *buildOrderGraph(Order *order) {
  13         ASSERT(order->graph == NULL);
  14         OrderGraph *orderGraph = new OrderGraph(order);
  15         order->graph = orderGraph;
  16         uint constrSize = order->constraints.getSize();
  17         for (uint j = 0; j < constrSize; j++) {
  18                 orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
  19         }
  20         return orderGraph;
  21 }
  22
  23 //Builds only the subgraph for the must order graph.
  24 OrderGraph *buildMustOrderGraph(Order *order) {
  25         ASSERT(order->graph == NULL);
  26         OrderGraph *orderGraph = new OrderGraph(order);
  27         uint constrSize = order->constraints.getSize();
  28         for (uint j = 0; j < constrSize; j++) {
  29                 orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
  30         }
  31         return orderGraph;
  32 }
  33
  34 void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  35         Polarity polarity = constr->polarity;
  36         BooleanValue mustval = constr->boolVal;
  37         switch (polarity) {
  38         case P_BOTHTRUEFALSE:
  39         case P_TRUE: {
  40                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  41                 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
  42                         _1to2->mustPos = true;
  43                 _1to2->polPos = true;
  44                 node1->addNewOutgoingEdge(_1to2);
  45                 node2->addNewIncomingEdge(_1to2);
  46                 if (constr->polarity == P_TRUE)
  47                         break;
  48         }
  49         case P_FALSE: {
  50                 if (order->type == SATC_TOTAL) {
  51                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
  52                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  53                                 _2to1->mustPos = true;
  54                         _2to1->polPos = true;
  55                         node2->addNewOutgoingEdge(_2to1);
  56                         node1->addNewIncomingEdge(_2to1);
  57                 } else {
  58                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  59                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  60                                 _1to2->mustNeg = true;
  61                         _1to2->polNeg = true;
  62                         node1->addNewOutgoingEdge(_1to2);
  63                         node2->addNewIncomingEdge(_1to2);
  64                 }
  65                 break;
  66         }
  67         case P_UNDEFINED:
  68                 //There is an unreachable order constraint if this assert fires
  69                 //Clients can easily do this, so don't do anything.
  70                 ;
  71         }
  72 }
  73
  74 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  75         BooleanValue mustval = constr->boolVal;
  76         switch (mustval) {
  77         case BV_UNSAT:
  78         case BV_MUSTBETRUE: {
  79                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  80                 _1to2->mustPos = true;
  81                 _1to2->polPos = true;
  82                 node1->addNewOutgoingEdge(_1to2);
  83                 node2->addNewIncomingEdge(_1to2);
  84                 if (constr->boolVal == BV_MUSTBETRUE)
  85                         break;
  86         }
  87         case BV_MUSTBEFALSE: {
  88                 if (order->type == SATC_TOTAL) {
  89                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
  90                         _2to1->mustPos = true;
  91                         _2to1->polPos = true;
  92                         node2->addNewOutgoingEdge(_2to1);
  93                         node1->addNewIncomingEdge(_2to1);
  94                 } else {
  95                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  96                         _1to2->mustNeg = true;
  97                         _1to2->polNeg = true;
  98                         node1->addNewOutgoingEdge(_1to2);
  99                         node2->addNewIncomingEdge(_1to2);
 100                 }
 101                 break;
 102         }
 103         case BV_UNDEFINED:
 104                 //Do Nothing
 105                 break;
 106         }
 107 }
 108
 109 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
 110         OrderNode *node = new OrderNode(id);
 111         OrderNode *tmp = nodes.get(node);
 112         if ( tmp != NULL) {
 113                 delete node;
 114                 node = tmp;
 115         } else {
 116                 nodes.add(node);
 117                 allNodes.push(node);
 118         }
 119         return node;
 120 }
 121
 122 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
 123         OrderNode node(id);
 124         OrderNode *tmp = nodes.get(&node);
 125         return tmp;
 126 }
 127
 128 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 129         OrderEdge *edge = new OrderEdge(begin, end);
 130         OrderEdge *tmp = edges.get(edge);
 131         if ( tmp != NULL ) {
 132                 delete edge;
 133                 edge = tmp;
 134         } else {
 135                 edges.add(edge);
 136         }
 137         return edge;
 138 }
 139
 140 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 141         OrderEdge edge(begin, end);
 142         OrderEdge *tmp = edges.get(&edge);
 143         return tmp;
 144 }
 145
 146 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
 147         OrderEdge inverseedge(edge->sink, edge->source);
 148         OrderEdge *tmp = edges.get(&inverseedge);
 149         return tmp;
 150 }
 151
 152 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 153         OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 154         OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 155         addOrderEdge(from, to, bOrder);
 156 }
 157
 158 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 159         OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 160         OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 161         addMustOrderEdge(from, to, bOrder);
 162 }
 163
 164 OrderGraph::~OrderGraph() {
 165         uint size=allNodes.getSize();
 166         for(uint i=0;i<size;i++)
 167                 delete allNodes.get(i);
 168
 169         SetIteratorOrderEdge *eiterator = edges.iterator();
 170         while (eiterator->hasNext()) {
 171                 OrderEdge *edge = eiterator->next();
 172                 delete edge;
 173         }
 174         delete eiterator;
 175 }
 176
 177 bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
 178         HashsetOrderNode visited;
 179         visited.add(source);
 180         SetIteratorOrderEdge *iterator = source->outEdges.iterator();
 181         bool found = false;
 182         while (iterator->hasNext()) {
 183                 OrderEdge *edge = iterator->next();
 184                 if (edge->polPos) {
 185                         OrderNode *node = edge->sink;
 186                         if (!visited.contains(node)) {
 187                                 if ( node == destination ) {
 188                                         found = true;
 189                                         break;
 190                                 }
 191                                 visited.add(node);
 192                                 found = isTherePathVisit(visited, node, destination);
 193                                 if (found) {
 194                                         break;
 195                                 }
 196                         }
 197                 }
 198         }
 199         delete iterator;
 200         return found;
 201 }
 202
 203 bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination) {
 204         SetIteratorOrderEdge *iterator = current->outEdges.iterator();
 205         bool found = false;
 206         while (iterator->hasNext()) {
 207                 OrderEdge *edge = iterator->next();
 208                 if (edge->polPos) {
 209                         OrderNode *node = edge->sink;
 210                         if (node == destination) {
 211                                 found = true;
 212                                 break;
 213                         }
 214                         visited.add(node);
 215                         if (isTherePathVisit(visited, node, destination)) {
 216                                 found = true;
 217                                 break;
 218                         }
 219                 }
 220         }
 221         delete iterator;
 222         return found;
 223 }
 224
 225 void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
 226         SetIteratorOrderNode *iterator = getNodes();
 227         while (iterator->hasNext()) {
 228                 OrderNode *node = iterator->next();
 229                 if (node->status == NOTVISITED) {
 230                         node->status = VISITED;
 231                         DFSNodeVisit(node, finishNodes, false, false, 0);
 232                         node->status = FINISHED;
 233                         finishNodes->push(node);
 234                 }
 235         }
 236         delete iterator;
 237 }
 238
 239 void OrderGraph::DFSMust(Vector<OrderNode *> *finishNodes) {
 240         SetIteratorOrderNode *iterator = getNodes();
 241         while (iterator->hasNext()) {
 242                 OrderNode *node = iterator->next();
 243                 if (node->status == NOTVISITED) {
 244                         node->status = VISITED;
 245                         DFSNodeVisit(node, finishNodes, false, true, 0);
 246                         node->status = FINISHED;
 247                         finishNodes->push(node);
 248                 }
 249         }
 250         delete iterator;
 251 }
 252
 253 void OrderGraph::DFSReverse(Vector<OrderNode *> *finishNodes) {
 254         uint size = finishNodes->getSize();
 255         uint sccNum = 1;
 256         for (int i = size - 1; i >= 0; i--) {
 257                 OrderNode *node = finishNodes->get(i);
 258                 if (node->status == NOTVISITED) {
 259                         node->status = VISITED;
 260                         DFSNodeVisit(node, NULL, true, false, sccNum);
 261                         node->sccNum = sccNum;
 262                         node->status = FINISHED;
 263                         sccNum++;
 264                 }
 265         }
 266 }
 267
 268 void OrderGraph::DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
 269         SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
 270         while (iterator->hasNext()) {
 271                 OrderEdge *edge = iterator->next();
 272                 if (mustvisit) {
 273                         if (!edge->mustPos)
 274                                 continue;
 275                 } else
 276                 if (!edge->polPos && !edge->pseudoPos)          //Ignore edges that do not have positive polarity
 277                         continue;
 278
 279                 OrderNode *child = isReverse ? edge->source : edge->sink;
 280                 if (child->status == NOTVISITED) {
 281                         child->status = VISITED;
 282                         DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
 283                         child->status = FINISHED;
 284                         if (finishNodes != NULL) {
 285                                 finishNodes->push(child);
 286                         }
 287                         if (isReverse)
 288                                 child->sccNum = sccNum;
 289                 }
 290         }
 291         delete iterator;
 292 }
 293
 294 void OrderGraph::resetNodeInfoStatusSCC() {
 295         SetIteratorOrderNode *iterator = getNodes();
 296         while (iterator->hasNext()) {
 297                 iterator->next()->status = NOTVISITED;
 298         }
 299         delete iterator;
 300 }
 301
 302 void OrderGraph::computeStronglyConnectedComponentGraph() {
 303         Vector<OrderNode *> finishNodes;
 304         DFS(&finishNodes);
 305         resetNodeInfoStatusSCC();
 306         DFSReverse(&finishNodes);
 307         resetNodeInfoStatusSCC();
 308 }
 309
 310 /** This function computes a source set for every nodes, the set of
 311     nodes that can reach that node via pospolarity edges.  It then
 312     looks for negative polarity edges from nodes in the the source set
 313     to determine whether we need to generate pseudoPos edges. */
 314
 315 void OrderGraph::completePartialOrderGraph() {
 316         Vector<OrderNode *> finishNodes;
 317         DFS(&finishNodes);
 318         resetNodeInfoStatusSCC();
 319         HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
 320
 321         Vector<OrderNode *> sccNodes;
 322
 323         uint size = finishNodes.getSize();
 324         uint sccNum = 1;
 325         for (int i = size - 1; i >= 0; i--) {
 326                 OrderNode *node = finishNodes.get(i);
 327                 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
 328                 table->put(node, sources);
 329
 330                 if (node->status == NOTVISITED) {
 331                         //Need to do reverse traversal here...
 332                         node->status = VISITED;
 333                         DFSNodeVisit(node, &sccNodes, true, false, sccNum);
 334                         node->status = FINISHED;
 335                         node->sccNum = sccNum;
 336                         sccNum++;
 337                         sccNodes.push(node);
 338
 339                         //Compute in set for entire SCC
 340                         uint rSize = sccNodes.getSize();
 341                         for (uint j = 0; j < rSize; j++) {
 342                                 OrderNode *rnode = sccNodes.get(j);
 343                                 //Compute source sets
 344                                 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
 345                                 while (iterator->hasNext()) {
 346                                         OrderEdge *edge = iterator->next();
 347                                         OrderNode *parent = edge->source;
 348                                         if (edge->polPos) {
 349                                                 sources->add(parent);
 350                                                 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
 351                                                 sources->addAll(parent_srcs);
 352                                         }
 353                                 }
 354                                 delete iterator;
 355                         }
 356                         for (uint j = 0; j < rSize; j++) {
 357                                 //Copy in set of entire SCC
 358                                 OrderNode *rnode = sccNodes.get(j);
 359                                 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
 360                                 table->put(rnode, set);
 361
 362                                 //Use source sets to compute pseudoPos edges
 363                                 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 364                                 while (iterator->hasNext()) {
 365                                         OrderEdge *edge = iterator->next();
 366                                         OrderNode *parent = edge->source;
 367                                         ASSERT(parent != rnode);
 368                                         if (edge->polNeg && parent->sccNum != rnode->sccNum &&
 369                                                         sources->contains(parent)) {
 370                                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(rnode, parent);
 371                                                 newedge->pseudoPos = true;
 372                                         }
 373                                 }
 374                                 delete iterator;
 375                         }
 376
 377                         sccNodes.clear();
 378                 }
 379         }
 380
 381         table->resetAndDeleteVals();
 382         delete table;
 383         resetNodeInfoStatusSCC();
 384 }