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.
19 package gov.nasa.jpf.listener;
21 import gov.nasa.jpf.vm.Instruction;
22 import gov.nasa.jpf.Config;
23 import gov.nasa.jpf.JPFConfigException;
24 import gov.nasa.jpf.PropertyListenerAdapter;
25 import gov.nasa.jpf.jvm.bytecode.*;
26 import gov.nasa.jpf.search.Search;
27 import gov.nasa.jpf.util.FieldSpec;
28 import gov.nasa.jpf.util.VarSpec;
29 import gov.nasa.jpf.vm.FieldInfo;
30 import gov.nasa.jpf.vm.VM;
31 import gov.nasa.jpf.vm.LocalVarInfo;
32 import gov.nasa.jpf.vm.MethodInfo;
33 import gov.nasa.jpf.vm.StackFrame;
34 import gov.nasa.jpf.vm.ThreadInfo;
37 * little listener that checks value ranges of specified numeric fields and local vars
39 * configuration examples:
41 * range.fields=speed,..
42 * range.speed.field=x.y.SomeClass.velocity
46 * range.vars=altitude,..
47 * range.altitude.var=x.y.SomeClass.computeTrajectory(int):a
48 * range.altitude.min=125000
51 public class NumericValueChecker extends PropertyListenerAdapter {
53 static abstract class RangeCheck {
56 RangeCheck (double min, double max){
61 String check (long v){
63 return String.format("%d < %d", v, (long)min);
64 } else if (v > (long)max){
65 return String.format("%d > %d", v, (long)max);
69 String check (double v){
71 return String.format("%f < %f", v, min);
72 } else if (v > (long)max){
73 return String.format("%f > %f", v, max);
79 static class FieldCheck extends RangeCheck {
82 FieldCheck (FieldSpec fspec, double min, double max){
87 boolean matches (FieldInfo fi){
88 return fspec.matches(fi);
92 static class VarCheck extends RangeCheck {
95 VarCheck (VarSpec vspec, double min, double max){
100 LocalVarInfo getMatch (MethodInfo mi, int pc, int slotIdx){
101 return vspec.getMatchingLocalVarInfo(mi, pc, slotIdx);
105 class Visitor extends JVMInstructionVisitorAdapter {
107 void checkFieldInsn (JVMFieldInstruction insn){
108 if (fieldChecks != null){
109 FieldInfo fi = insn.getFieldInfo();
111 for (int i = 0; i < fieldChecks.length; i++) {
112 FieldCheck fc = fieldChecks[i];
113 if (fc.matches(fi)) {
114 if (fi.isNumericField()) {
115 long lv = insn.getLastValue();
116 String errorCond = fi.isFloatingPointField()
117 ? fc.check(Double.longBitsToDouble(lv)) : fc.check(lv);
119 if (errorCond != null) {
120 error = String.format("field %s out of range: %s\n\t at %s",
121 fi.getFullName(), errorCond, insn.getSourceLocation());
122 vm.breakTransition("fieldValueOutOfRange"); // terminate this transition
131 void checkVarInsn (JVMLocalVariableInstruction insn){
132 if (varChecks != null){
133 ThreadInfo ti = ThreadInfo.getCurrentThread();
134 StackFrame frame = ti.getTopFrame();
135 int slotIdx = insn.getLocalVariableIndex();
137 for (int i = 0; i < varChecks.length; i++) {
138 VarCheck vc = varChecks[i];
140 MethodInfo mi = insn.getMethodInfo();
141 int pc = insn.getPosition()+1; // the scope would begin on the next insn, we are still at the xSTORE
142 LocalVarInfo lvar = vc.getMatch(mi, pc, slotIdx);
144 long v = lvar.getSlotSize() == 1 ? frame.getLocalVariable(slotIdx) : frame.getLongLocalVariable(slotIdx);
145 String errorCond = lvar.isFloatingPoint()
146 ? vc.check(Double.longBitsToDouble(v)) : vc.check(v);
148 if (errorCond != null) {
149 error = String.format("local variable %s out of range: %s\n\t at %s",
150 lvar.getName(), errorCond, insn.getSourceLocation());
151 vm.breakTransition("localVarValueOutOfRange"); // terminate this transition
160 public void visit(PUTFIELD insn){
161 checkFieldInsn(insn);
164 public void visit(PUTSTATIC insn){
165 checkFieldInsn(insn);
169 public void visit(ISTORE insn){
173 public void visit(LSTORE insn){
177 public void visit(FSTORE insn){
181 public void visit(DSTORE insn){
191 // the stuff we monitor
192 FieldCheck[] fieldChecks;
193 VarCheck[] varChecks;
195 String error; // where we store errorCond details
197 public NumericValueChecker (Config conf){
198 visitor = new Visitor();
200 createFieldChecks(conf);
201 createVarChecks(conf);
204 private void createFieldChecks(Config conf){
205 String[] checkIds = conf.getCompactTrimmedStringArray("range.fields");
206 if (checkIds.length > 0){
207 fieldChecks = new FieldCheck[checkIds.length];
209 for (int i = 0; i < checkIds.length; i++) {
210 String id = checkIds[i];
211 FieldCheck check = null;
212 String keyPrefix = "range." + id;
213 String spec = conf.getString(keyPrefix + ".field");
215 FieldSpec fs = FieldSpec.createFieldSpec(spec);
217 double min = conf.getDouble(keyPrefix + ".min", Double.MIN_VALUE);
218 double max = conf.getDouble(keyPrefix + ".max", Double.MAX_VALUE);
219 check = new FieldCheck(fs, min, max);
223 throw new JPFConfigException("illegal field range check specification for " + id);
225 fieldChecks[i] = check;
230 private void createVarChecks(Config conf){
231 String[] checkIds = conf.getCompactTrimmedStringArray("range.vars");
232 if (checkIds.length > 0){
233 varChecks = new VarCheck[checkIds.length];
235 for (int i = 0; i < checkIds.length; i++) {
236 String id = checkIds[i];
237 VarCheck check = null;
238 String keyPrefix = "range." + id;
239 String spec = conf.getString(keyPrefix + ".var");
241 VarSpec vs = VarSpec.createVarSpec(spec);
243 double min = conf.getDouble(keyPrefix + ".min", Double.MIN_VALUE);
244 double max = conf.getDouble(keyPrefix + ".max", Double.MAX_VALUE);
245 check = new VarCheck(vs, min, max);
249 throw new JPFConfigException("illegal variable range check specification for " + id);
251 varChecks[i] = check;
257 public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn){
259 ((JVMInstruction)executedInsn).accept(visitor);
263 public boolean check(Search search, VM vm) {
264 return (error == null);
268 public void reset () {
273 public String getErrorMessage(){