From db8159df12d7899302779f9c2c85f410f91904b1 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 19 Jul 2019 13:15:20 -0700 Subject: [PATCH 1/1] Adding location.mode variable conflict tracker. --- .../jpf/listener/VariableConflictTracker.java | 108 ++++++++++++------ 1 file changed, 75 insertions(+), 33 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java b/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java index 77593f4..4a2c4f1 100644 --- a/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java @@ -21,6 +21,9 @@ import gov.nasa.jpf.Config; 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; @@ -37,28 +40,40 @@ import java.util.List; */ public class VariableConflictTracker extends ListenerAdapter { - private final HashMap executionMap = new HashMap<>(); + private final HashMap writeMap = new HashMap<>(); + private final HashMap readMap = new HashMap<>(); private final HashSet conflictSet = new HashSet<>(); private final HashSet 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)) { @@ -70,32 +85,59 @@ public class VariableConflictTracker extends ListenerAdapter { 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); } } -- 2.34.1