src/main/gov/nasa/jpf/listener/ConflictTracker.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   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
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  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.
  17  */
  18 package gov.nasa.jpf.listener;
  19
  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;
  30
  31 import java.io.PrintWriter;
  32
  33 import java.util.*;
  34
  35 /**
  36  * Listener using data flow analysis to find conflicts between smartApps.
  37  **/
  38
  39 public class ConflictTracker extends ListenerAdapter {
  40
  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 HashSet<String> manualSet = new HashSet<String>(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions
  45   private final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
  46   private HashSet<NameValuePair> tempSetSet = new HashSet<NameValuePair>();
  47   private long timeout;
  48   private long startTime;
  49   private Node parentNode = new Node(-2);
  50   private String operation;
  51   private String detail;
  52   private String errorMessage;
  53   private int depth;
  54   private int id;
  55   private boolean conflictFound = false;
  56   private boolean isSet = false;
  57   private boolean manual = false;
  58
  59   private final String SET_LOCATION_METHOD = "setLocationMode";
  60   private final String LOCATION_VAR = "locationMode";
  61
  62   public ConflictTracker(Config config, JPF jpf) {
  63     out = new PrintWriter(System.out, true);
  64
  65     String[] conflictVars = config.getStringArray("variables");
  66     // We are not tracking anything if it is null
  67     if (conflictVars != null) {
  68       for (String var : conflictVars) {
  69         conflictSet.add(var);
  70       }
  71     }
  72     String[] apps = config.getStringArray("apps");
  73     // We are not tracking anything if it is null
  74     if (apps != null) {
  75       for (String var : apps) {
  76         appSet.add(var);
  77       }
  78     }
  79     String[] manualClasses = config.getStringArray("manualClasses");
  80     // We are not tracking anything if it is null
  81     if (manualClasses != null) {
  82       for (String var : manualClasses) {
  83         manualSet.add(var);
  84       }
  85     }
  86
  87     // Timeout input from config is in minutes, so we need to convert into millis
  88     timeout = config.getInt("timeout", 0) * 60 * 1000;
  89     startTime = System.currentTimeMillis();
  90   }
  91
  92   boolean propagateTheChange(Node currentNode) {
  93         HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
  94
  95         while(!changed.isEmpty()) {
  96                 // Get the first element of HashSet and remove it from the changed set
  97                 Node nodeToProcess = changed.iterator().next();
  98                 changed.remove(nodeToProcess);
  99
 100                 // Update the edge
 101                 boolean isChanged = updateEdge(currentNode, nodeToProcess);
 102
 103                 // Check for a conflict in this transition(currentNode -> nodeToProcess)
 104                 if (checkForConflict(currentNode))
 105                         return true;
 106
 107                 // Checking if the out set has changed or not(Add its successors to the change list!)
 108                 if (isChanged) {
 109                         for (Node i : nodeToProcess.getSuccessors()) {
 110                                 if (!changed.contains(i))
 111                                         changed.add(i);
 112                         }
 113                 }
 114       }
 115
 116       return false;
 117   }
 118
 119   String createErrorMessage(NameValuePair pair, HashMap<String, String> valueMap, HashMap<String, Integer> writerMap) {
 120         String message = "Conflict found between the two apps. App"+pair.getAppNum()+
 121                          " has written the value: "+pair.getValue()+
 122                          " to the variable: "+pair.getVarName()+" while App"+
 123                          writerMap.get(pair.getVarName())+" is overwriting the value: "
 124                          +valueMap.get(pair.getVarName())+" to the same variable!";
 125         return message;
 126   }
 127
 128   boolean checkForConflict(Node nodeToProcess) {
 129         HashMap<String, String> valueMap = new HashMap<String, String>(); // HashMap from varName to value
 130         HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); // HashMap from varName to appNum
 131
 132         // Update the valueMap and check if we have conflict in the setSet
 133         for (NameValuePair i : nodeToProcess.getSetSet()) {
 134                 if (i.getIsManual()) // Manual input: we have no conflict
 135                         continue; // If this manual write is the last write, this is actually a break
 136
 137                 if (valueMap.containsKey(i.getVarName())) {
 138                         if (!valueMap.get(i.getVarName()).equals(i.getValue())) { // Check if their value is different we have a conflict
 139                                 errorMessage = createErrorMessage(i, valueMap, writerMap);
 140                                 return true;
 141                         }
 142                         else // We have two writers writing the same value
 143                                 writerMap.put(i.getVarName(), i.getAppNum()+writerMap.get(i.getVarName()));
 144                 } else {
 145                         valueMap.put(i.getVarName(), i.getValue());
 146                         writerMap.put(i.getVarName(), i.getAppNum());
 147                 }
 148         }
 149
 150         // Comparing the outSet to setSet
 151         for (NameValuePair i : nodeToProcess.getOutSet()) {
 152                 if (valueMap.containsKey(i.getVarName())) {
 153                         String value = valueMap.get(i.getVarName());
 154                         Integer writer = writerMap.get(i.getVarName());
 155                         if ((value != null)&&(writer != null)) {
 156                                 if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { // We have different values
 157                                         errorMessage = createErrorMessage(i, valueMap, writerMap);
 158                                         return true;
 159                                 }
 160                         }
 161                 }
 162         }
 163
 164         return false;
 165   }
 166
 167   boolean updateEdge(Node parentNode, Node currentNode) {
 168         HashSet<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
 169         HashSet<String> updatedVarNames = new HashSet<String>();
 170         HashMap<String, Integer> lastWriter = new HashMap<String, Integer>(); // Store the last writer of each variable
 171         boolean isChanged = false;
 172
 173         for (NameValuePair i : setSet) {
 174                 updatedVarNames.add(i.getVarName());
 175                 lastWriter.put(i.getVarName(), i.getAppNum());
 176         }
 177
 178         for (NameValuePair i : parentNode.getOutSet()) {
 179                 if (!updatedVarNames.contains(i.getVarName()))
 180                         isChanged |= currentNode.getOutSet().add(i);
 181         }
 182
 183         for (NameValuePair i : setSet) {
 184                 if (i.getAppNum().equals(lastWriter.get(i.getVarName()))) // Add the last writer of each variable to outSet
 185                         isChanged |= currentNode.getOutSet().add(i);
 186         }
 187
 188         return isChanged;
 189   }
 190
 191   static class Node {
 192         Integer id;
 193         HashSet<Node> predecessors = new HashSet<Node>();
 194         HashSet<Node> successors = new HashSet<Node>();
 195         HashSet<NameValuePair> setSet = new HashSet<NameValuePair>();
 196         HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
 197         HashMap<Node, HashSet<NameValuePair>> setSetMap = new HashMap<Node, HashSet<NameValuePair>>();
 198
 199
 200         Node(Integer id) {
 201                 this.id = id;
 202         }
 203
 204         void addPredecessor(Node node) {
 205                 predecessors.add(node);
 206         }
 207
 208         void addSuccessor(Node node) {
 209                 successors.add(node);
 210         }
 211
 212         void setSetSet(HashSet<NameValuePair> setSet, boolean isManual) {
 213               if (isManual)
 214                 this.setSet = new HashSet<NameValuePair>();
 215               for (NameValuePair i : setSet) {
 216                 this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual()));
 217               }
 218         }
 219
 220         Integer getId() {
 221                 return id;
 222         }
 223
 224         HashSet<Node> getPredecessors() {
 225                 return predecessors;
 226         }
 227
 228         HashSet<Node> getSuccessors() {
 229                 return successors;
 230         }
 231
 232         HashSet<NameValuePair> getSetSet() {
 233                 return setSet;
 234         }
 235
 236         HashSet<NameValuePair> getOutSet() {
 237                 return outSet;
 238         }
 239
 240         HashMap<Node, HashSet<NameValuePair>> getSetSetMap() {
 241                 return setSetMap;
 242         }
 243   }
 244
 245   static class NameValuePair {
 246         Integer appNum;
 247         String value;
 248         String varName;
 249         boolean isManual;
 250
 251         NameValuePair(Integer appNum, String value, String varName, boolean isManual) {
 252                 this.appNum = appNum;
 253                 this.value = value;
 254                 this.varName = varName;
 255                 this.isManual = isManual;
 256         }
 257
 258         void setAppNum(Integer appNum) {
 259                 this.appNum = appNum;
 260         }
 261
 262         void setValue(String value) {
 263                 this.value = value;
 264         }
 265
 266         void setVarName(String varName) {
 267                 this.varName = varName;
 268         }
 269
 270     void setIsManual(String varName) {
 271                 this.isManual = isManual;
 272         }
 273
 274         Integer getAppNum() {
 275                 return appNum;
 276         }
 277
 278         String getValue() {
 279                 return value;
 280         }
 281
 282         String getVarName() {
 283                 return varName;
 284         }
 285
 286         boolean getIsManual() {
 287                 return isManual;
 288         }
 289
 290         @Override
 291         public boolean equals(Object o) {
 292       if (o instanceof NameValuePair) {
 293         NameValuePair other = (NameValuePair) o;
 294         if (varName.equals(other.getVarName()))
 295           return appNum.equals(other.getAppNum());
 296       }
 297       return false;
 298         }
 299
 300         @Override
 301         public int hashCode() {
 302                 return appNum.hashCode() * 31 + varName.hashCode();
 303         }
 304   }
 305
 306   @Override
 307   public void stateRestored(Search search) {
 308     id = search.getStateId();
 309     depth = search.getDepth();
 310     operation = "restored";
 311     detail = null;
 312
 313     out.println("The state is restored to state with id: "+id+", depth: "+depth);
 314
 315     // Update the parent node
 316     if (nodes.containsKey(id)) {
 317           parentNode = nodes.get(id);
 318     } else {
 319           parentNode = new Node(id);
 320     }
 321   }
 322
 323   @Override
 324   public void searchStarted(Search search) {
 325     out.println("----------------------------------- search started");
 326   }
 327
 328
 329   @Override
 330   public void stateAdvanced(Search search) {
 331     String theEnd = null;
 332     id = search.getStateId();
 333     depth = search.getDepth();
 334     operation = "forward";
 335
 336     // Check for the conflict in this new transition
 337     conflictFound = checkForConflict(parentNode);
 338
 339     // Add the node to the list of nodes
 340     nodes.put(id, new Node(id));
 341     Node currentNode = nodes.get(id);
 342
 343     // Update the setSet for this new node
 344     if (isSet) {
 345       currentNode.setSetSet(tempSetSet, manual);
 346       tempSetSet = new HashSet<NameValuePair>();
 347       isSet = false;
 348       manual = false;
 349     }
 350
 351     if (search.isNewState()) {
 352       detail = "new";
 353     } else {
 354       detail = "visited";
 355     }
 356
 357     if (search.isEndState()) {
 358       out.println("This is the last state!");
 359       theEnd = "end";
 360     }
 361
 362     out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
 363
 364     // Updating the predecessors for this node
 365     // Check if parent node is already in successors of the current node or not
 366     if (!(currentNode.getPredecessors().contains(parentNode)))
 367         currentNode.addPredecessor(parentNode);
 368
 369     // Update the successors for this node
 370     // Check if current node is already in successors of the parent node or not
 371     if (!(parentNode.getSuccessors().contains(currentNode)))
 372         parentNode.addSuccessor(currentNode);
 373
 374
 375     // Update the setSetMap of the current node
 376     for (Node i : currentNode.getPredecessors()) {
 377         currentNode.getSetSetMap().put(i, i.getSetSet());
 378     }
 379
 380     // Update the edge and check if the outset of the current node is changed or not to propagate the change
 381     boolean isChanged = updateEdge(parentNode, currentNode);
 382
 383     // Check if the outSet of this state has changed, update all of its successors' sets if any
 384     if (isChanged)
 385         conflictFound = conflictFound || propagateTheChange(currentNode);
 386
 387     // Update the parent node
 388     if (nodes.containsKey(id)) {
 389           parentNode = nodes.get(id);
 390     } else {
 391           parentNode = new Node(id);
 392     }
 393   }
 394
 395   @Override
 396   public void stateBacktracked(Search search) {
 397     id = search.getStateId();
 398     depth = search.getDepth();
 399     operation = "backtrack";
 400     detail = null;
 401
 402     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 403
 404     // Update the parent node
 405     if (nodes.containsKey(id)) {
 406           parentNode = nodes.get(id);
 407     } else {
 408           parentNode = new Node(id);
 409     }
 410   }
 411
 412   @Override
 413   public void searchFinished(Search search) {
 414     out.println("----------------------------------- search finished");
 415   }
 416
 417   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
 418     StackFrame frame;
 419     int lo, hi;
 420
 421     frame = ti.getTopFrame();
 422
 423     if ((inst instanceof JVMLocalVariableInstruction) ||
 424         (inst instanceof JVMFieldInstruction))
 425     {
 426       if (frame.getTopPos() < 0)
 427         return(null);
 428
 429       lo = frame.peek();
 430       hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 431
 432       return(decodeValue(type, lo, hi));
 433     }
 434
 435     if (inst instanceof JVMArrayElementInstruction)
 436       return(getArrayValue(ti, type));
 437
 438     return(null);
 439   }
 440
 441   private final static String decodeValue(byte type, int lo, int hi) {
 442     switch (type) {
 443       case Types.T_ARRAY:   return(null);
 444       case Types.T_VOID:    return(null);
 445
 446       case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
 447       case Types.T_BYTE:    return(String.valueOf(lo));
 448       case Types.T_CHAR:    return(String.valueOf((char) lo));
 449       case Types.T_DOUBLE:  return(String.valueOf(Types.intsToDouble(lo, hi)));
 450       case Types.T_FLOAT:   return(String.valueOf(Types.intToFloat(lo)));
 451       case Types.T_INT:     return(String.valueOf(lo));
 452       case Types.T_LONG:    return(String.valueOf(Types.intsToLong(lo, hi)));
 453       case Types.T_SHORT:   return(String.valueOf(lo));
 454
 455       case Types.T_REFERENCE:
 456         ElementInfo ei = VM.getVM().getHeap().get(lo);
 457         if (ei == null)
 458           return(null);
 459
 460         ClassInfo ci = ei.getClassInfo();
 461         if (ci == null)
 462           return(null);
 463
 464         if (ci.getName().equals("java.lang.String"))
 465           return('"' + ei.asString() + '"');
 466
 467         return(ei.toString());
 468
 469       default:
 470         System.err.println("Unknown type: " + type);
 471         return(null);
 472      }
 473   }
 474
 475   private String getArrayValue(ThreadInfo ti, byte type) {
 476     StackFrame frame;
 477     int lo, hi;
 478
 479     frame = ti.getTopFrame();
 480     lo    = frame.peek();
 481     hi    = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 482
 483     return(decodeValue(type, lo, hi));
 484   }
 485
 486   private byte getType(ThreadInfo ti, Instruction inst) {
 487     StackFrame frame;
 488     FieldInfo fi;
 489     String type;
 490
 491     frame = ti.getTopFrame();
 492     if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
 493       return (Types.T_REFERENCE);
 494     }
 495
 496     type = null;
 497
 498     if (inst instanceof JVMLocalVariableInstruction) {
 499       type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
 500     } else if (inst instanceof JVMFieldInstruction){
 501       fi = ((JVMFieldInstruction) inst).getFieldInfo();
 502       type = fi.getType();
 503     }
 504
 505     if (inst instanceof JVMArrayElementInstruction) {
 506       return (getTypeFromInstruction(inst));
 507     }
 508
 509     if (type == null) {
 510       return (Types.T_VOID);
 511     }
 512
 513     return (decodeType(type));
 514   }
 515
 516   private final static byte getTypeFromInstruction(Instruction inst) {
 517     if (inst instanceof JVMArrayElementInstruction)
 518       return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
 519
 520     return(Types.T_VOID);
 521   }
 522
 523   private final static byte decodeType(String type) {
 524     if (type.charAt(0) == '?'){
 525       return(Types.T_REFERENCE);
 526     } else {
 527       return Types.getBuiltinType(type);
 528     }
 529   }
 530
 531   // Find the variable writer
 532   // It should be one of the apps listed in the .jpf file
 533   private String getWriter(List<StackFrame> sfList, HashSet<String> writerSet) {
 534     // Start looking from the top of the stack backward
 535     for(int i=sfList.size()-1; i>=0; i--) {
 536       MethodInfo mi = sfList.get(i).getMethodInfo();
 537       if(!mi.isJPFInternal()) {
 538         String method = mi.getStackTraceName();
 539         // Check against the writers in the writerSet
 540         for(String writer : writerSet) {
 541           if (method.contains(writer)) {
 542             return writer;
 543           }
 544         }
 545       }
 546     }
 547
 548     return null;
 549   }
 550
 551   private void writeWriterAndValue(String writer, String value, String var) {
 552     // Update the temporary Set set.
 553     NameValuePair temp = new NameValuePair(1, value, var, manual);
 554     if (writer.equals("App2"))
 555         temp = new NameValuePair(2, value, var, manual);
 556
 557     if (tempSetSet.contains(temp))
 558         tempSetSet.remove(temp);
 559     tempSetSet.add(temp);
 560     // Set isSet to true
 561     isSet = true;
 562   }
 563
 564   @Override
 565   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 566     // Instantiate timeoutTimer
 567     if (timeout > 0) {
 568       if (System.currentTimeMillis() - startTime > timeout) {
 569         StringBuilder sbTimeOut = new StringBuilder();
 570         sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
 571         Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString());
 572         ti.setNextPC(nextIns);
 573       }
 574     }
 575
 576     if (conflictFound) {
 577       StringBuilder sb = new StringBuilder();
 578       sb.append(errorMessage);
 579       Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
 580       ti.setNextPC(nextIns);
 581     } else {
 582       if (conflictSet.contains(LOCATION_VAR)) {
 583         MethodInfo mi = executedInsn.getMethodInfo();
 584         // Find the last load before return and get the value here
 585         if (mi.getName().equals(SET_LOCATION_METHOD) &&
 586                 executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) {
 587           byte type  = getType(ti, executedInsn);
 588           String value = getValue(ti, executedInsn, type);
 589
 590           // Extract the writer app name
 591           ClassInfo ci = mi.getClassInfo();
 592           String writer = ci.getName();
 593
 594           // Update the temporary Set set.
 595           writeWriterAndValue(writer, value, LOCATION_VAR);
 596         }
 597       } else {
 598         if (executedInsn instanceof WriteInstruction) {
 599           String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
 600           for (String var : conflictSet) {
 601             if (varId.contains(var)) {
 602               // Get variable info
 603               byte type = getType(ti, executedInsn);
 604               String value = getValue(ti, executedInsn, type);
 605               String writer = getWriter(ti.getStack(), appSet);
 606               // Just return if the writer is not one of the listed apps in the .jpf file
 607               if (writer == null)
 608                 return;
 609
 610               if (getWriter(ti.getStack(), manualSet) != null)
 611                 manual = true;
 612
 613               // Update the temporary Set set.
 614               writeWriterAndValue(writer, value, var);
 615             }
 616           }
 617         }
 618       }
 619     }
 620   }
 621 }