src/peers/gov/nasa/jpf/vm/JPF_java_io_InputStreamReader.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 import java.nio.ByteBuffer;
  25 import java.nio.CharBuffer;
  26 import java.nio.charset.Charset;
  27 import java.nio.charset.CharsetDecoder;
  28
  29 public class JPF_java_io_InputStreamReader extends NativePeer {
  30
  31   static final int BUF_SIZE = 128;
  32
  33   // <2do> decoder should be stored on a per-reader basis, since Charsets
  34   // might differ
  35   CharsetDecoder decoder;
  36
  37   // ..same here - that's a shared resource with state! Only works for now
  38   // since all InputStreamReader decoding is protected by the same lock
  39   ByteBuffer in = ByteBuffer.allocate(BUF_SIZE);
  40   CharBuffer out = CharBuffer.allocate(BUF_SIZE);
  41
  42   public JPF_java_io_InputStreamReader() {
  43     decoder = Charset.defaultCharset().newDecoder();
  44   }
  45
  46   @MJI
  47   public int decode___3BI_3CIZ__I (MJIEnv env, int objref,
  48                                          int bref, int len, int cref, int off,
  49                                          boolean endOfInput){
  50     int c = -1;
  51     int lim = in.limit();
  52
  53     if (lim < in.capacity()){ // left-over bytes
  54       in.clear();
  55       in.position(lim);
  56     } else {
  57       decoder.reset();
  58     }
  59     for (int i=0; i<len; i++){
  60       in.put(env.getByteArrayElement(bref,i));
  61     }
  62     in.flip();
  63
  64     decoder.decode(in,out,endOfInput);
  65
  66     int n = out.position();
  67     for (int i=0, j=off; i<n; i++,j++){
  68       env.setCharArrayElement(cref,j, out.get(i));
  69     }
  70     out.clear();
  71     if (n == len){
  72       in.clear();
  73     }
  74
  75     return n;
  76   }
  77
  78
  79   // <2do> - that fails if we have a multi byte char and there is a backtrack
  80   // between decode() calls. Granted, that seems strange, but there is an
  81   // InputStream.read() in the loop which might just branch into user code
  82   @MJI
  83   public int decode__IZ__I (MJIEnv env, int objref, int b, boolean endOfInput){
  84     int c = -1;
  85     int lim = in.limit();
  86
  87     // this is terrible overhead to get a single char, I must be doing something wrong..
  88
  89     if (lim < in.capacity()){ // left-over bytes
  90       in.clear();
  91       in.position(lim);
  92     } else {
  93       decoder.reset();
  94     }
  95
  96     in.put((byte)b);
  97     in.flip();
  98
  99     decoder.decode(in,out,endOfInput);
 100
 101     if (out.position() == 1){
 102       c = out.get(0);
 103       out.clear();
 104       in.clear();
 105     }
 106
 107     return c;
 108   }
 109 }