src/main/gov/nasa/jpf/vm/ChoiceGeneratorBase.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.vm;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.util.ObjectList;
  22
  23 import java.lang.reflect.Array;
  24 import java.util.Comparator;
  25 import java.util.Random;
  26
  27 /**
  28  * abstract root class for configurable choice generators
  29  */
  30 public abstract class ChoiceGeneratorBase<T> implements ChoiceGenerator<T> {
  31
  32   /**
  33    * choice randomization policies, which can be set from JPF configuration
  34    */
  35   static enum ChoiceRandomizationPolicy {
  36     VAR_SEED,    // randomize choices using a different seed for every JPF run
  37     FIXED_SEED,  // randomize choices using a fixed seed for each JPF run (reproducible, seed can be specified as cg.seed)
  38     NONE         // don't randomize choices
  39   };
  40
  41   static ChoiceRandomizationPolicy randomization;
  42
  43   // the marker for the current choice used in String conversion
  44   public static final char MARKER = '>';
  45   protected static Random random = new Random(42);
  46
  47
  48   // want the id to be visible to subclasses outside package
  49   protected String id;
  50
  51   // for subsequent access, there is no need to translate a JPF String object reference
  52   // into a host VM String anymore (we just need it for creation to look up
  53   // the class if this is a named CG)
  54   protected int idRef;
  55
  56   // used to cut off further choice enumeration
  57   protected boolean isDone;
  58
  59   // we keep a linked list of CG's
  60   protected ChoiceGenerator<?> prev;
  61
  62   // the instruction that created this CG
  63   protected Instruction insn;
  64
  65   // the state id of the state in which the CG was created
  66   protected int stateId;
  67
  68   // and the thread that executed this insn
  69   protected ThreadInfo ti;
  70
  71   // free attributes (set on demand)
  72   protected Object attr;
  73
  74   // answer if this is a cascaded CG, i.e. we had more than one registered
  75   // within the same transition. Note this is NOT set for the last CG registered
  76   protected boolean isCascaded;
  77
  78   // in case this is initialized from a VM context
  79   public static void init(Config config) {
  80
  81     randomization = config.getEnum("cg.randomize_choices",
  82                                    ChoiceRandomizationPolicy.values(), ChoiceRandomizationPolicy.NONE);
  83
  84     // if the randomize_choices is set to random then we need to
  85     // pick the seed based on the system time.
  86
  87     if (randomization == ChoiceRandomizationPolicy.VAR_SEED) {
  88       random.setSeed(System.currentTimeMillis());
  89     } else if (randomization == ChoiceRandomizationPolicy.FIXED_SEED){
  90       long seed = config.getLong("cg.seed", 42);
  91       random.setSeed( seed);
  92     }
  93   }
  94
  95   public static boolean useRandomization() {
  96     return (randomization != ChoiceRandomizationPolicy.NONE);
  97   }
  98
  99   /**
 100    *  don't use this since it is not safe for cascaded ChoiceGenerators
 101    * (we need the 'id' to be as context specific as possible)
 102    */
 103   @Deprecated
 104   protected ChoiceGeneratorBase() {
 105     id = "?";
 106   }
 107
 108   protected ChoiceGeneratorBase(String id) {
 109     this.id = id;
 110   }
 111
 112   @Override
 113   public ChoiceGeneratorBase<?> clone() throws CloneNotSupportedException {
 114     return (ChoiceGeneratorBase<?>)super.clone();
 115   }
 116
 117   @Override
 118   public ChoiceGenerator<?> deepClone() throws CloneNotSupportedException {
 119     ChoiceGenerator<?> clone = (ChoiceGenerator<?>) super.clone();
 120     // we need to deep copy the parent CG
 121     if (prev != null){
 122       clone.setPreviousChoiceGenerator( prev.deepClone());
 123     }
 124     return clone;
 125   }
 126
 127   @Override
 128   public String getId() {
 129     return id;
 130   }
 131
 132   @Override
 133   public int getIdRef() {
 134     return idRef;
 135   }
 136
 137   @Override
 138   public void setIdRef(int idRef) {
 139     this.idRef = idRef;
 140   }
 141
 142   @Override
 143   public void setId(String id) {
 144     this.id = id;
 145   }
 146
 147   @Override
 148   public boolean isSchedulingPoint() {
 149     return false;
 150   }
 151
 152   //--- the getters and setters for the CG creation info
 153   @Override
 154   public void setThreadInfo(ThreadInfo ti) {
 155     this.ti = ti;
 156   }
 157
 158   @Override
 159   public ThreadInfo getThreadInfo() {
 160     return ti;
 161   }
 162
 163   @Override
 164   public void setInsn(Instruction insn) {
 165     this.insn = insn;
 166   }
 167
 168   @Override
 169   public Instruction getInsn() {
 170     return insn;
 171   }
 172
 173   @Override
 174   public void setContext(ThreadInfo tiCreator) {
 175     ti = tiCreator;
 176     insn = tiCreator.getPC();
 177   }
 178
 179   @Override
 180   public void setStateId(int stateId){
 181     this.stateId = stateId;
 182
 183     if (isCascaded){
 184       getCascadedParent().setStateId(stateId);
 185     }
 186   }
 187
 188   @Override
 189   public int getStateId(){
 190     return stateId;
 191   }
 192
 193   @Override
 194   public String getSourceLocation() {
 195     return insn.getSourceLocation();
 196   }
 197
 198   @Override
 199   public boolean supportsReordering(){
 200     return false;
 201   }
 202
 203   /**
 204    * reorder according to a user provided comparator
 205    * @returns instance to reordered CG of same choice type,
 206    * null if not supported by particular CG subclass
 207    *
 208    * Note: this should only be called before the first advance, since it
 209    * can reset the CG enumeration status
 210    */
 211   @Override
 212   public ChoiceGenerator<T> reorder (Comparator<T> comparator){
 213     return null;
 214   }
 215
 216   @Override
 217   public void setPreviousChoiceGenerator(ChoiceGenerator<?> cg) {
 218     prev = cg;
 219   }
 220
 221   @Override
 222   public void setCascaded() {
 223     isCascaded = true;
 224   }
 225
 226   @Override
 227   public boolean isCascaded() {
 228     return isCascaded;
 229   }
 230
 231   @Override
 232   public <C extends ChoiceGenerator<?>> C getPreviousChoiceGeneratorOfType(Class<C> cls) {
 233     ChoiceGenerator<?> cg = prev;
 234
 235     while (cg != null) {
 236       if (cls.isInstance(cg)) {
 237         return (C) cg;
 238       }
 239       cg = cg.getPreviousChoiceGenerator();
 240     }
 241     return null;
 242   }
 243
 244   /**
 245    * returns the prev CG if it was registered for the same insn
 246    */
 247   @Override
 248   public ChoiceGenerator<?> getCascadedParent() {
 249     if (prev != null) {
 250       if (prev.isCascaded()) {
 251         return prev;
 252       }
 253     }
 254
 255     return null;
 256   }
 257
 258   /**
 259    * return array with all cascaded parents and this CG, in registration order
 260    */
 261   @Override
 262   public ChoiceGenerator<?>[] getCascade() {
 263     int n = 0;
 264     for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getCascadedParent()) {
 265       n++;
 266     }
 267
 268     ChoiceGenerator<?>[] a = new ChoiceGenerator<?>[n];
 269
 270     for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getCascadedParent()) {
 271       a[--n] = cg;
 272     }
 273
 274     return a;
 275   }
 276
 277   /**
 278    * return array with all parents and this CG, in registration order
 279    */
 280   @Override
 281   public ChoiceGenerator<?>[] getAll() {
 282     int n = 0;
 283     for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) {
 284       n++;
 285     }
 286
 287     ChoiceGenerator<?>[] a = new ChoiceGenerator<?>[n];
 288
 289     for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) {
 290       a[--n] = cg;
 291     }
 292
 293     return a;
 294   }
 295
 296   /**
 297    * return array with all CGs (including this one) of given 'cgType', in registration order
 298    */
 299   @Override
 300   public <C extends ChoiceGenerator<?>> C[] getAllOfType(Class<C> cgType) {
 301     int n = 0;
 302     for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) {
 303       if (cgType.isAssignableFrom(cg.getClass())) {
 304         n++;
 305       }
 306     }
 307
 308     C[] a = (C[]) Array.newInstance(cgType, n);
 309
 310     for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) {
 311       if (cgType.isAssignableFrom(cg.getClass())) {
 312         a[--n] = (C) cg;
 313       }
 314     }
 315
 316     return a;
 317   }
 318
 319   @Override
 320   public int getNumberOfParents(){
 321     int n=0;
 322     for (ChoiceGenerator cg = prev; cg != null; cg = cg.getPreviousChoiceGenerator()){
 323       n++;
 324     }
 325     return n;
 326   }
 327
 328   @Override
 329   public void setCurrent(){
 330     // nothing, can be overridden by subclasses to do context specific initialization
 331     // the first time this CG becomes the current one
 332   }
 333
 334   // we can't put the advanceForCurrentInsn() here because it has to do
 335   // notifications, which are the SystemState responsibility
 336   /**
 337    * advance n choices
 338    * pretty braindead generic solution, but if more speed is needed, we can easily override
 339    * in the concrete CGs (it's used for path replay)
 340    */
 341   @Override
 342   public void advance(int nChoices) {
 343     while (nChoices-- > 0) {
 344       advance();
 345     }
 346   }
 347
 348   @Override
 349   public void select (int choiceIndex) {
 350     reset();
 351     advance(choiceIndex+1);
 352     setDone();
 353   }
 354
 355   // override this to support explicit CG enumeration from listeners etc.
 356
 357   /**
 358    * explicit choice enumeration. Override if supported
 359    * @return choice value or null if not supported
 360    */
 361   @Override
 362   public T getChoice (int idx){
 363     return null;
 364   }
 365
 366   //--- generic choice set getter implementation
 367   // Note - this requires an overloaded getChoice() and can be very slow (depending on CG implementation)
 368
 369   @Override
 370   public T[] getAllChoices(){
 371     int n = getTotalNumberOfChoices();
 372     T[] a = (T[]) new Object[n];
 373     for (int i=0; i<n; i++){
 374       T c = getChoice(i);
 375       if (c == null){
 376         return null; // CG doesn't support choice enumeration
 377       } else {
 378         a[i] = c;
 379       }
 380     }
 381     return a;
 382   }
 383
 384   @Override
 385   public T[] getProcessedChoices(){
 386     int n = getProcessedNumberOfChoices();
 387     T[] a = (T[]) new Object[n];
 388     for (int i=0; i<n; i++){
 389       T c = getChoice(i);
 390       if (c == null){
 391         return null; // CG doesn't support choice enumeration
 392       } else {
 393         a[i] = c;
 394       }
 395     }
 396     return a;
 397   }
 398
 399   @Override
 400   public T[] getUnprocessedChoices(){
 401     int n = getTotalNumberOfChoices();
 402     int m = getProcessedNumberOfChoices();
 403     T[] a = (T[]) new Object[n];
 404     for (int i=m-1; i<n; i++){
 405       T c = getChoice(i);
 406       if (c == null){
 407         return null; // CG doesn't support choice enumeration
 408       } else {
 409         a[i] = c;
 410       }
 411     }
 412     return a;
 413   }
 414
 415
 416   @Override
 417   public boolean isDone() {
 418     return isDone;
 419   }
 420
 421   @Override
 422   public void setDone() {
 423     isDone = true;
 424   }
 425
 426   @Override
 427   public boolean isProcessed() {
 428     return isDone || !hasMoreChoices();
 429   }
 430
 431   //--- the generic attribute API
 432   @Override
 433   public boolean hasAttr() {
 434     return (attr != null);
 435   }
 436
 437   @Override
 438   public boolean hasAttr(Class<?> attrType) {
 439     return ObjectList.containsType(attr, attrType);
 440   }
 441
 442   public boolean hasAttrValue (Object a){
 443     return ObjectList.contains(attr, a);
 444   }
 445
 446   /**
 447    * this returns all of them - use either if you know there will be only
 448    * one attribute at a time, or check/process result with ObjectList
 449    */
 450   @Override
 451   public Object getAttr() {
 452     return attr;
 453   }
 454
 455   /**
 456    * this replaces all of them - use only if you know
 457    *  - there will be only one attribute at a time
 458    *  - you obtained the value you set by a previous getXAttr()
 459    *  - you constructed a multi value list with ObjectList.createList()
 460    */
 461   @Override
 462   public void setAttr(Object a) {
 463     attr = a;
 464   }
 465
 466   @Override
 467   public void addAttr(Object a) {
 468     attr = ObjectList.add(attr, a);
 469   }
 470
 471   @Override
 472   public void removeAttr(Object a) {
 473     attr = ObjectList.remove(attr, a);
 474   }
 475
 476   @Override
 477   public void replaceAttr(Object oldAttr, Object newAttr) {
 478     attr = ObjectList.replace(attr, oldAttr, newAttr);
 479   }
 480
 481   /**
 482    * this only returns the first attr of this type, there can be more
 483    * if you don't use client private types or the provided type is too general
 484    */
 485   @Override
 486   public <T> T getAttr(Class<T> attrType) {
 487     return ObjectList.getFirst(attr, attrType);
 488   }
 489
 490   @Override
 491   public <T> T getNextAttr(Class<T> attrType, Object prev) {
 492     return ObjectList.getNext(attr, attrType, prev);
 493   }
 494
 495   @Override
 496   public ObjectList.Iterator attrIterator() {
 497     return ObjectList.iterator(attr);
 498   }
 499
 500   @Override
 501   public <T> ObjectList.TypedIterator<T> attrIterator(Class<T> attrType) {
 502     return ObjectList.typedIterator(attr, attrType);
 503   }
 504
 505   // -- end attrs --
 506   @Override
 507   public String toString() {
 508     StringBuilder b = new StringBuilder(getClass().getName());
 509     b.append(" {id:\"");
 510     b.append(id);
 511     b.append("\" ,");
 512     b.append(getProcessedNumberOfChoices());
 513     b.append('/');
 514     b.append(getTotalNumberOfChoices());
 515     b.append(",isCascaded:");
 516     b.append(isCascaded);
 517
 518     if (attr != null) {
 519       b.append(",attrs:[");
 520       int i = 0;
 521       for (Object a : ObjectList.iterator(attr)) {
 522         if (i++ > 1) {
 523           b.append(',');
 524         }
 525         b.append(a);
 526       }
 527       b.append(']');
 528     }
 529
 530     b.append('}');
 531
 532     return b.toString();
 533   }
 534
 535   @Override
 536   public ChoiceGenerator<?> getPreviousChoiceGenerator() {
 537     return prev;
 538   }
 539
 540   // override if there is special choice randomization support
 541   @Override
 542   public ChoiceGenerator<T> randomize(){
 543     return this;
 544   }
 545 }