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.
18 package gov.nasa.jpf.listener;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.ListenerAdapter;
22 import gov.nasa.jpf.jvm.bytecode.*;
23 import gov.nasa.jpf.vm.*;
24 import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
25 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
26 import gov.nasa.jpf.vm.bytecode.StoreInstruction;
27 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
31 // TODO: Fix for Groovy's model-checking
32 // TODO: This is a listener created to detect device conflicts and global variable conflicts
34 * Simple listener tool to track conflicts between 2 apps.
35 * A conflict is defined as one app trying to change the state of a variable
36 * into its opposite value after being set by the other app,
37 * e.g., app1 attempts to change variable A to false after A has been set by app2 to true earlier.
39 public class VariableConflictTracker extends ListenerAdapter {
41 private final HashMap<String, VarChange> writeMap = new HashMap<>();
42 private final HashMap<String, VarChange> readMap = new HashMap<>();
43 private final HashSet<String> conflictSet = new HashSet<>();
44 private final HashSet<String> appSet = new HashSet<>();
45 private boolean trackLocationVar;
47 private long startTime;
49 private final String SET_LOCATION_METHOD = "setLocationMode";
50 private final String LOCATION_VAR = "location.mode";
52 public VariableConflictTracker(Config config) {
53 String[] conflictVars = config.getStringArray("variables");
54 // We are not tracking anything if it is null
55 if (conflictVars != null) {
56 for (String var : conflictVars) {
60 String[] apps = config.getStringArray("apps");
61 // We are not tracking anything if it is null
63 for (String var : apps) {
67 trackLocationVar = config.getBoolean("track_location_var_conflict", false);
68 // Timeout input from config is in minutes, so we need to convert into millis
69 timeout = config.getInt("timeout", 0) * 60 * 1000;
70 startTime = System.currentTimeMillis();
74 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
75 // Instantiate timeoutTimer
77 if (System.currentTimeMillis() - startTime > timeout) {
78 StringBuilder sb = new StringBuilder();
79 sb.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
80 Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
81 ti.setNextPC(nextIns);
85 // CASE #1: Detecting variable write-after-write conflict
86 if (executedInsn instanceof WriteInstruction) {
87 // Check for write-after-write conflict
88 String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
89 for(String var : conflictSet) {
91 if (varId.contains(var)) {
93 byte type = getType(ti, executedInsn);
94 String value = getValue(ti, executedInsn, type);
95 //System.out.println("\n\n" + ti.getStackTrace() + "\n\n");
96 String writer = getWriter(ti.getStack());
97 // Just return if the writer is not one of the listed apps in the .jpf file
101 // Check and throw error if conflict is detected
102 checkWriteMapAndThrowError(var, value, writer, ti);
107 // CASE #2: Detecting global variable location.mode write-after-write conflict
108 if (trackLocationVar) {
109 MethodInfo mi = executedInsn.getMethodInfo();
110 // Find the last load before return and get the value here
111 if (mi.getName().equals(SET_LOCATION_METHOD) &&
112 executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) {
113 byte type = getType(ti, executedInsn);
114 String value = getValue(ti, executedInsn, type);
116 // Extract the writer app name
117 ClassInfo ci = mi.getClassInfo();
118 String writer = ci.getName();
120 // Check and throw error if conflict is detected
121 checkWriteMapAndThrowError(LOCATION_VAR, value, writer, ti);
126 private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
128 if (writeMap.containsKey(var)) {
129 // Subsequent writes to the variable
130 VarChange current = writeMap.get(var);
131 if (current.writer != writer) {
132 // Conflict is declared when:
133 // 1) Current writer != previous writer, e.g., App1 vs. App2
134 // 2) Current value != previous value, e.g., "locked" vs. "unlocked"
135 if (current.value == null) {
137 StringBuilder sb = new StringBuilder();
138 sb.append("Conflict between apps " + current.writer + " and " + writer + ": ");
139 sb.append("Current value cannot be read (null value)... Please double check with your app output!");
140 Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
141 ti.setNextPC(nextIns);
143 if (!current.value.equals(value)) {
145 StringBuilder sb = new StringBuilder();
146 sb.append("Conflict between apps " + current.writer + " and " + writer + ": ");
147 sb.append(writer + " has attempted to write the value " + value + " into ");
148 sb.append("variable " + var + " that had already had the value " + current.value);
149 sb.append(" previously written by " + current.writer);
150 Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
151 ti.setNextPC(nextIns);
154 // No conflict is declared if this variable is written subsequently by the same writer
155 current.writer = writer;
156 current.value = value;
159 // First write to the variable
160 VarChange change = new VarChange(writer, value);
161 writeMap.put(var, change);
169 VarChange(String writer, String value) {
170 this.writer = writer;
175 // Find the variable writer
176 // It should be one of the apps listed in the .jpf file
177 private String getWriter(List<StackFrame> sfList) {
178 // Start looking from the top of the stack backward
179 for(int i=sfList.size()-1; i>=0; i--) {
180 MethodInfo mi = sfList.get(i).getMethodInfo();
181 if(!mi.isJPFInternal()) {
182 String method = mi.getStackTraceName();
183 // Check against the apps in the appSet
184 for(String app : appSet) {
185 // There is only one writer at a time but we need to always
186 // check all the potential writers in the list
187 if (method.contains(app)) {
197 private byte getType(ThreadInfo ti, Instruction inst) {
202 frame = ti.getTopFrame();
203 if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
204 return (Types.T_REFERENCE);
209 if (inst instanceof JVMLocalVariableInstruction) {
210 type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
211 } else if (inst instanceof JVMFieldInstruction){
212 fi = ((JVMFieldInstruction) inst).getFieldInfo();
216 if (inst instanceof JVMArrayElementInstruction) {
217 return (getTypeFromInstruction(inst));
221 return (Types.T_VOID);
224 return (decodeType(type));
227 private final static byte getTypeFromInstruction(Instruction inst) {
228 if (inst instanceof JVMArrayElementInstruction)
229 return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
231 return(Types.T_VOID);
234 private final static byte getTypeFromInstruction(JVMArrayElementInstruction inst) {
237 name = inst.getClass().getName();
238 name = name.substring(name.lastIndexOf('.') + 1);
240 switch (name.charAt(0)) {
241 case 'A': return(Types.T_REFERENCE);
242 case 'B': return(Types.T_BYTE); // Could be a boolean but it is better to assume a byte.
243 case 'C': return(Types.T_CHAR);
244 case 'F': return(Types.T_FLOAT);
245 case 'I': return(Types.T_INT);
246 case 'S': return(Types.T_SHORT);
247 case 'D': return(Types.T_DOUBLE);
248 case 'L': return(Types.T_LONG);
251 return(Types.T_VOID);
254 private final static String encodeType(byte type) {
256 case Types.T_BYTE: return("B");
257 case Types.T_CHAR: return("C");
258 case Types.T_DOUBLE: return("D");
259 case Types.T_FLOAT: return("F");
260 case Types.T_INT: return("I");
261 case Types.T_LONG: return("J");
262 case Types.T_REFERENCE: return("L");
263 case Types.T_SHORT: return("S");
264 case Types.T_VOID: return("V");
265 case Types.T_BOOLEAN: return("Z");
266 case Types.T_ARRAY: return("[");
272 private final static byte decodeType(String type) {
273 if (type.charAt(0) == '?'){
274 return(Types.T_REFERENCE);
276 return Types.getBuiltinType(type);
280 private String getName(ThreadInfo ti, Instruction inst, byte type) {
285 if ((inst instanceof JVMLocalVariableInstruction) ||
286 (inst instanceof JVMFieldInstruction)) {
287 name = ((LocalVariableInstruction) inst).getVariableId();
288 name = name.substring(name.lastIndexOf('.') + 1);
293 if (inst instanceof JVMArrayElementInstruction) {
294 store = inst instanceof StoreInstruction;
295 name = getArrayName(ti, type, store);
296 index = getArrayIndex(ti, type, store);
297 return(name + '[' + index + ']');
303 private String getValue(ThreadInfo ti, Instruction inst, byte type) {
307 frame = ti.getTopFrame();
309 if ((inst instanceof JVMLocalVariableInstruction) ||
310 (inst instanceof JVMFieldInstruction))
312 if (frame.getTopPos() < 0)
316 hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
318 return(decodeValue(type, lo, hi));
321 if (inst instanceof JVMArrayElementInstruction)
322 return(getArrayValue(ti, type));
327 private String getArrayName(ThreadInfo ti, byte type, boolean store) {
331 offset = calcOffset(type, store) + 1;
332 // <2do> String is really not a good attribute type to retrieve!
333 StackFrame frame = ti.getTopFrame();
334 attr = frame.getOperandAttr( offset, String.class);
343 private int getArrayIndex(ThreadInfo ti, byte type, boolean store) {
346 offset = calcOffset(type, store);
348 return(ti.getTopFrame().peek(offset));
351 private final static int calcOffset(byte type, boolean store) {
355 return(Types.getTypeSize(type));
358 private String getArrayValue(ThreadInfo ti, byte type) {
362 frame = ti.getTopFrame();
364 hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
366 return(decodeValue(type, lo, hi));
369 private final static String decodeValue(byte type, int lo, int hi) {
371 case Types.T_ARRAY: return(null);
372 case Types.T_VOID: return(null);
374 case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
375 case Types.T_BYTE: return(String.valueOf(lo));
376 case Types.T_CHAR: return(String.valueOf((char) lo));
377 case Types.T_DOUBLE: return(String.valueOf(Types.intsToDouble(lo, hi)));
378 case Types.T_FLOAT: return(String.valueOf(Types.intToFloat(lo)));
379 case Types.T_INT: return(String.valueOf(lo));
380 case Types.T_LONG: return(String.valueOf(Types.intsToLong(lo, hi)));
381 case Types.T_SHORT: return(String.valueOf(lo));
383 case Types.T_REFERENCE:
384 ElementInfo ei = VM.getVM().getHeap().get(lo);
388 ClassInfo ci = ei.getClassInfo();
392 if (ci.getName().equals("java.lang.String"))
393 return('"' + ei.asString() + '"');
395 return(ei.toString());
398 System.err.println("Unknown type: " + type);