src/peers/gov/nasa/jpf/vm/JPF_java_io_FileDescriptor.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.vm;
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.annotation.MJI;
  24 import gov.nasa.jpf.util.DynamicObjectArray;
  25 import gov.nasa.jpf.util.JPFLogger;
  26 import gov.nasa.jpf.vm.MJIEnv;
  27 import gov.nasa.jpf.vm.NativePeer;
  28
  29 import java.io.File;
  30 import java.io.FileInputStream;
  31 import java.io.FileOutputStream;
  32 import java.io.IOException;
  33 import java.nio.channels.FileChannel;
  34
  35 /**
  36  * native peer for file descriptors, which are our basic interface to
  37  * access file contents. The implementation used here just forwards
  38  * to FileInputStreams, which is terribly inefficient for frequent
  39  * restores (in which case a simple byte[] buffer would be more efficient)
  40  */
  41 public class JPF_java_io_FileDescriptor extends NativePeer {
  42
  43   static JPFLogger logger = JPF.getLogger("java.io.FileDescriptor");
  44
  45
  46   // NOTE: keep those in sync with the model class
  47   static final int FD_READ = 0;
  48   static final int FD_WRITE = 1;
  49
  50   static final int FD_NEW = 0;
  51   static final int FD_OPENED = 1;
  52   static final int FD_CLOSED = 2;
  53
  54
  55   int count=2;  // count out std handles
  56   DynamicObjectArray<Object> content;
  57
  58   public JPF_java_io_FileDescriptor (Config conf){
  59     content = new DynamicObjectArray<Object>();
  60     count = 2;
  61   }
  62
  63   @MJI
  64   public int open__Ljava_lang_String_2I__I (MJIEnv env, int objref,
  65                                                    int fnameRef, int mode){
  66     String fname = env.getStringObject(fnameRef);
  67     if (mode == FD_READ){
  68       return openRead(fname);
  69     } else if (mode == FD_WRITE){
  70       return openWrite(fname);
  71     } else {
  72       env.throwException("java.io.IOException", "illegal open mode: " + mode);
  73       return -1;
  74     }
  75   }
  76
  77   @MJI
  78   public int openRead (String fname) {
  79     File file = new File(fname);
  80     if (file.exists()) {
  81       try {
  82         FileInputStream fis = new FileInputStream(file);
  83         fis.getChannel(); // just to allocate one
  84
  85         count++;
  86         content.set(count, fis);
  87
  88         logger.info("opening ", fname, " (read) => ", count);
  89
  90         return count;
  91
  92       } catch (IOException x) {
  93         logger.warning("failed to open ", fname, " (read) : ", x);
  94       }
  95     } else {
  96       logger.info("cannot open ", fname, " (read) : file not found");
  97     }
  98
  99     return -1;
 100   }
 101
 102   @MJI
 103   public int openWrite (String fname){
 104     File file = new File(fname);
 105     try {
 106       FileOutputStream fos = new FileOutputStream(file);
 107       fos.getChannel(); // just to allocate one
 108
 109       count++;
 110       content.set(count, fos);
 111
 112       logger.info("opening ", fname, " (write) => ", count);
 113
 114       return count;
 115
 116     } catch (IOException x) {
 117       logger.warning("failed to open ", fname, " (write) : ", x);
 118     }
 119
 120     return -1;
 121   }
 122
 123   @MJI
 124   public void close0 (MJIEnv env, int objref) {
 125     int fd = env.getIntField(objref, "fd");
 126
 127     try {
 128       Object fs = content.get(fd);
 129
 130       if (fs != null){
 131         logger.info("closing ", fd);
 132
 133         if (fs instanceof FileInputStream){
 134           ((FileInputStream)fs).close();
 135         } else {
 136           ((FileOutputStream)fs).close();
 137         }
 138       } else {
 139         logger.warning("cannot close ", fd, " : no such stream");
 140       }
 141       content.set(fd, null);
 142
 143     } catch (ArrayIndexOutOfBoundsException aobx){
 144       env.throwException("java.io.IOException", "file not open");
 145     } catch (IOException iox) {
 146       env.throwException("java.io.IOException", iox.getMessage());
 147     }
 148   }
 149
 150   // that's a JPF specific thing - we backrack into
 151   // a state where the file was still open, and hence don't want to
 152   // change the FileDescriptor identify
 153   void reopen (MJIEnv env, int objref) throws IOException {
 154     int fd = env.getIntField(objref, "fd");
 155     long off = env.getLongField(objref,"off");
 156
 157     if (content.get(fd) == null){
 158       int mode = env.getIntField(objref, "mode");
 159       int fnRef = env.getReferenceField(objref, "fileName");
 160       String fname = env.getStringObject(fnRef);
 161
 162       if (mode == FD_READ){
 163         FileInputStream fis = new FileInputStream(fname);
 164         FileChannel fc = fis.getChannel(); // just to allocate one
 165         fc.position(off);
 166         content.set(fd, fis);
 167
 168       } else if (mode == FD_WRITE){
 169         FileOutputStream fos = new FileOutputStream(fname);
 170         FileChannel fc = fos.getChannel(); // just to allocate one
 171         fc.position(off);
 172         content.set(fd, fos);
 173
 174       } else {
 175         env.throwException("java.io.IOException", "illegal mode: " + mode);
 176       }
 177     }
 178   }
 179
 180   @MJI
 181   public void write__I__ (MJIEnv env, int objref, int b){
 182     int fd = env.getIntField(objref, "fd");
 183     long off = env.getLongField(objref,"off");
 184
 185     try {
 186       // this is terrible overhead
 187       Object fs = content.get(fd);
 188       if (fs != null){
 189         if (fs instanceof FileOutputStream){
 190           FileOutputStream fos = (FileOutputStream)fs;
 191           FileChannel fc = fos.getChannel();
 192           fc.position(off);
 193           fos.write(b);
 194           env.setLongField(objref, "off", fc.position());
 195
 196         } else {
 197           env.throwException("java.io.IOException", "write attempt on file opened for read access");
 198         }
 199
 200       } else {
 201         if (env.getIntField(objref, "state") == FD_OPENED){ // backtracked
 202           reopen(env,objref);
 203           write__I__(env,objref,b); // try again
 204         } else {
 205           env.throwException("java.io.IOException", "write attempt on closed file");
 206         }
 207       }
 208     } catch (ArrayIndexOutOfBoundsException aobx){
 209       env.throwException("java.io.IOException", "file not open");
 210     } catch (IOException iox) {
 211       env.throwException("java.io.IOException", iox.getMessage());
 212     }
 213   }
 214
 215   @MJI
 216   public void write___3BII__ (MJIEnv env, int objref,
 217                                      int bref, int offset, int len){
 218     int fd = env.getIntField(objref, "fd");
 219     long off = env.getLongField(objref,"off");
 220
 221     try {
 222       // this is terrible overhead
 223       Object fs = content.get(fd);
 224       if (fs != null){
 225         if (fs instanceof FileOutputStream){
 226           FileOutputStream fos = (FileOutputStream)fs;
 227           FileChannel fc = fos.getChannel();
 228           fc.position(off);
 229
 230           byte[] buf = new byte[len]; // <2do> make this a permanent buffer
 231           for (int i=0, j=offset; i<len; i++, j++){
 232             buf[i] = env.getByteArrayElement(bref, j);
 233           }
 234           fos.write(buf);
 235
 236           env.setLongField(objref, "off", fc.position());
 237
 238         } else {
 239           env.throwException("java.io.IOException", "write attempt on file opened for read access");
 240         }
 241
 242       } else {
 243         if (env.getIntField(objref, "state") == FD_OPENED){ // backtracked
 244           reopen(env,objref);
 245           write___3BII__(env,objref,bref,offset,len); // try again
 246         } else {
 247           env.throwException("java.io.IOException", "write attempt on closed file");
 248         }
 249       }
 250     } catch (ArrayIndexOutOfBoundsException aobx){
 251       env.throwException("java.io.IOException", "file not open");
 252     } catch (IOException iox) {
 253       env.throwException("java.io.IOException", iox.getMessage());
 254     }
 255   }
 256
 257   @MJI
 258   public int read____I (MJIEnv env, int objref) {
 259     int fd = env.getIntField(objref, "fd");
 260     long off = env.getLongField(objref,"off");
 261
 262     try {
 263       // this is terrible overhead
 264       Object fs = content.get(fd);
 265       if (fs != null){
 266         if (fs instanceof FileInputStream){
 267           FileInputStream fis = (FileInputStream)fs;
 268           FileChannel fc = fis.getChannel();
 269           fc.position(off);
 270           int r = fis.read();
 271           env.setLongField(objref, "off", fc.position());
 272           return r;
 273
 274         } else {
 275           env.throwException("java.io.IOException", "read attempt on file opened for write access");
 276           return -1;
 277         }
 278
 279       } else {
 280         if (env.getIntField(objref, "state") == FD_OPENED){ // backtracked
 281           reopen(env,objref);
 282           return read____I(env,objref); // try again
 283         } else {
 284           env.throwException("java.io.IOException", "read attempt on closed file");
 285           return -1;
 286         }
 287       }
 288     } catch (ArrayIndexOutOfBoundsException aobx){
 289       env.throwException("java.io.IOException", "file not open");
 290       return -1;
 291     } catch (IOException iox) {
 292       env.throwException("java.io.IOException", iox.getMessage());
 293       return -1;
 294     }
 295   }
 296
 297   @MJI
 298   public int read___3BII__I (MJIEnv env, int objref, int bufref, int offset, int len) {
 299     int fd = env.getIntField(objref, "fd");
 300     long off = env.getLongField(objref,"off");
 301
 302     try {
 303       Object fs = content.get(fd);
 304       if (fs != null){
 305         if (fs instanceof FileInputStream){
 306           FileInputStream fis = (FileInputStream)fs;
 307           FileChannel fc = fis.getChannel();
 308           fc.position(off);
 309
 310           byte[] buf = new byte[len]; // <2do> make this a permanent buffer
 311
 312           int r = fis.read(buf);
 313           for (int i=0, j=offset; i<len; i++, j++) {
 314             env.setByteArrayElement(bufref, j, buf[i]);
 315           }
 316           env.setLongField(objref, "off", fc.position());
 317           return r;
 318
 319         } else {
 320           env.throwException("java.io.IOException", "read attempt on file opened for write access");
 321           return -1;
 322         }
 323
 324       } else {
 325         if (env.getIntField(objref, "state") == FD_OPENED){ // backtracked
 326           reopen(env,objref);
 327           return read___3BII__I(env,objref,bufref,offset,len); // try again
 328         } else {
 329           env.throwException("java.io.IOException", "read attempt on closed file");
 330           return -1;
 331         }
 332       }
 333     } catch (ArrayIndexOutOfBoundsException aobx){
 334       env.throwException("java.io.IOException", "file not open");
 335       return -1;
 336     } catch (IOException iox) {
 337       env.throwException("java.io.IOException", iox.getMessage());
 338       return -1;
 339     }
 340   }
 341
 342   @MJI
 343   public long skip__J__J (MJIEnv env, int objref, long nBytes) {
 344     int fd = env.getIntField(objref, "fd");
 345     long off = env.getLongField(objref,"off");
 346
 347     try {
 348       Object fs = content.get(fd);
 349       if (fs != null){
 350         if (fs instanceof FileInputStream){
 351           FileInputStream fis = (FileInputStream)fs;
 352           FileChannel fc = fis.getChannel();
 353           fc.position(off);
 354
 355           long r = fis.skip(nBytes);
 356           env.setLongField(objref, "off", fc.position());
 357           return r;
 358
 359         } else {
 360           env.throwException("java.io.IOException", "skip attempt on file opened for write access");
 361           return -1;
 362         }
 363
 364       } else {
 365         env.throwException("java.io.IOException", "skip attempt on closed file");
 366         return -1;
 367       }
 368
 369     } catch (ArrayIndexOutOfBoundsException aobx){
 370       env.throwException("java.io.IOException", "file not open");
 371       return -1;
 372     } catch (IOException iox) {
 373       env.throwException("java.io.IOException", iox.getMessage());
 374       return -1;
 375     }
 376   }
 377
 378   @MJI
 379   public void sync____ (MJIEnv env, int objref){
 380     int fd = env.getIntField(objref, "fd");
 381
 382     try {
 383       Object fs = content.get(fd);
 384       if (fs != null){
 385         if (fs instanceof FileOutputStream){
 386           ((FileOutputStream)fs).flush();
 387         } else {
 388           // nothing
 389         }
 390
 391       } else {
 392         env.throwException("java.io.IOException", "sync attempt on closed file");
 393       }
 394
 395     } catch (ArrayIndexOutOfBoundsException aobx){
 396       env.throwException("java.io.IOException", "file not open");
 397     } catch (IOException iox) {
 398       env.throwException("java.io.IOException", iox.getMessage());
 399     }
 400   }
 401
 402   @MJI
 403   public int available____I (MJIEnv env, int objref) {
 404     int fd = env.getIntField(objref, "fd");
 405     long off = env.getLongField(objref,"off");
 406
 407     try {
 408       Object fs = content.get(fd);
 409       if (fs != null){
 410         if (fs instanceof FileInputStream){
 411           FileInputStream fis = (FileInputStream)fs;
 412           FileChannel fc = fis.getChannel();
 413           fc.position(off);
 414           return fis.available();
 415
 416         } else {
 417           env.throwException("java.io.IOException", "available() on file opened for write access");
 418           return -1;
 419         }
 420
 421       } else {
 422         env.throwException("java.io.IOException", "available() on closed file");
 423         return -1;
 424       }
 425
 426     } catch (ArrayIndexOutOfBoundsException aobx){
 427       env.throwException("java.io.IOException", "file not open");
 428       return -1;
 429     } catch (IOException iox) {
 430       env.throwException("java.io.IOException", iox.getMessage());
 431       return -1;
 432     }
 433
 434   }
 435 }