Skip to content

Make use of Java 17 in CPAchecker

Philipp Wendler requested to merge 993-java-17 into trunk

This MR bumps the Java version required by CPAchecker from Java 11 to Java 17 and, more importantly, adopts new features from Java 12 to 17 in the code base. It is intended as an overview over what can be done in Java 17 and as a place for discussions about these features, i.e., whether and how we want to use them in CPAchecker.
@All Please provide feedback, especially with regards to my thoughts listed below, even if this MR is already closed!
Do not attempt to review this MR in one go, instead look at the description below and individual commits.

Overview of new features

Switch expressions

  • switch can be used as an expression, e.g., return switch(...) { ... }. yield is used as keyword to produce a value.
  • Benefit: Compiler checks all that cases return exactly one value. A switch over an enum without default clause guarantees that all enum constants are present and provides compile-time instead of run-time safety (used in 9a0c1f6c).
  • Examples: 5c6f6c15 (together with arrow labels)
  • Thought: Good to use at least for switch statements with a single effect (return or assignment to a single variable), less clear for switch statements with assignments to more than one variable. Error Prone and Eclipse contain automated refactorings for switch expressions, but for converting more instances we need to wait until these refactorings are improved.

Arrow labels for switch

  • Note: Introduced as part of switch expressions, but both features are orthogonal! Arrow labels can occur in switch statements, and classic case labels can occur in switch expressions! Make sure to understand which benefit is caused by which syntax.
  • Switch can use case value -> ... instead of case value: .... Both kinds of cases cannot be mixed. For switch expressions where an arrow case contains a single expression, no yield is necessary. More than one value can be specified for a case.
  • Benefit: Easier to understand because no fall through allowed/possible, enforces use of blocks ({...}) for cases with more than one statement, which prevents accidental reuse of variables across cases as in bcad922b, 67591a83.
  • Examples: 81adc577, 5c6f6c15 (together with switch expressions)
  • Thought: We might want to require this to be used exclusively and forbid classic case ...: labels? Intended fall throughs are are. Or only for switch instances that do not use fall through?

Records

  • Immutable data classes with automatically generated constructor, equals(), hashCode(), and toString(). Often a one-liner is sufficient and worth it even for just storing some tuples in a list temporarily.
  • Benefit: Much less effort to write a proper data class, better understandable than using Pair and Triple due to the names given to the record and its components.
  • Examples: cd9c5bc2, 2ed9f060, a2fd7eb9
  • Thought: Should be used where possible. Should replace all uses of Triple and maybe also Pair, or at least pairs with identical types for both parts?

Sealed classes

  • Allows to restrict subclassing to an explicit list of given subclasses. In the future allows pattern matching.
  • Can be used in CPAchecker for many class hierarchies like AST nodes etc.
  • Benefit: The compiler can detect more impossible instanceof checks. This found some bugs already (62163392, 0cd1a6c3, 32f04c9f).
  • Examples: ebca798c, b443f28e, 82277cc8
  • Thought: Good to use where possible, especially for core class hierarchies.

Pattern matching for instanceof

  • Allows to write the following instead of a declaration of a new variable with an explicit cast:
    if (o instanceof Foo foo) {
        foo.method_on_Foo()
    }
    This is even possible if the instanceof condition is negated.
  • Benefit: less repetition, often allows to merge nested if and reduce indentation: 4c0ed3b2
  • Example: 3aa5233b
  • Thought: Good to use, but unclear whether we should also use it with negated conditions?

Text blocks

  • Allows to write multi-line strings with """ as delimiter. Both trailing spaces and common indentation are removed automatically from the string, typically leaving only the content that is desired.
  • Benefit: Easier to read for strings with line breaks.
  • Examples: f416dcab
  • Thought: Good to use for multi-line strings, but unclear whether it is worth for long single-line strings (which would need escaping of line breaks in a text block)?

String::formatted(Object... args)

  • Instance method for string formatting (as in Python) instead of static String.format(String, Object... args).
  • Benefit: slightly shorter, easier to read because most important part (the string template) comes first.
  • Thought: Good replacement for all uses of String.format, can be produced by a Refaster rule once Refaster works with Java 17.

Fixes #993 (closed)

Edited by Philipp Wendler

Merge request reports