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     Hashtable abstractadd;
  19     Hashtable abstractremove;
  20     Hashtable conjtonodemap;
  21     Set removedset;
  22
  23     State state;
  24
  25     public Termination(State state) {
  26         this.state=state;
  27         conjunctions=new HashSet();
  28         conjunctionmap=new Hashtable();
  29         abstractrepair=new HashSet();
  30         scopenodes=new HashSet();
  31         scopesatisfy=new Hashtable();
  32         scopefalsify=new Hashtable();
  33         consequence=new Hashtable();
  34         updatenodes=new HashSet();
  35         consequencenodes=new HashSet();
  36         abstractadd=new Hashtable();
  37         abstractremove=new Hashtable();
  38         conjtonodemap=new Hashtable();
  39
  40         generateconjunctionnodes();
  41         generatescopenodes();
  42         generaterepairnodes();
  43         generatedatastructureupdatenodes();
  44         generatecompensationnodes();
  45
  46         generateabstractedges();
  47         generatescopeedges();
  48         generateupdateedges();
  49
  50         HashSet superset=new HashSet();
  51         superset.addAll(conjunctions);
  52         HashSet closureset=new HashSet();
  53         //      closureset.addAll(updatenodes);
  54         //superset.addAll(abstractrepair);
  55         //superset.addAll(updatenodes);
  56         //superset.addAll(scopenodes);
  57         //superset.addAll(consequencenodes);
  58         GraphNode.computeclosure(superset,closureset);
  59         try {
  60             GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
  61         } catch (Exception e) {
  62             e.printStackTrace();
  63             System.exit(-1);
  64         }
  65         for(Iterator it=updatenodes.iterator();it.hasNext();) {
  66             GraphNode gn=(GraphNode)it.next();
  67             TermNode tn=(TermNode)gn.getOwner();
  68             MultUpdateNode mun=tn.getUpdate();
  69             System.out.println(gn.getTextLabel());
  70             System.out.println(mun.toString());
  71         }
  72         GraphAnalysis ga=new GraphAnalysis(this);
  73         removedset=ga.doAnalysis();
  74         if (removedset==null) {
  75             System.out.println("Can't generate terminating repair algorithm!");
  76             System.exit(-1);
  77         }
  78         System.out.println("Removing:");
  79         for(Iterator it=removedset.iterator();it.hasNext();) {
  80             GraphNode gn=(GraphNode)it.next();
  81             System.out.println(gn.getTextLabel());
  82         }
  83
  84         superset=new HashSet();
  85         superset.addAll(conjunctions);
  86         superset.removeAll(removedset);
  87         GraphNode.computeclosure(superset,removedset);
  88         try {
  89             GraphNode.DOTVisitor.visit(new FileOutputStream("graphfinal.dot"),superset);
  90         } catch (Exception e) {
  91             e.printStackTrace();
  92             System.exit(-1);
  93         }
  94
  95     }
  96
  97     void generateconjunctionnodes() {
  98         Vector constraints=state.vConstraints;
  99         for(int i=0;i<constraints.size();i++) {
 100             Constraint c=(Constraint)constraints.get(i);
 101             DNFConstraint dnf=c.dnfconstraint;
 102             for(int j=0;j<dnf.size();j++) {
 103                 TermNode tn=new TermNode(c,dnf.get(j));
 104                 GraphNode gn=new GraphNode("Conj"+i+"A"+j,
 105                                            "Conj ("+i+","+j+") "+dnf.get(j).name()
 106                                            ,tn);
 107                 conjunctions.add(gn);
 108                 if (!conjunctionmap.containsKey(c))
 109                     conjunctionmap.put(c,new HashSet());
 110                 ((Set)conjunctionmap.get(c)).add(gn);
 111                 conjtonodemap.put(dnf.get(j),gn);
 112             }
 113             for(int j=0;j<c.numQuantifiers();j++) {
 114                 Quantifier q=c.getQuantifier(j);
 115                 if (q instanceof SetQuantifier) {
 116                     SetQuantifier sq=(SetQuantifier)q;
 117                     VarExpr ve=new VarExpr(sq.getVar());
 118                     InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sq.getSet()));
 119                     DNFConstraint dconst=new DNFConstraint(ip);
 120                     dconst=dconst.not();
 121                     TermNode tn=new TermNode(c,dconst.get(0));
 122                     GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
 123                                                "Conj ("+i+","+j+") "+dconst.get(0).name()
 124                                                ,tn);
 125                     conjunctions.add(gn);
 126                     if (!conjunctionmap.containsKey(c))
 127                         conjunctionmap.put(c,new HashSet());
 128                     ((Set)conjunctionmap.get(c)).add(gn);
 129                     conjtonodemap.put(dconst.get(0),gn);
 130                 } else if (q instanceof RelationQuantifier) {
 131                     RelationQuantifier rq=(RelationQuantifier)q;
 132                     VarExpr ve=new VarExpr(rq.y);
 133                     InclusionPredicate ip=new InclusionPredicate(ve,new ImageSetExpr(rq.x,rq.getRelation()));
 134                     DNFConstraint dconst=new DNFConstraint(ip);
 135                     dconst=dconst.not();
 136                     TermNode tn=new TermNode(c,dconst.get(0));
 137                     GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
 138                                                "Conj ("+i+","+j+") "+dconst.get(0).name()
 139                                                ,tn);
 140                     conjunctions.add(gn);
 141                     if (!conjunctionmap.containsKey(c))
 142                         conjunctionmap.put(c,new HashSet());
 143                     ((Set)conjunctionmap.get(c)).add(gn);
 144                     conjtonodemap.put(dconst.get(0),gn);
 145                 }
 146             }
 147         }
 148     }
 149
 150     void generateupdateedges() {
 151         for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
 152             GraphNode gn=(GraphNode)updateiterator.next();
 153             TermNode tn=(TermNode)gn.getOwner();
 154             MultUpdateNode mun=tn.getUpdate();
 155             /* Cycle through the rules to look for possible conflicts */
 156             for(int i=0;i<state.vRules.size();i++) {
 157                 Rule r=(Rule) state.vRules.get(i);
 158                 if (ConcreteInterferes.interferes(mun,r,true)) {
 159                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 160                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 161                     gn.addEdge(e);
 162                 }
 163                 if (ConcreteInterferes.interferes(mun,r,false)) {
 164                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 165                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 166                     gn.addEdge(e);
 167                 }
 168             }
 169         }
 170     }
 171
 172     void generateabstractedges() {
 173         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 174             GraphNode gn=(GraphNode)absiterator.next();
 175             TermNode tn=(TermNode)gn.getOwner();
 176             AbstractRepair ar=(AbstractRepair)tn.getAbstract();
 177
 178             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 179                 GraphNode gn2=(GraphNode)conjiterator.next();
 180                 TermNode tn2=(TermNode)gn2.getOwner();
 181                 Conjunction conj=tn2.getConjunction();
 182                 Constraint cons=tn2.getConstraint();
 183
 184                 for(int i=0;i<conj.size();i++) {
 185                     DNFPredicate dp=conj.get(i);
 186                     if (AbstractInterferes.interferes(ar,cons)||
 187                         AbstractInterferes.interferes(ar,dp)) {
 188                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 189                         gn.addEdge(e);
 190                         break;
 191                     }
 192                 }
 193             }
 194
 195             for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 196                 GraphNode gn2=(GraphNode)scopeiterator.next();
 197                 TermNode tn2=(TermNode)gn2.getOwner();
 198                 ScopeNode sn2=tn2.getScope();
 199                 if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) {
 200                     GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 201                     gn.addEdge(e);
 202                 }
 203             }
 204         }
 205     }
 206
 207     void generatescopeedges() {
 208         for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 209             GraphNode gn=(GraphNode)scopeiterator.next();
 210             TermNode tn=(TermNode)gn.getOwner();
 211             ScopeNode sn=tn.getScope();
 212
 213             /* Interference edges with conjunctions */
 214             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 215                 GraphNode gn2=(GraphNode)conjiterator.next();
 216                 TermNode tn2=(TermNode)gn2.getOwner();
 217                 Conjunction conj=tn2.getConjunction();
 218                 Constraint constr=tn2.getConstraint();
 219                 for(int i=0;i<conj.size();i++) {
 220                     DNFPredicate dp=conj.get(i);
 221                     if (AbstractInterferes.interferes(sn,dp)||
 222                         AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),constr)) {
 223                         GraphNode.Edge e=new GraphNode.Edge("interferes",gn2);
 224                         GraphNode gnconseq=(GraphNode)consequence.get(sn);
 225                         gnconseq.addEdge(e);
 226                         break;
 227                     }
 228                 }
 229             }
 230
 231             /* Now see if this could effect other model defintion rules */
 232             for(int i=0;i<state.vRules.size();i++) {
 233                 Rule r=(Rule) state.vRules.get(i);
 234                 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
 235                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 236                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 237                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 238                     gnconseq.addEdge(e);
 239                 }
 240                 if (AbstractInterferes.interferes(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
 241                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 242                     GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode);
 243                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 244                     gnconseq.addEdge(e);
 245                 }
 246             }
 247         }
 248     }
 249
 250     /* Generates the abstract repair nodes */
 251     void generaterepairnodes() {
 252         /* Generate repairs of conjunctions */
 253         for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 254             GraphNode gn=(GraphNode)conjiterator.next();
 255             TermNode tn=(TermNode)gn.getOwner();
 256             Conjunction conj=tn.getConjunction();
 257             for(int i=0;i<conj.size();i++) {
 258                 DNFPredicate dp=conj.get(i);
 259                 int[] array=dp.getPredicate().getRepairs(dp.isNegated());
 260                 Descriptor d=dp.getPredicate().getDescriptor();
 261                 for(int j=0;j<array.length;j++) {
 262                     AbstractRepair ar=new AbstractRepair(dp,array[j],d);
 263                     TermNode tn2=new TermNode(ar);
 264                     GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
 265                     GraphNode.Edge e=new GraphNode.Edge("abstract",gn2);
 266                     gn.addEdge(e);
 267                     abstractrepair.add(gn2);
 268                 }
 269             }
 270         }
 271         /* Generate additional abstract repairs */
 272         Vector setdescriptors=state.stSets.getAllDescriptors();
 273         for(int i=0;i<setdescriptors.size();i++) {
 274             SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
 275
 276             /* XXXXXXX: Not sure what to do here */
 277             VarExpr ve=new VarExpr("DUMMY");
 278             InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
 279
 280             DNFPredicate tp=new DNFPredicate(false,ip);
 281             AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd);
 282             TermNode tn=new TermNode(ar);
 283             GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
 284             abstractrepair.add(gn);
 285             abstractadd.put(sd,gn);
 286
 287             DNFPredicate tp2=new DNFPredicate(true,ip);
 288             AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd);
 289             TermNode tn2=new TermNode(ar2);
 290             GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
 291             abstractrepair.add(gn2);
 292             abstractremove.put(sd,gn2);
 293         }
 294
 295         Vector relationdescriptors=state.stRelations.getAllDescriptors();
 296         for(int i=0;i<relationdescriptors.size();i++) {
 297             RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
 298
 299             /* XXXXXXX: Not sure what to do here */
 300             VarDescriptor vd1=new VarDescriptor("DUMMY1");
 301             VarExpr ve2=new VarExpr("DUMMY2");
 302
 303             InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
 304
 305             DNFPredicate tp=new DNFPredicate(false,ip);
 306             AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd);
 307             TermNode tn=new TermNode(ar);
 308             GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
 309             abstractrepair.add(gn);
 310             abstractadd.put(rd,gn);
 311
 312             DNFPredicate tp2=new DNFPredicate(true,ip);
 313             AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd);
 314             TermNode tn2=new TermNode(ar2);
 315             GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
 316             abstractrepair.add(gn2);
 317             abstractremove.put(rd,gn2);
 318         }
 319
 320     }
 321
 322     int compensationcount=0;
 323     void generatecompensationnodes() {
 324         for(int i=0;i<state.vRules.size();i++) {
 325             Rule r=(Rule) state.vRules.get(i);
 326             Vector possiblerules=new Vector();
 327             /* Construct bindings */
 328             /* No need to construct bindings on remove
 329                Vector bindings=new Vector();
 330                constructbindings(bindings, r,true);
 331             */
 332             for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
 333                 GraphNode gn=(GraphNode)scopesatisfy.get(r);
 334                 TermNode tn=(TermNode) gn.getOwner();
 335                 ScopeNode sn=tn.getScope();
 336                 MultUpdateNode mun=new MultUpdateNode(sn);
 337                 TermNode tn2=new TermNode(mun);
 338                 GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
 339                 UpdateNode un=new UpdateNode(r);
 340                 //              un.addBindings(bindings);
 341                 // Not necessary
 342                 if (j<r.numQuantifiers()) {
 343                     /* Remove quantifier */
 344                     Quantifier q=r.getQuantifier(j);
 345                     if (q instanceof RelationQuantifier) {
 346                         RelationQuantifier rq=(RelationQuantifier)q;
 347                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 348                         toe.td=ReservedTypeDescriptor.INT;
 349                         Updates u=new Updates(toe,true);
 350                         un.addUpdate(u);
 351                         if (abstractremove.containsKey(rq.relation)) {
 352                             GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
 353                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 354                             gn2.addEdge(e);
 355                         } else {
 356                             continue; /* Abstract repair doesn't exist */
 357                         }
 358                     } else if (q instanceof SetQuantifier) {
 359                         SetQuantifier sq=(SetQuantifier)q;
 360                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 361                         eoe.td=ReservedTypeDescriptor.INT;
 362                         Updates u=new Updates(eoe,true);
 363                         un.addUpdate(u);
 364                         if (abstractremove.containsKey(sq.set)) {
 365                             GraphNode agn=(GraphNode)abstractremove.get(sq.set);
 366                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 367                             gn2.addEdge(e);
 368                         } else {
 369                             continue; /* Abstract repair doesn't exist */
 370                         }
 371                     } else {
 372                         continue;
 373                     }
 374                 } else {
 375                     int c=j-r.numQuantifiers();
 376                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
 377                         continue;
 378                     }
 379                 }
 380                 if (!un.checkupdates()) /* Make sure we have a good update */
 381                     continue;
 382
 383                 mun.addUpdate(un);
 384
 385                 GraphNode.Edge e=new GraphNode.Edge("abstract"+compensationcount,gn2);
 386                 compensationcount++;
 387                 gn.addEdge(e);
 388                 updatenodes.add(gn2);
 389             }
 390         }
 391     }
 392
 393     void generatedatastructureupdatenodes() {
 394         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 395             GraphNode gn=(GraphNode)absiterator.next();
 396             TermNode tn=(TermNode) gn.getOwner();
 397             AbstractRepair ar=tn.getAbstract();
 398             if (ar.getType()==AbstractRepair.ADDTOSET) {
 399                 generateaddtosetrelation(gn,ar);
 400             } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
 401                 generateremovefromsetrelation(gn,ar);
 402             } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
 403                 generateaddtosetrelation(gn,ar);
 404             } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
 405                 generateremovefromsetrelation(gn,ar);
 406             } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 407                 /* Generate remove/add pairs */
 408                 generateremovefromsetrelation(gn,ar);
 409                 generateaddtosetrelation(gn,ar);
 410                 /* Generate atomic modify */
 411                 generatemodifyrelation(gn,ar);
 412             }
 413         }
 414     }
 415
 416     int removefromcount=0;
 417     void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
 418         Vector possiblerules=new Vector();
 419         for(int i=0;i<state.vRules.size();i++) {
 420             Rule r=(Rule) state.vRules.get(i);
 421             if ((r.getInclusion() instanceof SetInclusion)&&
 422                 (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
 423                 possiblerules.add(r);
 424             if ((r.getInclusion() instanceof RelationInclusion)&&
 425                 (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
 426                 possiblerules.add(r);
 427         }
 428         if (possiblerules.size()==0)
 429             return;
 430         int[] count=new int[possiblerules.size()];
 431         while(remains(count,possiblerules)) {
 432             MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
 433             TermNode tn=new TermNode(mun);
 434             GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
 435
 436             boolean goodflag=true;
 437             for(int i=0;i<possiblerules.size();i++) {
 438                 Rule r=(Rule)possiblerules.get(i);
 439                 UpdateNode un=new UpdateNode(r);
 440                 /* Construct bindings */
 441                 /* No Need to construct bindings on remove
 442                    Vector bindings=new Vector();
 443                    constructbindings(bindings, r,true);
 444                   un.addBindings(bindings);*/
 445                 if (count[i]<r.numQuantifiers()) {
 446                     /* Remove quantifier */
 447                     Quantifier q=r.getQuantifier(count[i]);
 448                     if (q instanceof RelationQuantifier) {
 449                         RelationQuantifier rq=(RelationQuantifier)q;
 450                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 451                         toe.td=ReservedTypeDescriptor.INT;
 452                         Updates u=new Updates(toe,true);
 453                         un.addUpdate(u);
 454                         if (abstractremove.containsKey(rq.relation)) {
 455                             GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
 456                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 457                             gn2.addEdge(e);
 458                         } else {
 459                             goodflag=false;break; /* Abstract repair doesn't exist */
 460                         }
 461                     } else if (q instanceof SetQuantifier) {
 462                         SetQuantifier sq=(SetQuantifier)q;
 463                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 464                         eoe.td=ReservedTypeDescriptor.INT;
 465                         Updates u=new Updates(eoe,true);
 466                         un.addUpdate(u);
 467                         if (abstractremove.containsKey(sq.set)) {
 468                             GraphNode agn=(GraphNode)abstractremove.get(sq.set);
 469                             GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 470                             gn2.addEdge(e);
 471                         } else {
 472                             goodflag=false;break; /* Abstract repair doesn't exist */
 473                         }
 474                     } else {goodflag=false;break;}
 475                 } else {
 476                     int c=count[i]-r.numQuantifiers();
 477                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c))) {
 478                         goodflag=false;break;
 479                     }
 480                 }
 481                 if (!un.checkupdates()) {
 482                     goodflag=false;
 483                     break;
 484                 }
 485                 mun.addUpdate(un);
 486             }
 487             if (goodflag) {
 488                 GraphNode.Edge e=new GraphNode.Edge("abstract"+removefromcount,gn2);
 489                 removefromcount++;
 490                 gn.addEdge(e);
 491                 updatenodes.add(gn2);
 492             }
 493             increment(count,possiblerules);
 494         }
 495     }
 496
 497     static void increment(int count[], Vector rules) {
 498         count[0]++;
 499         for(int i=0;i<(rules.size()-1);i++) {
 500             if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
 501                 count[i+1]++;
 502                 count[i]=0;
 503             } else break;
 504         }
 505     }
 506
 507     static boolean remains(int count[], Vector rules) {
 508         for(int i=0;i<rules.size();i++) {
 509             if (count[i]>=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) {
 510                 return false;
 511             }
 512         }
 513         return true;
 514     }
 515
 516     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
 517     }
 518
 519
 520     boolean constructbindings(Vector bindings, Rule r, boolean isremoval) {
 521         boolean goodupdate=true;
 522         Inclusion inc=r.getInclusion();
 523         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 524             Quantifier q=(Quantifier)iterator.next();
 525             if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
 526                 VarDescriptor vd=null;
 527                 SetDescriptor set=null;
 528                 if (q instanceof SetQuantifier) {
 529                     vd=((SetQuantifier)q).getVar();
 530                 } else
 531                     vd=((ForQuantifier)q).getVar();
 532                 if(inc instanceof SetInclusion) {
 533                     SetInclusion si=(SetInclusion)inc;
 534                     if ((si.elementexpr instanceof VarExpr)&&
 535                         (((VarExpr)si.elementexpr).getVar()==vd)) {
 536                         /* Can solve for v */
 537                         Binding binding=new Binding(vd,0);
 538                         bindings.add(binding);
 539                     } else
 540                         goodupdate=false;
 541                 } else if (inc instanceof RelationInclusion) {
 542                     RelationInclusion ri=(RelationInclusion)inc;
 543                     boolean f1=true;
 544                     boolean f2=true;
 545                     if ((ri.getLeftExpr() instanceof VarExpr)&&
 546                         (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 547                                 /* Can solve for v */
 548                         Binding binding=new Binding(vd,0);
 549                         bindings.add(binding);
 550                     } else f1=false;
 551                     if ((ri.getRightExpr() instanceof VarExpr)&&
 552                         (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 553                                 /* Can solve for v */
 554                         Binding binding=new Binding(vd,0);
 555                         bindings.add(binding);
 556                     } else f2=false;
 557                     if (!(f1||f2))
 558                         goodupdate=false;
 559                 } else throw new Error("Inclusion not recognized");
 560                 if (!goodupdate)
 561                     if (isremoval) {
 562                         Binding binding=new Binding(vd);
 563                         bindings.add(binding);
 564                         goodupdate=true;
 565                     } else
 566                         break;
 567             } else if (q instanceof RelationQuantifier) {
 568                 RelationQuantifier rq=(RelationQuantifier)q;
 569                 for(int k=0;k<2;k++) {
 570                     VarDescriptor vd=(k==0)?rq.x:rq.y;
 571                     if(inc instanceof SetInclusion) {
 572                         SetInclusion si=(SetInclusion)inc;
 573                         if ((si.elementexpr instanceof VarExpr)&&
 574                             (((VarExpr)si.elementexpr).getVar()==vd)) {
 575                             /* Can solve for v */
 576                             Binding binding=new Binding(vd,0);
 577                             bindings.add(binding);
 578                         } else
 579                             goodupdate=false;
 580                     } else if (inc instanceof RelationInclusion) {
 581                         RelationInclusion ri=(RelationInclusion)inc;
 582                         boolean f1=true;
 583                         boolean f2=true;
 584                         if ((ri.getLeftExpr() instanceof VarExpr)&&
 585                             (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
 586                             /* Can solve for v */
 587                             Binding binding=new Binding(vd,0);
 588                             bindings.add(binding);
 589                         } else f1=false;
 590                         if ((ri.getRightExpr() instanceof VarExpr)&&
 591                             (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
 592                             /* Can solve for v */
 593                             Binding binding=new Binding(vd,0);
 594                             bindings.add(binding);
 595                         } else f2=false;
 596                         if (!(f1||f2))
 597                             goodupdate=false;
 598                     } else throw new Error("Inclusion not recognized");
 599                     if (!goodupdate)
 600                         if (isremoval) {
 601                             Binding binding=new Binding(vd);
 602                             bindings.add(binding);
 603                             goodupdate=true;
 604                         } else
 605                             break;
 606                 }
 607                 if (!goodupdate)
 608                     break;
 609             } else throw new Error("Quantifier not recognized");
 610         }
 611         return goodupdate;
 612     }
 613
 614     static int addtocount=0;
 615     void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
 616         //      System.out.println("Attempting to generate add to set");
 617         //System.out.println(ar.getPredicate().getPredicate().name());
 618         //System.out.println(ar.getPredicate().isNegated());
 619         for(int i=0;i<state.vRules.size();i++) {
 620             Rule r=(Rule) state.vRules.get(i);
 621             /* See if this is a good rule*/
 622             //System.out.println(r.getGuardExpr().name());
 623             if ((r.getInclusion() instanceof SetInclusion&&
 624                 ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
 625                 (r.getInclusion() instanceof RelationInclusion&&
 626                  ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
 627
 628                 /* First solve for quantifiers */
 629                 Vector bindings=new Vector();
 630                 /* Construct bindings */
 631                 //System.out.println("Attempting to generate add to set: #2");
 632                 if (!constructbindings(bindings,r,false))
 633                     continue;
 634                 //System.out.println("Attempting to generate add to set: #3");
 635                 //Generate add instruction
 636                 DNFRule dnfrule=r.getDNFGuardExpr();
 637                 for(int j=0;j<dnfrule.size();j++) {
 638                     Inclusion inc=r.getInclusion();
 639                     UpdateNode un=new UpdateNode(r);
 640                     un.addBindings(bindings);
 641                     /* Now build update for tuple/set inclusion condition */
 642                     if(inc instanceof SetInclusion) {
 643                         SetInclusion si=(SetInclusion)inc;
 644                         if (!(si.elementexpr instanceof VarExpr)) {
 645                             Updates up=new Updates(si.elementexpr,0);
 646                             un.addUpdate(up);
 647                         } else {
 648                             VarDescriptor vd=((VarExpr)si.elementexpr).getVar();
 649                             if (un.getBinding(vd)==null) {
 650                                 Updates up=new Updates(si.elementexpr,0);
 651                                 un.addUpdate(up);
 652                             }
 653                         }
 654                     } else if (inc instanceof RelationInclusion) {
 655                         RelationInclusion ri=(RelationInclusion)inc;
 656                         if (!(ri.getLeftExpr() instanceof VarExpr)) {
 657                             Updates up=new Updates(ri.getLeftExpr(),0);
 658                             un.addUpdate(up);
 659                         } else {
 660                             VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
 661                             if (un.getBinding(vd)==null) {
 662                                 Updates up=new Updates(ri.getLeftExpr(),0);
 663                                 un.addUpdate(up);
 664                             }
 665                         }
 666                         if (!(ri.getRightExpr() instanceof VarExpr)) {
 667                             Updates up=new Updates(ri.getRightExpr(),1);
 668                             un.addUpdate(up);
 669                         } else {
 670                             VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
 671                             if (un.getBinding(vd)==null) {
 672                                 Updates up=new Updates(ri.getRightExpr(),1);
 673                                 un.addUpdate(up);
 674                             }
 675                         }
 676                     }
 677                     //Finally build necessary updates to satisfy conjunction
 678                     RuleConjunction ruleconj=dnfrule.get(j);
 679                     /* Add in updates for quantifiers */
 680                     //System.out.println("Attempting to generate add to set #4");
 681                     MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
 682                     TermNode tn=new TermNode(mun);
 683                     GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
 684
 685                     if (processquantifers(gn2,un, r)&&debugdd()&&
 686                         processconjunction(un,ruleconj)&&
 687                         un.checkupdates()) {
 688                         //System.out.println("Attempting to generate add to set #5");
 689                         mun.addUpdate(un);
 690                         GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
 691                         addtocount++;
 692                         gn.addEdge(e);
 693                         updatenodes.add(gn2);}
 694                 }
 695             }
 696         }
 697     }
 698
 699     boolean debugdd() {
 700         //System.out.println("Attempting to generate add to set DD");
 701         return true;
 702     }
 703
 704     boolean processquantifers(GraphNode gn,UpdateNode un, Rule r) {
 705         Inclusion inc=r.getInclusion();
 706         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
 707             Quantifier q=(Quantifier)iterator.next();
 708             /* Add quantifier */
 709             /* FIXME: Analysis to determine when this update is necessary */
 710             if (q instanceof RelationQuantifier) {
 711                 RelationQuantifier rq=(RelationQuantifier)q;
 712                 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 713                 toe.td=ReservedTypeDescriptor.INT;
 714                 Updates u=new Updates(toe,false);
 715                 un.addUpdate(u);
 716                 if (abstractremove.containsKey(rq.relation)) {
 717                     GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
 718                     GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 719                     gn.addEdge(e);
 720                 } else {
 721                     return false;
 722                 }
 723
 724             } else if (q instanceof SetQuantifier) {
 725                 SetQuantifier sq=(SetQuantifier)q;
 726                 ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 727                 eoe.td=ReservedTypeDescriptor.INT;
 728                 Updates u=new Updates(eoe,false);
 729                 un.addUpdate(u);
 730                 if (abstractremove.containsKey(sq.set)) {
 731                     GraphNode agn=(GraphNode)abstractadd.get(sq.set);
 732                     GraphNode.Edge e=new GraphNode.Edge("requires",agn);
 733                     gn.addEdge(e);
 734                 } else {
 735                     return false;
 736                 }
 737             } else return false;
 738         }
 739         return true;
 740     }
 741
 742     boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj){
 743         boolean okay=true;
 744         for(int k=0;k<ruleconj.size();k++) {
 745             DNFExpr de=ruleconj.get(k);
 746             Expr e=de.getExpr();
 747             if (e instanceof OpExpr) {
 748                 OpExpr ex=(OpExpr)de.getExpr();
 749                 Opcode op=ex.getOpcode();
 750                 Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
 751                 un.addUpdate(up);
 752             } else if (e instanceof ElementOfExpr) {
 753                 Updates up=new Updates(e,de.getNegation());
 754                 un.addUpdate(up);
 755             } else if (e instanceof TupleOfExpr) {
 756                 Updates up=new Updates(e,de.getNegation());
 757                 un.addUpdate(up);
 758             } else if (e instanceof BooleanLiteralExpr) {
 759                 boolean truth=((BooleanLiteralExpr)e).getValue();
 760                 if (de.getNegation())
 761                     truth=!truth;
 762                 if (!truth) {
 763                     okay=false;
 764                     break;
 765                 }
 766             } else {
 767                 System.out.println(e.getClass().getName());
 768                 throw new Error("Error #213");
 769             }
 770         }
 771         return okay;
 772     }
 773
 774     void generatescopenodes() {
 775         for(int i=0;i<state.vRules.size();i++) {
 776             Rule r=(Rule) state.vRules.get(i);
 777             ScopeNode satisfy=new ScopeNode(r,true);
 778             TermNode tnsatisfy=new TermNode(satisfy);
 779             GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
 780             ConsequenceNode cnsatisfy=new ConsequenceNode();
 781             TermNode ctnsatisfy=new TermNode(cnsatisfy);
 782             GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
 783             consequence.put(satisfy,cgnsatisfy);
 784             GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
 785             gnsatisfy.addEdge(esat);
 786             consequencenodes.add(cgnsatisfy);
 787             scopesatisfy.put(r,gnsatisfy);
 788             scopenodes.add(gnsatisfy);
 789
 790             ScopeNode falsify=new ScopeNode(r,false);
 791             TermNode tnfalsify=new TermNode(falsify);
 792             GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
 793             ConsequenceNode cnfalsify=new ConsequenceNode();
 794             TermNode ctnfalsify=new TermNode(cnfalsify);
 795             GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
 796             consequence.put(falsify,cgnfalsify);
 797             GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
 798             gnfalsify.addEdge(efals);
 799             consequencenodes.add(cgnfalsify);
 800             scopefalsify.put(r,gnfalsify);
 801             scopenodes.add(gnfalsify);
 802         }
 803     }
 804 }