Added minimum size analysis.

Improved safe check in DotExpr.
Changed naming scheme in dumpstructures.
Fixed bug in must/cant node analysis

diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
index d6dc251382ff1a89bb786aab0759d52beb656d44..3deab4939293bcef58fdc030b007d028a7c5cdfe 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
+++ b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
@@ -19,7 +19,7 @@ public class ConstraintDependence {
        nodetonode=new Hashtable();
        constructnodes();
     }
        nodetonode=new Hashtable();
        constructnodes();
     }

-    
+

     public Set computeOrdering() {
        HashSet allnodes=new HashSet();
        allnodes.addAll(constnodes);
     public Set computeOrdering() {
        HashSet allnodes=new HashSet();
        allnodes.addAll(constnodes);


@@ -36,7 +36,7 @@ public class ConstraintDependence {
                     return g1.getFinishingTime() - g2.getFinishingTime();
                 }
             });
                     return g1.getFinishingTime() - g2.getFinishingTime();
                 }
             });

-       
+

         topologicalsort.addAll(constnodes);
        return topologicalsort;
     }
         topologicalsort.addAll(constnodes);
        return topologicalsort;
     }


@@ -110,7 +110,7 @@ public class ConstraintDependence {
            constnodes.add(gn);
        }
     }
            constnodes.add(gn);
        }
     }

