13 public UpdateNode(Rule r) {
15 bindings=new Vector();
16 invariants=new Vector();
17 binding=new Hashtable();
21 public Rule getRule() {
25 public String toString() {
28 for(int i=0;i<bindings.size();i++)
29 st+=bindings.get(i).toString()+"\n";
30 st+="---------------------\n";
32 for(int i=0;i<updates.size();i++)
33 st+=updates.get(i).toString()+"\n";
34 st+="---------------------\n";
36 for(int i=0;i<invariants.size();i++)
37 st+=((Expr)invariants.get(i)).name()+"\n";
38 st+="---------------------\n";
42 public void addBindings(Vector v) {
43 for (int i=0;i<v.size();i++) {
44 addBinding((Binding)v.get(i));
48 public boolean checkupdates(State state) {
49 if (!checkconflicts()) /* Do we have conflicting concrete updates */
51 if (!checknoupdates(state))
53 if (computeordering()) /* Ordering exists */
58 private boolean checknoupdates(State state) {
59 Set noupdate=state.noupdate;
60 for(int i=0;i<updates.size();i++) {
61 Updates u=(Updates)updates.get(i);
63 continue; /* Abstract updates don't change fields */
64 Descriptor d=u.getDescriptor();
65 if (noupdate.contains(d))
71 private boolean computeordering() {
72 /* Build dependency graph between updates */
73 HashSet graph=new HashSet();
74 Hashtable mapping=new Hashtable();
75 for(int i=0;i<updates.size();i++) {
76 Updates u=(Updates)updates.get(i);
77 GraphNode gn=new GraphNode(String.valueOf(i),u);
81 for(int i=0;i<updates.size();i++) {
82 Updates u1=(Updates)updates.get(i);
85 for(int j=0;j<updates.size();j++) {
86 Updates u2=(Updates)updates.get(j);
89 Descriptor d=u1.getDescriptor();
94 subexpr=((DotExpr)u2.getLeftExpr()).getExpr();
95 intindex=((DotExpr)u2.getLeftExpr()).getIndex();
97 if (u2.getRightExpr().usesDescriptor(d)||
98 (subexpr!=null&&subexpr.usesDescriptor(d))||
99 (intindex!=null&&intindex.usesDescriptor(d))) {
100 /* Add edge for dependency */
101 GraphNode gn1=(GraphNode) mapping.get(u1);
102 GraphNode gn2=(GraphNode) mapping.get(u2);
103 GraphNode.Edge e=new GraphNode.Edge("dependency",gn2);
109 if (!GraphNode.DFS.depthFirstSearch(graph)) /* DFS & check for acyclicity */
112 TreeSet topologicalsort = new TreeSet(new Comparator() {
113 public boolean equals(Object obj) { return false; }
114 public int compare(Object o1, Object o2) {
115 GraphNode g1 = (GraphNode) o1;
116 GraphNode g2 = (GraphNode) o2;
117 return g2.getFinishingTime() - g1.getFinishingTime();
120 topologicalsort.addAll(graph);
121 Vector sortedvector=new Vector();
122 for(Iterator sort=topologicalsort.iterator();sort.hasNext();) {
123 GraphNode gn=(GraphNode)sort.next();
124 sortedvector.add(gn.getOwner());
126 updates=sortedvector; //replace updates with the sorted array
130 private boolean checkconflicts() {
131 Set toremove=new HashSet();
132 for(int i=0;i<updates.size();i++) {
133 Updates u1=(Updates)updates.get(i);
134 if (!u1.isAbstract()) {
135 Descriptor d=u1.getDescriptor();
136 for(int j=0;j<invariants.size();j++) {
137 Expr invariant=(Expr)invariants.get(j);
138 if (invariant.usesDescriptor(d))
142 for(int j=0;j<updates.size();j++) {
143 Updates u2=(Updates)updates.get(j);
146 if (u1.isAbstract()||u2.isAbstract())
147 continue; /* Abstract updates are already accounted for by graph */
148 if (u1.getDescriptor()!=u2.getDescriptor())
149 continue; /* No interference - different descriptors */
151 if ((u1.getOpcode()==Opcode.GT||u1.getOpcode()==Opcode.GE)&&
152 (u2.getOpcode()==Opcode.GT||u2.getOpcode()==Opcode.GE))
153 continue; /* Can be satisfied simultaneously */
155 if ((u1.getOpcode()==Opcode.LT||u1.getOpcode()==Opcode.LE)&&
156 (u2.getOpcode()==Opcode.LT||u2.getOpcode()==Opcode.LE))
158 if ((u1.getOpcode()==u2.getOpcode())&&
159 u1.isExpr()&&u2.isExpr()&&
160 u1.getRightExpr().equals(null, u2.getRightExpr())) {
161 /*We'll remove the second occurence*/
169 /* Handle = or != NULL */
170 if ((((u1.getOpcode()==Opcode.EQ)&&(u2.getOpcode()==Opcode.NE))||
171 ((u1.getOpcode()==Opcode.NE)&&(u2.getOpcode()==Opcode.EQ)))&&
172 (((u1.isExpr()&&u1.getRightExpr().isNull())&&(!u2.isExpr()||u2.getRightExpr().isNonNull()))
173 ||((!u1.isExpr()||u1.getRightExpr().isNonNull())&&(u2.isExpr()&&u2.getRightExpr().isNull())))) {
174 if (u1.getOpcode()==Opcode.NE)
181 /* Handle = and != to different constants */
182 if ((((u1.getOpcode()==Opcode.EQ)&&(u2.getOpcode()==Opcode.NE))||
183 ((u1.getOpcode()==Opcode.NE)&&(u2.getOpcode()==Opcode.EQ)))&&
184 (u1.isExpr()&&u1.getRightExpr() instanceof LiteralExpr)&&
185 (u2.isExpr()&&u2.getRightExpr() instanceof LiteralExpr)&&
186 !u1.getRightExpr().equals(u2.getRightExpr())) {
187 if (u1.getOpcode()==Opcode.NE)
194 /* Compatible operations < & <= */
195 if (((u1.getOpcode()==Opcode.LT)||(u1.getOpcode()==Opcode.LE))&&
196 ((u2.getOpcode()==Opcode.LT)||(u2.getOpcode()==Opcode.LE)))
199 /* Compatible operations > & >= */
200 if (((u1.getOpcode()==Opcode.GT)||(u1.getOpcode()==Opcode.GE))&&
201 ((u2.getOpcode()==Opcode.GT)||(u2.getOpcode()==Opcode.GE)))
206 /* Equality & Comparisons */
209 return false; /* They interfere */
212 updates.removeAll(toremove);
216 public void addBinding(Binding b) {
218 binding.put(b.getVar(),b);
221 public int numBindings() {
222 return bindings.size();
225 public Binding getBinding(int i) {
226 return (Binding)bindings.get(i);
229 public Binding getBinding(VarDescriptor vd) {
230 if (binding.containsKey(vd))
231 return (Binding)binding.get(vd);
236 public void addInvariant(Expr e) {
240 public int numInvariants() {
241 return invariants.size();
244 public Expr getInvariant(int i) {
245 return (Expr)invariants.get(i);
248 public void addUpdate(Updates u) {
252 public int numUpdates() {
253 return updates.size();
255 public Updates getUpdate(int i) {
256 return (Updates)updates.get(i);
259 private MultUpdateNode getMultUpdateNode(boolean negate, Descriptor d, RepairGenerator rg) {
260 Termination termination=rg.termination;
261 MultUpdateNode mun=null;
264 gn=(GraphNode)termination.abstractremove.get(d);
266 gn=(GraphNode)termination.abstractadd.get(d);
267 TermNode tn=(TermNode)gn.getOwner();
268 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
269 GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
270 if (!rg.removed.contains(gn2)) {
271 TermNode tn2=(TermNode)gn2.getOwner();
272 if (tn2.getType()==TermNode.UPDATE) {
279 throw new Error("Can't find update node!");
283 public void generate_abstract(CodeWriter cr, Updates u, RepairGenerator rg) {
284 State state=rg.state;
285 Expr abstractexpr=u.getLeftExpr();
286 boolean negated=u.negate;
290 boolean istuple=false;
291 if (abstractexpr instanceof TupleOfExpr) {
292 TupleOfExpr toe=(TupleOfExpr) abstractexpr;
297 } else if (abstractexpr instanceof ElementOfExpr) {
298 ElementOfExpr eoe=(ElementOfExpr) abstractexpr;
303 throw new Error("Unsupported Expr");
305 MultUpdateNode mun=getMultUpdateNode(negated,d,rg);
306 VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
307 VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
308 left.generate(cr, leftvar);
310 right.generate(cr,rightvar);
314 RelationDescriptor rd=(RelationDescriptor)d;
315 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
316 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
318 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
320 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
322 for(int i=0;i<state.vRules.size();i++) {
323 Rule r=(Rule)state.vRules.get(i);
324 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
325 for(int j=0;j<mun.numUpdates();j++) {
326 UpdateNode un=mun.getUpdate(i);
327 if (un.getRule()==r) {
328 /* Update for rule rule r */
329 String name=(String)rg.updatenames.get(un);
330 cr.outputline("RepairHashaddrelation("+rg.strepairtable+","+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
336 SetDescriptor sd=(SetDescriptor) d;
337 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
339 for(int i=0;i<state.vRules.size();i++) {
340 Rule r=(Rule)state.vRules.get(i);
341 if (r.getInclusion().getTargetDescriptors().contains(sd)) {
342 for(int j=0;j<mun.numUpdates();j++) {
343 UpdateNode un=mun.getUpdate(j);
344 if (un.getRule()==r) {
345 /* Update for rule rule r */
346 String name=(String)rg.updatenames.get(un);
347 cr.outputline("RepairHashaddset("+rg.strepairtable+","+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
354 /* Generate update */
356 RelationDescriptor rd=(RelationDescriptor) d;
357 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
358 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
360 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
362 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
364 UpdateNode un=mun.getUpdate(0);
365 String name=(String)rg.updatenames.get(un);
366 cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
368 SetDescriptor sd=(SetDescriptor)d;
369 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
371 UpdateNode un=mun.getUpdate(0);
372 /* Update for rule rule r */
373 String name=(String)rg.updatenames.get(un);
374 cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+");");
379 public void generate(CodeWriter cr, boolean removal, boolean modify, String slot0, String slot1, String slot2, RepairGenerator rg) {
380 if (!removal&&!modify)
381 generate_bindings(cr, slot0,slot1);
382 for(int i=0;i<updates.size();i++) {
383 Updates u=(Updates)updates.get(i);
384 VarDescriptor right=VarDescriptor.makeNew("right");
385 if (u.getType()==Updates.ABSTRACT) {
386 generate_abstract(cr, u, rg);
390 switch(u.getType()) {
392 u.getRightExpr().generate(cr,right);
394 case Updates.POSITION:
395 case Updates.ACCESSPATH:
396 if (u.getRightPos()==0) {
397 cr.addDeclaration("int", right.getSafeSymbol());
398 cr.outputline(right.getSafeSymbol()+"="+slot0+";");
399 } else if (u.getRightPos()==1) {
400 cr.addDeclaration("int", right.getSafeSymbol());
401 cr.outputline(right.getSafeSymbol()+"="+slot1+";");
402 } else if (u.getRightPos()==2) {
403 cr.addDeclaration("int", right.getSafeSymbol());
404 cr.outputline(right.getSafeSymbol()+"="+slot2+";");
405 } else throw new Error("Error w/ Position");
411 if (u.getType()==Updates.ACCESSPATH) {
412 VarDescriptor newright=VarDescriptor.makeNew("right");
413 generate_accesspath(cr, right,newright,u);
416 VarDescriptor left=VarDescriptor.makeNew("left");
417 u.getLeftExpr().generate(cr,left);
418 Opcode op=u.getOpcode();
419 cr.outputline("if (!("+left.getSafeSymbol()+op+right.getSafeSymbol()+"))");
423 cr.outputline(right.getSafeSymbol()+"++;");
424 else if (op==Opcode.GE)
426 else if (op==Opcode.EQ)
428 else if (op==Opcode.NE)
429 cr.outputline(right.getSafeSymbol()+"++;");
430 else if (op==Opcode.LT)
431 cr.outputline(right.getSafeSymbol()+"--;");
432 else if (op==Opcode.LE)
434 else throw new Error();
437 VarDescriptor vd=((VarExpr)u.getLeftExpr()).getVar();
438 cr.outputline(vd.getSafeSymbol()+"="+right.getSafeSymbol()+";");
439 if (Compiler.PRINTREPAIRS) {
440 cr.outputline("printf(\""+u.getLeftExpr().toString()+"=%d\\n\","+right.getSafeSymbol()+");");
442 } else if (u.isField()) {
444 Expr subexpr=((DotExpr)u.getLeftExpr()).getExpr();
445 Expr intindex=((DotExpr)u.getLeftExpr()).getIndex();
446 VarDescriptor subvd=VarDescriptor.makeNew("subexpr");
447 VarDescriptor indexvd=VarDescriptor.makeNew("index");
448 subexpr.generate(cr,subvd);
451 intindex.generate(cr,indexvd);
452 FieldDescriptor fd=(FieldDescriptor)u.getDescriptor();
453 if (Compiler.PRINTREPAIRS) {
454 if (intindex==null) {
455 cr.outputline("printf(\"0x%x."+fd.toString()+
456 "=%d\\n\","+subvd.getSafeSymbol()+","+right.getSafeSymbol()+");");
458 cr.outputline("printf(\"0x%x."+fd.toString()+
459 "[%d]=%d\\n\","+subvd.getSafeSymbol()+
460 ","+indexvd.getSafeSymbol()+","+right.getSafeSymbol()+");");
465 StructureTypeDescriptor std=(StructureTypeDescriptor)subexpr.getType();
466 Expr offsetbits = std.getOffsetExpr(fd);
467 if (fd instanceof ArrayDescriptor) {
468 fd = ((ArrayDescriptor) fd).getField();
471 if (intindex != null) {
472 Expr basesize = fd.getBaseSizeExpr();
473 offsetbits = new OpExpr(Opcode.ADD, offsetbits, new OpExpr(Opcode.MULT, basesize, intindex));
475 Expr offsetbytes = new OpExpr(Opcode.SHR, offsetbits,new IntegerLiteralExpr(3));
476 Expr byteaddress=new OpExpr(Opcode.ADD, offsetbytes, subexpr);
477 VarDescriptor addr=VarDescriptor.makeNew("byteaddress");
478 byteaddress.generate(cr,addr);
480 if (fd.getType() instanceof ReservedTypeDescriptor && !fd.getPtr()) {
481 ReservedTypeDescriptor rtd=(ReservedTypeDescriptor)fd.getType();
482 if (rtd==ReservedTypeDescriptor.INT) {
483 cr.outputline("*((int *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
484 } else if (rtd==ReservedTypeDescriptor.SHORT) {
485 cr.outputline("*((short *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
486 } else if (rtd==ReservedTypeDescriptor.BYTE) {
487 cr.outputline("*((char *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
488 } else if (rtd==ReservedTypeDescriptor.BIT) {
489 Expr tmp = new OpExpr(Opcode.SHL, offsetbytes, new IntegerLiteralExpr(3));
490 Expr offset=new OpExpr(Opcode.SUB, offsetbits, tmp);
491 Expr mask=new OpExpr(Opcode.SHL, new IntegerLiteralExpr(1), offset);
492 VarDescriptor maskvar=VarDescriptor.makeNew("mask");
493 mask.generate(cr,maskvar);
494 cr.outputline("*((char *) "+addr.getSafeSymbol()+")|="+maskvar.getSafeSymbol()+";");
495 cr.outputline("if (!"+right.getSafeSymbol()+")");
496 cr.outputline("*((char *) "+addr.getSafeSymbol()+")^="+maskvar.getSafeSymbol()+";");
497 } else throw new Error();
500 cr.outputline("*((int *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
508 private void generate_accesspath(CodeWriter cr, VarDescriptor right, VarDescriptor newright, Updates u) {
509 Vector dotvector=new Vector();
510 Expr ptr=u.getRightExpr();
511 VarExpr rightve=new VarExpr(right);
512 right.td=ReservedTypeDescriptor.INT;
515 /* Does something other than a dereference? */
517 if (ptr instanceof DotExpr)
518 ptr=((DotExpr)ptr).left;
519 else if (ptr instanceof CastExpr)
520 ptr=((CastExpr)ptr).getExpr();
521 if (ptr instanceof VarExpr) {
522 /* Finished constructing vector */
526 ArrayAnalysis.AccessPath ap=u.getAccessPath();
527 VarDescriptor init=VarDescriptor.makeNew("init");
529 cr.addDeclaration("int", init.getSafeSymbol());
530 cr.outputline(init.getSafeSymbol()+"= SimpleHashfirstkey("+ap.getSet().getSafeSymbol()+"_hash);");
531 init.td=ap.getSet().getType();
535 Expr newexpr=new VarExpr(init);
537 for(int i=dotvector.size()-1;i>=0;i--) {
538 Expr e=(Expr)dotvector.get(i);
539 if (e instanceof CastExpr) {
541 newexpr=new CastExpr(((CastExpr)e).getType(),newexpr);
542 } else if (e instanceof DotExpr) {
543 DotExpr de=(DotExpr)e;
544 if (de.getField() instanceof ArrayDescriptor) {
545 DotExpr de2=new DotExpr(newexpr,de.field,new IntegerLiteralExpr(0));
547 de2.fieldtype=de.fieldtype;
549 OpExpr offset=new OpExpr(Opcode.SUB,rightve,de2);
550 OpExpr index=new OpExpr(Opcode.DIV,offset,de.fieldtype.getSizeExpr());
551 if (u.getRightPos()==apindex) {
552 index.generate(cr,newright);
555 DotExpr de3=new DotExpr(newexpr,de.field,index);
558 de3.fieldtype=de.fieldtype;
562 DotExpr de2=new DotExpr(newexpr,de.field,null);
564 de2.fieldtype=de.fieldtype;
569 } else throw new Error();
574 private void generate_bindings(CodeWriter cr, String slot0, String slot1) {
575 for(int i=0;i<bindings.size();i++) {
576 Binding b=(Binding)bindings.get(i);
578 if (b.getType()==Binding.SEARCH) {
579 VarDescriptor vd=b.getVar();
580 cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
581 cr.outputline(vd.getSafeSymbol()+"=SimpleHashfirstkey("+b.getSet().getSafeSymbol()+"_hash);");
582 } else if (b.getType()==Binding.CREATE) {
583 throw new Error("Creation not supported");
584 // source.generateSourceAlloc(cr,vd,b.getSet());
586 VarDescriptor vd=b.getVar();
587 switch(b.getPosition()) {
589 cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
590 cr.outputline(vd.getSafeSymbol()+"="+slot0+";");
593 cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
594 cr.outputline(vd.getSafeSymbol()+"="+slot1+";");
597 throw new Error("Slot >1 doesn't exist.");