Improve precision of interference analysis. Allow sizeof(v.r1.r2) expressions.
authorbdemsky <bdemsky>
Sun, 15 Aug 2004 05:14:18 +0000 (05:14 +0000)
committerbdemsky <bdemsky>
Sun, 15 Aug 2004 05:14:18 +0000 (05:14 +0000)
Repair/RepairCompiler/MCC/IR/AbstractInterferes.java
Repair/RepairCompiler/MCC/IR/ImageSetExpr.java
Repair/RepairCompiler/MCC/IR/OpExpr.java
Repair/RepairCompiler/MCC/IR/RelationExpr.java
Repair/RepairCompiler/MCC/IR/RepairGenerator.java
Repair/RepairCompiler/MCC/IR/SemanticChecker.java
Repair/RepairCompiler/MCC/IR/Sources.java
Repair/RepairCompiler/MCC/IR/Termination.java

index 3e534324ee6a97d6fd0cbbfeed523e50769cd45e..31db16c97707ce6bb2879d8916d7ae2d4d546e06 100755 (executable)
@@ -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)&&(size1<size2)))
+               return false;
+       }
+
        if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
            (ar.getType()==AbstractRepair.ADDTOSET||ar.getType()==AbstractRepair.ADDTORELATION)&&
            (dp.getPredicate() instanceof ExprPredicate)&&
@@ -235,6 +301,8 @@ class AbstractInterferes {
                (op2==Opcode.GT))
                return false;
        }
+
+
        if (ar.getDescriptor()==dp.getPredicate().getDescriptor()&&
            (ar.getType()==AbstractRepair.MODIFYRELATION)&&
            (dp.getPredicate() instanceof ExprPredicate)&&
@@ -374,6 +442,33 @@ class AbstractInterferes {
            }
        }
 
+       /* 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)&&
index ead3fce5811d91865a96b3b326b5154da08a4bd7..e1aec13de9a07744e9eed9c78827e8f8ab682dd7 100755 (executable)
@@ -123,19 +123,74 @@ public class ImageSetExpr extends SetExpr {
 
     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("~");
@@ -146,5 +201,4 @@ public class ImageSetExpr extends SetExpr {
     public TypeDescriptor typecheck(SemanticAnalyzer sa) {
         throw new IRException("not supported");
     }
-
 }
index dfa0c1433dda72f5bff7d60a1a17d466c86609bf..4c0971cdd452a141a5cf057acd858e55c4c5fe44 100755 (executable)
@@ -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() + ";");
         }
index e5ebf677eecd812700d09aa34afef4e3d8ee8967..1f2bb48991788278c474d48ecafda4c81144d997 100755 (executable)
@@ -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);
index f1ff4d3e28963c6021edf4a041fe989d22f8c871..a6586bc6de6cf77ca44bd9d6f62ffea7730e85c8 100755 (executable)
@@ -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 */
index 66e5744647644a30f1148455c3c0e5f13c38206e..23e83f4b785377173e563a645e09735e3da66ac4 100755 (executable)
@@ -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();
         }
index 73af6898033014c7e4459edcfb1d90e88793d178..fd8205fbcc81f5c06fa697e257000194aec304f1 100755 (executable)
@@ -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;");
                    }
                }
            }
index d0197b5d8b000337659ead3f847cdd95b978cef4..09e1abe62bf8e99506fea8aabb7101a01d0a5d28 100755 (executable)
@@ -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;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);
@@ -1336,4 +1361,29 @@ public class Termination {
        }
        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;
+    }
 }