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