Adding manual transactions to the conflict tracker

diff --git a/main.jpf b/main.jpf
index cfef551bc29338a9abf72d472ea41f4975d12145..efa82cc77d190d2ea759554fc519344628a12dc5 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -5,7 +5,7 @@ target = main
 #listener=gov.nasa.jpf.listener.StateReducer
 #listener=gov.nasa.jpf.listener.StateReducerOld
 #listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer
-listener=gov.nasa.jpf.listener.ConflictTracker
+listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer
 
 # Potentially conflicting variables
 # Alarms
@@ -34,9 +34,6 @@ variables=currentLock
 # Potentially conflicting apps (we default to App1 and App2 for now)
 apps=App1,App2
 
-# Writer classes with manual input to detect direct-direct interactions
-manualClasses=appTouch,AeonKeyFob,Button,NfcTouch,ThreeAxis
-
 # Tracking the location.mode variable conflict
 #track_location_var_conflict=true
 

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index fd7311715a21d1636c5d67972a8b47f2a4fef422..b05c9f3837f115902a14b19fb746c9068ef94f94 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -75,13 +75,6 @@ public class ConflictTracker extends ListenerAdapter {
         appSet.add(var);
       }
     }
-    String[] manualClasses = config.getStringArray("manualClasses");
-    // We are not tracking anything if it is null
-    if (manualClasses != null) {
-      for (String var : manualClasses) {
-        manualSet.add(var);
-      }
-    }
 
     // Timeout input from config is in minutes, so we need to convert into millis
     timeout = config.getInt("timeout", 0) * 60 * 1000;
@@ -422,7 +415,7 @@ public class ConflictTracker extends ListenerAdapter {
 
       lo = frame.peek();
       hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
-
+       
       return(decodeValue(type, lo, hi));
     }
 
@@ -457,7 +450,7 @@ public class ConflictTracker extends ListenerAdapter {
 
         if (ci.getName().equals("java.lang.String"))
           return('"' + ei.asString() + '"');
-
+       
         return(ei.toString());
 
       default:
@@ -582,6 +575,14 @@ public class ConflictTracker extends ListenerAdapter {
       if (executedInsn instanceof WriteInstruction) {
         String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
          
+       // Check if we have an update to isManualTransaction to update manual field
+       if (varId.contains("isManualTransaction")) {
+               byte type = getType(ti, executedInsn);
+               String value = getValue(ti, executedInsn, type);
+            
+               manual = (value.equals("true"))?true:false;
+       }
+ 
         for (String var : conflictSet) {
           if (varId.contains(var)) {
             // Get variable info
@@ -593,9 +594,6 @@ public class ConflictTracker extends ListenerAdapter {
             if (writer == null)
               return;
             
-            //if (getWriter(ti.getStack(), manualSet) != null)
-            //  manual = true;
-            
             // Update the current updates
             writeWriterAndValue(writer, var, value);
           }