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::addEdge(uint64_t first, uint64_t second) {
  75         OrderNode *node1 = getOrderNodeFromOrderGraph(first);
  76         OrderNode *node2 = getOrderNodeFromOrderGraph(second);
  77         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  78         _1to2->polPos = true;
  79         _1to2->mustPos = true;
  80         node1->addNewOutgoingEdge(_1to2);
  81         node2->addNewIncomingEdge(_1to2);
  82 }
  83
  84 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  85         BooleanValue mustval = constr->boolVal;
  86         switch (mustval) {
  87         case BV_UNSAT:
  88         case BV_MUSTBETRUE: {
  89                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  90                 _1to2->mustPos = true;
  91                 _1to2->polPos = true;
  92                 node1->addNewOutgoingEdge(_1to2);
  93                 node2->addNewIncomingEdge(_1to2);
  94                 if (constr->boolVal == BV_MUSTBETRUE)
  95                         break;
  96         }
  97         case BV_MUSTBEFALSE: {
  98                 if (order->type == SATC_TOTAL) {
  99                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
 100                         _2to1->mustPos = true;
 101                         _2to1->polPos = true;
 102                         node2->addNewOutgoingEdge(_2to1);
 103                         node1->addNewIncomingEdge(_2to1);
 104                 } else {
 105                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
 106                         _1to2->mustNeg = true;
 107                         _1to2->polNeg = true;
 108                         node1->addNewOutgoingEdge(_1to2);
 109                         node2->addNewIncomingEdge(_1to2);
 110                 }
 111                 break;
 112         }
 113         case BV_UNDEFINED:
 114                 //Do Nothing
 115                 break;
 116         }
 117 }
 118
 119 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
 120         OrderNode *node = new OrderNode(id);
 121         OrderNode *tmp = nodes.get(node);
 122         if ( tmp != NULL) {
 123                 delete node;
 124                 node = tmp;
 125         } else {
 126                 nodes.add(node);
 127                 allNodes.push(node);
 128         }
 129         return node;
 130 }
 131
 132 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
 133         OrderNode node(id);
 134         OrderNode *tmp = 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         uint size=allNodes.getSize();
 176         for(uint i=0;i<size;i++)
 177                 delete allNodes.get(i);
 178
 179         SetIteratorOrderEdge *eiterator = edges.iterator();
 180         while (eiterator->hasNext()) {
 181                 OrderEdge *edge = eiterator->next();
 182                 delete edge;
 183         }
 184         delete eiterator;
 185 }
 186
 187 bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
 188         HashsetOrderNode visited;
 189         visited.add(source);
 190         SetIteratorOrderEdge *iterator = source->outEdges.iterator();
 191         bool found = false;
 192         while (iterator->hasNext()) {
 193                 OrderEdge *edge = iterator->next();
 194                 if (edge->polPos) {
 195                         OrderNode *node = edge->sink;
 196                         if (!visited.contains(node)) {
 197                                 if ( node == destination ) {
 198                                         found = true;
 199                                         break;
 200                                 }
 201                                 visited.add(node);
 202                                 found = isTherePathVisit(visited, node, destination);
 203                                 if (found) {
 204                                         break;
 205                                 }
 206                         }
 207                 }
 208         }
 209         delete iterator;
 210         return found;
 211 }
 212
 213 bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination) {
 214         SetIteratorOrderEdge *iterator = current->outEdges.iterator();
 215         bool found = false;
 216         while (iterator->hasNext()) {
 217                 OrderEdge *edge = iterator->next();
 218                 if (edge->polPos) {
 219                         OrderNode *node = edge->sink;
 220                         if (node == destination) {
 221                                 found = true;
 222                                 break;
 223                         }
 224                         visited.add(node);
 225                         if (isTherePathVisit(visited, node, destination)) {
 226                                 found = true;
 227                                 break;
 228                         }
 229                 }
 230         }
 231         delete iterator;
 232         return found;
 233 }
 234
 235 void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
 236         SetIteratorOrderNode *iterator = getNodes();
 237         while (iterator->hasNext()) {
 238                 OrderNode *node = iterator->next();
 239                 if (node->status == NOTVISITED) {
 240                         node->status = VISITED;
 241                         DFSNodeVisit(node, finishNodes, false, false, 0);
 242                         node->status = FINISHED;
 243                         finishNodes->push(node);
 244                 }
 245         }
 246         delete iterator;
 247 }
 248
 249 void OrderGraph::DFSMust(Vector<OrderNode *> *finishNodes) {
 250         SetIteratorOrderNode *iterator = getNodes();
 251         while (iterator->hasNext()) {
 252                 OrderNode *node = iterator->next();
 253                 if (node->status == NOTVISITED) {
 254                         node->status = VISITED;
 255                         DFSNodeVisit(node, finishNodes, false, true, 0);
 256                         node->status = FINISHED;
 257                         finishNodes->push(node);
 258                 }
 259         }
 260         delete iterator;
 261 }
 262
 263 void OrderGraph::DFSReverse(Vector<OrderNode *> *finishNodes) {
 264         uint size = finishNodes->getSize();
 265         uint sccNum = 1;
 266         for (int i = size - 1; i >= 0; i--) {
 267                 OrderNode *node = finishNodes->get(i);
 268                 if (node->status == NOTVISITED) {
 269                         node->status = VISITED;
 270                         DFSNodeVisit(node, NULL, true, false, sccNum);
 271                         node->sccNum = sccNum;
 272                         node->status = FINISHED;
 273                         sccNum++;
 274                 }
 275         }
 276 }
 277
 278 void OrderGraph::DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
 279         SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
 280         while (iterator->hasNext()) {
 281                 OrderEdge *edge = iterator->next();
 282                 if (mustvisit) {
 283                         if (!edge->mustPos)
 284                                 continue;
 285                 } else
 286                 if (!edge->polPos && !edge->pseudoPos)          //Ignore edges that do not have positive polarity
 287                         continue;
 288
 289                 OrderNode *child = isReverse ? edge->source : edge->sink;
 290                 if (child->status == NOTVISITED) {
 291                         child->status = VISITED;
 292                         DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
 293                         child->status = FINISHED;
 294                         if (finishNodes != NULL) {
 295                                 finishNodes->push(child);
 296                         }
 297                         if (isReverse)
 298                                 child->sccNum = sccNum;
 299                 }
 300         }
 301         delete iterator;
 302 }
 303
 304 void OrderGraph::resetNodeInfoStatusSCC() {
 305         SetIteratorOrderNode *iterator = getNodes();
 306         while (iterator->hasNext()) {
 307                 iterator->next()->status = NOTVISITED;
 308         }
 309         delete iterator;
 310 }
 311
 312 void OrderGraph::computeStronglyConnectedComponentGraph() {
 313         Vector<OrderNode *> finishNodes;
 314         DFS(&finishNodes);
 315         resetNodeInfoStatusSCC();
 316         DFSReverse(&finishNodes);
 317         resetNodeInfoStatusSCC();
 318 }
 319
 320 /** This function computes a source set for every nodes, the set of
 321     nodes that can reach that node via pospolarity edges.  It then
 322     looks for negative polarity edges from nodes in the the source set
 323     to determine whether we need to generate pseudoPos edges. */
 324
 325 void OrderGraph::completePartialOrderGraph() {
 326         Vector<OrderNode *> finishNodes;
 327         DFS(&finishNodes);
 328         resetNodeInfoStatusSCC();
 329         HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
 330
 331         Vector<OrderNode *> sccNodes;
 332
 333         uint size = finishNodes.getSize();
 334         uint sccNum = 1;
 335         for (int i = size - 1; i >= 0; i--) {
 336                 OrderNode *node = finishNodes.get(i);
 337                 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
 338                 table->put(node, sources);
 339
 340                 if (node->status == NOTVISITED) {
 341                         //Need to do reverse traversal here...
 342                         node->status = VISITED;
 343                         DFSNodeVisit(node, &sccNodes, true, false, sccNum);
 344                         node->status = FINISHED;
 345                         node->sccNum = sccNum;
 346                         sccNum++;
 347                         sccNodes.push(node);
 348
 349                         //Compute in set for entire SCC
 350                         uint rSize = sccNodes.getSize();
 351                         for (uint j = 0; j < rSize; j++) {
 352                                 OrderNode *rnode = sccNodes.get(j);
 353                                 //Compute source sets
 354                                 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
 355                                 while (iterator->hasNext()) {
 356                                         OrderEdge *edge = iterator->next();
 357                                         OrderNode *parent = edge->source;
 358                                         if (edge->polPos) {
 359                                                 sources->add(parent);
 360                                                 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
 361                                                 sources->addAll(parent_srcs);
 362                                         }
 363                                 }
 364                                 delete iterator;
 365                         }
 366                         for (uint j = 0; j < rSize; j++) {
 367                                 //Copy in set of entire SCC
 368                                 OrderNode *rnode = sccNodes.get(j);
 369                                 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
 370                                 table->put(rnode, set);
 371
 372                                 //Use source sets to compute pseudoPos edges
 373                                 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 374                                 while (iterator->hasNext()) {
 375                                         OrderEdge *edge = iterator->next();
 376                                         OrderNode *parent = edge->source;
 377                                         ASSERT(parent != rnode);
 378                                         if (edge->polNeg && parent->sccNum != rnode->sccNum &&
 379                                                         sources->contains(parent)) {
 380                                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(rnode, parent);
 381                                                 newedge->pseudoPos = true;
 382                                         }
 383                                 }
 384                                 delete iterator;
 385                         }
 386
 387                         sccNodes.clear();
 388                 }
 389         }
 390
 391         table->resetAndDeleteVals();
 392         delete table;
 393         resetNodeInfoStatusSCC();
 394 }