class UpdateNode {
Vector updates;
Vector bindings;
+ Vector invariants;
Hashtable binding;
Rule rule;
-
public UpdateNode(Rule r) {
updates=new Vector();
bindings=new Vector();
+ invariants=new Vector();
binding=new Hashtable();
rule=r;
}
public String toString() {
String st="";
+ st+="Bindings:\n";
for(int i=0;i<bindings.size();i++)
st+=bindings.get(i).toString()+"\n";
st+="---------------------\n";
+ st+="Updates:\n";
for(int i=0;i<updates.size();i++)
st+=updates.get(i).toString()+"\n";
+ st+="---------------------\n";
+ st+="Invariants:\n";
+ for(int i=0;i<invariants.size();i++)
+ st+=((Expr)invariants.get(i)).name()+"\n";
+ st+="---------------------\n";
return st;
}
}
}
- public boolean checkupdates() {
+ public boolean checkupdates(State state) {
if (!checkconflicts()) /* Do we have conflicting concrete updates */
return false;
+ if (!checknoupdates(state))
+ return false;
if (computeordering()) /* Ordering exists */
return true;
return false;
}
+ private boolean checknoupdates(State state) {
+ Set noupdate=state.noupdate;
+ for(int i=0;i<updates.size();i++) {
+ Updates u=(Updates)updates.get(i);
+ if (u.isAbstract())
+ continue; /* Abstract updates don't change fields */
+ Descriptor d=u.getDescriptor();
+ if (noupdate.contains(d))
+ return false;
+ }
+ return true;
+ }
+
private boolean computeordering() {
/* Build dependency graph between updates */
HashSet graph=new HashSet();
if (!u2.isExpr())
continue;
Descriptor d=u1.getDescriptor();
- if (u2.getRightExpr().usesDescriptor(d)) {
+ Expr subexpr=null;
+ Expr intindex=null;
+
+ if (u2.isField()) {
+ subexpr=((DotExpr)u2.getLeftExpr()).getExpr();
+ intindex=((DotExpr)u2.getLeftExpr()).getIndex();
+ }
+ if (u2.getRightExpr().usesDescriptor(d)||
+ (subexpr!=null&&subexpr.usesDescriptor(d))||
+ (intindex!=null&&intindex.usesDescriptor(d))) {
/* Add edge for dependency */
GraphNode gn1=(GraphNode) mapping.get(u1);
GraphNode gn2=(GraphNode) mapping.get(u2);
Set toremove=new HashSet();
for(int i=0;i<updates.size();i++) {
Updates u1=(Updates)updates.get(i);
+ if (!u1.isAbstract()) {
+ Descriptor d=u1.getDescriptor();
+ for(int j=0;j<invariants.size();j++) {
+ Expr invariant=(Expr)invariants.get(j);
+ if (invariant.usesDescriptor(d))
+ return false;
+ }
+ }
for(int j=0;j<updates.size();j++) {
Updates u2=(Updates)updates.get(j);
if (i==j)
continue; /* Abstract updates are already accounted for by graph */
if (u1.getDescriptor()!=u2.getDescriptor())
continue; /* No interference - different descriptors */
-
+
if ((u1.getOpcode()==Opcode.GT||u1.getOpcode()==Opcode.GE)&&
(u2.getOpcode()==Opcode.GT||u2.getOpcode()==Opcode.GE))
continue; /* Can be satisfied simultaneously */
toremove.add(u2);
continue;
}
-
+
/* Compatible operations < & <= */
if (((u1.getOpcode()==Opcode.LT)||(u1.getOpcode()==Opcode.LE))&&
((u2.getOpcode()==Opcode.LT)||(u2.getOpcode()==Opcode.LE)))
public Binding getBinding(int i) {
return (Binding)bindings.get(i);
}
-
+
public Binding getBinding(VarDescriptor vd) {
if (binding.containsKey(vd))
return (Binding)binding.get(vd);
return null;
}
+ public void addInvariant(Expr e) {
+ invariants.add(e);
+ }
+
+ public int numInvariants() {
+ return invariants.size();
+ }
+
+ public Expr getInvariant(int i) {
+ return (Expr)invariants.get(i);
+ }
+
public void addUpdate(Updates u) {
updates.add(u);
}
boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
if (usageimage)
- cr.outputline(rg.stmodel+"->"+rd.getJustSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
+ cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
if (usageinvimage)
- cr.outputline(rg.stmodel+"->"+rd.getJustSafeSymbol() + "_hashinv->remove((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
-
+ cr.outputline("SimpleHashremove("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
+
for(int i=0;i<state.vRules.size();i++) {
Rule r=(Rule)state.vRules.get(i);
if (r.getInclusion().getTargetDescriptors().contains(rd)) {
if (un.getRule()==r) {
/* Update for rule rule r */
String name=(String)rg.updatenames.get(un);
- cr.outputline(rg.strepairtable+"->addrelation("+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
+ cr.outputline("RepairHashaddrelation("+rg.strepairtable+","+rd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+",(int) &"+name+");");
}
}
}
}
} else {
SetDescriptor sd=(SetDescriptor) d;
- cr.outputline(rg.stmodel+"->"+sd.getJustSafeSymbol() + "_hash->remove((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
+ cr.outputline("SimpleHashremove("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
for(int i=0;i<state.vRules.size();i++) {
Rule r=(Rule)state.vRules.get(i);
if (un.getRule()==r) {
/* Update for rule rule r */
String name=(String)rg.updatenames.get(un);
- cr.outputline(rg.strepairtable+"->addset("+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
+ cr.outputline("RepairHashaddset("+rg.strepairtable+","+sd.getNum()+","+r.getNum()+","+leftvar.getSafeSymbol()+",(int) &"+name+");");
}
}
}
boolean usageimage=rd.testUsage(RelationDescriptor.IMAGE);
boolean usageinvimage=rd.testUsage(RelationDescriptor.INVIMAGE);
if (usageimage)
- cr.outputline(rg.stmodel+"->"+rd.getJustSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
+ cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + rightvar.getSafeSymbol() + ");");
if (usageinvimage)
- cr.outputline(rg.stmodel+"->"+rd.getJustSafeSymbol() + "_hashinv->add((int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
+ cr.outputline("SimpleHashadd("+rg.stmodel+"->"+rd.getJustSafeSymbol()+"_hashinv, (int)" + rightvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
UpdateNode un=mun.getUpdate(0);
String name=(String)rg.updatenames.get(un);
cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
} else {
SetDescriptor sd=(SetDescriptor)d;
- cr.outputline(rg.stmodel+"->"+sd.getJustSafeSymbol() + "_hash->add((int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
+ cr.outputline("SimpleHashadd("+rg.stmodel+"->"+sd.getJustSafeSymbol()+"_hash, (int)" + leftvar.getSafeSymbol() + ", (int)" + leftvar.getSafeSymbol() + ");");
UpdateNode un=mun.getUpdate(0);
/* Update for rule rule r */
cr.outputline(name+"(this,"+rg.stmodel+","+rg.strepairtable+","+leftvar.getSafeSymbol()+");");
}
}
-
}
public void generate(CodeWriter cr, boolean removal, boolean modify, String slot0, String slot1, String slot2, RepairGenerator rg) {
u.getRightExpr().generate(cr,right);
break;
case Updates.POSITION:
- if (u.getRightPos()==0)
- cr.outputline("int "+right.getSafeSymbol()+"="+slot0+";");
- else if (u.getRightPos()==1)
- cr.outputline("int "+right.getSafeSymbol()+"="+slot1+";");
- else if (u.getRightPos()==2)
- cr.outputline("int "+right.getSafeSymbol()+"="+slot2+";");
- else throw new Error("Error w/ Position");
+ case Updates.ACCESSPATH:
+ if (u.getRightPos()==0) {
+ cr.addDeclaration("int", right.getSafeSymbol());
+ cr.outputline(right.getSafeSymbol()+"="+slot0+";");
+ } else if (u.getRightPos()==1) {
+ cr.addDeclaration("int", right.getSafeSymbol());
+ cr.outputline(right.getSafeSymbol()+"="+slot1+";");
+ } else if (u.getRightPos()==2) {
+ cr.addDeclaration("int", right.getSafeSymbol());
+ cr.outputline(right.getSafeSymbol()+"="+slot2+";");
+ } else throw new Error("Error w/ Position");
break;
default:
throw new Error();
}
+
+ if (u.getType()==Updates.ACCESSPATH) {
+ VarDescriptor newright=VarDescriptor.makeNew("right");
+ generate_accesspath(cr, right,newright,u);
+ right=newright;
+ }
VarDescriptor left=VarDescriptor.makeNew("left");
u.getLeftExpr().generate(cr,left);
Opcode op=u.getOpcode();
intindex.generate(cr,indexvd);
FieldDescriptor fd=(FieldDescriptor)u.getDescriptor();
StructureTypeDescriptor std=(StructureTypeDescriptor)subexpr.getType();
+ Expr offsetbits = std.getOffsetExpr(fd);
if (fd instanceof ArrayDescriptor) {
fd = ((ArrayDescriptor) fd).getField();
}
- Expr offsetbits = std.getOffsetExpr(fd);
if (intindex != null) {
Expr basesize = fd.getBaseSizeExpr();
offsetbits = new OpExpr(Opcode.ADD, offsetbits, new OpExpr(Opcode.MULT, basesize, intindex));
} else if (rtd==ReservedTypeDescriptor.BIT) {
Expr tmp = new OpExpr(Opcode.SHL, offsetbytes, new IntegerLiteralExpr(3));
Expr offset=new OpExpr(Opcode.SUB, offsetbits, tmp);
- Expr mask=new OpExpr(Opcode.SHR, new IntegerLiteralExpr(1), offset);
+ Expr mask=new OpExpr(Opcode.SHL, new IntegerLiteralExpr(1), offset);
VarDescriptor maskvar=VarDescriptor.makeNew("mask");
mask.generate(cr,maskvar);
cr.outputline("*((char *) "+addr.getSafeSymbol()+")|="+maskvar.getSafeSymbol()+";");
}
}
+
+ private void generate_accesspath(CodeWriter cr, VarDescriptor right, VarDescriptor newright, Updates u) {
+ Vector dotvector=new Vector();
+ Expr ptr=u.getRightExpr();
+ VarExpr rightve=new VarExpr(right);
+ right.td=ReservedTypeDescriptor.INT;
+
+ while(true) {
+ /* Does something other than a dereference? */
+ dotvector.add(ptr);
+ if (ptr instanceof DotExpr)
+ ptr=((DotExpr)ptr).left;
+ else if (ptr instanceof CastExpr)
+ ptr=((CastExpr)ptr).getExpr();
+ if (ptr instanceof VarExpr) {
+ /* Finished constructing vector */
+ break;
+ }
+ }
+ ArrayAnalysis.AccessPath ap=u.getAccessPath();
+ VarDescriptor init=VarDescriptor.makeNew("init");
+ if (ap.isSet()) {
+ cr.addDeclaration("int", init.getSafeSymbol());
+ cr.outputline(init.getSafeSymbol()+"= SimpleHashfirstkey("+ap.getSet().getSafeSymbol()+"_hash);");
+ init.td=ap.getSet().getType();
+ } else {
+ init=ap.getVar();
+ }
+ Expr newexpr=new VarExpr(init);
+ int apindex=0;
+ for(int i=dotvector.size()-1;i>=0;i--) {
+ Expr e=(Expr)dotvector.get(i);
+ if (e instanceof CastExpr) {
+ newexpr.td=e.td;
+ newexpr=new CastExpr(((CastExpr)e).getType(),newexpr);
+ } else if (e instanceof DotExpr) {
+ DotExpr de=(DotExpr)e;
+ if (de.getField() instanceof ArrayDescriptor) {
+ DotExpr de2=new DotExpr(newexpr,de.field,new IntegerLiteralExpr(0));
+ de2.fd=de.fd;
+ de2.fieldtype=de.fieldtype;
+ de2.td=de.td;
+ OpExpr offset=new OpExpr(Opcode.SUB,rightve,de2);
+ OpExpr index=new OpExpr(Opcode.DIV,offset,de.fieldtype.getSizeExpr());
+ if (u.getRightPos()==apindex) {
+ index.generate(cr,newright);
+ return;
+ } else {
+ DotExpr de3=new DotExpr(newexpr,de.field,index);
+ de3.fd=de.fd;
+ de3.td=de.td;
+ de3.fieldtype=de.fieldtype;
+ newexpr=de3;
+ }
+ } else {
+ DotExpr de2=new DotExpr(newexpr,de.field,null);
+ de2.fd=de.fd;
+ de2.fieldtype=de.fieldtype;
+ de2.td=de.td;
+ newexpr=de2;
+ }
+ apindex++;
+ } else throw new Error();
+ }
+ throw new Error();
+ }
+
private void generate_bindings(CodeWriter cr, String slot0, String slot1) {
for(int i=0;i<bindings.size();i++) {
Binding b=(Binding)bindings.get(i);
if (b.getType()==Binding.SEARCH) {
VarDescriptor vd=b.getVar();
- cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+b.getSet().getSafeSymbol()+"->firstkey();");
+ cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
+ cr.outputline(vd.getSafeSymbol()+"=SimpleHashfirstkey("+b.getSet().getSafeSymbol()+"_hash);");
} else if (b.getType()==Binding.CREATE) {
throw new Error("Creation not supported");
// source.generateSourceAlloc(cr,vd,b.getSet());
VarDescriptor vd=b.getVar();
switch(b.getPosition()) {
case 0:
- cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+slot0+";");
+ cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
+ cr.outputline(vd.getSafeSymbol()+"="+slot0+";");
break;
case 1:
- cr.outputline(vd.getType().getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"="+slot1+";");
+ cr.addDeclaration(vd.getType().getGenerateType().getSafeSymbol(), vd.getSafeSymbol());
+ cr.outputline(vd.getSafeSymbol()+"="+slot1+";");
break;
default:
throw new Error("Slot >1 doesn't exist.");