From: amiraj Date: Thu, 17 Oct 2019 19:16:51 +0000 (-0700) Subject: Add the ConflictTracker to the main branch X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=3ff801c3f7ff84683ddf258df8f8f35d7cfc241e Add the ConflictTracker to the main branch --- diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java new file mode 100644 index 0000000..9fb12cf --- /dev/null +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -0,0 +1,584 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package gov.nasa.jpf.listener; + +import gov.nasa.jpf.Config; +import gov.nasa.jpf.JPF; +import gov.nasa.jpf.ListenerAdapter; +import gov.nasa.jpf.search.Search; +import gov.nasa.jpf.jvm.bytecode.*; +import gov.nasa.jpf.vm.*; +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 java.io.PrintWriter; + +import java.util.*; + +/** + * Listener using data flow analysis to find conflicts between smartApps. + **/ + +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 long timeout; + private long startTime; + private Node parentNode = new Node(-2); + private String operation; + private String detail; + private String errorMessage; + private int depth; + private int id; + private boolean conflictFound = false; + private boolean isSet = false; + private boolean manual = false; + + + public ConflictTracker(Config config, JPF jpf) { + out = new PrintWriter(System.out, true); + + String[] conflictVars = config.getStringArray("variables"); + // We are not tracking anything if it is null + if (conflictVars != null) { + for (String var : conflictVars) { + conflictSet.add(var); + } + } + String[] apps = config.getStringArray("apps"); + // We are not tracking anything if it is null + if (apps != null) { + for (String var : apps) { + 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()); + + 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); + } + } + } + + return false; + } + + boolean setOutSet(Node currentNode) { + Integer prevSize = currentNode.getOutSet().size(); + + // Update based on setSet + for (NameValuePair i : currentNode.getSetSet()) { + if (currentNode.getOutSet().contains(i)) + currentNode.getOutSet().remove(i); + currentNode.getOutSet().add(i); + } + + // 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; + } + + void setInSet(Node currentNode) { + for (Node i : currentNode.getPredecessors()) { + currentNode.getInSet().addAll(i.getOutSet()); + } + } + + boolean checkForConflict(Node currentNode) { + HashMap valueMap = new HashMap(); // HashMap from varName to value + 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()); + } + + // 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; + } + } + } + + return false; + } + + boolean updateSets(Node currentNode) { + // Set input set according to output set of pred states of current state + setInSet(currentNode); + + // Set outSet according to inSet, and setSet of current node, check if there is a change + return setOutSet(currentNode); + } + + static class Node { + Integer id; + HashSet predecessors = new HashSet(); + HashSet successors = new HashSet(); + HashSet inSet = new HashSet(); + HashSet setSet = new HashSet(); + HashSet outSet = new HashSet(); + + 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())); + } + } + + Integer getId() { + return id; + } + + HashSet getPredecessors() { + return predecessors; + } + + HashSet getSuccessors() { + return successors; + } + + HashSet getInSet() { + return inSet; + } + + HashSet getSetSet() { + return setSet; + } + + HashSet getOutSet() { + return outSet; + } + } + + 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; + } + + void setIsManual(String varName) { + this.isManual = isManual; + } + + Integer getAppNum() { + return appNum; + } + + String getValue() { + return value; + } + + String getVarName() { + return varName; + } + + boolean getIsManual() { + return isManual; + } + + @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 void stateRestored(Search search) { + id = search.getStateId(); + depth = search.getDepth(); + operation = "restored"; + detail = null; + + 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); + } + } + + @Override + public void searchStarted(Search search) { + out.println("----------------------------------- search started"); + } + + + @Override + public void stateAdvanced(Search search) { + String theEnd = null; + id = search.getStateId(); + depth = search.getDepth(); + operation = "forward"; + + // Add the node to the list of nodes + 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; + } + + if (search.isNewState()) { + detail = "new"; + } else { + detail = "visited"; + } + + if (search.isEndState()) { + out.println("This is the last state!"); + theEnd = "end"; + } + + 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.addPredecessor(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); + + // 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) + conflictFound = conflictFound || propagateTheChange(currentNode); + + // Update the parent node + if (nodes.containsKey(id)) { + parentNode = nodes.get(id); + } else { + parentNode = new Node(id); + } + } + + @Override + public void stateBacktracked(Search search) { + id = search.getStateId(); + depth = search.getDepth(); + operation = "backtrack"; + detail = null; + + 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); + } + } + + @Override + public void searchFinished(Search search) { + out.println("----------------------------------- search finished"); + } + + private String getValue(ThreadInfo ti, Instruction inst, byte type) { + StackFrame frame; + int lo, hi; + + frame = ti.getTopFrame(); + + if ((inst instanceof JVMLocalVariableInstruction) || + (inst instanceof JVMFieldInstruction)) + { + if (frame.getTopPos() < 0) + return(null); + + lo = frame.peek(); + hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0; + + return(decodeValue(type, lo, hi)); + } + + if (inst instanceof JVMArrayElementInstruction) + return(getArrayValue(ti, type)); + + return(null); + } + + private final static String decodeValue(byte type, int lo, int hi) { + switch (type) { + case Types.T_ARRAY: return(null); + case Types.T_VOID: return(null); + + case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo))); + case Types.T_BYTE: return(String.valueOf(lo)); + case Types.T_CHAR: return(String.valueOf((char) lo)); + case Types.T_DOUBLE: return(String.valueOf(Types.intsToDouble(lo, hi))); + case Types.T_FLOAT: return(String.valueOf(Types.intToFloat(lo))); + case Types.T_INT: return(String.valueOf(lo)); + case Types.T_LONG: return(String.valueOf(Types.intsToLong(lo, hi))); + case Types.T_SHORT: return(String.valueOf(lo)); + + case Types.T_REFERENCE: + ElementInfo ei = VM.getVM().getHeap().get(lo); + if (ei == null) + return(null); + + ClassInfo ci = ei.getClassInfo(); + if (ci == null) + return(null); + + if (ci.getName().equals("java.lang.String")) + return('"' + ei.asString() + '"'); + + return(ei.toString()); + + default: + System.err.println("Unknown type: " + type); + return(null); + } + } + + private String getArrayValue(ThreadInfo ti, byte type) { + StackFrame frame; + int lo, hi; + + frame = ti.getTopFrame(); + lo = frame.peek(); + hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0; + + return(decodeValue(type, lo, hi)); + } + + private byte getType(ThreadInfo ti, Instruction inst) { + StackFrame frame; + FieldInfo fi; + String type; + + frame = ti.getTopFrame(); + if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) { + return (Types.T_REFERENCE); + } + + type = null; + + if (inst instanceof JVMLocalVariableInstruction) { + type = ((JVMLocalVariableInstruction) inst).getLocalVariableType(); + } else if (inst instanceof JVMFieldInstruction){ + fi = ((JVMFieldInstruction) inst).getFieldInfo(); + type = fi.getType(); + } + + if (inst instanceof JVMArrayElementInstruction) { + return (getTypeFromInstruction(inst)); + } + + if (type == null) { + return (Types.T_VOID); + } + + return (decodeType(type)); + } + + private final static byte getTypeFromInstruction(Instruction inst) { + if (inst instanceof JVMArrayElementInstruction) + return(getTypeFromInstruction((JVMArrayElementInstruction) inst)); + + return(Types.T_VOID); + } + + private final static byte decodeType(String type) { + if (type.charAt(0) == '?'){ + return(Types.T_REFERENCE); + } else { + return Types.getBuiltinType(type); + } + } + + // Find the variable writer + // It should be one of the apps listed in the .jpf file + 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 writers in the writerSet + for(String writer : writerSet) { + if (method.contains(writer)) { + return writer; + } + } + } + } + + return null; + } + + @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(); + sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!"); + Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString()); + ti.setNextPC(nextIns); + } + } + + if (conflictFound) { + StringBuilder sb = new StringBuilder(); + 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 + 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; + + } + } + + + } + + } + +}