Migrate KeY v3.0 fixes to main

LICENSE.TXT

@@ -3,7 +3,7 @@
        Copyright (C) 2001-2011 Universitaet Karlsruhe (TH), Germany
                                Universitaet Koblenz-Landau, Germany
                                Chalmers University of Technology, Sweden
-       Copyright (C) 2011-2019 Karlsruhe Institute of Technology, Germany
+       Copyright (C) 2011-2026 Karlsruhe Institute of Technology, Germany
                                Technical University Darmstadt, Germany
                                Chalmers University of Technology, Sweden
 

README.md

@@ -2,6 +2,7 @@
 
 [![Tests](https://github.com/KeYProject/key/actions/workflows/tests.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/tests.yml) [![CodeQuality](https://github.com/KeYProject/key/actions/workflows/code_quality.yml/badge.svg)](https://github.com/KeYProject/key/actions/workflows/code_quality.yml)
 
+![Maven metadata URL](https://img.shields.io/maven-metadata/v?metadataUrl=https%3A%2F%2Fcentral.sonatype.com%2Frepository%2Fmaven-snapshots%2Forg%2Fkey-project%2Fkey.core%2Fmaven-metadata.xml&label=maven%20snapshots)
 ![Maven metadata URL](https://img.shields.io/maven-metadata/v?metadataUrl=https%3A%2F%2Frepo1.maven.org%2Fmaven2%2Forg%2Fkey-project%2Fkey.core%2Fmaven-metadata.xml&label=maven%20central)
 
 
@@ -29,7 +30,7 @@ Feel free to use the project templates to get started using KeY:
 
 * Hardware: >=2 GB RAM
 * Operating System: Linux/Unix, MacOSX, Windows
-* Java 21 or newer
+* Java 17 or newer
 * Optionally, KeY can make use of the following binaries:
   * SMT Solvers:
     * [Z3](https://github.com/Z3Prover/z3#z3)

build.gradle

@@ -19,8 +19,20 @@ plugins {
 
     // Plugin for publishing via the new Nexus API
     alias(libs.plugins.maven.publish) apply false
+
+    //alias(libs.plugins.license.report)
 }
 
+/* // required for generated the license report THIRD_PARTY_LICENSES.txt
+licenseReport {
+    unionParentPomLicenses = false
+    outputDir = layout.buildDirectory.dir("licenses").get().asFile
+    projects = [project] + project.subprojects
+    configurations = ['runtimeClasspath']
+    excludeOwnGroup = true
+    excludeBoms = false
+}
+*/
 
 // Configure this project for use inside IntelliJ:
 idea {
@@ -46,6 +58,8 @@ subprojects {
     apply plugin: "idea"
     apply plugin: "eclipse"
 
+//    apply plugin: libs.plugins.license.report
+
     apply plugin: "com.diffplug.spotless"
     apply plugin: "org.checkerframework"
     apply plugin: "com.vanniktech.maven.publish"
@@ -299,7 +313,11 @@ subprojects {
 
         pom {
             name = project.name
-            description = project.description
+            afterEvaluate {
+                description = project.description
+                assert (project.description != null && project.description != "") : "Description of modules are required at maven-central"
+                print(project.description)
+            }
             url = 'https://key-project.org/'
 
             licenses {

gradle.properties

@@ -1 +1,4 @@
-org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8
+org.gradle.jvmargs=-Xmx2g -XX:MaxMetaspaceSize=512m -Dfile.encoding=UTF-8
+
+# do not release automatically at Maven Central
+mavenCentralAutomaticPublishing=false

gradle/libs.versions.toml

@@ -98,3 +98,4 @@ spotless = { id = "com.diffplug.spotless", version.ref = "spotless" }
 checkerframework = { id = "org.checkerframework", version.ref = "checkerframework-gradle" }
 maven-publish = { id = "com.vanniktech.maven.publish", version.ref = "maven-publish" }
 shadow = { id = "com.gradleup.shadow", version.ref = "shadow" }
+license-report = { id = "com.github.jk1.dependency-license-report", version = "3.1.4" }

key.core.infflow/build.gradle

@@ -1,3 +1,4 @@
+description = "Information-Flow / Non-interference calculus for Java using the KeY theorem prover"
 
 
 dependencies {

key.core.wd/build.gradle

@@ -1,3 +1,6 @@
+description = "Well-defined calculus for JML specifciation and Java using the KeY theorem prover"
+
+
 dependencies {
     api(project(":key.core"))
 

key.core/src/main/java/de/uka/ilkd/key/control/InstantiationFileHandler.java

@@ -5,8 +5,7 @@
 
 import java.io.*;
 import java.nio.charset.StandardCharsets;
-import java.nio.file.Files;
-import java.nio.file.Path;
+import java.nio.file.*;
 import java.util.*;
 
 import de.uka.ilkd.key.control.instantiation_model.TacletFindModel;
@@ -33,30 +32,44 @@ public class InstantiationFileHandler {
 
     private static Map<String, List<List<String>>> hm;
 
-    /// Finds the current place to store used instantiation. If there was a version switch
+    /// Finds the current place to store used instantiations. If there was a version change
     /// (the folder does not exist), this method tries to copy previous instantiations to
-    /// the new directory silently.
-    ///
-    /// It is guaranteed, that the folder exists.
+    /// the new directory silently. However, if both old and new instantiations exist, they are not
+    /// merge, i.e. only the new ones are used currently.
     private static Path getStoragePath() {
         Path cur = PathConfig.currentPaths.keyConfigDir.resolve("instantiations");
         if (Files.exists(cur)) {
+            /*
+             * At the moment, we do not merge when old and new instantiations are
+             * present. In the future, we could go one step further and try to merge.
+             */
             return cur;
         }
-
-        Path prev = PathConfig.previousPaths.keyConfigDir.resolve("instantiations");
+        // create the directory for storing instantiations
         try {
             Files.createDirectories(cur);
+        } catch (IOException e) {
+            LOGGER.warn("Could not create the instantiations folder {}", cur, e);
+        }
+
+        // Check if instantiations from older key version exist. If so, try to copy them over.
+        Path prev = PathConfig.previousPaths.keyConfigDir.resolve("instantiations");
+        if (Files.exists(prev)) {
             try (var files = Files.walk(prev)) {
                 files.forEach(path -> {
                     try {
-                        Files.copy(path, cur.resolve(path.relativize(prev)));
-                    } catch (IOException ignore) {
+                        Path target = cur.resolve(prev.relativize(path));
+                        // Do not overwrite existing file!
+                        if (!Files.exists(target)) {
+                            Files.copy(path, target);
+                        }
+                    } catch (IOException inner) {
+                        LOGGER.warn("Could not copy instantiation file {}", path, inner);
                     }
                 });
+            } catch (IOException e) {
+                LOGGER.warn("Could not copy instantiation files from {} to {}", prev, cur, e);
             }
-        } catch (IOException e) {
-            throw new RuntimeException(e);
         }
         return cur;
     }
@@ -82,9 +95,9 @@ private static void createHashMap() {
         hm = new TreeMap<>();
         try (var stream = Files.list(INSTANTIATION_DIR)) {
             // using a TreeMap here avoids non-determinsm introduce by the file system.
-            stream.forEach(file -> hm.put(file.toString(), null));
+            stream.forEach(file -> hm.put(file.getFileName().toString(), null));
         } catch (IOException e) {
-            LOGGER.warn("Could not read the instantions folder {}", INSTANTIATION_DIR, e);
+            LOGGER.warn("Could not read the instantiations folder {}", INSTANTIATION_DIR, e);
         }
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java

@@ -80,6 +80,7 @@ public class InitConfig {
 
     /** HashMap for quick lookups taclet name->taclet */
     private Map<Name, Taclet> activatedTacletCache = null;
+    private boolean defaultsComputed;
 
     /** the fileRepo which is responsible for consistency between source code and proof */
     private FileRepo fileRepo;
@@ -104,6 +105,9 @@ public InitConfig(Services services) {
     /// combines the found choices in KeY files, together with the current settings.
     /// The namespace of choices has to be filled.
     public void computeDefaults(ChoiceInformation ci) {
+        if (defaultsComputed) {
+            return;
+        }
         var currentDefaultChoices =
             ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices();
 
@@ -145,6 +149,8 @@ public void computeDefaults(ChoiceInformation ci) {
             }
             settings.getChoiceSettings().setDefaultChoices(defaults);
         }
+        activatedTacletCache = null;
+        defaultsComputed = true;
     }
 
     /**
@@ -203,6 +209,14 @@ public Map<Taclet, TacletBuilder<? extends Taclet>> getTaclet2Builder() {
     }
 
 
+    /**
+     * @return an immutable mapping from a category to its default choice
+     */
+    public @NonNull Map<String, Choice> getCategory2DefaultChoices() {
+        return Collections.unmodifiableMap(category2DefaultChoice);
+    }
+
+
     /**
      * sets the set of activated choices of this initial configuration. For categories without a
      * specified choice the default choice contained in category2DefaultChoice is added.
@@ -448,6 +462,7 @@ public InitConfig copyWithServices(Services services) {
         ic.header = header;
         ic.justifInfo = justifInfo.copy();
         ic.fileRepo = fileRepo; // TODO: copy instead? delete via dispose method?
+        ic.defaultsComputed = defaultsComputed;
         return ic;
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java

@@ -23,6 +23,7 @@
 import de.uka.ilkd.key.logic.label.OriginTermLabelFactory;
 import de.uka.ilkd.key.logic.op.*;
 import de.uka.ilkd.key.logic.sort.GenericSort;
+import de.uka.ilkd.key.nparser.ChoiceInformation;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.JavaModel;
 import de.uka.ilkd.key.proof.Proof;
@@ -392,11 +393,14 @@ private void populateNamespaces(Proof proof) {
         }
     }
 
-    // what is the purpose of this method?
+    /**
+     * Updates the global settings the taclet options that declared in
+     * {@code optionDeclaration.key}.
+     * A proof created afterwards inherits these settings unless it overwrites it.
+     */
     private InitConfig determineEnvironment(ProofOblInput po, InitConfig initConfig) {
-        // TODO: what does this actually do?
         ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().updateChoices(initConfig.choiceNS(),
-            false);
+            initConfig.getCategory2DefaultChoices(), false);
         return initConfig;
     }
 
@@ -505,7 +509,7 @@ public InitConfig prepare(EnvInput envInput) throws ProofInputException {
         var warnings = ic.getProfile()
                 .prepareInitConfig(ic, additionalProfileOptions);
         addWarnings(warnings);
-
+        ic.computeDefaults(new ChoiceInformation());
         return ic;
     }
 

key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java

@@ -256,7 +256,7 @@ public Path readBootClassPath() {
         if (!bootClassPathFile.isAbsolute()) {
             // convert to absolute by resolving against the parent path of the parsed file
             Path parentDirectory = file.file().getParent();
-            bootClassPathFile = parentDirectory.resolve(bootClassPathFile);
+            bootClassPathFile = parentDirectory.resolve(bootClassPathFile).normalize();
         }
         if (!Files.isDirectory(bootClassPathFile)) {
             // Report the missing directory at the \bootclasspath declaration in the .key file,
@@ -297,7 +297,7 @@ private static Location locationOrUndefined(ProblemInformation pi, String path)
             } else {
                 var f = Paths.get(normalizeStoredPath(cp));
                 if (!f.isAbsolute()) {
-                    f = parentDirectory.resolve(f);
+                    f = parentDirectory.resolve(f).normalize();
                 }
                 if (!Files.exists(f)) {
                     // Point at the \classpath declaration in the .key file instead of letting the
@@ -321,7 +321,7 @@ public Path readJavaPath() throws ProofInputException {
             if (!absFile.isAbsolute()) {
                 // convert to absolute by resolving against the parent path of the parsed file
                 Path parent = file.file().getParent();
-                absFile = parent.resolve(javaPath);
+                absFile = parent.resolve(javaPath).normalize();
             }
             if (!Files.exists(absFile)) {
                 throw new ProofInputException(String.format(

key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java

@@ -97,9 +97,12 @@ public void setChoiceCategories(Map<String, Set<String>> c2C) {
      * updates <code>category2Choices</code> if new entries are found in <code>choiceNS</code> or if
      * entries of <code>category2Choices</code> are no longer present in <code>choiceNS</code>
      *
+     * @param choiceNS the choices declared by the loaded problem file
+     * @param defaults the default choice of each category
      * @param remove remove entries not present in <code>choiceNS</code>
      */
-    public void updateChoices(Namespace<Choice> choiceNS, boolean remove) {
+    public void updateChoices(Namespace<Choice> choiceNS, Map<String, Choice> defaults,
+            boolean remove) {
         // Translate the given namespace into a map of 'string -> list[string]'
         HashMap<String, Set<String>> c2C = new LinkedHashMap<>();
         for (Choice c : choiceNS.allElements()) {
@@ -118,11 +121,11 @@ public void updateChoices(Namespace<Choice> choiceNS, boolean remove) {
             }
         }
 
+        // ensure that default values are set if a key is present
         var defaultTmp = new HashMap<>(category2Default);
         for (var pair : category2Default.entrySet()) {
             var s = pair.getKey();
             var v = pair.getValue();
-            // if key is known then the default value should exist
             if (category2Choices.containsKey(s)) {
                 if (!category2Choices.get(s).contains(v)) {
                     defaultTmp.put(s, category2Choices.get(s).iterator().next());
@@ -131,6 +134,16 @@ public void updateChoices(Namespace<Choice> choiceNS, boolean remove) {
                 defaultTmp.remove(s);
             }
         }
+
+        for (var category : category2Choices.keySet()) {
+            if (!defaultTmp.containsKey(category)) {
+                var declared = defaults.get(category);
+                if (declared != null) {
+                    defaultTmp.put(category, declared.name().toString());
+                }
+            }
+        }
+
         setDefaultChoices(defaultTmp);
     }
 

key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java

@@ -229,7 +229,7 @@ public void loadSettings() {
                     loadSettingsFromJSONStream(in);
                 }
             } catch (Exception e) {
-                LOGGER.warn("No proof-settings could be loaded, using defaults", e);
+                LOGGER.warn("No proof settings could be loaded, using defaults");
             }
         }
     }

key.core/src/main/java/de/uka/ilkd/key/util/KeYConstants.java

@@ -10,6 +10,6 @@ public interface KeYConstants {
         KeYResourceManager.getManager().getVersion() + " (internal: " + INTERNAL_VERSION + ")";
 
     String COPYRIGHT = UnicodeHelper.COPYRIGHT + " Copyright 2001"
-        + UnicodeHelper.ENDASH + "2024 " + "Karlsruhe Institute of Technology, "
+        + UnicodeHelper.ENDASH + "2026 " + "Karlsruhe Institute of Technology, "
         + "Chalmers University of Technology, and Technische Universit\u00e4t Darmstadt";
 }

key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java

@@ -212,9 +212,10 @@ public static ProofCollection automaticJavaDL() throws IOException {
          * If the fork mode is not set to noFork, the launched subprocesses
          * get the specified amount of heap memory.
          *
-         * Heap memory for subprocesses (like 500m or 2G)
+         * Heap memory for subprocesses (like 500m or 3G)
          */
-        // forkMemory = 1000m
+        settings.setForkMemory("3g");
+
 
         /*
          * To run the forked JVM in debug mode, set the TCP port to listen to here.

key.core/src/testFixtures/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java

@@ -256,6 +256,7 @@ protected void reload(boolean verbose, Path proofFile, Proof loadedProof, boolea
         if (settings.reloadEnabled() && (testProperty == TestProperty.PROVABLE) && success) {
             // Save the available proof to a temporary file.
             ProofSaver.saveToFile(proofFile, loadedProof);
+            loadedProof.dispose();
             reloadProof(proofFile);
             if (verbose) {
                 LOGGER.debug("... success: reloaded.");

key.ncore.calculus/build.gradle

@@ -1,3 +1,5 @@
+description = "Pattern Matchern New core KeY theorem prover"
+
 repositories {
     mavenCentral()
 }

key.ncore.matcher/build.gradle

@@ -1,6 +1,4 @@
-repositories {
-    mavenCentral()
-}
+description = "Compiling Matching Algorithm of the KeY theorem prover"
 
 dependencies {
     api project(':key.util')

key.ui/examples/heap/FM2024Tutorial/ArrayList/src/List.java

@@ -5,7 +5,7 @@ public interface List {
 
     //@ public instance invariant \subset(\singleton(this.seq), footprint);
     //@ public instance invariant \subset(\singleton(this.footprint), footprint);
-    //@ public accessible \inv: footprint;
+    //@ accessible \inv: footprint;
 
     /*@ public normal_behaviour
       @   requires 0 <= index && index < seq.length;

key.ui/examples/newBook/Chapter_16/Sort/Sort.java

@@ -6,7 +6,7 @@ public class Sort {
       @ ensures (\forall int i; start <= i && i<a.length;a[\result] >= a[i]);
       @ ensures start <= \result && \result < a.length;
       @ */
-    int /*@ strictly_pure @*/ max(int start) {
+    /*@ strictly_pure @*/ int max(int start) {
         int counter = start; int idx = start;
         /*@ loop_invariant  start<=counter && counter<=a.length
           @              && start<=idx && idx<a.length  && start<a.length