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         uint constrSize = order->constraints.getSize();
  16         for (uint j = 0; j < constrSize; j++) {
  17                 orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
  18         }
  19         return orderGraph;
  20 }
  21
  22 //Builds only the subgraph for the must order graph.
  23 OrderGraph *buildMustOrderGraph(Order *order) {
  24         ASSERT(order->graph == NULL);
  25         OrderGraph *orderGraph = new OrderGraph(order);
  26         uint constrSize = order->constraints.getSize();
  27         for (uint j = 0; j < constrSize; j++) {
  28                 orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
  29         }
  30         return orderGraph;
  31 }
  32
  33 void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  34         Polarity polarity = constr->polarity;
  35         BooleanValue mustval = constr->boolVal;
  36         switch (polarity) {
  37         case P_BOTHTRUEFALSE:
  38         case P_TRUE: {
  39                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  40                 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
  41                         _1to2->mustPos = true;
  42                 _1to2->polPos = true;
  43                 node1->addNewOutgoingEdge(_1to2);
  44                 node2->addNewIncomingEdge(_1to2);
  45                 if (constr->polarity == P_TRUE)
  46                         break;
  47         }
  48         case P_FALSE: {
  49                 if (order->type == SATC_TOTAL) {
  50                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
  51                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  52                                 _2to1->mustPos = true;
  53                         _2to1->polPos = true;
  54                         node2->addNewOutgoingEdge(_2to1);
  55                         node1->addNewIncomingEdge(_2to1);
  56                 } else {
  57                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  58                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  59                                 _1to2->mustNeg = true;
  60                         _1to2->polNeg = true;
  61                         node1->addNewOutgoingEdge(_1to2);
  62                         node2->addNewIncomingEdge(_1to2);
  63                 }
  64                 break;
  65         }
  66         case P_UNDEFINED:
  67                 //There is an unreachable order constraint if this assert fires
  68                 //Clients can easily do this, so don't do anything.
  69                 ;
  70         }
  71 }
  72
  73 void OrderGraph::addEdge(uint64_t first, uint64_t second) {
  74         OrderNode *node1 = getOrderNodeFromOrderGraph(first);
  75         OrderNode *node2 = getOrderNodeFromOrderGraph(second);
  76         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  77         _1to2->polPos = true;
  78         _1to2->mustPos = true;
  79         node1->addNewOutgoingEdge(_1to2);
  80         node2->addNewIncomingEdge(_1to2);
  81 }
  82
  83 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  84         BooleanValue mustval = constr->boolVal;
  85         switch (mustval) {
  86         case BV_UNSAT:
  87         case BV_MUSTBETRUE: {
  88                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  89                 _1to2->mustPos = true;
  90                 _1to2->polPos = true;
  91                 node1->addNewOutgoingEdge(_1to2);
  92                 node2->addNewIncomingEdge(_1to2);
  93                 if (constr->boolVal == BV_MUSTBETRUE)
  94                         break;
  95         }
  96         case BV_MUSTBEFALSE: {
  97                 if (order->type == SATC_TOTAL) {
  98                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
  99                         _2to1->mustPos = true;
 100                         _2to1->polPos = true;
 101                         node2->addNewOutgoingEdge(_2to1);
 102                         node1->addNewIncomingEdge(_2to1);
 103                 } else {
 104                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
 105                         _1to2->mustNeg = true;
 106                         _1to2->polNeg = true;
 107                         node1->addNewOutgoingEdge(_1to2);
 108                         node2->addNewIncomingEdge(_1to2);
 109                 }
 110                 break;
 111         }
 112         case BV_UNDEFINED:
 113                 //Do Nothing
 114                 break;
 115         }
 116 }
 117
 118 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
 119         OrderNode *node = new OrderNode(id);
 120         OrderNode *tmp = (OrderNode*)nodes.get(node);
 121         if ( tmp != NULL) {
 122                 delete node;
 123                 node = tmp;
 124         } else {
 125                 nodes.add(node);
 126         }
 127         return node;
 128 }
 129
 130 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
 131         OrderNodeKey node(id);
 132         OrderNode *tmp = (OrderNode*)nodes.get(&node);
 133         return tmp;
 134 }
 135
 136 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 137         OrderEdge *edge = new OrderEdge(begin, end);
 138         OrderEdge *tmp = edges.get(edge);
 139         if ( tmp != NULL ) {
 140                 delete edge;
 141                 edge = tmp;
 142         } else {
 143                 edges.add(edge);
 144         }
 145         return edge;
 146 }
 147
 148 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 149         OrderEdge edge(begin, end);
 150         OrderEdge *tmp = edges.get(&edge);
 151         return tmp;
 152 }
 153
 154 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
 155         OrderEdge inverseedge(edge->sink, edge->source);
 156         OrderEdge *tmp = edges.get(&inverseedge);
 157         return tmp;
 158 }
 159
 160 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 161         OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 162         OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 163         addOrderEdge(from, to, bOrder);
 164 }
 165
 166 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 167         OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 168         OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 169         addMustOrderEdge(from, to, bOrder);
 170 }
 171
 172 OrderGraph::~OrderGraph() {
 173         nodes.resetAndDelete();
 174         edges.resetAndDelete();
 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 = (OrderNode*)iterator->next();
 229                 if (node->status == NOTVISITED && !node->removed) {
 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 = (OrderNode*)iterator->next();
 243                 if (node->status == NOTVISITED && !node->removed) {
 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                 ((OrderNode*)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 }