src/peers/gov/nasa/jpf/vm/JPF_java_lang_System.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.Config;
  21 import gov.nasa.jpf.annotation.MJI;
  22 import java.io.FileInputStream;
  23 import java.io.IOException;
  24 import java.util.Map;
  25 import java.util.Properties;
  26
  27 /**
  28  * MJI NativePeer class for java.lang.System library abstraction
  29  */
  30 public class JPF_java_lang_System extends NativePeer {
  31
  32   @MJI
  33   public void arraycopy__Ljava_lang_Object_2ILjava_lang_Object_2II__V (MJIEnv env, int clsObjRef,
  34                                                                               int srcArrayRef, int srcIdx,
  35                                                                               int dstArrayRef, int dstIdx,
  36                                                                               int length) {
  37     if ((srcArrayRef == MJIEnv.NULL) || (dstArrayRef == MJIEnv.NULL)) {
  38       env.throwException("java.lang.NullPointerException");
  39       return;
  40     }
  41
  42     ElementInfo eiSrc = env.getElementInfo(srcArrayRef);
  43     ElementInfo eiDst = env.getModifiableElementInfo(dstArrayRef);
  44
  45     try {
  46       eiDst.copyElements( env.getThreadInfo(), eiSrc ,srcIdx, dstIdx, length);
  47     } catch (IndexOutOfBoundsException iobx){
  48       env.throwException("java.lang.IndexOutOfBoundsException", iobx.getMessage());
  49     } catch (ArrayStoreException asx){
  50       env.throwException("java.lang.ArrayStoreException", asx.getMessage());
  51     }
  52   }
  53
  54   @MJI
  55   public int getenv__Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int clsObjRef,
  56                                                                          int keyRef){
  57     String k = env.getStringObject(keyRef);
  58     String v = System.getenv(k);
  59
  60     if (v == null){
  61       return MJIEnv.NULL;
  62     } else {
  63       return env.newString(v);
  64     }
  65   }
  66
  67
  68   int createPrintStream (MJIEnv env, int clsObjRef){
  69     ThreadInfo ti = env.getThreadInfo();
  70     Instruction insn = ti.getPC();
  71     StackFrame frame = ti.getTopFrame();
  72     ClassInfo ci = ClassLoaderInfo.getSystemResolvedClassInfo("gov.nasa.jpf.ConsoleOutputStream");
  73
  74     if (ci.initializeClass(ti)) {
  75       env.repeatInvocation();
  76       return MJIEnv.NULL;
  77     }
  78
  79     return env.newObject(ci);
  80   }
  81
  82   @MJI
  83   public int createSystemOut____Ljava_io_PrintStream_2 (MJIEnv env, int clsObjRef){
  84     return createPrintStream(env,clsObjRef);
  85   }
  86
  87   @MJI
  88   public int createSystemErr____Ljava_io_PrintStream_2 (MJIEnv env, int clsObjRef){
  89     return createPrintStream(env,clsObjRef);
  90   }
  91
  92   int getProperties (MJIEnv env, Properties p){
  93     int n = p.size() * 2;
  94     int aref = env.newObjectArray("Ljava/lang/String;", n);
  95     int i=0;
  96
  97     for (Map.Entry<Object,Object> e : p.entrySet() ){
  98       env.setReferenceArrayElement(aref,i++,
  99                                    env.newString(e.getKey().toString()));
 100       env.setReferenceArrayElement(aref,i++,
 101                                    env.newString(e.getValue().toString()));
 102     }
 103
 104     return aref;
 105   }
 106
 107   int getSysPropsFromHost (MJIEnv env){
 108     return getProperties(env, System.getProperties());
 109   }
 110
 111   int getSysPropsFromFile (MJIEnv env){
 112     Config conf = env.getConfig();
 113
 114     String cf = conf.getString("vm.sysprop.file", "system.properties");
 115     if (cf != null){
 116       try {
 117         Properties p = new Properties();
 118         FileInputStream fis = new FileInputStream(cf);
 119         p.load(fis);
 120
 121         return getProperties(env, p);
 122
 123       } catch (IOException iox){
 124         return MJIEnv.NULL;
 125       }
 126     }
 127     //.. not yet
 128     return MJIEnv.NULL;
 129   }
 130
 131   static String JAVA_CLASS_PATH = "java.class.path";
 132
 133   @MJI
 134   public String getSUTJavaClassPath(VM vm) {
 135     ClassInfo system = ClassLoaderInfo.getSystemResolvedClassInfo("java.lang.System");
 136
 137     ThreadInfo ti = vm.getCurrentThread();
 138     Heap heap = vm.getHeap();
 139     ElementInfo eiClassPath = heap.newString(JAVA_CLASS_PATH, ti);
 140
 141     MethodInfo miGetProperty = system.getMethod("getProperty(Ljava/lang/String;)Ljava/lang/String;", true);
 142     DirectCallStackFrame frame = miGetProperty.createDirectCallStackFrame(ti, 0);
 143     frame.setReferenceArgument( 0, eiClassPath.getObjectRef(), null);
 144     frame.setFireWall(); // we don't want exceptions to escape into the SUT
 145
 146
 147     try {
 148       ti.executeMethodHidden(frame);
 149
 150     } catch (UncaughtException e) {
 151        ti.clearPendingException();
 152        StackFrame caller = ti.popAndGetModifiableTopFrame();
 153        caller.advancePC();
 154        return null;
 155     }
 156
 157     int ref = frame.peek();
 158     ElementInfo metaResult = heap.get(ref);
 159     String result = metaResult.asString();
 160
 161     return result;
 162   }
 163
 164   int getSelectedSysPropsFromHost (MJIEnv env){
 165     Config conf = env.getConfig();
 166     String keys[] = conf.getStringArray("vm.sysprop.keys");
 167
 168     if (keys == null){
 169       String[] defKeys = {
 170         "path.separator",
 171         "line.separator",
 172         "file.separator",
 173         "user.name",
 174         "user.dir",
 175         "user.timezone",
 176         "user.country",
 177         "java.home",
 178         "java.version",
 179         "java.io.tmpdir",
 180         JAVA_CLASS_PATH
 181         //... and probably some more
 182         // <2do> what about -Dkey=value commandline options
 183       };
 184       keys = defKeys;
 185     }
 186
 187     int aref = env.newObjectArray("Ljava/lang/String;", keys.length * 2);
 188     int i=0;
 189
 190     for (String s : keys) {
 191       String v;
 192
 193       int idx = s.indexOf('/');
 194       if (idx >0){ // this one is an explicit key/value pair from vm.system.properties
 195         v = s.substring(idx+1);
 196         s = s.substring(0,idx);
 197
 198       } else {
 199         // the special beasts first (if they weren't overridden with vm.system.properties)
 200         if (s == JAVA_CLASS_PATH) {
 201           // maybe we should just use vm.classpath
 202           // NOTE: the curent classloader at the point it has to be a system classloader.
 203           ClassPath cp = ClassLoaderInfo.getCurrentClassLoader().getClassPath();
 204           // <2do> should be consistent with path.separator (this is host VM notation)
 205           v = cp.toString();
 206
 207         } else { // we bluntly grab it from the host VM properties
 208           v = System.getProperty(s);
 209         }
 210       }
 211
 212       if (v != null){
 213         env.setReferenceArrayElement(aref,i++, env.newString(s));
 214         env.setReferenceArrayElement(aref,i++, env.newString(v));
 215       }
 216     }
 217
 218     return aref;
 219   }
 220
 221   /**
 222    * policy of how to initialize system properties of the system under test
 223    */
 224   static enum SystemPropertyPolicy {
 225     SELECTED,  // copy host values for keys specified in
 226     FILE,
 227     HOST
 228   };
 229
 230   @MJI
 231   public int getKeyValuePairs_____3Ljava_lang_String_2 (MJIEnv env, int clsObjRef){
 232     Config conf = env.getConfig();
 233     SystemPropertyPolicy sysPropSrc = conf.getEnum( "vm.sysprop.source", SystemPropertyPolicy.values(), SystemPropertyPolicy.SELECTED);
 234
 235     if (sysPropSrc == SystemPropertyPolicy.FILE){
 236       return getSysPropsFromFile(env);
 237     } else if (sysPropSrc == SystemPropertyPolicy.HOST){
 238       return getSysPropsFromHost(env);
 239     } else if (sysPropSrc == SystemPropertyPolicy.SELECTED){
 240       return getSelectedSysPropsFromHost(env);
 241     }
 242
 243     return 0;
 244   }
 245
 246   // <2do> - this break every app which uses time delta thresholds
 247   // (sort of "if ((t2 - t1) > d)"). Ok, we can't deal with
 248   // real time, but we could at least give some SystemState dependent
 249   // increment
 250   @MJI
 251   public long currentTimeMillis____J (MJIEnv env, int clsObjRef) {
 252     return env.currentTimeMillis();
 253   }
 254
 255   // <2do> - likewise. Java 1.5's way to measure relative time
 256   @MJI
 257   public long nanoTime____J (MJIEnv env, int clsObjRef) {
 258     return env.nanoTime();
 259   }
 260
 261   // this works on the assumption that we sure break the transition, and
 262   // then the search determines that it is an end state (all terminated)
 263   @MJI
 264   public void exit__I__V (MJIEnv env, int clsObjRef, int ret) {
 265     ThreadInfo ti = env.getThreadInfo();
 266     env.getVM().terminateProcess(ti);
 267   }
 268
 269   @MJI
 270   public void gc____V (MJIEnv env, int clsObjRef) {
 271     env.getSystemState().activateGC();
 272   }
 273
 274   @MJI
 275   public int identityHashCode__Ljava_lang_Object_2__I (MJIEnv env, int clsObjRef, int objref) {
 276     return (objref ^ 0xABCD);
 277   }
 278
 279 }