1 package gov.nasa.jpf.tools; 20 21 import gov.nasa.jpf.Config; 22 import gov.nasa.jpf.VMListener; 23 import gov.nasa.jpf.SearchListener; 24 import gov.nasa.jpf.VM; 25 import gov.nasa.jpf.Search; 26 import gov.nasa.jpf.jvm.JVM; 27 import gov.nasa.jpf.jvm.bytecode.Instruction; 28 import gov.nasa.jpf.jvm.ThreadInfo; 29 import java.util.ArrayList ; 30 import gov.nasa.jpf.jvm.bytecode.FieldInstruction; 31 import gov.nasa.jpf.jvm.ElementInfo; 32 import gov.nasa.jpf.jvm.bytecode.VariableAccessor; 33 import java.util.HashMap ; 34 import java.util.Iterator ; 35 import java.util.Collection ; 36 import java.util.List ; 37 import java.util.Collections ; 38 import gov.nasa.jpf.JPF; 39 import gov.nasa.jpf.jvm.bytecode.StoreInstruction; 40 import gov.nasa.jpf.jvm.bytecode.ArrayStoreInstruction; 41 import gov.nasa.jpf.jvm.bytecode.GETFIELD; 42 import gov.nasa.jpf.jvm.bytecode.GETSTATIC; 43 import gov.nasa.jpf.jvm.DynamicArea; 44 import gov.nasa.jpf.jvm.bytecode.ALOAD; 45 46 47 53 public class VarTracker implements VMListener, SearchListener { 54 55 int changeThreshold = 1; 56 boolean filterSystemVars = false; 57 String classFilter = null; 58 59 ArrayList queue = new ArrayList (); 60 ThreadInfo lastThread; 61 HashMap stat = new HashMap (); 62 int nStates = 0; 63 int maxDepth; 64 65 void print (int n, int length) { 66 String s = Integer.toString(n); 67 int l = length - s.length(); 68 69 for (int i=0; i<l; i++) { 70 System.out.print(' '); 71 } 72 73 System.out.print(s); 74 } 75 76 void report (String message) { 77 System.out.println("VarTracker results:"); 78 System.out.println(" states: " + nStates); 79 System.out.println(" max depth: " + maxDepth); 80 System.out.println(" term reason: " + message); 81 System.out.println(); 82 System.out.println(" minChange: " + changeThreshold); 83 System.out.println(" filterSysVars: " + filterSystemVars); 84 85 if (classFilter != null) { 86 System.out.println(" classFilter: " + classFilter); 87 } 88 89 System.out.println(); 90 System.out.println(" change variable"); 91 System.out.println("---------------------------------------"); 92 93 Collection values = stat.values(); 94 List valueList = new ArrayList (); 95 valueList.addAll(values); 96 Collections.sort(valueList); 97 98 for (Iterator it = valueList.iterator(); it.hasNext();) { 99 VarStat s = (VarStat)it.next(); 100 int n = s.getChangeCount(); 101 102 if (n < changeThreshold) { 103 break; 104 } 105 106 print(s.nChanges, 12); 107 System.out.print(" "); 108 System.out.println(s.id); 109 } 110 } 111 112 public void stateAdvanced(Search search) { 113 114 if (search.isNewState()) { int stateId = search.getStateNumber(); 116 nStates++; 117 int depth = search.getSearchDepth(); 118 if (depth > maxDepth) maxDepth = depth; 119 120 if (!queue.isEmpty()) { 121 for (Iterator it = queue.iterator(); it.hasNext(); ){ 122 VarChange change = (VarChange) it.next(); 123 String id = change.getVariableId(); 124 VarStat s = (VarStat)stat.get(id); 125 if (s == null) { 126 s = new VarStat(id, stateId); 127 stat.put(id, s); 128 } else { 129 if (s.lastState != stateId) { s.nChanges++; 132 s.lastState = stateId; 133 } 134 } 135 } 136 } 137 } 138 139 queue.clear(); 140 } 141 142 public void stateBacktracked(Search search) { 143 } 145 146 public void stateProcessed (Search search) { 147 } 149 150 public void stateRestored(Search search) { 151 } 153 154 public void propertyViolated(Search search) { 155 report("property violated"); 156 } 157 158 public void searchStarted(Search search) { 159 } 161 162 public void searchConstraintHit(Search search) { 163 report("search constraint hit"); 164 165 System.exit(0); } 167 168 public void searchFinished(Search search) { 169 report("search finished"); 170 } 171 172 public void instructionExecuted(VM vm) { 173 JVM jvm = (JVM)vm; 174 Instruction insn = jvm.getLastInstruction(); 175 ThreadInfo ti = jvm.getLastThreadInfo(); 176 String varId; 177 178 if ( ((((insn instanceof GETFIELD) || (insn instanceof GETSTATIC))) 179 && ((FieldInstruction)insn).isReferenceField()) || 180 (insn instanceof ALOAD)) { 181 int objRef = ti.peek(); 185 if (objRef != -1) { 186 ElementInfo ei = DynamicArea.getHeap().get(objRef); 187 if (ei.isArray()) { 188 varId = ((VariableAccessor)insn).getVariableId(); 189 190 ti.setOperandAttr( varId); 194 } 195 } 196 } 197 else if (insn instanceof StoreInstruction) { 202 if (insn instanceof ArrayStoreInstruction) { 203 Object attr = ti.getOperandAttr(-1); 206 if (attr != null) { 207 varId = attr.toString() + "[]"; 208 } else { 209 varId = "?[]"; 210 } 211 } else { 212 varId = ((VariableAccessor)insn).getVariableId(); 213 } 214 215 if (filterChange(varId)) { 216 queue.add(new VarChange(varId)); 217 lastThread = ti; 218 } 219 } 220 } 221 222 boolean filterChange (String varId) { 223 224 if (filterSystemVars) { 226 if (varId.startsWith("java.")) return false; 227 if (varId.startsWith("javax.")) return false; 228 if (varId.startsWith("sun.")) return false; 229 } 230 231 if ((classFilter != null) && (!varId.startsWith(classFilter))) { 233 return false; 234 } 235 236 for (int i=0; i<queue.size(); i++) { 239 VarChange change = (VarChange) queue.get(i); 240 if (change.getVariableId().equals(varId)) { 241 return false; 242 } 243 } 244 245 return true; 246 } 247 248 public void threadStarted(VM vm) { 249 } 251 252 public void threadTerminated(VM vm) { 253 } 255 256 public void classLoaded(VM vm) { 257 } 259 260 public void objectCreated(VM vm) { 261 } 263 264 public void objectReleased(VM vm) { 265 } 267 268 public void gcBegin(VM vm) { 269 } 271 272 public void gcEnd(VM vm) { 273 } 275 276 public void exceptionThrown(VM vm) { 277 } 279 280 void filterArgs (String [] args) { 281 for (int i=0; i<args.length; i++) { 282 if (args[i].equals("-noSystemVars")) { 283 filterSystemVars = true; 284 args[i] = null; 285 } else if (args[i].equals("-minChange")) { 286 args[i++] = null; 287 if (i < args.length) { 288 changeThreshold = Integer.parseInt(args[i]); 289 args[i] = null; 290 } 291 } else if (args[i].equals("-classFilter")) { 292 args[i++] = null; 293 if (i < args.length) { 294 classFilter = args[i]; 295 args[i] = null; 296 } 297 } 298 } 299 } 300 301 static void printUsage () { 302 System.out.println("VarTracker - a JPF listener tool to report how often variables changed"); 303 System.out.println(" at least once in every state (to detect state space holes)"); 304 System.out.println("usage: java gov.nasa.jpf.tools.VarTracker <jpf-options> <varTracker-options> <class>"); 305 System.out.println(" -noSystemVars : don't report system variable changes (java*)"); 306 System.out.println(" -minChange <num> : don't report variables with less than <num> changes"); 307 System.out.println(" -classFilter <string> : only report changes in classes starting with <string>"); 308 } 309 310 public static void main (String [] args) { 311 if (args.length == 0) { 312 printUsage(); 313 return; 314 } 315 316 VarTracker listener = new VarTracker(); 317 listener.filterArgs(args); 318 319 Config conf = JPF.createConfig(args); 320 322 JPF jpf = new JPF(conf); 323 jpf.addSearchListener(listener); 324 jpf.addVMListener(listener); 325 326 jpf.run(); 327 } 328 } 329 330 class VarStat implements Comparable { 332 String id; int nChanges; 334 335 int lastState; 337 340 VarStat (String varId, int stateId) { 341 id = varId; 342 nChanges = 1; 343 344 lastState = stateId; 345 } 346 347 int getChangeCount () { 348 return nChanges; 349 } 350 351 public int compareTo (Object o) { 352 VarStat other = (VarStat) o; 353 354 if (other.nChanges > nChanges) { 355 return 1; 356 } else if (other.nChanges == nChanges) { 357 return 0; 358 } else { 359 return -1; 360 } 361 } 362 } 363 364 class VarChange { 366 String id; 367 368 VarChange (String varId) { 369 id = varId; 370 } 371 372 String getVariableId () { 373 return id; 374 } 375 } 376 | Popular Tags |