Repair/RepairCompiler/MCC/IR/Termination.java

   1 package MCC.IR;
   2 import java.util.*;
   3 import java.io.*;
   4 import MCC.State;
   5
   6 public class Termination {
   7     HashSet conjunctions;
   8     Hashtable conjunctionmap;
   9
  10     HashSet abstractrepair;
  11     HashSet updatenodes;
  12     HashSet consequencenodes;
  13
  14     HashSet scopenodes;
  15     Hashtable scopesatisfy;
  16     Hashtable scopefalsify;
  17     Hashtable consequence;
  18
  19     State state;
  20
  21     public Termination(State state) {
  22         this.state=state;
  23         conjunctions=new HashSet();
  24         conjunctionmap=new Hashtable();
  25         abstractrepair=new HashSet();
  26         scopenodes=new HashSet();
  27         scopesatisfy=new Hashtable();
  28         scopefalsify=new Hashtable();
  29         consequence=new Hashtable();
  30         updatenodes=new HashSet();
  31         consequencenodes=new HashSet();
  32
  33         generateconjunctionnodes();
  34         generatescopenodes();
  35         generaterepairnodes();
  36         generatedatastructureupdatenodes();
  37
  38         generateabstractedges();
  39         generatescopeedges();
  40         generateupdateedges();
  41
  42         HashSet superset=new HashSet();
  43         superset.addAll(conjunctions);
  44         superset.addAll(abstractrepair);
  45         superset.addAll(updatenodes);
  46         superset.addAll(scopenodes);
  47         superset.addAll(consequencenodes);
  48         try {
  49             GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
  50         } catch (Exception e) {
  51             e.printStackTrace();
  52             System.exit(-1);
  53         }
  54     }
  55
  56     void generateconjunctionnodes() {
  57         Vector constraints=state.vConstraints;
  58         for(int i=0;i<constraints.size();i++) {
  59             Constraint c=(Constraint)constraints.get(i);
  60             DNFConstraint dnf=c.dnfconstraint;
  61             for(int j=0;j<dnf.size();j++) {
  62                 TermNode tn=new TermNode(c,dnf.get(j));
  63                 GraphNode gn=new GraphNode("Conjunction"+i+"B"+j,tn);
  64                 conjunctions.add(gn);
  65                 conjunctionmap.put(c,gn);
  66             }
  67         }
  68     }
  69
  70     void generateupdateedges() {
  71         for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
  72             GraphNode gn=(GraphNode)updateiterator.next();
  73             TermNode tn=(TermNode)gn.getOwner();
  74             MultUpdateNode mun=tn.getUpdate();
  75             /* Cycle through the rules to look for possible conflicts */
  76             for(int i=0;i<state.vRules.size();i++) {
  77                 Rule r=(Rule) state.vRules.get(i);
  78                 if (ConcreteInterferes.interferes(mun,r,true)) {
  79                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
  80                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
  81                     gn.addEdge(e);
  82                 }
  83                 if (ConcreteInterferes.interferes(mun,r,false)) {
  84                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
  85                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
  86                     gn.addEdge(e);
  87                 }
  88             }
  89         }
  90     }
  91
  92     void generateabstractedges() {
  93         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
  94             GraphNode gn=(GraphNode)absiterator.next();
  95             TermNode tn=(TermNode)gn.getOwner();
  96             AbstractRepair ar=(AbstractRepair)tn.getAbstract();
  97
  98             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
  99                 GraphNode gn2=(GraphNode)conjiterator.next();
 100                 TermNode tn2=(TermNode)gn2.getOwner();
 101                 Conjunction conj=tn2.getConjunction();
 102                 for(int i=0;i<conj.size();i++) {
 103                     DNFPredicate dp=conj.get(i);
 104                     if (AbstractInterferes.interferes(ar,dp)) {
 105                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 106                         gn.addEdge(e);
 107                         break;
 108                     }
 109                 }
 110             }
 111         }
 112     }
 113
 114     void generatescopeedges() {
 115         for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 116             GraphNode gn=(GraphNode)scopeiterator.next();
 117             TermNode tn=(TermNode)gn.getOwner();
 118             ScopeNode sn=tn.getScope();
 119
 120             /* Interference edges with conjunctions */
 121             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 122                 GraphNode gn2=(GraphNode)conjiterator.next();
 123                 TermNode tn2=(TermNode)gn2.getOwner();
 124                 Conjunction conj=tn2.getConjunction();
 125                 for(int i=0;i<conj.size();i++) {
 126                     DNFPredicate dp=conj.get(i);
 127                     if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),dp)) {
 128                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 129                         GraphNode gnconseq=(GraphNode)consequence.get(sn);
 130                         gnconseq.addEdge(e);
 131                         break;
 132                     }
 133                 }
 134             }
 135
 136             /* Now see if this could effect other model defintion rules */
 137             for(int i=0;i<state.vRules.size();i++) {
 138                 Rule r=(Rule) state.vRules.get(i);
 139                 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
 140                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 141                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 142                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 143                     gnconseq.addEdge(e);
 144                 }
 145                 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
 146                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 147                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 148                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 149                     gnconseq.addEdge(e);
 150                 }
 151             }
 152         }
 153     }
 154
 155
 156     void generaterepairnodes() {
 157         for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 158             GraphNode gn=(GraphNode)conjiterator.next();
 159             TermNode tn=(TermNode)gn.getOwner();
 160             Conjunction conj=tn.getConjunction();
 161             for(int i=0;i<conj.size();i++) {
 162                 DNFPredicate dp=conj.get(i);
 163                 int[] array=dp.getPredicate().getRepairs(dp.isNegated());
 164                 Descriptor d=dp.getPredicate().getDescriptor();
 165                 for(int j=0;j<array.length;j++) {
 166                     AbstractRepair ar=new AbstractRepair(dp,array[j],d);
 167                     TermNode tn2=new TermNode(ar);
 168                     GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+j,tn2);
 169                     GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
 170                     gn.addEdge(e);
 171                     abstractrepair.add(gn2);
 172                 }
 173             }
 174         }
 175     }
 176
 177     void generatedatastructureupdatenodes() {
 178         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 179             GraphNode gn=(GraphNode)absiterator.next();
 180             TermNode tn=(TermNode) gn.getOwner();
 181             AbstractRepair ar=tn.getAbstract();
 182             if (ar.getType()==AbstractRepair.ADDTOSET) {
 183                 generateaddtoset(gn,ar);
 184             } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
 185                 generateremovefromset(gn,ar);
 186             } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
 187                 generateaddtorelation(gn,ar);
 188             } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
 189                 generateremovefromrelation(gn,ar);
 190             } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 191                 generatemodifyrelation(gn,ar);
 192             }
 193         }
 194     }
 195
 196     void generateremovefromset(GraphNode gn,AbstractRepair ar) {
 197         Vector possiblerules=new Vector();
 198         for(int i=0;i<state.vRules.size();i++) {
 199             Rule r=(Rule) state.vRules.get(i);
 200             if ((r.getInclusion() instanceof SetInclusion)&&
 201                 (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
 202                 possiblerules.add(r);
 203         }
 204         int[] count=new int[possiblerules.size()];
 205         while(remains(count,possiblerules)) {
 206             MultUpdateNode mun=new MultUpdateNode(ar);
 207             for(int i=0;i<possiblerules.size();i++) {
 208                 UpdateNode un=new UpdateNode();
 209                 mun.addUpdate(un);
 210                 /* CODE HERE*/
 211             }
 212             increment(count,possiblerules);
 213         }
 214     }
 215
 216     static void increment(int count[], Vector rules) {
 217         count[0]++;
 218         for(int i=0;i<(rules.size()-1);i++) {
 219             if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
 220                 count[i+1]++;
 221                 count[i]=0;
 222             } else break;
 223         }
 224     }
 225
 226     static boolean remains(int count[], Vector rules) {
 227         for(int i=0;i<rules.size();i++) {
 228             if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
 229                 return false;
 230             }
 231         }
 232         return true;
 233     }
 234
 235     void generateremovefromrelation(GraphNode gn,AbstractRepair ar) {}
 236     void generateaddtorelation(GraphNode gn,AbstractRepair ar) {}
 237     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {}
 238
 239     static int addtocount=0;
 240     void generateaddtoset(GraphNode gn, AbstractRepair ar) {
 241         for(int i=0;i<state.vRules.size();i++) {
 242             Rule r=(Rule) state.vRules.get(i);
 243             if (r.getInclusion() instanceof SetInclusion) {
 244                 if (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()) {
 245                     //Generate add instruction
 246                     DNFRule dnfrule=r.getDNFGuardExpr();
 247                     for(int j=0;j<dnfrule.size();j++) {
 248                         Inclusion inc=r.getInclusion();
 249                         UpdateNode un=new UpdateNode();
 250                         /* First solve for quantifiers */
 251                         boolean goodupdate=true;
 252                         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 253                             Quantifier q=(Quantifier)iterator.next();
 254                             boolean foundall=true;
 255                             if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
 256                                 VarDescriptor vd=null;
 257                                 SetDescriptor set=null;
 258                                 if (q instanceof SetQuantifier) {
 259                                     vd=((SetQuantifier)q).getVar();
 260                                 } else
 261                                     vd=((ForQuantifier)q).getVar();
 262                                 if(inc instanceof SetInclusion) {
 263                                     SetInclusion si=(SetInclusion)inc;
 264                                     if ((si.elementexpr instanceof VarExpr)&&
 265                                         (((VarExpr)si.elementexpr).getVar()==vd)) {
 266                                         /* Can solve for v */
 267                                         Binding binding=new Binding(vd,0);
 268                                         un.addBinding(binding);
 269                                     } else
 270                                         foundall=false;
 271                                 } else if (inc instanceof RelationInclusion) {
 272                                     RelationInclusion ri=(RelationInclusion)inc;
 273                                     boolean f1=true;
 274                                     boolean f2=true;
 275                                     if ((ri.getLeftExpr() instanceof VarExpr)&&
 276                                         (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 277                                         /* Can solve for v */
 278                                         Binding binding=new Binding(vd,0);
 279                                         un.addBinding(binding);
 280                                     } else f1=false;
 281                                     if ((ri.getRightExpr() instanceof VarExpr)&&
 282                                         (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 283                                         /* Can solve for v */
 284                                         Binding binding=new Binding(vd,0);
 285                                         un.addBinding(binding);
 286                                     } else f2=false;
 287                                     if (!(f1||f2))
 288                                         foundall=false;
 289                                 } else throw new Error("Inclusion not recognized");
 290                             } else if (q instanceof RelationQuantifier) {
 291                                 RelationQuantifier rq=(RelationQuantifier)q;
 292                                 for(int k=0;k<2;k++) {
 293                                     VarDescriptor vd=(k==0)?rq.x:rq.y;
 294                                     if(inc instanceof SetInclusion) {
 295                                         SetInclusion si=(SetInclusion)inc;
 296                                         if ((si.elementexpr instanceof VarExpr)&&
 297                                             (((VarExpr)si.elementexpr).getVar()==vd)) {
 298                                             /* Can solve for v */
 299                                             Binding binding=new Binding(vd,0);
 300                                             un.addBinding(binding);
 301                                         } else
 302                                             foundall=false;
 303                                     } else if (inc instanceof RelationInclusion) {
 304                                         RelationInclusion ri=(RelationInclusion)inc;
 305                                         boolean f1=true;
 306                                         boolean f2=true;
 307                                         if ((ri.getLeftExpr() instanceof VarExpr)&&
 308                                             (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 309                                             /* Can solve for v */
 310                                             Binding binding=new Binding(vd,0);
 311                                             un.addBinding(binding);
 312                                         } else f1=false;
 313                                         if ((ri.getRightExpr() instanceof VarExpr)&&
 314                                                    (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 315                                             /* Can solve for v */
 316                                             Binding binding=new Binding(vd,0);
 317                                             un.addBinding(binding);
 318                                         } else f2=false;
 319                                         if (!(f1||f2))
 320                                             foundall=false;
 321                                     } else throw new Error("Inclusion not recognized");
 322                                 }
 323                             } else throw new Error("Quantifier not recognized");
 324                             if (!foundall) {
 325                                 goodupdate=false;
 326                                 break;
 327                             }
 328                             /* Now build update for tuple/set inclusion condition */
 329                             if(inc instanceof SetInclusion) {
 330                                 SetInclusion si=(SetInclusion)inc;
 331                                 if (!(si.elementexpr instanceof VarExpr)) {
 332                                     Updates up=new Updates(si.elementexpr,0);
 333                                     un.addUpdate(up);
 334                                 }
 335                             }
 336                             if (inc instanceof RelationInclusion) {
 337                                 RelationInclusion ri=(RelationInclusion)inc;
 338                                 if (!(ri.getLeftExpr() instanceof VarExpr)) {
 339                                     Updates up=new Updates(ri.getLeftExpr(),0);
 340                                     un.addUpdate(up);
 341                                 }
 342                                 if (!(ri.getRightExpr() instanceof VarExpr)) {
 343                                     Updates up=new Updates(ri.getRightExpr(),0);
 344                                     un.addUpdate(up);
 345                                 }
 346                             }
 347                             //Finally build necessary updates to satisfy conjunction
 348                             RuleConjunction ruleconj=dnfrule.get(j);
 349                             for(int k=0;k<ruleconj.size();k++) {
 350                                 DNFExpr de=ruleconj.get(k);
 351                                 Expr e=de.getExpr();
 352                                 if (e instanceof OpExpr) {
 353                                     OpExpr ex=(OpExpr)de.getExpr();
 354                                     Opcode op=ex.getOpcode();
 355                                     if (de.getNegation()) {
 356                                         /* remove negation through opcode translation */
 357                                         if (op==Opcode.GT)
 358                                             op=Opcode.LE;
 359                                         else if (op==Opcode.GE)
 360                                             op=Opcode.LT;
 361                                         else if (op==Opcode.EQ)
 362                                             op=Opcode.NE;
 363                                         else if (op==Opcode.NE)
 364                                             op=Opcode.EQ;
 365                                         else if (op==Opcode.LT)
 366                                             op=Opcode.GE;
 367                                         else if (op==Opcode.LE)
 368                                             op=Opcode.GT;
 369                                     }
 370                                     Updates up=new Updates(ex.left,ex.right,op);
 371                                     un.addUpdate(up);
 372                                 } else if (e instanceof ElementOfExpr) {
 373                                     Updates up=new Updates(e,de.getNegation());
 374                                     un.addUpdate(up);
 375                                 } else if (e instanceof TupleOfExpr) {
 376                                     Updates up=new Updates(e,de.getNegation());
 377                                     un.addUpdate(up);
 378                                 } else throw new Error("Error #213");
 379                             }
 380                         }
 381                         MultUpdateNode mun=new MultUpdateNode(ar);
 382                         mun.addUpdate(un);
 383                         TermNode tn=new TermNode(mun);
 384                         GraphNode gn2=new GraphNode("Update"+addtocount,tn);
 385                         GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
 386                         addtocount++;
 387                         gn.addEdge(e);
 388                         updatenodes.add(gn2);
 389                     }
 390                 }
 391             }
 392         }
 393     }
 394
 395     void generatescopenodes() {
 396         for(int i=0;i<state.vRules.size();i++) {
 397             Rule r=(Rule) state.vRules.get(i);
 398             ScopeNode satisfy=new ScopeNode(r,true);
 399             TermNode tnsatisfy=new TermNode(satisfy);
 400             GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
 401             ConsequenceNode cnsatisfy=new ConsequenceNode();
 402             TermNode ctnsatisfy=new TermNode(cnsatisfy);
 403             GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
 404             consequence.put(satisfy,cgnsatisfy);
 405             GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
 406             gnsatisfy.addEdge(esat);
 407             consequencenodes.add(cgnsatisfy);
 408             scopesatisfy.put(r,gnsatisfy);
 409             scopenodes.add(gnsatisfy);
 410
 411             ScopeNode falsify=new ScopeNode(r,false);
 412             TermNode tnfalsify=new TermNode(falsify);
 413             GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
 414             ConsequenceNode cnfalsify=new ConsequenceNode();
 415             TermNode ctnfalsify=new TermNode(cnfalsify);
 416             GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
 417             consequence.put(falsify,cgnfalsify);
 418             GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
 419             gnfalsify.addEdge(efals);
 420             consequencenodes.add(cgnfalsify);
 421             scopefalsify.put(r,gnfalsify);
 422             scopenodes.add(gnfalsify);
 423         }
 424     }
 425 }