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;
020:
021: import java.io.FileWriter;
022: import java.io.IOException;
023:
024: import gov.nasa.jpf.Config;
025: import gov.nasa.jpf.JPFException;
026: import gov.nasa.jpf.VM;
027: import gov.nasa.jpf.Search;
028: import gov.nasa.jpf.SearchListener;
029: import gov.nasa.jpf.SearchListenerMulticaster;
030: import gov.nasa.jpf.SearchState;
031: import gov.nasa.jpf.State;
032:
033: import gov.nasa.jpf.Error;
034: import gov.nasa.jpf.ErrorList;
035: import gov.nasa.jpf.Path;
036: import gov.nasa.jpf.Property;
037:
038: import gov.nasa.jpf.util.Debug;
039: import gov.nasa.jpf.Transition;
040:
041: import gov.nasa.jpf.util.DynamicIntArray;
042:
043: /**
044: * the mother of all search classes. Mostly takes care of listeners, keeping
045: * track of state attributes and errors. This class mainly keeps the
046: * general search info like depth, configured properties etc.
047: */
048: public abstract class AbstractSearch implements Search {
049: protected ErrorList errors = new ErrorList();
050:
051: protected int depth = 0;
052: protected VM vm;
053: protected Property property;
054:
055: // the forward() attributes, e.g. used by the listeners
056: protected boolean isEndState = false;
057: protected boolean isNewState = true;
058:
059: protected boolean matchDepth;
060: protected long minFreeMemory;
061: protected int depthLimit;
062:
063: protected String lastSearchConstraint;
064:
065: // these states control the search loop
066: protected boolean done = false;
067: protected boolean doBacktrack = false;
068: SearchListener listener;
069:
070: Config config; // to later-on access settings that are only used once (not ideal)
071:
072: // statistics
073: //int maxSearchDepth = 0;
074:
075: /** (on demand) storage to keep track of state depths */
076: DynamicIntArray stateDepth;
077:
078: protected AbstractSearch(Config config, VM vm) {
079: this .vm = vm;
080: this .config = config;
081:
082: depthLimit = config.getInt("search.depth_limit", -1);
083: matchDepth = config.getBoolean("search.match_depth");
084: minFreeMemory = config.getMemorySize("search.min_free",
085: 1024 << 10);
086:
087: try {
088: property = getProperties(config);
089: if (property == null) {
090: Debug.println(Debug.ERROR, "no property");
091: }
092:
093: addListeners(config);
094: } catch (Throwable t) {
095: Debug.println(Debug.ERROR, "Search initialization failed: "
096: + t);
097: }
098: }
099:
100: public void addProperty(Property newProperty) {
101: property = PropertyMulticaster.add(property, newProperty);
102: }
103:
104: public void removeProperty(Property oldProperty) {
105: property = PropertyMulticaster.remove(property, oldProperty);
106: }
107:
108: /**
109: * return set of configured properties
110: * note there is a nameclash here - JPF 'properties' have nothing to do with
111: * Java properties (java.util.Properties)
112: */
113: protected Property getProperties(Config config)
114: throws Config.Exception {
115: Property props = null;
116:
117: Object[] a = config.getInstances("search.properties",
118: Property.class);
119: if (a != null) {
120: for (int i = 0; i < a.length; i++) {
121: props = PropertyMulticaster.add(props, (Property) a[i]);
122: }
123: }
124:
125: return props;
126: }
127:
128: protected boolean hasPropertyTermination() {
129: if (isPropertyViolated()) {
130: if (done) {
131: return true;
132: }
133: }
134:
135: return false;
136: }
137:
138: boolean isPropertyViolated() {
139: if ((property != null) && !property.check(vm, null)) {
140: error(property, vm.getPath());
141: return true;
142: }
143:
144: return false;
145: }
146:
147: void addListeners(Config config) throws Config.Exception {
148: Object[] listeners = config.getInstances("search.listener",
149: SearchListener.class);
150: if (listeners != null) {
151: for (int i = 0; i < listeners.length; i++) {
152: addListener((SearchListener) listeners[i]);
153: }
154: }
155: }
156:
157: public void addListener(SearchListener newListener) {
158: listener = SearchListenerMulticaster.add(listener, newListener);
159: }
160:
161: public void removeListener(SearchListener removeListener) {
162: listener = SearchListenerMulticaster.remove(listener,
163: removeListener);
164: }
165:
166: public ErrorList getErrors() {
167: return errors;
168: }
169:
170: public VM getVM() {
171: return vm;
172: }
173:
174: public boolean isEndState() {
175: return isEndState;
176: }
177:
178: public boolean hasNextState() {
179: return !isEndState();
180: }
181:
182: public boolean isNewState() {
183: boolean isNew = vm.isNewState();
184:
185: if (matchDepth) {
186: int id = vm.getStateId();
187:
188: if (isNew) {
189: setStateDepth(id, depth);
190: } else {
191: if (depth >= getStateDepth(id)) {
192: return false;
193: }
194: }
195: }
196:
197: return isNew;
198: }
199:
200: public boolean isVisitedState() {
201: return !isNewState();
202: }
203:
204: public int getSearchDepth() {
205: return depth;
206: }
207:
208: public String getSearchConstraint() {
209: return lastSearchConstraint;
210: }
211:
212: public Transition getTransition() {
213: return vm.getLastTransition();
214: }
215:
216: public int getStateNumber() {
217: return vm.getStateId();
218: }
219:
220: public boolean requestBacktrack() {
221: return false;
222: }
223:
224: public boolean supportsBacktrack() {
225: return false;
226: }
227:
228: public boolean supportsRestoreState() {
229: // not supported by default
230: return false;
231: }
232:
233: protected int getMaxSearchDepth() {
234: int searchDepth = Integer.MAX_VALUE;
235:
236: if (depthLimit > 0) {
237: int initialDepth = vm.getPathLength();
238:
239: if ((Integer.MAX_VALUE - initialDepth) > depthLimit) {
240: searchDepth = depthLimit + initialDepth;
241: }
242: }
243:
244: return searchDepth;
245: }
246:
247: public int getDepthLimit() {
248: return depthLimit;
249: }
250:
251: protected SearchState getSearchState() {
252: return new AbstractSearchState();
253: }
254:
255: protected void error(Property property, Path path) {
256: Error error = new Error(property, path);
257:
258: if (config.getBoolean("search.print_errors")) {
259: Debug.println(Debug.ERROR, error);
260: } else {
261: Debug.println(Debug.ERROR, "\tFound error #"
262: + errors.size());
263: }
264:
265: String fname = config.getString("search.error_path");
266: boolean getAllErrors = config
267: .getBoolean("search.multiple_errors");
268: if (fname != null) {
269: if (getAllErrors) {
270: int i = fname.lastIndexOf('.');
271:
272: if (i >= 0) {
273: fname = fname.substring(0, i) + '-' + errors.size()
274: + fname.substring(i);
275: }
276: }
277:
278: savePath(path, fname);
279: }
280:
281: errors.addError(error);
282: done = !getAllErrors;
283: notifyPropertyViolated();
284: }
285:
286: public void savePath(Path path, String fname) {
287: try {
288: FileWriter w = new FileWriter(fname);
289: vm.savePath(path, w);
290: w.close();
291: } catch (IOException e) {
292: Debug.println(Debug.ERROR, "Failed to saved trace: "
293: + fname);
294: }
295: }
296:
297: protected void notifyStateAdvanced() {
298: if (listener != null) {
299: listener.stateAdvanced(this );
300: }
301: }
302:
303: protected void notifyStateProcessed() {
304: if (listener != null) {
305: listener.stateProcessed(this );
306: }
307: }
308:
309: protected void notifyStateRestored() {
310: if (listener != null) {
311: listener.stateRestored(this );
312: }
313: }
314:
315: protected void notifyStateBacktracked() {
316: if (listener != null) {
317: listener.stateBacktracked(this );
318: }
319: }
320:
321: protected void notifyPropertyViolated() {
322: if (listener != null) {
323: listener.propertyViolated(this );
324: }
325: }
326:
327: protected void notifySearchStarted() {
328: if (listener != null) {
329: listener.searchStarted(this );
330: }
331: }
332:
333: protected void notifySearchConstraintHit(String constraintId) {
334: if (listener != null) {
335: lastSearchConstraint = constraintId;
336: listener.searchConstraintHit(this );
337: }
338: }
339:
340: protected void notifySearchFinished() {
341: if (listener != null) {
342: listener.searchFinished(this );
343: }
344: }
345:
346: protected boolean forward() {
347: boolean ret = vm.forward();
348:
349: if (ret) {
350: isNewState = vm.isNewState();
351: } else {
352: isNewState = false;
353: }
354:
355: isEndState = vm.isEndState();
356:
357: return ret;
358: }
359:
360: protected boolean backtrack() {
361: isNewState = false;
362: isEndState = false;
363:
364: return vm.backtrack();
365: }
366:
367: protected void restoreState(State state) {
368: // not supported by default
369: }
370:
371: void setStateDepth(int stateId, int depth) {
372: if (stateDepth == null) {
373: stateDepth = new DynamicIntArray(1024);
374: }
375:
376: stateDepth.set(stateId, depth);
377: }
378:
379: int getStateDepth(int stateId) {
380: try {
381: return stateDepth.get(stateId);
382: } catch (Throwable x) {
383: throw new JPFException("failed to determine state depth: "
384: + x);
385: }
386: }
387:
388: /**
389: * check if we have a minimum amount of free memory left. If not, we rather want to stop in time
390: * (with a threshold amount left) so that we can report something useful, and not just die silently
391: * with a OutOfMemoryError (which isn't handled too gracefully by most VMs)
392: */
393: boolean checkStateSpaceLimit() {
394: Runtime rt = Runtime.getRuntime();
395:
396: long avail = rt.freeMemory();
397:
398: // we could also just check for a max number of states, but what really
399: // limits us is the memory required to store states
400:
401: if (avail < minFreeMemory) {
402: // try to collect first
403: rt.gc();
404: avail = rt.freeMemory();
405:
406: if (avail < minFreeMemory) {
407: // Ok, we give up, threshold reached
408: return false;
409: }
410: }
411:
412: return true;
413: }
414:
415: /**
416: * DOCUMENT ME!
417: */
418: class AbstractSearchState implements SearchState {
419: int depth;
420:
421: AbstractSearchState() {
422: depth = AbstractSearch.this .depth;
423: }
424:
425: public int getSearchDepth() {
426: return depth;
427: }
428: }
429: }
|