src/peers/gov/nasa/jpf/vm/JPF_java_io_OutputStreamWriter.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.CharsetEncoder;
  28
  29 /**
  30  * native peer for OutputStreamWriter, to avoid that we have the
  31  * char-to-byte conversion in JPF
  32  *
  33  * <2do> this needs to be de-staticed (see model class)
  34  */
  35 public class JPF_java_io_OutputStreamWriter extends NativePeer {
  36
  37   static final int BUF_SIZE=128; // needs to be the same as in the model class!
  38   static CharsetEncoder encoder;
  39
  40   static CharBuffer in = CharBuffer.allocate(BUF_SIZE);
  41   static ByteBuffer out = ByteBuffer.allocate(BUF_SIZE*6); // worst case UTF-8
  42
  43   public JPF_java_io_OutputStreamWriter() {
  44     encoder = Charset.defaultCharset().newEncoder();
  45   }
  46
  47   @MJI
  48   public int encode___3CII_3B__I (MJIEnv env, int objref,
  49                                          int cref, int off, int len,
  50                                          int bref){
  51     if (len > BUF_SIZE){ // check for buffer overflow
  52       len = BUF_SIZE;
  53     }
  54     int imax = off+len;
  55
  56     out.clear();
  57     in.clear();
  58
  59     for (int i=off; i<imax; i++){
  60       in.put(env.getCharArrayElement(cref, i));
  61     }
  62
  63     in.flip();
  64     encoder.encode(in,out,true);
  65
  66     int n = out.position();
  67     for (int i=0; i<n; i++){
  68       env.setByteArrayElement(bref,i,out.get(i));
  69     }
  70
  71     return n;
  72   }
  73
  74   @MJI
  75   public int encode__Ljava_lang_String_2II_3B__I (MJIEnv env, int objref,
  76                                          int sref, int off, int len,
  77                                          int bref){
  78     int cref = env.getReferenceField(sref, "value");
  79
  80     return encode___3CII_3B__I(env,objref,cref,off,len,bref);
  81   }
  82
  83   @MJI
  84   public int encode__C_3B__I (MJIEnv env, int objref, char c, int bufref) {
  85     out.clear();
  86
  87     in.clear();
  88     in.put(c);
  89     in.flip();
  90
  91     encoder.encode(in,out,true);
  92
  93     int n = out.position();
  94     for (int i=0; i<n; i++){
  95       env.setByteArrayElement(bufref,i,out.get(i));
  96     }
  97
  98     return n;
  99   }
 100 }