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;
25 static boolean DEBUG=false;
29 public RepairGenerator(State state, Termination t) {
31 updatenames=new Hashtable();
32 usedupdates=new HashSet();
35 togenerate=new HashSet();
36 togenerate.addAll(termination.conjunctions);
37 togenerate.removeAll(removed);
38 GraphNode.computeclosure(togenerate,removed);
41 sources=new Sources(state);
42 Repair.repairgenerator=this;
45 private void name_updates() {
47 for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
48 GraphNode gn=(GraphNode) it.next();
49 TermNode tn=(TermNode) gn.getOwner();
50 MultUpdateNode mun=tn.getUpdate();
51 if (togenerate.contains(gn))
52 for (int i=0;i<mun.numUpdates();i++) {
53 UpdateNode un=mun.getUpdate(i);
54 String name="update"+String.valueOf(count++);
55 updatenames.put(un,name);
60 public void generate(OutputStream outputrepair, OutputStream outputaux,OutputStream outputhead, String st) {
61 this.outputrepair = new java.io.PrintWriter(outputrepair, true);
62 this.outputaux = new java.io.PrintWriter(outputaux, true);
63 this.outputhead = new java.io.PrintWriter(outputhead, true);
67 generate_tokentable();
68 generate_hashtables();
69 generate_stateobject();
75 CodeWriter crhead = new StandardCodeWriter(this.outputhead);
76 CodeWriter craux = new StandardCodeWriter(this.outputaux);
77 crhead.outputline("};");
78 craux.outputline("};");
82 private void generate_updates() {
84 CodeWriter crhead = new StandardCodeWriter(outputhead);
85 CodeWriter craux = new StandardCodeWriter(outputaux);
88 String repairtable="repairtable";
91 for(Iterator it=termination.updatenodes.iterator();it.hasNext();) {
92 GraphNode gn=(GraphNode) it.next();
93 TermNode tn=(TermNode) gn.getOwner();
94 MultUpdateNode mun=tn.getUpdate();
95 boolean isrelation=(mun.getDescriptor() instanceof RelationDescriptor);
96 if (togenerate.contains(gn))
97 for (int i=0;i<mun.numUpdates();i++) {
98 UpdateNode un=mun.getUpdate(i);
99 String methodname=(String)updatenames.get(un);
102 case MultUpdateNode.ADD:
104 crhead.outputline("void "+methodname+"("+name+"_state * " +state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+", int "+right+");");
105 craux.outputline("void "+methodname+"("+name+"_state * "+ state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+", int "+right+")");
107 crhead.outputline("void "+methodname+"("+name+"_state * "+ state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+");");
108 craux.outputline("void "+methodname+"("+name+"_state * "+state+","+name+" * "+model+", RepairHash * "+repairtable+", int "+left+")");
111 un.generate(craux, false, left,right);
114 case MultUpdateNode.REMOVE:
116 String methodcall="void "+methodname+"("+name+"_state * "+state+","+name+" * "+model+", RepairHash * "+repairtable;
117 for(int j=0;j<r.numQuantifiers();j++) {
118 Quantifier q=r.getQuantifier(j);
119 if (q instanceof SetQuantifier) {
120 SetQuantifier sq=(SetQuantifier) q;
121 methodcall+=","+sq.getVar().getType().getGenerateType().getSafeSymbol()+" "+sq.getVar().getSafeSymbol();
122 } else if (q instanceof RelationQuantifier) {
123 RelationQuantifier rq=(RelationQuantifier) q;
125 methodcall+=","+rq.x.getType().getGenerateType().getSafeSymbol()+" "+rq.x.getSafeSymbol();
126 methodcall+=","+rq.y.getType().getGenerateType().getSafeSymbol()+" "+rq.y.getSafeSymbol();
127 } else if (q instanceof ForQuantifier) {
128 ForQuantifier fq=(ForQuantifier) q;
129 methodcall+=",int "+fq.getVar().getSafeSymbol();
133 crhead.outputline(methodcall+";");
134 craux.outputline(methodcall);
136 un.generate(craux, true, null,null);
139 case MultUpdateNode.MODIFY:
141 throw new Error("Nonimplement Update");
147 private void generate_call() {
148 CodeWriter cr = new StandardCodeWriter(outputrepair);
149 VarDescriptor vdstate=VarDescriptor.makeNew("repairstate");
150 cr.outputline(name+"_state * "+vdstate.getSafeSymbol()+"=new "+name+"_state();");
151 Iterator globals=state.stGlobals.descriptors();
152 while (globals.hasNext()) {
153 VarDescriptor vd=(VarDescriptor) globals.next();
154 cr.outputline(vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+"=("+vd.getType().getGenerateType().getSafeSymbol()+")"+vd.getSafeSymbol()+";");
156 /* Insert repair here */
157 cr.outputline(vdstate.getSafeSymbol()+"->doanalysis();");
158 globals=state.stGlobals.descriptors();
159 while (globals.hasNext()) {
160 VarDescriptor vd=(VarDescriptor) globals.next();
161 cr.outputline("*(("+vd.getType().getGenerateType().getSafeSymbol()+"*) &"+vd.getSafeSymbol()+")="+vdstate.getSafeSymbol()+"->"+vd.getSafeSymbol()+";");
163 cr.outputline("delete "+vdstate.getSafeSymbol()+";");
166 private void generate_tokentable() {
167 CodeWriter cr = new StandardCodeWriter(outputrepair);
168 Iterator tokens = TokenLiteralExpr.tokens.keySet().iterator();
171 cr.outputline("// Token values");
174 while (tokens.hasNext()) {
175 Object token = tokens.next();
176 cr.outputline("// " + token.toString() + " = " + TokenLiteralExpr.tokens.get(token).toString());
183 private void generate_stateobject() {
184 CodeWriter crhead = new StandardCodeWriter(outputhead);
185 crhead.outputline("class "+name+"_state {");
186 crhead.outputline("public:");
187 Iterator globals=state.stGlobals.descriptors();
188 while (globals.hasNext()) {
189 VarDescriptor vd=(VarDescriptor) globals.next();
190 crhead.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+";");
194 private void generate_hashtables() {
195 CodeWriter craux = new StandardCodeWriter(outputaux);
196 CodeWriter crhead = new StandardCodeWriter(outputhead);
197 crhead.outputline("#include \"SimpleHash.h\"");
198 crhead.outputline("#include <stdio.h>");
199 crhead.outputline("#include <stdlib.h>");
200 crhead.outputline("class "+name+" {");
201 crhead.outputline("public:");
202 crhead.outputline(name+"();");
203 crhead.outputline("~"+name+"();");
204 craux.outputline("#include \""+headername+"\"");
206 craux.outputline(name+"::"+name+"() {");
207 craux.outputline("// creating hashtables ");
210 Iterator sets = state.stSets.descriptors();
212 /* first pass create all the hash tables */
213 while (sets.hasNext()) {
214 SetDescriptor set = (SetDescriptor) sets.next();
215 crhead.outputline("SimpleHash* " + set.getSafeSymbol() + "_hash;");
216 craux.outputline(set.getSafeSymbol() + "_hash = new SimpleHash();");
219 /* second pass build relationships between hashtables */
220 sets = state.stSets.descriptors();
222 while (sets.hasNext()) {
223 SetDescriptor set = (SetDescriptor) sets.next();
224 Iterator subsets = set.subsets();
226 while (subsets.hasNext()) {
227 SetDescriptor subset = (SetDescriptor) subsets.next();
228 craux.outputline(subset.getSafeSymbol() + "_hash->addParent(" + set.getSafeSymbol() + "_hash);");
232 /* build relations */
233 Iterator relations = state.stRelations.descriptors();
235 /* first pass create all the hash tables */
236 while (relations.hasNext()) {
237 RelationDescriptor relation = (RelationDescriptor) relations.next();
239 if (relation.testUsage(RelationDescriptor.IMAGE)) {
240 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hash;");
241 craux.outputline(relation.getSafeSymbol() + "_hash = new SimpleHash();");
244 if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
245 crhead.outputline("SimpleHash* " + relation.getSafeSymbol() + "_hashinv;");
246 craux.outputline(relation.getSafeSymbol() + "_hashinv = new SimpleHash();");
250 craux.outputline("}");
251 crhead.outputline("};");
252 craux.outputline(name+"::~"+name+"() {");
253 craux.outputline("// deleting hashtables");
255 /* build destructor */
256 sets = state.stSets.descriptors();
258 /* first pass create all the hash tables */
259 while (sets.hasNext()) {
260 SetDescriptor set = (SetDescriptor) sets.next();
261 craux.outputline("delete "+set.getSafeSymbol() + "_hash;");
264 /* destroy relations */
265 relations = state.stRelations.descriptors();
267 /* first pass create all the hash tables */
268 while (relations.hasNext()) {
269 RelationDescriptor relation = (RelationDescriptor) relations.next();
271 if (relation.testUsage(RelationDescriptor.IMAGE)) {
272 craux.outputline("delete "+relation.getSafeSymbol() + "_hash;");
275 if (relation.testUsage(RelationDescriptor.INVIMAGE)) {
276 craux.outputline("delete " + relation.getSafeSymbol() + ";");
279 craux.outputline("}");
282 private void generate_worklist() {
283 CodeWriter crhead = new StandardCodeWriter(outputhead);
284 CodeWriter craux = new StandardCodeWriter(outputaux);
285 oldmodel=VarDescriptor.makeNew("oldmodel");
286 newmodel=VarDescriptor.makeNew("newmodel");
287 worklist=VarDescriptor.makeNew("worklist");
288 goodflag=VarDescriptor.makeNew("goodflag");
289 repairtable=VarDescriptor.makeNew("repairtable");
290 crhead.outputline("void doanalysis();");
291 craux.outputline("void "+name +"_state::doanalysis()");
293 craux.outputline(name+ " * "+oldmodel.getSafeSymbol()+"=0;");
294 craux.outputline("WorkList * "+worklist.getSafeSymbol()+" = new WorkList();");
295 craux.outputline("RepairHash * "+repairtable.getSafeSymbol()+"=0;");
296 craux.outputline("while (1)");
298 craux.outputline("int "+goodflag.getSafeSymbol()+"=1;");
299 craux.outputline(name+ " * "+newmodel.getSafeSymbol()+"=new "+name+"();");
302 private void generate_teardown() {
303 CodeWriter cr = new StandardCodeWriter(outputaux);
304 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
305 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
306 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
307 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
308 cr.outputline("delete "+newmodel.getSafeSymbol()+";");
309 cr.outputline("delete "+worklist.getSafeSymbol()+";");
313 private void generate_rules() {
314 /* first we must sort the rules */
315 Iterator allrules = state.vRules.iterator();
316 Vector emptyrules = new Vector(); // rules with no quantifiers
317 Vector worklistrules = new Vector(); // the rest of the rules
318 RelationDescriptor.prefix = newmodel.getSafeSymbol()+"->";
319 SetDescriptor.prefix = newmodel.getSafeSymbol()+"->";
321 while (allrules.hasNext()) {
322 Rule rule = (Rule) allrules.next();
323 ListIterator quantifiers = rule.quantifiers();
324 boolean noquantifiers = true;
325 while (quantifiers.hasNext()) {
326 Quantifier quantifier = (Quantifier) quantifiers.next();
327 if (quantifier instanceof ForQuantifier) {
328 // ok, because integers exist already!
331 noquantifiers = false;
336 emptyrules.add(rule);
338 worklistrules.add(rule);
342 Iterator iterator_er = emptyrules.iterator();
343 while (iterator_er.hasNext()) {
344 Rule rule = (Rule) iterator_er.next();
346 final SymbolTable st = rule.getSymbolTable();
347 CodeWriter cr = new StandardCodeWriter(outputaux) {
348 public SymbolTable getSymbolTable() { return st; }
350 cr.outputline("// build " +escape(rule.toString()));
352 ListIterator quantifiers = rule.quantifiers();
353 while (quantifiers.hasNext()) {
354 Quantifier quantifier = (Quantifier) quantifiers.next();
355 quantifier.generate_open(cr);
360 rule.getGuardExpr().prettyPrint(cr);
363 /* now we have to generate the guard test */
364 VarDescriptor guardval = VarDescriptor.makeNew();
365 rule.getGuardExpr().generate(cr, guardval);
366 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
369 /* now we have to generate the inclusion code */
371 rule.getInclusion().generate(cr);
373 while (quantifiers.hasPrevious()) {
374 Quantifier quantifier = (Quantifier) quantifiers.previous();
383 CodeWriter cr2 = new StandardCodeWriter(outputaux);
385 cr2.outputline("while ("+goodflag.getSafeSymbol()+"&&"+worklist.getSafeSymbol()+"->hasMoreElements())");
387 VarDescriptor idvar=VarDescriptor.makeNew("id");
388 cr2.outputline("int "+idvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getid();");
390 String elseladder = "if";
392 Iterator iterator_rules = worklistrules.iterator();
393 while (iterator_rules.hasNext()) {
395 Rule rule = (Rule) iterator_rules.next();
396 int dispatchid = rule.getNum();
399 final SymbolTable st = rule.getSymbolTable();
400 CodeWriter cr = new StandardCodeWriter(outputaux) {
401 public SymbolTable getSymbolTable() { return st; }
405 cr.outputline(elseladder + " ("+idvar.getSafeSymbol()+" == " + dispatchid + ")");
407 VarDescriptor typevar=VarDescriptor.makeNew("type");
408 VarDescriptor leftvar=VarDescriptor.makeNew("left");
409 VarDescriptor rightvar=VarDescriptor.makeNew("right");
410 cr.outputline("int "+typevar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->gettype();");
411 cr.outputline("int "+leftvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getlvalue();");
412 cr.outputline("int "+rightvar.getSafeSymbol()+"="+worklist.getSafeSymbol()+"->getrvalue();");
413 cr.outputline("// build " +escape(rule.toString()));
416 for (int j=0;j<rule.numQuantifiers();j++) {
417 Quantifier quantifier = rule.getQuantifier(j);
418 quantifier.generate_open(cr, typevar.getSafeSymbol(),j,leftvar.getSafeSymbol(),rightvar.getSafeSymbol());
424 rule.getGuardExpr().prettyPrint(cr);
427 /* now we have to generate the guard test */
429 VarDescriptor guardval = VarDescriptor.makeNew();
430 rule.getGuardExpr().generate(cr, guardval);
432 cr.outputline("if (" + guardval.getSafeSymbol() + ")");
435 /* now we have to generate the inclusion code */
437 rule.getInclusion().generate(cr);
440 for (int j=0;j<rule.numQuantifiers();j++) {
444 // close startblocks generated by DotExpr memory checks
445 //DotExpr.generate_memory_endblocks(cr);
447 cr.endblock(); // end else-if WORKLIST ladder
449 elseladder = "else if";
453 cr2.outputline("else");
455 cr2.outputline("printf(\"VERY BAD !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\\n\\n\");");
456 cr2.outputline("exit(1);");
458 // end block created for worklist
462 public static String escape(String s) {
464 for(int i=0;i<s.length();i++) {
474 private void generate_checks() {
476 /* do constraint checks */
477 Vector constraints = state.vConstraints;
479 for (int i = 0; i < constraints.size(); i++) {
481 Constraint constraint = (Constraint) constraints.elementAt(i);
485 final SymbolTable st = constraint.getSymbolTable();
487 CodeWriter cr = new StandardCodeWriter(outputaux) {
488 public SymbolTable getSymbolTable() { return st; }
491 cr.outputline("// checking " + escape(constraint.toString()));
494 ListIterator quantifiers = constraint.quantifiers();
496 while (quantifiers.hasNext()) {
497 Quantifier quantifier = (Quantifier) quantifiers.next();
498 quantifier.generate_open(cr);
501 cr.outputline("int maybe = 0;");
503 /* now we have to generate the guard test */
505 VarDescriptor constraintboolean = VarDescriptor.makeNew("constraintboolean");
506 constraint.getLogicStatement().generate(cr, constraintboolean);
508 cr.outputline("if (maybe)");
510 cr.outputline("printf(\"maybe fail " + escape(constraint.toString()) + ". \");");
511 cr.outputline("exit(1);");
514 cr.outputline("else if (!" + constraintboolean.getSafeSymbol() + ")");
517 cr.outputline("printf(\"fail " + escape(constraint.toString()) + ". \");");
520 /* Build new repair table */
521 cr.outputline("if ("+repairtable.getSafeSymbol()+")");
522 cr.outputline("delete "+repairtable.getSafeSymbol()+";");
523 cr.outputline(repairtable.getSafeSymbol()+"=new RepairHash();");
526 /* Compute cost of each repair */
527 VarDescriptor mincost=VarDescriptor.makeNew("mincost");
528 VarDescriptor mincostindex=VarDescriptor.makeNew("mincostindex");
529 DNFConstraint dnfconst=constraint.dnfconstraint;
530 cr.outputline("int "+mincostindex.getSafeSymbol()+";");
531 if (dnfconst.size()>1) {
533 for(int j=0;j<dnfconst.size();j++) {
534 Conjunction conj=dnfconst.get(j);
535 GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj);
536 if (removed.contains(gn))
539 VarDescriptor costvar;
543 costvar=VarDescriptor.makeNew("cost");
544 for(int k=0;k<conj.size();k++) {
545 DNFPredicate dpred=conj.get(k);
546 Predicate p=dpred.getPredicate();
547 boolean negate=dpred.isNegated();
548 VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
549 p.generate(cr,predvalue);
551 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
553 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
555 cr.outputline("int "+costvar.getSafeSymbol()+"="+cost.getCost(dpred)+";");
557 cr.outputline(costvar.getSafeSymbol()+"+="+cost.getCost(dpred)+";");
561 cr.outputline("if ("+costvar.getSafeSymbol()+"<"+mincost.getSafeSymbol()+")");
563 cr.outputline(mincost.getSafeSymbol()+"="+costvar.getSafeSymbol()+";");
564 cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
567 cr.outputline(mincostindex.getSafeSymbol()+"="+j+";");
571 cr.outputline("switch("+mincostindex.getSafeSymbol()+") {");
572 for(int j=0;j<dnfconst.size();j++) {
573 Conjunction conj=dnfconst.get(j);
574 GraphNode gn=(GraphNode)termination.conjtonodemap.get(conj); if (removed.contains(gn))
576 cr.outputline("case "+j+":");
577 for(int k=0;k<conj.size();k++) {
578 DNFPredicate dpred=conj.get(k);
579 Predicate p=dpred.getPredicate();
580 boolean negate=dpred.isNegated();
581 VarDescriptor predvalue=VarDescriptor.makeNew("Predicatevalue");
582 p.generate(cr,predvalue);
584 cr.outputline("if (maybe||"+predvalue.getSafeSymbol()+")");
586 cr.outputline("if (maybe||!"+predvalue.getSafeSymbol()+")");
588 if (p instanceof InclusionPredicate)
589 generateinclusionrepair(conj,dpred, cr);
590 else if (p instanceof ExprPredicate) {
591 ExprPredicate ep=(ExprPredicate)p;
592 if (ep.getType()==ExprPredicate.SIZE)
593 generatesizerepair(conj,dpred,cr);
594 else if (ep.getType()==ExprPredicate.COMPARISON)
595 generatecomparisonrepair(conj,dpred,cr);
596 } else throw new Error("Unrecognized Predicate");
601 cr.outputline("break;");
605 cr.outputline(goodflag.getSafeSymbol()+"=0;");
606 cr.outputline("if ("+oldmodel.getSafeSymbol()+")");
607 cr.outputline("delete "+oldmodel.getSafeSymbol()+";");
608 cr.outputline(oldmodel.getSafeSymbol()+"="+newmodel.getSafeSymbol()+";");
609 cr.outputline("break;"); /* Rebuild model and all */
613 while (quantifiers.hasPrevious()) {
614 Quantifier quantifier = (Quantifier) quantifiers.previous();
617 cr.outputline("if ("+goodflag.getSafeSymbol()+")");
618 cr.outputline("break;");
626 private MultUpdateNode getmultupdatenode(Conjunction conj, DNFPredicate dpred, int repairtype) {
627 MultUpdateNode mun=null;
628 GraphNode gn=(GraphNode) termination.conjtonodemap.get(conj);
629 for(Iterator edgeit=gn.edges();(mun==null)&&edgeit.hasNext();) {
630 GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
631 TermNode tn2=(TermNode)gn2.getOwner();
632 if (tn2.getType()==TermNode.ABSTRACT) {
633 AbstractRepair ar=tn2.getAbstract();
634 if (((repairtype==-1)||(ar.getType()==repairtype))&&
635 ar.getPredicate()==dpred) {
636 for(Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
637 GraphNode gn3=((GraphNode.Edge) edgeit2.next()).getTarget();
638 if (!removed.contains(gn3)) {
639 TermNode tn3=(TermNode)gn3.getOwner();
640 if (tn3.getType()==TermNode.UPDATE) {
652 public void generatecomparisonrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
653 MultUpdateNode munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
654 MultUpdateNode munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
655 ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
656 RelationDescriptor rd=(RelationDescriptor)ep.getDescriptor();
657 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
658 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
659 boolean inverted=ep.inverted();
660 boolean negated=dpred.isNegated();
661 OpExpr expr=(OpExpr)ep.expr;
662 Opcode opcode=expr.getOpcode();
663 VarDescriptor leftside=VarDescriptor.makeNew("leftside");
664 VarDescriptor rightside=VarDescriptor.makeNew("rightside");
665 VarDescriptor newvalue=VarDescriptor.makeNew("newvalue");
667 expr.getLeftExpr().generate(cr,leftside);
668 expr.getRightExpr().generate(cr,newvalue);
669 cr.outputline(rd.getRange().getType().getGenerateType().getSafeSymbol()+" "+rightside.getSafeSymbol()+";");
670 cr.outputline(rd.getSafeSymbol()+"_hash->get("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
672 expr.getLeftExpr().generate(cr,rightside);
673 expr.getRightExpr().generate(cr,newvalue);
674 cr.outputline(rd.getDomain().getType().getGenerateType().getSafeSymbol()+" "+leftside.getSafeSymbol()+";");
675 cr.outputline(rd.getSafeSymbol()+"_hashinv->get("+leftside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
678 if (opcode==Opcode.GT) {
680 } else if (opcode==Opcode.GE) {
682 } else if (opcode==Opcode.LT) {
684 } else if (opcode==Opcode.LE) {
686 } else if (opcode==Opcode.EQ) {
688 } else if (opcode==Opcode.NE) {
691 throw new Error("Unrecognized Opcode");
694 if (opcode==Opcode.GT) {
695 cr.outputline(newvalue.getSafeSymbol()+"++;");
696 } else if (opcode==Opcode.GE) {
698 } else if (opcode==Opcode.LT) {
699 cr.outputline(newvalue.getSafeSymbol()+"--;");
700 } else if (opcode==Opcode.LE) {
702 } else if (opcode==Opcode.EQ) {
704 } else if (opcode==Opcode.NE) {
705 cr.outputline(newvalue.getSafeSymbol()+"++;");
707 throw new Error("Unrecognized Opcode");
709 /* Do abstract repairs */
711 cr.outputline(rd.getSafeSymbol()+"_hash->remove("+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
713 cr.outputline(rd.getSafeSymbol()+"_hash->add("+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
715 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
719 cr.outputline(rd.getSafeSymbol()+"_hashinv->remove("+rightside.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
721 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newvalue.getSafeSymbol()+","+leftside.getSafeSymbol()+");");
723 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+rightside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
726 /* Do concrete repairs */
727 /* Start with scheduling removal */
728 for(int i=0;i<state.vRules.size();i++) {
729 Rule r=(Rule)state.vRules.get(i);
730 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
731 for(int j=0;j<munremove.numUpdates();j++) {
732 UpdateNode un=munremove.getUpdate(i);
733 if (un.getRule()==r) {
734 /* Update for rule r */
735 String name=(String)updatenames.get(un);
736 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftside.getSafeSymbol()+","+rightside.getSafeSymbol()+",(int) &"+name+");");
741 /* Now do addition */
742 UpdateNode un=munadd.getUpdate(0);
743 String name=(String)updatenames.get(un);
745 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftside.getSafeSymbol()+","+newvalue.getSafeSymbol()+");");
747 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newvalue.getSafeSymbol()+","+rightside.getSafeSymbol()+");");
751 public void generatesizerepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr) {
752 ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
753 OpExpr expr=(OpExpr)ep.expr;
754 Opcode opcode=expr.getOpcode();
756 boolean negated=dpred.isNegated();
758 if (opcode==Opcode.GT) {
760 } else if (opcode==Opcode.GE) {
762 } else if (opcode==Opcode.LT) {
764 } else if (opcode==Opcode.LE) {
766 } else if (opcode==Opcode.EQ) {
768 } else if (opcode==Opcode.NE) {
771 throw new Error("Unrecognized Opcode");
774 MultUpdateNode munremove;
776 MultUpdateNode munadd;
777 if (ep.getDescriptor() instanceof RelationDescriptor) {
778 munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMRELATION);
779 munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTORELATION);
781 munremove=getmultupdatenode(conj,dpred,AbstractRepair.REMOVEFROMSET);
782 munadd=getmultupdatenode(conj,dpred,AbstractRepair.ADDTOSET);
784 int size=ep.leftsize();
785 VarDescriptor sizevar=VarDescriptor.makeNew("size");
786 ((OpExpr)expr).left.generate(cr, sizevar);
787 VarDescriptor change=VarDescriptor.makeNew("change");
788 cr.outputline("int "+change.getSafeSymbol()+";");
789 boolean generateadd=false;
790 boolean generateremove=false;
791 if (opcode==Opcode.GT) {
792 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
794 generateremove=false;
795 } else if (opcode==Opcode.GE) {
796 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
798 generateremove=false;
799 } else if (opcode==Opcode.LT) {
800 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size-1)+"-"+sizevar.getSafeSymbol()+";");
803 } else if (opcode==Opcode.LE) {
804 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
807 } else if (opcode==Opcode.EQ) {
808 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size)+"-"+sizevar.getSafeSymbol()+";");
811 } else if (opcode==Opcode.NE) {
812 cr.outputline(change.getSafeSymbol()+"="+String.valueOf(size+1)+"-"+sizevar.getSafeSymbol()+";");
814 generateremove=false;
816 throw new Error("Unrecognized Opcode");
818 Descriptor d=ep.getDescriptor();
819 if (generateremove) {
820 cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
822 /* Find element to remove */
823 VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
824 VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
825 if (d instanceof RelationDescriptor) {
827 rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
828 cr.outputline("int "+leftvar.getSafeSymbol()+";");
829 cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
831 leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
832 cr.outputline("int "+rightvar.getSafeSymbol()+";");
833 cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
836 cr.outputline("int "+leftvar.getSafeSymbol()+"="+d.getSafeSymbol()+"_hash->firstkey();");
838 /* Generate abstract remove instruction */
839 if (d instanceof RelationDescriptor) {
840 RelationDescriptor rd=(RelationDescriptor) d;
841 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
842 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
844 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
846 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
848 cr.outputline(d.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
850 /* Generate concrete remove instruction */
851 for(int i=0;i<state.vRules.size();i++) {
852 Rule r=(Rule)state.vRules.get(i);
853 if (r.getInclusion().getTargetDescriptors().contains(d)) {
854 for(int j=0;j<munremove.numUpdates();j++) {
855 UpdateNode un=munremove.getUpdate(i);
856 if (un.getRule()==r) {
857 /* Update for rule rule r */
858 String name=(String)updatenames.get(un);
859 if (d instanceof RelationDescriptor) {
860 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
862 cr.outputline(repairtable.getSafeSymbol()+"->addset("+d.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
872 cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
874 VarDescriptor newobject=VarDescriptor.makeNew("newobject");
875 if (d instanceof RelationDescriptor) {
876 VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)ep.expr).setexpr).vd;
877 RelationDescriptor rd=(RelationDescriptor)d;
878 if (sources.relsetSource(rd,!ep.inverted())) {
880 SetDescriptor sd=sources.relgetSourceSet(rd,!ep.inverted());
881 VarDescriptor iterator=VarDescriptor.makeNew("iterator");
882 cr.outputline(sd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
883 cr.outputline("for("+iterator.getSafeSymbol()+"="+sd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
886 cr.outputline("if !"+rd.getSafeSymbol()+"_hashinv->contains("+iterator.getSafeSymbol()+"->key(),"+otherside.getSafeSymbol()+")");
888 cr.outputline("if !"+rd.getSafeSymbol()+"_hash->contains("+otherside.getSafeSymbol()+","+iterator.getSafeSymbol()+"->key())");
890 cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
891 cr.outputline(iterator.getSafeSymbol()+"->next();");
893 } else if (sources.relallocSource(rd,!ep.inverted())) {
894 /* Allocation Source*/
895 sources.relgenerateSourceAlloc(cr,newobject,rd,!ep.inverted());
896 } else throw new Error("No source for adding to Relation");
898 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
899 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
901 cr.outputline(rd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
903 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
905 UpdateNode un=munadd.getUpdate(0);
906 String name=(String)updatenames.get(un);
907 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
909 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
910 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
912 cr.outputline(rd.getSafeSymbol()+"_hash->add("+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
914 cr.outputline(rd.getSafeSymbol()+"_hashinv->add("+newobject.getSafeSymbol()+","+otherside.getSafeSymbol()+");");
915 UpdateNode un=munadd.getUpdate(0);
916 String name=(String)updatenames.get(un);
917 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+otherside.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
920 SetDescriptor sd=(SetDescriptor)d;
921 if (sources.setSource(sd)) {
924 SetDescriptor sourcesd=sources.getSourceSet(sd);
925 VarDescriptor iterator=VarDescriptor.makeNew("iterator");
926 cr.outputline(sourcesd.getType().getGenerateType().getSafeSymbol() +" "+newobject.getSafeSymbol()+";");
927 cr.outputline("for("+iterator.getSafeSymbol()+"="+sourcesd.getSafeSymbol()+"_hash->iterator();"+iterator.getSafeSymbol()+".hasNext();)");
929 cr.outputline("if !"+sd.getSafeSymbol()+"_hash->contains("+iterator.getSafeSymbol()+"->key())");
930 cr.outputline(newobject.getSafeSymbol()+"="+iterator.getSafeSymbol()+".key();");
931 cr.outputline(iterator.getSafeSymbol()+"->next();");
933 } else if (sources.allocSource(sd)) {
934 /* Allocation Source*/
935 sources.generateSourceAlloc(cr,newobject,sd);
936 } else throw new Error("No source for adding to Set");
937 cr.outputline(sd.getSafeSymbol()+"_hash->add("+newobject.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
938 UpdateNode un=munadd.getUpdate(0);
939 String name=(String)updatenames.get(un);
940 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+newobject.getSafeSymbol()+");");
946 public void generateinclusionrepair(Conjunction conj, DNFPredicate dpred, CodeWriter cr){
947 InclusionPredicate ip=(InclusionPredicate) dpred.getPredicate();
948 boolean negated=dpred.isNegated();
949 MultUpdateNode mun=getmultupdatenode(conj,dpred,-1);
950 VarDescriptor leftvar=VarDescriptor.makeNew("left");
951 ip.expr.generate(cr, leftvar);
954 if (ip.setexpr instanceof ImageSetExpr) {
955 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
956 VarDescriptor rightvar=ise.getVar();
957 boolean inverse=ise.inverted();
958 RelationDescriptor rd=ise.getRelation();
959 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
960 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
963 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + rightvar + ", (int)" + leftvar + ");");
965 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + leftvar + ", (int)" + rightvar + ");");
968 cr.outputline(rd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + rightvar + ");");
970 cr.outputline(rd.getSafeSymbol() + "_hashinv->remove((int)" + rightvar + ", (int)" + leftvar + ");");
972 for(int i=0;i<state.vRules.size();i++) {
973 Rule r=(Rule)state.vRules.get(i);
974 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
975 for(int j=0;j<mun.numUpdates();j++) {
976 UpdateNode un=mun.getUpdate(i);
977 if (un.getRule()==r) {
978 /* Update for rule rule r */
979 String name=(String)updatenames.get(un);
981 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
983 cr.outputline(repairtable.getSafeSymbol()+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
990 SetDescriptor sd=ip.setexpr.sd;
991 cr.outputline(sd.getSafeSymbol() + "_hash->remove((int)" + leftvar + ", (int)" + leftvar + ");");
993 for(int i=0;i<state.vRules.size();i++) {
994 Rule r=(Rule)state.vRules.get(i);
995 if (r.getInclusion().getTargetDescriptors().contains(sd)) {
996 for(int j=0;j<mun.numUpdates();j++) {
997 UpdateNode un=mun.getUpdate(i);
998 if (un.getRule()==r) {
999 /* Update for rule rule r */
1000 String name=(String)updatenames.get(un);
1001 cr.outputline(repairtable.getSafeSymbol()+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
1008 /* Generate update */
1009 if (ip.setexpr instanceof ImageSetExpr) {
1010 ImageSetExpr ise=(ImageSetExpr) ip.setexpr;
1011 VarDescriptor rightvar=ise.getVar();
1012 boolean inverse=ise.inverted();
1013 RelationDescriptor rd=ise.getRelation();
1014 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1015 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1018 cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + rightvar + ", (int)" + leftvar + ");");
1020 cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + leftvar + ", (int)" + rightvar + ");");
1023 cr.outputline(rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
1025 cr.outputline(rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1027 UpdateNode un=mun.getUpdate(0);
1028 String name=(String)updatenames.get(un);
1030 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1032 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
1035 SetDescriptor sd=ip.setexpr.sd;
1036 cr.outputline(sd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + leftvar + ");");
1038 UpdateNode un=mun.getUpdate(0);
1039 /* Update for rule rule r */
1040 String name=(String)updatenames.get(un);
1041 cr.outputline(name+"(this,"+newmodel.getSafeSymbol()+","+repairtable.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
1048 public static Vector getrulelist(Descriptor d) {
1049 Vector dispatchrules = new Vector();
1050 Vector rules = State.currentState.vRules;
1052 for (int i = 0; i < rules.size(); i++) {
1053 Rule rule = (Rule) rules.elementAt(i);
1054 Set requiredsymbols = rule.getRequiredDescriptors();
1056 // #TBD#: in general this is wrong because these descriptors may contain descriptors
1057 // bound in "in?" expressions which need to be dealt with in a topologically sorted
1060 if (rule.getRequiredDescriptors().contains(d)) {
1061 dispatchrules.addElement(rule);
1064 return dispatchrules;
1067 private boolean need_compensation(Rule r) {
1068 GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1069 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1070 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1071 GraphNode gn2=edge.getTarget();
1072 if (!removed.contains(gn2)) {
1073 TermNode tn2=(TermNode)gn2.getOwner();
1074 if (tn2.getType()==TermNode.CONSEQUENCE)
1081 private UpdateNode find_compensation(Rule r) {
1082 GraphNode gn=(GraphNode)termination.scopefalsify.get(r);
1083 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
1084 GraphNode.Edge edge=(GraphNode.Edge)edgeit.next();
1085 GraphNode gn2=edge.getTarget();
1086 if (!removed.contains(gn2)) {
1087 TermNode tn2=(TermNode)gn2.getOwner();
1088 if (tn2.getType()==TermNode.UPDATE) {
1089 MultUpdateNode mun=tn2.getUpdate();
1090 for(int i=0;i<mun.numUpdates();i++) {
1091 UpdateNode un=mun.getUpdate(i);
1092 if (un.getRule()==r)
1098 throw new Error("No Compensation Update could be found");
1101 public void generate_dispatch(CodeWriter cr, RelationDescriptor rd, String leftvar, String rightvar) {
1102 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
1103 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
1105 if (!(usageinvimage||usageimage)) /* not used at all*/
1108 cr.outputline("// RELATION DISPATCH ");
1109 cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1111 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hash->contains("+leftvar+","+rightvar+"))");
1113 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+rd.getJustSafeSymbol()+"_hashinv->contains("+rightvar+","+leftvar+"))");
1115 /* Adding new item */
1116 /* Perform safety checks */
1117 cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1118 cr.outputline(repairtable.getSafeSymbol()+"->containsrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+"))");
1120 /* Have update to call into */
1121 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1123 for(int i=0;i<currentrule.numQuantifiers();i++) {
1124 if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1125 parttype=parttype+", int, int";
1127 parttype=parttype+", int";
1129 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1130 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getrelation("+rd.getNum()+","+currentrule.getNum()+","+leftvar+","+rightvar+");");
1131 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+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;");
1152 /* Build standard compensation actions */
1153 if (need_compensation(currentrule)) {
1154 UpdateNode un=find_compensation(currentrule);
1155 String name=(String)updatenames.get(un);
1156 usedupdates.add(un); /* Mark as used */
1157 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+repairtable.getSafeSymbol();
1158 for(int i=0;i<currentrule.numQuantifiers();i++) {
1159 Quantifier q=currentrule.getQuantifier(i);
1160 if (q instanceof SetQuantifier) {
1161 SetQuantifier sq=(SetQuantifier) q;
1162 methodcall+=","+sq.getVar().getSafeSymbol();
1163 } else if (q instanceof RelationQuantifier) {
1164 RelationQuantifier rq=(RelationQuantifier) q;
1165 methodcall+=","+rq.x.getSafeSymbol();
1166 methodcall+=","+rq.y.getSafeSymbol();
1167 } else if (q instanceof ForQuantifier) {
1168 ForQuantifier fq=(ForQuantifier) q;
1169 methodcall+=","+fq.getVar().getSafeSymbol();
1173 cr.outputline(methodcall);
1174 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1175 cr.outputline("continue;");
1180 String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1181 cr.outputline("int " + addeditem + ";");
1182 if (rd.testUsage(RelationDescriptor.IMAGE)) {
1183 cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hash->add((int)" + leftvar + ", (int)" + rightvar + ");");
1186 if (rd.testUsage(RelationDescriptor.INVIMAGE)) {
1187 cr.outputline(addeditem + " = " + rd.getSafeSymbol() + "_hashinv->add((int)" + rightvar + ", (int)" + leftvar + ");");
1190 cr.outputline("if (" + addeditem + ")");
1193 Vector dispatchrules = getrulelist(rd);
1195 if (dispatchrules.size() == 0) {
1196 cr.outputline("// nothing to dispatch");
1201 for(int i = 0; i < dispatchrules.size(); i++) {
1202 Rule rule = (Rule) dispatchrules.elementAt(i);
1203 if (rule.getGuardExpr().getRequiredDescriptors().contains(rd)) {
1204 /* Guard depends on this relation, so we recomput everything */
1205 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1207 for (int j=0;j<rule.numQuantifiers();j++) {
1208 Quantifier q=rule.getQuantifier(j);
1209 if (q.getRequiredDescriptors().contains(rd)) {
1211 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+leftvar+","+rightvar+");");
1220 public void generate_dispatch(CodeWriter cr, SetDescriptor sd, String setvar) {
1222 cr.outputline("// SET DISPATCH ");
1224 cr.outputline("if ("+oldmodel.getSafeSymbol()+"&&");
1225 cr.outputline("!"+oldmodel.getSafeSymbol() +"->"+sd.getJustSafeSymbol()+"_hash->contains("+setvar+"))");
1227 /* Adding new item */
1228 /* Perform safety checks */
1229 cr.outputline("if ("+repairtable.getSafeSymbol()+"&&");
1230 cr.outputline(repairtable.getSafeSymbol()+"->containsset("+sd.getNum()+","+currentrule.getNum()+","+setvar+"))");
1232 /* Have update to call into */
1233 VarDescriptor funptr=VarDescriptor.makeNew("updateptr");
1235 for(int i=0;i<currentrule.numQuantifiers();i++) {
1236 if (currentrule.getQuantifier(i) instanceof RelationQuantifier)
1237 parttype=parttype+", int, int";
1239 parttype=parttype+", int";
1241 cr.outputline("void (*"+funptr.getSafeSymbol()+") ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")=");
1242 cr.outputline("(void (*) ("+name+"_state *,"+name+"*,RepairHash *"+parttype+")) "+repairtable.getSafeSymbol()+"->getset("+sd.getNum()+","+currentrule.getNum()+","+setvar+");");
1243 String methodcall="("+funptr.getSafeSymbol()+") (this,"+oldmodel.getSafeSymbol()+","+
1244 repairtable.getSafeSymbol();
1245 for(int i=0;i<currentrule.numQuantifiers();i++) {
1246 Quantifier q=currentrule.getQuantifier(i);
1247 if (q instanceof SetQuantifier) {
1248 SetQuantifier sq=(SetQuantifier) q;
1249 methodcall+=","+sq.getVar().getSafeSymbol();
1250 } else if (q instanceof RelationQuantifier) {
1251 RelationQuantifier rq=(RelationQuantifier) q;
1252 methodcall+=","+rq.x.getSafeSymbol();
1253 methodcall+=","+rq.y.getSafeSymbol();
1254 } else if (q instanceof ForQuantifier) {
1255 ForQuantifier fq=(ForQuantifier) q;
1256 methodcall+=","+fq.getVar().getSafeSymbol();
1260 cr.outputline(methodcall);
1261 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1262 cr.outputline("continue;");
1265 /* Build standard compensation actions */
1266 if (need_compensation(currentrule)) {
1267 UpdateNode un=find_compensation(currentrule);
1268 String name=(String)updatenames.get(un);
1269 usedupdates.add(un); /* Mark as used */
1271 String methodcall=name+"(this,"+oldmodel.getSafeSymbol()+","+
1272 repairtable.getSafeSymbol();
1273 for(int i=0;i<currentrule.numQuantifiers();i++) {
1274 Quantifier q=currentrule.getQuantifier(i);
1275 if (q instanceof SetQuantifier) {
1276 SetQuantifier sq=(SetQuantifier) q;
1277 methodcall+=","+sq.getVar().getSafeSymbol();
1278 } else if (q instanceof RelationQuantifier) {
1279 RelationQuantifier rq=(RelationQuantifier) q;
1280 methodcall+=","+rq.x.getSafeSymbol();
1281 methodcall+=","+rq.y.getSafeSymbol();
1282 } else if (q instanceof ForQuantifier) {
1283 ForQuantifier fq=(ForQuantifier) q;
1284 methodcall+=","+fq.getVar().getSafeSymbol();
1288 cr.outputline(methodcall);
1289 cr.outputline(goodflag.getSafeSymbol()+"=0;");
1290 cr.outputline("continue;");
1295 String addeditem = (VarDescriptor.makeNew("addeditem")).getSafeSymbol();
1296 cr.outputline("int " + addeditem + " = 1;");
1297 cr.outputline(addeditem + " = " + sd.getSafeSymbol() + "_hash->add((int)" + setvar + ", (int)" + setvar + ");");
1299 Vector dispatchrules = getrulelist(sd);
1301 if (dispatchrules.size() == 0) {
1302 cr.outputline("// nothing to dispatch");
1307 for(int i = 0; i < dispatchrules.size(); i++) {
1308 Rule rule = (Rule) dispatchrules.elementAt(i);
1309 if (SetDescriptor.expand(rule.getGuardExpr().getRequiredDescriptors()).contains(sd)) {
1310 /* Guard depends on this relation, so we recompute everything */
1311 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+",-1,0,0);");
1313 for (int j=0;j<rule.numQuantifiers();j++) {
1314 Quantifier q=rule.getQuantifier(j);
1315 if (SetDescriptor.expand(q.getRequiredDescriptors()).contains(sd)) {
1317 cr.outputline(worklist.getSafeSymbol()+"->add("+rule.getNum()+","+j+","+setvar+",0);");