restoring the KeY book example

Author: wadoon

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"
 }
+

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<Integer> {
     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<File> 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<String> 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<Proof> 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 {

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/"
         });
     }
 }

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<a.length; a[i]==b[i]);
+      @*/
+    public void arrCopy(int[] a, int[] b) {
+        for (int i = 0; i < a.length; i++) {
+            b[i] = a[i];
+        }
+    }
+}

key.util/src/main/java/org/key_project/util/collection/ImmutableMap.java

@@ -3,6 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.util.collection;
 
+import org.jspecify.annotations.Nullable;
+
 import java.util.Iterator;
 
 

key.util/src/main/java/org/key_project/util/collection/ImmutableMapEntry.java

@@ -3,12 +3,14 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.util.collection;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * This interface declares a tupel of two values. The first one is of type <S> and named key, the
  * second one is of type <T> and named value
  */
 
-public interface ImmutableMapEntry<S, T> extends java.io.Serializable {
+public interface ImmutableMapEntry<S extends @Nullable Object, T extends @Nullable Object> extends java.io.Serializable {
 
     /** @return the first part of the tupel */
     S key();

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"));