From: bdemsky <bdemsky>
Date: Wed, 5 Oct 2005 10:14:29 +0000 (+0000)
Subject: Added minimum size analysis.
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=commitdiff_plain;h=23ac0c09ffe5d225de83ca4195ae5448434b0a71;hp=d0cc93fb75919256c617501584fdbd8cd6bfd35e

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 d6dc251..3deab49 100755
--- 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();
     }
-    
+
     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);
     }
diff --git a/Repair/RepairCompiler/MCC/IR/DotExpr.java b/Repair/RepairCompiler/MCC/IR/DotExpr.java
index be8d324..2e5021e 100755
--- 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;
+
 	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() {
diff --git a/Repair/RepairCompiler/MCC/IR/ExactSize.java b/Repair/RepairCompiler/MCC/IR/ExactSize.java
index 1b665fc..c1a1c6f 100755
--- 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 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();
     }
 }
diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java
index 06ab42c..6b690a8 100755
--- 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;
 	}
-	
+
 	/* 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)
diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java
index 046e060..0d074f6 100755
--- 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++) {
+                    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);
diff --git a/Repair/RepairCompiler/structextract/dumpstructures.c b/Repair/RepairCompiler/structextract/dumpstructures.c
index 01e7d57..8a95dea 100755
--- 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) {
-      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;