diff --git a/key.core.testgen/build.gradle b/key.core.testgen/build.gradle index f7038cc682e..d9e1b273150 100644 --- a/key.core.testgen/build.gradle +++ b/key.core.testgen/build.gradle @@ -3,4 +3,7 @@ description "Test Case Generation based on proof attempts." dependencies { implementation project(":key.core") implementation("com.squareup:javapoet:1.13.0") + + implementation "info.picocli:picocli:4.7.5" } + diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java index 3f2d0d5f8ea..1f941d10651 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TGMain.java @@ -3,50 +3,114 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.testgen; +import de.uka.ilkd.key.api.ProofManagementApi; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; +import de.uka.ilkd.key.speclang.Contract; import de.uka.ilkd.key.testgen.settings.TestGenerationSettings; import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLog; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import picocli.CommandLine; import java.io.File; -import java.util.Objects; +import java.util.ArrayList; +import java.util.LinkedList; +import java.util.List; +import java.util.concurrent.Callable; -public class TGMain { +@CommandLine.Command(name = "tcgen", mixinStandardHelpOptions = true, + description = "Generator of Testcases based on Proof Attempts") +public class TGMain implements Callable { private final static Logger LOGGER = LoggerFactory.getLogger("main"); public static void main(String[] args) throws ProblemLoaderException, InterruptedException { + int exitCode = new CommandLine(new TGMain()).execute(args); + System.exit(exitCode); + } + + @CommandLine.Parameters(description = "KeY or Java file.", arity = "1..*") + private List files = new LinkedList<>(); + + @CommandLine.Option(names = {"-s", "--symbex"}, + description = "apply symbex", negatable = true) + private boolean symbex; + + @CommandLine.Option(names = {"-c", "--contract"}, + arity = "*", + description = "name of the contract to be loaded in the Java environment") + private List contractNames = new ArrayList<>(); + + @CommandLine.Option(names = {"--all-contracts"}, + description = "name of the contract to be loaded in the Java environment") + private boolean allContracts = false; + + + @CommandLine.Option(names = {"-o", "--output"}, description = "Output folder") + private File outputFolder = new File("out"); + + @CommandLine.Option(names = {"-r", "--rfl"}, description = "Use Reflection class", negatable = true) + private boolean useReflection = false; + + @CommandLine.Option(names = {"-f", "--format"}, description = "Use Reflection class") + private Format format = Format.JUnit4; + + + @CommandLine.Option(names = {"--max-unwinds"}, description = "max unwinds") + private int maxUnwinds = 10; + @CommandLine.Option(names = {"--dups"}, description = "remove duplicates", negatable = true) + private boolean removeDuplicates; + + @Override + public Integer call() throws Exception { if (SolverTypes.Z3_CE_SOLVER.checkForSupport()) { LOGGER.error("Z3 not found! Bye."); - System.exit(1); - return; + return 1; } else { LOGGER.info("Z3 found; Version {}", SolverTypes.Z3_CE_SOLVER.getInstalledVersion()); } - var settings = new TestGenerationSettings(); - String fileName = null; - for (int i = 0; i < args.length; i++) { - var a = args[i]; - if (a.startsWith("--")) { - switch (a) { - case "--output" -> settings.setOutputPath(args[++i]); - case "--rfl" -> settings.setRFL(true); - case "--format" -> settings.setFormat(Format.valueOf(args[++i])); + TestGenerationLog log = new SysoutTestGenerationLog(); + settings.setOutputPath(outputFolder.getAbsolutePath()); + settings.setRFL(useReflection); + settings.setFormat(format); + settings.setApplySymbolicExecution(symbex); + settings.setMaxUnwinds(maxUnwinds); + settings.setRemoveDuplicates(removeDuplicates); + + for (File file : files) { + List proofs = new LinkedList<>(); + var env = KeYEnvironment.load(file); + Proof proof = env.getLoadedProof(); + if (proof == null) { // non-key file + var print = contractNames.isEmpty(); + final var api = new ProofManagementApi(env); + var contracts = api.getProofContracts(); + for (Contract contract : contracts) { + final var name = contract.getName(); + if (print) { + LOGGER.info("Contract found: {}", name); + } + + if (allContracts || contractNames.contains(name)) { + proofs.add(api.startProof(contract).getProof()); + } } - } else { - fileName = a; + } else { // key file + proofs = List.of(proof); } - } - var env = KeYEnvironment.load(new File(Objects.requireNonNull(fileName))); - TestGenerationLog log = new SysoutTestGenerationLog(); - Proof proof = env.getLoadedProof(); - TestgenFacade.generateTestcases(env, proof, settings, log); + for (Proof p : proofs) { + TestgenFacade.generateTestcases(env, p, settings, log); + p.dispose(); + } + + env.dispose(); + } + return 0; } private static class SysoutTestGenerationLog implements TestGenerationLog { diff --git a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/TestcaseGenerationE2ETest.java b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/TestcaseGenerationE2ETest.java index 6302711423e..c70f64cad7b 100644 --- a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/TestcaseGenerationE2ETest.java +++ b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/TestcaseGenerationE2ETest.java @@ -12,7 +12,16 @@ public class TestcaseGenerationE2ETest { @Test public void binarySearch() throws ProblemLoaderException, InterruptedException { TGMain.main(new String[]{ - "--output", "testcases/binarysearch/actual", "testcases/binarysearch/attempt.proof" + "--output", "testcases/binarysearch/actual", "testcases/binarysearch/attempt.proof" + }); + } + + @Test + public void arrayUtil() throws ProblemLoaderException, InterruptedException { + TGMain.main(new String[]{ + "--all-contracts", + "--output", "testcases/arrayutil/actual", + "testcases/arrayutil/src/" }); } } diff --git a/key.core.testgen/testcases/arrayutil/src/ArrayUtils.java b/key.core.testgen/testcases/arrayutil/src/ArrayUtils.java new file mode 100644 index 00000000000..19b30f44f75 --- /dev/null +++ b/key.core.testgen/testcases/arrayutil/src/ArrayUtils.java @@ -0,0 +1,14 @@ +/** From the second KeY book. + * https://link.springer.com/chapter/10.1007/978-3-319-49812-6_12 + * Listing 12.1 + */ +public class ArrayUtils { + /*@ public normal_behavior + @ ensures (\forall int i; 0<=i && i and named key, the * second one is of type and named value */ -public interface ImmutableMapEntry extends java.io.Serializable { +public interface ImmutableMapEntry extends java.io.Serializable { /** @return the first part of the tupel */ S key(); diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java index 9bd2aa7d82a..02eddad15c0 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java @@ -66,11 +66,6 @@ public void actionPerformed(ActionEvent e) { }; private final TestGenerationLog logger = new TestGenerationLog() { - @Override - public void write(String t) { - textArea.append(t); - } - @Override public void writeln(String line) { ThreadUtilities.invokeOnEventQueue(() -> textArea.append(line + "\n"));