From aba31a4e9a0ea1e1cf30a6f4eb66baca2ae52c5d Mon Sep 17 00:00:00 2001 From: bdemsky Date: Fri, 16 Apr 2004 00:19:44 +0000 Subject: [PATCH] Additional enhancements to compute mustremove and cantremove sets for node elimination. --- Repair/RepairCompiler/MCC/IR/CastExpr.java | 4 + .../MCC/IR/ConcreteInterferes.java | 9 +- .../RepairCompiler/MCC/IR/GraphAnalysis.java | 99 ++++++++++++++++++- Repair/RepairCompiler/MCC/IR/Termination.java | 48 ++++++--- Repair/RepairCompiler/MCC/IR/Updates.java | 9 +- 5 files changed, 150 insertions(+), 19 deletions(-) diff --git a/Repair/RepairCompiler/MCC/IR/CastExpr.java b/Repair/RepairCompiler/MCC/IR/CastExpr.java index c472ffa..44e085d 100755 --- a/Repair/RepairCompiler/MCC/IR/CastExpr.java +++ b/Repair/RepairCompiler/MCC/IR/CastExpr.java @@ -11,6 +11,10 @@ public class CastExpr extends Expr { return expr.freeVars(); } + public Expr getExpr() { + return expr; + } + public void findmatch(Descriptor d, Set s) { expr.findmatch(d,s); } diff --git a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java index eefde7f..8cb19f8 100755 --- a/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java +++ b/Repair/RepairCompiler/MCC/IR/ConcreteInterferes.java @@ -319,7 +319,14 @@ class ConcreteInterferes { leftdescriptor=((VarExpr)lexpr2).getVar(); else if (lexpr2 instanceof DotExpr) { Expr e=lexpr2; - for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ; + do { + for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ; + if (e instanceof VarExpr) + break; + if (e instanceof CastExpr) + e=((CastExpr)e).getExpr(); + else throw new Error("Bad Expr Type:"+e.name()); + } while (true); leftdescriptor=((VarExpr)e).getVar(); } else throw new Error("Bad Expr"); diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java index 37abc39..7f44c18 100755 --- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java +++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java @@ -1,5 +1,6 @@ package MCC.IR; import java.util.*; +import java.io.*; import MCC.State; public class GraphAnalysis { @@ -49,7 +50,6 @@ public class GraphAnalysis { couldremove.addAll(optionalabstractrepair); couldremove.retainAll(cycles); - /* Look for constraints which can only be satisfied one way */ Vector constraints=termination.state.vConstraints; @@ -68,7 +68,7 @@ public class GraphAnalysis { } /* Search through conjunction which must be satisfied, and attempt - to generate appropriate repair actions + to generate appropriate repair actions. */ HashSet newset=new HashSet(); for(Iterator cit=cantremove.iterator();cit.hasNext();) { @@ -170,8 +170,41 @@ public class GraphAnalysis { if (termination.conjunctions.contains(gn)) return null; // Out of luck } - - + + /* Search through abstract repair actions & correspond data structure updates */ + for(Iterator it=termination.abstractrepairadd.iterator();it.hasNext();) { + GraphNode gn=(GraphNode)it.next(); + TermNode tn=(TermNode)gn.getOwner(); + + for (Iterator edgeit=gn.edges();edgeit.hasNext();) { + GraphNode.Edge e=(GraphNode.Edge)edgeit.next(); + GraphNode gn2=e.getTarget(); + TermNode tn2=(TermNode)gn2.getOwner(); + if (tn2.getType()!=TermNode.UPDATE) + continue; + + boolean containsgn=cantremove.contains(gn); + boolean containsgn2=cantremove.contains(gn2); + + cantremove.add(gn); + cantremove.add(gn2); + + Set cycle=GraphNode.findcycles(cantremove); + if (cycle.contains(gn2)) { + if (!mustremove.contains(gn2)) { + change=true; + mustremove.add(gn2); + } + } + + if (!containsgn) + cantremove.remove(gn); + if (!containsgn2) + cantremove.remove(gn2); + } + } + + /* Searches individual conjunctions + abstract action +updates for cycles */ for(Iterator it=termination.conjunctions.iterator();it.hasNext();) { GraphNode gn=(GraphNode)it.next(); boolean foundnocycle=false; @@ -189,8 +222,10 @@ public class GraphAnalysis { if (tn3.getType()!=TermNode.UPDATE) continue; boolean containsgn=cantremove.contains(gn); + boolean containsgn2=cantremove.contains(gn2); boolean containsgn3=cantremove.contains(gn3); cantremove.add(gn); + cantremove.add(gn2); cantremove.add(gn3); Set cycle=GraphNode.findcycles(cantremove); if (cycle.contains(gn3)) { @@ -204,6 +239,8 @@ public class GraphAnalysis { } if (!containsgn) cantremove.remove(gn); + if (!containsgn2) + cantremove.remove(gn2); if (!containsgn3) cantremove.remove(gn3); } @@ -215,6 +252,53 @@ public class GraphAnalysis { } } } + + /* Searches scope nodes + compensation nodes */ + for(Iterator it=termination.scopenodes.iterator();it.hasNext();) { + GraphNode gn=(GraphNode)it.next(); + boolean foundcompensation=false; + if (nodes.contains(gn)) { + for (Iterator edgeit=gn.edges();edgeit.hasNext();) { + GraphNode.Edge e=(GraphNode.Edge)edgeit.next(); + GraphNode gn2=e.getTarget(); + TermNode tn2=(TermNode)gn2.getOwner(); + + if (tn2.getType()!=TermNode.UPDATE) + continue; + /* We have a compensation node */ + boolean containsgn=cantremove.contains(gn); + boolean containsgn2=cantremove.contains(gn2); + cantremove.add(gn); + cantremove.add(gn2); + + Set cycle=GraphNode.findcycles(cantremove); + if (cycle.contains(gn2)) { + if (!mustremove.contains(gn2)) { + change=true; + mustremove.add(gn2); + } + } else { + if (!mustremove.contains(gn2)) + foundcompensation=true; + } + if (!containsgn) + cantremove.remove(gn); + if (!containsgn2) + cantremove.remove(gn2); + } + } + if (!foundcompensation) { + for (Iterator edgeit=gn.edges();edgeit.hasNext();) { + GraphNode.Edge e=(GraphNode.Edge)edgeit.next(); + GraphNode gn2=e.getTarget(); + TermNode tn2=(TermNode)gn2.getOwner(); + if (tn2.getType()==TermNode.UPDATE) { + cantremove.add(gn2); + break; + } + } + } + } couldremove.removeAll(mustremove); couldremove.removeAll(cantremove); @@ -224,6 +308,13 @@ public class GraphAnalysis { if(change) continue; //recalculate + try { + GraphNode.DOTVisitor.visit(new FileOutputStream("graphsearch.dot"),nodes); + } catch (Exception e) { + e.printStackTrace(); + System.exit(-1); + } + System.out.println("Searching set of "+couldremove.size()+" nodes."); System.out.println("Eliminated must "+mustremove.size()+" nodes"); System.out.println("Eliminated cant "+cantremove.size()+" nodes"); diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 2dccba3..55f4952 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -9,6 +9,8 @@ public class Termination { Hashtable conjunctionmap; HashSet abstractrepair; + HashSet abstractrepairadd; + HashSet updatenodes; HashSet consequencenodes; @@ -29,6 +31,7 @@ public class Termination { conjunctions=new HashSet(); conjunctionmap=new Hashtable(); abstractrepair=new HashSet(); + abstractrepairadd=new HashSet(); scopenodes=new HashSet(); scopesatisfy=new Hashtable(); scopefalsify=new Hashtable(); @@ -293,6 +296,7 @@ public class Termination { predtoabstractmap.put(tp,new HashSet()); ((Set)predtoabstractmap.get(tp)).add(gn); abstractrepair.add(gn); + abstractrepairadd.add(gn); abstractadd.put(sd,gn); DNFPredicate tp2=new DNFPredicate(true,ip); @@ -303,6 +307,7 @@ public class Termination { predtoabstractmap.put(tp2,new HashSet()); ((Set)predtoabstractmap.get(tp2)).add(gn2); abstractrepair.add(gn2); + abstractrepairadd.add(gn2); abstractremove.put(sd,gn2); } @@ -324,6 +329,7 @@ public class Termination { predtoabstractmap.put(tp,new HashSet()); ((Set)predtoabstractmap.get(tp)).add(gn); abstractrepair.add(gn); + abstractrepairadd.add(gn); abstractadd.put(rd,gn); DNFPredicate tp2=new DNFPredicate(true,ip); @@ -334,6 +340,7 @@ public class Termination { predtoabstractmap.put(tp2,new HashSet()); ((Set)predtoabstractmap.get(tp2)).add(gn2); abstractrepair.add(gn2); + abstractrepairadd.add(gn2); abstractremove.put(rd,gn2); } @@ -577,8 +584,11 @@ public class Termination { } RelationInclusion ri=(RelationInclusion)r.getInclusion(); if (!(ri.getLeftExpr() instanceof VarExpr)) { - Updates up=new Updates(ri.getLeftExpr(),leftindex); - un.addUpdate(up); + if (ri.getLeftExpr().isValue()) { + Updates up=new Updates(ri.getLeftExpr(),leftindex); + un.addUpdate(up); + } else + goodflag=false; } else { VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar(); if (vd.isGlobal()) { @@ -588,8 +598,11 @@ public class Termination { goodflag=false; } if (!(ri.getRightExpr() instanceof VarExpr)) { - Updates up=new Updates(ri.getRightExpr(),rightindex); - un.addUpdate(up); + if (ri.getRightExpr().isValue()) { + Updates up=new Updates(ri.getRightExpr(),rightindex); + un.addUpdate(up); + } else + goodflag=false; } else { VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar(); if (vd.isGlobal()) { @@ -741,11 +754,14 @@ public class Termination { if(inc instanceof SetInclusion) { SetInclusion si=(SetInclusion)inc; if (!(si.elementexpr instanceof VarExpr)) { - Updates up=new Updates(si.elementexpr,0); - un.addUpdate(up); + if (si.elementexpr.isValue()) { + Updates up=new Updates(si.elementexpr,0); + un.addUpdate(up); + } else + continue; } else { VarDescriptor vd=((VarExpr)si.elementexpr).getVar(); - if (un.getBinding(vd)==null) { + if (vd.isGlobal()) { Updates up=new Updates(si.elementexpr,0); un.addUpdate(up); } @@ -753,21 +769,27 @@ public class Termination { } else if (inc instanceof RelationInclusion) { RelationInclusion ri=(RelationInclusion)inc; if (!(ri.getLeftExpr() instanceof VarExpr)) { - Updates up=new Updates(ri.getLeftExpr(),0); - un.addUpdate(up); + if (ri.getLeftExpr().isValue()) { + Updates up=new Updates(ri.getLeftExpr(),0); + un.addUpdate(up); + } else + continue; } else { VarDescriptor vd=((VarExpr)ri.getLeftExpr()).getVar(); - if (un.getBinding(vd)==null) { + if (vd.isGlobal()) { Updates up=new Updates(ri.getLeftExpr(),0); un.addUpdate(up); } } if (!(ri.getRightExpr() instanceof VarExpr)) { - Updates up=new Updates(ri.getRightExpr(),1); - un.addUpdate(up); + if (ri.getRightExpr().isValue()) { + Updates up=new Updates(ri.getRightExpr(),1); + un.addUpdate(up); + } else + continue; } else { VarDescriptor vd=((VarExpr)ri.getRightExpr()).getVar(); - if (un.getBinding(vd)==null) { + if (vd.isGlobal()) { Updates up=new Updates(ri.getRightExpr(),1); un.addUpdate(up); } diff --git a/Repair/RepairCompiler/MCC/IR/Updates.java b/Repair/RepairCompiler/MCC/IR/Updates.java index a4e6d80..f17d956 100755 --- a/Repair/RepairCompiler/MCC/IR/Updates.java +++ b/Repair/RepairCompiler/MCC/IR/Updates.java @@ -57,7 +57,14 @@ class Updates { return ((VarExpr)leftexpr).getVar(); } else if (isField()) { Expr e=leftexpr; - for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ; + do { + for(;e instanceof DotExpr;e=((DotExpr)e).getExpr()) ; + if (e instanceof VarExpr) + break; + if (e instanceof CastExpr) + e=((CastExpr)e).getExpr(); + else throw new Error("Unrecognized Expr:"+e.name()); + } while(true); return ((VarExpr)e).getVar(); } else { System.out.println(toString()); -- 2.34.1