X-Git-Url: http://plrg.eecs.uci.edu/git/?p=repair.git;a=blobdiff_plain;f=Repair%2FRepairCompiler%2FMCC%2FIR%2FTermination.java;h=046e06062ba0481f9f21aa9a4d270f8475c9dc02;hp=9f00c5b04611ee51dd02ebb952c9268d65741049;hb=494b62b8ddfc3c3a7282aab4ad96d0e10fb1d1bc;hpb=472bc7976276ec6771d9e22688c4926d488053e5 diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 9f00c5b..046e060 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -31,6 +31,12 @@ public class Termination { 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; @@ -50,7 +56,7 @@ public class Termination { predtoabstractmap=new Hashtable(); if (!Compiler.REPAIR) return; - + 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 (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); } } @@ -268,46 +293,71 @@ 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(); - - 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; - } - } + /* 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 + else e=((DotExpr)e).getExpr(); while (e instanceof CastExpr) @@ -959,9 +1083,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 { @@ -971,18 +1107,43 @@ 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); @@ -1009,12 +1170,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; @@ -1022,18 +1197,42 @@ 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); @@ -1056,16 +1255,15 @@ public class Termination { } 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,Hashtable setmapping) { 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); @@ -1074,12 +1272,11 @@ public class Termination { un.addUpdate(u); if (abstractadd.containsKey(rq.relation)) { GraphNode agn=(GraphNode)abstractadd.get(rq.relation); - GraphNode.Edge e=new GraphNode.Edge("requires",agn); + GraphNode.Edge e=new GraphNode.Edge("requiresadd5",agn); gn.addEdge(e); } else { return false; } - } else if (q instanceof SetQuantifier) { SetQuantifier sq=(SetQuantifier)q; if (un.getBinding(sq.var).getType()==Binding.SEARCH) { @@ -1099,7 +1296,7 @@ public class Termination { un.addUpdate(u); if (abstractadd.containsKey(sq.set)) { GraphNode agn=(GraphNode)abstractadd.get(sq.set); - GraphNode.Edge e=new GraphNode.Edge("requires",agn); + GraphNode.Edge e=new GraphNode.Edge("requiresadd6",agn); gn.addEdge(e); } else { return false; @@ -1144,7 +1341,7 @@ public class Termination { } else if (e instanceof TupleOfExpr) { Updates up=new Updates(e,de.getNegation()); un.addUpdate(up); - } else if (e instanceof BooleanLiteralExpr) { + } else if (e instanceof BooleanLiteralExpr) { boolean truth=((BooleanLiteralExpr)e).getValue(); if (de.getNegation()) truth=!truth; @@ -1221,4 +1418,29 @@ public class Termination { } return true; } + + boolean equivalent(SetExpr se, RelationExpr re) { + if (!(se instanceof ImageSetExpr)) + return false; + ImageSetExpr ise=(ImageSetExpr)se; + while(re!=null&&ise!=null) { + if (re.getRelation()!=ise.getRelation()) + return false; + if (re.inverted()!=ise.inverted()) + return false; + if (ise.isimageset) { + ise=ise.getImageSetExpr(); + if (!(re.getExpr() instanceof RelationExpr)) + return false; + re=(RelationExpr)re.getExpr(); + } else { + if (!(re.getExpr() instanceof VarExpr)) + return false; + if (((VarExpr)re.getExpr()).getVar()==ise.getVar()) + return true; //everything matches + return false; + } + } + return false; + } }