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 sets, store the outSet to temp before its changes
 101       boolean isChanged = updateSets(nodeToProcess);
 102
 103       // Check for a conflict
 104       if (checkForConflict(nodeToProcess))
 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   boolean setOutSet(Node currentNode) {
 120         Integer prevSize = currentNode.getOutSet().size();
 121
 122         // Update based on setSet
 123         for (NameValuePair i : currentNode.getSetSet()) {
 124       if (currentNode.getOutSet().contains(i))
 125         currentNode.getOutSet().remove(i);
 126       currentNode.getOutSet().add(i);
 127         }
 128
 129         // Add all the inSet
 130         currentNode.getOutSet().addAll(currentNode.getInSet());
 131
 132         // Check if the outSet is changed
 133         if (!prevSize.equals(currentNode.getOutSet().size()))
 134       return true;
 135
 136         return false;
 137   }
 138
 139   void setInSet(Node currentNode) {
 140         for (Node i : currentNode.getPredecessors()) {
 141       currentNode.getInSet().addAll(i.getOutSet());
 142     }
 143   }
 144
 145   boolean checkForConflict(Node currentNode) {
 146         HashMap<String, String> valueMap = new HashMap<String, String>(); // HashMap from varName to value
 147         HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); // HashMap from varName to appNum
 148
 149         for (NameValuePair i : currentNode.getSetSet()) {
 150       if (i.getIsManual()) // Manual input: we have no conflict
 151         continue;
 152
 153       valueMap.put(i.getVarName(), i.getValue());
 154       if (writerMap.containsKey(i.getVarName()))
 155         writerMap.put(i.getVarName(), i.getAppNum()+writerMap.get(i.getVarName())); // We have two writers?
 156       else
 157         writerMap.put(i.getVarName(), i.getAppNum());
 158         }
 159
 160         // Comparing the inSet and setSet to find the conflict
 161         for (NameValuePair i : currentNode.getInSet()) {
 162       if (valueMap.containsKey(i.getVarName())) {
 163         String value = valueMap.get(i.getVarName());
 164         Integer writer = writerMap.get(i.getVarName());
 165         if ((value != null)&&(writer != null)) {
 166           if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { // We have different values
 167             errorMessage = "Conflict found between the two apps. App"+i.getAppNum()+" has written the value: "+i.getValue()+
 168                     " to the variable: "+i.getVarName()+" while App"+writerMap.get(i.getVarName())+" is overwriting the value: "
 169                     +valueMap.get(i.getVarName())+" to the same variable!";
 170             return true;
 171           }
 172         }
 173       }
 174         }
 175
 176         return false;
 177   }
 178
 179   boolean updateSets(Node currentNode) {
 180         // Set input set according to output set of pred states of current state
 181     setInSet(currentNode);
 182
 183         // Set outSet according to inSet, and setSet of current node, check if there is a change
 184     return setOutSet(currentNode);
 185   }
 186
 187   static class Node {
 188         Integer id;
 189         HashSet<Node> predecessors = new HashSet<Node>();
 190         HashSet<Node> successors = new HashSet<Node>();
 191         HashSet<NameValuePair> inSet = new HashSet<NameValuePair>();
 192         HashSet<NameValuePair> setSet = new HashSet<NameValuePair>();
 193         HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
 194
 195         Node(Integer id) {
 196                 this.id = id;
 197         }
 198
 199         void addPredecessor(Node node) {
 200                 predecessors.add(node);
 201         }
 202
 203         void addSuccessor(Node node) {
 204                 successors.add(node);
 205         }
 206
 207         void setSetSet(HashSet<NameValuePair> setSet, boolean isManual) {
 208       if (isManual)
 209         this.setSet = new HashSet<NameValuePair>();
 210       for (NameValuePair i : setSet) {
 211         this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual()));
 212       }
 213         }
 214
 215         Integer getId() {
 216                 return id;
 217         }
 218
 219         HashSet<Node> getPredecessors() {
 220                 return predecessors;
 221         }
 222
 223         HashSet<Node> getSuccessors() {
 224                 return successors;
 225         }
 226
 227         HashSet<NameValuePair> getInSet() {
 228                 return inSet;
 229         }
 230
 231         HashSet<NameValuePair> getSetSet() {
 232                 return setSet;
 233         }
 234
 235         HashSet<NameValuePair> getOutSet() {
 236                 return outSet;
 237         }
 238   }
 239
 240   static class NameValuePair {
 241         Integer appNum;
 242         String value;
 243         String varName;
 244         boolean isManual;
 245
 246         NameValuePair(Integer appNum, String value, String varName, boolean isManual) {
 247       this.appNum = appNum;
 248       this.value = value;
 249       this.varName = varName;
 250       this.isManual = isManual;
 251         }
 252
 253         void setAppNum(Integer appNum) {
 254                 this.appNum = appNum;
 255         }
 256
 257         void setValue(String value) {
 258                 this.value = value;
 259         }
 260
 261         void setVarName(String varName) {
 262                 this.varName = varName;
 263         }
 264
 265     void setIsManual(String varName) {
 266                 this.isManual = isManual;
 267         }
 268
 269         Integer getAppNum() {
 270                 return appNum;
 271         }
 272
 273         String getValue() {
 274                 return value;
 275         }
 276
 277         String getVarName() {
 278                 return varName;
 279         }
 280
 281         boolean getIsManual() {
 282                 return isManual;
 283         }
 284
 285         @Override
 286         public boolean equals(Object o) {
 287       if (o instanceof NameValuePair) {
 288         NameValuePair other = (NameValuePair) o;
 289         if (varName.equals(other.getVarName()))
 290           return appNum.equals(other.getAppNum());
 291       }
 292       return false;
 293         }
 294
 295         @Override
 296         public int hashCode() {
 297                 return appNum.hashCode() * 31 + varName.hashCode();
 298         }
 299   }
 300
 301   @Override
 302   public void stateRestored(Search search) {
 303     id = search.getStateId();
 304     depth = search.getDepth();
 305     operation = "restored";
 306     detail = null;
 307
 308     out.println("The state is restored to state with id: "+id+", depth: "+depth);
 309
 310     // Update the parent node
 311     if (nodes.containsKey(id)) {
 312           parentNode = nodes.get(id);
 313     } else {
 314           parentNode = new Node(id);
 315     }
 316   }
 317
 318   @Override
 319   public void searchStarted(Search search) {
 320     out.println("----------------------------------- search started");
 321   }
 322
 323
 324   @Override
 325   public void stateAdvanced(Search search) {
 326     String theEnd = null;
 327     id = search.getStateId();
 328     depth = search.getDepth();
 329     operation = "forward";
 330
 331     // Add the node to the list of nodes
 332     nodes.put(id, new Node(id));
 333     Node currentNode = nodes.get(id);
 334
 335     // Update the setSet for this new node
 336     if (isSet) {
 337       currentNode.setSetSet(tempSetSet, manual);
 338       tempSetSet = new HashSet<NameValuePair>();
 339       isSet = false;
 340       manual = false;
 341     }
 342
 343     if (search.isNewState()) {
 344       detail = "new";
 345     } else {
 346       detail = "visited";
 347     }
 348
 349     if (search.isEndState()) {
 350       out.println("This is the last state!");
 351       theEnd = "end";
 352     }
 353
 354     out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
 355
 356     // Updating the predecessors for this node
 357     // Check if parent node is already in successors of the current node or not
 358     if (!(currentNode.getPredecessors().contains(parentNode)))
 359         currentNode.addPredecessor(parentNode);
 360
 361     // Update the successors for this node
 362     // Check if current node is already in successors of the parent node or not
 363     if (!(parentNode.getSuccessors().contains(currentNode)))
 364         parentNode.addSuccessor(currentNode);
 365
 366     // Update the sets, check if the outSet is changed or not
 367     boolean isChanged = updateSets(currentNode);
 368
 369     // Check for a conflict
 370     conflictFound = checkForConflict(currentNode);
 371
 372     // Check if the outSet of this state has changed, update all of its successors' sets if any
 373     if (isChanged)
 374         conflictFound = conflictFound || propagateTheChange(currentNode);
 375
 376     // Update the parent node
 377     if (nodes.containsKey(id)) {
 378           parentNode = nodes.get(id);
 379     } else {
 380           parentNode = new Node(id);
 381     }
 382   }
 383
 384   @Override
 385   public void stateBacktracked(Search search) {
 386     id = search.getStateId();
 387     depth = search.getDepth();
 388     operation = "backtrack";
 389     detail = null;
 390
 391     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 392
 393     // Update the parent node
 394     if (nodes.containsKey(id)) {
 395           parentNode = nodes.get(id);
 396     } else {
 397           parentNode = new Node(id);
 398     }
 399   }
 400
 401   @Override
 402   public void searchFinished(Search search) {
 403     out.println("----------------------------------- search finished");
 404   }
 405
 406   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
 407     StackFrame frame;
 408     int lo, hi;
 409
 410     frame = ti.getTopFrame();
 411
 412     if ((inst instanceof JVMLocalVariableInstruction) ||
 413         (inst instanceof JVMFieldInstruction))
 414     {
 415       if (frame.getTopPos() < 0)
 416         return(null);
 417
 418       lo = frame.peek();
 419       hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 420
 421       return(decodeValue(type, lo, hi));
 422     }
 423
 424     if (inst instanceof JVMArrayElementInstruction)
 425       return(getArrayValue(ti, type));
 426
 427     return(null);
 428   }
 429
 430   private final static String decodeValue(byte type, int lo, int hi) {
 431     switch (type) {
 432       case Types.T_ARRAY:   return(null);
 433       case Types.T_VOID:    return(null);
 434
 435       case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
 436       case Types.T_BYTE:    return(String.valueOf(lo));
 437       case Types.T_CHAR:    return(String.valueOf((char) lo));
 438       case Types.T_DOUBLE:  return(String.valueOf(Types.intsToDouble(lo, hi)));
 439       case Types.T_FLOAT:   return(String.valueOf(Types.intToFloat(lo)));
 440       case Types.T_INT:     return(String.valueOf(lo));
 441       case Types.T_LONG:    return(String.valueOf(Types.intsToLong(lo, hi)));
 442       case Types.T_SHORT:   return(String.valueOf(lo));
 443
 444       case Types.T_REFERENCE:
 445         ElementInfo ei = VM.getVM().getHeap().get(lo);
 446         if (ei == null)
 447           return(null);
 448
 449         ClassInfo ci = ei.getClassInfo();
 450         if (ci == null)
 451           return(null);
 452
 453         if (ci.getName().equals("java.lang.String"))
 454           return('"' + ei.asString() + '"');
 455
 456         return(ei.toString());
 457
 458       default:
 459         System.err.println("Unknown type: " + type);
 460         return(null);
 461      }
 462   }
 463
 464   private String getArrayValue(ThreadInfo ti, byte type) {
 465     StackFrame frame;
 466     int lo, hi;
 467
 468     frame = ti.getTopFrame();
 469     lo    = frame.peek();
 470     hi    = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 471
 472     return(decodeValue(type, lo, hi));
 473   }
 474
 475   private byte getType(ThreadInfo ti, Instruction inst) {
 476     StackFrame frame;
 477     FieldInfo fi;
 478     String type;
 479
 480     frame = ti.getTopFrame();
 481     if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
 482       return (Types.T_REFERENCE);
 483     }
 484
 485     type = null;
 486
 487     if (inst instanceof JVMLocalVariableInstruction) {
 488       type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
 489     } else if (inst instanceof JVMFieldInstruction){
 490       fi = ((JVMFieldInstruction) inst).getFieldInfo();
 491       type = fi.getType();
 492     }
 493
 494     if (inst instanceof JVMArrayElementInstruction) {
 495       return (getTypeFromInstruction(inst));
 496     }
 497
 498     if (type == null) {
 499       return (Types.T_VOID);
 500     }
 501
 502     return (decodeType(type));
 503   }
 504
 505   private final static byte getTypeFromInstruction(Instruction inst) {
 506     if (inst instanceof JVMArrayElementInstruction)
 507       return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
 508
 509     return(Types.T_VOID);
 510   }
 511
 512   private final static byte decodeType(String type) {
 513     if (type.charAt(0) == '?'){
 514       return(Types.T_REFERENCE);
 515     } else {
 516       return Types.getBuiltinType(type);
 517     }
 518   }
 519
 520   // Find the variable writer
 521   // It should be one of the apps listed in the .jpf file
 522   private String getWriter(List<StackFrame> sfList, HashSet<String> writerSet) {
 523     // Start looking from the top of the stack backward
 524     for(int i=sfList.size()-1; i>=0; i--) {
 525       MethodInfo mi = sfList.get(i).getMethodInfo();
 526       if(!mi.isJPFInternal()) {
 527         String method = mi.getStackTraceName();
 528         // Check against the writers in the writerSet
 529         for(String writer : writerSet) {
 530           if (method.contains(writer)) {
 531             return writer;
 532           }
 533         }
 534       }
 535     }
 536
 537     return null;
 538   }
 539
 540   private void writeWriterAndValue(String writer, String value, String var) {
 541     // Update the temporary Set set.
 542     NameValuePair temp = new NameValuePair(1, value, var, manual);
 543     if (writer.equals("App2"))
 544         temp = new NameValuePair(2, value, var, manual);
 545
 546     if (tempSetSet.contains(temp))
 547         tempSetSet.remove(temp);
 548     tempSetSet.add(temp);
 549     // Set isSet to true
 550     isSet = true;
 551   }
 552
 553   @Override
 554   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 555     // Instantiate timeoutTimer
 556     if (timeout > 0) {
 557       if (System.currentTimeMillis() - startTime > timeout) {
 558         StringBuilder sbTimeOut = new StringBuilder();
 559         sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
 560         Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString());
 561         ti.setNextPC(nextIns);
 562       }
 563     }
 564
 565     if (conflictFound) {
 566       StringBuilder sb = new StringBuilder();
 567       sb.append(errorMessage);
 568       Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
 569       ti.setNextPC(nextIns);
 570     } else {
 571       if (conflictSet.contains(LOCATION_VAR)) {
 572         MethodInfo mi = executedInsn.getMethodInfo();
 573         // Find the last load before return and get the value here
 574         if (mi.getName().equals(SET_LOCATION_METHOD) &&
 575                 executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) {
 576           byte type  = getType(ti, executedInsn);
 577           String value = getValue(ti, executedInsn, type);
 578
 579           // Extract the writer app name
 580           ClassInfo ci = mi.getClassInfo();
 581           String writer = ci.getName();
 582
 583           // Update the temporary Set set.
 584           writeWriterAndValue(writer, value, LOCATION_VAR);
 585         }
 586       } else {
 587         if (executedInsn instanceof WriteInstruction) {
 588           String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
 589           for (String var : conflictSet) {
 590             if (varId.contains(var)) {
 591               // Get variable info
 592               byte type = getType(ti, executedInsn);
 593               String value = getValue(ti, executedInsn, type);
 594               String writer = getWriter(ti.getStack(), appSet);
 595               // Just return if the writer is not one of the listed apps in the .jpf file
 596               if (writer == null)
 597                 return;
 598
 599               if (getWriter(ti.getStack(), manualSet) != null)
 600                 manual = true;
 601
 602               // Update the temporary Set set.
 603               writeWriterAndValue(writer, value, var);
 604             }
 605           }
 606         }
 607       }
 608     }
 609   }
 610 }