Mercurial > hg > Members > kono > jpf-core
diff src/main/gov/nasa/jpf/util/test/TestJPF.java @ 0:61d41facf527
initial v8 import (history reset)
author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
---|---|
date | Fri, 23 Jan 2015 10:14:01 -0800 |
parents | |
children |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/main/gov/nasa/jpf/util/test/TestJPF.java Fri Jan 23 10:14:01 2015 -0800 @@ -0,0 +1,1181 @@ +/* + * Copyright (C) 2014, United States Government, as represented by the + * Administrator of the National Aeronautics and Space Administration. + * All rights reserved. + * + * The Java Pathfinder core (jpf-core) platform is licensed under the + * Apache License, Version 2.0 (the "License"); you may not use this file except + * in compliance with the License. You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0. + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package gov.nasa.jpf.util.test; + +import gov.nasa.jpf.Config; +import gov.nasa.jpf.Error; +import gov.nasa.jpf.JPF; +import gov.nasa.jpf.JPFShell; +import gov.nasa.jpf.Property; +import gov.nasa.jpf.annotation.FilterField; +import gov.nasa.jpf.tool.RunTest; +import gov.nasa.jpf.util.DevNullPrintStream; +import gov.nasa.jpf.util.TypeRef; +import gov.nasa.jpf.util.JPFSiteUtils; +import gov.nasa.jpf.util.Reflection; +import gov.nasa.jpf.vm.ExceptionInfo; +import gov.nasa.jpf.vm.NoUncaughtExceptionsProperty; +import gov.nasa.jpf.vm.NotDeadlockedProperty; + +import java.io.PrintStream; +import java.io.PrintWriter; +import java.lang.annotation.Annotation; +import java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; +import java.lang.reflect.Modifier; +import java.util.ArrayList; +import java.util.List; + +/** + * base class for JPF unit tests. TestJPF mostly includes JPF invocations + * that check for occurrence or absence of certain execution results + * + * This class can be used in two modes: + * + * <ol> + * <li> wrapping a number of related tests for different SuTs into one class + * (suite) that calls the various JPF runners with complete argument lists + * (as in JPF.main(String[]args)) </li> + * + * <li> derive a class from TestJPF that uses the "..This" methods, which in + * turn use reflection to automatically append the test class and method to the + * JPF.main argument list (based on the calling class / method names). Note that + * you have to obey naming conventions for this to work: + * + * <li> the SuT class has to be the same as the test class without "Test", e.g. + * "CastTest" -> "Cast" </li> + * + * <li> the SuT method has to have the same name as the @Test method that + * invokes JPF, e.g. "CastTest {.. @Test void testArrayCast() ..}" -> + * "Cast {.. void testArrayCast()..} </li> + * </ol> + */ +public abstract class TestJPF implements JPFShell { + static PrintStream out = System.out; + + public static final String UNNAMED_PACKAGE = ""; + public static final String SAME_PACKAGE = null; + + //--- those are only used outside of JPF execution + @FilterField protected static boolean globalRunDirectly, globalShowConfig; + + @FilterField protected static boolean runDirectly; // don't run test methods through JPF, invoke it directly + @FilterField protected static boolean stopOnFailure; // stop as soon as we encounter a failed test or error + @FilterField protected static boolean showConfig; // for debugging purposes + @FilterField protected static boolean showConfigSources; // for debugging purposes + @FilterField protected static boolean hideSummary; + + @FilterField protected static boolean quiet; // don't show test output + + @FilterField protected String sutClassName; + + static class GlobalArg { + String key; + String val; + + GlobalArg (String k, String v){ + key = k; + val = v; + } + } + + // it seems wrong to pull globalArgs here instead of setting it from + // RunTest, but RunTest has to make sure TestJPF is loaded through the + // JPFClassLoader, i.e. cannot directly reference this class. + + @FilterField static ArrayList<GlobalArg> globalArgs; + + protected static ArrayList<GlobalArg> getGlobalArgs() { + // NOTE - this is only set if we execute tests from build.xml + Config globalConf = RunTest.getConfig(); + if (globalConf != null){ + ArrayList<GlobalArg> list = new ArrayList<GlobalArg>(); + + //--- the "test.<key>" specs + String[] testKeys = globalConf.getKeysStartingWith("test."); + if (testKeys.length > 0){ + for (String key : testKeys){ + String val = globalConf.getString(key); + // <2do> this is a hack to avoid the problem of not being able to store + // empty/nil/null values in the global config (they are removed during global config init) + if (val.equals("REMOVE")){ + val = null; + } + + key = key.substring(5); + + list.add(new GlobalArg(key,val)); + } + } + + return list; + } + + return null; + } + + static { + if (!isJPFRun()){ + globalArgs = getGlobalArgs(); + } + } + + //--- internal methods + + public static void fail (String msg, String[] args, String cause){ + StringBuilder sb = new StringBuilder(); + + sb.append(msg); + if (args != null){ + for (String s : args){ + sb.append(s); + sb.append(' '); + } + } + + if (cause != null){ + sb.append(':'); + sb.append(cause); + } + + fail(sb.toString()); + } + + public static void fail (){ + throw new AssertionError(); + } + + public static void fail (String msg){ + throw new AssertionError(msg); + } + + public void report (String[] args) { + if (!quiet){ + out.print(" running jpf with args:"); + + for (int i = 0; i < args.length; i++) { + out.print(' '); + out.print(args[i]); + } + + out.println(); + } + } + + /** + * compute the SuT class name for a given JUnit test class: remove + * optionally ending "..Test", and replace package (if specified) + * + * @param testClassName the JUnit test class + * @param sutPackage optional SuT package name (without ending '.', null + * os SAME_PACKAGE means same package, "" or UNNAMED_PACKAGE means unnamed package) + * @return main class name of system under test + */ + protected static String getSutClassName (String testClassName, String sutPackage){ + + String sutClassName = testClassName; + + int i = sutClassName.lastIndexOf('.'); + if (i >= 0){ // testclass has a package + + if (sutPackage == null){ // use same package + // nothing to do + } else if (sutPackage.length() > 0) { // explicit sut package + sutClassName = sutPackage + sutClassName.substring(i); + + } else { // unnamed sut package + sutClassName = sutClassName.substring(i+1); + } + + } else { // test class has no package + if (sutPackage == null || sutPackage.length() == 0){ // use same package + // nothing to do + } else { // explicit sut package + sutClassName = sutPackage + '.' + sutClassName; + } + } + + if (sutClassName.endsWith("JPF")) { + sutClassName = sutClassName.substring(0, sutClassName.length() - 3); + } + + return sutClassName; + } + + // we can't set the sutClassName only from main() called methods (like + // runTestsOfThisClass()) since main() doesn't get called if this is executed + // by Ant (via <junit> task) + // the default ctor is always executed + public TestJPF () { + sutClassName = getSutClassName(getClass().getName(), SAME_PACKAGE); + } + + + + //------ the API to be used by subclasses + + /** + * to be used from default ctor of derived class if the SuT is in a different + * package + * @param sutClassName the qualified SuT class name to be checked by JPF + */ + protected TestJPF (String sutClassName){ + this.sutClassName = sutClassName; + } + + public static boolean isJPFRun () { + return false; + } + + public static boolean isJUnitRun() { + // intercepted by native peer if this runs under JPF + Throwable t = new Throwable(); + t.fillInStackTrace(); + + for (StackTraceElement se : t.getStackTrace()){ + if (se.getClassName().startsWith("org.junit.")){ + return true; + } + } + + return false; + } + + public static boolean isRunTestRun() { + // intercepted by native peer if this runs under JPF + Throwable t = new Throwable(); + t.fillInStackTrace(); + + for (StackTraceElement se : t.getStackTrace()){ + if (se.getClassName().equals("gov.nasa.jpf.tool.RunTest")){ + return true; + } + } + + return false; + } + + + protected static void getOptions (String[] args){ + runDirectly = globalRunDirectly; + showConfig = globalShowConfig; + + // hideSummary and stopOnFailure only make sense as global options anyways + + if (args != null){ + for (int i=0; i<args.length; i++){ + String a = args[i]; + if (a != null){ + if (a.length() > 0){ + if (a.charAt(0) == '-'){ + a = a.substring(1); + + if (a.equals("d")){ + runDirectly = true; + } else if (a.equals("s") || a.equals("show")){ + showConfig = true; + } else if (a.equals("l") || a.equals("log")){ + showConfigSources = true; + } else if (a.equals("q") || a.equals("quiet")){ + quiet = true; + } else if (a.equals("x")){ + stopOnFailure = true; + } else if (a.equals("h")){ + hideSummary = true; + } + args[i] = null; // set it consumed + + } else { + break; // done, this is a test method + } + } + } + } + } + } + + protected static boolean hasExplicitTestMethods(String[] args){ + for (String a : args){ + if (a != null){ + return true; + } + } + + return false; + } + + protected static List<Method> getMatchingMethods(Class<? extends TestJPF> testCls, + int setModifiers, int unsetModifiers, String[] annotationNames){ + List<Method> list = new ArrayList<Method>(); + + for (Method m : testCls.getMethods()){ + if (isMatchingMethod(m, setModifiers, unsetModifiers, annotationNames)){ + list.add(m); + } + } + + return list; + } + + protected static boolean isMatchingMethod(Method m, int setModifiers, int unsetModifiers, String[] annotationNames) { + int mod = m.getModifiers(); + if (((mod & setModifiers) != 0) && ((mod & unsetModifiers) == 0)) { + if (m.getParameterTypes().length == 0) { + if (annotationNames != null){ + Annotation[] annotations = m.getAnnotations(); + for (int i = 0; i < annotations.length; i++) { + String annotType = annotations[i].annotationType().getName(); + for (int j = 0; j < annotationNames.length; j++) { + if (annotType.equals(annotationNames[j])) { + return true; + } + } + } + } else { + return true; + } + } + } + + return false; + } + + protected static List<Method> getContextMethods(Class<? extends TestJPF> testCls, + int setModifiers, int unsetModifiers, String annotation){ + String[] annotations = {annotation}; + + List<Method> list = new ArrayList<Method>(); + for (Method m : testCls.getMethods()){ + if (isMatchingMethod(m, setModifiers, unsetModifiers, annotations)){ + list.add(m); + } + } + return list; + } + + protected static List<Method> getBeforeMethods(Class<? extends TestJPF> testCls){ + return getContextMethods(testCls, Modifier.PUBLIC, Modifier.STATIC, "org.junit.Before"); + } + + protected static List<Method> getAfterMethods(Class<? extends TestJPF> testCls){ + return getContextMethods(testCls, Modifier.PUBLIC, Modifier.STATIC, "org.junit.After"); + } + + protected static List<Method> getBeforeClassMethods(Class<? extends TestJPF> testCls){ + return getContextMethods(testCls, Modifier.PUBLIC | Modifier.STATIC, 0, "org.junit.BeforeClass"); + } + + protected static List<Method> getAfterClassMethods(Class<? extends TestJPF> testCls){ + return getContextMethods(testCls, Modifier.PUBLIC | Modifier.STATIC, 0, "org.junit.AfterClass"); + } + + protected static boolean haveTestMethodSpecs( String[] args){ + if (args != null && args.length > 0){ + for (int i=0; i<args.length; i++){ + if (args[i] != null){ + return true; + } + } + } + + return false; + } + + protected static List<Method> getTestMethods(Class<? extends TestJPF> testCls, String[] args){ + String[] testAnnotations = {"org.junit.Test", "org.testng.annotations.Test"}; + + if (haveTestMethodSpecs( args)){ // test methods specified as arguments + List<Method> list = new ArrayList<Method>(); + + for (String test : args){ + if (test != null){ + + try { + Method m = testCls.getMethod(test); + + if (isMatchingMethod(m, Modifier.PUBLIC, Modifier.STATIC, null /*testAnnotations*/ )){ + list.add(m); + } else { + throw new RuntimeException("test method must be @Test annotated public instance method without arguments: " + test); + } + + } catch (NoSuchMethodException x) { + throw new RuntimeException("method: " + test + + "() not in test class: " + testCls.getName(), x); + } + } + } + + return list; + + } else { // no explicit test method specification, get all matches + return getMatchingMethods(testCls, Modifier.PUBLIC, Modifier.STATIC, testAnnotations); + } + } + + + protected static void reportTestStart(String mthName){ + if (!quiet){ + System.out.println(); + System.out.print("......................................... testing "); + System.out.print(mthName); + System.out.println("()"); + } + } + + protected static void reportTestInitialization(String mthName){ + if (!quiet){ + System.out.print(".... running test initialization: "); + System.out.print(mthName); + System.out.println("()"); + } + } + + protected static void reportTestCleanup(String mthName){ + if (!quiet){ + System.out.print(".... running test cleanup: "); + System.out.print(mthName); + System.out.println("()"); + } + } + + protected static void reportTestFinished(String msg){ + if (!quiet){ + System.out.print("......................................... "); + System.out.println(msg); + } + } + + protected static void reportResults(String clsName, int nTests, int nFailures, int nErrors, List<String> results){ + System.out.println(); + System.out.print("......................................... execution of testsuite: " + clsName); + if (nFailures > 0 || nErrors > 0){ + System.out.println(" FAILED"); + } else if (nTests > 0) { + System.out.println(" SUCCEEDED"); + } else { + System.out.println(" OBSOLETE"); + } + + if (!quiet){ + if (results != null) { + int i = 0; + for (String result : results) { + System.out.print(".... [" + ++i + "] "); + System.out.println(result); + } + } + } + + System.out.print("........................................."); + System.out.println(" tests: " + nTests + ", failures: " + nFailures + ", errors: " + nErrors); + } + + + static void invoke (Method m, Object testObject) throws IllegalAccessException, InvocationTargetException { + PrintStream sysOut = null; + + try { + if (quiet){ + sysOut = System.out; + System.setOut( new DevNullPrintStream()); + } + + m.invoke( testObject); + + } finally { + if (quiet){ + System.setOut( sysOut); + } + } + } + + /** + * this is the main test loop if this TestJPF instance is executed directly + * or called from RunTest. It is *not* called if this is executed from JUnit + */ + public static void runTests (Class<? extends TestJPF> testCls, String... args){ + int nTests = 0; + int nFailures = 0; + int nErrors = 0; + String testMethodName = null; + List<String> results = null; + + getOptions(args); + globalRunDirectly = runDirectly; + globalShowConfig = showConfig; + boolean globalStopOnFailure = stopOnFailure; + + try { + List<Method> testMethods = getTestMethods(testCls, args); + results = new ArrayList<String>(testMethods.size()); + + // check if we have JUnit style housekeeping methods (initialization and + // cleanup should use the same mechanisms as JUnit) + + List<Method> beforeClassMethods = getBeforeClassMethods(testCls); + List<Method> afterClassMethods = getAfterClassMethods(testCls); + + List<Method> beforeMethods = getBeforeMethods(testCls); + List<Method> afterMethods = getAfterMethods(testCls); + + for (Method initMethod : beforeClassMethods) { + reportTestInitialization(initMethod.getName()); + initMethod.invoke(null); + } + + for (Method testMethod : testMethods) { + testMethodName = testMethod.getName(); + String result = testMethodName; + try { + Object testObject = testCls.newInstance(); + + nTests++; + reportTestStart( testMethodName); + + // run per test initialization methods + for (Method initMethod : beforeMethods){ + reportTestInitialization( initMethod.getName()); + invoke( initMethod, testObject); + } + + // now run the test method itself + invoke( testMethod, testObject); + result += ": Ok"; + + // run per test initialization methods + for (Method cleanupMethod : afterMethods){ + reportTestCleanup( cleanupMethod.getName()); + invoke( cleanupMethod, testObject); + } + + } catch (InvocationTargetException x) { + Throwable cause = x.getCause(); + cause.printStackTrace(); + if (cause instanceof AssertionError) { + nFailures++; + reportTestFinished("test method failed with: " + cause.getMessage()); + result += ": Failed"; + } else { + nErrors++; + reportTestFinished("unexpected error while executing test method: " + cause.getMessage()); + result += ": Error"; + } + + if (globalStopOnFailure){ + break; + } + } + + results.add(result); + reportTestFinished(result); + } + + for (Method cleanupMethod : afterClassMethods) { + reportTestCleanup( cleanupMethod.getName()); + cleanupMethod.invoke(null); + } + + + //--- those exceptions are unexpected and represent unrecoverable test harness errors + } catch (InvocationTargetException x) { + Throwable cause = x.getCause(); + cause.printStackTrace(); + nErrors++; + reportTestFinished("TEST ERROR: @BeforeClass,@AfterClass method failed: " + x.getMessage()); + + } catch (InstantiationException x) { + nErrors++; + reportTestFinished("TEST ERROR: cannot instantiate test class: " + x.getMessage()); + } catch (IllegalAccessException x) { // can't happen if getTestMethods() worked + nErrors++; + reportTestFinished("TEST ERROR: default constructor or test method not public: " + testMethodName); + } catch (IllegalArgumentException x) { // can't happen if getTestMethods() worked + nErrors++; + reportTestFinished("TEST ERROR: illegal argument for test method: " + testMethodName); + } catch (RuntimeException rx) { + nErrors++; + reportTestFinished("TEST ERROR: " + rx.toString()); + } + + if (!hideSummary){ + reportResults(testCls.getName(), nTests, nFailures, nErrors, results); + } + + if (nErrors > 0 || nFailures > 0){ + if (isRunTestRun()){ + // we need to reportTestFinished this test has failed + throw new RunTest.Failed(); + } + } + } + + static String getProperty(String key){ + // intercepted by peer + return null; + } + + /** + * this is the JPF entry method in case there is no main() in the test class + * + * <2do> we should support test method arguments here + */ + static void runTestMethod(String args[]) throws Throwable { + String testClsName = getProperty("target"); + String testMthName = getProperty("target.test_method"); + + Class<?> testCls = Class.forName(testClsName); + Object target = testCls.newInstance(); + + Method method = testCls.getMethod(testMthName); + + try { + method.invoke(target); + } catch (InvocationTargetException e) { + throw e.getCause(); + } + } + + /** + * NOTE: this needs to be called from the concrete test class, typically from + * its main() method, otherwise we don't know the name of the class we have + * to pass to JPF + */ + protected static void runTestsOfThisClass (String[] testMethods){ + // needs to be at the same stack level, so we can't delegate + Class<? extends TestJPF> testClass = Reflection.getCallerClass(TestJPF.class); + runTests(testClass, testMethods); + } + + /** + * needs to be broken up into two methods for cases that do additional + * JPF initialization (jpf-inspector) + * + * this is called from the various verifyX() methods (i.e. host VM) to + * start JPF, it is never executed under JPF + */ + protected JPF createAndRunJPF (StackTraceElement testMethod, String[] args) { + JPF jpf = createJPF( testMethod, args); + if (jpf != null){ + jpf.run(); + } + return jpf; + } + + /** + * this is never executed under JPF + */ + protected JPF createJPF (StackTraceElement testMethod, String[] args) { + JPF jpf = null; + + Config conf = new Config(args); + + // --- add global args (if we run under RunTest) + if (globalArgs != null) { + for (GlobalArg ga : globalArgs) { + String key = ga.key; + String val = ga.val; + if (val != null){ + conf.put(key, val); + } else { + conf.remove(key); + } + } + } + + setTestTargetKeys(conf, testMethod); + + // --- initialize the classpath from <projectId>.test_classpath + String projectId = JPFSiteUtils.getCurrentProjectId(); + if (projectId != null) { + String testCp = conf.getString(projectId + ".test_classpath"); + if (testCp != null) { + conf.append("classpath", testCp, ","); + } + } + + // --- if we have any specific test property overrides, do so + conf.promotePropertyCategory("test."); + + getOptions(args); + + if (showConfig || showConfigSources) { + PrintWriter pw = new PrintWriter(System.out, true); + if (showConfigSources) { + conf.printSources(pw); + } + + if (showConfig) { + conf.print(pw); + } + pw.flush(); + } + + jpf = new JPF(conf); + + return jpf; + } + + protected void setTestTargetKeys(Config conf, StackTraceElement testMethod) { + conf.put("target.entry", "runTestMethod([Ljava/lang/String;)V"); + conf.put("target", testMethod.getClassName()); + conf.put("target.test_method", testMethod.getMethodName()); + } + + //--- the JPFShell interface + @Override + public void start(String[] testMethods){ + Class<? extends TestJPF> testClass = getClass(); // this is an instance method + runTests(testClass, testMethods); + } + + protected StackTraceElement getCaller(){ + StackTraceElement[] st = (new Throwable()).getStackTrace(); + return st[2]; + } + + protected StackTraceElement setTestMethod (String clsName, String mthName){ + return new StackTraceElement( clsName, mthName, null, -1); + } + + protected StackTraceElement setTestMethod (String mthName){ + return new StackTraceElement( getClass().getName(), mthName, null, -1); + } + + + //--- the JPF run test methods + + /** + * run JPF expecting a AssertionError in the SuT + * @param args JPF main() arguments + */ + protected JPF assertionError (StackTraceElement testMethod, String... args){ + return unhandledException( testMethod, "java.lang.AssertionError", null, args ); + } + protected JPF assertionError (String... args) { + return unhandledException( getCaller(), "java.lang.AssertionError", null, args ); + } + + protected JPF assertionErrorDetails (StackTraceElement testMethod, String details, String... args) { + return unhandledException( testMethod, "java.lang.AssertionError", details, args ); + } + protected JPF assertionErrorDetails (String details, String... args) { + return unhandledException( getCaller(), "java.lang.AssertionError", details, args ); + } + protected boolean verifyAssertionErrorDetails (String details, String... args){ + if (runDirectly) { + return true; + } else { + unhandledException( getCaller(), "java.lang.AssertionError", details, args); + return false; + } + } + protected boolean verifyAssertionError (String... args){ + if (runDirectly) { + return true; + } else { + unhandledException( getCaller(), "java.lang.AssertionError", null, args); + return false; + } + } + + /** + * run JPF expecting no SuT property violations + */ + protected JPF noPropertyViolation (StackTraceElement testMethod, String... args) { + JPF jpf = null; + + report(args); + + try { + jpf = createAndRunJPF( testMethod, args); + } catch (Throwable t) { + // we get as much as one little hickup and we declare it failed + t.printStackTrace(); + fail("JPF internal exception executing: ", args, t.toString()); + return jpf; + } + + List<Error> errors = jpf.getSearchErrors(); + if ((errors != null) && (errors.size() > 0)) { + fail("JPF found unexpected errors: " + (errors.get(0)).getDescription()); + } + + return jpf; + } + + protected JPF noPropertyViolation (String... args) { + return noPropertyViolation( getCaller(), args); + } + + protected boolean verifyNoPropertyViolation (String...args){ + if (runDirectly) { + return true; + } else { + noPropertyViolation( getCaller(), args); + return false; + } + } + + /** + * NOTE: this uses the exception class name because it might be an + * exception type that is only known to JPF (i.e. not in the native classpath) + * + * @param xClassName name of the exception base type that is expected + * @param details detail message of the expected exception + * @param args JPF arguments + */ + protected JPF unhandledException (StackTraceElement testMethod, String xClassName, String details, String... args) { + JPF jpf = null; + + report(args); + + try { + jpf = createAndRunJPF(testMethod, args); + } catch (Throwable t) { + t.printStackTrace(); + fail("JPF internal exception executing: ", args, t.toString()); + return jpf; + } + + Error error = jpf.getLastError(); + if (error != null){ + Property errorProperty = error.getProperty(); + if (errorProperty instanceof NoUncaughtExceptionsProperty){ + ExceptionInfo xi = ((NoUncaughtExceptionsProperty)errorProperty).getUncaughtExceptionInfo(); + String xn = xi.getExceptionClassname(); + if (!xn.equals(xClassName)) { + fail("JPF caught wrong exception: " + xn + ", expected: " + xClassName); + } + + if (details != null) { + String gotDetails = xi.getDetails(); + if (gotDetails == null) { + fail("JPF caught the right exception but no details, expected: " + details); + } else { + if (!gotDetails.endsWith(details)) { + fail("JPF caught the right exception but the details were wrong: " + gotDetails + ", expected: " + details); + } + } + } + } else { // error not a NoUncaughtExceptionsProperty + fail("JPF failed to catch exception executing: ", args, ("expected " + xClassName)); + } + } else { // no error + fail("JPF failed to catch exception executing: ", args, ("expected " + xClassName)); + } + + return jpf; + } + + protected JPF unhandledException (String xClassName, String details, String... args) { + return unhandledException( getCaller(), xClassName, details, args); + } + + + protected boolean verifyUnhandledExceptionDetails (String xClassName, String details, String... args){ + if (runDirectly) { + return true; + } else { + unhandledException( getCaller(), xClassName, details, args); + return false; + } + } + protected boolean verifyUnhandledException (String xClassName, String... args){ + if (runDirectly) { + return true; + } else { + unhandledException( getCaller(), xClassName, null, args); + return false; + } + } + + + /** + * run JPF expecting it to throw an exception + * NOTE - xClassName needs to be the concrete exception, not a super class + * @param args JPF main() arguments + */ + protected JPF jpfException (StackTraceElement testMethod, Class<? extends Throwable> xCls, String... args) { + JPF jpf = null; + Throwable exception = null; + + report(args); + + try { + jpf = createAndRunJPF( testMethod, args); + } catch (JPF.ExitException xx) { + exception = xx.getCause(); + } catch (Throwable x) { + exception = x; + } + + if (exception != null){ + if (!xCls.isAssignableFrom(exception.getClass())){ + fail("JPF produced wrong exception: " + exception + ", expected: " + xCls.getName()); + } + } else { + fail("JPF failed to produce exception, expected: " + xCls.getName()); + } + + return jpf; + } + + protected JPF jpfException (Class<? extends Throwable> xCls, String... args) { + return jpfException( getCaller(), xCls, args); + } + + protected boolean verifyJPFException (TypeRef xClsSpec, String... args){ + if (runDirectly) { + return true; + + } else { + try { + Class<? extends Throwable> xCls = xClsSpec.asNativeSubclass(Throwable.class); + + jpfException( getCaller(), xCls, args); + + } catch (ClassCastException ccx){ + fail("not a property type: " + xClsSpec); + } catch (ClassNotFoundException cnfx){ + fail("property class not found: " + xClsSpec); + } + return false; + } + } + + + + /** + * run JPF expecting a property violation of the SuT + * @param args JPF main() arguments + */ + protected JPF propertyViolation (StackTraceElement testMethod, Class<? extends Property> propertyCls, String... args ){ + JPF jpf = null; + + report(args); + + try { + jpf = createAndRunJPF( testMethod, args); + } catch (Throwable t) { + t.printStackTrace(); + fail("JPF internal exception executing: ", args, t.toString()); + } + + List<Error> errors = jpf.getSearchErrors(); + if (errors != null) { + for (Error e : errors) { + if (propertyCls == e.getProperty().getClass()) { + return jpf; // success, we got the sucker + } + } + } + + fail("JPF failed to detect error: " + propertyCls.getName()); + return jpf; + } + + protected JPF propertyViolation (Class<? extends Property> propertyCls, String... args ){ + return propertyViolation( getCaller(), propertyCls, args); + } + + protected boolean verifyPropertyViolation (TypeRef propertyClsSpec, String... args){ + if (runDirectly) { + return true; + + } else { + try { + Class<? extends Property> propertyCls = propertyClsSpec.asNativeSubclass(Property.class); + propertyViolation( getCaller(), propertyCls, args); + + } catch (ClassCastException ccx){ + fail("not a property type: " + propertyClsSpec); + } catch (ClassNotFoundException cnfx){ + fail("property class not found: " + propertyClsSpec); + } + return false; + } + } + + + /** + * run JPF expecting a deadlock in the SuT + * @param args JPF main() arguments + */ + protected JPF deadlock (String... args) { + return propertyViolation( getCaller(), NotDeadlockedProperty.class, args ); + } + + protected boolean verifyDeadlock (String... args){ + if (runDirectly) { + return true; + } else { + propertyViolation( getCaller(), NotDeadlockedProperty.class, args); + return false; + } + } + + // these are the org.junit.Assert APIs, but we don't want org.junit to be + // required to run tests + + public static void assertEquals(String msg, Object expected, Object actual){ + if (expected == null && actual == null) { + return; + } + + if (expected != null && expected.equals(actual)) { + return; + } + + fail(msg); + } + + public static void assertEquals(Object expected, Object actual){ + assertEquals("", expected, actual); + } + + public static void assertEquals(String msg, int expected, int actual){ + if (expected != actual) { + fail(msg); + } + } + + public static void assertEquals(int expected, int actual){ + assertEquals("expected != actual : " + expected + " != " + actual, expected, actual); + } + + public static void assertEquals(String msg, long expected, long actual){ + if (expected != actual) { + fail(msg); + } + } + + public static void assertEquals(long expected, long actual){ + assertEquals("expected != actual : " + expected + " != " + actual, + expected, actual); + } + + public static void assertEquals(double expected, double actual){ + if (expected != actual){ + fail("expected != actual : " + expected + " != " + actual); + } + } + + public static void assertEquals(String msg, double expected, double actual){ + if (expected != actual){ + fail(msg); + } + } + + public static void assertEquals(float expected, float actual){ + if (expected != actual){ + fail("expected != actual : " + expected + " != " + actual); + } + } + + public static void assertEquals(String msg, float expected, float actual){ + if (expected != actual){ + fail(msg); + } + } + + public static void assertEquals(String msg, double expected, double actual, double delta){ + if (Math.abs(expected - actual) > delta) { + fail(msg); + } + } + + public static void assertEquals(double expected, double actual, double delta){ + assertEquals("Math.abs(expected - actual) > delta : " + "Math.abs(" + expected + " - " + actual + ") > " + delta, + expected, actual, delta); + } + + public static void assertEquals(String msg, float expected, float actual, float delta){ + if (Math.abs(expected - actual) > delta) { + fail(msg); + } + } + + public static void assertEquals(float expected, float actual, float delta){ + assertEquals("Math.abs(expected - actual) > delta : " + "Math.abs(" + expected + " - " + actual + ") > " + delta, + expected, actual, delta); + } + + public static void assertArrayEquals(byte[] expected, byte[] actual){ + if (((expected == null) != (actual == null)) || + (expected.length != actual.length)){ + fail("array sizes different"); + } + + for (int i=0; i<expected.length; i++){ + if (expected[i] != actual[i]){ + fail("array element" + i + " different, expected " + expected[i] + ", actual " + actual[i]); + } + } + } + + public static void assertNotNull(String msg, Object o) { + if (o == null) { + fail(msg); + } + } + + public static void assertNotNull(Object o){ + assertNotNull("o == null", o); + } + + public static void assertNull(String msg, Object o){ + if (o != null) { + fail(msg); + } + } + + public static void assertNull(Object o){ + assertNull("o != null", o); + } + + public static void assertSame(String msg, Object expected, Object actual){ + if (expected != actual) { + fail(msg); + } + } + + public static void assertSame(Object expected, Object actual){ + assertSame("expected != actual : " + expected + " != " + actual, expected, actual); + } + + public static void assertFalse (String msg, boolean cond){ + if (cond) { + fail(msg); + } + } + + public static void assertFalse (boolean cond){ + assertFalse("", cond); + } + + public static void assertTrue (String msg, boolean cond){ + if (!cond) { + fail(msg); + } + } + + public static void assertTrue (boolean cond){ + assertTrue("", cond); + } +}