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