src/main/gov/nasa/jpf/listener/NumericValueChecker.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.listener;
  20
  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;
  35
  36 /**
  37  * little listener that checks value ranges of specified numeric fields and local vars
  38  *
  39  * configuration examples:
  40  *
  41  *  range.fields=speed,..
  42  *  range.speed.field=x.y.SomeClass.velocity
  43  *  range.speed.min=300
  44  *  range.speed.max=500
  45  *
  46  *  range.vars=altitude,..
  47  *  range.altitude.var=x.y.SomeClass.computeTrajectory(int):a
  48  *  range.altitude.min=125000
  49  *
  50  */
  51 public class NumericValueChecker extends PropertyListenerAdapter {
  52
  53   static abstract class RangeCheck {
  54     double min, max;
  55
  56     RangeCheck (double min, double max){
  57       this.min = min;
  58       this.max = max;
  59     }
  60
  61     String check (long v){
  62       if (v < (long)min){
  63         return String.format("%d < %d", v, (long)min);
  64       } else if (v > (long)max){
  65         return String.format("%d > %d", v, (long)max);
  66       }
  67       return null;
  68     }
  69     String check (double v){
  70       if (v < min){
  71         return String.format("%f < %f", v, min);
  72       } else if (v > (long)max){
  73         return String.format("%f > %f", v, max);
  74       }
  75       return null;
  76     }
  77   }
  78
  79   static class FieldCheck extends RangeCheck {
  80     FieldSpec fspec;
  81
  82     FieldCheck (FieldSpec fspec, double min, double max){
  83       super(min,max);
  84       this.fspec = fspec;
  85     }
  86
  87     boolean matches (FieldInfo fi){
  88       return fspec.matches(fi);
  89     }
  90   }
  91
  92   static class VarCheck extends RangeCheck {
  93     VarSpec vspec;
  94
  95     VarCheck (VarSpec vspec, double min, double max){
  96       super(min,max);
  97       this.vspec = vspec;
  98     }
  99
 100     LocalVarInfo getMatch (MethodInfo mi, int pc, int slotIdx){
 101       return vspec.getMatchingLocalVarInfo(mi, pc, slotIdx);
 102     }
 103   }
 104
 105   class Visitor extends JVMInstructionVisitorAdapter {
 106
 107     void checkFieldInsn (JVMFieldInstruction insn){
 108       if (fieldChecks != null){
 109         FieldInfo fi = insn.getFieldInfo();
 110
 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);
 118
 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
 123                 break;
 124               }
 125             }
 126           }
 127         }
 128       }
 129     }
 130
 131     void checkVarInsn (JVMLocalVariableInstruction insn){
 132       if (varChecks != null){
 133         ThreadInfo ti = ThreadInfo.getCurrentThread();
 134         StackFrame frame = ti.getTopFrame();
 135         int slotIdx = insn.getLocalVariableIndex();
 136
 137         for (int i = 0; i < varChecks.length; i++) {
 138           VarCheck vc = varChecks[i];
 139
 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);
 143           if (lvar != null) {
 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);
 147
 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
 152               break;
 153             }
 154           }
 155         }
 156       }
 157     }
 158
 159     @Override
 160     public void visit(PUTFIELD insn){
 161       checkFieldInsn(insn);
 162     }
 163     @Override
 164     public void visit(PUTSTATIC insn){
 165       checkFieldInsn(insn);
 166     }
 167
 168     @Override
 169     public void visit(ISTORE insn){
 170       checkVarInsn(insn);
 171     }
 172     @Override
 173     public void visit(LSTORE insn){
 174       checkVarInsn(insn);
 175     }
 176     @Override
 177     public void visit(FSTORE insn){
 178       checkVarInsn(insn);
 179     }
 180     @Override
 181     public void visit(DSTORE insn){
 182       checkVarInsn(insn);
 183     }
 184
 185   }
 186
 187
 188   VM vm;
 189   Visitor visitor;
 190
 191   // the stuff we monitor
 192   FieldCheck[] fieldChecks;
 193   VarCheck[] varChecks;
 194
 195   String error; // where we store errorCond details
 196
 197   public NumericValueChecker (Config conf){
 198     visitor = new Visitor();
 199
 200     createFieldChecks(conf);
 201     createVarChecks(conf);
 202   }
 203
 204   private void createFieldChecks(Config conf){
 205     String[] checkIds = conf.getCompactTrimmedStringArray("range.fields");
 206     if (checkIds.length > 0){
 207       fieldChecks = new FieldCheck[checkIds.length];
 208
 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");
 214         if (spec != null) {
 215           FieldSpec fs = FieldSpec.createFieldSpec(spec);
 216           if (fs != null) {
 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);
 220           }
 221         }
 222         if (check == null) {
 223           throw new JPFConfigException("illegal field range check specification for " + id);
 224         }
 225         fieldChecks[i] = check;
 226       }
 227     }
 228   }
 229
 230   private void createVarChecks(Config conf){
 231     String[] checkIds = conf.getCompactTrimmedStringArray("range.vars");
 232     if (checkIds.length > 0){
 233       varChecks = new VarCheck[checkIds.length];
 234
 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");
 240         if (spec != null) {
 241           VarSpec vs = VarSpec.createVarSpec(spec);
 242           if (vs != null) {
 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);
 246           }
 247         }
 248         if (check == null) {
 249           throw new JPFConfigException("illegal variable range check specification for " + id);
 250         }
 251         varChecks[i] = check;
 252       }
 253     }
 254   }
 255
 256   @Override
 257   public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn){
 258     this.vm = vm;
 259     ((JVMInstruction)executedInsn).accept(visitor);
 260   }
 261
 262   @Override
 263   public boolean check(Search search, VM vm) {
 264     return (error == null);
 265   }
 266
 267   @Override
 268   public void reset () {
 269     error = null;
 270   }
 271
 272   @Override
 273   public String getErrorMessage(){
 274     return error;
 275   }
 276 }