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=c8bb079c07248c0633e5ac67caf59863f668cb36;hp=9fb12cf3dac2aa6a4769468a7966edf7a7d5e710;hb=fb03d04f1c3952b9ea983ac73fa8f7daa64e1307;hpb=3ff801c3f7ff84683ddf258df8f8f35d7cfc241e diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index 9fb12cf..c8bb079 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -37,13 +37,12 @@ import java.util.*; **/ public class ConflictTracker extends ListenerAdapter { - private final PrintWriter out; private final HashSet conflictSet = new HashSet(); // Variables we want to track private final HashSet appSet = new HashSet(); // Apps we want to find their conflicts private final HashSet manualSet = new HashSet(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions private final HashMap nodes = new HashMap(); // Nodes of a graph - private HashSet tempSetSet = new HashSet(); + private ArrayList tempSetSet = new ArrayList(); private long timeout; private long startTime; private Node parentNode = new Node(-2); @@ -53,9 +52,10 @@ public class ConflictTracker extends ListenerAdapter { private int depth; private int id; 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); @@ -89,122 +89,211 @@ 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); + + for (Node node : currentNode.getSuccessors()) { + parentQueueMap.put(node, parents); + } 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 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; + } } } - } - return false; + // 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; } - boolean setOutSet(Node currentNode) { - Integer prevSize = currentNode.getOutSet().size(); + 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; + } - // Update based on setSet - for (NameValuePair i : currentNode.getSetSet()) { - if (currentNode.getOutSet().contains(i)) - currentNode.getOutSet().remove(i); - currentNode.getOutSet().add(i); + 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 isManualMap = new HashMap(); // HashMap from varName to isManual + + // 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); + isManualMap.put(varName, isManual); + } else { + valueMap.put(varName, value); + writerMap.put(varName, appNum); + isManualMap.put(varName, isManual); + } } - // 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; - } + // Check for conflict between outSet and this transition setSet + for (NameValuePair i : parentNode.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()) + &&!isManualMap.get(i.getVarName())) { + // We have different values and different writers + errorMessage = createErrorMessage(i, valueMap, writerMap); + return true; + } + } + } + } - void setInSet(Node currentNode) { - for (Node i : currentNode.getPredecessors()) { - currentNode.getInSet().addAll(i.getOutSet()); - } + return false; } - boolean checkForConflict(Node currentNode) { - HashMap valueMap = new HashMap(); // HashMap from varName to value - HashMap writerMap = new HashMap(); // HashMap from varName to appNum + 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(); + + for (int i = 0;i < setSet.size();i++) { + updatedVarNames.add(setSet.get(i).getVarName()); + } + } - 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()); + for (NameValuePair i : parentNode.getOutSet()) { + outSetVarMap.put(i.getVarName(), i.getAppNum()); + if (!updatedVarNames.contains(i.getVarName())) + isChanged |= currentNode.getOutSet().add(i); } - // Comparing the inSet and setSet to find the conflict - for (NameValuePair i : currentNode.getInSet()) { - if (valueMap.containsKey(i.getVarName())) { - if (!(valueMap.get(i.getVarName()).equals(i.getValue()))) // We have different values - if (!(writerMap.get(i.getVarName()).equals(i.getAppNum()))) {// We have different writers - 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; + + 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 false; + return isChanged; } - boolean updateSets(Node currentNode) { - // Set input set according to output set of pred states of current state - setInSet(currentNode); + 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); + } - // Set outSet according to inSet, and setSet of current node, check if there is a change - return setOutSet(currentNode); + // 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; + Integer id; HashSet predecessors = new HashSet(); HashSet successors = new HashSet(); - HashSet inSet = new HashSet(); - HashSet setSet = new HashSet(); HashSet outSet = new HashSet(); + HashMap outgoingEdges = new HashMap(); Node(Integer id) { - this.id = id; - } - - void addPredecessor(Node node) { - predecessors.add(node); - } - - void addSuccessor(Node node) { - successors.add(node); - } - - void setSetSet(HashSet setSet, boolean isManual) { - if (isManual) - this.setSet = new HashSet(); - for (NameValuePair i : setSet) { - this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual())); - } + this.id = id; } Integer getId() { @@ -219,16 +308,44 @@ public class ConflictTracker extends ListenerAdapter { return successors; } - HashSet getInSet() { - return inSet; + HashSet getOutSet() { + return outSet; + } + + HashMap getOutgoingEdges() { + return outgoingEdges; } + } - HashSet getSetSet() { - return setSet; + 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; } - HashSet getOutSet() { - return outSet; + Node getSource() { + return source; + } + + Node getDestination() { + return destination; + } + + HashMap> getSetSetMap() { + return setSetMap; + } + + HashMap getLastWriter() { + return lastWriter; + } + + HashMap getLastValue() { + return lastValue; } } @@ -239,10 +356,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) { @@ -279,12 +396,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 @@ -304,9 +421,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); } } @@ -319,21 +436,26 @@ 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 - nodes.put(id, new Node(id)); + // Add the node to the list of nodes + if (nodes.get(id) == null) + nodes.put(id, new Node(id)); + Node currentNode = nodes.get(id); - // Update the setSet for this new node - if (isSet) { - currentNode.setSetSet(tempSetSet, manual); - tempSetSet = new HashSet(); - isSet = false; - manual = false; - } + // Update the edge based on the current transition + updateTheEdge(currentNode, transition); + + // Reset the temporary variables and flags + tempSetSet = new ArrayList(); + manual = false; + + // Check for the conflict in this transition + conflictFound = checkForConflict(parentNode, currentNode, transition); if (search.isNewState()) { detail = "new"; @@ -351,28 +473,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 sets, check if the outSet is changed or not - boolean isChanged = updateSets(currentNode); - - // Check for a conflict - conflictFound = checkForConflict(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) + 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); + } + } 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); } } @@ -387,9 +513,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); } } @@ -407,13 +533,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) @@ -532,9 +658,17 @@ public class ConflictTracker extends ListenerAdapter { return null; } + private void writeWriterAndValue(String writer, String value, String var) { + // Update the temporary Set set. + NameValuePair temp = new NameValuePair(1, value, var, manual); + if (writer.equals("App2")) + temp = new NameValuePair(2, value, var, manual); + + tempSetSet.add(temp); + } + @Override public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { - // Instantiate timeoutTimer if (timeout > 0) { if (System.currentTimeMillis() - startTime > timeout) { StringBuilder sbTimeOut = new StringBuilder(); @@ -549,36 +683,45 @@ 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); + } + } + } + } + } + } }