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
  41   private final PrintWriter out;
  42   private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
  43   private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
  44   private final HashMap<Integer, ArrayList<Integer>> predSet = new HashMap<Integer, ArrayList<Integer>>();
  45   private final HashMap<Integer, ArrayList<Integer>> succSet = new HashMap<Integer, ArrayList<Integer>>();
  46   private final HashMap<Integer, DataSet> setSet = new HashMap<Integer, DataSet>();
  47   private final HashMap<Integer, DataSet> inSet = new HashMap<Integer, DataSet>();
  48   private final HashMap<Integer, DataSet> outSet = new HashMap<Integer, DataSet>();
  49   volatile private String operation;
  50   volatile private String detail;
  51   volatile private int depth;
  52   volatile private int id;
  53   volatile private int parentId = -2;
  54   volatile private int conflictFound = 0;
  55   Transition transition;
  56   Object annotation;
  57   String label;
  58
  59
  60   public ConflictTracker(Config conf, JPF jpf) {
  61     out = new PrintWriter(System.out, true);
  62
  63     String[] conflictVars = conf.getStringArray("variables");
  64     // We are not tracking anything if it is null
  65     if (conflictVars != null) {
  66       for (String var : conflictVars) {
  67         conflictSet.add(var);
  68       }
  69     }
  70     String[] apps = conf.getStringArray("apps");
  71     // We are not tracking anything if it is null
  72     if (apps != null) {
  73       for (String var : apps) {
  74         appSet.add(var);
  75       }
  76     }
  77   }
  78
  79   class DataList {
  80         boolean appSet;
  81         String value;
  82
  83         DataList(boolean appSet, String value) {
  84                 this.appSet = appSet;
  85                 this.value = value;
  86         }
  87   }
  88
  89   class DataSet {
  90         HashMap<Integer, DataList> dataSet = new HashMap<Integer, DataList>();
  91
  92         DataSet(HashMap<Integer, DataList> dataSet) {
  93                 this.dataSet = dataSet;
  94         }
  95   }
  96
  97   @Override
  98   public void stateRestored(Search search) {
  99     id = search.getStateId();
 100     depth = search.getDepth();
 101     operation = "restored";
 102     detail = null;
 103
 104     out.println("The state is restored to state with id: "+id+", depth: "+depth);
 105
 106     parentId = id;
 107   }
 108
 109   @Override
 110   public void searchStarted(Search search) {
 111     out.println("----------------------------------- search started");
 112   }
 113
 114   @Override
 115   public void stateAdvanced(Search search) {
 116     String theEnd = null;
 117     id = search.getStateId();
 118     depth = search.getDepth();
 119     operation = "forward";
 120
 121     if (search.isNewState()) {
 122       detail = "new";
 123     } else {
 124       detail = "visited";
 125     }
 126
 127     if (search.isEndState()) {
 128       out.println("This is the last state!");
 129       theEnd = "end";
 130     }
 131
 132     out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd);
 133
 134
 135     //Set input set of this state to empty!
 136     HashMap<Integer, DataList> inDataSet = new HashMap<Integer, DataList>();
 137     inDataSet.put(0, new DataList(false, "NA"));
 138     inDataSet.put(1, new DataList(false, "NA"));
 139     DataSet inTempDataSet = new DataSet(inDataSet);
 140     inSet.put(id, inTempDataSet);
 141
 142     //Set output set of this state to empty if it is not initialized!
 143     if (!outSet.containsKey(id)) {
 144          HashMap<Integer, DataList> outDataSet = new HashMap<Integer, DataList>();
 145          outDataSet.put(0, new DataList(false, "NA"));
 146          outDataSet.put(1, new DataList(false, "NA"));
 147          DataSet outTempDataSet = new DataSet(outDataSet);
 148          outSet.put(id, outTempDataSet);
 149     }
 150
 151     //Create a temp data set of out set of this node
 152     DataList tempDataList1 = new DataList(outSet.get(id).dataSet.get(0).appSet, outSet.get(id).dataSet.get(0).value);
 153     DataList tempDataList2 = new DataList(outSet.get(id).dataSet.get(1).appSet, outSet.get(id).dataSet.get(1).value);
 154     HashMap<Integer, DataList> tempOutDataSet = new HashMap<Integer, DataList>();
 155     tempOutDataSet.put(0, tempDataList1);
 156     tempOutDataSet.put(1, tempDataList2);
 157     DataSet tempDataSet = new DataSet(tempOutDataSet);
 158
 159     //Set input set according to output set of pred states of current state
 160     if (predSet.containsKey(id)) {
 161         for (Integer i : predSet.get(id)) {
 162                 if ((outSet.get(i).dataSet.get(0).appSet == true)||(inSet.get(id).dataSet.get(0).appSet == true)) {
 163                         inSet.get(id).dataSet.get(0).appSet = true;
 164                         inSet.get(id).dataSet.get(0).value = outSet.get(i).dataSet.get(0).value;
 165                 }
 166                 if ((outSet.get(i).dataSet.get(1).appSet == true)||(inSet.get(id).dataSet.get(1).appSet == true)) {
 167                         inSet.get(id).dataSet.get(1).appSet = true;
 168                         inSet.get(id).dataSet.get(1).value = outSet.get(i).dataSet.get(1).value;
 169                 }
 170         }
 171     }
 172
 173     //Set output set to inset or setSet
 174     if (setSet.containsKey(id)) {
 175         if ((setSet.get(id).dataSet.get(0).appSet == true)&&(setSet.get(id).dataSet.get(1).appSet == true)) { //App1 & App2 are writers
 176                 outSet.get(id).dataSet.get(0).appSet = true;
 177                 outSet.get(id).dataSet.get(0).value = setSet.get(id).dataSet.get(0).value;
 178                 outSet.get(id).dataSet.get(1).appSet = true;
 179                 outSet.get(id).dataSet.get(1).value = setSet.get(id).dataSet.get(1).value;
 180         } else if (setSet.get(id).dataSet.get(0).appSet == true) { //App1 is a writer
 181                 outSet.get(id).dataSet.get(0).appSet = true;
 182                 outSet.get(id).dataSet.get(0).value = setSet.get(id).dataSet.get(0).value;
 183                 outSet.get(id).dataSet.get(1).appSet = inSet.get(id).dataSet.get(1).appSet;
 184                 outSet.get(id).dataSet.get(1).value = inSet.get(id).dataSet.get(1).value;
 185         } else if (setSet.get(id).dataSet.get(1).appSet == true) { //App2 is a writer
 186                 outSet.get(id).dataSet.get(0).appSet = inSet.get(id).dataSet.get(0).appSet;
 187                 outSet.get(id).dataSet.get(0).value = inSet.get(id).dataSet.get(0).value;
 188                 outSet.get(id).dataSet.get(1).appSet = true;
 189                 outSet.get(id).dataSet.get(1).value = setSet.get(id).dataSet.get(1).value;
 190         }
 191     } else {
 192         outSet.get(id).dataSet.get(0).appSet = inSet.get(id).dataSet.get(0).appSet;
 193         outSet.get(id).dataSet.get(0).value = inSet.get(id).dataSet.get(0).value;
 194         outSet.get(id).dataSet.get(1).appSet = inSet.get(id).dataSet.get(1).appSet;
 195         outSet.get(id).dataSet.get(1).value = inSet.get(id).dataSet.get(1).value;
 196     }
 197
 198     if ((outSet.get(id).dataSet.get(0).appSet == true)&&(outSet.get(id).dataSet.get(1).appSet == true)) { //Both apps have set the device
 199         if (!(outSet.get(id).dataSet.get(0).value.equals(outSet.get(id).dataSet.get(1).value))) //Values set by the apps are not the same, and we have a conflict!
 200                 conflictFound = 1;
 201     }
 202
 203     if ((outSet.get(id).dataSet.get(0).appSet != tempDataSet.dataSet.get(0).appSet)||
 204         ((!outSet.get(id).dataSet.get(0).value.equals(tempDataSet.dataSet.get(0).value)))||
 205         (outSet.get(id).dataSet.get(1).appSet != tempDataSet.dataSet.get(1).appSet)||
 206         ((!outSet.get(id).dataSet.get(1).value.equals(tempDataSet.dataSet.get(1).value)))) {
 207                 ArrayList<Integer> changed = new ArrayList<Integer>(predSet.get(id));
 208                 while(!changed.isEmpty()) {
 209                         //Get a random node inside the changed list!
 210                         Integer rnd = new Random().nextInt(changed.size());
 211                         Integer nodeToProcess  = changed.get(rnd);
 212                         changed.remove(nodeToProcess);
 213
 214                         //Initialize the empty input set for the current node
 215                         HashMap<Integer, DataList> nodeDataSet = new HashMap<Integer, DataList>();
 216                         nodeDataSet.put(0, new DataList(false, "NA"));
 217                         nodeDataSet.put(1, new DataList(false, "NA"));
 218                         DataSet nodeTempDataSet = new DataSet(nodeDataSet);
 219                         inSet.put(nodeToProcess, nodeTempDataSet);
 220
 221                         //Store current output to temp dataset
 222                         HashMap<Integer, DataList> currentOutDataSet = new HashMap<Integer, DataList>();
 223                         currentOutDataSet.put(0, new DataList(outSet.get(nodeToProcess).dataSet.get(0).appSet, outSet.get(nodeToProcess).dataSet.get(0).value));
 224                         currentOutDataSet.put(1, new DataList(outSet.get(nodeToProcess).dataSet.get(1).appSet, outSet.get(nodeToProcess).dataSet.get(1).value));
 225                         DataSet currentDataSet = new DataSet(currentOutDataSet);
 226
 227                         //Update the in set based on predecessors
 228                         for (Integer i : predSet.get(nodeToProcess)) {
 229                                 if ((outSet.get(i).dataSet.get(0).appSet == true)||(inSet.get(nodeToProcess).dataSet.get(0).appSet == true)) {
 230                                         inSet.get(nodeToProcess).dataSet.get(0).appSet = true;
 231                                         inSet.get(nodeToProcess).dataSet.get(0).value = outSet.get(i).dataSet.get(0).value;
 232                                 }
 233
 234                                 if ((outSet.get(i).dataSet.get(1).appSet == true)||(inSet.get(nodeToProcess).dataSet.get(1).appSet == true)) {
 235                                         inSet.get(nodeToProcess).dataSet.get(1).appSet = true;
 236                                         inSet.get(nodeToProcess).dataSet.get(1).value = outSet.get(i).dataSet.get(1).value;
 237                                 }
 238                         }
 239
 240                         //Set output set to inset or setSet
 241                         if (setSet.containsKey(nodeToProcess)) {
 242                                 if ((setSet.get(nodeToProcess).dataSet.get(0).appSet == true)&&(setSet.get(nodeToProcess).dataSet.get(1).appSet == true)) { //App1 & App2 are writers
 243                                         outSet.get(nodeToProcess).dataSet.get(0).appSet = true;
 244                                         outSet.get(nodeToProcess).dataSet.get(0).value = setSet.get(nodeToProcess).dataSet.get(0).value;
 245                                         outSet.get(nodeToProcess).dataSet.get(1).appSet = true;
 246                                         outSet.get(nodeToProcess).dataSet.get(1).value = setSet.get(nodeToProcess).dataSet.get(1).value;
 247                                 } else if (setSet.get(nodeToProcess).dataSet.get(0).appSet == true) { //App1 is a writer
 248                                         outSet.get(nodeToProcess).dataSet.get(0).appSet = true;
 249                                         outSet.get(nodeToProcess).dataSet.get(0).value = setSet.get(nodeToProcess).dataSet.get(0).value;
 250                                         outSet.get(nodeToProcess).dataSet.get(1).appSet = inSet.get(nodeToProcess).dataSet.get(1).appSet;
 251                                         outSet.get(nodeToProcess).dataSet.get(1).value = inSet.get(nodeToProcess).dataSet.get(1).value;
 252                                 } else if (setSet.get(nodeToProcess).dataSet.get(1).appSet == true) { //App2 is a writer
 253                                         outSet.get(nodeToProcess).dataSet.get(0).appSet = inSet.get(nodeToProcess).dataSet.get(0).appSet;
 254                                         outSet.get(nodeToProcess).dataSet.get(0).value = inSet.get(nodeToProcess).dataSet.get(0).value;
 255                                         outSet.get(nodeToProcess).dataSet.get(1).appSet = true;
 256                                         outSet.get(nodeToProcess).dataSet.get(1).value = setSet.get(nodeToProcess).dataSet.get(1).value;
 257                                 }
 258                         } else {
 259                                 outSet.get(nodeToProcess).dataSet.get(0).appSet = inSet.get(nodeToProcess).dataSet.get(0).appSet;
 260                                 outSet.get(nodeToProcess).dataSet.get(0).value = inSet.get(nodeToProcess).dataSet.get(0).value;
 261                                 outSet.get(nodeToProcess).dataSet.get(1).appSet = inSet.get(nodeToProcess).dataSet.get(1).appSet;
 262                                 outSet.get(nodeToProcess).dataSet.get(1).value = inSet.get(nodeToProcess).dataSet.get(1).value;
 263                         }
 264
 265                         //Checking if the output set has changed or not(Add its successors to the change list!)
 266                         if ((outSet.get(nodeToProcess).dataSet.get(0).appSet != currentDataSet.dataSet.get(0).appSet)||
 267                             !(outSet.get(nodeToProcess).dataSet.get(0).value.equals(currentDataSet.dataSet.get(0).value))||
 268                             (outSet.get(nodeToProcess).dataSet.get(1).appSet != currentDataSet.dataSet.get(1).appSet)||
 269                             !(outSet.get(nodeToProcess).dataSet.get(1).value.equals(currentDataSet.dataSet.get(1).value))) {
 270                                 for (Integer i : succSet.get(nodeToProcess))
 271                                         if (!changed.contains(i))
 272                                                 changed.add(i);
 273                         }
 274
 275                 }
 276     }
 277
 278     //Update the pred
 279     if (succSet.containsKey(id)) {
 280         ArrayList<Integer> ids = succSet.get(id);
 281         if (!ids.contains(parentId)) {
 282                 ids.add(parentId);
 283                 succSet.put(id, ids);
 284         }
 285     } else if (parentId != -2) {
 286         ArrayList<Integer> ids = new ArrayList<Integer>();
 287         ids.add(parentId);
 288         succSet.put(id, ids);
 289     }
 290
 291     //Update the suc
 292     if (succSet.containsKey(parentId)) {
 293         ArrayList<Integer> ids = succSet.get(parentId);
 294         if (!ids.contains(id)) {
 295                 ids.add(id);
 296                 succSet.put(parentId, ids);
 297         }
 298     } else if (parentId != -2) {
 299         ArrayList<Integer> ids = new ArrayList<Integer>();
 300         ids.add(id);
 301         succSet.put(parentId, ids);
 302     }
 303
 304     parentId = id;
 305
 306   }
 307
 308   @Override
 309   public void stateBacktracked(Search search) {
 310     id = search.getStateId();
 311     depth = search.getDepth();
 312     operation = "backtrack";
 313     detail = null;
 314
 315     out.println("The state is backtracked to state with id: "+id+", depth: "+depth);
 316
 317     parentId = id;
 318   }
 319
 320   @Override
 321   public void searchFinished(Search search) {
 322     out.println("----------------------------------- search finished");
 323   }
 324
 325   private String getValue(ThreadInfo ti, Instruction inst, byte type) {
 326     StackFrame frame;
 327     int lo, hi;
 328
 329     frame = ti.getTopFrame();
 330
 331     if ((inst instanceof JVMLocalVariableInstruction) ||
 332         (inst instanceof JVMFieldInstruction))
 333     {
 334        if (frame.getTopPos() < 0)
 335          return(null);
 336
 337        lo = frame.peek();
 338        hi = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 339
 340        return(decodeValue(type, lo, hi));
 341     }
 342
 343     if (inst instanceof JVMArrayElementInstruction)
 344       return(getArrayValue(ti, type));
 345
 346     return(null);
 347   }
 348
 349   private final static String decodeValue(byte type, int lo, int hi) {
 350     switch (type) {
 351       case Types.T_ARRAY:   return(null);
 352       case Types.T_VOID:    return(null);
 353
 354       case Types.T_BOOLEAN: return(String.valueOf(Types.intToBoolean(lo)));
 355       case Types.T_BYTE:    return(String.valueOf(lo));
 356       case Types.T_CHAR:    return(String.valueOf((char) lo));
 357       case Types.T_DOUBLE:  return(String.valueOf(Types.intsToDouble(lo, hi)));
 358       case Types.T_FLOAT:   return(String.valueOf(Types.intToFloat(lo)));
 359       case Types.T_INT:     return(String.valueOf(lo));
 360       case Types.T_LONG:    return(String.valueOf(Types.intsToLong(lo, hi)));
 361       case Types.T_SHORT:   return(String.valueOf(lo));
 362
 363       case Types.T_REFERENCE:
 364         ElementInfo ei = VM.getVM().getHeap().get(lo);
 365         if (ei == null)
 366           return(null);
 367
 368         ClassInfo ci = ei.getClassInfo();
 369         if (ci == null)
 370           return(null);
 371
 372         if (ci.getName().equals("java.lang.String"))
 373           return('"' + ei.asString() + '"');
 374
 375         return(ei.toString());
 376
 377       default:
 378         System.err.println("Unknown type: " + type);
 379         return(null);
 380      }
 381   }
 382
 383   private String getArrayValue(ThreadInfo ti, byte type) {
 384     StackFrame frame;
 385     int lo, hi;
 386
 387     frame = ti.getTopFrame();
 388     lo    = frame.peek();
 389     hi    = frame.getTopPos() >= 1 ? frame.peek(1) : 0;
 390
 391     return(decodeValue(type, lo, hi));
 392   }
 393
 394   private byte getType(ThreadInfo ti, Instruction inst) {
 395     StackFrame frame;
 396     FieldInfo fi;
 397     String type;
 398
 399     frame = ti.getTopFrame();
 400     if ((frame.getTopPos() >= 0) && (frame.isOperandRef())) {
 401       return (Types.T_REFERENCE);
 402     }
 403
 404     type = null;
 405
 406     if (inst instanceof JVMLocalVariableInstruction) {
 407       type = ((JVMLocalVariableInstruction) inst).getLocalVariableType();
 408     } else if (inst instanceof JVMFieldInstruction){
 409       fi = ((JVMFieldInstruction) inst).getFieldInfo();
 410       type = fi.getType();
 411     }
 412
 413     if (inst instanceof JVMArrayElementInstruction) {
 414       return (getTypeFromInstruction(inst));
 415     }
 416
 417     if (type == null) {
 418       return (Types.T_VOID);
 419     }
 420
 421     return (decodeType(type));
 422   }
 423
 424   private final static byte getTypeFromInstruction(Instruction inst) {
 425     if (inst instanceof JVMArrayElementInstruction)
 426       return(getTypeFromInstruction((JVMArrayElementInstruction) inst));
 427
 428     return(Types.T_VOID);
 429   }
 430
 431   private final static byte decodeType(String type) {
 432     if (type.charAt(0) == '?'){
 433       return(Types.T_REFERENCE);
 434     } else {
 435       return Types.getBuiltinType(type);
 436     }
 437   }
 438
 439   // Find the variable writer
 440   // It should be one of the apps listed in the .jpf file
 441   private String getWriter(List<StackFrame> sfList) {
 442     // Start looking from the top of the stack backward
 443     for(int i=sfList.size()-1; i>=0; i--) {
 444       MethodInfo mi = sfList.get(i).getMethodInfo();
 445       if(!mi.isJPFInternal()) {
 446         String method = mi.getStackTraceName();
 447         // Check against the apps in the appSet
 448         for(String app : appSet) {
 449           // There is only one writer at a time but we need to always
 450           // check all the potential writers in the list
 451           if (method.contains(app)) {
 452             return app;
 453           }
 454         }
 455       }
 456     }
 457
 458     return null;
 459   }
 460
 461   @Override
 462   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 463     if (conflictFound == 1) {
 464       StringBuilder sb = new StringBuilder();
 465       sb.append("Conflict found between two apps!");
 466       Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString());
 467       ti.setNextPC(nextIns);
 468     } else if (executedInsn instanceof WriteInstruction) {
 469       String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
 470       for(String var : conflictSet) {
 471
 472         if (varId.contains(var)) {
 473           // Get variable info
 474           byte type  = getType(ti, executedInsn);
 475           String value = getValue(ti, executedInsn, type);
 476           String writer = getWriter(ti.getStack());
 477           // Just return if the writer is not one of the listed apps in the .jpf file
 478           if (writer == null)
 479             return;
 480
 481           //Update the HashMap for Set set.
 482         if (setSet.containsKey(id)) {
 483                 if (writer.equals("App1")) {
 484                         setSet.get(id).dataSet.get(0).appSet = true;
 485                         setSet.get(id).dataSet.get(0).value = value;
 486                 } else if (writer.equals("App2")) {
 487                         setSet.get(id).dataSet.get(1).appSet = true;
 488                         setSet.get(id).dataSet.get(1).value = value;
 489                 }
 490         } else {
 491                 HashMap<Integer, DataList> dataSet = new HashMap<Integer, DataList>();
 492                 DataList dataList1 = new DataList(false, "NA");
 493                 DataList dataList2 = new DataList(false, "NA");
 494                 if (writer.equals("App1")) {
 495                         dataList1.appSet = true;
 496                         dataList1.value = value;
 497                 } else if (writer.equals("App2")) {
 498                         dataList2.appSet = true;
 499                         dataList2.value = value;
 500                 }
 501                 dataSet.put(0, dataList1);
 502                 dataSet.put(1, dataList2);
 503                 DataSet tempDataSet = new DataSet(dataSet);
 504                 setSet.put(id, tempDataSet);
 505         }
 506
 507        }
 508       }
 509
 510
 511     }
 512
 513   }
 514
 515 }