From 362adb780b8a80cc4cbd30d6fa9442000cedbf23 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frank=20Sch=C3=BCssele?= Date: Tue, 20 Aug 2024 15:59:01 +0200 Subject: [PATCH] Only allow skip files next to the tests itself --- .../regression/c/{ => noMathSAT}/skip.yml | 0 .../examples/programs/regression/bpl/skip.yml | 9 ----- .../regression/bpl/toolDirectives/skip.yml | 8 +++++ .../regression/c/interprocedural/skip.yml | 10 ++++++ trunk/examples/programs/regression/c/skip.yml | 9 ----- .../AbstractRegressionTestSuite.java | 35 ++++++++++--------- 6 files changed, 36 insertions(+), 35 deletions(-) rename trunk/examples/programs/FloatingPoint/regression/c/{ => noMathSAT}/skip.yml (100%) create mode 100644 trunk/examples/programs/regression/bpl/toolDirectives/skip.yml create mode 100644 trunk/examples/programs/regression/c/interprocedural/skip.yml diff --git a/trunk/examples/programs/FloatingPoint/regression/c/skip.yml b/trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/skip.yml similarity index 100% rename from trunk/examples/programs/FloatingPoint/regression/c/skip.yml rename to trunk/examples/programs/FloatingPoint/regression/c/noMathSAT/skip.yml diff --git a/trunk/examples/programs/regression/bpl/skip.yml b/trunk/examples/programs/regression/bpl/skip.yml index 031a706355e..b241000ef13 100644 --- a/trunk/examples/programs/regression/bpl/skip.yml +++ b/trunk/examples/programs/regression/bpl/skip.yml @@ -34,12 +34,3 @@ unknown symbol (@diff: - task: BugLiveVariables04-Safe.bpl settings: AutomizerBpl-nestedInterpolants.epf toolchain: AutomizerBpl.xml - -# 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 diff --git a/trunk/examples/programs/regression/bpl/toolDirectives/skip.yml b/trunk/examples/programs/regression/bpl/toolDirectives/skip.yml new file mode 100644 index 00000000000..d79a7d11335 --- /dev/null +++ b/trunk/examples/programs/regression/bpl/toolDirectives/skip.yml @@ -0,0 +1,8 @@ +# 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 diff --git a/trunk/examples/programs/regression/c/interprocedural/skip.yml b/trunk/examples/programs/regression/c/interprocedural/skip.yml new file mode 100644 index 00000000000..78b3932a404 --- /dev/null +++ b/trunk/examples/programs/regression/c/interprocedural/skip.yml @@ -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 \ No newline at end of file diff --git a/trunk/examples/programs/regression/c/skip.yml b/trunk/examples/programs/regression/c/skip.yml index 463e0fba225..9f91edc0a51 100644 --- a/trunk/examples/programs/regression/c/skip.yml +++ b/trunk/examples/programs/regression/c/skip.yml @@ -116,15 +116,6 @@ TIMEOUT: - task: builtin_ffs.c settings: BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf toolchain: BlockEncodingV2AutomizerC.xml -- 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 unable to decide satisfiability of path constraint: - task: array10_pattern_simplified.c 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 84e85b801dd..f232fbfb590 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 @@ -117,12 +117,12 @@ public Collection createTestCases() { final Predicate filesRegexFilter = getFilesRegexFilter(); for (final Config runConfiguration : runConfigurations) { final Collection inputFiles = getInputFiles(filesRegexFilter, runConfiguration); - final NestedMap3 skippedTests = getSkippedTests(runConfiguration); + final NestedMap3 skippedTests = getSkippedTests(inputFiles); for (final File inputFile : inputFiles) { final UltimateRunDefinition urd = new UltimateRunDefinition(inputFile, runConfiguration.getSettingsFile(), runConfiguration.getToolchainFile(), getTimeout(runConfiguration, inputFile)); - final String overridenVerdict = skippedTests.get(inputFile.getName(), + final String overridenVerdict = skippedTests.get(inputFile, runConfiguration.getSettingsFile().getName(), runConfiguration.getToolchainFile().getName()); rtr.add(buildTestCase(urd, getTestResultDecider(urd, overridenVerdict))); } @@ -130,28 +130,29 @@ public Collection createTestCases() { return rtr; } - private static NestedMap3 getSkippedTests(final Config runConfiguration) { - final NestedMap3 result = new NestedMap3<>(); - final File settingsDir = runConfiguration.getSettingsFile().getParentFile(); - final File toolchainDir = runConfiguration.getToolchainFile().getParentFile(); - if (settingsDir.equals(toolchainDir)) { - addSkippedTest(new File(settingsDir, SKIPPED_FILENAME), result); - } else if (settingsDir.toString().length() < toolchainDir.toString().length()) { - addSkippedTest(new File(settingsDir, SKIPPED_FILENAME), result); - addSkippedTest(new File(toolchainDir, SKIPPED_FILENAME), result); - } else { - addSkippedTest(new File(toolchainDir, SKIPPED_FILENAME), result); - addSkippedTest(new File(settingsDir, SKIPPED_FILENAME), result); - } + /** + * 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) { + 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()) { - map.put(triples.get("task"), triples.get("settings"), triples.get("toolchain"), entry.getKey()); + 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) {