wip picocli

Author: wadoon

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/Constants.java

@@ -5,28 +5,26 @@
 
 import org.key_project.util.java.StringUtil;
 
-public interface Constants {
-
+public class Constants {
     /**
      * Constant for the line break which is used by the operating system.
      * <p>
      * <b>Do not use {@code \n}!</b>
      */
-    String NEW_LINE = StringUtil.NEW_LINE;
-    String NULLABLE = "/*@ nullable */";
-    String ALL_OBJECTS = "allObjects";
-    String ALL_INTS = "allInts";
-    String ALL_BOOLS = "allBools";
-    String ALL_HEAPS = "allHeaps";
-    String ALL_FIELDS = "allFields";
-    String ALL_SEQ = "allSeq";
-    String ALL_LOCSETS = "allLocSets";
-
-    String OBJENESIS_NAME = "objenesis-2.2.jar";
-
-    String OLDMap = "old";
-
-    String TAB = "   ";
+    public static final String NEW_LINE = StringUtil.NEW_LINE;
+    public static final String NULLABLE = "/*@ nullable */";
+    public static final String ALL_OBJECTS = "allObjects";
+    public static final String ALL_INTS = "allInts";
+    public static final String ALL_BOOLS = "allBools";
+    public static final String ALL_HEAPS = "allHeaps";
+    public static final String ALL_FIELDS = "allFields";
+    public static final String ALL_SEQ = "allSeq";
+    public static final String ALL_LOCSETS = "allLocSets";
+    public static final String OBJENESIS_NAME = "objenesis-2.2.jar";
+    public static final String OLD_MAP = "old";
+    public static final String TAB = "   ";
+    public static final String DUMMY_POSTFIX = "DummyImpl";
 
-    String DUMMY_POSTFIX = "DummyImpl";
+    private Constants() {
+    }
 }

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

@@ -1,3 +1,6 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.testgen;
 
 import java.io.IOException;
@@ -7,30 +10,38 @@
 import java.util.Objects;
 
 /**
+ * This class manages the different paths in the output folder.
  * @author Alexander Weigl
  * @version 1 (02.02.24)
  */
 public record OutputEnvironment(Path targetFolder) {
+    /** Returns the source code folder */
     public Path getSourceDir() {
         return targetFolder.resolve("src");
     }
 
+    /** Returns the test code folder */
     public Path getTestSourceDir() {
         return targetFolder.resolve("test");
     }
 
+    /** Returns the path to the ANT build.xml file */
     public Path getAntFile() {
         return targetFolder.resolve("build.xml");
     }
 
+    /** Returns the path to the README.md file */
     public Path getReadmeFile() {
         return targetFolder.resolve("README.md");
     }
 
+    /**
+     * Initialize/create the necessary directories.
+     * @throws IOException if the output folder is not write or the folders can not be created.
+     */
     public void init() throws IOException {
         Files.createDirectories(getSourceDir());
         Files.createDirectories(getTestSourceDir());
-
         installAntFile();
     }
 

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/OutputEnvironment.java

@@ -26,11 +26,6 @@
 import org.key_project.logic.op.Operator;
 import org.key_project.logic.sort.Sort;
 
-import org.jspecify.annotations.Nullable;
-
-import org.key_project.logic.sort.Sort;
-
-import org.jspecify.annotations.Nullable;
 import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -47,8 +42,8 @@ public ProofInfo(Proof proof) {
     public IProgramMethod getMUT() {
         SpecificationRepository spec = services.getSpecificationRepository();
         IObserverFunction f = spec.getTargetOfProof(proof);
-        if (f instanceof IProgramMethod) {
-            return (IProgramMethod) f;
+        if (f instanceof IProgramMethod pm) {
+            return pm;
         } else {
             return null;
         }
@@ -65,8 +60,8 @@ public String getMUTCall() {
         StringBuilder params = new StringBuilder();
         for (ParameterDeclaration p : m.getParameters()) {
             for (VariableSpecification v : p.getVariables()) {
-                IProgramVariable var = v.getProgramVariable();
-                params.append(",").append(var.name());
+                IProgramVariable pvar = v.getProgramVariable();
+                params.append(",").append(pvar.name());
             }
         }
         if (!params.isEmpty()) {
@@ -123,9 +118,8 @@ public JTerm getPreConTerm() {
         Contract c = getContract();
         if (c instanceof FunctionalOperationContract t) {
             OriginalVariables orig = t.getOrigVars();
-            JTerm post = t.getPre(services.getTypeConverter().getHeapLDT().getHeap(), orig.self,
+            return t.getPre(services.getTypeConverter().getHeapLDT().getHeap(), orig.self,
                     orig.params, orig.atPres, services);
-            return post;
         }
         // no pre <==> false
         return services.getTermBuilder().ff();

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

@@ -7,7 +7,7 @@
 import java.util.HashSet;
 import javax.lang.model.element.Modifier;
 
-import de.uka.ilkd.key.logic.sort.Sort;
+import org.key_project.logic.sort.Sort;
 
 import com.squareup.javapoet.*;
 
@@ -77,8 +77,8 @@ public void addSort(String s) {
      */
     private HashSet<String> sortsToString() {
         final HashSet<String> result = new HashSet<>();
-        for (final Sort var : usedObjectSorts) {
-            String sort = var.toString();
+        for (final Sort s : usedObjectSorts) {
+            String sort = s.toString();
             // We only want Object-Types
             if (!" jbyte jint jlong jfloat jdouble jboolean jchar ".contains(" " + sort + " ")) {
                 if (" jbyte[] jint[] jlong[] jfloat[] jdouble[] jboolean[] jchar[] "
@@ -191,8 +191,6 @@ private void staticInitializer(boolean ghostMapActive, TypeSpec.Builder clazz) {
      * All calls to create objects for the given sorts
      */
     private void instances(final HashSet<String> sorts, TypeSpec.Builder clazz) {
-        // r.append(NEW_LINE).append(" // ---The methods for object creation---").append(NEW_LINE)
-        // .append(NEW_LINE);
         for (final String sort : sorts) {
             clazz.addMethod(newRef(sort));
         }

key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java

@@ -12,66 +12,61 @@
 import java.util.concurrent.Future;
 import java.util.regex.Pattern;
 
-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.smt.testgen.TGPhase;
 import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLifecycleListener;
+
+import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 import picocli.CommandLine;
 
-import java.io.File;
-import java.util.ArrayList;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.concurrent.Callable;
-
 @CommandLine.Command(name = "tcgen", mixinStandardHelpOptions = true,
-        description = "Generator of Testcases based on Proof Attempts")
+    description = "Generator of Testcases based on Proof Attempts")
 public class TGMain implements Callable<Integer> {
-    private final static Logger LOGGER = LoggerFactory.getLogger("main");
+    private static final Logger LOGGER = LoggerFactory.getLogger("main");
 
-    public static void main(String[] args) throws ProblemLoaderException, InterruptedException {
+    public static void main(String[] args) {
         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.Parameters(description = "Number of parallel jobs", defaultValue = "4")
+    @CommandLine.Option(names = "-T", description = "Number of parallel jobs", defaultValue = "4")
     private int numberOfThreads = 4;
 
-    @CommandLine.Option(names = {"-s", "--symbex"},
+    @CommandLine.Option(names = { "-s", "--symbex" },
         description = "apply symbolic execution", negatable = true)
     private boolean symbex;
 
     @CommandLine.Option(names = { "-c", "--contract" }, arity = "*",
         description = "name of the contract to be loaded in the Java environment. Can be a regular expression")
     private List<String> contractNames = new ArrayList<>();
 
-    @CommandLine.Option(names = {"--all-contracts"},
+    @CommandLine.Option(names = { "--all-contracts" },
         description = "test case generation for all contracts")
     private boolean allContracts = false;
 
-    @CommandLine.Option(names = {"-o", "--output"}, description = "Output folder")
+    @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)
+    @CommandLine.Option(names = { "-r", "--rfl" }, description = "Use Reflection class",
+        negatable = true)
     private boolean useReflection = false;
 
     @CommandLine.Option(names = { "-f", "--format" },
         description = "use Reflection class for instantiation")
-    private Format format = Format.JUNIT_4;
+    private JUnitFormat format = JUnitFormat.JUNIT_4;
 
     @CommandLine.Option(names = { "--max-unwinds" }, description = "max unwinds of loops")
     private int maxUnwinds = 10;
 
-    @CommandLine.Option(names = {"--dups"}, description = "remove duplicates", negatable = true)
+    @CommandLine.Option(names = { "--dups" }, description = "remove duplicates", negatable = true)
     private boolean removeDuplicates;
 
     @CommandLine.Option(names = { "--only-tests" },
@@ -118,14 +113,15 @@ public Integer call() throws Exception {
             Proof proof = env.getLoadedProof();
             if (proof == null) { // non-key file
                 var print = contractNames.isEmpty();
-                final var api = new ProofManagementApi(env);
-                var contracts = api.getProofContracts();
+                var contracts = env.getProofContracts();
                 for (Contract contract : contracts) {
                     final var name = contract.getName();
                     if (print) {
                         LOGGER.info("Contract found: {}", name);
                     } else if (allContracts || contractNameMatcher.test(name)) {
-                        proofs.add(api.startProof(contract).getProof());
+                        var p =
+                            env.createProof(contract.createProofObl(env.getInitConfig(), contract));
+                        proofs.add(p);
                     }
                 }
             } else { // key file
@@ -134,14 +130,13 @@ public Integer call() throws Exception {
 
             LOGGER.info("Number of proof found: {}", proofs.size());
 
-            var exec = Executors.newFixedThreadPool(numberOfThreads);
-            try {
+            try (var exec = Executors.newFixedThreadPool(numberOfThreads);) {
                 LOGGER.info("Start processing with {} threads", numberOfThreads);
                 var tasks = proofs.stream().map(
                     p -> TestgenFacade.generateTestcasesTask(env, p, settings, log)).toList();
                 var futures = tasks.stream().map(exec::submit).toList();
                 for (Future<?> future : futures) {
-                    future.wait();
+                    future.get();
                 }
             } finally {
                 proofs.forEach(Proof::dispose);
@@ -154,11 +149,13 @@ public Integer call() throws Exception {
 
 
 class SysoutTestGenerationLifecycleListener implements TestGenerationLifecycleListener {
-    private final static Logger LOGGER = LoggerFactory.getLogger("main");
+    private static final Logger LOGGER = LoggerFactory.getLogger("main");
 
     @Override
-        public void writeln(@Nullable String message) {
-            if(message!=null){ LOGGER.info(message);}
+    public void writeln(Object sender, @Nullable String message) {
+        if (message != null) {
+            LOGGER.info(message);
+        }
     }
 
     @Override

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

@@ -7,6 +7,8 @@
 import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLifecycleListener;
 
 /**
+ * Reporter for test case generation.
+ *
  * @author Alexander Weigl
  * @version 1 (24.05.24)
  */