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