Repair/RepairCompiler/MCC/IR/RepairGenerator.java

   1 package MCC.IR;
   2
   3 import java.io.*;
   4 import java.util.*;
   5 import MCC.State;
   6
   7 public class RepairGenerator {
   8     State state;
   9     java.io.PrintWriter outputrepair = null;
  10     java.io.PrintWriter outputaux = null;
  11     java.io.PrintWriter outputhead = null;
  12     String name="foo";
  13     String headername;
  14     static VarDescriptor oldmodel=null;
  15     static VarDescriptor newmodel=null;
  16     static VarDescriptor worklist=null;
  17     static VarDescriptor repairtable=null;
  18     static VarDescriptor goodflag=null;
  19     Rule currentrule=null;
  20     Hashtable updatenames;
  21     HashSet usedupdates;
  22     Termination termination;
  23     Set removed;
  24     static boolean DEBUG=false;
  25     Cost cost;
  26     Sources sources;
  27
  28     public RepairGenerator(State state, Termination t) {
  29         this.state = state;
  30         updatenames=new Hashtable();
  31         usedupdates=new HashSet();
  32         termination=t;
  33         removed=t.removedset;
  34         cost=new Cost();
  35         sources=new Sources(state);
  36         Repair.repairgenerator=this;
  37     }
  38
  39     private void name_updates() {
  40         int count=0;
  41         for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
  42             GraphNode gn=(GraphNode) it.next();
  43             TermNode tn=(TermNode) gn.getOwner();
  44             MultUpdateNode mun=tn.getUpdate();
  45             for (int i=0;i<mun.numUpdates();i++) {
  46                 UpdateNode un=mun.getUpdate(i);
  47                 String name="update"+String.valueOf(count++);
  48                 updatenames.put(un,name);
  49             }
  50         }
  51     }
  52
  53     public void generate(OutputStream outputrepair, OutputStream outputaux,OutputStream outputhead, String st) {
  54         this.outputrepair = new java.io.PrintWriter(outputrepair, true);
  55         this.outputaux = new java.io.PrintWriter(outputaux, true);
  56         this.outputhead = new java.io.PrintWriter(outputhead, true);
  57         headername=st;
  58         name_updates();
  59
  60         generate_tokentable();
  61         generate_hashtables();
  62         generate_stateobject();
  63         generate_call();
  64         generate_worklist();
  65         generate_rules();
  66         generate_checks();
  67         generate_teardown();
  68         CodeWriter crhead = new StandardCodeWriter(this.outputhead);
  69         CodeWriter craux = new StandardCodeWriter(this.outputaux);
  70         crhead.outputline("};");
  71         craux.outputline("};");
  72     }
  73
  74
  75
  76     private void generate_call() {
  77         CodeWriter cr = new StandardCodeWriter(outputrepair);
  78         VarDescriptor vdstate=VarDescriptor.makeNew("repairstate");
  79         cr.outputline(name+"_state * "+vdstate.getSafeSymbol()+"=new "+name+"_state();");
  80         Iterator globals=state.stGlobals.descriptors();
  81         while (globals.hasNext()) {
  82             VarDescriptor vd=(VarDescriptor) globals.next();
  83             cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
  84         }
  85         /* Insert repair here */
  86         cr.outputline(vdstate.getSafeSymbol()+"->doanalysis();");
  87         globals=state.stGlobals.descriptors();
  88         while (globals.hasNext()) {
  89             VarDescriptor vd=(VarDescriptor) globals.next();
  90             cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";");
  91         }
  92         cr.outputline("delete "+vdstate.getSafeSymbol()+";");
  93     }
  94
  95     private void generate_tokentable() {
  96         CodeWriter cr = new StandardCodeWriter(outputrepair);
  97         Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();
  98
  99         cr.outputline("");
 100         cr.outputline("// Token values");
 101         cr.outputline("");
 102
 103         while (tokens.hasNext()) {
 104             Object token = tokens.next();
 105             cr.outputline("// " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString());
 106         }
 107
 108         cr.outputline("");
 109         cr.outputline("");
 110     }
 111
 112     private void generate_stateobject() {
 113         CodeWriter crhead = new StandardCodeWriter(outputhead);
 114         crhead.outputline("class "+name+"_state {");
 115         crhead.outputline("public:");
 116         Iterator globals=state.stGlobals.descriptors();
 117         while (globals.hasNext()) {
 118             VarDescriptor vd=(VarDescriptor) globals.next();
 119             crhead.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+";");
 120         }
 121     }
 122
 123     private void generate_hashtables() {
 124         CodeWriter craux = new StandardCodeWriter(outputaux);
 125         CodeWriter crhead = new StandardCodeWriter(outputhead);
 126         crhead.outputline("#include \"SimpleHash.h\"");
 127         crhead.outputline("#include <stdio.h>");
 128         crhead.outputline("#include <stdlib.h>");
 129         crhead.outputline("class "+name+" {");
 130         crhead.outputline("public:");
 131         crhead.outputline(name+"();");
 132         crhead.outputline("~"+name+"();");
 133         craux.outputline("#include \""+headername+"\"");
 134
 135         craux.outputline(name+"::"+name+"() {");
 136         craux.outputline("// creating hashtables ");
 137
 138         /* build sets */
 139         Iterator sets = state.stSets.descriptors();
 140
 141         /* first pass create all the hash tables */
 142         while (sets.hasNext()) {
 143             SetDescriptor set = (SetDescriptor) sets.next();
 144             crhead.outputline("SimpleHash* " + set.getSafeSymbol() + "_hash;");
 145             craux.outputline(set.getSafeSymbol() + "_hash = new SimpleHash();");
 146         }
 147
 148         /* second pass build relationships between hashtables */
 149         sets = state.stSets.descriptors();
 150
 151         while (sets.hasNext()) {
 152             SetDescriptor set = (SetDescriptor) sets.next();
 153             Iterator subsets = set.subsets();
 154
 155             while (subsets.hasNext()) {
 156                 SetDescriptor subset = (SetDescriptor) subsets.next();
 157                 craux.outputline(subset.getSafeSymbol() + "_hash->addParent(" + set.getSafeSymbol() + "_hash);");
 158             }
 159         }
 160
 161         /* build relations */
 162         Iterator relations = state.stRelations.descriptors();
 163
 164         /* first pass create all the hash tables */
 165         while (relations.hasNext()) {
 166             RelationDescriptor relation = (RelationDescriptor) relations.next();
 167
 168             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 169                 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hash;");
 170                 craux.outputline(relation.getSafeSymbol() + "_hash = new SimpleHash();");
 171             }
 172
 173             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 174                 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hashinv;");
 175                 craux.outputline(relation.getSafeSymbol() + "_hashinv = new SimpleHash();");
 176             }
 177         }
 178
 179         craux.outputline("}");
 180         crhead.outputline("};");
 181         craux.outputline(name+"::~"+name+"() {");
 182         craux.outputline("// deleting hashtables");
 183
 184         /* build destructor */
 185         sets = state.stSets.descriptors();
 186
 187         /* first pass create all the hash tables */
 188         while (sets.hasNext()) {
 189             SetDescriptor set = (SetDescriptor) sets.next();
 190             craux.outputline("delete "+set.getSafeSymbol() + "_hash;");
 191         }
 192
 193         /* destroy relations */
 194         relations = state.stRelations.descriptors();
 195
 196         /* first pass create all the hash tables */
 197         while (relations.hasNext()) {
 198             RelationDescriptor relation = (RelationDescriptor) relations.next();
 199
 200             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 201                 craux.outputline("delete "+relation.getSafeSymbol() + "_hash;");
 202             }
 203
 204             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 205                 craux.outputline("delete " + relation.getSafeSymbol() + ";");
 206             }
 207         }
 208         craux.outputline("}");
 209     }
 210
 211     private void generate_worklist() {
 212         CodeWriter crhead = new StandardCodeWriter(outputhead);
 213         CodeWriter craux = new StandardCodeWriter(outputaux);
 214         oldmodel=VarDescriptor.makeNew("oldmodel");
 215         newmodel=VarDescriptor.makeNew("newmodel");
 216         worklist=VarDescriptor.makeNew("worklist");
 217         goodflag=VarDescriptor.makeNew("goodflag");
 218         repairtable=VarDescriptor.makeNew("repairtable");
 219         crhead.outputline("void doanalysis();");
 220         craux.outputline("void "+name +"_state::doanalysis()");
 221         craux.startblock();
 222         craux.outputline(name+ " * "+oldmodel.getSafeSymbol()+"=0;");
 223         craux.outputline("WorkList * "+worklist.getSafeSymbol()+" = new WorkList();");
 224         craux.outputline("RepairHash * "+repairtable.getSafeSymbol()+"=0;");
 225         craux.outputline("while (1)");
 226         craux.startblock();
 227         craux.outputline("int "+goodflag.getSafeSymbol()+"=1;");
 228         craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
 229     }
 230
 231     private void generate_teardown() {
 232         CodeWriter cr = new StandardCodeWriter(outputaux);
 233         cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 234         cr.outputline("delete "+repairtable.getSafeSymbol()+";");
 235         cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 236         cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 237         cr.outputline("delete "+newmodel.getSafeSymbol()+";");
 238         cr.outputline("delete "+worklist.getSafeSymbol()+";");
 239         cr.endblock();
 240     }
 241
 242     private void generate_rules() {
 243         /* first we must sort the rules */
 244         Iterator allrules = state.vRules.iterator();
 245         Vector emptyrules = new Vector(); // rules with no quantifiers
 246         Vector worklistrules = new Vector(); // the rest of the rules
 247         RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 248         SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 249
 250         while (allrules.hasNext()) {
 251             Rule rule = (Rule) allrules.next();
 252             ListIterator quantifiers = rule.quantifiers();
 253             boolean noquantifiers = true;
 254             while (quantifiers.hasNext()) {
 255                 Quantifier quantifier = (Quantifier) quantifiers.next();
 256                 if (quantifier instanceof ForQuantifier) {
 257                     // ok, because integers exist already!
 258                 } else {
 259                     // real quantifier
 260                     noquantifiers = false;
 261                     break;
 262                 }
 263             }
 264             if (noquantifiers) {
 265                 emptyrules.add(rule);
 266             } else {
 267                 worklistrules.add(rule);
 268             }
 269         }
 270
 271         Iterator iterator_er = emptyrules.iterator();
 272         while (iterator_er.hasNext()) {
 273             Rule rule = (Rule) iterator_er.next();
 274             {
 275                 final SymbolTable st = rule.getSymbolTable();
 276                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 277                         public SymbolTable getSymbolTable() { return st; }
 278                     };
 279                 cr.outputline("// build " +escape(rule.toString()));
 280                 cr.startblock();
 281                 ListIterator quantifiers = rule.quantifiers();
 282                 while (quantifiers.hasNext()) {
 283                     Quantifier quantifier = (Quantifier) quantifiers.next();
 284                     quantifier.generate_open(cr);
 285                 }
 286
 287                 /* pretty print! */
 288                 cr.output("//");
 289                 rule.getGuardExpr().prettyPrint(cr);
 290                 cr.outputline("");
 291
 292                 /* now we have to generate the guard test */
 293                 VarDescriptor guardval = VarDescriptor.makeNew();
 294                 rule.getGuardExpr().generate(cr, guardval);
 295                 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 296                 cr.startblock();
 297
 298                 /* now we have to generate the inclusion code */
 299                 currentrule=rule;
 300                 rule.getInclusion().generate(cr);
 301                 cr.endblock();
 302                 while (quantifiers.hasPrevious()) {
 303                     Quantifier quantifier = (Quantifier) quantifiers.previous();
 304                     cr.endblock();
 305                 }
 306                 cr.endblock();
 307                 cr.outputline("");
 308                 cr.outputline("");
 309             }
 310         }
 311
 312         CodeWriter cr2 = new StandardCodeWriter(outputaux);
 313
 314         cr2.outputline("while ("+goodflag.getSafeSymbol()+"&&"+worklist.getSafeSymbol()+"->hasMoreElements())");
 315         cr2.startblock();
 316         VarDescriptor idvar=VarDescriptor.makeNew("id");
 317         cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
 318
 319         String elseladder = "if";
 320
 321         Iterator iterator_rules = worklistrules.iterator();
 322         while (iterator_rules.hasNext()) {
 323
 324             Rule rule = (Rule) iterator_rules.next();
 325             int dispatchid = rule.getNum();
 326
 327             {
 328                 final SymbolTable st = rule.getSymbolTable();
 329                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 330                         public SymbolTable getSymbolTable() { return st; }
 331                     };
 332
 333                 cr.indent();
 334                 cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
 335                 cr.startblock();
 336                 VarDescriptor typevar=VarDescriptor.makeNew("type");
 337                 VarDescriptor leftvar=VarDescriptor.makeNew("left");
 338                 VarDescriptor rightvar=VarDescriptor.makeNew("right");
 339                 cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
 340                 cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
 341                 cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
 342                 cr.outputline("// build " +escape(rule.toString()));
 343
 344
 345                 for (int j=0;j<rule.numQuantifiers();j++) {
 346                     Quantifier quantifier = rule.getQuantifier(j);
 347                     quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
 348                 }
 349
 350                 /* pretty print! */
 351                 cr.output("//");
 352
 353                 rule.getGuardExpr().prettyPrint(cr);
 354                 cr.outputline("");
 355
 356                 /* now we have to generate the guard test */
 357
 358                 VarDescriptor guardval = VarDescriptor.makeNew();
 359                 rule.getGuardExpr().generate(cr, guardval);
 360
 361                 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 362                 cr.startblock();
 363
 364                 /* now we have to generate the inclusion code */
 365                 currentrule=rule;
 366                 rule.getInclusion().generate(cr);
 367                 cr.endblock();
 368
 369                 for (int j=0;j<rule.numQuantifiers();j++) {
 370                     cr.endblock();
 371                 }
 372
 373                 // close startblocks generated by DotExpr memory checks
 374                 //DotExpr.generate_memory_endblocks(cr);
 375
 376                 cr.endblock(); // end else-if WORKLIST ladder
 377
 378                 elseladder = "else if";
 379             }
 380         }
 381
 382         cr2.outputline("else");
 383         cr2.startblock();
 384         cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
 385         cr2.outputline("exit(1);");
 386         cr2.endblock();
 387         // end block created for worklist
 388         cr2.endblock();
 389     }
 390
 391     public static String escape(String s) {
 392         String newstring="";
 393         for(int i=0;i<s.length();i++) {
 394             char c=s.charAt(i);
 395             if (c=='"')
 396                 newstring+="\"";
 397             else
 398                 newstring+=c;
 399         }
 400         return newstring;
 401     }
 402
 403     private void generate_checks() {
 404
 405         /* do constraint checks */
 406         Vector constraints = state.vConstraints;
 407
 408         for (int i = 0; i < constraints.size(); i++) {
 409
 410             Constraint constraint = (Constraint) constraints.elementAt(i);
 411
 412             {
 413
 414                 final SymbolTable st = constraint.getSymbolTable();
 415
 416                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 417                         public SymbolTable getSymbolTable() { return st; }
 418                     };
 419
 420                 cr.outputline("// checking " + escape(constraint.toString()));
 421                 cr.startblock();
 422
 423                 ListIterator quantifiers = constraint.quantifiers();
 424
 425                 while (quantifiers.hasNext()) {
 426                     Quantifier quantifier = (Quantifier) quantifiers.next();
 427                     quantifier.generate_open(cr);
 428                 }
 429
 430                 cr.outputline("int maybe = 0;");
 431
 432                 /* now we have to generate the guard test */
 433
 434                 VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
 435                 constraint.getLogicStatement().generate(cr, constraintboolean);
 436
 437                 cr.outputline("if (maybe)");
 438                 cr.startblock();
 439                 cr.outputline("printf(\"maybe fail " +  escape(constraint.toString()) + ". \");");
 440                 cr.outputline("exit(1);");
 441                 cr.endblock();
 442
 443                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
 444                 cr.startblock();
 445                 if (DEBUG)
 446                     cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \");");
 447
 448                 /* Do repairs */
 449                 /* Build new repair table */
 450                 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 451                 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
 452                 cr.outputline(repairtable.getSafeSymbol()+"=new RepairHash();");
 453
 454
 455                 /* Compute cost of each repair */
 456                 VarDescriptor mincost=VarDescriptor.makeNew("mincost");
 457                 VarDescriptor mincostindex=VarDescriptor.makeNew("mincostindex");
 458                 DNFConstraint dnfconst=constraint.dnfconstraint;
 459                 cr.outputline("int "+mincostindex.getSafeSymbol()+";");
 460                 if (dnfconst.size()>1) {
 461                     boolean first=true;
 462                     for(int j=0;j<dnfconst.size();j++) {
 463                         Conjunction conj=dnfconst.get(j);
 464                         GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
 465                         if (removed.contains(gn))
 466                             continue;
 467
 468                         VarDescriptor costvar;
 469                         if (first) {
 470                             costvar=mincost;
 471                         } else
 472                             costvar=VarDescriptor.makeNew("cost");
 473                         for(int k=0;k<conj.size();k++) {
 474                             DNFPredicate dpred=conj.get(k);
 475                             Predicate p=dpred.getPredicate();
 476                             boolean negate=dpred.isNegated();
 477                             VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 478                             p.generate(cr,predvalue);
 479                             if (negate)
 480                                 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 481                             else
 482                                 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 483                             if (k==0)
 484                                 cr.outputline("int "+costvar.getSafeSymbol()+"="+cost.getCost(dpred)+";");
 485                             else
 486                                 cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
 487                         }
 488
 489                         if(!first) {
 490                             cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
 491                             cr.startblock();
 492                             cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
 493                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
 494                             cr.endblock();
 495                         } else
 496                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
 497                         first=false;
 498                     }
 499                 }
 500                 cr.outputline("switch("+mincostindex.getSafeSymbol()+") {");
 501                 for(int j=0;j<dnfconst.size();j++) {
 502                     Conjunction conj=dnfconst.get(j);
 503                     GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);                    if (removed.contains(gn))
 504                         continue;
 505                     cr.outputline("case "+j+":");
 506                     for(int k=0;k<conj.size();k++) {
 507                         DNFPredicate dpred=conj.get(k);
 508                         Predicate p=dpred.getPredicate();
 509                         boolean negate=dpred.isNegated();
 510                         VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 511                         p.generate(cr,predvalue);
 512                         if (negate)
 513                             cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 514                         else
 515                             cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 516                         if (p instanceof InclusionPredicate)
 517                             generateinclusionrepair(conj,dpred, cr);
 518                         else if (p instanceof ExprPredicate) {
 519                             ExprPredicate ep=(ExprPredicate)p;
 520                             if (ep.getType()==ExprPredicate.SIZE)
 521                                 generatesizerepair(conj,dpred,cr);
 522                             else if (ep.getType()==ExprPredicate.COMPARISON)
 523                                 generatecomparisonrepair(conj,dpred,cr);
 524                         } else throw new Error("Unrecognized Predicate");
 525                     }
 526                     /* Update model */
 527
 528                     cr.outputline("break;");
 529                 }
 530                 cr.outputline("}");
 531
 532                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
 533                 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 534                 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 535                 cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
 536                 cr.outputline("break;");  /* Rebuild model and all */
 537
 538                 cr.endblock();
 539
 540                 while (quantifiers.hasPrevious()) {
 541                     Quantifier quantifier = (Quantifier) quantifiers.previous();
 542                     cr.endblock();
 543                 }
 544                 cr.outputline("if ("+goodflag.getSafeSymbol()+")");
 545                 cr.outputline("break;");
 546                 cr.endblock();
 547                 cr.outputline("");
 548                 cr.outputline("");
 549             }
 550         }
 551     }
 552
 553     private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
 554         MultUpdateNode mun=null;
 555         GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
 556
 557         for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
 558             GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
 559             TermNode tn2=(TermNode)gn2.getOwner();
 560             if (tn2.getType()==TermNode.ABSTRACT) {
 561                 AbstractRepair ar=tn2.getAbstract();
 562                 if (((repairtype==-1)||(ar.getType()==repairtype))&&
 563                     ar.getPredicate()==dpred) {
 564                     for(Iterator edgeit2=gn2.edges();edgeit.hasNext();) {
 565                         GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
 566                         if (!removed.contains(gn3)) {
 567                             TermNode tn3=(TermNode)gn3.getOwner();
 568                             if (tn3.getType()==TermNode.UPDATE) {
 569                                 mun=tn3.getUpdate();
 570                                 break;
 571                             }
 572                         }
 573                     }
 574                 }
 575             }
 576         }
 577         return mun;
 578     }
 579
 580     public void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
 581         MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
 582         MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
 583         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 584         RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
 585         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 586         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 587         boolean inverted=ep.inverted();
 588         boolean negated=dpred.isNegated();
 589         OpExpr expr=(OpExpr)ep.expr;
 590         Opcode opcode=expr.getOpcode();
 591         VarDescriptor leftside=VarDescriptor.makeNew("leftside");
 592         VarDescriptor rightside=VarDescriptor.makeNew("rightside");
 593         VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
 594         if (!inverted) {
 595             expr.getLeftExpr().generate(cr,leftside);
 596             expr.getRightExpr().generate(cr,newvalue);
 597             cr.outputline(rd.getRange().getType().getGenerateType().getSafeSymbol()+" "+rightside.getSafeSymbol()+";");
 598             cr.outputline(rd.getSafeSymbol()+"_hash->get("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 599         } else {
 600             expr.getLeftExpr().generate(cr,rightside);
 601             expr.getRightExpr().generate(cr,newvalue);
 602             cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
 603             cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+leftside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 604         }
 605         if (negated)
 606             if (opcode==Opcode.GT) {
 607                 opcode=Opcode.LE;
 608             } else if (opcode==Opcode.GE) {
 609                 opcode=Opcode.LT;
 610             } else if (opcode==Opcode.LT) {
 611                 opcode=Opcode.GE;
 612             } else if (opcode==Opcode.LE) {
 613                 opcode=Opcode.GT;
 614             } else if (opcode==Opcode.EQ) {
 615                 opcode=Opcode.NE;
 616             } else if (opcode==Opcode.NE) {
 617                 opcode=Opcode.EQ;
 618             } else {
 619                 throw new Error("Unrecognized Opcode");
 620             }
 621
 622         if (opcode==Opcode.GT) {
 623             cr.outputline(newvalue.getSafeSymbol()+"++;");
 624         } else if (opcode==Opcode.GE) {
 625             /* Equal */
 626         } else if (opcode==Opcode.LT) {
 627             cr.outputline(newvalue.getSafeSymbol()+"--;");
 628         } else if (opcode==Opcode.LE) {
 629             /* Equal */
 630         } else if (opcode==Opcode.EQ) {
 631             /* Equal */
 632         } else if (opcode==Opcode.NE) {
 633             cr.outputline(newvalue.getSafeSymbol()+"++;");
 634         } else {
 635             throw new Error("Unrecognized Opcode");
 636         }
 637         /* Do abstract repairs */
 638         if (usageimage) {
 639             cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 640             if (!inverted) {
 641                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 642             } else {
 643                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 644             }
 645         }
 646         if (usageinvimage) {
 647             cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 648             if (!inverted) {
 649                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 650             } else {
 651                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 652             }
 653         }
 654         /* Do concrete repairs */
 655         /* Start with scheduling removal */
 656         for(int i=0;i<state.vRules.size();i++) {
 657             Rule r=(Rule)state.vRules.get(i);
 658             if (r.getInclusion().getTargetDescriptors().contains(rd)) {
 659                 for(int j=0;j<munremove.numUpdates();j++) {
 660                     UpdateNode un=munremove.getUpdate(i);
 661                     if (un.getRule()==r) {
 662                         /* Update for rule r */
 663                         String name=(String)updatenames.get(un);
 664                         cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
 665                     }
 666                 }
 667             }
 668         }
 669         /* Now do addition */
 670         UpdateNode un=munadd.getUpdate(0);
 671         String name=(String)updatenames.get(un);
 672         if (!inverted) {
 673             cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 674         } else {
 675             cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 676         }
 677     }
 678
 679     public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {
 680         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 681         OpExpr expr=(OpExpr)ep.expr;
 682         Opcode opcode=expr.getOpcode();
 683         {
 684             boolean negated=dpred.isNegated();
 685             if (negated)
 686                 if (opcode==Opcode.GT) {
 687                     opcode=Opcode.LE;
 688                 } else if (opcode==Opcode.GE) {
 689                     opcode=Opcode.LT;
 690                 } else if (opcode==Opcode.LT) {
 691                     opcode=Opcode.GE;
 692                 } else if (opcode==Opcode.LE) {
 693                     opcode=Opcode.GT;
 694                 } else if (opcode==Opcode.EQ) {
 695                     opcode=Opcode.NE;
 696                 } else if (opcode==Opcode.NE) {
 697                     opcode=Opcode.EQ;
 698                 } else {
 699                     throw new Error("Unrecognized Opcode");
 700                 }
 701         }
 702         MultUpdateNode munremove;
 703
 704         MultUpdateNode munadd;
 705         if (ep.getDescriptor() instanceof RelationDescriptor) {
 706             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
 707             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
 708         } else {
 709             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
 710             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
 711         }
 712         int size=ep.leftsize();
 713         VarDescriptor sizevar=VarDescriptor.makeNew("size");
 714         ((OpExpr)expr).left.generate(cr, sizevar);
 715         VarDescriptor change=VarDescriptor.makeNew("change");
 716         cr.outputline("int "+change.getSafeSymbol()+";");
 717         boolean generateadd=false;
 718         boolean generateremove=false;
 719         if (opcode==Opcode.GT) {
 720             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
 721             generateadd=true;
 722             generateremove=false;
 723         } else if (opcode==Opcode.GE) {
 724             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 725             generateadd=true;
 726             generateremove=false;
 727         } else if (opcode==Opcode.LT) {
 728             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
 729             generateadd=false;
 730             generateremove=true;
 731         } else if (opcode==Opcode.LE) {
 732             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 733             generateadd=false;
 734             generateremove=true;
 735         } else if (opcode==Opcode.EQ) {
 736             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 737             generateadd=true;
 738             generateremove=true;
 739         } else if (opcode==Opcode.NE) {
 740             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
 741             generateadd=true;
 742             generateremove=false;
 743         } else {
 744             throw new Error("Unrecognized Opcode");
 745         }
 746         Descriptor d=ep.getDescriptor();
 747         if (generateremove) {
 748             cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
 749             cr.startblock();
 750             /* Find element to remove */
 751             VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
 752             VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
 753             if (d instanceof RelationDescriptor) {
 754                 if (ep.inverted()) {
 755                     rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
 756                     cr.outputline("int "+leftvar.getSafeSymbol()+";");
 757                     cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
 758                 } else {
 759                     leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
 760                     cr.outputline("int "+rightvar.getSafeSymbol()+";");
 761                     cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
 762                 }
 763             } else {
 764                 cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
 765             }
 766             /* Generate abstract remove instruction */
 767             if (d instanceof RelationDescriptor) {
 768                 RelationDescriptor rd=(RelationDescriptor) d;
 769                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 770                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 771                 if (usageimage)
 772                     cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
 773                 if (usageinvimage)
 774                     cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
 775             } else {
 776                 cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
 777             }
 778             /* Generate concrete remove instruction */
 779             for(int i=0;i<state.vRules.size();i++) {
 780                 Rule r=(Rule)state.vRules.get(i);
 781                 if (r.getInclusion().getTargetDescriptors().contains(d)) {
 782                     for(int j=0;j<munremove.numUpdates();j++) {
 783                         UpdateNode un=munremove.getUpdate(i);
 784                         if (un.getRule()==r) {
 785                                 /* Update for rule rule r */
 786                             String name=(String)updatenames.get(un);
 787                             if (d instanceof RelationDescriptor) {
 788                                 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
 789                             } else {
 790                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
 791                             }
 792                         }
 793                     }
 794                 }
 795             }
 796             cr.endblock();
 797         }
 798         if (generateadd) {
 799             cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
 800             cr.startblock();
 801             cr.endblock();
 802         }
 803     }
 804
 805     public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
 806         InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate();
 807         boolean negated=dpred.isNegated();
 808         MultUpdateNode mun=getmultupdatenode(conj,dpred,-1);
 809         VarDescriptor leftvar=VarDescriptor.makeNew("left");
 810         ip.expr.generate(cr, leftvar);
 811
 812         if (negated) {
 813             if (ip.setexpr instanceof ImageSetExpr) {
 814                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
 815                 VarDescriptor rightvar=ise.getVar();
 816                 boolean inverse=ise.inverted();
 817                 RelationDescriptor rd=ise.getRelation();
 818                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 819                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 820                 if (inverse) {
 821                     if (usageimage)
 822                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar + ", (int)" + leftvar + ");");
 823                     if (usageinvimage)
 824                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar + ", (int)" + rightvar + ");");
 825                 } else {
 826                     if (usageimage)
 827                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
 828                     if (usageinvimage)
 829                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
 830                 }
 831                 for(int i=0;i<state.vRules.size();i++) {
 832                     Rule r=(Rule)state.vRules.get(i);
 833                     if (r.getInclusion().getTargetDescriptors().contains(rd)) {
 834                         for(int j=0;j<mun.numUpdates();j++) {
 835                             UpdateNode un=mun.getUpdate(i);
 836                             if (un.getRule()==r) {
 837                                 /* Update for rule rule r */
 838                                 String name=(String)updatenames.get(un);
 839                                 if (inverse) {
 840                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
 841                                 } else {
 842                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
 843                                 }
 844                             }
 845                         }
 846                     }
 847                 }
 848             } else {
 849                 SetDescriptor sd=ip.setexpr.sd;
 850                 cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
 851
 852                 for(int i=0;i<state.vRules.size();i++) {
 853                     Rule r=(Rule)state.vRules.get(i);
 854                     if (r.getInclusion().getTargetDescriptors().contains(sd)) {
 855                         for(int j=0;j<mun.numUpdates();j++) {
 856                             UpdateNode un=mun.getUpdate(i);
 857                             if (un.getRule()==r) {
 858                                 /* Update for rule rule r */
 859                                 String name=(String)updatenames.get(un);
 860                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
 861                             }
 862                         }
 863                     }
 864                 }
 865             }
 866         } else {
 867             /* Generate update */
 868             if (ip.setexpr instanceof ImageSetExpr) {
 869                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
 870                 VarDescriptor rightvar=ise.getVar();
 871                 boolean inverse=ise.inverted();
 872                 RelationDescriptor rd=ise.getRelation();
 873                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 874                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 875                 if (inverse) {
 876                     if (usageimage)
 877                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar + ", (int)" + leftvar + ");");
 878                     if (usageinvimage)
 879                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar + ", (int)" + rightvar + ");");
 880                 } else {
 881                     if (usageimage)
 882                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
 883                     if (usageinvimage)
 884                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
 885                 }
 886                 UpdateNode un=mun.getUpdate(0);
 887                 String name=(String)updatenames.get(un);
 888                 if (inverse) {
 889                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
 890                 } else {
 891                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
 892                 }
 893             } else {
 894                 SetDescriptor sd=ip.setexpr.sd;
 895                 cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + leftvar + ");");
 896
 897                 UpdateNode un=mun.getUpdate(0);
 898                 /* Update for rule rule r */
 899                 String name=(String)updatenames.get(un);
 900                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
 901             }
 902         }
 903     }
 904
 905
 906
 907     public static Vector getrulelist(Descriptor d) {
 908         Vector dispatchrules = new Vector();
 909         Vector rules = State.currentState.vRules;
 910
 911         for (int i = 0; i < rules.size(); i++) {
 912             Rule rule = (Rule) rules.elementAt(i);
 913             Set requiredsymbols = rule.getRequiredDescriptors();
 914
 915             // #TBD#: in general this is wrong because these descriptors may contain descriptors
 916             // bound in "in?" expressions which need to be dealt with in a topologically sorted
 917             // fashion...
 918
 919             if (rule.getRequiredDescriptors().contains(d)) {
 920                 dispatchrules.addElement(rule);
 921             }
 922         }
 923         return dispatchrules;
 924     }
 925
 926     private boolean need_compensation(Rule r) {
 927         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
 928         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
 929             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 930             GraphNode gn2=edge.getTarget();
 931             if (!removed.contains(gn2)) {
 932                 TermNode tn2=(TermNode)gn2.getOwner();
 933                 if (tn2.getType()==TermNode.CONSEQUENCE)
 934                     return false;
 935             }
 936         }
 937         return true;
 938     }
 939
 940     private UpdateNode find_compensation(Rule r) {
 941         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
 942         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
 943             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
 944             GraphNode gn2=edge.getTarget();
 945             if (!removed.contains(gn2)) {
 946                 TermNode tn2=(TermNode)gn2.getOwner();
 947                 if (tn2.getType()==TermNode.UPDATE) {
 948                     MultUpdateNode mun=tn2.getUpdate();
 949                     for(int i=0;i<mun.numUpdates();i++) {
 950                         UpdateNode un=mun.getUpdate(i);
 951                         if (un.getRule()==r)
 952                             return un;
 953                     }
 954                 }
 955             }
 956         }
 957         throw new Error("No Compensation Update could be found");
 958     }
 959
 960     public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
 961         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 962         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 963
 964         if (!(usageinvimage||usageimage)) /* not used at all*/
 965             return;
 966
 967         cr.outputline("// RELATION DISPATCH ");
 968         cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
 969         if (usageimage)
 970             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
 971         else
 972             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
 973         cr.startblock(); {
 974             /* Adding new item */
 975             /* Perform safety checks */
 976             cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
 977             cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
 978             cr.startblock(); {
 979                 /* Have update to call into */
 980                 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
 981                 String parttype="";
 982                 for(int i=0;i<currentrule.numQuantifiers();i++) {
 983                     if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
 984                         parttype=parttype+", int, int";
 985                     else
 986                         parttype=parttype+", int";
 987                 }
 988                 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
 989                 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
 990                 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
 991                 for(int i=0;i<currentrule.numQuantifiers();i++) {
 992                     Quantifier q=currentrule.getQuantifier(i);
 993                     if (q instanceof SetQuantifier) {
 994                         SetQuantifier sq=(SetQuantifier) q;
 995                         methodcall+=","+sq.getVar().getSafeSymbol();
 996                     } else if (q instanceof RelationQuantifier) {
 997                         RelationQuantifier rq=(RelationQuantifier) q;
 998                         methodcall+=","+rq.x.getSafeSymbol();
 999                         methodcall+=","+rq.y.getSafeSymbol();
1000                     } else if (q instanceof ForQuantifier) {
1001                         ForQuantifier fq=(ForQuantifier) q;
1002                         methodcall+=","+fq.getVar().getSafeSymbol();
1003                     }
1004                 }
1005                 methodcall+=");";
1006                 cr.outputline(methodcall);
1007                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1008                 cr.outputline("continue;");
1009             }
1010             cr.endblock();
1011             /* Build standard compensation actions */
1012             if (need_compensation(currentrule)) {
1013                 UpdateNode un=find_compensation(currentrule);
1014                 String name=(String)updatenames.get(un);
1015                 usedupdates.add(un); /* Mark as used */
1016                 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1017                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1018                     Quantifier q=currentrule.getQuantifier(i);
1019                     if (q instanceof SetQuantifier) {
1020                         SetQuantifier sq=(SetQuantifier) q;
1021                         methodcall+=","+sq.getVar().getSafeSymbol();
1022                     } else if (q instanceof RelationQuantifier) {
1023                         RelationQuantifier rq=(RelationQuantifier) q;
1024                         methodcall+=","+rq.x.getSafeSymbol();
1025                         methodcall+=","+rq.y.getSafeSymbol();
1026                     } else if (q instanceof ForQuantifier) {
1027                         ForQuantifier fq=(ForQuantifier) q;
1028                         methodcall+=","+fq.getVar().getSafeSymbol();
1029                     }
1030                 }
1031                 methodcall+=");";
1032                 cr.outputline(methodcall);
1033                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1034                 cr.outputline("continue;");
1035             }
1036         }
1037         cr.endblock();
1038
1039         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1040         cr.outputline("int " + addeditem + ";");
1041         if (rd.testUsage(RelationDescriptor.IMAGE)) {
1042             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
1043         }
1044
1045         if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1046             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1047         }
1048
1049         cr.outputline("if (" + addeditem + ")");
1050         cr.startblock();
1051
1052         Vector dispatchrules = getrulelist(rd);
1053
1054         if (dispatchrules.size() == 0) {
1055             cr.outputline("// nothing to dispatch");
1056             cr.endblock();
1057             return;
1058         }
1059
1060         for(int i = 0; i < dispatchrules.size(); i++) {
1061             Rule rule = (Rule) dispatchrules.elementAt(i);
1062             if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
1063                 /* Guard depends on this relation, so we recomput everything */
1064                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1065             } else {
1066                 for (int j=0;j<rule.numQuantifiers();j++) {
1067                     Quantifier q=rule.getQuantifier(j);
1068                     if (q.getRequiredDescriptors().contains(rd)) {
1069                         /* Generate add */
1070                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1071                     }
1072                 }
1073             }
1074         }
1075         cr.endblock();
1076     }
1077
1078
1079     public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1080
1081         cr.outputline("// SET DISPATCH ");
1082
1083         cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1084         cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
1085         cr.startblock(); {
1086             /* Adding new item */
1087             /* Perform safety checks */
1088             cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1089             cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
1090             cr.startblock(); {
1091                 /* Have update to call into */
1092                 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1093                 String parttype="";
1094                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1095                     if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1096                         parttype=parttype+", int, int";
1097                     else
1098                         parttype=parttype+", int";
1099                 }
1100                 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1101                 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getset("+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
1102                 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+
1103                               repairtable.getSafeSymbol();
1104                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1105                     Quantifier q=currentrule.getQuantifier(i);
1106                     if (q instanceof SetQuantifier) {
1107                         SetQuantifier sq=(SetQuantifier) q;
1108                         methodcall+=","+sq.getVar().getSafeSymbol();
1109                     } else if (q instanceof RelationQuantifier) {
1110                         RelationQuantifier rq=(RelationQuantifier) q;
1111                         methodcall+=","+rq.x.getSafeSymbol();
1112                         methodcall+=","+rq.y.getSafeSymbol();
1113                     } else if (q instanceof ForQuantifier) {
1114                         ForQuantifier fq=(ForQuantifier) q;
1115                         methodcall+=","+fq.getVar().getSafeSymbol();
1116                     }
1117                 }
1118                 methodcall+=");";
1119                 cr.outputline(methodcall);
1120                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1121                 cr.outputline("continue;");
1122             }
1123             cr.endblock();
1124             /* Build standard compensation actions */
1125             if (need_compensation(currentrule)) {
1126                 UpdateNode un=find_compensation(currentrule);
1127                 String name=(String)updatenames.get(un);
1128                 usedupdates.add(un); /* Mark as used */
1129
1130                 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
1131                               repairtable.getSafeSymbol();
1132                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1133                     Quantifier q=currentrule.getQuantifier(i);
1134                     if (q instanceof SetQuantifier) {
1135                         SetQuantifier sq=(SetQuantifier) q;
1136                         methodcall+=","+sq.getVar().getSafeSymbol();
1137                     } else if (q instanceof RelationQuantifier) {
1138                         RelationQuantifier rq=(RelationQuantifier) q;
1139                         methodcall+=","+rq.x.getSafeSymbol();
1140                         methodcall+=","+rq.y.getSafeSymbol();
1141                     } else if (q instanceof ForQuantifier) {
1142                         ForQuantifier fq=(ForQuantifier) q;
1143                         methodcall+=","+fq.getVar().getSafeSymbol();
1144                     }
1145                 }
1146                 methodcall+=");";
1147                 cr.outputline(methodcall);
1148                 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1149                 cr.outputline("continue;");
1150             }
1151         }
1152         cr.endblock();
1153
1154         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1155         cr.outputline("int " + addeditem + " = 1;");
1156         cr.outputline(addeditem + " = " + sd.getSafeSymbol() + "_hash->add((int)" + setvar +  ", (int)" + setvar + ");");
1157         cr.startblock();
1158         Vector dispatchrules = getrulelist(sd);
1159
1160         if (dispatchrules.size() == 0) {
1161             cr.outputline("// nothing to dispatch");
1162             cr.endblock();
1163             return;
1164         }
1165
1166         for(int i = 0; i < dispatchrules.size(); i++) {
1167             Rule rule = (Rule) dispatchrules.elementAt(i);
1168             if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
1169                 /* Guard depends on this relation, so we recompute everything */
1170                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1171             } else {
1172                 for (int j=0;j<rule.numQuantifiers();j++) {
1173                     Quantifier q=rule.getQuantifier(j);
1174                     if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1175                         /* Generate add */
1176                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");
1177                     }
1178                 }
1179             }
1180         }
1181         cr.endblock();
1182     }
1183 }
1184
1185
1186