Mercurial > hg > Members > kono > jpf-core
view src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java @ 15:cb7500a46eab
some minor syntax fixes to make IntelliJ happy
author | Peter Mehlitz <pcmehlitz@gmail.com> |
---|---|
date | Wed, 18 Mar 2015 11:52:11 -0700 |
parents | b920e6b1be83 |
children | caa0924e093d |
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.JPF; import gov.nasa.jpf.annotation.MJI; import gov.nasa.jpf.util.JPFLogger; import gov.nasa.jpf.util.event.CheckEvent; import gov.nasa.jpf.util.event.EventContext; import gov.nasa.jpf.util.event.Event; import gov.nasa.jpf.util.event.EventChoiceGenerator; import gov.nasa.jpf.util.event.EventTree; import gov.nasa.jpf.util.event.NoEvent; /** * native peer for EventProducer */ public class JPF_gov_nasa_jpf_EventProducer extends NativePeer { static final String CG_NAME = "processNextEvent"; public static JPFLogger log = JPF.getLogger("event"); protected EventTree eventTree; protected Event event; protected EventContext ctx; // optional public JPF_gov_nasa_jpf_EventProducer (Config config){ eventTree = config.getEssentialInstance(EventTree.CONFIG_KEY, EventTree.class); ctx = config.getInstance("event.context.class", EventContext.class); logger.info("event tree generated by: ", eventTree.getClass().getName()); if (ctx != null){ logger.info("using context event: ", ctx.getClass().getName()); } } //--- those can be used by subclasses to add additional processing steps during processNextEvent /** * override this if the event processing results in direct calls, i.e. there is no change in the model method calling * processNextEvent */ protected boolean hasReturnedFormDirectCall (MJIEnv env, int objRef){ return false; } /** * nothing here, to be overridden in case processing has to happen in the native peer * this is only called from within generateNextEvent() */ protected void processEvent (MJIEnv env, int objRef){ } /** * evaluate a pseudo event that checks properties */ protected boolean checkEvent (MJIEnv env, int objRef){ return ((CheckEvent)event).check(env); } /** * nothing here, to be overridden by subclasses that have to force states, modify the CG on the fly etc. */ protected EventChoiceGenerator processNextCG (MJIEnv env, int objRef, EventChoiceGenerator cg){ return cg; } /** * this is our main purpose in life - processing events * * @return true if there was another event, false if there isn't any event left on this path */ @MJI public boolean processNextEvent____Z (MJIEnv env, int objRef){ ThreadInfo ti = env.getThreadInfo(); if (hasReturnedFormDirectCall( env, objRef)){ return true; } SystemState ss = env.getSystemState(); EventChoiceGenerator cg; event = null; if (!ti.isFirstStepInsn()){ EventChoiceGenerator cgPrev = ss.getLastChoiceGeneratorOfType(EventChoiceGenerator.class); if (cgPrev != null){ cg = cgPrev.getSuccessor(CG_NAME, ctx); } else { cg = new EventChoiceGenerator( CG_NAME, eventTree.getRoot(), ctx); } if ((cg = processNextCG(env, objRef, cg)) != null){ if (log.isInfoLogged()){ log.info("next event generator: ", cg.toString()); } ss.setNextChoiceGenerator(cg); env.repeatInvocation(); return true; // does not matter } else { log.info("no more events"); return false; } } else { // re-execution cg = ss.getCurrentChoiceGenerator(CG_NAME, EventChoiceGenerator.class); event = cg.getNextChoice(); if (event != null) { if (!(event instanceof NoEvent)) { if (event instanceof CheckEvent) { CheckEvent ce = (CheckEvent) event; if (log.isInfoLogged()) { log.info("checking: ", ce.getExpression()); } if (!checkEvent(env, objRef)) { env.throwAssertion("checking " + ce.getExpression() + " failed"); } } else { if (log.isInfoLogged()) { log.info("processing event: ", event.toString()); } processEvent(env, objRef); } } return true; } else { return false; } } } @MJI(noOrphanWarning=true) public int getEventName____Ljava_lang_String_2 (MJIEnv env, int objRef){ if (event != null && !(event instanceof NoEvent)){ return env.newString( event.getName()); } else { return MJIEnv.NULL; } } //--- for testing and debugging purposes (requires special EventTree implementations e.g. derived from TestEventTree) // <2do> should be moved to subclass @MJI(noOrphanWarning=true) public boolean checkPath____Z (MJIEnv env, int objRef){ SystemState ss = env.getSystemState(); EventChoiceGenerator cg = ss.getLastChoiceGeneratorOfType(EventChoiceGenerator.class); if (cg != null){ Event lastEvent = cg.getNextChoice(); if (eventTree.checkPath(lastEvent)){ return true; } else { log.warning("trace check for event ", lastEvent.toString(), " failed"); return false; } } else { return false; // there should have been one } } @MJI(noOrphanWarning=true) public boolean isCompletelyCovered____Z (MJIEnv env, int objRef){ return eventTree.isCompletelyCovered(); } }