X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FConflictTracker.java;h=8b4e28486c6bb972e14ba9834db430cb3c6b10ef;hp=3621a49ac3598589be39941c1107a27b20a919c2;hb=f5ce0dc8b32aad58a543397deada4febfccf9c87;hpb=70f667e8578c5c07681ab1c95485fd34ea4f2ea9

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 3621a49..8b4e284 100644
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -37,7 +37,6 @@ import java.util.*;
  **/
 
 public class ConflictTracker extends ListenerAdapter {
-
   private final PrintWriter out;
   private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
   private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
@@ -89,226 +88,308 @@ public class ConflictTracker extends ListenerAdapter {
   }
 
   boolean propagateTheChange(Node currentNode) {
-	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 edge
-      		boolean isChanged = updateEdge(currentNode, nodeToProcess);
-
-      		// Check for a conflict in this transition(currentNode -> nodeToProcess)
-      		if (checkForConflict(nodeToProcess))
-       			return true;
+    HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
+    boolean isChanged = false;
+
+    for (Node node : currentNode.getSuccessors()) {
+      isChanged = false;
+      isChanged = updateTheOutSet(currentNode, node);
+      if (isChanged)
+        changed.add(node);
+    }
 
-      		// Checking if the out set has changed or not(Add its successors to the change list!)
-      		if (isChanged) {
-			propagateTheChange(nodeToProcess);
-      		}
+    while(!changed.isEmpty()) {
+      // Get the first element of the changed set and remove it
+      Node nodeToProcess = changed.iterator().next();
+      changed.remove(nodeToProcess);
+
+      // Update all the successors of the node
+      for (Node node : nodeToProcess.getSuccessors()) {
+	isChanged = false;
+      	isChanged = updateTheOutSet(nodeToProcess, node);
+	if (isChanged) {
+          changed.add(node);
+          if (checkAllSuccForConflict(node))
+            return true;
+	}
       }
-
-      return false;
+    }
+    return false;
   }
 
   String createErrorMessage(NameValuePair pair, HashMap<String, String> valueMap, HashMap<String, Integer> writerMap) {
-	String message = "Conflict found between the two apps. App"+pair.getAppNum()+
-			 " has written the value: "+pair.getValue()+
-			 " to the variable: "+pair.getVarName()+" while App"+
-			 writerMap.get(pair.getVarName())+" is overwriting the value: "
-			 +valueMap.get(pair.getVarName())+" to the same variable!";
-	System.out.println(message);	
-	return message;
+    String message = "Conflict found between the two apps. App"+pair.getAppNum()+
+		     " has written the value: "+pair.getValue()+
+		     " to the variable: "+pair.getVarName()+" while App"
+		     +writerMap.get(pair.getVarName())+" is overwriting the value: "
+		     +valueMap.get(pair.getVarName())+" to the same variable!";
+    System.out.println(message);	
+    return message;
   }
 
-  boolean checkForConflict(Node nodeToProcess) {
-	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
-
-	// Update the valueMap
-	for (int i = 0;i < nodeToProcess.getSetSet().size();i++) {
-		NameValuePair nameValuePair = nodeToProcess.getSetSet().get(i);
-
-		if (valueMap.containsKey(nameValuePair.getVarName())) {
-			// Check if we have a same writer
-			if (!writerMap.get(nameValuePair.getVarName()).equals(nameValuePair.getAppNum())) {
-				// Check if we have a conflict or not
-				if (!valueMap.get(nameValuePair.getVarName()).equals(nameValuePair.getValue())) {
-					errorMessage = createErrorMessage(nameValuePair, valueMap, writerMap);
-					return true;
-				} else { // We have two writers writing the same value
-					writerMap.put(nameValuePair.getVarName(), 3); // 3 represents both apps
-				}	
-			} else {
-				// Check if we have more than one value with the same writer
-				if (!valueMap.get(nameValuePair.getVarName()).equals(nameValuePair.getValue())) {
-					valueMap.put(nameValuePair.getVarName(), "twoValue"); // We have one writer writing more than one value in a same event
-				}
-			}	
-		} else {
-			valueMap.put(nameValuePair.getVarName(), nameValuePair.getValue());
-			writerMap.put(nameValuePair.getVarName(), nameValuePair.getAppNum());
-		}
-	}
+  boolean checkAllSuccForConflict(Node currentNode) {
+    for (Node node : currentNode.getSuccessors()) {
+      HashMap<Transition, ArrayList<NameValuePair>> setSets = currentNode.getOutgoingEdges().get(node).getSetSetMap();
+      for (Map.Entry mapElement : setSets.entrySet()) {
+        Transition transition = (Transition)mapElement.getKey();
+	if (checkForConflict(currentNode, node, transition))
+	  return true;
+      }
+    }
+    return false;
+  }
 
-	// Comparing the outSet to setSet
-	for (NameValuePair i : nodeToProcess.getOutSet()) {
-		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 = createErrorMessage(i, valueMap, writerMap);
-					return true;
-				}
-			}
-		}
+  boolean checkForConflict(Node parentNode, Node currentNode, Transition currentTransition) {
+    ArrayList<NameValuePair> setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap().get(currentTransition);
+    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
+    HashMap<String, String> firstValueMap = new HashMap<String, String>(); // HashMap from varName to value - first instruction in transition
+    HashMap<String, Integer> firstWriterMap = new HashMap<String, Integer>(); // HashMap from varName to appNum - first instruction in transition
+	
+    // Update the valueMap and writerMap + check for conflict between the elements of setSet
+    for (int i = 0;i < setSet.size();i++) {
+      NameValuePair nameValuePair = setSet.get(i);
+      String varName = nameValuePair.getVarName();
+      String value = nameValuePair.getValue();
+      Integer appNum = nameValuePair.getAppNum();
+      Boolean isManual = nameValuePair.getIsManual();
+
+      if (valueMap.containsKey(varName)) {
+        // Check if we have a same writer
+	if (!writerMap.get(varName).equals(appNum)) {
+	  // Check if we have a conflict or not
+	  if (!valueMap.get(varName).equals(value)) {
+	    errorMessage = createErrorMessage(nameValuePair, valueMap, writerMap);
+	    return true;
+	  }
+	}
+	valueMap.put(varName, value);
+	writerMap.put(varName, appNum);
+      } else {
+        valueMap.put(varName, value);
+	writerMap.put(varName, appNum);
+	if (!isManual) {
+	  firstValueMap.put(varName, value);
+	  firstWriterMap.put(varName, appNum);
 	}
+      }
+    }
 
-	return false;
+    // Check for conflict between outSet and this transition setSet
+    for (NameValuePair i : parentNode.getOutSet()) {
+      if (firstValueMap.containsKey(i.getVarName())) {
+        String value = firstValueMap.get(i.getVarName());
+        Integer writer = firstWriterMap.get(i.getVarName());
+        if ((value != null)&&(writer != null)) {
+          if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { 
+	    // We have different values and different writers
+	    errorMessage = createErrorMessage(i, firstValueMap, firstWriterMap);
+	    return true;
+	  }
+        }
+      }
+    }
+    return false;
   }
 
