Remove deprecated java commands

[brianhuffman]

This removes all the deprecated java-related commands, and also removes the dependency on the jvm-verifier package.

Fixes #993.

[brianhuffman]

As yet I have not removed the integration tests that use the old java verification commands. I wasn't sure whether they should just be removed, or maybe we should instead update them all to use the new verification commands instead.

Broken tests include test0001, test_ecdsa, and test_examples.

Which reminds me, I suppose I should also remove the old-style ecdsa proof, and rename ecdsa-crucible.saw to just ecdsa.saw.

[atomb]

Thanks for doing this! As you suggest, I think I'd like to have those broken tests updated to use the Crucible alternatives if possible before merging. In cases where that really doesn't make sense, though, perhaps we can just remove them.

[brianhuffman]

I tried adapting test0001 to use the new JVM verification commands, and I ran into the following error message:

resolveSAWTerm: unimplemented type char (FIXME)

Apparently we haven't needed to use any 8-bit integers in any of our more recent examples. It should be pretty easy to fix this. But as it's kind of orthogonal, maybe that fix should go into a separate PR.

[atomb]

Yeah, that makes sense to me.

[brianhuffman]

I have a fix for the "unimplemented type char" error in #1008. We should get that PR merged before this one; then I can update the test0001 to use the new-style verification commands at the same time.

[brianhuffman]

After merging #1008 I took another look at test0001, which looks like it's supposed to be verifying a Java implementation of MD5 against a cryptol spec. I can convert the setup block to the form jvm_verify expects, but then it doesn't work (using quickcheck as a tactic finds a counterexample right away).

I realized that the original test actually doesn't specify any tactic to use (there is no java_verify_tactic declaration) and in that case the java_verify command just silently skips the proof (it does symbolic simulation only). If I add a java_verify_tactic declaration that just does print_goal followed by assume_unsat, the test works, but the first goal is just the constant False.

So it seems like this purported "test" is actually completely bogus. Maybe the spec was actually correct at one time, and the proof used to actually work, and then there was a regression that we never noticed because the test doesn't run the proof? Or maybe the spec was always wrong? I don't know! There are no comments at all in the test script. I don't even know what this test is really supposed to test. I'm not sure what I should do about it.

@atomb: It looks like you were the last person to edit the proof script (dd7121b and ae78026). Do you remember anything about this?

[atomb]

Oh, nice! :-P It's been a while, so I don't remember much about that example. It would be nice to have at least one non-trivial test beyond the ECDSA one, though. I wonder what it looks like using jvm_extract, as the original version used. My suspicion is that it's something to do with byte or bit ordering, but that's just a hunch.

[brianhuffman]

It sounds like it would be worthwhile to resurrect that test case and verify that MD5 algorithm with the new jvm verification commands. I'll open a ticket for that and get to work on it.

[atomb]

Thanks, @brianhuffman!

[brianhuffman]

This PR is waiting on #1011 to get merged first.

[brianhuffman]

It looks like test0023_java_assert_false is still using the old java_verify command and needs to be updated.

Subdirectories examples/ecdsa and examples/java also contain proofs with java_verify, which also need to be updated.

[brianhuffman]

#1011 and #1028 have both been merged now. So the remaining examples still using the old java commands are examples/ecdsa (which already has been ported to use the new commands, so we should just remove the old one and rename ecdsa-crucible.saw to ecdsa.saw) and test0023_java_assert_false.

[brianhuffman]

I was suprised to see that the CI shows integration test test0023_java_assert_false as passing, even when the commands it tries to run have been removed! It turns out that this is an expected-failure test, but instead of using the fails combinator, it actually has a test.sh that checks the exit code from saw to ensure that test.saw fails. It just can't tell whether the verification failed, or whether the verification command just didn't exist.

I'm making a patch now that will update test0023 to use jvm_verify, to and also make it use the fails combinator, so that it won't need the funny shell script that flips the exit code.

[atomb]

Yeah, using the fails function is a much better solution than checking the exit code in the shell. I'm glad we have it now!

[atomb]

It is very satisfying to see this much code going away. :)