X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FTermination.java;h=8585655710d9b7362f79815640074d404bfb38f4;hp=1ec1dc202a1b7322d15dd724f0dc7ad966df8029;hb=87862c69c1cb47c83a858f0b6e52d9c0bc25913f;hpb=7f5349f8ce0cad85a83e9485b3d083296f9f7737 diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 1ec1dc2..8585655 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -26,8 +26,17 @@ public class Termination { ComputeMaxSize maxsize; State state; AbstractInterferes abstractinterferes; + ConcreteInterferes concreteinterferes; ConstraintDependence constraintdependence; ExactSize exactsize; + ArrayAnalysis arrayanalysis; + Sources sources; + static String conjoption="style=bold"; + static String absrepoption="shape=box,color=blue,style=bold"; + static String updateoption="shape=box,color=red,style=bold"; + static String scopeoption="color=brown"; + static String conseqoption="style=bold,color=green"; + static String compoption="shape=box,color=purple,style=bold"; public Termination(State state) { this.state=state; @@ -54,27 +63,37 @@ public class Termination { for(int i=0;i"+((GraphNode)scopesatisfy.get(r)).getLabel()); + } + if (concreteinterferes.interferes(mun,r,true)) { GraphNode scopenode=(GraphNode)scopesatisfy.get(r); - GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode); + GraphNode.Edge e=new GraphNode.Edge("satisfyscopeinterferes",scopenode); gn.addEdge(e); } - if (ConcreteInterferes.interferes(mun,r,false)) { + if (Compiler.DEBUGGRAPH) { + System.out.println(gn.getLabel()+"--->"+((GraphNode)scopefalsify.get(r)).getLabel()); + } + if (concreteinterferes.interferes(mun,r,false)) { GraphNode scopenode=(GraphNode)scopefalsify.get(r); - GraphNode.Edge e=new GraphNode.Edge("interferes",scopenode); + GraphNode.Edge e=new GraphNode.Edge("falsifyscopeinterferes",scopenode); gn.addEdge(e); } } @@ -206,42 +293,103 @@ public class Termination { GraphNode gn=(GraphNode)absiterator.next(); TermNode tn=(TermNode)gn.getOwner(); AbstractRepair ar=(AbstractRepair)tn.getAbstract(); - + for(Iterator conjiterator=conjunctions.iterator();conjiterator.hasNext();) { GraphNode gn2=(GraphNode)conjiterator.next(); TermNode tn2=(TermNode)gn2.getOwner(); Conjunction conj=tn2.getConjunction(); Constraint cons=tn2.getConstraint(); + /* See if this is a relation wellformedness constraint + that is trivially satisfied. */ + if (abstractinterferes.checkrelationconstraint(ar, cons)) + continue; + if (AbstractInterferes.interferesquantifier(ar,cons)) { + GraphNode.Edge e=new GraphNode.Edge("interferesquantifier",gn2); + gn.addEdge(e); + } else { + for(int i=0;i1)&&(op==Opcode.LT))|| + ((size>=1)&&(op==Opcode.LE))) { + for(int i2=0;i2=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)) { @@ -672,9 +1110,21 @@ public class Termination { } 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 (set==null||!si.getSet().getType().isSubtypeOf(set.getType())) + return false; Binding binding=new Binding(vd,0); bindings.add(binding); } else { @@ -684,16 +1134,45 @@ public class Termination { 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)) @@ -718,12 +1197,26 @@ public class Termination { 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; @@ -731,16 +1224,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)) @@ -762,103 +1283,14 @@ public class Termination { return goodupdate; } - static int addtocount=0; - void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) { - 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