From: amiraj <amiraj.95@uci.edu>
Date: Thu, 17 Oct 2019 01:57:05 +0000 (-0700)
Subject: Make more changes to the direct-direct detection feature to detect manual overwrites... 
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=58bfe64321889f03644870cda7b72f0cd0d100fb;p=jpf-core.git

Make more changes to the direct-direct detection feature to detect manual overwrites interactions as well
---

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index fc14574..adbab19 100644
--- 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;