Skip to content

Commit d883e5e

Browse files
wadoonwadoon
committed
Single files instead of one large files
1 parent 87ad062 commit d883e5e

38 files changed

+415
-530
lines changed

‎gradle/wrapper/gradle-wrapper.properties‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
distributionBase=GRADLE_USER_HOME
22
distributionPath=wrapper/dists
3-
distributionUrl=https\://services.gradle.org/distributions/gradle-8.12-bin.zip
3+
distributionUrl=https\://services.gradle.org/distributions/gradle-8.12.1-bin.zip
44
zipStoreBase=GRADLE_USER_HOME
55
zipStorePath=wrapper/dists

‎key.core/src/test/java/de/uka/ilkd/key/macros/scripts/TestProofScriptCommand.java‎

Lines changed: 27 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,13 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.macros.scripts;
55

6-
import java.io.FileNotFoundException;
6+
import java.io.File;
77
import java.io.IOException;
8-
import java.net.URI;
98
import java.net.URISyntaxException;
10-
import java.net.URL;
119
import java.nio.file.Files;
1210
import java.nio.file.Path;
13-
import java.util.Arrays;
11+
import java.nio.file.Paths;
12+
import java.util.ArrayList;
1413
import java.util.List;
1514

1615
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -33,32 +32,42 @@
3332
import static org.assertj.core.api.Assertions.assertThat;
3433
import static org.junit.jupiter.api.Assertions.assertTrue;
3534

