Skip to content

Commit 4603f13

Browse files
wadoonwadoon
committed
restoring the KeY book example
1 parent 98f5508 commit 4603f13

33 files changed

+504
-435
lines changed

‎key.core.testgen/build.gradle‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,7 @@ description = "Test Case Generation based on proof attempts."
33
dependencies {
44
implementation project(":key.core")
55
implementation("com.squareup:javapoet:1.13.0")
6+
7+
implementation "info.picocli:picocli:4.7.5"
68
}
9+

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Format.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,5 +4,5 @@
44
package de.uka.ilkd.key.testgen;
55

66
public enum Format {
7-
Plain, JUnit4, JUnit5, TestNG,
7+
JUnit4, JUnit5
88
}

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,8 @@ public KeYJavaType getTypeOfClassUnderTest() {
9494

9595
@Nullable
9696
public KeYJavaType getReturnType() {
97-
return getMUT().getType();
97+
var mut = getMUT();
98+
return mut != null ? mut.getType() : null;
9899
}
99100

100101
public Contract getContract() {

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/RefEx.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,8 @@ public record RefEx(@Nullable String rcObjType, String rcObj, String fieldType,
1717
@Override
1818
public String toString() {
1919
if (rcObjType != null && !rcObjType.isEmpty()) {
20-
return "((" + rcObjType + ")" + rcObj + ")." + field;
20+
return "((%s)%s).%s".formatted(rcObjType, rcObj, field);
2121
}
22-
return rcObj + "." + field;
22+
return "%s.%s".formatted(rcObj, field);
2323
}
2424
}

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java‎

Lines changed: 91 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -3,65 +3,129 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.testgen;
55

6+
import de.uka.ilkd.key.api.ProofManagementApi;
67
import de.uka.ilkd.key.control.KeYEnvironment;
78
import de.uka.ilkd.key.proof.Proof;
89
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
910
import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
11+
import de.uka.ilkd.key.speclang.Contract;
1012
import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
11-
import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLog;
13+
import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLogger;
1214
import org.slf4j.Logger;
1315
import org.slf4j.LoggerFactory;
16+
import picocli.CommandLine;
1417

1518
import java.io.File;
16-
import java.util.Objects;
19+
import java.util.ArrayList;
20+
import java.util.LinkedList;
21+
import java.util.List;
22+
import java.util.concurrent.Callable;
1723

18-
public class TGMain {
24+
@CommandLine.Command(name = "tcgen", mixinStandardHelpOptions = true,
25+
description = "Generator of Testcases based on Proof Attempts")
26+
public class TGMain implements Callable<Integer> {
1927
private final static Logger LOGGER = LoggerFactory.getLogger("main");
2028

2129
public static void main(String[] args) throws ProblemLoaderException, InterruptedException {
30+
int exitCode = new CommandLine(new TGMain()).execute(args);
31+
System.exit(exitCode);
32+
}
33+
34+
@CommandLine.Parameters(description = "KeY or Java file.", arity = "1..*")
35+
private List<File> files = new LinkedList<>();
36+
37+
@CommandLine.Option(names = {"-s", "--symbex"},
38+
description = "apply symbex", negatable = true)
39+
private boolean symbex;
40+
41+
@CommandLine.Option(names = {"-c", "--contract"},
42+
arity = "*",
43+
description = "name of the contract to be loaded in the Java environment")
44+
private List<String> contractNames = new ArrayList<>();
45+
46+
@CommandLine.Option(names = {"--all-contracts"},
47+
description = "name of the contract to be loaded in the Java environment")
48+
private boolean allContracts = false;
49+
50+
51+
@CommandLine.Option(names = {"-o", "--output"}, description = "Output folder")
52+
private File outputFolder = new File("out");
53+
54+
@CommandLine.Option(names = {"-r", "--rfl"}, description = "Use Reflection class", negatable = true)
55+
private boolean useReflection = false;
56+
57+
@CommandLine.Option(names = {"-f", "--format"}, description = "Use Reflection class")
58+
private Format format = Format.JUnit4;
59+
60+
61+
@CommandLine.Option(names = {"--max-unwinds"}, description = "max unwinds")
62+
private int maxUnwinds = 10;
63+
@CommandLine.Option(names = {"--dups"}, description = "remove duplicates", negatable = true)
64+
private boolean removeDuplicates;
65+
66+
@Override
67+
public Integer call() throws Exception {
2268
if (SolverTypes.Z3_CE_SOLVER.checkForSupport()) {
2369
LOGGER.error("Z3 not found! Bye.");
24-
System.exit(1);
25-
return;
70+
return 1;
2671
} else {
2772
LOGGER.info("Z3 found; Version {}", SolverTypes.Z3_CE_SOLVER.getInstalledVersion());
2873
}
2974

30-
3175
var settings = new TestGenerationSettings();
32-
String fileName = null;
33-
for (int i = 0; i < args.length; i++) {
34-
var a = args[i];
35-
if (a.startsWith("--")) {
36-
switch (a) {
37-
case "--output" -> settings.setOutputPath(args[++i]);
38-
case "--rfl" -> settings.setRFL(true);
39-
case "--format" -> settings.setFormat(Format.valueOf(args[++i]));
76+
TestGenerationLogger log = new SysoutTestGenerationLogger();
77+
settings.setOutputPath(outputFolder.getAbsolutePath());
78+
settings.setRFL(useReflection);
79+
settings.setFormat(format);
80+
settings.setApplySymbolicExecution(symbex);
81+
settings.setMaxUnwinds(maxUnwinds);
82+
settings.setRemoveDuplicates(removeDuplicates);
83+
84+
for (File file : files) {
85+
List<Proof> proofs = new LinkedList<>();
86+
var env = KeYEnvironment.load(file);
87+
Proof proof = env.getLoadedProof();
88+
if (proof == null) { // non-key file
89+
var print = contractNames.isEmpty();
90+
final var api = new ProofManagementApi(env);
91+
var contracts = api.getProofContracts();
92+
for (Contract contract : contracts) {
93+
final var name = contract.getName();
94+
if (print) {
95+
LOGGER.info("Contract found: {}", name);
96+
}
97+
98+
if (allContracts || contractNames.contains(name)) {
99+
proofs.add(api.startProof(contract).getProof());
100+
}
40101
}
41-
} else {
42-
fileName = a;
102+
} else { // key file
103+
proofs = List.of(proof);
104+
}
105+
106+
for (Proof p : proofs) {
107+
TestgenFacade.generateTestcases(env, p, settings, log);
108+
p.dispose();
43109
}
44-
}
45110

46-
var env = KeYEnvironment.load(new File(Objects.requireNonNull(fileName)));
47-
TestGenerationLog log = new SysoutTestGenerationLog();
48-
Proof proof = env.getLoadedProof();
49-
TestgenFacade.generateTestcases(env, proof, settings, log);
111+
env.dispose();
112+
}
113+
return 0;
50114
}
51115

52-
private static class SysoutTestGenerationLog implements TestGenerationLog {
116+
private static class SysoutTestGenerationLogger implements TestGenerationLogger {
53117
@Override
54-
public void writeln(String string) {
55-
LOGGER.info(string);
118+
public void writeln(String message) {
119+
LOGGER.info(message);
56120
}
57121

58122
@Override
59-
public void writeException(Throwable t) {
60-
LOGGER.error("Error occurred!", t);
123+
public void writeException(Throwable throwable) {
124+
LOGGER.error("Error occurred!", throwable);
61125
}
62126

63127
@Override
64-
public void testGenerationCompleted() {
128+
public void close() {
65129
}
66130
}
67131
}

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java‎

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -31,13 +31,15 @@
3131
import de.uka.ilkd.key.testgen.oracle.OracleGenerator;
3232
import de.uka.ilkd.key.testgen.oracle.OracleMethodCall;
3333
import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
34-
import de.uka.ilkd.key.testgen.smt.testgen.MemoryTestGenerationLog;
35-
import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLog;
34+
import de.uka.ilkd.key.testgen.smt.testgen.MemoryTestGenerationLogger;
35+
import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLogger;
3636
import de.uka.ilkd.key.util.KeYConstants;
3737

3838
import org.key_project.logic.Term;
3939
import org.jspecify.annotations.NullMarked;
4040
import org.jspecify.annotations.Nullable;
41+
import org.jspecify.annotations.NullMarked;
42+
import org.jspecify.annotations.Nullable;
4143
import org.key_project.logic.sort.Sort;
4244
import org.key_project.prover.sequent.SequentFormula;
4345
import org.key_project.util.java.StringUtil;
@@ -92,7 +94,7 @@ public class TestCaseGenerator {
9294
private final Path dontCopy;
9395
protected final Path modDir;
9496
protected final String directory;
95-
private final TestGenerationLog logger;
97+
private final TestGenerationLogger logger;
9698
private final String fileName;
9799
private final String packageName;
98100
private final String mutName;
@@ -106,8 +108,8 @@ public class TestCaseGenerator {
106108

107109
private final TestGenerationSettings settings;
108110

109-
public TestCaseGenerator(Proof proof, TestGenerationSettings settings, @Nullable TestGenerationLog log) {
110-
logger = Objects.requireNonNullElse(log, new MemoryTestGenerationLog());
111+
public TestCaseGenerator(Proof proof, TestGenerationSettings settings, @Nullable TestGenerationLogger log) {
112+
logger = Objects.requireNonNullElse(log, new MemoryTestGenerationLogger());
111113
this.settings = settings;
112114

113115
fileName = "TestGeneric" + TestCaseGenerator.FILE_COUNTER;
@@ -360,9 +362,6 @@ public JavaFile createTestCaseContent(Collection<SMTSolver> problemSolvers) {
360362
switch (settings.useJunit()) {
361363
case JUnit4 -> ms.addAnnotation(JUNIT4_TEST_ANNOTATION);
362364
case JUnit5 -> ms.addAnnotation(JUNIT5_TEST_ANNOTATION);
363-
case TestNG -> ms.addAnnotation(TESTNG_TEST_ANNOTATION);
364-
case Plain -> {
365-
}
366365
}
367366
ms.addComment("Test preamble: creating objects and intializing test data");
368367
generateTestCase(ms, m, typeInfMap);

‎key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestgenFacade.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@
1818
import de.uka.ilkd.key.smt.solvertypes.SolverTypes;
1919
import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro;
2020
import de.uka.ilkd.key.testgen.settings.TestGenerationSettings;
21-
import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLog;
21+
import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLogger;
2222
import org.jspecify.annotations.Nullable;
2323

2424
import java.io.IOException;
@@ -35,7 +35,7 @@ public record TestgenFacade(TestGenerationSettings settings) {
3535
*/
3636
public static void generateTestcases(KeYEnvironment<?> env, Proof proof,
3737
TestGenerationSettings settings,
38-
@Nullable TestGenerationLog log) throws InterruptedException {
38+
@Nullable TestGenerationLogger log) throws InterruptedException {
3939
final TestCaseGenerator tg = new TestCaseGenerator(proof, settings, log);
4040

4141
NewSMTTranslationSettings newSettings = new NewSMTTranslationSettings();

0 commit comments

Comments
 (0)