//)
return false;
+
+ // If the update changes something in the middle of a size
+ // expression, it interferes with it.
+ if ((dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)&&
+ (((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr instanceof ImageSetExpr)&&
+ ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).isimageset&&
+ ((ImageSetExpr)((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr).ise.usesDescriptor(ar.getDescriptor())) {
+ return true;
+ }
+
+ // If the update changes something in the middle of a
+ // comparison expression, it interferes with it.
+ if ((dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)&&
+ (((RelationExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).getExpr().usesDescriptor(ar.getDescriptor()))) {
+ return true;
+ }
+
/* This if handles all the c comparisons in the paper */
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
return false;
}
}
+
+ /* This if handles all the c comparisons in the paper */
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
+ (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
+ boolean neg1=ar.getPredicate().isNegated();
+ Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
+ int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
+ int size2=1;
+ op1=Opcode.translateOpcode(neg1,op1);
+
+ if ((op1==Opcode.EQ)||(op1==Opcode.NE)||(op1==Opcode.GT)||op1==Opcode.GE) {
+ int size1a=0;
+ if((op1==Opcode.EQ)||(op1==Opcode.GE))
+ size1a=size1;
+ if((op1==Opcode.GT)||(op1==Opcode.NE))
+ size1a=size1+1;
+ if (size1a==size2)
+ return false;
+ }
+ }
+
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.MODIFYRELATION)&&
+ (dp.getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+ int size1=1;
+
+ boolean neg2=dp.isNegated();
+ Opcode op2=((ExprPredicate)dp.getPredicate()).getOp();
+ int size2=((ExprPredicate)dp.getPredicate()).rightSize();
+
+ op2=Opcode.translateOpcode(neg2,op2);
+
+ if (((op2==Opcode.EQ)&&(size1==size2))||
+ ((op2==Opcode.NE)&&(size1!=size2))||
+ ((op2==Opcode.GE)&&(size1>=size2))||
+ ((op2==Opcode.GT)&&(size1>size2))||
+ ((op2==Opcode.LE)&&(size1<=size2))||
+ ((op2==Opcode.LT)&&(size1<size2)))
+ return false;
+ }
+
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
(dp.getPredicate() instanceof ExprPredicate)&&
(op2==Opcode.GT))
return false;
}
+
+
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.MODIFYRELATION)&&
(dp.getPredicate() instanceof ExprPredicate)&&
}
}
+ /* This handles all the c comparisons in the paper */
+ if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
+ (ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
+ (ar.getPredicate().getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate() instanceof ExprPredicate)&&
+ (dp.getPredicate().inverted()==ar.getPredicate().getPredicate().inverted())&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
+ boolean neg1=ar.getPredicate().isNegated();
+ Opcode op1=((ExprPredicate)ar.getPredicate().getPredicate()).getOp();
+ int size1=((ExprPredicate)ar.getPredicate().getPredicate()).rightSize();
+ int size2=1;
+ /* Translate the opcodes */
+ op1=Opcode.translateOpcode(neg1,op1);
+
+ if (((op1==Opcode.EQ)||(op1==Opcode.LT)||op1==Opcode.LE)||(op1==Opcode.NE)) {
+ int size1a=0;
+
+ if((op1==Opcode.EQ)||(op1==Opcode.LE))
+ size1a=size1;
+ if((op1==Opcode.LT)||(op1==Opcode.NE))
+ size1a=size1-1;
+
+ if (size1a==size2)
+ return false;
+ }
+ }
+
if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
(ar.getType()==AbstractRepair.REMOVEFROMSET||ar.getType()==AbstractRepair.REMOVEFROMRELATION)&&
(dp.getPredicate() instanceof ExprPredicate)&&
public void generate_inclusion(CodeWriter writer, VarDescriptor dest, VarDescriptor element) {
String hash = inverse ? "_hashinv->contains(" : "_hash->contains(" ;
- writer.outputline("int " + dest.getSafeSymbol() + " = " + rd.getSafeSymbol() + hash + vd.getSafeSymbol() + ", " + element.getSafeSymbol() + ");");
+ if (!isimageset) {
+ writer.outputline("int " + dest.getSafeSymbol() + " = " + rd.getSafeSymbol() + hash + vd.getSafeSymbol() + ", " + element.getSafeSymbol() + ");");
+ } else {
+ VarDescriptor newset=VarDescriptor.makeNew("newset");
+ generate_set(writer,newset);
+ writer.outputline("int "+dest.getSafeSymbol()+"="+newset.getSafeSymbol()+"->contains("+element.getSafeSymbol()+");");
+ writer.outputline("delete "+newset.getSafeSymbol()+";");
+ }
}
public void generate_size(CodeWriter writer, VarDescriptor dest) {
assert dest != null;
- assert vd != null;
assert rd != null;
- String hash = inverse ? "_hashinv->count(" : "_hash->count(" ;
- writer.outputline("int " + dest.getSafeSymbol() + " = " + rd.getSafeSymbol() + hash + vd.getSafeSymbol() + ");");
+ if (!isimageset) {
+ String hash = inverse ? "_hashinv->count(" : "_hash->count(" ;
+ writer.outputline("int " + dest.getSafeSymbol() + " = " + rd.getSafeSymbol() + hash + vd.getSafeSymbol() + ");");
+ } else {
+ VarDescriptor newset=VarDescriptor.makeNew("newset");
+ generate_set(writer,newset);
+ writer.outputline("int "+dest.getSafeSymbol()+"="+newset.getSafeSymbol()+"->count();");
+ writer.outputline("delete "+newset.getSafeSymbol()+";");
+ }
+ }
+
+ public void generate_leftside(CodeWriter writer, VarDescriptor dest) {
+ if (!isimageset) {
+ writer.outputline(vd.getType().getGenerateType()+" "+dest.getSafeSymbol()+" = "+vd.getSafeSymbol()+";");
+ } else {
+ VarDescriptor iseset=VarDescriptor.makeNew("set");
+ ise.generate_set(writer,iseset);
+ writer.outputline("int "+dest.getSafeSymbol()+" = "+iseset.getSafeSymbol()+"->firstkey();");
+ writer.outputline("delete "+iseset.getSafeSymbol()+";");
+ }
+ }
+
+ public void generate_set(CodeWriter writer, VarDescriptor dest) {
+ if (!isimageset) {
+ String hash = inverse ? "_hashinv->imageSet(" : "_hash->imageSet(" ;
+ writer.outputline("SimpleHash * "+dest.getSafeSymbol()+"="+rd.getSafeSymbol()+hash+vd.getSafeSymbol()+");");
+ } else {
+ VarDescriptor iseset=VarDescriptor.makeNew("set");
+ ise.generate_set(writer,iseset);
+
+ VarDescriptor itvd=VarDescriptor.makeNew("iterator");
+ writer.outputline("SimpleIterator "+itvd.getSafeSymbol()+";");
+ writer.outputline(iseset.getSafeSymbol()+"->iterator("+itvd.getSafeSymbol()+");");
+
+ writer.outputline("SimpleHash *"+dest.getSafeSymbol()+"=new SimpleHash(10);");
+ writer.outputline("while ("+itvd.getSafeSymbol()+".hasNext()) {");
+
+ VarDescriptor keyvd=VarDescriptor.makeNew("key");
+
+ writer.outputline("int "+keyvd.getSafeSymbol()+"="+itvd.getSafeSymbol()+".next();");
+ String hash = inverse ? "_hashinv->imageSet(" : "_hash->imageSet(" ;
+ VarDescriptor newset=VarDescriptor.makeNew("newset");
+ writer.outputline("SimpleHash * "+newset.getSafeSymbol()+"="+rd.getSafeSymbol()+hash+keyvd.getSafeSymbol()+");");
+ writer.outputline(dest.getSafeSymbol()+"->addAll("+newset.getSafeSymbol()+");");
+ writer.outputline("delete "+newset.getSafeSymbol()+";");
+ writer.outputline("}");
+ writer.outputline("delete "+iseset.getSafeSymbol()+";");
+ }
}
public void prettyPrint(PrettyPrinter pp) {
- pp.output(vd.toString());
+ if (!isimageset)
+ pp.output(vd.toString());
+ else
+ ise.prettyPrint(pp);
pp.output(".");
if (inverse) {
pp.output("~");
public TypeDescriptor typecheck(SemanticAnalyzer sa) {
throw new IRException("not supported");
}
-
}
public void generate(CodeWriter writer, VarDescriptor dest) {
VarDescriptor ld = VarDescriptor.makeNew("leftop");
+ /* Check for loop invariant hoisting. */
if (writer.getInvariantValue()!=null&&
writer.getInvariantValue().isInvariant(this)) {
writer.outputline("maybe="+writer.getInvariantValue().getMaybe(this).getSafeSymbol()+";");
return;
}
- left.generate(writer, ld);
+ left.generate(writer, ld);
VarDescriptor rd = null;
VarDescriptor lm=VarDescriptor.makeNew("lm");
VarDescriptor rm=VarDescriptor.makeNew("rm");
writer.outputline("int "+dest.getSafeSymbol() + " = " + ld.getSafeSymbol() + " || " + rd.getSafeSymbol() + ";");
} else if (opcode != Opcode.NOT) { /* two operands */
assert rd != null;
- writer.outputline("int " + dest.getSafeSymbol() + " = " +
- ld.getSafeSymbol() + " " + opcode.toString() + " " + rd.getSafeSymbol() + ";");
+ writer.outputline("int " + dest.getSafeSymbol() + " = " +
+ ld.getSafeSymbol() + " " + opcode.toString() + " " + rd.getSafeSymbol() + ";");
} else if (opcode == Opcode.NOT) {
writer.outputline("int " + dest.getSafeSymbol() + " = !" + ld.getSafeSymbol() + ";");
}
String found = (VarDescriptor.makeNew("found")).getSafeSymbol();
expr.generate(writer, domain);
writer.outputline(relation.getRange().getType().getGenerateType().getSafeSymbol() + " " + dest.getSafeSymbol() + ";");
- writer.outputline("int " + found + " = " + relation.getSafeSymbol() + "_hash" + strinverse + "->get(" + domain.getSafeSymbol() + ", " + dest.getSafeSymbol() + ");");
- writer.outputline("if (!" + found + ") { maybe = 1; }");
- }
-
- // #TBD#: don't think this method is needed (or even called/referenced)
- /*
- public void generate_set(CodeWriter writer, VarDescriptor dest) {
- VarDescriptor domain = VarDescriptor.makeNew("domain");
- expr.generate(writer, domain);
- writer.outputline(relation.getRange().getType().getGenerateType().getSafeSymbol() + " " + dest.getSafeSymbol() + " = " + relation.getSafeSymbol() + "_hash->get(" + domain.getSafeSymbol() + ");");
- }
- */
+ writer.outputline("int "+found+" = "+relation.getSafeSymbol() + "_hash" + strinverse + "->get(" + domain.getSafeSymbol() + ", " + dest.getSafeSymbol() + ");");
+ writer.outputline("if (!" + found + ") { maybe = 1; }");
+ }
public void prettyPrint(PrettyPrinter pp) {
expr.prettyPrint(pp);
VarDescriptor rightvar=VarDescriptor.makeNew("rightvar");
if (d instanceof RelationDescriptor) {
if (ep.inverted()) {
- rightvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
+ ((ImageSetExpr)((SizeofExpr)expr.left).setexpr).generate_leftside(cr,rightvar);
cr.outputline("int "+leftvar.getSafeSymbol()+";");
cr.outputline(d.getSafeSymbol()+"_hashinv->get((int)"+rightvar.getSafeSymbol()+","+leftvar.getSafeSymbol()+");");
} else {
- leftvar=((ImageSetExpr)((SizeofExpr)((OpExpr)expr).left).setexpr).getVar();
+ ((ImageSetExpr)((SizeofExpr)expr.left).setexpr).generate_leftside(cr,leftvar);
cr.outputline("int "+rightvar.getSafeSymbol()+"=0;");
cr.outputline(d.getSafeSymbol()+"_hash->get((int)"+leftvar.getSafeSymbol()+","+rightvar.getSafeSymbol()+");");
}
}
cr.endblock();
}
+
+// In some cases the analysis has determined that generating removes
+// is unnecessary
+ if (generateadd&&munadd==null)
+ generateadd=false;
+
if (generateadd) {
cr.outputline("for(;"+change.getSafeSymbol()+">0;"+change.getSafeSymbol()+"--)");
cr.startblock();
VarDescriptor newobject=VarDescriptor.makeNew("newobject");
if (d instanceof RelationDescriptor) {
- VarDescriptor otherside=((ImageSetExpr)((SizeofExpr)((OpExpr)ep.expr).left).setexpr).vd;
+ VarDescriptor otherside=VarDescriptor.makeNew("otherside");
+ ((ImageSetExpr)((SizeofExpr)expr.left).setexpr).generate_leftside(cr,otherside);
+
RelationDescriptor rd=(RelationDescriptor)d;
if (termination.sources.relsetSource(rd,!ep.inverted())) {
/* Set Source */
RelationDescriptor relation = lookupRelation(pn.getChild("dotinv").getChild("relation").getTerminal());
relation.addUsage(RelationDescriptor.INVIMAGE);
return new ImageSetExpr(ImageSetExpr.INVERSE, vd, relation);
+ } else if (pn.getChild("dotset") != null) {
+ ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotset").getChild("setexpr"));
+ RelationDescriptor relation = lookupRelation(pn.getChild("dotset").getChild("relation").getTerminal());
+ relation.addUsage(RelationDescriptor.IMAGE);
+ return new ImageSetExpr(ise, relation);
+ } else if (pn.getChild("dotinvset") != null) {
+ ImageSetExpr ise = (ImageSetExpr) parse_setexpr(pn.getChild("dotinvset").getChild("setexpr"));
+ RelationDescriptor relation = lookupRelation(pn.getChild("dotinvset").getChild("relation").getTerminal());
+ relation.addUsage(RelationDescriptor.INVIMAGE);
+ return new ImageSetExpr(ImageSetExpr.INVERSE, ise, relation);
} else {
throw new IRException();
}
String vtable="_ZTV";
vtable+=td.getSymbol().length();
vtable+=td.getSymbol();
- cr.outputline("((int**) &"+vd.getSafeSymbol()+")[0] = (int *)"+vtable+"+2;");
+ cr.outputline("((int**) "+vd.getSafeSymbol()+")[0] = (int *) & "+vtable+"+2;");
}
}
}
GraphNode gn=(GraphNode)conjiterator.next();
TermNode tn=(TermNode)gn.getOwner();
Conjunction conj=tn.getConjunction();
+ loop:
for(int i=0;i<conj.size();i++) {
DNFPredicate dp=conj.get(i);
int[] array=dp.getPredicate().getRepairs(dp.isNegated(),this);
Descriptor d=dp.getPredicate().getDescriptor();
+ if ((dp.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+ boolean neg=dp.isNegated();
+ Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
+ int size=((ExprPredicate)dp.getPredicate()).rightSize();
+ op=Opcode.translateOpcode(neg,op);
+ if (((size==1)&&(op==Opcode.EQ))||
+ ((size!=1)&&(op==Opcode.NE))||
+ ((size<=1)&&(op==Opcode.GE))||
+ ((size<1)&&(op==Opcode.GT))||
+ ((size>1)&&(op==Opcode.LT))||
+ ((size>=1)&&(op==Opcode.LE))) {
+ for(int i2=0;i2<conj.size();i2++) {
+ DNFPredicate dp2=conj.get(i2);
+ if ((dp2.getPredicate() instanceof ExprPredicate)&&
+ (((ExprPredicate)dp2.getPredicate()).getType()==ExprPredicate.COMPARISON)) {
+ if (equivalent(((SizeofExpr)((OpExpr)((ExprPredicate)dp.getPredicate()).expr).left).setexpr,
+ (RelationExpr)((OpExpr)((ExprPredicate)dp2.getPredicate()).expr).left))
+ continue loop; // comparison predicate ensure that size expr is true - no need to generate abstract repairs...
+ }
+ }
+ }
+ }
+
for(int j=0;j<array.length;j++) {
AbstractRepair ar=new AbstractRepair(dp,array[j],d,sources);
TermNode tn2=new TermNode(ar);
}
return true;
}
+
+ boolean equivalent(SetExpr se, RelationExpr re) {
+ if (!(se instanceof ImageSetExpr))
+ return false;
+ ImageSetExpr ise=(ImageSetExpr)se;
+ while(re!=null&&ise!=null) {
+ if (re.getRelation()!=ise.getRelation())
+ return false;
+ if (re.inverted()!=ise.inverted())
+ return false;
+ if (ise.isimageset) {
+ ise=ise.getImageSetExpr();
+ if (!(re.getExpr() instanceof RelationExpr))
+ return false;
+ re=(RelationExpr)re.getExpr();
+ } else {
+ if (!(re.getExpr() instanceof VarExpr))
+ return false;
+ if (((VarExpr)re.getExpr()).getVar()==ise.getVar())
+ return true; //everything matches
+ return false;
+ }
+ }
+ return false;
+ }
}