Make more changes to the direct-direct detection feature to detect manual overwrites...

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index fc1457492dd79bd9fe9797ac86e05d5e6eb2399f..adbab197d443a24af07bb9c58004a3b0795e241a 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -53,6 +53,7 @@ public class ConflictTracker extends ListenerAdapter {
   private int id;
   private boolean conflictFound = false;
   private boolean isSet = false;
+  private boolean manual = false;
  
   
   public ConflictTracker(Config config, JPF jpf) {
@@ -113,29 +114,25 @@ public class ConflictTracker extends ListenerAdapter {
   }
 
   boolean setOutSet(Node currentNode) {
-       boolean isChanged = false;
-       
-       // Update based on inSet
-       for (NameValuePair i : currentNode.getInSet()) {
-               if (!currentNode.getOutSet().contains(i)) {
-                       isChanged = true;
-                       currentNode.getOutSet().add(i);
-               }
-       }
+       Integer prevSize = currentNode.getOutSet().size();
 
-       // Overwrite based on setSet
+       // Update based on setSet
        for (NameValuePair i : currentNode.getSetSet()) {
-               if (!currentNode.getOutSet().contains(i))
-                       isChanged = true;
-               else
-                       currentNode.getOutSet().remove(i);
+               if (currentNode.getOutSet().contains(i))
+                       currentNode.getOutSet().remove(i);      
                currentNode.getOutSet().add(i);
        }
 
-       return isChanged;
+       // Add all the inSet
+       currentNode.getOutSet().addAll(currentNode.getInSet());
+
+       // Check if the outSet is changed
+       if (!prevSize.equals(currentNode.getOutSet().size()))
+               return true;
+       
+       return false;
   }
 
-  //Is it ok to point to the same object? (Not passed by value?)
   void setInSet(Node currentNode) {
        for (Node i : currentNode.getPredecessors()) {
                currentNode.getInSet().addAll(i.getOutSet());
@@ -143,17 +140,26 @@ public class ConflictTracker extends ListenerAdapter {
   }
 
   boolean checkForConflict(Node currentNode) {
-       HashMap<String, String> valueMap = new HashMap<String, String>();
-       HashMap<String, Boolean> isManualMap = new HashMap<String, Boolean>();
+       HashMap<String, String> valueMap = new HashMap<String, String>(); // HashMap from varName to value
+       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
+                       return false;
 
-       for (NameValuePair i : currentNode.getOutSet()) {
+               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())) {
-                       if (!(isManualMap.get(i.getVarName())&&(i.getIsManual())))
-                               if (!(valueMap.get(i.getVarName()).equals(i.getValue())))
+                       if (!(valueMap.get(i.getVarName()).equals(i.getValue())))
+                               if (!(writerMap.get(i.getVarName()).equals(i.getAppNum())))
                                        return true;
-               } else {
-                       valueMap.put(i.getVarName(), i.getValue());
-                       isManualMap.put(i.getVarName(), i.getIsManual());
                }
        }
 
@@ -188,7 +194,9 @@ public class ConflictTracker extends ListenerAdapter {
                successors.add(node);
        }
 
-       void setSetSet(HashSet<NameValuePair> setSet) {
+       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()));
                }
@@ -316,9 +324,10 @@ public class ConflictTracker extends ListenerAdapter {
 
     // Update the setSet for this new node
     if (isSet) {
-      currentNode.setSetSet(tempSetSet);
+      currentNode.setSetSet(tempSetSet, manual);
       tempSetSet = new HashSet<NameValuePair>(); 
       isSet = false;
+      manual = false;
     }
 
     if (search.isNewState()) {
@@ -544,19 +553,18 @@ public class ConflictTracker extends ListenerAdapter {
           byte type  = getType(ti, executedInsn);
           String value = getValue(ti, executedInsn, type);
           String writer = getWriter(ti.getStack(), appSet);
-         boolean isManual = false;
           // 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)
-               isManual = true;
+               manual = true;
 
          // Update the temporary Set set.
          if (writer.equals("App1"))
-                 tempSetSet.add(new NameValuePair(1, value, var, isManual));
+                 tempSetSet.add(new NameValuePair(1, value, var, manual));
          else if (writer.equals("App2"))
-                 tempSetSet.add(new NameValuePair(2, value, var, isManual));
+                 tempSetSet.add(new NameValuePair(2, value, var, manual));
          // Set isSet to true
          isSet = true;