001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf.search.heuristic;
020:
021: import gov.nasa.jpf.Config;
022: import gov.nasa.jpf.VM;
023: import gov.nasa.jpf.search.AbstractSearch;
024: import gov.nasa.jpf.util.CoverageManager;
025:
026: import java.util.Comparator;
027: import java.util.TreeSet;
028: import gov.nasa.jpf.VMState;
029:
030: /**
031: * a search strategy class that computes all immediate successors of a given
032: * state, puts them into a priority queue (the priority is provided by a
033: * Heuristic strategy object), and processes states in the sequence of
034: * highest priorities. Note that the queue is search-global, i.e. we might hop
035: * between search levels.
036: */
037: public class HeuristicSearch extends AbstractSearch {
038:
039: static final String DEFAULT_HEURISTIC_PACKAGE = "gov.nasa.jpf.search.heuristic.";
040:
041: protected TreeSet queue;
042: protected int numberNewChildren = 0;
043: protected HeuristicState h_state;
044: protected HeuristicState new_h_state;
045: protected Heuristic heuristic;
046:
047: protected boolean useAstar;
048: protected boolean pathCoverage = false; // set by some Heuristics instances
049: protected int initHeuristicValue;
050: protected int queueLimit;
051:
052: // statistics
053: int maxHeuristic = Integer.MIN_VALUE;
054: int minHeuristic = Integer.MAX_VALUE;
055: int heuristicTotal = 0;
056: int heuristicCount = 0;
057:
058: public HeuristicSearch(Config config, VM vm)
059: throws Config.Exception {
060: super (config, vm);
061:
062: // note this covers three potential Heuristic implementation ctors:
063: // (a) (Config,HeuristicSearch), (b) (Config), (c) default
064: Class[] argTypes = { Config.class, HeuristicSearch.class };
065: Object[] args = { config, this };
066: heuristic = (Heuristic) config.getEssentialInstance(
067: "search.heuristic.class", Heuristic.class, argTypes,
068: args);
069:
070: useAstar = config.getBoolean("search.heuristic.astar");
071: pathCoverage = config.getBoolean("search.coverage.path");
072:
073: Comparator comp = (Comparator) config.getEssentialInstance(
074: "search.heuristic.comparator.class", Comparator.class);
075:
076: queue = new TreeSet(comp);
077:
078: queueLimit = config.getInt("search.heuristic.queue_limit", -1);
079:
080: initHeuristicValue = config.getInt(
081: "search.heuristic.initial_value", 0);
082: }
083:
084: public HeuristicState getNew() {
085: return new_h_state;
086: }
087:
088: public HeuristicState getOld() {
089: return h_state;
090: }
091:
092: protected void generateChildren(int maxDepth) {
093:
094: // <2do> add listener notifications to keep track of queue size
095:
096: boolean allChildren = false;
097: numberNewChildren = 0;
098:
099: while (!done && !allChildren) {
100: if (pathCoverage) {
101: h_state.restoreCoverage();
102: }
103:
104: CoverageManager.setLastIncrements(-1);
105:
106: if (!forward()) {
107: notifyStateProcessed();
108: return;
109: }
110:
111: depth = vm.getPathLength();
112: notifyStateAdvanced();
113:
114: if (hasPropertyTermination()) {
115: return;
116: }
117:
118: if (!isEndState) {
119:
120: if (!isNewState) { // we have seen this
121: backtrack();
122: notifyStateBacktracked();
123:
124: } else if (depth >= maxDepth) { // don't want to see this
125: notifySearchConstraintHit(DEPTH_CONSTRAINT);
126:
127: backtrack();
128: notifyStateBacktracked();
129:
130: } else { // this is a new state, add to queue
131: new_h_state = new HeuristicState(getStateNumber(),
132: initHeuristicValue);
133:
134: int h_value = heuristic.heuristicValue();
135:
136: if (vm.isInterestingState()) {
137: h_value = 0;
138: } else if (vm.isBoringState()) {
139: h_value = (maxHeuristic + 1);
140: }
141:
142: // update HeuristicSearch specific statistics
143: if (maxHeuristic < h_value) {
144: maxHeuristic = h_value;
145: }
146: if (minHeuristic > h_value) {
147: minHeuristic = h_value;
148: }
149: heuristicTotal += h_value;
150: heuristicCount++;
151:
152: if (useAstar) {
153: h_value += vm.getPathLength();
154: }
155:
156: if (h_value >= 0) {
157: new_h_state.setPriority(h_value);
158:
159: // note that we only need to backtrack up to this point (from
160: // future forwards), hence we don't need full restorability
161: // (which is too expensive)
162: // <2do> might change in the future with a different state history rep
163: VMState vmState = vm.getState();
164: vmState.makeForwardRestorable();
165: new_h_state.setVirtualState(vmState);
166:
167: numberNewChildren++;
168:
169: if (pathCoverage) {
170: new_h_state.saveCoverage();
171: }
172:
173: queue.add(new_h_state);
174:
175: if ((queueLimit > 0)
176: && (queue.size() > queueLimit)) {
177: queue.remove(queue.last());
178: notifySearchConstraintHit(QUEUE_CONSTRAINT);
179: }
180: }
181:
182: backtrack(); // back to our parent, to get the next child
183: notifyStateBacktracked();
184: }
185:
186: } else { // no next state, nothing to queue
187: backtrack();
188: notifyStateBacktracked();
189: }
190: }
191: }
192:
193: public int getQueueSize() {
194: return queue.size();
195: }
196:
197: private void expandState() {
198: int s = queue.size();
199: h_state = (HeuristicState) (queue.first());
200: queue.remove(h_state);
201:
202: vm.restoreState(h_state.getVirtualState());
203:
204: heuristic.processParent();
205: }
206:
207: public void search() {
208: int maxDepth = getMaxSearchDepth();
209:
210: int sid = getStateNumber();
211: h_state = new HeuristicState(sid, initHeuristicValue);
212: heuristic.processParent();
213:
214: if (pathCoverage) {
215: h_state.saveCoverage();
216: }
217:
218: done = false;
219:
220: notifySearchStarted();
221:
222: if (hasPropertyTermination()) {
223: return;
224: }
225:
226: generateChildren(maxDepth);
227: while ((queue.size() != 0) && !done) {
228: expandState();
229: notifyStateRestored();
230:
231: // we could re-init the scheduler here
232: generateChildren(maxDepth);
233: }
234:
235: notifySearchFinished();
236: }
237:
238: public void setPathCoverage(boolean b) {
239: pathCoverage = b;
240:
241: CoverageManager.setPathCoverage(b); // <2do> bad redundancy
242: }
243:
244: public void setInstructionCoverage(boolean b) {
245: CoverageManager.setInstructionCoverage(b); // <2do> bad propagation, see 'setPathCoverage'
246: }
247:
248: public void setCalcBranchCoverage(boolean b) {
249: CoverageManager.setCalcBranchCoverage(b);
250: }
251: }
|