Adding location.mode variable conflict tracker.

diff --git a/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java b/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java
index 77593f445eb031817623399b1cdebe7bf61bf8ef..4a2c4f15b596ca235fd80e65f9ebad696b696db6 100644 (file)
--- 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.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;
 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
 
 import java.util.HashMap;


@@ -37,28 +40,40 @@ import java.util.List;
  */
 public class VariableConflictTracker extends ListenerAdapter {
 
  */
 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 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");
 
   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");
     }
     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) {
   }
 
   @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)) {
       for(String var : conflictSet) {
 
         if (varId.contains(var)) {


@@ -70,32 +85,59 @@ public class VariableConflictTracker extends ListenerAdapter {
           if (writer == null)
             return;
 
           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);

     }
   }
 
     }
   }