-    
+

     private void constructconjunctionnodes(Termination termination) {
        /*for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
          GraphNode conjnode=(GraphNode)it.next();
     private void constructconjunctionnodes(Termination termination) {
        /*for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
          GraphNode conjnode=(GraphNode)it.next();


@@ -137,7 +137,7 @@ public class ConstraintDependence {
            GraphNode conjnode=(GraphNode)it.next();
            if (removedset.contains(conjnode))
                continue;
            GraphNode conjnode=(GraphNode)it.next();
            if (removedset.contains(conjnode))
                continue;

-           
+

            TermNode tn=(TermNode)conjnode.getOwner();
            Conjunction conj=tn.getConjunction();
            for(int i=0;i<conj.size();i++) {
            TermNode tn=(TermNode)conjnode.getOwner();
            Conjunction conj=tn.getConjunction();
            for(int i=0;i<conj.size();i++) {


@@ -215,7 +215,7 @@ public class ConstraintDependence {
        }
        return foundrule;
     }
        }
        return foundrule;
     }

- 
+

     static private Set providesfunction(State state, Function f) {
        return providesfunction(state,f,false);
     }
     static private Set providesfunction(State state, Function f) {
        return providesfunction(state,f,false);
     }

diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index be8d32489fbae24cd327c32c5192b6f99005c2fa..2e5021e940909a488fec446aa81790f79f63f319 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/DotExpr.java
+++ b/Repair/RepairCompiler/MCC/IR/DotExpr.java
@@ -57,12 +57,23 @@ public class DotExpr extends Expr {
     public boolean isSafe() {
        if (!left.isSafe())
            return false;
     public boolean isSafe() {
        if (!left.isSafe())
            return false;

+

        FieldDescriptor tmpfd=fd;
        FieldDescriptor tmpfd=fd;

-       if (tmpfd instanceof ArrayDescriptor)
-           return false; // Arrays could be out of bounds
+

        if (tmpfd.getPtr()) // Pointers cound be invalid
            return false;
        if (tmpfd.getPtr()) // Pointers cound be invalid
            return false;

-       return true;
+
+       if (tmpfd instanceof ArrayDescriptor) {
+            Expr arrayindex=((ArrayDescriptor)tmpfd).getIndexBound();
+            if (index instanceof IntegerLiteralExpr&&arrayindex instanceof IntegerLiteralExpr) {
+                int indexvalue=((IntegerLiteralExpr)index).getValue();
+                int arrayindexvalue=((IntegerLiteralExpr)arrayindex).getValue();
+                if (indexvalue>=0&&indexvalue<arrayindexvalue)
+                    return true;
+            }
+           return false; // Otherwise, arrays could be out of bounds
+        }
+        return true;

     }
 
     public Set freeVars() {
     }
 
     public Set freeVars() {

diff --git a/Repair/RepairCompiler/MCC/IR/ExactSize.java b/Repair/RepairCompiler/MCC/IR/ExactSize.java
index 1b665fce32aace3d8826702d310135c162c5cb3e..c1a1c6f9c1516ae275ef0b93589f845f8ce60e86 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/ExactSize.java
+++ b/Repair/RepairCompiler/MCC/IR/ExactSize.java
@@ -8,15 +8,32 @@ class ExactSize {
     private Hashtable sizemap;
     private Hashtable constraintmap;
     private SetAnalysis setanalysis;
     private Hashtable sizemap;
     private Hashtable constraintmap;
     private SetAnalysis setanalysis;

+    private Hashtable minsize;
+    private Hashtable constraintensureminsize;

 
     public ExactSize(State state) {
        this.state=state;
        this.sizemap=new Hashtable();
 
     public ExactSize(State state) {
        this.state=state;
        this.sizemap=new Hashtable();

+        this.minsize=new Hashtable();
+        this.constraintensureminsize=new Hashtable();

        this.constraintmap=new Hashtable();
        this.setanalysis=state.setanalysis;
        computesizes();
     }
        this.constraintmap=new Hashtable();
        this.setanalysis=state.setanalysis;
        computesizes();
     }

-    
+
+    public int minSize(SetDescriptor sd) {
+       SizeObject so=new SizeObject(sd);
+       if (minsize.containsKey(so))
+           return ((Integer)minsize.get(so)).intValue();
+       else
+           return 0;
+    }
+
+    public Constraint ensuresMinSize(SetDescriptor sd) {
+        SizeObject so=new SizeObject(sd);
+       return (Constraint)constraintensureminsize.get(so);
+    }
+

     public int getsize(SetDescriptor sd) {
        SizeObject so=new SizeObject(sd);
        if (sizemap.containsKey(so))
     public int getsize(SetDescriptor sd) {
        SizeObject so=new SizeObject(sd);
        if (sizemap.containsKey(so))


@@ -55,6 +72,56 @@ class ExactSize {
        return null;
     }
 
        return null;
     }
 

+    private void constructminsizes() {
+        boolean change=true;
+        HashSet usedsources=new HashSet();
+        while (change) {
+            change=false;
+            for(int i=0;i<state.vRules.size();i++) {
+                Rule r=(Rule)state.vRules.get(i);
+                //model defition rule with no condition
+                if ((!(r.getGuardExpr() instanceof BooleanLiteralExpr))||
+                    (!((BooleanLiteralExpr)r.getGuardExpr()).getValue()))
+                    continue;
+                //inclusion condition needs to be safe
+                if ((!(r.getInclusion() instanceof SetInclusion))||
+                    (!((SetInclusion)r.getInclusion()).getExpr().isSafe()))
+                    continue;
+                //needs exactly 1 quantifier which is a set quantifier
+                if (r.numQuantifiers()!=1||
+                    (!(r.getQuantifier(0) instanceof SetQuantifier)))
+                    continue;
+                SetQuantifier sq=(SetQuantifier)r.getQuantifier(0);
+                SetDescriptor sd=sq.getSet();
+                int size=-1;
+                Constraint source=null;
+                if (getsize(sd)>0) {
+                    size=getsize(sd);
+                    source=getConstraint(sd);
+                } else if (minSize(sd)>0) {
+                    size=minSize(sd);
+                    source=ensuresMinSize(sd);
+                } else continue;
+                if (size>1)
+                    size=1; //would need more in depth analysis otherwise
+                SetDescriptor newsd=((SetInclusion)r.getInclusion()).getSet();
+                if (usedsources.contains(newsd))
+                    continue; //avoid dependence cycles in our analysis
+                //need to force repair to fix one of the constraints in the cycle
+                int currentsize=minSize(newsd);
+                if (size>currentsize) {
+                    SizeObject so=new SizeObject(newsd);
+                    minsize.put(so, new Integer(size));
+                    constraintensureminsize.put(so,source);
+                    usedsources.add(source);
+                   System.out.println("Set "+newsd.toString()+" has minimum size "+size);
+                    change=true;
+                    //need update
+                }
+            }
+        }
+    }
+

     private void computesizes() {
        for(Iterator it=state.stSets.descriptors();it.hasNext();) {
            SetDescriptor sd=(SetDescriptor)it.next();
     private void computesizes() {
        for(Iterator it=state.stSets.descriptors();it.hasNext();) {
            SetDescriptor sd=(SetDescriptor)it.next();


@@ -88,7 +155,7 @@ class ExactSize {
                                            break;
                                        }
                                    }
                                            break;
                                        }
                                    }

-                               }                       
+                               }

                            }
                        }
                    }
                            }
                        }
                    }


@@ -143,7 +210,7 @@ class ExactSize {
                                            break;
                                        }
                                    }
                                            break;
                                        }
                                    }

-                               }                       
+                               }

                            }
                        }
                    }
                            }
                        }
                    }


@@ -160,5 +227,6 @@ class ExactSize {
                }
            }
        }
                }
            }
        }

+        constructminsizes();

     }
 }
     }
 }

diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 06ab42c72b98294110465fa24fd0f027251e54a3..6b690a859c4da45ee161c5a48367f63daf65bc20 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
+++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
@@ -66,7 +66,7 @@ public class GraphAnalysis {
                termination.updatenodes.contains(gn2))
                return false;
        }
                termination.updatenodes.contains(gn2))
                return false;
        }

-       
+

        /* Make sure all abstractrepairs/consequence nodes in the dependent nodes
           are well formed. */
     outerloop:
        /* Make sure all abstractrepairs/consequence nodes in the dependent nodes
           are well formed. */
     outerloop:


@@ -77,11 +77,11 @@ public class GraphAnalysis {
                boolean ismodify=false;
                int numadd=0;
                int numremove=0;
                boolean ismodify=false;
                int numadd=0;
                int numremove=0;

-               
+

                if (termination.abstractrepair.contains(gn2)&&
                    ((TermNode)gn2.getOwner()).getAbstract().getType()==AbstractRepair.MODIFYRELATION)
                    ismodify=true;
                if (termination.abstractrepair.contains(gn2)&&
                    ((TermNode)gn2.getOwner()).getAbstract().getType()==AbstractRepair.MODIFYRELATION)
                    ismodify=true;

-   
+

                innerloop:
                for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
                    GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();
                innerloop:
                for(Iterator edgeit=gn2.edges();edgeit.hasNext();) {
                    GraphNode gn3=((GraphNode.Edge)edgeit.next()).getTarget();


@@ -354,9 +354,10 @@ public class GraphAnalysis {
            /* Searches individual conjunctions + abstract action +updates for cycles */
            for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
                GraphNode gn=(GraphNode)it.next();
            /* Searches individual conjunctions + abstract action +updates for cycles */
            for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
                GraphNode gn=(GraphNode)it.next();

-               boolean foundnocycle=false;
-               
+

                for (Iterator edgeit=gn.edges();edgeit.hasNext();) {
                for (Iterator edgeit=gn.edges();edgeit.hasNext();) {

+                    boolean foundnocycle=false;
+

                    GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
                    GraphNode gn2=e.getTarget();
                    TermNode tn2=(TermNode)gn2.getOwner();
                    GraphNode.Edge e=(GraphNode.Edge)edgeit.next();
                    GraphNode gn2=e.getTarget();
                    TermNode tn2=(TermNode)gn2.getOwner();


@@ -365,14 +366,14 @@ public class GraphAnalysis {
                    AbstractRepair ar=tn2.getAbstract();
                    boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
                    int numadd=0;int numremove=0;
                    AbstractRepair ar=tn2.getAbstract();
                    boolean ismodify=ar.getType()==AbstractRepair.MODIFYRELATION;
                    int numadd=0;int numremove=0;

-                   
+

                    for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
                        GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
                        GraphNode gn3=e2.getTarget();
                        TermNode tn3=(TermNode)gn3.getOwner();
                        if (tn3.getType()!=TermNode.UPDATE)
                            continue;
                    for (Iterator edgeit2=gn2.edges();edgeit2.hasNext();) {
                        GraphNode.Edge e2=(GraphNode.Edge)edgeit2.next();
                        GraphNode gn3=e2.getTarget();
                        TermNode tn3=(TermNode)gn3.getOwner();
                        if (tn3.getType()!=TermNode.UPDATE)
                            continue;

-                       
+

                        boolean containsgn=cantremove.contains(gn);
                        boolean containsgn2=cantremove.contains(gn2);
                        boolean containsgn3=cantremove.contains(gn3);
                        boolean containsgn=cantremove.contains(gn);
                        boolean containsgn2=cantremove.contains(gn2);
                        boolean containsgn3=cantremove.contains(gn3);


@@ -417,14 +418,15 @@ public class GraphAnalysis {
                                mustremove.add(gn3);
                        }
                    }
                                mustremove.add(gn3);
                        }
                    }

-               }

 
 

-               if(!foundnocycle) {
-                   if (!mustremove.contains(gn)) {
-                       change=true;
-                       mustremove.add(gn);
-                   }
-               }
+
+                    if(!foundnocycle) {
+                        if (!mustremove.contains(gn)) {
+                            change=true;
+                            mustremove.add(gn);
+                        }
+                    }
+                }

            }
 
            /* Searches scope nodes + compensation nodes */
            }
 
            /* Searches scope nodes + compensation nodes */


@@ -450,7 +452,7 @@ public class GraphAnalysis {
                                change=true;
                                mustremove.add(gn2);
                            }
                                change=true;
                                mustremove.add(gn2);
                            }

