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