cee0d24b62df5953a0cc4fd8f58d32a54594fdaa
[jpf-core.git] / src / main / gov / nasa / jpf / listener / VariableConflictTracker.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 package gov.nasa.jpf.listener;
19
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;
28
29 import java.util.*;
30
31 // TODO: Fix for Groovy's model-checking
32 // TODO: This is a listener created to detect device conflicts and global variable conflicts
33 /**
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.
38  */
39 public class VariableConflictTracker extends ListenerAdapter {
40
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;
46   private int timeout;
47   private Timer timeoutTimer;
48   private TimeoutTask timeoutTask;
49
50   private final String SET_LOCATION_METHOD = "setLocationMode";
51   private final String LOCATION_VAR = "location.mode";
52
53   public VariableConflictTracker(Config config) {
54     String[] conflictVars = config.getStringArray("variables");
55     // We are not tracking anything if it is null
56     if (conflictVars != null) {
57       for (String var : conflictVars) {
58         conflictSet.add(var);
59       }
60     }
61     String[] apps = config.getStringArray("apps");
62     // We are not tracking anything if it is null
63     if (apps != null) {
64       for (String var : apps) {
65         appSet.add(var);
66       }
67     }
68     trackLocationVar = config.getBoolean("track_location_var_conflict", false);
69     // Timeout is in minutes
70     timeout = config.getInt("timeout", 0);
71     timeoutTimer = null;
72     timeoutTask = null;
73   }
74
75   // Create a task for timer to do a timeout
76   private class TimeoutTask extends TimerTask {
77
78     VM vm;
79     Timer timer;
80
81     public TimeoutTask(VM vm, Timer timer) {
82       this.vm = vm;
83       this.timer = timer;
84     }
85
86     @Override
87     public void run() {
88       StringBuilder sb = new StringBuilder();
89       sb.append("Execution timeout!\n");
90       ThreadInfo ti = this.vm.getCurrentThread();
91       Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
92       ti.setNextPC(nextIns);
93       this.cancel();
94       this.timer.cancel();
95     }
96   }
97
98   @Override
99   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
100     // Instantiate timeoutTimer
101     if (timeout > 0 && timeoutTimer == null && timeoutTask == null) {
102       timeoutTimer = new Timer();
103       timeoutTask = new TimeoutTask(vm, timeoutTimer);
104       timeoutTimer.schedule(timeoutTask, timeout * 60 * 1000);
105     }
106
107     // CASE #1: Detecting variable write-after-write conflict
108     if (executedInsn instanceof WriteInstruction) {
109       // Check for write-after-write conflict
110       String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
111       for(String var : conflictSet) {
112
113         if (varId.contains(var)) {
114           // Get variable info
115           byte type  = getType(ti, executedInsn);
116           String value = getValue(ti, executedInsn, type);
117           //System.out.println("\n\n" + ti.getStackTrace() + "\n\n");
118           String writer = getWriter(ti.getStack());
119           // Just return if the writer is not one of the listed apps in the .jpf file
120           if (writer == null)
121             return;
122
123           // Check and throw error if conflict is detected
124           checkWriteMapAndThrowError(var, value, writer, ti);
125         }
126       }
127     }
128
129     // CASE #2: Detecting global variable location.mode write-after-write conflict
130     if (trackLocationVar) {
131       MethodInfo mi = executedInsn.getMethodInfo();
132       // Find the last load before return and get the value here
133       if (mi.getName().equals(SET_LOCATION_METHOD) &&
134               executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) {
135         byte type  = getType(ti, executedInsn);
136         String value = getValue(ti, executedInsn, type);
137
138         // Extract the writer app name
139         ClassInfo ci = mi.getClassInfo();
140         String writer = ci.getName();
141
142         // Check and throw error if conflict is detected
143         checkWriteMapAndThrowError(LOCATION_VAR, value, writer, ti);
144       }
145     }
146   }
147
148   private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
149
150     if (writeMap.containsKey(var)) {
151       // Subsequent writes to the variable
152       VarChange current = writeMap.get(var);
153       if (current.writer != writer) {
154         // Conflict is declared when:
155         // 1) Current writer != previous writer, e.g., App1 vs. App2
156         // 2) Current value != previous value, e.g., "locked" vs. "unlocked"
157         if (!current.value.equals(value)) {
158
159           StringBuilder sb = new StringBuilder();
160           sb.append("Conflict between apps " + current.writer + " and " + writer + ": ");
161           sb.append(writer + " has attempted to write the value " + value + " into ");
162           sb.append("variable " + var + " that had already had the value " + current.value);
163           sb.append(" previously written by " + current.writer);
164           Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
165           ti.setNextPC(nextIns);
166         }
167       } else {
168         // No conflict is declared if this variable is written subsequently by the same writer
169         current.writer = writer;
170         current.value = value;
171       }
172     } else {
173       // First write to the variable
174       VarChange change = new VarChange(writer, value);
175       writeMap.put(var, change);
176     }
177   }
178
179   class VarChange {
180     String writer;
181     String value;
182     
183     VarChange(String writer, String value) {
184       this.writer = writer;
185       this.value = value;
186     }
187   }
188
189   // Find the variable writer
190   // It should be one of the apps listed in the .jpf file
191   private String getWriter(List<StackFrame> sfList) {
192     // Start looking from the top of the stack backward
193     for(int i=sfList.size()-1; i>=0; i--) {
194       MethodInfo mi = sfList.get(i).getMethodInfo();
195       if(!mi.isJPFInternal()) {
196         String method = mi.getStackTraceName();
197         // Check against the apps in the appSet
198         for(String app : appSet) {
199           // There is only one writer at a time but we need to always
200           // check all the potential writers in the list
201           if (method.contains(app)) {
202             return app;
203           }
204         }
205       }
206     }
207
208     return null;
209   }
210
211   private byte getType(ThreadInfo ti, Instruction inst) {
212     StackFrame frame;
213     FieldInfo fi;
214     String type;
215
216     frame = ti.getTopFrame();
217     if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
218       return (Types.T_REFERENCE);
219     }
220
221     type = null;
222
223     if (inst instanceof JVMLocalVariableInstruction) {
224       type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
225     } else if (inst instanceof JVMFieldInstruction){
226       fi = ((JVMFieldInstruction) inst).getFieldInfo();
227       type = fi.getType();
228     }
229
230     if (inst instanceof JVMArrayElementInstruction) {
231       return (getTypeFromInstruction(inst));
232     }
233
234     if (type == null) {
235       return (Types.T_VOID);
236     }
237
238     return (decodeType(type));
239   }
240
241   private final static byte getTypeFromInstruction(Instruction inst) {
242     if (inst instanceof JVMArrayElementInstruction)
243       return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
244
245     return(Types.T_VOID);
246   }
247
248   private final static byte getTypeFromInstruction(JVMArrayElementInstruction inst) {
249     String name;
250
251     name = inst.getClass().getName();
252     name = name.substring(name.lastIndexOf('.') + 1);
253
254     switch (name.charAt(0)) {
255       case 'A': return(Types.T_REFERENCE);
256       case 'B': return(Types.T_BYTE);      // Could be a boolean but it is better to assume a byte.
257       case 'C': return(Types.T_CHAR);
258       case 'F': return(Types.T_FLOAT);
259       case 'I': return(Types.T_INT);
260       case 'S': return(Types.T_SHORT);
261       case 'D': return(Types.T_DOUBLE);
262       case 'L': return(Types.T_LONG);
263     }
264
265     return(Types.T_VOID);
266   }
267
268   private final static String encodeType(byte type) {
269     switch (type) {
270       case Types.T_BYTE:    return("B");
271       case Types.T_CHAR:    return("C");
272       case Types.T_DOUBLE:  return("D");
273       case Types.T_FLOAT:   return("F");
274       case Types.T_INT:     return("I");
275       case Types.T_LONG:    return("J");
276       case Types.T_REFERENCE:  return("L");
277       case Types.T_SHORT:   return("S");
278       case Types.T_VOID:    return("V");
279       case Types.T_BOOLEAN: return("Z");
280       case Types.T_ARRAY:   return("[");
281     }
282
283     return("?");
284   }
285
286   private final static byte decodeType(String type) {
287     if (type.charAt(0) == '?'){
288       return(Types.T_REFERENCE);
289     } else {
290       return Types.getBuiltinType(type);
291     }
292   }
293
294   private String getName(ThreadInfo ti, Instruction inst, byte type) {
295     String name;
296     int index;
297     boolean store;
298
299     if ((inst instanceof JVMLocalVariableInstruction) ||
300             (inst instanceof JVMFieldInstruction)) {
301       name = ((LocalVariableInstruction) inst).getVariableId();
302       name = name.substring(name.lastIndexOf('.') + 1);
303
304       return(name);
305     }
306
307     if (inst instanceof JVMArrayElementInstruction) {
308       store  = inst instanceof StoreInstruction;
309       name   = getArrayName(ti, type, store);
310       index  = getArrayIndex(ti, type, store);
311       return(name + '[' + index + ']');
312     }
313
314     return(null);
315   }
316
317   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
318     StackFrame frame;
319     int lo, hi;
320
321     frame = ti.getTopFrame();
322
323     if ((inst instanceof JVMLocalVariableInstruction) ||
324         (inst instanceof JVMFieldInstruction))
325     {
326        if (frame.getTopPos() < 0)
327          return(null);
328
329        lo = frame.peek();
330        hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
331
332        return(decodeValue(type, lo, hi));
333     }
334
335     if (inst instanceof JVMArrayElementInstruction)
336       return(getArrayValue(ti, type));
337
338     return(null);
339   }
340
341   private String getArrayName(ThreadInfo ti, byte type, boolean store) {
342     String attr;
343     int offset;
344
345     offset = calcOffset(type, store) + 1;
346     // <2do> String is really not a good attribute type to retrieve!
347     StackFrame frame = ti.getTopFrame();
348     attr   = frame.getOperandAttr( offset, String.class);
349
350     if (attr != null) {
351       return(attr);
352     }
353
354     return("?");
355   }
356
357   private int getArrayIndex(ThreadInfo ti, byte type, boolean store) {
358     int offset;
359
360     offset = calcOffset(type, store);
361
362     return(ti.getTopFrame().peek(offset));
363   }
364
365   private final static int calcOffset(byte type, boolean store) {
366     if (!store)
367       return(0);
368
369     return(Types.getTypeSize(type));
370   }
371
372   private String getArrayValue(ThreadInfo ti, byte type) {
373     StackFrame frame;
374     int lo, hi;
375
376     frame = ti.getTopFrame();
377     lo    = frame.peek();
378     hi    = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
379
380     return(decodeValue(type, lo, hi));
381   }
382
383   private final static String decodeValue(byte type, int lo, int hi) {
384     switch (type) {
385       case Types.T_ARRAY:   return(null);
386       case Types.T_VOID:    return(null);
387
388       case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
389       case Types.T_BYTE:    return(String.valueOf(lo));
390       case Types.T_CHAR:    return(String.valueOf((char) lo));
391       case Types.T_DOUBLE:  return(String.valueOf(Types.intsToDouble(lo, hi)));
392       case Types.T_FLOAT:   return(String.valueOf(Types.intToFloat(lo)));
393       case Types.T_INT:     return(String.valueOf(lo));
394       case Types.T_LONG:    return(String.valueOf(Types.intsToLong(lo, hi)));
395       case Types.T_SHORT:   return(String.valueOf(lo));
396
397       case Types.T_REFERENCE:
398         ElementInfo ei = VM.getVM().getHeap().get(lo);
399         if (ei == null)
400           return(null);
401
402         ClassInfo ci = ei.getClassInfo();
403         if (ci == null)
404           return(null);
405
406         if (ci.getName().equals("java.lang.String"))
407           return('"' + ei.asString() + '"');
408
409         return(ei.toString());
410
411       default:
412         System.err.println("Unknown type: " + type);
413         return(null);
414      }
415   }
416 }