Implement a memory invalidation pass for jvm_verify

[brianhuffman]

This is analogous to what was done for LLVM in #549, and prevents unsoundness caused by executing overrides with incomplete specs.

Fixes #900.

Note that this PR does not implement all the features exactly as they were discussed in the comment thread for #900: Currently, fields without points-to declarations in the post-state section are invalidated, rather than asserted to be equal to their initial values. The plan is to implement that feature separately, by having the same setup spec translate to a slightly different MethodSpec value when post-state points-to declarations are absent.

[brianhuffman]

It's likely that this PR in its current state will horribly break the ECDSA proof. If that's the case, then I should probably implement the additional features discussed in the #900 thread before merging this PR. I'll keep this in draft state until I know whether that will be necessary.

[brianhuffman]

The CI results show everything as passing, yet on my local repo ecdsa.saw fails somewhere in the middle (while verifying method sq). I thought that CI was running ecdsa.saw, so what's going on here?

[RyanGlScott]

It looks like test_ecdsa is specifically being excluded from CI :\

saw-script/.github/ci.sh

Line 171 in 9d812c9

for t in test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done

[brianhuffman]

It looks like I was mistaken: ecdsa.saw (which is run by the test_ecdsa integration test) is specifically excluded from CI for some reason.

saw-script/.github/ci.sh

Line 171 in 9d812c9

for t in test0019_jss_switch_statement test_crucible_jvm test_ecdsa test_issue108 test_tutorial1 test_tutorial2 test_tutorial_w4; do echo $t >> disabled_tests.txt; done

This kind of defeats the purpose of PR #932 and means that issue #901 is not really fixed.

[brianhuffman]

I've now opened #1070 to see if we can re-enable all the integration tests that were disabled in CI without explanation.

[brianhuffman]

Instead of doing an invalidation pass, I think we're going to want to implement per-field write permission bits in the crucible-jvm memory model. The explicit user-provided frame conditions required by this PR are just too onerous, and yield overrides that are not as generally applicable as we want.

[brianhuffman]

A memory invalidation pass is not the approach we want to take to fix this problem; we instead want to implement write permissions in the crucible-jvm memory model.