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 {
41 private final PrintWriter out;
42 private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
43 private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
44 private final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
45 private final DataSet tempSetSet = new DataSet(false, "NA", false, "NA");
46 volatile private Node parentNode = new Node(-2);
47 volatile private String operation;
48 volatile private String detail;
49 volatile private int depth;
50 volatile private int id;
51 volatile private boolean conflictFound = false;
52 volatile private boolean isSet = false;
53 Transition transition;
58 public ConflictTracker(Config conf, JPF jpf) {
59 out = new PrintWriter(System.out, true);
61 String[] conflictVars = conf.getStringArray("variables");
62 // We are not tracking anything if it is null
63 if (conflictVars != null) {
64 for (String var : conflictVars) {
68 String[] apps = conf.getStringArray("apps");
69 // We are not tracking anything if it is null
71 for (String var : apps) {
77 public void setOutSet(Node currentNode) {
78 DataList inSetApp1List = currentNode.getInSet().getApp1DataList(); //Store the app1List of inSet of current node to temp data set
79 DataList inSetApp2List = currentNode.getInSet().getApp2DataList(); //Store the app2List of inSet of current node to temp data set
80 DataList setSetApp1List = currentNode.getSetSet().getApp1DataList(); //Store the app1List of setSet of current node to temp data set
81 DataList setSetApp2List = currentNode.getSetSet().getApp2DataList(); //Store the app2List of setSet of current node to temp data set
82 DataSet outSetTemp = currentNode.getOutSet(); //Store the outSet of current node to temp data set
84 if ((setSetApp1List.getAppSet())&&(setSetApp2List.getAppSet())) {
85 //App1 & App2 are writers
86 outSetTemp.setApp1DataList(setSetApp1List.getAppSet(), setSetApp1List.getValue());
87 outSetTemp.setApp2DataList(setSetApp2List.getAppSet(), setSetApp2List.getValue());
88 } else if (setSetApp2List.getAppSet()) {
90 outSetTemp.setApp1DataList(setSetApp1List.getAppSet(), setSetApp1List.getValue());
91 outSetTemp.setApp2DataList(inSetApp2List.getAppSet(), inSetApp2List.getValue());
92 } else if (setSetApp2List.getAppSet()) {
94 outSetTemp.setApp1DataList(inSetApp1List.getAppSet(),inSetApp1List.getValue());
95 outSetTemp.setApp2DataList(setSetApp2List.getAppSet(), setSetApp2List.getValue());
97 //No writer for this node => outSet = inSet
98 outSetTemp.setApp1DataList(inSetApp1List.getAppSet(), inSetApp1List.getValue());
99 outSetTemp.setApp2DataList(inSetApp2List.getAppSet(), inSetApp2List.getValue());
103 public void setInSet(Node currentNode) {
104 for (Node i : currentNode.getPredecessors()) {
105 //Check to see if dataList1 of predNode(i) is valid or not: if valid get its value
106 if (i.getOutSet().getApp1DataList().getAppSet()) {
107 currentNode.getInSet().setApp1DataList(true, i.getOutSet().getApp1DataList().getValue());
110 //Check to see if dataList2 of predNode(i) is valid or not: if valid get its value
111 if (i.getOutSet().getApp2DataList().getAppSet()) {
112 currentNode.getInSet().setApp2DataList(true, i.getOutSet().getApp2DataList().getValue());
117 boolean checkOutSetChange(Node currentNode, DataSet tempOutSet) {
118 DataList outSetApp1List = currentNode.getOutSet().getApp1DataList(); //Store the app1List of inSet of current node to temp data set
119 DataList outSetApp2List = currentNode.getOutSet().getApp2DataList(); //Store the app2List of inSet of current node to temp data set
120 DataList tempSetApp1List = tempOutSet.getApp1DataList(); //Store the app1List of tempOutSet of current node to temp data set
121 DataList tempSetApp2List = tempOutSet.getApp2DataList(); //Store the app1List of tempOutSet of current node to temp data set
123 //Return 1 if the outSet has changed!
124 return ((outSetApp1List.getAppSet() != tempSetApp1List.getAppSet())||
125 !(outSetApp1List.getValue().equals(tempSetApp1List.getValue()))||
126 (outSetApp2List.getAppSet() != tempSetApp2List.getAppSet())||
127 !(outSetApp2List.getValue().equals(tempSetApp2List.getValue())));
130 public void checkForConflict(Node currentNode) {
131 DataList outSetApp1List = currentNode.getOutSet().getApp1DataList(); //Store the app1List of inSet of current node to temp data set
132 DataList outSetApp2List = currentNode.getOutSet().getApp2DataList(); //Store the app2List of inSet of current node to temp data set
134 if ((outSetApp1List.getAppSet() == true)&&(outSetApp2List.getAppSet() == true)) {
135 //Both apps have set the device
136 if (!(outSetApp1List.getValue().equals(outSetApp2List.getValue()))) {
137 //Values set by the apps are not the same, and we have a conflict!
138 conflictFound = true;
145 ArrayList<Node> predecessors = new ArrayList<Node>();
146 ArrayList<Node> successors = new ArrayList<Node>();
147 DataSet inSet = new DataSet(false, "NA", false, "NA");
148 DataSet setSet = new DataSet(false, "NA", false, "NA");
149 DataSet outSet = new DataSet(false, "NA", false, "NA");
155 void addPredecessor(Node node) {
156 predecessors.add(node);
159 void addSuccessor(Node node) {
160 successors.add(node);
164 this.inSet = new DataSet(false, "NA", false, "NA");
167 void setInSet(DataSet inSet) {
168 this.inSet.setApp1DataList(inSet.getApp1DataList().getAppSet(), inSet.getApp1DataList().getValue());
169 this.inSet.setApp2DataList(inSet.getApp2DataList().getAppSet(), inSet.getApp2DataList().getValue());
172 void setSetSet(DataSet setSet) {
173 this.setSet.setApp1DataList(setSet.getApp1DataList().getAppSet(), setSet.getApp1DataList().getValue());
174 this.setSet.setApp2DataList(setSet.getApp2DataList().getAppSet(), setSet.getApp2DataList().getValue());
177 void setOutSet(DataSet outSet) {
178 this.outSet.setApp1DataList(outSet.getApp1DataList().getAppSet(), outSet.getApp1DataList().getValue());
179 this.outSet.setApp2DataList(outSet.getApp2DataList().getAppSet(), outSet.getApp2DataList().getValue());
186 ArrayList<Node> getPredecessors() {
190 ArrayList<Node> getSuccessors() {
198 DataSet getOutSet() {
202 DataSet getSetSet() {
211 DataList(boolean appSet, String value) {
212 this.appSet = appSet;
216 void setAppSet(boolean appSet) {
217 this.appSet = appSet;
220 void setValue(String value) {
224 boolean getAppSet() {
234 DataList app1DataList = new DataList(false, "NA");
235 DataList app2DataList = new DataList(false, "NA");
237 DataSet(boolean app1Set, String app1Value, boolean app2Set, String app2Value) {
238 app1DataList.setAppSet(app1Set);
239 app1DataList.setValue(app1Value);
240 app2DataList.setAppSet(app2Set);
241 app2DataList.setValue(app2Value);
244 void setApp1DataList(boolean appSet, String value) {
245 app1DataList.setAppSet(appSet);
246 app1DataList.setValue(value);
249 void setApp2DataList(boolean appSet, String value) {
250 app2DataList.setAppSet(appSet);
251 app2DataList.setValue(value);
254 DataList getApp1DataList() {
258 DataList getApp2DataList() {
264 public void stateRestored(Search search) {
265 id = search.getStateId();
266 depth = search.getDepth();
267 operation = "restored";
270 out.println("The state is restored to state with id: "+id+", depth: "+depth);
272 //Update the parent node
273 parentNode = new Node(id);
277 public void searchStarted(Search search) {
278 out.println("----------------------------------- search started");
283 public void stateAdvanced(Search search) {
284 String theEnd = null;
285 id = search.getStateId();
286 depth = search.getDepth();
287 operation = "forward";
289 //Add the node to the list of nodes
290 nodes.put(id, new Node(id));
291 Node currentNode = nodes.get(id);
293 if (search.isNewState()) {
296 //Update the setSet for this new node
298 currentNode.setSetSet(tempSetSet);
305 if (search.isEndState()) {
306 out.println("This is the last state!");
310 out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
312 //Updating the predecessors for this node
313 //Check if parent node is already in successors of the current node or not
314 if (!(currentNode.getPredecessors().contains(parentNode)))
315 currentNode.addPredecessor(parentNode);
317 //Update the successors for this node
318 //Check if current node is already in successors of the parent node or not
319 if (!(parentNode.getSuccessors().contains(currentNode)))
320 parentNode.addSuccessor(currentNode);
323 //Set the input set of this state to empty
324 currentNode.emptyInSet();
327 //Store the out set of this state to the temporary data set
328 DataSet tempOutSet = new DataSet(currentNode.getOutSet().getApp1DataList().getAppSet(),
329 currentNode.getOutSet().getApp1DataList().getValue(),
330 currentNode.getOutSet().getApp2DataList().getAppSet(),
331 currentNode.getOutSet().getApp2DataList().getValue());
334 //Set input set according to output set of pred states of current state
335 setInSet(currentNode);
339 //Set dataLists of outSet to dataLists of setSet if it is valid, otherwise to dataLists of inSet
340 setOutSet(currentNode);
343 //Check for a conflict
344 checkForConflict(currentNode);
348 //Check if the outSet of this state has changed, update all of its successors' sets if any
349 if (checkOutSetChange(currentNode, tempOutSet)) {
350 ArrayList<Node> changed = new ArrayList<Node>(currentNode.getSuccessors());
351 while(!changed.isEmpty()) {
352 //Get a random node inside the changed list and remove it from the list
353 Integer rnd = new Random().nextInt(changed.size());
354 Node nodeToProcess = changed.get(rnd);
355 changed.remove(nodeToProcess);
357 //Initialize the empty input set for current node
358 nodeToProcess.emptyInSet();
360 //Store the out set of this state to the temporary data set
361 tempOutSet = new DataSet(nodeToProcess.getOutSet().getApp1DataList().getAppSet(),
362 nodeToProcess.getOutSet().getApp1DataList().getValue(),
363 nodeToProcess.getOutSet().getApp2DataList().getAppSet(),
364 nodeToProcess.getOutSet().getApp2DataList().getValue());
367 //Set input set according to output set of pred states of current state
368 setInSet(nodeToProcess);
371 //Set outSet to setSet if it is valid, otherwise to inSet
372 setOutSet(nodeToProcess);
375 //Checking if the out set has changed or not(Add its successors to the change list!)
376 if (checkOutSetChange(nodeToProcess, tempOutSet)) {
377 for (Node i : nodeToProcess.getSuccessors()) {
378 if (!changed.contains(i))
385 //Update the parent node
386 parentNode = new Node(id);
391 public void stateBacktracked(Search search) {
392 id = search.getStateId();
393 depth = search.getDepth();
394 operation = "backtrack";
397 out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
399 //Update the parent node
400 parentNode = new Node(id);
404 public void searchFinished(Search search) {
405 out.println("----------------------------------- search finished");
408 private String getValue(ThreadInfo ti, Instruction inst, byte type) {
412 frame = ti.getTopFrame();
414 if ((inst instanceof JVMLocalVariableInstruction) ||
415 (inst instanceof JVMFieldInstruction))
417 if (frame.getTopPos() < 0)
421 hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
423 return(decodeValue(type, lo, hi));
426 if (inst instanceof JVMArrayElementInstruction)
427 return(getArrayValue(ti, type));
432 private final static String decodeValue(byte type, int lo, int hi) {
434 case Types.T_ARRAY: return(null);
435 case Types.T_VOID: return(null);
437 case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
438 case Types.T_BYTE: return(String.valueOf(lo));
439 case Types.T_CHAR: return(String.valueOf((char) lo));
440 case Types.T_DOUBLE: return(String.valueOf(Types.intsToDouble(lo, hi)));
441 case Types.T_FLOAT: return(String.valueOf(Types.intToFloat(lo)));
442 case Types.T_INT: return(String.valueOf(lo));
443 case Types.T_LONG: return(String.valueOf(Types.intsToLong(lo, hi)));
444 case Types.T_SHORT: return(String.valueOf(lo));
446 case Types.T_REFERENCE:
447 ElementInfo ei = VM.getVM().getHeap().get(lo);
451 ClassInfo ci = ei.getClassInfo();
455 if (ci.getName().equals("java.lang.String"))
456 return('"' + ei.asString() + '"');
458 return(ei.toString());
461 System.err.println("Unknown type: " + type);
466 private String getArrayValue(ThreadInfo ti, byte type) {
470 frame = ti.getTopFrame();
472 hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
474 return(decodeValue(type, lo, hi));
477 private byte getType(ThreadInfo ti, Instruction inst) {
482 frame = ti.getTopFrame();
483 if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
484 return (Types.T_REFERENCE);
489 if (inst instanceof JVMLocalVariableInstruction) {
490 type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
491 } else if (inst instanceof JVMFieldInstruction){
492 fi = ((JVMFieldInstruction) inst).getFieldInfo();
496 if (inst instanceof JVMArrayElementInstruction) {
497 return (getTypeFromInstruction(inst));
501 return (Types.T_VOID);
504 return (decodeType(type));
507 private final static byte getTypeFromInstruction(Instruction inst) {
508 if (inst instanceof JVMArrayElementInstruction)
509 return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
511 return(Types.T_VOID);
514 private final static byte decodeType(String type) {
515 if (type.charAt(0) == '?'){
516 return(Types.T_REFERENCE);
518 return Types.getBuiltinType(type);
522 // Find the variable writer
523 // It should be one of the apps listed in the .jpf file
524 private String getWriter(List<StackFrame> sfList) {
525 // Start looking from the top of the stack backward
526 for(int i=sfList.size()-1; i>=0; i--) {
527 MethodInfo mi = sfList.get(i).getMethodInfo();
528 if(!mi.isJPFInternal()) {
529 String method = mi.getStackTraceName();
530 // Check against the apps in the appSet
531 for(String app : appSet) {
532 // There is only one writer at a time but we need to always
533 // check all the potential writers in the list
534 if (method.contains(app)) {
545 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
547 StringBuilder sb = new StringBuilder();
548 sb.append("Conflict found between two apps!");
549 Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
550 ti.setNextPC(nextIns);
551 } else if (executedInsn instanceof WriteInstruction) {
552 String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
553 for(String var : conflictSet) {
555 if (varId.contains(var)) {
557 byte type = getType(ti, executedInsn);
558 String value = getValue(ti, executedInsn, type);
559 String writer = getWriter(ti.getStack());
560 // Just return if the writer is not one of the listed apps in the .jpf file
564 //Update the temporary Set set.
565 if (writer.equals("App1"))
566 tempSetSet.setApp1DataList(true, value);
567 else if (writer.equals("App2"))
568 tempSetSet.setApp2DataList(true, value);