7 public class RepairGenerator {
9 java.io.PrintWriter outputrepair = null;
10 java.io.PrintWriter outputaux = null;
11 java.io.PrintWriter outputhead = null;
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;
22 Termination termination;
24 static boolean DEBUG=false;
28 public RepairGenerator(State state, Termination t) {
30 updatenames=new Hashtable();
31 usedupdates=new HashSet();
35 sources=new Sources(state);
36 Repair.repairgenerator=this;
39 private void name_updates() {
41 for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
42 GraphNode gn=(GraphNode) it.next();
43 TermNode tn=(TermNode) gn.getOwner();
44 MultUpdateNode mun=tn.getUpdate();
45 for (int i=0;i<mun.numUpdates();i++) {
46 UpdateNode un=mun.getUpdate(i);
47 String name="update"+String.valueOf(count++);
48 updatenames.put(un,name);
53 public void generate(OutputStream outputrepair, OutputStream outputaux,OutputStream outputhead, String st) {
54 this.outputrepair = new java.io.PrintWriter(outputrepair, true);
55 this.outputaux = new java.io.PrintWriter(outputaux, true);
56 this.outputhead = new java.io.PrintWriter(outputhead, true);
60 generate_tokentable();
61 generate_hashtables();
62 generate_stateobject();
68 CodeWriter crhead = new StandardCodeWriter(this.outputhead);
69 CodeWriter craux = new StandardCodeWriter(this.outputaux);
70 crhead.outputline("};");
71 craux.outputline("};");
76 private void generate_call() {
77 CodeWriter cr = new StandardCodeWriter(outputrepair);
78 VarDescriptor vdstate=VarDescriptor.makeNew("repairstate");
79 cr.outputline(name+"_state * "+vdstate.getSafeSymbol()+"=new "+name+"_state();");
80 Iterator globals=state.stGlobals.descriptors();
81 while (globals.hasNext()) {
82 VarDescriptor vd=(VarDescriptor) globals.next();
83 cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
85 /* Insert repair here */
86 cr.outputline(vdstate.getSafeSymbol()+"->doanalysis();");
87 globals=state.stGlobals.descriptors();
88 while (globals.hasNext()) {
89 VarDescriptor vd=(VarDescriptor) globals.next();
90 cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";");
92 cr.outputline("delete "+vdstate.getSafeSymbol()+";");
95 private void generate_tokentable() {
96 CodeWriter cr = new StandardCodeWriter(outputrepair);
97 Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();
100 cr.outputline("// Token values");
103 while (tokens.hasNext()) {
104 Object token = tokens.next();
105 cr.outputline("// " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString());
112 private void generate_stateobject() {
113 CodeWriter crhead = new StandardCodeWriter(outputhead);
114 crhead.outputline("class "+name+"_state {");
115 crhead.outputline("public:");
116 Iterator globals=state.stGlobals.descriptors();
117 while (globals.hasNext()) {
118 VarDescriptor vd=(VarDescriptor) globals.next();
119 crhead.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+";");
123 private void generate_hashtables() {
124 CodeWriter craux = new StandardCodeWriter(outputaux);
125 CodeWriter crhead = new StandardCodeWriter(outputhead);
126 crhead.outputline("#include \"SimpleHash.h\"");
127 crhead.outputline("#include <stdio.h>");
128 crhead.outputline("#include <stdlib.h>");
129 crhead.outputline("class "+name+" {");
130 crhead.outputline("public:");
131 crhead.outputline(name+"();");
132 crhead.outputline("~"+name+"();");
133 craux.outputline("#include \""+headername+"\"");
135 craux.outputline(name+"::"+name+"() {");
136 craux.outputline("// creating hashtables ");
139 Iterator sets = state.stSets.descriptors();
141 /* first pass create all the hash tables */
142 while (sets.hasNext()) {
143 SetDescriptor set = (SetDescriptor) sets.next();
144 crhead.outputline("SimpleHash* " + set.getSafeSymbol() + "_hash;");
145 craux.outputline(set.getSafeSymbol() + "_hash = new SimpleHash();");
148 /* second pass build relationships between hashtables */
149 sets = state.stSets.descriptors();
151 while (sets.hasNext()) {
152 SetDescriptor set = (SetDescriptor) sets.next();
153 Iterator subsets = set.subsets();
155 while (subsets.hasNext()) {
156 SetDescriptor subset = (SetDescriptor) subsets.next();
157 craux.outputline(subset.getSafeSymbol() + "_hash->addParent(" + set.getSafeSymbol() + "_hash);");
161 /* build relations */
162 Iterator relations = state.stRelations.descriptors();
164 /* first pass create all the hash tables */
165 while (relations.hasNext()) {
166 RelationDescriptor relation = (RelationDescriptor) relations.next();
168 if (relation.testUsage(RelationDescriptor.IMAGE)) {
169 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hash;");
170 craux.outputline(relation.getSafeSymbol() + "_hash = new SimpleHash();");
173 if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
174 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hashinv;");
175 craux.outputline(relation.getSafeSymbol() + "_hashinv = new SimpleHash();");
179 craux.outputline("}");
180 crhead.outputline("};");
181 craux.outputline(name+"::~"+name+"() {");
182 craux.outputline("// deleting hashtables");
184 /* build destructor */
185 sets = state.stSets.descriptors();
187 /* first pass create all the hash tables */
188 while (sets.hasNext()) {
189 SetDescriptor set = (SetDescriptor) sets.next();
190 craux.outputline("delete "+set.getSafeSymbol() + "_hash;");
193 /* destroy relations */
194 relations = state.stRelations.descriptors();
196 /* first pass create all the hash tables */
197 while (relations.hasNext()) {
198 RelationDescriptor relation = (RelationDescriptor) relations.next();
200 if (relation.testUsage(RelationDescriptor.IMAGE)) {
201 craux.outputline("delete "+relation.getSafeSymbol() + "_hash;");
204 if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
205 craux.outputline("delete " + relation.getSafeSymbol() + ";");
208 craux.outputline("}");
211 private void generate_worklist() {
212 CodeWriter crhead = new StandardCodeWriter(outputhead);
213 CodeWriter craux = new StandardCodeWriter(outputaux);
214 oldmodel=VarDescriptor.makeNew("oldmodel");
215 newmodel=VarDescriptor.makeNew("newmodel");
216 worklist=VarDescriptor.makeNew("worklist");
217 goodflag=VarDescriptor.makeNew("goodflag");
218 repairtable=VarDescriptor.makeNew("repairtable");
219 crhead.outputline("void doanalysis();");
220 craux.outputline("void "+name +"_state::doanalysis()");
222 craux.outputline(name+ " * "+oldmodel.getSafeSymbol()+"=0;");
223 craux.outputline("WorkList * "+worklist.getSafeSymbol()+" = new WorkList();");
224 craux.outputline("RepairHash * "+repairtable.getSafeSymbol()+"=0;");
225 craux.outputline("while (1)");
227 craux.outputline("int "+goodflag.getSafeSymbol()+"=1;");
228 craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
231 private void generate_teardown() {
232 CodeWriter cr = new StandardCodeWriter(outputaux);
233 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
234 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
235 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
236 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
237 cr.outputline("delete "+newmodel.getSafeSymbol()+";");
238 cr.outputline("delete "+worklist.getSafeSymbol()+";");
242 private void generate_rules() {
243 /* first we must sort the rules */
244 Iterator allrules = state.vRules.iterator();
245 Vector emptyrules = new Vector(); // rules with no quantifiers
246 Vector worklistrules = new Vector(); // the rest of the rules
247 RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
248 SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
250 while (allrules.hasNext()) {
251 Rule rule = (Rule) allrules.next();
252 ListIterator quantifiers = rule.quantifiers();
253 boolean noquantifiers = true;
254 while (quantifiers.hasNext()) {
255 Quantifier quantifier = (Quantifier) quantifiers.next();
256 if (quantifier instanceof ForQuantifier) {
257 // ok, because integers exist already!
260 noquantifiers = false;
265 emptyrules.add(rule);
267 worklistrules.add(rule);
271 Iterator iterator_er = emptyrules.iterator();
272 while (iterator_er.hasNext()) {
273 Rule rule = (Rule) iterator_er.next();
275 final SymbolTable st = rule.getSymbolTable();
276 CodeWriter cr = new StandardCodeWriter(outputaux) {
277 public SymbolTable getSymbolTable() { return st; }
279 cr.outputline("// build " +escape(rule.toString()));
281 ListIterator quantifiers = rule.quantifiers();
282 while (quantifiers.hasNext()) {
283 Quantifier quantifier = (Quantifier) quantifiers.next();
284 quantifier.generate_open(cr);
289 rule.getGuardExpr().prettyPrint(cr);
292 /* now we have to generate the guard test */
293 VarDescriptor guardval = VarDescriptor.makeNew();
294 rule.getGuardExpr().generate(cr, guardval);
295 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
298 /* now we have to generate the inclusion code */
300 rule.getInclusion().generate(cr);
302 while (quantifiers.hasPrevious()) {
303 Quantifier quantifier = (Quantifier) quantifiers.previous();
312 CodeWriter cr2 = new StandardCodeWriter(outputaux);
314 cr2.outputline("while ("+goodflag.getSafeSymbol()+"&&"+worklist.getSafeSymbol()+"->hasMoreElements())");
316 VarDescriptor idvar=VarDescriptor.makeNew("id");
317 cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
319 String elseladder = "if";
321 Iterator iterator_rules = worklistrules.iterator();
322 while (iterator_rules.hasNext()) {
324 Rule rule = (Rule) iterator_rules.next();
325 int dispatchid = rule.getNum();
328 final SymbolTable st = rule.getSymbolTable();
329 CodeWriter cr = new StandardCodeWriter(outputaux) {
330 public SymbolTable getSymbolTable() { return st; }
334 cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
336 VarDescriptor typevar=VarDescriptor.makeNew("type");
337 VarDescriptor leftvar=VarDescriptor.makeNew("left");
338 VarDescriptor rightvar=VarDescriptor.makeNew("right");
339 cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
340 cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
341 cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
342 cr.outputline("// build " +escape(rule.toString()));
345 for (int j=0;j<rule.numQuantifiers();j++) {
346 Quantifier quantifier = rule.getQuantifier(j);
347 quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
353 rule.getGuardExpr().prettyPrint(cr);
356 /* now we have to generate the guard test */
358 VarDescriptor guardval = VarDescriptor.makeNew();
359 rule.getGuardExpr().generate(cr, guardval);
361 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
364 /* now we have to generate the inclusion code */
366 rule.getInclusion().generate(cr);
369 for (int j=0;j<rule.numQuantifiers();j++) {
373 // close startblocks generated by DotExpr memory checks
374 //DotExpr.generate_memory_endblocks(cr);
376 cr.endblock(); // end else-if WORKLIST ladder
378 elseladder = "else if";
382 cr2.outputline("else");
384 cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
385 cr2.outputline("exit(1);");
387 // end block created for worklist
391 public static String escape(String s) {
393 for(int i=0;i<s.length();i++) {
403 private void generate_checks() {
405 /* do constraint checks */
406 Vector constraints = state.vConstraints;
408 for (int i = 0; i < constraints.size(); i++) {
410 Constraint constraint = (Constraint) constraints.elementAt(i);
414 final SymbolTable st = constraint.getSymbolTable();
416 CodeWriter cr = new StandardCodeWriter(outputaux) {
417 public SymbolTable getSymbolTable() { return st; }
420 cr.outputline("// checking " + escape(constraint.toString()));
423 ListIterator quantifiers = constraint.quantifiers();
425 while (quantifiers.hasNext()) {
426 Quantifier quantifier = (Quantifier) quantifiers.next();
427 quantifier.generate_open(cr);
430 cr.outputline("int maybe = 0;");
432 /* now we have to generate the guard test */
434 VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
435 constraint.getLogicStatement().generate(cr, constraintboolean);
437 cr.outputline("if (maybe)");
439 cr.outputline("printf(\"maybe fail " + escape(constraint.toString()) + ". \");");
440 cr.outputline("exit(1);");
443 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
446 cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \");");
449 /* Build new repair table */
450 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
451 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
452 cr.outputline(repairtable.getSafeSymbol()+"=new RepairHash();");
455 /* Compute cost of each repair */
456 VarDescriptor mincost=VarDescriptor.makeNew("mincost");
457 VarDescriptor mincostindex=VarDescriptor.makeNew("mincostindex");
458 DNFConstraint dnfconst=constraint.dnfconstraint;
459 cr.outputline("int "+mincostindex.getSafeSymbol()+";");
460 if (dnfconst.size()>1) {
462 for(int j=0;j<dnfconst.size();j++) {
463 Conjunction conj=dnfconst.get(j);
464 GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
465 if (removed.contains(gn))
468 VarDescriptor costvar;
472 costvar=VarDescriptor.makeNew("cost");
473 for(int k=0;k<conj.size();k++) {
474 DNFPredicate dpred=conj.get(k);
475 Predicate p=dpred.getPredicate();
476 boolean negate=dpred.isNegated();
477 VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
478 p.generate(cr,predvalue);
480 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
482 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
484 cr.outputline("int "+costvar.getSafeSymbol()+"="+cost.getCost(dpred)+";");
486 cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
490 cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
492 cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
493 cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
496 cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
500 cr.outputline("switch("+mincostindex.getSafeSymbol()+") {");
501 for(int j=0;j<dnfconst.size();j++) {
502 Conjunction conj=dnfconst.get(j);
503 GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj); if (removed.contains(gn))
505 cr.outputline("case "+j+":");
506 for(int k=0;k<conj.size();k++) {
507 DNFPredicate dpred=conj.get(k);
508 Predicate p=dpred.getPredicate();
509 boolean negate=dpred.isNegated();
510 VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
511 p.generate(cr,predvalue);
513 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
515 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
516 if (p instanceof InclusionPredicate)
517 generateinclusionrepair(conj,dpred, cr);
518 else if (p instanceof ExprPredicate) {
519 ExprPredicate ep=(ExprPredicate)p;
520 if (ep.getType()==ExprPredicate.SIZE)
521 generatesizerepair(conj,dpred,cr);
522 else if (ep.getType()==ExprPredicate.COMPARISON)
523 generatecomparisonrepair(conj,dpred,cr);
524 } else throw new Error("Unrecognized Predicate");
528 cr.outputline("break;");
532 cr.outputline(goodflag.getSafeSymbol()+"=0;");
533 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
534 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
535 cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
536 cr.outputline("break;"); /* Rebuild model and all */
540 while (quantifiers.hasPrevious()) {
541 Quantifier quantifier = (Quantifier) quantifiers.previous();
544 cr.outputline("if ("+goodflag.getSafeSymbol()+")");
545 cr.outputline("break;");
553 private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
554 MultUpdateNode mun=null;
555 GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
557 for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
558 GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
559 TermNode tn2=(TermNode)gn2.getOwner();
560 if (tn2.getType()==TermNode.ABSTRACT) {
561 AbstractRepair ar=tn2.getAbstract();
562 if (((repairtype==-1)||(ar.getType()==repairtype))&&
563 ar.getPredicate()==dpred) {
564 for(Iterator edgeit2=gn2.edges();edgeit.hasNext();) {
565 GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
566 if (!removed.contains(gn3)) {
567 TermNode tn3=(TermNode)gn3.getOwner();
568 if (tn3.getType()==TermNode.UPDATE) {
580 public void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
581 MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
582 MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
583 ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
584 RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
585 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
586 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
587 boolean inverted=ep.inverted();
588 boolean negated=dpred.isNegated();
589 OpExpr expr=(OpExpr)ep.expr;
590 Opcode opcode=expr.getOpcode();
591 VarDescriptor leftside=VarDescriptor.makeNew("leftside");
592 VarDescriptor rightside=VarDescriptor.makeNew("rightside");
593 VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
595 expr.getLeftExpr().generate(cr,leftside);
596 expr.getRightExpr().generate(cr,newvalue);
597 cr.outputline(rd.getRange().getType().getGenerateType().getSafeSymbol()+" "+rightside.getSafeSymbol()+";");
598 cr.outputline(rd.getSafeSymbol()+"_hash->get("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
600 expr.getLeftExpr().generate(cr,rightside);
601 expr.getRightExpr().generate(cr,newvalue);
602 cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
603 cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+leftside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
606 if (opcode==Opcode.GT) {
608 } else if (opcode==Opcode.GE) {
610 } else if (opcode==Opcode.LT) {
612 } else if (opcode==Opcode.LE) {
614 } else if (opcode==Opcode.EQ) {
616 } else if (opcode==Opcode.NE) {
619 throw new Error("Unrecognized Opcode");
622 if (opcode==Opcode.GT) {
623 cr.outputline(newvalue.getSafeSymbol()+"++;");
624 } else if (opcode==Opcode.GE) {
626 } else if (opcode==Opcode.LT) {
627 cr.outputline(newvalue.getSafeSymbol()+"--;");
628 } else if (opcode==Opcode.LE) {
630 } else if (opcode==Opcode.EQ) {
632 } else if (opcode==Opcode.NE) {
633 cr.outputline(newvalue.getSafeSymbol()+"++;");
635 throw new Error("Unrecognized Opcode");
637 /* Do abstract repairs */
639 cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
641 cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
643 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
647 cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
649 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
651 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
654 /* Do concrete repairs */
655 /* Start with scheduling removal */
656 for(int i=0;i<state.vRules.size();i++) {
657 Rule r=(Rule)state.vRules.get(i);
658 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
659 for(int j=0;j<munremove.numUpdates();j++) {
660 UpdateNode un=munremove.getUpdate(i);
661 if (un.getRule()==r) {
662 /* Update for rule r */
663 String name=(String)updatenames.get(un);
664 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
669 /* Now do addition */
670 UpdateNode un=munadd.getUpdate(0);
671 String name=(String)updatenames.get(un);
673 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
675 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
679 public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {
680 ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
681 OpExpr expr=(OpExpr)ep.expr;
682 Opcode opcode=expr.getOpcode();
684 boolean negated=dpred.isNegated();
686 if (opcode==Opcode.GT) {
688 } else if (opcode==Opcode.GE) {
690 } else if (opcode==Opcode.LT) {
692 } else if (opcode==Opcode.LE) {
694 } else if (opcode==Opcode.EQ) {
696 } else if (opcode==Opcode.NE) {
699 throw new Error("Unrecognized Opcode");
702 MultUpdateNode munremove;
704 MultUpdateNode munadd;
705 if (ep.getDescriptor() instanceof RelationDescriptor) {
706 munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
707 munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
709 munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
710 munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
712 int size=ep.leftsize();
713 VarDescriptor sizevar=VarDescriptor.makeNew("size");
714 ((OpExpr)expr).left.generate(cr, sizevar);
715 VarDescriptor change=VarDescriptor.makeNew("change");
716 cr.outputline("int "+change.getSafeSymbol()+";");
717 boolean generateadd=false;
718 boolean generateremove=false;
719 if (opcode==Opcode.GT) {
720 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
722 generateremove=false;
723 } else if (opcode==Opcode.GE) {
724 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
726 generateremove=false;
727 } else if (opcode==Opcode.LT) {
728 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
731 } else if (opcode==Opcode.LE) {
732 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
735 } else if (opcode==Opcode.EQ) {
736 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
739 } else if (opcode==Opcode.NE) {
740 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
742 generateremove=false;
744 throw new Error("Unrecognized Opcode");
746 Descriptor d=ep.getDescriptor();
747 if (generateremove) {
748 cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
750 /* Find element to remove */
751 VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
752 VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
753 if (d instanceof RelationDescriptor) {
755 rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
756 cr.outputline("int "+leftvar.getSafeSymbol()+";");
757 cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
759 leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
760 cr.outputline("int "+rightvar.getSafeSymbol()+";");
761 cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
764 cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
766 /* Generate abstract remove instruction */
767 if (d instanceof RelationDescriptor) {
768 RelationDescriptor rd=(RelationDescriptor) d;
769 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
770 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
772 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
774 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
776 cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
778 /* Generate concrete remove instruction */
779 for(int i=0;i<state.vRules.size();i++) {
780 Rule r=(Rule)state.vRules.get(i);
781 if (r.getInclusion().getTargetDescriptors().contains(d)) {
782 for(int j=0;j<munremove.numUpdates();j++) {
783 UpdateNode un=munremove.getUpdate(i);
784 if (un.getRule()==r) {
785 /* Update for rule rule r */
786 String name=(String)updatenames.get(un);
787 if (d instanceof RelationDescriptor) {
788 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
790 cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
799 cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
805 public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
806 InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate();
807 boolean negated=dpred.isNegated();
808 MultUpdateNode mun=getmultupdatenode(conj,dpred,-1);
809 VarDescriptor leftvar=VarDescriptor.makeNew("left");
810 ip.expr.generate(cr, leftvar);
813 if (ip.setexpr instanceof ImageSetExpr) {
814 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
815 VarDescriptor rightvar=ise.getVar();
816 boolean inverse=ise.inverted();
817 RelationDescriptor rd=ise.getRelation();
818 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
819 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
822 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar + ", (int)" + leftvar + ");");
824 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar + ", (int)" + rightvar + ");");
827 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
829 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
831 for(int i=0;i<state.vRules.size();i++) {
832 Rule r=(Rule)state.vRules.get(i);
833 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
834 for(int j=0;j<mun.numUpdates();j++) {
835 UpdateNode un=mun.getUpdate(i);
836 if (un.getRule()==r) {
837 /* Update for rule rule r */
838 String name=(String)updatenames.get(un);
840 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
842 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
849 SetDescriptor sd=ip.setexpr.sd;
850 cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
852 for(int i=0;i<state.vRules.size();i++) {
853 Rule r=(Rule)state.vRules.get(i);
854 if (r.getInclusion().getTargetDescriptors().contains(sd)) {
855 for(int j=0;j<mun.numUpdates();j++) {
856 UpdateNode un=mun.getUpdate(i);
857 if (un.getRule()==r) {
858 /* Update for rule rule r */
859 String name=(String)updatenames.get(un);
860 cr.outputline(repairtable.getSafeSymbol()+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
867 /* Generate update */
868 if (ip.setexpr instanceof ImageSetExpr) {
869 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
870 VarDescriptor rightvar=ise.getVar();
871 boolean inverse=ise.inverted();
872 RelationDescriptor rd=ise.getRelation();
873 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
874 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
877 cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar + ", (int)" + leftvar + ");");
879 cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar + ", (int)" + rightvar + ");");
882 cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
884 cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
886 UpdateNode un=mun.getUpdate(0);
887 String name=(String)updatenames.get(un);
889 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
891 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
894 SetDescriptor sd=ip.setexpr.sd;
895 cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + leftvar + ");");
897 UpdateNode un=mun.getUpdate(0);
898 /* Update for rule rule r */
899 String name=(String)updatenames.get(un);
900 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
907 public static Vector getrulelist(Descriptor d) {
908 Vector dispatchrules = new Vector();
909 Vector rules = State.currentState.vRules;
911 for (int i = 0; i < rules.size(); i++) {
912 Rule rule = (Rule) rules.elementAt(i);
913 Set requiredsymbols = rule.getRequiredDescriptors();
915 // #TBD#: in general this is wrong because these descriptors may contain descriptors
916 // bound in "in?" expressions which need to be dealt with in a topologically sorted
919 if (rule.getRequiredDescriptors().contains(d)) {
920 dispatchrules.addElement(rule);
923 return dispatchrules;
926 private boolean need_compensation(Rule r) {
927 GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
928 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
929 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
930 GraphNode gn2=edge.getTarget();
931 if (!removed.contains(gn2)) {
932 TermNode tn2=(TermNode)gn2.getOwner();
933 if (tn2.getType()==TermNode.CONSEQUENCE)
940 private UpdateNode find_compensation(Rule r) {
941 GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
942 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
943 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
944 GraphNode gn2=edge.getTarget();
945 if (!removed.contains(gn2)) {
946 TermNode tn2=(TermNode)gn2.getOwner();
947 if (tn2.getType()==TermNode.UPDATE) {
948 MultUpdateNode mun=tn2.getUpdate();
949 for(int i=0;i<mun.numUpdates();i++) {
950 UpdateNode un=mun.getUpdate(i);
957 throw new Error("No Compensation Update could be found");
960 public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
961 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
962 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
964 if (!(usageinvimage||usageimage)) /* not used at all*/
967 cr.outputline("// RELATION DISPATCH ");
968 cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
970 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
972 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
974 /* Adding new item */
975 /* Perform safety checks */
976 cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
977 cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
979 /* Have update to call into */
980 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
982 for(int i=0;i<currentrule.numQuantifiers();i++) {
983 if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
984 parttype=parttype+", int, int";
986 parttype=parttype+", int";
988 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
989 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
990 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
991 for(int i=0;i<currentrule.numQuantifiers();i++) {
992 Quantifier q=currentrule.getQuantifier(i);
993 if (q instanceof SetQuantifier) {
994 SetQuantifier sq=(SetQuantifier) q;
995 methodcall+=","+sq.getVar().getSafeSymbol();
996 } else if (q instanceof RelationQuantifier) {
997 RelationQuantifier rq=(RelationQuantifier) q;
998 methodcall+=","+rq.x.getSafeSymbol();
999 methodcall+=","+rq.y.getSafeSymbol();
1000 } else if (q instanceof ForQuantifier) {
1001 ForQuantifier fq=(ForQuantifier) q;
1002 methodcall+=","+fq.getVar().getSafeSymbol();
1006 cr.outputline(methodcall);
1007 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1008 cr.outputline("continue;");
1011 /* Build standard compensation actions */
1012 if (need_compensation(currentrule)) {
1013 UpdateNode un=find_compensation(currentrule);
1014 String name=(String)updatenames.get(un);
1015 usedupdates.add(un); /* Mark as used */
1016 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1017 for(int i=0;i<currentrule.numQuantifiers();i++) {
1018 Quantifier q=currentrule.getQuantifier(i);
1019 if (q instanceof SetQuantifier) {
1020 SetQuantifier sq=(SetQuantifier) q;
1021 methodcall+=","+sq.getVar().getSafeSymbol();
1022 } else if (q instanceof RelationQuantifier) {
1023 RelationQuantifier rq=(RelationQuantifier) q;
1024 methodcall+=","+rq.x.getSafeSymbol();
1025 methodcall+=","+rq.y.getSafeSymbol();
1026 } else if (q instanceof ForQuantifier) {
1027 ForQuantifier fq=(ForQuantifier) q;
1028 methodcall+=","+fq.getVar().getSafeSymbol();
1032 cr.outputline(methodcall);
1033 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1034 cr.outputline("continue;");
1039 String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1040 cr.outputline("int " + addeditem + ";");
1041 if (rd.testUsage(RelationDescriptor.IMAGE)) {
1042 cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
1045 if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1046 cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1049 cr.outputline("if (" + addeditem + ")");
1052 Vector dispatchrules = getrulelist(rd);
1054 if (dispatchrules.size() == 0) {
1055 cr.outputline("// nothing to dispatch");
1060 for(int i = 0; i < dispatchrules.size(); i++) {
1061 Rule rule = (Rule) dispatchrules.elementAt(i);
1062 if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
1063 /* Guard depends on this relation, so we recomput everything */
1064 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1066 for (int j=0;j<rule.numQuantifiers();j++) {
1067 Quantifier q=rule.getQuantifier(j);
1068 if (q.getRequiredDescriptors().contains(rd)) {
1070 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1079 public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1081 cr.outputline("// SET DISPATCH ");
1083 cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1084 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
1086 /* Adding new item */
1087 /* Perform safety checks */
1088 cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1089 cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
1091 /* Have update to call into */
1092 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1094 for(int i=0;i<currentrule.numQuantifiers();i++) {
1095 if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1096 parttype=parttype+", int, int";
1098 parttype=parttype+", int";
1100 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1101 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getset("+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
1102 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+
1103 repairtable.getSafeSymbol();
1104 for(int i=0;i<currentrule.numQuantifiers();i++) {
1105 Quantifier q=currentrule.getQuantifier(i);
1106 if (q instanceof SetQuantifier) {
1107 SetQuantifier sq=(SetQuantifier) q;
1108 methodcall+=","+sq.getVar().getSafeSymbol();
1109 } else if (q instanceof RelationQuantifier) {
1110 RelationQuantifier rq=(RelationQuantifier) q;
1111 methodcall+=","+rq.x.getSafeSymbol();
1112 methodcall+=","+rq.y.getSafeSymbol();
1113 } else if (q instanceof ForQuantifier) {
1114 ForQuantifier fq=(ForQuantifier) q;
1115 methodcall+=","+fq.getVar().getSafeSymbol();
1119 cr.outputline(methodcall);
1120 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1121 cr.outputline("continue;");
1124 /* Build standard compensation actions */
1125 if (need_compensation(currentrule)) {
1126 UpdateNode un=find_compensation(currentrule);
1127 String name=(String)updatenames.get(un);
1128 usedupdates.add(un); /* Mark as used */
1130 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
1131 repairtable.getSafeSymbol();
1132 for(int i=0;i<currentrule.numQuantifiers();i++) {
1133 Quantifier q=currentrule.getQuantifier(i);
1134 if (q instanceof SetQuantifier) {
1135 SetQuantifier sq=(SetQuantifier) q;
1136 methodcall+=","+sq.getVar().getSafeSymbol();
1137 } else if (q instanceof RelationQuantifier) {
1138 RelationQuantifier rq=(RelationQuantifier) q;
1139 methodcall+=","+rq.x.getSafeSymbol();
1140 methodcall+=","+rq.y.getSafeSymbol();
1141 } else if (q instanceof ForQuantifier) {
1142 ForQuantifier fq=(ForQuantifier) q;
1143 methodcall+=","+fq.getVar().getSafeSymbol();
1147 cr.outputline(methodcall);
1148 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1149 cr.outputline("continue;");
1154 String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1155 cr.outputline("int " + addeditem + " = 1;");
1156 cr.outputline(addeditem + " = " + sd.getSafeSymbol() + "_hash->add((int)" + setvar + ", (int)" + setvar + ");");
1158 Vector dispatchrules = getrulelist(sd);
1160 if (dispatchrules.size() == 0) {
1161 cr.outputline("// nothing to dispatch");
1166 for(int i = 0; i < dispatchrules.size(); i++) {
1167 Rule rule = (Rule) dispatchrules.elementAt(i);
1168 if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
1169 /* Guard depends on this relation, so we recompute everything */
1170 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1172 for (int j=0;j<rule.numQuantifiers();j++) {
1173 Quantifier q=rule.getQuantifier(j);
1174 if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1176 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");