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 HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
  45   private final HashSet<NameValuePair> tempSetSet = new HashSet<NameValuePair>();
  46   private long timeout;
  47   private long startTime;
  48   private Node parentNode = new Node(-2);
  49   private String operation;
  50   private String detail;
  51   private int depth;
  52   private int id;
  53   private boolean conflictFound = false;
  54   private boolean isSet = false;
  55
  56
  57   public ConflictTracker(Config config, JPF jpf) {
  58     out = new PrintWriter(System.out, true);
  59
  60     String[] conflictVars = config.getStringArray("variables");
  61     // We are not tracking anything if it is null
  62     if (conflictVars != null) {
  63       for (String var : conflictVars) {
  64         conflictSet.add(var);
  65       }
  66     }
  67     String[] apps = config.getStringArray("apps");
  68     // We are not tracking anything if it is null
  69     if (apps != null) {
  70       for (String var : apps) {
  71         appSet.add(var);
  72       }
  73     }
  74     // Timeout input from config is in minutes, so we need to convert into millis
  75     timeout = config.getInt("timeout", 0) * 60 * 1000;
  76     startTime = System.currentTimeMillis();
  77   }
  78
  79   void propagateTheChange(Node currentNode) {
  80         HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
  81         boolean isChanged;
  82
  83         while(!changed.isEmpty()) {
  84                 // Get the first element of HashSet and remove it from the changed set
  85                 Node nodeToProcess = changed.iterator().next();
  86                 changed.remove(nodeToProcess);
  87
  88                 // Update the sets, store the outSet to temp before its changes
  89                 isChanged = updateSets(nodeToProcess);
  90
  91                 // Check for a conflict
  92                 conflictFound = checkForConflict(nodeToProcess);
  93
  94                 // Checking if the out set has changed or not(Add its successors to the change list!)
  95                 if (isChanged) {
  96                         for (Node i : nodeToProcess.getSuccessors()) {
  97                                 if (!changed.contains(i))
  98                                         changed.add(i);
  99                         }
 100                 }
 101         }
 102   }
 103
 104   boolean setOutSet(Node currentNode) {
 105         boolean isChanged = false;
 106         HashMap<NameValuePair, String> outSet = new HashMap<NameValuePair, String>();
 107
 108         // Store the outSet of current node to HashMap to help for the search in O(n)
 109         for (NameValuePair i : currentNode.getOutSet()) {
 110                 outSet.put(i, i.getValue());
 111         }
 112
 113         // Update based on inSet
 114         for (NameValuePair i : currentNode.getInSet()) {
 115                 if (currentNode.getOutSet().contains(i)) {
 116                         if (outSet.get(i) != i.getValue())
 117                                 isChanged = true;
 118                         currentNode.getOutSet().remove(i);
 119                 } else {
 120                         isChanged = true;
 121                 }
 122                 currentNode.getOutSet().add(i);
 123         }
 124
 125         // Overwrite the outSet based on setSet if we have a writer
 126         for (NameValuePair i : currentNode.getSetSet()) {
 127                 if (currentNode.getOutSet().contains(i)) {
 128                         if (outSet.get(i) != i.getValue())
 129                                 isChanged = true;
 130                         currentNode.getOutSet().remove(i);
 131                 } else {
 132                         isChanged = true;
 133                 }
 134                 currentNode.getOutSet().add(i);
 135         }
 136
 137         return isChanged;
 138   }
 139
 140   void setInSet(Node currentNode) {
 141         for (Node i : currentNode.getPredecessors()) {
 142                 currentNode.getInSet().addAll(i.getOutSet());
 143         }
 144   }
 145
 146   boolean checkForConflict(Node currentNode) {
 147         HashMap<String, String> varNameMap = new HashMap<String, String>();
 148
 149         for (NameValuePair i : currentNode.getOutSet()) {
 150                 if (varNameMap.containsKey(i.getVarName())) {
 151                         if (varNameMap.get(i) != i.getValue()) {
 152                                 return true;
 153                         }
 154                 } else {
 155                         varNameMap.put(i.getVarName(), i.getValue());
 156                 }
 157         }
 158
 159         return false;
 160   }
 161
 162   boolean updateSets(Node currentNode) {
 163         // Set input set according to output set of pred states of current state
 164         setInSet(currentNode);
 165
 166         // Set outSet according to inSet, and setSet of current node, check if there is a change
 167         return setOutSet(currentNode);
 168   }
 169
 170   static class Node {
 171         Integer id;
 172         HashSet<Node> predecessors = new HashSet<Node>();
 173         HashSet<Node> successors = new HashSet<Node>();
 174         HashSet<NameValuePair> inSet = new HashSet<NameValuePair>();
 175         HashSet<NameValuePair> setSet = new HashSet<NameValuePair>();
 176         HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
 177
 178         Node(Integer id) {
 179                 this.id = id;
 180         }
 181
 182         void addPredecessor(Node node) {
 183                 predecessors.add(node);
 184         }
 185
 186         void addSuccessor(Node node) {
 187                 successors.add(node);
 188         }
 189
 190         void setSetSet(HashSet<NameValuePair> setSet) {
 191                 this.setSet.addAll(setSet);
 192         }
 193
 194         Integer getId() {
 195                 return id;
 196         }
 197
 198         HashSet<Node> getPredecessors() {
 199                 return predecessors;
 200         }
 201
 202         HashSet<Node> getSuccessors() {
 203                 return successors;
 204         }
 205
 206         HashSet<NameValuePair> getInSet() {
 207                 return inSet;
 208         }
 209
 210         HashSet<NameValuePair> getSetSet() {
 211                 return setSet;
 212         }
 213
 214         HashSet<NameValuePair> getOutSet() {
 215                 return outSet;
 216         }
 217   }
 218
 219   static class NameValuePair {
 220         Integer appNum;
 221         String value;
 222         String varName;
 223
 224         NameValuePair(Integer appNum, String value, String varName) {
 225                 this.appNum = appNum;
 226                 this.value = value;
 227                 this.varName = varName;
 228         }
 229
 230         void setAppNum(Integer appNum) {
 231                 this.appNum = appNum;
 232         }
 233
 234         void setValue(String value) {
 235                 this.value = value;
 236         }
 237
 238         void setVarName(String varName) {
 239                 this.varName = varName;
 240         }
 241
 242         Integer getAppNum() {
 243                 return appNum;
 244         }
 245
 246         String getValue() {
 247                 return value;
 248         }
 249
 250         String getVarName() {
 251                 return varName;
 252         }
 253
 254         @Override
 255         public boolean equals(Object o) {
 256                 if (o instanceof NameValuePair) {
 257                         NameValuePair other = (NameValuePair) o;
 258                         if (varName.equals(other.getVarName()))
 259                                 return appNum.equals(other.getAppNum());
 260                 }
 261                 return false;
 262         }
 263
 264         @Override
 265         public int hashCode() {
 266                 return appNum.hashCode() * 31 + varName.hashCode();
 267         }
 268   }
 269
 270   @Override
 271   public void stateRestored(Search search) {
 272     id = search.getStateId();
 273     depth = search.getDepth();
 274     operation = "restored";
 275     detail = null;
 276
 277     out.println("The state is restored to state with id: "+id+", depth: "+depth);
 278
 279     // Update the parent node
 280     parentNode = new Node(id);
 281   }
 282
 283   @Override
 284   public void searchStarted(Search search) {
 285     out.println("----------------------------------- search started");
 286   }
 287
 288
 289   @Override
 290   public void stateAdvanced(Search search) {
 291     String theEnd = null;
 292     id = search.getStateId();
 293     depth = search.getDepth();
 294     operation = "forward";
 295
 296     // Add the node to the list of nodes
 297     nodes.put(id, new Node(id));
 298     Node currentNode = nodes.get(id);
 299
 300     // Update the setSet for this new node
 301     if (isSet) {
 302       currentNode.setSetSet(tempSetSet);
 303       isSet = false;
 304     }
 305
 306     if (search.isNewState()) {
 307       detail = "new";
 308     } else {
 309       detail = "visited";
 310     }
 311
 312     if (search.isEndState()) {
 313       out.println("This is the last state!");
 314       theEnd = "end";
 315     }
 316
 317     out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
 318
 319     // Updating the predecessors for this node
 320     // Check if parent node is already in successors of the current node or not
 321     if (!(currentNode.getPredecessors().contains(parentNode)))
 322         currentNode.addPredecessor(parentNode);
 323
 324     // Update the successors for this node
 325     // Check if current node is already in successors of the parent node or not
 326     if (!(parentNode.getSuccessors().contains(currentNode)))
 327         parentNode.addSuccessor(currentNode);
 328
 329     // Update the sets, check if the outSet is changed or not
 330     boolean isChanged = updateSets(currentNode);
 331
 332     // Check for a conflict
 333     conflictFound = checkForConflict(currentNode);
 334
 335     // Check if the outSet of this state has changed, update all of its successors' sets if any
 336     if (isChanged)
 337         propagateTheChange(currentNode);
 338
 339     // Update the parent node
 340     parentNode = new Node(id);
 341   }
 342
 343   @Override
 344   public void stateBacktracked(Search search) {
 345     id = search.getStateId();
 346     depth = search.getDepth();
 347     operation = "backtrack";
 348     detail = null;
 349
 350     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 351
 352     // Update the parent node
 353     parentNode = new Node(id);
 354   }
 355
 356   @Override
 357   public void searchFinished(Search search) {
 358     out.println("----------------------------------- search finished");
 359   }
 360
 361   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
 362     StackFrame frame;
 363     int lo, hi;
 364
 365     frame = ti.getTopFrame();
 366
 367     if ((inst instanceof JVMLocalVariableInstruction) ||
 368         (inst instanceof JVMFieldInstruction))
 369     {
 370        if (frame.getTopPos() < 0)
 371          return(null);
 372
 373        lo = frame.peek();
 374        hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 375
 376        return(decodeValue(type, lo, hi));
 377     }
 378
 379     if (inst instanceof JVMArrayElementInstruction)
 380       return(getArrayValue(ti, type));
 381
 382     return(null);
 383   }
 384
 385   private final static String decodeValue(byte type, int lo, int hi) {
 386     switch (type) {
 387       case Types.T_ARRAY:   return(null);
 388       case Types.T_VOID:    return(null);
 389
 390       case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
 391       case Types.T_BYTE:    return(String.valueOf(lo));
 392       case Types.T_CHAR:    return(String.valueOf((char) lo));
 393       case Types.T_DOUBLE:  return(String.valueOf(Types.intsToDouble(lo, hi)));
 394       case Types.T_FLOAT:   return(String.valueOf(Types.intToFloat(lo)));
 395       case Types.T_INT:     return(String.valueOf(lo));
 396       case Types.T_LONG:    return(String.valueOf(Types.intsToLong(lo, hi)));
 397       case Types.T_SHORT:   return(String.valueOf(lo));
 398
 399       case Types.T_REFERENCE:
 400         ElementInfo ei = VM.getVM().getHeap().get(lo);
 401         if (ei == null)
 402           return(null);
 403
 404         ClassInfo ci = ei.getClassInfo();
 405         if (ci == null)
 406           return(null);
 407
 408         if (ci.getName().equals("java.lang.String"))
 409           return('"' + ei.asString() + '"');
 410
 411         return(ei.toString());
 412
 413       default:
 414         System.err.println("Unknown type: " + type);
 415         return(null);
 416      }
 417   }
 418
 419   private String getArrayValue(ThreadInfo ti, byte type) {
 420     StackFrame frame;
 421     int lo, hi;
 422
 423     frame = ti.getTopFrame();
 424     lo    = frame.peek();
 425     hi    = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 426
 427     return(decodeValue(type, lo, hi));
 428   }
 429
 430   private byte getType(ThreadInfo ti, Instruction inst) {
 431     StackFrame frame;
 432     FieldInfo fi;
 433     String type;
 434
 435     frame = ti.getTopFrame();
 436     if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
 437       return (Types.T_REFERENCE);
 438     }
 439
 440     type = null;
 441
 442     if (inst instanceof JVMLocalVariableInstruction) {
 443       type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
 444     } else if (inst instanceof JVMFieldInstruction){
 445       fi = ((JVMFieldInstruction) inst).getFieldInfo();
 446       type = fi.getType();
 447     }
 448
 449     if (inst instanceof JVMArrayElementInstruction) {
 450       return (getTypeFromInstruction(inst));
 451     }
 452
 453     if (type == null) {
 454       return (Types.T_VOID);
 455     }
 456
 457     return (decodeType(type));
 458   }
 459
 460   private final static byte getTypeFromInstruction(Instruction inst) {
 461     if (inst instanceof JVMArrayElementInstruction)
 462       return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
 463
 464     return(Types.T_VOID);
 465   }
 466
 467   private final static byte decodeType(String type) {
 468     if (type.charAt(0) == '?'){
 469       return(Types.T_REFERENCE);
 470     } else {
 471       return Types.getBuiltinType(type);
 472     }
 473   }
 474
 475   // Find the variable writer
 476   // It should be one of the apps listed in the .jpf file
 477   private String getWriter(List<StackFrame> sfList) {
 478     // Start looking from the top of the stack backward
 479     for(int i=sfList.size()-1; i>=0; i--) {
 480       MethodInfo mi = sfList.get(i).getMethodInfo();
 481       if(!mi.isJPFInternal()) {
 482         String method = mi.getStackTraceName();
 483         // Check against the apps in the appSet
 484         for(String app : appSet) {
 485           // There is only one writer at a time but we need to always
 486           // check all the potential writers in the list
 487           if (method.contains(app)) {
 488             return app;
 489           }
 490         }
 491       }
 492     }
 493
 494     return null;
 495   }
 496
 497   @Override
 498   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 499     // Instantiate timeoutTimer
 500     if (timeout > 0) {
 501       if (System.currentTimeMillis() - startTime > timeout) {
 502         StringBuilder sbTimeOut = new StringBuilder();
 503         sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
 504         Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString());
 505         ti.setNextPC(nextIns);
 506       }
 507     }
 508
 509     if (conflictFound) {
 510       StringBuilder sb = new StringBuilder();
 511       sb.append("Conflict found between two apps!");
 512       Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
 513       ti.setNextPC(nextIns);
 514     } else if (executedInsn instanceof WriteInstruction) {
 515       String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
 516       for(String var : conflictSet) {
 517
 518         if (varId.contains(var)) {
 519           // Get variable info
 520           byte type  = getType(ti, executedInsn);
 521           String value = getValue(ti, executedInsn, type);
 522           String writer = getWriter(ti.getStack());
 523           // Just return if the writer is not one of the listed apps in the .jpf file
 524           if (writer == null)
 525             return;
 526
 527         // Update the temporary Set set.
 528         if (writer.equals("App1"))
 529                 tempSetSet.add(new NameValuePair(1, value, var));
 530         else if (writer.equals("App2"))
 531                 tempSetSet.add(new NameValuePair(2, value, var));
 532         // Set isSet to 1
 533         isSet = true;
 534
 535        }
 536       }
 537
 538
 539     }
 540
 541   }
 542
 543 }