Miscellaneous cleanups.
[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.WriteInstruction;
25
26 import java.util.HashMap;
27 import java.util.HashSet;
28 import java.util.List;
29
30 // TODO: Fix for Groovy's model-checking
31 // TODO: This is a listener created to detect device conflicts and global variable conflicts
32 /**
33  * Simple listener tool to track conflicts between 2 apps.
34  * A conflict is defined as one app trying to change the state of a variable
35  * into its opposite value after being set by the other app,
36  * e.g., app1 attempts to change variable A to false after A has been set by app2 to true earlier.
37  */
38 public class VariableConflictTracker extends ListenerAdapter {
39
40   private final HashMap<String, VarChange> executionMap = new HashMap<>();
41   private final HashSet<String> conflictSet = new HashSet<>();
42   private final HashSet<String> appSet = new HashSet<>();
43
44   public VariableConflictTracker(Config config) {
45     String[] conflictVars = config.getStringArray("variables");
46     for(String var : conflictVars) {
47       conflictSet.add(var);
48     }
49     String[] apps = config.getStringArray("apps");
50     for(String var : apps) {
51       appSet.add(var);
52     }
53   }
54
55   @Override
56   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
57     String varId = "";
58
59     if (executedInsn instanceof WriteInstruction){
60
61       varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
62       for(String var : conflictSet) {
63
64         if (varId.contains(var)) {
65           // Get variable info
66           byte type  = getType(ti, executedInsn);
67           String value = getValue(ti, executedInsn, type);
68           String writer = getWriter(ti.getStack());
69           // Just return if the writer is not one of the listed apps in the .jpf file
70           if (writer == null)
71             return;
72
73           if (executionMap.containsKey(var)) {
74             // Subsequent accesses to the variable
75             VarChange current = executionMap.get(var);
76             if (current.writer != writer) {
77               // Conflict is declared when:
78               // 1) Current writer != previous writer, e.g., App1 vs. App2
79               // 2) Current value != previous value, e.g., "locked" vs. "unlocked"
80               if (!current.value.equals(value)) {
81
82                 String msg = "Conflict between apps " + current.writer + " and " +
83                               writer + " for variable " + var;
84                 Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", msg);
85                 ti.setNextPC(nextIns);
86               }
87             } else {
88               // No conflict is declared if this variable is accessed subsequently by the same writer
89               current.writer = writer;
90               current.value = value;
91             }
92           } else {
93             // First access to the variable
94             VarChange change = new VarChange(writer, value);
95             executionMap.put(var, change);
96           }
97         }
98       }
99     }
100   }
101
102   class VarChange {
103     String writer;
104     String value;
105     
106     VarChange(String writer, String value) {
107       this.writer = writer;
108       this.value = value;
109     }
110   }
111
112   // Find the variable writer
113   // It should be one of the apps listed in the .jpf file
114   private String getWriter(List<StackFrame> sfList) {
115
116     for(StackFrame sf : sfList) {
117       MethodInfo mi = sf.getMethodInfo();
118       if(!mi.isJPFInternal()) {
119         String method = mi.getStackTraceName();
120         // Check against the apps in the appSet
121         for(String app : appSet) {
122           if (method.contains(app)) {
123             return app;
124           }
125         }
126       }
127     }
128
129     return null;
130   }
131
132   private byte getType(ThreadInfo ti, Instruction inst) {
133     StackFrame frame;
134     FieldInfo fi;
135     String type;
136
137     frame = ti.getTopFrame();
138     if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
139       return (Types.T_REFERENCE);
140     }
141
142     type = null;
143
144     if (inst instanceof JVMLocalVariableInstruction) {
145       type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
146     } else if (inst instanceof JVMFieldInstruction){
147       fi = ((JVMFieldInstruction) inst).getFieldInfo();
148       type = fi.getType();
149     }
150
151     if (inst instanceof JVMArrayElementInstruction) {
152       return (getTypeFromInstruction(inst));
153     }
154
155     if (type == null) {
156       return (Types.T_VOID);
157     }
158
159     return (decodeType(type));
160   }
161
162   private final static byte getTypeFromInstruction(Instruction inst) {
163     if (inst instanceof JVMArrayElementInstruction)
164       return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
165
166     return(Types.T_VOID);
167   }
168
169   private final static byte getTypeFromInstruction(JVMArrayElementInstruction inst) {
170     String name;
171
172     name = inst.getClass().getName();
173     name = name.substring(name.lastIndexOf('.') + 1);
174
175     switch (name.charAt(0)) {
176       case 'A': return(Types.T_REFERENCE);
177       case 'B': return(Types.T_BYTE);      // Could be a boolean but it is better to assume a byte.
178       case 'C': return(Types.T_CHAR);
179       case 'F': return(Types.T_FLOAT);
180       case 'I': return(Types.T_INT);
181       case 'S': return(Types.T_SHORT);
182       case 'D': return(Types.T_DOUBLE);
183       case 'L': return(Types.T_LONG);
184     }
185
186     return(Types.T_VOID);
187   }
188
189   private final static String encodeType(byte type) {
190     switch (type) {
191       case Types.T_BYTE:    return("B");
192       case Types.T_CHAR:    return("C");
193       case Types.T_DOUBLE:  return("D");
194       case Types.T_FLOAT:   return("F");
195       case Types.T_INT:     return("I");
196       case Types.T_LONG:    return("J");
197       case Types.T_REFERENCE:  return("L");
198       case Types.T_SHORT:   return("S");
199       case Types.T_VOID:    return("V");
200       case Types.T_BOOLEAN: return("Z");
201       case Types.T_ARRAY:   return("[");
202     }
203
204     return("?");
205   }
206
207   private final static byte decodeType(String type) {
208     if (type.charAt(0) == '?'){
209       return(Types.T_REFERENCE);
210     } else {
211       return Types.getBuiltinType(type);
212     }
213   }
214
215   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
216     StackFrame frame;
217     int lo, hi;
218
219     frame = ti.getTopFrame();
220
221     if ((inst instanceof JVMLocalVariableInstruction) ||
222         (inst instanceof JVMFieldInstruction))
223     {
224        if (frame.getTopPos() < 0)
225          return(null);
226
227        lo = frame.peek();
228        hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
229
230        return(decodeValue(type, lo, hi));
231     }
232
233     return(null);
234   }
235
236   private final static String decodeValue(byte type, int lo, int hi) {
237     switch (type) {
238       case Types.T_ARRAY:   return(null);
239       case Types.T_VOID:    return(null);
240
241       case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
242       case Types.T_BYTE:    return(String.valueOf(lo));
243       case Types.T_CHAR:    return(String.valueOf((char) lo));
244       case Types.T_DOUBLE:  return(String.valueOf(Types.intsToDouble(lo, hi)));
245       case Types.T_FLOAT:   return(String.valueOf(Types.intToFloat(lo)));
246       case Types.T_INT:     return(String.valueOf(lo));
247       case Types.T_LONG:    return(String.valueOf(Types.intsToLong(lo, hi)));
248       case Types.T_SHORT:   return(String.valueOf(lo));
249
250       case Types.T_REFERENCE:
251         ElementInfo ei = VM.getVM().getHeap().get(lo);
252         if (ei == null)
253           return(null);
254
255         ClassInfo ci = ei.getClassInfo();
256         if (ci == null)
257           return(null);
258
259         if (ci.getName().equals("java.lang.String"))
260           return('"' + ei.asString() + '"');
261
262         return(ei.toString());
263
264       default:
265         System.err.println("Unknown type: " + type);
266         return(null);
267      }
268   }
269 }