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