From 6c433e9b39cb6c35efc164c8a9831884891de263 Mon Sep 17 00:00:00 2001
From: rtrimana <rtrimana@uci.edu>
Date: Fri, 2 Aug 2019 10:09:05 -0700
Subject: [PATCH 1/1] Adding a timeout feature.

---
 main.jpf                                      |  7 +++-
 .../jpf/listener/VariableConflictTracker.java | 38 +++++++++++++++++--
 2 files changed, 39 insertions(+), 6 deletions(-)

diff --git a/main.jpf b/main.jpf
index 04f14be..7b9a3ad 100644
--- a/main.jpf
+++ b/main.jpf
@@ -5,9 +5,9 @@ listener=gov.nasa.jpf.listener.VariableConflictTracker
 
 # Potentially conflicting variables
 # Alarms
-variables=currentAlarm
+#variables=currentAlarm
 # Locks
-#variables=currentLock
+variables=currentLock
 # 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
 
+# Timeout in minutes (default is 0 which means no timeout)
+timeout=3
+
 #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 80bc940..24eb874 100644
--- 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 int timeout;
+  private Timer timeoutTimer;
 
   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);
+    // 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) {
+    // 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
@@ -79,6 +108,7 @@ public class VariableConflictTracker extends ListenerAdapter {
           // 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)
@@ -108,7 +138,7 @@ public class VariableConflictTracker extends ListenerAdapter {
       }
     }
   }
-  
+
   private void checkWriteMapAndThrowError(String var, String value, String writer, ThreadInfo ti) {
 
     if (writeMap.containsKey(var)) {
-- 
2.34.1