From e15c7465828903a522d0a902df422356d1c343a6 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 6 Apr 2025 20:32:44 +0200 Subject: [PATCH 1/4] A tool for rewriting the settings in KeY files to the new JSON-like format. --- key.core/src/main/antlr4/KeYLexer.g4 | 6 +- .../java/de/uka/ilkd/key/RewriteSettings.java | 96 +++++++++++++++++++ .../uka/ilkd/key/settings/Configuration.java | 4 + .../uka/ilkd/key/settings/ProofSettings.java | 2 +- 4 files changed, 106 insertions(+), 2 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/RewriteSettings.java diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 544c9371a42..de0bba6cf68 100644 --- a/key.core/src/main/antlr4/KeYLexer.g4 +++ b/key.core/src/main/antlr4/KeYLexer.g4 @@ -40,6 +40,10 @@ lexer grammar KeYLexer; } private Token tokenBackStorage = null; + private boolean proofIsEOF = true; + public void setProofIsEOF(boolean b) { proofIsEOF = b;} + public boolean isProofIsEOF() { return proofIsEOF;} + @Override public void emit(Token token) { int MAX_K = 10; @@ -51,7 +55,7 @@ lexer grammar KeYLexer; break; } } - if(token.getType() == PROOF) { + if(token.getType() == PROOF && isProofIsEOF()) { tokenBackStorage = super.emitEOF(); //will later be overwritten the EOF token } diff --git a/key.core/src/main/java/de/uka/ilkd/key/RewriteSettings.java b/key.core/src/main/java/de/uka/ilkd/key/RewriteSettings.java new file mode 100644 index 00000000000..8c28b2e2703 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/RewriteSettings.java @@ -0,0 +1,96 @@ +/* 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; + +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.Collections; +import java.util.Iterator; + +import de.uka.ilkd.key.nparser.KeYLexer; +import de.uka.ilkd.key.nparser.ParsingFacade; +import de.uka.ilkd.key.settings.ProofSettings; + +import org.antlr.v4.runtime.CharStreams; +import org.antlr.v4.runtime.Token; +import org.antlr.v4.runtime.misc.ParseCancellationException; + +/** + * @author Alexander Weigl + * @version 1 (4/6/25) + */ +public class RewriteSettings { + public static void main(String[] args) throws IOException { + if (args.length == 0) { + args = new String[] { + "key.core/src/test/resources/testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__a()]_JML_normal_behavior_operation_contract_0.proof" }; + } + + for (String arg : args) { + var path = Paths.get(arg); + var files = Files.isDirectory( + path) ? Files.walk(path).filter(it -> Files.isRegularFile(it) + && (it.getFileName().toString().endsWith(".key") || + it.getFileName().toString().endsWith(".proof"))) + .toList() + : Collections.singletonList(path); + for (var file : files) { + rewrite(file); + } + + } + } + + private static void rewrite(Path file) throws IOException { + var lex = ParsingFacade.createLexer(file); + lex.setProofIsEOF(false); + var ctx = lex.getAllTokens(); + var output = new StringBuilder(); + + boolean hit = false; + for (Iterator iterator = ctx.iterator(); iterator.hasNext();) { + var token = iterator.next(); + if (token.getType() == KeYLexer.KEYSETTINGS) { + output.append(token.getText()); + + while (iterator.hasNext() && token.getType() != KeYLexer.STRING_LITERAL) { + token = iterator.next(); + } + + if (token.getType() != KeYLexer.STRING_LITERAL) { + return; + } + + hit = true; + + final var text = token.getText(); + var settings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS); + settings.loadSettingsFromPropertyString(text.substring(1, text.length() - 1)); + output.append(settings.settingsToString()); + + while (iterator.hasNext() && token.getType() != KeYLexer.RBRACE) { + token = iterator.next(); + } + } else { + output.append(token.getText()); + } + } + + if (!hit) { + System.err.printf("No settings in file %s found%n", file); + return; + } + + try { + ParsingFacade.parseFile(CharStreams.fromString(output.toString())); + Files.writeString(file, output.toString()); + } catch (ParseCancellationException e) { + System.err.printf("Error parsing after rewrite file %s: %s", file, e.getMessage()); + System.err.println(output); + System.exit(1); + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 8efef1a3e1b..2a7e7eee7ae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -466,6 +466,10 @@ public ConfigurationWriter printIndent() { } public ConfigurationWriter printComment(String comment) { + if (comment == null || comment.isBlank()) { + return this; + } + if (comment.contains("\n")) { out.format("/* %s */\n", comment); } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java index b06d2307847..26fdf9f400f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java @@ -136,7 +136,7 @@ public Configuration getConfiguration() { * Used by saveSettings() and settingsToString() */ public void settingsToStream(Writer out) { - getConfiguration().save(out, "Proof-Settings-Config-File"); + getConfiguration().save(out, ""); } /** From 6a7cca56f57d6da2bef57c4b95b39b69642aca10 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 22 Nov 2025 16:21:08 +0100 Subject: [PATCH 2/4] move into script folder finishing --- .../uka/ilkd/key/settings/Configuration.java | 8 +++--- .../settings}/RewriteSettings.java | 25 ++++++++++++++----- 2 files changed, 23 insertions(+), 10 deletions(-) rename {key.core/src/main/java/de/uka/ilkd/key => scripts/settings}/RewriteSettings.java (78%) diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 2a7e7eee7ae..5ae4e65ce76 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -513,7 +513,7 @@ public ConfigurationWriter printValue(Object value) { } private ConfigurationWriter printMap(Map value) { - out.format("{ "); + out.format("{"); indent += 4; newline().printIndent(); for (Iterator> iterator = @@ -529,7 +529,7 @@ private ConfigurationWriter printMap(Map value) { } indent -= 4; newline().printIndent(); - out.format(" }"); + out.format("}"); return this; } @@ -540,7 +540,7 @@ private ConfigurationWriter print(String s) { } private ConfigurationWriter printSeq(Collection value) { - out.format("[ "); + out.format("["); indent += 4; newline(); printIndent(); @@ -559,7 +559,7 @@ private ConfigurationWriter printSeq(Collection value) { } indent -= 4; newline().printIndent(); - out.format(" ]"); + out.format("]"); return this; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/RewriteSettings.java b/scripts/settings/RewriteSettings.java similarity index 78% rename from key.core/src/main/java/de/uka/ilkd/key/RewriteSettings.java rename to scripts/settings/RewriteSettings.java index 8c28b2e2703..66da4615fb6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/RewriteSettings.java +++ b/scripts/settings/RewriteSettings.java @@ -1,7 +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; import java.io.IOException; import java.nio.file.Files; @@ -18,15 +17,29 @@ import org.antlr.v4.runtime.Token; import org.antlr.v4.runtime.misc.ParseCancellationException; -/** - * @author Alexander Weigl - * @version 1 (4/6/25) - */ +/// This is a java program for rewriting the settings of KeY files from the old format to the new format. +/// The old format was a string contain a properties file (`key=value`). The new format is JSON-like tree structure +/// with the advantage of type safety and structureness. +/// +/// ## How to run the program +/// 1. Compile key to receive a fatjar +/// ```sh +/// key> gradle assemble +/// ``` +/// +/// 2. Run this program using the shadow jar. Requires a rather new JDK/JRE: +/// ```sh +/// java -cp ../../key.ui/build/libs/key-2.12.4-dev-exe.jar RewriteSettings.java +/// ``` +/// (no compilation needed) +/// +/// @author Alexander Weigl +/// @version 1 (4/6/25) public class RewriteSettings { public static void main(String[] args) throws IOException { if (args.length == 0) { args = new String[] { - "key.core/src/test/resources/testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__a()]_JML_normal_behavior_operation_contract_0.proof" }; + "../../key.core/src/test/resources/testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__a()]_JML_normal_behavior_operation_contract_0.proof" }; } for (String arg : args) { From 304fce276918fcaa85fe3aa06f811057bd6810a7 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 22 Nov 2025 16:29:59 +0100 Subject: [PATCH 3/4] added gzip support --- scripts/settings/RewriteSettings.java | 56 +++++++++++++++++---------- 1 file changed, 36 insertions(+), 20 deletions(-) diff --git a/scripts/settings/RewriteSettings.java b/scripts/settings/RewriteSettings.java index 66da4615fb6..970e57e2f45 100644 --- a/scripts/settings/RewriteSettings.java +++ b/scripts/settings/RewriteSettings.java @@ -2,21 +2,23 @@ * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -import java.io.IOException; -import java.nio.file.Files; -import java.nio.file.Path; -import java.nio.file.Paths; -import java.util.Collections; -import java.util.Iterator; - import de.uka.ilkd.key.nparser.KeYLexer; import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.settings.ProofSettings; - import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.Token; import org.antlr.v4.runtime.misc.ParseCancellationException; +import java.io.IOException; +import java.nio.charset.Charset; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.Collections; +import java.util.Iterator; +import java.util.zip.GZIPInputStream; +import java.util.zip.GZIPOutputStream; + /// This is a java program for rewriting the settings of KeY files from the old format to the new format. /// The old format was a string contain a properties file (`key=value`). The new format is JSON-like tree structure /// with the advantage of type safety and structureness. @@ -25,12 +27,12 @@ /// 1. Compile key to receive a fatjar /// ```sh /// key> gradle assemble -/// ``` +///``` /// /// 2. Run this program using the shadow jar. Requires a rather new JDK/JRE: /// ```sh /// java -cp ../../key.ui/build/libs/key-2.12.4-dev-exe.jar RewriteSettings.java -/// ``` +///``` /// (no compilation needed) /// /// @author Alexander Weigl @@ -38,18 +40,18 @@ public class RewriteSettings { public static void main(String[] args) throws IOException { if (args.length == 0) { - args = new String[] { - "../../key.core/src/test/resources/testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__a()]_JML_normal_behavior_operation_contract_0.proof" }; + args = new String[]{ + "../../key.core/src/test/resources/testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__a()]_JML_normal_behavior_operation_contract_0.proof"}; } for (String arg : args) { var path = Paths.get(arg); var files = Files.isDirectory( - path) ? Files.walk(path).filter(it -> Files.isRegularFile(it) - && (it.getFileName().toString().endsWith(".key") || - it.getFileName().toString().endsWith(".proof"))) - .toList() - : Collections.singletonList(path); + path) ? Files.walk(path).filter(it -> Files.isRegularFile(it) + && (it.getFileName().toString().endsWith(".key") || + it.getFileName().toString().endsWith(".proof"))) + .toList() + : Collections.singletonList(path); for (var file : files) { rewrite(file); } @@ -58,13 +60,20 @@ public static void main(String[] args) throws IOException { } private static void rewrite(Path file) throws IOException { - var lex = ParsingFacade.createLexer(file); + boolean isGzip = file.getFileName().toString().endsWith(".gz"); + KeYLexer lex; + if (isGzip) { + var input = CharStreams.fromStream(new GZIPInputStream(Files.newInputStream(file))); + lex = ParsingFacade.createLexer(input); + } else { + lex = ParsingFacade.createLexer(file); + } lex.setProofIsEOF(false); var ctx = lex.getAllTokens(); var output = new StringBuilder(); boolean hit = false; - for (Iterator iterator = ctx.iterator(); iterator.hasNext();) { + for (Iterator iterator = ctx.iterator(); iterator.hasNext(); ) { var token = iterator.next(); if (token.getType() == KeYLexer.KEYSETTINGS) { output.append(token.getText()); @@ -99,7 +108,13 @@ private static void rewrite(Path file) throws IOException { try { ParsingFacade.parseFile(CharStreams.fromString(output.toString())); - Files.writeString(file, output.toString()); + if (!isGzip) { + Files.writeString(file, output.toString()); + } else { + try (var out = new GZIPOutputStream(Files.newOutputStream(file))) { + out.write(output.toString().getBytes(Charset.defaultCharset())); + } + } } catch (ParseCancellationException e) { System.err.printf("Error parsing after rewrite file %s: %s", file, e.getMessage()); System.err.println(output); @@ -107,3 +122,4 @@ private static void rewrite(Path file) throws IOException { } } } + From 81238cc661f617701352cde8c60ab46dd28bcd38 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 22 Nov 2025 16:40:04 +0100 Subject: [PATCH 4/4] using logger, force flag --- scripts/settings/RewriteSettings.java | 31 +++++++++++++++++++++------ 1 file changed, 25 insertions(+), 6 deletions(-) diff --git a/scripts/settings/RewriteSettings.java b/scripts/settings/RewriteSettings.java index 970e57e2f45..f43bfb3add7 100644 --- a/scripts/settings/RewriteSettings.java +++ b/scripts/settings/RewriteSettings.java @@ -8,6 +8,8 @@ import org.antlr.v4.runtime.CharStreams; import org.antlr.v4.runtime.Token; import org.antlr.v4.runtime.misc.ParseCancellationException; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; import java.io.IOException; import java.nio.charset.Charset; @@ -38,6 +40,10 @@ /// @author Alexander Weigl /// @version 1 (4/6/25) public class RewriteSettings { + private static final Logger LOGGER = LoggerFactory.getLogger(RewriteSettings.class); + private static boolean ERROR = false; + private static boolean ALWAYS_WRITE = false; + public static void main(String[] args) throws IOException { if (args.length == 0) { args = new String[]{ @@ -45,6 +51,10 @@ public static void main(String[] args) throws IOException { } for (String arg : args) { + if ("-f".equals(arg)) { + ALWAYS_WRITE = true; + } + var path = Paths.get(arg); var files = Files.isDirectory( path) ? Files.walk(path).filter(it -> Files.isRegularFile(it) @@ -55,12 +65,13 @@ public static void main(String[] args) throws IOException { for (var file : files) { rewrite(file); } - } + System.exit(ERROR ? 1 : 0); } private static void rewrite(Path file) throws IOException { boolean isGzip = file.getFileName().toString().endsWith(".gz"); + LOGGER.info("Rewriting: {} (isGzip:{})", file.getFileName(), isGzip); KeYLexer lex; if (isGzip) { var input = CharStreams.fromStream(new GZIPInputStream(Files.newInputStream(file))); @@ -102,12 +113,21 @@ private static void rewrite(Path file) throws IOException { } if (!hit) { - System.err.printf("No settings in file %s found%n", file); + LOGGER.warn("No settings in file {} found", file); return; } + boolean write = true; try { ParsingFacade.parseFile(CharStreams.fromString(output.toString())); + } catch (ParseCancellationException e) { + write = false; + LOGGER.error("Error parsing after rewrite file {}: {}", file, e.getMessage(), e); + System.err.println(output); + } + + if (write || ALWAYS_WRITE) { + if (!isGzip) { Files.writeString(file, output.toString()); } else { @@ -115,10 +135,9 @@ private static void rewrite(Path file) throws IOException { out.write(output.toString().getBytes(Charset.defaultCharset())); } } - } catch (ParseCancellationException e) { - System.err.printf("Error parsing after rewrite file %s: %s", file, e.getMessage()); - System.err.println(output); - System.exit(1); + LOGGER.info("File translated, tested and written: {}", file); + } else { + ERROR = true; } } }