src/peers/gov/nasa/jpf/vm/JPF_java_io_ObjectInputStream.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 package gov.nasa.jpf.vm;
  19
  20 import gov.nasa.jpf.annotation.MJI;
  21 import gov.nasa.jpf.vm.MJIEnv;
  22 import gov.nasa.jpf.vm.NativePeer;
  23
  24 public class JPF_java_io_ObjectInputStream extends NativePeer {
  25
  26   @MJI
  27   public int latestUserDefinedLoader____Ljava_lang_ClassLoader_2 (MJIEnv env, int clsRef){
  28     // class loaders are not yet supported
  29     return MJIEnv.NULL;
  30   }
  31
  32   @MJI
  33   public void bytesToDoubles___3BI_3DII__ (MJIEnv env, int clsRef,
  34                                                   int baRef, int bOff,
  35                                                   int daRef, int dOff,
  36                                                   int nDoubles){
  37     int imax = dOff + nDoubles;
  38     int j=bOff;
  39
  40     for (int i=dOff; i<imax; i++){
  41       byte b0 = env.getByteArrayElement(baRef, j++);
  42       byte b1 = env.getByteArrayElement(baRef, j++);
  43       byte b2 = env.getByteArrayElement(baRef, j++);
  44       byte b3 = env.getByteArrayElement(baRef, j++);
  45       byte b4 = env.getByteArrayElement(baRef, j++);
  46       byte b5 = env.getByteArrayElement(baRef, j++);
  47       byte b6 = env.getByteArrayElement(baRef, j++);
  48       byte b7 = env.getByteArrayElement(baRef, j++);
  49
  50       long bits = 0x00000000000000ff & b7;
  51       bits <<= 8;
  52       bits |= 0x00000000000000ff & b6;
  53       bits <<= 8;
  54       bits |= 0x00000000000000ff & b5;
  55       bits <<= 8;
  56       bits |= 0x00000000000000ff & b4;
  57       bits <<= 8;
  58       bits |= 0x00000000000000ff & b3;
  59       bits <<= 8;
  60       bits |= 0x00000000000000ff & b2;
  61       bits <<= 8;
  62       bits |= 0x00000000000000ff & b1;
  63       bits <<= 8;
  64       bits |= 0x00000000000000ff & b0;
  65
  66       double d = Double.longBitsToDouble(bits);
  67       env.setDoubleArrayElement(daRef, i, d);
  68     }
  69   }
  70
  71   @MJI
  72   public void bytesToFloats___3BI_3FII__ (MJIEnv env, int clsRef,
  73                                                  int baRef, int bOff,
  74                                                  int faRef, int fOff,
  75                                                  int nFloats){
  76     int imax = fOff + nFloats;
  77     int j=bOff;
  78
  79     for (int i=fOff; i<imax; i++){
  80       byte b0 = env.getByteArrayElement(baRef, j++);
  81       byte b1 = env.getByteArrayElement(baRef, j++);
  82       byte b2 = env.getByteArrayElement(baRef, j++);
  83       byte b3 = env.getByteArrayElement(baRef, j++);
  84
  85       int bits = 0x000000ff & b3;
  86       bits <<= 8;
  87       bits |= 0x000000ff & b2;
  88       bits <<= 8;
  89       bits |= 0x000000ff & b1;
  90       bits <<= 8;
  91       bits |= 0x000000ff & b0;
  92
  93       float f = Float.intBitsToFloat(bits);
  94       env.setFloatArrayElement(faRef, i, f);
  95     }
  96   }
  97 }