Improved safe check in DotExpr.
Changed naming scheme in dumpstructures.
Fixed bug in must/cant node analysis
nodetonode=new Hashtable();
constructnodes();
}
-
+
public Set computeOrdering() {
HashSet allnodes=new HashSet();
allnodes.addAll(constnodes);
return g1.getFinishingTime() - g2.getFinishingTime();
}
});
-
+
topologicalsort.addAll(constnodes);
return topologicalsort;
}
constnodes.add(gn);
}
}
-
+
private void constructconjunctionnodes(Termination termination) {
/*for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
GraphNode conjnode=(GraphNode)it.next();
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++) {
}
return foundrule;
}
-
+
static private Set providesfunction(State state, Function f) {
return providesfunction(state,f,false);
}
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() {
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))
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();
break;
}
}
- }
+ }
}
}
}
break;
}
}
- }
+ }
}
}
}
}
}
}
+ constructminsizes();
}
}
termination.updatenodes.contains(gn2))
return false;
}
-
+
/* Make sure all abstractrepairs/consequence nodes in the dependent nodes
are well formed. */
outerloop:
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();
/* 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();
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);
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 */
change=true;
mustremove.add(gn2);
}
- }
+ }
if (!containsgn)
cantremove.remove(gn);
if (!containsgn2)
}
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);
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;
projects / repair.git / commitdiff