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=134346775940c10aaf5acd5db90d67c8b16159b9;hp=9fb12cf3dac2aa6a4769468a7966edf7a7d5e710;hb=503dc126771633ff83c758fd5d0d7c9f3236c3e3;hpb=3ff801c3f7ff84683ddf258df8f8f35d7cfc241e diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index 9fb12cf..1343467 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -55,7 +55,9 @@ public class ConflictTracker extends ListenerAdapter { 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); @@ -91,24 +93,24 @@ public class ConflictTracker extends ListenerAdapter { HashSet changed = new HashSet(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 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 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); + } + } } return false; @@ -119,9 +121,9 @@ public class ConflictTracker extends ListenerAdapter { // Update based on setSet for (NameValuePair i : currentNode.getSetSet()) { - if (currentNode.getOutSet().contains(i)) - currentNode.getOutSet().remove(i); - currentNode.getOutSet().add(i); + if (currentNode.getOutSet().contains(i)) + currentNode.getOutSet().remove(i); + currentNode.getOutSet().add(i); } // Add all the inSet @@ -129,15 +131,15 @@ public class ConflictTracker extends ListenerAdapter { // Check if the outSet is changed if (!prevSize.equals(currentNode.getOutSet().size())) - return true; + return true; return false; } void setInSet(Node currentNode) { for (Node i : currentNode.getPredecessors()) { - currentNode.getInSet().addAll(i.getOutSet()); - } + currentNode.getInSet().addAll(i.getOutSet()); + } } boolean checkForConflict(Node currentNode) { @@ -145,27 +147,30 @@ public class ConflictTracker extends ListenerAdapter { HashMap writerMap = new HashMap(); // HashMap from varName to appNum 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()); + 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()); } // 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; - } - } + 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 = "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; + } + } + } } return false; @@ -173,10 +178,10 @@ public class ConflictTracker extends ListenerAdapter { boolean updateSets(Node currentNode) { // Set input set according to output set of pred states of current state - setInSet(currentNode); + setInSet(currentNode); // Set outSet according to inSet, and setSet of current node, check if there is a change - return setOutSet(currentNode); + return setOutSet(currentNode); } static class Node { @@ -200,11 +205,11 @@ public class ConflictTracker extends ListenerAdapter { } 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())); - } + if (isManual) + this.setSet = new HashSet(); + for (NameValuePair i : setSet) { + this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual())); + } } Integer getId() { @@ -239,10 +244,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) { @@ -257,7 +262,7 @@ public class ConflictTracker extends ListenerAdapter { this.varName = varName; } - void setIsManual(String varName) { + void setIsManual(String varName) { this.isManual = isManual; } @@ -279,12 +284,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 +309,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); } } @@ -370,9 +375,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); } } @@ -387,9 +392,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 +412,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,6 +537,19 @@ 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); + + if (tempSetSet.contains(temp)) + tempSetSet.remove(temp); + tempSetSet.add(temp); + // Set isSet to true + isSet = true; + } + @Override public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { // Instantiate timeoutTimer @@ -549,36 +567,44 @@ 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); + } + } + } + } + } + } }