[JVM] examples/ecdsa.saw slows on first run and fails to verify signHash for OpenJDK 9+

[WeeknightMVP]

On my first run of examples/ecdsa/ecdsa.saw in an Ubuntu 18.04 workspace with OpenJDK 17, set_unit required about 22m29s to verify, and signHash failed while looking for char[] value in class java/lang/Object:

saw-script/examples/ecdsa$ javac --version
javac 17.0.5
saw-script/examples/ecdsa$ readlink -f $(which javac)
/usr/lib/jvm/java-17-openjdk-amd64/bin/javac
saw-script/examples/ecdsa$ make verify
mkdir -p build
javac -g -cp src src/com/galois/ecc/*.java -d build
javac -g -cp build:tests tests/com/galois/ecc/*.java -d build
../../bin/saw -c build ecdsa.saw



[23:26:33.979] Loading file ".../saw-script/examples/ecdsa/ecdsa.saw"
[warning] at cryptol-spec/bv.cry:33:9--33:12
    This binding for `sum` shadows the existing binding at
    Cryptol:1158:1--1158:4



[warning] at cryptol-spec/ref_ec_mul.cry:96:13--96:16
    This binding for `abs` shadows the existing binding at
    Cryptol:605:1--605:4


[warning] at cryptol-spec/p384_ec_mul.cry:20:13--20:16
    This binding for `sum` shadows the existing binding at
    Cryptol:1158:1--1158:4

[warning] at cryptol-spec/ecc.cry:119:5--119:8
    This binding for `sum` shadows the existing binding at
    Cryptol:1158:1--1158:4

[23:26:35.237] Proving and registering rewrite rules.
[23:26:35.964] WARNING: admitting goal prove_print
[23:26:36.019] WARNING: admitting goal prove_print
[23:26:43.970] Performing verification.
[23:26:43.971] Verifying set_unit
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[23:49:13.012] Proof succeeded! set_unit
[23:49:13.012] Time: 1349.041570434s

...

[23:56:17.909] Verifying signHash
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[23:57:21.261] resolveField: Field FieldId {fieldIdClass = ClassName "java/lang/Object", fieldIdName = "value", fieldIdType = char[]} not found
CallStack (from HasCallStack):
  error, called at src/Lang/Crucible/JVM/Translation/Monad.hs:61:15 in crucible-jvm-0.2-inplace:Lang.Crucible.JVM.Translation.Monad
  jvmFail, called at src/Lang/Crucible/JVM/Translation/Class.hs:843:23 in crucible-jvm-0.2-inplace:Lang.Crucible.JVM.Translation.Class
Makefile:31: recipe for target 'verify' failed
make: *** [verify] Error 2

Suspecting these might have something to do with Jigsaw (Open/JDK 9+), I adapted Makefile to use a JAVA_BIN environment variable... (Note that this might not be portable to other platforms.) (Also note that the signHash failure is probably an instance of a known issue that remains open. The first run slowness might be known too, but I don't see a related issue.)

JAVA_BIN?=$(shell readlink -f $(shell which javac) | sed "s:/javac::")
JAR=${JAVA_BIN}/jar
JAVA=${JAVA_BIN}/java
JAVAC=${JAVA_BIN}/javac
JAVADOC=${JAVA_BIN}/javadoc

SAW?=../../bin/saw

all : build

build : build/com/galois/ecc/ECCProvider.class

# Create Java class files
build/com/galois/ecc/ECCProvider.class :
        mkdir -p build
        ${JAVAC} -g -cp src src/com/galois/ecc/*.java -d build
        ${JAVAC} -g -cp build:tests tests/com/galois/ecc/*.java -d build

# Build Javadoc documentation.
doc :
        ${JAVADOC} -classpath src -d doc -public src/com/galois/ecc/*

# Clean up generated files
clean :
        rm -rf doc build

# Run Java with 64bit data (much faster).
run64 :
        ${JAVA} -cp build -d64 com.galois.ecc.ECC


ecdsa.jar: build
        cd build && ${JAR} -cf ../ecdsa.jar com

# Run the SAWScript verification
verify : build
        ${SAW} -c build ecdsa.saw

.PHONY : build clean doc run32 run64 verify

...and reran the script after specifying OpenJDK 8, which still failed:

saw-script/examples/ecdsa$ export JAVA_BIN=$(readlink -f $(which javac) | sed "s:-17-:-8-:" | sed "s:/javac::")
saw-script/examples/ecdsa$ echo $JAVA_BIN
/usr/lib/jvm/java-8-openjdk-amd64/bin
saw-script/examples/ecdsa$ make clean
rm -rf doc build
saw-script/examples/ecdsa$ make verify
mkdir -p build
/usr/lib/jvm/java-8-openjdk-amd64/bin/javac -g -cp src src/com/galois/ecc/*.java -d build
/usr/lib/jvm/java-8-openjdk-amd64/bin/javac -g -cp build:tests tests/com/galois/ecc/*.java -d build
../../bin/saw -c build ecdsa.saw
[20:42:40.862] Loading file ".../saw-script/examples/ecdsa/ecdsa.saw"
{same warnings}
...
[20:42:50.838] Verifying set_unit
...
[20:42:56.103] Proof succeeded! set_unit
[20:42:56.103] Time: 5.264830342s
...
[20:49:59.638] Verifying signHash
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[20:51:04.478] resolveField: Field FieldId {fieldIdClass = ClassName "java/lang/Object", fieldIdName = "value", fieldIdType = char[]} not found
CallStack (from HasCallStack):
  error, called at src/Lang/Crucible/JVM/Translation/Monad.hs:61:15 in crucible-jvm-0.2-inplace:Lang.Crucible.JVM.Translation.Monad
  jvmFail, called at src/Lang/Crucible/JVM/Translation/Class.hs:843:23 in crucible-jvm-0.2-inplace:Lang.Crucible.JVM.Translation.Class
Makefile:37: recipe for target 'verify' failed
make: *** [verify] Error 2

From here, I adapted Makefile to specify -b $JAVA_BIN for SAW...

# ...
# Run the SAWScript verification
verify : build
        ${SAW} -b ${JAVA_BIN} -c build ecdsa.saw

..and reran the script, which succeeded this time:

saw-script/examples/ecdsa$ make clean
rm -rf doc build
saw-script/examples/ecdsa$ make verify
mkdir -p build
/usr/lib/jvm/java-8-openjdk-amd64/bin/javac -g -cp src src/com/galois/ecc/*.java -d build
/usr/lib/jvm/java-8-openjdk-amd64/bin/javac -g -cp build:tests tests/com/galois/ecc/*.java -d build
../../bin/saw -c build ecdsa.saw
...
[21:01:30.030] Verifying signHash
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[21:02:41.956] Symbolic simulation completed with side conditions.
[21:02:55.200] Proof succeeded! signHash
[21:02:55.200] Time: 85.170231328s

[21:02:55.206] Verifying verifySignature
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[21:03:13.456] Proof succeeded! verifySignature
[21:03:13.456] Time: 18.249645484s

[21:03:13.456] Done.

I tried one more time with OpenJDK 17, which verified set_unit much more quickly (~5.17s), but failed to verify signHash for the same reason:

saw-script/examples/ecdsa$ export JAVA_BIN=$(readlink -f $(which javac) | sed "s:/javac::")
saw-script/examples/ecdsa$ echo $JAVA_BIN
/usr/lib/jvm/java-17-openjdk-amd64/bin
saw-script/examples/ecdsa$ make clean
rm -rf doc build
saw-script/examples/ecdsa$ make verify
mkdir -p build
mkdir -p build
/usr/lib/jvm/java-17-openjdk-amd64/bin/javac -g -cp src src/com/galois/ecc/*.java -d build
/usr/lib/jvm/java-17-openjdk-amd64/bin/javac -g -cp build:tests tests/com/galois/ecc/*.java -d build
../../bin/saw -b /usr/lib/jvm/java-17-openjdk-amd64/bin -c build ecdsa.saw
...
[21:08:46.327] Performing verification.
[21:08:46.328] Verifying set_unit
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[21:08:51.501] Proof succeeded! set_unit
[21:08:51.501] Time: 5.172725269s
...
[21:15:54.039] Verifying signHash
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[21:17:02.090] resolveField: Field FieldId {fieldIdClass = ClassName "java/lang/Object", fieldIdName = "value", fieldIdType = char[]} not found
CallStack (from HasCallStack):
  error, called at src/Lang/Crucible/JVM/Translation/Monad.hs:61:15 in crucible-jvm-0.2-inplace:Lang.Crucible.JVM.Translation.Monad
  jvmFail, called at src/Lang/Crucible/JVM/Translation/Class.hs:843:23 in crucible-jvm-0.2-inplace:Lang.Crucible.JVM.Translation.Class
Makefile:37: recipe for target 'verify' failed
make: *** [verify] Error 2

I installed OpenJDK 11 and tried again, slowing on the first run and failing in the same way as for OpenJDK 17 (again probably because of crucible#641).

[RyanGlScott]

This is a combination of two issues:

• crucible-jvm takes a long time to extract all of the classes it needs from JDK9+. (On subsequent invocations, all of the classes are cached, but the first extraction of each class is quite slow.) This is a Crucible issue, not a SAW one, so I have opened Long crucible-jvm initial startup times with JDK9+ crucible#1060 to track this.
• As you have pointed out, our experimental JDK9+ support simply doesn't work for the String class at the moment. See crucible-jvm: Investigate bugs when verifying JDK 9+ code that uses String crucible#641.