X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FConflictTracker.java;h=620d1be410597f8ef34963696a895ca7c3e1592b;hb=899f4a49b5d96061d6cc942a7ce26e8ec8958fa2;hp=831442b16f345f60e4f1f6ce3f000def8fc7f789;hpb=0cf261c59c66a46800aab1eaee6591092f12b01c;p=jpf-core.git diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index 831442b..620d1be 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -27,6 +27,7 @@ import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction; import gov.nasa.jpf.vm.bytecode.ReadInstruction; import gov.nasa.jpf.vm.bytecode.StoreInstruction; import gov.nasa.jpf.vm.bytecode.WriteInstruction; +import gov.nasa.jpf.vm.choice.IntChoiceFromSet; import java.io.PrintWriter; @@ -37,28 +38,35 @@ import java.util.*; **/ public class ConflictTracker extends ListenerAdapter { + private final PrintWriter out; + private final HashMap nodes = new HashMap(); // Nodes of a graph 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 ArrayList tempSetSet = new ArrayList(); + private HashSet transitions = new HashSet(); + private ArrayList currUpdates = new ArrayList(); private long timeout; private long startTime; private Node parentNode = new Node(-2); private String operation; private String detail; private String errorMessage; + private String varName; private int depth; private int id; - private boolean conflictFound = false; private boolean manual = false; + private boolean conflictFound = false; + private int currentEvent = -1; + private boolean debugMode = false; + private int popRef = 0; 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); + debugMode = config.getBoolean("debug_mode", false); String[] conflictVars = config.getStringArray("variables"); // We are not tracking anything if it is null @@ -74,344 +82,260 @@ 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(); } - boolean propagateTheChange(Node currentNode) { - HashSet changed = new HashSet(currentNode.getSuccessors()); - HashMap> parentQueueMap = new HashMap>(); - HashSet parents = new HashSet(); - parents.add(currentNode); + void propagateChange(Edge newEdge) { + HashSet changed = new HashSet(); - for (Node node : currentNode.getSuccessors()) { - parentQueueMap.put(node, parents); - } + // Add the current node to the changed set + changed.add(newEdge); - 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 + Edge edgeToProcess = changed.iterator().next(); + changed.remove(edgeToProcess); - // 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); - } - } + //If propagating change on edge causes change, enqueue all the target node's out edges + if (propagateEdge(edgeToProcess)) { + Node dst = edgeToProcess.getDst(); + for (Edge e : dst.getOutEdges()) { + changed.add(e); + } } - - 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; + } } - 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 - - - // 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(); - - 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; - } else { // We have two writers writing the same value - writerMap.put(varName, 3); // 3 represents both apps - } - } else { - // Check if we have more than one value with the same writer - if (!valueMap.get(varName).equals(value)) { - // We have one writer writing more than one value in a same event - valueMap.put(varName, "twoValue"); - } - } - } else { - valueMap.put(varName, value); - writerMap.put(varName, appNum); - } - } - - // 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())) { - // We have different values and different writers - errorMessage = createErrorMessage(i, valueMap, writerMap); - return true; - } - } - } - } - - return false; - } + boolean propagateEdge(Edge e) { + HashMap> srcUpdates = e.getSrc().getLastUpdates(); + HashMap> dstUpdates = e.getDst().getLastUpdates(); + ArrayList edgeUpdates = e.getUpdates(); + HashMap lastupdate = new HashMap(); + boolean changed = false; + + //Go through each update on the current transition + for(int i=0; i confupdates = null; + + //See if we have already updated this device attribute + if (lastupdate.containsKey(io)) { + confupdates = new HashSet(); + confupdates.add(lastupdate.get(io)); + } else if (srcUpdates.containsKey(io)){ + confupdates = srcUpdates.get(io); + } - 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()); - } + //Check for conflict with the appropriate update set if we are not a manual transition + //If this is debug mode, then we do not report any conflicts + if (!debugMode && confupdates != null && !u.isManual()) { + for(Update u2: confupdates) { + if (conflicts(u, u2)) { + //throw new RuntimeException(createErrorMessage(u, u2)); + conflictFound = true; + errorMessage = createErrorMessage(u, u2); + } } + } + lastupdate.put(io, u); + } + for(IndexObject io: srcUpdates.keySet()) { + //Only propagate src changes if the transition doesn't update the device attribute + if (!lastupdate.containsKey(io)) { + //Make sure destination has hashset in map + if (!dstUpdates.containsKey(io)) + dstUpdates.put(io, new HashSet()); + + changed |= dstUpdates.get(io).addAll(srcUpdates.get(io)); + } + } + for(IndexObject io: lastupdate.keySet()) { + //Make sure destination has hashset in map + if (!dstUpdates.containsKey(io)) + dstUpdates.put(io, new HashSet()); + + changed |= dstUpdates.get(io).add(lastupdate.get(io)); + } + return changed; + } - - 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(); + //Method to check for conflicts between two updates + //Have conflict if same device, same attribute, different app, different vaalue + boolean conflicts(Update u, Update u2) { + return (!u.getApp().equals(u2.getApp())) && + u.getDeviceId().equals(u2.getDeviceId()) && + u.getAttribute().equals(u2.getAttribute()) && + (!u.getValue().equals(u2.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; + String createErrorMessage(Update u, Update u2) { + String message = "Conflict found between the two apps. "+u.getApp()+ + " has written the value: "+u.getValue()+ + " to the attribute: "+u.getAttribute()+" while " + +u2.getApp()+" is writing the value: " + +u2.getValue()+" to the same variable!"; + System.out.println(message); + return message; } - 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); - } + Edge createEdge(Node parent, Node current, Transition transition, int evtNum) { + //Check if this transition is explored. If so, just skip everything + if (transitions.contains(transition)) + return null; - // 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()); - } - } + //Create edge + Edge e = new Edge(parent, current, transition, evtNum, currUpdates); + parent.addOutEdge(e); - + //Mark transition as explored + transitions.add(transition); + return e; + } 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 getId() { - return id; - } - - HashSet getPredecessors() { - return predecessors; - } + Integer id; + Vector outEdges = new Vector(); + HashMap> lastUpdates = new HashMap>(); + + Node(Integer id) { + this.id = id; + } - HashSet getSuccessors() { - return successors; - } + Integer getId() { + return id; + } - HashSet getOutSet() { - return outSet; - } + Vector getOutEdges() { + return outEdges; + } - HashMap getOutgoingEdges() { - return outgoingEdges; - } + void addOutEdge(Edge e) { + outEdges.add(e); + } + + HashMap> getLastUpdates() { + return lastUpdates; + } } + //Each Edge corresponds to a transition 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; + Transition transition; + int eventNumber; + ArrayList updates = new ArrayList(); + + Edge(Node src, Node dst, Transition t, int evtNum, ArrayList _updates) { + this.source = src; + this.destination = dst; + this.transition = t; + this.eventNumber = evtNum; + this.updates.addAll(_updates); + } - Node getSource() { - return source; - } + Node getSrc() { + return source; + } - Node getDestination() { - return destination; - } + Node getDst() { + return destination; + } - HashMap> getSetSetMap() { - return setSetMap; - } + Transition getTransition() { + return transition; + } - HashMap getLastWriter() { - return lastWriter; - } + int getEventNumber() { return eventNumber; } - HashMap getLastValue() { - return lastValue; - } + ArrayList getUpdates() { + return updates; + } } - 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; - } - - void setAppNum(Integer appNum) { - this.appNum = appNum; - } - - void setValue(String value) { - this.value = value; - } - - void setVarName(String varName) { - this.varName = varName; - } + static class Update { + String appName; + String deviceId; + String attribute; + String value; + boolean ismanual; + + Update(String _appName, String _deviceId, String _attribute, String _value, boolean _ismanual) { + this.appName = _appName; + this.deviceId = _deviceId; + this.attribute = _attribute; + this.value = _value; + this.ismanual = _ismanual; + } - void setIsManual(String varName) { - this.isManual = isManual; - } + boolean isManual() { + return ismanual; + } + + String getApp() { + return appName; + } - Integer getAppNum() { - return appNum; - } + String getDeviceId() { + return deviceId; + } - String getValue() { - return value; - } + String getAttribute() { + return attribute; + } + + String getValue() { + return value; + } - String getVarName() { - return varName; - } + //Gets an index object for indexing updates by just device and attribute + IndexObject getIndex() { + return new IndexObject(this); + } - boolean getIsManual() { - return isManual; - } + public boolean equals(Object o) { + if (!(o instanceof Update)) + return false; + Update u=(Update)o; + return (getDeviceId().equals(u.getDeviceId()) && + getAttribute().equals(u.getAttribute()) && + getApp().equals(u.getApp()) && + getValue().equals(u.getValue())); + } - @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; - } + public int hashCode() { + return (getDeviceId().hashCode() << 3) ^ + (getAttribute().hashCode() << 2) ^ + (getApp().hashCode() << 1) ^ + getValue().hashCode(); + } - @Override - public int hashCode() { - return appNum.hashCode() * 31 + varName.hashCode(); - } + public String toString() { + return "<"+getAttribute()+", "+getValue()+", "+getApp()+", "+ismanual+">"; + } } + static class IndexObject { + Update u; + IndexObject(Update _u) { + this.u = _u; + } + + public boolean equals(Object o) { + if (!(o instanceof IndexObject)) + return false; + IndexObject io=(IndexObject)o; + return (u.getDeviceId().equals(io.u.getDeviceId()) && + u.getAttribute().equals(io.u.getAttribute())); + } + public int hashCode() { + return (u.getDeviceId().hashCode() << 1) ^ u.getAttribute().hashCode(); + } + } + @Override public void stateRestored(Search search) { id = search.getStateId(); @@ -422,19 +346,53 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is restored to state with id: "+id+", depth: "+depth); // Update the parent node - if (nodes.containsKey(id)) { - parentNode = nodes.get(id); - } else { - parentNode = new Node(id); - } + parentNode = getNode(id); } @Override public void searchStarted(Search search) { out.println("----------------------------------- search started"); } - + private Node getNode(Integer id) { + if (!nodes.containsKey(id)) + nodes.put(id, new Node(id)); + return nodes.get(id); + } + + public void printGraph() { + System.out.println("digraph testgraph {"); + for(Integer i : nodes.keySet()) { + Node n = nodes.get(i); + System.out.print("N"+i+"[label=\""); + + for(IndexObject io:n.lastUpdates.keySet()) { + for(Update u:n.lastUpdates.get(io)) { + System.out.print(u.toString().replace("\"", "\\\"")+", "); + } + } + System.out.println("\"];"); + for(Edge e:n.outEdges) { + System.out.print("N"+e.getSrc().getId()+"->N"+e.getDst().getId()+"[label=\""); + for(Update u:e.getUpdates()) { + System.out.print(u.toString().replace("\"", "\\\"")+", "); + } + System.out.println("\"];"); + } + } + + System.out.println("}"); + } + + @Override + public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator currentCG) { + + if (currentCG instanceof IntChoiceFromSet) { + IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; + currentEvent = icsCG.getNextChoice(); + } + } + @Override public void stateAdvanced(Search search) { String theEnd = null; @@ -444,20 +402,18 @@ public class ConflictTracker extends ListenerAdapter { operation = "forward"; // Add the node to the list of nodes - if (nodes.get(id) == null) - nodes.put(id, new Node(id)); + Node currentNode = getNode(id); - Node currentNode = nodes.get(id); - - // Update the edge based on the current transition - updateTheEdge(currentNode, transition); + // Create an edge based on the current transition + Edge newEdge = createEdge(parentNode, currentNode, transition, currentEvent); // Reset the temporary variables and flags - tempSetSet = new ArrayList(); + currUpdates.clear(); manual = false; - // Check for the conflict in this transition - conflictFound = checkForConflict(parentNode, currentNode, transition); + // If we have a new Edge, check for conflicts + if (newEdge != null) + propagateChange(newEdge); if (search.isNewState()) { detail = "new"; @@ -472,36 +428,8 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd); - // 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); - - // 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); - - // 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); - } - } - conflictFound = conflictFound || propagateTheChange(currentNode); - } // Update the parent node - if (nodes.containsKey(id)) { - parentNode = nodes.get(id); - } else { - parentNode = new Node(id); - } + parentNode = currentNode; } @Override @@ -514,16 +442,15 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is backtracked to state with id: "+id+", depth: "+depth); // Update the parent node - if (nodes.containsKey(id)) { - parentNode = nodes.get(id); - } else { - parentNode = new Node(id); - } + parentNode = getNode(id); } @Override public void searchFinished(Search search) { out.println("----------------------------------- search finished"); + + //Comment out the following line to print the explored graph + printGraph(); } private String getValue(ThreadInfo ti, Instruction inst, byte type) { @@ -541,6 +468,16 @@ public class ConflictTracker extends ListenerAdapter { lo = frame.peek(); hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0; + // TODO: Fix for integer values (need to dig deeper into the stack frame to find the right value other than 0) + // TODO: Seems to be a problem since this is Groovy (not Java) + if (type == Types.T_INT || type == Types.T_LONG || type == Types.T_SHORT) { + int offset = 0; + while (lo == 0) { + lo = frame.peek(offset); + offset++; + } + } + return(decodeValue(type, lo, hi)); } @@ -575,7 +512,7 @@ public class ConflictTracker extends ListenerAdapter { if (ci.getName().equals("java.lang.String")) return('"' + ei.asString() + '"'); - + return(ei.toString()); default: @@ -660,13 +597,9 @@ 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); + private void writeWriterAndValue(String writer, String attribute, String value) { + Update u = new Update(writer, "DEVICE", attribute, value, manual); + currUpdates.add(u); } @Override @@ -686,44 +619,53 @@ public class ConflictTracker extends ListenerAdapter { Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString()); ti.setNextPC(nextIns); } 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); + // Check if we are ready to pop the values + if (popRef == 2) { + byte type = getType(ti, executedInsn); + varName = getValue(ti, executedInsn, type); + String writer = getWriter(ti.getStack(), appSet); + + popRef = popRef-1; + } else if (popRef == 1) { + byte type = getType(ti, executedInsn); + String value = getValue(ti, executedInsn, type); + String writer = getWriter(ti.getStack(), appSet); + + for (String var: conflictSet) { + if (varName.contains(var)) { + if (writer != null) + writeWriterAndValue(writer, varName, value); + } + } - // Extract the writer app name - ClassInfo ci = mi.getClassInfo(); - String writer = ci.getName(); + popRef = popRef-1; + } - // 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); - } - } + + if (executedInsn.getMnemonic().equals("getfield")) { + if (executedInsn.toString().contains("deviceValueSmartThing") || + executedInsn.toString().contains("deviceIntValueSmartThing")) { + if (executedInsn.getNext() != null) { + if (executedInsn.getNext().getMnemonic().contains("load")) { + + if (executedInsn.getNext().getNext() != null) + if (executedInsn.getNext().getNext().getMnemonic().contains("load")) + popRef = 2; + } + } + } + } + + if (executedInsn instanceof WriteInstruction) { + String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName(); + // Check if we have an update to isManualTransaction to update manual field + if (varId.contains("isManualTransaction")) { + byte type = getType(ti, executedInsn); + String value = getValue(ti, executedInsn, type); + + manual = (value.equals("true"))?true:false; } } - } + } } }