In Alire, how to use SPARKlib without all assertions enabled?

General
,
1

I have recently published my first crate (Proven_Components) that contains a bunch of reusable packages that I’ve written over the years and updated as Ada evolved. Most are now formally proven.

Proof for one of them (sorting) requires the Multisets package from SPARKlib. Before publishing the project as a crate it depended on the SPARKlib gpr files included with gnatprove. I used gnatprove’s approach to exclude all the SPARKlib sources not in the transitive closure of Multisets.

Now, as a crate, it depends on the SPARKlib crate and my client projects are having difficulties building. I understand the problem that the compiler is complaining about, but not how to address it in the context of Alire and the SPARKlib crate.

My code follows the convention of not testing at run-time those conditions that were also tested via preconditions. The preconditions are functional, in other words, not just for proof. I always want my code’s preconditions executed at run-time. Along the same line, I don’t want most of the other assertions enabled, eg Ghost code and Loop_Invariants. I never want them executed. I usually don’t want postconditions enabled, either, except when debugging.

Therefore, in my various client projects I have a configurations pragma file containing a pragma Assertions_Policy enabling preconditions (and a few others) but disabling the other assertions.

In alire this leads to conflicts in ghost policies when building. Presumably one or more of the units in SPARKlib has a precondition that calls Ghost code.

I can compile individual client files without the problem occurring. The problem arises when building the whole client project, because the builder tries to compile all the sources in SPARKlib, not just the ones required.

The fact that it didn’t conflict outside of Alire doesn’t mean that Alire is wrong about this. The SPARKlib gpr files provided in gnatprove are convoluted, shall we say, and the gpr file in the SPARKlib crate is quite different. I may have just been lucky before switching to the SPARKlib crate.

However, I assume the problem stems from the fact that SPARKlib.gpr in the crate applies “-gnata” unilaterally now, unlike the SPARKLib gpr files in gnatprove.

So, bottom line: how can I use SPARKlib in Alire in the way that, IMO, it should be possible to use it?

2

Alire supports three variants: release, debug and validation.The way I do it is to activate all checks in in validation but not in release. That way users of the libraries aren’t slowed down by the checks.

More importantly I use separate prove crates so there is no dependency on SPARK for the end user. Which is also considered best practice and the Alire moderators will question crates with gnatprove dependencies.

See How to Set Up Unit Tests and SPARK Proofs for details.

3

SPARKlib 15.1.0 did apply -gnata unilaterally, but the recently released SPARKlib 16.1.0 makes this configurable via the SPARKLIB_BUILD GPR external variable. This variable accepts three values:

  • "Production" (default) sets -O2 -gnatn
  • "Assertions" sets -O2 -gnatn -gnata -g
  • "Debug" sets -Og -g

This can be set in an alire.toml with:

[gpr-set-externals]
SPARKLIB_BUILD = "Assertions"

Also, GNAT, GNATprove, and SPARKlib version 16 support Assertion Levels, which can be used selectively enable different kinds of assertions.

SPARKlib 16 defines three assertion levels:

  • SPARKlib_Defensive is used for preconditions in SPARKlib.
  • SPARKlib_Logic is used for the ghost code that models the formal containers.
  • SPARKlib_Full is used for postconditions in SPARKlib. This one depends on level Static so it is never enabled at run-time.

So if you want to enable precondition checks in SPARKlib, which keeping other assertions in model functions turned off you can use:

pragma Assertion_Policy (SPARKlib_Defensive => Check);
pragma Assertion_Policy (SPARKlib_Logic => Ignore);

You can also define your own assertion levels if you want to have more control over which assertions/contracts are executed in your code.

Hopefully this helps with solving your problem.

4

Thanks, I’ll take a look!

5

Those changes to SPARKlib sound like a considerable improvement indeed. Unfortunately my immediate client project requires a cross-compiler, and if I am correct, there is no currently available gnat 16 cross-compiler.

Thanks for this! I have something to look forward to using in the future anyway.