From db84f722e9e7c832a386f2bb5ea8c39816547412 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sun, 15 Aug 2004 05:14:18 +0000 Subject: [PATCH] Improve precision of interference analysis. Allow sizeof(v.r1.r2) expressions. --- .../MCC/IR/AbstractInterferes.java | 95 +++++++++++++++++++ .../RepairCompiler/MCC/IR/ImageSetExpr.java | 66 +++++++++++-- Repair/RepairCompiler/MCC/IR/OpExpr.java | 7 +- .../RepairCompiler/MCC/IR/RelationExpr.java | 15 +-- .../MCC/IR/RepairGenerator.java | 14 ++- .../MCC/IR/SemanticChecker.java | 10 ++ Repair/RepairCompiler/MCC/IR/Sources.java | 2 +- Repair/RepairCompiler/MCC/IR/Termination.java | 50 ++++++++++ 8 files changed, 234 insertions(+), 25 deletions(-) diff --git a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java index 3e53432..31db16c 100755 --- a/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java +++ b/Repair/RepairCompiler/MCC/IR/AbstractInterferes.java @@ -180,6 +180,25 @@ class AbstractInterferes { //) 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)&& @@ -212,6 +231,53 @@ class AbstractInterferes { 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)&&(size1contains(" : "_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("~"); @@ -146,5 +201,4 @@ public class ImageSetExpr extends SetExpr { public TypeDescriptor typecheck(SemanticAnalyzer sa) { throw new IRException("not supported"); } - } diff --git a/Repair/RepairCompiler/MCC/IR/OpExpr.java b/Repair/RepairCompiler/MCC/IR/OpExpr.java index dfa0c14..4c0971c 100755 --- a/Repair/RepairCompiler/MCC/IR/OpExpr.java +++ b/Repair/RepairCompiler/MCC/IR/OpExpr.java @@ -348,6 +348,7 @@ public class OpExpr extends Expr { 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()+";"); @@ -355,7 +356,7 @@ public class OpExpr extends Expr { return; } - left.generate(writer, ld); + left.generate(writer, ld); VarDescriptor rd = null; VarDescriptor lm=VarDescriptor.makeNew("lm"); VarDescriptor rm=VarDescriptor.makeNew("rm"); @@ -390,8 +391,8 @@ public class OpExpr extends Expr { 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() + ";"); } diff --git a/Repair/RepairCompiler/MCC/IR/RelationExpr.java b/Repair/RepairCompiler/MCC/IR/RelationExpr.java index e5ebf67..1f2bb48 100755 --- a/Repair/RepairCompiler/MCC/IR/RelationExpr.java +++ b/Repair/RepairCompiler/MCC/IR/RelationExpr.java @@ -107,18 +107,9 @@ public class RelationExpr extends Expr { 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); diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java index f1ff4d3..a6586bc 100755 --- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java +++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java @@ -1222,11 +1222,11 @@ public class RepairGenerator { 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()+");"); } @@ -1265,13 +1265,21 @@ public class RepairGenerator { } 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 */ diff --git a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java index 66e5744..23e83f4 100755 --- a/Repair/RepairCompiler/MCC/IR/SemanticChecker.java +++ b/Repair/RepairCompiler/MCC/IR/SemanticChecker.java @@ -1455,6 +1455,16 @@ public class SemanticChecker { 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(); } diff --git a/Repair/RepairCompiler/MCC/IR/Sources.java b/Repair/RepairCompiler/MCC/IR/Sources.java index 73af689..fd8205f 100755 --- a/Repair/RepairCompiler/MCC/IR/Sources.java +++ b/Repair/RepairCompiler/MCC/IR/Sources.java @@ -54,7 +54,7 @@ public class Sources { 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;"); } } } diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index d0197b5..09e1abe 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -386,10 +386,35 @@ public class Termination { GraphNode gn=(GraphNode)conjiterator.next(); TermNode tn=(TermNode)gn.getOwner(); Conjunction conj=tn.getConjunction(); + loop: for(int i=0;i1)&&(op==Opcode.LT))|| + ((size>=1)&&(op==Opcode.LE))) { + for(int i2=0;i2