-  boolean updateEdge(Node parentNode, Node currentNode) {
-	ArrayList<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
-	HashSet<String> updatedVarNames = new HashSet<String>();
-	boolean isChanged = false;
-	
-	if (setSet != null) {
-		for (int i = 0;i < setSet.size();i++) {
-			updatedVarNames.add(setSet.get(i).getVarName());
-		}
-	}
+  boolean updateTheOutSet(Node parentNode, Node currentNode) {
+    HashMap<Transition, ArrayList<NameValuePair>> setSets = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap();
+    HashSet<String> updatedVarNames = new HashSet<String>();
+    Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+    HashMap<String, Integer> lastWriter = currentEdge.getLastWriter();
+    HashMap<String, String> lastValue = currentEdge.getLastValue();
+    HashMap<String, Integer> outSetVarMap = new HashMap<String, Integer>();
+    boolean isChanged = false;
+
+    for (Map.Entry mapElement : setSets.entrySet()) {
+      ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
+  
+      for (int i = 0;i < setSet.size();i++) {
+        updatedVarNames.add(setSet.get(i).getVarName());
+      }
+    }
+
+    for (NameValuePair i : parentNode.getOutSet()) {
+      outSetVarMap.put(i.getVarName(), i.getAppNum());
+      if (!updatedVarNames.contains(i.getVarName()))
+        isChanged |= currentNode.getOutSet().add(i);
+    }
 
-	for (NameValuePair i : parentNode.getOutSet()) {
-		if (!updatedVarNames.contains(i.getVarName()))
-			isChanged |= currentNode.getOutSet().add(i);
-	}
 
-	if (setSet != null) {
-		for (int i = 0;i < setSet.size();i++) {
-			isChanged |= currentNode.getOutSet().add(setSet.get(i));
-		}
+    for (Map.Entry mapElement : setSets.entrySet()) {
+      ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
+  
+      for (int i = 0;i < setSet.size();i++) {
+        String varName = setSet.get(i).getVarName();
+	Integer writer = lastWriter.get(varName);
+	String value = lastValue.get(varName);
+
+	if (setSet.get(i).getAppNum().equals(writer) 
+	  && setSet.get(i).getValue().equals(value)) {
+	  if (outSetVarMap.containsKey(varName)) {
+	    Integer hashCode = outSetVarMap.get(varName).hashCode() * 31 +
+	                       varName.hashCode();
+	    currentNode.getOutSet().remove(hashCode);
+	  }
+          isChanged |= currentNode.getOutSet().add(setSet.get(i));
 	}
+      }
+    }
+    return isChanged;
+  }
+
+  void updateTheEdge(Node currentNode, Transition transition) {
+    if (parentNode.getOutgoingEdges().containsKey(currentNode)) {
+      Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+        if (currentEdge.getSetSetMap().containsKey(transition)) { // Update the transition
+	  if (manual)
+	    currentEdge.getSetSetMap().put(transition, tempSetSet);
+	  else
+	    currentEdge.getSetSetMap().get(transition).addAll(tempSetSet);
+	} else { // Add a new transition
+	    currentEdge.getSetSetMap().put(transition, tempSetSet);
+        }
+    } else {
+      parentNode.getOutgoingEdges().put(currentNode, new Edge(parentNode, currentNode));
+      Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+      currentEdge.getSetSetMap().put(transition, tempSetSet);
+    }
 
-	return isChanged;
+    // Update the last writer and last value for this edge for each varName
+    Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+    ArrayList<NameValuePair> setSet = currentEdge.getSetSetMap().get(transition);
+    for (int i = 0;i < setSet.size();i++) {
+      NameValuePair nameValuePair = setSet.get(i);
+      currentEdge.getLastWriter().put(nameValuePair.getVarName(), nameValuePair.getAppNum());
+      currentEdge.getLastValue().put(nameValuePair.getVarName(), nameValuePair.getValue());
+    }
   }
 
+  
+
   static class Node {
-        Integer id;
-	HashSet<Node> predecessors = new HashSet<Node>();
-	HashSet<Node> successors = new HashSet<Node>();
-	HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
-	HashMap<Node, ArrayList<NameValuePair>> setSetMap = new HashMap<Node, ArrayList<NameValuePair>>();
-	ArrayList<NameValuePair> setSet = new ArrayList<NameValuePair>();
+    Integer id;
+    HashSet<Node> predecessors = new HashSet<Node>();
+    HashSet<Node> successors = new HashSet<Node>();
+    HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
+    HashMap<Node, Edge> outgoingEdges = new HashMap<Node, Edge>();
+
+    Node(Integer id) {
+      this.id = id;
+    }
 
+    Integer getId() {
+      return id;
+    }
 
-	Node(Integer id) {
-	  this.id = id;
-	}
+    HashSet<Node> getPredecessors() {
+      return predecessors;
+    }
 
-	void addPredecessor(Node node) {
-	  predecessors.add(node);
-	}
+    HashSet<Node> getSuccessors() {
+      return successors;
+    }
 
-	void addSuccessor(Node node) {
-	  successors.add(node);
-	}
+    HashSet<NameValuePair> getOutSet() {
+      return outSet;
+    }
 
-	void setSetSet(ArrayList<NameValuePair> setSet, boolean isManual) {
-	  if (isManual)
-	    this.setSet = new ArrayList<NameValuePair>();
+    HashMap<Node, Edge> getOutgoingEdges() {
+      return outgoingEdges;
+    }
+  }
 
-	  for (int i = 0;i < setSet.size();i++) {
-	    this.setSet.add(new NameValuePair(setSet.get(i).getAppNum(), setSet.get(i).getValue(), 
-					      setSet.get(i).getVarName(), setSet.get(i).getIsManual()));
-	    }
-	}
+  static class Edge {
+    Node source, destination;
+    HashMap<String, Integer> lastWriter = new HashMap<String, Integer>();
+    HashMap<String, String> lastValue = new HashMap<String, String>();
+    HashMap<Transition, ArrayList<NameValuePair>> setSetMap = new HashMap<Transition, ArrayList<NameValuePair>>();
 
-	Integer getId() {
-		return id;
-	}
+    Edge(Node source, Node destination) {
+      this.source = source;
+      this.destination = destination;
+    }
 
-	HashSet<Node> getPredecessors() {
-		return predecessors;
-	}
+    Node getSource() {
+      return source;
+    }
 
-	HashSet<Node> getSuccessors() {
-		return successors;
-	}
+    Node getDestination() {
+      return destination;
+    }
 
-	ArrayList<NameValuePair> getSetSet() {
-		return setSet;
-	}
+    HashMap<Transition, ArrayList<NameValuePair>> getSetSetMap() {
+      return setSetMap;
+    }
 
-	HashSet<NameValuePair> getOutSet() {
-		return outSet;
-	}
+    HashMap<String, Integer> getLastWriter() {
+      return lastWriter;
+    }
 
-	HashMap<Node, ArrayList<NameValuePair>> getSetSetMap() {
-		return setSetMap;
-	}
+    HashMap<String, String> getLastValue() {
+      return lastValue;
+    }
   }
 
   static class NameValuePair {
-	Integer appNum;
-	String value;
-	String varName;
-	boolean isManual;
-
-	NameValuePair(Integer appNum, String value, String varName, boolean isManual) {
-      		this.appNum = appNum;
-      		this.value = value;
-      		this.varName = varName;
-      		this.isManual = isManual;
-	}
+    Integer appNum;
+    String value;
+    String varName;
+    boolean isManual;
+
+    NameValuePair(Integer appNum, String value, String varName, boolean isManual) {
+      this.appNum = appNum;
+      this.value = value;
+      this.varName = varName;
+      this.isManual = isManual;
+    }
 
-	void setAppNum(Integer appNum) {
-		this.appNum = appNum;
-	}
+    void setAppNum(Integer appNum) {
+      this.appNum = appNum;
+    }
 
-	void setValue(String value) {
-		this.value = value;
-	}
+    void setValue(String value) {
+      this.value = value;
+    }
 
-	void setVarName(String varName) {
-		this.varName = varName;
-	}
+    void setVarName(String varName) {
+      this.varName = varName;
+    }
 
     void setIsManual(String varName) {
-		this.isManual = isManual;
-	}
+      this.isManual = isManual;
+    }
 
-	Integer getAppNum() {
-		return appNum;
-	}
+    Integer getAppNum() {
+      return appNum;
+    }
 
-	String getValue() {
-		return value;
-	}
+    String getValue() {
+      return value;
+    }
 
-	String getVarName() {
-		return varName;
-	}
+    String getVarName() {
+      return varName;
+    }
 
-	boolean getIsManual() {
-		return isManual;
-	}
+    boolean getIsManual() {
+      return isManual;
+    }
 
-	@Override
-	public boolean equals(Object o) {
+    @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;
-	}
+    }
 
-	@Override
-	public int hashCode() {
-		return appNum.hashCode() * 31 + varName.hashCode();
-	}
+    @Override
+    public int hashCode() {
+      return appNum.hashCode() * 31 + varName.hashCode();
+    }
   }
 
   @Override
