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