src/peers/gov/nasa/jpf/vm/JPF_java_io_File.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.annotation.MJI;
  22 import gov.nasa.jpf.vm.ElementInfo;
  23 import gov.nasa.jpf.vm.MJIEnv;
  24 import gov.nasa.jpf.vm.NativePeer;
  25
  26 import java.io.File;
  27 import java.io.IOException;
  28 import java.net.MalformedURLException;
  29 import java.net.URI;
  30 import java.net.URL;
  31
  32 /**
  33  * intercept and forward some of the filesystem access methods. This is very
  34  * slow, if a program uses this heavily we should keep the forwarding File
  35  * object around and modify the model class accordingly
  36  */
  37 public class JPF_java_io_File extends NativePeer {
  38
  39   static File getFile(MJIEnv env, int objref) {
  40     int fnref = env.getReferenceField(objref, "filename");
  41     String fname = env.getStringObject(fnref);
  42     return new File(fname);
  43   }
  44
  45   static int createJPFFile(MJIEnv env, File file) {
  46     int newFileRef = env.newObject("java.io.File");
  47     ElementInfo fileEI = env.getModifiableElementInfo(newFileRef);
  48
  49     int fileNameRef = env.newString(file.getPath());
  50     fileEI.setReferenceField("filename", fileNameRef);
  51
  52     return newFileRef;
  53   }
  54
  55   @MJI
  56   public int getParentFile____Ljava_io_File_2(MJIEnv env, int objref) {
  57     File thisFile = getFile(env, objref);
  58     File parent = thisFile.getParentFile();
  59
  60     return createJPFFile(env, parent);
  61   }
  62
  63   @MJI
  64   public int getAbsolutePath____Ljava_lang_String_2 (MJIEnv env, int objref) {
  65     String pn = getFile(env,objref).getAbsolutePath();
  66     return env.newString(pn);
  67   }
  68
  69   @MJI
  70   public int getAbsoluteFile____Ljava_io_File_2 (MJIEnv env, int objref) {
  71     File absoluteFile = getFile(env, objref).getAbsoluteFile();
  72     return createJPFFile(env, absoluteFile);
  73   }
  74
  75   @MJI
  76   public int getCanonicalPath____Ljava_lang_String_2 (MJIEnv env, int objref) {
  77     try {
  78       String pn = getFile(env,objref).getCanonicalPath();
  79       return env.newString(pn);
  80     } catch (IOException iox) {
  81       env.throwException("java.io.IOException", iox.getMessage());
  82       return MJIEnv.NULL;
  83     }
  84   }
  85
  86   @MJI
  87   public int getCanonicalFile____Ljava_io_File_2(MJIEnv env, int objref) {
  88     try {
  89       File file = getFile(env, objref);
  90       File canonicalFile = file.getCanonicalFile();
  91       return createJPFFile(env, canonicalFile);
  92     } catch (IOException iox) {
  93       env.throwException("java.io.IOException", iox.getMessage());
  94       return MJIEnv.NULL;
  95     }
  96   }
  97
  98   // internal helper
  99   @SuppressWarnings("deprecation")
 100   @MJI
 101   public int getURLSpec____Ljava_lang_String_2 (MJIEnv env, int objref){
 102     try {
 103       File f = getFile(env,objref);
 104       URL url = f.toURL();
 105       return env.newString(url.toString());
 106     } catch (MalformedURLException mfux) {
 107       env.throwException("java.net.MalformedURLException", mfux.getMessage());
 108       return MJIEnv.NULL;
 109     }
 110   }
 111
 112   @MJI
 113   public int getURISpec____Ljava_lang_String_2 (MJIEnv env, int objref){
 114     File f = getFile(env, objref);
 115     URI uri = f.toURI();
 116     return env.newString(uri.toString());
 117   }
 118
 119   @MJI
 120   public boolean isAbsolute____Z (MJIEnv env, int objref) {
 121     return getFile(env, objref).isAbsolute();
 122   }
 123
 124   @MJI
 125   public boolean isDirectory____Z (MJIEnv env, int objref) {
 126     return getFile(env,objref).isDirectory();
 127   }
 128
 129   @MJI
 130   public boolean isFile____Z (MJIEnv env, int objref) {
 131     return getFile(env,objref).isFile();
 132   }
 133
 134   @MJI
 135   public boolean delete____Z (MJIEnv env, int objref) {
 136     return getFile(env,objref).delete();
 137   }
 138
 139   @MJI
 140   public long length____J (MJIEnv env, int objref) {
 141     return getFile(env,objref).length();
 142   }
 143
 144   @MJI
 145   public boolean canRead____Z (MJIEnv env, int objref) {
 146     return getFile(env,objref).canRead();
 147   }
 148
 149   @MJI
 150   public boolean canWrite____Z (MJIEnv env, int objref) {
 151     return getFile(env,objref).canWrite();
 152   }
 153
 154   @MJI
 155   public boolean exists____Z (MJIEnv env, int objref) {
 156     return getFile(env,objref).exists();
 157   }
 158
 159   @MJI
 160   public boolean createNewFile____Z(MJIEnv env, int objref) {
 161     File fileToCreate = getFile(env, objref);
 162     try {
 163       return fileToCreate.createNewFile();
 164
 165     } catch (IOException iox) {
 166       env.throwException("java.io.IOException", iox.getMessage());
 167       return false;
 168     }
 169   }
 170
 171   @MJI
 172   public int list_____3Ljava_lang_String_2(MJIEnv env, int objref){
 173           File f=getFile(env,objref);
 174     if (f.isDirectory()){
 175       String[] farr=f.list();
 176       return env.newStringArray(farr);
 177     } else {
 178       return MJIEnv.NULL;
 179     }
 180   }
 181
 182   @MJI
 183   public int listRoots_____3Ljava_io_File_2(MJIEnv env, int classRef) {
 184     File[] roots = File.listRoots();
 185     int rootResultRef = env.newObjectArray("java.io.File", roots.length);
 186     ElementInfo rootsEI = env.getModifiableElementInfo(rootResultRef);
 187
 188     for (int i = 0; i < roots.length; i++) {
 189       int rootFileRef = createJPFFile(env, roots[i]);
 190       rootsEI.setReferenceElement(i, rootFileRef);
 191     }
 192
 193     return rootResultRef;
 194   }
 195   // <2do> ..and lots more
 196 }