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