Detecting location mode read/write using the old method.
authorrtrimana <rtrimana@uci.edu>
Fri, 18 Oct 2019 20:22:29 +0000 (13:22 -0700)
committerrtrimana <rtrimana@uci.edu>
Fri, 18 Oct 2019 20:22:29 +0000 (13:22 -0700)
src/main/gov/nasa/jpf/listener/ConflictTracker.java

index 51e34fc..db47836 100644 (file)
@@ -55,7 +55,9 @@ public class ConflictTracker extends ListenerAdapter {
   private boolean conflictFound = false;
   private boolean isSet = false;
   private boolean manual = false;
+
+  private final String SET_LOCATION_METHOD = "setLocationMode";
+  private final String LOCATION_VAR = "locationMode";
   
   public ConflictTracker(Config config, JPF jpf) {
     out = new PrintWriter(System.out, true);
@@ -91,24 +93,24 @@ public class ConflictTracker extends ListenerAdapter {
        HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
 
        while(!changed.isEmpty()) {
-               // Get the first element of HashSet and remove it from the changed set
-               Node nodeToProcess = changed.iterator().next();
-               changed.remove(nodeToProcess);
-                       
-               // Update the sets, store the outSet to temp before its changes
-               boolean isChanged = updateSets(nodeToProcess);
-
-               // Check for a conflict
-               if (checkForConflict(nodeToProcess))
-                       return true;
-                       
-               // Checking if the out set has changed or not(Add its successors to the change list!)
-               if (isChanged) {
-                       for (Node i : nodeToProcess.getSuccessors()) {
-                               if (!changed.contains(i))
-                                       changed.add(i);
-                       }
-               }
+      // Get the first element of HashSet and remove it from the changed set
+      Node nodeToProcess = changed.iterator().next();
+      changed.remove(nodeToProcess);
+
+      // Update the sets, store the outSet to temp before its changes
+      boolean isChanged = updateSets(nodeToProcess);
+
+      // Check for a conflict
+      if (checkForConflict(nodeToProcess))
+        return true;
+
+      // Checking if the out set has changed or not(Add its successors to the change list!)
+      if (isChanged) {
+        for (Node i : nodeToProcess.getSuccessors()) {
+          if (!changed.contains(i))
+            changed.add(i);
+        }
+      }
        }
 
        return false;
@@ -119,9 +121,9 @@ public class ConflictTracker extends ListenerAdapter {
 
        // Update based on setSet
        for (NameValuePair i : currentNode.getSetSet()) {
-               if (currentNode.getOutSet().contains(i))
-                       currentNode.getOutSet().remove(i);      
-               currentNode.getOutSet().add(i);
+      if (currentNode.getOutSet().contains(i))
+        currentNode.getOutSet().remove(i);
+      currentNode.getOutSet().add(i);
        }
 
        // Add all the inSet
@@ -129,15 +131,15 @@ public class ConflictTracker extends ListenerAdapter {
 
        // Check if the outSet is changed
        if (!prevSize.equals(currentNode.getOutSet().size()))
-               return true;
+      return true;
        
        return false;
   }
 
   void setInSet(Node currentNode) {
        for (Node i : currentNode.getPredecessors()) {
-               currentNode.getInSet().addAll(i.getOutSet());
-       }
+      currentNode.getInSet().addAll(i.getOutSet());
+    }
   }
 
   boolean checkForConflict(Node currentNode) {
@@ -145,30 +147,30 @@ public class ConflictTracker extends ListenerAdapter {
        HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); // HashMap from varName to appNum
 
        for (NameValuePair i : currentNode.getSetSet()) {
-               if (i.getIsManual()) // Manual input: we have no conflict
-                       continue;
-
-               valueMap.put(i.getVarName(), i.getValue());
-               if (writerMap.containsKey(i.getVarName()))
-                       writerMap.put(i.getVarName(), i.getAppNum()+writerMap.get(i.getVarName())); // We have two writers?
-               else
-                       writerMap.put(i.getVarName(), i.getAppNum());
+      if (i.getIsManual()) // Manual input: we have no conflict
+        continue;
+
+      valueMap.put(i.getVarName(), i.getValue());
+      if (writerMap.containsKey(i.getVarName()))
+        writerMap.put(i.getVarName(), i.getAppNum()+writerMap.get(i.getVarName())); // We have two writers?
+      else
+        writerMap.put(i.getVarName(), i.getAppNum());
        }
 
        // Comparing the inSet and setSet to find the conflict
        for (NameValuePair i : currentNode.getInSet()) {
-               if (valueMap.containsKey(i.getVarName())) {
-                       String value = valueMap.get(i.getVarName());
-                       Integer writer = writerMap.get(i.getVarName());
-                       if ((value != null)&&(writer != null)) {
-                               if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { // We have different values
-                                       errorMessage = "Conflict found between the two apps. App"+i.getAppNum()+" has written the value: "+i.getValue()+
-                                                       " to the variable: "+i.getVarName()+" while App"+writerMap.get(i.getVarName())+" is overwriting the value: "
-                                                       +valueMap.get(i.getVarName())+" to the same variable!";
-                                       return true;
-                               }
-                       }
-               }
+      if (valueMap.containsKey(i.getVarName())) {
+        String value = valueMap.get(i.getVarName());
+        Integer writer = writerMap.get(i.getVarName());
+        if ((value != null)&&(writer != null)) {
+          if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { // We have different values
+            errorMessage = "Conflict found between the two apps. App"+i.getAppNum()+" has written the value: "+i.getValue()+
+                    " to the variable: "+i.getVarName()+" while App"+writerMap.get(i.getVarName())+" is overwriting the value: "
+                    +valueMap.get(i.getVarName())+" to the same variable!";
+            return true;
+          }
+        }
+      }
        }
 
        return false;
@@ -176,10 +178,10 @@ public class ConflictTracker extends ListenerAdapter {
 
   boolean updateSets(Node currentNode) {
        // Set input set according to output set of pred states of current state
-       setInSet(currentNode);
+    setInSet(currentNode);
 
        // Set outSet according to inSet, and setSet of current node, check if there is a change
-       return setOutSet(currentNode);
+    return setOutSet(currentNode);
   }
 
   static class Node {
@@ -203,11 +205,11 @@ public class ConflictTracker extends ListenerAdapter {
        }
 
        void setSetSet(HashSet<NameValuePair> setSet, boolean isManual) {
-               if (isManual)
-                       this.setSet = new HashSet<NameValuePair>();
-               for (NameValuePair i : setSet) {
-                       this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual()));
-               }
+      if (isManual)
+        this.setSet = new HashSet<NameValuePair>();
+      for (NameValuePair i : setSet) {
+        this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual()));
+      }
        }
 
        Integer getId() {
@@ -242,10 +244,10 @@ public class ConflictTracker extends ListenerAdapter {
        boolean isManual;
 
        NameValuePair(Integer appNum, String value, String varName, boolean isManual) {
-               this.appNum = appNum;
-               this.value = value;
-               this.varName = varName;
-               this.isManual = isManual;
+      this.appNum = appNum;
+      this.value = value;
+      this.varName = varName;
+      this.isManual = isManual;
        }
 
        void setAppNum(Integer appNum) {
@@ -260,7 +262,7 @@ public class ConflictTracker extends ListenerAdapter {
                this.varName = varName;
        }
 
-        void setIsManual(String varName) {
+    void setIsManual(String varName) {
                this.isManual = isManual;
        }
 
@@ -282,12 +284,12 @@ public class ConflictTracker extends ListenerAdapter {
 
        @Override
        public boolean equals(Object o) {
-               if (o instanceof NameValuePair) {
-                       NameValuePair other = (NameValuePair) o;
-                       if (varName.equals(other.getVarName()))
-                               return appNum.equals(other.getAppNum());
-               }
-               return false;
+      if (o instanceof NameValuePair) {
+        NameValuePair other = (NameValuePair) o;
+        if (varName.equals(other.getVarName()))
+          return appNum.equals(other.getAppNum());
+      }
+      return false;
        }
 
        @Override
@@ -307,9 +309,9 @@ public class ConflictTracker extends ListenerAdapter {
   
     // Update the parent node
     if (nodes.containsKey(id)) {
-       parentNode = nodes.get(id);
+         parentNode = nodes.get(id);
     } else {
-       parentNode = new Node(id);
+         parentNode = new Node(id);
     }
   }
 
@@ -373,9 +375,9 @@ public class ConflictTracker extends ListenerAdapter {
 
     // Update the parent node
     if (nodes.containsKey(id)) {
-       parentNode = nodes.get(id);
+         parentNode = nodes.get(id);
     } else {
-       parentNode = new Node(id);
+         parentNode = new Node(id);
     }
   }
 
@@ -390,9 +392,9 @@ public class ConflictTracker extends ListenerAdapter {
 
     // Update the parent node
     if (nodes.containsKey(id)) {
-       parentNode = nodes.get(id);
+         parentNode = nodes.get(id);
     } else {
-       parentNode = new Node(id);
+         parentNode = new Node(id);
     }
   }
 
@@ -410,13 +412,13 @@ public class ConflictTracker extends ListenerAdapter {
     if ((inst instanceof JVMLocalVariableInstruction) ||
         (inst instanceof JVMFieldInstruction))
     {
-       if (frame.getTopPos() < 0)
-         return(null);
+      if (frame.getTopPos() < 0)
+        return(null);
 
-       lo = frame.peek();
-       hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
+      lo = frame.peek();
+      hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 
-       return(decodeValue(type, lo, hi));
+      return(decodeValue(type, lo, hi));
     }
 
     if (inst instanceof JVMArrayElementInstruction)
@@ -535,6 +537,16 @@ public class ConflictTracker extends ListenerAdapter {
     return null;
   }
 
+  private void writeWriterAndValue(String writer, String value, String var) {
+    // Update the temporary Set set.
+    if (writer.equals("App1"))
+      tempSetSet.add(new NameValuePair(1, value, var, manual));
+    else if (writer.equals("App2"))
+      tempSetSet.add(new NameValuePair(2, value, var, manual));
+    // Set isSet to true
+    isSet = true;
+  }
+
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     // Instantiate timeoutTimer
@@ -552,36 +564,44 @@ public class ConflictTracker extends ListenerAdapter {
       sb.append(errorMessage);
       Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
       ti.setNextPC(nextIns);
-    } else if (executedInsn instanceof WriteInstruction) {
-      String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
-      for(String var : conflictSet) {
-
-        if (varId.contains(var)) {
-          // Get variable info
+    } else {
+      if (conflictSet.contains(LOCATION_VAR)) {
+        MethodInfo mi = executedInsn.getMethodInfo();
+        // Find the last load before return and get the value here
+        if (mi.getName().equals(SET_LOCATION_METHOD) &&
+                executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) {
           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;
-
-         if (getWriter(ti.getStack(), manualSet) != null)
-               manual = true;
-
-         // Update the temporary Set set.
-         if (writer.equals("App1"))
-                 tempSetSet.add(new NameValuePair(1, value, var, manual));
-         else if (writer.equals("App2"))
-                 tempSetSet.add(new NameValuePair(2, value, var, manual));
-         // Set isSet to true
-         isSet = true;
-                 
-       }
-     }
 
-      
-  }
-  
- }
+          // Extract the writer app name
+          ClassInfo ci = mi.getClassInfo();
+          String writer = ci.getName();
 
+          // Update the temporary Set set.
+          writeWriterAndValue(writer, value, LOCATION_VAR);
+        }
+      } else {
+        if (executedInsn instanceof WriteInstruction) {
+          String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+          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;
+
+              if (getWriter(ti.getStack(), manualSet) != null)
+                manual = true;
+
+              // Update the temporary Set set.
+              writeWriterAndValue(writer, value, var);
+            }
+          }
+        }
+      }
+    }
+  }
 }