From: Seyed Amir Hossein Aqajari <saqajari@circinus-40.ics.uci.edu>
Date: Tue, 24 Mar 2020 22:50:03 +0000 (-0700)
Subject: Making analysis compatible with new infrastructure
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=fcfca6bc7d3d5509a9eb080b9ccaa5d3349169cf

Making analysis compatible with new infrastructure
---

diff --git a/main.jpf b/main.jpf
index 9ce7d13..e1ac21c 100644
--- a/main.jpf
+++ b/main.jpf
@@ -16,7 +16,7 @@ listener=gov.nasa.jpf.listener.ConflictTracker
 # Alarms
 #variables=currentAlarm
 # Locks
-variables=currentLock
+variables=lock
 # Thermostats
 #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode
 # Switches
diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index b426d26..cbd7e66 100644
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -52,12 +52,14 @@ public class ConflictTracker extends ListenerAdapter {
   private String operation;
   private String detail;
   private String errorMessage;
+  private String varName;
   private int depth;
   private int id;
   private boolean manual = false;
   private boolean conflictFound = false;
   private int currentEvent = -1;
   private boolean debugMode = false;
+  private int popRef = 0;
 
   private final String SET_LOCATION_METHOD = "setLocationMode";
   private final String LOCATION_VAR = "locationMode";
@@ -610,14 +612,54 @@ public class ConflictTracker extends ListenerAdapter {
         ti.setNextPC(nextIns);
       }
     }
-    
-    if (conflictFound) {
 
+    if (conflictFound) {
       StringBuilder sb = new StringBuilder();
       sb.append(errorMessage);
       Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
       ti.setNextPC(nextIns);
     } else {
+      // Check if we are ready to pop the values
+      if (popRef == 2) {
+      	byte type = getType(ti, executedInsn);
+        varName = getValue(ti, executedInsn, type);
+	String writer = getWriter(ti.getStack(), appSet);
+
+	popRef = popRef-1;
+      } else if (popRef == 1) {
+	byte type = getType(ti, executedInsn);
+	String value = getValue(ti, executedInsn, type);
+	String writer = getWriter(ti.getStack(), appSet);	
+
+	for (String var: conflictSet) {
+		if (varName.contains(var)) {
+			if (writer != null) {
+				System.out.println("################# writer: "+writer);
+				System.out.println("################# variable: "+varName);
+				System.out.println("################# value: "+value);
+				System.out.println("################# manual: "+manual);
+				writeWriterAndValue(writer, varName, value);
+			}
+		}
+	}
+
+      	popRef = popRef-1;
+      }
+
+
+      if (executedInsn.getMnemonic().equals("getfield")) {
+      	if (executedInsn.toString().contains("deviceValueSmartThing") || 
+	    executedInsn.toString().contains("deviceIntValueSmartThing")) {
+		if (executedInsn.getNext() != null) {
+			if (executedInsn.getNext().getMnemonic().contains("load")) {
+
+				if (executedInsn.getNext().getNext() != null)
+					if (executedInsn.getNext().getNext().getMnemonic().contains("load"))
+						popRef = 2;
+			}
+      		}
+	}
+      }
 
       if (executedInsn instanceof WriteInstruction) {
         String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
@@ -625,25 +667,10 @@ public class ConflictTracker extends ListenerAdapter {
         if (varId.contains("isManualTransaction")) {
           byte type = getType(ti, executedInsn);
           String value = getValue(ti, executedInsn, type);
-          System.out.println();
+
           manual = (value.equals("true"))?true:false;
         }
-        for (String var : conflictSet) {
-          if (varId.contains(var)) {
-            // Get variable info
-            byte type = getType(ti, executedInsn);
-            String value = getValue(ti, executedInsn, type);
-            String writer = getWriter(ti.getStack(), appSet);
-
-            // Just return if the writer is not one of the listed apps in the .jpf file
-            if (writer == null)
-              return;
-            
-            // Update the current updates
-            writeWriterAndValue(writer, var, value);
-          }
-        }
       }
-    }
+    }    
   }
 }