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.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;
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
41 * @author Nastaran Shafiei <nastaran.shafiei@gmail.com>
43 public class DistributedSimpleDot extends SimpleDot {
45 static final String MP_START_NODE_ATTRS = "shape=octagon,fillcolor=green";
46 static final String MP_NODE_ATTRS = "shape=octagon,fillcolor=azure2";
48 protected String mpNodeAttrs;
49 protected String mpStartNodeAttrs;
51 protected Instruction insn;
53 public DistributedSimpleDot (Config config, JPF jpf) {
56 mpNodeAttrs = config.getString("dot.mp_node_attr", MP_NODE_ATTRS);
57 startNodeAttrs = config.getString("dot.mp_start_node_attr", MP_START_NODE_ATTRS);
61 public void instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nextInstruction, Instruction executedInstruction) {
62 insn = executedInstruction;
66 public void stateAdvanced(Search search){
67 int id = search.getStateId();
68 long edgeId = ((long)lastId << 32) | id;
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)
75 String lastInst = getNextCG();
76 String choice = prcId+"."+getLastChoice();
78 if (search.isErrorState()) {
79 String eid = "e" + search.getNumberOfErrors();
80 printTransition(getStateId(lastId), eid, choice, getError(search));
84 } else if (search.isNewState()) {
86 if (search.isEndState()) {
87 printTransition(getStateId(lastId), getStateId(id), choice, lastInst);
88 printEndState(getStateId(id));
90 printTransition(getStateId(lastId), getStateId(id), choice, lastInst);
91 printMultiProcessState(getStateId(id));
94 } else { // already visited state
95 printTransition(getStateId(lastId), getStateId(id), choice, lastInst);
98 seenEdges.add(edgeId);
103 protected String getNextCG(){
104 if (insn instanceof EXECUTENATIVE) {
105 return getNativeExecCG((EXECUTENATIVE)insn);
107 } else if (insn instanceof JVMFieldInstruction) { // shared object field access
108 return getFieldAccessCG((JVMFieldInstruction)insn);
110 } else if (insn instanceof LockInstruction){ // monitor_enter
111 return getLockCG((LockInstruction)insn);
113 } else if (insn instanceof JVMInvokeInstruction){ // sync method invoke
114 return getInvokeCG((JVMInvokeInstruction)insn);
115 } else if(insn instanceof DIRECTCALLRETURN && vm.getCurrentThread().getNextPC()==null) {
119 return insn.getMnemonic(); // our generic fallback
122 protected void printMultiProcessState(String stateId){
123 if(GlobalSchedulingPoint.isGlobal(vm.getNextChoiceGenerator())) {
127 pw.print(mpNodeAttrs);
130 pw.println(" // multiprc state");
135 protected String getNativeExecCG (EXECUTENATIVE insn){
136 MethodInfo mi = insn.getExecutedMethod();
137 String s = mi.getName();
139 if (s.equals("start")) {
140 s = lastTi.getName() + ".start";
141 } else if (s.equals("wait")) {
142 s = lastTi.getName() + ".wait";
149 protected String getLastChoice() {
150 ChoiceGenerator<?> cg = vm.getChoiceGenerator();
151 Object choice = cg.getNextChoice();
153 if (choice instanceof ThreadInfo){
154 return ((ThreadInfo) choice).getName();
156 return choice.toString();