src/ASTAnalyses/Order/orderanalysis.cc

   1 #include <stdint.h>
   2
   3 #include "orderanalysis.h"
   4 #include "structs.h"
   5 #include "csolver.h"
   6 #include "boolean.h"
   7 #include "ordergraph.h"
   8 #include "order.h"
   9 #include "ordernode.h"
  10 #include "rewriter.h"
  11 #include "mutableset.h"
  12 #include "tunable.h"
  13
  14 void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
  15         SetIteratorOrderNode *iterator = graph->getNodes();
  16         while (iterator->hasNext()) {
  17                 OrderNode *node = iterator->next();
  18                 if (node->status == NOTVISITED) {
  19                         node->status = VISITED;
  20                         DFSNodeVisit(node, finishNodes, false, false, 0);
  21                         node->status = FINISHED;
  22                         finishNodes->push(node);
  23                 }
  24         }
  25         delete iterator;
  26 }
  27
  28 void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
  29         uint size = finishNodes->getSize();
  30         uint sccNum = 1;
  31         for (int i = size - 1; i >= 0; i--) {
  32                 OrderNode *node = finishNodes->get(i);
  33                 if (node->status == NOTVISITED) {
  34                         node->status = VISITED;
  35                         DFSNodeVisit(node, NULL, true, false, sccNum);
  36                         node->sccNum = sccNum;
  37                         node->status = FINISHED;
  38                         sccNum++;
  39                 }
  40         }
  41 }
  42
  43 void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
  44         SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
  45         while (iterator->hasNext()) {
  46                 OrderEdge *edge = iterator->next();
  47                 if (mustvisit) {
  48                         if (!edge->mustPos)
  49                                 continue;
  50                 } else
  51                 if (!edge->polPos && !edge->pseudoPos)  //Ignore edges that do not have positive polarity
  52                         continue;
  53
  54                 OrderNode *child = isReverse ? edge->source : edge->sink;
  55                 if (child->status == NOTVISITED) {
  56                         child->status = VISITED;
  57                         DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
  58                         child->status = FINISHED;
  59                         if (finishNodes != NULL)
  60                                 finishNodes->push(child);
  61                         if (isReverse)
  62                                 child->sccNum = sccNum;
  63                 }
  64         }
  65         delete iterator;
  66 }
  67
  68 void resetNodeInfoStatusSCC(OrderGraph *graph) {
  69         SetIteratorOrderNode *iterator = graph->getNodes();
  70         while (iterator->hasNext()) {
  71                 iterator->next()->status = NOTVISITED;
  72         }
  73         delete iterator;
  74 }
  75
  76 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
  77         Vector<OrderNode *> finishNodes;
  78         DFS(graph, &finishNodes);
  79         resetNodeInfoStatusSCC(graph);
  80         DFSReverse(graph, &finishNodes);
  81         resetNodeInfoStatusSCC(graph);
  82 }
  83
  84 bool isMustBeTrueNode(OrderNode *node) {
  85         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
  86         while (iterator->hasNext()) {
  87                 OrderEdge *edge = iterator->next();
  88                 if (!edge->mustPos) {
  89                         delete iterator;
  90                         return false;
  91                 }
  92         }
  93         delete iterator;
  94         iterator = node->outEdges.iterator();
  95         while (iterator->hasNext()) {
  96                 OrderEdge *edge = iterator->next();
  97                 if (!edge->mustPos) {
  98                         delete iterator;
  99                         return false;
 100                 }
 101         }
 102         delete iterator;
 103         return true;
 104 }
 105
 106 void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
 107         SetIteratorOrderEdge *iterin = node->inEdges.iterator();
 108         while (iterin->hasNext()) {
 109                 OrderEdge *inEdge = iterin->next();
 110                 OrderNode *srcNode = inEdge->source;
 111                 srcNode->outEdges.remove(inEdge);
 112                 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
 113                 while (iterout->hasNext()) {
 114                         OrderEdge *outEdge = iterout->next();
 115                         OrderNode *sinkNode = outEdge->sink;
 116                         sinkNode->inEdges.remove(outEdge);
 117                         //Adding new edge to new sink and src nodes ...
 118                         if (srcNode == sinkNode) {
 119                                 This->setUnSAT();
 120                                 delete iterout;
 121                                 delete iterin;
 122                                 return;
 123                         }
 124                         OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
 125                         newEdge->mustPos = true;
 126                         newEdge->polPos = true;
 127                         if (newEdge->mustNeg)
 128                                 This->setUnSAT();
 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                         }
 305                         delete iterator;
 306                 }
 307         }
 308
 309         table->resetanddelete();
 310         delete table;
 311 }
 312
 313 /* This function finds edges that would form a cycle with must edges
 314    and forces them to be mustNeg.  It also decides whether an edge
 315    must be true because of transitivity from other must be true
 316    edges. */
 317
 318 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
 319         Vector<OrderNode *> finishNodes;
 320         //Topologically sort the mustPos edge graph
 321         DFSMust(graph, &finishNodes);
 322         resetNodeInfoStatusSCC(graph);
 323
 324         //Find any backwards edges that complete cycles and force them to be mustNeg
 325         DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
 326 }
 327
 328 /* This function finds edges that must be positive and forces the
 329    inverse edge to be negative (and clears its positive polarity if it
 330    had one). */
 331
 332 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
 333         SetIteratorOrderEdge *iterator = graph->getEdges();
 334         while (iterator->hasNext()) {
 335                 OrderEdge *edge = iterator->next();
 336                 if (edge->mustPos) {
 337                         OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
 338                         if (invEdge != NULL) {
 339                                 if (!invEdge->mustPos) {
 340                                         invEdge->polPos = false;
 341                                 } else
 342                                         solver->setUnSAT();
 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                                 invEdge->mustNeg = true;
 373                                 invEdge->polNeg = true;
 374                         }
 375                 }
 376                 if (edge->mustNeg && !edge->mustPos) {
 377                         edge->polPos = false;
 378                 }
 379         }
 380         delete iterator;
 381 }