Repair/RepairCompiler/MCC/IR/Termination.java

   1 package MCC.IR;
   2 import java.util.*;
   3 import java.io.*;
   4 import MCC.State;
   5 import MCC.Compiler;
   6
   7 public class Termination {
   8     HashSet conjunctions;
   9     Hashtable conjunctionmap;
  10
  11     HashSet abstractrepair;
  12     HashSet abstractrepairadd;
  13
  14     HashSet updatenodes;
  15     HashSet consequencenodes;
  16
  17     HashSet scopenodes;
  18     Hashtable scopesatisfy;
  19     Hashtable scopefalsify;
  20     Hashtable consequence;
  21     Hashtable abstractadd;
  22     Hashtable abstractremove;
  23     Hashtable conjtonodemap;
  24     Hashtable predtoabstractmap;
  25     Set removedset;
  26     ComputeMaxSize maxsize;
  27     State state;
  28     AbstractInterferes abstractinterferes;
  29     ConcreteInterferes concreteinterferes;
  30     ConstraintDependence constraintdependence;
  31     ExactSize exactsize;
  32     ArrayAnalysis arrayanalysis;
  33     Sources sources;
  34     static String conjoption="style=bold";
  35     static String absrepoption="shape=box,color=blue,style=bold";
  36     static String updateoption="shape=box,color=red,style=bold";
  37     static String scopeoption="color=brown";
  38     static String conseqoption="style=bold,color=green";
  39     static String compoption="shape=box,color=purple,style=bold";
  40
  41     public Termination(State state) {
  42         this.state=state;
  43         conjunctions=new HashSet();
  44         conjunctionmap=new Hashtable();
  45         abstractrepair=new HashSet();
  46         abstractrepairadd=new HashSet();
  47         scopenodes=new HashSet();
  48         scopesatisfy=new Hashtable();
  49         scopefalsify=new Hashtable();
  50         consequence=new Hashtable();
  51         updatenodes=new HashSet();
  52         consequencenodes=new HashSet();
  53         abstractadd=new Hashtable();
  54         abstractremove=new Hashtable();
  55         conjtonodemap=new Hashtable();
  56         predtoabstractmap=new Hashtable();
  57         if (!Compiler.REPAIR)
  58             return;
  59
  60
  61         for(int i=0;i<state.vRules.size();i++)
  62             System.out.println(state.vRules.get(i));
  63         for(int i=0;i<state.vConstraints.size();i++)
  64             System.out.println(state.vConstraints.get(i));
  65
  66         sources=new Sources(state);
  67         maxsize=new ComputeMaxSize(state);
  68         exactsize=new ExactSize(state);
  69         arrayanalysis=new ArrayAnalysis(state,this);
  70
  71         abstractinterferes=new AbstractInterferes(this);
  72         concreteinterferes=new ConcreteInterferes(this);
  73         generateconjunctionnodes();
  74         constraintdependence=new ConstraintDependence(state,this);
  75
  76         debugmsg("*****Generating scope nodes*****");
  77         generatescopenodes();
  78         debugmsg("*****Generating repair nodes*****");
  79         generaterepairnodes();
  80         debugmsg("*****Generating data structure nodes*****");
  81         generatedatastructureupdatenodes();
  82         debugmsg("*****Generating compensation nodes*****");
  83         if (!Compiler.OMITCOMP)
  84             generatecompensationnodes();
  85         debugmsg("*****Generating abstract edges*****");
  86         generateabstractedges();
  87         debugmsg("*****Generating scope edges*****");
  88         generatescopeedges();
  89         debugmsg("*****Generating update edges*****");
  90         generateupdateedges();
  91
  92
  93         HashSet superset=new HashSet();
  94         superset.addAll(conjunctions);
  95         HashSet closureset=new HashSet();
  96         debugmsg("Computing closure");
  97         GraphNode.computeclosure(superset,closureset);
  98         try {
  99             GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
 100         } catch (Exception e) {
 101             e.printStackTrace();
 102             System.exit(-1);
 103         }
 104
 105         generatedebuggraphs();
 106
 107         for(Iterator it=updatenodes.iterator();it.hasNext();) {
 108             GraphNode gn=(GraphNode)it.next();
 109             TermNode tn=(TermNode)gn.getOwner();
 110             MultUpdateNode mun=tn.getUpdate();
 111             System.out.println(gn.getTextLabel());
 112             System.out.println(mun.toString());
 113         }
 114         GraphAnalysis ga=new GraphAnalysis(this);
 115         removedset=ga.doAnalysis();
 116         if (removedset==null) {
 117             System.out.println("Can't generate terminating repair algorithm!");
 118             System.exit(-1);
 119         }
 120
 121         System.out.println("Removing:");
 122         for(Iterator it=removedset.iterator();it.hasNext();) {
 123             GraphNode gn=(GraphNode)it.next();
 124             System.out.println(gn.getTextLabel());
 125         }
 126
 127         superset=new HashSet();
 128         superset.addAll(conjunctions);
 129         superset.removeAll(removedset);
 130         GraphNode.computeclosure(superset,removedset);
 131         try {
 132             GraphNode.DOTVisitor.visit(new FileOutputStream("graphfinal.dot"),superset);
 133         } catch (Exception e) {
 134             e.printStackTrace();
 135             System.exit(-1);
 136         }
 137         constraintdependence.traversedependences(this);
 138     }
 139
 140     void generatedebuggraphs() {
 141         for (int i=0;i<Compiler.debuggraphs.size();i++) {
 142             DebugItem di=(DebugItem) Compiler.debuggraphs.get(i);
 143             HashSet superset=new HashSet();
 144             Constraint constr=(Constraint)state.vConstraints.get(di.constraintnum);
 145
 146             if (di.conjunctionnum==-1) {
 147                 superset.addAll((Set)conjunctionmap.get(constr));
 148             } else {
 149                 DNFConstraint dnf=constr.dnfconstraint;
 150                 superset.add(conjtonodemap.get(dnf.get(di.conjunctionnum)));
 151             }
 152
 153             GraphNode.boundedcomputeclosure(superset,null,di.depth);
 154             try {
 155                 GraphNode.DOTVisitor.visit(new FileOutputStream("graph"+di.constraintnum+"-"+di.depth+(di.conjunctionnum==-1?"":"-"+di.conjunctionnum)+".dot"),superset);
 156             } catch (Exception e) {
 157                 e.printStackTrace();
 158                 System.exit(-1);
 159             }
 160         }
 161     }
 162
 163
 164     /** This method generates a node for each conjunction in the DNF
 165      * form of each constraint.  It also converts the quantifiers into
 166      * conjunctions also - constraints can be satisfied by removing
 167      * items from the sets and relations they are quantified over */
 168
 169     void generateconjunctionnodes() {
 170         Vector constraints=state.vConstraints;
 171         // Constructs conjunction nodes
 172         for(int i=0;i<constraints.size();i++) {
 173             Constraint c=(Constraint)constraints.get(i);
 174             DNFConstraint dnf=c.dnfconstraint;
 175             for(int j=0;j<dnf.size();j++) {
 176                 TermNode tn=new TermNode(c,dnf.get(j));
 177                 GraphNode gn=new GraphNode("Conj"+i+"A"+j,
 178                                            "Conj ("+i+","+j+") "+dnf.get(j).name()
 179                                            ,tn);
 180                 gn.setOption(conjoption);
 181                 conjunctions.add(gn);
 182                 if (!conjunctionmap.containsKey(c))
 183                     conjunctionmap.put(c,new HashSet());
 184                 ((Set)conjunctionmap.get(c)).add(gn);
 185                 conjtonodemap.put(dnf.get(j),gn);
 186             }
 187             // Construct quantifier "conjunction" nodes
 188             for(int j=0;j<c.numQuantifiers();j++) {
 189                 Quantifier q=c.getQuantifier(j);
 190                 if (q instanceof SetQuantifier) {
 191                     SetQuantifier sq=(SetQuantifier)q;
 192                     VarExpr ve=new VarExpr(sq.getVar());
 193                     InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sq.getSet()));
 194                     DNFConstraint dconst=new DNFConstraint(ip);
 195                     dconst=dconst.not();
 196                     TermNode tn=new TermNode(c,dconst.get(0));
 197                     tn.setquantifiernode();
 198                     GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
 199                                                "Conj ("+i+","+j+") "+dconst.get(0).name()
 200                                                ,tn);
 201                     gn.setOption(conjoption);
 202                     conjunctions.add(gn);
 203                     if (!conjunctionmap.containsKey(c))
 204                         conjunctionmap.put(c,new HashSet());
 205                     ((Set)conjunctionmap.get(c)).add(gn);
 206                     conjtonodemap.put(dconst.get(0),gn);
 207
 208                 } else if (q instanceof RelationQuantifier) {
 209                     RelationQuantifier rq=(RelationQuantifier)q;
 210                     VarExpr ve=new VarExpr(rq.y);
 211                     InclusionPredicate ip=new InclusionPredicate(ve,new ImageSetExpr(rq.x,rq.getRelation()));
 212                     DNFConstraint dconst=new DNFConstraint(ip);
 213                     dconst=dconst.not();
 214                     TermNode tn=new TermNode(c,dconst.get(0));
 215                     tn.setquantifiernode();
 216                     GraphNode gn=new GraphNode("Conj"+i+"AQ"+j,
 217                                                "Conj ("+i+","+j+") "+dconst.get(0).name()
 218                                                ,tn);
 219                     gn.setOption(conjoption);
 220                     conjunctions.add(gn);
 221                     if (!conjunctionmap.containsKey(c))
 222                         conjunctionmap.put(c,new HashSet());
 223                     ((Set)conjunctionmap.get(c)).add(gn);
 224                     conjtonodemap.put(dconst.get(0),gn);
 225                 }
 226             }
 227         }
 228     }
 229
 230     void generateupdateedges() {
 231         for(Iterator updateiterator=updatenodes.iterator();updateiterator.hasNext();) {
 232             GraphNode gn=(GraphNode)updateiterator.next();
 233             TermNode tn=(TermNode)gn.getOwner();
 234             MultUpdateNode mun=tn.getUpdate();
 235             for(int i=0;i<mun.numUpdates();i++) {
 236                 UpdateNode un=mun.getUpdate(i);
 237                 for(int j=0;j<un.numUpdates();j++) {
 238                     Updates u=un.getUpdate(j);
 239                     if (u.getType()==Updates.ABSTRACT) {
 240                         Expr e=u.getLeftExpr();
 241                         boolean negated=u.negate;
 242                         if (e instanceof TupleOfExpr) {
 243                             TupleOfExpr toe=(TupleOfExpr)e;
 244                             if (negated) {
 245                                 GraphNode agn=(GraphNode)abstractremove.get(toe.relation);
 246                                 GraphNode.Edge edge=new GraphNode.Edge("requirestupleremove",agn);
 247                                 gn.addEdge(edge);
 248                             } else {
 249                                 GraphNode agn=(GraphNode)abstractadd.get(toe.relation);
 250                                 GraphNode.Edge edge=new GraphNode.Edge("requirestupleadd",agn);
 251                                 gn.addEdge(edge);
 252                             }
 253                         } else if (e instanceof ElementOfExpr) {
 254                             ElementOfExpr eoe=(ElementOfExpr)e;
 255                             if (negated) {
 256                                 GraphNode agn=(GraphNode)abstractremove.get(eoe.set);
 257                                 GraphNode.Edge edge=new GraphNode.Edge("requireselementremove",agn);
 258                                 gn.addEdge(edge);
 259                             } else {
 260                                 GraphNode agn=(GraphNode)abstractadd.get(eoe.set);
 261                                 GraphNode.Edge edge=new GraphNode.Edge("requireselementadd",agn);
 262                                 gn.addEdge(edge);
 263                             }
 264                         } else throw new Error("Unrecognized Abstract Update");
 265                     }
 266                 }
 267             }
 268             /* Cycle through the rules to look for possible conflicts */
 269             for(int i=0;i<state.vRules.size();i++) {
 270                 Rule r=(Rule) state.vRules.get(i);
 271                 if (Compiler.DEBUGGRAPH) {
 272                     System.out.println(gn.getLabel()+"--->"+((GraphNode)scopesatisfy.get(r)).getLabel());
 273                 }
 274                 if (concreteinterferes.interferes(mun,r,true)) {
 275                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 276                     GraphNode.Edge e=new GraphNode.Edge("satisfyscopeinterferes",scopenode);
 277                     gn.addEdge(e);
 278                 }
 279                 if (Compiler.DEBUGGRAPH) {
 280                     System.out.println(gn.getLabel()+"--->"+((GraphNode)scopefalsify.get(r)).getLabel());
 281                 }
 282                 if (concreteinterferes.interferes(mun,r,false)) {
 283                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 284                     GraphNode.Edge e=new GraphNode.Edge("falsifyscopeinterferes",scopenode);
 285                     gn.addEdge(e);
 286                 }
 287             }
 288         }
 289     }
 290
 291     void generateabstractedges() {
 292         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 293             GraphNode gn=(GraphNode)absiterator.next();
 294             TermNode tn=(TermNode)gn.getOwner();
 295             AbstractRepair ar=(AbstractRepair)tn.getAbstract();
 296
 297             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 298                 GraphNode gn2=(GraphNode)conjiterator.next();
 299                 TermNode tn2=(TermNode)gn2.getOwner();
 300                 Conjunction conj=tn2.getConjunction();
 301                 Constraint cons=tn2.getConstraint();
 302                 /* See if this is a relation wellformedness constraint
 303                    that is trivially satisfied. */
 304                 if (abstractinterferes.checkrelationconstraint(ar, cons))
 305                     continue;
 306                 if (AbstractInterferes.interferesquantifier(ar,cons)) {
 307                     GraphNode.Edge e=new GraphNode.Edge("interferesquantifier",gn2);
 308                     gn.addEdge(e);
 309                 } else {
 310                     for(int i=0;i<conj.size();i++) {
 311                         DNFPredicate dp=conj.get(i);
 312
 313                         if (!abstractinterferes.interfereswithpredicate(ar,dp))
 314                             continue;
 315                         if (getConstraint(gn)==null||
 316                             !abstractinterferes.interferemodifies(ar,getConstraint(gn),dp,cons)) {
 317                             GraphNode.Edge e=new GraphNode.Edge("interferesmodify",gn2);
 318                             gn.addEdge(e);
 319                             break;
 320                         }
 321                     }
 322                 }
 323             }
 324             for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 325                 GraphNode gn2=(GraphNode)scopeiterator.next();
 326                 TermNode tn2=(TermNode)gn2.getOwner();
 327                 ScopeNode sn2=tn2.getScope();
 328                 if (AbstractInterferes.interfereswithrule(ar,sn2.getRule(),sn2.getSatisfy())) {
 329                     GraphNode.Edge e=new GraphNode.Edge("interfereswithrule",gn2);
 330                     gn.addEdge(e);
 331                 }
 332             }
 333         }
 334     }
 335
 336     Constraint getConstraint(GraphNode gn) {
 337         for(Iterator it=gn.inedges();it.hasNext();) {
 338             GraphNode.Edge e=(GraphNode.Edge)it.next();
 339             GraphNode gnsource=e.getSource();
 340             TermNode tnsource=(TermNode)gnsource.getOwner();
 341             if (tnsource.getType()==TermNode.CONJUNCTION) {
 342                 return tnsource.getConstraint();
 343             }
 344         }
 345         return null;
 346     }
 347
 348     void generatescopenodes() {
 349         for(int i=0;i<state.vRules.size();i++) {
 350             Rule r=(Rule) state.vRules.get(i);
 351             ScopeNode satisfy=new ScopeNode(r,true);
 352             TermNode tnsatisfy=new TermNode(satisfy);
 353             GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy);
 354             gnsatisfy.setOption(scopeoption);
 355             if (Compiler.MERGENODES)
 356                 gnsatisfy.setMerge();
 357             ConsequenceNode cnsatisfy=new ConsequenceNode();
 358             TermNode ctnsatisfy=new TermNode(cnsatisfy);
 359             GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy);
 360             cgnsatisfy.setOption(conseqoption);
 361             consequence.put(satisfy,cgnsatisfy);
 362             GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy);
 363             gnsatisfy.addEdge(esat);
 364             consequencenodes.add(cgnsatisfy);
 365             scopesatisfy.put(r,gnsatisfy);
 366             scopenodes.add(gnsatisfy);
 367
 368             ScopeNode falsify=new ScopeNode(r,false);
 369             TermNode tnfalsify=new TermNode(falsify);
 370             GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify);
 371             gnfalsify.setOption(scopeoption);
 372             if (Compiler.MERGENODES)
 373                 gnfalsify.setMerge();
 374             ConsequenceNode cnfalsify=new ConsequenceNode();
 375             TermNode ctnfalsify=new TermNode(cnfalsify);
 376             GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify);
 377             cgnfalsify.setOption(conseqoption);
 378             consequence.put(falsify,cgnfalsify);
 379             GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify);
 380             gnfalsify.addEdge(efals);
 381             consequencenodes.add(cgnfalsify);
 382             scopefalsify.put(r,gnfalsify);
 383             scopenodes.add(gnfalsify);
 384         }
 385     }
 386
 387     void generatescopeedges() {
 388         for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) {
 389             GraphNode gn=(GraphNode)scopeiterator.next();
 390             TermNode tn=(TermNode)gn.getOwner();
 391             ScopeNode sn=tn.getScope();
 392
 393             /* Interference edges with conjunctions */
 394             for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 395                 GraphNode gn2=(GraphNode)conjiterator.next();
 396                 TermNode tn2=(TermNode)gn2.getOwner();
 397                 Conjunction conj=tn2.getConjunction();
 398                 Constraint constr=tn2.getConstraint();
 399                 for(int i=0;i<conj.size();i++) {
 400                     DNFPredicate dp=conj.get(i);
 401                     if (abstractinterferes.scopeinterfereswithpredicate(sn,dp)||
 402                         AbstractInterferes.interfereswithquantifier(sn.getDescriptor(),sn.getSatisfy(),constr)) {
 403                         GraphNode.Edge e=new GraphNode.Edge("interferesconjunction",gn2);
 404                         GraphNode gnconseq=(GraphNode)consequence.get(sn);
 405                         gnconseq.addEdge(e);
 406                         break;
 407                     }
 408                 }
 409             }
 410
 411             /* Now see if this could effect other model defintion rules */
 412             for(int i=0;i<state.vRules.size();i++) {
 413                 Rule r=(Rule) state.vRules.get(i);
 414                 if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,true)) {
 415                     GraphNode scopenode=(GraphNode)scopesatisfy.get(r);
 416                     GraphNode.Edge e=new GraphNode.Edge("interferesscopesatisfy2",scopenode);
 417                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 418                     gnconseq.addEdge(e);
 419                 }
 420                 if (AbstractInterferes.interfereswithrule(sn.getDescriptor(),sn.getSatisfy(),r,false)) {
 421                     GraphNode scopenode=(GraphNode)scopefalsify.get(r);
 422                     GraphNode.Edge e=new GraphNode.Edge("interferesscopefalsify2",scopenode);
 423                     GraphNode gnconseq=(GraphNode)consequence.get(sn);
 424                     gnconseq.addEdge(e);
 425                 }
 426             }
 427         }
 428     }
 429
 430     /** This method generates the abstract repair nodes. */
 431     void generaterepairnodes() {
 432         /* Generate repairs of conjunctions */
 433         for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) {
 434             GraphNode gn=(GraphNode)conjiterator.next();
 435             TermNode tn=(TermNode)gn.getOwner();
 436             Conjunction conj=tn.getConjunction();
 437         loop:
 438             for(int i=0;i<conj.size();i++) {
 439                 DNFPredicate dp=conj.get(i);
 440                 int[] array=dp.getPredicate().getRepairs(dp.isNegated(),this);
 441                 Descriptor d=dp.getPredicate().getDescriptor();
 442                 if ((dp.getPredicate() instanceof ExprPredicate)&&
 443                     (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
 444                     boolean neg=dp.isNegated();
 445                     Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
 446                     int size=((ExprPredicate)dp.getPredicate()).rightSize();
 447                     op=Opcode.translateOpcode(neg,op);
 448                     if (((size==1)&&(op==Opcode.EQ))||
 449                         ((size!=1)&&(op==Opcode.NE))||
 450                         ((size<=1)&&(op==Opcode.GE))||
 451                         ((size<1)&&(op==Opcode.GT))||
 452                         ((size>1)&&(op==Opcode.LT))||
 453                         ((size>=1)&&(op==Opcode.LE))) {
 454                         for(int i2=0;i2<conj.size();i2++) {
 455                             DNFPredicate dp2=conj.get(i2);
 456                             if ((dp2.getPredicate() instanceof ExprPredicate)&&
 457                                 (((ExprPredicate)dp2.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
 458                                 if (equivalent(((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr,
 459                                                (RelationExpr)((OpExpr)((ExprPredicate)dp2.getPredicate()).expr).left))
 460                                     continue loop; // comparison predicate ensure that size expr is true - no need to generate abstract repairs...
 461                             }
 462                         }
 463                     }
 464                 }
 465
 466                 for(int j=0;j<array.length;j++) {
 467                     AbstractRepair ar=new AbstractRepair(dp,array[j],d,sources);
 468                     TermNode tn2=new TermNode(ar);
 469                     //              GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
 470                     GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),dp.name()+" "+ar.type(),tn2);
 471                     gn2.setOption(absrepoption);
 472                     GraphNode.Edge e=new GraphNode.Edge("abstractedge1",gn2);
 473                     gn.addEdge(e);
 474                     if (!predtoabstractmap.containsKey(dp))
 475                         predtoabstractmap.put(dp,new HashSet());
 476                     ((Set)predtoabstractmap.get(dp)).add(gn2);
 477                     abstractrepair.add(gn2);
 478                 }
 479             }
 480         }
 481         /* Generate additional abstract repairs */
 482         Vector setdescriptors=state.stSets.getAllDescriptors();
 483         for(int i=0;i<setdescriptors.size();i++) {
 484             SetDescriptor sd=(SetDescriptor)setdescriptors.get(i);
 485
 486             VarExpr ve=new VarExpr("DUMMY");
 487             InclusionPredicate ip=new InclusionPredicate(ve,new SetExpr(sd));
 488             DNFPredicate tp=new DNFPredicate(false,ip);
 489             AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd,sources);
 490             TermNode tn=new TermNode(ar);
 491             GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn);
 492             gn.setOption(absrepoption);
 493             if (!predtoabstractmap.containsKey(tp))
 494                 predtoabstractmap.put(tp,new HashSet());
 495             ((Set)predtoabstractmap.get(tp)).add(gn);
 496             abstractrepair.add(gn);
 497             abstractrepairadd.add(gn);
 498             abstractadd.put(sd,gn);
 499
 500             DNFPredicate tp2=new DNFPredicate(true,ip);
 501             AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd,sources);
 502             TermNode tn2=new TermNode(ar2);
 503             GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2);
 504             gn2.setOption(absrepoption);
 505             if (!predtoabstractmap.containsKey(tp2))
 506                 predtoabstractmap.put(tp2,new HashSet());
 507             ((Set)predtoabstractmap.get(tp2)).add(gn2);
 508             abstractrepair.add(gn2);
 509             abstractrepairadd.add(gn2);
 510             abstractremove.put(sd,gn2);
 511         }
 512
 513         Vector relationdescriptors=state.stRelations.getAllDescriptors();
 514         for(int i=0;i<relationdescriptors.size();i++) {
 515             RelationDescriptor rd=(RelationDescriptor)relationdescriptors.get(i);
 516             VarDescriptor vd1=new VarDescriptor("DUMMY1");
 517             VarExpr ve2=new VarExpr("DUMMY2");
 518
 519             InclusionPredicate ip=new InclusionPredicate(ve2,new ImageSetExpr(vd1, rd));
 520
 521             DNFPredicate tp=new DNFPredicate(false,ip);
 522             AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd,sources);
 523             TermNode tn=new TermNode(ar);
 524             GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn);
 525             gn.setOption(absrepoption);
 526             if (!predtoabstractmap.containsKey(tp))
 527                 predtoabstractmap.put(tp,new HashSet());
 528             ((Set)predtoabstractmap.get(tp)).add(gn);
 529             abstractrepair.add(gn);
 530             abstractrepairadd.add(gn);
 531             abstractadd.put(rd,gn);
 532
 533             DNFPredicate tp2=new DNFPredicate(true,ip);
 534             AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd,sources);
 535             TermNode tn2=new TermNode(ar2);
 536             GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2);
 537             gn2.setOption(absrepoption);
 538             if (!predtoabstractmap.containsKey(tp2))
 539                 predtoabstractmap.put(tp2,new HashSet());
 540             ((Set)predtoabstractmap.get(tp2)).add(gn2);
 541             abstractrepair.add(gn2);
 542             abstractrepairadd.add(gn2);
 543             abstractremove.put(rd,gn2);
 544         }
 545     }
 546
 547     int compensationcount=0;
 548     void generatecompensationnodes() {
 549         for(int i=0;i<state.vRules.size();i++) {
 550             Rule r=(Rule) state.vRules.get(i);
 551             Vector possiblerules=new Vector();
 552
 553             for(int j=0;j<(r.numQuantifiers()+r.getDNFNegGuardExpr().size());j++) {
 554                 GraphNode gn=(GraphNode)scopesatisfy.get(r);
 555                 TermNode tn=(TermNode) gn.getOwner();
 556                 ScopeNode sn=tn.getScope();
 557                 MultUpdateNode mun=new MultUpdateNode(sn);
 558                 TermNode tn2=new TermNode(mun);
 559                 GraphNode gn2=new GraphNode("CompRem"+compensationcount,tn2);
 560                 gn2.setOption(compoption);
 561                 UpdateNode un=new UpdateNode(r);
 562
 563                 if (j<r.numQuantifiers()) {
 564                     /* Remove quantifier */
 565                     Quantifier q=r.getQuantifier(j);
 566                     if (q instanceof RelationQuantifier) {
 567                         RelationQuantifier rq=(RelationQuantifier)q;
 568                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 569                         toe.td=ReservedTypeDescriptor.INT;
 570                         Updates u=new Updates(toe,true);
 571                         un.addUpdate(u);
 572                         if (abstractremove.containsKey(rq.relation)) {
 573                             GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
 574                             GraphNode.Edge e=new GraphNode.Edge("requiresremove1",agn);
 575                             gn2.addEdge(e);
 576                         } else {
 577                             continue; /* Abstract repair doesn't exist */
 578                         }
 579                     } else if (q instanceof SetQuantifier) {
 580                         SetQuantifier sq=(SetQuantifier)q;
 581                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 582                         eoe.td=ReservedTypeDescriptor.INT;
 583                         Updates u=new Updates(eoe,true);
 584                         un.addUpdate(u);
 585                         if (abstractremove.containsKey(sq.set)) {
 586                             GraphNode agn=(GraphNode)abstractremove.get(sq.set);
 587                             GraphNode.Edge e=new GraphNode.Edge("requiresremove2",agn);
 588                             gn2.addEdge(e);
 589                         } else {
 590                             continue; /* Abstract repair doesn't exist */
 591                         }
 592                     } else {
 593                         continue;
 594                     }
 595                 } else {
 596                     /* Negate conjunction */
 597                     int c=j-r.numQuantifiers();
 598                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c),null)) {
 599                         continue;
 600                     }
 601                 }
 602                 if (!un.checkupdates()) /* Make sure we have a good update */
 603                     continue;
 604
 605                 mun.addUpdate(un);
 606                 GraphNode.Edge e=new GraphNode.Edge("abstractcomp"+compensationcount,gn2);
 607                 compensationcount++;
 608                 gn.addEdge(e);
 609                 updatenodes.add(gn2);
 610             }
 611         }
 612     }
 613
 614     void generatedatastructureupdatenodes() {
 615         for(Iterator absiterator=abstractrepair.iterator();absiterator.hasNext();) {
 616             GraphNode gn=(GraphNode)absiterator.next();
 617             System.out.println("Analysing: "+gn.getTextLabel());
 618             TermNode tn=(TermNode) gn.getOwner();
 619             AbstractRepair ar=tn.getAbstract();
 620             if (ar.getType()==AbstractRepair.ADDTOSET) {
 621                 generateaddtosetrelation(gn,ar);
 622             } else if (ar.getType()==AbstractRepair.REMOVEFROMSET) {
 623                 generateremovefromsetrelation(gn,ar);
 624             } else if (ar.getType()==AbstractRepair.ADDTORELATION) {
 625                 generateaddtosetrelation(gn,ar);
 626             } else if (ar.getType()==AbstractRepair.REMOVEFROMRELATION) {
 627                 generateremovefromsetrelation(gn,ar);
 628             } else if (ar.getType()==AbstractRepair.MODIFYRELATION) {
 629                 /* Generate remove/add pairs */
 630                 if (ar.needsRemoves(state))
 631                     generateremovefromsetrelation(gn,ar);
 632                 generateaddtosetrelation(gn,ar);
 633                 /* Generate atomic modify */
 634                 generatemodifyrelation(gn,ar);
 635             }
 636         }
 637     }
 638
 639
 640     /** This method generates concrete data structure updates which
 641      * remove an object (or tuple) from a set (or relation).*/
 642
 643     int removefromcount=0;
 644     void generateremovefromsetrelation(GraphNode gn,AbstractRepair ar) {
 645         /* Construct the set of all rules which could add something to the given set or relation */
 646
 647         Vector possiblerules=new Vector();
 648         for(int i=0;i<state.vRules.size();i++) {
 649             Rule r=(Rule) state.vRules.get(i);
 650             if ((r.getInclusion() instanceof SetInclusion)&&
 651                 (ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet()))
 652                 possiblerules.add(r);
 653             if ((r.getInclusion() instanceof RelationInclusion)&&
 654                 (ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation()))
 655                 possiblerules.add(r);
 656         }
 657         if (possiblerules.size()==0)
 658             return;
 659
 660         /* Loop through different ways of falsifying each of these rules */
 661         int[] count=new int[possiblerules.size()];
 662         while(remains(count,possiblerules,true)) {
 663             MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.REMOVE);
 664             TermNode tn=new TermNode(mun);
 665             GraphNode gn2=new GraphNode("UpdateRem"+removefromcount,tn);
 666             gn2.setOption(updateoption);
 667
 668             boolean goodflag=true;
 669             for(int i=0;i<possiblerules.size();i++) {
 670                 Rule r=(Rule)possiblerules.get(i);
 671                 UpdateNode un=new UpdateNode(r);
 672
 673                 if (count[i]<r.numQuantifiers()) {
 674                     /* Remove quantifier */
 675                     Quantifier q=r.getQuantifier(count[i]);
 676                     if (q instanceof RelationQuantifier) {
 677                         RelationQuantifier rq=(RelationQuantifier)q;
 678                         TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
 679                         toe.td=ReservedTypeDescriptor.INT;
 680                         Updates u=new Updates(toe,true);
 681                         un.addUpdate(u);
 682                         if (abstractremove.containsKey(rq.relation)) {
 683                             GraphNode agn=(GraphNode)abstractremove.get(rq.relation);
 684                             GraphNode.Edge e=new GraphNode.Edge("requiresremove3",agn);
 685                             gn2.addEdge(e);
 686                         } else {
 687                             goodflag=false;break; /* Abstract repair doesn't exist */
 688                         }
 689                     } else if (q instanceof SetQuantifier) {
 690                         SetQuantifier sq=(SetQuantifier)q;
 691                         ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
 692                         eoe.td=ReservedTypeDescriptor.INT;
 693                         Updates u=new Updates(eoe,true);
 694                         un.addUpdate(u);
 695                         if (abstractremove.containsKey(sq.set)) {
 696                             GraphNode agn=(GraphNode)abstractremove.get(sq.set);
 697                             GraphNode.Edge e=new GraphNode.Edge("requiresremove4",agn);
 698                             gn2.addEdge(e);
 699                         } else {
 700                             goodflag=false;break; /* Abstract repair doesn't exist */
 701                         }
 702                     } else {goodflag=false;break;}
 703                 } else {
 704                     int c=count[i]-r.numQuantifiers();
 705                     if (!processconjunction(un,r.getDNFNegGuardExpr().get(c),null)) {
 706                         goodflag=false;break;
 707                     }
 708                 }
 709                 if (!un.checkupdates()) {
 710                     goodflag=false;
 711                     break;
 712                 }
 713                 mun.addUpdate(un);
 714             }
 715             if (goodflag) {
 716                 GraphNode.Edge e=new GraphNode.Edge("abstract3"+(removefromcount++),gn2);
 717                 gn.addEdge(e);
 718                 updatenodes.add(gn2);
 719             }
 720             increment(count,possiblerules,true);
 721         }
 722     }
 723
 724     /** This method increments to the next possibility. */
 725
 726     static private void increment(int count[], Vector rules,boolean isremove) {
 727         count[0]++;
 728         for(int i=0;i<(rules.size()-1);i++) {
 729             int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
 730             if (count[i]>=num) {
 731                 count[i+1]++;
 732                 count[i]=0;
 733             } else break;
 734         }
 735     }
 736
 737
 738     /** This method test if there remain any possibilities to loop
 739      * through. */
 740     static private boolean remains(int count[], Vector rules, boolean isremove) {
 741         for(int i=0;i<rules.size();i++) {
 742             int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size();
 743             if (count[i]>=num) {
 744                 return false;
 745             }
 746         }
 747         return true;
 748     }
 749
 750     /** This method generates data structure updates to implement the
 751      *  abstract atomic modification specified by ar. */
 752
 753     int modifycount=0;
 754     void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {
 755         RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor();
 756         ExprPredicate exprPredicate=(ExprPredicate)ar.getPredicate().getPredicate();
 757         boolean inverted=exprPredicate.inverted();
 758         int leftindex=0;
 759         int rightindex=1;
 760         if (inverted)
 761             leftindex=2;
 762         else
 763             rightindex=2;
 764
 765         // construct set of possible rules
 766         Vector possiblerules=new Vector();
 767         for(int i=0;i<state.vRules.size();i++) {
 768             Rule r=(Rule) state.vRules.get(i);
 769             if ((r.getInclusion() instanceof RelationInclusion)&&
 770                 (rd==((RelationInclusion)r.getInclusion()).getRelation()))
 771                 possiblerules.add(r);
 772         }
 773         if (possiblerules.size()==0)
 774             return;
 775
 776         // increment through this set
 777         int[] count=new int[possiblerules.size()];
 778         while(remains(count,possiblerules,false)) {
 779             MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.MODIFY);
 780             TermNode tn=new TermNode(mun);
 781             GraphNode gn2=new GraphNode("UpdateMod"+modifycount,tn);
 782             gn2.setOption(updateoption);
 783
 784             boolean goodflag=true;
 785             for(int i=0;i<possiblerules.size();i++) {
 786                 Rule r=(Rule)possiblerules.get(i);
 787                 UpdateNode un=new UpdateNode(r);
 788
 789                 int c=count[i];
 790                 if (!processconjunction(un,r.getDNFGuardExpr().get(c),null)) {
 791                     goodflag=false;break;
 792                 }
 793                 RelationInclusion ri=(RelationInclusion)r.getInclusion();
 794                 if (!(ri.getLeftExpr() instanceof VarExpr)) {
 795                     if (ri.getLeftExpr().isValue(ri.getRelation().getDomain().getType())) {
 796                         Updates up=new Updates(ri.getLeftExpr(),leftindex,ri.getRelation().getDomain().getType());
 797                         un.addUpdate(up);
 798                     } else {
 799                         if (inverted)
 800                             goodflag=false;
 801                         else un.addInvariant(ri.getLeftExpr());
 802                     }
 803                 } else {
 804                     VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar();
 805                     if (vd.isGlobal()) {
 806                         Updates up=new Updates(ri.getLeftExpr(),leftindex,null);
 807                         un.addUpdate(up);
 808                     } else if (inverted)
 809                         goodflag=false;
 810                 }
 811                 if (!(ri.getRightExpr() instanceof VarExpr)) {
 812                     if (ri.getRightExpr().isValue(ri.getRelation().getRange().getType())) {
 813                         Updates up=new Updates(ri.getRightExpr(),rightindex,ri.getRelation().getRange().getType());
 814                         un.addUpdate(up);
 815                     } else {
 816                         if (!inverted)
 817                             goodflag=false;
 818                         else
 819                             un.addInvariant(ri.getLeftExpr());
 820                     }
 821                 } else {
 822                     VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar();
 823                     if (vd.isGlobal()) {
 824                         Updates up=new Updates(ri.getRightExpr(),rightindex,null);
 825                         un.addUpdate(up);
 826                     } else if (!inverted)
 827                         goodflag=false;
 828                 }
 829
 830                 if (!un.checkupdates()) {
 831                     goodflag=false;
 832                     break;
 833                 }
 834                 mun.addUpdate(un);
 835             }
 836             if (goodflag) {
 837                 GraphNode.Edge e=new GraphNode.Edge("abstract4"+modifycount,gn2);
 838                 modifycount++;
 839                 gn.addEdge(e);
 840                 updatenodes.add(gn2);
 841             }
 842             increment(count,possiblerules,false);
 843         }
 844     }
 845
 846     /** Generate concrete data structure update to add an object(or
 847      * tuple) to a set (or relation). */
 848
 849     static int addtocount=0;
 850     void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
 851         for(int i=0;i<state.vRules.size();i++) {
 852             Rule r=(Rule) state.vRules.get(i);
 853
 854
 855             /* See if this is a good rule*/
 856             if ((r.getInclusion() instanceof SetInclusion&&
 857                  ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
 858                 (r.getInclusion() instanceof RelationInclusion&&
 859                  ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
 860
 861                 /* First solve for quantifiers */
 862                 Vector bindings=new Vector();
 863                 /* Construct bindings */
 864
 865                 Hashtable setmapping=new Hashtable();
 866                 System.out.println("Attempting to construct bindings");
 867
 868                 if (!constructbindings(bindings,r,ar,setmapping,false))
 869                     continue;
 870                 System.out.println("Bindings constructed");
 871                 //Generate add instruction
 872                 DNFRule dnfrule=r.getDNFGuardExpr();
 873                  endloop:
 874                 for(int j=0;j<dnfrule.size();j++) {
 875                     Inclusion inc=r.getInclusion();
 876                     UpdateNode un=new UpdateNode(r);
 877                     un.addBindings(bindings);
 878                     /* Now build update for tuple/set inclusion condition */
 879                     if(inc instanceof SetInclusion) {
 880                         SetInclusion si=(SetInclusion)inc;
 881                         Expr e=si.elementexpr;
 882
 883                         while(e instanceof CastExpr) {
 884                             CastExpr ce=(CastExpr)e;
 885                             if (ce.getType()!=si.getSet().getType())
 886                                 continue endloop;
 887                             e=ce.getExpr();
 888                         }
 889
 890                         if (!(e instanceof VarExpr)) {
 891                             if (e.isValue(si.getSet().getType())) {
 892                                 Updates up=new Updates(e,0,si.getSet().getType());
 893                                 un.addUpdate(up);
 894                             } else {
 895                                 /* We're an add to set*/
 896                                 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,e);
 897                                 SetDescriptor set=sources.setSource(si.getSet())?
 898                                     sources.getSourceSet(si.getSet()):null;
 899                                 if (set==null)
 900                                     continue;
 901                                 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
 902                                 if (rap==ArrayAnalysis.AccessPath.NONE)
 903                                     continue;
 904                                 if (!rap.equal(ap))
 905                                     continue;
 906                                 if (!constructarrayupdate(un, e, rap, 0))
 907                                     continue;
 908                             }
 909                         } else {
 910                             VarDescriptor vd=((VarExpr)e).getVar();
 911                             if (vd.isGlobal()) {
 912                                 Updates up=new Updates(e,0,null);
 913                                 un.addUpdate(up);
 914                             }
 915                         }
 916                     } else if (inc instanceof RelationInclusion) {
 917                         RelationInclusion ri=(RelationInclusion)inc;
 918
 919                         Expr e=ri.getLeftExpr();
 920
 921                         while(e instanceof CastExpr) {
 922                             CastExpr ce=(CastExpr)e;
 923                             if (ce.getType()!=ri.getRelation().getDomain().getType())
 924                                 continue endloop;
 925                             e=ce.getExpr();
 926                         }
 927                         if (!(e instanceof VarExpr)) {
 928                             if (e.isValue(ri.getRelation().getDomain().getType())) {
 929                                 Updates up=new Updates(e,0,ri.getRelation().getDomain().getType());
 930                                 if (ar.getDomainSet()!=null)
 931                                     setmapping.put(e,ar.getDomainSet());
 932                                 un.addUpdate(up);
 933                             } else {
 934                                 /* We don't handly relation modifies */
 935                                 if (ar.getType()==AbstractRepair.MODIFYRELATION)
 936                                     continue;
 937                                 /* We're an add to relation*/
 938                                 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,e);
 939                                 SetDescriptor set=sources.relsetSource(ri.getRelation(),true /* Domain*/)?
 940                                     sources.relgetSourceSet(ri.getRelation(),true):null;
 941                                 if (set==null)
 942                                     continue;
 943                                 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
 944                                 if (rap==ArrayAnalysis.AccessPath.NONE||
 945                                     !rap.equal(ap)||
 946                                     !constructarrayupdate(un, e, rap, 0))
 947                                     continue;
 948                                 if (ar.getDomainSet()!=null)
 949                                     setmapping.put(e,ar.getDomainSet());
 950
 951                             }
 952                         } else {
 953                             VarDescriptor vd=((VarExpr)e).getVar();
 954                             if (vd.isGlobal()) {
 955                                 Updates up=new Updates(e,0,null);
 956                                 if (ar.getDomainSet()!=null)
 957                                     setmapping.put(e,ar.getDomainSet());
 958                                 un.addUpdate(up);
 959                             }
 960                         }
 961
 962                         e=ri.getRightExpr();
 963
 964                         while(e instanceof CastExpr) {
 965                             CastExpr ce=(CastExpr)e;
 966                             if (ce.getType()!=ri.getRelation().getRange().getType())
 967                                 continue endloop;
 968                             e=ce.getExpr();
 969                         }
 970                         if (!(e instanceof VarExpr)) {
 971                             if (e.isValue(ri.getRelation().getRange().getType())) {
 972                                 Updates up=new Updates(e,1,ri.getRelation().getRange().getType());
 973                                 un.addUpdate(up);
 974                             } else {
 975                                 /* We don't handly relation modifies */
 976                                 if (ar.getType()==AbstractRepair.MODIFYRELATION)
 977                                     continue;
 978                                 /* We're an add to relation*/
 979                                 ArrayAnalysis.AccessPath rap=arrayanalysis.analyzeExpr(r,e);
 980                                 SetDescriptor set=sources.relsetSource(ri.getRelation(),false /* Range*/)?
 981                                     sources.relgetSourceSet(ri.getRelation(),false):null;
 982                                 if (set==null)
 983                                     continue;
 984                                 ArrayAnalysis.AccessPath ap=arrayanalysis.getSet(set);
 985
 986                                 if (rap==ArrayAnalysis.AccessPath.NONE||
 987                                     !rap.equal(ap)||
 988                                     !constructarrayupdate(un, e, rap, 1))
 989                                     continue;
 990                                 if (ar.getRangeSet()!=null)
 991                                     setmapping.put(e,ar.getRangeSet());
 992                             }
 993                         } else {
 994                             VarDescriptor vd=((VarExpr)e).getVar();
 995                             if (vd.isGlobal()) {
 996                                 Updates up=new Updates(e,1,null);
 997                                 if (ar.getRangeSet()!=null)
 998                                     setmapping.put(e,ar.getRangeSet());
 999                                 un.addUpdate(up);
1000                             }
1001                         }
1002                     }
1003                     System.out.println("Built inclusion condition updates.");
1004                     //Finally build necessary updates to satisfy conjunction
1005                     RuleConjunction ruleconj=dnfrule.get(j);
1006
1007                     /* Add in updates for quantifiers */
1008                     MultUpdateNode mun=new MultUpdateNode(ar,MultUpdateNode.ADD);
1009                     TermNode tn=new TermNode(mun);
1010                     GraphNode gn2=new GraphNode("UpdateAdd"+addtocount,tn);
1011                     gn2.setOption(updateoption);
1012
1013                     if (debugmsg("Start processing quantifiers")&&
1014                         processquantifiers(gn2,un, r,setmapping)&&
1015                         debugmsg("Finished processing quantifiers")&&
1016                         processconjunction(un,ruleconj,setmapping)&&
1017                         debugmsg("Finished processing conjunction")&&
1018                         un.checkupdates()&&
1019                         debugmsg("Updates checked")) {
1020                         mun.addUpdate(un);
1021                         GraphNode.Edge e=new GraphNode.Edge("abstract5"+addtocount,gn2);
1022                         addtocount++;
1023                         gn.addEdge(e);
1024                         updatenodes.add(gn2);
1025                     }
1026                 }
1027             }
1028         }
1029     }
1030
1031     boolean debugmsg(String st) {
1032         System.out.println(st);
1033         return true;
1034     }
1035
1036     boolean constructarrayupdate(UpdateNode un, Expr lexpr, ArrayAnalysis.AccessPath ap, int slotnumber) {
1037         System.out.println("Constructing array update");
1038         Expr e=null;
1039         for (int i=ap.numFields()-1;i>=0;i--) {
1040             if (e==null)
1041                 e=lexpr;
1042             else
1043                 e=((DotExpr)e).getExpr();
1044
1045             while (e instanceof CastExpr)
1046                 e=((CastExpr)e).getExpr();
1047
1048             DotExpr de=(DotExpr)e;
1049             FieldDescriptor fd=ap.getField(i);
1050             if (fd instanceof ArrayDescriptor) {
1051                 // We have an ArrayDescriptor!
1052                 Expr index=de.getIndex();
1053                 if (!index.isValue(null)) {/* Not assignable */
1054                     System.out.println("ERROR:Index isn't assignable");
1055                     return false;
1056                 }
1057                 Updates updates=new Updates(index,i,ap,lexpr,slotnumber);
1058                 un.addUpdate(updates);
1059             }
1060         }
1061         return true;
1062     }
1063
1064     /** This method constructs bindings for an update using rule
1065      * r. The boolean flag isremoval indicates that the update
1066      * performs a removal.  The function returns true if it is able to
1067      * generate a valid set of bindings and false otherwise. */
1068
1069     boolean constructbindings(Vector bindings, Rule r, AbstractRepair ar, Hashtable setmapping, boolean isremoval) {
1070         boolean goodupdate=true;
1071         Inclusion inc=r.getInclusion();
1072
1073         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
1074             Quantifier q=(Quantifier)iterator.next();
1075             if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) {
1076                 VarDescriptor vd=null;
1077                 SetDescriptor set=null;
1078                 if (q instanceof SetQuantifier) {
1079                     vd=((SetQuantifier)q).getVar();
1080                     set=((SetQuantifier)q).getSet();
1081                 } else {
1082                     vd=((ForQuantifier)q).getVar();
1083                 }
1084                 if(inc instanceof SetInclusion) {
1085                     SetInclusion si=(SetInclusion)inc;
1086                     Expr tmpe=si.elementexpr;
1087                     Expr e=si.elementexpr;
1088
1089                     while(e instanceof CastExpr) {
1090                         CastExpr ce=(CastExpr)e;
1091                         if (ce.getType()!=si.getSet().getType())
1092                             return false;
1093                         e=ce.getExpr();
1094                     }
1095
1096                     if ((e instanceof VarExpr)&&
1097                         (((VarExpr)e).getVar()==vd)) {
1098                         /* Can solve for v */
1099                         if (set==null||!si.getSet().getType().isSubtypeOf(set.getType()))
1100                             return false;
1101                         Binding binding=new Binding(vd,0);
1102                         bindings.add(binding);
1103                     } else {
1104                         goodupdate=false;
1105                     }
1106                 } else if (inc instanceof RelationInclusion) {
1107                     RelationInclusion ri=(RelationInclusion)inc;
1108                     boolean f1=true;
1109                     boolean f2=true;
1110
1111                     Expr e=ri.getLeftExpr();
1112
1113                     while(e instanceof CastExpr) {
1114                         CastExpr ce=(CastExpr)e;
1115                         if (ce.getType()!=ri.getRelation().getDomain().getType())
1116                             return false;
1117                         e=ce.getExpr();
1118                     }
1119
1120                     if ((e instanceof VarExpr)&&
1121                         (((VarExpr)e).getVar()==vd)) {
1122                                 /* Can solve for v */
1123                         Binding binding=new Binding(vd,0);
1124                         if (!ri.getRelation().getDomain().getType().isSubtypeOf(set.getType()))
1125                             return false;
1126                         if (ar.getDomainSet()!=null)
1127                             setmapping.put(ri.getLeftExpr(),ar.getDomainSet());
1128                         bindings.add(binding);
1129                     } else f1=false;
1130
1131
1132                     e=ri.getRightExpr();
1133
1134                     while(e instanceof CastExpr) {
1135                         CastExpr ce=(CastExpr)e;
1136                         if (ce.getType()!=ri.getRelation().getRange().getType())
1137                             return false;
1138                         e=ce.getExpr();
1139                     }
1140
1141                     if ((e instanceof VarExpr)&&
1142                         (((VarExpr)e).getVar()==vd)) {
1143                                 /* Can solve for v */
1144                         Binding binding=new Binding(vd,1);
1145                         if (!ri.getRelation().getRange().getType().isSubtypeOf(set.getType()))
1146                             return false;
1147                         if (ar.getRangeSet()!=null)
1148                             setmapping.put(ri.getRightExpr(),ar.getRangeSet());
1149                         bindings.add(binding);
1150                     } else f2=false;
1151                     if (!(f1||f2))
1152                         goodupdate=false;
1153                 } else throw new Error("Inclusion not recognized");
1154                 if (!goodupdate)
1155                     if (isremoval) {
1156                         /* Removals don't need bindings anymore
1157                            Binding binding=new Binding(vd);
1158                            bindings.add(binding);*/
1159                         goodupdate=true;
1160                     } else if (q instanceof SetQuantifier) {
1161                         /* Create new element to bind to */
1162                         // search if the set 'set' has a size
1163                         Binding binding=new Binding(vd,set,exactsize.getsize(set)==1);
1164                         bindings.add(binding);
1165                         goodupdate=true;
1166
1167                     } else
1168                         goodupdate=false;
1169             } else if (q instanceof RelationQuantifier) {
1170                 RelationQuantifier rq=(RelationQuantifier)q;
1171                 for(int k=0;k<2;k++) {
1172                     VarDescriptor vd=(k==0)?rq.x:rq.y;
1173                     TypeDescriptor td=(k==0)?rq.getRelation().getDomain().getType():rq.getRelation().getRange().getType();
1174                     if(inc instanceof SetInclusion) {
1175                         SetInclusion si=(SetInclusion)inc;
1176
1177                         Expr e=si.elementexpr;
1178
1179                         while(e instanceof CastExpr) {
1180                             CastExpr ce=(CastExpr)e;
1181                             if (ce.getType()!=td)
1182                                 return false;
1183                             e=ce.getExpr();
1184                         }
1185
1186                         if ((e instanceof VarExpr)&&
1187                             (((VarExpr)e).getVar()==vd)) {
1188                             /* Can solve for v */
1189                             Binding binding=new Binding(vd,0);
1190
1191                             if (!si.getSet().getType().isSubtypeOf(td))
1192                                 return false;
1193                             bindings.add(binding);
1194                         } else
1195                             goodupdate=false;
1196                     } else if (inc instanceof RelationInclusion) {
1197                         RelationInclusion ri=(RelationInclusion)inc;
1198                         boolean f1=true;
1199                         boolean f2=true;
1200
1201
1202                         Expr e=ri.getLeftExpr();
1203
1204                         while(e instanceof CastExpr) {
1205                             CastExpr ce=(CastExpr)e;
1206                             if (ce.getType()!=ri.getRelation().getDomain().getType())
1207                                 return false;
1208                             e=ce.getExpr();
1209                         }
1210                         if ((ri.getLeftExpr() instanceof VarExpr)&&
1211                             (((VarExpr)ri.getLeftExpr()).getVar()==vd)) {
1212                             /* Can solve for v */
1213                             Binding binding=new Binding(vd,0);
1214                             if (!ri.getRelation().getDomain().getType().isSubtypeOf(td))
1215                                 return false;
1216                             if (ar.getDomainSet()!=null)
1217                                 setmapping.put(ri.getLeftExpr(),ar.getDomainSet());
1218                             bindings.add(binding);
1219                         } else f1=false;
1220
1221
1222                         e=ri.getRightExpr();
1223
1224                         while(e instanceof CastExpr) {
1225                             CastExpr ce=(CastExpr)e;
1226                             if (ce.getType()!=ri.getRelation().getRange().getType())
1227                                 return false;
1228                             e=ce.getExpr();
1229                         }
1230                         if ((ri.getRightExpr() instanceof VarExpr)&&
1231                             (((VarExpr)ri.getRightExpr()).getVar()==vd)) {
1232                             /* Can solve for v */
1233                             Binding binding=new Binding(vd,1);
1234                             if (!ri.getRelation().getRange().getType().isSubtypeOf(td))
1235                                 return false;
1236                             if (ar.getRangeSet()!=null)
1237                                 setmapping.put(ri.getRightExpr(),ar.getRangeSet());
1238                             bindings.add(binding);
1239                         } else f2=false;
1240                         if (!(f1||f2))
1241                             goodupdate=false;
1242                     } else throw new Error("Inclusion not recognized");
1243                     if (!goodupdate)
1244                         if (isremoval) {
1245                             /* Removals don't need bindings anymore
1246                                Binding binding=new Binding(vd);
1247                                bindings.add(binding);*/
1248                             goodupdate=true;
1249                         } else
1250                             break;
1251                 }
1252                 if (!goodupdate)
1253                     break;
1254             } else throw new Error("Quantifier not recognized");
1255         }
1256         return goodupdate;
1257     }
1258
1259     /** Adds updates that add an item to the appropriate set or
1260      * relation quantified over by the model definition rule.. */
1261
1262     boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r,Hashtable setmapping) {
1263         Inclusion inc=r.getInclusion();
1264         for(Iterator iterator=r.quantifiers();iterator.hasNext();) {
1265             Quantifier q=(Quantifier)iterator.next();
1266             /* Add quantifier */
1267             if (q instanceof RelationQuantifier) {
1268                 RelationQuantifier rq=(RelationQuantifier)q;
1269                 TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation);
1270                 toe.td=ReservedTypeDescriptor.INT;
1271                 Updates u=new Updates(toe,false);
1272                 un.addUpdate(u);
1273                 if (abstractadd.containsKey(rq.relation)) {
1274                     GraphNode agn=(GraphNode)abstractadd.get(rq.relation);
1275                     GraphNode.Edge e=new GraphNode.Edge("requiresadd5",agn);
1276                     gn.addEdge(e);
1277                 } else {
1278                     return false;
1279                 }
1280             } else if (q instanceof SetQuantifier) {
1281                 SetQuantifier sq=(SetQuantifier)q;
1282                 if (un.getBinding(sq.var).getType()==Binding.SEARCH) {
1283                     Binding b=un.getBinding(sq.var);
1284                     Constraint reqc=exactsize.getConstraint(b.getSet());
1285                     constraintdependence.requiresConstraint(gn,reqc);
1286                     continue; /* Don't need to ensure addition for search */
1287                 }
1288                 VarExpr ve=new VarExpr(sq.var);
1289                 SetDescriptor sd=findExpr(setmapping, ve);
1290                 if (sd!=null&&sd.isSubset(sq.set))
1291                     continue; /* this update is trivially true */
1292
1293                 ElementOfExpr eoe=new ElementOfExpr(ve,sq.set);
1294                 eoe.td=ReservedTypeDescriptor.INT;
1295                 Updates u=new Updates(eoe,false);
1296                 un.addUpdate(u);
1297                 if (abstractadd.containsKey(sq.set)) {
1298                     GraphNode agn=(GraphNode)abstractadd.get(sq.set);
1299                     GraphNode.Edge e=new GraphNode.Edge("requiresadd6",agn);
1300                     gn.addEdge(e);
1301                 } else {
1302                     return false;
1303                 }
1304             } else return false;
1305         }
1306         return true;
1307     }
1308
1309     static SetDescriptor findExpr(Hashtable setmapping, Expr e) {
1310         if (setmapping==null)
1311             return null;
1312         Set kset=setmapping.keySet();
1313         for(Iterator it=kset.iterator();it.hasNext();) {
1314             Expr expr=(Expr)it.next();
1315             if (expr.equals(null,e)) {
1316                 return (SetDescriptor)setmapping.get(expr);
1317             }
1318         }
1319         return null;
1320     }
1321
1322     /** This method generates the necessary updates to satisfy the
1323      * conjunction ruleconj. */
1324
1325     boolean  processconjunction(UpdateNode un,RuleConjunction ruleconj,Hashtable setmapping) {
1326         boolean okay=true;
1327         for(int k=0;k<ruleconj.size();k++) {
1328             DNFExpr de=ruleconj.get(k);
1329             Expr e=de.getExpr();
1330             if (e instanceof OpExpr) {
1331                 OpExpr ex=(OpExpr)de.getExpr();
1332                 Opcode op=ex.getOpcode();
1333                 Updates up=new Updates(ex.left,ex.right,op, de.getNegation());
1334                 un.addUpdate(up);
1335             } else if (e instanceof ElementOfExpr) {
1336                 SetDescriptor sd=findExpr(setmapping, ((ElementOfExpr)e).element);
1337                 if (sd!=null&&sd.isSubset(((ElementOfExpr)e).set))
1338                     continue; /* this update is trivially true */
1339                 Updates up=new Updates(e,de.getNegation());
1340                 un.addUpdate(up);
1341             } else if (e instanceof TupleOfExpr) {
1342                 Updates up=new Updates(e,de.getNegation());
1343                 un.addUpdate(up);
1344             } else if (e instanceof BooleanLiteralExpr) {
1345                 boolean truth=((BooleanLiteralExpr)e).getValue();
1346                 if (de.getNegation())
1347                     truth=!truth;
1348                 if (!truth) {
1349                     okay=false;
1350                     break;
1351                 }
1352             } else {
1353                 System.out.println(e.getClass().getName());
1354                 throw new Error("Unrecognized Expr");
1355             }
1356         }
1357         return okay;
1358     }
1359
1360     /** This method sees if when the quantifiers listed in set are
1361      *  fixed, whether there can be more than one unique binding for
1362      *  the constraint or model definition rule qs.*/
1363     public boolean analyzeQuantifiers(Quantifiers qs,Set set) {
1364         for(int i=0;i<qs.numQuantifiers();i++) {
1365             Quantifier q=qs.getQuantifier(i);
1366             if (set.contains(q))
1367                 continue;
1368             if (q instanceof SetQuantifier) {
1369                 SetDescriptor sd=((SetQuantifier)q).getSet();
1370                 if (maxsize.getsize(sd)<=1&&
1371                     maxsize.getsize(sd)>=0)
1372                     continue;
1373             } else if (q instanceof RelationQuantifier) {
1374                 RelationDescriptor rd=((RelationQuantifier)q).getRelation();
1375                 if (maxsize.getsize(rd)<=1&&
1376                     maxsize.getsize(rd)>=0)
1377                     continue;
1378             }
1379             return false;
1380         }
1381         return true;
1382     }
1383
1384     public boolean mutuallyexclusive(SetDescriptor sd1, SetDescriptor sd2) {
1385         if (mutualexclusive(sd1,sd2)||
1386             mutualexclusive(sd2,sd1))
1387             return true;
1388         else
1389             return false;
1390     }
1391
1392     private boolean mutualexclusive(SetDescriptor sd1, SetDescriptor sd2) {
1393         Vector rules=state.vRules;
1394         for(int i=0;i<rules.size();i++) {
1395             Rule r=(Rule)rules.get(i);
1396             if (r.getInclusion().getTargetDescriptors().contains(sd1)) {
1397                 /* Rule may add items to sd1 */
1398                 SetInclusion si=(SetInclusion)r.getInclusion();
1399                 Expr ve=si.getExpr();
1400                 DNFRule drule=r.getDNFGuardExpr();
1401                 for(int j=0;j<drule.size();j++) {
1402                     RuleConjunction rconj=drule.get(j);
1403                     boolean containsexclusion=false;
1404                     for (int k=0;k<rconj.size();k++) {
1405                         DNFExpr dexpr=rconj.get(k);
1406                         if (dexpr.getNegation()&&
1407                             dexpr.getExpr() instanceof ElementOfExpr&&
1408                             ((ElementOfExpr)dexpr.getExpr()).element.equals(null,ve)) {
1409                             SetDescriptor sd=((ElementOfExpr)dexpr.getExpr()).set;
1410                             if (sd.isSubset(sd2))
1411                                 containsexclusion=true;
1412                         }
1413                     }
1414                     if (!containsexclusion)
1415                         return false;
1416                 }
1417             }
1418         }
1419         return true;
1420     }
1421
1422     boolean equivalent(SetExpr se, RelationExpr re) {
1423         if (!(se instanceof ImageSetExpr))
1424             return false;
1425         ImageSetExpr ise=(ImageSetExpr)se;
1426         while(re!=null&&ise!=null) {
1427             if (re.getRelation()!=ise.getRelation())
1428                 return false;
1429             if (re.inverted()!=ise.inverted())
1430                 return false;
1431             if (ise.isimageset) {
1432                 ise=ise.getImageSetExpr();
1433                 if (!(re.getExpr() instanceof RelationExpr))
1434                     return false;
1435                 re=(RelationExpr)re.getExpr();
1436             } else {
1437                 if (!(re.getExpr() instanceof VarExpr))
1438                     return false;
1439                 if (((VarExpr)re.getExpr()).getVar()==ise.getVar())
1440                     return true; //everything matches
1441                 return false;
1442             }
1443         }
1444         return false;
1445     }
1446 }