From: amiraj Date: Wed, 16 Oct 2019 22:19:00 +0000 (-0700) Subject: Adding feature to differentiate direct-direct interactions and conflicts X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;ds=sidebyside;h=27de7960e1c17d08df67f86de29e5b394b16d8c5;p=jpf-core.git Adding feature to differentiate direct-direct interactions and conflicts --- diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index c3e0e2f..fc14574 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -41,8 +41,9 @@ 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 final HashSet tempSetSet = new HashSet(); + private HashSet tempSetSet = new HashSet(); private long timeout; private long startTime; private Node parentNode = new Node(-2); @@ -71,14 +72,21 @@ public class ConflictTracker extends ListenerAdapter { appSet.add(var); } } + String[] manualClasses = config.getStringArray("manualClasses"); + // We are not tracking anything if it is null + if (manualClasses != null) { + for (String var : manualClasses) { + manualSet.add(var); + } + } + // Timeout input from config is in minutes, so we need to convert into millis timeout = config.getInt("timeout", 0) * 60 * 1000; startTime = System.currentTimeMillis(); } - void propagateTheChange(Node currentNode) { + boolean propagateTheChange(Node currentNode) { HashSet changed = new HashSet(currentNode.getSuccessors()); - boolean isChanged; while(!changed.isEmpty()) { // Get the first element of HashSet and remove it from the changed set @@ -86,10 +94,11 @@ public class ConflictTracker extends ListenerAdapter { changed.remove(nodeToProcess); // Update the sets, store the outSet to temp before its changes - isChanged = updateSets(nodeToProcess); + boolean isChanged = updateSets(nodeToProcess); // Check for a conflict - conflictFound = checkForConflict(nodeToProcess); + if (checkForConflict(nodeToProcess)) + return true; // Checking if the out set has changed or not(Add its successors to the change list!) if (isChanged) { @@ -99,44 +108,34 @@ public class ConflictTracker extends ListenerAdapter { } } } + + return false; } boolean setOutSet(Node currentNode) { boolean isChanged = false; - HashMap outSet = new HashMap(); - - // Store the outSet of current node to HashMap to help for the search in O(n) - for (NameValuePair i : currentNode.getOutSet()) { - outSet.put(i, i.getValue()); - } - + // Update based on inSet for (NameValuePair i : currentNode.getInSet()) { - if (currentNode.getOutSet().contains(i)) { - if (outSet.get(i) != i.getValue()) - isChanged = true; - currentNode.getOutSet().remove(i); - } else { + if (!currentNode.getOutSet().contains(i)) { isChanged = true; + currentNode.getOutSet().add(i); } - currentNode.getOutSet().add(i); } - // Overwrite the outSet based on setSet if we have a writer + // Overwrite based on setSet for (NameValuePair i : currentNode.getSetSet()) { - if (currentNode.getOutSet().contains(i)) { - if (outSet.get(i) != i.getValue()) - isChanged = true; - currentNode.getOutSet().remove(i); - } else { + if (!currentNode.getOutSet().contains(i)) isChanged = true; - } + else + currentNode.getOutSet().remove(i); currentNode.getOutSet().add(i); } return isChanged; } + //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()); @@ -144,15 +143,17 @@ public class ConflictTracker extends ListenerAdapter { } boolean checkForConflict(Node currentNode) { - HashMap varNameMap = new HashMap(); + HashMap valueMap = new HashMap(); + HashMap isManualMap = new HashMap(); for (NameValuePair i : currentNode.getOutSet()) { - if (varNameMap.containsKey(i.getVarName())) { - if (varNameMap.get(i) != i.getValue()) { - return true; - } + if (valueMap.containsKey(i.getVarName())) { + if (!(isManualMap.get(i.getVarName())&&(i.getIsManual()))) + if (!(valueMap.get(i.getVarName()).equals(i.getValue()))) + return true; } else { - varNameMap.put(i.getVarName(), i.getValue()); + valueMap.put(i.getVarName(), i.getValue()); + isManualMap.put(i.getVarName(), i.getIsManual()); } } @@ -188,7 +189,9 @@ public class ConflictTracker extends ListenerAdapter { } void setSetSet(HashSet setSet) { - this.setSet.addAll(setSet); + for (NameValuePair i : setSet) { + this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual())); + } } Integer getId() { @@ -220,11 +223,13 @@ public class ConflictTracker extends ListenerAdapter { Integer appNum; String value; String varName; + boolean isManual; - NameValuePair(Integer appNum, String value, String varName) { + 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) { @@ -239,6 +244,10 @@ public class ConflictTracker extends ListenerAdapter { this.varName = varName; } + void setIsManual(String varName) { + this.isManual = isManual; + } + Integer getAppNum() { return appNum; } @@ -251,6 +260,10 @@ public class ConflictTracker extends ListenerAdapter { return varName; } + boolean getIsManual() { + return isManual; + } + @Override public boolean equals(Object o) { if (o instanceof NameValuePair) { @@ -277,7 +290,11 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is restored to state with id: "+id+", depth: "+depth); // Update the parent node - parentNode = new Node(id); + if (nodes.containsKey(id)) { + parentNode = nodes.get(id); + } else { + parentNode = new Node(id); + } } @Override @@ -295,11 +312,12 @@ public class ConflictTracker extends ListenerAdapter { // Add the node to the list of nodes nodes.put(id, new Node(id)); - Node currentNode = nodes.get(id); + Node currentNode = nodes.get(id); // Update the setSet for this new node if (isSet) { currentNode.setSetSet(tempSetSet); + tempSetSet = new HashSet(); isSet = false; } @@ -328,16 +346,20 @@ public class ConflictTracker extends ListenerAdapter { // Update the sets, check if the outSet is changed or not boolean isChanged = updateSets(currentNode); - + // Check for a conflict conflictFound = checkForConflict(currentNode); // Check if the outSet of this state has changed, update all of its successors' sets if any if (isChanged) - propagateTheChange(currentNode); - + conflictFound = conflictFound || propagateTheChange(currentNode); + // Update the parent node - parentNode = new Node(id); + if (nodes.containsKey(id)) { + parentNode = nodes.get(id); + } else { + parentNode = new Node(id); + } } @Override @@ -350,7 +372,11 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is backtracked to state with id: "+id+", depth: "+depth); // Update the parent node - parentNode = new Node(id); + if (nodes.containsKey(id)) { + parentNode = nodes.get(id); + } else { + parentNode = new Node(id); + } } @Override @@ -474,18 +500,16 @@ public class ConflictTracker extends ListenerAdapter { // Find the variable writer // It should be one of the apps listed in the .jpf file - private String getWriter(List sfList) { + private String getWriter(List sfList, HashSet writerSet) { // Start looking from the top of the stack backward for(int i=sfList.size()-1; i>=0; i--) { MethodInfo mi = sfList.get(i).getMethodInfo(); if(!mi.isJPFInternal()) { String method = mi.getStackTraceName(); - // Check against the apps in the appSet - for(String app : appSet) { - // There is only one writer at a time but we need to always - // check all the potential writers in the list - if (method.contains(app)) { - return app; + // Check against the writers in the writerSet + for(String writer : writerSet) { + if (method.contains(writer)) { + return writer; } } } @@ -519,25 +543,29 @@ public class ConflictTracker extends ListenerAdapter { // Get variable info byte type = getType(ti, executedInsn); String value = getValue(ti, executedInsn, type); - String writer = getWriter(ti.getStack()); + 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; - // Update the temporary Set set. - if (writer.equals("App1")) - tempSetSet.add(new NameValuePair(1, value, var)); - else if (writer.equals("App2")) - tempSetSet.add(new NameValuePair(2, value, var)); - // Set isSet to 1 - isSet = true; + if (getWriter(ti.getStack(), manualSet) != null) + isManual = true; + + // Update the temporary Set set. + if (writer.equals("App1")) + tempSetSet.add(new NameValuePair(1, value, var, isManual)); + else if (writer.equals("App2")) + tempSetSet.add(new NameValuePair(2, value, var, isManual)); + // Set isSet to true + isSet = true; } - } + } - } - } + + } }