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     PrintWrapper outputrepair = null;
  11     PrintWrapper outputaux = null;
  12     PrintWrapper outputhead = null;
  13     public static String name="foo";
  14     public static String postfix="";
  15     String headername;
  16     static VarDescriptor oldmodel=null;
  17     static VarDescriptor newmodel=null;
  18     static VarDescriptor worklist=null;
  19     static VarDescriptor repairtable=null;
  20     static VarDescriptor goodflag=null;
  21     Rule currentrule=null;
  22     Hashtable updatenames;
  23     HashSet usedupdates;
  24     Termination termination;
  25     Set removed;
  26     HashSet togenerate;
  27     static boolean DEBUG=false;
  28     Cost cost;
  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         mrd=ModelRuleDependence.doAnalysis(state);
  44         Repair.repairgenerator=this;
  45     }
  46
  47     private void generatetypechecks(boolean flag) {
  48         if (flag) {
  49             DotExpr.DOTYPECHECKS=true;
  50             VarExpr.DOTYPECHECKS=true;
  51             DotExpr.DONULL=true;
  52             VarExpr.DONULL=true;
  53         } else {
  54             VarExpr.DOTYPECHECKS=false;
  55             DotExpr.DOTYPECHECKS=false;
  56             VarExpr.DONULL=true;
  57             DotExpr.DONULL=true;
  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"+RepairGenerator.name+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 PrintWrapper(new java.io.PrintWriter(outputrepair, true));
  78         this.outputaux = new PrintWrapper(new java.io.PrintWriter(outputaux, true));
  79         this.outputhead = new PrintWrapper(new java.io.PrintWriter(outputhead, true));
  80
  81         headername=st;
  82         name_updates();
  83         generatetypechecks(true);
  84         generate_tokentable();
  85         RelationDescriptor.prefix = "thisvar->";
  86         SetDescriptor.prefix = "thisvar->";
  87
  88         generate_hashtables();
  89         generate_stateobject();
  90
  91
  92         /* Rewrite globals */
  93         CodeWriter craux = new StandardCodeWriter(this.outputaux);
  94         for (Iterator it=this.state.stGlobals.descriptors();it.hasNext();) {
  95             VarDescriptor vd=(VarDescriptor)it.next();
  96             craux.outputline("#define "+vd.getSafeSymbol()+" thisvar->"+vd.getSafeSymbol());
  97         }
  98
  99
 100         generate_call();
 101         generate_start();
 102         generate_rules();
 103         if (!Compiler.REPAIR||Compiler.GENERATEDEBUGPRINT) {
 104             generate_print();
 105         }
 106         generate_checks();
 107         generate_teardown();
 108         CodeWriter crhead = new StandardCodeWriter(this.outputhead);
 109         craux = new StandardCodeWriter(this.outputaux);
 110         craux.outputline("return noerrors;");
 111         craux.emptyBuffer();
 112         craux.endblock();
 113
 114         if (Compiler.GENERATEDEBUGHOOKS) {
 115             crhead.outputline("void debughook();");
 116             craux.outputline("void debughook() {}");
 117         }
 118         generatetypechecks(false);
 119         generate_computesizes();
 120         generatetypechecks(true);
 121         generate_recomputesizes();
 122         generatetypechecks(false);
 123         generate_updates();
 124         StructureGenerator sg=new StructureGenerator(state,this);
 125         sg.buildall();
 126         crhead.outputline("#endif");
 127     }
 128
 129     String ststate="state";
 130     String stmodel="model";
 131     String strepairtable="repairtable";
 132     String stleft="left";
 133     String stright="right";
 134     String stnew="newvalue";
 135
 136     private void generate_updates() {
 137         int count=0;
 138         CodeWriter crhead = new StandardCodeWriter(outputhead);
 139         CodeWriter craux = new StandardCodeWriter(outputaux);
 140         RelationDescriptor.prefix = "model->";
 141         SetDescriptor.prefix = "model->";
 142
 143         /* Rewrite globals */
 144
 145         for (Iterator it=this.state.stGlobals.descriptors();it.hasNext();) {
 146             VarDescriptor vd=(VarDescriptor)it.next();
 147             craux.outputline("#undef "+vd.getSafeSymbol());
 148             craux.outputline("#define "+vd.getSafeSymbol()+" "+ststate+"->"+vd.getSafeSymbol());
 149         }
 150
 151         for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
 152             GraphNode gn=(GraphNode) it.next();
 153             TermNode tn=(TermNode) gn.getOwner();
 154             MultUpdateNode mun=tn.getUpdate();
 155             boolean isrelation=(mun.getDescriptor() instanceof RelationDescriptor);
 156             if (togenerate.contains(gn))
 157             for (int i=0;i<mun.numUpdates();i++) {
 158                 UpdateNode un=mun.getUpdate(i);
 159                 String methodname=(String)updatenames.get(un);
 160
 161                 switch(mun.op) {
 162                 case MultUpdateNode.ADD:
 163                     if (isrelation) {
 164                         crhead.outputline("void "+methodname+"(struct "+name+"_state * " +ststate+",struct "+name+" * "+stmodel+", struct RepairHash * "+strepairtable+", int "+stleft+", int "+stright+");");
 165                         craux.outputline("void "+methodname+"(struct "+name+"_state * "+ ststate+", struct "+name+" * "+stmodel+", struct RepairHash * "+strepairtable+", int "+stleft+", int "+stright+")");
 166                     } else {
 167                         crhead.outputline("void "+methodname+"(struct "+name+"_state * "+ ststate+", struct "+name+" * "+stmodel+", struct RepairHash * "+strepairtable+", int "+stleft+");");
 168                         craux.outputline("void "+methodname+"(struct "+name+"_state * "+ststate+", struct "+name+" * "+stmodel+", struct RepairHash * "+strepairtable+", int "+stleft+")");
 169                     }
 170                     craux.startblock();
 171                     craux.startBuffer();
 172                     craux.addDeclaration("int","maybe");
 173                     craux.outputline("maybe=0;");
 174                     if (Compiler.GENERATEINSTRUMENT)
 175                         craux.outputline("updatecount++;");
 176
 177                     final SymbolTable st = un.getRule().getSymbolTable();
 178                     CodeWriter cr = new StandardCodeWriter(outputaux) {
 179                         public SymbolTable getSymbolTable() { return st; }
 180                     };
 181                     un.generate(cr, false, false, stleft,stright, null,this);
 182                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 183                     craux.emptyBuffer();
 184                     craux.endblock();
 185                     break;
 186                 case MultUpdateNode.REMOVE: {
 187                     Rule r=un.getRule();
 188                     String methodcall="void "+methodname+"(struct "+name+"_state * "+ststate+", struct "+name+" * "+stmodel+", struct RepairHash * "+strepairtable;
 189                     for(int j=0;j<r.numQuantifiers();j++) {
 190                         Quantifier q=r.getQuantifier(j);
 191                         if (q instanceof SetQuantifier) {
 192                             SetQuantifier sq=(SetQuantifier) q;
 193                             methodcall+=","+sq.getVar().getType().getGenerateType().getSafeSymbol()+" "+sq.getVar().getSafeSymbol();
 194                         } else if (q instanceof RelationQuantifier) {
 195                             RelationQuantifier rq=(RelationQuantifier) q;
 196
 197                             methodcall+=","+rq.x.getType().getGenerateType().getSafeSymbol()+" "+rq.x.getSafeSymbol();
 198                             methodcall+=","+rq.y.getType().getGenerateType().getSafeSymbol()+" "+rq.y.getSafeSymbol();
 199                         } else if (q instanceof ForQuantifier) {
 200                             ForQuantifier fq=(ForQuantifier) q;
 201                             methodcall+=",int "+fq.getVar().getSafeSymbol();
 202                         }
 203                     }
 204                     methodcall+=")";
 205                     crhead.outputline(methodcall+";");
 206                     craux.outputline(methodcall);
 207                     craux.startblock();
 208                     craux.startBuffer();
 209                     craux.addDeclaration("int","maybe");
 210                     craux.outputline("maybe=0;");
 211                     if (Compiler.GENERATEINSTRUMENT)
 212                         craux.outputline("updatecount++;");
 213                     final SymbolTable st2 = un.getRule().getSymbolTable();
 214                     CodeWriter cr2 = new StandardCodeWriter(outputaux) {
 215                         public SymbolTable getSymbolTable() { return st2; }
 216                     };
 217                     un.generate(cr2, true, false, null,null, null,this);
 218                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 219                     craux.emptyBuffer();
 220                     craux.endblock();
 221                 }
 222                     break;
 223                 case MultUpdateNode.MODIFY: {
 224                     Rule r=un.getRule();
 225                     String methodcall="void "+methodname+"(struct "+name+"_state * "+ststate+", struct "+name+" * "+stmodel+", struct RepairHash * "+strepairtable;
 226                     for(int j=0;j<r.numQuantifiers();j++) {
 227                         Quantifier q=r.getQuantifier(j);
 228                         if (q instanceof SetQuantifier) {
 229                             SetQuantifier sq=(SetQuantifier) q;
 230                             methodcall+=","+sq.getVar().getType().getGenerateType().getSafeSymbol()+" "+sq.getVar().getSafeSymbol();
 231                         } else if (q instanceof RelationQuantifier) {
 232                             RelationQuantifier rq=(RelationQuantifier) q;
 233
 234                             methodcall+=", "+rq.x.getType().getGenerateType().getSafeSymbol()+" "+rq.x.getSafeSymbol();
 235                             methodcall+=", "+rq.y.getType().getGenerateType().getSafeSymbol()+" "+rq.y.getSafeSymbol();
 236                         } else if (q instanceof ForQuantifier) {
 237                             ForQuantifier fq=(ForQuantifier) q;
 238                             methodcall+=", int "+fq.getVar().getSafeSymbol();
 239                         }
 240                     }
 241                     methodcall+=", int "+stleft+", int "+stright+", int "+stnew;
 242                     methodcall+=")";
 243                     crhead.outputline(methodcall+";");
 244                     craux.outputline(methodcall);
 245                     craux.startblock();
 246                     craux.startBuffer();
 247                     craux.outputline("int maybe=0;");
 248                     if (Compiler.GENERATEINSTRUMENT)
 249                         craux.outputline("updatecount++;");
 250                     final SymbolTable st2 = un.getRule().getSymbolTable();
 251                     CodeWriter cr2 = new StandardCodeWriter(outputaux) {
 252                         public SymbolTable getSymbolTable() { return st2; }
 253                     };
 254                     un.generate(cr2, false, true, stleft, stright, stnew, this);
 255                     craux.outputline("if (maybe) printf(\"REALLY BAD\");");
 256                     craux.emptyBuffer();
 257                     craux.endblock();
 258                 }
 259                     break;
 260
 261                 default:
 262                     throw new Error("Nonimplement Update");
 263                 }
 264             }
 265         }
 266     }
 267
 268     private void generate_call() {
 269         CodeWriter cr = new StandardCodeWriter(outputrepair);
 270         VarDescriptor vdstate=VarDescriptor.makeNew("repairstate");
 271         cr.addDeclaration("struct "+ name+"_state *", vdstate.getSafeSymbol());
 272         cr.outputline(vdstate.getSafeSymbol()+"=allocate"+name+"_state();");
 273         Iterator globals=state.stGlobals.descriptors();
 274         while (globals.hasNext()) {
 275             VarDescriptor vd=(VarDescriptor) globals.next();
 276             cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
 277         }
 278         /* Insert repair here */
 279         cr.outputline("doanalysis"+postfix+"("+vdstate.getSafeSymbol()+");");
 280         globals=state.stGlobals.descriptors();
 281         while (globals.hasNext()) {
 282             VarDescriptor vd=(VarDescriptor) globals.next();
 283             cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";");
 284         }
 285         cr.outputline("free"+name+"_state("+vdstate.getSafeSymbol()+");");
 286     }
 287
 288     private void generate_tokentable() {
 289         CodeWriter cr = new StandardCodeWriter(outputrepair);
 290         Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();
 291
 292         cr.outputline("");
 293         cr.outputline("/* Token values*/");
 294         cr.outputline("");
 295
 296         while (tokens.hasNext()) {
 297             Object token = tokens.next();
 298             cr.outputline("/* " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString()+"*/");
 299         }
 300
 301         cr.outputline("");
 302         cr.outputline("");
 303     }
 304
 305     private void generate_stateobject() {
 306         CodeWriter crhead = new StandardCodeWriter(outputhead);
 307         CodeWriter craux = new StandardCodeWriter(outputaux);
 308         crhead.outputline("struct "+name+"_state {");
 309         Iterator globals=state.stGlobals.descriptors();
 310         while (globals.hasNext()) {
 311             VarDescriptor vd=(VarDescriptor) globals.next();
 312             crhead.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+";");
 313         }
 314         crhead.outputline("};");
 315         crhead.outputline("struct "+name+"_state * allocate"+name+"_state();");
 316         craux.outputline("struct "+name+"_state * allocate"+name+"_state()");
 317         craux.startblock();
 318         craux.outputline("return (struct "+name+"_state *) malloc(sizeof(struct "+name+"_state));");
 319         craux.endblock();
 320
 321         crhead.outputline("void free"+name+"_state(struct "+name+"_state *);");
 322         craux.outputline("void free"+name+"_state(struct "+name+"_state * thisvar)");
 323         craux.startblock();
 324         craux.outputline("free(thisvar);");
 325         craux.endblock();
 326
 327         crhead.outputline("void "+name+"_statecomputesizes(struct "+name+"_state * ,int *,int **);");
 328         crhead.outputline("void "+name+"_staterecomputesizes(struct "+name+"_state *);");
 329     }
 330
 331     private void generate_computesizes() {
 332         int max=TypeDescriptor.counter;
 333         TypeDescriptor[] tdarray=new TypeDescriptor[max];
 334         for(Iterator it=state.stTypes.descriptors();it.hasNext();) {
 335             TypeDescriptor ttd=(TypeDescriptor)it.next();
 336             tdarray[ttd.getId()]=ttd;
 337         }
 338         final SymbolTable st = state.stGlobals;
 339         CodeWriter cr = new StandardCodeWriter(outputaux) {
 340                 public SymbolTable getSymbolTable() { return st; }
 341             };
 342
 343         cr.outputline("void "+name+"_statecomputesizes(struct "+name+"_state * thisvar,int *sizearray,int **numele)");
 344         cr.startblock();
 345         cr.startBuffer();
 346         cr.addDeclaration("int","maybe");
 347         cr.outputline("maybe=0;");
 348         for(int i=0;i<max;i++) {
 349             TypeDescriptor td=tdarray[i];
 350             Expr size=td.getSizeExpr();
 351             VarDescriptor vd=VarDescriptor.makeNew("size");
 352             size.generate(cr,vd);
 353             cr.outputline("sizearray["+i+"]="+vd.getSafeSymbol()+";");
 354         }
 355         for(int i=0;i<max;i++) {
 356             TypeDescriptor td=tdarray[i];
 357             if (td instanceof StructureTypeDescriptor) {
 358                 StructureTypeDescriptor std=(StructureTypeDescriptor) td;
 359                 for(int j=0;j<std.fieldlist.size();j++) {
 360                     FieldDescriptor fd=(FieldDescriptor)std.fieldlist.get(j);
 361                     if (fd instanceof ArrayDescriptor) {
 362                         ArrayDescriptor ad=(ArrayDescriptor)fd;
 363                         Expr index=ad.getIndexBound();
 364                         VarDescriptor vd=VarDescriptor.makeNew("index");
 365                         index.generate(cr,vd);
 366                         cr.outputline("numele["+i+"]["+j+"]="+vd.getSafeSymbol()+";");
 367                     }
 368                 }
 369             }
 370         }
 371         cr.outputline("if (maybe) printf(\"BAD ERROR\");");
 372         cr.emptyBuffer();
 373         cr.endblock();
 374     }
 375
 376     private void generate_recomputesizes() {
 377         int max=TypeDescriptor.counter;
 378         TypeDescriptor[] tdarray=new TypeDescriptor[max];
 379         for(Iterator it=state.stTypes.descriptors();it.hasNext();) {
 380             TypeDescriptor ttd=(TypeDescriptor)it.next();
 381             tdarray[ttd.getId()]=ttd;
 382         }
 383         final SymbolTable st = state.stGlobals;
 384         CodeWriter cr = new StandardCodeWriter(outputaux) {
 385                 public SymbolTable getSymbolTable() { return st; }
 386             };
 387         cr.outputline("void "+name+"_staterecomputesizes(struct "+name+"_state * thisvar)");
 388         cr.startblock();
 389         cr.startBuffer();
 390         cr.addDeclaration("int","maybe");
 391         cr.outputline("maybe=0;");
 392         for(int i=0;i<max;i++) {
 393             TypeDescriptor td=tdarray[i];
 394             Expr size=td.getSizeExpr();
 395             VarDescriptor vd=VarDescriptor.makeNew("size");
 396             size.generate(cr,vd);
 397         }
 398         for(int i=0;i<max;i++) {
 399             TypeDescriptor td=tdarray[i];
 400             if (td instanceof StructureTypeDescriptor) {
 401                 StructureTypeDescriptor std=(StructureTypeDescriptor) td;
 402                 for(int j=0;j<std.fieldlist.size();j++) {
 403                     FieldDescriptor fd=(FieldDescriptor)std.fieldlist.get(j);
 404                     if (fd instanceof ArrayDescriptor) {
 405                         ArrayDescriptor ad=(ArrayDescriptor)fd;
 406                         Expr index=ad.getIndexBound();
 407                         VarDescriptor vd=VarDescriptor.makeNew("index");
 408                         index.generate(cr,vd);
 409                     }
 410                 }
 411             }
 412         }
 413         cr.outputline("if (maybe) printf(\"BAD ERROR\");");
 414         cr.emptyBuffer();
 415         cr.endblock();
 416     }
 417
 418
 419     private void generate_hashtables() {
 420         CodeWriter craux = new StandardCodeWriter(outputaux);
 421         CodeWriter crhead = new StandardCodeWriter(outputhead);
 422         crhead.outputline("#ifndef "+name+"_h");
 423         crhead.outputline("#define "+name+"_h");
 424         crhead.outputline("#include \"SimpleHash.h\"");
 425         crhead.outputline("#include \"instrument.h\"");
 426         crhead.outputline("#include <stdio.h>");
 427         crhead.outputline("#include <stdlib.h>");
 428         crhead.outputline("struct "+name+" * allocate"+name+"();");
 429         crhead.outputline("void free"+name+"(struct "+name+" *);");
 430         crhead.outputline("struct "+name+" {");
 431         craux.outputline("#include \""+headername+"\"");
 432         craux.outputline("#include \"size.h\"");
 433         if (Compiler.TIME) {
 434             craux.outputline("#include <sys/time.h>");
 435         }
 436         if (Compiler.ALLOCATECPLUSPLUS) {
 437             for(Iterator it=state.stTypes.descriptors();it.hasNext();) {
 438                 TypeDescriptor td=(TypeDescriptor)it.next();
 439                 if (td instanceof StructureTypeDescriptor) {
 440                     if (((StructureTypeDescriptor)td).size()>0) {
 441                         FieldDescriptor fd=((StructureTypeDescriptor)td).get(0);
 442                         if (fd.getSymbol().startsWith("_vptr_")) {
 443                             String vtable="_ZTV";
 444                             vtable+=td.getSymbol().length();
 445                             vtable+=td.getSymbol();
 446                             craux.outputline("extern void * "+vtable+";");
 447                         }
 448                     }
 449                 }
 450             }
 451         }
 452         craux.outputline("struct "+ name+"* allocate"+name+"()");
 453         craux.startblock();
 454         craux.outputline("/* creating hashtables */");
 455
 456         /* build sets */
 457         Iterator sets = state.stSets.descriptors();
 458         craux.addDeclaration("struct "+name+"*", "thisvar");
 459         craux.outputline("thisvar=(struct "+name+"*) malloc(sizeof(struct "+name+"));");
 460
 461         /* first pass create all the hash tables */
 462         while (sets.hasNext()) {
 463             SetDescriptor set = (SetDescriptor) sets.next();
 464             crhead.outputline("struct SimpleHash* " + set.getJustSafeSymbol() + "_hash;");
 465             craux.outputline(set.getSafeSymbol() + "_hash = noargallocateSimpleHash();");
 466         }
 467
 468         /* second pass build relationships between hashtables */
 469         sets = state.stSets.descriptors();
 470
 471         while (sets.hasNext()) {
 472             SetDescriptor set = (SetDescriptor) sets.next();
 473             Iterator subsets = set.subsets();
 474
 475             while (subsets.hasNext()) {
 476                 SetDescriptor subset = (SetDescriptor) subsets.next();
 477                 craux.outputline("SimpleHashaddParent("+subset.getSafeSymbol() +"_hash ,"+ set.getSafeSymbol() + "_hash);");
 478             }
 479         }
 480
 481         /* build relations */
 482         Iterator relations = state.stRelations.descriptors();
 483
 484         /* first pass create all the hash tables */
 485         while (relations.hasNext()) {
 486             RelationDescriptor relation = (RelationDescriptor) relations.next();
 487
 488             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 489                 crhead.outputline("struct SimpleHash* " + relation.getJustSafeSymbol() + "_hash;");
 490                 craux.outputline(relation.getSafeSymbol() + "_hash = noargallocateSimpleHash();");
 491             }
 492
 493             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 494                 crhead.outputline("struct SimpleHash* " + relation.getJustSafeSymbol() + "_hashinv;");
 495                 craux.outputline(relation.getSafeSymbol() + "_hashinv = noargallocateSimpleHash();");
 496             }
 497         }
 498         craux.outputline("return thisvar;");
 499         craux.endblock();
 500         crhead.outputline("};");
 501         craux.outputline("void free"+name+"(struct "+ name +"* thisvar)");
 502         craux.startblock();
 503         craux.outputline("/* deleting hashtables */");
 504
 505         /* build destructor */
 506         sets = state.stSets.descriptors();
 507
 508         /* first pass create all the hash tables */
 509         while (sets.hasNext()) {
 510             SetDescriptor set = (SetDescriptor) sets.next();
 511             craux.outputline("freeSimpleHash("+set.getSafeSymbol() + "_hash);");
 512         }
 513
 514         /* destroy relations */
 515         relations = state.stRelations.descriptors();
 516
 517         /* first pass create all the hash tables */
 518         while (relations.hasNext()) {
 519             RelationDescriptor relation = (RelationDescriptor) relations.next();
 520
 521             if (relation.testUsage(RelationDescriptor.IMAGE)) {
 522                 craux.outputline("freeSimpleHash("+relation.getSafeSymbol() + "_hash);");
 523             }
 524
 525             if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
 526                 craux.outputline("freeSimpleHash(" + relation.getSafeSymbol() + "_hashinv);");
 527             }
 528         }
 529         craux.outputline("free(thisvar);");
 530         craux.endblock();
 531     }
 532
 533     private void generate_start() {
 534         CodeWriter crhead = new StandardCodeWriter(outputhead);
 535         CodeWriter craux = new StandardCodeWriter(outputaux);
 536         oldmodel=VarDescriptor.makeNew("oldmodel");
 537         newmodel=VarDescriptor.makeNew("newmodel");
 538         worklist=VarDescriptor.makeNew("worklist");
 539         goodflag=VarDescriptor.makeNew("goodflag");
 540         repairtable=VarDescriptor.makeNew("repairtable");
 541
 542         if (Compiler.GENERATEINSTRUMENT) {
 543             craux.outputline("int updatecount;");
 544             craux.outputline("int rebuildcount;");
 545             craux.outputline("int abstractcount;");
 546         }
 547
 548         crhead.outputline("int doanalysis"+postfix+"(struct "+name+"_state *);");
 549         craux.outputline("int doanalysis"+postfix+"(struct "+name+"_state * thisvar)");
 550
 551         craux.startblock();
 552         craux.outputline("int highmark;"); /* This declaration is special...need it to be first */
 553         craux.outputline("int noerrors=1;");
 554         craux.startBuffer();
 555
 556         if (Compiler.TIME) {
 557             craux.outputline("struct timeval _begin_time,_end_time;");
 558             craux.outputline("gettimeofday(&_begin_time,NULL);");
 559         }
 560         if (Compiler.GENERATEINSTRUMENT) {
 561             craux.outputline("updatecount=0;");
 562             craux.outputline("rebuildcount=0;");
 563             craux.outputline("abstractcount=0;");
 564         }
 565
 566
 567         craux.addDeclaration("struct "+name+ " * ",oldmodel.getSafeSymbol());
 568         craux.outputline(oldmodel.getSafeSymbol()+"=0;");
 569         craux.addDeclaration("struct WorkList * ",worklist.getSafeSymbol());
 570         craux.outputline(worklist.getSafeSymbol()+" = allocateWorkList();");
 571         craux.addDeclaration("struct RepairHash * ",repairtable.getSafeSymbol());
 572         craux.outputline(repairtable.getSafeSymbol()+"=0;");
 573         craux.outputline("initializestack(&highmark);");
 574         craux.outputline(name+"_statecomputesizes(thisvar, arsize, arnumelements);");
 575         craux.outputline("computesizes();");
 576         craux.outputline(name+"_staterecomputesizes(thisvar);");
 577         craux.outputline("while (1)");
 578         craux.startblock();
 579         craux.addDeclaration("struct "+name+ " * ",newmodel.getSafeSymbol());
 580         craux.outputline(newmodel.getSafeSymbol()+"=allocate"+name+"();");
 581         craux.outputline("WorkListreset("+worklist.getSafeSymbol()+");");
 582         if (Compiler.GENERATEINSTRUMENT)
 583             craux.outputline("rebuildcount++;");
 584     }
 585
 586     private void generate_teardown() {
 587         CodeWriter cr = new StandardCodeWriter(outputaux);
 588         cr.endblock();
 589         if (Compiler.TIME) {
 590             cr.outputline("gettimeofday(&_end_time,NULL);");
 591             cr.outputline("printf(\"time=%ld uS\\n\",(_end_time.tv_sec-_begin_time.tv_sec)*1000000+_end_time.tv_usec-_begin_time.tv_usec);");
 592         }
 593
 594         if (Compiler.GENERATEINSTRUMENT) {
 595             cr.outputline("printf(\"updatecount=%d\\n\",updatecount);");
 596             cr.outputline("printf(\"rebuildcount=%d\\n\",rebuildcount);");
 597             cr.outputline("printf(\"abstractcount=%d\\n\",abstractcount);");
 598         }
 599
 600     }
 601
 602     private void generate_print() {
 603
 604         final SymbolTable st = new SymbolTable();
 605
 606         CodeWriter cr = new StandardCodeWriter(outputaux) {
 607                 public SymbolTable getSymbolTable() { return st; }
 608             };
 609
 610         cr.outputline("/* printing sets!*/");
 611         cr.outputline("printf(\"\\n\\nPRINTING SETS AND RELATIONS\\n\");");
 612
 613         Iterator setiterator = state.stSets.descriptors();
 614         while (setiterator.hasNext()) {
 615             SetDescriptor sd = (SetDescriptor) setiterator.next();
 616             if (sd.getSymbol().equals("int") || sd.getSymbol().equals("token")) {
 617                 continue;
 618             }
 619
 620             String setname = sd.getSafeSymbol();
 621
 622             cr.startblock();
 623             cr.outputline("/* printing set " + setname+"*/");
 624             cr.outputline("printf(\"\\nPrinting set " + sd.getSymbol() + " - %d elements \\n\", SimpleHashcountset("+setname+"_hash));");
 625             cr.addDeclaration("struct SimpleIterator","__setiterator");
 626             cr.outputline("SimpleHashiterator("+setname+"_hash,&__setiterator);");
 627             cr.outputline("while (hasNext(&__setiterator))");
 628             cr.startblock();
 629             cr.addDeclaration("int","__setval");
 630             cr.outputline("__setval = (int) next(&__setiterator);");
 631
 632             TypeDescriptor td = sd.getType();
 633             if (td instanceof StructureTypeDescriptor) {
 634                 StructureTypeDescriptor std = (StructureTypeDescriptor) td;
 635                 VarDescriptor vd = new VarDescriptor ("__setval", "__setval", td, false);
 636                 std.generate_printout(cr, vd);
 637             } else { // Missing type descriptor or reserved type, just print int
 638                 cr.outputline("printf(\"<%d> \", __setval);");
 639             }
 640
 641
 642             cr.endblock();
 643             cr.endblock();
 644         }
 645
 646         Iterator reliterator = state.stRelations.descriptors();
 647         while (reliterator.hasNext()) {
 648             RelationDescriptor rd = (RelationDescriptor) reliterator.next();
 649
 650
 651             String relname = rd.getSafeSymbol();
 652             if (rd.testUsage(RelationDescriptor.IMAGE)) {
 653                 cr.startblock();
 654                 cr.outputline("/* printing relation " + relname+"*/");
 655                 cr.outputline("printf(\"\\nPrinting relation " + rd.getSymbol() + " - %d elements \\n\", SimpleHashcountset("+relname+"_hash));");
 656                 cr.addDeclaration("struct SimpleIterator","__reliterator");
 657                 cr.outputline("SimpleHashiterator("+relname+"_hash,&__reliterator);");
 658                 cr.outputline("while (hasNext(&__reliterator))");
 659                 cr.startblock();
 660                 cr.addDeclaration("int","__relval");
 661                 cr.addDeclaration("int","__relval2");
 662                 cr.outputline("__relval2 = (int) key(&__reliterator);");
 663                 cr.outputline("__relval = (int) next(&__reliterator);");
 664
 665                 cr.outputline("printf(\"<%ld,%ld> \", __relval2,__relval);");
 666
 667                 cr.endblock();
 668                 cr.endblock();
 669             } else if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
 670                 cr.startblock();
 671                 cr.outputline("/* printing inv relation " + relname+"*/");
 672                 cr.outputline("printf(\"\\nPrinting relation using inv" + rd.getSymbol() + " - %d elements \\n\", SimpleHashcountset("+relname+"_hash));");
 673                 cr.addDeclaration("struct SimpleIterator","__reliterator");
 674                 cr.outputline("SimpleHashiterator("+relname+"_hashinv,&__reliterator);");
 675                 cr.outputline("while (hasNext(&__reliterator))");
 676                 cr.startblock();
 677                 cr.addDeclaration("int","__relval");
 678                 cr.addDeclaration("int","__relval2");
 679                 cr.outputline("__relval2 = (int) key(&__reliterator);");
 680                 cr.outputline("__relval = (int) next(&__reliterator);");
 681
 682
 683                 cr.outputline("printf(\"<%ld,%ld> \", __relval,__relval2);");
 684
 685                 cr.endblock();
 686                 cr.endblock();
 687             }
 688
 689         }
 690
 691         cr.outputline("printf(\"\\n\\n------------------- END PRINTING\\n\");");
 692     }
 693
 694     Set ruleset=null;
 695     private void generate_rules() {
 696         /* first we must sort the rules */
 697         RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 698         SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
 699         System.out.println("SCC="+(mrd.numSCC()-1));
 700         for(int sccindex=0;sccindex<mrd.numSCC();sccindex++) {
 701             ruleset=mrd.getSCC(sccindex);
 702             boolean needworklist=mrd.hasCycle(sccindex);
 703
 704             if (!needworklist) {
 705                 Iterator iterator_rs = ruleset.iterator();
 706                 while (iterator_rs.hasNext()) {
 707                     Rule rule = (Rule) iterator_rs.next();
 708                     if (rule.getnogenerate())
 709                         continue;
 710                     {
 711                         final SymbolTable st = rule.getSymbolTable();
 712                         CodeWriter cr = new StandardCodeWriter(outputaux) {
 713                                 public SymbolTable getSymbolTable() { return st; }
 714                             };
 715                         InvariantValue ivalue=new InvariantValue();
 716                         cr.setInvariantValue(ivalue);
 717
 718                         cr.outputline("/* build " +escape(rule.toString())+"*/");
 719                         cr.startblock();
 720                         cr.addDeclaration("int","maybe");
 721                         cr.outputline("maybe=0;");
 722
 723                         Expr ruleexpr=rule.getGuardExpr();
 724                         HashSet invariantvars=new HashSet();
 725                         Set invariants=ruleexpr.findInvariants(invariantvars);
 726
 727                         if ((ruleexpr instanceof BooleanLiteralExpr)&&
 728                             ((BooleanLiteralExpr)ruleexpr).getValue()) {
 729                             if (rule.getInclusion() instanceof SetInclusion) {
 730                                 invariants.addAll(((SetInclusion)rule.getInclusion()).getExpr().findInvariants(invariantvars));
 731                             } else if (rule.getInclusion() instanceof RelationInclusion) {
 732                                 invariants.addAll(((RelationInclusion)rule.getInclusion()).getLeftExpr().findInvariants(invariantvars));
 733                                 invariants.addAll(((RelationInclusion)rule.getInclusion()).getRightExpr().findInvariants(invariantvars));
 734                             }
 735                         }
 736                         ListIterator quantifiers = rule.quantifiers();
 737                         while (quantifiers.hasNext()) {
 738                             Quantifier quantifier = (Quantifier) quantifiers.next();
 739                             if (quantifier instanceof ForQuantifier) {
 740                                 ForQuantifier fq=(ForQuantifier)quantifier;
 741                                 invariants.addAll(fq.lower.findInvariants(invariantvars));
 742                                 invariants.addAll(fq.upper.findInvariants(invariantvars));
 743                             }
 744                         }
 745
 746                         int openparencount=0;
 747                         for(Iterator invit=invariants.iterator();invit.hasNext();) {
 748                             Expr invexpr=(Expr)invit.next();
 749                             VarDescriptor tmpvd=VarDescriptor.makeNew("tmpvar");
 750                             VarDescriptor maybevd=VarDescriptor.makeNew("maybevar");
 751                             invexpr.generate(cr,tmpvd);
 752                             cr.addDeclaration("int ",maybevd.getSafeSymbol());
 753                             cr.outputline(maybevd.getSafeSymbol()+"=maybe;");
 754                             cr.outputline("maybe=0;");
 755                             ivalue.assignPair(invexpr,tmpvd,maybevd);
 756                             openparencount++;
 757                             cr.startblock();
 758                         }
 759                         quantifiers = rule.quantifiers();
 760                         while (quantifiers.hasNext()) {
 761                             Quantifier quantifier = (Quantifier) quantifiers.next();
 762                             quantifier.generate_open(cr);
 763                         }
 764
 765                         /* pretty print! */
 766                         cr.output("/*");
 767                         rule.getGuardExpr().prettyPrint(cr);
 768                         cr.outputline("*/");
 769
 770                         /* now we have to generate the guard test */
 771                         VarDescriptor guardval = VarDescriptor.makeNew();
 772                         rule.getGuardExpr().generate(cr, guardval);
 773                         cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 774                         cr.startblock();
 775
 776                         /* now we have to generate the inclusion code */
 777                         currentrule=rule;
 778                         rule.getInclusion().generate(cr);
 779                         cr.endblock();
 780                         while (quantifiers.hasPrevious()) {
 781                             Quantifier quantifier = (Quantifier) quantifiers.previous();
 782                             cr.endblock();
 783                         }
 784                         cr.endblock();
 785                         while((openparencount--)>0)
 786                             cr.endblock();
 787                         cr.outputline("");
 788                         cr.outputline("");
 789                     }
 790                 }
 791             } else {
 792                 CodeWriter cr2 = new StandardCodeWriter(outputaux);
 793
 794                 for(Iterator initialworklist=ruleset.iterator();initialworklist.hasNext();) {
 795                     /** Construct initial worklist set */
 796                     Rule rule=(Rule)initialworklist.next();
 797                     cr2.outputline("WorkListadd("+worklist.getSafeSymbol()+","+rule.getNum()+",-1,0,0);");
 798                 }
 799
 800                 cr2.outputline("while (WorkListhasMoreElements("+worklist.getSafeSymbol()+"))");
 801                 cr2.startblock();
 802                 VarDescriptor idvar=VarDescriptor.makeNew("id");
 803                 cr2.addDeclaration("int ",idvar.getSafeSymbol());
 804                 cr2.outputline(idvar.getSafeSymbol()+"=WorkListgetid("+worklist.getSafeSymbol()+");");
 805
 806                 String elseladder = "if";
 807
 808                 Iterator iterator_rules = ruleset.iterator();
 809                 while (iterator_rules.hasNext()) {
 810
 811                     Rule rule = (Rule) iterator_rules.next();
 812                     int dispatchid = rule.getNum();
 813
 814                     {
 815                         final SymbolTable st = rule.getSymbolTable();
 816                         CodeWriter cr = new StandardCodeWriter(outputaux) {
 817                                 public SymbolTable getSymbolTable() { return st; }
 818                             };
 819
 820                         cr.indent();
 821                         cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
 822                         cr.startblock();
 823                         cr.addDeclaration("int","maybe");
 824                         cr.outputline("maybe=0;");
 825                         VarDescriptor typevar=VarDescriptor.makeNew("type");
 826                         VarDescriptor leftvar=VarDescriptor.makeNew("left");
 827                         VarDescriptor rightvar=VarDescriptor.makeNew("right");
 828                         cr.addDeclaration("int",typevar.getSafeSymbol());
 829                         cr.outputline(typevar.getSafeSymbol()+"= WorkListgettype("+worklist.getSafeSymbol()+");");
 830                         cr.addDeclaration("int",leftvar.getSafeSymbol());
 831                         cr.outputline(leftvar.getSafeSymbol()+"= WorkListgetlvalue("+worklist.getSafeSymbol()+");");
 832                         cr.addDeclaration("int",rightvar.getSafeSymbol());
 833                         cr.outputline(rightvar.getSafeSymbol()+"= WorkListgetrvalue("+worklist.getSafeSymbol()+");");
 834                         cr.outputline("/* build " +escape(rule.toString())+"*/");
 835
 836
 837                         for (int j=0;j<rule.numQuantifiers();j++) {
 838                             Quantifier quantifier = rule.getQuantifier(j);
 839                             quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
 840                         }
 841
 842                         /* pretty print! */
 843                         cr.output("/*");
 844
 845                         rule.getGuardExpr().prettyPrint(cr);
 846                         cr.outputline("*/");
 847
 848                         /* now we have to generate the guard test */
 849
 850                         VarDescriptor guardval = VarDescriptor.makeNew();
 851                         rule.getGuardExpr().generate(cr, guardval);
 852
 853                         cr.outputline("if (" + guardval.getSafeSymbol() + ")");
 854                         cr.startblock();
 855
 856                         /* now we have to generate the inclusion code */
 857                         currentrule=rule;
 858                         rule.getInclusion().generate(cr);
 859                         cr.endblock();
 860
 861                         for (int j=0;j<rule.numQuantifiers();j++) {
 862                             cr.endblock();
 863                         }
 864
 865                         // close startblocks generated by DotExpr memory checks
 866                         //DotExpr.generate_memory_endblocks(cr);
 867
 868                         cr.endblock(); // end else-if WORKLIST ladder
 869
 870                         elseladder = "else if";
 871                     }
 872                 }
 873                 cr2.outputline("else");
 874                 cr2.startblock();
 875                 cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
 876                 cr2.outputline("exit(1);");
 877                 cr2.endblock();
 878                 // end block created for worklist
 879                 cr2.outputline("WorkListpop("+worklist.getSafeSymbol()+");");
 880                 cr2.endblock();
 881             }
 882         }
 883     }
 884
 885     public static String escape(String s) {
 886         String newstring="";
 887         for(int i=0;i<s.length();i++) {
 888             char c=s.charAt(i);
 889             if (c=='"')
 890                 newstring+="\"";
 891             else
 892                 newstring+=c;
 893         }
 894         return newstring;
 895     }
 896
 897     private void generate_checks() {
 898         /* do constraint checks */
 899         Iterator i;
 900         if (Compiler.REPAIR)
 901             i=termination.constraintdependence.computeOrdering().iterator();
 902         else
 903             i=state.vConstraints.iterator();
 904         for (; i.hasNext();) {
 905             Constraint constraint;
 906             if (Compiler.REPAIR)
 907                 constraint= (Constraint) ((GraphNode)i.next()).getOwner();
 908             else
 909                 constraint=(Constraint)i.next();
 910
 911             {
 912                 final SymbolTable st = constraint.getSymbolTable();
 913                 CodeWriter cr = new StandardCodeWriter(outputaux);
 914                 cr.pushSymbolTable(constraint.getSymbolTable());
 915
 916                 cr.outputline("/* checking " + escape(constraint.toString())+"*/");
 917                 cr.startblock();
 918
 919                 ListIterator quantifiers = constraint.quantifiers();
 920
 921                 while (quantifiers.hasNext()) {
 922                     Quantifier quantifier = (Quantifier) quantifiers.next();
 923                     quantifier.generate_open(cr);
 924                 }
 925
 926                 cr.addDeclaration("int","maybe");
 927                 cr.outputline("maybe = 0;");
 928
 929                 /* now we have to generate the guard test */
 930
 931                 VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
 932                 constraint.getLogicStatement().generate(cr, constraintboolean);
 933
 934                 cr.outputline("if (maybe)");
 935                 cr.startblock();
 936                 cr.outputline("printf(\"maybe fail " +  escape(constraint.toString()) + ". \\n\");");
 937                 cr.outputline("noerrors=0;");
 938                 //cr.outputline("exit(1);");
 939                 cr.endblock();
 940
 941                 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
 942                 cr.startblock();
 943                 cr.outputline("noerrors=0;");
 944                 if (!Compiler.REPAIR||Compiler.GENERATEDEBUGHOOKS)
 945                     cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \\n\");");
 946
 947                 if (Compiler.REPAIR) {
 948                 /* Do repairs */
 949                 /* Build new repair table */
 950
 951                 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
 952                 cr.outputline("freeRepairHash("+repairtable.getSafeSymbol()+");");
 953                 cr.outputline(repairtable.getSafeSymbol()+"=noargallocateRepairHash();");
 954
 955                 if (Compiler.GENERATEDEBUGHOOKS)
 956                     cr.outputline("debughook();");
 957                 /* Compute cost of each repair */
 958                 VarDescriptor mincost=VarDescriptor.makeNew("mincost");
 959                 VarDescriptor mincostindex=VarDescriptor.makeNew("mincostindex");
 960                 Vector dnfconst=new Vector();
 961                 dnfconst.addAll((Set)termination.conjunctionmap.get(constraint));
 962
 963                 if (dnfconst.size()<=1) {
 964                     cr.addDeclaration("int",mincostindex.getSafeSymbol());
 965                     cr.outputline(mincostindex.getSafeSymbol()+"=0;");
 966                 }
 967                 if (dnfconst.size()>1) {
 968                     cr.addDeclaration("int",mincostindex.getSafeSymbol());
 969                     boolean first=true;
 970                     for(int j=0;j<dnfconst.size();j++) {
 971                         GraphNode gn=(GraphNode)dnfconst.get(j);
 972                         Conjunction conj=((TermNode)gn.getOwner()).getConjunction();
 973                         if (removed.contains(gn))
 974                             continue;
 975
 976                         VarDescriptor costvar;
 977                         if (first) {
 978                             costvar=mincost;
 979                         } else
 980                             costvar=VarDescriptor.makeNew("cost");
 981                         for(int k=0;k<conj.size();k++) {
 982                             DNFPredicate dpred=conj.get(k);
 983                             Predicate p=dpred.getPredicate();
 984                             boolean negate=dpred.isNegated();
 985                             VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
 986                             p.generate(cr,predvalue);
 987                             if (k==0) {
 988                                 cr.addDeclaration("int",costvar.getSafeSymbol());
 989                                 cr.outputline(costvar.getSafeSymbol()+"=0;");
 990                             }
 991                             if (negate)
 992                                 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
 993                             else
 994                                 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
 995                             cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
 996                         }
 997
 998                         if(!first) {
 999                             cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
1000                             cr.startblock();
1001                             cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
1002                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
1003                             cr.endblock();
1004                         } else
1005                             cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
1006                         first=false;
1007                     }
1008                 }
1009                 cr.outputline("switch("+mincostindex.getSafeSymbol()+")");
1010                 cr.startblock();
1011                 for(int j=0;j<dnfconst.size();j++) {
1012                     GraphNode gn=(GraphNode)dnfconst.get(j);
1013                     Conjunction conj=((TermNode)gn.getOwner()).getConjunction();
1014                     if (removed.contains(gn))
1015                         continue;
1016                     cr.outputline("case "+j+":");
1017                     cr.startblock();
1018                     for(int k=0;k<conj.size();k++) {
1019                         DNFPredicate dpred=conj.get(k);
1020                         Predicate p=dpred.getPredicate();
1021                         boolean negate=dpred.isNegated();
1022                         VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
1023                         p.generate(cr,predvalue);
1024                         if (negate)
1025                             cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
1026                         else
1027                             cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
1028                         cr.startblock();
1029                         if (Compiler.GENERATEINSTRUMENT)
1030                             cr.outputline("abstractcount++;");
1031                         if (p instanceof InclusionPredicate)
1032                             generateinclusionrepair(conj,dpred, cr);
1033                         else if (p instanceof ExprPredicate) {
1034                             ExprPredicate ep=(ExprPredicate)p;
1035                             if (ep.getType()==ExprPredicate.SIZE)
1036                                 generatesizerepair(conj,dpred,cr);
1037                             else if (ep.getType()==ExprPredicate.COMPARISON)
1038                                 generatecomparisonrepair(conj,dpred,cr);
1039                         } else throw new Error("Unrecognized Predicate");
1040                         cr.endblock();
1041                     }
1042                     /* Update model */
1043                     cr.endblock();
1044                     cr.outputline("break;");
1045                 }
1046                 cr.endblock();
1047
1048                 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
1049                 cr.outputline("free"+name+"("+oldmodel.getSafeSymbol()+");");
1050                 cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
1051                 cr.outputline("goto rebuild;");  /* Rebuild model and all */
1052                 }
1053                 cr.endblock();
1054
1055                 while (quantifiers.hasPrevious()) {
1056                     Quantifier quantifier = (Quantifier) quantifiers.previous();
1057                     cr.endblock();
1058                 }
1059                 cr.endblock();
1060                 cr.outputline("");
1061                 cr.outputline("");
1062             }
1063         }
1064         CodeWriter cr = new StandardCodeWriter(outputaux);
1065         cr.startblock();
1066         cr.outputline("if ("+repairtable.getSafeSymbol()+")");
1067         cr.outputline("freeRepairHash("+repairtable.getSafeSymbol()+");");
1068         cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
1069         cr.outputline("free"+name+"("+oldmodel.getSafeSymbol()+");");
1070         cr.outputline("free"+name+"("+newmodel.getSafeSymbol()+");");
1071         cr.outputline("freeWorkList("+worklist.getSafeSymbol()+");");
1072         cr.outputline("resettypemap();");
1073         cr.outputline("break;");
1074         cr.endblock();
1075         cr.outputline("rebuild:");
1076         cr.outputline(";");
1077     }
1078
1079     private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
1080         Set nodes=getmultupdatenodeset(conj,dpred,repairtype);
1081         Iterator it=nodes.iterator();
1082         if (it.hasNext())
1083             return (MultUpdateNode)it.next();
1084         else
1085             return null;
1086     }
1087
1088     private Set getmultupdatenodeset(Conjunction conj, DNFPredicate dpred, int repairtype) {
1089         HashSet hs=new HashSet();
1090         GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
1091         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1092             GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
1093             TermNode tn2=(TermNode)gn2.getOwner();
1094             if (tn2.getType()==TermNode.ABSTRACT) {
1095                 AbstractRepair ar=tn2.getAbstract();
1096                 if (((repairtype==-1)||(ar.getType()==repairtype))&&
1097                     ar.getPredicate()==dpred) {
1098                     for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
1099                         GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
1100                         if (!removed.contains(gn3)) {
1101                             TermNode tn3=(TermNode)gn3.getOwner();
1102                             if (tn3.getType()==TermNode.UPDATE) {
1103                                 hs.add(tn3.getUpdate());
1104                             }
1105                         }
1106                     }
1107                 }
1108             }
1109         }
1110         return hs;
1111     }
1112
1113     private AbstractRepair getabstractrepair(Conjunction conj, DNFPredicate dpred, int repairtype) {
1114         HashSet hs=new HashSet();
1115         MultUpdateNode mun=null;
1116         GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
1117         for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
1118             GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
1119             TermNode tn2=(TermNode)gn2.getOwner();
1120             if (tn2.getType()==TermNode.ABSTRACT) {
1121                 AbstractRepair ar=tn2.getAbstract();
1122                 if (((repairtype==-1)||(ar.getType()==repairtype))&&
1123                     ar.getPredicate()==dpred) {
1124                     return ar;
1125                 }
1126             }
1127         }
1128         return null;
1129     }
1130
1131
1132     /** Generates abstract (and concrete) repair for a comparison */
1133
1134     private void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
1135         Set updates=getmultupdatenodeset(conj,dpred,AbstractRepair.MODIFYRELATION);
1136         AbstractRepair ar=getabstractrepair(conj,dpred,AbstractRepair.MODIFYRELATION);
1137         MultUpdateNode munmodify=null;
1138         MultUpdateNode munadd=null;
1139         MultUpdateNode munremove=null;
1140         for(Iterator it=updates.iterator();it.hasNext();) {
1141             MultUpdateNode mun=(MultUpdateNode)it.next();
1142             if (mun.getType()==MultUpdateNode.ADD) {
1143                 munadd=mun;
1144             } else if (mun.getType()==MultUpdateNode.REMOVE) {
1145                 munremove=mun;
1146             } else if (mun.getType()==MultUpdateNode.MODIFY) {
1147                 munmodify=mun;
1148             }
1149         }
1150
1151         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
1152         RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
1153         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1154         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1155         boolean inverted=ep.inverted();
1156         boolean negated=dpred.isNegated();
1157         OpExpr expr=(OpExpr)ep.expr;
1158         Opcode opcode=expr.getOpcode();
1159         VarDescriptor leftside=VarDescriptor.makeNew("leftside");
1160         VarDescriptor rightside=VarDescriptor.makeNew("rightside");
1161         VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
1162         boolean needremoveloop=ar.mayNeedFunctionEnforcement(state)&&ar.needsRemoves(state);
1163
1164         if (needremoveloop&&((munadd==null)||(munremove==null))) {
1165             System.out.println("Warning:  need to have individual remove operations for"+dpred.name());
1166             needremoveloop=false;
1167         }
1168         if (needremoveloop) {
1169             cr.outputline("while (1)");
1170             cr.startblock();
1171         }
1172         if (!inverted) {
1173             ((RelationExpr)expr.getLeftExpr()).getExpr().generate(cr,leftside);
1174             expr.getRightExpr().generate(cr,newvalue);
1175             cr.addDeclaration(rd.getRange().getType().getGenerateType().getSafeSymbol(),rightside.getSafeSymbol());
1176             cr.outputline("SimpleHashget("+rd.getSafeSymbol()+"_hash,"+leftside.getSafeSymbol()+", &"+rightside.getSafeSymbol()+");");
1177         } else {
1178             ((RelationExpr)expr.getLeftExpr()).getExpr().generate(cr,rightside);
1179             expr.getRightExpr().generate(cr,newvalue);
1180             cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
1181             cr.outputline("SimpleHashget("+rd.getSafeSymbol()+"_hashinv,"+rightside.getSafeSymbol()+", &"+leftside.getSafeSymbol()+");");
1182         }
1183
1184         opcode=Opcode.translateOpcode(negated,opcode);
1185
1186         if (opcode==Opcode.GT) {
1187             cr.outputline(newvalue.getSafeSymbol()+"++;");
1188         } else if (opcode==Opcode.GE) {
1189             /* Equal */
1190         } else if (opcode==Opcode.LT) {
1191             cr.outputline(newvalue.getSafeSymbol()+"--;");
1192         } else if (opcode==Opcode.LE) {
1193             /* Equal */
1194         } else if (opcode==Opcode.EQ) {
1195             /* Equal */
1196         } else if (opcode==Opcode.NE) { /* search for FLAGNE if this is changed*/
1197             cr.outputline(newvalue.getSafeSymbol()+"++;");
1198         } else {
1199             throw new Error("Unrecognized Opcode");
1200         }
1201         /* Do abstract repairs */
1202         if (usageimage) {
1203             cr.outputline("SimpleHashremove("+rd.getSafeSymbol()+"_hash, "+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
1204         }
1205         if (usageinvimage) {
1206             cr.outputline("SimpleHashremove("+rd.getSafeSymbol()+"_hashinv, "+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
1207         }
1208
1209         if (needremoveloop) {
1210             if (!inverted) {
1211                 cr.outputline("if (SimpleHashcontainskey("+rd.getSafeSymbol()+"_hash, "+leftside.getSafeSymbol()+"))");
1212                 cr.startblock();
1213             } else {
1214                 cr.outputline("if (SimpleHashcontainskey("+rd.getSafeSymbol()+"_hashinv, "+rightside.getSafeSymbol()+"))");
1215                 cr.startblock();
1216             }
1217             for(int i=0;i<state.vRules.size();i++) {
1218                 Rule r=(Rule)state.vRules.get(i);
1219                 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
1220                     for(int j=0;j<munremove.numUpdates();j++) {
1221                         UpdateNode un=munremove.getUpdate(i);
1222                         if (un.getRule()==r) {
1223                                 /* Update for rule r */
1224                             String name=(String)updatenames.get(un);
1225                             cr.outputline("RepairHashaddrelation("+repairtable.getSafeSymbol()+","+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
1226                         }
1227                     }
1228                 }
1229             }
1230             cr.outputline("continue;");
1231             cr.endblock();
1232         }
1233
1234         if (usageimage) {
1235             if (!inverted) {
1236                 cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hash,"+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
1237             } else {
1238                 cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hash, "+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
1239             }
1240         }
1241         if (usageinvimage) {
1242             if (!inverted) {
1243                 cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hashinv, "+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
1244             } else {
1245                 cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hashinv,"+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
1246             }
1247         }
1248         /* Do concrete repairs */
1249         if (munmodify!=null&&(!ar.mayNeedFunctionEnforcement(state))||(munadd==null)||(ar.needsRemoves(state)&&(munremove==null))) {
1250             for(int i=0;i<state.vRules.size();i++) {
1251                 Rule r=(Rule)state.vRules.get(i);
1252                 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
1253                     for(int j=0;j<munmodify.numUpdates();j++) {
1254                         UpdateNode un=munmodify.getUpdate(j);
1255                         if (un.getRule()==r) {
1256                             /* Update for rule r */
1257                             String name=(String)updatenames.get(un);
1258                             cr.outputline("RepairHashaddrelation2("+repairtable.getSafeSymbol()+","+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+","+newvalue.getSafeSymbol()+");");
1259                         }
1260                     }
1261                 }
1262             }
1263         } else {
1264             /* Start with scheduling removal */
1265             if (ar.needsRemoves(state))
1266                 for(int i=0;i<state.vRules.size();i++) {
1267                     Rule r=(Rule)state.vRules.get(i);
1268                     if (r.getInclusion().getTargetDescriptors().contains(rd)) {
1269                         for(int j=0;j<munremove.numUpdates();j++) {
1270                             UpdateNode un=munremove.getUpdate(i);
1271                             if (un.getRule()==r) {
1272                                 /* Update for rule r */
1273                                 String name=(String)updatenames.get(un);
1274                                 cr.outputline("RepairHashaddrelation("+repairtable.getSafeSymbol()+","+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
1275                             }
1276                         }
1277                     }
1278                 }
1279             /* Now do addition */
1280             UpdateNode un=munadd.getUpdate(0);
1281             String name=(String)updatenames.get(un);
1282             if (!inverted) {
1283                 cr.outputline(name+"(thisvar,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
1284             } else {
1285                 cr.outputline(name+"(thisvar,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
1286             }
1287         }
1288         if (needremoveloop) {
1289             cr.outputline("break;");
1290             cr.endblock();
1291         }
1292     }
1293
1294     public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {
1295         ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
1296         OpExpr expr=(OpExpr)ep.expr;
1297         Opcode opcode=expr.getOpcode();
1298         opcode=Opcode.translateOpcode(dpred.isNegated(),opcode);
1299
1300         MultUpdateNode munremove;
1301
1302         MultUpdateNode munadd;
1303         if (ep.getDescriptor() instanceof RelationDescriptor) {
1304             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
1305             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
1306         } else {
1307             munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
1308             munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
1309         }
1310         int size=ep.rightSize();
1311         VarDescriptor sizevar=VarDescriptor.makeNew("size");
1312         ((OpExpr)expr).left.generate(cr, sizevar);
1313         VarDescriptor change=VarDescriptor.makeNew("change");
1314         cr.addDeclaration("int",change.getSafeSymbol());
1315         boolean generateadd=false;
1316         boolean generateremove=false;
1317         if (opcode==Opcode.GT) {
1318             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
1319             generateadd=true;
1320             generateremove=false;
1321         } else if (opcode==Opcode.GE) {
1322             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
1323             generateadd=true;
1324             generateremove=false;
1325         } else if (opcode==Opcode.LT) {
1326             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
1327             generateadd=false;
1328             generateremove=true;
1329         } else if (opcode==Opcode.LE) {
1330             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
1331             generateadd=false;
1332             generateremove=true;
1333         } else if (opcode==Opcode.EQ) {
1334             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
1335             if (size==0)
1336                 generateadd=false;
1337             else
1338                 generateadd=true;
1339             generateremove=true;
1340         } else if (opcode==Opcode.NE) {
1341             cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
1342             generateadd=true;
1343             generateremove=false;
1344         } else {
1345             throw new Error("Unrecognized Opcode");
1346         }
1347
1348 // In some cases the analysis has determined that generating removes
1349 // is unnecessary
1350         if (generateremove&&munremove==null)
1351             generateremove=false;
1352
1353         Descriptor d=ep.getDescriptor();
1354         if (generateremove) {
1355             cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
1356             cr.startblock();
1357             /* Find element to remove */
1358             VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
1359             VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
1360             if (d instanceof RelationDescriptor) {
1361                 if (ep.inverted()) {
1362                     ((ImageSetExpr)((SizeofExpr)expr.left).setexpr).generate_leftside(cr,rightvar);
1363                     cr.addDeclaration("int",leftvar.getSafeSymbol());
1364                     cr.outputline("SimpleHashget("+d.getSafeSymbol()+"_hashinv,(int)"+rightvar.getSafeSymbol()+", &"+leftvar.getSafeSymbol()+");");
1365                 } else {
1366                     ((ImageSetExpr)((SizeofExpr)expr.left).setexpr).generate_leftside(cr,leftvar);
1367                     cr.addDeclaration("int",rightvar.getSafeSymbol());
1368                     cr.outputline("SimpleHashget("+d.getSafeSymbol()+"_hash ,(int)"+leftvar.getSafeSymbol()+", &"+rightvar.getSafeSymbol()+");");
1369                 }
1370             } else {
1371                 cr.addDeclaration("int",leftvar.getSafeSymbol());
1372                 cr.outputline(leftvar.getSafeSymbol()+"= SimpleHashfirstkey("+d.getSafeSymbol()+"_hash);");
1373             }
1374             /* Generate abstract remove instruction */
1375             if (d instanceof RelationDescriptor) {
1376                 RelationDescriptor rd=(RelationDescriptor) d;
1377                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1378                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1379                 if (usageimage)
1380                     cr.outputline("SimpleHashremove("+rd.getSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1381                 if (usageinvimage)
1382                     cr.outputline("SimpleHashremove("+rd.getSafeSymbol()+"_hashinv ,(int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1383             } else {
1384                 cr.outputline("SimpleHashremove("+d.getSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1385             }
1386             /* Generate concrete remove instruction */
1387             for(int i=0;i<state.vRules.size();i++) {
1388                 Rule r=(Rule)state.vRules.get(i);
1389                 if (r.getInclusion().getTargetDescriptors().contains(d)) {
1390                     for(int j=0;j<munremove.numUpdates();j++) {
1391                         UpdateNode un=munremove.getUpdate(j);
1392                         if (un.getRule()==r) {
1393                                 /* Update for rule rule r */
1394                             String name=(String)updatenames.get(un);
1395                             if (d instanceof RelationDescriptor) {
1396                                 cr.outputline("RepairHashaddrelation("+repairtable.getSafeSymbol()+","+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1397                             } else {
1398                                 cr.outputline("RepairHashaddset("+repairtable.getSafeSymbol()+","+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1399                             }
1400                         }
1401                     }
1402                 }
1403             }
1404             cr.endblock();
1405         }
1406
1407 // In some cases the analysis has determined that generating removes
1408 // is unnecessary
1409         if (generateadd&&munadd==null)
1410             generateadd=false;
1411
1412         if (generateadd) {
1413
1414             cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
1415             cr.startblock();
1416             VarDescriptor newobject=VarDescriptor.makeNew("newobject");
1417             if (d instanceof RelationDescriptor) {
1418                 VarDescriptor otherside=VarDescriptor.makeNew("otherside");
1419                 ((ImageSetExpr)((SizeofExpr)expr.left).setexpr).generate_leftside(cr,otherside);
1420
1421                 RelationDescriptor rd=(RelationDescriptor)d;
1422                 if (termination.sources.relsetSource(rd,!ep.inverted())) {
1423                     /* Set Source */
1424                     SetDescriptor sd=termination.sources.relgetSourceSet(rd,!ep.inverted());
1425                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
1426                     cr.addDeclaration(sd.getType().getGenerateType().getSafeSymbol(),newobject.getSafeSymbol());
1427                     cr.addDeclaration("struct SimpleIterator",iterator.getSafeSymbol());
1428                     cr.outputline("for(SimpleHashiterator("+sd.getSafeSymbol()+"_hash , &"+ iterator.getSafeSymbol() +"); hasNext(&"+iterator.getSafeSymbol()+");)");
1429                     cr.startblock();
1430                     if (ep.inverted()) {
1431                         cr.outputline("if (!SimpleHashcontainskeydata("+rd.getSafeSymbol()+"_hashinv,"+iterator.getSafeSymbol()+".key(),"+otherside.getSafeSymbol()+"))");
1432                     } else {
1433                         cr.outputline("if (!SimpleHashcontainskeydata("+rd.getSafeSymbol()+"_hash, "+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+".key()))");
1434                     }
1435                     cr.outputline(newobject.getSafeSymbol()+"=key(&"+iterator.getSafeSymbol()+");");
1436                     cr.outputline("next(&"+iterator.getSafeSymbol()+");");
1437                     cr.endblock();
1438                 } else if (termination.sources.relallocSource(rd,!ep.inverted())) {
1439                     /* Allocation Source*/
1440                     termination.sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
1441                 } else throw new Error("No source for adding to Relation");
1442                 if (ep.inverted()) {
1443                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1444                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1445                     if (usageimage)
1446                         cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hash, "+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1447                     if (usageinvimage)
1448                         cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hashinv, "+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1449
1450                     UpdateNode un=munadd.getUpdate(0);
1451                     String name=(String)updatenames.get(un);
1452                     cr.outputline(name+"(thisvar,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1453                 } else {
1454                     boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1455                     boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1456                     if (usageimage)
1457                         cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hash, "+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1458                     if (usageinvimage)
1459                         cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hashinv, "+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
1460                     UpdateNode un=munadd.getUpdate(0);
1461                     String name=(String)updatenames.get(un);
1462                     cr.outputline(name+"(thisvar, "+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1463                 }
1464             } else {
1465                 SetDescriptor sd=(SetDescriptor)d;
1466                 if (termination.sources.setSource(sd)) {
1467                     /* Set Source */
1468                     /* Set Source */
1469                     SetDescriptor sourcesd=termination.sources.getSourceSet(sd);
1470                     VarDescriptor iterator=VarDescriptor.makeNew("iterator");
1471                     cr.addDeclaration(sourcesd.getType().getGenerateType().getSafeSymbol(), newobject.getSafeSymbol());
1472                     cr.addDeclaration("struct SimpleIterator",iterator.getSafeSymbol());
1473                     cr.outputline("for(SimpleHashiterator("+sourcesd.getSafeSymbol()+"_hash, &"+iterator.getSafeSymbol()+"); hasNext(&"+iterator.getSafeSymbol()+");)");
1474                     cr.startblock();
1475                     cr.outputline("if (!SimpleHashcontainskey("+sd.getSafeSymbol()+"_hash, key(&"+iterator.getSafeSymbol()+")))");
1476                     cr.outputline(newobject.getSafeSymbol()+"=key(&"+iterator.getSafeSymbol()+");");
1477                     cr.outputline("next(&"+iterator.getSafeSymbol()+");");
1478                     cr.endblock();
1479                 } else if (termination.sources.allocSource(sd)) {
1480                     /* Allocation Source*/
1481                     termination.sources.generateSourceAlloc(cr,newobject,sd);
1482                 } else throw new Error("No source for adding to Set");
1483                 cr.outputline("SimpleHashadd("+sd.getSafeSymbol()+"_hash, "+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1484                 UpdateNode un=munadd.getUpdate(0);
1485                 String name=(String)updatenames.get(un);
1486                 cr.outputline(name+"(thisvar,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
1487             }
1488             cr.endblock();
1489         }
1490     }
1491
1492     public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
1493         InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate();
1494         boolean negated=dpred.isNegated();
1495         MultUpdateNode mun=getmultupdatenode(conj,dpred,-1);
1496         VarDescriptor leftvar=VarDescriptor.makeNew("left");
1497         ip.expr.generate(cr, leftvar);
1498
1499         if (negated) {
1500             if (ip.setexpr instanceof ImageSetExpr) {
1501                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1502                 VarDescriptor rightvar=ise.getVar();
1503                 boolean inverse=ise.inverted();
1504                 RelationDescriptor rd=ise.getRelation();
1505                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1506                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1507                 if (inverse) {
1508                     if (usageimage)
1509                         cr.outputline("SimpleHashremove("+rd.getSafeSymbol()+"_hash, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1510                     if (usageinvimage)
1511                         cr.outputline("SimpleHashremove("+rd.getSafeSymbol()+"_hashinv, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1512                 } else {
1513                     if (usageimage)
1514                         cr.outputline("SimpleHashremove("+rd.getSafeSymbol()+"_hash ,(int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1515                     if (usageinvimage)
1516                         cr.outputline("SimpleHashremove("+rd.getSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1517                 }
1518                 for(int i=0;i<state.vRules.size();i++) {
1519                     Rule r=(Rule)state.vRules.get(i);
1520                     if (r.getInclusion().getTargetDescriptors().contains(rd)) {
1521                         for(int j=0;j<mun.numUpdates();j++) {
1522                             UpdateNode un=mun.getUpdate(j);
1523                             if (un.getRule()==r) {
1524                                 /* Update for rule rule r */
1525                                 String name=(String)updatenames.get(un);
1526                                 if (inverse) {
1527                                     cr.outputline("RepairHashaddrelation("+repairtable.getSafeSymbol()+","+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1528                                 } else {
1529                                     cr.outputline("RepairHashaddrelation("+repairtable.getSafeSymbol()+","+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
1530                                 }
1531                             }
1532                         }
1533                     }
1534                 }
1535             } else {
1536                 SetDescriptor sd=ip.setexpr.sd;
1537                 cr.outputline("SimpleHashremove("+sd.getSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1538
1539                 for(int i=0;i<state.vRules.size();i++) {
1540                     Rule r=(Rule)state.vRules.get(i);
1541                     if (r.getInclusion().getTargetDescriptors().contains(sd)) {
1542                         for(int j=0;j<mun.numUpdates();j++) {
1543                             UpdateNode un=mun.getUpdate(j);
1544                             if (un.getRule()==r) {
1545                                 /* Update for rule rule r */
1546                                 String name=(String)updatenames.get(un);
1547                                 cr.outputline("RepairHashaddset("+repairtable.getSafeSymbol()+","+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1548                             }
1549                         }
1550                     }
1551                 }
1552             }
1553         } else {
1554             /* Generate update */
1555             if (ip.setexpr instanceof ImageSetExpr) {
1556                 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1557                 VarDescriptor rightvar=ise.getVar();
1558                 boolean inverse=ise.inverted();
1559                 RelationDescriptor rd=ise.getRelation();
1560                 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1561                 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1562                 if (inverse) {
1563                     if (usageimage)
1564                         cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hash, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1565                     if (usageinvimage)
1566                         cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hashinv, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1567                 } else {
1568                     if (usageimage)
1569                         cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
1570                     if (usageinvimage)
1571                         cr.outputline("SimpleHashadd("+rd.getSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1572                 }
1573                 UpdateNode un=mun.getUpdate(0);
1574                 String name=(String)updatenames.get(un);
1575                 if (inverse) {
1576                     cr.outputline(name+"(thisvar,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1577                 } else {
1578                     cr.outputline(name+"(thisvar,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1579                 }
1580             } else {
1581                 SetDescriptor sd=ip.setexpr.sd;
1582                 cr.outputline("SimpleHashadd("+sd.getSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
1583
1584                 UpdateNode un=mun.getUpdate(0);
1585                 /* Update for rule rule r */
1586                 String name=(String)updatenames.get(un);
1587                 cr.outputline(name+"(thisvar,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1588             }
1589         }
1590     }
1591
1592     public static Vector getrulelist(Descriptor d) {
1593         Vector dispatchrules = new Vector();
1594         Vector rules = State.currentState.vRules;
1595
1596         for (int i = 0; i < rules.size(); i++) {
1597             Rule rule = (Rule) rules.elementAt(i);
1598             Set requiredsymbols = rule.getRequiredDescriptors();
1599
1600             // #TBD#: in general this is wrong because these descriptors may contain descriptors
1601             // bound in "in?" expressions which need to be dealt with in a topologically sorted
1602             // fashion...
1603
1604             if (rule.getRequiredDescriptors().contains(d)) {
1605                 dispatchrules.addElement(rule);
1606             }
1607         }
1608         return dispatchrules;
1609     }
1610
1611     private boolean need_compensation(Rule r) {
1612         if (!Compiler.REPAIR)
1613             return false;
1614         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1615         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1616             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1617             GraphNode gn2=edge.getTarget();
1618             if (!removed.contains(gn2)) {
1619                 TermNode tn2=(TermNode)gn2.getOwner();
1620                 if (tn2.getType()==TermNode.CONSEQUENCE)
1621                     return false;
1622             }
1623         }
1624         return true;
1625     }
1626
1627     private UpdateNode find_compensation(Rule r) {
1628         GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1629         for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1630             GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1631             GraphNode gn2=edge.getTarget();
1632             if (!removed.contains(gn2)) {
1633                 TermNode tn2=(TermNode)gn2.getOwner();
1634                 if (tn2.getType()==TermNode.UPDATE) {
1635                     MultUpdateNode mun=tn2.getUpdate();
1636                     for(int i=0;i<mun.numUpdates();i++) {
1637                         UpdateNode un=mun.getUpdate(i);
1638                         if (un.getRule()==r)
1639                             return un;
1640                     }
1641                 }
1642             }
1643         }
1644         throw new Error("No Compensation Update could be found");
1645     }
1646
1647     public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
1648         boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1649         boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1650
1651         if (!(usageinvimage||usageimage)) /* not used at all*/
1652             return;
1653
1654         cr.outputline("/* RELATION DISPATCH */");
1655         if (Compiler.REPAIR) {
1656             cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1657             if (usageimage)
1658                 cr.outputline("!SimpleHashcontainskeydata("+oldmodel.getSafeSymbol()+"->"+rd.getJustSafeSymbol() + "_hash, "+leftvar+","+rightvar+"))");
1659             else
1660                 cr.outputline("!SimpleHashcontainskeydata("+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv, "+rightvar+","+leftvar+"))");
1661
1662             cr.startblock(); {
1663                 /* Adding new item */
1664                 /* Perform safety checks */
1665                 cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1666                 cr.outputline("RepairHashcontainsrelation("+repairtable.getSafeSymbol()+","+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
1667                 cr.startblock(); {
1668                     /* Have update to call into */
1669                     VarDescriptor mdfyptr=VarDescriptor.makeNew("modifyptr");
1670                     VarDescriptor ismdfyptr=VarDescriptor.makeNew("ismodifyptr");
1671                     cr.addDeclaration("int ",ismdfyptr.getSafeSymbol());
1672                     cr.outputline(ismdfyptr.getSafeSymbol()+"=RepairHashismodify("+repairtable.getSafeSymbol()+","+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1673
1674
1675
1676
1677                     String parttype="";
1678                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1679                         if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1680                             parttype=parttype+", int, int";
1681                         else
1682                             parttype=parttype+", int";
1683                     }
1684
1685                     VarDescriptor tmpptr=VarDescriptor.makeNew("tempupdateptr");
1686
1687                     String methodcall="(thisvar,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1688                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1689                         Quantifier q=currentrule.getQuantifier(i);
1690                         if (q instanceof SetQuantifier) {
1691                             SetQuantifier sq=(SetQuantifier) q;
1692                             methodcall+=","+sq.getVar().getSafeSymbol();
1693                         } else if (q instanceof RelationQuantifier) {
1694                             RelationQuantifier rq=(RelationQuantifier) q;
1695                             methodcall+=","+rq.x.getSafeSymbol();
1696                             methodcall+=","+rq.y.getSafeSymbol();
1697                         } else if (q instanceof ForQuantifier) {
1698                             ForQuantifier fq=(ForQuantifier) q;
1699                             methodcall+=","+fq.getVar().getSafeSymbol();
1700                         }
1701                     }
1702
1703
1704
1705                     cr.addDeclaration("void *",tmpptr.getSafeSymbol());
1706                     cr.outputline(tmpptr.getSafeSymbol()+"=");
1707                     cr.outputline("(void *) RepairHashgetrelation("+repairtable.getSafeSymbol()+","+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1708                     cr.outputline("if ("+ismdfyptr.getSafeSymbol()+")");
1709                     {
1710                         VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1711                         String methodcallprefix="("+funptr.getSafeSymbol()+") ";
1712                         cr.startblock();
1713                         cr.addDeclaration("int",mdfyptr.getSafeSymbol());
1714                         cr.outputline(mdfyptr.getSafeSymbol()+"=RepairHashgetrelation2("+repairtable.getSafeSymbol()+","+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1715                         cr.addDeclaration("void (*"+funptr.getSafeSymbol()+") (struct "+name+"_state *, struct "+name+"*, struct RepairHash *"+parttype+",int,int,int);");
1716                         cr.outputline(funptr.getSafeSymbol()+"="+"(void (*) (struct "+name+"_state *, struct "+name+"*, struct RepairHash *"+parttype+",int,int,int)) "+tmpptr.getSafeSymbol()+";");
1717                         cr.outputline(methodcallprefix+methodcall+","+leftvar+", "+rightvar+", "+mdfyptr.getSafeSymbol() +");");
1718                         cr.endblock();
1719                     }
1720                     cr.outputline("else ");
1721                     {
1722                         VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1723                         String methodcallprefix="("+funptr.getSafeSymbol()+") ";
1724                         cr.startblock();
1725                         cr.addDeclaration("void (*"+funptr.getSafeSymbol()+") (struct "+name+"_state *, struct "+name+"*,struct RepairHash *"+parttype+");");
1726                         cr.outputline(funptr.getSafeSymbol()+"="+"(void (*) (struct "+name+"_state *,struct "+name+"*,struct RepairHash *"+parttype+")) "+tmpptr.getSafeSymbol()+";");
1727                         cr.outputline(methodcallprefix+methodcall+");");
1728                         cr.endblock();
1729                     }
1730                     cr.outputline("free"+name+"("+newmodel.getSafeSymbol()+");");
1731                     cr.outputline("goto rebuild;");
1732                 }
1733                 cr.endblock();
1734
1735                 /* Build standard compensation actions */
1736                 if (need_compensation(currentrule)) {
1737                     UpdateNode un=find_compensation(currentrule);
1738                     String name=(String)updatenames.get(un);
1739                     usedupdates.add(un); /* Mark as used */
1740                     String methodcall=name+"(thisvar,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1741                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1742                         Quantifier q=currentrule.getQuantifier(i);
1743                         if (q instanceof SetQuantifier) {
1744                             SetQuantifier sq=(SetQuantifier) q;
1745                             methodcall+=","+sq.getVar().getSafeSymbol();
1746                         } else if (q instanceof RelationQuantifier) {
1747                             RelationQuantifier rq=(RelationQuantifier) q;
1748                             methodcall+=","+rq.x.getSafeSymbol();
1749                             methodcall+=","+rq.y.getSafeSymbol();
1750                         } else if (q instanceof ForQuantifier) {
1751                             ForQuantifier fq=(ForQuantifier) q;
1752                             methodcall+=","+fq.getVar().getSafeSymbol();
1753                         }
1754                     }
1755                     methodcall+=");";
1756                     cr.outputline(methodcall);
1757                     cr.outputline("free"+name+"("+newmodel.getSafeSymbol()+");");
1758                     cr.outputline("goto rebuild;");
1759                 }
1760             }
1761             cr.endblock();
1762         }
1763
1764         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1765         cr.startblock();
1766         cr.addDeclaration("int" , addeditem);
1767         cr.outputline(addeditem + "=0;");
1768
1769         String ifstring="if (!maybe";
1770         if (rd.getDomain().getType() instanceof StructureTypeDescriptor)  {
1771             ifstring+="&&"+leftvar;
1772         }
1773
1774         if (rd.getRange().getType() instanceof StructureTypeDescriptor)  {
1775             ifstring+="&&"+rightvar;
1776         }
1777
1778         ifstring+=")";
1779
1780         if (rd.testUsage(RelationDescriptor.IMAGE)) {
1781             cr.outputline(ifstring);
1782             cr.outputline(addeditem + " = SimpleHashadd("+rd.getSafeSymbol()+"_hash, (int)" + leftvar + ", (int)" + rightvar+ ");");
1783         }
1784
1785         if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1786             cr.outputline(ifstring);
1787             cr.outputline(addeditem + " = SimpleHashadd("+rd.getSafeSymbol()+"_hashinv, (int)" + rightvar + ", (int)" + leftvar + ");");
1788         }
1789
1790
1791         Vector dispatchrules = getrulelist(rd);
1792
1793         Set toremove=new HashSet();
1794         for(int i=0;i<dispatchrules.size();i++) {
1795             Rule r=(Rule)dispatchrules.get(i);
1796             if (!ruleset.contains(r))
1797                 toremove.add(r);
1798         }
1799         dispatchrules.removeAll(toremove);
1800         if (dispatchrules.size() == 0) {
1801             cr.outputline("/* nothing to dispatch */");
1802             cr.endblock();
1803             return;
1804         }
1805
1806         cr.outputline("if (" + addeditem + ")");
1807         cr.startblock();
1808
1809         for(int i = 0; i < dispatchrules.size(); i++) {
1810             Rule rule = (Rule) dispatchrules.elementAt(i);
1811             if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
1812                 /* Guard depends on this relation, so we recomput everything */
1813                 cr.outputline("WorkListadd("+worklist.getSafeSymbol()+","+rule.getNum()+",-1,0,0);");
1814             } else {
1815                 for (int j=0;j<rule.numQuantifiers();j++) {
1816                     Quantifier q=rule.getQuantifier(j);
1817                     if (q.getRequiredDescriptors().contains(rd)) {
1818                         /* Generate add */
1819                         cr.outputline("WorkListadd("+worklist.getSafeSymbol()+","+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1820                     }
1821                 }
1822             }
1823         }
1824         cr.endblock();
1825         cr.endblock();
1826     }
1827
1828
1829     public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1830         cr.outputline("/* SET DISPATCH */");
1831         if (Compiler.REPAIR) {
1832             cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1833             cr.outputline("!SimpleHashcontainskey("+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash, "+setvar+"))");
1834             cr.startblock(); {
1835                 /* Adding new item */
1836                 /* See if there is an outstanding update in the repairtable */
1837                 cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1838                 cr.outputline("RepairHashcontainsset("+repairtable.getSafeSymbol()+","+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
1839                 cr.startblock(); {
1840                     /* Have update to call into */
1841                     VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1842                     String parttype="";
1843                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1844                         if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1845                             parttype=parttype+", int, int";
1846                         else
1847                             parttype=parttype+", int";
1848                     }
1849                     cr.addDeclaration("void (*"+funptr.getSafeSymbol()+") (struct "+name+"_state *,struct "+name+"*,struct RepairHash *"+parttype+");");
1850                     cr.outputline(funptr.getSafeSymbol()+"=");
1851                     cr.outputline("(void (*) (struct "+name+"_state *,struct "+name+"*,struct RepairHash *"+parttype+")) RepairHashgetset("+repairtable.getSafeSymbol()+","+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
1852                     String methodcall="("+funptr.getSafeSymbol()+") (thisvar,"+oldmodel.getSafeSymbol()+","+
1853                         repairtable.getSafeSymbol();
1854                     for(int i=0;i<currentrule.numQuantifiers();i++) {
1855                         Quantifier q=currentrule.getQuantifier(i);
1856                         if (q instanceof SetQuantifier) {
1857                             SetQuantifier sq=(SetQuantifier) q;
1858                             methodcall+=","+sq.getVar().getSafeSymbol();
1859                         } else if (q instanceof RelationQuantifier) {
1860                             RelationQuantifier rq=(RelationQuantifier) q;
1861                             methodcall+=","+rq.x.getSafeSymbol();
1862                             methodcall+=","+rq.y.getSafeSymbol();
1863                         } else if (q instanceof ForQuantifier) {
1864                             ForQuantifier fq=(ForQuantifier) q;
1865                             methodcall+=","+fq.getVar().getSafeSymbol();
1866                         }
1867                     }
1868                     methodcall+=");";
1869                     cr.outputline(methodcall);
1870                     cr.outputline("free"+name+"("+newmodel.getSafeSymbol()+");");
1871                     cr.outputline("goto rebuild;");
1872                 }
1873                 cr.endblock();
1874                 /* Build standard compensation actions */
1875                 Vector ruleset=new Vector();
1876                 ruleset.add(currentrule);
1877                 if (state.implicitruleinv.containsKey(currentrule))
1878                     ruleset.addAll((Set)state.implicitruleinv.get(currentrule));
1879                 for(int i=0;i<ruleset.size();i++) {
1880                     Rule itrule=(Rule)ruleset.get(i);
1881
1882                     if (need_compensation(itrule)) {
1883                         UpdateNode un=find_compensation(itrule);
1884                         String name=(String)updatenames.get(un);
1885                         usedupdates.add(un); /* Mark as used */
1886
1887                         String methodcall=name+"(thisvar,"+oldmodel.getSafeSymbol()+","+
1888                             repairtable.getSafeSymbol();
1889                         for(int j=0;j<currentrule.numQuantifiers();j++) {
1890                             Quantifier q=currentrule.getQuantifier(j);
1891                             if (q instanceof SetQuantifier) {
1892                                 SetQuantifier sq=(SetQuantifier) q;
1893                                 methodcall+=","+sq.getVar().getSafeSymbol();
1894                             } else if (q instanceof RelationQuantifier) {
1895                                 RelationQuantifier rq=(RelationQuantifier) q;
1896                                 methodcall+=","+rq.x.getSafeSymbol();
1897                                 methodcall+=","+rq.y.getSafeSymbol();
1898                             } else if (q instanceof ForQuantifier) {
1899                                 ForQuantifier fq=(ForQuantifier) q;
1900                                 methodcall+=","+fq.getVar().getSafeSymbol();
1901                             }
1902                         }
1903                         methodcall+=");";
1904                         if (currentrule!=itrule) {
1905                             SetDescriptor sdrule=((SetInclusion)itrule.getInclusion()).getSet();
1906                             cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1907                             cr.outputline("!SimpleHashcontainskey("+ oldmodel.getSafeSymbol() +"->"+sdrule.getJustSafeSymbol() +"_hash,"+setvar+"))");
1908                             cr.startblock();
1909                         }
1910                         cr.outputline(methodcall);
1911                         cr.outputline("free"+name+"("+newmodel.getSafeSymbol()+");");
1912                         cr.outputline("goto rebuild;");
1913                         cr.endblock();
1914                     }
1915                     if (currentrule==itrule)
1916                         cr.endblock();
1917                 }
1918             }
1919         }
1920
1921         cr.startblock();
1922         String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1923         cr.addDeclaration("int", addeditem);
1924         cr.outputline(addeditem + " = 0;");
1925         if (sd.getType() instanceof StructureTypeDescriptor)  {
1926             cr.outputline("if (!maybe&&"+setvar+")");
1927         } else
1928             cr.outputline("if (!maybe)");
1929         cr.outputline(addeditem + " = SimpleHashadd("+sd.getSafeSymbol()+"_hash, (int)" + setvar +  ", (int)" + setvar + ");");
1930         cr.startblock();
1931         Vector dispatchrules = getrulelist(sd);
1932
1933         Set toremove=new HashSet();
1934         for(int i=0;i<dispatchrules.size();i++) {
1935             Rule r=(Rule)dispatchrules.get(i);
1936             if (!ruleset.contains(r))
1937                 toremove.add(r);
1938         }
1939         dispatchrules.removeAll(toremove);
1940
1941         if (dispatchrules.size() == 0) {
1942             cr.outputline("/* nothing to dispatch */");
1943             cr.endblock();
1944             cr.endblock();
1945             return;
1946         }
1947         /* Add item to worklist if new */
1948         cr.outputline("if ("+addeditem+")");
1949         cr.startblock();
1950         for(int i = 0; i < dispatchrules.size(); i++) {
1951             Rule rule = (Rule) dispatchrules.elementAt(i);
1952             if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
1953                 /* Guard depends on this relation, so we recompute everything */
1954                 cr.outputline("WorkListadd("+worklist.getSafeSymbol()+","+rule.getNum()+",-1,0,0);");
1955             } else {
1956                 for (int j=0;j<rule.numQuantifiers();j++) {
1957                     Quantifier q=rule.getQuantifier(j);
1958                     if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1959                         /* Generate add */
1960                         cr.outputline("WorkListadd("+worklist.getSafeSymbol()+","+rule.getNum()+","+j+","+setvar+",0);");
1961                     }
1962                 }
1963             }
1964         }
1965         cr.endblock();
1966         cr.endblock();
1967         cr.endblock();
1968     }
1969 }