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                         }
  62                         if (isReverse)
  63                                 child->sccNum = sccNum;
  64                 }
  65         }
  66         delete iterator;
  67 }
  68
  69 void resetNodeInfoStatusSCC(OrderGraph *graph) {
  70         SetIteratorOrderNode *iterator = graph->getNodes();
  71         while (iterator->hasNext()) {
  72                 iterator->next()->status = NOTVISITED;
  73         }
  74         delete iterator;
  75 }
  76
  77 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
  78         Vector<OrderNode *> finishNodes;
  79         DFS(graph, &finishNodes);
  80         resetNodeInfoStatusSCC(graph);
  81         DFSReverse(graph, &finishNodes);
  82         resetNodeInfoStatusSCC(graph);
  83 }
  84
  85
  86
  87 /** This function computes a source set for every nodes, the set of
  88     nodes that can reach that node via pospolarity edges.  It then
  89     looks for negative polarity edges from nodes in the the source set
  90     to determine whether we need to generate pseudoPos edges. */
  91
  92 void completePartialOrderGraph(OrderGraph *graph) {
  93         Vector<OrderNode *> finishNodes;
  94         DFS(graph, &finishNodes);
  95         resetNodeInfoStatusSCC(graph);
  96         HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
  97
  98         Vector<OrderNode *> sccNodes;
  99
 100         uint size = finishNodes.getSize();
 101         uint sccNum = 1;
 102         for (int i = size - 1; i >= 0; i--) {
 103                 OrderNode *node = finishNodes.get(i);
 104                 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
 105                 table->put(node, sources);
 106
 107                 if (node->status == NOTVISITED) {
 108                         //Need to do reverse traversal here...
 109                         node->status = VISITED;
 110                         DFSNodeVisit(node, &sccNodes, true, false, sccNum);
 111                         node->status = FINISHED;
 112                         node->sccNum = sccNum;
 113                         sccNum++;
 114                         sccNodes.push(node);
 115
 116                         //Compute in set for entire SCC
 117                         uint rSize = sccNodes.getSize();
 118                         for (uint j = 0; j < rSize; j++) {
 119                                 OrderNode *rnode = sccNodes.get(j);
 120                                 //Compute source sets
 121                                 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
 122                                 while (iterator->hasNext()) {
 123                                         OrderEdge *edge = iterator->next();
 124                                         OrderNode *parent = edge->source;
 125                                         if (edge->polPos) {
 126                                                 sources->add(parent);
 127                                                 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
 128                                                 sources->addAll(parent_srcs);
 129                                         }
 130                                 }
 131                                 delete iterator;
 132                         }
 133                         for (uint j = 0; j < rSize; j++) {
 134                                 //Copy in set of entire SCC
 135                                 OrderNode *rnode = sccNodes.get(j);
 136                                 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
 137                                 table->put(rnode, set);
 138
 139                                 //Use source sets to compute pseudoPos edges
 140                                 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 141                                 while (iterator->hasNext()) {
 142                                         OrderEdge *edge = iterator->next();
 143                                         OrderNode *parent = edge->source;
 144                                         ASSERT(parent != rnode);
 145                                         if (edge->polNeg && parent->sccNum != rnode->sccNum &&
 146                                                         sources->contains(parent)) {
 147                                                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
 148                                                 newedge->pseudoPos = true;
 149                                         }
 150                                 }
 151                                 delete iterator;
 152                         }
 153
 154                         sccNodes.clear();
 155                 }
 156         }
 157
 158         table->resetanddelete();
 159         delete table;
 160         resetNodeInfoStatusSCC(graph);
 161 }
 162
 163 void DFSMust(OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
 164         SetIteratorOrderNode *iterator = graph->getNodes();
 165         while (iterator->hasNext()) {
 166                 OrderNode *node = iterator->next();
 167                 if (node->status == NOTVISITED) {
 168                         node->status = VISITED;
 169                         DFSNodeVisit(node, finishNodes, false, true, 0);
 170                         node->status = FINISHED;
 171                         finishNodes->push(node);
 172                 }
 173         }
 174         delete iterator;
 175 }
 176
 177 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
 178         uint size = finishNodes->getSize();
 179         HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
 180
 181         for (int i = size - 1; i >= 0; i--) {
 182                 OrderNode *node = finishNodes->get(i);
 183                 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
 184                 table->put(node, sources);
 185
 186                 {
 187                         //Compute source sets
 188                         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 189                         while (iterator->hasNext()) {
 190                                 OrderEdge *edge = iterator->next();
 191                                 OrderNode *parent = edge->source;
 192                                 if (edge->mustPos) {
 193                                         sources->add(parent);
 194                                         HashsetOrderNode *parent_srcs = (HashsetOrderNode *) table->get(parent);
 195                                         sources->addAll(parent_srcs);
 196                                 }
 197                         }
 198                         delete iterator;
 199                 }
 200                 if (computeTransitiveClosure) {
 201                         //Compute full transitive closure for nodes
 202                         SetIteratorOrderNode *srciterator = sources->iterator();
 203                         while (srciterator->hasNext()) {
 204                                 OrderNode *srcnode = srciterator->next();
 205                                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
 206                                 newedge->mustPos = true;
 207                                 newedge->polPos = true;
 208                                 if (newedge->mustNeg)
 209                                         solver->setUnSAT();
 210                                 srcnode->outEdges.add(newedge);
 211                                 node->inEdges.add(newedge);
 212                         }
 213                         delete srciterator;
 214                 }
 215                 {
 216                         //Use source sets to compute mustPos edges
 217                         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
 218                         while (iterator->hasNext()) {
 219                                 OrderEdge *edge = iterator->next();
 220                                 OrderNode *parent = edge->source;
 221                                 if (!edge->mustPos && sources->contains(parent)) {
 222                                         edge->mustPos = true;
 223                                         edge->polPos = true;
 224                                         if (edge->mustNeg)
 225                                                 solver->setUnSAT();
 226                                 }
 227                         }
 228                         delete iterator;
 229                 }
 230                 {
 231                         //Use source sets to compute mustNeg for edges that would introduce cycle if true
 232                         SetIteratorOrderEdge *iterator = node->outEdges.iterator();
 233                         while (iterator->hasNext()) {
 234                                 OrderEdge *edge = iterator->next();
 235                                 OrderNode *child = edge->sink;
 236                                 if (!edge->mustNeg && sources->contains(child)) {
 237                                         edge->mustNeg = true;
 238                                         edge->polNeg = true;
 239                                         if (edge->mustPos) {
 240                                                 solver->setUnSAT();
 241                                         }
 242                                 }
 243                         }
 244                         delete iterator;
 245                 }
 246         }
 247
 248         table->resetanddelete();
 249         delete table;
 250 }
 251
 252 /* This function finds edges that would form a cycle with must edges
 253    and forces them to be mustNeg.  It also decides whether an edge
 254    must be true because of transitivity from other must be true
 255    edges. */
 256
 257 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
 258         Vector<OrderNode *> finishNodes;
 259         //Topologically sort the mustPos edge graph
 260         DFSMust(graph, &finishNodes);
 261         resetNodeInfoStatusSCC(graph);
 262
 263         //Find any backwards edges that complete cycles and force them to be mustNeg
 264         DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
 265 }
 266
 267 /* This function finds edges that must be positive and forces the
 268    inverse edge to be negative (and clears its positive polarity if it
 269    had one). */
 270
 271 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
 272         SetIteratorOrderEdge *iterator = graph->getEdges();
 273         while (iterator->hasNext()) {
 274                 OrderEdge *edge = iterator->next();
 275                 if (edge->mustPos) {
 276                         OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
 277                         if (invEdge != NULL) {
 278                                 if (!invEdge->mustPos) {
 279                                         invEdge->polPos = false;
 280                                 } else
 281                                         solver->setUnSAT();
 282                                 invEdge->mustNeg = true;
 283                                 invEdge->polNeg = true;
 284                         }
 285                 }
 286         }
 287         delete iterator;
 288 }
 289
 290 /** This finds edges that must be positive and forces the inverse edge
 291     to be negative.  It also clears the negative flag of this edge.
 292     It also finds edges that must be negative and clears the positive
 293     polarity. */
 294
 295 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
 296         SetIteratorOrderEdge *iterator = graph->getEdges();
 297         while (iterator->hasNext()) {
 298                 OrderEdge *edge = iterator->next();
 299                 if (edge->mustPos) {
 300                         if (!edge->mustNeg) {
 301                                 edge->polNeg = false;
 302                         } else {
 303                                 solver->setUnSAT();
 304                         }
 305                         OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
 306                         if (invEdge != NULL) {
 307                                 if (!invEdge->mustPos)
 308                                         invEdge->polPos = false;
 309                                 else
 310                                         solver->setUnSAT();
 311                                 invEdge->mustNeg = true;
 312                                 invEdge->polNeg = true;
 313                         }
 314                 }
 315                 if (edge->mustNeg && !edge->mustPos) {
 316                         edge->polPos = false;
 317                 }
 318         }
 319         delete iterator;
 320 }