2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.util.ObjectList;
23 import java.lang.reflect.Array;
24 import java.util.Comparator;
25 import java.util.Random;
28 * abstract root class for configurable choice generators
30 public abstract class ChoiceGeneratorBase<T> implements ChoiceGenerator<T> {
33 * choice randomization policies, which can be set from JPF configuration
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
41 static ChoiceRandomizationPolicy randomization;
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);
48 // want the id to be visible to subclasses outside package
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)
56 // used to cut off further choice enumeration
57 protected boolean isDone;
59 // we keep a linked list of CG's
60 protected ChoiceGenerator<?> prev;
62 // the instruction that created this CG
63 protected Instruction insn;
65 // the state id of the state in which the CG was created
66 protected int stateId;
68 // and the thread that executed this insn
69 protected ThreadInfo ti;
71 // free attributes (set on demand)
72 protected Object attr;
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;
78 // in case this is initialized from a VM context
79 public static void init(Config config) {
81 randomization = config.getEnum("cg.randomize_choices",
82 ChoiceRandomizationPolicy.values(), ChoiceRandomizationPolicy.NONE);
84 // if the randomize_choices is set to random then we need to
85 // pick the seed based on the system time.
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);
95 public static boolean useRandomization() {
96 return (randomization != ChoiceRandomizationPolicy.NONE);
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)
104 protected ChoiceGeneratorBase() {
108 protected ChoiceGeneratorBase(String id) {
113 public ChoiceGeneratorBase<?> clone() throws CloneNotSupportedException {
114 return (ChoiceGeneratorBase<?>)super.clone();
118 public ChoiceGenerator<?> deepClone() throws CloneNotSupportedException {
119 ChoiceGenerator<?> clone = (ChoiceGenerator<?>) super.clone();
120 // we need to deep copy the parent CG
122 clone.setPreviousChoiceGenerator( prev.deepClone());
128 public String getId() {
133 public int getIdRef() {
138 public void setIdRef(int idRef) {
143 public void setId(String id) {
148 public boolean isSchedulingPoint() {
152 //--- the getters and setters for the CG creation info
154 public void setThreadInfo(ThreadInfo ti) {
159 public ThreadInfo getThreadInfo() {
164 public void setInsn(Instruction insn) {
169 public Instruction getInsn() {
174 public void setContext(ThreadInfo tiCreator) {
176 insn = tiCreator.getPC();
180 public void setStateId(int stateId){
181 this.stateId = stateId;
184 getCascadedParent().setStateId(stateId);
189 public int getStateId(){
194 public String getSourceLocation() {
195 return insn.getSourceLocation();
199 public boolean supportsReordering(){
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
208 * Note: this should only be called before the first advance, since it
209 * can reset the CG enumeration status
212 public ChoiceGenerator<T> reorder (Comparator<T> comparator){
217 public void setPreviousChoiceGenerator(ChoiceGenerator<?> cg) {
222 public void setCascaded() {
227 public boolean isCascaded() {
232 public <C extends ChoiceGenerator<?>> C getPreviousChoiceGeneratorOfType(Class<C> cls) {
233 ChoiceGenerator<?> cg = prev;
236 if (cls.isInstance(cg)) {
239 cg = cg.getPreviousChoiceGenerator();
245 * returns the prev CG if it was registered for the same insn
248 public ChoiceGenerator<?> getCascadedParent() {
250 if (prev.isCascaded()) {
259 * return array with all cascaded parents and this CG, in registration order
262 public ChoiceGenerator<?>[] getCascade() {
264 for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getCascadedParent()) {
268 ChoiceGenerator<?>[] a = new ChoiceGenerator<?>[n];
270 for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getCascadedParent()) {
278 * return array with all parents and this CG, in registration order
281 public ChoiceGenerator<?>[] getAll() {
283 for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) {
287 ChoiceGenerator<?>[] a = new ChoiceGenerator<?>[n];
289 for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) {
297 * return array with all CGs (including this one) of given 'cgType', in registration order
300 public <C extends ChoiceGenerator<?>> C[] getAllOfType(Class<C> cgType) {
302 for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) {
303 if (cgType.isAssignableFrom(cg.getClass())) {
308 C[] a = (C[]) Array.newInstance(cgType, n);
310 for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) {
311 if (cgType.isAssignableFrom(cg.getClass())) {
320 public int getNumberOfParents(){
322 for (ChoiceGenerator cg = prev; cg != null; cg = cg.getPreviousChoiceGenerator()){
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
334 // we can't put the advanceForCurrentInsn() here because it has to do
335 // notifications, which are the SystemState responsibility
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)
342 public void advance(int nChoices) {
343 while (nChoices-- > 0) {
349 public void select (int choiceIndex) {
351 advance(choiceIndex+1);
355 // override this to support explicit CG enumeration from listeners etc.
358 * explicit choice enumeration. Override if supported
359 * @return choice value or null if not supported
362 public T getChoice (int idx){
366 //--- generic choice set getter implementation
367 // Note - this requires an overloaded getChoice() and can be very slow (depending on CG implementation)
370 public T[] getAllChoices(){
371 int n = getTotalNumberOfChoices();
372 T[] a = (T[]) new Object[n];
373 for (int i=0; i<n; i++){
376 return null; // CG doesn't support choice enumeration
385 public T[] getProcessedChoices(){
386 int n = getProcessedNumberOfChoices();
387 T[] a = (T[]) new Object[n];
388 for (int i=0; i<n; i++){
391 return null; // CG doesn't support choice enumeration
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++){
407 return null; // CG doesn't support choice enumeration
417 public boolean isDone() {
422 public void setDone() {
427 public boolean isProcessed() {
428 return isDone || !hasMoreChoices();
431 //--- the generic attribute API
433 public boolean hasAttr() {
434 return (attr != null);
438 public boolean hasAttr(Class<?> attrType) {
439 return ObjectList.containsType(attr, attrType);
442 public boolean hasAttrValue (Object a){
443 return ObjectList.contains(attr, a);
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
451 public Object getAttr() {
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()
462 public void setAttr(Object a) {
467 public void addAttr(Object a) {
468 attr = ObjectList.add(attr, a);
472 public void removeAttr(Object a) {
473 attr = ObjectList.remove(attr, a);
477 public void replaceAttr(Object oldAttr, Object newAttr) {
478 attr = ObjectList.replace(attr, oldAttr, newAttr);
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
486 public <T> T getAttr(Class<T> attrType) {
487 return ObjectList.getFirst(attr, attrType);
491 public <T> T getNextAttr(Class<T> attrType, Object prev) {
492 return ObjectList.getNext(attr, attrType, prev);
496 public ObjectList.Iterator attrIterator() {
497 return ObjectList.iterator(attr);
501 public <T> ObjectList.TypedIterator<T> attrIterator(Class<T> attrType) {
502 return ObjectList.typedIterator(attr, attrType);
507 public String toString() {
508 StringBuilder b = new StringBuilder(getClass().getName());
512 b.append(getProcessedNumberOfChoices());
514 b.append(getTotalNumberOfChoices());
515 b.append(",isCascaded:");
516 b.append(isCascaded);
519 b.append(",attrs:[");
521 for (Object a : ObjectList.iterator(attr)) {
536 public ChoiceGenerator<?> getPreviousChoiceGenerator() {
540 // override if there is special choice randomization support
542 public ChoiceGenerator<T> randomize(){