ViperServer is overwhelmed by a program that crashes Viper

[fpoli]

The following program crashes Silicon and Carbon with "java.lang.IllegalArgumentException: requirement failed". The issue that I'm reporting is that after verifying the program 3 times, the IDE stop reporting errors and the log says that the "ViperServer is overwhelmed". Updating Viper restores the IDE because that restarts the server, but it's not ideal.

domain HeapVersion {}

method Arc_clone(x: Ref, y: HeapVersion)
    requires Map[Ref, HeapVersion]()[x] == y

(A "Restart Viper server" command might be useful to workaround similar issues without having to redownload Viper.)

Full log after updating Viper:

Server: Updating Viper Tools ...
ERROR: Error checking Settings files: SyntaxError: Unexpected token } in JSON at position 2160
- Server: Java home found: /home/fpoli/opt/jvm-15/bin/java. It's version is: openjdk version "15.0.1" 2020-10-20
OpenJDK Runtime Environment Zulu15.28+51-CA (build 15.0.1+9)
OpenJDK 64-Bit Server VM Zulu15.28+51-CA (build 15.0.1+9, mixed mode, sharing)

Server: The settings are ok
Server: Change Backend: from carbon to silicon
ERROR: Error checking Settings files: SyntaxError: Unexpected token } in JSON at position 2160
- Server: Java home found: /home/fpoli/opt/jvm-15/bin/java. It's version is: openjdk version "15.0.1" 2020-10-20
OpenJDK Runtime Environment Zulu15.28+51-CA (build 15.0.1+9)
OpenJDK 64-Bit Server VM Zulu15.28+51-CA (build 15.0.1+9, mixed mode, sharing)

Server: The settings are ok
- Server: Java home found: /home/fpoli/opt/jvm-15/bin/java. It's version is: openjdk version "15.0.1" 2020-10-20
OpenJDK Runtime Environment Zulu15.28+51-CA (build 15.0.1+9)
OpenJDK 64-Bit Server VM Zulu15.28+51-CA (build 15.0.1+9, mixed mode, sharing)

Server: The backend is ready for verification
Reset all viper files
AutoVerify after backend change
Backend ready: silicon
- Request verification for 20220119_140839.vpr
Server: start or restart verification
Server: Abort running verification
Server: verify 20220119_140839.vpr
Server: silicon verification started
Received non-standard ViperServer message of type backend_configuration.
Server: Issue of severity 1: [silicon] [exception] 1:1 The verification job #0 resulted in a terrible error: java.util.concurrent.ExecutionException: viper.server.core.ServerCrashException: java.lang.IllegalArgumentException: requirement failed
Server: Number of Steps: 0
Verifying 20220119_140839.vpr failed after 0 seconds with 1 errors
- Request verification for 20220119_140839.vpr
Server: start or restart verification
Server: verify 20220119_140839.vpr
Server: silicon verification started
Received non-standard ViperServer message of type backend_configuration.
Server: Issue of severity 1: [silicon] [exception] 1:1 The verification job #1 resulted in a terrible error: java.util.concurrent.ExecutionException: viper.server.core.ServerCrashException: java.lang.IllegalArgumentException: requirement failed
Server: Number of Steps: 0
Verifying 20220119_140839.vpr failed after 0 seconds with 1 errors
- Request verification for 20220119_140839.vpr
Server: start or restart verification
Server: verify 20220119_140839.vpr
Server: silicon verification started
Received non-standard ViperServer message of type backend_configuration.
Server: Issue of severity 1: [silicon] [exception] 1:1 The verification job #2 resulted in a terrible error: java.util.concurrent.ExecutionException: viper.server.core.ServerCrashException: java.lang.IllegalArgumentException: requirement failed
Server: Number of Steps: 0
Verifying 20220119_140839.vpr failed after 0 seconds with 1 errors
Server: The backend is ready for verification
Reset all viper files
AutoVerify after backend change
Backend ready: carbon
- Request verification for 20220119_140839.vpr
Server: start or restart verification
Server: verify 20220119_140839.vpr
Server: carbon verification started
Received non-standard ViperServer message of type backend_configuration.
ERROR: Server: ViperServer is overwhelmed (ViperServer returned job ID -1). Try again in a few seconds.
- Request verification for 20220119_140839.vpr
Server: start or restart verification
Server: Abort running verification
Server: verify 20220119_140839.vpr
Server: carbon verification started
Received non-standard ViperServer message of type backend_configuration.
ERROR: Server: ViperServer is overwhelmed (ViperServer returned job ID -1). Try again in a few seconds.

[alexanderjsummers]

The same happens with viperproject/silver#569 - after three runs no output of any kind appears in the IDE ever again (the same message is visible in the console output if expected). This isn't easy to spot/diagnose; I'm also not sure why it happens. So we should consider (a) not having ViperServer stop responding, if possible, and (b) displaying a clear error message if we do need this behaviour

[JonasAlaif]

Sorry that I missed these silver issues @alexanderjsummers. viperproject/silver#575 should fix both of them. I agree that terrible error isn't a good thing to report; imo we should write that viperserver crashed and possibly tell the user to file a bug report in the relevant repo - we should be able to tell if it's a Silver/Carbon/... crash.

[ArquintL]

After @JonasAlaif's fix, it's somewhat hard to reproduce the issue.
However, I've verified a file three times that results in a StackOverflow exception in Silicon and it seems that the latest pre-release correctly handles such exceptions, i.e. cleans up state in ViperServer such that future verifications are possible.
Thus, I'm going to close the issue for now. Fixed by #113