Adding a timeout feature.

diff --git a/main.jpf b/main.jpf
index 04f14be990eb3bb5c2c3b99cd909a1f165b21430..7b9a3ad94abf66bf46c4ac3c5d22e725ae1e7b6b 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -5,9 +5,9 @@ listener=gov.nasa.jpf.listener.VariableConflictTracker
 
 # Potentially conflicting variables
 # Alarms
 
 # Potentially conflicting variables
 # Alarms

-variables=currentAlarm
+#variables=currentAlarm

 # Locks
 # Locks

-#variables=currentLock
+variables=currentLock

 # Thermostats
 #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode
 # Switches
 # Thermostats
 #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode
 # Switches


@@ -25,4 +25,7 @@ apps=App1,App2
 # Tracking the location.mode variable conflict
 #track_location_var_conflict=true
 
 # Tracking the location.mode variable conflict
 #track_location_var_conflict=true
 

+# Timeout in minutes (default is 0 which means no timeout)
+timeout=3
+

 #search.class = gov.nasa.jpf.search.heuristic.UserHeuristic
 #search.class = gov.nasa.jpf.search.heuristic.UserHeuristic

diff --git a/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java b/src/main/gov/nasa/jpf/listener/VariableConflictTracker.java
index 80bc9409cd87fbd68f0f237d4a46e3ad01cb9685..24eb8743cf24eedce698b5f31fc58ea473a7c781 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 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
 
 // 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 final HashSet<String> conflictSet = new HashSet<>();
   private final HashSet<String> appSet = new HashSet<>();
   private boolean trackLocationVar;

+  private int timeout;
+  private Timer timeoutTimer;

 
   private final String SET_LOCATION_METHOD = "setLocationMode";
   private final String LOCATION_VAR = "location.mode";
 
   private final String SET_LOCATION_METHOD = "setLocationMode";
   private final String LOCATION_VAR = "location.mode";


@@ -65,10 +65,39 @@ public class VariableConflictTracker extends ListenerAdapter {
       }
     }
     trackLocationVar = config.getBoolean("track_location_var_conflict", false);
       }
     }
     trackLocationVar = config.getBoolean("track_location_var_conflict", false);

+    // Timeout is in minutes
+    timeout = config.getInt("timeout", 0);
+    timeoutTimer = null;
+  }
+
+  // Create a task for timer to do a timeout
+  private class TimeoutTask extends TimerTask {
+
+    ThreadInfo ti;
+
+    public TimeoutTask(ThreadInfo ti) {
+      this.ti = ti;
+    }
+
+    @Override
+    public void run() {
+      StringBuilder sb = new StringBuilder();
+      sb.append("Execution timeout!\n");
+      Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
+      ti.setNextPC(nextIns);
+    }

   }
 
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
   }
 
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {

+    // Instantiate timeoutTimer
+    if (timeoutTimer == null && timeout > 0) {
+      ThreadList threads = vm.getThreadList();
+      ThreadInfo mainThread = threads.getThreadInfoForId(0);
+      timeoutTimer = new Timer();
+      timeoutTimer.schedule(new TimeoutTask(mainThread), timeout * 60 * 1000);
+    }
+

     // CASE #1: Detecting variable write-after-write conflict
     if (executedInsn instanceof WriteInstruction) {
       // Check for write-after-write conflict
     // CASE #1: Detecting variable write-after-write conflict
     if (executedInsn instanceof WriteInstruction) {
       // Check for write-after-write conflict


@@ -79,6 +108,7 @@ public class VariableConflictTracker extends ListenerAdapter {
           // Get variable info
           byte type  = getType(ti, executedInsn);
           String value = getValue(ti, executedInsn, type);
           // Get variable info
           byte type  = getType(ti, executedInsn);
           String value = getValue(ti, executedInsn, type);

+          //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)
           String writer = getWriter(ti.getStack());
           // Just return if the writer is not one of the listed apps in the .jpf file
           if (writer == null)


@@ -108,7 +138,7 @@ public class VariableConflictTracker extends ListenerAdapter {
       }
     }
   }
       }
     }
   }

-  
+

   private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
 
     if (writeMap.containsKey(var)) {
   private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
 
     if (writeMap.containsKey(var)) {