Progress can exceed 100%

[rayman2000]

See This occurred when editing a file that was currently being verified. It is not reproducible yet.

[rayman2000]

Due to the "Verification of" and the progress bar, this is almost certainly a broken progress update (and not a broken finished or abort update). The number is formatted here: https://github.com/viperproject/viper-ide/blob/197805c348e3ba3442334d9183f59fe1db463bf6/client/src/Helper.ts#L55-L58 The formatting helper checks for below 0 but not above 100. Seem like ideally neither would ever get to here.

[rayman2000]

formatProgress is called from updateProgressLabel, which is called from here:

https://github.com/viperproject/viper-ide/blob/197805c348e3ba3442334d9183f59fe1db463bf6/client/src/Log.ts#L149-L158

We either use the provided data.progress or data.current / data.total if data.progress does not exist. data.current and data.total are never set in any caller, so data.progress must be set incorrectly. data.progress is always the return value of getProgress.

https://github.com/viperproject/viper-ide/blob/197805c348e3ba3442334d9183f59fe1db463bf6/client/src/VerificationController.ts#L623-L650

If we assign to progress here, then we are below 100. So the input must already be wrong and the timing is also messed up so that we do not reassign.

[rayman2000]

We call getProgress either with lastProgress (which is only set in getProgress, so can not be the origin of a too high number) or by the params in a StateChangeParams. So it looks like we can only get a number over 100 from ViperServer, we can not produce it in the IDE and we additionally need the timing stuff to be such that progress is not assigned to in getProgress.

[rayman2000]

Progress is updated in ProgressCoordinator. In theory, it might be possible to receive too many BackendOutputs, making current go higher than total. Strangely, updateProgress is only ever called with BackendOutputType.FunctionVerified.

[rayman2000]

Important interlude:

A Sink that materializes into a Publisher

[rayman2000]

It looks like a ProgressCoordinator is unique per FileManager, not per RelayActor. So if a new verification task is started, it will overwrite the progress coordinator, which may still receive EntitySuccessMessages from the original verification task. We can hopefully fix this by moving the progress coordinator into the relay actor instead of the file manager, but unless we can reproduce the error, it is hard to be sure that this actually solves the problem.

[rayman2000]

There is an easy fix: just force the output of progress to be <100, setting it to 99 if necessary. This will fix the display of the IDE, but not the underlying problem. Since the problem seems to be exceedingly rare, I do not think we should do this.

[sakehl]

It looks like a ProgressCoordinator is unique per FileManager, not per RelayActor. So if a new verification task is started, it will overwrite the progress coordinator, which may still receive EntitySuccessMessages from the original verification task. We can hopefully fix this by moving the progress coordinator into the relay actor instead of the file manager, but unless we can reproduce the error, it is hard to be sure that this actually solves the problem.

I got a file where this seems to be consistently happening. At least at my end it stays stuck on 102%.

SubDirectionHalide-0.vpr.txt

I've seen it more often as well.

[rayman2000]

@sakehl

So for me this file times out at 99% (I may need beefier hardware). Does this also happen the first time you verify a file after reloading or only in later attempts? Our current assumption is something to do with caching, but if it happens the first time then it is probably something else.

[sakehl]

When I loaded the file as new I immediately got this. So the first time.

This is the output of `Viper` in VS Code

