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   // Public graph: to allow the StateReducer class to access it
  42   public static final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
  43   // Private
  44   private final PrintWriter out;
  45   private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
  46   private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
  47   private final HashSet<String> manualSet = new HashSet<String>(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions
  48   private HashSet<Transition> transitions = new HashSet<Transition>();
  49   private ArrayList<Update> currUpdates = new ArrayList<Update>();
  50   private long timeout;
  51   private long startTime;
  52   private Node parentNode = new Node(-2);
  53   private String operation;
  54   private String detail;
  55   private String errorMessage;
  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
  63   private final String SET_LOCATION_METHOD = "setLocationMode";
  64   private final String LOCATION_VAR = "locationMode";
  65
  66   public ConflictTrackerOld(Config config, JPF jpf) {
  67     out = new PrintWriter(System.out, true);
  68     debugMode = config.getBoolean("debug_mode", false);
  69
  70     if (!debugMode) {
  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
  87     // Timeout input from config is in minutes, so we need to convert into millis
  88     timeout = config.getInt("timeout", 0) * 60 * 1000;
  89     startTime = System.currentTimeMillis();
  90   }
  91
  92   void propagateChange(Edge newEdge) {
  93     HashSet<Edge> changed = new HashSet<Edge>();
  94
  95     // Add the current node to the changed set
  96     changed.add(newEdge);
  97
  98     while(!changed.isEmpty()) {
  99       // Get the first element of the changed set and remove it
 100       Edge edgeToProcess = changed.iterator().next();
 101       changed.remove(edgeToProcess);
 102
 103       //If propagating change on edge causes change, enqueue all the target node's out edges
 104       if (propagateEdge(edgeToProcess)) {
 105         Node dst = edgeToProcess.getDst();
 106         for (Edge e : dst.getOutEdges()) {
 107           changed.add(e);
 108         }
 109       }
 110     }
 111   }
 112
 113   boolean propagateEdge(Edge e) {
 114     HashMap<IndexObject, HashSet<Update>> srcUpdates = e.getSrc().getLastUpdates();
 115     HashMap<IndexObject, HashSet<Update>> dstUpdates = e.getDst().getLastUpdates();
 116     ArrayList<Update> edgeUpdates = e.getUpdates();
 117     HashMap<IndexObject, Update> lastupdate = new HashMap<IndexObject, Update>();
 118     boolean changed = false;
 119
 120     //Go through each update on the current transition
 121     for(int i=0; i<edgeUpdates.size(); i++) {
 122       Update u = edgeUpdates.get(i);
 123       IndexObject io = u.getIndex();
 124       HashSet<Update> confupdates = null;
 125
 126       //See if we have already updated this device attribute
 127       if (lastupdate.containsKey(io)) {
 128         confupdates = new HashSet<Update>();
 129         confupdates.add(lastupdate.get(io));
 130       } else if (srcUpdates.containsKey(io)){
 131         confupdates = srcUpdates.get(io);
 132       }
 133
 134       //Check for conflict with the appropriate update set if we are not a manual transition
 135       if (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     if (!debugMode) {
 350       parentNode = getNode(id);
 351     }
 352   }
 353
 354   @Override
 355   public void searchStarted(Search search) {
 356     out.println("----------------------------------- search started");
 357   }
 358
 359   private Node getNode(Integer id) {
 360     if (!nodes.containsKey(id))
 361       nodes.put(id, new Node(id));
 362     return nodes.get(id);
 363   }
 364
 365   public void printGraph() {
 366     System.out.println("digraph testgraph {");
 367     for(Integer i : nodes.keySet()) {
 368       Node n = nodes.get(i);
 369       System.out.print("N"+i+"[label=\"");
 370
 371       for(IndexObject io:n.lastUpdates.keySet()) {
 372         for(Update u:n.lastUpdates.get(io)) {
 373           System.out.print(u.toString().replace("\"", "\\\"")+", ");
 374         }
 375       }
 376       System.out.println("\"];");
 377       for(Edge e:n.outEdges) {
 378         System.out.print("N"+e.getSrc().getId()+"->N"+e.getDst().getId()+"[label=\"");
 379         for(Update u:e.getUpdates()) {
 380           System.out.print(u.toString().replace("\"", "\\\"")+", ");
 381         }
 382         System.out.println("\"];");
 383       }
 384     }
 385
 386     System.out.println("}");
 387   }
 388
 389   @Override
 390   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
 391
 392     if (!debugMode) {
 393       if (currentCG instanceof IntChoiceFromSet) {
 394         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
 395         currentEvent = icsCG.getNextChoice();
 396       }
 397     }
 398   }
 399
 400   @Override
 401   public void stateAdvanced(Search search) {
 402     String theEnd = null;
 403     Transition transition = search.getTransition();
 404     id = search.getStateId();
 405     depth = search.getDepth();
 406     operation = "forward";
 407
 408     if (!debugMode) {
 409       // Add the node to the list of nodes
 410       Node currentNode = getNode(id);
 411
 412       // Create an edge based on the current transition
 413       Edge newEdge = createEdge(parentNode, currentNode, transition, currentEvent);
 414
 415       // Reset the temporary variables and flags
 416       currUpdates.clear();
 417       manual = false;
 418
 419       // If we have a new Edge, check for conflicts
 420       if (newEdge != null)
 421         propagateChange(newEdge);
 422
 423       if (search.isNewState()) {
 424         detail = "new";
 425       } else {
 426         detail = "visited";
 427       }
 428
 429       if (search.isEndState()) {
 430         out.println("This is the last state!");
 431         theEnd = "end";
 432       }
 433
 434       out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
 435
 436       // Update the parent node
 437       parentNode = currentNode;
 438     }
 439   }
 440
 441   @Override
 442   public void stateBacktracked(Search search) {
 443     id = search.getStateId();
 444     depth = search.getDepth();
 445     operation = "backtrack";
 446     detail = null;
 447
 448     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 449
 450     if (!debugMode) {
 451       // Update the parent node
 452       parentNode = getNode(id);
 453     }
 454   }
 455
 456   @Override
 457   public void searchFinished(Search search) {
 458     out.println("----------------------------------- search finished");
 459
 460     if (!debugMode) {
 461       //Comment out the following line to print the explored graph
 462       printGraph();
 463     }
 464   }
 465
 466   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
 467     StackFrame frame;
 468     int lo, hi;
 469
 470     frame = ti.getTopFrame();
 471
 472     if ((inst instanceof JVMLocalVariableInstruction) ||
 473             (inst instanceof JVMFieldInstruction))
 474     {
 475       if (frame.getTopPos() < 0)
 476         return(null);
 477
 478       lo = frame.peek();
 479       hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 480
 481       // TODO: Fix for integer values (need to dig deeper into the stack frame to find the right value other than 0)
 482       // TODO: Seems to be a problem since this is Groovy (not Java)
 483       if (type == Types.T_INT || type == Types.T_LONG || type == Types.T_SHORT) {
 484         int offset = 0;
 485         while (lo == 0) {
 486           lo = frame.peek(offset);
 487           offset++;
 488         }
 489       }
 490
 491       return(decodeValue(type, lo, hi));
 492     }
 493
 494     if (inst instanceof JVMArrayElementInstruction)
 495       return(getArrayValue(ti, type));
 496
 497     return(null);
 498   }
 499
 500   private final static String decodeValue(byte type, int lo, int hi) {
 501     switch (type) {
 502       case Types.T_ARRAY:   return(null);
 503       case Types.T_VOID:    return(null);
 504
 505       case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
 506       case Types.T_BYTE:    return(String.valueOf(lo));
 507       case Types.T_CHAR:    return(String.valueOf((char) lo));
 508       case Types.T_DOUBLE:  return(String.valueOf(Types.intsToDouble(lo, hi)));
 509       case Types.T_FLOAT:   return(String.valueOf(Types.intToFloat(lo)));
 510       case Types.T_INT:     return(String.valueOf(lo));
 511       case Types.T_LONG:    return(String.valueOf(Types.intsToLong(lo, hi)));
 512       case Types.T_SHORT:   return(String.valueOf(lo));
 513
 514       case Types.T_REFERENCE:
 515         ElementInfo ei = VM.getVM().getHeap().get(lo);
 516         if (ei == null)
 517           return(null);
 518
 519         ClassInfo ci = ei.getClassInfo();
 520         if (ci == null)
 521           return(null);
 522
 523         if (ci.getName().equals("java.lang.String"))
 524           return('"' + ei.asString() + '"');
 525
 526         return(ei.toString());
 527
 528       default:
 529         System.err.println("Unknown type: " + type);
 530         return(null);
 531     }
 532   }
 533
 534   private String getArrayValue(ThreadInfo ti, byte type) {
 535     StackFrame frame;
 536     int lo, hi;
 537
 538     frame = ti.getTopFrame();
 539     lo    = frame.peek();
 540     hi    = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 541
 542     return(decodeValue(type, lo, hi));
 543   }
 544
 545   private byte getType(ThreadInfo ti, Instruction inst) {
 546     StackFrame frame;
 547     FieldInfo fi;
 548     String type;
 549
 550     frame = ti.getTopFrame();
 551     if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
 552       return (Types.T_REFERENCE);
 553     }
 554
 555     type = null;
 556
 557     if (inst instanceof JVMLocalVariableInstruction) {
 558       type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
 559     } else if (inst instanceof JVMFieldInstruction){
 560       fi = ((JVMFieldInstruction) inst).getFieldInfo();
 561       type = fi.getType();
 562     }
 563
 564     if (inst instanceof JVMArrayElementInstruction) {
 565       return (getTypeFromInstruction(inst));
 566     }
 567
 568     if (type == null) {
 569       return (Types.T_VOID);
 570     }
 571
 572     return (decodeType(type));
 573   }
 574
 575   private final static byte getTypeFromInstruction(Instruction inst) {
 576     if (inst instanceof JVMArrayElementInstruction)
 577       return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
 578
 579     return(Types.T_VOID);
 580   }
 581
 582   private final static byte decodeType(String type) {
 583     if (type.charAt(0) == '?'){
 584       return(Types.T_REFERENCE);
 585     } else {
 586       return Types.getBuiltinType(type);
 587     }
 588   }
 589
 590   // Find the variable writer
 591   // It should be one of the apps listed in the .jpf file
 592   private String getWriter(List<StackFrame> sfList, HashSet<String> writerSet) {
 593     // Start looking from the top of the stack backward
 594     for(int i=sfList.size()-1; i>=0; i--) {
 595       MethodInfo mi = sfList.get(i).getMethodInfo();
 596       if(!mi.isJPFInternal()) {
 597         String method = mi.getStackTraceName();
 598         // Check against the writers in the writerSet
 599         for(String writer : writerSet) {
 600           if (method.contains(writer)) {
 601             return writer;
 602           }
 603         }
 604       }
 605     }
 606
 607     return null;
 608   }
 609
 610   private void writeWriterAndValue(String writer, String attribute, String value) {
 611     Update u = new Update(writer, "DEVICE", attribute, value, manual);
 612     currUpdates.add(u);
 613   }
 614
 615   @Override
 616   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 617     if (timeout > 0) {
 618       if (System.currentTimeMillis() - startTime > timeout) {
 619         StringBuilder sbTimeOut = new StringBuilder();
 620         sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
 621         Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString());
 622         ti.setNextPC(nextIns);
 623       }
 624     }
 625
 626     if (!debugMode) {
 627       if (conflictFound) {
 628
 629         StringBuilder sb = new StringBuilder();
 630         sb.append(errorMessage);
 631         Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
 632         ti.setNextPC(nextIns);
 633       } else {
 634
 635         if (executedInsn instanceof WriteInstruction) {
 636           String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
 637           // Check if we have an update to isManualTransaction to update manual field
 638           if (varId.contains("isManualTransaction")) {
 639             byte type = getType(ti, executedInsn);
 640             String value = getValue(ti, executedInsn, type);
 641             System.out.println();
 642             manual = (value.equals("true"))?true:false;
 643           }
 644           for (String var : conflictSet) {
 645             if (varId.contains(var)) {
 646               // Get variable info
 647               byte type = getType(ti, executedInsn);
 648               String value = getValue(ti, executedInsn, type);
 649               String writer = getWriter(ti.getStack(), appSet);
 650
 651               // Just return if the writer is not one of the listed apps in the .jpf file
 652               if (writer == null)
 653                 return;
 654
 655               // Update the current updates
 656               writeWriterAndValue(writer, var, value);
 657             }
 658           }
 659         }
 660       }
 661     }
 662   }
 663 }