src/main/gov/nasa/jpf/util/test/JPF_gov_nasa_jpf_util_test_TestJPF.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.util.test;
  20
  21 import gov.nasa.jpf.annotation.MJI;
  22 import gov.nasa.jpf.vm.ClassInfo;
  23 import gov.nasa.jpf.vm.DirectCallStackFrame;
  24 import gov.nasa.jpf.vm.MJIEnv;
  25 import gov.nasa.jpf.vm.MethodInfo;
  26 import gov.nasa.jpf.vm.NativePeer;
  27 import gov.nasa.jpf.vm.StackFrame;
  28 import gov.nasa.jpf.vm.ThreadInfo;
  29
  30 import java.util.ArrayList;
  31
  32 /**
  33  * native peer for our test class root
  34  */
  35 public class JPF_gov_nasa_jpf_util_test_TestJPF extends NativePeer {
  36
  37   ClassInfo testClass;
  38   MethodInfo testClassCtor;
  39
  40   MethodInfo[] testMethods = null;
  41   int index = 0;
  42   int testObjRef = MJIEnv.NULL;
  43
  44   boolean done;
  45
  46   private static void pushDirectCallFrame(MJIEnv env, MethodInfo mi, int objRef) {
  47     ThreadInfo ti = env.getThreadInfo();
  48
  49     DirectCallStackFrame frame = mi.createDirectCallStackFrame(ti, 0);
  50     frame.setReferenceArgument( 0, objRef, null);
  51     ti.pushFrame(frame);
  52   }
  53
  54   private boolean initializeTestMethods(MJIEnv env, String[] selectedTests) {
  55     if (selectedTests != null && selectedTests.length > 0) {
  56       testMethods = new MethodInfo[selectedTests.length];
  57       int i = 0;
  58       for (String test : selectedTests) {
  59         MethodInfo mi = testClass.getMethod(test + "()V", false);
  60         if (mi != null && mi.isPublic() && !mi.isStatic()) {
  61           testMethods[i++] = mi;
  62         } else {
  63           env.throwException("java.lang.RuntimeException",
  64                   "no such test method: public void " + test + "()");
  65           return false;
  66         }
  67       }
  68     } else { // collect all public void test..() methods
  69       ArrayList<MethodInfo> list = new ArrayList<MethodInfo>();
  70       for (MethodInfo mi : testClass) {
  71         if (mi.getName().startsWith("test") && mi.isPublic() && !mi.isStatic() &&
  72                 mi.getSignature().equals("()V")) {
  73           list.add(mi);
  74         }
  75       }
  76       testMethods = list.toArray(new MethodInfo[list.size()]);
  77     }
  78
  79     return true;
  80   }
  81
  82   //--- our exported native methods
  83
  84   public JPF_gov_nasa_jpf_util_test_TestJPF () {
  85     done = false;
  86     index = 0;
  87     testObjRef = MJIEnv.NULL;
  88     testMethods = null;
  89     testClass = null;
  90     testClassCtor = null;
  91   }
  92
  93   @MJI
  94   public void $init____V (MJIEnv env, int objRef){
  95     // nothing
  96   }
  97
  98   @MJI
  99   public void runTestsOfThisClass___3Ljava_lang_String_2__V (MJIEnv env, int clsObjRef,
 100                                                                     int selectedTestsRef) {
 101     ThreadInfo ti = env.getThreadInfo();
 102
 103     if (!done) {
 104       if (testMethods == null) {
 105         StackFrame frame = env.getCallerStackFrame(); // the runTestsOfThisClass() caller
 106
 107         testClass = frame.getClassInfo();
 108         testClassCtor = testClass.getMethod("<init>()V", true);
 109
 110         String[] selectedTests = env.getStringArrayObject(selectedTestsRef);
 111         if (initializeTestMethods(env, selectedTests)) {
 112           env.repeatInvocation();
 113         }
 114
 115       } else { // this is re-executed
 116         if (testObjRef == MJIEnv.NULL) { // create a new test object
 117           testObjRef = env.newObject(testClass);
 118
 119           if (testClassCtor != null) {
 120             pushDirectCallFrame(env, testClassCtor, testObjRef);
 121             env.repeatInvocation();
 122           }
 123
 124         } else { // enter the next test
 125           if (testMethods != null && (index < testMethods.length)) {
 126             MethodInfo miTest = testMethods[index++];
 127             pushDirectCallFrame(env, miTest, testObjRef);
 128
 129             if (index < testMethods.length) {
 130               testObjRef = MJIEnv.NULL;
 131             } else {
 132               done = true;
 133             }
 134
 135             env.repeatInvocation();
 136           }
 137         }
 138       }
 139     }
 140   }
 141
 142   @MJI
 143   public int createAndRunJPF__Ljava_lang_StackTraceElement_2_3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2 (MJIEnv env, int clsObjRef, int a1, int a2){
 144     // don't get recursive
 145     return MJIEnv.NULL;
 146   }
 147
 148   @MJI
 149   public int getProperty__Ljava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int clsObjRef, int keyRef){
 150     String key = env.getStringObject(keyRef);
 151     String val = env.getConfig().getString(key);
 152
 153     if (val != null){
 154       return env.newString(val);
 155     } else {
 156       return MJIEnv.NULL;
 157     }
 158   }
 159
 160   /**
 161    * if any of our methods are executed, we know that we already run under JPF
 162    */
 163   @MJI
 164   public boolean isJPFRun____Z (MJIEnv env, int clsObjRef){
 165     return true;
 166   }
 167
 168   @MJI
 169   public boolean isJUnitRun____Z (MJIEnv env, int clsObjRef){
 170     return false;
 171   }
 172
 173   @MJI
 174   public boolean isRunTestRun____Z (MJIEnv env, int clsObjRef){
 175     return false;
 176   }
 177
 178
 179   // we need to override these so that the actual test code gets executed
 180   // if we fail to intercept, the bytecode will actually start JPF
 181   @MJI
 182   public int noPropertyViolation___3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2 (MJIEnv env, int clsObjRef, int jpfArgsRef){
 183     return MJIEnv.NULL;
 184   }
 185
 186   @MJI
 187   public boolean verifyNoPropertyViolation___3Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef, int jpfArgsRef){
 188     return true;
 189   }
 190
 191   @MJI
 192   public boolean verifyAssertionErrorDetails__Ljava_lang_String_2_3Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef,
 193                                   int detailsRef, int jpfArgsRef){
 194     return true;
 195   }
 196
 197   @MJI
 198   public boolean verifyAssertionError___3Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef, int jpfArgsRef){
 199     return true;
 200   }
 201
 202   @MJI
 203   public int unhandledException__Ljava_lang_String_2Ljava_lang_String_2_3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2 (MJIEnv env, int clsObjRef,
 204                                   int xClassNameRef, int detailsRef, int jpfArgsRef){
 205     return MJIEnv.NULL;
 206   }
 207
 208   @MJI
 209   public boolean verifyUnhandledException__Ljava_lang_String_2_3Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef,
 210                                   int xClassNameRef, int jpfArgsRef){
 211     return true;
 212   }
 213
 214   @MJI
 215   public boolean verifyUnhandledExceptionDetails__Ljava_lang_String_2Ljava_lang_String_2_3Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef,
 216                                   int xClassNameRef, int detailsRef, int jpfArgsRef){
 217     return true;
 218   }
 219
 220   @MJI
 221   public int propertyViolation__Ljava_lang_Class_2_3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2 (MJIEnv env, int clsObjRef,
 222                                   int propClsRef, int jpfArgsRef){
 223     return MJIEnv.NULL;
 224   }
 225
 226   @MJI
 227   public boolean verifyPropertyViolation__Lgov_nasa_jpf_util_TypeRef_2_3Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef,
 228                                   int propClsRef, int jpfArgsRef){
 229     return true;
 230   }
 231
 232   @MJI
 233   public int jpfException__Ljava_lang_Class_2_3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2 (MJIEnv env, int clsObjRef,
 234                                   int xClsRef, int jpfArgsRef){
 235     return MJIEnv.NULL;
 236   }
 237
 238   @MJI
 239   public boolean verifyJPFException__Lgov_nasa_jpf_util_TypeRef_2_3Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef,
 240                                   int xClsRef, int jpfArgsRef){
 241     return true;
 242   }
 243
 244   @MJI
 245   public int deadlock___3Ljava_lang_String_2__Lgov_nasa_jpf_JPF_2 (MJIEnv env, int clsObjRef, int jpfArgsRef){
 246     return MJIEnv.NULL;
 247   }
 248
 249   @MJI
 250   public boolean verifyDeadlock___3Ljava_lang_String_2__Z (MJIEnv env, int clsObjRef, int jpfArgsRef){
 251     return true;
 252   }
 253
 254
 255 }