ASTBuilder: Generate sealed class hierarchy

[maul-esel]

This PR changes the ASTBuilder such that it marks the generated AST classes as sealed (for abstract supertypes such as Expression) resp. final (for concrete classes such as IdentifierExpression).

The intent is to have a precise, complete and closed description of the elements that can make up an AST. As a major consequence, this enables exhaustiveness checks for pattern matching! Code can now switch over all types of e.g. Boogie expressions like this:

switch (expr) {
case IdentifierExpression idExpr -> ...
case BooleanLiteral boolLit -> ...
... (more cases) ...
}

without needing to include a default case, as the compiler can be sure whether or not all cases are handled. This doesn't just get rid of an annoying line of code, it will also have the benefit that if new AST classes are added, the compiler immediately reports all the case distinctions where the new classes must be handled -- rather than silently going to the default and crashing (or worse, behaving incorrectly) at runtime.

My hope is that such pattern matching can be particularly useful when (back-)translating between C, ACSL, Boogie and SMT. I was fiddling around in the IcfgBuilder code when I had this idea; there are several places there that could benefit from pattern matching.

Other Changes

To make this change work, I had to get rid of two hand-written classes that extend the Boogie resp. ACSL expressions and were used in backtranslation. One of them is now in the official ACSL AST (as the backtranslation creates instances that are passed on to other code), the other no longer extends the Boogie AST.

Limitations

I stopped short of even more pattern-matching support by making the classes records -- this would be a more complex change:

• Records cannot have superclasses (other than java.lang.Record). So we would have to replace abstract base classes like Expression with (sealed) interfaces. Some functionality could be implemented in those interfaces with default methods, but all fields would have to be generated in each concrete implementation.
• Records can only have immutable fields, and our AST classes have some write-once fields particularly for the ILocation. These cannot easily be made final because the object graph is cyclic -- the node points to the location, and the location points to the node.

As there seem to be some plans to support better pattern matching for (non-record) classes in future Java versions, perhaps the goal of better AST pattern matching can then be achieved in an easier way.

[danieldietsch]

This is a really nice change!

[schuessf]

Nice change, I have just one open question regarding the change in the AST.

[schuessf]

I just started the Nightly build to be sure that there is no issue with this change 🙂

[maul-esel]

👍 Thanks. I always forget that it has to be re-enabled after creating the PR. The previous build for the branch looks good though.

[maul-esel]

If there are no further objections and the CI does not show new problems, I will merge this tonight.

[schuessf]

👍 Thanks. I always forget that it has to be re-enabled after creating the PR. The previous build for the branch looks good though.

Oh, if you ran it on the branch before, there are probably to crucial changes. I just did not find any reference in this PR to a succesful Nightly. But it does not hurt to wait for another Nightly run either.