Mercurial > hg > Members > kono > jpf-core

comparison src/tests/gov/nasa/jpf/test/basic/JPF_gov_nasa_jpf_test_basic_MJITest.java @ 0:61d41facf527

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial v8 import (history reset)
author Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date Fri, 23 Jan 2015 10:14:01 -0800
parents
children
comparison
equal deleted inserted replaced
-1:000000000000 0:61d41facf527
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 }