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