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 }