Remove dependency on jvm-verifier #993
Comments
|
I've found myself needing to change code in I was initially hopeful that I could get away with only replacing a small subset of |
|
One approach would be to start by removing all the deprecated |
|
#1005 removes the dependency of the |
|
Plan: Remove JSS tests, and move jar files into saw repo examples directory. |
This allows SAW to deal with JDK 9 or later, which packages its standard library not in a JAR file, but in a JIMAGE file. Extracting `.class` files from JIMAGE files proves to be surprisingly tricky, and I've carefully documented the intricacies of doing so in `Note [Loading classes from JIMAGE files]` in `SAWScript.JavaCodebase`. This fixes #861. This depends on #1030 to work. Remaining tasks: * Ideally, the code in `SAWScript.JavaCodebase` would be upstreamed to `crucible-jvm`, where the all-important `Codebase` data type lives. Unfortunately, some parts of SAW (e.g., `java_verify` still rely on the `jvm-verifier` library, which defines a separate `Codebase` type. SAW is in the process of phasing out the use of `jvm-verifier` in favor of `crucible-jvm` (see #993), but until that happens, I needed to introduce some ugly hacks in order to make everything typecheck. In particular, the (hopefully temporary) `SAWScript.JavaCodebase` module defines a shim version of `Codebase` that puts the experimental new things that I added in an `ExperimentalCodebase` constructor, but preserving the ability to use the `jvm-verifier` version of `Codebase` in the `LegacyCodebase` constructor. If JDK 8 or earlier is used, then `LegacyCodebase` is chosen, and if JDK 9 or later is used, then `ExperimentalCodebase` is chosen. * Unfortunately, `java_verify` doesn't work with `ExperimentalCodebase`. Nor would we necessarily want to make this happen, as that would require upstreaming changes to `jvm-verifier`, which we are in the process of phasing out. As a result, this is blocked on #993. * The CI should be updated to test more versions of the JDK than just 8. Other things: * I removed the dependency on the `xdg-basedir`, as it was unused. This dependency was likely added quite some time ago, and it appears that `saw-script` switched over to using XDG-related functionality from the `directory` library since then. I opted to use `directory` to find the `.cache` directory as well, so I have made that clear in the `.cabal` file.
This allows SAW to deal with JDK 9 or later, which packages its standard library not in a JAR file, but in a JIMAGE file. Extracting `.class` files from JIMAGE files proves to be surprisingly tricky, and I've carefully documented the intricacies of doing so in `Note [Loading classes from JIMAGE files]` in `SAWScript.JavaCodebase`. This fixes #861. Remaining tasks: * Ideally, the code in `SAWScript.JavaCodebase` would be upstreamed to `crucible-jvm`, where the all-important `Codebase` data type lives. Unfortunately, some parts of SAW (e.g., `java_verify` still rely on the `jvm-verifier` library, which defines a separate `Codebase` type. SAW is in the process of phasing out the use of `jvm-verifier` in favor of `crucible-jvm` (see #993), but until that happens, I needed to introduce some ugly hacks in order to make everything typecheck. In particular, the (hopefully temporary) `SAWScript.JavaCodebase` module defines a shim version of `Codebase` that puts the experimental new things that I added in an `ExperimentalCodebase` constructor, but preserving the ability to use the `jvm-verifier` version of `Codebase` in the `LegacyCodebase` constructor. If JDK 8 or earlier is used, then `LegacyCodebase` is chosen, and if JDK 9 or later is used, then `ExperimentalCodebase` is chosen. * Unfortunately, `java_verify` doesn't work with `ExperimentalCodebase`. Nor would we necessarily want to make this happen, as that would require upstreaming changes to `jvm-verifier`, which we are in the process of phasing out. As a result, this is blocked on #993. * The CI should be updated to test more versions of the JDK than just 8. Other things: * I removed the dependency on the `xdg-basedir`, as it was unused. This dependency was likely added quite some time ago, and it appears that `saw-script` switched over to using XDG-related functionality from the `directory` library since then. I opted to use `directory` to find the `.cache` directory as well, so I have made that clear in the `.cabal` file.
Now that Crucible-based Java verification has better functionality and reasonable performance relative to
jvm-verifier(e.g., see #399), it's getting close to time to cut the dependency onjvm-verifier.The text was updated successfully, but these errors were encountered: