Fixing a few bugs in the statistics printout.

[jpf-core.git] / src / main / gov / nasa / jpf / listener / VariableConflictTracker.java

diff --git a/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java b/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java
index 80bc9409cd87fbd68f0f237d4a46e3ad01cb9685..0359ed14b0cd54802e17fe7623a3057c1b29a8df 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java
@@ -26,9 +26,7 @@ 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 java.util.HashSet;
-import java.util.List;
+import java.util.*;
 
 // TODO: Fix for Groovy's model-checking
 // TODO: This is a listener created to detect device conflicts and global variable conflicts
@@ -45,6 +43,8 @@ public class VariableConflictTracker extends ListenerAdapter {
   private final HashSet<String> conflictSet = new HashSet<>();
   private final HashSet<String> appSet = new HashSet<>();
   private boolean trackLocationVar;
+  private long timeout;
+  private long startTime;
 
   private final String SET_LOCATION_METHOD = "setLocationMode";
   private final String LOCATION_VAR = "location.mode";
@@ -65,10 +65,23 @@ public class VariableConflictTracker extends ListenerAdapter {
       }
     }
     trackLocationVar = config.getBoolean("track_location_var_conflict", false);
+    // Timeout input from config is in minutes, so we need to convert into millis
+    timeout = config.getInt("timeout", 0) * 60 * 1000;
+    startTime = System.currentTimeMillis();
   }
 
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+    // Instantiate timeoutTimer
+    if (timeout > 0) {
+      if (System.currentTimeMillis() - startTime > timeout) {
+        StringBuilder sb = new StringBuilder();
+        sb.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
+        Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
+        ti.setNextPC(nextIns);
+      }
+    }
+
     // CASE #1: Detecting variable write-after-write conflict
     if (executedInsn instanceof WriteInstruction) {
       // Check for write-after-write conflict
@@ -79,7 +92,8 @@ public class VariableConflictTracker extends ListenerAdapter {
           // Get variable info
           byte type  = getType(ti, executedInsn);
           String value = getValue(ti, executedInsn, type);
-          String writer = getWriter(ti.getStack());
+          //System.out.println("\n\n" + ti.getStackTrace() + "\n\n");
+          String writer = getWriter(ti.getStack());         
           // Just return if the writer is not one of the listed apps in the .jpf file
           if (writer == null)
             return;
@@ -108,7 +122,7 @@ public class VariableConflictTracker extends ListenerAdapter {
       }
     }
   }
-  
+
   private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
 
     if (writeMap.containsKey(var)) {
@@ -134,9 +148,11 @@ public class VariableConflictTracker extends ListenerAdapter {
         current.value = value;
       }
     } else {
-      // First write to the variable
-      VarChange change = new VarChange(writer, value);
-      writeMap.put(var, change);
+      // First write to the variable only if it is not null
+                       if (value != null) {
+                               VarChange change = new VarChange(writer, value);
+                               writeMap.put(var, change);
+                       }
     }
   }