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