import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.jvm.bytecode.*;
import gov.nasa.jpf.vm.*;
+import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
+import gov.nasa.jpf.vm.bytecode.ReadInstruction;
+import gov.nasa.jpf.vm.bytecode.StoreInstruction;
import gov.nasa.jpf.vm.bytecode.WriteInstruction;
import java.util.HashMap;
*/
public class VariableConflictTracker extends ListenerAdapter {
- private final HashMap<String, VarChange> executionMap = new HashMap<>();
+ private final HashMap<String, VarChange> writeMap = new HashMap<>();
+ private final HashMap<String, VarChange> readMap = new HashMap<>();
private final HashSet<String> conflictSet = new HashSet<>();
private final HashSet<String> appSet = new HashSet<>();
+ private boolean trackLocationVar;
+
+ private final String SET_LOCATION_METHOD = "setLocationMode";
+ private final String LOCATION_VAR = "location.mode";
public VariableConflictTracker(Config config) {
String[] conflictVars = config.getStringArray("variables");
- for(String var : conflictVars) {
- conflictSet.add(var);
+ // We are not tracking anything if it is null
+ if (conflictVars != null) {
+ for (String var : conflictVars) {
+ conflictSet.add(var);
+ }
}
String[] apps = config.getStringArray("apps");
- for(String var : apps) {
- appSet.add(var);
+ // We are not tracking anything if it is null
+ if (apps != null) {
+ for (String var : apps) {
+ appSet.add(var);
+ }
}
+ trackLocationVar = config.getBoolean("track_location_var_conflict", false);
}
@Override
public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
- String varId = "";
-
- if (executedInsn instanceof WriteInstruction){
- varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+ // CASE #1: Detecting variable write-after-write conflict
+ if (executedInsn instanceof WriteInstruction) {
+ // Check for write-after-write conflict
+ String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
for(String var : conflictSet) {
if (varId.contains(var)) {
if (writer == null)
return;
- if (executionMap.containsKey(var)) {
- // Subsequent accesses to the variable
- VarChange current = executionMap.get(var);
- if (current.writer != writer) {
- // Conflict is declared when:
- // 1) Current writer != previous writer, e.g., App1 vs. App2
- // 2) Current value != previous value, e.g., "locked" vs. "unlocked"
- if (!current.value.equals(value)) {
-
- String msg = "Conflict between apps " + current.writer + " and " +
- writer + " for variable " + var;
- Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", msg);
- ti.setNextPC(nextIns);
- }
- } else {
- // No conflict is declared if this variable is accessed subsequently by the same writer
- current.writer = writer;
- current.value = value;
- }
- } else {
- // First access to the variable
- VarChange change = new VarChange(writer, value);
- executionMap.put(var, change);
- }
+ // Check and throw error if conflict is detected
+ checkWriteMapAndThrowError(var, value, writer, ti);
+ }
+ }
+ }
+
+ // CASE #2: Detecting global variable location.mode write-after-write conflict
+ if (trackLocationVar) {
+ MethodInfo mi = executedInsn.getMethodInfo();
+ // Find the last load before return and get the value here
+ if (mi.getName().equals(SET_LOCATION_METHOD) &&
+ executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) {
+ byte type = getType(ti, executedInsn);
+ String value = getValue(ti, executedInsn, type);
+
+ // Extract the writer app name
+ ClassInfo ci = mi.getClassInfo();
+ String writer = ci.getName();
+
+ // Check and throw error if conflict is detected
+ checkWriteMapAndThrowError(LOCATION_VAR, value, writer, ti);
+ }
+ }
+ }
+
+ private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
+
+ if (writeMap.containsKey(var)) {
+ // Subsequent writes to the variable
+ VarChange current = writeMap.get(var);
+ if (current.writer != writer) {
+ // Conflict is declared when:
+ // 1) Current writer != previous writer, e.g., App1 vs. App2
+ // 2) Current value != previous value, e.g., "locked" vs. "unlocked"
+ if (!current.value.equals(value)) {
+
+ StringBuilder sb = new StringBuilder();
+ sb.append("Conflict between apps " + current.writer + " and " + writer + ": ");
+ sb.append(writer + " has attempted to write the value " + value + " into ");
+ sb.append("variable " + var + " that had already had the value " + current.value);
+ sb.append(" previously written by " + current.writer);
+ Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
+ ti.setNextPC(nextIns);
}
+ } else {
+ // No conflict is declared if this variable is written subsequently by the same writer
+ current.writer = writer;
+ current.value = value;
}
+ } else {
+ // First write to the variable
+ VarChange change = new VarChange(writer, value);
+ writeMap.put(var, change);
}
}