diff --git a/key.core/src/main/antlr4/KeYLexer.g4 b/key.core/src/main/antlr4/KeYLexer.g4 index 544c9371a4..de0bba6cf6 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/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 8efef1a3e1..5ae4e65ce7 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 { @@ -509,7 +513,7 @@ public ConfigurationWriter printValue(Object value) { } private ConfigurationWriter printMap(Map value) { - out.format("{ "); + out.format("{"); indent += 4; newline().printIndent(); for (Iterator> iterator = @@ -525,7 +529,7 @@ private ConfigurationWriter printMap(Map value) { } indent -= 4; newline().printIndent(); - out.format(" }"); + out.format("}"); return this; } @@ -536,7 +540,7 @@ private ConfigurationWriter print(String s) { } private ConfigurationWriter printSeq(Collection value) { - out.format("[ "); + out.format("["); indent += 4; newline(); printIndent(); @@ -555,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/settings/ProofSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java index b06d230784..26fdf9f400 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, ""); } /** diff --git a/scripts/settings/RewriteSettings.java b/scripts/settings/RewriteSettings.java new file mode 100644 index 0000000000..f43bfb3add --- /dev/null +++ b/scripts/settings/RewriteSettings.java @@ -0,0 +1,144 @@ +/* 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 */ + +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 org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +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. +/// +/// ## 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 { + 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[]{ + "../../key.core/src/test/resources/testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__a()]_JML_normal_behavior_operation_contract_0.proof"}; + } + + 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) + && (it.getFileName().toString().endsWith(".key") || + it.getFileName().toString().endsWith(".proof"))) + .toList() + : Collections.singletonList(path); + 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))); + 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(); ) { + 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) { + 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 { + try (var out = new GZIPOutputStream(Files.newOutputStream(file))) { + out.write(output.toString().getBytes(Charset.defaultCharset())); + } + } + LOGGER.info("File translated, tested and written: {}", file); + } else { + ERROR = true; + } + } +} +