doc/devel/jpf_tests.md

   1 # Writing JPF Tests #
   2
   3 As a complex runtime system for (almost) arbitrary Java programs, it goes without saying that JPF needs a lot of regression tests. You can find these under the `src/tests` directories in (hopefully) all JPF projects. All tests follow the same scheme, which is motivated by the need to run tests in a number of different ways:
   4
   5   1. as part of the Ant-based build system, i.e. from build.xml
   6   1. as explicitly invoked JUnit tests
   7   1. by directly running JPF on the test application (i.e. without JUnit, either as a JPF `shell` or via RunTest.jar)
   8   1. by running the test application on a normal JVM
   9
  10 The rationale for this is to support various levels of inspection and debugging.
  11
  12 Each test conceptually consists of a test driver (e.g. executed under JUnit) which starts JPF from within its `@Test` annotated methods, and a class that is executed by JPF in order to check the verification goals. For convenience reasons, jpf-core provides infrastructure that enables you to implement both parts in the same class. This can be confusing at first - **the test class is used to start JPF on itself**.
  13
  14 ![Figure: Unit Testing in JPF](../graphics/new-testing.svg){align=center width=870}
  15
  16 The `main()` method of `TestJPF` derived classes always look the same and can be safely copied between tests:
  17
  18 ~~~~~~~~ {.java}
  19 public static void main(String[] testMethods){
  20   runTestsOfThisClass(testMethods);
  21 }
  22 ~~~~~~~~
  23
  24 This method serves two purposes. First, it is used to start the test outside JUnit, either on all `@Test` annotated instance methods, or just on the ones which names are provided as arguments. Second, it serves as the entry point for JPF when it executes the class. In this case, `TestJPF` takes care of invoking JPF on the test class and providing the name of the test method this was executed from.
  25
  26 Other than that, test classes just consist of (almost) normal `@Test` annotated JUnit test methods, which all share the same structure
  27
  28 ~~~~~~~~ {.java}
  29 import org.junit.Test;
  30
  31 @Test public void testX () {
  32   if (verifyNoPropertyViolation(JPF_ARGS){
  33     .. code to verify by JPF
  34   }
  35 }
  36 ~~~~~~~~
  37
  38 The trick is the call to `verifyNoPropertyViolation()`, or any of the other `verifyXX()` methods of `TestJPF`. If executed by the host VM, i.e. from JUnit, it starts JPF on the same class and the containing method, and returns `false`. This means the corresponding `if` block is **not** executed by the host VM.
  39
  40 When JPF is invoked, the argument to the main() method is set to the method name from which JPF got invoked, which causes `runTestsOfThisMethod()` to execute exactly this method again, but this time under JPF. Instead of re-executing the same `TestJPF.verifyX()` method again (and becoming infinitely recursive), we use a native peer `JPF_gov_nasa_jpf_util_test_TestJPF` which intercepts the `verifyX()` call and simply returns true, i.e. this time *only* the `if` block gets executed.
  41
  42 The rest of the host VM executed `TestJPF.verifyX()` checks the results of the JPF run, and accordingly throws an `AssertionError` in case it does not correspond to the expected result. The most common goals are
  43
  44  * `verifyNoPropertyViolation` - JPF is not supposed to find an error
  45  * `verifyPropertyViolation` - JPF is supposed to find the specified property violation
  46  * `verifyUnhandledException` - JPF is supposed to detect an unhandled exception of the specified type
  47  * `verifyAssertionError` - same for AssertionErrors
  48  * `verifyDeadlock` - JPF is supposed to find a deadlock
  49
  50 Each of these methods actually delegate running JPF to a corresponding method whose name does not start with 'verify..'. These workhorse methods expect explicit specification of the JPF arguments (including SUT main class name and method names), but they return JPF objects, and therefore can be used for more sophisticated JPF inspection (e.g. to find out about the number of states).
  51
  52 `TestJPF` also provides some convenience methods that can be used within test methods to find out which environment the code is executed from:
  53
  54  * `isJPFRun()` - returns true if the code is executed under JPF
  55  * `isJUnitRun()` - returns true if the code is executed under JUnit by the host VM
  56  * `isRunTestRun()` - returns true if the code is executed by RunTest.jar
  57
  58 Here is an example of a typical test method that uses some of these features:
  59
  60 ~~~~~~~~ {.java}
  61   @Test public void testIntFieldPerturbation() {
  62
  63     if (!isJPFRun()){ // run this outside of JPF
  64       Verify.resetCounter(0);
  65     }
  66
  67     if (verifyNoPropertyViolation("+listener=.listener.Perturbator",
  68                                   "+perturb.fields=data",
  69                                   "+perturb.data.class=.perturb.IntOverUnder",...
  70                                   "+perturb.data.delta=1")){
  71       // run this under JPF
  72       System.out.println("instance field perturbation test");
  73
  74       int d = data; // this should be perturbated
  75       System.out.println("d = " + d);
  76
  77       Verify.incrementCounter(0);
  78
  79     } else { // run this outside of JPF
  80       assert Verify.getCounter(0) == 3;
  81     }
  82   }
  83 ~~~~~~~~
  84
  85 ## Running JPF tests from command line ##
  86 To run JPF tests from the command line, use the RunTest.jar either from `jpf-core/build`, or the one that is distributed with your project containing the tests (`tools/RunTest.jar` for JPF projects). This is an executable jar that expects the test class and (optional) method test names as arguments. If no method names are provided, all `@Test` annotated methods are executed. Most projects have a convenience script `bin/test` to execute RunTest.jar.
  87
  88 ~~~~~~~~ {.bash}
  89 > bin/test gov.nasa.jpf.test.mc.data.PerturbatorTest testIntFieldPerturbation
  90
  91 ......................................... testing testIntFieldPerturbation
  92   running jpf with args: +listener=.listener.Perturbator +perturb.fields=data +perturb.data.class=.perturb.IntOverUnder +perturb.data.field=gov.nasa.jpf.test.mc.data.PerturbatorTest.data +perturb.data.delta=1 gov.nasa.jpf.test.mc.data.PerturbatorTest testIntFieldPerturbation
  93 JavaPathfinder v5.x - (C) RIACS/NASA Ames Research Center
  94
  95
  96 ====================================================== system under test
  97 application: gov/nasa/jpf/test/mc/data/PerturbatorTest.java
  98 arguments:   testIntFieldPerturbation
  99
 100 ====================================================== search started: 9/10/10 7:03 PM
 101 instance field perturbation test
 102 d = 43
 103 d = 42
 104 ...
 105 ====================================================== search finished: 9/10/10 7:03 PM
 106 ......................................... testIntFieldPerturbation: Ok
 107
 108 ......................................... execution of testsuite: gov.nasa.jpf.test.mc.data.PerturbatorTest SUCCEEDED
 109 .... [1] testIntFieldPerturbation: Ok
 110 ......................................... tests: 1, failures: 0, errors: 0
 111 ~~~~~~~~
 112
 113 ## Running JPF tests under JUnit ##
 114
 115 This is the preferred way to execute JPF regression tests, which is usually done from an Ant build.xml script containing a standard target such as
 116
 117 ~~~~~~~~ {.xml}
 118   ...
 119   <target name="test" depends="build" description="run core regression tests" if="have_tests">
 120      ...
 121      <junit printsummary="on" showoutput="off" haltonfailure="yes"
 122             fork="yes" forkmode="perTest" maxmemory="1024m" outputtoformatters="true">
 123        <classpath>
 124          <path refid="lib.path"/>
 125          <pathelement location="build/tests"/>
 126          ...
 127        </classpath>
 128        <batchtest todir="build/tests">
 129           <fileset dir="build/tests">
 130             <exclude name="**/JPF_*.class"/>
 131             <include name="**/*Test.class"/>
 132           </fileset>
 133       </batchtest>
 134     </junit>
 135   </target>
 136 ~~~~~~~~
 137
 138 Most JPF projects have build.xml files you can use as examples.
 139
 140 Please note this means that you should not have any inner classes, interfaces, annotation types etc. with a name ending with `"Test"` since JUnit would interpret these as test cases and most likely complain about missing constructors and `main()` methods.
 141
 142 ## Debugging tests ##
 143
 144 Typically, JPF tests are only executed from within an IDE if they fail and need to be debugged.
 145
 146 Under NetBeans, this can be done by selecting the test class, and then executing the *Debug File* command from the context menu. This will pop up a dialog that lets you enter a specific test method to debug. This method requires a properly set up ide-file-target.xml, which comes with most JPF projects.
 147
 148 Under Eclipse, you can select the test class and then execute **Debug As..** -> **Java Application**.