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 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
  31
  32 import java.io.PrintWriter;
  33
  34 import java.util.*;
  35
  36 /**
  37  * Listener using data flow analysis to find conflicts between smartApps.
  38  **/
  39
  40 public class ConflictTracker extends ListenerAdapter {
  41
  42   private final PrintWriter out;
  43   private final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
  44   private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
  45   private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
  46   private final HashSet<String> manualSet = new HashSet<String>(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions
  47   private HashSet<Transition> transitions = new HashSet<Transition>();
  48   private ArrayList<Update> currUpdates = new ArrayList<Update>();
  49   private long timeout;
  50   private long startTime;
  51   private Node parentNode = new Node(-2);
  52   private String operation;
  53   private String detail;
  54   private String errorMessage;
  55   private String varName;
  56   private int depth;
  57   private int id;
  58   private boolean manual = false;
  59   private boolean conflictFound = false;
  60   private int currentEvent = -1;
  61   private boolean debugMode = false;
  62   private int popRef = 0;
  63
  64   private final String SET_LOCATION_METHOD = "setLocationMode";
  65   private final String LOCATION_VAR = "locationMode";
  66
  67   public ConflictTracker(Config config, JPF jpf) {
  68     out = new PrintWriter(System.out, true);
  69     debugMode = config.getBoolean("debug_mode", false);
  70
  71     String[] conflictVars = config.getStringArray("variables");
  72     // We are not tracking anything if it is null
  73     if (conflictVars != null) {
  74       for (String var : conflictVars) {
  75         conflictSet.add(var);
  76       }
  77     }
  78     String[] apps = config.getStringArray("apps");
  79     // We are not tracking anything if it is null
  80     if (apps != null) {
  81       for (String var : apps) {
  82         appSet.add(var);
  83       }
  84     }
  85
  86     // Timeout input from config is in minutes, so we need to convert into millis
  87     timeout = config.getInt("timeout", 0) * 60 * 1000;
  88     startTime = System.currentTimeMillis();
  89   }
  90
  91   void propagateChange(Edge newEdge) {
  92     HashSet<Edge> changed = new HashSet<Edge>();
  93
  94     // Add the current node to the changed set
  95     changed.add(newEdge);
  96
  97     while(!changed.isEmpty()) {
  98       // Get the first element of the changed set and remove it
  99       Edge edgeToProcess = changed.iterator().next();
 100       changed.remove(edgeToProcess);
 101
 102       //If propagating change on edge causes change, enqueue all the target node's out edges
 103       if (propagateEdge(edgeToProcess)) {
 104         Node dst = edgeToProcess.getDst();
 105         for (Edge e : dst.getOutEdges()) {
 106           changed.add(e);
 107         }
 108       }
 109     }
 110   }
 111
 112   boolean propagateEdge(Edge e) {
 113     HashMap<IndexObject, HashSet<Update>> srcUpdates = e.getSrc().getLastUpdates();
 114     HashMap<IndexObject, HashSet<Update>> dstUpdates = e.getDst().getLastUpdates();
 115     ArrayList<Update> edgeUpdates = e.getUpdates();
 116     HashMap<IndexObject, Update> lastupdate = new HashMap<IndexObject, Update>();
 117     boolean changed = false;
 118
 119     //Go through each update on the current transition
 120     for(int i=0; i<edgeUpdates.size(); i++) {
 121       Update u = edgeUpdates.get(i);
 122       IndexObject io = u.getIndex();
 123       HashSet<Update> confupdates = null;
 124
 125       //See if we have already updated this device attribute
 126       if (lastupdate.containsKey(io)) {
 127         confupdates = new HashSet<Update>();
 128         confupdates.add(lastupdate.get(io));
 129       } else if (srcUpdates.containsKey(io)){
 130         confupdates = srcUpdates.get(io);
 131       }
 132
 133       //Check for conflict with the appropriate update set if we are not a manual transition
 134       //If this is debug mode, then we do not report any conflicts
 135       if (!debugMode && confupdates != null && !u.isManual()) {
 136         for(Update u2: confupdates) {
 137           if (conflicts(u, u2)) {
 138             //throw new RuntimeException(createErrorMessage(u, u2));
 139             conflictFound = true;
 140                 errorMessage = createErrorMessage(u, u2);
 141           }
 142         }
 143       }
 144       lastupdate.put(io, u);
 145     }
 146     for(IndexObject io: srcUpdates.keySet()) {
 147       //Only propagate src changes if the transition doesn't update the device attribute
 148       if (!lastupdate.containsKey(io)) {
 149         //Make sure destination has hashset in map
 150         if (!dstUpdates.containsKey(io))
 151           dstUpdates.put(io, new HashSet<Update>());
 152
 153         changed |= dstUpdates.get(io).addAll(srcUpdates.get(io));
 154       }
 155     }
 156     for(IndexObject io: lastupdate.keySet()) {
 157       //Make sure destination has hashset in map
 158       if (!dstUpdates.containsKey(io))
 159         dstUpdates.put(io, new HashSet<Update>());
 160
 161       changed |= dstUpdates.get(io).add(lastupdate.get(io));
 162     }
 163     return changed;
 164   }
 165
 166   //Method to check for conflicts between two updates
 167   //Have conflict if same device, same attribute, different app, different vaalue
 168   boolean conflicts(Update u, Update u2) {
 169     return (!u.getApp().equals(u2.getApp())) &&
 170       u.getDeviceId().equals(u2.getDeviceId()) &&
 171       u.getAttribute().equals(u2.getAttribute()) &&
 172       (!u.getValue().equals(u2.getValue()));
 173   }
 174
 175   String createErrorMessage(Update u, Update u2) {
 176     String message = "Conflict found between the two apps. "+u.getApp()+
 177                      " has written the value: "+u.getValue()+
 178       " to the attribute: "+u.getAttribute()+" while "
 179       +u2.getApp()+" is writing the value: "
 180       +u2.getValue()+" to the same variable!";
 181     System.out.println(message);
 182     return message;
 183   }
 184
 185   Edge createEdge(Node parent, Node current, Transition transition, int evtNum) {
 186     //Check if this transition is explored.  If so, just skip everything
 187     if (transitions.contains(transition))
 188       return null;
 189
 190     //Create edge
 191     Edge e = new Edge(parent, current, transition, evtNum, currUpdates);
 192     parent.addOutEdge(e);
 193
 194     //Mark transition as explored
 195     transitions.add(transition);
 196     return e;
 197   }
 198
 199   static class Node {
 200     Integer id;
 201     Vector<Edge> outEdges = new Vector<Edge>();
 202     HashMap<IndexObject, HashSet<Update>> lastUpdates = new HashMap<IndexObject,  HashSet<Update>>();
 203
 204     Node(Integer id) {
 205       this.id = id;
 206     }
 207
 208     Integer getId() {
 209       return id;
 210     }
 211
 212     Vector<Edge> getOutEdges() {
 213       return outEdges;
 214     }
 215
 216     void addOutEdge(Edge e) {
 217       outEdges.add(e);
 218     }
 219
 220     HashMap<IndexObject, HashSet<Update>> getLastUpdates() {
 221       return lastUpdates;
 222     }
 223   }
 224
 225   //Each Edge corresponds to a transition
 226   static class Edge {
 227     Node source, destination;
 228     Transition transition;
 229     int eventNumber;
 230     ArrayList<Update> updates = new ArrayList<Update>();
 231
 232     Edge(Node src, Node dst, Transition t, int evtNum, ArrayList<Update> _updates) {
 233       this.source = src;
 234       this.destination = dst;
 235       this.transition = t;
 236       this.eventNumber = evtNum;
 237       this.updates.addAll(_updates);
 238     }
 239
 240     Node getSrc() {
 241       return source;
 242     }
 243
 244     Node getDst() {
 245       return destination;
 246     }
 247
 248     Transition getTransition() {
 249       return transition;
 250     }
 251
 252     int getEventNumber() { return eventNumber; }
 253
 254     ArrayList<Update> getUpdates() {
 255       return updates;
 256     }
 257   }
 258
 259   static class Update {
 260     String appName;
 261     String deviceId;
 262     String attribute;
 263     String value;
 264     boolean ismanual;
 265
 266     Update(String _appName, String _deviceId, String _attribute, String _value, boolean _ismanual) {
 267       this.appName = _appName;
 268       this.deviceId = _deviceId;
 269       this.attribute = _attribute;
 270       this.value = _value;
 271       this.ismanual = _ismanual;
 272     }
 273
 274     boolean isManual() {
 275       return ismanual;
 276     }
 277
 278     String getApp() {
 279       return appName;
 280     }
 281
 282     String getDeviceId() {
 283       return deviceId;
 284     }
 285
 286     String getAttribute() {
 287       return attribute;
 288     }
 289
 290     String getValue() {
 291       return value;
 292     }
 293
 294     //Gets an index object for indexing updates by just device and attribute
 295     IndexObject getIndex() {
 296       return new IndexObject(this);
 297     }
 298
 299     public boolean equals(Object o) {
 300       if (!(o instanceof Update))
 301         return false;
 302       Update u=(Update)o;
 303       return (getDeviceId().equals(u.getDeviceId()) &&
 304               getAttribute().equals(u.getAttribute()) &&
 305               getApp().equals(u.getApp()) &&
 306               getValue().equals(u.getValue()));
 307     }
 308
 309     public int hashCode() {
 310       return (getDeviceId().hashCode() << 3) ^
 311         (getAttribute().hashCode() << 2) ^
 312         (getApp().hashCode() << 1) ^
 313         getValue().hashCode();
 314     }
 315
 316     public String toString() {
 317       return "<"+getAttribute()+", "+getValue()+", "+getApp()+", "+ismanual+">";
 318     }
 319   }
 320
 321   static class IndexObject {
 322     Update u;
 323     IndexObject(Update _u) {
 324       this.u = _u;
 325     }
 326
 327     public boolean equals(Object o) {
 328       if (!(o instanceof IndexObject))
 329         return false;
 330       IndexObject io=(IndexObject)o;
 331       return (u.getDeviceId().equals(io.u.getDeviceId()) &&
 332               u.getAttribute().equals(io.u.getAttribute()));
 333     }
 334     public int hashCode() {
 335       return (u.getDeviceId().hashCode() << 1) ^ u.getAttribute().hashCode();
 336     }
 337   }
 338
 339   @Override
 340   public void stateRestored(Search search) {
 341     id = search.getStateId();
 342     depth = search.getDepth();
 343     operation = "restored";
 344     detail = null;
 345
 346     out.println("The state is restored to state with id: "+id+", depth: "+depth);
 347
 348     // Update the parent node
 349     parentNode = getNode(id);
 350   }
 351
 352   @Override
 353   public void searchStarted(Search search) {
 354     out.println("----------------------------------- search started");
 355   }
 356
 357   private Node getNode(Integer id) {
 358     if (!nodes.containsKey(id))
 359       nodes.put(id, new Node(id));
 360     return nodes.get(id);
 361   }
 362
 363   public void printGraph() {
 364     System.out.println("digraph testgraph {");
 365     for(Integer i : nodes.keySet()) {
 366       Node n = nodes.get(i);
 367       System.out.print("N"+i+"[label=\"");
 368
 369       for(IndexObject io:n.lastUpdates.keySet()) {
 370         for(Update u:n.lastUpdates.get(io)) {
 371           System.out.print(u.toString().replace("\"", "\\\"")+", ");
 372         }
 373       }
 374       System.out.println("\"];");
 375       for(Edge e:n.outEdges) {
 376         System.out.print("N"+e.getSrc().getId()+"->N"+e.getDst().getId()+"[label=\"");
 377         for(Update u:e.getUpdates()) {
 378           System.out.print(u.toString().replace("\"", "\\\"")+", ");
 379         }
 380         System.out.println("\"];");
 381       }
 382     }
 383
 384     System.out.println("}");
 385   }
 386
 387   @Override
 388   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
 389
 390     if (currentCG instanceof IntChoiceFromSet) {
 391       IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
 392       currentEvent = icsCG.getNextChoice();
 393     }
 394   }
 395
 396   @Override
 397   public void stateAdvanced(Search search) {
 398     String theEnd = null;
 399     Transition transition = search.getTransition();
 400     id = search.getStateId();
 401     depth = search.getDepth();
 402     operation = "forward";
 403
 404     // Add the node to the list of nodes
 405     Node currentNode = getNode(id);
 406
 407     // Create an edge based on the current transition
 408     Edge newEdge = createEdge(parentNode, currentNode, transition, currentEvent);
 409
 410     // Reset the temporary variables and flags
 411     currUpdates.clear();
 412     manual = false;
 413
 414     // If we have a new Edge, check for conflicts
 415     if (newEdge != null)
 416       propagateChange(newEdge);
 417
 418     if (search.isNewState()) {
 419       detail = "new";
 420     } else {
 421       detail = "visited";
 422     }
 423
 424     if (search.isEndState()) {
 425       out.println("This is the last state!");
 426       theEnd = "end";
 427     }
 428
 429     out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
 430
 431     // Update the parent node
 432     parentNode = currentNode;
 433   }
 434
 435   @Override
 436   public void stateBacktracked(Search search) {
 437     id = search.getStateId();
 438     depth = search.getDepth();
 439     operation = "backtrack";
 440     detail = null;
 441
 442     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 443
 444     // Update the parent node
 445     parentNode = getNode(id);
 446   }
 447
 448   @Override
 449   public void searchFinished(Search search) {
 450     out.println("----------------------------------- search finished");
 451
 452     //Comment out the following line to print the explored graph
 453     printGraph();
 454   }
 455
 456   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
 457     StackFrame frame;
 458     int lo, hi;
 459
 460     frame = ti.getTopFrame();
 461
 462     if ((inst instanceof JVMLocalVariableInstruction) ||
 463         (inst instanceof JVMFieldInstruction))
 464     {
 465       if (frame.getTopPos() < 0)
 466         return(null);
 467
 468       lo = frame.peek();
 469       hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 470
 471       // TODO: Fix for integer values (need to dig deeper into the stack frame to find the right value other than 0)
 472       // TODO: Seems to be a problem since this is Groovy (not Java)
 473       if (type == Types.T_INT || type == Types.T_LONG || type == Types.T_SHORT) {
 474         int offset = 0;
 475         while (lo == 0) {
 476           lo = frame.peek(offset);
 477           offset++;
 478         }
 479       }
 480
 481       return(decodeValue(type, lo, hi));
 482     }
 483
 484     if (inst instanceof JVMArrayElementInstruction)
 485       return(getArrayValue(ti, type));
 486
 487     return(null);
 488   }
 489
 490   private final static String decodeValue(byte type, int lo, int hi) {
 491     switch (type) {
 492       case Types.T_ARRAY:   return(null);
 493       case Types.T_VOID:    return(null);
 494
 495       case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
 496       case Types.T_BYTE:    return(String.valueOf(lo));
 497       case Types.T_CHAR:    return(String.valueOf((char) lo));
 498       case Types.T_DOUBLE:  return(String.valueOf(Types.intsToDouble(lo, hi)));
 499       case Types.T_FLOAT:   return(String.valueOf(Types.intToFloat(lo)));
 500       case Types.T_INT:     return(String.valueOf(lo));
 501       case Types.T_LONG:    return(String.valueOf(Types.intsToLong(lo, hi)));
 502       case Types.T_SHORT:   return(String.valueOf(lo));
 503
 504       case Types.T_REFERENCE:
 505         ElementInfo ei = VM.getVM().getHeap().get(lo);
 506         if (ei == null)
 507           return(null);
 508
 509         ClassInfo ci = ei.getClassInfo();
 510         if (ci == null)
 511           return(null);
 512
 513         if (ci.getName().equals("java.lang.String"))
 514           return('"' + ei.asString() + '"');
 515
 516         return(ei.toString());
 517
 518       default:
 519         System.err.println("Unknown type: " + type);
 520         return(null);
 521      }
 522   }
 523
 524   private String getArrayValue(ThreadInfo ti, byte type) {
 525     StackFrame frame;
 526     int lo, hi;
 527
 528     frame = ti.getTopFrame();
 529     lo    = frame.peek();
 530     hi    = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 531
 532     return(decodeValue(type, lo, hi));
 533   }
 534
 535   private byte getType(ThreadInfo ti, Instruction inst) {
 536     StackFrame frame;
 537     FieldInfo fi;
 538     String type;
 539
 540     frame = ti.getTopFrame();
 541     if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
 542       return (Types.T_REFERENCE);
 543     }
 544
 545     type = null;
 546
 547     if (inst instanceof JVMLocalVariableInstruction) {
 548       type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
 549     } else if (inst instanceof JVMFieldInstruction){
 550       fi = ((JVMFieldInstruction) inst).getFieldInfo();
 551       type = fi.getType();
 552     }
 553
 554     if (inst instanceof JVMArrayElementInstruction) {
 555       return (getTypeFromInstruction(inst));
 556     }
 557
 558     if (type == null) {
 559       return (Types.T_VOID);
 560     }
 561
 562     return (decodeType(type));
 563   }
 564
 565   private final static byte getTypeFromInstruction(Instruction inst) {
 566     if (inst instanceof JVMArrayElementInstruction)
 567       return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
 568
 569     return(Types.T_VOID);
 570   }
 571
 572   private final static byte decodeType(String type) {
 573     if (type.charAt(0) == '?'){
 574       return(Types.T_REFERENCE);
 575     } else {
 576       return Types.getBuiltinType(type);
 577     }
 578   }
 579
 580   // Find the variable writer
 581   // It should be one of the apps listed in the .jpf file
 582   private String getWriter(List<StackFrame> sfList, HashSet<String> writerSet) {
 583     // Start looking from the top of the stack backward
 584     for(int i=sfList.size()-1; i>=0; i--) {
 585       MethodInfo mi = sfList.get(i).getMethodInfo();
 586       if(!mi.isJPFInternal()) {
 587         String method = mi.getStackTraceName();
 588         // Check against the writers in the writerSet
 589         for(String writer : writerSet) {
 590           if (method.contains(writer)) {
 591             return writer;
 592           }
 593         }
 594       }
 595     }
 596
 597     return null;
 598   }
 599
 600   private void writeWriterAndValue(String writer, String attribute, String value) {
 601     Update u = new Update(writer, "DEVICE", attribute, value, manual);
 602     currUpdates.add(u);
 603   }
 604
 605   @Override
 606   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 607     if (timeout > 0) {
 608       if (System.currentTimeMillis() - startTime > timeout) {
 609         StringBuilder sbTimeOut = new StringBuilder();
 610         sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
 611         Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString());
 612         ti.setNextPC(nextIns);
 613       }
 614     }
 615
 616     if (conflictFound) {
 617       StringBuilder sb = new StringBuilder();
 618       sb.append(errorMessage);
 619       Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
 620       ti.setNextPC(nextIns);
 621     } else {
 622       // Check if we are ready to pop the values
 623       if (popRef == 2) {
 624         byte type = getType(ti, executedInsn);
 625         varName = getValue(ti, executedInsn, type);
 626         String writer = getWriter(ti.getStack(), appSet);
 627
 628         popRef = popRef-1;
 629       } else if (popRef == 1) {
 630         byte type = getType(ti, executedInsn);
 631         String value = getValue(ti, executedInsn, type);
 632         String writer = getWriter(ti.getStack(), appSet);
 633
 634         for (String var: conflictSet) {
 635                 if (varName.contains(var)) {
 636                         if (writer != null) {
 637                                 System.out.println("################# writer: "+writer);
 638                                 System.out.println("################# variable: "+varName);
 639                                 System.out.println("################# value: "+value);
 640                                 System.out.println("################# manual: "+manual);
 641                                 writeWriterAndValue(writer, varName, value);
 642                         }
 643                 }
 644         }
 645
 646         popRef = popRef-1;
 647       }
 648
 649
 650       if (executedInsn.getMnemonic().equals("getfield")) {
 651         if (executedInsn.toString().contains("deviceValueSmartThing") ||
 652             executedInsn.toString().contains("deviceIntValueSmartThing")) {
 653                 if (executedInsn.getNext() != null) {
 654                         if (executedInsn.getNext().getMnemonic().contains("load")) {
 655
 656                                 if (executedInsn.getNext().getNext() != null)
 657                                         if (executedInsn.getNext().getNext().getMnemonic().contains("load"))
 658                                                 popRef = 2;
 659                         }
 660                 }
 661         }
 662       }
 663
 664       if (executedInsn instanceof WriteInstruction) {
 665         String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
 666         // Check if we have an update to isManualTransaction to update manual field
 667         if (varId.contains("isManualTransaction")) {
 668           byte type = getType(ti, executedInsn);
 669           String value = getValue(ti, executedInsn, type);
 670
 671           manual = (value.equals("true"))?true:false;
 672         }
 673       }
 674     }
 675   }
 676 }