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