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