Adopt Google Java style

[Baltoli]

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
• The Haskell backend (and booster)'s Haskell code is formatted with Fourmolu
• Pyk's Python code is formatted with Black

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¹?
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 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².
• One big diff will end up getting applied to the whole project³.
• 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⁴?
• Are there other tools you're aware of to do the same job?

Footnotes

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. ↩

[Baltoli]

Comments to address:

• Fail fast; the tests should all depend on the formatting check
• Make sure that the message is clear on what to do in case of a failure

[Baltoli]

@radumereuta I resolved both your comments re. comment layout. For anyone reading / reviewing this change, a point I picked up while doing so is that the formatter will reformat JavaDoc comments (/**) but will not reformat ordinary block comments (/*).

If comment layouts are broken by the formatter, changing the type of comment is likely to be the answer.

[Scott-Guest]

I don't care much about the specifics of the formatting (only that something consistent is enforced!), so I'm happy with the proposed changes.

In terms of the JavaDoc comments @radumereuta mentioned, you can also wrap things in a <pre> tag and they won't be formatted: https://github.com/google/google-java-format/wiki/FAQ#why-doesnt-the-formatter-touch-pre-or-table:~:text=Formatting%20can%20be%20disabled%20in%20javadoc%20comments%20using%20the%20%3Cpre%3E%20tag.

[Baltoli]

Going to mark this as ready for review; I'd like to get it merged next week so that I can continue with automated cleanups, and we don't end up with a load of merge conflicts.

[dwightguth]

I'm not super thrilled about the order of imports, but this seems like a reasonable way of applying a standard format everywhere, and given that this is used by Google engineers it almost certainly has integrations with pretty much any editor we might choose to use, which was my main concern. So I'm going to approve this.

[radumereuta]

This is so large. I think I managed to go through half of it. I would like it if we check all the comments so they don't lose the important structures. Sometimes they really matter.
Code looks fine.

[Baltoli]

I have addressed @radumereuta's comments re. formatting of comments, and I'm confident that any more such cases will be easy to fix. In the interests of not having such a large diff hanging around for ages, as planned I'm going to merge this now - if there are any issues with tooling etc. please let me know and we can work out a solution.