Cache does not seem to be initialized

[oeb25]

When using the HTTP server I get java.lang.NullPointerException: Cannot invoke "scala.Option.foreach(scala.Function1)" because the return value of "viper.server.core.ViperCache$._cacheFile()" is null as the last event after calling /verify/0 using the Silicon backend.

I tried to look into it and the ViperCache.initialize does not seem to be called at any point in the execution. It seems this should have been called by ViperCoreServer.start which maybe should have been called by ViperHttpServer.start. I've verified that ViperHttpServer.start is called, and it calls super.start so I would have thought that this called ViperCoreServer.start since it extends from it? I don't know Scala so this might all be incorrect :)

Minimal reproduction

The following bash script triggers the issue. It assumes z3 is in the PATH and VIPERSERVER should probably be changed to point to the correct JAR.

#!/bin/bash

set -xe

trap 'kill $(jobs -p)' EXIT

VIPERSERVER=target/scala-*/viperserver.jar
export Z3_EXE=$(which z3)

echo "method a() ensures true {}" > tiny.vpr
TINY_FILE=$(realpath tiny.vpr)

java -jar $VIPERSERVER --port 56644 &

sleep 2

curl --location --request POST "http://localhost:56644/verify" \
    --header 'Content-Type: application/json' \
    --data-raw "{\"arg\": \"silicon $TINY_FILE\"}"

sleep 2

curl --location --request GET 'http://localhost:56644/verify/0'

The verification succeeds as expected:

{
  "msg_body": {
    "details": {
      "cached": false,
      "entity": {
        "name": "a",
        "position": {
          "end": "1:27",
          "file": "tiny.vpr",
          "start": "1:1"
        },
        "type": "method"
      },
      "time": 29
    },
    "kind": "for_entity",
    "status": "success",
    "verifier": "silicon"
  },
  "msg_type": "verification_result"
}

But the final message returned is the NullPointerException:

{
  "msg_body": {
    "message": "java.lang.NullPointerException: Cannot invoke \"scala.Option.foreach(scala.Function1)\" because the return value of \"viper.server.core.ViperCache$._cacheFile()\" is null",
    "stacktrace": [
      "viper.server.core.ViperCache$.writeToFile(ViperCache.scala:282)",
      "viper.server.core.ViperBackend.postCaching(VerificationWorker.scala:301)",
      "viper.server.core.ViperBackend.$anonfun$execute$4(VerificationWorker.scala:154)",
      "scala.util.Either.map(Either.scala:382)",
      "viper.server.core.ViperBackend.$anonfun$execute$3(VerificationWorker.scala:153)",
      "scala.util.Either.flatMap(Either.scala:352)",
      "viper.server.core.ViperBackend.$anonfun$execute$1(VerificationWorker.scala:151)",
      "scala.util.Either.flatMap(Either.scala:352)",
      "viper.server.core.ViperBackend.execute(VerificationWorker.scala:150)",
      "viper.server.core.VerificationWorker.run(VerificationWorker.scala:65)",
      "viper.server.core.VerificationWorker.call(VerificationWorker.scala:106)",
      "viper.server.core.VerificationWorker.call(VerificationWorker.scala:30)",
      "java.base/java.util.concurrent.FutureTask.run(FutureTask.java:317)",
      "java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)",
      "java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)",
      "java.base/java.lang.Thread.run(Thread.java:1589)"
    ]
  },
  "msg_type": "exception_report"
}

The issue is still there with --cacheFile set on the call to viperserver.jar.

[ArquintL]

Thanks a lot for this very detailed and reproducible bug report! While I've just created a PR fixing this issue, you can use the following command as a workaround with your current ViperServer JAR:

curl --location --request POST "http://localhost:56644/verify" \
    --header 'Content-Type: application/json' \
    --data-raw "{\"arg\": \"silicon --disableCaching $TINY_FILE\"}"

[oeb25]

This is great thanks! Just checked with the latest master, and it no longer produces an exception!

Thank you :)