Repair/RepairCompiler/MCC/IR/RepairGenerator.java

   1 package MCC.IR;
   2
   3 import java.io.*;
   4 import java.util.*;
   5 import MCC.State;
   6 import MCC.Compiler;
   7
   8 public class RepairGenerator {
   9     State state;
  10     java.io.PrintWriter outputrepair = null;
  11     java.io.PrintWriter outputaux = null;
  12     java.io.PrintWriter outputhead = null;
  13     String name="foo";
  14     String headername;
  15     static VarDescriptor oldmodel=null;
  16     static VarDescriptor newmodel=null;
  17     static VarDescriptor worklist=null;
  18     static VarDescriptor repairtable=null;
  19     static VarDescriptor goodflag=null;
  20     Rule currentrule=null;
  21     Hashtable updatenames;
  22     HashSet usedupdates;
  23     Termination termination;
  24     Set removed;
  25     HashSet togenerate;
  26     static boolean DEBUG=false;
  27     Cost cost;
  28     Sources sources;
  29     ModelRuleDependence mrd;
  30
  31     public RepairGenerator(State state, Termination t) {
  32         this.state = state;
  33         updatenames=new Hashtable();
  34         usedupdates=new HashSet();
  35         termination=t;
  36         removed=t.removedset;
  37         togenerate=new HashSet();
  38         togenerate.addAll(termination.conjunctions);
  39         if (Compiler.REPAIR)
  40             togenerate.removeAll(removed);
  41         GraphNode.computeclosure(togenerate,removed);
  42         cost=new Cost();
  43         sources=new Sources(state);
  44         mrd=ModelRuleDependence.doAnalysis(state);
  45         Repair.repairgenerator=this;
  46     }
  47
  48     private void generatetypechecks(boolean flag) {
  49         if (flag) {
  50             DotExpr.DOTYPECHECKS=true;
  51             VarExpr.DOTYPECHECKS=true;
  52             DotExpr.DONULL=true;
  53             VarExpr.DONULL=true;
  54         } else {
  55             VarExpr.DOTYPECHECKS=false;
  56             DotExpr.DOTYPECHECKS=false;
  57             VarExpr.DONULL=true;
  58             DotExpr.DONULL=true;
  59         }
  60     }
  61
  62
  63     private void name_updates() {
  64         int count=0;
  65         for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
  66             GraphNode gn=(GraphNode) it.next();
  67             TermNode tn=(TermNode) gn.getOwner();
  68             MultUpdateNode mun=tn.getUpdate();
  69             if (togenerate.contains(gn))
  70             for (int i=0;i<mun.numUpdates();i++) {
  71                 UpdateNode un=mun.getUpdate(i);
  72                 String name="update"+String.valueOf(count++);
  73                 updatenames.put(un,name);
  74             }
  75         }
  76     }
  77
  78     public void generate(OutputStream outputrepair, OutputStream outputaux,OutputStream outputhead, String st) {
  79         this.outputrepair = new java.io.PrintWriter(outputrepair, true);
  80         this.outputaux = new java.io.PrintWriter(outputaux, true);
  81         this.outputhead = new java.io.PrintWriter(outputhead, true);
  82         headername=st;
  83         name_updates();
  84         generatetypechecks(true);
  85         generate_tokentable();
  86         generate_hashtables();
  87         generate_stateobject();
  88         generate_call();
  89         generate_start();
  90         generate_rules();
  91         generate_checks();
  92         generate_teardown();
  93         CodeWriter crhead = new StandardCodeWriter(this.outputhead);
  94         CodeWriter craux = new StandardCodeWriter(this.outputaux);
  95         crhead.outputline("};");
  96         craux.outputline("}");
  97         generatetypechecks(false);
  98         generate_computesizes();
  99         generatetypechecks(true);
 100         generate_recomputesizes();
 101         generatetypechecks(false);
 102         generate_updates();
 103         StructureGenerator sg=new StructureGenerator(state,this);
 104         sg.buildall();
 105         crhead.outputline("#endif");
 106     }
 107
 108     String ststate="state";
 109     String stmodel="model";
 110     String strepairtable="repairtable";
 111     String stleft="left";
 112     String stright="right";
 113     String stnew="newvalue";
 114
 115     private void generate_updates() {
 116         int count=0;
 117         CodeWriter crhead = new StandardCodeWriter(outputhead);
 118         CodeWriter craux = new StandardCodeWriter(outputaux);
 119
 120         /* Rewrite globals */
 121
 122         for (Iterator it=this.state.stGlobals.descriptors();it.hasNext();) {
 123             VarDescriptor vd=(VarDescriptor)it.next();
 124             craux.outputline("#define "+vd.getSafeSymbol()+" "+ststate+"->"+vd.getSafeSymbol());
 125         }
 126
 127         for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
 128             GraphNode gn=(GraphNode) it.next();
 129             TermNode tn=(TermNode) gn.getOwner();
 130             MultUpdateNode mun=tn.getUpdate();
 131             boolean isrelation=(mun.getDescriptor() instanceof RelationDescriptor);
 132             if (togenerate.contains(gn))
 133             for (int i=0;i<mun.numUpdates();i++) {
 134                 UpdateNode un=mun.getUpdate(i);
 135                 String methodname=(String)updatenames.get(un);
 136
 137                 switch(mun.op) {
 138                 case MultUpdateNode.ADD:
 139                     if (isrelation) {
 140                         crhead.outputline("void "+methodname+"("+name+"_state * " +ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+", int "+stright+");");
 141                         craux.outputline("void "+methodname+"("+name+"_state * "+ ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+", int "+stright+")");
 142                     } else {
 143                         crhead.outputline("void "+methodname+"("+name+"_state * "+ ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+");");
 144                         craux.outputline("void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable+", int "+stleft+")");
 145                     }
 146                     craux.startblock();
 147                     craux.outputline("int maybe=0;");
 148                     final SymbolTable st = un.getRule().getSymbolTable();
 149                     CodeWriter cr = new StandardCodeWriter(outputaux) {
 150                         public SymbolTable getSymbolTable() { return st; }
 151                     };
 152                     un.generate(cr, false, false, stleft,stright, null,this);
 153                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 154                     craux.endblock();
 155                     break;
 156                 case MultUpdateNode.REMOVE: {
 157                     Rule r=un.getRule();
 158                     String methodcall="void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable;
 159                     for(int j=0;j<r.numQuantifiers();j++) {
 160                         Quantifier q=r.getQuantifier(j);
 161                         if (q instanceof SetQuantifier) {
 162                             SetQuantifier sq=(SetQuantifier) q;
 163                             methodcall+=","+sq.getVar().getType().getGenerateType().getSafeSymbol()+" "+sq.getVar().getSafeSymbol();
 164                         } else if (q instanceof RelationQuantifier) {
 165                             RelationQuantifier rq=(RelationQuantifier) q;
 166
 167                             methodcall+=","+rq.x.getType().getGenerateType().getSafeSymbol()+" "+rq.x.getSafeSymbol();
 168                             methodcall+=","+rq.y.getType().getGenerateType().getSafeSymbol()+" "+rq.y.getSafeSymbol();
 169                         } else if (q instanceof ForQuantifier) {
 170                             ForQuantifier fq=(ForQuantifier) q;
 171                             methodcall+=",int "+fq.getVar().getSafeSymbol();
 172                         }
 173                     }
 174                     methodcall+=")";
 175                     crhead.outputline(methodcall+";");
 176                     craux.outputline(methodcall);
 177                     craux.startblock();
 178                     craux.outputline("int maybe=0;");
 179                     final SymbolTable st2 = un.getRule().getSymbolTable();
 180                     CodeWriter cr2 = new StandardCodeWriter(outputaux) {
 181                         public SymbolTable getSymbolTable() { return st2; }
 182                     };
 183                     un.generate(cr2, true, false, null,null, null,this);
 184                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 185                     craux.endblock();
 186                 }
 187                     break;
 188                 case MultUpdateNode.MODIFY: {
 189                     Rule r=un.getRule();
 190                     String methodcall="void "+methodname+"("+name+"_state * "+ststate+","+name+" * "+stmodel+", RepairHash * "+strepairtable;
 191                     for(int j=0;j<r.numQuantifiers();j++) {
 192                         Quantifier q=r.getQuantifier(j);
 193                         if (q instanceof SetQuantifier) {
 194                             SetQuantifier sq=(SetQuantifier) q;
 195                             methodcall+=","+sq.getVar().getType().getGenerateType().getSafeSymbol()+" "+sq.getVar().getSafeSymbol();
 196                         } else if (q instanceof RelationQuantifier) {
 197                             RelationQuantifier rq=(RelationQuantifier) q;
 198
 199                             methodcall+=", "+rq.x.getType().getGenerateType().getSafeSymbol()+" "+rq.x.getSafeSymbol();
 200                             methodcall+=", "+rq.y.getType().getGenerateType().getSafeSymbol()+" "+rq.y.getSafeSymbol();
 201                         } else if (q instanceof ForQuantifier) {
 202                             ForQuantifier fq=(ForQuantifier) q;
 203                             methodcall+=", int "+fq.getVar().getSafeSymbol();
 204                         }
 205                     }
 206                     methodcall+=", "+stleft+", "+stright+", "+stnew;
 207                     methodcall+=")";
 208                     crhead.outputline(methodcall+";");
 209                     craux.outputline(methodcall);
 210                     craux.startblock();
 211                     craux.outputline("int maybe=0;");
 212                     final SymbolTable st2 = un.getRule().getSymbolTable();
 213                     CodeWriter cr2 = new StandardCodeWriter(outputaux) {
 214                         public SymbolTable getSymbolTable() { return st2; }
 215                     };
 216                     un.generate(cr2, false, true, stleft, stright, stnew, this);
 217                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 218                     craux.endblock();
 219                 }
 220                     break;
 221
 222                 default:
 223                     throw new Error("Nonimplement Update");
 224                 }
 225             }
 226         }
 227     }
 228
 229     private void generate_call() {
 230         CodeWriter cr = new StandardCodeWriter(outputrepair);
 231         VarDescriptor vdstate=VarDescriptor.makeNew("repairstate");
 232         cr.outputline(name+"_state * "+vdstate.getSafeSymbol()+"=new "+name+"_state();");
 233         Iterator globals=state.stGlobals.descriptors();
 234         while (globals.hasNext()) {
 235             VarDescriptor vd=(VarDescriptor) globals.next();
 236             cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
 237         }
 238         /* Insert repair here */
 239         cr.outputline(vdstate.getSafeSymbol()+"->doanalysis();");
 240         globals=state.stGlobals.descriptors();
 241         while (globals.hasNext()) {
 242             VarDescriptor vd=(VarDescriptor) globals.next();
 243             cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";");
 244         }
 245         cr.outputline("delete "+vdstate.getSafeSymbol()+";");
 246     }
 247
 248     private void generate_tokentable() {
 249         CodeWriter cr = new StandardCodeWriter(outputrepair);
 250         Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();
 251
 252         cr.outputline("");
 253         cr.outputline("// Token values");
 254         cr.outputline("");
 255
 256         while (tokens.hasNext()) {
 257             Object token = tokens.next();
 258             cr.outputline("// " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString());
 259         }
 260
 261         cr.outputline("");
 262         cr.outputline("");
 263     }
 264
 265     private void generate_stateobject() {
 266         CodeWriter crhead = new StandardCodeWriter(outputhead);
 267         crhead.outputline("class "+name+"_state {");
 268         crhead.outputline("public:");
 269         Iterator globals=state.stGlobals.descriptors();
 270         while (globals.hasNext()) {
 271             VarDescriptor vd=(VarDescriptor) globals.next();
 272             crhead.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+";");
 273         }
 274         crhead.outputline("void computesizes(int *,int **);");
 275         crhead.outputline("void recomputesizes();");
 276     }
 277
 278     private void generate_computesizes() {
 279         int max=TypeDescriptor.counter;
 280         TypeDescriptor[] tdarray=new TypeDescriptor[max];
 281         for(Iterator it=state.stTypes.descriptors();it.hasNext();) {
 282             TypeDescriptor ttd=(TypeDescriptor)it.next();
 283             tdarray[ttd.getId()]=ttd;
 284         }
 285         CodeWriter cr=new StandardCodeWriter(outputaux);
 286         cr.outputline("void "+name+"_state::computesizes(int *sizearray,int **numele) {");
 287         for(int i=0;i<max;i++) {
 288             TypeDescriptor td=tdarray[i];
 289             Expr size=td.getSizeExpr();
 290             VarDescriptor vd=VarDescriptor.makeNew("size");
 291             size.generate(cr,vd);
 292             cr.outputline("sizearray["+i+"]="+vd.getSafeSymbol()+";");
 293         }
 294         for(int i=0;i<max;i++) {
 295             TypeDescriptor td=tdarray[i];
 296             if (td instanceof StructureTypeDescriptor) {
 297                 StructureTypeDescriptor std=(StructureTypeDescriptor) td;
 298                 for(int j=0;j<std.fieldlist.size();j++) {
 299                     FieldDescriptor fd=(FieldDescriptor)std.fieldlist.get(j);
 300                     if (fd instanceof ArrayDescriptor) {
 301                         ArrayDescriptor ad=(ArrayDescriptor)fd;
 302                         Expr index=ad.getIndexBound();
 303                         VarDescriptor vd=VarDescriptor.makeNew("index");
 304                         index.generate(cr,vd);
 305                         cr.outputline("numele["+i+"]["+j+"]="+vd.getSafeSymbol()+";");
 306                     }
 307                 }
 308             }
 309         }
 310         cr.outputline("}");
 311     }
 312
 313     private void generate_recomputesizes() {
 314         int max=TypeDescriptor.counter;
 315         TypeDescriptor[] tdarray=new TypeDescriptor[max];
 316         for(Iterator it=state.stTypes.descriptors();it.hasNext();) {
 317             TypeDescriptor ttd=(TypeDescriptor)it.next();
 318             tdarray[ttd.getId()]=ttd;
 319         }
 320         CodeWriter cr=new StandardCodeWriter(outputaux);
 321         cr.outputline("void "+name+"_state::recomputesizes() {");
 322         for(int i=0;i<max;i++) {
 323             TypeDescriptor td=tdarray[i];
 324             Expr size=td.getSizeExpr();
 325             VarDescriptor vd=VarDescriptor.makeNew("size");
 326             size.generate(cr,vd);
 327         }
 328         for(int i=0;i<max;i++) {
 329             TypeDescriptor td=tdarray[i];
 330             if (td instanceof StructureTypeDescriptor) {
 331                 StructureTypeDescriptor std=(StructureTypeDescriptor) td;
 332                 for(int j=0;j<std.fieldlist.size();j++) {
 333                     FieldDescriptor fd=(FieldDescriptor)std.fieldlist.get(j);
 334                     if (fd instanceof ArrayDescriptor) {
 335                         ArrayDescriptor ad=(ArrayDescriptor)fd;
 336                         Expr index=ad.getIndexBound();
 337                         VarDescriptor vd=VarDescriptor.makeNew("index");
 338                         index.generate(cr,vd);
 339                     }
 340                 }
 341             }
 342         }
 343         cr.outputline("}");
 344     }
 345
 346
 347     private void generate_hashtables() {
 348         CodeWriter craux = new StandardCodeWriter(outputaux);
 349         CodeWriter crhead = new StandardCodeWriter(outputhead);
 350         crhead.outputline("#ifndef "+name+"_h");
 351         crhead.outputline("#define "+name+"_h");
 352         crhead.outputline("#include \"SimpleHash.h\"");
 353         crhead.outputline("extern \"C\" {");
 354         crhead.outputline("#include \"instrument.h\"");
 355         crhead.outputline("}");
 356         crhead.outputline("#include <stdio.h>");
 357         crhead.outputline("#include <stdlib.h>");
 358         crhead.outputline("class "+name+" {");
 359         crhead.outputline("public:");
 360         crhead.outputline(name+"();");
 361         crhead.outputline("~"+name+"();");
 362         craux.outputline("#include \""+headername+"\"");
 363         craux.outputline("#include \"size.h\"");
 364
 365         craux.outputline(name+"::"+name+"() {");
 366         craux.outputline("// creating hashtables ");
 367
 368         /* build sets */
 369         Iterator sets = state.stSets.descriptors();
 370
 371         /* first pass create all the hash tables */
 372         while (sets.hasNext()) {
 373             SetDescriptor set = (SetDescriptor) sets.next();
 374             crhead.outputline("SimpleHash* " + set.getSafeSymbol() + "_hash;");
 375             craux.outputline(set.getSafeSymbol() + "_hash = new SimpleHash();");
 376         }
 377
 378         /* second pass build relationships between hashtables */
 379         sets = state.stSets.descriptors();
 380
 381         while (sets.hasNext()) {
 382             SetDescriptor set = (SetDescriptor) sets.next();
 383             Iterator subsets = set.subsets();
 384
 385             while (subsets.hasNext()) {
 386                 SetDescriptor subset = (SetDescriptor) subsets.next();
 387                 craux.outputline(subset.getSafeSymbol() + "_hash->addParent(" + set.getSafeSymbol() + "_hash);");
 388             }
 389         }
 390
 391         /* build relations */
 392         Iterator relations = state.stRelations.descriptors();
 393
 394         /* first pass create all the hash tables */
 395         while (relations.hasNext()) {
 396             RelationDescriptor relation = (RelationDescriptor) relations.next();
 397
 398             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 399                 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hash;");
 400                 craux.outputline(relation.getSafeSymbol() + "_hash = new SimpleHash();");
 401             }
 402
 403             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 404                 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hashinv;");
 405                 craux.outputline(relation.getSafeSymbol() + "_hashinv = new SimpleHash();");
 406             }
 407         }
 408
 409         craux.outputline("}");
 410         crhead.outputline("};");
 411         craux.outputline(name+"::~"+name+"() {");
 412         craux.outputline("// deleting hashtables");
 413
 414         /* build destructor */
 415         sets = state.stSets.descriptors();
 416
 417         /* first pass create all the hash tables */
 418         while (sets.hasNext()) {
 419             SetDescriptor set = (SetDescriptor) sets.next();
 420             craux.outputline("delete "+set.getSafeSymbol() + "_hash;");
 421         }
 422
 423         /* destroy relations */
 424         relations = state.stRelations.descriptors();
 425
 426         /* first pass create all the hash tables */
 427         while (relations.hasNext()) {
 428             RelationDescriptor relation = (RelationDescriptor) relations.next();
 429
 430             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 431                 craux.outputline("delete "+relation.getSafeSymbol() + "_hash;");
 432             }
 433
 434             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 435                 craux.outputline("delete " + relation.getSafeSymbol() + "_hashinv;");
 436             }
 437         }
 438         craux.outputline("}");
 439     }
 440
 441     private void generate_start() {
 442         CodeWriter crhead = new StandardCodeWriter(outputhead);
 443         CodeWriter craux = new StandardCodeWriter(outputaux);
 444         oldmodel=VarDescriptor.makeNew("oldmodel");
 445         newmodel=VarDescriptor.makeNew("newmodel");
 446         worklist=VarDescriptor.makeNew("worklist");
 447         goodflag=VarDescriptor.makeNew("goodflag");
 448         repairtable=VarDescriptor.makeNew("repairtable");
 449         crhead.outputline("void doanalysis();");
 450         craux.outputline("void "+name +"_state::doanalysis()");
 451         craux.startblock();
 452         craux.outputline("int highmark;");
 453         craux.outputline("initializestack(&highmark);");
 454         craux.outputline("typeobject *typeobject1=gettypeobject();");
 455         craux.outputline("typeobject1->computesizes(this);");
 456         craux.outputline("recomputesizes();");
 457         craux.outputline(name+ " * "+oldmodel.getSafeSymbol()+"=0;");
 458         craux.outputline("WorkList * "+worklist.getSafeSymbol()+" = new WorkList();");
 459         craux.outputline("RepairHash * "+repairtable.getSafeSymbol()+"=0;");
 460         craux.outputline("while (1)");
 461         craux.startblock();
 462         craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
 463     }
 464
 465     private void generate_teardown() {
 466         CodeWriter cr = new StandardCodeWriter(outputaux);
 467         cr.endblock();
 468     }
 469
 470     Set ruleset=null;
 471     private void generate_rules() {
 472         /* first we must sort the rules */
 473         RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 474         SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 475         System.out.println("SCC="+(mrd.numSCC()-1));
 476         for(int sccindex=0;sccindex<mrd.numSCC();sccindex++) {
 477             ruleset=mrd.getSCC(sccindex);
 478             boolean needworklist=mrd.hasCycle(sccindex);
 479
 480             if (!needworklist) {
 481                 Iterator iterator_rs = ruleset.iterator();
 482                 while (iterator_rs.hasNext()) {
 483                     Rule rule = (Rule) iterator_rs.next();
 484                     {
 485                         final SymbolTable st = rule.getSymbolTable();
 486                         CodeWriter cr = new StandardCodeWriter(outputaux) {
 487                                 public SymbolTable getSymbolTable() { return st; }
 488                             };
 489                         cr.outputline("// build " +escape(rule.toString()));
 490                         cr.startblock();
 491                         cr.outputline("int maybe=0;");
 492                         ListIterator quantifiers = rule.quantifiers();
 493                         while (quantifiers.hasNext()) {
 494                             Quantifier quantifier = (Quantifier) quantifiers.next();
 495                             quantifier.generate_open(cr);
 496                         }
 497
 498                         /* pretty print! */
 499                         cr.output("//");
 500                         rule.getGuardExpr().prettyPrint(cr);
 501                         cr.outputline("");
 502
 503                         /* now we have to generate the guard test */
 504                         VarDescriptor guardval = VarDescriptor.makeNew();
 505                         rule.getGuardExpr().generate(cr, guardval);
 506                         cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 507                         cr.startblock();
 508
 509                         /* now we have to generate the inclusion code */
 510                         currentrule=rule;
 511                         rule.getInclusion().generate(cr);
 512                         cr.endblock();
 513                         while (quantifiers.hasPrevious()) {
 514                             Quantifier quantifier = (Quantifier) quantifiers.previous();
 515                             cr.endblock();
 516                         }
 517                         cr.endblock();
 518                         cr.outputline("");
 519                         cr.outputline("");
 520                     }
 521                 }
 522             } else {
 523                 CodeWriter cr2 = new StandardCodeWriter(outputaux);
 524
 525                 for(Iterator initialworklist=ruleset.iterator();initialworklist.hasNext();) {
 526                     /** Construct initial worklist set */
 527                     Rule rule=(Rule)initialworklist.next();
 528                     cr2.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
 529                 }
 530
 531                 cr2.outputline("while ("+worklist.getSafeSymbol()+"->hasMoreElements())");
 532                 cr2.startblock();
 533                 VarDescriptor idvar=VarDescriptor.makeNew("id");
 534                 cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
 535
 536                 String elseladder = "if";
 537
 538                 Iterator iterator_rules = ruleset.iterator();
 539                 while (iterator_rules.hasNext()) {
 540
 541                     Rule rule = (Rule) iterator_rules.next();
 542                     int dispatchid = rule.getNum();
 543
 544                     {
 545                         final SymbolTable st = rule.getSymbolTable();
 546                         CodeWriter cr = new StandardCodeWriter(outputaux) {
 547                                 public SymbolTable getSymbolTable() { return st; }
 548                             };
 549
 550                         cr.indent();
 551                         cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
 552                         cr.startblock();
 553                         cr.outputline("int maybe=0;");
 554                         VarDescriptor typevar=VarDescriptor.makeNew("type");
 555                         VarDescriptor leftvar=VarDescriptor.makeNew("left");
 556                         VarDescriptor rightvar=VarDescriptor.makeNew("right");
 557                         cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
 558                         cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
 559                         cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
 560                         cr.outputline("// build " +escape(rule.toString()));
 561
 562
 563                         for (int j=0;j<rule.numQuantifiers();j++) {
 564                             Quantifier quantifier = rule.getQuantifier(j);
 565                             quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
 566                         }
 567
 568                         /* pretty print! */
 569                         cr.output("//");
 570
 571                         rule.getGuardExpr().prettyPrint(cr);
 572                         cr.outputline("");
 573
 574                         /* now we have to generate the guard test */
 575
 576                         VarDescriptor guardval = VarDescriptor.makeNew();
 577                         rule.getGuardExpr().generate(cr, guardval);
 578
 579                         cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 580                         cr.startblock();
 581
 582                         /* now we have to generate the inclusion code */
 583                         currentrule=rule;
 584                         rule.getInclusion().generate(cr);
 585                         cr.endblock();
 586
 587                         for (int j=0;j<rule.numQuantifiers();j++) {
 588                             cr.endblock();
 589                         }
 590
 591                         // close startblocks generated by DotExpr memory checks
 592                         //DotExpr.generate_memory_endblocks(cr);
 593
 594                         cr.endblock(); // end else-if WORKLIST ladder
 595
 596                         elseladder = "else if";
 597                     }
 598                 }
 599                 cr2.outputline("else");
 600                 cr2.startblock();
 601                 cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
 602                 cr2.outputline("exit(1);");
 603                 cr2.endblock();
 604                 // end block created for worklist
 605                 cr2.outputline(worklist.getSafeSymbol()+"->pop();");
 606                 cr2.endblock();
 607             }
 608         }
 609     }
 610
 611     public static String escape(String s) {
 612         String newstring="";
 613         for(int i=0;i<s.length();i++) {
 614             char c=s.charAt(i);
 615             if (c=='"')
 616                 newstring+="\"";
 617             else
 618                 newstring+=c;
 619         }
 620         return newstring;
 621     }
 622
 623     private void generate_checks() {
 624
 625         /* do constraint checks */
 626         Vector constraints = state.vConstraints;
 627
 628         for (int i = 0; i < constraints.size(); i++) {
 629             Constraint constraint = (Constraint) constraints.elementAt(i);
 630
 631             {
 632                 final SymbolTable st = constraint.getSymbolTable();
 633                 CodeWriter cr = new StandardCodeWriter(outputaux) {
 634                         public SymbolTable getSymbolTable() { return st; }
 635                     };
 636                 cr.outputline("// checking " + escape(constraint.toString()));
 637                 cr.startblock();
 638
 639                 ListIterator quantifiers = constraint.quantifiers();
 640
 641                 while (quantifiers.hasNext()) {
 642                     Quantifier quantifier = (Quantifier) quantifiers.next();
 643                     quantifier.generate_open(cr);
 644                 }
 645
 646                 cr.outputline("int maybe = 0;");
 647
 648                 /* now we have to generate the guard test */
 649
 650                 VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
 651                 constraint.getLogicStatement().generate(cr, constraintboolean);
 652
 653                 cr.outputline("if (maybe)");
 654                 cr.startblock();
 655                 cr.outputline("printf(\"maybe fail " +  escape(constraint.toString()) + ". \\n\");");
 656                 cr.outputline("exit(1);");
 657                 cr.endblock();
 658
 659                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
 660                 cr.startblock();
 661                 if (!Compiler.REPAIR)
 662                     cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \\n\");");
 663                 else {
 664                 /* Do repairs */
 665                 /* Build new repair table */
 666                 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 667                 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
 668                 cr.outputline(repairtable.getSafeSymbol()+"=new RepairHash();");
 669
 670
 671                 /* Compute cost of each repair */
 672                 VarDescriptor mincost=VarDescriptor.makeNew("mincost");
 673                 VarDescriptor mincostindex=VarDescriptor.makeNew("mincostindex");
 674                 DNFConstraint dnfconst=constraint.dnfconstraint;
 675                 if (dnfconst.size()<=1) {
 676                     cr.outputline("int "+mincostindex.getSafeSymbol()+"=0;");
 677                 }
 678                 if (dnfconst.size()>1) {
 679                     cr.outputline("int "+mincostindex.getSafeSymbol()+";");
 680                     boolean first=true;
 681                     for(int j=0;j<dnfconst.size();j++) {
 682                         Conjunction conj=dnfconst.get(j);
 683                         GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
 684                         if (removed.contains(gn))
 685                             continue;
 686
 687                         VarDescriptor costvar;
 688                         if (first) {
 689                             costvar=mincost;
 690                         } else
 691                             costvar=VarDescriptor.makeNew("cost");
 692                         for(int k=0;k<conj.size();k++) {
 693                             DNFPredicate dpred=conj.get(k);
 694                             Predicate p=dpred.getPredicate();
 695                             boolean negate=dpred.isNegated();
 696                             VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 697                             p.generate(cr,predvalue);
 698                             if (negate)
 699                                 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 700                             else
 701                                 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 702                             if (k==0)
 703                                 cr.outputline("int "+costvar.getSafeSymbol()+"="+cost.getCost(dpred)+";");
 704                             else
 705                                 cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
 706                         }
 707
 708                         if(!first) {
 709                             cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
 710                             cr.startblock();
 711                             cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
 712                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
 713                             cr.endblock();
 714                         } else
 715                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
 716                         first=false;
 717                     }
 718                 }
 719                 cr.outputline("switch("+mincostindex.getSafeSymbol()+") {");
 720                 for(int j=0;j<dnfconst.size();j++) {
 721                     Conjunction conj=dnfconst.get(j);
 722                     GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
 723                     if (removed.contains(gn))
 724                         continue;
 725                     cr.outputline("case "+j+":");
 726                     for(int k=0;k<conj.size();k++) {
 727                         DNFPredicate dpred=conj.get(k);
 728                         Predicate p=dpred.getPredicate();
 729                         boolean negate=dpred.isNegated();
 730                         VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 731                         p.generate(cr,predvalue);
 732                         if (negate)
 733                             cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 734                         else
 735                             cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 736                         cr.startblock();
 737                         if (p instanceof InclusionPredicate)
 738                             generateinclusionrepair(conj,dpred, cr);
 739                         else if (p instanceof ExprPredicate) {
 740                             ExprPredicate ep=(ExprPredicate)p;
 741                             if (ep.getType()==ExprPredicate.SIZE)
 742                                 generatesizerepair(conj,dpred,cr);
 743                             else if (ep.getType()==ExprPredicate.COMPARISON)
 744                                 generatecomparisonrepair(conj,dpred,cr);
 745                         } else throw new Error("Unrecognized Predicate");
 746                         cr.endblock();
 747                     }
 748                     /* Update model */
 749                     cr.outputline("break;");
 750                 }
 751                 cr.outputline("}");
 752
 753                 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 754                 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 755                 cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
 756                 cr.outputline("goto rebuild;");  /* Rebuild model and all */
 757                 }
 758                 cr.endblock();
 759
 760                 while (quantifiers.hasPrevious()) {
 761                     Quantifier quantifier = (Quantifier) quantifiers.previous();
 762                     cr.endblock();
 763                 }
 764                 cr.endblock();
 765                 cr.outputline("");
 766                 cr.outputline("");
 767             }
 768         }
 769         CodeWriter cr = new StandardCodeWriter(outputaux);
 770         cr.startblock();
 771         cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 772         cr.outputline("delete "+repairtable.getSafeSymbol()+";");
 773         cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
 774         cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
 775         cr.outputline("delete "+newmodel.getSafeSymbol()+";");
 776         cr.outputline("delete "+worklist.getSafeSymbol()+";");
 777         cr.outputline("resettypemap();");
 778         cr.outputline("break;");
 779         cr.endblock();
 780         cr.outputline("rebuild:");
 781         cr.outputline(";");
 782
 783     }
 784
 785     private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
 786         MultUpdateNode mun=null;
 787         GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
 788         for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
 789             GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
 790             TermNode tn2=(TermNode)gn2.getOwner();
 791             if (tn2.getType()==TermNode.ABSTRACT) {
 792                 AbstractRepair ar=tn2.getAbstract();
 793                 if (((repairtype==-1)||(ar.getType()==repairtype))&&
 794                     ar.getPredicate()==dpred) {
 795                     for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
 796                         GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
 797                         if (!removed.contains(gn3)) {
 798                             TermNode tn3=(TermNode)gn3.getOwner();
 799                             if (tn3.getType()==TermNode.UPDATE) {
 800                                 mun=tn3.getUpdate();
 801                                 break;
 802                             }
 803                         }
 804                     }
 805                 }
 806             }
 807         }
 808         return mun;
 809     }
 810
 811     /** Generates abstract (and concrete) repair for a comparison */
 812
 813     private void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
 814         MultUpdateNode munmodify=getmultupdatenode(conj,dpred,AbstractRepair.MODIFYRELATION);
 815         MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
 816         MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
 817         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 818         RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
 819         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
 820         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
 821         boolean inverted=ep.inverted();
 822         boolean negated=dpred.isNegated();
 823         OpExpr expr=(OpExpr)ep.expr;
 824         Opcode opcode=expr.getOpcode();
 825         VarDescriptor leftside=VarDescriptor.makeNew("leftside");
 826         VarDescriptor rightside=VarDescriptor.makeNew("rightside");
 827         VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
 828         if (!inverted) {
 829             expr.getLeftExpr().generate(cr,leftside);
 830             expr.getRightExpr().generate(cr,newvalue);
 831             cr.outputline(rd.getRange().getType().getGenerateType().getSafeSymbol()+" "+rightside.getSafeSymbol()+";");
 832             cr.outputline(rd.getSafeSymbol()+"_hash->get("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 833         } else {
 834             expr.getLeftExpr().generate(cr,rightside);
 835             expr.getRightExpr().generate(cr,newvalue);
 836             cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
 837             cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+leftside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 838         }
 839         if (negated)
 840             if (opcode==Opcode.GT) {
 841                 opcode=Opcode.LE;
 842             } else if (opcode==Opcode.GE) {
 843                 opcode=Opcode.LT;
 844             } else if (opcode==Opcode.LT) {
 845                 opcode=Opcode.GE;
 846             } else if (opcode==Opcode.LE) {
 847                 opcode=Opcode.GT;
 848             } else if (opcode==Opcode.EQ) {
 849                 opcode=Opcode.NE;
 850             } else if (opcode==Opcode.NE) {
 851                 opcode=Opcode.EQ;
 852             } else {
 853                 throw new Error("Unrecognized Opcode");
 854             }
 855
 856         if (opcode==Opcode.GT) {
 857             cr.outputline(newvalue.getSafeSymbol()+"++;");
 858         } else if (opcode==Opcode.GE) {
 859             /* Equal */
 860         } else if (opcode==Opcode.LT) {
 861             cr.outputline(newvalue.getSafeSymbol()+"--;");
 862         } else if (opcode==Opcode.LE) {
 863             /* Equal */
 864         } else if (opcode==Opcode.EQ) {
 865             /* Equal */
 866         } else if (opcode==Opcode.NE) {
 867             cr.outputline(newvalue.getSafeSymbol()+"++;");
 868         } else {
 869             throw new Error("Unrecognized Opcode");
 870         }
 871         /* Do abstract repairs */
 872         if (usageimage) {
 873             cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 874             if (!inverted) {
 875                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 876             } else {
 877                 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 878             }
 879         }
 880         if (usageinvimage) {
 881             cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 882             if (!inverted) {
 883                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
 884             } else {
 885                 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 886             }
 887         }
 888         /* Do concrete repairs */
 889         if (munmodify!=null) {
 890             for(int i=0;i<state.vRules.size();i++) {
 891                 Rule r=(Rule)state.vRules.get(i);
 892                 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
 893                     for(int j=0;j<munmodify.numUpdates();j++) {
 894                         UpdateNode un=munmodify.getUpdate(i);
 895                         if (un.getRule()==r) {
 896                             /* Update for rule r */
 897                             String name=(String)updatenames.get(un);
 898                             cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+","+newvalue.getSafeSymbol()+");");
 899                         }
 900                     }
 901                 }
 902             }
 903
 904         } else {
 905             /* Start with scheduling removal */
 906             for(int i=0;i<state.vRules.size();i++) {
 907                 Rule r=(Rule)state.vRules.get(i);
 908                 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
 909                     for(int j=0;j<munremove.numUpdates();j++) {
 910                         UpdateNode un=munremove.getUpdate(i);
 911                         if (un.getRule()==r) {
 912                             /* Update for rule r */
 913                             String name=(String)updatenames.get(un);
 914                             cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
 915                         }
 916                     }
 917                 }
 918             }
 919             /* Now do addition */
 920             UpdateNode un=munadd.getUpdate(0);
 921             String name=(String)updatenames.get(un);
 922             if (!inverted) {
 923                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
 924             } else {
 925                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
 926             }
 927         }
 928     }
 929
 930     public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {
 931         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
 932         OpExpr expr=(OpExpr)ep.expr;
 933         Opcode opcode=expr.getOpcode();
 934         {
 935             boolean negated=dpred.isNegated();
 936             if (negated)
 937                 if (opcode==Opcode.GT) {
 938                     opcode=Opcode.LE;
 939                 } else if (opcode==Opcode.GE) {
 940                     opcode=Opcode.LT;
 941                 } else if (opcode==Opcode.LT) {
 942                     opcode=Opcode.GE;
 943                 } else if (opcode==Opcode.LE) {
 944                     opcode=Opcode.GT;
 945                 } else if (opcode==Opcode.EQ) {
 946                     opcode=Opcode.NE;
 947                 } else if (opcode==Opcode.NE) {
 948                     opcode=Opcode.EQ;
 949                 } else {
 950                     throw new Error("Unrecognized Opcode");
 951                 }
 952         }
 953         MultUpdateNode munremove;
 954
 955         MultUpdateNode munadd;
 956         if (ep.getDescriptor() instanceof RelationDescriptor) {
 957             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
 958             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
 959         } else {
 960             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
 961             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
 962         }
 963         int size=ep.leftsize();
 964         VarDescriptor sizevar=VarDescriptor.makeNew("size");
 965         ((OpExpr)expr).left.generate(cr, sizevar);
 966         VarDescriptor change=VarDescriptor.makeNew("change");
 967         cr.outputline("int "+change.getSafeSymbol()+";");
 968         boolean generateadd=false;
 969         boolean generateremove=false;
 970         if (opcode==Opcode.GT) {
 971             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
 972             generateadd=true;
 973             generateremove=false;
 974         } else if (opcode==Opcode.GE) {
 975             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 976             generateadd=true;
 977             generateremove=false;
 978         } else if (opcode==Opcode.LT) {
 979             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
 980             generateadd=false;
 981             generateremove=true;
 982         } else if (opcode==Opcode.LE) {
 983             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 984             generateadd=false;
 985             generateremove=true;
 986         } else if (opcode==Opcode.EQ) {
 987             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
 988             if (size==0)
 989                 generateadd=false;
 990             else
 991                 generateadd=true;
 992             generateremove=true;
 993         } else if (opcode==Opcode.NE) {
 994             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
 995             generateadd=true;
 996             generateremove=false;
 997         } else {
 998             throw new Error("Unrecognized Opcode");
 999         }
1000         Descriptor d=ep.getDescriptor();
1001         if (generateremove) {
1002             cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
1003             cr.startblock();
1004             /* Find element to remove */
1005             VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
1006             VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
1007             if (d instanceof RelationDescriptor) {
1008                 if (ep.inverted()) {
1009                     rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
1010                     cr.outputline("int "+leftvar.getSafeSymbol()+";");
1011                     cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1012                 } else {
1013                     leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
1014                     cr.outputline("int "+rightvar.getSafeSymbol()+"=0;");
1015                     cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1016                 }
1017             } else {
1018                 cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
1019             }
1020             /* Generate abstract remove instruction */
1021             if (d instanceof RelationDescriptor) {
1022                 RelationDescriptor rd=(RelationDescriptor) d;
1023                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1024                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1025                 if (usageimage)
1026                     cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1027                 if (usageinvimage)
1028                     cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1029             } else {
1030                 cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1031             }
1032             /* Generate concrete remove instruction */
1033             for(int i=0;i<state.vRules.size();i++) {
1034                 Rule r=(Rule)state.vRules.get(i);
1035                 if (r.getInclusion().getTargetDescriptors().contains(d)) {
1036                     for(int j=0;j<munremove.numUpdates();j++) {
1037                         UpdateNode un=munremove.getUpdate(j);
1038                         if (un.getRule()==r) {
1039                                 /* Update for rule rule r */
1040                             String name=(String)updatenames.get(un);
1041                             if (d instanceof RelationDescriptor) {
1042                                 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1043                             } else {
1044                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1045                             }
1046                         }
1047                     }
1048                 }
1049             }
1050             cr.endblock();
1051         }
1052         if (generateadd) {
1053
1054             cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
1055             cr.startblock();
1056             VarDescriptor newobject=VarDescriptor.makeNew("newobject");
1057             if (d instanceof RelationDescriptor) {
1058                 VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)((OpExpr)ep.expr).left).setexpr).vd;
1059                 RelationDescriptor rd=(RelationDescriptor)d;
1060                 if (sources.relsetSource(rd,!ep.inverted())) {
1061                     /* Set Source */
1062                     SetDescriptor sd=sources.relgetSourceSet(rd,!ep.inverted());
1063                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
1064                     cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
1065                     cr.outputline("for("+iterator.getSafeSymbol()+"="+sd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
1066                     cr.startblock();
1067                     if (ep.inverted()) {
1068                         cr.outputline("if !"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+"->key(),"+otherside.getSafeSymbol()+")");
1069                     } else {
1070                         cr.outputline("if !"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+"->key())");
1071                     }
1072                     cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
1073                     cr.outputline(iterator.getSafeSymbol()+"->next();");
1074                     cr.endblock();
1075                 } else if (sources.relallocSource(rd,!ep.inverted())) {
1076                     /* Allocation Source*/
1077                     sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
1078                 } else throw new Error("No source for adding to Relation");
1079                 if (ep.inverted()) {
1080                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1081                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1082                     if (usageimage)
1083                         cr.outputline(rd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1084                     if (usageinvimage)
1085                         cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1086
1087                     UpdateNode un=munadd.getUpdate(0);
1088                     String name=(String)updatenames.get(un);
1089                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1090                 } else {
1091                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1092                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1093                     if (usageimage)
1094                         cr.outputline(rd.getSafeSymbol()+"_hash->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1095                     if (usageinvimage)
1096                         cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1097                     UpdateNode un=munadd.getUpdate(0);
1098                     String name=(String)updatenames.get(un);
1099                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1100                 }
1101             } else {
1102                 SetDescriptor sd=(SetDescriptor)d;
1103                 if (sources.setSource(sd)) {
1104                     /* Set Source */
1105                     /* Set Source */
1106                     SetDescriptor sourcesd=sources.getSourceSet(sd);
1107                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
1108                     cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
1109                     cr.outputline("for("+iterator.getSafeSymbol()+"="+sourcesd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
1110                     cr.startblock();
1111                     cr.outputline("if !"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+"->key())");
1112                     cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
1113                     cr.outputline(iterator.getSafeSymbol()+"->next();");
1114                     cr.endblock();
1115                 } else if (sources.allocSource(sd)) {
1116                     /* Allocation Source*/
1117                     sources.generateSourceAlloc(cr,newobject,sd);
1118                 } else throw new Error("No source for adding to Set");
1119                 cr.outputline(sd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1120                 UpdateNode un=munadd.getUpdate(0);
1121                 String name=(String)updatenames.get(un);
1122                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1123             }
1124             cr.endblock();
1125         }
1126     }
1127
1128     public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
1129         InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate();
1130         boolean negated=dpred.isNegated();
1131         MultUpdateNode mun=getmultupdatenode(conj,dpred,-1);
1132         VarDescriptor leftvar=VarDescriptor.makeNew("left");
1133         ip.expr.generate(cr, leftvar);
1134
1135         if (negated) {
1136             if (ip.setexpr instanceof ImageSetExpr) {
1137                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1138                 VarDescriptor rightvar=ise.getVar();
1139                 boolean inverse=ise.inverted();
1140                 RelationDescriptor rd=ise.getRelation();
1141                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1142                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1143                 if (inverse) {
1144                     if (usageimage)
1145                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1146                     if (usageinvimage)
1147                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1148                 } else {
1149                     if (usageimage)
1150                         cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1151                     if (usageinvimage)
1152                         cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1153                 }
1154                 for(int i=0;i<state.vRules.size();i++) {
1155                     Rule r=(Rule)state.vRules.get(i);
1156                     if (r.getInclusion().getTargetDescriptors().contains(rd)) {
1157                         for(int j=0;j<mun.numUpdates();j++) {
1158                             UpdateNode un=mun.getUpdate(i);
1159                             if (un.getRule()==r) {
1160                                 /* Update for rule rule r */
1161                                 String name=(String)updatenames.get(un);
1162                                 if (inverse) {
1163                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1164                                 } else {
1165                                     cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1166                                 }
1167                             }
1168                         }
1169                     }
1170                 }
1171             } else {
1172                 SetDescriptor sd=ip.setexpr.sd;
1173                 cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1174
1175                 for(int i=0;i<state.vRules.size();i++) {
1176                     Rule r=(Rule)state.vRules.get(i);
1177                     if (r.getInclusion().getTargetDescriptors().contains(sd)) {
1178                         for(int j=0;j<mun.numUpdates();j++) {
1179                             UpdateNode un=mun.getUpdate(i);
1180                             if (un.getRule()==r) {
1181                                 /* Update for rule rule r */
1182                                 String name=(String)updatenames.get(un);
1183                                 cr.outputline(repairtable.getSafeSymbol()+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1184                             }
1185                         }
1186                     }
1187                 }
1188             }
1189         } else {
1190             /* Generate update */
1191             if (ip.setexpr instanceof ImageSetExpr) {
1192                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1193                 VarDescriptor rightvar=ise.getVar();
1194                 boolean inverse=ise.inverted();
1195                 RelationDescriptor rd=ise.getRelation();
1196                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1197                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1198                 if (inverse) {
1199                     if (usageimage)
1200                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1201                     if (usageinvimage)
1202                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1203                 } else {
1204                     if (usageimage)
1205                         cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1206                     if (usageinvimage)
1207                         cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1208                 }
1209                 UpdateNode un=mun.getUpdate(0);
1210                 String name=(String)updatenames.get(un);
1211                 if (inverse) {
1212                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1213                 } else {
1214                     cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1215                 }
1216             } else {
1217                 SetDescriptor sd=ip.setexpr.sd;
1218                 cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1219
1220                 UpdateNode un=mun.getUpdate(0);
1221                 /* Update for rule rule r */
1222                 String name=(String)updatenames.get(un);
1223                 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1224             }
1225         }
1226     }
1227
1228     public static Vector getrulelist(Descriptor d) {
1229         Vector dispatchrules = new Vector();
1230         Vector rules = State.currentState.vRules;
1231
1232         for (int i = 0; i < rules.size(); i++) {
1233             Rule rule = (Rule) rules.elementAt(i);
1234             Set requiredsymbols = rule.getRequiredDescriptors();
1235
1236             // #TBD#: in general this is wrong because these descriptors may contain descriptors
1237             // bound in "in?" expressions which need to be dealt with in a topologically sorted
1238             // fashion...
1239
1240             if (rule.getRequiredDescriptors().contains(d)) {
1241                 dispatchrules.addElement(rule);
1242             }
1243         }
1244         return dispatchrules;
1245     }
1246
1247     private boolean need_compensation(Rule r) {
1248         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1249         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1250             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1251             GraphNode gn2=edge.getTarget();
1252             if (!removed.contains(gn2)) {
1253                 TermNode tn2=(TermNode)gn2.getOwner();
1254                 if (tn2.getType()==TermNode.CONSEQUENCE)
1255                     return false;
1256             }
1257         }
1258         return true;
1259     }
1260
1261     private UpdateNode find_compensation(Rule r) {
1262         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1263         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1264             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1265             GraphNode gn2=edge.getTarget();
1266             if (!removed.contains(gn2)) {
1267                 TermNode tn2=(TermNode)gn2.getOwner();
1268                 if (tn2.getType()==TermNode.UPDATE) {
1269                     MultUpdateNode mun=tn2.getUpdate();
1270                     for(int i=0;i<mun.numUpdates();i++) {
1271                         UpdateNode un=mun.getUpdate(i);
1272                         if (un.getRule()==r)
1273                             return un;
1274                     }
1275                 }
1276             }
1277         }
1278         throw new Error("No Compensation Update could be found");
1279     }
1280
1281     public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
1282         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1283         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1284
1285         if (!(usageinvimage||usageimage)) /* not used at all*/
1286             return;
1287
1288         cr.outputline("// RELATION DISPATCH ");
1289         cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1290         if (usageimage)
1291             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
1292         else
1293             cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
1294         cr.startblock(); {
1295             /* Adding new item */
1296             /* Perform safety checks */
1297             cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1298             cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
1299             cr.startblock(); {
1300                 /* Have update to call into */
1301                 VarDescriptor mdfyptr=VarDescriptor.makeNew("modifyptr");
1302                 cr.outputline("int "+mdfyptr.getSafeSymbol()+"="+repairtable.getSafeSymbol()+"->getrelation2("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1303
1304                 String parttype="";
1305                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1306                     if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1307                         parttype=parttype+", int, int";
1308                     else
1309                         parttype=parttype+", int";
1310                 }
1311                 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1312                 VarDescriptor tmpptr=VarDescriptor.makeNew("tempupdateptr");
1313
1314                 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1315                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1316                     Quantifier q=currentrule.getQuantifier(i);
1317                     if (q instanceof SetQuantifier) {
1318                         SetQuantifier sq=(SetQuantifier) q;
1319                         methodcall+=","+sq.getVar().getSafeSymbol();
1320                     } else if (q instanceof RelationQuantifier) {
1321                         RelationQuantifier rq=(RelationQuantifier) q;
1322                         methodcall+=","+rq.x.getSafeSymbol();
1323                         methodcall+=","+rq.y.getSafeSymbol();
1324                     } else if (q instanceof ForQuantifier) {
1325                         ForQuantifier fq=(ForQuantifier) q;
1326                         methodcall+=","+fq.getVar().getSafeSymbol();
1327                     }
1328                 }
1329
1330
1331
1332                 cr.outputline("void *"+tmpptr.getSafeSymbol()+"=");
1333                 cr.outputline("(void *) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1334                 cr.outputline("if ("+mdfyptr.getSafeSymbol()+")");
1335                 {
1336                     cr.startblock();
1337                     cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+"int,int,int)="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+"int,int,int)) "+tmpptr.getSafeSymbol());
1338                     cr.outputline(methodcall+leftvar+", "+rightvar+", "+mdfyptr.getSafeSymbol() +");");
1339                     cr.endblock();
1340                 }
1341                 cr.outputline("else ");
1342                 {
1343                     cr.startblock();
1344                     cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")="+"(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+tmpptr.getSafeSymbol());
1345                     cr.outputline(methodcall+");");
1346                     cr.endblock();
1347                 }
1348                 cr.outputline("goto rebuild;");
1349             }
1350             cr.endblock();
1351             /* Build standard compensation actions */
1352             if (need_compensation(currentrule)) {
1353                 UpdateNode un=find_compensation(currentrule);
1354                 String name=(String)updatenames.get(un);
1355                 usedupdates.add(un); /* Mark as used */
1356                 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1357                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1358                     Quantifier q=currentrule.getQuantifier(i);
1359                     if (q instanceof SetQuantifier) {
1360                         SetQuantifier sq=(SetQuantifier) q;
1361                         methodcall+=","+sq.getVar().getSafeSymbol();
1362                     } else if (q instanceof RelationQuantifier) {
1363                         RelationQuantifier rq=(RelationQuantifier) q;
1364                         methodcall+=","+rq.x.getSafeSymbol();
1365                         methodcall+=","+rq.y.getSafeSymbol();
1366                     } else if (q instanceof ForQuantifier) {
1367                         ForQuantifier fq=(ForQuantifier) q;
1368                         methodcall+=","+fq.getVar().getSafeSymbol();
1369                     }
1370                 }
1371                 methodcall+=");";
1372                 cr.outputline(methodcall);
1373                 cr.outputline("goto rebuild;");
1374             }
1375         }
1376         cr.endblock();
1377
1378         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1379         cr.outputline("int " + addeditem + ";");
1380         if (rd.testUsage(RelationDescriptor.IMAGE)) {
1381             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar+ ");");
1382         }
1383
1384         if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1385             cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1386         }
1387
1388         cr.outputline("if (" + addeditem + ")");
1389         cr.startblock();
1390
1391         Vector dispatchrules = getrulelist(rd);
1392
1393         Set toremove=new HashSet();
1394         for(int i=0;i<dispatchrules.size();i++) {
1395             Rule r=(Rule)dispatchrules.get(i);
1396             if (!ruleset.contains(r))
1397                 toremove.add(r);
1398         }
1399         dispatchrules.removeAll(toremove);
1400         if (dispatchrules.size() == 0) {
1401             cr.outputline("// nothing to dispatch");
1402             cr.endblock();
1403             return;
1404         }
1405
1406         cr.outputline("if ("+addeditem+")");
1407         cr.startblock();
1408         for(int i = 0; i < dispatchrules.size(); i++) {
1409             Rule rule = (Rule) dispatchrules.elementAt(i);
1410             if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
1411                 /* Guard depends on this relation, so we recomput everything */
1412                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1413             } else {
1414                 for (int j=0;j<rule.numQuantifiers();j++) {
1415                     Quantifier q=rule.getQuantifier(j);
1416                     if (q.getRequiredDescriptors().contains(rd)) {
1417                         /* Generate add */
1418                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1419                     }
1420                 }
1421             }
1422         }
1423         cr.endblock();
1424         cr.endblock();
1425     }
1426
1427
1428     public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1429
1430         cr.outputline("// SET DISPATCH ");
1431
1432         cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1433         cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
1434         cr.startblock(); {
1435             /* Adding new item */
1436             /* Perform safety checks */
1437             cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1438             cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
1439             cr.startblock(); {
1440                 /* Have update to call into */
1441                 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1442                 String parttype="";
1443                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1444                     if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1445                         parttype=parttype+", int, int";
1446                     else
1447                         parttype=parttype+", int";
1448                 }
1449                 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1450                 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getset("+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
1451                 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+
1452                               repairtable.getSafeSymbol();
1453                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1454                     Quantifier q=currentrule.getQuantifier(i);
1455                     if (q instanceof SetQuantifier) {
1456                         SetQuantifier sq=(SetQuantifier) q;
1457                         methodcall+=","+sq.getVar().getSafeSymbol();
1458                     } else if (q instanceof RelationQuantifier) {
1459                         RelationQuantifier rq=(RelationQuantifier) q;
1460                         methodcall+=","+rq.x.getSafeSymbol();
1461                         methodcall+=","+rq.y.getSafeSymbol();
1462                     } else if (q instanceof ForQuantifier) {
1463                         ForQuantifier fq=(ForQuantifier) q;
1464                         methodcall+=","+fq.getVar().getSafeSymbol();
1465                     }
1466                 }
1467                 methodcall+=");";
1468                 cr.outputline(methodcall);
1469                 cr.outputline("goto rebuild;");
1470             }
1471             cr.endblock();
1472             /* Build standard compensation actions */
1473             if (need_compensation(currentrule)) {
1474                 UpdateNode un=find_compensation(currentrule);
1475                 String name=(String)updatenames.get(un);
1476                 usedupdates.add(un); /* Mark as used */
1477
1478                 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
1479                               repairtable.getSafeSymbol();
1480                 for(int i=0;i<currentrule.numQuantifiers();i++) {
1481                     Quantifier q=currentrule.getQuantifier(i);
1482                     if (q instanceof SetQuantifier) {
1483                         SetQuantifier sq=(SetQuantifier) q;
1484                         methodcall+=","+sq.getVar().getSafeSymbol();
1485                     } else if (q instanceof RelationQuantifier) {
1486                         RelationQuantifier rq=(RelationQuantifier) q;
1487                         methodcall+=","+rq.x.getSafeSymbol();
1488                         methodcall+=","+rq.y.getSafeSymbol();
1489                     } else if (q instanceof ForQuantifier) {
1490                         ForQuantifier fq=(ForQuantifier) q;
1491                         methodcall+=","+fq.getVar().getSafeSymbol();
1492                     }
1493                 }
1494                 methodcall+=");";
1495                 cr.outputline(methodcall);
1496                 cr.outputline("goto rebuild;");
1497             }
1498         }
1499         cr.endblock();
1500
1501         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1502         cr.outputline("int " + addeditem + " = 1;");
1503         cr.outputline(addeditem + " = " + sd.getSafeSymbol() + "_hash->add((int)" + setvar +  ", (int)" + setvar + ");");
1504         cr.startblock();
1505         Vector dispatchrules = getrulelist(sd);
1506
1507         Set toremove=new HashSet();
1508         for(int i=0;i<dispatchrules.size();i++) {
1509             Rule r=(Rule)dispatchrules.get(i);
1510             if (!ruleset.contains(r))
1511                 toremove.add(r);
1512         }
1513         dispatchrules.removeAll(toremove);
1514
1515         if (dispatchrules.size() == 0) {
1516             cr.outputline("// nothing to dispatch");
1517             cr.endblock();
1518             return;
1519         }
1520         cr.outputline("if ("+addeditem+")");
1521         cr.startblock();
1522         for(int i = 0; i < dispatchrules.size(); i++) {
1523             Rule rule = (Rule) dispatchrules.elementAt(i);
1524             if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
1525                 /* Guard depends on this relation, so we recompute everything */
1526                 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1527             } else {
1528                 for (int j=0;j<rule.numQuantifiers();j++) {
1529                     Quantifier q=rule.getQuantifier(j);
1530                     if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1531                         /* Generate add */
1532                         cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");
1533                     }
1534                 }
1535             }
1536         }
1537
1538         cr.endblock();
1539         cr.endblock();
1540     }
1541 }