Show minimum required time for successful proof

[treiher]

Is your feature request related to a problem? Please describe.
I want to improve the proof time for already known correct code. One way to achieve that is reducing the timeout to reduce wasting time on a prover which is unable to prove a certain VC. Unfortunately, the current output of SPAT does not allow getting the minimum required time easily. It may can be determined manually by using the details option, but that is quite tedious.

Here is an example of the current output:

RFLX.RFLX_Types.U64_Insert => 120.0 s/1.6 ks
`-VC_PRECONDITION rflx-rflx_generic_types.adb:221:39 => 120.0 s/491.0 s
 `-CVC4: 120.0 s (Timeout)
  -Z3: 120.0 s (Timeout)
  -altergo: 188.2 ms (Valid)
 `-Z3: 120.0 s (Timeout)
  -CVC4: 5.4 s (Valid)
 `-Z3: 120.0 s (Timeout)
  -CVC4: 5.3 s (Valid)
 `-Z3: 60.0 ms (Valid)
 `-Z3: 40.0 ms (Valid)
 `-Z3: 20.0 ms (Valid)
 `-Trivial: 0.0 s (Valid)

SPAT shows a very high maximum time used by a prover (120.0 s), while it cannot be seen easily that the required time could be reduced significantly when reducing the timeout (5.4 s + some buffer for the shown VC).

Describe the solution you'd like
It would be nice if the output could be extended by a value for the maximum time needed by any prover for a valid proof. For example:

RFLX.RFLX_Types.U64_Insert => 5.4 s/120.0 s/1.6 ks
`-VC_PRECONDITION rflx-rflx_generic_types.adb:221:39 => 5.4 s/120.0 s/491.0 s
[...]

It would be also helpful to be able to sort the output by this value, so that the maximum value for the whole project can be easily seen.

[Jellix]

Good suggestion.

Just to make sure: I am assuming you used the --report-mode=failed option already, so that only proofs with failed proof attempts are shown?

Also, related to #26.

[treiher]

Just to make sure: I am assuming you used the --report-mode=failed option already, so that only proofs with failed proof attempts are shown?

Yes, --report-mode=failed is already a nice way to narrow it down to the problematic parts. Actually, changing the order of the provers helped a lot in the example shown above.

[Jellix]

@treiher I just released version v0.9.5-pre, if you could kindly try out the new feature and see if it works for you? I'm aware there are still some rough edges.

[treiher]

It works fine for me in v0.9.5-pre. Thanks for adding! Do you plan to add the value also to the summary? I think it would make sense to have it there as well.

BTW: I first tried the current version on master (d494d06), but this led to a constrained error:

$ run_spat -Ptest.gpr -ct -rf

raised CONSTRAINT_ERROR : spat-proof_attempt.adb:64 range check failed

[Jellix]

It works fine for me in v0.9.5-pre. Thanks for adding! Do you plan to add the value also to the summary?

I see what I can do.

BTW: I first tried the current version on master (d494d06), but this led to a constrained error:

$ run_spat -Ptest.gpr -ct -rf

raised CONSTRAINT_ERROR : spat-proof_attempt.adb:64 range check failed

Assuming there was just a test.adb in that project, would you by any chance be able to provide the test.spark file? If I am not mistaken, that constraint error would indicate that the number of steps reported there was more than 2 billion (i.e. exceeding the range of Natural). Guess, I should use a 64 bit integer for that, anyway.

[treiher]

Here is the relevant file: rflx-rflx_types.spark

[Jellix]

Here is the relevant file: rflx-rflx_types.spark

Thanks. Almost as suspected, but not quite.

"Z3": {
  "result": "Out Of Memory",
  "steps": -1,
  "time": 9.51000000000000E+00
}

A negative step value. I must admit, I did not anticipate that.

[senier]

"Z3": {
  "result": "Out Of Memory",
  "steps": -1,
  "time": 9.51000000000000E+00
}

A negative step value. I must admit, I did not anticipate that.

This could be useful input for yet another optimization criterion, as it may indicate that you should increase your --memlimit parameter.

[Jellix]

FWIW, the maximum time for successful proof and maximum time for single proof are now also shown in the summary (#39).

I close this one for now, feel free to open a new issue, if you find something.

New pre-release upcoming.