X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FTermination.java;h=d0197b5d8b000337659ead3f847cdd95b978cef4;hp=f9ae3bb5d6c3e04a5be791b38df7dbc1997e056e;hb=f9e84f661a348d52ec5a96e246f028e3cb102fb4;hpb=0ddd66cf596f161886dc67214f3fb2e19f6f7168 diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index f9ae3bb..d0197b5 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -2,12 +2,15 @@ package MCC.IR; import java.util.*; import java.io.*; import MCC.State; +import MCC.Compiler; public class Termination { HashSet conjunctions; Hashtable conjunctionmap; HashSet abstractrepair; + HashSet abstractrepairadd; + HashSet updatenodes; HashSet consequencenodes; @@ -17,14 +20,24 @@ public class Termination { Hashtable consequence; Hashtable abstractadd; Hashtable abstractremove; - + Hashtable conjtonodemap; + Hashtable predtoabstractmap; + Set removedset; + ComputeMaxSize maxsize; State state; + AbstractInterferes abstractinterferes; + ConcreteInterferes concreteinterferes; + ConstraintDependence constraintdependence; + ExactSize exactsize; + ArrayAnalysis arrayanalysis; + Sources sources; public Termination(State state) { this.state=state; conjunctions=new HashSet(); conjunctionmap=new Hashtable(); abstractrepair=new HashSet(); + abstractrepairadd=new HashSet(); scopenodes=new HashSet(); scopesatisfy=new Hashtable(); scopefalsify=new Hashtable(); @@ -33,9 +46,27 @@ public class Termination { consequencenodes=new HashSet(); abstractadd=new Hashtable(); abstractremove=new Hashtable(); + conjtonodemap=new Hashtable(); + predtoabstractmap=new Hashtable(); + if (!Compiler.REPAIR) + return; + + + for(int i=0;i=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) { + int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size(); + if (count[i]>=num) { count[i+1]++; count[i]=0; } else break; } } - static boolean remains(int count[], Vector rules) { + + /** This method test if there remain any possibilities to loop + * through. */ + static private boolean remains(int count[], Vector rules, boolean isremove) { for(int i=0;i=(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size()))) { + int num=isremove?(((Rule)rules.get(i)).numQuantifiers()+(((Rule)rules.get(i)).getDNFNegGuardExpr().size())):((Rule)rules.get(i)).getDNFGuardExpr().size(); + if (count[i]>=num) { return false; } } return true; } + /** This method generates data structure updates to implement the + * abstract atomic modification specified by ar. */ + + int modifycount=0; void generatemodifyrelation(GraphNode gn, AbstractRepair ar) { + RelationDescriptor rd=(RelationDescriptor)ar.getDescriptor(); + ExprPredicate exprPredicate=(ExprPredicate)ar.getPredicate().getPredicate(); + boolean inverted=exprPredicate.inverted(); + int leftindex=0; + int rightindex=1; + if (inverted) + leftindex=2; + else + rightindex=2; + + // construct set of possible rules + Vector possiblerules=new Vector(); + for(int i=0;i=0;i--) { + if (e==null) + e=lexpr; + else + e=((DotExpr)e).getExpr(); + + while (e instanceof CastExpr) + e=((CastExpr)e).getExpr(); + + DotExpr de=(DotExpr)e; + FieldDescriptor fd=ap.getField(i); + if (fd instanceof ArrayDescriptor) { + // We have an ArrayDescriptor! + Expr index=de.getIndex(); + if (!index.isValue(null)) {/* Not assignable */ + System.out.println("ERROR:Index isn't assignable"); + return false; + } + Updates updates=new Updates(index,i,ap,lexpr,slotnumber); + un.addUpdate(updates); + } + } + return true; } + /** This method constructs bindings for an update using rule + * r. The boolean flag isremoval indicates that the update + * performs a removal. The function returns true if it is able to + * generate a valid set of bindings and false otherwise. */ - boolean constructbindings(Vector bindings, Rule r, boolean isremoval) { + boolean constructbindings(Vector bindings, Rule r, AbstractRepair ar, Hashtable setmapping, boolean isremoval) { boolean goodupdate=true; Inclusion inc=r.getInclusion(); + for(Iterator iterator=r.quantifiers();iterator.hasNext();) { Quantifier q=(Quantifier)iterator.next(); if ((q instanceof SetQuantifier)||(q instanceof ForQuantifier)) { @@ -437,31 +995,75 @@ public class Termination { SetDescriptor set=null; if (q instanceof SetQuantifier) { vd=((SetQuantifier)q).getVar(); - } else + set=((SetQuantifier)q).getSet(); + } else { vd=((ForQuantifier)q).getVar(); + } if(inc instanceof SetInclusion) { SetInclusion si=(SetInclusion)inc; - if ((si.elementexpr instanceof VarExpr)&& - (((VarExpr)si.elementexpr).getVar()==vd)) { + Expr tmpe=si.elementexpr; + Expr e=si.elementexpr; + + while(e instanceof CastExpr) { + CastExpr ce=(CastExpr)e; + if (ce.getType()!=si.getSet().getType()) + return false; + e=ce.getExpr(); + } + + if ((e instanceof VarExpr)&& + (((VarExpr)e).getVar()==vd)) { /* Can solve for v */ + if (!si.getSet().getType().isSubtypeOf(set.getType())) + return false; Binding binding=new Binding(vd,0); bindings.add(binding); - } else + } else { goodupdate=false; + } } else if (inc instanceof RelationInclusion) { RelationInclusion ri=(RelationInclusion)inc; boolean f1=true; boolean f2=true; - if ((ri.getLeftExpr() instanceof VarExpr)&& - (((VarExpr)ri.getLeftExpr()).getVar()==vd)) { + + Expr e=ri.getLeftExpr(); + + while(e instanceof CastExpr) { + CastExpr ce=(CastExpr)e; + if (ce.getType()!=ri.getRelation().getDomain().getType()) + return false; + e=ce.getExpr(); + } + + if ((e instanceof VarExpr)&& + (((VarExpr)e).getVar()==vd)) { /* Can solve for v */ Binding binding=new Binding(vd,0); + if (!ri.getRelation().getDomain().getType().isSubtypeOf(set.getType())) + return false; + if (ar.getDomainSet()!=null) + setmapping.put(ri.getLeftExpr(),ar.getDomainSet()); bindings.add(binding); } else f1=false; - if ((ri.getRightExpr() instanceof VarExpr)&& - (((VarExpr)ri.getRightExpr()).getVar()==vd)) { + + + e=ri.getRightExpr(); + + while(e instanceof CastExpr) { + CastExpr ce=(CastExpr)e; + if (ce.getType()!=ri.getRelation().getRange().getType()) + return false; + e=ce.getExpr(); + } + + if ((e instanceof VarExpr)&& + (((VarExpr)e).getVar()==vd)) { /* Can solve for v */ - Binding binding=new Binding(vd,0); + Binding binding=new Binding(vd,1); + if (!ri.getRelation().getRange().getType().isSubtypeOf(set.getType())) + return false; + if (ar.getRangeSet()!=null) + setmapping.put(ri.getRightExpr(),ar.getRangeSet()); bindings.add(binding); } else f2=false; if (!(f1||f2)) @@ -469,21 +1071,43 @@ public class Termination { } else throw new Error("Inclusion not recognized"); if (!goodupdate) if (isremoval) { - Binding binding=new Binding(vd); + /* Removals don't need bindings anymore + Binding binding=new Binding(vd); + bindings.add(binding);*/ + goodupdate=true; + } else if (q instanceof SetQuantifier) { + /* Create new element to bind to */ + // search if the set 'set' has a size + Binding binding=new Binding(vd,set,exactsize.getsize(set)==1); bindings.add(binding); goodupdate=true; + } else - break; + goodupdate=false; } else if (q instanceof RelationQuantifier) { RelationQuantifier rq=(RelationQuantifier)q; for(int k=0;k<2;k++) { VarDescriptor vd=(k==0)?rq.x:rq.y; + TypeDescriptor td=(k==0)?rq.getRelation().getDomain().getType():rq.getRelation().getRange().getType(); if(inc instanceof SetInclusion) { SetInclusion si=(SetInclusion)inc; - if ((si.elementexpr instanceof VarExpr)&& - (((VarExpr)si.elementexpr).getVar()==vd)) { + + Expr e=si.elementexpr; + + while(e instanceof CastExpr) { + CastExpr ce=(CastExpr)e; + if (ce.getType()!=td) + return false; + e=ce.getExpr(); + } + + if ((e instanceof VarExpr)&& + (((VarExpr)e).getVar()==vd)) { /* Can solve for v */ Binding binding=new Binding(vd,0); + + if (!si.getSet().getType().isSubtypeOf(td)) + return false; bindings.add(binding); } else goodupdate=false; @@ -491,16 +1115,44 @@ public class Termination { RelationInclusion ri=(RelationInclusion)inc; boolean f1=true; boolean f2=true; + + + Expr e=ri.getLeftExpr(); + + while(e instanceof CastExpr) { + CastExpr ce=(CastExpr)e; + if (ce.getType()!=ri.getRelation().getDomain().getType()) + return false; + e=ce.getExpr(); + } if ((ri.getLeftExpr() instanceof VarExpr)&& (((VarExpr)ri.getLeftExpr()).getVar()==vd)) { /* Can solve for v */ Binding binding=new Binding(vd,0); + if (!ri.getRelation().getDomain().getType().isSubtypeOf(td)) + return false; + if (ar.getDomainSet()!=null) + setmapping.put(ri.getLeftExpr(),ar.getDomainSet()); bindings.add(binding); } else f1=false; + + + e=ri.getRightExpr(); + + while(e instanceof CastExpr) { + CastExpr ce=(CastExpr)e; + if (ce.getType()!=ri.getRelation().getRange().getType()) + return false; + e=ce.getExpr(); + } if ((ri.getRightExpr() instanceof VarExpr)&& (((VarExpr)ri.getRightExpr()).getVar()==vd)) { /* Can solve for v */ - Binding binding=new Binding(vd,0); + Binding binding=new Binding(vd,1); + if (!ri.getRelation().getRange().getType().isSubtypeOf(td)) + return false; + if (ar.getRangeSet()!=null) + setmapping.put(ri.getRightExpr(),ar.getRangeSet()); bindings.add(binding); } else f2=false; if (!(f1||f2)) @@ -508,8 +1160,9 @@ public class Termination { } else throw new Error("Inclusion not recognized"); if (!goodupdate) if (isremoval) { - Binding binding=new Binding(vd); - bindings.add(binding); + /* Removals don't need bindings anymore + Binding binding=new Binding(vd); + bindings.add(binding);*/ goodupdate=true; } else break; @@ -520,123 +1173,46 @@ public class Termination { } return goodupdate; } - - static int addtocount=0; - void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) { - System.out.println("Attempting to generate add to set"); - System.out.println(ar.getPredicate().getPredicate().name()); - System.out.println(ar.getPredicate().isNegated()); - for(int i=0;i=0) + continue; + } else if (q instanceof RelationQuantifier) { + RelationDescriptor rd=((RelationQuantifier)q).getRelation(); + if (maxsize.getsize(rd)<=1&& + maxsize.getsize(rd)>=0) + continue; + } + return false; + } + return true; + } - ScopeNode falsify=new ScopeNode(r,false); - TermNode tnfalsify=new TermNode(falsify); - GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify); - ConsequenceNode cnfalsify=new ConsequenceNode(); - TermNode ctnfalsify=new TermNode(cnfalsify); - GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify); - consequence.put(falsify,cgnfalsify); - GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify); - gnfalsify.addEdge(efals); - consequencenodes.add(cgnfalsify); - scopefalsify.put(r,gnfalsify); - scopenodes.add(gnfalsify); + public boolean mutuallyexclusive(SetDescriptor sd1, SetDescriptor sd2) { + if (mutualexclusive(sd1,sd2)|| + mutualexclusive(sd2,sd1)) + return true; + else + return false; + } + + private boolean mutualexclusive(SetDescriptor sd1, SetDescriptor sd2) { + Vector rules=state.vRules; + for(int i=0;i