Improve time of verification checks in CI

[treiher]

Even with the introduced caching (#122) the verification checks take too much time. All of the last successful CI runs took more then one hour. (Does the caching even work at the moment?)

Currently we run the verification on a set of real-world protocol messages and some artificial test cases. An better approach could be to replace the current tests by a smaller subset which ideally still covers most of all potential cases. I think one (or a small number of) artificial message(s) could be enough to get a good coverage and reduce the needed verification time significantly. All currently used test cases could be still run in the nightly tests.

[treiher]

The currently used caching seems to work only partially. Here is a small excerpt of the proof results analyzed by SPAT. Lines with "0.0 s/0.0 s/0.0 s" indicate parts which were not verified again.

[...]
RFLX.TLV.Message.Get_Length             => 50.0 ms/50.0 ms/130.0 ms
RFLX.TLV.Message.Get_Tag                => 40.0 ms/40.0 ms/80.0 ms
RFLX.TLV.Message.Has_Buffer             => 0.0 s/0.0 s/0.0 s
RFLX.TLV.Message.Incomplete             => 0.0 s/0.0 s/0.0 s
RFLX.TLV.Message.Incomplete_Message     => 0.0 s/0.0 s/0.0 s
RFLX.TLV.Message.Initialize             => 50.0 ms/50.0 ms/670.0 ms
RFLX.TLV.Message.Initialize_Value       => 70.0 ms/70.0 ms/1.0 s
RFLX.TLV.Message.Initialized            => 20.0 ms/20.0 ms/20.0 ms
RFLX.TLV.Message.Invalid                => 0.0 s/0.0 s/0.0 s
RFLX.TLV.Message.Invalid_Successor      => 0.0 s/0.0 s/0.0 s
RFLX.TLV.Message.Message_Last           => 40.0 ms/40.0 ms/150.0 ms
RFLX.TLV.Message.Path_Condition         => 40.0 ms/40.0 ms/40.0 ms
RFLX.TLV.Message.Predecessor            => 0.0 s/0.0 s/0.0 s
RFLX.TLV.Message.Present                => 30.0 ms/30.0 ms/30.0 ms
RFLX.TLV.Message.Reset_Dependent_Fields => 110.0 ms/110.0 ms/920.0 ms
[...]

[treiher]

The reason for the partial caching is that GitHub´s cache action does not update the cache on a cache hit. It seems to be intended for caching dependencies only.

As workaround we could use a custom cache action which adds this feature: https://github.com/Componolit/github-action-cache.

[treiher]

With the custom cache action we are at 18 min for a successful verification if no changes have been made before. I think that is good enough for the moment. We can look into replacing the current verification tests by a smaller set in #208, where we intend to test features in a more structured way.

[treiher]

This issue is still not resolved. Often the verification test checks need more than one hour even if there were no changes on the SPARK code.

[treiher]

Checking in shape files (why3shapes.gz; additionally to the already checked in session files) should improve the runtime of GNATprove. For some reason this seems not to be the case for GNAT Community 2020, but for more recent versions. We should analyze the effect of these changes again after the release of GNAT Community 2021 (#494).

Disabling --proof-warnings could also decrease the runtime of GNATprove, but this issue will probably be fixed in future versions. I could not see any significant time savings for our tests after disabling this option.

[treiher]

Checking in shape files (why3shapes.gz; additionally to the already checked in session files) should improve the runtime of GNATprove. For some reason this seems not to be the case for GNAT Community 2020, but for more recent versions. We should analyze the effect of these changes again after the release of GNAT Community 2021 (#494).

Caching the proof results by adding session files and shape files works well with GNAT Community 2021. All verification tests are executed in less than 25 min in our GitHub workflows.