2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
18 package gov.nasa.jpf.listener;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.JPF;
22 import gov.nasa.jpf.ListenerAdapter;
23 import gov.nasa.jpf.search.Search;
24 import gov.nasa.jpf.jvm.bytecode.*;
25 import gov.nasa.jpf.vm.*;
26 import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
27 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
28 import gov.nasa.jpf.vm.bytecode.StoreInstruction;
29 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
31 import java.io.PrintWriter;
36 * Listener using data flow analysis to find conflicts between smartApps.
39 public class ConflictTracker extends ListenerAdapter {
40 private final PrintWriter out;
41 private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
42 private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
43 private final HashSet<String> manualSet = new HashSet<String>(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions
44 private final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
45 private ArrayList<NameValuePair> tempSetSet = new ArrayList<NameValuePair>();
47 private long startTime;
48 private Node parentNode = new Node(-2);
49 private String operation;
50 private String detail;
51 private String errorMessage;
54 private boolean conflictFound = false;
55 private boolean manual = false;
57 private final String SET_LOCATION_METHOD = "setLocationMode";
58 private final String LOCATION_VAR = "locationMode";
60 public ConflictTracker(Config config, JPF jpf) {
61 out = new PrintWriter(System.out, true);
63 String[] conflictVars = config.getStringArray("variables");
64 // We are not tracking anything if it is null
65 if (conflictVars != null) {
66 for (String var : conflictVars) {
70 String[] apps = config.getStringArray("apps");
71 // We are not tracking anything if it is null
73 for (String var : apps) {
77 String[] manualClasses = config.getStringArray("manualClasses");
78 // We are not tracking anything if it is null
79 if (manualClasses != null) {
80 for (String var : manualClasses) {
85 // Timeout input from config is in minutes, so we need to convert into millis
86 timeout = config.getInt("timeout", 0) * 60 * 1000;
87 startTime = System.currentTimeMillis();
90 boolean propagateTheChange(Node currentNode) {
91 HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
92 HashMap<Node, HashSet<Node>> parentQueueMap = new HashMap<Node, HashSet<Node>>();
93 HashSet<Node> parents = new HashSet<Node>();
94 parents.add(currentNode);
96 for (Node node : currentNode.getSuccessors()) {
97 parentQueueMap.put(node, parents);
100 while(!changed.isEmpty()) {
101 // Get the first element of the changed set and remove it
102 Node nodeToProcess = changed.iterator().next();
103 changed.remove(nodeToProcess);
105 // Update the changed parents
107 parents = parentQueueMap.get(nodeToProcess);
108 boolean isChanged = false;
110 for (Node node : parents) {
112 isChanged |= updateTheOutSet(node, nodeToProcess);
115 // Check for a conflict if the outSet of nodeToProcess is changed
117 for (Node node : nodeToProcess.getSuccessors()) {
118 HashMap<Transition, ArrayList<NameValuePair>> setSets = nodeToProcess.getOutgoingEdges().get(node).getSetSetMap();
119 for (Map.Entry mapElement : setSets.entrySet()) {
120 Transition transition = (Transition)mapElement.getKey();
121 if (checkForConflict(nodeToProcess, node, transition))
127 // Update the parents list for the successors of the current node
129 parents.add(nodeToProcess);
131 // Checking if the out set has changed or not(Add its successors to the change list!)
133 for (Node i : nodeToProcess.getSuccessors()) {
134 if (!changed.contains(i))
137 // Update the list of updated parents for the current node
138 if (parentQueueMap.containsKey(i))
139 parentQueueMap.get(i).add(nodeToProcess);
141 parentQueueMap.put(i, parents);
149 String createErrorMessage(NameValuePair pair, HashMap<String, String> valueMap, HashMap<String, Integer> writerMap) {
150 String message = "Conflict found between the two apps. App"+pair.getAppNum()+
151 " has written the value: "+pair.getValue()+
152 " to the variable: "+pair.getVarName()+" while App"
153 +writerMap.get(pair.getVarName())+" is overwriting the value: "
154 +valueMap.get(pair.getVarName())+" to the same variable!";
155 System.out.println(message);
159 boolean checkForConflict(Node parentNode, Node currentNode, Transition currentTransition) {
160 ArrayList<NameValuePair> setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap().get(currentTransition);
161 HashMap<String, String> valueMap = new HashMap<String, String>(); // HashMap from varName to value
162 HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); // HashMap from varName to appNum
163 HashMap<String, String> firstValueMap = new HashMap<String, String>(); // HashMap from varName to value - first instruction in transition
164 HashMap<String, Integer> firstWriterMap = new HashMap<String, Integer>(); // HashMap from varName to appNum - first instruction in transition
167 // Update the valueMap and writerMap + check for conflict between the elements of setSet
168 for (int i = 0;i < setSet.size();i++) {
169 NameValuePair nameValuePair = setSet.get(i);
170 String varName = nameValuePair.getVarName();
171 String value = nameValuePair.getValue();
172 Integer appNum = nameValuePair.getAppNum();
173 Boolean isManual = nameValuePair.getIsManual();
175 if (valueMap.containsKey(varName)) {
176 // Check if we have a same writer
177 if (!writerMap.get(varName).equals(appNum)) {
178 // Check if we have a conflict or not
179 if (!valueMap.get(varName).equals(value)) {
180 errorMessage = createErrorMessage(nameValuePair, valueMap, writerMap);
184 valueMap.put(varName, value);
185 writerMap.put(varName, appNum);
187 valueMap.put(varName, value);
188 writerMap.put(varName, appNum);
190 firstValueMap.put(varName, value);
191 firstWriterMap.put(varName, appNum);
196 // Check for conflict between outSet and this transition setSet
197 for (NameValuePair i : parentNode.getOutSet()) {
198 if (valueMap.containsKey(i.getVarName())) {
199 String value = firstValueMap.get(i.getVarName());
200 Integer writer = firstWriterMap.get(i.getVarName());
201 if ((value != null)&&(writer != null)) {
202 if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) {
203 // We have different values and different writers
204 errorMessage = createErrorMessage(i, firstValueMap, firstWriterMap);
214 boolean updateTheOutSet(Node parentNode, Node currentNode) {
215 HashMap<Transition, ArrayList<NameValuePair>> setSets = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap();
216 HashSet<String> updatedVarNames = new HashSet<String>();
217 Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
218 HashMap<String, Integer> lastWriter = currentEdge.getLastWriter();
219 HashMap<String, String> lastValue = currentEdge.getLastValue();
220 HashMap<String, Integer> outSetVarMap = new HashMap<String, Integer>();
221 boolean isChanged = false;
223 for (Map.Entry mapElement : setSets.entrySet()) {
224 ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
226 for (int i = 0;i < setSet.size();i++) {
227 updatedVarNames.add(setSet.get(i).getVarName());
232 for (NameValuePair i : parentNode.getOutSet()) {
233 outSetVarMap.put(i.getVarName(), i.getAppNum());
234 if (!updatedVarNames.contains(i.getVarName()))
235 isChanged |= currentNode.getOutSet().add(i);
239 for (Map.Entry mapElement : setSets.entrySet()) {
240 ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
242 for (int i = 0;i < setSet.size();i++) {
243 String varName = setSet.get(i).getVarName();
244 Integer writer = lastWriter.get(varName);
245 String value = lastValue.get(varName);
247 if (setSet.get(i).getAppNum().equals(writer)
248 && setSet.get(i).getValue().equals(value)) {
249 if (outSetVarMap.containsKey(varName)) {
250 Integer hashCode = outSetVarMap.get(varName).hashCode() * 31 +
252 currentNode.getOutSet().remove(hashCode);
254 isChanged |= currentNode.getOutSet().add(setSet.get(i));
262 void updateTheEdge(Node currentNode, Transition transition) {
263 if (parentNode.getOutgoingEdges().containsKey(currentNode)) {
264 Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
265 if (currentEdge.getSetSetMap().containsKey(transition)) { // Update the transition
267 currentEdge.getSetSetMap().put(transition, tempSetSet);
269 currentEdge.getSetSetMap().get(transition).addAll(tempSetSet);
270 } else { // Add a new transition
271 currentEdge.getSetSetMap().put(transition, tempSetSet);
274 parentNode.getOutgoingEdges().put(currentNode, new Edge(parentNode, currentNode));
275 Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
276 currentEdge.getSetSetMap().put(transition, tempSetSet);
279 // Update the last writer and last value for this edge for each varName
280 Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
281 ArrayList<NameValuePair> setSet = currentEdge.getSetSetMap().get(transition);
282 for (int i = 0;i < setSet.size();i++) {
283 NameValuePair nameValuePair = setSet.get(i);
284 currentEdge.getLastWriter().put(nameValuePair.getVarName(), nameValuePair.getAppNum());
285 currentEdge.getLastValue().put(nameValuePair.getVarName(), nameValuePair.getValue());
293 HashSet<Node> predecessors = new HashSet<Node>();
294 HashSet<Node> successors = new HashSet<Node>();
295 HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
296 HashMap<Node, Edge> outgoingEdges = new HashMap<Node, Edge>();
306 HashSet<Node> getPredecessors() {
310 HashSet<Node> getSuccessors() {
314 HashSet<NameValuePair> getOutSet() {
318 HashMap<Node, Edge> getOutgoingEdges() {
319 return outgoingEdges;
324 Node source, destination;
325 HashMap<String, Integer> lastWriter = new HashMap<String, Integer>();
326 HashMap<String, String> lastValue = new HashMap<String, String>();
327 HashMap<Transition, ArrayList<NameValuePair>> setSetMap = new HashMap<Transition, ArrayList<NameValuePair>>();
329 Edge(Node source, Node destination) {
330 this.source = source;
331 this.destination = destination;
338 Node getDestination() {
342 HashMap<Transition, ArrayList<NameValuePair>> getSetSetMap() {
346 HashMap<String, Integer> getLastWriter() {
350 HashMap<String, String> getLastValue() {
355 static class NameValuePair {
361 NameValuePair(Integer appNum, String value, String varName, boolean isManual) {
362 this.appNum = appNum;
364 this.varName = varName;
365 this.isManual = isManual;
368 void setAppNum(Integer appNum) {
369 this.appNum = appNum;
372 void setValue(String value) {
376 void setVarName(String varName) {
377 this.varName = varName;
380 void setIsManual(String varName) {
381 this.isManual = isManual;
384 Integer getAppNum() {
392 String getVarName() {
396 boolean getIsManual() {
401 public boolean equals(Object o) {
402 if (o instanceof NameValuePair) {
403 NameValuePair other = (NameValuePair) o;
404 if (varName.equals(other.getVarName()))
405 return appNum.equals(other.getAppNum());
411 public int hashCode() {
412 return appNum.hashCode() * 31 + varName.hashCode();
417 public void stateRestored(Search search) {
418 id = search.getStateId();
419 depth = search.getDepth();
420 operation = "restored";
423 out.println("The state is restored to state with id: "+id+", depth: "+depth);
425 // Update the parent node
426 if (nodes.containsKey(id)) {
427 parentNode = nodes.get(id);
429 parentNode = new Node(id);
434 public void searchStarted(Search search) {
435 out.println("----------------------------------- search started");
440 public void stateAdvanced(Search search) {
441 String theEnd = null;
442 Transition transition = search.getTransition();
443 id = search.getStateId();
444 depth = search.getDepth();
445 operation = "forward";
447 // Add the node to the list of nodes
448 if (nodes.get(id) == null)
449 nodes.put(id, new Node(id));
451 Node currentNode = nodes.get(id);
453 // Update the edge based on the current transition
454 updateTheEdge(currentNode, transition);
456 // Reset the temporary variables and flags
457 tempSetSet = new ArrayList<NameValuePair>();
460 // Check for the conflict in this transition
461 conflictFound = checkForConflict(parentNode, currentNode, transition);
463 if (search.isNewState()) {
469 if (search.isEndState()) {
470 out.println("This is the last state!");
474 out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
476 // Updating the predecessors for this node
477 // Check if parent node is already in successors of the current node or not
478 if (!(currentNode.getPredecessors().contains(parentNode)))
479 currentNode.getPredecessors().add(parentNode);
481 // Update the successors for this node
482 // Check if current node is already in successors of the parent node or not
483 if (!(parentNode.getSuccessors().contains(currentNode)))
484 parentNode.getSuccessors().add(currentNode);
486 // Update the outset of the current node and check if it is changed or not to propagate the change
487 boolean isChanged = updateTheOutSet(parentNode, currentNode);
489 // Check if the outSet of this state has changed, update all of its successors' sets if any
491 for (Node node : currentNode.getSuccessors()) {
492 HashMap<Transition, ArrayList<NameValuePair>> setSets = currentNode.getOutgoingEdges().get(node).getSetSetMap();
493 for (Map.Entry mapElement : setSets.entrySet()) {
494 Transition currentTransition = (Transition)mapElement.getKey();
495 conflictFound = conflictFound || checkForConflict(currentNode, node, currentTransition);
498 conflictFound = conflictFound || propagateTheChange(currentNode);
500 // Update the parent node
501 if (nodes.containsKey(id)) {
502 parentNode = nodes.get(id);
504 parentNode = new Node(id);
509 public void stateBacktracked(Search search) {
510 id = search.getStateId();
511 depth = search.getDepth();
512 operation = "backtrack";
515 out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
517 // Update the parent node
518 if (nodes.containsKey(id)) {
519 parentNode = nodes.get(id);
521 parentNode = new Node(id);
526 public void searchFinished(Search search) {
527 out.println("----------------------------------- search finished");
530 private String getValue(ThreadInfo ti, Instruction inst, byte type) {
534 frame = ti.getTopFrame();
536 if ((inst instanceof JVMLocalVariableInstruction) ||
537 (inst instanceof JVMFieldInstruction))
539 if (frame.getTopPos() < 0)
543 hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
545 return(decodeValue(type, lo, hi));
548 if (inst instanceof JVMArrayElementInstruction)
549 return(getArrayValue(ti, type));
554 private final static String decodeValue(byte type, int lo, int hi) {
556 case Types.T_ARRAY: return(null);
557 case Types.T_VOID: return(null);
559 case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
560 case Types.T_BYTE: return(String.valueOf(lo));
561 case Types.T_CHAR: return(String.valueOf((char) lo));
562 case Types.T_DOUBLE: return(String.valueOf(Types.intsToDouble(lo, hi)));
563 case Types.T_FLOAT: return(String.valueOf(Types.intToFloat(lo)));
564 case Types.T_INT: return(String.valueOf(lo));
565 case Types.T_LONG: return(String.valueOf(Types.intsToLong(lo, hi)));
566 case Types.T_SHORT: return(String.valueOf(lo));
568 case Types.T_REFERENCE:
569 ElementInfo ei = VM.getVM().getHeap().get(lo);
573 ClassInfo ci = ei.getClassInfo();
577 if (ci.getName().equals("java.lang.String"))
578 return('"' + ei.asString() + '"');
580 return(ei.toString());
583 System.err.println("Unknown type: " + type);
588 private String getArrayValue(ThreadInfo ti, byte type) {
592 frame = ti.getTopFrame();
594 hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
596 return(decodeValue(type, lo, hi));
599 private byte getType(ThreadInfo ti, Instruction inst) {
604 frame = ti.getTopFrame();
605 if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
606 return (Types.T_REFERENCE);
611 if (inst instanceof JVMLocalVariableInstruction) {
612 type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
613 } else if (inst instanceof JVMFieldInstruction){
614 fi = ((JVMFieldInstruction) inst).getFieldInfo();
618 if (inst instanceof JVMArrayElementInstruction) {
619 return (getTypeFromInstruction(inst));
623 return (Types.T_VOID);
626 return (decodeType(type));
629 private final static byte getTypeFromInstruction(Instruction inst) {
630 if (inst instanceof JVMArrayElementInstruction)
631 return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
633 return(Types.T_VOID);
636 private final static byte decodeType(String type) {
637 if (type.charAt(0) == '?'){
638 return(Types.T_REFERENCE);
640 return Types.getBuiltinType(type);
644 // Find the variable writer
645 // It should be one of the apps listed in the .jpf file
646 private String getWriter(List<StackFrame> sfList, HashSet<String> writerSet) {
647 // Start looking from the top of the stack backward
648 for(int i=sfList.size()-1; i>=0; i--) {
649 MethodInfo mi = sfList.get(i).getMethodInfo();
650 if(!mi.isJPFInternal()) {
651 String method = mi.getStackTraceName();
652 // Check against the writers in the writerSet
653 for(String writer : writerSet) {
654 if (method.contains(writer)) {
664 private void writeWriterAndValue(String writer, String value, String var) {
665 // Update the temporary Set set.
666 NameValuePair temp = new NameValuePair(1, value, var, manual);
667 if (writer.equals("App2"))
668 temp = new NameValuePair(2, value, var, manual);
670 tempSetSet.add(temp);
674 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
676 if (System.currentTimeMillis() - startTime > timeout) {
677 StringBuilder sbTimeOut = new StringBuilder();
678 sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
679 Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString());
680 ti.setNextPC(nextIns);
685 StringBuilder sb = new StringBuilder();
686 sb.append(errorMessage);
687 Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
688 ti.setNextPC(nextIns);
690 if (conflictSet.contains(LOCATION_VAR)) {
691 MethodInfo mi = executedInsn.getMethodInfo();
692 // Find the last load before return and get the value here
693 if (mi.getName().equals(SET_LOCATION_METHOD) &&
694 executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) {
695 byte type = getType(ti, executedInsn);
696 String value = getValue(ti, executedInsn, type);
698 // Extract the writer app name
699 ClassInfo ci = mi.getClassInfo();
700 String writer = ci.getName();
702 // Update the temporary Set set.
703 writeWriterAndValue(writer, value, LOCATION_VAR);
706 if (executedInsn instanceof WriteInstruction) {
707 String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
709 for (String var : conflictSet) {
710 if (varId.contains(var)) {
712 byte type = getType(ti, executedInsn);
713 String value = getValue(ti, executedInsn, type);
714 String writer = getWriter(ti.getStack(), appSet);
715 // Just return if the writer is not one of the listed apps in the .jpf file
719 if (getWriter(ti.getStack(), manualSet) != null)
722 // Update the temporary Set set.
723 writeWriterAndValue(writer, value, var);