From 9f853a376c28deeae82cb6e9e2841c4f2a0d2fa3 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Wed, 25 Mar 2020 18:56:27 -0700 Subject: [PATCH 1/1] Fixing bugs and cleaning up: Continuing sub-graph executions when there is no matched states or cycles that contain all events; checking in the old ConflictTracker for testing. --- main.jpf | 3 +- .../nasa/jpf/listener/ConflictTrackerOld.java | 649 ++++++++++++++++++ .../gov/nasa/jpf/listener/StateReducer.java | 31 +- 3 files changed, 674 insertions(+), 9 deletions(-) create mode 100644 src/main/gov/nasa/jpf/listener/ConflictTrackerOld.java diff --git a/main.jpf b/main.jpf index 713b4db..5d6e6a8 100644 --- a/main.jpf +++ b/main.jpf @@ -6,7 +6,8 @@ target = main #listener=gov.nasa.jpf.listener.StateReducerOld #listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer -listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerSimple +listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer +#listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerSimple #listener=gov.nasa.jpf.listener.ConflictTracker #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerClean diff --git a/src/main/gov/nasa/jpf/listener/ConflictTrackerOld.java b/src/main/gov/nasa/jpf/listener/ConflictTrackerOld.java new file mode 100644 index 0000000..0341cd5 --- /dev/null +++ b/src/main/gov/nasa/jpf/listener/ConflictTrackerOld.java @@ -0,0 +1,649 @@ +/* + * 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 gov.nasa.jpf.vm.choice.IntChoiceFromSet; + +import java.io.PrintWriter; + +import java.util.*; + +/** + * Listener using data flow analysis to find conflicts between smartApps. + **/ + +public class ConflictTrackerOld 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 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 int depth; + private int id; + private boolean manual = false; + private boolean conflictFound = false; + private int currentEvent = -1; + private boolean debugMode = false; + + private final String SET_LOCATION_METHOD = "setLocationMode"; + private final String LOCATION_VAR = "locationMode"; + + public ConflictTrackerOld(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 + 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); + } + } + + // 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 propagateChange(Edge newEdge) { + HashSet changed = new HashSet(); + + // 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 + Edge edgeToProcess = changed.iterator().next(); + changed.remove(edgeToProcess); + + //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); + } + } + } + } + + 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); + } + + //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; + } + + //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())); + } + + 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; + } + + 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; + + //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; + Vector outEdges = new Vector(); + HashMap> lastUpdates = new HashMap>(); + + Node(Integer id) { + this.id = id; + } + + Integer getId() { + return id; + } + + Vector getOutEdges() { + return outEdges; + } + + void addOutEdge(Edge e) { + outEdges.add(e); + } + + HashMap> getLastUpdates() { + return lastUpdates; + } + } + + //Each Edge corresponds to a transition + static class Edge { + 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 getSrc() { + return source; + } + + Node getDst() { + return destination; + } + + Transition getTransition() { + return transition; + } + + int getEventNumber() { return eventNumber; } + + ArrayList getUpdates() { + return updates; + } + } + + 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; + } + + boolean isManual() { + return ismanual; + } + + String getApp() { + return appName; + } + + String getDeviceId() { + return deviceId; + } + + String getAttribute() { + return attribute; + } + + String getValue() { + return value; + } + + //Gets an index object for indexing updates by just device and attribute + IndexObject getIndex() { + return new IndexObject(this); + } + + 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())); + } + + public int hashCode() { + return (getDeviceId().hashCode() << 3) ^ + (getAttribute().hashCode() << 2) ^ + (getApp().hashCode() << 1) ^ + getValue().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(); + depth = search.getDepth(); + operation = "restored"; + detail = null; + + out.println("The state is restored to state with id: "+id+", depth: "+depth); + + // Update the parent node + 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; + Transition transition = search.getTransition(); + id = search.getStateId(); + depth = search.getDepth(); + operation = "forward"; + + // Add the node to the list of nodes + Node currentNode = getNode(id); + + // Create an edge based on the current transition + Edge newEdge = createEdge(parentNode, currentNode, transition, currentEvent); + + // Reset the temporary variables and flags + currUpdates.clear(); + manual = false; + + // If we have a new Edge, check for conflicts + if (newEdge != null) + propagateChange(newEdge); + + 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); + + // Update the parent node + parentNode = currentNode; + } + + @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 + 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) { + 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; + + // 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)); + } + + 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; + } + + private void writeWriterAndValue(String writer, String attribute, String value) { + Update u = new Update(writer, "DEVICE", attribute, value, manual); + currUpdates.add(u); + } + + @Override + public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { + 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(); + // 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); + System.out.println(); + manual = (value.equals("true"))?true:false; + } + 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; + + // Update the current updates + writeWriterAndValue(writer, var, value); + } + } + } + } + } +} \ No newline at end of file diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index afa1f87..e031354 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -187,6 +187,12 @@ public class StateReducer extends ListenerAdapter { return copyOfChoices; } + private void continueExecutingThisTrace(IntChoiceFromSet icsCG) { + // We repeat the same trace if a state match is not found yet + IntChoiceFromSet setCG = setNewCG(icsCG); + unusedCG.add(setCG); + } + private void initializeChoiceGenerators(IntChoiceFromSet icsCG, Integer[] cgChoices) { if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) { // Update the choices of the first CG and add '-1' @@ -204,11 +210,18 @@ public class StateReducer extends ListenerAdapter { IntChoiceFromSet setCG = setNewCG(icsCG); cgMap.put(setCG, refChoices[choiceCounter]); } else { - // We repeat the same trace if a state match is not found yet - IntChoiceFromSet setCG = setNewCG(icsCG); - unusedCG.add(setCG); + continueExecutingThisTrace(icsCG); + } + } + + private void manageChoiceGeneratorsInSubsequentTraces(IntChoiceFromSet icsCG) { + // If this is the first iteration of the trace then set other CGs done + if (choiceCounter <= choiceUpperBound) { + icsCG.setDone(); + } else { + // If this is the subsequent iterations of the trace then set up new CGs to continue the execution + continueExecutingThisTrace(icsCG); } - choiceCounter++; } @Override @@ -229,8 +242,10 @@ public class StateReducer extends ListenerAdapter { initializeChoiceGenerators(icsCG, cgChoices); } else { // Set new CGs to done so that the search algorithm explores the existing CGs - icsCG.setDone(); + //icsCG.setDone(); + manageChoiceGeneratorsInSubsequentTraces(icsCG); } + choiceCounter++; } } } @@ -321,12 +336,11 @@ public class StateReducer extends ListenerAdapter { private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) { // Traverse the sub-graphs if (isResetAfterAnalysis) { - // Advance choice counter for sub-graphs - choiceCounter++; // Do this for every CG after finishing each backtrack list // We try to update the CG with a backtrack list if the state has been visited multiple times //if ((icsCG.getNextChoice() == -1 || choiceCounter > 1) && cgMap.containsKey(icsCG)) { - if ((!icsCG.hasMoreChoices() || choiceCounter > 1) && cgMap.containsKey(icsCG)) { + //if ((!icsCG.hasMoreChoices() || choiceCounter > 1) && cgMap.containsKey(icsCG)) { + if (choiceCounter > 1 && cgMap.containsKey(icsCG)) { int event = cgMap.get(icsCG); LinkedList choiceLists = backtrackMap.get(event); if (choiceLists != null && choiceLists.peekFirst() != null) { @@ -338,6 +352,7 @@ public class StateReducer extends ListenerAdapter { // Set done if this was the last backtrack list icsCG.setDone(); } + setDoneUnusedCG(); saveVisitedStates(); } } else { -- 2.34.1