Adopt Google Java style (#3757)

This PR is an initial attempt to build some consensus around a
consistent, automated code style for the K Frontend's Java code. Other
parts of K already do this for other languages, and so I think there's a
pretty clear precedent that we should want to set something similar up
for our largest, oldest codebase:
* The LLVM backend's C++ code is formatted with
[`clang-format`](https://github.com/runtimeverification/llvm-backend/blob/master/.clang-format)
* The Haskell backend (and booster)'s Haskell code is formatted with
[Fourmolu](https://github.com/runtimeverification/hs-backend-booster/blob/main/fourmolu.yaml)
* Pyk's Python code is formatted with
[Black](https://github.com/runtimeverification/pyk/blob/41706ef5081585a4c71f7fccb4dea2d7a3796421/Makefile#L88-L89)

At a high level, the notional benefits of doing this are:
* Improved readability of code
* More focused PR review; no consideration needs to be given to
formatting when reading and reviewing code
* Eliminates "diff noise" from unrelated formatting changes
* Consistency across the whole codebase; there are nearly 100 unique
contributors to K which means that small variations in style have been
accrued over time

I have done some research into available auto-formatters for Java,
focusing on the following points:
1. Is the style agreeable to developers, and do we as a team feel happy
with the results it produces?
2. Can the style be applied locally using our existing tools[^1]?
3. Can the style be enforced in CI using our existing Github Actions
infrastructure?
4. Is there a community consensus around using this style in practice?

Beginning with (4) the standout contender for a "standardised" tool
that's used by lots of Java developers in practice is Google's
`google-java-format` tool, which is designed to apply the [Google Java
Style](https://google.github.io/styleguide/javaguide.html)
automatically. This PR focuses on using this tool and evaluating its
tradeoffs; if we later decide it's totally unworkable then we can
revisit this evaluation with a different tool.

My summary of the pros and cons of this format are:

#### Pros

* Implemented and maintained by a large company who rely on it for their
own tooling.
  * Includes support for new language features and syntax.
* It is unlikely that Google will stop using this tool on their Java
code, and so the chances that it ends up bit-rotting into uselessness
are very small.
* Active secondary ecosystem for IDE and CI tooling.
  * Official IntelliJ plugin
  * Third-party, actively maintained Maven integration
  * Third-party, actively maintained Github action
* **Personally speaking**, I like the style that's been applied; a skim
through the diff suggests that some of the expressions I've found
hardest to parse in the frontend are now a bit clearer
* Easy enough to get working locally; the only real issue I had was that
I seemingly hadn't updated IntelliJ in two years and the JDK version it
has internally was too old.
* Works well in CI; this PR adds an action to the test workflow that
checks formatting.

#### Cons

* Not configurable beyond 2/4 space indentation; this is by design on
Google's part[^2].
* One big diff will end up getting applied to the whole project[^3].
* Others may not prefer the style used.

I hope that this is a fair summary of the tradeoffs of doing this kind
of tooling update; I'd like to get opinions from everyone who works on
this code to make sure that we're all as happy as possible with what we
end up doing. Things to think about in particular:
* Do you like the code style, from skimming the diff?
* Does the "format locally with IntelliJ, check + enforce in CI"
workflow work for you, or would you rather have CI make commits to your
branch so that you don't have to worry about formatting[^4]?
* Are there other tools you're aware of to do the same job?


[^1]: By this I really just mean IntelliJ; I'm not aware of anyone using
different tools to develop the K Frontend. If you're using some other
setup then please let me know!
[^2]: This is also the situation we have with Black for Python, however,
and that works fine!
[^3]: Though this is true for _any_ formatter, and we probably just need
to accept this pain as a once-off cost of doing business.
[^4]: The former is how we do automatic formatting for the other
projects, so I am treating it as the default option here.

.github/workflows/test-pr.yml

@@ -29,10 +29,32 @@ jobs:
             git push origin HEAD:${GITHUB_HEAD_REF}
           fi
 
+  format-check:
+    name: 'Check Java code formatting'
+    runs-on: ubuntu-latest
+    needs: version-sync
+    steps:
+      - name: 'Check out code'
+        uses: actions/checkout@v3
+        with:
+          token: ${{ secrets.JENKINS_GITHUB_PAT }}
+          # fetch-depth 0 means deep clone the repo
+          fetch-depth: 0
+      - name: 'Set up Java 17'
+        uses: actions/setup-java@v3
+        with:
+          distribution: 'zulu'
+          java-version: 17
+      - name: 'Check code is formatted correctly'
+        uses: axel-op/googlejavaformat-action@v3
+        with:
+          version: 1.18.1
+          args: "--dry-run --set-exit-if-changed"
+
   nix-maven:
     name: 'Nix: Maven'
     runs-on: ubuntu-20.04
-    needs: version-sync
+    needs: format-check
     steps:
 
       - name: 'Check out code, set up Git'
@@ -75,7 +97,7 @@ jobs:
   test-k:
     name: 'K Tests'
     runs-on: [self-hosted, linux, normal]
-    needs: version-sync
+    needs: format-check
     steps:
       - name: 'Check out code'
         uses: actions/checkout@v3
@@ -112,7 +134,7 @@ jobs:
   test-package-ubuntu-jammy:
     name: 'K Ubuntu Jammy Package'
     runs-on: [self-hosted, linux, normal]
-    needs: version-sync
+    needs: format-check
     steps:
       - uses: actions/checkout@v3
       - name: 'Build and Test'

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java

@@ -2,83 +2,83 @@
 package org.kframework.backend.haskell;
 
 import com.google.inject.Inject;
+import java.io.IOException;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
 import org.kframework.attributes.Att;
 import org.kframework.backend.kore.KoreBackend;
 import org.kframework.compile.Backend;
 import org.kframework.kompile.KompileOptions;
 import org.kframework.main.GlobalOptions;
 import org.kframework.main.Tool;
 import org.kframework.utils.Stopwatch;
-import org.kframework.utils.errorsystem.KExceptionManager;
 import org.kframework.utils.errorsystem.KEMException;
+import org.kframework.utils.errorsystem.KExceptionManager;
 import org.kframework.utils.file.FileUtil;
 
-import java.io.IOException;
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.List;
-import java.util.Set;
-import java.util.HashSet;
-
 public class HaskellBackend extends KoreBackend {
 
-    private final KompileOptions kompileOptions;
-    private final GlobalOptions globalOptions;
-    private final FileUtil files;
-    private final HaskellKompileOptions haskellKompileOptions;
-
-    @Inject
-    public HaskellBackend(
-            KompileOptions kompileOptions,
-            GlobalOptions globalOptions,
-            HaskellKompileOptions haskellKompileOptions,
-            FileUtil files,
-            KExceptionManager kem,
-            Tool tool) {
-        super(kompileOptions, files, kem, false, tool);
-        this.files = files;
-        this.haskellKompileOptions = haskellKompileOptions;
-        this.kompileOptions = kompileOptions;
-        this.globalOptions = globalOptions;
-    }
+  private final KompileOptions kompileOptions;
+  private final GlobalOptions globalOptions;
+  private final FileUtil files;
+  private final HaskellKompileOptions haskellKompileOptions;
 
+  @Inject
+  public HaskellBackend(
+      KompileOptions kompileOptions,
+      GlobalOptions globalOptions,
+      HaskellKompileOptions haskellKompileOptions,
+      FileUtil files,
+      KExceptionManager kem,
+      Tool tool) {
+    super(kompileOptions, files, kem, false, tool);
+    this.files = files;
+    this.haskellKompileOptions = haskellKompileOptions;
+    this.kompileOptions = kompileOptions;
+    this.globalOptions = globalOptions;
+  }
 
-    @Override
-    public void accept(Backend.Holder h) {
-        Stopwatch sw = new Stopwatch(globalOptions);
-        String kore = getKompiledString(h.def, true);
-        h.def = null;
-        files.saveToKompiled("definition.kore", kore);
-        sw.printIntermediate("  Print definition.kore");
-        ProcessBuilder pb = files.getProcessBuilder();
-        List<String> args = new ArrayList<>();
-        if (haskellKompileOptions.noHaskellBinary) {
-            args.add("kore-parser");
-            args.add("--no-print-definition");
-            args.add("definition.kore");
-        } else {
-            args.add(haskellKompileOptions.haskellBackendCommand);
-            args.add("definition.kore");
-            args.add("--module");
-            args.add(kompileOptions.mainModule(files));
-            args.add("--output");
-            args.add("haskellDefinition.bin");
-            args.add("--serialize");
-        }
-        try {
-          Process p = pb.command(args).directory(files.resolveKompiled(".")).inheritIO().start();
-          int exit = p.waitFor();
-          if (exit != 0) {
-              throw KEMException.criticalError("Haskell backend reported errors validating compiled definition.\nExamine output to see errors.");
-          }
-        } catch (IOException | InterruptedException e) {
-            throw KEMException.criticalError("Error with I/O while executing kore-parser", e);
-        }
-        sw.printIntermediate("  Validate def");
+  @Override
+  public void accept(Backend.Holder h) {
+    Stopwatch sw = new Stopwatch(globalOptions);
+    String kore = getKompiledString(h.def, true);
+    h.def = null;
+    files.saveToKompiled("definition.kore", kore);
+    sw.printIntermediate("  Print definition.kore");
+    ProcessBuilder pb = files.getProcessBuilder();
+    List<String> args = new ArrayList<>();
+    if (haskellKompileOptions.noHaskellBinary) {
+      args.add("kore-parser");
+      args.add("--no-print-definition");
+      args.add("definition.kore");
+    } else {
+      args.add(haskellKompileOptions.haskellBackendCommand);
+      args.add("definition.kore");
+      args.add("--module");
+      args.add(kompileOptions.mainModule(files));
+      args.add("--output");
+      args.add("haskellDefinition.bin");
+      args.add("--serialize");
     }
-
-    @Override
-    public Set<Att.Key> excludedModuleTags() {
-        return new HashSet<>(Arrays.asList(Att.CONCRETE(), Att.KAST()));
+    try {
+      Process p = pb.command(args).directory(files.resolveKompiled(".")).inheritIO().start();
+      int exit = p.waitFor();
+      if (exit != 0) {
+        throw KEMException.criticalError(
+            "Haskell backend reported errors validating compiled definition.\n"
+                + "Examine output to see errors.");
+      }
+    } catch (IOException | InterruptedException e) {
+      throw KEMException.criticalError("Error with I/O while executing kore-parser", e);
     }
+    sw.printIntermediate("  Validate def");
+  }
+
+  @Override
+  public Set<Att.Key> excludedModuleTags() {
+    return new HashSet<>(Arrays.asList(Att.CONCRETE(), Att.KAST()));
+  }
 }

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java

@@ -6,80 +6,81 @@
 import com.google.inject.Module;
 import com.google.inject.TypeLiteral;
 import com.google.inject.multibindings.MapBinder;
+import java.util.Collections;
+import java.util.List;
+import java.util.function.Function;
 import org.apache.commons.lang3.tuple.Pair;
 import org.kframework.definition.Definition;
 import org.kframework.main.AbstractKModule;
 import org.kframework.rewriter.Rewriter;
 
-import java.util.Collections;
-import java.util.List;
-import java.util.function.Function;
-
-/**
- * Created by traiansf on 9/13/18.
- */
+/** Created by traiansf on 9/13/18. */
 public class HaskellBackendKModule extends AbstractKModule {
 
-    @Override
-    public List<Module> getKompileModules() {
-        List<Module> mods = super.getKompileModules();
-        mods.add(new AbstractModule() {
-            @Override
-            protected void configure() {
-                binder().requireAtInjectOnConstructors();
-                bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
-                installHaskellBackend(binder());
-            }
+  @Override
+  public List<Module> getKompileModules() {
+    List<Module> mods = super.getKompileModules();
+    mods.add(
+        new AbstractModule() {
+          @Override
+          protected void configure() {
+            binder().requireAtInjectOnConstructors();
+            bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
+            installHaskellBackend(binder());
+          }
         });
-        return mods;
-    }
+    return mods;
+  }
 
-    private void installHaskellBackend(Binder binder) {
-        MapBinder<String, org.kframework.compile.Backend> mapBinder = MapBinder.newMapBinder(
-                binder, String.class, org.kframework.compile.Backend.class);
-        mapBinder.addBinding("haskell").to(HaskellBackend.class);
-    }
+  private void installHaskellBackend(Binder binder) {
+    MapBinder<String, org.kframework.compile.Backend> mapBinder =
+        MapBinder.newMapBinder(binder, String.class, org.kframework.compile.Backend.class);
+    mapBinder.addBinding("haskell").to(HaskellBackend.class);
+  }
 
-    @Override
-    public List<Pair<Class<?>, Boolean>> krunOptions() {
-        return Collections.singletonList(Pair.of(HaskellKRunOptions.class, true));
-    }
+  @Override
+  public List<Pair<Class<?>, Boolean>> krunOptions() {
+    return Collections.singletonList(Pair.of(HaskellKRunOptions.class, true));
+  }
 
-    @Override
-    public List<Pair<Class<?>, Boolean>> kompileOptions() {
-        return Collections.singletonList(Pair.of(HaskellKompileOptions.class, true));
-    }
+  @Override
+  public List<Pair<Class<?>, Boolean>> kompileOptions() {
+    return Collections.singletonList(Pair.of(HaskellKompileOptions.class, true));
+  }
 
-    @Override
-    public List<Module> getKRunModules() {
-        return Collections.singletonList(new AbstractModule() {
-            @Override
-            protected void configure() {
-                binder().requireAtInjectOnConstructors();
-                installHaskellRewriter(binder());
-            }
+  @Override
+  public List<Module> getKRunModules() {
+    return Collections.singletonList(
+        new AbstractModule() {
+          @Override
+          protected void configure() {
+            binder().requireAtInjectOnConstructors();
+            installHaskellRewriter(binder());
+          }
         });
-    }
-
-    private void installHaskellRewriter(Binder binder) {
-        bindOptions(HaskellBackendKModule.this::krunOptions, binder);
+  }
 
-        MapBinder<String, Function<Definition, Rewriter>> rewriterBinder = MapBinder.newMapBinder(
-                binder, TypeLiteral.get(String.class), new TypeLiteral<Function<Definition, Rewriter>>() {
-                });
-        rewriterBinder.addBinding("haskell").to(HaskellRewriter.class);
-    }
+  private void installHaskellRewriter(Binder binder) {
+    bindOptions(HaskellBackendKModule.this::krunOptions, binder);
 
+    MapBinder<String, Function<Definition, Rewriter>> rewriterBinder =
+        MapBinder.newMapBinder(
+            binder,
+            TypeLiteral.get(String.class),
+            new TypeLiteral<Function<Definition, Rewriter>>() {});
+    rewriterBinder.addBinding("haskell").to(HaskellRewriter.class);
+  }
 
-    @Override
-    public List<Module> getKProveModules() {
-        return Collections.singletonList(new AbstractModule() {
-            @Override
-            protected void configure() {
-                binder().requireAtInjectOnConstructors();
-                installHaskellBackend(binder());
-                installHaskellRewriter(binder());
-            }
+  @Override
+  public List<Module> getKProveModules() {
+    return Collections.singletonList(
+        new AbstractModule() {
+          @Override
+          protected void configure() {
+            binder().requireAtInjectOnConstructors();
+            installHaskellBackend(binder());
+            installHaskellRewriter(binder());
+          }
         });
-    }
+  }
 }