Making analysis compatible with new infrastructure

diff --git a/main.jpf b/main.jpf
index 9ce7d13f67420d97c2fba09b1fbb5144ca71c35f..e1ac21cedd88afce006dc3def74ba1d519055a91 100644 (file)
--- 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 b426d26f49d85044ddefebae2311263eb21cc361..cbd7e6642095ca7a1e24a04104543c86b2203002 100644 (file)
--- 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);
-          }
-        }
       }
-    }
+    }    
   }
 }