Skip to content

Commit 8fb9091

Browse files
wadoonwadoon
committed
use YAML for test fixture
1 parent 16e5728 commit 8fb9091

34 files changed

+443
-839
lines changed

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

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

6-
import java.io.BufferedReader;
76
import java.io.FileNotFoundException;
87
import java.io.IOException;
98
import java.net.URISyntaxException;
109
import java.net.URL;
1110
import java.nio.file.Files;
1211
import java.nio.file.Path;
13-
import java.nio.file.Paths;
14-
import java.util.ArrayList;
1512
import java.util.Arrays;
1613
import java.util.List;
17-
import java.util.stream.Collectors;
1814

1915
import com.fasterxml.jackson.databind.ObjectMapper;
2016
import com.fasterxml.jackson.dataformat.yaml.YAMLFactory;
@@ -24,7 +20,6 @@
2420
import de.uka.ilkd.key.proof.Goal;
2521
import de.uka.ilkd.key.proof.Proof;
2622
import de.uka.ilkd.key.smt.newsmt2.MasterHandlerTest;
27-
import de.uka.ilkd.key.util.LineProperties;
2823

2924
import org.key_project.util.collection.ImmutableList;
3025

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

Lines changed: 69 additions & 119 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.smt.newsmt2;
55

6+
import com.fasterxml.jackson.core.type.TypeReference;
67
import com.fasterxml.jackson.databind.ObjectMapper;
78
import com.fasterxml.jackson.dataformat.yaml.YAMLFactory;
8-
import com.fasterxml.jackson.dataformat.yaml.YAMLGenerator;
99
import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
1010
import de.uka.ilkd.key.control.KeYEnvironment;
1111
import de.uka.ilkd.key.logic.Sequent;
@@ -17,9 +17,7 @@
1717
import de.uka.ilkd.key.smt.solvertypes.SolverType;
1818
import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation;
1919
import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
20-
import de.uka.ilkd.key.util.LineProperties;
21-
import org.jspecify.annotations.Nullable;
22-
import org.junit.jupiter.api.Assertions;
20+
import org.assertj.core.api.Assertions;
2321
import org.junit.jupiter.api.Assumptions;
2422
import org.junit.jupiter.params.ParameterizedTest;
2523
import org.junit.jupiter.params.provider.Arguments;
@@ -28,20 +26,14 @@
2826
import org.slf4j.Logger;
2927
import org.slf4j.LoggerFactory;
3028

31-
import java.io.*;
29+
import java.io.IOException;
30+
import java.io.OutputStream;
3231
import java.net.URISyntaxException;
33-
import java.net.URL;
3432
import java.nio.charset.StandardCharsets;
3533
import java.nio.file.Files;
3634
import java.nio.file.Path;
37-
import java.nio.file.Paths;
38-
import java.util.ArrayList;
39-
import java.util.HashMap;
40-
import java.util.List;
41-
import java.util.Properties;
42-
import java.util.stream.Collectors;
35+
import java.util.*;
4336

44-
import static org.junit.jupiter.api.Assertions.assertTrue;
4537
import static org.junit.jupiter.api.Assertions.fail;
4638
import static org.junit.jupiter.api.Assumptions.assumeFalse;
4739