-                       } 
+                       }

                        if (!containsgn)
                            cantremove.remove(gn);
                        if (!containsgn2)
                        if (!containsgn)
                            cantremove.remove(gn);
                        if (!containsgn2)

diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 046e06062ba0481f9f21aa9a4d270f8475c9dc02..0d074f6a3146bdfeeb19e50c5852878ff4198d2d 100755 (executable)
--- a/Repair/RepairCompiler/MCC/IR/Termination.java
+++ b/Repair/RepairCompiler/MCC/IR/Termination.java
@@ -464,6 +464,34 @@ public class Termination {
                }
 
                for(int j=0;j<array.length;j++) {
                }
 
                for(int j=0;j<array.length;j++) {

+                    if (array[j]==AbstractRepair.ADDTOSET) {
+
+                        System.out.println("1");
+                        if ((dp.getPredicate() instanceof ExprPredicate)&&
+                            (((ExprPredicate)dp.getPredicate()).getType()==ExprPredicate.SIZE)) {
+                            System.out.println("2");
+                            boolean neg=dp.isNegated();
+                            Opcode op=((ExprPredicate)dp.getPredicate()).getOp();
+                            int size=((ExprPredicate)dp.getPredicate()).rightSize();
+                            op=Opcode.translateOpcode(neg,op);
+                            Descriptor des=((ExprPredicate)dp.getPredicate()).getDescriptor();
+                            if (des instanceof SetDescriptor) {
+                                System.out.println("3");
+
+                                int minsize=exactsize.minSize((SetDescriptor)des);
+                                Constraint reqc=exactsize.ensuresMinSize((SetDescriptor)des);
+                                if (((size==minsize)&&(op==Opcode.EQ))||
+                                    ((size<=minsize)&&(op==Opcode.GE))||
+                                    ((size<minsize)&&(op==Opcode.GT))) {
+                                    System.out.println("4");
+                                    constraintdependence.requiresConstraint(gn,reqc);
+                                    //force good ordering
+                                    continue; //no repair action needed here...
+                                }
+                            }
+                        }
+                    }
+

                    AbstractRepair ar=new AbstractRepair(dp,array[j],d,sources);
                    TermNode tn2=new TermNode(ar);
                    //              GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);
                    AbstractRepair ar=new AbstractRepair(dp,array[j],d,sources);
                    TermNode tn2=new TermNode(ar);
                    //              GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2);

diff --git a/Repair/RepairCompiler/structextract/dumpstructures.c b/Repair/RepairCompiler/structextract/dumpstructures.c
index 01e7d5732f71d6c3799f2dea06d6c79ad7a218c9..8a95dea964b3bfc27b989b424984e415481c6a68 100755 (executable)
--- a/Repair/RepairCompiler/structextract/dumpstructures.c
+++ b/Repair/RepairCompiler/structextract/dumpstructures.c
@@ -582,14 +582,38 @@ char * printname(dwarf_entry * type,int op) {
   case DW_TAG_structure_type: {
     collection_type *ctype=(collection_type*)type->entry_ptr;
     if (op==GETTYPE&&ctype->name==NULL&&assigntype) {
   case DW_TAG_structure_type: {
     collection_type *ctype=(collection_type*)type->entry_ptr;
     if (op==GETTYPE&&ctype->name==NULL&&assigntype) {

-      ctype->name=(char*)malloc(100);
-      sprintf(ctype->name,"unnamed_0x%lx",type->ID);
+      char *newb=(char *)malloc(1000);
+      int newchars=0;
+      int i;
+      ctype->name=newb;
+      newchars=sprintf(newb,"unnamed_",type->ID);
+      newb+=newchars;
+      for(i=0;i<ctype->num_members;i++) {
+        dwarf_entry * de=ctype->members[i];
+        if (de->tag_name==DW_TAG_member) {
+          member * me=(member *)de->entry_ptr;
+          newchars=sprintf(newb,"%s",me->name);
+          newb+=newchars;
+        }
+      }

     }
     if (op==GETTYPE)
       return ctype->name;
     if (op==GETJUSTTYPE&&ctype->name==NULL&&assigntype) {
     }
     if (op==GETTYPE)
       return ctype->name;
     if (op==GETJUSTTYPE&&ctype->name==NULL&&assigntype) {

-      ctype->name=(char*)malloc(100);
-      sprintf(ctype->name,"unnamed_0x%lx",type->ID);
+      char *newb=(char *)malloc(1000);
+      int newchars=0;
+      int i;
+      ctype->name=newb;
+      newchars=sprintf(newb,"unnamed_",type->ID);
+      newb+=newchars;
+      for(i=0;i<ctype->num_members;i++) {
+        dwarf_entry * de=ctype->members[i];
+        if (de->tag_name==DW_TAG_member) {
+          member * me=(member *)de->entry_ptr;
+          newchars=sprintf(newb,"%s",me->name);
+          newb+=newchars;
+        }
+      }

     }
     if (op==GETJUSTTYPE)
       return ctype->name;
     }
     if (op==GETJUSTTYPE)
       return ctype->name;