Merging tool for code style XML files, remove formatter version lock

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()
 

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);

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.");

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;

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() {

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java

@@ -1428,7 +1428,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();
     }
 
     /**
@@ -1463,7 +1463,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,

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;
         }

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])

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() {

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);

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 '\'':

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;
         }

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);
+        }
+    }
+}