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 <[email protected]>

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

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

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

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

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

trunk/examples/programs/quantifier/regression/bpl/.testignore

@@ -0,0 +1,4 @@
+overapproximation:
+- task: AuxVarInCall.bpl
+  settings: AutomizerBpl-forwardPredicates.epf
+  toolchain: AutomizerBpl.xml

trunk/examples/programs/regression/bpl/.testignore

@@ -0,0 +1,4 @@
+TIMEOUT:
+- task: nestedWhileSimple-Safe.bpl
+  settings: PdrAutomizerBpl.epf
+  toolchain: PdrAutomizerBpl.xml

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

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

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

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

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);

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
 	}
 }

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 [email protected]
  * @author Daniel Dietsch ([email protected])
@@ -50,19 +51,33 @@ public class SafetyCheckTestResultDecider extends ThreeTierTestResultDecider<Saf
 	/**
 	 *
 	 * @param ultimateRunDefinition
+	 * @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 SafetyCheckTestResultDecider(final UltimateRunDefinition ultimateRunDefinition,
+			final boolean unknownIsJUnitSuccess, final String overridenExpectedVerdict) {
+		super(ultimateRunDefinition, unknownIsJUnitSuccess, overridenExpectedVerdict);
+	}
+
+	/**
 	 *
+	 * @param ultimateRunDefinition
 	 * @param unknownIsJUnitSuccess
-	 *            if true the TestResult UNKNOWN is a success for JUnit, if
-	 *            false, the TestResult UNKNOWN is a failure for JUnit.
+	 *            if true the TestResult UNKNOWN is a success for JUnit, if false, the TestResult UNKNOWN is a failure
+	 *            for JUnit.
 	 */
-	public SafetyCheckTestResultDecider(final UltimateRunDefinition ultimateRunDefinition, final boolean unknownIsJUnitSuccess) {
+	public SafetyCheckTestResultDecider(final UltimateRunDefinition ultimateRunDefinition,
+			final boolean unknownIsJUnitSuccess) {
 		super(ultimateRunDefinition, unknownIsJUnitSuccess);
 	}
 
 	@Override
 	public IExpectedResultFinder<SafetyCheckerOverallResult> 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<SafetyCheckerOverallResult> expectedResultFinder,
 				final IOverallResultEvaluator<SafetyCheckerOverallResult> 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: