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