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 if ((currentNode.getSetSet().getDataList1().getAppSet())&&(currentNode.getSetSet().getDataList2().getAppSet())) { //App1 & App2 are writers
79 currentNode.getOutSet().setDataList1(currentNode.getSetSet().getDataList1().getAppSet(), currentNode.getSetSet().getDataList1().getValue());
80 currentNode.getOutSet().setDataList2(currentNode.getSetSet().getDataList2().getAppSet(), currentNode.getSetSet().getDataList2().getValue());
81 } else if (currentNode.getSetSet().getDataList1().getAppSet()) { //App1 is a writer
82 currentNode.getOutSet().setDataList1(currentNode.getSetSet().getDataList1().getAppSet(), currentNode.getSetSet().getDataList1().getValue());
83 currentNode.getOutSet().setDataList2(currentNode.getInSet().getDataList2().getAppSet(), currentNode.getInSet().getDataList2().getValue());
84 } else if (currentNode.getSetSet().getDataList2().getAppSet()) { //App2 is a writer
85 currentNode.getOutSet().setDataList1(currentNode.getInSet().getDataList1().getAppSet(), currentNode.getInSet().getDataList1().getValue());
86 currentNode.getOutSet().setDataList2(currentNode.getSetSet().getDataList2().getAppSet(), currentNode.getSetSet().getDataList2().getValue());
87 } else { //No writer for this node => outSet = inSet
88 currentNode.getOutSet().setDataList1(currentNode.getInSet().getDataList1().getAppSet(), currentNode.getInSet().getDataList1().getValue());
89 currentNode.getOutSet().setDataList2(currentNode.getInSet().getDataList2().getAppSet(), currentNode.getInSet().getDataList2().getValue());
93 public void setInSet(Node currentNode) {
94 for (Node i : currentNode.getPredecessors()) {
95 //Check to see if dataList1 of predNode(i) is valid or not: if valid get its value
96 if (i.getOutSet().getDataList1().getAppSet()) {
97 currentNode.getInSet().setDataList1(true, i.getOutSet().getDataList1().getValue());
100 //Check to see if dataList2 of predNode(i) is valid or not: if valid get its value
101 if (i.getOutSet().getDataList2().getAppSet()) {
102 currentNode.getInSet().setDataList2(true, i.getOutSet().getDataList2().getValue());
107 boolean checkOutSetChange(Node currentNode, DataSet tempOutSet) {
108 return ((currentNode.getOutSet().getDataList1().getAppSet() != tempOutSet.getDataList1().getAppSet())||
109 !(currentNode.getOutSet().getDataList1().getValue().equals(tempOutSet.getDataList1().getValue()))||
110 (currentNode.getOutSet().getDataList2().getAppSet() != tempOutSet.getDataList2().getAppSet())||
111 !(currentNode.getOutSet().getDataList2().getValue().equals(tempOutSet.getDataList2().getValue())));
114 public void checkForConflict(Node currentNode) {
115 if ((currentNode.getOutSet().getDataList1().getAppSet() == true)&&(currentNode.getOutSet().getDataList2().getAppSet() == true)) { //Both apps have set the device
116 if (!(currentNode.getOutSet().getDataList1().getValue().equals(currentNode.getOutSet().getDataList2().getValue()))) //Values set by the apps are not the same, and we have a conflict!
117 conflictFound = true;
123 ArrayList<Node> predecessors = new ArrayList<Node>();
124 ArrayList<Node> successors = new ArrayList<Node>();
125 DataSet inSet = new DataSet(false, "NA", false, "NA");
126 DataSet setSet = new DataSet(false, "NA", false, "NA");
127 DataSet outSet = new DataSet(false, "NA", false, "NA");
133 void addPredecessor(Node node) {
134 predecessors.add(node);
137 void addSuccessor(Node node) {
138 successors.add(node);
142 this.inSet = new DataSet(false, "NA", false, "NA");
145 void setInSet(DataSet inSet) {
146 this.inSet.setDataList1(inSet.getDataList1().getAppSet(), inSet.getDataList1().getValue());
147 this.inSet.setDataList2(inSet.getDataList2().getAppSet(), inSet.getDataList2().getValue());
150 void setSetSet(DataSet setSet) {
151 this.setSet.setDataList1(setSet.getDataList1().getAppSet(), setSet.getDataList1().getValue());
152 this.setSet.setDataList2(setSet.getDataList2().getAppSet(), setSet.getDataList2().getValue());
155 void setOutSet(DataSet outSet) {
156 this.outSet.setDataList1(outSet.getDataList1().getAppSet(), outSet.getDataList1().getValue());
157 this.outSet.setDataList2(outSet.getDataList2().getAppSet(), outSet.getDataList2().getValue());
164 ArrayList<Node> getPredecessors() {
168 ArrayList<Node> getSuccessors() {
176 DataSet getOutSet() {
180 DataSet getSetSet() {
189 DataList(boolean appSet, String value) {
190 this.appSet = appSet;
194 void setAppSet(boolean appSet) {
195 this.appSet = appSet;
198 void setValue(String value) {
202 boolean getAppSet() {
212 DataList dataList1 = new DataList(false, "NA");
213 DataList dataList2 = new DataList(false, "NA");
215 DataSet(boolean appSet1, String value1, boolean appSet2, String value2) {
216 dataList1.setAppSet(appSet1);
217 dataList1.setValue(value1);
218 dataList2.setAppSet(appSet2);
219 dataList2.setValue(value2);
222 void setDataList1(boolean appSet, String value) {
223 dataList1.setAppSet(appSet);
224 dataList1.setValue(value);
227 void setDataList2(boolean appSet, String value) {
228 dataList2.setAppSet(appSet);
229 dataList2.setValue(value);
232 DataList getDataList1() {
236 DataList getDataList2() {
242 public void stateRestored(Search search) {
243 id = search.getStateId();
244 depth = search.getDepth();
245 operation = "restored";
248 out.println("The state is restored to state with id: "+id+", depth: "+depth);
250 //Update the parent node
251 parentNode = new Node(id);
255 public void searchStarted(Search search) {
256 out.println("----------------------------------- search started");
261 public void stateAdvanced(Search search) {
262 String theEnd = null;
263 id = search.getStateId();
264 depth = search.getDepth();
265 operation = "forward";
267 //Add the node to the list of nodes
268 nodes.put(id, new Node(id));
269 Node currentNode = nodes.get(id);
271 if (search.isNewState()) {
274 //Update the setSet for this new node
276 currentNode.setSetSet(tempSetSet);
283 if (search.isEndState()) {
284 out.println("This is the last state!");
288 out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
290 //Updating the predecessors for this node
291 //Check if parent node is already in successors of the current node or not
292 if (!(currentNode.getPredecessors().contains(parentNode)))
293 currentNode.addPredecessor(parentNode);
295 //Update the successors for this node
296 //Check if current node is already in successors of the parent node or not
297 if (!(parentNode.getSuccessors().contains(currentNode)))
298 parentNode.addSuccessor(currentNode);
301 //Set the input set of this state to empty
302 currentNode.emptyInSet();
305 //Store the out set of this state to the temporary data set
306 DataSet tempOutSet = new DataSet(currentNode.getOutSet().getDataList1().getAppSet(),
307 currentNode.getOutSet().getDataList1().getValue(),
308 currentNode.getOutSet().getDataList2().getAppSet(),
309 currentNode.getOutSet().getDataList2().getValue());
312 //Set input set according to output set of pred states of current state
313 setInSet(currentNode);
317 //Set dataLists of outSet to dataLists of setSet if it is valid, otherwise to dataLists of inSet
318 setOutSet(currentNode);
321 //Check for a conflict
322 checkForConflict(currentNode);
326 //Check if the outSet of this state has changed, update all of its successors' sets if any
327 if (checkOutSetChange(currentNode, tempOutSet)) {
328 ArrayList<Node> changed = new ArrayList<Node>(currentNode.getSuccessors());
329 while(!changed.isEmpty()) {
330 //Get a random node inside the changed list and remove it from the list
331 Integer rnd = new Random().nextInt(changed.size());
332 Node nodeToProcess = changed.get(rnd);
333 changed.remove(nodeToProcess);
335 //Initialize the empty input set for current node
336 nodeToProcess.emptyInSet();
338 //Store the out set of this state to the temporary data set
339 tempOutSet = new DataSet(nodeToProcess.getOutSet().getDataList1().getAppSet(),
340 nodeToProcess.getOutSet().getDataList1().getValue(),
341 nodeToProcess.getOutSet().getDataList2().getAppSet(),
342 nodeToProcess.getOutSet().getDataList2().getValue());
345 //Set input set according to output set of pred states of current state
346 setInSet(nodeToProcess);
349 //Set outSet to setSet if it is valid, otherwise to inSet
350 setOutSet(nodeToProcess);
353 //Checking if the out set has changed or not(Add its successors to the change list!)
354 if (checkOutSetChange(nodeToProcess, tempOutSet)) {
355 for (Node i : nodeToProcess.getSuccessors()) {
356 if (!changed.contains(i))
363 //Update the parent node
364 parentNode = new Node(id);
369 public void stateBacktracked(Search search) {
370 id = search.getStateId();
371 depth = search.getDepth();
372 operation = "backtrack";
375 out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
377 //Update the parent node
378 parentNode = new Node(id);
382 public void searchFinished(Search search) {
383 out.println("----------------------------------- search finished");
386 private String getValue(ThreadInfo ti, Instruction inst, byte type) {
390 frame = ti.getTopFrame();
392 if ((inst instanceof JVMLocalVariableInstruction) ||
393 (inst instanceof JVMFieldInstruction))
395 if (frame.getTopPos() < 0)
399 hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
401 return(decodeValue(type, lo, hi));
404 if (inst instanceof JVMArrayElementInstruction)
405 return(getArrayValue(ti, type));
410 private final static String decodeValue(byte type, int lo, int hi) {
412 case Types.T_ARRAY: return(null);
413 case Types.T_VOID: return(null);
415 case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
416 case Types.T_BYTE: return(String.valueOf(lo));
417 case Types.T_CHAR: return(String.valueOf((char) lo));
418 case Types.T_DOUBLE: return(String.valueOf(Types.intsToDouble(lo, hi)));
419 case Types.T_FLOAT: return(String.valueOf(Types.intToFloat(lo)));
420 case Types.T_INT: return(String.valueOf(lo));
421 case Types.T_LONG: return(String.valueOf(Types.intsToLong(lo, hi)));
422 case Types.T_SHORT: return(String.valueOf(lo));
424 case Types.T_REFERENCE:
425 ElementInfo ei = VM.getVM().getHeap().get(lo);
429 ClassInfo ci = ei.getClassInfo();
433 if (ci.getName().equals("java.lang.String"))
434 return('"' + ei.asString() + '"');
436 return(ei.toString());
439 System.err.println("Unknown type: " + type);
444 private String getArrayValue(ThreadInfo ti, byte type) {
448 frame = ti.getTopFrame();
450 hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
452 return(decodeValue(type, lo, hi));
455 private byte getType(ThreadInfo ti, Instruction inst) {
460 frame = ti.getTopFrame();
461 if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
462 return (Types.T_REFERENCE);
467 if (inst instanceof JVMLocalVariableInstruction) {
468 type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
469 } else if (inst instanceof JVMFieldInstruction){
470 fi = ((JVMFieldInstruction) inst).getFieldInfo();
474 if (inst instanceof JVMArrayElementInstruction) {
475 return (getTypeFromInstruction(inst));
479 return (Types.T_VOID);
482 return (decodeType(type));
485 private final static byte getTypeFromInstruction(Instruction inst) {
486 if (inst instanceof JVMArrayElementInstruction)
487 return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
489 return(Types.T_VOID);
492 private final static byte decodeType(String type) {
493 if (type.charAt(0) == '?'){
494 return(Types.T_REFERENCE);
496 return Types.getBuiltinType(type);
500 // Find the variable writer
501 // It should be one of the apps listed in the .jpf file
502 private String getWriter(List<StackFrame> sfList) {
503 // Start looking from the top of the stack backward
504 for(int i=sfList.size()-1; i>=0; i--) {
505 MethodInfo mi = sfList.get(i).getMethodInfo();
506 if(!mi.isJPFInternal()) {
507 String method = mi.getStackTraceName();
508 // Check against the apps in the appSet
509 for(String app : appSet) {
510 // There is only one writer at a time but we need to always
511 // check all the potential writers in the list
512 if (method.contains(app)) {
523 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
525 StringBuilder sb = new StringBuilder();
526 sb.append("Conflict found between two apps!");
527 Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
528 ti.setNextPC(nextIns);
529 } else if (executedInsn instanceof WriteInstruction) {
530 String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
531 for(String var : conflictSet) {
533 if (varId.contains(var)) {
535 byte type = getType(ti, executedInsn);
536 String value = getValue(ti, executedInsn, type);
537 String writer = getWriter(ti.getStack());
538 // Just return if the writer is not one of the listed apps in the .jpf file
542 //Update the temporary Set set.
543 if (writer.equals("App1"))
544 tempSetSet.setDataList1(true, value);
545 else if (writer.equals("App2"))
546 tempSetSet.setDataList2(true, value);