36-
3735
/**
3836
* see {@link MasterHandlerTest} from where I copied quite a bit.
3937
*/
4038
public class TestProofScriptCommand {
41-
public record TestInstance(String name, String key, String script, String exception,
39+
public record TestInstance(String key, String script, String exception,
4240
String[] goals, Integer selectedGoal) {
4341
}
4442

45-
4643
public static List<Arguments> data() throws IOException, URISyntaxException {
47-
URL url = TestProofScriptCommand.class.getResource("cases.yml");
48-
if (url == null) {
49-
throw new FileNotFoundException("Cannot find resource 'cases'.");
44+
var folder = Paths.get("src/test/resources/de/uka/ilkd/key/macros/scripts");
45+
try (var walker = Files.walk(folder)) {
46+
List<Path> files =
47+
walker.filter(it -> it.getFileName().toString().endsWith(".yml")).toList();
48+
var objectMapper = new ObjectMapper(new YAMLFactory());
49+
objectMapper.findAndRegisterModules();
50+
51+
List<Arguments> args = new ArrayList(files.size());
52+
for (Path path : files) {
53+
try {
54+
TestInstance instance =
55+
objectMapper.readValue(path.toFile(), TestInstance.class);
56+
args.add(Arguments.of(path.toFile(), instance));
57+
} catch (Exception e) {
58+
System.out.println(path);
59+
e.printStackTrace();
60+
throw e;
61+
}
62+
}
63+
return args;
5064
}
51-
52-
var objectMapper = new ObjectMapper(new YAMLFactory());
53-
objectMapper.findAndRegisterModules();
54-
TestInstance[] instances = objectMapper.readValue(url, TestInstance[].class);
55-
return Arrays.stream(instances).map(Arguments::of).toList();
5665
}
5766

5867
@ParameterizedTest
5968
@MethodSource("data")
60-
void testProofScript(TestInstance data) throws Exception {
61-
var name = data.name();
69+
void testProofScript(File file, TestInstance data) throws Exception {
70+
var name = file.getName().replace(".yml", "");
6271
Path tmpKey = Files.createTempFile("proofscript_key_" + name, ".key");
6372
Files.writeString(tmpKey, data.key());
6473

@@ -67,7 +76,7 @@ void testProofScript(TestInstance data) throws Exception {
6776
Proof proof = env.getLoadedProof();
6877

6978
ProofScriptEngine pse = new ProofScriptEngine(data.script(),
70-
new Location(URI.create("file:/"+data.name), Position.newOneBased(1, 1)));
79+
new Location(file.toURI(), Position.newOneBased(1, 1)));
7180

7281
boolean hasException = data.exception() != null;
7382
try {

‎key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java‎

Lines changed: 79 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@
99
import java.nio.charset.StandardCharsets;
1010
import java.nio.file.Files;
1111
import java.nio.file.Path;
12+
import java.nio.file.Paths;
13+
import java.util.stream.Stream;
1214
import java.util.*;
1315

1416
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -25,14 +27,12 @@
2527

2628
import org.key_project.util.Streams;
2729

28-
import com.fasterxml.jackson.core.type.TypeReference;
2930
import com.fasterxml.jackson.databind.ObjectMapper;
3031
import com.fasterxml.jackson.dataformat.yaml.YAMLFactory;
32+
import org.junit.jupiter.api.TestFactory;
33+
import org.junit.jupiter.api.DynamicTest;
3134
import org.assertj.core.api.Assertions;
3235
import org.junit.jupiter.api.Assumptions;
33-
import org.junit.jupiter.params.ParameterizedTest;
34-
import org.junit.jupiter.params.provider.Arguments;
35-
import org.junit.jupiter.params.provider.MethodSource;
3636
import org.slf4j.Logger;
3737
import org.slf4j.LoggerFactory;
3838

@@ -48,10 +48,13 @@
4848
*/
4949
public class MasterHandlerTest {
5050
/**
51-
* If this variable is set when running this test class, then those cases with expected result
52-
* "weak_valid" will raise an exception unless they can be proved using the solver.
51+
* If this variable is set when running this test class, then those cases with
52+
* expected result
53+
* "weak_valid" will raise an exception unless they can be proved using the
54+
* solver.
5355
* <p>
54-
* Otherwise, a "timeout" or "unknown" is accepted. This can be used to deal with test cases
56+
* Otherwise, a "timeout" or "unknown" is accepted. This can be used to deal
57+
* with test cases
5558
* that
5659
* should verify but do not yet do so.
5760
* <p>
@@ -65,61 +68,82 @@ public class MasterHandlerTest {
6568
&& it.getName().equals("Z3 (Legacy Translation)"))
6669
.findFirst().orElse(null);
6770

68-
public static List<Arguments> data()
69-
throws IOException, URISyntaxException, ProblemLoaderException {
70-
try (var input = MasterHandlerTest.class.getResourceAsStream("cases.yml")) {
71-
var om = new ObjectMapper(new YAMLFactory());
72-
TypeReference<HashMap<String, TestData>> typeRef = new TypeReference<>() {
73-
};
74-
Map<String, TestData> preData = om.readValue(input, typeRef);
75-
var result = new ArrayList<Arguments>(preData.size());
76-
for (var entry : preData.entrySet()) {
77-
final var value = entry.getValue();
78-
79-
if (value.state == TestDataState.IGNORE) {
80-
LOGGER.info("Test {} case has been marked ignore", entry.getKey());
81-
continue;
82-
}
71+
private static List<LoadedTestData> data = null;
72+
73+
public static List<LoadedTestData> data() throws IOException, URISyntaxException, ProblemLoaderException {
74+
if (data != null)
75+
return data;
76+
77+
var om = new ObjectMapper(new YAMLFactory());
78+
var path = Paths.get("src/test/resources/de/uka/ilkd/key/smt/newsmt2/cases/");
79+
try (var walker = Files.walk(path)) {
80+
List<Path> files = walker.filter(it -> it.getFileName().toString().endsWith(".yml")).toList();
81+
data = new ArrayList<>(files.size());
82+
83+
for (Path pFile : files) {
84+
try {
85+
var file = pFile.toFile();
86+
87+
TestData value = om.readValue(file, TestData.class);
88+
89+
if (value.state == TestDataState.IGNORE) {
90+
LOGGER.info("Test {} case has been marked ignore", file);
91+
continue;
92+
}
93+
94+
System.err.println(pFile);
95+
final var testData = value.load(file.getName().replace(".yml", ""));
96+
data.add(testData);
8397

84-
final var testData = value.load(entry.getKey());
85-
result.add(Arguments.of(testData));
98+
} catch (Exception e) {
99+
e.printStackTrace();
100+
throw e;
101+
}
86102
}
87-
return result;
103+
System.out.println(data);
104+
return data;
88105
}
89106
}
90107

108+
/**
109+
* Describes the state of a test instance.
110+
*/
91111
public enum TestDataState {
92112
EMPTY, EXTENDED, IGNORE
93113
}
94114

115+
/**
116+
* Expected outcome of a test instance.
117+
*/
95118
public enum Expectation {
96119
VALID, FAIL, IRRELEVANT
97120
}
98121

99122
/**
100-
* This class contains the information about the test fixtures that is loaded via the YAML.
101-
* @param contains a list of strings that are expected in the SMT translation
123+
* This class contains the information about the test fixtures that is loaded
124+
* via the YAML.
125+
*
126+
* @param contains a list of strings that are expected in the SMT translation
102127
* @param smtSettings required key/values in the smt settings.
103-
* @param expected expected output of Z3
104-
* @param state state of the test
105-
* @param javaSrc path to necessary java sources
106-
* @param keySrc contents of the key file to be loaded.
128+
* @param expected expected output of Z3
129+
* @param state state of the test
130+
* @param javaSrc path to necessary java sources
131+
* @param keySrc contents of the key file to be loaded.
107132
*/
108133
public record TestData(List<String> contains,
109-
Properties smtSettings,
110-
Expectation expected,
111-
TestDataState state,
112-
String javaSrc,
113-
String keySrc
114-
) {
134+
Properties smtSettings,
135+
Expectation expected,
136+
TestDataState state,
137+
String javaSrc,
138+
String keySrc) {
115139

116140
private LoadedTestData load(String name) throws IOException, ProblemLoaderException {
117141
var keySrc = keySrc();
118142
if (javaSrc != null && !javaSrc.isEmpty()) {
119143
Path srcDir = Files.createTempDirectory("SMT_key_" + name);
120144
Path tmpSrc = srcDir.resolve("src.java");
121145
Files.writeString(tmpSrc, javaSrc);
122-
keySrc += "\n\\javaSource \"%s\";\n".formatted(srcDir);
146+
keySrc += "\n/javaSource \"%s\";\n".formatted(srcDir);
123147
}
124148

125149
Path tmpKey = Files.createTempFile("SMT_key_%s".formatted(name), ".key");
@@ -140,6 +164,7 @@ private LoadedTestData load(String name) throws IOException, ProblemLoaderExcept
140164

141165
ModularSMTLib2Translator translator = new ModularSMTLib2Translator();
142166
var translation = translator.translateProblem(sequent, env.getServices(), settings).toString();
167+
env.dispose();
143168
return new LoadedTestData(name, this, translation);
144169
}
145170
}
@@ -151,8 +176,12 @@ public String toString() {
151176
}
152177
}
153178

154-
@ParameterizedTest
155-
@MethodSource("data")
179+
@TestFactory
180+
Stream<DynamicTest> testTranslation() throws Exception {
181+
return data().stream()
182+
.map(it -> DynamicTest.dynamicTest(it.name, () -> testTranslation(it)));
183+
}
184+
156185
void testTranslation(LoadedTestData data) throws Exception {
157186
if (DUMP_SMT) {
158187
Path tmpSmt = Files.createTempFile("SMT_key_%s".formatted(data.name), ".smt2");
@@ -164,13 +193,16 @@ void testTranslation(LoadedTestData data) throws Exception {
164193
.containsIgnoringWhitespaces(data.data.contains().toArray(new String[0]));
165194
}
166195

196+
@TestFactory
197+
Stream<DynamicTest> testZ3() throws Exception {
198+
return data().stream()
199+
.map(it -> DynamicTest.dynamicTest(it.name, () -> testZ3(it)));
200+
}
167201

168-
@ParameterizedTest
169-
@MethodSource("data")
170202
void testZ3(LoadedTestData data) throws Exception {
171203
Assumptions.assumeTrue(Z3_SOLVER != null);
172204
Assumptions.assumeTrue(Z3_SOLVER.isInstalled(false),
173-
"Z3 is not installed, this testcase is ignored.");
205+
"Z3 is not installed, this testcase is ignored.");
174206

175207
var expectation = data.data.expected;
176208
Assumptions.assumeTrue(expectation != null, "No Z3 expectation.");
@@ -187,9 +219,9 @@ void testZ3(LoadedTestData data) throws Exception {
187219

188220
try {
189221
String lookFor = switch (expectation) {
190-
case VALID -> "unsat";
191-
case FAIL -> "(sat|timeout)";
192-
case IRRELEVANT -> null;
222+
case VALID -> "unsat";
223+
case FAIL -> "(sat|timeout)";
224+
case IRRELEVANT -> null;
193225
};
194226

195227
if (lookFor != null) {
@@ -205,7 +237,7 @@ void testZ3(LoadedTestData data) throws Exception {
205237

206238
if (!STRICT_TEST) {
207239
assumeFalse(data.data.state == TestDataState.EXTENDED,
208-
"This is an extended test (will be run only in strict mode)");
240+
"This is an extended test (will be run only in strict mode)");
209241
}
210242

211243
if (lookFor != null) {

‎key.core/src/test/resources/de/uka/ilkd/key/macros/scripts/andRight.yml‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
key: |
2+
\predicates { a; b; }
3+
\problem { a & b }
4+
script: |
5+
rule andRight;
6+
goals:
7+
- ==> b
8+
- ==> a

0 commit comments

Comments
 (0)