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