X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FTermination.java;h=32b4a1b56866113aee0e9125c231f9a4a84aedd4;hb=202f42f08243277d9c252e6560f8366780c5478b;hp=4d34f0054c8ebf2d5468e01ce56682695a23391f;hpb=ce993d16a8b0057b8d5881be15aed42926e54783;p=repair.git diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 4d34f00..32b4a1b 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; @@ -15,54 +18,170 @@ public class Termination { Hashtable scopesatisfy; Hashtable scopefalsify; 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(); consequence=new Hashtable(); updatenodes=new HashSet(); consequencenodes=new HashSet(); + abstractadd=new Hashtable(); + abstractremove=new Hashtable(); + conjtonodemap=new Hashtable(); + predtoabstractmap=new Hashtable(); + if (!Compiler.REPAIR) + return; + + + for(int i=0;i "+gn2.getTextLabel()); + if (AbstractInterferes.interferes(ar,cons)|| + abstractinterferes.interferes(ar,dp)) { GraphNode.Edge e=new GraphNode.Edge("interferes",gn2); gn.addEdge(e); break; } } } + + for(Iterator scopeiterator=scopenodes.iterator();scopeiterator.hasNext();) { + GraphNode gn2=(GraphNode)scopeiterator.next(); + TermNode tn2=(TermNode)gn2.getOwner(); + ScopeNode sn2=tn2.getScope(); + if (AbstractInterferes.interferes(ar,sn2.getRule(),sn2.getSatisfy())) { + GraphNode.Edge e=new GraphNode.Edge("interferes",gn2); + gn.addEdge(e); + } + } + } + } + + void generatescopenodes() { + 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; } - void generateremovefromrelation(GraphNode gn,AbstractRepair ar) {} - void generateaddtorelation(GraphNode gn,AbstractRepair ar) {} - void generatemodifyrelation(GraphNode gn, AbstractRepair ar) {} + /** 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(); - 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); + 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()) {/* 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 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)) { + VarDescriptor vd=null; + SetDescriptor set=null; + if (q instanceof SetQuantifier) { + vd=((SetQuantifier)q).getVar(); + 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)) { + /* Can solve for v */ + Binding binding=new Binding(vd,0); + bindings.add(binding); + } 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)) { + /* Can solve for v */ + Binding binding=new Binding(vd,0); + bindings.add(binding); + } else f1=false; + if ((ri.getRightExpr() instanceof VarExpr)&& + (((VarExpr)ri.getRightExpr()).getVar()==vd)) { + /* Can solve for v */ + Binding binding=new Binding(vd,0); + bindings.add(binding); + } else f2=false; + if (!(f1||f2)) + goodupdate=false; + } else throw new Error("Inclusion not recognized"); + if (!goodupdate) + if (isremoval) { + /* 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 + 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; + if(inc instanceof SetInclusion) { + SetInclusion si=(SetInclusion)inc; + if ((si.elementexpr instanceof VarExpr)&& + (((VarExpr)si.elementexpr).getVar()==vd)) { + /* Can solve for v */ + Binding binding=new Binding(vd,0); + bindings.add(binding); + } 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)) { + /* Can solve for v */ + Binding binding=new Binding(vd,0); + bindings.add(binding); + } else f1=false; + if ((ri.getRightExpr() instanceof VarExpr)&& + (((VarExpr)ri.getRightExpr()).getVar()==vd)) { + /* Can solve for v */ + Binding binding=new Binding(vd,0); + bindings.add(binding); + } else f2=false; + if (!(f1||f2)) + goodupdate=false; + } else throw new Error("Inclusion not recognized"); + if (!goodupdate) + if (isremoval) { + /* Removals don't need bindings anymore + Binding binding=new Binding(vd); + bindings.add(binding);*/ + goodupdate=true; + } else + break; + } + if (!goodupdate) + break; + } else throw new Error("Quantifier not recognized"); + } + return goodupdate; + } + + /** Adds updates that add an item to the appropriate set or + * relation quantified over by the model definition rule.. */ + + boolean processquantifiers(GraphNode gn,UpdateNode un, Rule r) { + Inclusion inc=r.getInclusion(); + for(Iterator iterator=r.quantifiers();iterator.hasNext();) { + Quantifier q=(Quantifier)iterator.next(); + /* Add quantifier */ + /* FIXME: Analysis to determine when this update is necessary */ + if (q instanceof RelationQuantifier) { + RelationQuantifier rq=(RelationQuantifier)q; + TupleOfExpr toe=new TupleOfExpr(new VarExpr(rq.x),new VarExpr(rq.y),rq.relation); + toe.td=ReservedTypeDescriptor.INT; + Updates u=new Updates(toe,false); + un.addUpdate(u); + if (abstractadd.containsKey(rq.relation)) { + GraphNode agn=(GraphNode)abstractadd.get(rq.relation); + GraphNode.Edge e=new GraphNode.Edge("requires",agn); + gn.addEdge(e); + } else { + return false; + } + + } else if (q instanceof SetQuantifier) { + SetQuantifier sq=(SetQuantifier)q; + if (un.getBinding(sq.var).getType()==Binding.SEARCH) { + Binding b=un.getBinding(sq.var); + Constraint reqc=exactsize.getConstraint(b.getSet()); + constraintdependence.requiresConstraint(gn,reqc); + continue; /* Don't need to ensure addition for search */ + } + + ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set); + eoe.td=ReservedTypeDescriptor.INT; + Updates u=new Updates(eoe,false); + un.addUpdate(u); + if (abstractadd.containsKey(sq.set)) { + GraphNode agn=(GraphNode)abstractadd.get(sq.set); + GraphNode.Edge e=new GraphNode.Edge("requires",agn); + gn.addEdge(e); + } else { + return false; + } + } else return false; + } + return true; + } + + /** This method generates the necessary updates to satisfy the + * conjunction ruleconj. */ + + boolean processconjunction(UpdateNode un,RuleConjunction ruleconj){ + boolean okay=true; + for(int k=0;k=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; + } + + 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