src/main/gov/nasa/jpf/listener/SimpleDot.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   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
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  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.
  17  */
  18
  19 package gov.nasa.jpf.listener;
  20
  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;
  51
  52 import java.io.File;
  53 import java.io.FileWriter;
  54 import java.io.IOException;
  55 import java.io.PrintWriter;
  56 import java.util.HashSet;
  57
  58 /**
  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.
  62  * Good for papers.
  63  *
  64  * normal states are labeled with their numeric ids, end states are double circled.
  65  * start, end and error states are color filled
  66  *
  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
  69  *
  70  * we only render one backtrack edge per from-state
  71  *
  72  * <2do> GraphViz doesn't seem to handle color or fontname for head/tail labels correctly
  73  */
  74 public class SimpleDot extends ListenerAdapter {
  75
  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";
  86
  87
  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;
  99
 100   protected boolean showTarget;
 101   protected boolean printFile;
 102
 103   protected VM vm;
 104   protected String app;
 105   protected File file;
 106   protected PrintWriter pw;
 107
 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
 112
 113   // helper because GraphViz cannot eliminate duplicate edges
 114   HashSet<Long> seenEdges;
 115
 116   public SimpleDot( Config config, JPF jpf){
 117
 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);
 128
 129     printFile = config.getBoolean("dot.print_file", false);
 130     showTarget = config.getBoolean("dot.show_target", false);
 131
 132     // app and filename are not known until the search is started
 133
 134     jpf.addPublisherExtension(ConsolePublisher.class, this);
 135   }
 136
 137   void initialize (VM vm){
 138     Config config = vm.getConfig();
 139
 140     app = vm.getSUTName();
 141     app = app.replace("+", "__");
 142     app = app.replace('.', '_');
 143
 144     String fname = config.getString("dot.file");
 145     if (fname == null){
 146       fname = app + ".dot";
 147     }
 148
 149     try {
 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);
 155     }
 156
 157     seenEdges = new HashSet<Long>();
 158   }
 159
 160   //--- the listener interface
 161
 162   @Override
 163   public void searchStarted(Search search){
 164     vm = search.getVM();
 165
 166     initialize(vm);
 167
 168     printHeader();
 169     printStartState("S");
 170   }
 171
 172   @Override
 173   public void stateAdvanced(Search search){
 174     int id = search.getStateId();
 175     long edgeId = ((long)lastId << 32) | id;
 176
 177     if (id <0 || seenEdges.contains(edgeId)){
 178       return; // skip the root state and property violations (reported separately)
 179     }
 180
 181
 182     if (search.isErrorState()) {
 183       String eid = "e" + search.getNumberOfErrors();
 184       printTransition(getStateId(lastId), eid, getLastChoice(), getError(search));
 185       printErrorState(eid);
 186       lastErrorId = eid;
 187
 188     } else if (search.isNewState()) {
 189
 190       if (search.isEndState()) {
 191         printTransition(getStateId(lastId), getStateId(id), getLastChoice(), "return");
 192         printEndState(getStateId(id));
 193       } else {
 194         printTransition(getStateId(lastId), getStateId(id), getLastChoice(), getNextCG());
 195       }
 196
 197     } else { // already visited state
 198       printTransition(getStateId(lastId), getStateId(id), getLastChoice(), null);
 199     }
 200
 201     seenEdges.add(edgeId);
 202     lastId = id;
 203   }
 204
 205   @Override
 206   public void stateBacktracked(Search search){
 207     int id = search.getStateId();
 208     long edgeId = ((long)lastId << 32) | id;
 209
 210     if (!seenEdges.contains(edgeId)) {
 211       if(lastErrorId!=null) {
 212         printBacktrack(lastErrorId, getStateId(id));
 213         lastErrorId = null;
 214       } else {
 215         printBacktrack(getStateId(lastId), getStateId(id));
 216       }
 217       seenEdges.add(edgeId);
 218     }
 219     lastId = id;
 220   }
 221
 222   @Override
 223   public void stateRestored(Search search) {
 224     int id = search.getStateId();
 225     long edgeId = ((long)lastId << 32) | id;
 226
 227     if (!seenEdges.contains(edgeId)) {
 228       printRestored(getStateId(lastId), getStateId(id));
 229       seenEdges.add(edgeId);
 230     }
 231     lastId = id;
 232   }
 233
 234   @Override
 235   public void searchFinished (Search search){
 236     pw.println("}");
 237     pw.close();
 238   }
 239
 240   @Override
 241   public void threadStarted (VM vm, ThreadInfo ti){
 242     lastTi = ti;
 243   }
 244
 245   @Override
 246   public void objectWait (VM vm, ThreadInfo ti, ElementInfo ei){
 247     lastEi = ei;
 248     lastTi = ti;
 249   }
 250
 251   @Override
 252   public void publishFinished (Publisher publisher) {
 253     PrintWriter ppw = publisher.getOut();
 254     publisher.publishTopicStart("SimpleDot");
 255
 256     ppw.println("dot file generated: " + file.getPath());
 257
 258     if (printFile){
 259       ppw.println();
 260       FileUtils.printFile(ppw,file);
 261     }
 262   }
 263
 264
 265   //--- data collection
 266
 267   protected String getStateId (int id){
 268     return id < 0 ? "S" : Integer.toString(id);
 269   }
 270
 271   protected String getLastChoice() {
 272     ChoiceGenerator<?> cg = vm.getChoiceGenerator();
 273     Object choice = cg.getNextChoice();
 274
 275     if (choice instanceof ThreadInfo){
 276       int idx = ((ThreadInfo)choice).getId();
 277       return "T"+idx;
 278     } else {
 279       return choice.toString(); // we probably want more here
 280     }
 281   }
 282
 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();
 290
 291     if (insn instanceof EXECUTENATIVE) {
 292       return getNativeExecCG((EXECUTENATIVE)insn);
 293
 294     } else if (insn instanceof JVMFieldInstruction) { // shared object field access
 295       return getFieldAccessCG((JVMFieldInstruction)insn);
 296
 297     } else if (insn instanceof LockInstruction){ // monitor_enter
 298       return getLockCG((LockInstruction)insn);
 299
 300     } else if (insn instanceof JVMInvokeInstruction){ // sync method invoke
 301       return getInvokeCG((JVMInvokeInstruction)insn);
 302     }
 303
 304     return insn.getMnemonic(); // our generic fallback
 305   }
 306
 307   protected String getNativeExecCG (EXECUTENATIVE insn){
 308     MethodInfo mi = insn.getExecutedMethod();
 309     String s = mi.getName();
 310
 311     if (s.equals("start")) {
 312       s = "T" + lastTi.getId() + ".start";
 313     } else if (s.equals("wait")) {
 314       s = "T" + lastTi.getId() + ".wait";
 315     }
 316
 317     return s;
 318   }
 319
 320   protected String getFieldAccessCG (JVMFieldInstruction insn){
 321     String s;
 322
 323     if (insn instanceof JVMInstanceFieldInstruction) {
 324
 325       if (insn instanceof PUTFIELD) {
 326         s = "put";
 327       } else /* if (insn instanceof GETFIELD) */ {
 328         s = "get";
 329       }
 330
 331       if (showTarget){
 332         int ref = ((JVMInstanceFieldInstruction) insn).getLastThis();
 333         s = getInstanceRef(ref) + '.' + s;
 334       }
 335
 336     } else /* if (insn instanceof StaticFieldInstruction) */ {
 337       if (insn instanceof PUTSTATIC) {
 338         s = "put";
 339       } else /* if (insn instanceof GETSTATIC) */ {
 340         s = "get";
 341       }
 342
 343       if (showTarget){
 344         String clsName = ((JVMStaticFieldInstruction) insn).getLastClassName();
 345         s = Misc.stripToLastDot(clsName) + '.' + s;
 346       }
 347     }
 348
 349     String varId = insn.getFieldName();
 350     s = s + ' ' + varId;
 351
 352     return s;
 353   }
 354
 355   protected String getLockCG(LockInstruction insn){
 356     String s = "sync";
 357
 358     if (showTarget){
 359       int ref = insn.getLastLockRef();
 360       s = getInstanceRef(ref) + '.' + s;
 361     }
 362
 363     return s;
 364   }
 365
 366   protected String getInvokeCG (JVMInvokeInstruction insn){
 367     MethodInfo mi = insn.getInvokedMethod();
 368     String s = mi.getName() + "()";
 369
 370     if (showTarget){
 371       if (insn instanceof InstanceInvocation) {
 372         int ref = ((InstanceInvocation) insn).getLastObjRef();
 373         s = getInstanceRef(ref) + '.' + s;
 374
 375       } else if (insn instanceof INVOKESTATIC) {
 376         String clsName = ((INVOKESTATIC) insn).getInvokedClassName();
 377         s = Misc.stripToLastDot(clsName) + '.' + s;
 378       }
 379     }
 380
 381     return s;
 382   }
 383
 384   protected String getError (Search search){
 385     String e;
 386     Error error = search.getLastError();
 387     Property prop = error.getProperty();
 388
 389     if (prop instanceof NoUncaughtExceptionsProperty){
 390       ExceptionInfo xi = ((NoUncaughtExceptionsProperty)prop).getUncaughtExceptionInfo();
 391       return Misc.stripToLastDot(xi.getExceptionClassname());
 392
 393     } else if (prop instanceof NotDeadlockedProperty){
 394       return "deadlock";
 395     }
 396
 397     // fallback
 398     return Misc.stripToLastDot(prop.getClass().getName());
 399   }
 400
 401   protected static String getInstanceRef (int ref){
 402     return "@" + Integer.toHexString(ref).toUpperCase();
 403   }
 404
 405   protected static String getClassObjectRef (int ref){
 406     return "#" + Integer.toHexString(ref).toUpperCase();
 407   }
 408
 409   //--- dot file stuff
 410
 411   protected void printHeader(){
 412     pw.print("digraph ");
 413     pw.print(app);
 414     pw.println(" {");
 415
 416     pw.print("node [");
 417     pw.print(genericNodeAttrs);
 418     pw.println(']');
 419
 420     pw.print("edge [");
 421     pw.print(genericEdgeAttrs);
 422     pw.println(']');
 423
 424     pw.println(graphAttrs);
 425
 426     pw.println();
 427     pw.print("label=\"");
 428     pw.print(app);
 429     pw.print("\"");
 430     pw.println();
 431   }
 432
 433   protected void printTransition(String fromState, String toState, String choiceVal, String cgCause){
 434     pw.println();
 435     pw.print(fromState);
 436     pw.print(" -> ");
 437     pw.print( toState);
 438     pw.print(" [label=\"");
 439     pw.print(choiceVal);
 440     pw.print('"');
 441     if (cgCause != null){
 442       pw.print(NEW_EDGE_ATTRS);
 443       pw.print(",headlabel=\"");
 444       pw.print(cgCause);
 445       pw.print('"');
 446     } else {
 447       pw.print(VISITED_EDGE_ATTRS);
 448     }
 449     pw.println(']');
 450   }
 451
 452   protected void printBacktrack (String fromState, String toState){
 453     pw.println();
 454     pw.print(fromState);
 455     pw.print(" -> ");
 456     pw.print( toState);
 457
 458     pw.print(" [");
 459     pw.print(backtrackEdgeAttrs);
 460     pw.print(']');
 461
 462     pw.println("  // backtrack");
 463   }
 464
 465   protected void printRestored (String fromState, String toState){
 466     pw.println();
 467     pw.print(fromState);
 468     pw.print(" -> ");
 469     pw.print( toState);
 470
 471     pw.print(" [");
 472     pw.print(restoreEdgeAttrs);
 473     pw.print(']');
 474
 475     pw.println("  // restored");
 476   }
 477
 478   protected void printStartState(String stateId){
 479     pw.print(stateId);
 480
 481     pw.print(" [");
 482     pw.print(startNodeAttrs);
 483     pw.print(']');
 484
 485     pw.println("  // start state");
 486   }
 487
 488   protected void printEndState(String stateId){
 489     pw.print(stateId);
 490
 491     pw.print(" [");
 492     pw.print(endNodeAttrs);
 493     pw.print(']');
 494
 495     pw.println("  // end state");
 496   }
 497
 498   protected void printErrorState(String error){
 499     pw.print(error);
 500
 501     pw.print(" [");
 502     pw.print(errorNodeAttrs);
 503     pw.print(']');
 504
 505     pw.println("  // error state");
 506   }
 507 }