From a9b967e5d421e61da227166a21e748c055a44534 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Mon, 9 Sep 2024 22:34:58 +0200 Subject: [PATCH] Skip unsupported regression tests (#615) Add the possibility to mark regression tests as skipped after running them. Therefore we store tests (consisting of file, settings, toolchain) along with a verdict (represented using a regular expression) in a separate file. If running a test yield a result that matches this verdict, it is marked as skipped, otherwise as failed. This helps us to avoid test failures for tests that are expected or known to fail (mostly due to timeouts for some settings/toolchains). Co-authored-by: maul.esel --- .../concurrent/bpl/regression/.testignore | 17 +++ .../pthreads/races/regression/.testignore | 16 +++ .../pthreads/regression/.testignore | 5 + trunk/examples/lassos/regression/.testignore | 5 + .../regression/c/noMathSAT/.testignore | 7 + .../quantifier/regression/bpl/.testignore | 4 + .../programs/regression/bpl/.testignore | 4 + .../bpl/interprocedural/.testignore | 19 +++ .../regression/bpl/toolDirectives/.testignore | 25 ++++ .../programs/regression/c/.testignore | 126 ++++++++++++++++++ .../regression/c/interprocedural/.testignore | 10 ++ .../ultimate/test/UltimateTestCase.java | 16 ++- .../test/decider/ITestResultDecider.java | 6 +- .../decider/SafetyCheckTestResultDecider.java | 42 +++++- .../TerminationAnalysisTestResultDecider.java | 20 +++ .../decider/ThreeTierTestResultDecider.java | 24 +++- .../testfactory/FactoryTestRunner.java | 52 ++++++++ .../META-INF/MANIFEST.MF | 3 +- .../AbstractRegressionTestSuite.java | 50 ++++++- .../generic/ChcRegressionTestSuite.java | 6 +- .../generic/DataRaceRegressionTestSuite.java | 20 +-- .../generic/RegressionTestSuite.java | 6 + ...qCheckerRedundancyRegressionTestSuite.java | 3 +- ...nedIntegerOverflowRegressionTestSuite.java | 6 + .../TerminationRegressionTestSuite.java | 6 + 25 files changed, 463 insertions(+), 35 deletions(-) create mode 100644 trunk/examples/concurrent/bpl/regression/.testignore create mode 100644 trunk/examples/concurrent/pthreads/races/regression/.testignore create mode 100644 trunk/examples/concurrent/pthreads/regression/.testignore create mode 100644 trunk/examples/lassos/regression/.testignore create mode 100644 trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore create mode 100644 trunk/examples/programs/quantifier/regression/bpl/.testignore create mode 100644 trunk/examples/programs/regression/bpl/.testignore create mode 100644 trunk/examples/programs/regression/bpl/interprocedural/.testignore create mode 100644 trunk/examples/programs/regression/bpl/toolDirectives/.testignore create mode 100644 trunk/examples/programs/regression/c/.testignore create mode 100644 trunk/examples/programs/regression/c/interprocedural/.testignore diff --git a/trunk/examples/concurrent/bpl/regression/.testignore b/trunk/examples/concurrent/bpl/regression/.testignore new file mode 100644 index 00000000000..10b09b767bc --- /dev/null +++ b/trunk/examples/concurrent/bpl/regression/.testignore @@ -0,0 +1,17 @@ +# Timeout with Automizer, GemCutter succeeds +TIMEOUT: +- task: MirabelleConcurrentIncrement.bpl + settings: ReachSafety-32bit-Automizer.epf + toolchain: ReachSafety.xml +- task: concurrent_increment.bpl + settings: ReachSafety-32bit-Automizer.epf + toolchain: ReachSafety.xml +- task: equal-array-sums.bpl + settings: ReachSafety-32bit-Automizer.epf + toolchain: ReachSafety.xml +- task: loop-lockstep-example.bpl + settings: ReachSafety-32bit-Automizer.epf + toolchain: ReachSafety.xml +- task: sum_invariant.bpl + settings: ReachSafety-32bit-Automizer.epf + toolchain: ReachSafety.xml diff --git a/trunk/examples/concurrent/pthreads/races/regression/.testignore b/trunk/examples/concurrent/pthreads/races/regression/.testignore new file mode 100644 index 00000000000..a5de3d6a4dd --- /dev/null +++ b/trunk/examples/concurrent/pthreads/races/regression/.testignore @@ -0,0 +1,16 @@ +TIMEOUT: +- task: static-array-copy3.c + settings: DataRace-32bit-Automizer_Bitvector.epf + toolchain: DataRace.xml +- task: static-array-copy3.c + settings: DataRace-32bit-Automizer_Default.epf + toolchain: DataRace.xml +- task: static-array-copy3.c + settings: DataRace-32bit-GemCutter_Bitvector.epf + toolchain: DataRace.xml + +# Crash in MathSAT +SMTLIBException.*mathsat: +- task: struct-array-write.c + settings: DataRace-32bit-GemCutter_Bitvector.epf + toolchain: DataRace.xml diff --git a/trunk/examples/concurrent/pthreads/regression/.testignore b/trunk/examples/concurrent/pthreads/regression/.testignore new file mode 100644 index 00000000000..f0fe6b28fd3 --- /dev/null +++ b/trunk/examples/concurrent/pthreads/regression/.testignore @@ -0,0 +1,5 @@ +# Timeout with Automizer, GemCutter succeeds +TIMEOUT: +- task: NonAtomicIncrement_2Threads.c + settings: ReachSafety-32bit-Automizer.epf + toolchain: ReachSafety.xml diff --git a/trunk/examples/lassos/regression/.testignore b/trunk/examples/lassos/regression/.testignore new file mode 100644 index 00000000000..a62b29f6d08 --- /dev/null +++ b/trunk/examples/lassos/regression/.testignore @@ -0,0 +1,5 @@ +# The program contains non-linear-arithmetic, so we don't succeed with the linear setting +Unable to decide termination: +- task: ConvincingNondeterminism01.bpl + settings: BuchiAutomizerBpl-linear.epf + toolchain: BuchiAutomizerBpl.xml \ No newline at end of file diff --git a/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore new file mode 100644 index 00000000000..98f261bbceb --- /dev/null +++ b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/.testignore @@ -0,0 +1,7 @@ +TIMEOUT: +- task: SAS09-Float.c + settings: AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf + toolchain: AutomizerC.xml +- task: ctrans-float-rounding.c + settings: AutomizerC-Reach-32bit-Z3-IcWpLv-Float_Const.epf + toolchain: AutomizerC.xml diff --git a/trunk/examples/programs/quantifier/regression/bpl/.testignore b/trunk/examples/programs/quantifier/regression/bpl/.testignore new file mode 100644 index 00000000000..425385046fb --- /dev/null +++ b/trunk/examples/programs/quantifier/regression/bpl/.testignore @@ -0,0 +1,4 @@ +overapproximation: +- task: AuxVarInCall.bpl + settings: AutomizerBpl-forwardPredicates.epf + toolchain: AutomizerBpl.xml diff --git a/trunk/examples/programs/regression/bpl/.testignore b/trunk/examples/programs/regression/bpl/.testignore new file mode 100644 index 00000000000..0e6d1d6de5b --- /dev/null +++ b/trunk/examples/programs/regression/bpl/.testignore @@ -0,0 +1,4 @@ +TIMEOUT: +- task: nestedWhileSimple-Safe.bpl + settings: PdrAutomizerBpl.epf + toolchain: PdrAutomizerBpl.xml diff --git a/trunk/examples/programs/regression/bpl/interprocedural/.testignore b/trunk/examples/programs/regression/bpl/interprocedural/.testignore new file mode 100644 index 00000000000..0680edba95a --- /dev/null +++ b/trunk/examples/programs/regression/bpl/interprocedural/.testignore @@ -0,0 +1,19 @@ +TIMEOUT: +- task: BugLiveVariables03-Safe.bpl + settings: AutomizerBpl-FPandBP.epf + toolchain: AutomizerBpl.xml +- task: BugNestedSsaWithPendingContexts.bpl + settings: AutomizerBpl-forwardPredicates.epf + toolchain: AutomizerBpl.xml +- task: BugNoPredecessorOfReturnTransition.bpl + settings: PdrAutomizerBpl.epf + toolchain: PdrAutomizerBpl.xml + +# We are unable to backtranslate @diff from SMT to Boogie +unknown symbol.*@diff: +- task: BugLiveVariables03-Safe.bpl + settings: AutomizerBpl-nestedInterpolants.epf + toolchain: AutomizerBpl.xml +- task: BugLiveVariables04-Safe.bpl + settings: AutomizerBpl-nestedInterpolants.epf + toolchain: AutomizerBpl.xml diff --git a/trunk/examples/programs/regression/bpl/toolDirectives/.testignore b/trunk/examples/programs/regression/bpl/toolDirectives/.testignore new file mode 100644 index 00000000000..ad375761f78 --- /dev/null +++ b/trunk/examples/programs/regression/bpl/toolDirectives/.testignore @@ -0,0 +1,25 @@ +# Issue in SMTInterpol +Const is only supported for infinite index sort: +- task: ConstArray.bpl + settings: AutomizerBpl-nestedInterpolants.epf + toolchain: AutomizerBpl.xml +- task: ConstArray.bpl + settings: AutomizerBpl-nestedInterpolants.epf + toolchain: PdrAutomizerBpl.xml +- task: ConstArray.bpl + settings: PdrAutomizerBpl.epf + toolchain: PdrAutomizerBpl.xml + +Overapproximation: +- task: Overapproximation.bpl + settings: AutomizerBpl-nestedInterpolants.epf + toolchain: AutomizerBpl.xml +- task: Overapproximation.bpl + settings: AutomizerBpl-forwardPredicates.epf + toolchain: AutomizerBpl.xml +- task: Overapproximation.bpl + settings: AutomizerBpl-FPandBP.epf + toolchain: AutomizerBpl.xml +- task: Overapproximation.bpl + settings: PdrAutomizerBpl.epf + toolchain: PdrAutomizerBpl.xml diff --git a/trunk/examples/programs/regression/c/.testignore b/trunk/examples/programs/regression/c/.testignore new file mode 100644 index 00000000000..9f91edc0a51 --- /dev/null +++ b/trunk/examples/programs/regression/c/.testignore @@ -0,0 +1,126 @@ +# Fails due to overapproximation of bitwise operators in the integer translation +Overapproximation: +- task: bitwiseOrUnsigned.c + settings: AutomizerC-forwardPredicates.epf + toolchain: AutomizerC.xml +- task: bitwiseOrUnsigned.c + settings: AutomizerC-forwardPredicates_const.epf + toolchain: AutomizerC.xml +- task: bitwiseOrUnsigned.c + settings: AutomizerC-nestedInterpolants.epf + toolchain: AutomizerC.xml +- task: bitwiseOrUnsigned.c + settings: AutomizerC-nestedInterpolants_const.epf + toolchain: AutomizerC.xml +- task: bitwiseOrUnsigned.c + settings: BlockEncodingV2AutomizerC-forwardPredicates.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: bitwiseOrUnsigned.c + settings: KojakC-Reach-32Bit-Default.epf + toolchain: KojakC.xml +- task: bitwiseOrUnsignedMinimal.c + settings: AutomizerC-forwardPredicates.epf + toolchain: AutomizerC.xml +- task: bitwiseOrUnsignedMinimal.c + settings: AutomizerC-forwardPredicates_const.epf + toolchain: AutomizerC.xml +- task: bitwiseOrUnsignedMinimal.c + settings: AutomizerC-nestedInterpolants.epf + toolchain: AutomizerC.xml +- task: bitwiseOrUnsignedMinimal.c + settings: AutomizerC-nestedInterpolants_const.epf + toolchain: AutomizerC.xml +- task: bitwiseOrUnsignedMinimal.c + settings: BlockEncodingV2AutomizerC-forwardPredicates.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: bitwiseOrUnsignedMinimal.c + settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: bitwiseOrUnsignedMinimal.c + settings: KojakC-Reach-32Bit-Default.epf + toolchain: KojakC.xml +- task: builtin_ffs.c + settings: AutomizerC-forwardPredicates.epf + toolchain: AutomizerC.xml +- task: builtin_ffs.c + settings: AutomizerC-forwardPredicates_const.epf + toolchain: AutomizerC.xml +- task: builtin_ffs.c + settings: AutomizerC-nestedInterpolants.epf + toolchain: AutomizerC.xml +- task: builtin_ffs.c + settings: AutomizerC-nestedInterpolants_const.epf + toolchain: AutomizerC.xml +- task: builtin_ffs.c + settings: BlockEncodingV2AutomizerC-forwardPredicates.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: builtin_ffs.c + settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: builtin_ffs.c + settings: KojakC-Reach-32Bit-Default.epf + toolchain: KojakC.xml +- task: BitwiseOperations02.c + settings: AutomizerC-forwardPredicates.epf + toolchain: AutomizerC.xml +- task: BitwiseOperations02.c + settings: AutomizerC-forwardPredicates_const.epf + toolchain: AutomizerC.xml +- task: BitwiseOperations02.c + settings: AutomizerC-nestedInterpolants.epf + toolchain: AutomizerC.xml +- task: BitwiseOperations02.c + settings: AutomizerC-nestedInterpolants_const.epf + toolchain: AutomizerC.xml +- task: BitwiseOperations02.c + settings: BlockEncodingV2AutomizerC-forwardPredicates.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: BitwiseOperations02.c + settings: KojakC-Reach-32Bit-Default.epf + toolchain: KojakC.xml + +TIMEOUT: +- task: BitwiseOperations01.c + settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: BitwiseOperations02.c + settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: ShortCircuit-SideEffect-DoStatement-Safe.c + settings: AutomizerC-BitvectorTranslation.epf + toolchain: AutomizerC.xml +- task: ShortCircuit-SideEffect-ForStatement-Safe.c + settings: AutomizerC-BitvectorTranslation.epf + toolchain: AutomizerC.xml +- task: StructPositiveSum-Safe.c + settings: AutomizerC-BitvectorTranslation.epf + toolchain: AutomizerC.xml +- task: StructPositiveSum-Safe.c + settings: AutomizerC-forwardPredicates.epf + toolchain: AutomizerC.xml +- task: StructPositiveSum-Safe.c + settings: AutomizerC-forwardPredicates_const.epf + toolchain: AutomizerC.xml +- task: StructPositiveSum-Safe.c + settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: StructPositiveSum-Safe.c + settings: BlockEncodingV2AutomizerC-forwardPredicates.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: array10_pattern_simplified.c + settings: AutomizerC-BitvectorTranslation.epf + toolchain: AutomizerC.xml +- task: bitwiseOrUnsigned.c + settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf + toolchain: BlockEncodingV2AutomizerC.xml +- task: builtin_ffs.c + settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf + toolchain: BlockEncodingV2AutomizerC.xml + +unable to decide satisfiability of path constraint: +- task: array10_pattern_simplified.c + settings: AutomizerC-nestedInterpolants.epf + toolchain: AutomizerC.xml +- task: array10_pattern_simplified.c + settings: AutomizerC-nestedInterpolants_const.epf + toolchain: AutomizerC.xml diff --git a/trunk/examples/programs/regression/c/interprocedural/.testignore b/trunk/examples/programs/regression/c/interprocedural/.testignore new file mode 100644 index 00000000000..623f87ba48e --- /dev/null +++ b/trunk/examples/programs/regression/c/interprocedural/.testignore @@ -0,0 +1,10 @@ +TIMEOUT: +- task: Acsl01-EnsuresLocal-Safe.c + settings: AutomizerC-BitvectorTranslation.epf + toolchain: AutomizerC.xml +- task: Acsl03-EnsuresGlobal-Safe.c + settings: AutomizerC-BitvectorTranslation.epf + toolchain: AutomizerC.xml +- task: Tschingelhorn-Safe.c + settings: AutomizerC-BitvectorTranslation.epf + toolchain: AutomizerC.xml diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/UltimateTestCase.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/UltimateTestCase.java index f5e6e7ce22a..0effe6b2aa3 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/UltimateTestCase.java +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/UltimateTestCase.java @@ -38,6 +38,7 @@ import de.uni_freiburg.informatik.ultimate.test.decider.ITestResultDecider; import de.uni_freiburg.informatik.ultimate.test.decider.ITestResultDecider.TestResult; import de.uni_freiburg.informatik.ultimate.test.junitextension.testfactory.FactoryTestMethod; +import de.uni_freiburg.informatik.ultimate.test.junitextension.testfactory.FactoryTestRunner.SkipTestException; import de.uni_freiburg.informatik.ultimate.test.mocks.ConsoleLogger; import de.uni_freiburg.informatik.ultimate.test.reporting.IIncrementalLog; import de.uni_freiburg.informatik.ultimate.test.reporting.ITestLogfile; @@ -124,7 +125,7 @@ public void test() { final ILogger logger = getLoggerFromStarter(starter); logger.info("Deciding this test: " + deciderName); result = mDecider.getTestResult(starter.getServices()); - if (!returnCode.isOK() && result != TestResult.FAIL) { + if (!returnCode.isOK() && result != TestResult.FAIL && result != TestResult.IGNORE) { logger.fatal("#################### Overwriting decision of " + deciderName + " and setting test status to FAIL ####################"); logger.fatal("Ultimate returned an unexpected status:"); @@ -183,7 +184,12 @@ public void test() { } if (th != null) { message += " (Ultimate threw an Exception: " + th.getMessage() + ")"; + if (result == TestResult.IGNORE) { + skipTest(message, th); + } failTest(message, th); + } else if (result == TestResult.IGNORE) { + skipTest(message); } else { failTest(message); } @@ -266,6 +272,14 @@ private static void failTest(final String message, final Throwable th) throws Ul throw exception; } + private static void skipTest(final String message) { + throw new SkipTestException(message); + } + + private static void skipTest(final String message, final Throwable cause) { + throw new SkipTestException(message, cause); + } + @Override public int compareTo(final UltimateTestCase o) { return mUltimateRunDefinition.compareTo(o.mUltimateRunDefinition); diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ITestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ITestResultDecider.java index a564bc40151..e129c9f14b9 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ITestResultDecider.java +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ITestResultDecider.java @@ -128,6 +128,10 @@ public enum TestResult { /** * Success should always represent a JUnit test success. */ - SUCCESS + SUCCESS, + /** + * Marks a test as ignored + */ + IGNORE } } diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/SafetyCheckTestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/SafetyCheckTestResultDecider.java index f6245a295cb..1bcfa093b33 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/SafetyCheckTestResultDecider.java +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/SafetyCheckTestResultDecider.java @@ -28,6 +28,8 @@ package de.uni_freiburg.informatik.ultimate.test.decider; +import java.util.regex.Pattern; + import de.uni_freiburg.informatik.ultimate.core.lib.results.ExceptionOrErrorResult; import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition; import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.IExpectedResultFinder; @@ -38,8 +40,7 @@ import de.uni_freiburg.informatik.ultimate.test.util.TestUtil; /** - * Use keywords in filename and first line to decide correctness of safety - * checker results. + * Use keywords in filename and first line to decide correctness of safety checker results. * * @author heizmann@informatik.uni-freiburg.de * @author Daniel Dietsch (dietsch@informatik.uni-freiburg.de) @@ -50,19 +51,33 @@ public class SafetyCheckTestResultDecider extends ThreeTierTestResultDecider constructExpectedResultFinder() { - return new KeywordBasedExpectedResultFinder<>( - TestUtil.constructFilenameKeywordMap_AllSafetyChecker(), null, + return new KeywordBasedExpectedResultFinder<>(TestUtil.constructFilenameKeywordMap_AllSafetyChecker(), null, TestUtil.constructFirstlineKeywordMap_SafetyChecker()); } @@ -84,6 +99,19 @@ public class SafetyCheckerTestResultEvaluation implements ITestResultEvaluation< @Override public void evaluateTestResult(final IExpectedResultFinder expectedResultFinder, final IOverallResultEvaluator overallResultDeterminer) { + if (mOverridenExpectedVerdict != null) { + final SafetyCheckerOverallResult overallResult = overallResultDeterminer.getOverallResult(); + final String overallResultMsg = overallResultDeterminer.generateOverallResultMessage(); + final Pattern pattern = Pattern.compile(mOverridenExpectedVerdict, Pattern.CASE_INSENSITIVE); + if (pattern.matcher(overallResult.toString()) != null || pattern.matcher(overallResultMsg) != null) { + mTestResult = TestResult.IGNORE; + } else { + mTestResult = TestResult.FAIL; + } + mCategory = overallResult + " (Expected to match :" + mOverridenExpectedVerdict + ")"; + mMessage = " UltimateResult: " + overallResultMsg; + return; + } evaluateExpectedResult(expectedResultFinder); switch (expectedResultFinder.getExpectedResultFinderStatus()) { case ERROR: diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/TerminationAnalysisTestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/TerminationAnalysisTestResultDecider.java index be758501fe6..e76b822d0a1 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/TerminationAnalysisTestResultDecider.java +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/TerminationAnalysisTestResultDecider.java @@ -26,6 +26,8 @@ */ package de.uni_freiburg.informatik.ultimate.test.decider; +import java.util.regex.Pattern; + import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition; import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.IExpectedResultFinder; import de.uni_freiburg.informatik.ultimate.test.decider.expectedresult.KeywordBasedExpectedResultFinder; @@ -50,6 +52,11 @@ public TerminationAnalysisTestResultDecider( super(ultimateRunDefinition, unknownIsJUnitSuccess); } + public TerminationAnalysisTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, + final boolean unknownIsJUnitSuccess, final String overridenExpectedVerdict) { + super(ultimateRunDefinition, unknownIsJUnitSuccess, overridenExpectedVerdict); + } + @Override public IExpectedResultFinder constructExpectedResultFinder() { return new KeywordBasedExpectedResultFinder<>( @@ -79,6 +86,19 @@ public class TerminationAnalysisResultEvaluation implements ITestResultEvaluatio public void evaluateTestResult( final IExpectedResultFinder expectedResultFinder, final IOverallResultEvaluator overallResultDeterminer) { + if (mOverridenExpectedVerdict != null) { + final TerminationAnalysisOverallResult overallResult = overallResultDeterminer.getOverallResult(); + final String overallResultMsg = overallResultDeterminer.generateOverallResultMessage(); + final Pattern pattern = Pattern.compile(mOverridenExpectedVerdict, Pattern.CASE_INSENSITIVE); + if (pattern.matcher(overallResult.toString()) != null || pattern.matcher(overallResultMsg) != null) { + mTestResult = TestResult.IGNORE; + } else { + mTestResult = TestResult.FAIL; + } + mCategory = overallResult + " (Expected to match :" + mOverridenExpectedVerdict + ")"; + mMessage = " UltimateResult: " + overallResultMsg; + return; + } evaluateExpectedResult(expectedResultFinder); switch (expectedResultFinder.getExpectedResultFinderStatus()) { case ERROR: diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ThreeTierTestResultDecider.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ThreeTierTestResultDecider.java index a57530f01c4..e8770e5b78e 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ThreeTierTestResultDecider.java +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/decider/ThreeTierTestResultDecider.java @@ -59,6 +59,7 @@ public abstract class ThreeTierTestResultDecider implements ITes private final IExpectedResultFinder mExpectedResultEvaluation; private IOverallResultEvaluator mUltimateResultEvaluation; private ITestResultEvaluation mTestResultEvaluation; + protected final String mOverridenExpectedVerdict; /** * @@ -67,15 +68,32 @@ public abstract class ThreeTierTestResultDecider implements ITes * @param unknownIsJUnitSuccess * if true the TestResult UNKNOWN is a success for JUnit, if false, the TestResult UNKNOWN is a failure * for JUnit. + * + * @param overridenExpectedVerdict + * The expected verdict overridden in a separate file, null if not present. */ public ThreeTierTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, - final boolean unknownIsJUnitSuccess) { + final boolean unknownIsJUnitSuccess, final String overridenExpectedVerdict) { mUnknownIsJUnitSuccess = unknownIsJUnitSuccess; + mOverridenExpectedVerdict = overridenExpectedVerdict; mUltimateRunDefinition = ultimateRunDefinition; mExpectedResultEvaluation = constructExpectedResultFinder(); mExpectedResultEvaluation.findExpectedResult(ultimateRunDefinition); } + /** + * + * @param ultimateRunDefinition + * + * @param unknownIsJUnitSuccess + * if true the TestResult UNKNOWN is a success for JUnit, if false, the TestResult UNKNOWN is a failure + * for JUnit. + */ + public ThreeTierTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, + final boolean unknownIsJUnitSuccess) { + this(ultimateRunDefinition, unknownIsJUnitSuccess, null); + } + @Override public final TestResult getTestResult(final IUltimateServiceProvider services) { mUltimateResultEvaluation = constructUltimateResultEvaluation(); @@ -123,8 +141,10 @@ public boolean getJUnitSuccess(final TestResult testResult) { return mUnknownIsJUnitSuccess; case FAIL: return false; + case IGNORE: + return false; default: - throw new AssertionError("unknown actualResult"); + throw new AssertionError("unknown actualResult: " + testResult); } } diff --git a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/junitextension/testfactory/FactoryTestRunner.java b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/junitextension/testfactory/FactoryTestRunner.java index a8deda4a9b8..366949f2963 100644 --- a/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/junitextension/testfactory/FactoryTestRunner.java +++ b/trunk/source/Library-UltimateTest/src/de/uni_freiburg/informatik/ultimate/test/junitextension/testfactory/FactoryTestRunner.java @@ -47,7 +47,11 @@ import java.util.stream.Collector; import org.junit.AfterClass; +import org.junit.internal.AssumptionViolatedException; import org.junit.internal.runners.statements.RunAfters; +import org.junit.runner.Description; +import org.junit.runner.notification.Failure; +import org.junit.runner.notification.RunNotifier; import org.junit.runners.BlockJUnit4ClassRunner; import org.junit.runners.model.FrameworkMethod; import org.junit.runners.model.InitializationError; @@ -186,6 +190,54 @@ protected List computeTestMethods() { return mTests; } + @Override + protected void runChild(final FrameworkMethod method, final RunNotifier notifier) { + final Description description = describeChild(method); + if (isIgnored(method)) { + notifier.fireTestIgnored(description); + } else { + final Statement statement = new Statement() { + @Override + public void evaluate() throws Throwable { + methodBlock(method).evaluate(); + } + }; + myRunLeaf(method, description, notifier); + } + } + + protected final void myRunLeaf(final FrameworkMethod method, final Description description, + final RunNotifier notifier) { + notifier.fireTestStarted(description); + try { + methodBlock(method).evaluate(); + } catch (final AssumptionViolatedException e) { + notifier.fireTestAssumptionFailed(new Failure(description, e)); + } catch (final SkipTestException e) { + notifier.fireTestIgnored(description); + } catch (final Throwable e) { + notifier.fireTestFailure(new Failure(description, e)); + } finally { + notifier.fireTestFinished(description); + } + } + + public static class SkipTestException extends RuntimeException { + private static final long serialVersionUID = 1L; + + public SkipTestException() { + super(); + } + + public SkipTestException(final String message) { + super(message); + } + + public SkipTestException(final String message, final Throwable cause) { + super(message, cause); + } + } + @Override protected Object createTest() throws Exception { return mTestSuiteInstance; diff --git a/trunk/source/UltimateRegressionTest/META-INF/MANIFEST.MF b/trunk/source/UltimateRegressionTest/META-INF/MANIFEST.MF index b1d74518ecf..5094b7578c9 100644 --- a/trunk/source/UltimateRegressionTest/META-INF/MANIFEST.MF +++ b/trunk/source/UltimateRegressionTest/META-INF/MANIFEST.MF @@ -30,7 +30,8 @@ Require-Bundle: org.junit, de.uni_freiburg.informatik.ultimate.plugins.icfgtransformation, de.uni_freiburg.informatik.ultimate.lib.sifa, de.uni_freiburg.informatik.ultimate.plugins.sifa, - de.uni_freiburg.informatik.ultimate.plugins.generator.referee + de.uni_freiburg.informatik.ultimate.plugins.generator.referee, + org.yaml.snakeyaml Import-Package: de.uni_freiburg.informatik.ultimate.lib.pea, de.uni_freiburg.informatik.ultimate.lib.srparse, de.uni_freiburg.informatik.ultimate.lib.srparse.pattern, diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java index ef465d8905c..4ac5d6092bf 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/AbstractRegressionTestSuite.java @@ -27,17 +27,22 @@ package de.uni_freiburg.informatik.ultimate.regressiontest; import java.io.File; +import java.io.FileInputStream; +import java.io.FileNotFoundException; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; import java.util.Collections; import java.util.HashSet; import java.util.List; +import java.util.Map; import java.util.Set; import java.util.function.Predicate; import java.util.regex.Matcher; import java.util.stream.Collectors; +import org.yaml.snakeyaml.Yaml; + import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition; import de.uni_freiburg.informatik.ultimate.test.UltimateTestCase; import de.uni_freiburg.informatik.ultimate.test.UltimateTestSuite; @@ -48,6 +53,7 @@ import de.uni_freiburg.informatik.ultimate.test.reporting.IIncrementalLog; import de.uni_freiburg.informatik.ultimate.test.reporting.ITestSummary; import de.uni_freiburg.informatik.ultimate.test.util.TestUtil; +import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.NestedMap3; /** * An {@link AbstractRegressionTestSuite} is a {@link UltimateTestSuite} that automatically generates tests from folders @@ -62,6 +68,7 @@ public abstract class AbstractRegressionTestSuite extends UltimateTestSuite { private static final Predicate FILTER_XML = TestUtil.getFileEndingTest(".xml"); private static final Predicate FILTER_EPF = TestUtil.getFileEndingTest(".epf"); + private static final String SKIPPED_FILENAME = ".testignore"; protected long mTimeout; protected String mRootFolder; @@ -110,17 +117,51 @@ public Collection createTestCases() { final Predicate filesRegexFilter = getFilesRegexFilter(); for (final Config runConfiguration : runConfigurations) { final Collection inputFiles = getInputFiles(filesRegexFilter, runConfiguration); - + final NestedMap3 skippedTests = getSkippedTests(inputFiles); for (final File inputFile : inputFiles) { final UltimateRunDefinition urd = new UltimateRunDefinition(inputFile, runConfiguration.getSettingsFile(), runConfiguration.getToolchainFile(), getTimeout(runConfiguration, inputFile)); - rtr.add(buildTestCase(urd, getTestResultDecider(urd))); + final String overridenVerdict = skippedTests.get(inputFile, + runConfiguration.getSettingsFile().getName(), runConfiguration.getToolchainFile().getName()); + final ITestResultDecider decider = overridenVerdict == null ? getTestResultDecider(urd) + : getTestResultDecider(urd, overridenVerdict); + rtr.add(buildTestCase(urd, decider)); } } return rtr; } + /** + * Collect all tests that should be marked as skipped. To do so, all files with SKIPPED_FILENAME next to + * {@code inputFiles} are considered and a NestedMap3 is extracted from. + */ + private static NestedMap3 getSkippedTests(final Collection inputFiles) { + final NestedMap3 result = new NestedMap3<>(); + inputFiles.stream().map(x -> new File(x.getParentFile(), SKIPPED_FILENAME)).distinct() + .forEach(x -> addSkippedTest(x, result)); + return result; + } + + private static void addSkippedTest(final File ignoreFile, final NestedMap3 map) { + try { + final Map>> parsed = new Yaml().load(new FileInputStream(ignoreFile)); + for (final var entry : parsed.entrySet()) { + for (final Map triples : entry.getValue()) { + if (triples.values().stream().anyMatch(x -> x.contains("/"))) { + throw new UnsupportedOperationException("Invalid filename in ignore-file" + ignoreFile + + ". The filename may only contain a name, not a relative path. " + + "Add a new ignore-file next to the task itself (if desired)."); + } + map.put(new File(ignoreFile.getParentFile(), triples.get("task")), triples.get("settings"), + triples.get("toolchain"), entry.getKey()); + } + } + } catch (final FileNotFoundException e) { + // File does not exist, nothing to be ignored + } + } + protected long getTimeout(final Config rundef, final File file) { return mTimeout; } @@ -266,6 +307,11 @@ protected Collection getInputFiles(final Predicate regexFilter, fina protected abstract ITestResultDecider getTestResultDecider(UltimateRunDefinition runDefinition); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + throw new UnsupportedOperationException(getClass().getSimpleName() + " does not support skipping tests."); + } + public static final class Config extends de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair { diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java index 9911bef4a16..afee2f0b027 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ChcRegressionTestSuite.java @@ -51,14 +51,14 @@ public ChcRegressionTestSuite() { mTimeout = DEFAULT_TIMEOUT; mRootFolder = TestUtil.getPathFromTrunk("examples/smtlib/horn/regression"); -// // exclude paths that match the following regex -// mExcludeFilterRegex = + // // exclude paths that match the following regex + // mExcludeFilterRegex = mFiletypesToConsider = new String[] { ".smt2" }; } @Override protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition) { - boolean unknownIsSuccess = false; + final boolean unknownIsSuccess = false; return new ChcTestResultDecider(runDefinition, unknownIsSuccess); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/DataRaceRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/DataRaceRegressionTestSuite.java index 29547da85ac..9ee56f54f3f 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/DataRaceRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/DataRaceRegressionTestSuite.java @@ -26,16 +26,11 @@ */ package de.uni_freiburg.informatik.ultimate.regressiontest.generic; -import java.io.File; -import java.util.HashMap; -import java.util.Map; - import de.uni_freiburg.informatik.ultimate.regressiontest.AbstractRegressionTestSuite; import de.uni_freiburg.informatik.ultimate.test.UltimateRunDefinition; import de.uni_freiburg.informatik.ultimate.test.decider.ITestResultDecider; import de.uni_freiburg.informatik.ultimate.test.decider.SafetyCheckTestResultDecider; import de.uni_freiburg.informatik.ultimate.test.util.TestUtil; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; public class DataRaceRegressionTestSuite extends AbstractRegressionTestSuite { @@ -43,16 +38,11 @@ public class DataRaceRegressionTestSuite extends AbstractRegressionTestSuite { private static final String ROOT_DIR = TestUtil.getPathFromTrunk("examples/concurrent/pthreads/races"); private static final String FILE_ENDING = ".c"; - private final Map, Long> mSpecialTimeouts = new HashMap<>(); - public DataRaceRegressionTestSuite() { super(); mTimeout = TIMEOUT; mRootFolder = ROOT_DIR; mFiletypesToConsider = new String[] { FILE_ENDING }; - - mSpecialTimeouts.put(new Pair<>("DataRace-32bit-Automizer_Bitvector.epf", "static-array-copy3.c"), 250_000L); - mSpecialTimeouts.put(new Pair<>("DataRace-32bit-Automizer_Default.epf", "static-array-copy3.c"), 40_000L); } @Override @@ -61,12 +51,8 @@ protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition ru } @Override - protected long getTimeout(final Config config, final File file) { - final var pair = new Pair<>(config.getSettingsFile().getName(), file.getName()); - final var timeout = mSpecialTimeouts.get(pair); - if (timeout != null) { - return timeout; - } - return super.getTimeout(config, file); + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + return new SafetyCheckTestResultDecider(runDefinition, false, overridenExpectedVerdict); } } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/RegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/RegressionTestSuite.java index 0bcea8519e7..e8609420382 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/RegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/RegressionTestSuite.java @@ -58,4 +58,10 @@ protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition ru return new SafetyCheckTestResultDecider(runDefinition, false); } + @Override + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + return new SafetyCheckTestResultDecider(runDefinition, false, overridenExpectedVerdict); + } + } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java index d2026acec37..0613dd93d1b 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/ReqCheckerRedundancyRegressionTestSuite.java @@ -173,7 +173,8 @@ public boolean isSuccess(final ReqCheckerResult actual) { } return false; } - if ((mNoResults != -1 && actual.mNoResults != mNoResults) || DataStructureUtils.isDifferent(actual.mRedundant, mRedundant)) { + if ((mNoResults != -1 && actual.mNoResults != mNoResults) + || DataStructureUtils.isDifferent(actual.mRedundant, mRedundant)) { return false; } return true; diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/SignedIntegerOverflowRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/SignedIntegerOverflowRegressionTestSuite.java index d63f434fd8b..8dadef23f02 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/SignedIntegerOverflowRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/SignedIntegerOverflowRegressionTestSuite.java @@ -52,4 +52,10 @@ protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition ru return new SafetyCheckTestResultDecider(runDefinition, false); } + @Override + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + return new SafetyCheckTestResultDecider(runDefinition, false, overridenExpectedVerdict); + } + } diff --git a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/TerminationRegressionTestSuite.java b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/TerminationRegressionTestSuite.java index 7464ca629cf..8d7d383a8b2 100644 --- a/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/TerminationRegressionTestSuite.java +++ b/trunk/source/UltimateRegressionTest/src/de/uni_freiburg/informatik/ultimate/regressiontest/generic/TerminationRegressionTestSuite.java @@ -54,4 +54,10 @@ protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition ru return new TerminationAnalysisTestResultDecider(runDefinition, false); } + @Override + protected ITestResultDecider getTestResultDecider(final UltimateRunDefinition runDefinition, + final String overridenExpectedVerdict) { + return new TerminationAnalysisTestResultDecider(runDefinition, false, overridenExpectedVerdict); + } + }