2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
19 package gov.nasa.jpf.listener;
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.Error;
23 import gov.nasa.jpf.JPF;
24 import gov.nasa.jpf.JPFConfigException;
25 import gov.nasa.jpf.ListenerAdapter;
26 import gov.nasa.jpf.Property;
27 import gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE;
28 import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
29 import gov.nasa.jpf.jvm.bytecode.INVOKESTATIC;
30 import gov.nasa.jpf.jvm.bytecode.JVMInstanceFieldInstruction;
31 import gov.nasa.jpf.jvm.bytecode.InstanceInvocation;
32 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
33 import gov.nasa.jpf.jvm.bytecode.LockInstruction;
34 import gov.nasa.jpf.jvm.bytecode.PUTFIELD;
35 import gov.nasa.jpf.jvm.bytecode.PUTSTATIC;
36 import gov.nasa.jpf.jvm.bytecode.JVMStaticFieldInstruction;
37 import gov.nasa.jpf.report.ConsolePublisher;
38 import gov.nasa.jpf.report.Publisher;
39 import gov.nasa.jpf.search.Search;
40 import gov.nasa.jpf.util.FileUtils;
41 import gov.nasa.jpf.util.Misc;
42 import gov.nasa.jpf.vm.ChoiceGenerator;
43 import gov.nasa.jpf.vm.ElementInfo;
44 import gov.nasa.jpf.vm.ExceptionInfo;
45 import gov.nasa.jpf.vm.Instruction;
46 import gov.nasa.jpf.vm.VM;
47 import gov.nasa.jpf.vm.MethodInfo;
48 import gov.nasa.jpf.vm.NoUncaughtExceptionsProperty;
49 import gov.nasa.jpf.vm.NotDeadlockedProperty;
50 import gov.nasa.jpf.vm.ThreadInfo;
53 import java.io.FileWriter;
54 import java.io.IOException;
55 import java.io.PrintWriter;
56 import java.util.HashSet;
59 * an alternative Graphviz dot-file generator for simple,educational state graphs
60 * except of creating funny wallpapers, it doesn't help much in real life if the
61 * state count gets > 50, but for the small ones it's actually quite readable.
64 * normal states are labeled with their numeric ids, end states are double circled.
65 * start, end and error states are color filled
67 * edges have two labels: the choice value at the beginning and the CG cause
68 * at the end. Only the first incoming edge into a state shows the CG cause
70 * we only render one backtrack edge per from-state
72 * <2do> GraphViz doesn't seem to handle color or fontname for head/tail labels correctly
74 public class SimpleDot extends ListenerAdapter {
76 static final String GRAPH_ATTRS = "pad=0.5";
77 static final String GENERIC_NODE_ATTRS = "shape=circle,style=filled,fillcolor=white";
78 static final String GENERIC_EDGE_ATTRS = "fontsize=10,fontname=Helvetica,fontcolor=blue,color=cadetblue,style=\"setlinewidth(0.5)\",arrowhead=empty,arrowsize=0.5";
79 static final String START_NODE_ATTRS = "fillcolor=green";
80 static final String END_NODE_ATTRS = "shape=doublecircle,fillcolor=cyan";
81 static final String ERROR_NODE_ATTRS = "color=red,fillcolor=lightcoral";
82 static final String BACKTRACK_EDGE_ATTRS = "arrowhead=onormal,color=gray52,style=\"dotted\"";
83 static final String RESTORED_EDGE_ATTRS = "arrowhead=onormal,color=red,style=\"dotted\"";
84 static final String NEW_EDGE_ATTRS = "arrowhead=normal";
85 static final String VISITED_EDGE_ATTRS = "arrowhead=vee";
88 //--- configurable Graphviz attributes
89 protected String graphAttrs;
90 protected String genericNodeAttrs;
91 protected String genericEdgeAttrs;
92 protected String startNodeAttrs;
93 protected String endNodeAttrs;
94 protected String errorNodeAttrs;
95 protected String newEdgeAttrs;
96 protected String visitedEdgeAttrs;
97 protected String backtrackEdgeAttrs;
98 protected String restoreEdgeAttrs;
100 protected boolean showTarget;
101 protected boolean printFile;
104 protected String app;
106 protected PrintWriter pw;
108 protected int lastId = -1; // where we come from
109 protected String lastErrorId;
110 protected ElementInfo lastEi;
111 protected ThreadInfo lastTi; // the last started thread
113 // helper because GraphViz cannot eliminate duplicate edges
114 HashSet<Long> seenEdges;
116 public SimpleDot( Config config, JPF jpf){
118 graphAttrs = config.getString("dot.graph_attr", GRAPH_ATTRS);
119 genericNodeAttrs = config.getString("dot.node_attr", GENERIC_NODE_ATTRS);
120 genericEdgeAttrs = config.getString("dot.edge_attr", GENERIC_EDGE_ATTRS);
121 newEdgeAttrs = config.getString("dot.new_edge_attr", NEW_EDGE_ATTRS);
122 visitedEdgeAttrs = config.getString("dot.visited_edge_attr", VISITED_EDGE_ATTRS);
123 startNodeAttrs = config.getString("dot.start_node_attr", START_NODE_ATTRS);
124 endNodeAttrs = config.getString("dot.end_node_attr", END_NODE_ATTRS);
125 errorNodeAttrs = config.getString("dot.error_node_attr", ERROR_NODE_ATTRS);
126 backtrackEdgeAttrs = config.getString("dot.bt_edge_attr", BACKTRACK_EDGE_ATTRS);
127 restoreEdgeAttrs = config.getString("dot.restore_edge_attr", RESTORED_EDGE_ATTRS);
129 printFile = config.getBoolean("dot.print_file", false);
130 showTarget = config.getBoolean("dot.show_target", false);
132 // app and filename are not known until the search is started
134 jpf.addPublisherExtension(ConsolePublisher.class, this);
137 void initialize (VM vm){
138 Config config = vm.getConfig();
140 app = vm.getSUTName();
141 app = app.replace("+", "__");
142 app = app.replace('.', '_');
144 String fname = config.getString("dot.file");
146 fname = app + ".dot";
150 file = new File(fname);
151 FileWriter fw = new FileWriter(file);
152 pw = new PrintWriter(fw);
153 } catch (IOException iox){
154 throw new JPFConfigException("unable to open SimpleDot output file: " + fname);
157 seenEdges = new HashSet<Long>();
160 //--- the listener interface
163 public void searchStarted(Search search){
169 printStartState("S");
173 public void stateAdvanced(Search search){
174 int id = search.getStateId();
175 long edgeId = ((long)lastId << 32) | id;
177 if (id <0 || seenEdges.contains(edgeId)){
178 return; // skip the root state and property violations (reported separately)
182 if (search.isErrorState()) {
183 String eid = "e" + search.getNumberOfErrors();
184 printTransition(getStateId(lastId), eid, getLastChoice(), getError(search));
185 printErrorState(eid);
188 } else if (search.isNewState()) {
190 if (search.isEndState()) {
191 printTransition(getStateId(lastId), getStateId(id), getLastChoice(), "return");
192 printEndState(getStateId(id));
194 printTransition(getStateId(lastId), getStateId(id), getLastChoice(), getNextCG());
197 } else { // already visited state
198 printTransition(getStateId(lastId), getStateId(id), getLastChoice(), null);
201 seenEdges.add(edgeId);
206 public void stateBacktracked(Search search){
207 int id = search.getStateId();
208 long edgeId = ((long)lastId << 32) | id;
210 if (!seenEdges.contains(edgeId)) {
211 if(lastErrorId!=null) {
212 printBacktrack(lastErrorId, getStateId(id));
215 printBacktrack(getStateId(lastId), getStateId(id));
217 seenEdges.add(edgeId);
223 public void stateRestored(Search search) {
224 int id = search.getStateId();
225 long edgeId = ((long)lastId << 32) | id;
227 if (!seenEdges.contains(edgeId)) {
228 printRestored(getStateId(lastId), getStateId(id));
229 seenEdges.add(edgeId);
235 public void searchFinished (Search search){
241 public void threadStarted (VM vm, ThreadInfo ti){
246 public void objectWait (VM vm, ThreadInfo ti, ElementInfo ei){
252 public void publishFinished (Publisher publisher) {
253 PrintWriter ppw = publisher.getOut();
254 publisher.publishTopicStart("SimpleDot");
256 ppw.println("dot file generated: " + file.getPath());
260 FileUtils.printFile(ppw,file);
265 //--- data collection
267 protected String getStateId (int id){
268 return id < 0 ? "S" : Integer.toString(id);
271 protected String getLastChoice() {
272 ChoiceGenerator<?> cg = vm.getChoiceGenerator();
273 Object choice = cg.getNextChoice();
275 if (choice instanceof ThreadInfo){
276 int idx = ((ThreadInfo)choice).getId();
279 return choice.toString(); // we probably want more here
283 // this is the only method that's more tricky - we have to find a balance
284 // between being conscious enough to not clutter the graph, and expressive
285 // enough to understand it.
286 // <2do> this doesn't deal well with custom or data CGs yet
287 protected String getNextCG(){
288 ChoiceGenerator<?> cg = vm.getNextChoiceGenerator(); // that's the next one
289 Instruction insn = cg.getInsn();
291 if (insn instanceof EXECUTENATIVE) {
292 return getNativeExecCG((EXECUTENATIVE)insn);
294 } else if (insn instanceof JVMFieldInstruction) { // shared object field access
295 return getFieldAccessCG((JVMFieldInstruction)insn);
297 } else if (insn instanceof LockInstruction){ // monitor_enter
298 return getLockCG((LockInstruction)insn);
300 } else if (insn instanceof JVMInvokeInstruction){ // sync method invoke
301 return getInvokeCG((JVMInvokeInstruction)insn);
304 return insn.getMnemonic(); // our generic fallback
307 protected String getNativeExecCG (EXECUTENATIVE insn){
308 MethodInfo mi = insn.getExecutedMethod();
309 String s = mi.getName();
311 if (s.equals("start")) {
312 s = "T" + lastTi.getId() + ".start";
313 } else if (s.equals("wait")) {
314 s = "T" + lastTi.getId() + ".wait";
320 protected String getFieldAccessCG (JVMFieldInstruction insn){
323 if (insn instanceof JVMInstanceFieldInstruction) {
325 if (insn instanceof PUTFIELD) {
327 } else /* if (insn instanceof GETFIELD) */ {
332 int ref = ((JVMInstanceFieldInstruction) insn).getLastThis();
333 s = getInstanceRef(ref) + '.' + s;
336 } else /* if (insn instanceof StaticFieldInstruction) */ {
337 if (insn instanceof PUTSTATIC) {
339 } else /* if (insn instanceof GETSTATIC) */ {
344 String clsName = ((JVMStaticFieldInstruction) insn).getLastClassName();
345 s = Misc.stripToLastDot(clsName) + '.' + s;
349 String varId = insn.getFieldName();
355 protected String getLockCG(LockInstruction insn){
359 int ref = insn.getLastLockRef();
360 s = getInstanceRef(ref) + '.' + s;
366 protected String getInvokeCG (JVMInvokeInstruction insn){
367 MethodInfo mi = insn.getInvokedMethod();
368 String s = mi.getName() + "()";
371 if (insn instanceof InstanceInvocation) {
372 int ref = ((InstanceInvocation) insn).getLastObjRef();
373 s = getInstanceRef(ref) + '.' + s;
375 } else if (insn instanceof INVOKESTATIC) {
376 String clsName = ((INVOKESTATIC) insn).getInvokedClassName();
377 s = Misc.stripToLastDot(clsName) + '.' + s;
384 protected String getError (Search search){
386 Error error = search.getLastError();
387 Property prop = error.getProperty();
389 if (prop instanceof NoUncaughtExceptionsProperty){
390 ExceptionInfo xi = ((NoUncaughtExceptionsProperty)prop).getUncaughtExceptionInfo();
391 return Misc.stripToLastDot(xi.getExceptionClassname());
393 } else if (prop instanceof NotDeadlockedProperty){
398 return Misc.stripToLastDot(prop.getClass().getName());
401 protected static String getInstanceRef (int ref){
402 return "@" + Integer.toHexString(ref).toUpperCase();
405 protected static String getClassObjectRef (int ref){
406 return "#" + Integer.toHexString(ref).toUpperCase();
411 protected void printHeader(){
412 pw.print("digraph ");
417 pw.print(genericNodeAttrs);
421 pw.print(genericEdgeAttrs);
424 pw.println(graphAttrs);
427 pw.print("label=\"");
433 protected void printTransition(String fromState, String toState, String choiceVal, String cgCause){
438 pw.print(" [label=\"");
441 if (cgCause != null){
442 pw.print(NEW_EDGE_ATTRS);
443 pw.print(",headlabel=\"");
447 pw.print(VISITED_EDGE_ATTRS);
452 protected void printBacktrack (String fromState, String toState){
459 pw.print(backtrackEdgeAttrs);
462 pw.println(" // backtrack");
465 protected void printRestored (String fromState, String toState){
472 pw.print(restoreEdgeAttrs);
475 pw.println(" // restored");
478 protected void printStartState(String stateId){
482 pw.print(startNodeAttrs);
485 pw.println(" // start state");
488 protected void printEndState(String stateId){
492 pw.print(endNodeAttrs);
495 pw.println(" // end state");
498 protected void printErrorState(String error){
502 pw.print(errorNodeAttrs);
505 pw.println(" // error state");