src/tests/gov/nasa/jpf/test/basic/JPF_gov_nasa_jpf_test_basic_MJITest.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.test.basic;
  19
  20 import gov.nasa.jpf.annotation.MJI;
  21 import gov.nasa.jpf.vm.DirectCallStackFrame;
  22 import gov.nasa.jpf.vm.MJIEnv;
  23 import gov.nasa.jpf.vm.MethodInfo;
  24 import gov.nasa.jpf.vm.NativePeer;
  25 import gov.nasa.jpf.vm.ThreadInfo;
  26 import gov.nasa.jpf.vm.UncaughtException;
  27
  28 /**
  29  * native peer class for unit testing MJI
  30  */
  31 public class JPF_gov_nasa_jpf_test_basic_MJITest extends NativePeer {
  32
  33   // intercept <clinit>
  34   @MJI
  35   public void $clinit (MJIEnv env, int rcls) {
  36     System.out.println("# entering native <clinit>");
  37     env.setStaticIntField(rcls, "sdata", 42);
  38   }
  39
  40   // intercept MJITest(int i) ctor
  41   @MJI
  42   public void $init__I__V (MJIEnv env, int robj, int i) {
  43     // NOTE : if we directly intercept the ctor, then we also have
  44     // to take care of calling the proper superclass ctors
  45     // better approach is to refactor this into a separate native method
  46     // (say init0(..))
  47     System.out.println("# entering native <init>(I)");
  48     env.setIntField(robj, "idata", i);
  49   }
  50
  51   @MJI
  52   public int nativeCreate2DimIntArray__II___3_3I (MJIEnv env, int robj, int size1,
  53                                               int size2) {
  54     System.out.println("# entering nativeCreate2DimIntArray()");
  55     int ar = env.newObjectArray("[I", size1);
  56
  57     for (int i = 0; i < size1; i++) {
  58       int ea = env.newIntArray(size2);
  59
  60       if (i == 1) {
  61         env.setIntArrayElement(ea, 1, 42);
  62       }
  63
  64       env.setReferenceArrayElement(ar, i, ea);
  65     }
  66
  67     return ar;
  68   }
  69
  70   // check if the non-mangled name lookup works
  71   @MJI
  72   public int nativeCreateIntArray (MJIEnv env, int robj, int size) {
  73     System.out.println("# entering nativeCreateIntArray()");
  74
  75     int ar = env.newIntArray(size);
  76
  77     env.setIntArrayElement(ar, 1, 1);
  78
  79     return ar;
  80   }
  81
  82   @MJI
  83   public int nativeCreateStringArray (MJIEnv env, int robj, int size) {
  84     System.out.println("# entering nativeCreateStringArray()");
  85
  86     int ar = env.newObjectArray("Ljava/lang/String;", size);
  87     env.setReferenceArrayElement(ar, 1, env.newString("one"));
  88
  89     return ar;
  90   }
  91
  92   @MJI
  93   public void nativeException____V (MJIEnv env, int robj) {
  94     System.out.println("# entering nativeException()");
  95     env.throwException("java.lang.UnsupportedOperationException", "caught me");
  96   }
  97
  98   @SuppressWarnings("null")
  99   @MJI
 100   public int nativeCrash (MJIEnv env, int robj) {
 101     System.out.println("# entering nativeCrash()");
 102     String s = null;
 103     return s.length();
 104   }
 105
 106   @MJI
 107   public int nativeInstanceMethod (MJIEnv env, int robj, double d,
 108                                           char c, boolean b, int i) {
 109     System.out.println("# entering nativeInstanceMethod() d=" + d +
 110             ", c=" + c + ", b=" + b + ", i=" + i);
 111
 112     if ((d == 2.0) && (c == '?') && b) {
 113       return i + 2;
 114     }
 115
 116     return 0;
 117   }
 118
 119   @MJI
 120   public long nativeStaticMethod__JLjava_lang_String_2__J (MJIEnv env, int rcls, long l,
 121                                                                   int stringRef) {
 122     System.out.println("# entering nativeStaticMethod()");
 123
 124     String s = env.getStringObject(stringRef);
 125
 126     if ("Blah".equals(s)) {
 127       return l + 2;
 128     }
 129
 130     return 0;
 131   }
 132
 133
 134   /*
 135    * nativeRoundtripLoop shows how to
 136    *
 137    *  (1) round trip into JPF executed code from within native methods
 138    *
 139    *  (2) loop inside of native methods that do round trips (using the
 140    *      DirectCallStackFrame's local slots)
 141    *
 142    * the call chain is:
 143    *
 144    *   JPF: testRoundtripLoop
 145    *     VM: nativeRoundTripLoop  x 3
 146    *       JPF: roundtrip
 147    *         VM: nativeInnerRoundtrip
 148    */
 149
 150   @MJI
 151   public int nativeInnerRoundtrip__I__I (MJIEnv env, int robj, int a){
 152     System.out.println("# entering nativeInnerRoundtrip()");
 153
 154     return a+2;
 155   }
 156
 157   @MJI
 158   public int nativeRoundtripLoop__I__I (MJIEnv env, int robj, int a) {
 159     System.out.println("# entering nativeRoundtripLoop(): " + a);
 160
 161     MethodInfo mi = env.getClassInfo(robj).getMethod("roundtrip(I)I",false);
 162     ThreadInfo ti = env.getThreadInfo();
 163     DirectCallStackFrame frame = ti.getReturnedDirectCall();
 164
 165     if (frame == null){ // first time
 166       frame = mi.createDirectCallStackFrame(ti, 1);
 167       frame.setLocalVariable( 0, 0);
 168
 169       int argOffset = frame.setReferenceArgument(0, robj, null);
 170       frame.setArgument( argOffset, a+1, null);
 171
 172       ti.pushFrame(frame);
 173
 174       return 42; // whatever, we come back
 175
 176     } else { // direct call returned
 177
 178       // this method can't be executed unless the class is already initialized,
 179       // i.e. we don't have to check for overlayed clinit calls and the frame
 180       // has to be the one we pushed
 181       assert frame.getCallee() == mi;
 182
 183       // this shows how to get information back from the JPF roundtrip into
 184       // the native method
 185       int r = frame.getResult(); // the return value of the direct call above
 186       int i = frame.getLocalVariable(0);
 187
 188       if (i < 3) { // repeat the round trip
 189         // we have to reset so that the PC is re-initialized
 190         frame.reset();
 191         frame.setLocalVariable(0, i + 1);
 192
 193         int argOffset = frame.setReferenceArgument( 0, robj, null);
 194         frame.setArgument( argOffset, r+1, null);
 195
 196         ti.pushFrame(frame);
 197         return 42;
 198
 199       } else { // done, return the final value
 200         return r;
 201       }
 202     }
 203   }
 204
 205   /**
 206    * this shows how to synchronously JPF-enter a method from native peer or
 207    * listener code
 208    */
 209   @MJI
 210   public int nativeHiddenRoundtrip__I__I (MJIEnv env, int robj, int a){
 211     ThreadInfo ti = env.getThreadInfo();
 212
 213     System.out.println("# entering nativeHiddenRoundtrip: " + a);
 214     MethodInfo mi = env.getClassInfo(robj).getMethod("atomicStuff(I)I",false);
 215
 216     DirectCallStackFrame frame = mi.createDirectCallStackFrame(ti, 0);
 217
 218     int argOffset = frame.setReferenceArgument( 0, robj, null);
 219     frame.setArgument( argOffset, a, null);
 220     frame.setFireWall();
 221
 222     try {
 223       ti.executeMethodHidden(frame);
 224       //ti.advancePC();
 225
 226     } catch (UncaughtException ux) {  // frame's method is firewalled
 227       System.out.println("# hidden method execution failed, leaving nativeHiddenRoundtrip: " + ux);
 228       ti.clearPendingException();
 229       ti.popFrame(); // this is still the DirectCallStackFrame, and we want to continue execution
 230       return -1;
 231     }
 232
 233     // get the return value from the (already popped) frame
 234     int res = frame.getResult();
 235
 236     System.out.println("# exit nativeHiddenRoundtrip: " + res);
 237     return res;
 238   }
 239
 240 }