@@ -73,74 +65,63 @@ public class MasterHandlerTest {
7365

7466
public static List<Arguments> data()
7567
throws IOException, URISyntaxException, ProblemLoaderException {
76-
URL url = MasterHandlerTest.class.getResource("cases");
77-
if (url == null) {
78-
throw new FileNotFoundException("Cannot find resource 'cases'.");
79-
}
80-
81-
if (!url.getProtocol().equals("file")) {
82-
throw new IOException("Resource should be a file URL not " + url);
83-
}
84-
85-
Path directory = Paths.get(url.toURI());
86-
Assertions.assertTrue(Files.isDirectory(directory));
87-
88-
List<Path> files;
89-
try (var s = Files.list(directory)) {
90-
files = s.collect(Collectors.toList());
91-
}
92-
List<Arguments> result = new ArrayList<>(files.size());
93-
var td = new HashMap<String,TestData>();
94-
for (Path file : files) {
95-
try {
96-
final var testData = TestData.create(file);
97-
if (testData != null) {
98-
td.put(file.getFileName().toString(), testData);
99-
result.add(Arguments.of(testData));
68+
try (var input = MasterHandlerTest.class.getResourceAsStream("cases.yml")) {
69+
var om = new ObjectMapper(new YAMLFactory());
70+
TypeReference<HashMap<String, TestData>> typeRef = new TypeReference<>() {
71+
};
72+
Map<String, TestData> preData = om.readValue(input, typeRef);
73+
var result = new ArrayList<Arguments>(preData.size());
74+
for (var entry : preData.entrySet()) {
75+
final var value = entry.getValue();
76+
77+
if (value.state == TestDataState.IGNORE) {
78+
LOGGER.info("Test {} case has been marked ignore", entry.getKey());
79+
continue;
10080
}
101-
} catch (Exception e) {
102-
LOGGER.error("Error reading {}", file, e);
103-
// make sure faulty test cases fail
104-
throw e;
81+
82+
final var testData = value.load(entry.getKey());
83+
result.add(Arguments.of(testData));
10584
}
85+
return result;
10686
}
87+
}
10788

89+
public enum TestDataState {
90+
EMPTY, EXTENDED, IGNORE
91+
}
10892

109-
var om = new ObjectMapper(
110-
new YAMLFactory().enable(YAMLGenerator.Feature.LITERAL_BLOCK_STYLE));
111-
om.writeValue(System.out, td);
112-
return result;
93+
public enum Expectation {
94+
VALID, FAIL, IRRELEVANT
11395
}
11496

115-
public record TestData(String name, Path path,
116-
List<String> contains,
97+
/**
98+
* This class contains the information about the test fixtures that is loaded via the YAML.
99+
* @param contains a list of strings that are expected in the SMT translation
100+
* @param smtSettings required key/values in the smt settings.
101+
* @param expected expected output of Z3
102+
* @param state state of the test
103+
* @param javaSrc path to necessary java sources
104+
* @param keySrc contents of the key file to be loaded.
105+
*/
106+
public record TestData(List<String> contains,
117107
Properties smtSettings,
118-
String expected, String state, String translation) {
119-
120-
public static @Nullable TestData create(Path path) throws IOException, ProblemLoaderException {
121-
var name = path.getFileName().toString();
122-
var props = new LineProperties();
123-
try (BufferedReader reader = Files.newBufferedReader(path)) {
124-
props.read(reader);
125-
}
126-
127-
if ("ignore".equals(props.get("state"))) {
128-
LOGGER.info("Test case has been marked ignore");
129-
return null;
130-
}
131-
132-
List<String> sources = props.getLines("sources");
133-
List<String> lines = new ArrayList<>(props.getLines("KeY"));
134-
135-
if (!sources.isEmpty()) {
108+
Expectation expected,
109+
TestDataState state,
110+
String javaSrc,
111+
String keySrc
112+
) {
113+
114+
private LoadedTestData load(String name) throws IOException, ProblemLoaderException {
115+
var keySrc = keySrc();
116+
if (javaSrc != null && !javaSrc.isEmpty()) {
136117
Path srcDir = Files.createTempDirectory("SMT_key_" + name);
137118
Path tmpSrc = srcDir.resolve("src.java");
138-
Files.write(tmpSrc, sources);
139-
lines.add(0, "\\javaSource \"" + srcDir + "\";\n");
119+
Files.writeString(tmpSrc, javaSrc);
120+
keySrc += "\n\\javaSource \"%s\";\n".formatted(srcDir);
140121
}
141122

142-
Path tmpKey = Files.createTempFile("SMT_key_" + name, ".key");
143-
Files.write(tmpKey, lines);
123+
Path tmpKey = Files.createTempFile("SMT_key_%s".formatted(name), ".key");
124+
Files.writeString(tmpKey, keySrc);
144125

145126
KeYEnvironment<DefaultUserInterfaceControl> env = KeYEnvironment.load(tmpKey.toFile());
146127

@@ -151,73 +132,46 @@ public record TestData(String name, Path path,
151132
ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings(),
152133
proof.getSettings().getNewSMTSettings(), proof);
153134

154-
String updates = props.get("smt-settings");
155-
Properties smtSettings = null;
156-
if (updates != null) {
157-
Properties map = new Properties();
158-
map.load(new StringReader(updates));
159-
smtSettings = map;
160-
settings.getNewSettings().readSettings(map);
135+
if (smtSettings != null) {
136+
settings.getNewSettings().readSettings(smtSettings);
161137
}
162138

163139
ModularSMTLib2Translator translator = new ModularSMTLib2Translator();
164-
var translation =
165-
translator.translateProblem(sequent, env.getServices(), settings).toString();
166-
167-
var contains = new ArrayList<String>(4);
168-
int i = 1;
169-
while (props.containsKey("contains." + i)) {
170-
contains.add(props.get("contains." + i).trim());
171-
i++;
172-
}
173-
174-
var expectation = props.get("expected");
175-
var state = props.get("state");
176-
return new TestData(name, path, contains, smtSettings,expectation,state, translation);
140+
var translation = translator.translateProblem(sequent, env.getServices(), settings).toString();
141+
return new LoadedTestData(name, this, translation);
177142
}
143+
}
178144

145+
private record LoadedTestData(String name, TestData data, String translation) {
179146
@Override
180147
public String toString() {
181-
return name;
148+
return name();
182149
}
183150
}
184151

185152
@ParameterizedTest
186153
@MethodSource("data")
187-
public void testTranslation(TestData data) throws Exception {
154+
void testTranslation(LoadedTestData data) throws Exception {
188155
if (DUMP_SMT) {
189-
Path tmpSmt = Files.createTempFile("SMT_key_" + data.name, ".smt2");
156+
Path tmpSmt = Files.createTempFile("SMT_key_%s".formatted(data.name), ".smt2");
190157
Files.writeString(tmpSmt, data.translation);
191158
LOGGER.info("SMT2 for {} saved in: {}", data.name, tmpSmt);
192159
}
193160

194-
int i = 1;
195-
while (1!=2/*data.props.containsKey("contains." + i)*/) {
196-
assertTrue(
197-
true,//containsModuloSpaces(data.translation, data.props.get("contains." + i).trim()),
198-
"Occurrence check for contains." + i);
199-
i++;
200-
}
201-
202-
}
203-
204-
public static boolean containsModuloSpaces(String haystack, String needle) {
205-
String n = needle.replaceAll("\\s+", " ");
206-
String h = haystack.replaceAll("\\s+", " ");
207-
return h.contains(n);
161+
Assertions.assertThat(data.translation)
162+
.containsIgnoringWhitespaces(data.data.contains().toArray(new String[0]));
208163
}
209164

210165

211166
@ParameterizedTest
212167
@MethodSource("data")
213-
public void testZ3(TestData data) throws Exception {
168+
void testZ3(LoadedTestData data) throws Exception {
214169
Assumptions.assumeTrue(Z3_SOLVER != null);
215170
Assumptions.assumeTrue(Z3_SOLVER.isInstalled(false),
216171
"Z3 is not installed, this testcase is ignored.");
217172

218-
String expectation = data.expected;
173+
var expectation = data.data.expected;
219174
Assumptions.assumeTrue(expectation != null, "No Z3 expectation.");
220-
expectation = expectation.toLowerCase().trim();
221175

222176
// TODO Run Z3 on the SMT translation
223177
// FIXME This is a hack.
@@ -230,14 +184,11 @@ public void testZ3(TestData data) throws Exception {
230184
String[] response = Streams.toString(proc.getInputStream()).split(System.lineSeparator());
231185

232186
try {
233-
String lookFor = null;
234-
switch (expectation) {
235-
case "valid" -> lookFor = "unsat";
236-
case "fail" -> lookFor = "(sat|timeout)";
237-
case "irrelevant" -> {
238-
}
239-
default -> fail("Unexpected expectation: " + expectation);
240-
}
187+
String lookFor = switch (expectation) {
188+
case VALID -> "unsat";
189+
case FAIL -> "(sat|timeout)";
190+
case IRRELEVANT -> null;
191+
};
241192

242193
if (lookFor != null) {
243194
for (String line : response) {
@@ -251,7 +202,7 @@ public void testZ3(TestData data) throws Exception {
251202
}
252203

253204
if (!STRICT_TEST) {
254-
assumeFalse(false, //"extended".equals(data.props.get("state")),
205+
assumeFalse(data.data.state == TestDataState.EXTENDED,
255206
"This is an extended test (will be run only in strict mode)");
256207
}
257208

@@ -264,5 +215,4 @@ public void testZ3(TestData data) throws Exception {
264215
throw t;
265216
}
266217
}
267-
268218
}

0 commit comments

Comments
 (0)