2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.ListenerAdapter;
24 * time model that uses instruction count along current path to deduce
27 * NOTE: the requirement that time has to be strictly increasing along a path
28 * means we cannot skip the initialization
30 public class ConstInsnPathTime extends ListenerAdapter implements TimeModel {
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 {
42 int perInsnTime; // simple constant time assumed for each instruction
44 long transitionStartTime;
46 public ConstInsnPathTime (VM vm, Config conf){
47 perInsnTime = conf.getInt("vm.time.per_insn", 1);
53 protected long computeTime (){
54 ThreadInfo tiCurrent = vm.getCurrentThread();
55 long t = tiCurrent.getExecutedInstructions() * perInsnTime;
57 return transitionStartTime + t;
60 //-- the listener interface
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;
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);
75 TimeVal tvPrev = cgPrev.getAttr(TimeVal.class); // there has to be one
76 tv = new TimeVal(tvPrev.time + t);
87 public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG){
88 TimeVal tv = currentCG.getAttr(TimeVal.class);
90 transitionStartTime = tv.time;
92 transitionStartTime = 0;
96 //--- the TimeModel interface
98 public long currentTimeMillis() {
103 public long nanoTime() {
104 return computeTime();