src/main/gov/nasa/jpf/perturb/GenericDataAbstractor.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.perturb;
  20
  21 import java.util.Random;
  22 import java.util.Vector;
  23 import gov.nasa.jpf.Config;
  24 import gov.nasa.jpf.vm.ChoiceGenerator;
  25 import gov.nasa.jpf.vm.IntChoiceGenerator;
  26 import gov.nasa.jpf.vm.MethodInfo;
  27 import gov.nasa.jpf.vm.StackFrame;
  28 import gov.nasa.jpf.vm.Types;
  29 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
  30
  31 /**
  32  * This file implements a generic data abstraction module that can be used
  33  * with the Perturbator to execute a method with a choice of values for the
  34  * method parameters.
  35  *
  36  * This module handles all basic types and selects values for them as follows:
  37  * int, short: random negative integer | 0 | random positive integer
  38  * float: random negative floating point | 0 | random positive floating point
  39  * char: two random values in [0, 255] and an explicit 0
  40  * boolean: true | false
  41  *
  42  * An instance of this class is expected to be specialized for each method that we
  43  * want perturbed. The cstor creates a vector of valuations for the parameters
  44  * using all choices for each basic type such that each vector can be written
  45  * directly into the method stack frame for parameters
  46  *
  47  */
  48
  49 public class GenericDataAbstractor implements OperandPerturbator {
  50
  51   // A valuations helper class
  52   public class Valuation {
  53     protected int valuation[] = null;
  54
  55     public Valuation(int size) {
  56       valuation = new int[size];
  57     }
  58     // create an object from an existing valuation
  59     public Valuation(Valuation seedValuation) {
  60       valuation = seedValuation.valuation.clone();
  61     }
  62     public Valuation(Valuation val, int size) {
  63       valuation = new int[size];
  64       int[] valuationArray = val.getValuation();
  65       for (int i = 0; i < valuationArray.length; i++)
  66         valuation[i] = valuationArray[i];
  67     }
  68     public int[] getValuation() {
  69       return valuation;
  70     }
  71     public void add(int index, int element) {
  72       valuation[index] = element;
  73     }
  74   }
  75
  76   static long seed = 5;
  77
  78   protected MethodInfo mi;
  79   protected StackFrame stackFrame;
  80   protected int nParams;
  81   protected byte[] paramTypes = null;
  82   protected String[] paramTypeNames = null;
  83   protected String[] paramNames = null;
  84   protected Vector<Valuation> valuations = new Vector<Valuation>();
  85   protected int choices;
  86   protected int operandSize;
  87   protected Valuation valuation = null;
  88   protected boolean isStatic;
  89   protected Random randomizer = new Random(seed);
  90
  91   public GenericDataAbstractor (Config conf, String keyPrefix){
  92     // this will expand to read parameters from the configuration
  93     // to specialize the behavior of the abstractor
  94     mi = null;
  95     choices = 0;
  96   }
  97
  98   // At the time of instance creation we don't have the MethodInfo object
  99   // for the method that needs its parameters perturbed. Therefore, we
 100   // should set MethodInfo using a call to the following method before
 101   // we can use this instance to perturb a method invocation
 102   public void setMethodInfo(MethodInfo m, StackFrame frame) {
 103     if (mi != null)
 104       return;
 105
 106     mi = m;
 107     stackFrame = frame;
 108     // Need to figure out the right number of parameters.
 109     paramTypes = mi.getArgumentTypes();
 110     paramTypeNames = mi.getArgumentTypeNames();
 111     nParams = paramTypes.length;
 112     isStatic = mi.isStatic();
 113
 114     // now compute the operand size in 32-bit words
 115     operandSize = 0;
 116     for (byte type : paramTypes) {
 117       if (type == Types.T_LONG || type == Types.T_DOUBLE)
 118         operandSize += 2;
 119       else
 120         operandSize++;
 121     }
 122
 123     // useful when we call the various populate methods that populate
 124     // choice vectors. The parameter name can be used to specialize
 125     // population to parameter names
 126     paramNames = new String[nParams];
 127     if (nParams != 0) {
 128         String[] localVars = mi.getLocalVariableNames();
 129         for (int i = 0; i < nParams; i++) {
 130                 paramNames[i] = isStatic? localVars[i] : localVars[i + 1];
 131         }
 132     }
 133
 134     // We build an array of choices, with each choice being an index into
 135     // an array of integers representing the operand stack values.
 136     // We then use an IntChoiceGenerator to give us an index that is then
 137     // used to access the values we want to replace for the operands on the
 138     // stack
 139
 140     valuation = new Valuation(operandSize);
 141     valuations.add(valuation);
 142     populateValuations(frame, 0, 0);
 143
 144     // we now know how many choices there are and hence set choices
 145     choices = valuations.size() - 1;
 146   }
 147
 148   // Method to populate boolean values
 149   public int[] populateBoolean(MethodInfo mi, String name) {
 150     int[] bVec = {0 /* false */, 1 /* true */};
 151
 152     return bVec;
 153   }
 154
 155   // Method to populate character values
 156   public int[] populateChar(MethodInfo mi, String name) {
 157     int[] iVec = {Math.abs(randomizer.nextInt() % 255), 0, Math.abs(randomizer.nextInt() % 255)};
 158
 159     return iVec;
 160   }
 161
 162   // Method to populate byte values
 163   public int[] populateByte(MethodInfo mi, String name) {
 164     int[] iVec = {Math.abs(randomizer.nextInt() % 128), 0, -1 * Math.abs(randomizer.nextInt() % 127)};
 165
 166     return iVec;
 167   }
 168
 169   // Method to populate integer values
 170   public int[] populateInt(MethodInfo mi, String name) {
 171     int[] iVec = {Math.abs(randomizer.nextInt() % 100), 0, -1 * Math.abs(randomizer.nextInt() % 100)};
 172
 173     return iVec;
 174   }
 175
 176   // Method to populate integer values
 177   public int[] populateShort(MethodInfo mi, String name) {
 178     return populateInt(mi, name);
 179   }
 180
 181   // Method to populate long values
 182   public int[] populateLong(MethodInfo mi, String name) {
 183     long[] lVec = {Math.abs(randomizer.nextLong() % 100), 0, -1 * Math.abs(randomizer.nextLong() % 100)};
 184     int[] iVec = new int[lVec.length * 2];
 185
 186     int i = 0;
 187     for (long l : lVec) {
 188       iVec[i++] = Types.hiLong(l);
 189       iVec[i++] = Types.loLong(l);
 190     }
 191     return iVec;
 192   }
 193
 194   // Method to populate integer values
 195   public int[] populateFloat(MethodInfo mi, String name) {
 196     int[] fVec = {Float.floatToIntBits(randomizer.nextFloat()), 0,
 197         -1 * Float.floatToIntBits(randomizer.nextFloat())};
 198
 199     return fVec;
 200   }
 201
 202   // Method to populate long values
 203   public int[] populateDouble(MethodInfo mi, String name) {
 204     double[] dVec = {-1.414, 0.0, 3.141};
 205     int[] iVec = new int[dVec.length * 2];
 206
 207     int i = 0;
 208     for (double d : dVec) {
 209       iVec[i++] = Types.hiDouble(d);
 210       iVec[i++] = Types.loDouble(d);
 211     }
 212     return iVec;
 213   }
 214
 215   public void populateValuations(StackFrame frame, int paramIndex, int dataIndex) {
 216     if (paramIndex == nParams) {
 217       // copy the contents of the previous vector as a
 218       // suffix of it will be over-written, retaining
 219       // the valuations for all parameters ahead of the
 220       // suffix
 221       valuation = new Valuation(valuation);
 222       valuations.add(valuation);
 223     } else {
 224       switch (paramTypes[paramIndex]) {
 225         case Types.T_ARRAY:
 226           populateValuations(frame, paramIndex + 1, dataIndex + 1);
 227           break;
 228         case Types.T_BOOLEAN:
 229           int[] bVec = populateBoolean(mi, paramNames[paramIndex]);
 230           for (int i = 0; i < bVec.length; i++) {
 231             valuation.add(dataIndex, bVec[i]);
 232             populateValuations(frame, paramIndex + 1, dataIndex + 1);
 233           }
 234           break;
 235         case Types.T_FLOAT:
 236           int[] fVec = populateFloat(mi, paramNames[paramIndex]);
 237           for (int i = 0; i < fVec.length; i++) {
 238             valuation.add(dataIndex, fVec[i]);
 239             populateValuations(frame, paramIndex + 1, dataIndex + 1);
 240           }
 241           break;
 242         case Types.T_CHAR:
 243           int[] iVec = populateChar(mi, paramNames[paramIndex]);
 244           for (int i = 0; i < iVec.length; i++) {
 245             valuation.add(dataIndex, iVec[i]);
 246             populateValuations(frame, paramIndex + 1, dataIndex + 1);
 247           }
 248           break;
 249         case Types.T_BYTE:
 250           iVec = populateByte(mi, paramNames[paramIndex]);
 251           for (int i = 0; i < iVec.length; i++) {
 252             valuation.add(dataIndex, iVec[i]);
 253             populateValuations(frame, paramIndex + 1, dataIndex + 1);
 254           }
 255           break;
 256         case Types.T_INT:
 257           iVec = populateInt(mi, paramNames[paramIndex]);
 258           for (int i = 0; i < iVec.length; i++) {
 259             valuation.add(dataIndex, iVec[i]);
 260             populateValuations(frame, paramIndex + 1, dataIndex + 1);
 261           }
 262           break;
 263         case Types.T_SHORT:
 264           iVec = populateShort(mi, paramNames[paramIndex]);
 265           for (int i = 0; i < iVec.length; i++) {
 266             valuation.add(dataIndex, iVec[i]);
 267             populateValuations(frame, paramIndex + 1, dataIndex + 1);
 268           }
 269           break;
 270         case Types.T_LONG:
 271           int[] lVec = populateLong(mi, paramNames[paramIndex]);
 272           int i = 0;
 273           while (i < lVec.length) {
 274             valuation.add(dataIndex, lVec[i++]);
 275             valuation.add(dataIndex + 1, lVec[i++]);
 276             populateValuations(frame, paramIndex + 1, dataIndex + 2);
 277           }
 278           break;
 279         case Types.T_DOUBLE:
 280           int[] dVec = populateDouble(mi, paramNames[paramIndex]);
 281           i = 0;
 282           while (i < dVec.length) {
 283             valuation.add(dataIndex, dVec[i++]);
 284             valuation.add(dataIndex + 1, dVec[i++]);
 285             populateValuations(frame, paramIndex + 1, dataIndex + 2);
 286           }
 287           break;
 288       }
 289     }
 290   }
 291
 292   @Override
 293   public ChoiceGenerator<?> createChoiceGenerator (String id, StackFrame frame, Object refObject) {
 294     // We expect that the refObject in this case will be a MethodInfo object
 295     // Set it so that we can create valuation vectors
 296     assert refObject instanceof MethodInfo : "wrong refObject type for GenericDataAbstractor: " +
 297     refObject.getClass().getName();
 298
 299   setMethodInfo((MethodInfo)refObject, frame);
 300
 301   if (choices > 0) {
 302     // now create a choices vector which will be used to iterate over the number of
 303     // parameter valuations we want to use. We set each element of the vector simply
 304     // to an index into the valuations vector
 305     int[] indices = new int[choices];
 306     for (int i = 0; i < choices; i++) {
 307       indices[i] = i;
 308     }
 309     return new IntChoiceFromSet(id, indices);
 310   } else
 311     return null;
 312   }
 313
 314   @Override
 315   public boolean perturb(ChoiceGenerator<?>cg, StackFrame frame) {
 316     assert cg instanceof IntChoiceGenerator : "wrong choice generator type for GenericDataAbstractor: " + cg.getClass().getName();
 317
 318   int choice = ((IntChoiceGenerator)cg).getNextChoice();
 319   Valuation valuation = valuations.get(choice);
 320
 321   // iterate over the number of operands and set the operand array to the values
 322   // we have in the valuation vector
 323   int val = 0;
 324
 325   int top = frame.getTopPos();
 326   int stackIdx = frame.getLocalVariableCount() + ((isStatic)? 0 : 1);
 327   int argSize = paramTypes.length;
 328
 329   for (int j = 0; j < argSize; j++) { // j ranges over actual arguments
 330     if (!frame.isOperandRef(top - stackIdx)) {
 331       frame.setOperand(top - stackIdx++, valuation.getValuation()[val++], false);
 332       if (paramTypes[j] == Types.T_LONG || paramTypes[j] == Types.T_DOUBLE) {
 333         frame.setOperand(top - stackIdx++, valuation.getValuation()[val++], false);
 334       }
 335     }
 336   }
 337
 338   return cg.hasMoreChoices();
 339   }
 340
 341   @Override
 342   public Class<? extends ChoiceGenerator<?>> getChoiceGeneratorType(){
 343     return IntChoiceFromSet.class;
 344   }
 345 }