001 package daikon.diff;
002
003 import java.io.*;
004 import java.text.*;
005 import daikon.*;
006 import daikon.inv.Invariant;
007
008 /**
009 * Prints all the invariant pairs, including pairs containing
010 * identical invariants.
011 **/
012 public class PrintAllVisitor extends DepthFirstVisitor {
013
014 // Protected so subclasses can use it.
015 protected static final String lineSep = Global.lineSep;
016
017
018 protected static boolean HUMAN_OUTPUT = false;
019
020
021 private static DecimalFormat CONFIDENCE_FORMAT =
022 new DecimalFormat("0.####");
023
024 private PrintStream ps;
025 private boolean verbose;
026 private boolean printEmptyPpts;
027
028 /**
029 * Stores the output generated when visiting invariant nodes. This
030 * output cannot be printed directly to the print stream, because
031 * the Ppt output must come before the Invariant output.
032 **/
033 private StringBuffer bufOutput = new StringBuffer();
034
035 public PrintAllVisitor(PrintStream ps, boolean verbose,
036 boolean printEmptyPpts) {
037 this.ps = ps;
038 this.verbose = verbose;
039 this.printEmptyPpts = printEmptyPpts;
040 }
041
042 /**
043 * Prints the pair of program points, and all the invariants
044 * contained within them.
045 **/
046 public void visit(PptNode node) {
047 // Empty the string buffer
048 bufOutput.setLength(0);
049
050 super.visit(node);
051
052 if (bufOutput.length() > 0 || printEmptyPpts) {
053 Ppt ppt1 = node.getPpt1();
054 Ppt ppt2 = node.getPpt2();
055
056 ps.print("<");
057 if (ppt1 == null) {
058 ps.print((/*@Nullable*/ String) null);
059 } else {
060 ps.print(ppt1.name());
061 }
062
063 if (ppt1 == null || ppt2 == null || !ppt1.name().equals(ppt2.name())) {
064 ps.print(", ");
065 if (ppt2 == null) {
066 ps.print((/*@Nullable*/ String) null);
067 } else {
068 ps.print(ppt2.name());
069 }
070 }
071 ps.println(">");
072 ps.print(bufOutput.toString());
073 }
074 }
075
076 /**
077 * Prints a pair of invariants. Includes the type of the invariants
078 * and their relationship.
079 **/
080 public void visit(InvNode node) {
081
082 if (HUMAN_OUTPUT) {
083 printHumanOutput (node);
084 return;
085 }
086
087 Invariant inv1 = node.getInv1();
088 Invariant inv2 = node.getInv2();
089
090 bufPrint(" " + "<");
091
092 if (inv1 == null) {
093 bufPrint(null);
094 } else {
095 printInvariant(inv1);
096
097 }
098 bufPrint(", ");
099 if (inv2 == null) {
100 bufPrint((/*@Nullable*/ String) null);
101 } else {
102 printInvariant(inv2);
103 }
104 bufPrint(">");
105
106 int type = DetailedStatisticsVisitor.determineType(inv1, inv2);
107 String typeLabel = DetailedStatisticsVisitor.TYPE_LABELS[type];
108 int rel = DetailedStatisticsVisitor.determineRelationship(inv1, inv2);
109 String relLabel = DetailedStatisticsVisitor.RELATIONSHIP_LABELS[rel];
110
111 bufPrint(" (" + typeLabel + "," + relLabel + ")");
112
113 bufPrintln();
114 }
115
116
117 /**
118 * This method is an alternate printing procedure for
119 * an InvNode so that the output is more human readable.
120 * The format resembles cvs diff with '+' and '-' signs for
121 * the differing invariants. There is no information
122 * on justification or invariant type.
123 **/
124 public void printHumanOutput(InvNode node) {
125
126 Invariant inv1 = node.getInv1();
127 Invariant inv2 = node.getInv2();
128
129 // bufPrint(" " + "<");
130
131 if (inv1 != null && inv2 != null &&
132 (inv1.format().equals (inv2.format()))) {
133 return;
134 }
135
136 if (inv1 == null) {
137 // bufPrint((String) null);
138 } else {
139 // printInvariant(inv1);
140 bufPrintln (("- " + inv1.format()).trim());
141 }
142 // bufPrint(", ");
143 if (inv2 == null) {
144 // bufPrint((String) null);
145 } else {
146 bufPrintln (("+ " + inv2.format()).trim());
147 // printInvariant(inv2);
148 }
149 // bufPrint(">");
150
151 int type = DetailedStatisticsVisitor.determineType(inv1, inv2);
152 int rel = DetailedStatisticsVisitor.determineRelationship(inv1, inv2);
153
154 // String typeLabel = DetailedStatisticsVisitor.TYPE_LABELS[type];
155 // String relLabel = DetailedStatisticsVisitor.RELATIONSHIP_LABELS[rel];
156 // bufPrint(" (" + typeLabel + "," + relLabel + ")");
157
158 bufPrintln();
159 }
160
161
162 /**
163 * Prints an invariant, including its printability and possibly its
164 * confidence. Example: "argv != null {0.9999+}"
165 **/
166 protected void printInvariant(Invariant inv) {
167 if (verbose) {
168 bufPrint(inv.repr_prob());
169 bufPrint(" {");
170 printPrintability(inv);
171 bufPrint("}");
172 } else {
173 bufPrint(inv.format());
174 bufPrint(" {");
175 printConfidence(inv);
176 printPrintability(inv);
177 bufPrint("}");
178 }
179 }
180
181 /**
182 * Prints the confidence of the invariant. Confidences between
183 * .9999 and 1 are rounded to .9999.
184 **/
185 private void printConfidence(Invariant inv) {
186 double conf = inv.getConfidence();
187 if (.9999 < conf && conf < 1) {
188 conf = .9999;
189 }
190 bufPrint(CONFIDENCE_FORMAT.format(conf));
191 }
192
193 /** Prints '+' if the invariant is worth printing, '-' otherwise. **/
194 // XXX This routine takes up most of diff's runtime on large .inv
195 // files, and is not particularly interesting. There should perhaps
196 // be an option to turn it off. -SMcC
197 private void printPrintability(Invariant inv) {
198 if (inv.isWorthPrinting()) {
199 bufPrint("+");
200 } else {
201 bufPrint("-");
202 }
203 }
204
205 // "prints" by appending to a string buffer
206 protected void bufPrint(/*@Nullable*/ String s) {
207 bufOutput.append(s);
208 }
209 protected void bufPrintln(/*@Nullable*/ String s) {
210 bufPrint(s);
211 bufPrintln();
212 }
213 protected void bufPrintln() {
214 bufOutput.append(Global.lineSep);
215 }
216
217 }