Details

    • Type: New Feature
    • Status: Open
    • Priority: Medium
    • Resolution: Unresolved
    • Affects Version/s: None
    • Fix Version/s: 1000
    • Component/s: Runtime
    • Labels:
      None

      Description

      We should introduce a byte code verifier. This should ideally support the verification of class files with versions up to 1.7 and it should support the alternative verification mechanism introduced in JSR 202.

      One alternative is to use verifiers from other projects such as justice from BCEL. Note that we cannot use GPL code (e.g. from Maxine) because the GPL is not compatible with our license (the Eclipse Public License).

        Gliffy Diagrams

          Attachments

            Issue Links

              Activity

              Hide
              pdonald Peter Donald added a comment -

              Ideally any verifier we use would be capable of being extended to add custom intra-procedural verification rules and possibly even add inter-procedure linking constraints.

              i.e. For intra-procedural constraints we could add rules to ensure;

              • @Unpreemtible functions do not contain any "illegal" opcodes
              • @Pure functions do not not contain any mutator opcodes.
              • null is never assigned to a @Unboxed value
              • @Unboxed values never cast

              For inter-procedural constraints we could add rules like

              • @Unpreemtible functions can only call @Unpreemtible methods or equiv
              • @Pure functions can only call @Pure functions

              In the future we could also add all sorts of annotations and verify them. (Using Haskells naming mechanisms)

              • @IO procedure has side-effects and can only call @IO or @Pure
              • @STM procedure is a software transactional procedure and can only call @Pure or @STM
              • @STM_RO is a read-only STM and can only call @Pure or @STM_RO

              We could also use the "verifier" to automagically classify different procedures as @IO, @Pure, @STM etc which would simplify the compiler and enable many more optimizations with relatively minimal overhead (as data flow analysis already donw within verifier).

              Show
              pdonald Peter Donald added a comment - Ideally any verifier we use would be capable of being extended to add custom intra-procedural verification rules and possibly even add inter-procedure linking constraints. i.e. For intra-procedural constraints we could add rules to ensure; @Unpreemtible functions do not contain any "illegal" opcodes @Pure functions do not not contain any mutator opcodes. null is never assigned to a @Unboxed value @Unboxed values never cast For inter-procedural constraints we could add rules like @Unpreemtible functions can only call @Unpreemtible methods or equiv @Pure functions can only call @Pure functions In the future we could also add all sorts of annotations and verify them. (Using Haskells naming mechanisms) @IO procedure has side-effects and can only call @IO or @Pure @STM procedure is a software transactional procedure and can only call @Pure or @STM @STM_RO is a read-only STM and can only call @Pure or @STM_RO We could also use the "verifier" to automagically classify different procedures as @IO, @Pure, @STM etc which would simplify the compiler and enable many more optimizations with relatively minimal overhead (as data flow analysis already donw within verifier).

                People

                • Assignee:
                  Unassigned
                  Reporter:
                  pdonald Peter Donald
                • Votes:
                  0 Vote for this issue
                  Watchers:
                  0 Start watching this issue

                  Dates

                  • Created:
                    Updated: