From ca628f50b6dedc5c650dea4c6862260efba76136 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Thu, 15 Apr 2004 05:42:07 +0000 Subject: [PATCH] Started adding analysis for modifyrelation nodes. Added check flag. --- Repair/RepairCompiler/MCC/CLI.java | 4 +- Repair/RepairCompiler/MCC/Compiler.java | 2 +- .../RepairCompiler/MCC/IR/GraphAnalysis.java | 138 ++++++++++++++++-- .../MCC/IR/RepairGenerator.java | 4 +- Repair/RepairCompiler/MCC/IR/Termination.java | 17 +++ 5 files changed, 150 insertions(+), 15 deletions(-) diff --git a/Repair/RepairCompiler/MCC/CLI.java b/Repair/RepairCompiler/MCC/CLI.java index 9669077..609455a 100755 --- a/Repair/RepairCompiler/MCC/CLI.java +++ b/Repair/RepairCompiler/MCC/CLI.java @@ -11,7 +11,7 @@ import java.util.StringTokenizer; * files. * * @author le01, 6.035 Staff (6.035-staff@mit.edu) - * @version $Id: CLI.java,v 1.1 2003/07/07 16:13:33 droy Exp $ + * @version $Id: CLI.java,v 1.2 2004/04/15 05:41:46 bdemsky Exp $ */ public class CLI { /** @@ -180,6 +180,8 @@ public class CLI { } else if (args[i].equals("-native")) { context = 0; fNative = true; + } else if (args[i].equals("-checkonly")) { + Compiler.REPAIR=false; } else if (args[i].equals("-vis")) { context = 4; fVis = true; diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java index 0395872..cc1f0de 100755 --- a/Repair/RepairCompiler/MCC/Compiler.java +++ b/Repair/RepairCompiler/MCC/Compiler.java @@ -18,7 +18,7 @@ import MCC.IR.*; public class Compiler { /* Set this flag to false to turn repairs off */ - public static boolean REPAIR=false; + public static boolean REPAIR=true; public static void main(String[] args) { State state = null; diff --git a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java index 96a8645..37abc39 100755 --- a/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java +++ b/Repair/RepairCompiler/MCC/IR/GraphAnalysis.java @@ -17,8 +17,23 @@ public class GraphAnalysis { public Set doAnalysis() { HashSet cantremove=new HashSet(); HashSet mustremove=new HashSet(); + HashSet optionalabstractrepair=new HashSet(); + + for (Iterator it=termination.abstractrepair.iterator();it.hasNext();) { + GraphNode gn=(GraphNode)it.next(); + TermNode tn=(TermNode)gn.getOwner(); + AbstractRepair ar=tn.getAbstract(); + DNFPredicate dpred=ar.getPredicate(); + Set repairnodes=(Set)termination.predtoabstractmap.get(dpred); + if ((repairnodes.size()>1)&& + containsmodify(repairnodes)) { + optionalabstractrepair.add(gn); + } + } + cantremove.addAll(termination.scopenodes); cantremove.addAll(termination.abstractrepair); + cantremove.removeAll(optionalabstractrepair); while(true) { boolean change=false; @@ -28,9 +43,10 @@ public class GraphAnalysis { GraphNode.computeclosure(nodes,mustremove); Set cycles=GraphNode.findcycles(nodes); Set couldremove=new HashSet(); - couldremove.addAll(termination.conjunctions); + couldremove.addAll(termination.conjunctions); couldremove.addAll(termination.updatenodes); couldremove.addAll(termination.consequencenodes); + couldremove.addAll(optionalabstractrepair); couldremove.retainAll(cycles); @@ -50,6 +66,10 @@ public class GraphAnalysis { change=true; } } + + /* Search through conjunction which must be satisfied, and attempt + to generate appropriate repair actions + */ HashSet newset=new HashSet(); for(Iterator cit=cantremove.iterator();cit.hasNext();) { GraphNode gn=(GraphNode)cit.next(); @@ -60,12 +80,9 @@ public class GraphAnalysis { GraphNode.Edge e=(GraphNode.Edge)edgeit.next(); GraphNode gn2=e.getTarget(); TermNode tn2=(TermNode)gn2.getOwner(); - if (tn2.getType()==TermNode.ABSTRACT) { - AbstractRepair ar=tn2.getAbstract(); - if (ar.getType()==AbstractRepair.MODIFYRELATION) { - nomodify=false; - break; - } + if (nodes.contains(gn2)&&!mustremove.contains(gn2)&& + tn2.getType()==TermNode.ABSTRACT) { + HashSet updateset=new HashSet(); for(Iterator upit=gn2.edges();upit.hasNext();) { GraphNode.Edge e2=(GraphNode.Edge)upit.next(); @@ -75,13 +92,52 @@ public class GraphAnalysis { updateset.add(gn3); } updateset.removeAll(mustremove); - if (updateset.size()==1) + + AbstractRepair ar=tn2.getAbstract(); + DNFPredicate dpred=ar.getPredicate(); + Set repairnodes=(Set)termination.predtoabstractmap.get(dpred); + if (repairnodes.size()>1&& + containsmodify(repairnodes)) { + /* We are modifying a relation */ + HashSet retainednodes=new HashSet(); + retainednodes.addAll(repairnodes); + retainednodes.retainAll(nodes); + + if (ar.getType()==AbstractRepair.MODIFYRELATION) { + if (updateset.size()==0) { + if (retainednodes.size()>1) { + mustremove.add(gn); + change=true; + } else return null; /* Out of luck */ + } + if (updateset.size()==1&&retainednodes.size()==1) + toremove.addAll(updateset); /* Required update */ + } else { + /* Addition or removal to relation */ + assert (ar.getType()==AbstractRepair.ADDTORELATION)||(ar.getType()==AbstractRepair.REMOVEFROMRELATION); + if (updateset.size()==0) { + if (containsmodify(retainednodes)) { + /* Both ADD & REMOVE are no good */ + for(Iterator it=retainednodes.iterator();it.hasNext();) { + GraphNode gnit=(GraphNode)it.next(); + TermNode tnit=(TermNode)gnit.getOwner(); + AbstractRepair arit=tnit.getAbstract(); + if (arit.getType()!=AbstractRepair.MODIFYRELATION) { + mustremove.add(gnit); + change=true; + } + } + } else + return null; /* Out of luck */ + } + if (updateset.size()==1&&retainednodes.size()==2) + toremove.addAll(updateset); /* Required update */ + } + } else if (updateset.size()==1) toremove.addAll(updateset); } } - if (nomodify) { - newset.addAll(toremove); - } + newset.addAll(toremove); } } { @@ -182,6 +238,7 @@ public class GraphAnalysis { if (illegal(combination,couldremovevector)) break; Set combinationset=buildset(combination,couldremovevector); + checkmodify(combinationset); combinationset.addAll(mustremove); if (combinationset!=null) { System.out.println("Checkabstract="+checkAbstract(combinationset)); @@ -200,6 +257,44 @@ public class GraphAnalysis { } } + private void checkmodify(Set removednodes) { + for (Iterator it=removednodes.iterator();it.hasNext();) { + GraphNode gn=(GraphNode)it.next(); + TermNode tn=(TermNode)gn.getOwner(); + if (tn.getType()==TermNode.ABSTRACT) { + AbstractRepair ar=tn.getAbstract(); + DNFPredicate dpred=ar.getPredicate(); + Set repairnodes=(Set)termination.predtoabstractmap.get(dpred); + /* Has MODIFYRELATION */ + if (containsmodify(repairnodes)&& + (repairnodes.size()>1)&& + (ar.getType()==AbstractRepair.REMOVEFROMRELATION|| + ar.getType()==AbstractRepair.ADDTORELATION)) { + for(Iterator it2=repairnodes.iterator();it2.hasNext();) { + GraphNode gn2=(GraphNode)it2.next(); + TermNode tn2=(TermNode)gn2.getOwner(); + AbstractRepair ar2=tn2.getAbstract(); + if (ar2.getType()==AbstractRepair.REMOVEFROMRELATION|| + ar2.getType()==AbstractRepair.ADDTORELATION) { + removednodes.add(gn2); + } + } + } + } + } + } + + private static boolean containsmodify(Set repairnodes) { + for (Iterator it=repairnodes.iterator();it.hasNext();) { + GraphNode gn=(GraphNode) it.next(); + TermNode tn=(TermNode)gn.getOwner(); + AbstractRepair ar=tn.getAbstract(); + if (ar.getType()==AbstractRepair.MODIFYRELATION) + return true; + } + return false; + } + private static Set buildset(Vector combination, Vector couldremove) { Set s=new HashSet(); for(int i=0;i1)) { + HashSet retainednodes=new HashSet(); + retainednodes.addAll(repairnodes); + retainednodes.removeAll(removed); + if (!containsmodify(retainednodes)&& + (retainednodes.size()<2)) + return ERR_NOREPAIR; + } else if (removed.contains(gn2)) + return ERR_NOREPAIR; + } + } } } if (!foundrepair) diff --git a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java index 1419a68..53f424c 100755 --- a/Repair/RepairCompiler/MCC/IR/RepairGenerator.java +++ b/Repair/RepairCompiler/MCC/IR/RepairGenerator.java @@ -646,9 +646,9 @@ public class RepairGenerator { ListIterator quantifiers = constraint.quantifiers(); while (quantifiers.hasNext()) { - Quantifier quantifier = (Quantifier) quantifiers.next(); + Quantifier quantifier = (Quantifier) quantifiers.next(); quantifier.generate_open(cr); - } + } cr.outputline("int maybe = 0;"); diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 8aa0370..2dccba3 100755 --- a/Repair/RepairCompiler/MCC/IR/Termination.java +++ b/Repair/RepairCompiler/MCC/IR/Termination.java @@ -19,6 +19,7 @@ public class Termination { Hashtable abstractadd; Hashtable abstractremove; Hashtable conjtonodemap; + Hashtable predtoabstractmap; Set removedset; State state; @@ -37,6 +38,7 @@ public class Termination { abstractadd=new Hashtable(); abstractremove=new Hashtable(); conjtonodemap=new Hashtable(); + predtoabstractmap=new Hashtable(); if (!Compiler.REPAIR) return; @@ -267,6 +269,9 @@ public class Termination { GraphNode gn2=new GraphNode(gn.getLabel()+"A"+i+"B"+ar.type(),gn.getTextLabel()+" #"+i+" "+ar.type(),tn2); GraphNode.Edge e=new GraphNode.Edge("abstract",gn2); gn.addEdge(e); + if (!predtoabstractmap.containsKey(dp)) + predtoabstractmap.put(dp,new HashSet()); + ((Set)predtoabstractmap.get(dp)).add(gn2); abstractrepair.add(gn2); } } @@ -284,6 +289,9 @@ public class Termination { AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTOSET, sd); TermNode tn=new TermNode(ar); GraphNode gn=new GraphNode("AbstractAddSetRule"+i,tn); + if (!predtoabstractmap.containsKey(tp)) + predtoabstractmap.put(tp,new HashSet()); + ((Set)predtoabstractmap.get(tp)).add(gn); abstractrepair.add(gn); abstractadd.put(sd,gn); @@ -291,6 +299,9 @@ public class Termination { AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMSET, sd); TermNode tn2=new TermNode(ar2); GraphNode gn2=new GraphNode("AbstractRemSetRule"+i,tn2); + if (!predtoabstractmap.containsKey(tp2)) + predtoabstractmap.put(tp2,new HashSet()); + ((Set)predtoabstractmap.get(tp2)).add(gn2); abstractrepair.add(gn2); abstractremove.put(sd,gn2); } @@ -309,6 +320,9 @@ public class Termination { AbstractRepair ar=new AbstractRepair(tp, AbstractRepair.ADDTORELATION, rd); TermNode tn=new TermNode(ar); GraphNode gn=new GraphNode("AbstractAddRelRule"+i,tn); + if (!predtoabstractmap.containsKey(tp)) + predtoabstractmap.put(tp,new HashSet()); + ((Set)predtoabstractmap.get(tp)).add(gn); abstractrepair.add(gn); abstractadd.put(rd,gn); @@ -316,6 +330,9 @@ public class Termination { AbstractRepair ar2=new AbstractRepair(tp2, AbstractRepair.REMOVEFROMRELATION, rd); TermNode tn2=new TermNode(ar2); GraphNode gn2=new GraphNode("AbstractRemRelRule"+i,tn2); + if (!predtoabstractmap.containsKey(tp2)) + predtoabstractmap.put(tp2,new HashSet()); + ((Set)predtoabstractmap.get(tp2)).add(gn2); abstractrepair.add(gn2); abstractremove.put(rd,gn2); } -- 2.34.1