12 public UpdateNode(Rule r) {
14 bindings=new Vector();
15 invariants=new Vector();
16 binding=new Hashtable();
20 public Rule getRule() {
24 public String toString() {
27 for(int i=0;i<bindings.size();i++)
28 st+=bindings.get(i).toString()+"\n";
29 st+="---------------------\n";
31 for(int i=0;i<updates.size();i++)
32 st+=updates.get(i).toString()+"\n";
33 st+="---------------------\n";
35 for(int i=0;i<invariants.size();i++)
36 st+=((Expr)invariants.get(i)).name()+"\n";
37 st+="---------------------\n";
41 public void addBindings(Vector v) {
42 for (int i=0;i<v.size();i++) {
43 addBinding((Binding)v.get(i));
47 public boolean checkupdates() {
48 if (!checkconflicts()) /* Do we have conflicting concrete updates */
50 if (computeordering()) /* Ordering exists */
55 private boolean computeordering() {
56 /* Build dependency graph between updates */
57 HashSet graph=new HashSet();
58 Hashtable mapping=new Hashtable();
59 for(int i=0;i<updates.size();i++) {
60 Updates u=(Updates)updates.get(i);
61 GraphNode gn=new GraphNode(String.valueOf(i),u);
65 for(int i=0;i<updates.size();i++) {
66 Updates u1=(Updates)updates.get(i);
69 for(int j=0;j<updates.size();j++) {
70 Updates u2=(Updates)updates.get(j);
73 Descriptor d=u1.getDescriptor();
78 subexpr=((DotExpr)u2.getLeftExpr()).getExpr();
79 intindex=((DotExpr)u2.getLeftExpr()).getIndex();
81 if (u2.getRightExpr().usesDescriptor(d)||
82 (subexpr!=null&&subexpr.usesDescriptor(d))||
83 (intindex!=null&&intindex.usesDescriptor(d))) {
84 /* Add edge for dependency */
85 GraphNode gn1=(GraphNode) mapping.get(u1);
86 GraphNode gn2=(GraphNode) mapping.get(u2);
87 GraphNode.Edge e=new GraphNode.Edge("dependency",gn2);
93 if (!GraphNode.DFS.depthFirstSearch(graph)) /* DFS & check for acyclicity */
96 TreeSet topologicalsort = new TreeSet(new Comparator() {
97 public boolean equals(Object obj) { return false; }
98 public int compare(Object o1, Object o2) {
99 GraphNode g1 = (GraphNode) o1;
100 GraphNode g2 = (GraphNode) o2;
101 return g2.getFinishingTime() - g1.getFinishingTime();
104 topologicalsort.addAll(graph);
105 Vector sortedvector=new Vector();
106 for(Iterator sort=topologicalsort.iterator();sort.hasNext();) {
107 GraphNode gn=(GraphNode)sort.next();
108 sortedvector.add(gn.getOwner());
110 updates=sortedvector; //replace updates with the sorted array
114 private boolean checkconflicts() {
115 Set toremove=new HashSet();
116 for(int i=0;i<updates.size();i++) {
117 Updates u1=(Updates)updates.get(i);
118 if (!u1.isAbstract()) {
119 Descriptor d=u1.getDescriptor();
120 for(int j=0;j<invariants.size();j++) {
121 Expr invariant=(Expr)invariants.get(j);
122 if (invariant.usesDescriptor(d))
126 for(int j=0;j<updates.size();j++) {
127 Updates u2=(Updates)updates.get(j);
130 if (u1.isAbstract()||u2.isAbstract())
131 continue; /* Abstract updates are already accounted for by graph */
132 if (u1.getDescriptor()!=u2.getDescriptor())
133 continue; /* No interference - different descriptors */
135 if ((u1.getOpcode()==Opcode.GT||u1.getOpcode()==Opcode.GE)&&
136 (u2.getOpcode()==Opcode.GT||u2.getOpcode()==Opcode.GE))
137 continue; /* Can be satisfied simultaneously */
139 if ((u1.getOpcode()==Opcode.LT||u1.getOpcode()==Opcode.LE)&&
140 (u2.getOpcode()==Opcode.LT||u2.getOpcode()==Opcode.LE))
142 if ((u1.getOpcode()==u2.getOpcode())&&
143 u1.isExpr()&&u2.isExpr()&&
144 u1.getRightExpr().equals(null, u2.getRightExpr())) {
145 /*We'll remove the second occurence*/
153 /* Handle = or != NULL */
154 if ((((u1.getOpcode()==Opcode.EQ)&&(u2.getOpcode()==Opcode.NE))||
155 ((u1.getOpcode()==Opcode.NE)&&(u2.getOpcode()==Opcode.EQ)))&&
156 (((u1.isExpr()&&u1.getRightExpr().isNull())&&(!u2.isExpr()||u2.getRightExpr().isNonNull()))
157 ||((!u1.isExpr()||u1.getRightExpr().isNonNull())&&(u2.isExpr()&&u2.getRightExpr().isNull())))) {
158 if (u1.getOpcode()==Opcode.NE)
165 /* Handle = and != to different constants */
166 if ((((u1.getOpcode()==Opcode.EQ)&&(u2.getOpcode()==Opcode.NE))||
167 ((u1.getOpcode()==Opcode.NE)&&(u2.getOpcode()==Opcode.EQ)))&&
168 (u1.isExpr()&&u1.getRightExpr() instanceof LiteralExpr)&&
169 (u2.isExpr()&&u2.getRightExpr() instanceof LiteralExpr)&&
170 !u1.getRightExpr().equals(u2.getRightExpr())) {
171 if (u1.getOpcode()==Opcode.NE)
178 /* Compatible operations < & <= */
179 if (((u1.getOpcode()==Opcode.LT)||(u1.getOpcode()==Opcode.LE))&&
180 ((u2.getOpcode()==Opcode.LT)||(u2.getOpcode()==Opcode.LE)))
183 /* Compatible operations > & >= */
184 if (((u1.getOpcode()==Opcode.GT)||(u1.getOpcode()==Opcode.GE))&&
185 ((u2.getOpcode()==Opcode.GT)||(u2.getOpcode()==Opcode.GE)))
190 /* Equality & Comparisons */
193 return false; /* They interfere */
196 updates.removeAll(toremove);
200 public void addBinding(Binding b) {
202 binding.put(b.getVar(),b);
205 public int numBindings() {
206 return bindings.size();
209 public Binding getBinding(int i) {
210 return (Binding)bindings.get(i);
213 public Binding getBinding(VarDescriptor vd) {
214 if (binding.containsKey(vd))
215 return (Binding)binding.get(vd);
220 public void addInvariant(Expr e) {
224 public int numInvariants() {
225 return invariants.size();
228 public Expr getInvariant(int i) {
229 return (Expr)invariants.get(i);
232 public void addUpdate(Updates u) {
236 public int numUpdates() {
237 return updates.size();
239 public Updates getUpdate(int i) {
240 return (Updates)updates.get(i);
243 private MultUpdateNode getMultUpdateNode(boolean negate, Descriptor d, RepairGenerator rg) {
244 Termination termination=rg.termination;
245 MultUpdateNode mun=null;
248 gn=(GraphNode)termination.abstractremove.get(d);
250 gn=(GraphNode)termination.abstractadd.get(d);
251 TermNode tn=(TermNode)gn.getOwner();
252 for(Iterator edgeit=gn.edges();edgeit.hasNext();) {
253 GraphNode gn2=((GraphNode.Edge) edgeit.next()).getTarget();
254 if (!rg.removed.contains(gn2)) {
255 TermNode tn2=(TermNode)gn2.getOwner();
256 if (tn2.getType()==TermNode.UPDATE) {
263 throw new Error("Can't find update node!");
267 public void generate_abstract(CodeWriter cr, Updates u, RepairGenerator rg) {
268 State state=rg.state;
269 Expr abstractexpr=u.getLeftExpr();
270 boolean negated=u.negate;
274 boolean istuple=false;
275 if (abstractexpr instanceof TupleOfExpr) {
276 TupleOfExpr toe=(TupleOfExpr) abstractexpr;
281 } else if (abstractexpr instanceof ElementOfExpr) {
282 ElementOfExpr eoe=(ElementOfExpr) abstractexpr;
287 throw new Error("Unsupported Expr");
289 MultUpdateNode mun=getMultUpdateNode(negated,d,rg);
290 VarDescriptor leftvar=VarDescriptor.makeNew("leftvar");
291 VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
292 left.generate(cr, leftvar);
294 right.generate(cr,rightvar);
298 RelationDescriptor rd=(RelationDescriptor)d;
299 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
300 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
302 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
304 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
306 for(int i=0;i<state.vRules.size();i++) {
307 Rule r=(Rule)state.vRules.get(i);
308 if (r.getInclusion().getTargetDescriptors().contains(rd)) {
309 for(int j=0;j<mun.numUpdates();j++) {
310 UpdateNode un=mun.getUpdate(i);
311 if (un.getRule()==r) {
312 /* Update for rule rule r */
313 String name=(String)rg.updatenames.get(un);
314 cr.outputline("RepairHashaddrelation("+rg.strepairtable+","+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
320 SetDescriptor sd=(SetDescriptor) d;
321 cr.outputline("SimpleHashremove("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
323 for(int i=0;i<state.vRules.size();i++) {
324 Rule r=(Rule)state.vRules.get(i);
325 if (r.getInclusion().getTargetDescriptors().contains(sd)) {
326 for(int j=0;j<mun.numUpdates();j++) {
327 UpdateNode un=mun.getUpdate(j);
328 if (un.getRule()==r) {
329 /* Update for rule rule r */
330 String name=(String)rg.updatenames.get(un);
331 cr.outputline("RepairHashaddset("+rg.strepairtable+","+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
338 /* Generate update */
340 RelationDescriptor rd=(RelationDescriptor) d;
341 boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
342 boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
344 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
346 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
348 UpdateNode un=mun.getUpdate(0);
349 String name=(String)rg.updatenames.get(un);
350 cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
352 SetDescriptor sd=(SetDescriptor)d;
353 cr.outputline("SimpleHashadd("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
355 UpdateNode un=mun.getUpdate(0);
356 /* Update for rule rule r */
357 String name=(String)rg.updatenames.get(un);
358 cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+");");
363 public void generate(CodeWriter cr, boolean removal, boolean modify, String slot0, String slot1, String slot2, RepairGenerator rg) {
364 if (!removal&&!modify)
365 generate_bindings(cr, slot0,slot1);
366 for(int i=0;i<updates.size();i++) {
367 Updates u=(Updates)updates.get(i);
368 VarDescriptor right=VarDescriptor.makeNew("right");
369 if (u.getType()==Updates.ABSTRACT) {
370 generate_abstract(cr, u, rg);
374 switch(u.getType()) {
376 u.getRightExpr().generate(cr,right);
378 case Updates.POSITION:
379 case Updates.ACCESSPATH:
380 if (u.getRightPos()==0)
381 cr.outputline("int "+right.getSafeSymbol()+"="+slot0+";");
382 else if (u.getRightPos()==1)
383 cr.outputline("int "+right.getSafeSymbol()+"="+slot1+";");
384 else if (u.getRightPos()==2)
385 cr.outputline("int "+right.getSafeSymbol()+"="+slot2+";");
386 else throw new Error("Error w/ Position");
392 if (u.getType()==Updates.ACCESSPATH) {
393 VarDescriptor newright=VarDescriptor.makeNew("right");
394 generate_accesspath(cr, right,newright,u);
397 VarDescriptor left=VarDescriptor.makeNew("left");
398 u.getLeftExpr().generate(cr,left);
399 Opcode op=u.getOpcode();
400 cr.outputline("if (!("+left.getSafeSymbol()+op+right.getSafeSymbol()+"))");
404 cr.outputline(right.getSafeSymbol()+"++;");
405 else if (op==Opcode.GE)
407 else if (op==Opcode.EQ)
409 else if (op==Opcode.NE)
410 cr.outputline(right.getSafeSymbol()+"++;");
411 else if (op==Opcode.LT)
412 cr.outputline(right.getSafeSymbol()+"--;");
413 else if (op==Opcode.LE)
415 else throw new Error();
417 VarDescriptor vd=((VarExpr)u.getLeftExpr()).getVar();
418 cr.outputline(vd.getSafeSymbol()+"="+right.getSafeSymbol()+";");
419 } else if (u.isField()) {
421 Expr subexpr=((DotExpr)u.getLeftExpr()).getExpr();
422 Expr intindex=((DotExpr)u.getLeftExpr()).getIndex();
423 VarDescriptor subvd=VarDescriptor.makeNew("subexpr");
424 VarDescriptor indexvd=VarDescriptor.makeNew("index");
425 subexpr.generate(cr,subvd);
427 intindex.generate(cr,indexvd);
428 FieldDescriptor fd=(FieldDescriptor)u.getDescriptor();
429 StructureTypeDescriptor std=(StructureTypeDescriptor)subexpr.getType();
430 Expr offsetbits = std.getOffsetExpr(fd);
431 if (fd instanceof ArrayDescriptor) {
432 fd = ((ArrayDescriptor) fd).getField();
435 if (intindex != null) {
436 Expr basesize = fd.getBaseSizeExpr();
437 offsetbits = new OpExpr(Opcode.ADD, offsetbits, new OpExpr(Opcode.MULT, basesize, intindex));
439 Expr offsetbytes = new OpExpr(Opcode.SHR, offsetbits,new IntegerLiteralExpr(3));
440 Expr byteaddress=new OpExpr(Opcode.ADD, offsetbytes, subexpr);
441 VarDescriptor addr=VarDescriptor.makeNew("byteaddress");
442 byteaddress.generate(cr,addr);
444 if (fd.getType() instanceof ReservedTypeDescriptor && !fd.getPtr()) {
445 ReservedTypeDescriptor rtd=(ReservedTypeDescriptor)fd.getType();
446 if (rtd==ReservedTypeDescriptor.INT) {
447 cr.outputline("*((int *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
448 } else if (rtd==ReservedTypeDescriptor.SHORT) {
449 cr.outputline("*((short *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
450 } else if (rtd==ReservedTypeDescriptor.BYTE) {
451 cr.outputline("*((char *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
452 } else if (rtd==ReservedTypeDescriptor.BIT) {
453 Expr tmp = new OpExpr(Opcode.SHL, offsetbytes, new IntegerLiteralExpr(3));
454 Expr offset=new OpExpr(Opcode.SUB, offsetbits, tmp);
455 Expr mask=new OpExpr(Opcode.SHL, new IntegerLiteralExpr(1), offset);
456 VarDescriptor maskvar=VarDescriptor.makeNew("mask");
457 mask.generate(cr,maskvar);
458 cr.outputline("*((char *) "+addr.getSafeSymbol()+")|="+maskvar.getSafeSymbol()+";");
459 cr.outputline("if (!"+right.getSafeSymbol()+")");
460 cr.outputline("*((char *) "+addr.getSafeSymbol()+")^="+maskvar.getSafeSymbol()+";");
461 } else throw new Error();
464 cr.outputline("*((int *) "+addr.getSafeSymbol()+")="+right.getSafeSymbol()+";");
472 private void generate_accesspath(CodeWriter cr, VarDescriptor right, VarDescriptor newright, Updates u) {
473 Vector dotvector=new Vector();
474 Expr ptr=u.getRightExpr();
475 VarExpr rightve=new VarExpr(right);
476 right.td=ReservedTypeDescriptor.INT;
479 /* Does something other than a dereference? */
481 if (ptr instanceof DotExpr)
482 ptr=((DotExpr)ptr).left;
483 else if (ptr instanceof CastExpr)
484 ptr=((CastExpr)ptr).getExpr();
485 if (ptr instanceof VarExpr) {
486 /* Finished constructing vector */
490 ArrayAnalysis.AccessPath ap=u.getAccessPath();
491 VarDescriptor init=VarDescriptor.makeNew("init");
493 cr.outputline("int "+init.getSafeSymbol()+"= SimpleHashfirstkey("+ap.getSet().getSafeSymbol()+"_hash);");
494 init.td=ap.getSet().getType();
498 Expr newexpr=new VarExpr(init);
500 for(int i=dotvector.size()-1;i>=0;i--) {
501 Expr e=(Expr)dotvector.get(i);
502 if (e instanceof CastExpr) {
504 newexpr=new CastExpr(((CastExpr)e).getType(),newexpr);
505 } else if (e instanceof DotExpr) {
506 DotExpr de=(DotExpr)e;
507 if (de.getField() instanceof ArrayDescriptor) {
508 DotExpr de2=new DotExpr(newexpr,de.field,new IntegerLiteralExpr(0));
510 de2.fieldtype=de.fieldtype;
512 OpExpr offset=new OpExpr(Opcode.SUB,rightve,de2);
513 OpExpr index=new OpExpr(Opcode.DIV,offset,de.fieldtype.getSizeExpr());
514 if (u.getRightPos()==apindex) {
515 index.generate(cr,newright);
518 DotExpr de3=new DotExpr(newexpr,de.field,index);
521 de3.fieldtype=de.fieldtype;
525 DotExpr de2=new DotExpr(newexpr,de.field,null);
527 de2.fieldtype=de.fieldtype;
532 } else throw new Error();
537 private void generate_bindings(CodeWriter cr, String slot0, String slot1) {
538 for(int i=0;i<bindings.size();i++) {
539 Binding b=(Binding)bindings.get(i);
541 if (b.getType()==Binding.SEARCH) {
542 VarDescriptor vd=b.getVar();
543 cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"=SimpleHashfirstkey("+b.getSet().getSafeSymbol()+"_hash);");
544 } else if (b.getType()==Binding.CREATE) {
545 throw new Error("Creation not supported");
546 // source.generateSourceAlloc(cr,vd,b.getSet());
548 VarDescriptor vd=b.getVar();
549 switch(b.getPosition()) {
551 cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+slot0+";");
554 cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+slot1+";");
557 throw new Error("Slot >1 doesn't exist.");