Clean up the Java AST: Avoid sub-classes in favor of Enum

[wadoon]

Java AST Enum Refactoring

Overview

This PR performs a major refactoring of the Java AST structure by converting Modifier and Operator classes from individual class-based implementations to enum-based representations. This change significantly reduces code complexity and improves maintainability.

Key Changes

1. Modifier Refactoring

• New: ModifierKind enum (ModifierKind.java) - Centralizes all modifier kinds as enum constants
• Removed: Individual modifier classes:
  • Abstract, Final, Ghost, Model, Native, NoState, Private, Protected, Public, Static, StrictFp, Synchronized, Transient, TwoState, Volatile
  • AnnotationUseSpecification, Modifiers, VisibilityModifier
• Updated: Modifier class now uses ModifierKind enum instead of subclassing

2. Operator Refactoring

• New: Operator kind enums:

  • BinaryOperatorKind.java - All binary operator types
  • UnaryOperatorKind.java - All unary operator types
  • AssignmentKind.java - All assignment operator types
  • LogicFunctionalOperator.java - New interface for logical/functional operators

• New: Assignment hierarchy:

  • UnaryAssignment.java - Interface for unary assignments (++, --)
  • BinaryAssignment.java - Class for binary assignments (+=, -=, etc.)

• Removed: Individual operator classes (~60 files):

  • Binary operators: BinaryAnd, BinaryOr, BinaryXOr, BinaryNot, Divide, Equals, GreaterThan, GreaterOrEquals, LessThan, LessOrEquals, LogicalAnd, LogicalOr, Minus, Modulo, Plus, Times, etc.
  • Assignment operators: BinaryAndAssignment, BinaryOrAssignment, BinaryXOrAssignment, DivideAssignment, MinusAssignment, ModuloAssignment, PlusAssignment, ShiftLeftAssignment, ShiftRightAssignment, TimesAssignment, etc.
  • Unary operators: Negative, Positive, LogicalNot, PostIncrement, PostDecrement, PreIncrement, PreDecrement, ShiftLeft, ShiftRight, UnsignedShiftRight, etc.
  • ADT operators: AllFields, AllObjects, SeqConcat, SeqGet, SeqIndexOf, SeqLength, SeqPut, SeqReverse, SeqSingleton, SeqSub, SetMinus, SetUnion, Singleton, etc.

• Updated:

  • BinaryOperator.java - Now uses BinaryOperatorKind enum
  • UnaryOperator.java - Now uses UnaryOperatorKind enum, removed ExpressionStatement parent
  • Assignment.java - Refactored to use new kind system

3. Performance Improvements

• Improved hashcode distribution across AST elements
• Removed redundant second children traversal in equals() methods (super.equals() already traverses children)

4. Bug Fixes

• Fixed equality comparisons for program elements with kind (class equality check was insufficient)
• Fixed LocSetLDT and SeqLDT inconsistencies in responsibleFor/getFunctionFor
• Fixed visibility handling (JML_PACKAGE vs null duplication)
• Fixed JavaASTVisitor implementations
• Fixed CreatingASTVisitor issues

5. Cleanups

• Removed deprecated StrategyPresetsSettings and related UI components
• Removed unused IsBoundedByInequationFeature and RelevantSequentFormulasGenerator
• Minor code cleanups throughout the codebase

Impact Statistics

• 204 files changed
• 2,871 insertions(+), 9,554 deletions(-)
• Net reduction of ~6,700 lines of code

Files Modified

Core AST Changes

• KeYJavaASTFactory.java - Major refactoring (-1002 lines)
• Modifier.java, ModifierKind.java (new)
• BinaryOperator.java, UnaryOperator.java, Assignment.java
• BinaryOperatorKind.java (new), UnaryOperatorKind.java (new), AssignmentKind.java (new)
• BinaryAssignment.java (new), UnaryAssignment.java (new)

Visitor Updates

• CreatingASTVisitor.java - Updated for new AST structure (-520 lines)
• JavaASTVisitor.java - Updated visitor interface (-322 lines)
• Visitor.java - Updated base visitor
• PrettyPrinter.java - Updated printing logic (-354 lines)

Related Components

• JP2KeYConverter.java - Updated for new operator/modifier structure
• TypeConverter.java - Updated type conversions
• JavaInfo.java, JavaService.java - Updated services
• Various LDTs: LocSetLDT, SeqLDT, FloatLDT, DoubleLDT, SortLDT

UI Changes

• StrategySelectionView.java - Removed strategy presets UI (-593 lines)
• MainWindow.java - Minor updates
• IconFactory.java - Updated icons

Testing

• Added new JavaMatchingTests.java (442 lines)
• Updated existing tests for compatibility
• Replayed proofs from main branch

Migration Notes

For developers:

• Code checking modifier types should now use Modifier.kind() instead of instanceof checks
• Operator handling now uses enum kinds instead of class types
• Assignment expressions are now split into UnaryAssignment and BinaryAssignment

Related Issues

Checklist

• Code compiles without errors
• Existing tests pass
• New tests added where appropriate
• Proofs replayed successfully
• Code formatted according to project standards

[unp1]

I tried to fix some of the NPEs. The visibility modifier package private is being modelled as 'null', hence checking if inheritance is allowed threw NPEs. There seem (some pre-existing) inconsistencies. I grouped all vis changes in 796c1f0 for checking

[unp1]

The matching works now for the new AST and I hand the branch back to you.

[unp1]

Not necessary something to change, but please check:

The only issue I still see is that there are now two visibility modelings for "package private"

• 'null' for the Java side
• 'JML_PACKAGE' for the JML side

The different representations mean that one has to consider both when checking visibility properties. The 'moreRestrictive' implementation needed by RepresentsAxiom is therefore not symmetric.

Did not find a better way around. In any case the behavior should be now as for main.

A more unified solution would be to either have just one PACKAGE modifier used by both or the JML_PACKAGE modifier to be discarded and the annotated elements get as visibility modifier null (like in main). In any case, what and how to do (if anything), you are the better one to judge. Also with respect to jmltoolkit and preparations for that.

In any case thanks a lot and I approved but disabled auto-merge, so you can look at it first (as said one can leave it as it is, but it has this kind of asymmetry).

[wadoon]

Not necessary something to change, but please check:
In any case thanks a lot and I approved but disabled auto-merge, so you can look at it first (as said one can leave it as it is, but it has this kind of asymmetry).

But there is also a difference between specifying package-private and not specifying it syntactically.

What is the default modifier for contracts? Does it not follow the visibility of the method?