Members/kono/jpf-core: src/main/gov/nasa/jpf/search/Search.java comparison

comparison src/main/gov/nasa/jpf/search/Search.java @ 0:61d41facf527

initial v8 import (history reset)

author	Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date	Fri, 23 Jan 2015 10:14:01 -0800
parents
children

comparison

equal deleted inserted replaced

--1:000000000000
+:61d41facf527
+/*
+* 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.search;
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.ConfigChangeListener;
+import gov.nasa.jpf.Error;
+import gov.nasa.jpf.JPF;
+import gov.nasa.jpf.JPFException;
+import gov.nasa.jpf.JPFListenerException;
+import gov.nasa.jpf.Property;
+import gov.nasa.jpf.State;
+import gov.nasa.jpf.report.Reporter;
+import gov.nasa.jpf.util.IntVector;
+import gov.nasa.jpf.util.JPFLogger;
+import gov.nasa.jpf.util.Misc;
+import gov.nasa.jpf.vm.VM;
+import gov.nasa.jpf.vm.Path;
+import gov.nasa.jpf.vm.ThreadList;
+import gov.nasa.jpf.vm.Transition;
+import java.util.ArrayList;
+import java.util.List;
+import java.util.concurrent.atomic.AtomicBoolean;
+/**
+* the mother of all search classes. Mostly takes care of listeners, keeping
+* track of state attributes and errors. This class mainly keeps the
+* general search info like depth, configured properties etc.
+*/
+public abstract class Search {
+protected static JPFLogger log = JPF.getLogger("gov.nasa.jpf.search");
+/** error encountered during last transition, null otherwise */
+protected Error currentError = null;
+protected ArrayList<Error> errors = new ArrayList<Error>();
+protected int       depth = 0;
+protected VM       vm;
+protected ArrayList<Property> properties;
+protected boolean matchDepth;
+protected long    minFreeMemory;
+protected int     depthLimit;
+protected boolean getAllErrors;
+// message explaining the last search constraint hit
+protected String lastSearchConstraint;
+// these states control the search loop
+protected boolean done = false;
+protected boolean doBacktrack = false;
+// do we have a probe request
+protected AtomicBoolean notifyProbeListeners = new AtomicBoolean(false);
+/** search listeners. We keep them in a simple array to avoid
+creating objects on each notification */
+protected SearchListener[] listeners = new SearchListener[0];
+/** this is a special SearchListener that is always notified last, so that
+* PublisherExtensions can be sure the notification has been processed by all listeners */
+protected Reporter reporter;
+protected final Config config; // to later-on access settings that are only used once (not ideal)
+// don't forget to unregister or we have a HUGE memory leak if the same Config object is
+// reused for several JPF runs
+class ConfigListener implements ConfigChangeListener {
+@Override
+public void propertyChanged(Config config, String key, String oldValue, String newValue) {
+// Different Config instance
+if (!config.equals(Search.this.config)) {
+return;
+}
+// Check if Search configuration changed
+if (key.startsWith("search.")){
+String k = key.substring(7);
+if ("match_depth".equals(k) ||
+"min_free".equals(k) ||
+"multiple_errors".equals(k)){
+initialize(config);
+}
+}
+}
+@Override
+public void jpfRunTerminated (Config config){
+config.removeChangeListener(this);
+}
+}
+/** storage to keep track of state depths */
+protected final IntVector stateDepth = new IntVector();
+protected Search (Config config, VM vm) {
+this.vm = vm;
+this.config = config;
+initialize( config);
+properties = getProperties(config);
+if (properties.isEmpty()) {
+log.severe("no property");
+}
+config.addChangeListener( new ConfigListener());
+}
+protected void initialize( Config conf){
+depthLimit = conf.getInt("search.depth_limit", Integer.MAX_VALUE);
+matchDepth = conf.getBoolean("search.match_depth");
+minFreeMemory = conf.getMemorySize("search.min_free", 1024<<10);
+getAllErrors = conf.getBoolean("search.multiple_errors");
+}
+/**
+* called after the JPF run is finished. Shouldn't be public, but is called by JPF
+*/
+public void cleanUp(){
+// nothing here, the ConfigListener removes itself
+}
+public Config getConfig() {
+return config;
+}
+public abstract void search ();
+public void setReporter(Reporter reporter){
+this.reporter = reporter;
+}
+public void addListener (SearchListener newListener) {
+log.info("SearchListener added: ", newListener);
+listeners = Misc.appendElement(listeners, newListener);
+}
+public boolean hasListenerOfType (Class<?> listenerCls) {
+return Misc.hasElementOfType(listeners, listenerCls);
+}
+public <T> T getNextListenerOfType(Class<T> type, T prev){
+return Misc.getNextElementOfType(listeners, type, prev);
+}
+public void removeListener (SearchListener removeListener) {
+listeners = Misc.removeElement(listeners, removeListener);
+}
+public void addProperty (Property newProperty) {
+properties.add(newProperty);
+}
+public void removeProperty (Property oldProperty) {
+properties.remove(oldProperty);
+}
+/**
+* return set of configured properties
+* note there is a name clash here - JPF 'properties' have nothing to do with
+* Java properties (java.util.Properties)
+*/
+protected ArrayList<Property> getProperties (Config config) {
+Class<?>[] argTypes = { Config.class, Search.class };
+Object[] args = { config, this };
+ArrayList<Property> list = config.getInstances("search.properties", Property.class,
+argTypes, args);
+return list;
+}
+// check for property violation, return true if not done
+protected boolean hasPropertyTermination () {
+if (currentError != null){
+if (done){
+return true;
+} else { // we search for multiple errors, so we ignore and go on
+doBacktrack = true;
+}
+}
+return false;
+}
+// this should only be called once per transition, otherwise it keeps adding the same error
+protected boolean checkPropertyViolation () {
+for (Property p : properties) {
+if (!p.check(this, vm)) {
+error(p, vm.getClonedPath(), vm.getThreadList());
+return true;
+}
+}
+return false;
+}
+public List<Error> getErrors () {
+return errors;
+}
+public int getNumberOfErrors(){
+return errors.size();
+}
+public String getLastSearchConstraint() {
+return lastSearchConstraint;
+}
+/**
+* request a probe
+*
+* This does not do the actual listener notification, it only stores
+* the request, which is then processed from within JPFs inner execution loop.
+* As a consequence, probeSearch() can be called async, and searchProbed() listeners
+* don't have to bother with synchronization or inconsistent JPF states (notification
+* happens from within JPFs main thread after a completed Instruction execution)
+*/
+public void probeSearch(){
+notifyProbeListeners.set(true);
+}
+/**
+* this does the actual notification and resets the request, hence this call
+* should only happen from within JPFs main thread
+*/
+public void checkAndResetProbeRequest(){
+if (notifyProbeListeners.compareAndSet(true, false)){
+notifySearchProbed();
+}
+}
+/**
+* @return error encountered during *last* transition (null otherwise)
+*/
+public Error getCurrentError(){
+return currentError;
+}
+public Error getLastError() {
+int i=errors.size()-1;
+if (i >=0) {
+return errors.get(i);
+} else {
+return null;
+}
+}
+public boolean hasErrors(){
+return !errors.isEmpty();
+}
+public VM getVM() {
+return vm;
+}
+public boolean isEndState () {
+return vm.isEndState();
+}
+public boolean isErrorState(){
+return (currentError != null);
+}
+public boolean hasNextState () {
+return !isEndState();
+}
+public boolean transitionOccurred(){
+return vm.transitionOccurred();
+}
+public boolean isNewState () {
+boolean isNew = vm.isNewState();
+if (matchDepth) {
+int id = vm.getStateId();
+if (isNew) {
+setStateDepth(id, depth);
+} else {
+return depth < getStateDepth(id);
+}
+}
+return isNew;
+}
+public boolean isVisitedState () {
+return !isNewState();
+}
+public boolean isIgnoredState(){
+return vm.isIgnoredState();
+}
+public boolean isProcessedState(){
+return vm.getChoiceGenerator().isProcessed();
+}
+public boolean isDone(){
+return done;
+}
+public int getDepth () {
+return depth;
+}
+public String getSearchConstraint () {
+return lastSearchConstraint;
+}
+public Transition getTransition () {
+return vm.getLastTransition();
+}
+public int getStateId () {
+return vm.getStateId();
+}
+public int getPurgedStateId () {
+return -1; // a lot of Searches don't purge any states
+}
+/**
+* this is somewhat redundant to SystemState.setIgnored(), but we don't
+* want to mix the case of overriding state matching with backtracking when
+* searching for multiple errors
+*/
+public boolean requestBacktrack () {
+return doBacktrack = true;
+}
+protected boolean checkAndResetBacktrackRequest() {
+if (doBacktrack){
+doBacktrack = false;
+return true;
+} else {
+return false;
+}
+}
+public boolean supportsBacktrack () {
+return true;
+}
+public boolean supportsRestoreState () {
+// not supported by default
+return false;
+}
+public int getDepthLimit () {
+return depthLimit;
+}
+public void setDepthLimit(int limit){
+depthLimit = limit;
+}
+protected SearchState getSearchState () {
+return new SearchState(this);
+}
+// can be used by SearchListeners to create path-less errors (liveness)
+public void error (Property property) {
+error(property, null, null);
+}
+public void error (Property property, Path path, ThreadList threadList) {
+if (getAllErrors) {
+// otherwise we are going to overwrite it if we go on
+try {
+property = property.clone();
+path = path.clone();
+threadList = (ThreadList) threadList.clone(); // this makes it a snapshot (deep) clone
+} catch (CloneNotSupportedException cnsx){
+throw new JPFException("failed to clone error information: " + cnsx);
+}
+done = false;
+} else {
+done = true;
+}
+currentError = new Error(errors.size()+1, property, path, threadList);
+errors.add(currentError);
+// we should not reset the property until listeners have been notified
+// (the listener might be the property itself, in which case it could get
+// confused if propertyViolated() notifications happen after a reset)
+}
+public void resetProperties(){
+for (Property p : properties) {
+p.reset();
+}
+}
+protected void notifyStateAdvanced () {
+try {
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].stateAdvanced(this);
+}
+if (reporter != null){
+// reporter always comes last to ensure all listeners have been notified
+reporter.stateAdvanced(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during stateAdvanced() notification", t);
+}
+}
+protected void notifyStateProcessed() {
+try {
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].stateProcessed(this);
+}
+if (reporter != null){
+reporter.stateProcessed(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during stateProcessed() notification", t);
+}
+}
+protected void notifyStateStored() {
+try {
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].stateStored(this);
+}
+if (reporter != null){
+reporter.stateStored(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during stateStored() notification", t);
+}
+}
+protected void notifyStateRestored() {
+try {
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].stateRestored(this);
+}
+if (reporter != null){
+reporter.stateRestored(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during stateRestored() notification", t);
+}
+}
+protected void notifyStateBacktracked() {
+try {
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].stateBacktracked(this);
+}
+if (reporter != null){
+reporter.stateBacktracked(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during stateBacktracked() notification", t);
+}
+}
+protected void notifyStatePurged() {
+try {
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].statePurged(this);
+}
+if (reporter != null){
+reporter.statePurged(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during statePurged() notification", t);
+}
+}
+public void notifySearchProbed() {
+try {
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].searchProbed(this);
+}
+if (reporter != null){
+reporter.searchProbed(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during searchProbed() notification", t);
+}
+}
+protected void notifyPropertyViolated() {
+try {
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].propertyViolated(this);
+}
+if (reporter != null){
+reporter.propertyViolated(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during propertyViolated() notification", t);
+}
+// reset properties if getAllErrors is set
+if (getAllErrors){
+resetProperties();
+}
+}
+protected void notifySearchStarted() {
+try {
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].searchStarted(this);
+}
+if (reporter != null){
+reporter.searchStarted(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during searchStarted() notification", t);
+}
+}
+public void notifySearchConstraintHit(String details) {
+try {
+lastSearchConstraint = details;
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].searchConstraintHit(this);
+}
+if (reporter != null){
+reporter.searchConstraintHit(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during searchConstraintHit() notification", t);
+}
+}
+protected void notifySearchFinished() {
+try {
+for (int i = 0; i < listeners.length; i++) {
+listeners[i].searchFinished(this);
+}
+if (reporter != null){
+reporter.searchFinished(this);
+}
+} catch (Throwable t) {
+throw new JPFListenerException("exception during searchFinished() notification", t);
+}
+}
+protected boolean forward () {
+currentError = null;
+boolean ret = vm.forward();
+checkPropertyViolation();
+return ret;
+}
+protected boolean backtrack () {
+return vm.backtrack();
+}
+public void setIgnoredState (boolean cond) {
+vm.ignoreState(cond);
+}
+protected void restoreState (State state) {
+// not supported by default
+}
+/** this can be used by listeners to terminate the search */
+public void terminate () {
+done = true;
+}
+protected void setStateDepth (int stateId, int depth) {
+stateDepth.set(stateId, depth + 1);
+}
+public int getStateDepth (int stateId) {
+int depthPlusOne = stateDepth.get(stateId);
+if (depthPlusOne <= 0) {
+throw new JPFException("Asked for depth of unvisited state");
+} else {
+return depthPlusOne - 1;
+}
+}
+/**
+* check if we have a minimum amount of free memory left. If not, we rather want to stop in time
+* (with a threshold amount left) so that we can report something useful, and not just die silently
+* with a OutOfMemoryError (which isn't handled too gracefully by most VMs)
+*/
+public boolean checkStateSpaceLimit () {
+Runtime rt = Runtime.getRuntime();
+long avail = rt.freeMemory();
+// we could also just check for a max number of states, but what really
+// limits us is the memory required to store states
+if (avail < minFreeMemory) {
+// try to collect first
+rt.gc();
+avail = rt.freeMemory();
+if (avail < minFreeMemory) {
+// Ok, we give up, threshold reached
+return false;
+}
+}
+return true;
+}
+}

Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/search/Search.java @ 0:61d41facf527