src/main/gov/nasa/jpf/listener/DistributedSimpleDot.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.JPF;
  23 import gov.nasa.jpf.jvm.bytecode.DIRECTCALLRETURN;
  24 import gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE;
  25 import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
  26 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
  27 import gov.nasa.jpf.jvm.bytecode.LockInstruction;
  28 import gov.nasa.jpf.search.Search;
  29 import gov.nasa.jpf.vm.ChoiceGenerator;
  30 import gov.nasa.jpf.vm.GlobalSchedulingPoint;
  31 import gov.nasa.jpf.vm.Instruction;
  32 import gov.nasa.jpf.vm.MethodInfo;
  33 import gov.nasa.jpf.vm.ThreadInfo;
  34 import gov.nasa.jpf.vm.VM;
  35
  36 /**
  37  * This is a Graphviz dot-file generator similar to SimpleDot. It is useful in
  38  * the case of Multiprocess applications. It distinguishes local choices from global
  39  * choices.
  40  *
  41  * @author Nastaran Shafiei <nastaran.shafiei@gmail.com>
  42  */
  43 public class DistributedSimpleDot extends SimpleDot {
  44
  45   static final String MP_START_NODE_ATTRS = "shape=octagon,fillcolor=green";
  46   static final String MP_NODE_ATTRS = "shape=octagon,fillcolor=azure2";
  47
  48   protected String mpNodeAttrs;
  49   protected String mpStartNodeAttrs;
  50
  51   protected Instruction insn;
  52
  53   public DistributedSimpleDot (Config config, JPF jpf) {
  54     super(config, jpf);
  55
  56     mpNodeAttrs = config.getString("dot.mp_node_attr", MP_NODE_ATTRS);
  57     startNodeAttrs = config.getString("dot.mp_start_node_attr", MP_START_NODE_ATTRS);
  58   }
  59
  60   @Override
  61   public void instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nextInstruction, Instruction executedInstruction) {
  62     insn = executedInstruction;
  63   }
  64
  65   @Override
  66   public void stateAdvanced(Search search){
  67     int id = search.getStateId();
  68     long edgeId = ((long)lastId << 32) | id;
  69
  70     String prcId = "P"+Integer.toString(search.getVM().getCurrentApplicationContext().getId());
  71     if (id <0 || seenEdges.contains(edgeId)){
  72       return; // skip the root state and property violations (reported separately)
  73     }
  74
  75     String lastInst = getNextCG();
  76     String choice =  prcId+"."+getLastChoice();
  77
  78     if (search.isErrorState()) {
  79       String eid = "e" + search.getNumberOfErrors();
  80       printTransition(getStateId(lastId), eid, choice, getError(search));
  81       printErrorState(eid);
  82       lastErrorId = eid;
  83
  84     } else if (search.isNewState()) {
  85
  86       if (search.isEndState()) {
  87         printTransition(getStateId(lastId), getStateId(id), choice, lastInst);
  88         printEndState(getStateId(id));
  89       } else {
  90         printTransition(getStateId(lastId), getStateId(id), choice, lastInst);
  91         printMultiProcessState(getStateId(id));
  92       }
  93
  94     } else { // already visited state
  95       printTransition(getStateId(lastId), getStateId(id), choice, lastInst);
  96     }
  97
  98     seenEdges.add(edgeId);
  99     lastId = id;
 100   }
 101
 102   @Override
 103   protected String getNextCG(){
 104     if (insn instanceof EXECUTENATIVE) {
 105       return getNativeExecCG((EXECUTENATIVE)insn);
 106
 107     } else if (insn instanceof JVMFieldInstruction) { // shared object field access
 108       return getFieldAccessCG((JVMFieldInstruction)insn);
 109
 110     } else if (insn instanceof LockInstruction){ // monitor_enter
 111       return getLockCG((LockInstruction)insn);
 112
 113     } else if (insn instanceof JVMInvokeInstruction){ // sync method invoke
 114       return getInvokeCG((JVMInvokeInstruction)insn);
 115     } else if(insn instanceof DIRECTCALLRETURN && vm.getCurrentThread().getNextPC()==null) {
 116       return "return";
 117     }
 118
 119     return insn.getMnemonic(); // our generic fallback
 120   }
 121
 122   protected void printMultiProcessState(String stateId){
 123     if(GlobalSchedulingPoint.isGlobal(vm.getNextChoiceGenerator())) {
 124       pw.print(stateId);
 125
 126       pw.print(" [");
 127       pw.print(mpNodeAttrs);
 128       pw.print(']');
 129
 130       pw.println("  // multiprc state");
 131     }
 132   }
 133
 134   @Override
 135   protected String getNativeExecCG (EXECUTENATIVE insn){
 136     MethodInfo mi = insn.getExecutedMethod();
 137     String s = mi.getName();
 138
 139     if (s.equals("start")) {
 140       s = lastTi.getName() + ".start";
 141     } else if (s.equals("wait")) {
 142       s = lastTi.getName() + ".wait";
 143     }
 144
 145     return s;
 146   }
 147
 148   @Override
 149   protected String getLastChoice() {
 150     ChoiceGenerator<?> cg = vm.getChoiceGenerator();
 151     Object choice = cg.getNextChoice();
 152
 153     if (choice instanceof ThreadInfo){
 154        return ((ThreadInfo) choice).getName();
 155     } else {
 156       return choice.toString();
 157     }
 158   }
 159 }