``` 00:00.048 The ViperIDE is starting up. 00:00.049 The current version of Viper is: v.4.3.1 00:00.052 The logFile is located at: "/tmp/.vscode/viper (1).log" 00:00.870 - Java home found: /usr/lib/jvm/java-17-openjdk-amd64/bin/java. It's version is: openjdk version "17.0.10" 2024-01-16 OpenJDK Runtime Environment (build 17.0.10+7-Ubuntu-122.04.1) OpenJDK 64-Bit Server VM (build 17.0.10+7-Ubuntu-122.04.1, mixed mode, sharing) 00:01.171 - Spawning ViperServer with "/usr/lib/jvm/java-17-openjdk-amd64/bin/java" -Xmx2048m -Xss128m -cp :"/home/lars/.config/Code/User/globalStorage/viper-admin.viper/Nightly/ViperTools/backends/viperserver.jar" -server viper.server.ViperServerRunner --serverMode LSP --singleClient --backendSpecificCache --logLevel DEBUG --logFile "/tmp/.vscode/viperserver.log" 00:01.200 - ViperServer has been spawned and has PID 13630 00:03.369 Connected to ViperServer 00:03.830 it's not a viper file 00:03.831 Viper IDE is now active. 1:06:36.810 Active viper file changed to test.vpr 1:06:36.892 - Request verification for test.vpr 1:06:36.996 Received state change. 1:06:36.996 Changed FROM Stopped TO: VerificationRunning 1:06:39.809 Received non-standard ViperServer message of type copyright_report. 1:06:39.809 Received non-standard ViperServer message of type warnings_during_parsing. 1:06:39.809 Received non-standard ViperServer message of type ast_construction_result. 1:06:39.810 Received state change. 1:06:39.810 Changed FROM VerificationRunning TO: VerificationRunning 1:06:39.812 Received non-standard ViperServer message of type copyright_report. 1:06:39.865 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.875 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.933 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.935 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.936 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.938 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.939 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.941 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.942 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.944 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.944 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.946 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.946 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.948 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.949 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.951 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.951 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.953 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.953 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.955 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.956 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.958 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.959 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.961 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.962 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.963 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.964 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.966 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.966 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.968 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.969 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.971 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.971 Received non-standard ViperServer message of type configuration_confirmation. 1:06:39.973 Received non-standard ViperServer message of type configuration_confirmation. 1:06:40.839 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.840 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.842 Received non-standard ViperServer message of type warnings_during_typechecking. 1:06:40.843 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.843 Received non-standard ViperServer message of type warnings_during_typechecking. 1:06:40.843 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.844 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.844 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.844 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.845 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.845 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.852 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.852 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.853 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.853 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.853 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.854 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.855 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.856 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.856 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.857 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.857 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.858 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.864 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.864 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.865 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.866 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.866 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.867 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.876 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.877 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.877 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.877 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.878 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.879 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.879 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.880 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.880 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.881 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.881 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.881 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.882 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.882 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.883 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.883 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.884 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.884 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.885 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.885 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.886 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.886 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.886 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.886 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.887 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.887 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.888 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.888 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.889 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.889 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.889 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.889 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.890 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.890 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.890 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.890 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.891 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.891 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.891 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.892 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.892 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.892 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.893 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.893 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.893 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.894 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.894 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:40.894 Received non-standard ViperServer message of type quantifier_chosen_triggers_message. 1:06:42.235 Received state change. 1:06:42.235 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.277 Received state change. 1:06:42.277 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.292 Received state change. 1:06:42.292 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.297 Received state change. 1:06:42.297 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.307 Received state change. 1:06:42.307 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.308 Received state change. 1:06:42.308 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.311 Received state change. 1:06:42.311 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.317 Received state change. 1:06:42.317 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.319 Received state change. 1:06:42.319 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.324 Received state change. 1:06:42.324 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.328 Received state change. 1:06:42.328 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.333 Received state change. 1:06:42.334 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.352 Received state change. 1:06:42.352 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.352 Received state change. 1:06:42.352 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.366 Received state change. 1:06:42.366 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.367 Received state change. 1:06:42.367 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.375 Received state change. 1:06:42.375 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.380 Received state change. 1:06:42.380 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.404 Received state change. 1:06:42.404 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.405 Received state change. 1:06:42.405 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.407 Received state change. 1:06:42.407 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.439 Received state change. 1:06:42.439 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.441 Received state change. 1:06:42.441 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.460 Received state change. 1:06:42.460 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.460 Received state change. 1:06:42.460 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.470 Received state change. 1:06:42.470 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.475 Received state change. 1:06:42.475 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.479 Received state change. 1:06:42.479 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.484 Received state change. 1:06:42.484 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.485 Received state change. 1:06:42.485 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.496 Received state change. 1:06:42.496 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.662 Received state change. 1:06:42.662 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.662 Received state change. 1:06:42.662 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.663 Received state change. 1:06:42.663 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.663 Received state change. 1:06:42.663 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.673 Received state change. 1:06:42.673 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.677 Received state change. 1:06:42.677 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.685 Received state change. 1:06:42.685 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.693 Received state change. 1:06:42.694 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.698 Received state change. 1:06:42.699 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.740 Received state change. 1:06:42.740 Changed FROM VerificationRunning TO: VerificationRunning 1:06:42.741 Received state change. 1:06:42.741 Changed FROM VerificationRunning TO: VerificationRunning 1:07:24.149 Active viper file changed to test.vpr ```

[sakehl]

I disabled caching and the same happens. This is what ViperServer output gives:

viperserver_output.txt

[rayman2000]

All right thank you! Just FYI, this is mostly just a visual glitch. Your program is very likely timing out on the backend, the IDE should be showing 99%. If this is blocking you somehow then maybe set the time-out up or look into matching loops or so. (Maybe this was already clear, I just wanted to make sure).