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 }