Merging tool for code style XML files, remove formatter version lock (#3532)

wadoon · web-flow · commit 1b3f51f0c995 · 2024-12-05T19:59:39.000Z
diff --git 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 <oldStyleFile> <newStyleFile> 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/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
@@ -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
@@ -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
@@ -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
@@ -1427,7 +1427,7 @@ public ImmutableSet<LoopContract> 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();
     }
 
     /**
@@ -1462,7 +1462,7 @@ public ImmutableSet<LoopContract> 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
@@ -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
@@ -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<SequentFormula> insertionList =
             ImmutableSLList.<SequentFormula>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
@@ -50,7 +50,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
@@ -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
@@ -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
@@ -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;
         }
diff --git a/scripts/tools/checkstyle/CodestyleMerger.java 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.
+ * <br>
+ * 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 <oldFile> <newFile> <outputFile> [--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<String, Node> oldEntries = readXMLEntries(origDoc);
+            TreeMap<String, Node> 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<String, Node> 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<String, Node> mergeXMLEntries(TreeMap<String, Node> oldEntries,
+                                                         TreeMap<String, Node> newEntries,
+                                                         boolean overwriteValues) {
+        TreeMap<String, Node> 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<String, Node> readXMLEntries(Document origDoc) {
+        TreeMap<String, Node> 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);
+        }
+    }
+}
diff --git a/scripts/tools/checkstyle/keyCodeStyle.xml b/scripts/tools/checkstyle/keyCodeStyle.xml

Original file line number	Diff line number	Diff line change
`@@ -210,8 +210,9 @@ public void beginExpr(ProofElementID eid, String str) {`
`210`	`210`	`errors.add(e);`
`211`	`211`	`}`
`212`	`212`	`}`
`213`		`- case MERGE_ABSTRACTION_PREDICATES -> ((BuiltinRuleInformation) ruleInfo).currAbstractionPredicates =`
`214`		`- str;`
	`213`	`+ case MERGE_ABSTRACTION_PREDICATES ->`
	`214`	`+ ((BuiltinRuleInformation) ruleInfo).currAbstractionPredicates =`
	`215`	`+ str;`
`215`	`216`	`case MERGE_USER_CHOICES -> ((BuiltinRuleInformation) ruleInfo).currUserChoices = str;`
`216`	`217`	`case NOTES -> {`
`217`	`218`	`ruleInfo.notes = str;`
Original file line number	Diff line number	Diff line change
`@@ -270,7 +270,7 @@ public SVInstantiations addInteresting(SchemaVariable sv, InstantiationEntry<?>`
`270`	`270`	`Services services) {`
`271`	`271`	`return new SVInstantiations(map.put(sv, entry), interesting().put(sv, entry),`
`272`	`272`	`getUpdateContext(), getGenericSortInstantiations(), getGenericSortConditions())`
`273`		`- .checkSorts(sv, entry, false, services);`
	`273`	`+ .checkSorts(sv, entry, false, services);`
`274`	`274`	`}`
`275`	`275`
`276`	`276`
`@@ -653,7 +653,7 @@ public String toString() {`
`653`	`653`	`public SVInstantiations add(GenericSortCondition p_c, Services services) throws SortException {`
`654`	`654`	`return new SVInstantiations(map, interesting(), getUpdateContext(),`
`655`	`655`	`getGenericSortInstantiations(), getGenericSortConditions().prepend(p_c))`
`656`		`- .checkCondition(p_c, false, services);`
	`656`	`+ .checkCondition(p_c, false, services);`
`657`	`657`	`}`
`658`	`658`
`659`	`659`	`public ExecutionContext getExecutionContext() {`
Original file line number	Diff line number	Diff line change
`@@ -280,7 +280,7 @@ public Variable getVariable(String name, ProgramElement context) {`
`280`	`280`	`*/`
`281`	`281`	`EnumConstantSpecification ecs = (EnumConstantSpecification) ((EnumDeclaration) getType(`
`282`	`282`	`((Case) context.getASTParent()).getParent().getExpression()))`
`283`		`- .getVariableInScope(name);`
	`283`	`+ .getVariableInScope(name);`
`284`	`284`	`// must not resolve! qualifying enum constant in case-statements is forbidden!`
`285`	`285`	`return ecs;`
`286`	`286`	`}`
Original file line number	Diff line number	Diff line change
`@@ -50,7 +50,7 @@ private static ApplyStrategyInfo applyStrategy(Proof proof, Strategy strategy) {`
`50`	`50`	`proof.setActiveStrategy(strategy);`
`51`	`51`	`return new ApplyStrategy(`
`52`	`52`	`proof.getInitConfig().getProfile().getSelectedGoalChooserBuilder().create())`
`53`		`- .start(proof, proof.openGoals().head());`
	`53`	`+ .start(proof, proof.openGoals().head());`
`54`	`54`	`}`
`55`	`55`
`56`	`56`	`public final ProfilingDirectories getProfileDirectories() {`
Original file line number	Diff line number	Diff line change
`@@ -118,7 +118,7 @@ void appendDataToZipOutputStream(ZipOutputStream stream) throws IOException {`
`118`	`118`	`zipEntryFileName += ".exception";`
`119`	`119`	`data = (e.getClass().getSimpleName() + " occured while trying to read data.\n"`
`120`	`120`	`+ e.getMessage() + "\n" + serializeStackTrace(e))`
`121`		`- .getBytes(StandardCharsets.UTF_8);`
	`121`	`+ .getBytes(StandardCharsets.UTF_8);`
`122`	`122`	`}`
`123`	`123`	`stream.putNextEntry(new ZipEntry(zipEntryFileName));`
`124`	`124`	`stream.write(data);`