From: Seyed Amir Hossein Aqajari <saqajari@circinus-38.ics.uci.edu>
Date: Wed, 19 Feb 2020 19:21:38 +0000 (-0800)
Subject: Adding manual transactions to the conflict tracker
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=db2278abd14ee92e122b215c89a1f54bda6c30b1

Adding manual transactions to the conflict tracker
---

diff --git a/main.jpf b/main.jpf
index cfef551..efa82cc 100644
--- 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 fd73117..b05c9f3 100644
--- 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);
           }