Added minimum size analysis.
authorbdemsky <bdemsky>
Wed, 5 Oct 2005 10:14:29 +0000 (10:14 +0000)
committerbdemsky <bdemsky>
Wed, 5 Oct 2005 10:14:29 +0000 (10:14 +0000)
Improved safe check in DotExpr.
Changed naming scheme in dumpstructures.
Fixed bug in must/cant node analysis

Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
Repair/RepairCompiler/MCC/IR/DotExpr.java
Repair/RepairCompiler/MCC/IR/ExactSize.java
Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
Repair/RepairCompiler/MCC/IR/Termination.java
Repair/RepairCompiler/structextract/dumpstructures.c

index d6dc251..3deab49 100755 (executable)
@@ -19,7 +19,7 @@ public class ConstraintDependence {
        nodetonode=new Hashtable();
        constructnodes();
     }
-    
+
     public Set computeOrdering() {
        HashSet allnodes=new HashSet();
        allnodes.addAll(constnodes);
@@ -36,7 +36,7 @@ public class ConstraintDependence {
                     return g1.getFinishingTime() - g2.getFinishingTime();
                 }
             });
-       
+
         topologicalsort.addAll(constnodes);
        return topologicalsort;
     }
@@ -110,7 +110,7 @@ public class ConstraintDependence {
            constnodes.add(gn);
        }
     }
-    
+
     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;
-           
+
            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;
     }
+
     static private Set providesfunction(State state, Function f) {
        return providesfunction(state,f,false);
     }
index be8d324..2e5021e 100755 (executable)
@@ -57,12 +57,23 @@ public class DotExpr extends Expr {
     public boolean isSafe() {
        if (!left.isSafe())
            return false;
+
        FieldDescriptor tmpfd=fd;
-       if (tmpfd instanceof ArrayDescriptor)
-           return false; // Arrays could be out of bounds
+
        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() {
index 1b665fc..c1a1c6f 100755 (executable)
@@ -8,15 +8,32 @@ class ExactSize {
     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();
+        this.minsize=new Hashtable();
+        this.constraintensureminsize=new Hashtable();
        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))
@@ -55,6 +72,56 @@ class ExactSize {
        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();
@@ -88,7 +155,7 @@ class ExactSize {
                                            break;
                                        }
                                    }
-                               }                       
+                               }
                            }
                        }
                    }
@@ -143,7 +210,7 @@ class ExactSize {
                                            break;
                                        }
                                    }
-                               }                       
+                               }
                            }
                        }
                    }
@@ -160,5 +227,6 @@ class ExactSize {
                }
            }
        }
+        constructminsizes();
     }
 }
index 06ab42c..6b690a8 100755 (executable)
@@ -66,7 +66,7 @@ public class GraphAnalysis {
                termination.updatenodes.contains(gn2))
                return false;
        }
-       
+
        /* 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;
-               
+
                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();
@@ -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();
-               boolean foundnocycle=false;
-               
+
                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();
@@ -365,14 +366,14 @@ public class GraphAnalysis {
                    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;
-                       
+
                        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);
                        }
                    }
-               }
 
-               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 */
@@ -450,7 +452,7 @@ public class GraphAnalysis {
                                change=true;
                                mustremove.add(gn2);
                            }
-                       } 
+                       }
                        if (!containsgn)
                            cantremove.remove(gn);
                        if (!containsgn2)
index 046e060..0d074f6 100755 (executable)
@@ -464,6 +464,34 @@ public class Termination {
                }
 
                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);
index 01e7d57..8a95dea 100755 (executable)
@@ -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) {
-      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) {
-      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;