src/peers/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_EventProducer.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18
  19 package gov.nasa.jpf.vm;
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.annotation.MJI;
  24 import gov.nasa.jpf.util.JPFLogger;
  25 import gov.nasa.jpf.util.event.CheckEvent;
  26 import gov.nasa.jpf.util.event.EventContext;
  27 import gov.nasa.jpf.util.event.Event;
  28 import gov.nasa.jpf.util.event.EventChoiceGenerator;
  29 import gov.nasa.jpf.util.event.EventTree;
  30 import gov.nasa.jpf.util.event.NoEvent;
  31
  32 /**
  33  * native peer for EventProducer
  34  */
  35 public class JPF_gov_nasa_jpf_EventProducer extends NativePeer {
  36
  37   static final String CG_NAME = "processNextEvent";
  38
  39   public static JPFLogger log = JPF.getLogger("event");
  40
  41   protected EventTree eventTree;
  42   protected Event event;
  43
  44   protected EventContext ctx;  // optional
  45
  46   public JPF_gov_nasa_jpf_EventProducer (Config config){
  47     eventTree = config.getEssentialInstance(EventTree.CONFIG_KEY, EventTree.class);
  48     ctx = config.getInstance("event.context.class", EventContext.class);
  49
  50     logger.info("event tree generated by: ", eventTree.getClass().getName());
  51     if (ctx != null){
  52       logger.info("using context event: ", ctx.getClass().getName());
  53     }
  54   }
  55
  56   //--- those can be used by subclasses to add additional processing steps during processNextEvent
  57
  58   /**
  59    * override this if the event processing results in direct calls, i.e. there is no change in the model method calling
  60    * processNextEvent
  61    */
  62   protected boolean hasReturnedFormDirectCall (MJIEnv env,  int objRef){
  63     return false;
  64   }
  65
  66   /**
  67    * nothing here, to be overridden in case processing has to happen in the native peer
  68    * this is only called from within generateNextEvent()
  69    */
  70   protected void processEvent (MJIEnv env, int objRef){
  71   }
  72
  73   /**
  74    * evaluate a pseudo event that checks properties
  75    */
  76   protected boolean checkEvent (MJIEnv env, int objRef){
  77     return ((CheckEvent)event).check(env, objRef);
  78   }
  79
  80   /**
  81    * nothing here, to be overridden by subclasses that have to force states, modify the CG on the fly etc.
  82    */
  83   protected EventChoiceGenerator processNextCG (MJIEnv env, int objRef, EventChoiceGenerator cg){
  84     return cg;
  85   }
  86
  87   /**
  88    * this is our main purpose in life - processing events
  89    *
  90    * @return true if there was another event, false if there isn't any event left on this path
  91    */
  92   @MJI
  93   public boolean processNextEvent____Z (MJIEnv env, int objRef){
  94     ThreadInfo ti = env.getThreadInfo();
  95
  96     if (hasReturnedFormDirectCall( env, objRef)){
  97       return true;
  98     }
  99
 100     SystemState ss = env.getSystemState();
 101     EventChoiceGenerator cg;
 102
 103     event = null;
 104
 105     if (!ti.isFirstStepInsn()){
 106       EventChoiceGenerator cgPrev = ss.getLastChoiceGeneratorOfType(EventChoiceGenerator.class);
 107       if (cgPrev != null){
 108         cg = cgPrev.getSuccessor(CG_NAME, ctx);
 109       } else {
 110         cg = new EventChoiceGenerator( CG_NAME, eventTree.getRoot(), ctx);
 111       }
 112
 113       if ((cg = processNextCG(env, objRef, cg)) != null){
 114         if (log.isInfoLogged()){
 115           log.info("next event generator: ", cg.toString());
 116         }
 117         ss.setNextChoiceGenerator(cg);
 118         env.repeatInvocation();
 119         return true; // does not matter
 120
 121       } else {
 122         log.info("no more events");
 123         return false;
 124       }
 125
 126     } else { // re-execution
 127       cg = ss.getCurrentChoiceGenerator(CG_NAME, EventChoiceGenerator.class);
 128       event = cg.getNextChoice();
 129
 130       if (event != null) {
 131         if (!(event instanceof NoEvent)) {
 132           if (event instanceof CheckEvent) {
 133             CheckEvent ce = (CheckEvent) event;
 134             if (log.isInfoLogged()) {
 135               log.info("checking: ", ce.getExpression());
 136             }
 137             if (!checkEvent(env, objRef)) {
 138               env.throwAssertion("checking " + ce.getExpression() + " failed");
 139             }
 140
 141           } else {
 142             if (log.isInfoLogged()) {
 143               log.info("processing event: ", event.toString());
 144             }
 145             processEvent(env, objRef);
 146           }
 147         }
 148
 149         return true;
 150
 151       } else {
 152         return false;
 153       }
 154     }
 155   }
 156
 157   @MJI(noOrphanWarning=true)
 158   public int getEventName____Ljava_lang_String_2 (MJIEnv env, int objRef){
 159     if (event != null && !(event instanceof NoEvent)){
 160       return env.newString( event.getName());
 161     } else {
 162       return MJIEnv.NULL;
 163     }
 164   }
 165
 166   //--- for testing and debugging purposes (requires special EventTree implementations e.g. derived from TestEventTree)
 167   // <2do> should be moved to subclass
 168
 169   @MJI(noOrphanWarning=true)
 170   public boolean checkPath____Z (MJIEnv env, int objRef){
 171     SystemState ss = env.getSystemState();
 172     EventChoiceGenerator cg = ss.getLastChoiceGeneratorOfType(EventChoiceGenerator.class);
 173
 174     if (cg != null){
 175       Event lastEvent = cg.getNextChoice();
 176       if (eventTree.checkPath(lastEvent)){
 177         return true;
 178       } else {
 179         log.warning("trace check for event ", lastEvent.toString(), " failed");
 180         return false;
 181       }
 182
 183     } else {
 184       return false; // there should have been one
 185     }
 186   }
 187
 188   @MJI(noOrphanWarning=true)
 189   public boolean isCompletelyCovered____Z (MJIEnv env, int objRef){
 190     return eventTree.isCompletelyCovered();
 191   }
 192 }