From 1f48a88d122e21abf57ead759c19ee2cb9ddff3d Mon Sep 17 00:00:00 2001 From: Seyed Amir Hossein Aqajari Date: Thu, 5 Dec 2019 15:40:05 -0800 Subject: [PATCH] Fixing bugs in Conflict Tracker --- .../nasa/jpf/listener/ConflictTracker.java | 551 +++++++++--------- 1 file changed, 273 insertions(+), 278 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index 1f2fa7d..af9147b 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -88,329 +88,324 @@ public class ConflictTracker extends ListenerAdapter { } boolean propagateTheChange(Node currentNode) { - HashSet changed = new HashSet(currentNode.getSuccessors()); - HashMap> parentQueueMap = new HashMap>(); - HashSet parents = new HashSet(); - parents.add(currentNode); + HashSet changed = new HashSet(currentNode.getSuccessors()); + HashMap> parentQueueMap = new HashMap>(); + HashSet parents = new HashSet(); + parents.add(currentNode); - for (Node node : currentNode.getSuccessors()) { - parentQueueMap.put(node, parents); - } + for (Node node : currentNode.getSuccessors()) { + parentQueueMap.put(node, parents); + } + + while(!changed.isEmpty()) { + // Get the first element of the changed set and remove it + Node nodeToProcess = changed.iterator().next(); + changed.remove(nodeToProcess); - while(!changed.isEmpty()) { - // Get the first element of the changed set and remove it - Node nodeToProcess = changed.iterator().next(); - changed.remove(nodeToProcess); - - // Update the changed parents - parents.clear(); - parents = parentQueueMap.get(nodeToProcess); - boolean isChanged = false; - - for (Node node : parents) { - // Update the edge - isChanged |= updateTheOutSet(node, nodeToProcess); - } - - // Check for a conflict if the outSet of nodeToProcess is changed - if (isChanged) { - for (Node node : nodeToProcess.getSuccessors()) { - HashMap> setSets = nodeToProcess.getOutgoingEdges().get(node).getSetSetMap(); - for (Map.Entry mapElement : setSets.entrySet()) { - Transition transition = (Transition)mapElement.getKey(); - if (checkForConflict(nodeToProcess, node, transition)) - return true; - } - } - } - - // Update the parents list for the successors of the current node - parents.clear(); - parents.add(nodeToProcess); - - // 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); - - // Update the list of updated parents for the current node - if (parentQueueMap.containsKey(i)) - parentQueueMap.get(i).add(nodeToProcess); - else - parentQueueMap.put(i, parents); - } - } + // Update the changed parents + parents.clear(); + parents = parentQueueMap.get(nodeToProcess); + boolean isChanged = false; + + for (Node node : parents) { + // Update the edge + isChanged |= updateTheOutSet(node, nodeToProcess); } - return false; + // Check for a conflict if the outSet of nodeToProcess is changed + if (isChanged) { + for (Node node : nodeToProcess.getSuccessors()) { + HashMap> setSets = nodeToProcess.getOutgoingEdges().get(node).getSetSetMap(); + for (Map.Entry mapElement : setSets.entrySet()) { + Transition transition = (Transition)mapElement.getKey(); + if (checkForConflict(nodeToProcess, node, transition)) + return true; + } + } + } + + // Update the parents list for the successors of the current node + parents.clear(); + parents.add(nodeToProcess); + + // 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); + + // Update the list of updated parents for the current node + if (parentQueueMap.containsKey(i)) + parentQueueMap.get(i).add(nodeToProcess); + else + parentQueueMap.put(i, parents); + } + } + } + return false; } String createErrorMessage(NameValuePair pair, HashMap valueMap, HashMap 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 parentNode, Node currentNode, Transition currentTransition) { - ArrayList setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap().get(currentTransition); - HashMap valueMap = new HashMap(); // HashMap from varName to value - HashMap writerMap = new HashMap(); // HashMap from varName to appNum - HashMap firstValueMap = new HashMap(); // HashMap from varName to value - first instruction in transition - HashMap firstWriterMap = new HashMap(); // HashMap from varName to appNum - first instruction in transition + ArrayList setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap().get(currentTransition); + HashMap valueMap = new HashMap(); // HashMap from varName to value + HashMap writerMap = new HashMap(); // HashMap from varName to appNum + HashMap firstValueMap = new HashMap(); // HashMap from varName to value - first instruction in transition + HashMap firstWriterMap = new HashMap(); // 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); - } - } + // 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); } + } + } - // Check for conflict between outSet and this transition setSet - for (NameValuePair i : parentNode.getOutSet()) { - if (valueMap.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; + // Check for conflict between outSet and this transition setSet + for (NameValuePair i : parentNode.getOutSet()) { + if (valueMap.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 updateTheOutSet(Node parentNode, Node currentNode) { - HashMap> setSets = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap(); - HashSet updatedVarNames = new HashSet(); - Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode); - HashMap lastWriter = currentEdge.getLastWriter(); - HashMap lastValue = currentEdge.getLastValue(); - HashMap outSetVarMap = new HashMap(); - boolean isChanged = false; - - for (Map.Entry mapElement : setSets.entrySet()) { - ArrayList setSet = (ArrayList)mapElement.getValue(); + HashMap> setSets = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap(); + HashSet updatedVarNames = new HashSet(); + Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode); + HashMap lastWriter = currentEdge.getLastWriter(); + HashMap lastValue = currentEdge.getLastValue(); + HashMap outSetVarMap = new HashMap(); + boolean isChanged = false; + + for (Map.Entry mapElement : setSets.entrySet()) { + ArrayList setSet = (ArrayList)mapElement.getValue(); - for (int i = 0;i < setSet.size();i++) { - updatedVarNames.add(setSet.get(i).getVarName()); - } - } - + 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()) { + outSetVarMap.put(i.getVarName(), i.getAppNum()); + if (!updatedVarNames.contains(i.getVarName())) + isChanged |= currentNode.getOutSet().add(i); + } - for (Map.Entry mapElement : setSets.entrySet()) { - ArrayList setSet = (ArrayList)mapElement.getValue(); + for (Map.Entry mapElement : setSets.entrySet()) { + ArrayList setSet = (ArrayList)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; + 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); + 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); + } - // Update the last writer and last value for this edge for each varName - Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode); - ArrayList 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()); - } + // Update the last writer and last value for this edge for each varName + Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode); + ArrayList 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 predecessors = new HashSet(); - HashSet successors = new HashSet(); - HashSet outSet = new HashSet(); - HashMap outgoingEdges = new HashMap(); - - Node(Integer id) { - this.id = id; - } + Integer id; + HashSet predecessors = new HashSet(); + HashSet successors = new HashSet(); + HashSet outSet = new HashSet(); + HashMap outgoingEdges = new HashMap(); + + Node(Integer id) { + this.id = id; + } - Integer getId() { - return id; - } + Integer getId() { + return id; + } - HashSet getPredecessors() { - return predecessors; - } + HashSet getPredecessors() { + return predecessors; + } - HashSet getSuccessors() { - return successors; - } + HashSet getSuccessors() { + return successors; + } - HashSet getOutSet() { - return outSet; - } + HashSet getOutSet() { + return outSet; + } - HashMap getOutgoingEdges() { - return outgoingEdges; - } + HashMap getOutgoingEdges() { + return outgoingEdges; + } } static class Edge { - Node source, destination; - HashMap lastWriter = new HashMap(); - HashMap lastValue = new HashMap(); - HashMap> setSetMap = new HashMap>(); - - Edge(Node source, Node destination) { - this.source = source; - this.destination = destination; - } + Node source, destination; + HashMap lastWriter = new HashMap(); + HashMap lastValue = new HashMap(); + HashMap> setSetMap = new HashMap>(); + + Edge(Node source, Node destination) { + this.source = source; + this.destination = destination; + } - Node getSource() { - return source; - } + Node getSource() { + return source; + } - Node getDestination() { - return destination; - } + Node getDestination() { + return destination; + } - HashMap> getSetSetMap() { - return setSetMap; - } + HashMap> getSetSetMap() { + return setSetMap; + } - HashMap getLastWriter() { - return lastWriter; - } + HashMap getLastWriter() { + return lastWriter; + } - HashMap getLastValue() { - return lastValue; - } + HashMap 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; - } + void setIsManual(String varName) { + 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 @@ -424,9 +419,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); } } @@ -446,7 +441,7 @@ public class ConflictTracker extends ListenerAdapter { // 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); @@ -476,32 +471,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.getPredecessors().add(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.getSuccessors().add(currentNode); + parentNode.getSuccessors().add(currentNode); // Update the outset of the current node and check if it is changed or not to propagate the change boolean isChanged = updateTheOutSet(parentNode, currentNode); // Check if the outSet of this state has changed, update all of its successors' sets if any if (isChanged) { - for (Node node : currentNode.getSuccessors()) { - HashMap> setSets = currentNode.getOutgoingEdges().get(node).getSetSetMap(); - for (Map.Entry mapElement : setSets.entrySet()) { - Transition currentTransition = (Transition)mapElement.getKey(); - conflictFound = conflictFound || checkForConflict(currentNode, node, currentTransition); - } + for (Node node : currentNode.getSuccessors()) { + HashMap> setSets = currentNode.getOutgoingEdges().get(node).getSetSetMap(); + for (Map.Entry mapElement : setSets.entrySet()) { + Transition currentTransition = (Transition)mapElement.getKey(); + conflictFound = conflictFound || checkForConflict(currentNode, node, currentTransition); } - conflictFound = conflictFound || propagateTheChange(currentNode); + } + conflictFound = conflictFound || 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); } } @@ -516,9 +511,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); } } @@ -665,7 +660,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); } @@ -691,7 +686,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); -- 2.34.1