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