From 726db8dc825fb7f33f64f0aca6a4f63b0ba43313 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Fri, 4 Feb 2005 20:15:39 +0000 Subject: [PATCH] Options to print prettier graphs... --- Repair/RepairCompiler/MCC/CLI.java | 5 +- .../RepairCompiler/MCC/CRuntime/buildruntime | 2 +- Repair/RepairCompiler/MCC/Compiler.java | 1 + Repair/RepairCompiler/MCC/IR/GraphNode.java | 48 ++++++++++++++++--- Repair/RepairCompiler/MCC/IR/Termination.java | 30 +++++++++++- 5 files changed, 76 insertions(+), 10 deletions(-) diff --git a/Repair/RepairCompiler/MCC/CLI.java b/Repair/RepairCompiler/MCC/CLI.java index febfd74..7da685b 100755 --- a/Repair/RepairCompiler/MCC/CLI.java +++ b/Repair/RepairCompiler/MCC/CLI.java @@ -11,7 +11,7 @@ import MCC.IR.DebugItem; * files. * * @author le01, 6.035 Staff (6.035-staff@mit.edu) - * @version $Id: CLI.java,v 1.12 2004/08/16 20:53:53 bdemsky Exp $ + * @version $Id: CLI.java,v 1.13 2005/02/04 20:14:52 bdemsky Exp $ */ public class CLI { /** @@ -107,6 +107,7 @@ public class CLI { System.out.println("-prunequantifiernodes"); System.out.println("-cplusplus"); System.out.println("-time"); + System.out.println("-omitcomp"); System.exit(-1); } @@ -116,6 +117,8 @@ public class CLI { debug = true; } else if (args[i].equals("-checkonly")) { Compiler.REPAIR=false; + } else if (args[i].equals("-omitcomp")) { + Compiler.OMITCOMP=true; } else if (args[i].equals("-depth")) { Compiler.debuggraphs.add(new DebugItem(Integer.parseInt(args[i+1]),Integer.parseInt(args[i+2]))); i+=2; diff --git a/Repair/RepairCompiler/MCC/CRuntime/buildruntime b/Repair/RepairCompiler/MCC/CRuntime/buildruntime index 3f66d45..ac3149b 100755 --- a/Repair/RepairCompiler/MCC/CRuntime/buildruntime +++ b/Repair/RepairCompiler/MCC/CRuntime/buildruntime @@ -6,4 +6,4 @@ gcc $FLAG -c instrument.c gcc $FLAG -c libredblack/redblack.c gcc $FLAG -c stack.c gcc $FLAG -c size.c -gcc $FLAG -c cache_aux.c + diff --git a/Repair/RepairCompiler/MCC/Compiler.java b/Repair/RepairCompiler/MCC/Compiler.java index 41794e7..712079d 100755 --- a/Repair/RepairCompiler/MCC/Compiler.java +++ b/Repair/RepairCompiler/MCC/Compiler.java @@ -25,6 +25,7 @@ public class Compiler { public static boolean GENERATEDEBUGPRINT=false; public static boolean GENERATEINSTRUMENT=false; public static boolean ALLOCATECPLUSPLUS=false; + public static boolean OMITCOMP=false; public static boolean TIME=false; public static Vector debuggraphs=new Vector(); diff --git a/Repair/RepairCompiler/MCC/IR/GraphNode.java b/Repair/RepairCompiler/MCC/IR/GraphNode.java index 8c5c119..424a845 100755 --- a/Repair/RepairCompiler/MCC/IR/GraphNode.java +++ b/Repair/RepairCompiler/MCC/IR/GraphNode.java @@ -72,6 +72,16 @@ public class GraphNode { NodeStatus status = UNVISITED; String dotnodeparams = new String(); Object owner = null; + boolean merge=false; + String nodeoption=""; + + public void setOption(String option) { + this.nodeoption=option; + } + + public void setMerge() { + merge=true; + } public GraphNode(String label) { this.nodelabel = label; @@ -263,23 +273,49 @@ public class GraphNode { GraphNode gn = (GraphNode) i.next(); Iterator edges = gn.edges(); String label = gn.getTextLabel(); // + " [" + gn.discoverytime + "," + gn.finishingtime + "];"; - String option=""; - if (cycleset.contains(gn)) - option=",style=bold"; + String option=gn.nodeoption; if (special!=null&&special.contains(gn)) option+=",shape=box"; - output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + option+"];"); + if (!gn.merge) + output.println("\t" + gn.getLabel() + " [label=\"" + label + "\"" + gn.dotnodeparams + option+"];"); + if (!gn.merge) while (edges.hasNext()) { Edge edge = (Edge) edges.next(); GraphNode node = edge.getTarget(); if (nodes.contains(node)) { - String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\""; - output.println("\t" + gn.getLabel() + " -> " + node.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];"); + for(Iterator nodeit=nonmerge(node).iterator();nodeit.hasNext();) { + GraphNode node2=(GraphNode)nodeit.next(); + String edgelabel = useEdgeLabels ? "label=\"" + edge.getLabel() + "\"" : "label=\"\""; + output.println("\t" + gn.getLabel() + " -> " + node2.getLabel() + " [" + edgelabel + edge.dotnodeparams + "];"); + } } } } } + + Set nonmerge(GraphNode gn) { + HashSet newset=new HashSet(); + HashSet toprocess=new HashSet(); + toprocess.add(gn); + while(!toprocess.isEmpty()) { + GraphNode gn2=(GraphNode)toprocess.iterator().next(); + toprocess.remove(gn2); + if (!gn2.merge) + newset.add(gn2); + else { + Iterator edges = gn2.edges(); + while (edges.hasNext()) { + Edge edge = (Edge) edges.next(); + GraphNode node = edge.getTarget(); + if (!newset.contains(node)&&nodes.contains(node)) + toprocess.add(node); + } + } + } + return newset; + } + } /** This function returns the set of nodes involved in cycles. diff --git a/Repair/RepairCompiler/MCC/IR/Termination.java b/Repair/RepairCompiler/MCC/IR/Termination.java index 764453f..5d25732 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; @@ -74,7 +80,8 @@ public class Termination { debugmsg("Generating data structure nodes"); generatedatastructureupdatenodes(); debugmsg("Generating compensation nodes"); - generatecompensationnodes(); + if (!Compiler.OMITCOMP) + generatecompensationnodes(); debugmsg("Generating abstract edges"); generateabstractedges(); debugmsg("Generating scope edges"); @@ -170,6 +177,7 @@ public class Termination { GraphNode gn=new GraphNode("Conj"+i+"A"+j, "Conj ("+i+","+j+") "+dnf.get(j).name() ,tn); + gn.setOption(conjoption); conjunctions.add(gn); if (!conjunctionmap.containsKey(c)) conjunctionmap.put(c,new HashSet()); @@ -190,6 +198,7 @@ public class Termination { GraphNode gn=new GraphNode("Conj"+i+"AQ"+j, "Conj ("+i+","+j+") "+dconst.get(0).name() ,tn); + gn.setOption(conjoption); conjunctions.add(gn); if (!conjunctionmap.containsKey(c)) conjunctionmap.put(c,new HashSet()); @@ -207,6 +216,7 @@ public class Termination { GraphNode gn=new GraphNode("Conj"+i+"AQ"+j, "Conj ("+i+","+j+") "+dconst.get(0).name() ,tn); + gn.setOption(conjoption); conjunctions.add(gn); if (!conjunctionmap.containsKey(c)) conjunctionmap.put(c,new HashSet()); @@ -335,9 +345,12 @@ public class Termination { ScopeNode satisfy=new ScopeNode(r,true); TermNode tnsatisfy=new TermNode(satisfy); GraphNode gnsatisfy=new GraphNode("SatisfyRule"+i,tnsatisfy); + gnsatisfy.setOption(scopeoption); + gnsatisfy.setMerge(); ConsequenceNode cnsatisfy=new ConsequenceNode(); TermNode ctnsatisfy=new TermNode(cnsatisfy); GraphNode cgnsatisfy=new GraphNode("ConseqSatisfyRule"+i,ctnsatisfy); + cgnsatisfy.setOption(conseqoption); consequence.put(satisfy,cgnsatisfy); GraphNode.Edge esat=new GraphNode.Edge("consequencesatisfy"+i,cgnsatisfy); gnsatisfy.addEdge(esat); @@ -348,9 +361,12 @@ public class Termination { ScopeNode falsify=new ScopeNode(r,false); TermNode tnfalsify=new TermNode(falsify); GraphNode gnfalsify=new GraphNode("FalsifyRule"+i,tnfalsify); + gnfalsify.setOption(scopeoption); + gnfalsify.setMerge(); ConsequenceNode cnfalsify=new ConsequenceNode(); TermNode ctnfalsify=new TermNode(cnfalsify); GraphNode cgnfalsify=new GraphNode("ConseqFalsifyRule"+i,ctnfalsify); + cgnfalsify.setOption(conseqoption); consequence.put(falsify,cgnfalsify); GraphNode.Edge efals=new GraphNode.Edge("consequencefalsify"+i,cgnfalsify); gnfalsify.addEdge(efals); @@ -442,7 +458,9 @@ public class Termination { for(int j=0;j