src/ASTAnalyses/Order/orderanalysis.cc

   1 #include "orderanalysis.h"
   2 #include "structs.h"
   3 #include "csolver.h"
   4 #include "boolean.h"
   5 #include "ordergraph.h"
   6 #include "order.h"
   7 #include "ordernode.h"
   8 #include "rewriter.h"
   9 #include "mutableset.h"
  10 #include "tunable.h"
  11
  12 void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
  13         SetIteratorOrderNode *iterator = graph->getNodes();
  14         while (iterator->hasNext()) {
  15                 OrderNode *node = iterator->next();
  16                 if (node->status == NOTVISITED) {
  17                         node->status = VISITED;
  18                         DFSNodeVisit(node, finishNodes, false, false, 0);
  19                         node->status = FINISHED;
  20                         finishNodes->push(node);
  21                 }
  22         }
  23         delete iterator;
  24 }
  25
  26 void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
  27         uint size = finishNodes->getSize();
  28         uint sccNum = 1;
  29         for (int i = size - 1; i >= 0; i--) {
  30                 OrderNode *node = finishNodes->get(i);
  31                 if (node->status == NOTVISITED) {
  32                         node->status = VISITED;
  33                         DFSNodeVisit(node, NULL, true, false, sccNum);
  34                         node->sccNum = sccNum;
  35                         node->status = FINISHED;
  36                         sccNum++;
  37                 }
  38         }
  39 }
  40
  41 void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
  42         SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
  43         while (iterator->hasNext()) {
  44                 OrderEdge *edge = iterator->next();
  45                 if (mustvisit) {
  46                         if (!edge->mustPos)
  47                                 continue;
  48                 } else
  49                 if (!edge->polPos && !edge->pseudoPos)  //Ignore edges that do not have positive polarity
  50                         continue;
  51
  52                 OrderNode *child = isReverse ? edge->source : edge->sink;
  53
  54                 if (child->status == NOTVISITED) {
  55                         child->status = VISITED;
  56                         DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
  57                         child->status = FINISHED;
  58                         if (finishNodes != NULL)
  59                                 finishNodes->push(child);
  60                         if (isReverse)
  61                                 child->sccNum = sccNum;
  62                 }
  63         }
  64         delete iterator;
  65 }
  66
  67 void resetNodeInfoStatusSCC(OrderGraph *graph) {
  68         SetIteratorOrderNode *iterator = graph->getNodes();
  69         while (iterator->hasNext()) {
  70                 iterator->next()->status = NOTVISITED;
  71         }
  72         delete iterator;
  73 }
  74
  75 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
  76         Vector<OrderNode *> finishNodes;
  77         DFS(graph, &finishNodes);
  78         resetNodeInfoStatusSCC(graph);
  79         DFSReverse(graph, &finishNodes);
  80         resetNodeInfoStatusSCC(graph);
  81 }
  82
  83 bool isMustBeTrueNode(OrderNode *node) {
  84         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
  85         while (iterator->hasNext()) {
  86                 OrderEdge *edge = iterator->next();
  87                 if (!edge->mustPos) {
  88                         delete iterator;
  89                         return false;
  90                 }
  91         }
  92         delete iterator;
  93         iterator = node->outEdges.iterator();
  94         while (iterator->hasNext()) {
  95                 OrderEdge *edge = iterator->next();
  96                 if (!edge->mustPos) {
  97                         delete iterator;
  98                         return false;
  99                 }
 100         }
 101         delete iterator;
 102         return true;
 103 }
 104
 105 void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
 106         SetIteratorOrderEdge *iterin = node->inEdges.iterator();
 107         while (iterin->hasNext()) {
 108                 OrderEdge *inEdge = iterin->next();
 109                 OrderNode *srcNode = inEdge->source;
 110                 srcNode->outEdges.remove(inEdge);
 111                 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 112                 while (iterout->hasNext()) {
 113                         OrderEdge *outEdge = iterout->next();
 114                         OrderNode *sinkNode = outEdge->sink;
 115                         sinkNode->inEdges.remove(outEdge);
 116                         //Adding new edge to new sink and src nodes ...
 117                         if(srcNode == sinkNode){
 118                                 This->setUnSAT();
 119                                 delete iterout;
 120                                 delete iterin;
 121                                 return;
 122                         }
 123                         OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
 124                         newEdge->mustPos = true;
 125                         newEdge->polPos = true;
 126                         if (newEdge->mustNeg){
 127                                 This->setUnSAT();
 128                         }
 129                         srcNode->outEdges.add(newEdge);
 130                         sinkNode->inEdges.add(newEdge);
 131                 }
 132                 delete iterout;
 133         }
 134         delete iterin;
 135 }
 136
 137 void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
 138         SetIteratorOrderNode *iterator = graph->getNodes();
 139         while (iterator->hasNext()) {
 140                 OrderNode *node = iterator->next();
 141                 if (isMustBeTrueNode(node)) {
 142                         bypassMustBeTrueNode(This, graph, node);
 143                 }
 144         }
 145         delete iterator;
 146 }
 147
 148 /** This function computes a source set for every nodes, the set of
 149     nodes that can reach that node via pospolarity edges.  It then
 150     looks for negative polarity edges from nodes in the the source set
 151     to determine whether we need to generate pseudoPos edges. */
 152
 153 void completePartialOrderGraph(OrderGraph *graph) {
 154         Vector<OrderNode *> finishNodes;
 155         DFS(graph, &finishNodes);
 156         resetNodeInfoStatusSCC(graph);
 157         HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
 158
 159         Vector<OrderNode *> sccNodes;
 160
 161         uint size = finishNodes.getSize();
 162         uint sccNum = 1;
 163         for (int i = size - 1; i >= 0; i--) {
 164                 OrderNode *node = finishNodes.get(i);
 165                 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
 166                 table->put(node, sources);
 167
 168                 if (node->status == NOTVISITED) {
 169                         //Need to do reverse traversal here...
 170                         node->status = VISITED;
 171                         DFSNodeVisit(node, &sccNodes, true, false, sccNum);
 172                         node->status = FINISHED;
 173                         node->sccNum = sccNum;
 174                         sccNum++;
 175                         sccNodes.push(node);
 176
 177                         //Compute in set for entire SCC
 178                         uint rSize = sccNodes.getSize();
 179                         for (uint j = 0; j < rSize; j++) {
 180                                 OrderNode *rnode = sccNodes.get(j);
 181                                 //Compute source sets
 182                                 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
 183                                 while (iterator->hasNext()) {
 184                                         OrderEdge *edge = iterator->next();
 185                                         OrderNode *parent = edge->source;
 186                                         if (edge->polPos) {
 187                                                 sources->add(parent);
 188                                                 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
 189                                                 sources->addAll(parent_srcs);
 190                                         }
 191                                 }
 192                                 delete iterator;
 193                         }
 194                         for (uint j = 0; j < rSize; j++) {
 195                                 //Copy in set of entire SCC
 196                                 OrderNode *rnode = sccNodes.get(j);
 197                                 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
 198                                 table->put(rnode, set);
 199
 200                                 //Use source sets to compute pseudoPos edges
 201                                 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 202                                 while (iterator->hasNext()) {
 203                                         OrderEdge *edge = iterator->next();
 204                                         OrderNode *parent = edge->source;
 205                                         ASSERT(parent != rnode);
 206                                         if (edge->polNeg && parent->sccNum != rnode->sccNum &&
 207                                                         sources->contains(parent)) {
 208                                                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
 209                                                 newedge->pseudoPos = true;
 210                                         }
 211                                 }
 212                                 delete iterator;
 213                         }
 214
 215                         sccNodes.clear();
 216                 }
 217         }
 218
 219         table->resetanddelete();
 220         delete table;
 221         resetNodeInfoStatusSCC(graph);
 222 }
 223
 224 void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
 225         SetIteratorOrderNode *iterator = graph->getNodes();
 226         while (iterator->hasNext()) {
 227                 OrderNode *node = iterator->next();
 228                 if (node->status == NOTVISITED) {
 229                         node->status = VISITED;
 230                         DFSNodeVisit(node, finishNodes, false, true, 0);
 231                         node->status = FINISHED;
 232                         finishNodes->push(node);
 233                 }
 234         }
 235         delete iterator;
 236 }
 237
 238 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
 239         uint size = finishNodes->getSize();
 240         HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
 241
 242         for (int i = size - 1; i >= 0; i--) {
 243                 OrderNode *node = finishNodes->get(i);
 244                 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
 245                 table->put(node, sources);
 246
 247                 {
 248                         //Compute source sets
 249                         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 250                         while (iterator->hasNext()) {
 251                                 OrderEdge *edge = iterator->next();
 252                                 OrderNode *parent = edge->source;
 253                                 if (edge->mustPos) {
 254                                         sources->add(parent);
 255                                         HashsetOrderNode *parent_srcs = (HashsetOrderNode *) table->get(parent);
 256                                         sources->addAll(parent_srcs);
 257                                 }
 258                         }
 259                         delete iterator;
 260                 }
 261                 if (computeTransitiveClosure) {
 262                         //Compute full transitive closure for nodes
 263                         SetIteratorOrderNode *srciterator = sources->iterator();
 264                         while (srciterator->hasNext()) {
 265                                 OrderNode *srcnode = srciterator->next();
 266                                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
 267                                 newedge->mustPos = true;
 268                                 newedge->polPos = true;
 269                                 if (newedge->mustNeg)
 270                                         solver->setUnSAT();
 271                                 srcnode->outEdges.add(newedge);
 272                                 node->inEdges.add(newedge);
 273                         }
 274                         delete srciterator;
 275                 }
 276                 {
 277                         //Use source sets to compute mustPos edges
 278                         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 279                         while (iterator->hasNext()) {
 280                                 OrderEdge *edge = iterator->next();
 281                                 OrderNode *parent = edge->source;
 282                                 if (!edge->mustPos && sources->contains(parent)) {
 283                                         edge->mustPos = true;
 284                                         edge->polPos = true;
 285                                         if (edge->mustNeg)
 286                                                 solver->setUnSAT();
 287                                 }
 288                         }
 289                         delete iterator;
 290                 }
 291                 {
 292                         //Use source sets to compute mustNeg for edges that would introduce cycle if true
 293                         SetIteratorOrderEdge *iterator = node->outEdges.iterator();
 294                         while (iterator->hasNext()) {
 295                                 OrderEdge *edge = iterator->next();
 296                                 OrderNode *child = edge->sink;
 297                                 if (!edge->mustNeg && sources->contains(child)) {
 298                                         edge->mustNeg = true;
 299                                         edge->polNeg = true;
 300                                         if (edge->mustPos)
 301                                                 solver->setUnSAT();
 302                                 }
 303                         }
 304                         delete iterator;
 305                 }
 306         }
 307
 308         table->resetanddelete();
 309         delete table;
 310 }
 311
 312 /* This function finds edges that would form a cycle with must edges
 313    and forces them to be mustNeg.  It also decides whether an edge
 314    must be true because of transitivity from other must be true
 315    edges. */
 316
 317 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
 318         Vector<OrderNode *> finishNodes;
 319         //Topologically sort the mustPos edge graph
 320         DFSMust(graph, &finishNodes);
 321         resetNodeInfoStatusSCC(graph);
 322
 323         //Find any backwards edges that complete cycles and force them to be mustNeg
 324         DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
 325 }
 326
 327 /* This function finds edges that must be positive and forces the
 328    inverse edge to be negative (and clears its positive polarity if it
 329    had one). */
 330
 331 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
 332         SetIteratorOrderEdge *iterator = graph->getEdges();
 333         while (iterator->hasNext()) {
 334                 OrderEdge *edge = iterator->next();
 335                 if (edge->mustPos) {
 336                         OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
 337                         if (invEdge != NULL) {
 338                                 if (!invEdge->mustPos) {
 339                                         invEdge->polPos = false;
 340                                 } else {
 341                                         solver->setUnSAT();
 342                                 }
 343                                 invEdge->mustNeg = true;
 344                                 invEdge->polNeg = true;
 345                         }
 346                 }
 347         }
 348         delete iterator;
 349 }
 350
 351 /** This finds edges that must be positive and forces the inverse edge
 352     to be negative.  It also clears the negative flag of this edge.
 353     It also finds edges that must be negative and clears the positive
 354     polarity. */
 355
 356 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
 357         SetIteratorOrderEdge *iterator = graph->getEdges();
 358         while (iterator->hasNext()) {
 359                 OrderEdge *edge = iterator->next();
 360                 if (edge->mustPos) {
 361                         if (!edge->mustNeg) {
 362                                 edge->polNeg = false;
 363                         } else
 364                                 solver->setUnSAT();
 365
 366                         OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
 367                         if (invEdge != NULL) {
 368                                 if (!invEdge->mustPos)
 369                                         invEdge->polPos = false;
 370                                 else
 371                                         solver->setUnSAT();
 372
 373                                 invEdge->mustNeg = true;
 374                                 invEdge->polNeg = true;
 375                         }
 376                 }
 377                 if (edge->mustNeg && !edge->mustPos) {
 378                         edge->polPos = false;
 379                 }
 380         }
 381         delete iterator;
 382 }