JDK-8258138 : 4.10: Eliminate redundant 'final' checks in verification
  • Type: Bug
  • Component: specification
  • Sub-Component: vm
  • Priority: P4
  • Status: Resolved
  • Resolution: Fixed
  • Submitted: 2020-12-12
  • Updated: 2025-06-11
  • Resolved: 2025-06-11
The Version table provides details related to the release that this issue/RFE will be addressed.

Unresolved : Release in which this issue/RFE will be addressed.
Resolved: Release in which this issue/RFE has been resolved.
Fixed : Release in which this issue/RFE has been fixed. The release containing this fix may be available for download as an Early Access Release or a General Availability Release.

To download the current JDK release, click here.
JDK 25
25Fixed
Related Reports
Relates :  
Relates :  
Relates :  
Relates :  
Relates :  
Description
In JDK-8243582, it was recognized that the invariants associated with ACC_FINAL classes and methods are checked at class derivation time, *not* verification time. The appropriate rules were added to 5.3.5.

Meanwhile, 4.10 continues to claim that verification performs these checks. These rules should be removed.

Doing so properly will involve significant changes, as many of the rules defined in 4.10.1 exist solely to identify methods that might override an ACC_FINAL method in a superclass.
Comments
Concrete changes: - 4.10: Delete "In both strategies...", including the following 3 bullets - 4.10.1: Delete "A class is type safe if all its methods are type safe... and bytecode verification has completed successfully.", including the 'classIsTypeSafe' rule. Replace it with: "The Prolog predicate `methodIsTypeSafe` (4.10.1.5) determines whether the `Code` attribute of a particular method of a particular class or interface conforms to the structural constraints described in 4.9.2. The structural constraints are satisfied by the method if and only if the `methodIsTypeSafe` predicate is true." And revise the bullet: "Fourth, we specify how a method is type checked~~, for methods without code~~ (4.10.1.5) ~~and methods with code (4.10.1.6)~~." - 4.10.1.1: Begin the section with this, revising some useful text deleted from 4.10.1: "The Prolog term Class represents a binary class or interface that has been successfully loaded (5.3). This specification does not mandate the precise structure of this term." "Similarly, the Prolog term Method represents a method of a Class, and the Prolog term Loader represents a class loader of a Class. We do not specify the structure of the method or class loader." Delete the following unused Prolog accessors and update the count: 'classIsNotFinal', 'classMethods', 'classAttributes', 'methodAttributes', 'isInit', 'isNotFinal', 'isStatic', 'isNotStatic', 'isPrivate', 'isNotPrivate'. - 4.10.1.5: Delete this section. - 4.10.1.6: Move the first half into 4.10.1.5 (call it "Type Checking Methods"), through the 'instanceMethodInitialThisType' predicate. Delete the 'methodIsTypeSafe' rule and reuse this name for 'methodWithCodeIsTypeSafe'. Rename the remaining 4.10.1.6 section "Type Checking Code Streams"; adjust the intro: "~~We now compute whether the merged stream for a method is type correct, using the method's initial type state~~ *Given an incoming type state, the 'mergedCodeIsTypeSafe' predicate checks that a merged stream of instructions and stack map frames is type correct*:"
28-02-2025

Edit: for now, the normative rule about a VerifyError in 4.10.1 is essential and should be revised to talk about 'methodIsTypeSafe'. Per JDK-8323550, that rule really belongs in 4.10, along with a more comprehensive treatment of the relationship between static/structural constraints and verification. I've copied the suggested 4.10.1 text to that issue. For this issue: ~~Iff the predicate `classIsTypeSafe` is not true, the type checker must throw the exception `VerifyError` to indicate that the class file is malformed. Otherwise, the class file has type checked successfully and bytecode verification has completed successfully.~~ **The Prolog predicate `methodIsTypeSafe` (4.10.1.5) determines whether the `Code` attribute of a particular method is type safe. If a method with a `Code` attribute is not type safe, verification throws a `VerifyError` to indicate that the class file is malformed.** **If every method of a class with a `Code` attribute passes the `methodIsTypeSafe` check, the `class` file has type checked successfully and bytecode verification has completed successfully.**
27-02-2025