src/main/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 package gov.nasa.jpf.util.test;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.Error;
  22 import gov.nasa.jpf.JPF;
  23 import gov.nasa.jpf.JPFShell;
  24 import gov.nasa.jpf.Property;
  25 import gov.nasa.jpf.annotation.FilterField;
  26 import gov.nasa.jpf.tool.RunTest;
  27 import gov.nasa.jpf.util.DevNullPrintStream;
  28 import gov.nasa.jpf.util.TypeRef;
  29 import gov.nasa.jpf.util.JPFSiteUtils;
  30 import gov.nasa.jpf.util.Reflection;
  31 import gov.nasa.jpf.vm.ExceptionInfo;
  32 import gov.nasa.jpf.vm.NoUncaughtExceptionsProperty;
  33 import gov.nasa.jpf.vm.NotDeadlockedProperty;
  34
  35 import java.io.PrintStream;
  36 import java.io.PrintWriter;
  37 import java.lang.annotation.Annotation;
  38 import java.lang.reflect.InvocationTargetException;
  39 import java.lang.reflect.Method;
  40 import java.lang.reflect.Modifier;
  41 import java.util.ArrayList;
  42 import java.util.List;
  43
  44 /**
  45  * base class for JPF unit tests. TestJPF mostly includes JPF invocations
  46  * that check for occurrence or absence of certain execution results
  47  *
  48  * This class can be used in two modes:
  49  *
  50  * <ol>
  51  * <li> wrapping a number of related tests for different SuTs into one class
  52  * (suite) that calls the various JPF runners with complete argument lists
  53  * (as in JPF.main(String[]args)) </li>
  54  *
  55  * <li> derive a class from TestJPF that uses the "..This" methods, which in
  56  * turn use reflection to automatically append the test class and method to the
  57  * JPF.main argument list (based on the calling class / method names). Note that
  58  * you have to obey naming conventions for this to work:
  59  *
  60  * <li> the SuT class has to be the same as the test class without "Test", e.g.
  61  * "CastTest" -> "Cast" </li>
  62  *
  63  * <li> the SuT method has to have the same name as the @Test method that
  64  * invokes JPF, e.g. "CastTest {.. @Test void testArrayCast() ..}" ->
  65  * "Cast {.. void testArrayCast()..} </li>
  66  * </ol>
  67  */
  68 public abstract class TestJPF implements JPFShell  {
  69   static PrintStream out = System.out;
  70
  71   public static final String UNNAMED_PACKAGE = "";
  72   public static final String SAME_PACKAGE = null;
  73
  74   //--- those are only used outside of JPF execution
  75   @FilterField protected static boolean globalRunDirectly, globalShowConfig;
  76
  77   @FilterField protected static boolean runDirectly; // don't run test methods through JPF, invoke it directly
  78   @FilterField protected static boolean stopOnFailure; // stop as soon as we encounter a failed test or error
  79   @FilterField protected static boolean showConfig; // for debugging purposes
  80   @FilterField protected static boolean showConfigSources; // for debugging purposes
  81   @FilterField protected static boolean hideSummary;
  82
  83   @FilterField protected static boolean quiet; // don't show test output
  84
  85   @FilterField protected String sutClassName;
  86
  87   static class GlobalArg {
  88     String key;
  89     String val;
  90
  91     GlobalArg (String k, String v){
  92       key = k;
  93       val = v;
  94     }
  95   }
  96
  97   // it seems wrong to pull globalArgs here instead of setting it from
  98   // RunTest, but RunTest has to make sure TestJPF is loaded through the
  99   // JPFClassLoader, i.e. cannot directly reference this class.
 100
 101   @FilterField static ArrayList<GlobalArg> globalArgs;
 102
 103   protected static ArrayList<GlobalArg> getGlobalArgs() {
 104     // NOTE - this is only set if we execute tests from build.xml
 105     Config globalConf = RunTest.getConfig();
 106     if (globalConf != null){
 107       ArrayList<GlobalArg> list = new ArrayList<GlobalArg>();
 108
 109       //--- the "test.<key>" specs
 110       String[] testKeys = globalConf.getKeysStartingWith("test.");
 111       if (testKeys.length > 0){
 112         for (String key : testKeys){
 113           String val = globalConf.getString(key);
 114           // <2do> this is a hack to avoid the problem of not being able to store
 115           // empty/nil/null values in the global config (they are removed during global config init)
 116           if (val.equals("REMOVE")){
 117             val = null;
 118           }
 119
 120           key = key.substring(5);
 121
 122           list.add(new GlobalArg(key,val));
 123         }
 124       }
 125
 126       return list;
 127     }
 128
 129     return null;
 130   }
 131
 132   static {
 133     if (!isJPFRun()){
 134       globalArgs = getGlobalArgs();
 135     }
 136   }
 137
 138   //--- internal methods
 139
 140   public static void fail (String msg, String[] args, String cause){
 141     StringBuilder sb = new StringBuilder();
 142
 143     sb.append(msg);
 144     if (args != null){
 145       for (String s : args){
 146         sb.append(s);
 147         sb.append(' ');
 148       }
 149     }
 150
 151     if (cause != null){
 152       sb.append(':');
 153       sb.append(cause);
 154     }
 155
 156     fail(sb.toString());
 157   }
 158
 159   public static void fail (){
 160     throw new AssertionError();
 161   }
 162
 163   public static void fail (String msg){
 164     throw new AssertionError(msg);
 165   }
 166
 167   public void report (String[] args) {
 168     if (!quiet){
 169       out.print("  running jpf with args:");
 170
 171       for (int i = 0; i < args.length; i++) {
 172         out.print(' ');
 173         out.print(args[i]);
 174       }
 175
 176       out.println();
 177     }
 178   }
 179
 180   /**
 181    * compute the SuT class name for a given JUnit test class: remove
 182    * optionally ending "..Test", and replace package (if specified)
 183    *
 184    * @param testClassName the JUnit test class
 185    * @param sutPackage optional SuT package name (without ending '.', null
 186    * os SAME_PACKAGE means same package, "" or UNNAMED_PACKAGE means unnamed package)
 187    * @return main class name of system under test
 188    */
 189   protected static String getSutClassName (String testClassName, String sutPackage){
 190
 191     String sutClassName = testClassName;
 192
 193     int i = sutClassName.lastIndexOf('.');
 194     if (i >= 0){  // testclass has a package
 195
 196       if (sutPackage == null){   // use same package
 197         // nothing to do
 198       } else if (sutPackage.length() > 0) { // explicit sut package
 199         sutClassName = sutPackage + sutClassName.substring(i);
 200
 201       } else { // unnamed sut package
 202         sutClassName = sutClassName.substring(i+1);
 203       }
 204
 205     } else { // test class has no package
 206       if (sutPackage == null || sutPackage.length() == 0){   // use same package
 207         // nothing to do
 208       } else { // explicit sut package
 209         sutClassName = sutPackage + '.' + sutClassName;
 210       }
 211     }
 212
 213     if (sutClassName.endsWith("JPF")) {
 214       sutClassName = sutClassName.substring(0, sutClassName.length() - 3);
 215     }
 216
 217     return sutClassName;
 218   }
 219
 220   // we can't set the sutClassName only from main() called methods (like
 221   // runTestsOfThisClass()) since main() doesn't get called if this is executed
 222   // by Ant (via <junit> task)
 223   // the default ctor is always executed
 224   public TestJPF () {
 225     sutClassName = getSutClassName(getClass().getName(), SAME_PACKAGE);
 226   }
 227
 228
 229
 230   //------ the API to be used by subclasses
 231
 232   /**
 233    * to be used from default ctor of derived class if the SuT is in a different
 234    * package
 235    * @param sutClassName the qualified SuT class name to be checked by JPF
 236    */
 237   protected TestJPF (String sutClassName){
 238     this.sutClassName = sutClassName;
 239   }
 240
 241   public static boolean isJPFRun () {
 242     return false;
 243   }
 244
 245   public static boolean isJUnitRun() {
 246     // intercepted by native peer if this runs under JPF
 247     Throwable t = new Throwable();
 248     t.fillInStackTrace();
 249
 250     for (StackTraceElement se : t.getStackTrace()){
 251       if (se.getClassName().startsWith("org.junit.")){
 252         return true;
 253       }
 254     }
 255
 256     return false;
 257   }
 258
 259   public static boolean isRunTestRun() {
 260     // intercepted by native peer if this runs under JPF
 261     Throwable t = new Throwable();
 262     t.fillInStackTrace();
 263
 264     for (StackTraceElement se : t.getStackTrace()){
 265       if (se.getClassName().equals("gov.nasa.jpf.tool.RunTest")){
 266         return true;
 267       }
 268     }
 269
 270     return false;
 271   }
 272
 273
 274   protected static void getOptions (String[] args){
 275     runDirectly = globalRunDirectly;
 276     showConfig = globalShowConfig;
 277
 278     // hideSummary and stopOnFailure only make sense as global options anyways
 279
 280     if (args != null){
 281       for (int i=0; i<args.length; i++){
 282         String a = args[i];
 283         if (a != null){
 284           if (a.length() > 0){
 285             if (a.charAt(0) == '-'){
 286               a = a.substring(1);
 287
 288               if (a.equals("d")){
 289                 runDirectly = true;
 290               } else if (a.equals("s") || a.equals("show")){
 291                 showConfig = true;
 292               } else if (a.equals("l") || a.equals("log")){
 293                 showConfigSources = true;
 294               } else if (a.equals("q") || a.equals("quiet")){
 295                 quiet = true;
 296               } else if (a.equals("x")){
 297                 stopOnFailure = true;
 298               } else if (a.equals("h")){
 299                 hideSummary = true;
 300               }
 301               args[i] = null;  // set it consumed
 302
 303             } else {
 304               break; // done, this is a test method
 305             }
 306           }
 307         }
 308       }
 309     }
 310   }
 311
 312   protected static boolean hasExplicitTestMethods(String[] args){
 313     for (String a : args){
 314       if (a != null){
 315         return true;
 316       }
 317     }
 318
 319     return false;
 320   }
 321
 322   protected static List<Method> getMatchingMethods(Class<? extends TestJPF> testCls,
 323           int setModifiers, int unsetModifiers, String[] annotationNames){
 324     List<Method> list = new ArrayList<Method>();
 325
 326     for (Method m : testCls.getMethods()){
 327       if (isMatchingMethod(m, setModifiers, unsetModifiers, annotationNames)){
 328         list.add(m);
 329       }
 330     }
 331
 332     return list;
 333   }
 334
 335   protected static boolean isMatchingMethod(Method m, int setModifiers, int unsetModifiers, String[] annotationNames) {
 336     int mod = m.getModifiers();
 337     if (((mod & setModifiers) != 0) && ((mod & unsetModifiers) == 0)) {
 338       if (m.getParameterTypes().length == 0) {
 339         if (annotationNames != null){
 340           Annotation[] annotations = m.getAnnotations();
 341           for (int i = 0; i < annotations.length; i++) {
 342             String annotType = annotations[i].annotationType().getName();
 343             for (int j = 0; j < annotationNames.length; j++) {
 344               if (annotType.equals(annotationNames[j])) {
 345                 return true;
 346               }
 347             }
 348           }
 349         } else {
 350           return true;
 351         }
 352       }
 353     }
 354
 355     return false;
 356   }
 357
 358   protected static List<Method> getContextMethods(Class<? extends TestJPF> testCls,
 359                                                   int setModifiers, int unsetModifiers, String annotation){
 360     String[] annotations = {annotation};
 361
 362     List<Method> list = new ArrayList<Method>();
 363     for (Method m : testCls.getMethods()){
 364       if (isMatchingMethod(m, setModifiers, unsetModifiers, annotations)){
 365         list.add(m);
 366       }
 367     }
 368     return list;
 369   }
 370
 371   protected static List<Method> getBeforeMethods(Class<? extends TestJPF> testCls){
 372     return getContextMethods(testCls, Modifier.PUBLIC, Modifier.STATIC, "org.junit.Before");
 373   }
 374
 375   protected static List<Method> getAfterMethods(Class<? extends TestJPF> testCls){
 376     return getContextMethods(testCls, Modifier.PUBLIC, Modifier.STATIC, "org.junit.After");
 377   }
 378
 379   protected static List<Method> getBeforeClassMethods(Class<? extends TestJPF> testCls){
 380     return getContextMethods(testCls, Modifier.PUBLIC | Modifier.STATIC, 0, "org.junit.BeforeClass");
 381   }
 382
 383   protected static List<Method> getAfterClassMethods(Class<? extends TestJPF> testCls){
 384     return getContextMethods(testCls, Modifier.PUBLIC | Modifier.STATIC, 0, "org.junit.AfterClass");
 385   }
 386
 387   protected static boolean haveTestMethodSpecs( String[] args){
 388     if (args != null && args.length > 0){
 389       for (int i=0; i<args.length; i++){
 390         if (args[i] != null){
 391           return true;
 392         }
 393       }
 394     }
 395
 396     return false;
 397   }
 398
 399   protected static List<Method> getTestMethods(Class<? extends TestJPF> testCls, String[] args){
 400     String[] testAnnotations = {"org.junit.Test", "org.testng.annotations.Test"};
 401
 402     if (haveTestMethodSpecs( args)){ // test methods specified as arguments
 403       List<Method> list = new ArrayList<Method>();
 404
 405       for (String test : args){
 406         if (test != null){
 407
 408           try {
 409             Method m = testCls.getMethod(test);
 410
 411             if (isMatchingMethod(m, Modifier.PUBLIC, Modifier.STATIC, null /*testAnnotations*/ )){
 412               list.add(m);
 413             } else {
 414               throw new RuntimeException("test method must be @Test annotated public instance method without arguments: " + test);
 415             }
 416
 417           } catch (NoSuchMethodException x) {
 418             throw new RuntimeException("method: " + test
 419                     + "() not in test class: " + testCls.getName(), x);
 420           }
 421         }
 422       }
 423
 424       return list;
 425
 426     } else { // no explicit test method specification, get all matches
 427       return getMatchingMethods(testCls, Modifier.PUBLIC, Modifier.STATIC, testAnnotations);
 428     }
 429   }
 430
 431
 432   protected static void reportTestStart(String mthName){
 433     if (!quiet){
 434       System.out.println();
 435       System.out.print("......................................... testing ");
 436       System.out.print(mthName);
 437       System.out.println("()");
 438     }
 439   }
 440
 441   protected static void reportTestInitialization(String mthName){
 442     if (!quiet){
 443       System.out.print(".... running test initialization: ");
 444       System.out.print(mthName);
 445       System.out.println("()");
 446     }
 447   }
 448
 449   protected static void reportTestCleanup(String mthName){
 450     if (!quiet){
 451       System.out.print(".... running test cleanup: ");
 452       System.out.print(mthName);
 453       System.out.println("()");
 454     }
 455   }
 456
 457   protected static void reportTestFinished(String msg){
 458     if (!quiet){
 459       System.out.print("......................................... ");
 460       System.out.println(msg);
 461     }
 462   }
 463
 464   protected static void reportResults(String clsName, int nTests, int nFailures, int nErrors, List<String> results){
 465     System.out.println();
 466     System.out.print("......................................... execution of testsuite: " + clsName);
 467     if (nFailures > 0 || nErrors > 0){
 468       System.out.println(" FAILED");
 469     } else if (nTests > 0) {
 470       System.out.println(" SUCCEEDED");
 471     } else {
 472       System.out.println(" OBSOLETE");
 473     }
 474
 475     if (!quiet){
 476       if (results != null) {
 477         int i = 0;
 478         for (String result : results) {
 479           System.out.print(".... [" + ++i + "] ");
 480           System.out.println(result);
 481         }
 482       }
 483     }
 484
 485     System.out.print(".........................................");
 486     System.out.println(" tests: " + nTests + ", failures: " + nFailures + ", errors: " + nErrors);
 487   }
 488
 489
 490   static void invoke (Method m, Object testObject) throws IllegalAccessException, InvocationTargetException  {
 491     PrintStream sysOut = null;
 492
 493     try {
 494       if (quiet){
 495         sysOut = System.out;
 496         System.setOut( new DevNullPrintStream());
 497       }
 498
 499       m.invoke( testObject);
 500
 501     } finally {
 502       if (quiet){
 503         System.setOut( sysOut);
 504       }
 505     }
 506   }
 507
 508   /**
 509    * this is the main test loop if this TestJPF instance is executed directly
 510    * or called from RunTest. It is *not* called if this is executed from JUnit
 511    */
 512   public static void runTests (Class<? extends TestJPF> testCls, String... args){
 513     int nTests = 0;
 514     int nFailures = 0;
 515     int nErrors = 0;
 516     String testMethodName = null;
 517     List<String> results = null;
 518
 519     getOptions(args);
 520     globalRunDirectly = runDirectly;
 521     globalShowConfig = showConfig;
 522     boolean globalStopOnFailure = stopOnFailure;
 523
 524     try {
 525       List<Method> testMethods = getTestMethods(testCls, args);
 526       results = new ArrayList<String>(testMethods.size());
 527
 528       // check if we have JUnit style housekeeping methods (initialization and
 529       // cleanup should use the same mechanisms as JUnit)
 530
 531       List<Method> beforeClassMethods = getBeforeClassMethods(testCls);
 532       List<Method> afterClassMethods = getAfterClassMethods(testCls);
 533
 534       List<Method> beforeMethods = getBeforeMethods(testCls);
 535       List<Method> afterMethods = getAfterMethods(testCls);
 536
 537       for (Method initMethod : beforeClassMethods) {
 538         reportTestInitialization(initMethod.getName());
 539         initMethod.invoke(null);
 540       }
 541
 542       for (Method testMethod : testMethods) {
 543         testMethodName = testMethod.getName();
 544         String result = testMethodName;
 545         try {
 546           Object testObject = testCls.newInstance();
 547
 548           nTests++;
 549           reportTestStart( testMethodName);
 550
 551           // run per test initialization methods
 552           for (Method initMethod : beforeMethods){
 553             reportTestInitialization( initMethod.getName());
 554             invoke( initMethod, testObject);
 555           }
 556
 557           // now run the test method itself
 558           invoke( testMethod, testObject);
 559           result += ": Ok";
 560
 561           // run per test initialization methods
 562           for (Method cleanupMethod : afterMethods){
 563             reportTestCleanup( cleanupMethod.getName());
 564             invoke( cleanupMethod, testObject);
 565           }
 566
 567         } catch (InvocationTargetException x) {
 568           Throwable cause = x.getCause();
 569           cause.printStackTrace();
 570           if (cause instanceof AssertionError) {
 571             nFailures++;
 572             reportTestFinished("test method failed with: " + cause.getMessage());
 573             result += ": Failed";
 574           } else {
 575             nErrors++;
 576             reportTestFinished("unexpected error while executing test method: " + cause.getMessage());
 577             result += ": Error";
 578           }
 579
 580           if (globalStopOnFailure){
 581             break;
 582           }
 583         }
 584
 585         results.add(result);
 586         reportTestFinished(result);
 587       }
 588
 589       for (Method cleanupMethod : afterClassMethods) {
 590         reportTestCleanup( cleanupMethod.getName());
 591         cleanupMethod.invoke(null);
 592       }
 593
 594
 595     //--- those exceptions are unexpected and represent unrecoverable test harness errors
 596     } catch (InvocationTargetException x) {
 597       Throwable cause = x.getCause();
 598       cause.printStackTrace();
 599       nErrors++;
 600       reportTestFinished("TEST ERROR: @BeforeClass,@AfterClass method failed: " + x.getMessage());
 601
 602     } catch (InstantiationException x) {
 603       nErrors++;
 604       reportTestFinished("TEST ERROR: cannot instantiate test class: " + x.getMessage());
 605     } catch (IllegalAccessException x) { // can't happen if getTestMethods() worked
 606       nErrors++;
 607       reportTestFinished("TEST ERROR: default constructor or test method not public: " + testMethodName);
 608     } catch (IllegalArgumentException x) {  // can't happen if getTestMethods() worked
 609       nErrors++;
 610       reportTestFinished("TEST ERROR: illegal argument for test method: " + testMethodName);
 611     } catch (RuntimeException rx) {
 612       nErrors++;
 613       reportTestFinished("TEST ERROR: " + rx.toString());
 614     }
 615
 616     if (!hideSummary){
 617       reportResults(testCls.getName(), nTests, nFailures, nErrors, results);
 618     }
 619
 620     if (nErrors > 0 || nFailures > 0){
 621       if (isRunTestRun()){
 622         // we need to reportTestFinished this test has failed
 623         throw new RunTest.Failed();
 624       }
 625     }
 626   }
 627
 628   static String getProperty(String key){
 629     // intercepted by peer
 630     return null;
 631   }
 632
 633   /**
 634    * this is the JPF entry method in case there is no main() in the test class
 635    *
 636    * <2do> we should support test method arguments here
 637    */
 638   static void runTestMethod(String args[]) throws Throwable {
 639     String testClsName = getProperty("target");
 640     String testMthName = getProperty("target.test_method");
 641
 642     Class<?> testCls = Class.forName(testClsName);
 643     Object target = testCls.newInstance();
 644
 645     Method method = testCls.getMethod(testMthName);
 646
 647     try {
 648       method.invoke(target);
 649     } catch (InvocationTargetException e) {
 650       throw e.getCause();
 651     }
 652   }
 653
 654   /**
 655    * NOTE: this needs to be called from the concrete test class, typically from
 656    * its main() method, otherwise we don't know the name of the class we have
 657    * to pass to JPF
 658    */
 659   protected static void runTestsOfThisClass (String[] testMethods){
 660     // needs to be at the same stack level, so we can't delegate
 661     Class<? extends TestJPF> testClass = Reflection.getCallerClass(TestJPF.class);
 662     runTests(testClass, testMethods);
 663   }
 664
 665   /**
 666    * needs to be broken up into two methods for cases that do additional
 667    * JPF initialization (jpf-inspector)
 668    *
 669    * this is called from the various verifyX() methods (i.e. host VM) to
 670    * start JPF, it is never executed under JPF
 671    */
 672   protected JPF createAndRunJPF (StackTraceElement testMethod, String[] args) {
 673     JPF jpf = createJPF( testMethod, args);
 674     if (jpf != null){
 675       jpf.run();
 676     }
 677     return jpf;
 678   }
 679
 680   /**
 681    * this is never executed under JPF
 682    */
 683   protected JPF createJPF (StackTraceElement testMethod, String[] args) {
 684     JPF jpf = null;
 685
 686     Config conf = new Config(args);
 687
 688     // --- add global args (if we run under RunTest)
 689     if (globalArgs != null) {
 690       for (GlobalArg ga : globalArgs) {
 691         String key = ga.key;
 692         String val = ga.val;
 693         if (val != null){
 694           conf.put(key, val);
 695         } else {
 696           conf.remove(key);
 697         }
 698       }
 699     }
 700
 701     setTestTargetKeys(conf, testMethod);
 702
 703     // --- initialize the classpath from <projectId>.test_classpath
 704     String projectId = JPFSiteUtils.getCurrentProjectId();
 705     if (projectId != null) {
 706       String testCp = conf.getString(projectId + ".test_classpath");
 707       if (testCp != null) {
 708         conf.append("classpath", testCp, ",");
 709       }
 710     }
 711
 712     // --- if we have any specific test property overrides, do so
 713     conf.promotePropertyCategory("test.");
 714
 715     getOptions(args);
 716
 717     if (showConfig || showConfigSources) {
 718       PrintWriter pw = new PrintWriter(System.out, true);
 719       if (showConfigSources) {
 720         conf.printSources(pw);
 721       }
 722
 723       if (showConfig) {
 724         conf.print(pw);
 725       }
 726       pw.flush();
 727     }
 728
 729     jpf = new JPF(conf);
 730
 731     return jpf;
 732   }
 733
 734   protected void setTestTargetKeys(Config conf, StackTraceElement testMethod) {
 735     conf.put("target.entry", "runTestMethod([Ljava/lang/String;)V");
 736     conf.put("target", testMethod.getClassName());
 737     conf.put("target.test_method", testMethod.getMethodName());
 738   }
 739
 740   //--- the JPFShell interface
 741   @Override
 742   public void start(String[] testMethods){
 743     Class<? extends TestJPF> testClass = getClass(); // this is an instance method
 744     runTests(testClass, testMethods);
 745   }
 746
 747   protected StackTraceElement getCaller(){
 748     StackTraceElement[] st = (new Throwable()).getStackTrace();
 749     return st[2];
 750   }
 751
 752   protected StackTraceElement setTestMethod (String clsName, String mthName){
 753     return new StackTraceElement( clsName, mthName, null, -1);
 754   }
 755
 756   protected StackTraceElement setTestMethod (String mthName){
 757     return new StackTraceElement( getClass().getName(), mthName, null, -1);
 758   }
 759
 760
 761   //--- the JPF run test methods
 762
 763   /**
 764    * run JPF expecting a AssertionError in the SuT
 765    * @param args JPF main() arguments
 766    */
 767   protected JPF assertionError (StackTraceElement testMethod, String... args){
 768     return unhandledException( testMethod, "java.lang.AssertionError", null, args );
 769   }
 770   protected JPF assertionError (String... args) {
 771     return unhandledException( getCaller(), "java.lang.AssertionError", null, args );
 772   }
 773
 774   protected JPF assertionErrorDetails (StackTraceElement testMethod, String details, String... args) {
 775     return unhandledException( testMethod, "java.lang.AssertionError", details, args );
 776   }
 777   protected JPF assertionErrorDetails (String details, String... args) {
 778     return unhandledException( getCaller(), "java.lang.AssertionError", details, args );
 779   }
 780   protected boolean verifyAssertionErrorDetails (String details, String... args){
 781     if (runDirectly) {
 782       return true;
 783     } else {
 784       unhandledException( getCaller(), "java.lang.AssertionError", details, args);
 785       return false;
 786     }
 787   }
 788   protected boolean verifyAssertionError (String... args){
 789     if (runDirectly) {
 790       return true;
 791     } else {
 792       unhandledException( getCaller(), "java.lang.AssertionError", null, args);
 793       return false;
 794     }
 795   }
 796
 797   /**
 798    * run JPF expecting no SuT property violations
 799    */
 800   protected JPF noPropertyViolation (StackTraceElement testMethod, String... args) {
 801     JPF jpf = null;
 802
 803     report(args);
 804
 805     try {
 806       jpf = createAndRunJPF( testMethod, args);
 807     } catch (Throwable t) {
 808       // we get as much as one little hickup and we declare it failed
 809       t.printStackTrace();
 810       fail("JPF internal exception executing: ", args, t.toString());
 811       return jpf;
 812     }
 813
 814     List<Error> errors = jpf.getSearchErrors();
 815     if ((errors != null) && (errors.size() > 0)) {
 816       fail("JPF found unexpected errors: " + (errors.get(0)).getDescription());
 817     }
 818
 819     return jpf;
 820   }
 821
 822   protected JPF noPropertyViolation (String... args) {
 823     return noPropertyViolation( getCaller(), args);
 824   }
 825
 826   protected boolean verifyNoPropertyViolation (String...args){
 827     if (runDirectly) {
 828       return true;
 829     } else {
 830       noPropertyViolation( getCaller(), args);
 831       return false;
 832     }
 833   }
 834
 835   /**
 836    * NOTE: this uses the exception class name because it might be an
 837    * exception type that is only known to JPF (i.e. not in the native classpath)
 838    *
 839    * @param xClassName name of the exception base type that is expected
 840    * @param details detail message of the expected exception
 841    * @param args JPF arguments
 842    */
 843   protected JPF unhandledException (StackTraceElement testMethod, String xClassName, String details, String... args) {
 844     JPF jpf = null;
 845
 846     report(args);
 847
 848     try {
 849       jpf = createAndRunJPF(testMethod, args);
 850     } catch (Throwable t) {
 851       t.printStackTrace();
 852       fail("JPF internal exception executing: ", args, t.toString());
 853       return jpf;
 854     }
 855
 856     Error error = jpf.getLastError();
 857     if (error != null){
 858       Property errorProperty = error.getProperty();
 859       if (errorProperty instanceof NoUncaughtExceptionsProperty){
 860         ExceptionInfo xi = ((NoUncaughtExceptionsProperty)errorProperty).getUncaughtExceptionInfo();
 861         String xn = xi.getExceptionClassname();
 862         if (!xn.equals(xClassName)) {
 863           fail("JPF caught wrong exception: " + xn + ", expected: " + xClassName);
 864         }
 865
 866         if (details != null) {
 867           String gotDetails = xi.getDetails();
 868           if (gotDetails == null) {
 869             fail("JPF caught the right exception but no details, expected: " + details);
 870           } else {
 871             if (!gotDetails.endsWith(details)) {
 872               fail("JPF caught the right exception but the details were wrong: " + gotDetails + ", expected: " + details);
 873             }
 874           }
 875         }
 876       } else { // error not a NoUncaughtExceptionsProperty
 877         fail("JPF failed to catch exception executing: ", args, ("expected " + xClassName));
 878       }
 879     } else { // no error
 880       fail("JPF failed to catch exception executing: ", args, ("expected " + xClassName));
 881     }
 882
 883     return jpf;
 884   }
 885
 886   protected JPF unhandledException (String xClassName, String details, String... args) {
 887     return unhandledException( getCaller(), xClassName, details, args);
 888   }
 889
 890
 891   protected boolean verifyUnhandledExceptionDetails (String xClassName, String details, String... args){
 892     if (runDirectly) {
 893       return true;
 894     } else {
 895       unhandledException( getCaller(), xClassName, details, args);
 896       return false;
 897     }
 898   }
 899   protected boolean verifyUnhandledException (String xClassName, String... args){
 900     if (runDirectly) {
 901       return true;
 902     } else {
 903       unhandledException( getCaller(), xClassName, null, args);
 904       return false;
 905     }
 906   }
 907
 908
 909   /**
 910    * run JPF expecting it to throw an exception
 911    * NOTE - xClassName needs to be the concrete exception, not a super class
 912    * @param args JPF main() arguments
 913    */
 914   protected JPF jpfException (StackTraceElement testMethod, Class<? extends Throwable> xCls, String... args) {
 915     JPF jpf = null;
 916     Throwable exception = null;
 917
 918     report(args);
 919
 920     try {
 921       jpf = createAndRunJPF( testMethod, args);
 922     } catch (JPF.ExitException xx) {
 923       exception = xx.getCause();
 924     } catch (Throwable x) {
 925       exception = x;
 926     }
 927
 928     if (exception != null){
 929       if (!xCls.isAssignableFrom(exception.getClass())){
 930         fail("JPF produced wrong exception: " + exception + ", expected: " + xCls.getName());
 931       }
 932     } else {
 933       fail("JPF failed to produce exception, expected: " + xCls.getName());
 934     }
 935
 936     return jpf;
 937   }
 938
 939   protected JPF jpfException (Class<? extends Throwable> xCls, String... args) {
 940     return jpfException( getCaller(), xCls, args);
 941   }
 942
 943   protected boolean verifyJPFException (TypeRef xClsSpec, String... args){
 944     if (runDirectly) {
 945       return true;
 946
 947     } else {
 948       try {
 949         Class<? extends Throwable> xCls = xClsSpec.asNativeSubclass(Throwable.class);
 950
 951         jpfException( getCaller(), xCls, args);
 952
 953       } catch (ClassCastException ccx){
 954         fail("not a property type: " + xClsSpec);
 955       } catch (ClassNotFoundException cnfx){
 956         fail("property class not found: " + xClsSpec);
 957       }
 958       return false;
 959     }
 960   }
 961
 962
 963
 964   /**
 965    * run JPF expecting a property violation of the SuT
 966    * @param args JPF main() arguments
 967    */
 968   protected JPF propertyViolation (StackTraceElement testMethod, Class<? extends Property> propertyCls, String... args ){
 969     JPF jpf = null;
 970
 971     report(args);
 972
 973     try {
 974       jpf = createAndRunJPF( testMethod, args);
 975     } catch (Throwable t) {
 976       t.printStackTrace();
 977       fail("JPF internal exception executing: ", args, t.toString());
 978     }
 979
 980     List<Error> errors = jpf.getSearchErrors();
 981     if (errors != null) {
 982       for (Error e : errors) {
 983         if (propertyCls == e.getProperty().getClass()) {
 984           return jpf; // success, we got the sucker
 985         }
 986       }
 987     }
 988
 989     fail("JPF failed to detect error: " + propertyCls.getName());
 990     return jpf;
 991   }
 992
 993   protected JPF propertyViolation (Class<? extends Property> propertyCls, String... args ){
 994     return propertyViolation( getCaller(), propertyCls, args);
 995   }
 996
 997   protected boolean verifyPropertyViolation (TypeRef propertyClsSpec, String... args){
 998     if (runDirectly) {
 999       return true;
1000
1001     } else {
1002       try {
1003         Class<? extends Property> propertyCls = propertyClsSpec.asNativeSubclass(Property.class);
1004         propertyViolation( getCaller(), propertyCls, args);
1005
1006       } catch (ClassCastException ccx){
1007         fail("not a property type: " + propertyClsSpec);
1008       } catch (ClassNotFoundException cnfx){
1009         fail("property class not found: " + propertyClsSpec);
1010       }
1011       return false;
1012     }
1013   }
1014
1015
1016   /**
1017    * run JPF expecting a deadlock in the SuT
1018    * @param args JPF main() arguments
1019    */
1020   protected JPF deadlock (String... args) {
1021     return propertyViolation( getCaller(), NotDeadlockedProperty.class, args );
1022   }
1023
1024   protected boolean verifyDeadlock (String... args){
1025     if (runDirectly) {
1026       return true;
1027     } else {
1028       propertyViolation( getCaller(), NotDeadlockedProperty.class, args);
1029       return false;
1030     }
1031   }
1032
1033   // these are the org.junit.Assert APIs, but we don't want org.junit to be
1034   // required to run tests
1035
1036   public static void assertEquals(String msg, Object expected, Object actual){
1037     if (expected == null && actual == null) {
1038       return;
1039     }
1040
1041     if (expected != null && expected.equals(actual)) {
1042       return;
1043     }
1044
1045     fail(msg);
1046   }
1047
1048   public static void assertEquals(Object expected, Object actual){
1049     assertEquals("", expected, actual);
1050   }
1051
1052   public static void assertEquals(String msg, int expected, int actual){
1053     if (expected != actual) {
1054       fail(msg);
1055     }
1056   }
1057
1058   public static void assertEquals(int expected, int actual){
1059     assertEquals("expected != actual : " + expected + " != " + actual, expected, actual);
1060   }
1061
1062   public static void assertEquals(String msg, long expected, long actual){
1063     if (expected != actual) {
1064       fail(msg);
1065     }
1066   }
1067
1068   public static void assertEquals(long expected, long actual){
1069       assertEquals("expected != actual : " + expected + " != " + actual,
1070                    expected, actual);
1071   }
1072
1073   public static void assertEquals(double expected, double actual){
1074     if (expected != actual){
1075       fail("expected != actual : " + expected + " != " + actual);
1076     }
1077   }
1078
1079   public static void assertEquals(String msg, double expected, double actual){
1080     if (expected != actual){
1081       fail(msg);
1082     }
1083   }
1084
1085   public static void assertEquals(float expected, float actual){
1086     if (expected != actual){
1087       fail("expected != actual : " + expected + " != " + actual);
1088     }
1089   }
1090
1091   public static void assertEquals(String msg, float expected, float actual){
1092     if (expected != actual){
1093       fail(msg);
1094     }
1095   }
1096
1097   public static void assertEquals(String msg, double expected, double actual, double delta){
1098     if (Math.abs(expected - actual) > delta) {
1099       fail(msg);
1100     }
1101   }
1102
1103   public static void assertEquals(double expected, double actual, double delta){
1104     assertEquals("Math.abs(expected - actual) > delta : " + "Math.abs(" + expected + " - " + actual + ") > " + delta,
1105                  expected, actual, delta);
1106   }
1107
1108   public static void assertEquals(String msg, float expected, float actual, float delta){
1109     if (Math.abs(expected - actual) > delta) {
1110       fail(msg);
1111     }
1112   }
1113
1114   public static void assertEquals(float expected, float actual, float delta){
1115       assertEquals("Math.abs(expected - actual) > delta : " + "Math.abs(" + expected + " - " + actual + ") > " + delta,
1116                    expected, actual, delta);
1117   }
1118
1119   public static void assertArrayEquals(byte[] expected, byte[] actual){
1120     if (((expected == null) != (actual == null)) ||
1121         (expected.length != actual.length)){
1122       fail("array sizes different");
1123     }
1124
1125     for (int i=0; i<expected.length; i++){
1126       if (expected[i] != actual[i]){
1127         fail("array element" + i + " different, expected " + expected[i] + ", actual " + actual[i]);
1128       }
1129     }
1130   }
1131
1132   public static void assertNotNull(String msg, Object o) {
1133     if (o == null) {
1134       fail(msg);
1135     }
1136   }
1137
1138   public static void assertNotNull(Object o){
1139     assertNotNull("o == null", o);
1140   }
1141
1142   public static void assertNull(String msg, Object o){
1143     if (o != null) {
1144       fail(msg);
1145     }
1146   }
1147
1148   public static void assertNull(Object o){
1149     assertNull("o != null", o);
1150   }
1151
1152   public static void assertSame(String msg, Object expected, Object actual){
1153     if (expected != actual) {
1154       fail(msg);
1155     }
1156   }
1157
1158   public static void assertSame(Object expected, Object actual){
1159     assertSame("expected != actual : " + expected + " != " + actual, expected, actual);
1160   }
1161
1162   public static void assertFalse (String msg, boolean cond){
1163     if (cond) {
1164       fail(msg);
1165     }
1166   }
1167
1168   public static void assertFalse (boolean cond){
1169     assertFalse("", cond);
1170   }
1171
1172   public static void assertTrue (String msg, boolean cond){
1173     if (!cond) {
1174       fail(msg);
1175     }
1176   }
1177
1178   public static void assertTrue (boolean cond){
1179     assertTrue("", cond);
1180   }
1181 }