2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.test.basic;
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;
29 * native peer class for unit testing MJI
31 public class JPF_gov_nasa_jpf_test_basic_MJITest extends NativePeer {
35 public void $clinit (MJIEnv env, int rcls) {
36 System.out.println("# entering native <clinit>");
37 env.setStaticIntField(rcls, "sdata", 42);
40 // intercept MJITest(int i) ctor
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
47 System.out.println("# entering native <init>(I)");
48 env.setIntField(robj, "idata", i);
52 public int nativeCreate2DimIntArray__II___3_3I (MJIEnv env, int robj, int size1,
54 System.out.println("# entering nativeCreate2DimIntArray()");
55 int ar = env.newObjectArray("[I", size1);
57 for (int i = 0; i < size1; i++) {
58 int ea = env.newIntArray(size2);
61 env.setIntArrayElement(ea, 1, 42);
64 env.setReferenceArrayElement(ar, i, ea);
70 // check if the non-mangled name lookup works
72 public int nativeCreateIntArray (MJIEnv env, int robj, int size) {
73 System.out.println("# entering nativeCreateIntArray()");
75 int ar = env.newIntArray(size);
77 env.setIntArrayElement(ar, 1, 1);
83 public int nativeCreateStringArray (MJIEnv env, int robj, int size) {
84 System.out.println("# entering nativeCreateStringArray()");
86 int ar = env.newObjectArray("Ljava/lang/String;", size);
87 env.setReferenceArrayElement(ar, 1, env.newString("one"));
93 public void nativeException____V (MJIEnv env, int robj) {
94 System.out.println("# entering nativeException()");
95 env.throwException("java.lang.UnsupportedOperationException", "caught me");
98 @SuppressWarnings("null")
100 public int nativeCrash (MJIEnv env, int robj) {
101 System.out.println("# entering nativeCrash()");
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);
112 if ((d == 2.0) && (c == '?') && b) {
120 public long nativeStaticMethod__JLjava_lang_String_2__J (MJIEnv env, int rcls, long l,
122 System.out.println("# entering nativeStaticMethod()");
124 String s = env.getStringObject(stringRef);
126 if ("Blah".equals(s)) {
135 * nativeRoundtripLoop shows how to
137 * (1) round trip into JPF executed code from within native methods
139 * (2) loop inside of native methods that do round trips (using the
140 * DirectCallStackFrame's local slots)
144 * JPF: testRoundtripLoop
145 * VM: nativeRoundTripLoop x 3
147 * VM: nativeInnerRoundtrip
151 public int nativeInnerRoundtrip__I__I (MJIEnv env, int robj, int a){
152 System.out.println("# entering nativeInnerRoundtrip()");
158 public int nativeRoundtripLoop__I__I (MJIEnv env, int robj, int a) {
159 System.out.println("# entering nativeRoundtripLoop(): " + a);
161 MethodInfo mi = env.getClassInfo(robj).getMethod("roundtrip(I)I",false);
162 ThreadInfo ti = env.getThreadInfo();
163 DirectCallStackFrame frame = ti.getReturnedDirectCall();
165 if (frame == null){ // first time
166 frame = mi.createDirectCallStackFrame(ti, 1);
167 frame.setLocalVariable( 0, 0);
169 int argOffset = frame.setReferenceArgument(0, robj, null);
170 frame.setArgument( argOffset, a+1, null);
174 return 42; // whatever, we come back
176 } else { // direct call returned
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;
183 // this shows how to get information back from the JPF roundtrip into
185 int r = frame.getResult(); // the return value of the direct call above
186 int i = frame.getLocalVariable(0);
188 if (i < 3) { // repeat the round trip
189 // we have to reset so that the PC is re-initialized
191 frame.setLocalVariable(0, i + 1);
193 int argOffset = frame.setReferenceArgument( 0, robj, null);
194 frame.setArgument( argOffset, r+1, null);
199 } else { // done, return the final value
206 * this shows how to synchronously JPF-enter a method from native peer or
210 public int nativeHiddenRoundtrip__I__I (MJIEnv env, int robj, int a){
211 ThreadInfo ti = env.getThreadInfo();
213 System.out.println("# entering nativeHiddenRoundtrip: " + a);
214 MethodInfo mi = env.getClassInfo(robj).getMethod("atomicStuff(I)I",false);
216 DirectCallStackFrame frame = mi.createDirectCallStackFrame(ti, 0);
218 int argOffset = frame.setReferenceArgument( 0, robj, null);
219 frame.setArgument( argOffset, a, null);
223 ti.executeMethodHidden(frame);
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
233 // get the return value from the (already popped) frame
234 int res = frame.getResult();
236 System.out.println("# exit nativeHiddenRoundtrip: " + res);