@@ -320,11 +401,16 @@ public class ConflictTracker extends ListenerAdapter {
 
     out.println("The state is restored to state with id: "+id+", depth: "+depth);
   
+    if (id == 24 && depth == 5) {
+	    System.out.println("*****************************************");
+    	    System.out.println("*****************************************");
+	    System.out.println("*****************************************");
+    }
     // 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);
     }
   }
 
@@ -337,21 +423,27 @@ public class ConflictTracker extends ListenerAdapter {
   @Override
   public void stateAdvanced(Search search) {
     String theEnd = null;
+    Transition transition = search.getTransition();
     id = search.getStateId();
     depth = search.getDepth();
     operation = "forward";
 
     // Add the node to the list of nodes
     if (nodes.get(id) == null)
-	nodes.put(id, new Node(id));
+      nodes.put(id, new Node(id));
 
     Node currentNode = nodes.get(id);
 
-    // Update the setSet for this new node
-    currentNode.setSetSet(tempSetSet, manual);
-    tempSetSet = new ArrayList<NameValuePair>(); 
+    // Update the edge based on the current transition
+    updateTheEdge(currentNode, transition);
+
+    // Reset the temporary variables and flags
+    tempSetSet = new ArrayList<NameValuePair>();
     manual = false;
 
+    // Check for the conflict in this transition
+    conflictFound = checkForConflict(parentNode, currentNode, transition);
+
     if (search.isNewState()) {
       detail = "new";
     } else {
@@ -368,34 +460,32 @@ public class ConflictTracker extends ListenerAdapter {
     // Updating the predecessors for this node
     // Check if parent node is already in successors of the current node or not
     if (!(currentNode.getPredecessors().contains(parentNode)))
-	currentNode.addPredecessor(parentNode);
+      currentNode.getPredecessors().add(parentNode);
 
     // Update the successors for this node
     // Check if current node is already in successors of the parent node or not
     if (!(parentNode.getSuccessors().contains(currentNode)))
-        parentNode.addSuccessor(currentNode);
-
+      parentNode.getSuccessors().add(currentNode);
 
-    // Update the setSetMap of the current node
-    for (Node i : currentNode.getPredecessors()) {
-	currentNode.getSetSetMap().put(i, i.getSetSet());
-    }
+    // Update the outset of the current node and check if it is changed or not to propagate the change
+    boolean isChanged = updateTheOutSet(parentNode, currentNode);
 
-    // Update the edge and check if the outset of the current node is changed or not to propagate the change
-    boolean isChanged = updateEdge(parentNode, currentNode);
 
-    // Check for the conflict in this edge
-    conflictFound = checkForConflict(currentNode);
-    
+    System.out.println("######################### The outset is:");
+    for (NameValuePair nvp : currentNode.getOutSet()) {
+	System.out.println("writer: "+nvp.getAppNum());
+	System.out.println("value: "+nvp.getValue());
+	System.out.println("var : "+nvp.getVarName());
+    }	    
     // Check if the outSet of this state has changed, update all of its successors' sets if any
     if (isChanged)
-	conflictFound = conflictFound || propagateTheChange(currentNode);
-
+      conflictFound = conflictFound || checkAllSuccForConflict(currentNode) || propagateTheChange(currentNode);
+    
     // 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);
     }
   }
 
@@ -408,11 +498,17 @@ public class ConflictTracker extends ListenerAdapter {
 
     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 
+    if (id == 24 && depth == 5) {
+            System.out.println("*****************************************");
+            System.out.println("*****************************************");
+            System.out.println("*****************************************");
+    }
+
     // 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);
     }
   }
 
@@ -559,7 +655,7 @@ public class ConflictTracker extends ListenerAdapter {
     // Update the temporary Set set.
     NameValuePair temp = new NameValuePair(1, value, var, manual);
     if (writer.equals("App2"))
-    	temp = new NameValuePair(2, value, var, manual);
+      temp = new NameValuePair(2, value, var, manual);
     
     tempSetSet.add(temp);
   }
@@ -585,7 +681,7 @@ public class ConflictTracker extends ListenerAdapter {
         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) {
+            executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) {
           byte type  = getType(ti, executedInsn);
           String value = getValue(ti, executedInsn, type);
 
@@ -612,7 +708,10 @@ public class ConflictTracker extends ListenerAdapter {
 
               if (getWriter(ti.getStack(), manualSet) != null)
                 manual = true;
-
+	      
+	      System.out.println("############################## writer: "+writer);
+	      System.out.println("############################## value: "+value);
+	      System.out.println("############################## var: "+var);
               // Update the temporary Set set.
               writeWriterAndValue(writer, value, var);
             }