From 0cb78278bcd36e4a60e08c1318cc131d95b5c57f Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 5 Dec 2024 14:55:47 +0100 Subject: [PATCH 1/4] added small utility to merge xml formatter style files --- scripts/tools/checkstyle/CodestyleMerger.java | 160 ++++++++++++++++++ 1 file changed, 160 insertions(+) create mode 100644 scripts/tools/checkstyle/CodestyleMerger.java diff --git a/scripts/tools/checkstyle/CodestyleMerger.java b/scripts/tools/checkstyle/CodestyleMerger.java new file mode 100644 index 00000000000..cce5103c310 --- /dev/null +++ b/scripts/tools/checkstyle/CodestyleMerger.java @@ -0,0 +1,160 @@ +package org.key_project.codestylemerger; + +import org.w3c.dom.Document; +import org.w3c.dom.Node; +import org.w3c.dom.NodeList; +import org.xml.sax.SAXException; + +import javax.xml.parsers.DocumentBuilder; +import javax.xml.parsers.DocumentBuilderFactory; +import javax.xml.parsers.ParserConfigurationException; +import javax.xml.transform.*; +import javax.xml.transform.dom.DOMSource; +import javax.xml.transform.stream.StreamResult; +import java.io.File; +import java.io.IOException; +import java.util.TreeMap; + +/** + * Small utility to merge two code style files of the Eclipse formatter (as produced by the IDE when + * exporting code styles) into a single one. All entries with keys that are only present in one of + * them will end up in the output. When the option "--overwriteValues" is set, then entries that are + * present in both input files are taken from the new file, otherwise they are taken from the old + * one. + *
+ * The entries in the output are sorted lexicographically by the key names. + * + * @author Wolfram Pfeifer + */ +public class CodestyleMerger { + + // TODO: for an easier implementation, the flag overwriteValues can only be used at the end ... + public static final String USAGE = "Usage: codestylemerger [--overwriteValues]"; + public static final boolean VERBOSE = false; // could be an additional option in the future, + + public static void main(String[] args) { + + if (args.length < 3 || args.length > 4) { + System.out.println(USAGE); + System.exit(-1); + } + + boolean overwriteValues = false; + if (args.length == 4) { + String option = args[3]; + if (option.equals("--overwriteValues")) { + overwriteValues = true; + } else { + System.out.println(USAGE); + System.exit(-1); + } + } + + final File key = new File(args[0]); + final File other = new File(args[1]); + final File output = new File(args[2]); + + try { + DocumentBuilder builder = DocumentBuilderFactory.newInstance().newDocumentBuilder(); + + Document origDoc = builder.parse(key); + origDoc.getDocumentElement().normalize(); + Document newDoc = builder.parse(other); + newDoc.getDocumentElement().normalize(); + + // 1) read all entries of old and new file (using TreeMaps to keep entries sorted) + TreeMap oldEntries = readXMLEntries(origDoc); + TreeMap newEntries = readXMLEntries(newDoc); + + // log entries that are only present in the old file + oldEntries.forEach((k, v) -> { if (newEntries.get(k) == null) { + if (VERBOSE) { + System.out.println("Only present in old file: " + k); + } + }}); + + // 3) merge the entries + TreeMap resultEntries = mergeXMLEntries(oldEntries, newEntries, + overwriteValues); + + // 4) clear the existing profile + Node profile = origDoc.getElementsByTagName("profile").item(0); + while (profile.hasChildNodes()) { + profile.removeChild(profile.getFirstChild()); + } + + // 5) write the new profile + resultEntries.forEach((s, n) -> { + Node cloneNode = origDoc.adoptNode(n); + profile.appendChild(cloneNode); + }); + + // this seems to be the easiest way to get nice formatting ... + trimWhitespace(origDoc); + + // make sure that a proper indentation is used: + Transformer transformer = TransformerFactory.newInstance().newTransformer(); + transformer.setOutputProperty(OutputKeys.INDENT, "yes"); + transformer.setOutputProperty("{http://xml.apache.org/xslt}indent-amount", "4"); + + DOMSource dom = new DOMSource(origDoc); + StreamResult result = new StreamResult(output); + transformer.transform(dom, result); + + // output to console for debugging + //StreamResult res = new StreamResult(System.out); + //transformer.transform(dom, res); + System.out.println("Successfully wrote to file " + args[2]); + } catch (ParserConfigurationException | TransformerException | IOException | SAXException e) { + System.out.println(USAGE); + throw new RuntimeException(e); + } + } + + private static TreeMap mergeXMLEntries(TreeMap oldEntries, + TreeMap newEntries, + boolean overwriteValues) { + TreeMap resultEntries = new TreeMap<>(oldEntries); + newEntries.forEach((k, v) -> { + if (!resultEntries.containsKey(k)) { + resultEntries.put(k, v); + if (VERBOSE) { + System.out.println("Only present in new file: " + k); + } + } else if (resultEntries.containsKey(k) && overwriteValues) { + resultEntries.put(k, v); + if (VERBOSE) { + System.out.println("Replacing key " + k); + } + } else { + // maybe with a future verbosity level + if (VERBOSE) { + //System.out.println("Ignoring key " + k); + } + } + }); + return resultEntries; + } + + private static TreeMap readXMLEntries(Document origDoc) { + TreeMap entries = new TreeMap<>(); + NodeList ls = origDoc.getElementsByTagName("setting"); + for (int i = 0; i < ls.getLength(); i++) { + Node n = ls.item(i); + String k = n.getAttributes().getNamedItem("id").getNodeValue(); + entries.put(k, n); + } + return entries; + } + + private static void trimWhitespace(Node node) { + NodeList children = node.getChildNodes(); + for(int i = 0; i < children.getLength(); ++i) { + Node child = children.item(i); + if(child.getNodeType() == Node.TEXT_NODE) { + child.setTextContent(child.getTextContent().trim()); + } + trimWhitespace(child); + } + } +} \ No newline at end of file From 692605838a3f82fc83b84fe0d11239fe5f792b12 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 5 Dec 2024 15:14:03 +0100 Subject: [PATCH 2/4] removed formatter version lock and added new keys (via new styleMerge tool) --- build.gradle | 11 +++++--- scripts/tools/checkstyle/keyCodeStyle.xml | 33 +++++++++++++++++++++++ 2 files changed, 41 insertions(+), 3 deletions(-) diff --git a/build.gradle b/build.gradle index bf77f3a1cf3..99b0e5d759b 100644 --- a/build.gradle +++ b/build.gradle @@ -348,10 +348,15 @@ subprojects { toggleOffOn() removeUnusedImports() - /* At the moment, we have to ensure that version 4.22 of the eclipse formatter is run, since newer versions - * of the formatter crash in SymbolicExecutionTreeBuilder (seems to be a but in the formatter)! + + /* When new options are added in new versions of the Eclipse formatter, the easiest way is to export the new + * style file from the Eclipse GUI and then use the CodeStyleMerger tool in + * "$rootDir/scripts/tools/checkstyle/CodeStyleMerger.java" to merge the old and the new style files, + * i.e. "java CodeStyleMerger.java keyCodeStyle.xml". The tool adds all + * entries with keys that were not present in the old file and optionally overwrites the old entries. The + * file is output with ordered keys, such that the file can easily be diffed using git. */ - eclipse("4.22").configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml") + eclipse().configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml") trimTrailingWhitespace() // not sure how to set this in the xml file ... //googleJavaFormat().aosp().reflowLongStrings() diff --git a/scripts/tools/checkstyle/keyCodeStyle.xml b/scripts/tools/checkstyle/keyCodeStyle.xml index c90b83eb810..bf271d043a0 100644 --- a/scripts/tools/checkstyle/keyCodeStyle.xml +++ b/scripts/tools/checkstyle/keyCodeStyle.xml @@ -7,12 +7,15 @@ + + + @@ -25,6 +28,7 @@ + @@ -35,6 +39,8 @@ + + @@ -43,6 +49,8 @@ + + @@ -50,9 +58,12 @@ + + + @@ -75,11 +86,14 @@ + + + @@ -99,6 +113,7 @@ + @@ -113,6 +128,7 @@ + @@ -178,6 +194,8 @@ + + @@ -203,6 +221,7 @@ + @@ -241,6 +260,7 @@ + @@ -267,6 +287,8 @@ + + @@ -286,6 +308,8 @@ + + @@ -301,6 +325,7 @@ + @@ -326,6 +351,7 @@ + @@ -340,10 +366,14 @@ + + + + @@ -364,6 +394,7 @@ + @@ -373,6 +404,7 @@ + @@ -383,6 +415,7 @@ + From 9556c882e118089d693176ad50e28311203768df Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 5 Dec 2024 17:35:38 +0100 Subject: [PATCH 3/4] disable automatic formatting of Java code blocks in comments/JavaDoc --- scripts/tools/checkstyle/keyCodeStyle.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/tools/checkstyle/keyCodeStyle.xml b/scripts/tools/checkstyle/keyCodeStyle.xml index bf271d043a0..6546b32a669 100644 --- a/scripts/tools/checkstyle/keyCodeStyle.xml +++ b/scripts/tools/checkstyle/keyCodeStyle.xml @@ -106,7 +106,7 @@ - + From eded0d922f6a283a1abb961ea7c832c3045dedde Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Thu, 5 Dec 2024 17:36:55 +0100 Subject: [PATCH 4/4] applied formatting style --- .../testcase/util/TestSymbolicExecutionUtil.java | 2 +- .../java/de/uka/ilkd/key/macros/scripts/MacroCommand.java | 2 +- .../proof/io/IntermediatePresentationProofFileParser.java | 5 +++-- .../java/de/uka/ilkd/key/rule/inst/SVInstantiations.java | 4 ++-- .../ilkd/key/speclang/jml/translation/JMLSpecFactory.java | 4 ++-- .../java/recoder/service/KeYCrossReferenceSourceInfo.java | 2 +- .../src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java | 2 +- .../runallproofs/performance/DataRecordingTestFile.java | 2 +- .../java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java | 2 +- .../java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java | 3 ++- recoder/src/main/java/recoder/service/DefaultSourceInfo.java | 2 +- 11 files changed, 16 insertions(+), 14 deletions(-) diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java index 49a2d95a902..c445ff7b364 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java @@ -43,7 +43,7 @@ public class TestSymbolicExecutionUtil extends AbstractSymbolicExecutionTestCase public void test1ImproveReadability() throws ProblemLoaderException { File location = new File(testCaseDirectory, "/readability/InnerAndAnonymousTypeTest/InnerAndAnonymousTypeTest.java") - .getAbsoluteFile(); + .getAbsoluteFile(); assertTrue(location.exists(), "Could not find required resource: " + location); KeYEnvironment environment = KeYEnvironment.load(location, null, null, null); diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java index 2a431b1cad5..88f40a5346f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java @@ -131,7 +131,7 @@ public static PosInOccurrence extractMatchingPio(final Sequent sequent, final St for (int i = 1; i < sequent.size() + 1; i++) { final boolean matchesRegex = formatTermString( LogicPrinter.quickPrintTerm(sequent.getFormulabyNr(i).formula(), services)) - .matches(".*" + matchRegEx + ".*"); + .matches(".*" + matchRegEx + ".*"); if (matchesRegex) { if (matched) { throw new ScriptException("More than one occurrence of a matching term."); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java index 178990cb002..c3ef8763cc0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java @@ -210,8 +210,9 @@ public void beginExpr(ProofElementID eid, String str) { errors.add(e); } } - case MERGE_ABSTRACTION_PREDICATES -> ((BuiltinRuleInformation) ruleInfo).currAbstractionPredicates = - str; + case MERGE_ABSTRACTION_PREDICATES -> + ((BuiltinRuleInformation) ruleInfo).currAbstractionPredicates = + str; case MERGE_USER_CHOICES -> ((BuiltinRuleInformation) ruleInfo).currUserChoices = str; case NOTES -> { ruleInfo.notes = str; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java index d10a89efcd5..168508fac60 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java @@ -270,7 +270,7 @@ public SVInstantiations addInteresting(SchemaVariable sv, InstantiationEntry Services services) { return new SVInstantiations(map.put(sv, entry), interesting().put(sv, entry), getUpdateContext(), getGenericSortInstantiations(), getGenericSortConditions()) - .checkSorts(sv, entry, false, services); + .checkSorts(sv, entry, false, services); } @@ -653,7 +653,7 @@ public String toString() { public SVInstantiations add(GenericSortCondition p_c, Services services) throws SortException { return new SVInstantiations(map, interesting(), getUpdateContext(), getGenericSortInstantiations(), getGenericSortConditions().prepend(p_c)) - .checkCondition(p_c, false, services); + .checkCondition(p_c, false, services); } public ExecutionContext getExecutionContext() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index 5c65044189b..a9ef73b301f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -1428,7 +1428,7 @@ public ImmutableSet createJMLLoopContracts(final IProgramMethod me clauses.continues, clauses.returns, clauses.signals, clauses.signalsOnly, clauses.diverges, clauses.assignables, clauses.assignablesFree, clauses.hasAssignable, clauses.hasFreeAssignable, clauses.decreases, services) - .create(); + .create(); } /** @@ -1463,7 +1463,7 @@ public ImmutableSet createJMLLoopContracts(IProgramMethod method, clauses.continues, clauses.returns, clauses.signals, clauses.signalsOnly, clauses.diverges, clauses.assignables, clauses.assignablesFree, clauses.hasAssignable, clauses.hasFreeAssignable, clauses.decreases, services) - .create(); + .create(); } private ProgramVariableCollection createProgramVariablesForStatement(Statement statement, diff --git a/key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java b/key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java index 4e18b11c1f7..fa16983f5ea 100644 --- a/key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java +++ b/key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java @@ -280,7 +280,7 @@ public Variable getVariable(String name, ProgramElement context) { */ EnumConstantSpecification ecs = (EnumConstantSpecification) ((EnumDeclaration) getType( ((Case) context.getASTParent()).getParent().getExpression())) - .getVariableInScope(name); + .getVariableInScope(name); // must not resolve! qualifying enum constant in case-statements is forbidden! return ecs; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java index 8df3490b235..64b6ea7c097 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestSemisequent.java @@ -294,7 +294,7 @@ public void testListReplaceAddRedundantList() { // [exp.: p,q,a,b,c,r] Semisequent expected = extract(extract( extract(extract(origin.insertLast(con[4])).insertLast(con[5])).insertLast(con[6])) - .insertLast(con[2])); + .insertLast(con[2])); // insert:[a,b,c,r,r,q,p] ImmutableList insertionList = ImmutableSLList.nil().prepend(con[0]).prepend(con[1]).prepend(con[2]) diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java index 3617cbc09c9..9e6a42e9e88 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java @@ -52,7 +52,7 @@ private static ApplyStrategyInfo applyStrategy(Proof proof, Strategy strategy) { proof.setActiveStrategy(strategy); return new ApplyStrategy( proof.getInitConfig().getProfile().getSelectedGoalChooserBuilder().create()) - .start(proof, proof.openGoals().head()); + .start(proof, proof.openGoals().head()); } public final ProfilingDirectories getProfileDirectories() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java index 1193b3e5406..8ddaa942b20 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java @@ -118,7 +118,7 @@ void appendDataToZipOutputStream(ZipOutputStream stream) throws IOException { zipEntryFileName += ".exception"; data = (e.getClass().getSimpleName() + " occured while trying to read data.\n" + e.getMessage() + "\n" + serializeStackTrace(e)) - .getBytes(StandardCharsets.UTF_8); + .getBytes(StandardCharsets.UTF_8); } stream.putNextEntry(new ZipEntry(zipEntryFileName)); stream.write(data); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java index dd63b24f617..083d39d5f9a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java @@ -469,7 +469,8 @@ private void processChar(char strChar) throws BadLocationException { // case '*': // case '/': - case '(', ')', '[', ']', '{', '}', '%', '!', '^', '~', '&', '|', '.', ':', ';', '?', '<', '>', '=', '\'' -> + case '(', ')', '[', ']', '{', '}', '%', '!', '^', '~', '&', '|', '.', ':', ';', '?', '<', + '>', '=', '\'' -> // case ' ': // case '"': // case '\'': diff --git a/recoder/src/main/java/recoder/service/DefaultSourceInfo.java b/recoder/src/main/java/recoder/service/DefaultSourceInfo.java index 9ccb1b97074..61bf5ea293d 100644 --- a/recoder/src/main/java/recoder/service/DefaultSourceInfo.java +++ b/recoder/src/main/java/recoder/service/DefaultSourceInfo.java @@ -1578,7 +1578,7 @@ public Variable getVariable(String name, ProgramElement context) { */ EnumConstantSpecification ecs = (EnumConstantSpecification) ((EnumDeclaration) getType( ((Case) context.getASTParent()).getParent().getExpression())) - .getVariableInScope(name); + .getVariableInScope(name); // must not resolve! qualifying enum constant in case-statements is forbidden! return ecs; }