src/ASTAnalyses/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 *allocOrderGraph(Order *order) {
   9         OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
  10         This->nodes = new HashSetOrderNode();
  11         This->edges = new HashSetOrderEdge();
  12         This->order = order;
  13         return This;
  14 }
  15
  16 OrderGraph *buildOrderGraph(Order *order) {
  17         OrderGraph *orderGraph = allocOrderGraph(order);
  18         uint constrSize = order->constraints.getSize();
  19         for (uint j = 0; j < constrSize; j++) {
  20                 addOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
  21         }
  22         return orderGraph;
  23 }
  24
  25 //Builds only the subgraph for the must order graph.
  26 OrderGraph *buildMustOrderGraph(Order *order) {
  27         OrderGraph *orderGraph = allocOrderGraph(order);
  28         uint constrSize = order->constraints.getSize();
  29         for (uint j = 0; j < constrSize; j++) {
  30                 addMustOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
  31         }
  32         return orderGraph;
  33 }
  34
  35 void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  36         Polarity polarity = constr->polarity;
  37         BooleanValue mustval = constr->boolVal;
  38         Order *order = graph->order;
  39         switch (polarity) {
  40         case P_BOTHTRUEFALSE:
  41         case P_TRUE: {
  42                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  43                 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
  44                         _1to2->mustPos = true;
  45                 _1to2->polPos = true;
  46                 node1->addNewOutgoingEdge(_1to2);
  47                 node2->addNewIncomingEdge(_1to2);
  48                 if (constr->polarity == P_TRUE)
  49                         break;
  50         }
  51         case P_FALSE: {
  52                 if (order->type == TOTAL) {
  53                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
  54                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  55                                 _2to1->mustPos = true;
  56                         _2to1->polPos = true;
  57                         node2->addNewOutgoingEdge(_2to1);
  58                         node1->addNewIncomingEdge(_2to1);
  59                 } else {
  60                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  61                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  62                                 _1to2->mustNeg = true;
  63                         _1to2->polNeg = true;
  64                         node1->addNewOutgoingEdge(_1to2);
  65                         node2->addNewIncomingEdge(_1to2);
  66                 }
  67                 break;
  68         }
  69         case P_UNDEFINED:
  70                 //There is an unreachable order constraint if this assert fires
  71                 ASSERT(0);
  72         }
  73 }
  74
  75 void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  76         BooleanValue mustval = constr->boolVal;
  77         Order *order = graph->order;
  78         switch (mustval) {
  79         case BV_UNSAT:
  80         case BV_MUSTBETRUE: {
  81                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  82                 _1to2->mustPos = true;
  83                 _1to2->polPos = true;
  84                 node1->addNewOutgoingEdge(_1to2);
  85                 node2->addNewIncomingEdge(_1to2);
  86                 if (constr->boolVal == BV_MUSTBETRUE)
  87                         break;
  88         }
  89         case BV_MUSTBEFALSE: {
  90                 if (order->type == TOTAL) {
  91                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
  92                         _2to1->mustPos = true;
  93                         _2to1->polPos = true;
  94                         node2->addNewOutgoingEdge(_2to1);
  95                         node1->addNewIncomingEdge(_2to1);
  96                 } else {
  97                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  98                         _1to2->mustNeg = true;
  99                         _1to2->polNeg = true;
 100                         node1->addNewOutgoingEdge(_1to2);
 101                         node2->addNewIncomingEdge(_1to2);
 102                 }
 103                 break;
 104         }
 105         case BV_UNDEFINED:
 106                 //Do Nothing
 107                 break;
 108         }
 109 }
 110
 111 OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
 112         OrderNode *node = new OrderNode(id);
 113         OrderNode *tmp = graph->nodes->get(node);
 114         if ( tmp != NULL) {
 115                 delete node;
 116                 node = tmp;
 117         } else {
 118                 graph->nodes->add(node);
 119         }
 120         return node;
 121 }
 122
 123 OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
 124         OrderNode node(id);
 125         OrderNode *tmp = graph->nodes->get(&node);
 126         return tmp;
 127 }
 128
 129 OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
 130         OrderEdge *edge = new OrderEdge(begin, end);
 131         OrderEdge *tmp = graph->edges->get(edge);
 132         if ( tmp != NULL ) {
 133                 delete edge;
 134                 edge = tmp;
 135         } else {
 136                 graph->edges->add(edge);
 137         }
 138         return edge;
 139 }
 140
 141 OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
 142         OrderEdge edge(begin, end);
 143         OrderEdge *tmp = graph->edges->get(&edge);
 144         return tmp;
 145 }
 146
 147 OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
 148         OrderEdge inverseedge(edge->sink, edge->source);
 149         OrderEdge *tmp = graph->edges->get(&inverseedge);
 150         return tmp;
 151 }
 152
 153 void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
 154         OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
 155         OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
 156         addOrderEdge(graph, from, to, bOrder);
 157 }
 158
 159 void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
 160         OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
 161         OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
 162         addMustOrderEdge(graph, from, to, bOrder);
 163 }
 164
 165 void deleteOrderGraph(OrderGraph *graph) {
 166         HSIteratorOrderNode *iterator = graph->nodes->iterator();
 167         while (iterator->hasNext()) {
 168                 OrderNode *node = iterator->next();
 169                 delete node;
 170         }
 171         delete iterator;
 172
 173         HSIteratorOrderEdge *eiterator = graph->edges->iterator();
 174         while (eiterator->hasNext()) {
 175                 OrderEdge *edge = eiterator->next();
 176                 delete edge;
 177         }
 178         delete eiterator;
 179         delete graph->nodes;
 180         delete graph->edges;
 181         ourfree(graph);
 182 }