src/main/gov/nasa/jpf/vm/ConstInsnPathTime.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 package gov.nasa.jpf.vm;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.ListenerAdapter;
  22
  23 /**
  24  * time model that uses instruction count along current path to deduce
  25  * the execution time.
  26  *
  27  * NOTE: the requirement that time has to be strictly increasing along a path
  28  * means we cannot skip the initialization
  29  */
  30 public class ConstInsnPathTime extends ListenerAdapter implements TimeModel {
  31
  32   // note - this class is not public since we want to make sure this listener
  33   // is the only one using this type
  34   static class TimeVal {
  35     final long time;
  36     TimeVal (long t){
  37       time = t;
  38     }
  39   }
  40
  41   VM vm;
  42   int perInsnTime; // simple constant time assumed for each instruction
  43
  44   long transitionStartTime;
  45
  46   public ConstInsnPathTime (VM vm, Config conf){
  47     perInsnTime = conf.getInt("vm.time.per_insn", 1);
  48
  49     vm.addListener(this);
  50     this.vm = vm;
  51   }
  52
  53   protected long computeTime (){
  54     ThreadInfo tiCurrent = vm.getCurrentThread();
  55     long t = tiCurrent.getExecutedInstructions() * perInsnTime;
  56
  57     return transitionStartTime + t;
  58   }
  59
  60   //-- the listener interface
  61   @Override
  62   public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo ti, Instruction executedInsn){
  63     ChoiceGenerator<?> cgPrev = nextCG.getPreviousChoiceGenerator();
  64     ThreadInfo tiCurrent = vm.getCurrentThread();
  65     long t = tiCurrent.getExecutedInstructions() * perInsnTime;
  66
  67     TimeVal tv = null;
  68
  69     if (nextCG.isCascaded()){
  70       // there's got to be a previous one, and its associated with the same insn
  71       tv = cgPrev.getAttr(TimeVal.class);
  72
  73     } else {
  74       if (cgPrev != null){
  75         TimeVal tvPrev = cgPrev.getAttr(TimeVal.class); // there has to be one
  76         tv = new TimeVal(tvPrev.time + t);
  77
  78       } else {
  79         tv = new TimeVal( t);
  80       }
  81     }
  82
  83     nextCG.addAttr( tv);
  84   }
  85
  86   @Override
  87   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG){
  88     TimeVal tv = currentCG.getAttr(TimeVal.class);
  89     if (tv != null){
  90       transitionStartTime = tv.time;
  91     } else {
  92       transitionStartTime = 0;
  93     }
  94   }
  95
  96   //--- the TimeModel interface
  97   @Override
  98   public long currentTimeMillis() {
  99     return computeTime();
 100   }
 101
 102   @Override
 103   public long nanoTime() {
 104     return computeTime();
 105   }
 106
 107 }