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.listener;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.JPF;
22 import gov.nasa.jpf.ListenerAdapter;
23 import gov.nasa.jpf.annotation.JPFOption;
24 import gov.nasa.jpf.annotation.JPFOptions;
25 import gov.nasa.jpf.report.Publisher;
26 import gov.nasa.jpf.search.Search;
27 import gov.nasa.jpf.vm.Instruction;
28 import gov.nasa.jpf.vm.ThreadInfo;
29 import gov.nasa.jpf.vm.VM;
31 import java.lang.management.ManagementFactory;
32 import java.lang.management.MemoryMXBean;
33 import java.lang.management.MemoryUsage;
36 * Listener that implements various budget constraints
39 @JPFOption(type = "Long", key = "budget.max_time", defaultValue= "-1", comment = "stop search after specified duration [msec]"),
40 @JPFOption(type = "Long", key = "budget.max_heap", defaultValue = "-1", comment="stop search when VM heapsize reaches specified limit"),
41 @JPFOption(type = "Int", key = "budget.max_depth", defaultValue = "-1", comment = "stop search at specified search depth"),
42 @JPFOption(type = "long", key = "budget.max_insn", defaultValue = "-1", comment = "stop search after specified number of intstructions"),
43 @JPFOption(type = "Int", key = "budget.max_state", defaultValue = "-1", comment = "stop search when reaching specified number of new states"),
44 @JPFOption(type = "Int", key = "budget.max_new_states", defaultValue = "-1", comment="stop search ater specified number of non-replayed new states")
46 public class BudgetChecker extends ListenerAdapter {
48 static final int CHECK_INTERVAL = 10000;
49 static final int CHECK_INTERVAL1 = CHECK_INTERVAL-1;
60 //--- the budget thresholds
71 // the message explaining the exceeded budget
74 public BudgetChecker (Config conf, JPF jpf) {
76 //--- get the configured budget limits (0 means not set)
77 maxTime = conf.getDuration("budget.max_time", 0);
78 maxHeap = conf.getMemorySize("budget.max_heap", 0);
79 maxDepth = conf.getInt("budget.max_depth", 0);
80 maxInsn = conf.getLong("budget.max_insn", 0);
81 maxState = conf.getInt("budget.max_state", 0);
82 maxNewStates = conf.getInt("budget.max_new_states", 0);
84 tStart = System.currentTimeMillis();
87 mxb = ManagementFactory.getMemoryMXBean();
88 muStart = mxb.getHeapMemoryUsage();
89 mStart = muStart.getUsed();
92 search = jpf.getSearch();
96 public boolean timeExceeded() {
98 long dur = System.currentTimeMillis() - tStart;
100 message = "max time exceeded: " + Publisher.formatHMS(dur)
101 + " >= " + Publisher.formatHMS(maxTime);
109 public boolean heapExceeded() {
111 MemoryUsage mu = mxb.getHeapMemoryUsage();
112 long used = mu.getUsed() - mStart;
113 if (used > maxHeap) {
114 message = "max heap exceeded: " + (used / (1024*1024)) + "MB"
115 + " >= " + (maxHeap / (1024*1024)) + "MB" ;
123 public boolean depthExceeded () {
125 int d = search.getDepth();
127 message = "max search depth exceeded: " + maxDepth;
135 public boolean statesExceeded () {
137 int stateId = vm.getStateId();
138 if (stateId > maxState) {
139 message = "max states exceeded: " + maxState;;
147 public boolean insnExceeded () {
149 if (insnCount > maxInsn) {
150 message = "max instruction count exceeded: " + maxInsn;
157 public boolean newStatesExceeded(){
158 if (maxNewStates > 0){
159 if (newStates > maxNewStates) {
160 message = "max new state count exceeded: " + maxNewStates;
168 public void stateAdvanced (Search search) {
169 if (timeExceeded() || heapExceeded()) {
170 search.notifySearchConstraintHit(message);
174 if (search.isNewState()){
175 if (!vm.isTraceReplay()){
178 if (statesExceeded() || depthExceeded() || newStatesExceeded()){
179 search.notifySearchConstraintHit(message);
186 public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
187 if ((insnCount++ % CHECK_INTERVAL) == CHECK_INTERVAL1) {
189 if (timeExceeded() || heapExceeded() || insnExceeded()) {
190 search.notifySearchConstraintHit(message);
192 vm.getCurrentThread().breakTransition("budgetConstraint");