Mercurial > hg > Members > kono > jpf-core
view src/main/gov/nasa/jpf/vm/ChoiceGeneratorBase.java @ 3:fdc263e5806b
added inverse matching in StringSetMatcher. Since this is not easy to do in regexes, it's at the next hight level in StringSetMatcher
added a optional CG accessor interface (geChoice(i), getAllChoices(), getProcessedChoices() getUnprocessedChoices()) that can be used from listeners and peers to enumerate/analyse choice sets. Note that not all CGs have to support this as there is no requirement that CGs actually use pre-computed choice sets. The low level accessor is getChoice(i), ChoiceGeneratorBase provides generic (not very efficient) set accessor implementations. Note that ChoiceGeneratorBase.getChoice() has to be overridden in subclasses in order to support choice enumeration, the default impl is just there so that we don't break subclass compilation
author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
---|---|
date | Tue, 03 Feb 2015 08:49:33 -0800 |
parents | f6886b2bda4a |
children | 9d0c3f9df6e0 |
line wrap: on
line source
/* * Copyright (C) 2014, United States Government, as represented by the * Administrator of the National Aeronautics and Space Administration. * All rights reserved. * * The Java Pathfinder core (jpf-core) platform is licensed under the * Apache License, Version 2.0 (the "License"); you may not use this file except * in compliance with the License. You may obtain a copy of the License at * * http://www.apache.org/licenses/LICENSE-2.0. * * Unless required by applicable law or agreed to in writing, software * distributed under the License is distributed on an "AS IS" BASIS, * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. * See the License for the specific language governing permissions and * limitations under the License. */ package gov.nasa.jpf.vm; import gov.nasa.jpf.Config; import gov.nasa.jpf.util.ObjectList; import java.lang.reflect.Array; import java.util.Comparator; import java.util.Random; /** * abstract root class for configurable choice generators */ public abstract class ChoiceGeneratorBase<T> implements ChoiceGenerator<T> { /** * choice randomization policies, which can be set from JPF configuration */ static enum ChoiceRandomizationPolicy { VAR_SEED, // randomize choices using a different seed for every JPF run FIXED_SEED, // randomize choices using a fixed seed for each JPF run (reproducible, seed can be specified as cg.seed) NONE // don't randomize choices }; static ChoiceRandomizationPolicy randomization; // the marker for the current choice used in String conversion public static final char MARKER = '>'; protected static Random random = new Random(42); // want the id to be visible to subclasses outside package protected String id; // for subsequent access, there is no need to translate a JPF String object reference // into a host VM String anymore (we just need it for creation to look up // the class if this is a named CG) protected int idRef; // used to cut off further choice enumeration protected boolean isDone; // we keep a linked list of CG's protected ChoiceGenerator<?> prev; // the instruction that created this CG protected Instruction insn; // and the thread that executed this insn protected ThreadInfo ti; // free attributes (set on demand) protected Object attr; // answer if this is a cascaded CG, i.e. we had more than one registered // within the same transition. Note this is NOT set for the last CG registered protected boolean isCascaded; // in case this is initialized from a VM context public static void init(Config config) { randomization = config.getEnum("cg.randomize_choices", ChoiceRandomizationPolicy.values(), ChoiceRandomizationPolicy.NONE); // if the randomize_choices is set to random then we need to // pick the seed based on the system time. if (randomization == ChoiceRandomizationPolicy.VAR_SEED) { random.setSeed(System.currentTimeMillis()); } else if (randomization == ChoiceRandomizationPolicy.FIXED_SEED){ long seed = config.getLong("cg.seed", 42); random.setSeed( seed); } } public static boolean useRandomization() { return (randomization != ChoiceRandomizationPolicy.NONE); } /** * don't use this since it is not safe for cascaded ChoiceGenerators * (we need the 'id' to be as context specific as possible) */ @Deprecated protected ChoiceGeneratorBase() { id = "?"; } protected ChoiceGeneratorBase(String id) { this.id = id; } @Override public ChoiceGeneratorBase<?> clone() throws CloneNotSupportedException { return (ChoiceGeneratorBase<?>)super.clone(); } @Override public ChoiceGenerator<?> deepClone() throws CloneNotSupportedException { ChoiceGenerator<?> clone = (ChoiceGenerator<?>) super.clone(); // we need to deep copy the parent CG if (prev != null){ clone.setPreviousChoiceGenerator( prev.deepClone()); } return clone; } @Override public String getId() { return id; } @Override public int getIdRef() { return idRef; } @Override public void setIdRef(int idRef) { this.idRef = idRef; } @Override public void setId(String id) { this.id = id; } @Override public boolean isSchedulingPoint() { return false; } //--- the getters and setters for the CG creation info @Override public void setThreadInfo(ThreadInfo ti) { this.ti = ti; } @Override public ThreadInfo getThreadInfo() { return ti; } @Override public void setInsn(Instruction insn) { this.insn = insn; } @Override public Instruction getInsn() { return insn; } @Override public void setContext(ThreadInfo tiCreator) { ti = tiCreator; insn = tiCreator.getPC(); } @Override public String getSourceLocation() { return insn.getSourceLocation(); } @Override public boolean supportsReordering(){ return false; } /** * reorder according to a user provided comparator * @returns instance to reordered CG of same choice type, * null if not supported by particular CG subclass * * Note: this should only be called before the first advance, since it * can reset the CG enumeration status */ @Override public ChoiceGenerator<T> reorder (Comparator<T> comparator){ return null; } @Override public void setPreviousChoiceGenerator(ChoiceGenerator<?> cg) { prev = cg; } @Override public void setCascaded() { isCascaded = true; } @Override public boolean isCascaded() { return isCascaded; } @Override public <C extends ChoiceGenerator<?>> C getPreviousChoiceGeneratorOfType(Class<C> cls) { ChoiceGenerator<?> cg = prev; while (cg != null) { if (cls.isInstance(cg)) { return (C) cg; } cg = cg.getPreviousChoiceGenerator(); } return null; } /** * returns the prev CG if it was registered for the same insn */ @Override public ChoiceGenerator<?> getCascadedParent() { if (prev != null) { if (prev.isCascaded()) { return prev; } } return null; } /** * return array with all cascaded parents and this CG, in registration order */ @Override public ChoiceGenerator<?>[] getCascade() { int n = 0; for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getCascadedParent()) { n++; } ChoiceGenerator<?>[] a = new ChoiceGenerator<?>[n]; for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getCascadedParent()) { a[--n] = cg; } return a; } /** * return array with all parents and this CG, in registration order */ @Override public ChoiceGenerator<?>[] getAll() { int n = 0; for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) { n++; } ChoiceGenerator<?>[] a = new ChoiceGenerator<?>[n]; for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) { a[--n] = cg; } return a; } /** * return array with all CGs (including this one) of given 'cgType', in registration order */ @Override public <C extends ChoiceGenerator<?>> C[] getAllOfType(Class<C> cgType) { int n = 0; for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) { if (cgType.isAssignableFrom(cg.getClass())) { n++; } } C[] a = (C[]) Array.newInstance(cgType, n); for (ChoiceGenerator<?> cg = this; cg != null; cg = cg.getPreviousChoiceGenerator()) { if (cgType.isAssignableFrom(cg.getClass())) { a[--n] = (C) cg; } } return a; } @Override public int getNumberOfParents(){ int n=0; for (ChoiceGenerator cg = prev; cg != null; cg = cg.getPreviousChoiceGenerator()){ n++; } return n; } @Override public void setCurrent(){ // nothing, can be overridden by subclasses to do context specific initialization // the first time this CG becomes the current one } // we can't put the advanceForCurrentInsn() here because it has to do // notifications, which are the SystemState responsibility /** * advance n choices * pretty braindead generic solution, but if more speed is needed, we can easily override * in the concrete CGs (it's used for path replay) */ @Override public void advance(int nChoices) { while (nChoices-- > 0) { advance(); } } @Override public void select (int choiceIndex) { reset(); advance(choiceIndex+1); setDone(); } // override this to support explicit CG enumeration from listeners etc. /** * explicit choice enumeration. Override if supported * @return choice value or null if not supported */ @Override public T getChoice (int idx){ return null; } //--- generic choice set getter implementation // Note - this requires an overloaded getChoice() and can be very slow (depending on CG implementation) @Override public T[] getAllChoices(){ int n = getTotalNumberOfChoices(); T[] a = (T[]) new Object[n]; for (int i=0; i<n; i++){ T c = getChoice(i); if (c == null){ return null; // CG doesn't support choice enumeration } else { a[i] = c; } } return a; } @Override public T[] getProcessedChoices(){ int n = getProcessedNumberOfChoices(); T[] a = (T[]) new Object[n]; for (int i=0; i<n; i++){ T c = getChoice(i); if (c == null){ return null; // CG doesn't support choice enumeration } else { a[i] = c; } } return a; } @Override public T[] getUnprocessedChoices(){ int n = getTotalNumberOfChoices(); int m = getProcessedNumberOfChoices(); T[] a = (T[]) new Object[n]; for (int i=m-1; i<n; i++){ T c = getChoice(i); if (c == null){ return null; // CG doesn't support choice enumeration } else { a[i] = c; } } return a; } @Override public boolean isDone() { return isDone; } @Override public void setDone() { isDone = true; } @Override public boolean isProcessed() { return isDone || !hasMoreChoices(); } //--- the generic attribute API @Override public boolean hasAttr() { return (attr != null); } @Override public boolean hasAttr(Class<?> attrType) { return ObjectList.containsType(attr, attrType); } public boolean hasAttrValue (Object a){ return ObjectList.contains(attr, a); } /** * this returns all of them - use either if you know there will be only * one attribute at a time, or check/process result with ObjectList */ @Override public Object getAttr() { return attr; } /** * this replaces all of them - use only if you know * - there will be only one attribute at a time * - you obtained the value you set by a previous getXAttr() * - you constructed a multi value list with ObjectList.createList() */ @Override public void setAttr(Object a) { attr = a; } @Override public void addAttr(Object a) { attr = ObjectList.add(attr, a); } @Override public void removeAttr(Object a) { attr = ObjectList.remove(attr, a); } @Override public void replaceAttr(Object oldAttr, Object newAttr) { attr = ObjectList.replace(attr, oldAttr, newAttr); } /** * this only returns the first attr of this type, there can be more * if you don't use client private types or the provided type is too general */ @Override public <T> T getAttr(Class<T> attrType) { return ObjectList.getFirst(attr, attrType); } @Override public <T> T getNextAttr(Class<T> attrType, Object prev) { return ObjectList.getNext(attr, attrType, prev); } @Override public ObjectList.Iterator attrIterator() { return ObjectList.iterator(attr); } @Override public <T> ObjectList.TypedIterator<T> attrIterator(Class<T> attrType) { return ObjectList.typedIterator(attr, attrType); } // -- end attrs -- @Override public String toString() { StringBuilder b = new StringBuilder(getClass().getName()); b.append(" {id:\""); b.append(id); b.append("\" ,"); b.append(getProcessedNumberOfChoices()); b.append('/'); b.append(getTotalNumberOfChoices()); b.append(",isCascaded:"); b.append(isCascaded); if (attr != null) { b.append(",attrs:["); int i = 0; for (Object a : ObjectList.iterator(attr)) { if (i++ > 1) { b.append(','); } b.append(a); } b.append(']'); } b.append('}'); return b.toString(); } @Override public ChoiceGenerator<?> getPreviousChoiceGenerator() { return prev; } // override if there is special choice randomization support @Override public ChoiceGenerator<T> randomize(){ return this; } }