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 long timeout;
  47   private long startTime;
  48
  49   private final String SET_LOCATION_METHOD = "setLocationMode";
  50   private final String LOCATION_VAR = "location.mode";
  51
  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) {
  57         conflictSet.add(var);
  58       }
  59     }
  60     String[] apps = config.getStringArray("apps");
  61     // We are not tracking anything if it is null
  62     if (apps != null) {
  63       for (String var : apps) {
  64         appSet.add(var);
  65       }
  66     }
  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();
  71   }
  72
  73   @Override
  74   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
  75     // Instantiate timeoutTimer
  76     if (timeout > 0) {
  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);
  82       }
  83     }
  84
  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) {
  90
  91         if (varId.contains(var)) {
  92           // Get variable info
  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
  98           if (writer == null)
  99             return;
 100
 101           // Check and throw error if conflict is detected
 102           checkWriteMapAndThrowError(var, value, writer, ti);
 103         }
 104       }
 105     }
 106
 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);
 115
 116         // Extract the writer app name
 117         ClassInfo ci = mi.getClassInfo();
 118         String writer = ci.getName();
 119
 120         // Check and throw error if conflict is detected
 121         checkWriteMapAndThrowError(LOCATION_VAR, value, writer, ti);
 122       }
 123     }
 124   }
 125
 126   private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
 127
 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) {
 136
 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);
 142         }
 143         if (!current.value.equals(value)) {
 144
 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);
 152         }
 153       } else {
 154         // No conflict is declared if this variable is written subsequently by the same writer
 155         current.writer = writer;
 156         current.value = value;
 157       }
 158     } else {
 159       // First write to the variable
 160       VarChange change = new VarChange(writer, value);
 161       writeMap.put(var, change);
 162     }
 163   }
 164
 165   class VarChange {
 166     String writer;
 167     String value;
 168
 169     VarChange(String writer, String value) {
 170       this.writer = writer;
 171       this.value = value;
 172     }
 173   }
 174
 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)) {
 188             return app;
 189           }
 190         }
 191       }
 192     }
 193
 194     return null;
 195   }
 196
 197   private byte getType(ThreadInfo ti, Instruction inst) {
 198     StackFrame frame;
 199     FieldInfo fi;
 200     String type;
 201
 202     frame = ti.getTopFrame();
 203     if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
 204       return (Types.T_REFERENCE);
 205     }
 206
 207     type = null;
 208
 209     if (inst instanceof JVMLocalVariableInstruction) {
 210       type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
 211     } else if (inst instanceof JVMFieldInstruction){
 212       fi = ((JVMFieldInstruction) inst).getFieldInfo();
 213       type = fi.getType();
 214     }
 215
 216     if (inst instanceof JVMArrayElementInstruction) {
 217       return (getTypeFromInstruction(inst));
 218     }
 219
 220     if (type == null) {
 221       return (Types.T_VOID);
 222     }
 223
 224     return (decodeType(type));
 225   }
 226
 227   private final static byte getTypeFromInstruction(Instruction inst) {
 228     if (inst instanceof JVMArrayElementInstruction)
 229       return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
 230
 231     return(Types.T_VOID);
 232   }
 233
 234   private final static byte getTypeFromInstruction(JVMArrayElementInstruction inst) {
 235     String name;
 236
 237     name = inst.getClass().getName();
 238     name = name.substring(name.lastIndexOf('.') + 1);
 239
 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);
 249     }
 250
 251     return(Types.T_VOID);
 252   }
 253
 254   private final static String encodeType(byte type) {
 255     switch (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("[");
 267     }
 268
 269     return("?");
 270   }
 271
 272   private final static byte decodeType(String type) {
 273     if (type.charAt(0) == '?'){
 274       return(Types.T_REFERENCE);
 275     } else {
 276       return Types.getBuiltinType(type);
 277     }
 278   }
 279
 280   private String getName(ThreadInfo ti, Instruction inst, byte type) {
 281     String name;
 282     int index;
 283     boolean store;
 284
 285     if ((inst instanceof JVMLocalVariableInstruction) ||
 286             (inst instanceof JVMFieldInstruction)) {
 287       name = ((LocalVariableInstruction) inst).getVariableId();
 288       name = name.substring(name.lastIndexOf('.') + 1);
 289
 290       return(name);
 291     }
 292
 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 + ']');
 298     }
 299
 300     return(null);
 301   }
 302
 303   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
 304     StackFrame frame;
 305     int lo, hi;
 306
 307     frame = ti.getTopFrame();
 308
 309     if ((inst instanceof JVMLocalVariableInstruction) ||
 310         (inst instanceof JVMFieldInstruction))
 311     {
 312        if (frame.getTopPos() < 0)
 313          return(null);
 314
 315        lo = frame.peek();
 316        hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 317
 318        return(decodeValue(type, lo, hi));
 319     }
 320
 321     if (inst instanceof JVMArrayElementInstruction)
 322       return(getArrayValue(ti, type));
 323
 324     return(null);
 325   }
 326
 327   private String getArrayName(ThreadInfo ti, byte type, boolean store) {
 328     String attr;
 329     int offset;
 330
 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);
 335
 336     if (attr != null) {
 337       return(attr);
 338     }
 339
 340     return("?");
 341   }
 342
 343   private int getArrayIndex(ThreadInfo ti, byte type, boolean store) {
 344     int offset;
 345
 346     offset = calcOffset(type, store);
 347
 348     return(ti.getTopFrame().peek(offset));
 349   }
 350
 351   private final static int calcOffset(byte type, boolean store) {
 352     if (!store)
 353       return(0);
 354
 355     return(Types.getTypeSize(type));
 356   }
 357
 358   private String getArrayValue(ThreadInfo ti, byte type) {
 359     StackFrame frame;
 360     int lo, hi;
 361
 362     frame = ti.getTopFrame();
 363     lo    = frame.peek();
 364     hi    = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 365
 366     return(decodeValue(type, lo, hi));
 367   }
 368
 369   private final static String decodeValue(byte type, int lo, int hi) {
 370     switch (type) {
 371       case Types.T_ARRAY:   return(null);
 372       case Types.T_VOID:    return(null);
 373
 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));
 382
 383       case Types.T_REFERENCE:
 384         ElementInfo ei = VM.getVM().getHeap().get(lo);
 385         if (ei == null)
 386           return(null);
 387
 388         ClassInfo ci = ei.getClassInfo();
 389         if (ci == null)
 390           return(null);
 391
 392         if (ci.getName().equals("java.lang.String"))
 393           return('"' + ei.asString() + '"');
 394
 395         return(ei.toString());
 396
 397       default:
 398         System.err.println("Unknown type: " + type);
 399         return(null);
 400      }
 401   }
 402 }