A new grammar for configuration (KeYProject#3099)

This PR proposes an own JSON-like grammar for KeY settings and
configuration.

## Status Quo

Currently, we store our settings inside of Java Properties files. Either
for global settings inside `$HOME/.key` or inside of proof files. Java
Properties are a simple and easy solution, but also have some
disadvantages. For example,

* the lack of type safety (everything is a string),
* missing positional information (we are not able to give error messages
regarding incorrect settings),
* no support for adding comments, and
* no complex data structures.

## Proposal

I propose an own grammar, written an ANTLR4, for KeY's configuration
that is compatible with JSON and the grammar of KeY.

### Why an own grammar? (or why not JSON, TOML or Co.)

There are many popular grammars for configuration files, e.g., JSON,
TOML and YAML. I decided against them for the following reason:

* The grammar must be embeddable into our KeY files and grammar.
* No external dependencies and complexity. The grammar is small, and
parsing is done in a few hundred boring LoC.
* No support for storing additional information, like comments.

### The grammar

The grammar is an extension of JSON, allowing comments, multiline
strings, non-quoted keys, etc. An example is given in the comments
below.

The grammar is a recursive definition of values, which can simply be
expressed as an ANTLR4 grammar.

```antlr4
// Config
cfile: cvalue*;
ckv: doc=DOC_COMMENT? ckey ':' cvalue;
ckey: IDENT | STRING_LITERAL;
cvalue:
    IDENT #csymbol
  | STRING_LITERAL #cstring
  | BIN_LITERAL #cintb
  | HEX_LITERAL #cinth
  | MINUS? INT_LITERAL #cintd
  | FLOAT_LITERAL #cfpf
  | DOUBLE_LITERAL #cfpd
  | REAL_LITERAL #cfpr
  | (TRUE|FALSE) #cbool
  | LBRACE
     (ckv (COMMA ckv)*)? COMMA?
    RBRACE #table
  | LBRACKET (cvalue (COMMA cvalue)*)? RBRACKET KeYProject#986
```

### Changes

1. Settings inside proof files would no longer be strings instead the
section follows the grammar above.
2. All configuration files inside `$HOME/.key` will follow the new
grammar. In case of the presence of a properties or and JSON file, the
JSON takes advantage.
3. The interface for settings (`#writeSettings` and `#readSettings`) is
extended with two new methods which take an object of `Configuration`
(which is an extended `Map<String, Object>`) instead of a `Properties`
object.

### Migration strategies

In KeY files, we decide, based on the grammar (STRING_LITERAL vs.
JSON-object), which settings handling should be to trigger. All settings
are written as JSON-objects.

Author: wadoon

gradle/wrapper/gradle-wrapper.jar

@@ -83,10 +83,8 @@ done
 # This is normally unused
 # shellcheck disable=SC2034
 APP_BASE_NAME=${0##*/}
-APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit
-
-# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
-DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
+# Discard cd standard output in case $CDPATH is set (https://github.com/gradle/gradle/issues/25036)
+APP_HOME=$( cd "${APP_HOME:-./}" > /dev/null && pwd -P ) || exit
 
 # Use the maximum available, or set MAX_FD != -1 to use that value.
 MAX_FD=maximum
@@ -133,10 +131,13 @@ location of your Java installation."
     fi
 else
     JAVACMD=java
-    which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
+    if ! command -v java >/dev/null 2>&1
+    then
+        die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
 
 Please set the JAVA_HOME variable in your environment to match the
 location of your Java installation."
+    fi
 fi
 
 # Increase the maximum file descriptors if we can.
@@ -197,6 +198,10 @@ if "$cygwin" || "$msys" ; then
     done
 fi
 
+
+# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script.
+DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"'
+
 # Collect all arguments for the java command;
 #   * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of
 #     shell script including quotes and variable substitutions, so put them in

gradlew

@@ -26,19 +26,19 @@ public class TestGenerationSettings extends AbstractSettings {
     // endregion
 
     // region property names
-    private static final String PROP_APPLY_SYMBOLIC_EXECUTION =
-        "[TestGenSettings]applySymbolicExecution";
-    private static final String PROP_MAX_UWINDS = "[TestGenSettings]maxUnwinds";
-    private static final String PROP_OUTPUT_PATH = "[TestGenSettings]OutputPath";
-    private static final String PROP_REMOVE_DUPLICATES = "[TestGenSettings]RemoveDuplicates";
-    private static final String PROP_USE_RFL = "[TestGenSettings]UseRFL";
-    private static final String PROP_USE_JUNIT = "[TestGenSettings]UseJUnit";
-    private static final String PROP_CONCURRENT_PROCESSES = "[TestGenSettings]ConcurrentProcesses";
-    private static final String PROP_INVARIANT_FOR_ALL = "[TestGenSettings]InvariantForAll";
-    private static final String PROP_OPENJML_PATH = "[TestGenSettings]OpenJMLPath";
-    private static final String PROP_OBJENESIS_PATH = "[TestGenSettings]ObjenesisPath";
+    private static final String PROP_APPLY_SYMBOLIC_EXECUTION = "applySymbolicExecution";
+    private static final String PROP_MAX_UWINDS = "maxUnwinds";
+    private static final String PROP_OUTPUT_PATH = "OutputPath";
+    private static final String PROP_REMOVE_DUPLICATES = "RemoveDuplicates";
+    private static final String PROP_USE_RFL = "UseRFL";
+    private static final String PROP_USE_JUNIT = "UseJUnit";
+    private static final String PROP_CONCURRENT_PROCESSES = "ConcurrentProcesses";
+    private static final String PROP_INVARIANT_FOR_ALL = "InvariantForAll";
+    private static final String PROP_OPENJML_PATH = "OpenJMLPath";
+    private static final String PROP_OBJENESIS_PATH = "ObjenesisPath";
     private static final String PROP_INCLUDE_POST_CONDITION =
-        "[TestGenSettings]IncludePostCondition";
+        "IncludePostCondition";
+    private static final String CATEGORY = "TestGenSettings";
     // endregion
 
     // Option fields
@@ -56,14 +56,14 @@ public class TestGenerationSettings extends AbstractSettings {
 
 
     public TestGenerationSettings() {
-        applySymbolicExecution = TestGenerationSettings.DEFAULT_APPLYSYMBOLICEX;
-        maxUnwinds = TestGenerationSettings.DEFAULT_MAXUNWINDS;
-        outputPath = TestGenerationSettings.DEFAULT_OUTPUTPATH;
-        removeDuplicates = TestGenerationSettings.DEFAULT_REMOVEDUPLICATES;
-        useRFL = TestGenerationSettings.DEFAULT_USERFL;
-        useJunit = TestGenerationSettings.DEFAULT_USEJUNIT;
-        concurrentProcesses = TestGenerationSettings.DEFAULT_CONCURRENTPROCESSES;
-        invariantForAll = TestGenerationSettings.DEFAULT_INVARIANTFORALL;
+        applySymbolicExecution = DEFAULT_APPLYSYMBOLICEX;
+        maxUnwinds = DEFAULT_MAXUNWINDS;
+        outputPath = DEFAULT_OUTPUTPATH;
+        removeDuplicates = DEFAULT_REMOVEDUPLICATES;
+        useRFL = DEFAULT_USERFL;
+        useJunit = DEFAULT_USEJUNIT;
+        concurrentProcesses = DEFAULT_CONCURRENTPROCESSES;
+        invariantForAll = DEFAULT_INVARIANTFORALL;
         openjmlPath = DEFAULT_OPENJMLPATH;
         objenesisPath = DEFAULT_OBJENESISPATH;
         includePostCondition = DEFAULT_INCLUDEPOSTCONDITION;
@@ -128,39 +128,24 @@ public boolean includePostCondition() {
 
     @Override
     public void readSettings(Properties props) {
+        var prefix = "[" + CATEGORY + "]";
         setApplySymbolicExecution(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_APPLY_SYMBOLIC_EXECUTION,
-            TestGenerationSettings.DEFAULT_APPLYSYMBOLICEX));
-        setMaxUnwinds(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_MAX_UWINDS,
-            TestGenerationSettings.DEFAULT_MAXUNWINDS));
-        setOutputPath(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_OUTPUT_PATH,
-            TestGenerationSettings.DEFAULT_OUTPUTPATH));
+            prefix + PROP_APPLY_SYMBOLIC_EXECUTION, DEFAULT_APPLYSYMBOLICEX));
+        setMaxUnwinds(SettingsConverter.read(props, prefix + PROP_MAX_UWINDS, DEFAULT_MAXUNWINDS));
+        setOutputPath(SettingsConverter.read(props, prefix + PROP_OUTPUT_PATH, DEFAULT_OUTPUTPATH));
         setRemoveDuplicates(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_REMOVE_DUPLICATES,
-            TestGenerationSettings.DEFAULT_REMOVEDUPLICATES));
-        setRFL(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_USE_RFL,
-            TestGenerationSettings.DEFAULT_USERFL));
-        setUseJunit(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_USE_JUNIT,
-            TestGenerationSettings.DEFAULT_USEJUNIT));
+            prefix + PROP_REMOVE_DUPLICATES, DEFAULT_REMOVEDUPLICATES));
+        setRFL(SettingsConverter.read(props, prefix + PROP_USE_RFL, DEFAULT_USERFL));
+        setUseJunit(SettingsConverter.read(props, prefix + PROP_USE_JUNIT, DEFAULT_USEJUNIT));
         setConcurrentProcesses(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_CONCURRENT_PROCESSES,
-            TestGenerationSettings.DEFAULT_CONCURRENTPROCESSES));
+            prefix + PROP_CONCURRENT_PROCESSES, DEFAULT_CONCURRENTPROCESSES));
         setInvariantForAll(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_INVARIANT_FOR_ALL,
-            TestGenerationSettings.DEFAULT_INVARIANTFORALL));
-        setOpenjmlPath(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_OPENJML_PATH,
-            TestGenerationSettings.DEFAULT_OPENJMLPATH));
-        setObjenesisPath(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_OBJENESIS_PATH,
-            TestGenerationSettings.DEFAULT_OBJENESISPATH));
+            prefix + PROP_INVARIANT_FOR_ALL, DEFAULT_INVARIANTFORALL));
+        setOpenjmlPath(
+            SettingsConverter.read(props, prefix + PROP_OPENJML_PATH, DEFAULT_OPENJMLPATH));
+        setObjenesisPath(SettingsConverter.read(props, PROP_OBJENESIS_PATH, DEFAULT_OBJENESISPATH));
         setIncludePostCondition(SettingsConverter.read(props,
-            TestGenerationSettings.PROP_INCLUDE_POST_CONDITION,
-            TestGenerationSettings.DEFAULT_INCLUDEPOSTCONDITION));
+            PROP_INCLUDE_POST_CONDITION, DEFAULT_INCLUDEPOSTCONDITION));
     }
 
     public boolean removeDuplicates() {
@@ -252,22 +237,56 @@ public boolean useJunit() {
 
     @Override
     public void writeSettings(Properties props) {
-        SettingsConverter.store(props, TestGenerationSettings.PROP_APPLY_SYMBOLIC_EXECUTION,
+        var prefix = "[" + CATEGORY + "]";
+        SettingsConverter.store(props, prefix + PROP_APPLY_SYMBOLIC_EXECUTION,
             applySymbolicExecution);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_CONCURRENT_PROCESSES,
-            concurrentProcesses);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_INVARIANT_FOR_ALL,
-            invariantForAll);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_MAX_UWINDS, maxUnwinds);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_OUTPUT_PATH, outputPath);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_REMOVE_DUPLICATES,
-            removeDuplicates);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_USE_RFL, useRFL);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_USE_JUNIT, useJunit);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_OPENJML_PATH, openjmlPath);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_OBJENESIS_PATH, objenesisPath);
-        SettingsConverter.store(props, TestGenerationSettings.PROP_INCLUDE_POST_CONDITION,
-            includePostCondition);
+        SettingsConverter.store(props, prefix + PROP_CONCURRENT_PROCESSES, concurrentProcesses);
+        SettingsConverter.store(props, prefix + PROP_INVARIANT_FOR_ALL, invariantForAll);
+        SettingsConverter.store(props, prefix + PROP_MAX_UWINDS, maxUnwinds);
+        SettingsConverter.store(props, prefix + PROP_OUTPUT_PATH, outputPath);
+        SettingsConverter.store(props, prefix + PROP_REMOVE_DUPLICATES, removeDuplicates);
+        SettingsConverter.store(props, prefix + PROP_USE_RFL, useRFL);
+        SettingsConverter.store(props, prefix + PROP_USE_JUNIT, useJunit);
+        SettingsConverter.store(props, prefix + PROP_OPENJML_PATH, openjmlPath);
+        SettingsConverter.store(props, prefix + PROP_OBJENESIS_PATH, objenesisPath);
+        SettingsConverter.store(props, prefix + PROP_INCLUDE_POST_CONDITION, includePostCondition);
+    }
+
+    @Override
+    public void readSettings(Configuration props) {
+        var cat = props.getSection(CATEGORY);
+        if (cat == null)
+            return;
+        setApplySymbolicExecution(
+            cat.getBool(PROP_APPLY_SYMBOLIC_EXECUTION, DEFAULT_APPLYSYMBOLICEX));
+        setMaxUnwinds(cat.getInt(PROP_MAX_UWINDS, DEFAULT_MAXUNWINDS));
+        setOutputPath(cat.getString(PROP_OUTPUT_PATH, DEFAULT_OUTPUTPATH));
+        setRemoveDuplicates(cat.getBool(PROP_REMOVE_DUPLICATES, DEFAULT_REMOVEDUPLICATES));
+        setRFL(cat.getBool(PROP_USE_RFL, DEFAULT_USERFL));
+        setUseJunit(cat.getBool(PROP_USE_JUNIT, DEFAULT_USEJUNIT));
+        setConcurrentProcesses(cat.getInt(PROP_CONCURRENT_PROCESSES, DEFAULT_CONCURRENTPROCESSES));
+        setInvariantForAll(cat.getBool(PROP_INVARIANT_FOR_ALL, DEFAULT_INVARIANTFORALL));
+        setOpenjmlPath(cat.getString(PROP_OPENJML_PATH, DEFAULT_OPENJMLPATH));
+        setObjenesisPath(cat.getString(PROP_OBJENESIS_PATH, DEFAULT_OBJENESISPATH));
+        setIncludePostCondition(
+            cat.getBool(PROP_INCLUDE_POST_CONDITION, DEFAULT_INCLUDEPOSTCONDITION));
+    }
+
+    @Override
+    public void writeSettings(Configuration props) {
+        var cat = props.getOrCreateSection(CATEGORY);
+
+        cat.set(PROP_APPLY_SYMBOLIC_EXECUTION, applySymbolicExecution);
+        cat.set(PROP_CONCURRENT_PROCESSES, concurrentProcesses);
+        cat.set(PROP_INVARIANT_FOR_ALL, invariantForAll);
+        cat.set(PROP_MAX_UWINDS, maxUnwinds);
+        cat.set(PROP_OUTPUT_PATH, outputPath);
+        cat.set(PROP_REMOVE_DUPLICATES, removeDuplicates);
+        cat.set(PROP_USE_RFL, useRFL);
+        cat.set(PROP_USE_JUNIT, useJunit);
+        cat.set(PROP_OPENJML_PATH, openjmlPath);
+        cat.set(PROP_OBJENESIS_PATH, objenesisPath);
+        cat.set(PROP_INCLUDE_POST_CONDITION, includePostCondition);
     }
 
     public void set(TestGenerationSettings settings) {

key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java

@@ -408,8 +408,6 @@ SL_COMMENT
 
 DOC_COMMENT: '/*!' -> more, pushMode(docComment);
 ML_COMMENT: '/*' -> more, pushMode(COMMENT);
-
-
 BIN_LITERAL: '0' 'b' ('0' | '1' | '_')+ ('l'|'L')?;
 
 HEX_LITERAL: '0' 'x' (DIGIT | 'a'..'f' | 'A'..'F' | '_')+ ('l'|'L')?;
@@ -450,7 +448,7 @@ DOUBLE_LITERAL:
     ;
 
 REAL_LITERAL:
-    RATIONAL_LITERAL ('r' | 'R')
+    RATIONAL_LITERAL ('r' | 'R')?
     ;
 
 

key.core/src/main/antlr4/KeYLexer.g4

@@ -814,7 +814,8 @@ profile: PROFILE name=string_value SEMI;
 
 preferences
 :
-	KEYSETTINGS LBRACE (s=string_value)? RBRACE
+	KEYSETTINGS (LBRACE s=string_value? RBRACE
+	            |  c=cvalue ) // LBRACE, RBRACE included in cvalue#table
 ;
 
 proofScript
@@ -824,3 +825,23 @@ proofScript
 
 // PROOF
 proof: PROOF EOF;
+
+// Config
+cfile: cvalue* EOF;
+//csection: LBRACKET IDENT RBRACKET;
+ckv: doc=DOC_COMMENT? ckey ':' cvalue;
+ckey: IDENT | STRING_LITERAL;
+cvalue:
+    IDENT #csymbol
+  | STRING_LITERAL #cstring
+  | BIN_LITERAL #cintb
+  | HEX_LITERAL #cinth
+  | MINUS? INT_LITERAL #cintd
+  | MINUS? FLOAT_LITERAL #cfpf
+  | MINUS? DOUBLE_LITERAL #cfpd
+  | MINUS? REAL_LITERAL #cfpr
+  | (TRUE|FALSE) #cbool
+  | LBRACE
+     (ckv (COMMA ckv)*)? COMMA?
+    RBRACE #table
+  | LBRACKET (cvalue (COMMA cvalue)*)? COMMA? RBRACKET #list;

key.core/src/main/antlr4/KeYParser.g4

@@ -0,0 +1,113 @@
+/* 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.nparser;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.stream.Collectors;
+
+import de.uka.ilkd.key.settings.Configuration;
+import de.uka.ilkd.key.util.LinkedHashMap;
+
+import org.jspecify.annotations.NonNull;
+
+/**
+ * Translates the configuration grammar (something like JSON) into a {@link Configuration} object.
+ *
+ * @author Alexander Weigl
+ * @version 1 (03.04.23)
+ * @see KeyAst.ConfigurationFile#asConfiguration()
+ */
+class ConfigurationBuilder extends KeYParserBaseVisitor<Object> {
+    @Override
+    public List<Object> visitCfile(KeYParser.CfileContext ctx) {
+        return ctx.cvalue().stream().map(it -> it.accept(this)).collect(Collectors.toList());
+    }
+
+    @Override
+    public Object visitCkey(KeYParser.CkeyContext ctx) {
+        if (ctx.STRING_LITERAL() != null)
+            return sanitizeStringLiteral(ctx.STRING_LITERAL().getText());
+        return ctx.IDENT().getText();
+    }
+
+    @Override
+    public String visitCsymbol(KeYParser.CsymbolContext ctx) {
+        return ctx.IDENT().getText();
+    }
+
+
+    @Override
+    public String visitCstring(KeYParser.CstringContext ctx) {
+        final var text = ctx.getText();
+        return sanitizeStringLiteral(text);
+    }
+
+    @NonNull
+    private static String sanitizeStringLiteral(String text) {
+        return text.substring(1, text.length() - 1)
+                .replace("\\\"", "\"")
+                .replace("\\\\", "\\");
+    }
+
+    @Override
+    public Object visitCintb(KeYParser.CintbContext ctx) {
+        return Long.parseLong(ctx.getText(), 2);
+    }
+
+    @Override
+    public Object visitCinth(KeYParser.CinthContext ctx) {
+        return Long.parseLong(ctx.getText(), 16);
+    }
+
+    @Override
+    public Object visitCintd(KeYParser.CintdContext ctx) {
+        final var text = ctx.getText();
+        if (text.endsWith("L") || text.endsWith("l")) {
+            return Long.parseLong(text.substring(0, text.length() - 1), 10);
+        } else {
+            return Long.parseLong(text, 10);
+        }
+    }
+
+    @Override
+    public Object visitCfpf(KeYParser.CfpfContext ctx) {
+        return Double.parseDouble(ctx.getText());
+    }
+
+    @Override
+    public Object visitCfpd(KeYParser.CfpdContext ctx) {
+        return Double.parseDouble(ctx.getText());
+    }
+
+    @Override
+    public Object visitCfpr(KeYParser.CfprContext ctx) {
+        return Double.parseDouble(ctx.getText());
+    }
+
+    @Override
+    public Object visitCbool(KeYParser.CboolContext ctx) {
+        return Boolean.parseBoolean(ctx.getText());
+    }
+
+    @Override
+    public Object visitTable(KeYParser.TableContext ctx) {
+        final var data = new LinkedHashMap<String, Object>();
+        for (KeYParser.CkvContext context : ctx.ckv()) {
+            var name = context.ckey().accept(this).toString();
+            var val = context.cvalue().accept(this);
+            data.put(name, val);
+        }
+        return new Configuration(data);
+    }
+
+    @Override
+    public Object visitList(KeYParser.ListContext ctx) {
+        var seq = new ArrayList<>(ctx.children.size());
+        for (KeYParser.CvalueContext context : ctx.cvalue()) {
+            seq.add(context.accept(this));
+        }
+        return seq;
+    }
+}