Assertion_Policy as an aspect

[sttaft]

A customer recently asked whether they could specify the Assertion_Policy for some but not all of the subprograms in a package spec. We indicated you could have multiple Assertion_Policy pragmas in a package spec, but they pointed out they still want to be able to establish an overall default policy, and have certain subprograms definitely Check or definitely Ignore, but leave the rest to the default policy.

One possible solution is to support something like "Assertion_Policy ([Id =>] Restore)" which would return the policy for the given Id, or for all kinds of assertions, to what it was on the previous Assertion_Policy pragma, but that seems like it could quickly become a maintenance nightmare in big packages.

An alternative is to allow Assertion_Policy to be specified on an individual subprogram within a package. That would seem to argue for making it an aspect, with a syntax such as:

procedure Foo
   with Assertion_Policy => (Id1 => Ignore, Id2 => Check);

That seems like the most elegant solution to the problem. We would probably want to leave the pragma Assertion_Policy as non-obsolescent, since it is better for turning on and off within a given package or declarative part, but the ability to make it an aspect of individual declarations (and presumably of a package as a whole) would avoid the need for something like "Restore".

[ARG-Editor]

Would it be possible to find out the usage case for the customer? It doesn't seem likely to me that there is only one such configuration. (There often would be all checks on, and only critical checks, and probably no checks at all, and possibly some additional debugging configurations. So this sounds like the sort of thing that needs to be controlled by ghost code or something like it. (Of course, we might still need an aspect to be controlled by the ghost code mechanism (which really should be called a configuration mechanism, since it could include settings and code for debugging and for contract checks and probably other things I haven't thought of.)

              Randy.

[Jeff-Cousins]

How likely is it that any extensions to pragma Assertion_Policy would be implemented? I have yet to see pragma Assertion_Policy (assertion_aspect_mark => ...); work.

Sent from Mail for Windows

[sttaft]

Would it be possible to find out the usage case for the customer?

They use SPARK, so pre/postconditions are doing double duty -- they are used as part of formal proofs, but they are also used for run-time testing. However, there are some pre/postconditions which are only useful for SPARK -- they are too expensive for testing (e.g. because they use a universal quantifier), so they want to ignore those pre/postconditions for run-time checking. But there are other subprograms in the same package that they want to control more globally, so their contract checks are turned off in production, but turned on during testing. They intend to control that global mode distinction from the command line or some configuration-level pragma.

The problem is that they can use Assertion_Policy to go into "ignore" mode, but there is no way to go back into the "default" mode. So if they use a second Assertion_Policy pragma to end the "ignore" mode, the only choice is to go to "check" mode, which is not what they want in production.

By allowing an Assertion_Policy as an aspect, then they can make a subprogram-by-subprogram decision about whether or not to ignore the pre/postconditions for generated code, without worrying about preventing the other subprograms from being controlled more globally.

... It doesn't seem likely to me that there is only one such configuration. (There often would be all checks on, and only critical checks, and probably no checks at all, and possibly some additional debugging configurations.

They have only two states at this point. Yes, you could imagine having "slow" and a "very-slow" classifications for assertion expressions, but they would be happy at this point to be able to use the flexibility of a per-subprogram aspect. Having more than two levels might be of eventual interest, but that would argue even more strongly for having an aspect-based mechanism, rather than a turn-on/turn-off approach as currently provided by the Assertion_Policy pragma.

How likely is it that any extensions to pragma Assertion_Policy would be implemented? I have yet to see pragma Assertion_Policy (assertion_aspect_mark => ...); work.

As far as I know, the aspect_mark capability is supported by GNAT. I don't know about other compilers' support for this feature of Assertion_Policy.

[ARG-Editor]

Tucker answers:

They use SPARK, so pre/postconditions are doing double duty -- they are used as part of formal proofs, but they are also used for run-time testing. However, there are some pre/postconditions which are only useful for SPARK -- they are too expensive for testing (e.g. because they use a universal quantifier), so they want to ignore those pre/postconditions for run-time checking. But there are other subprograms in the same package that they want to control more globally, so their contract checks are turned off in production, but turned on during testing. They intend to control that global mode distinction from the command line or some configuration-level pragma.

This is essentially the use case I was thinking of. And this is exactly the usage case for "ghost code".

...

They have only two states at this point. Yes, you could imagine having "slow" and a "very-slow" classifications for assertion expressions, but they would be happy at this point to be able to use the flexibility of a per-subprogram aspect. Having more than two levels might be of eventual interest, but that would argue even more strongly for having an aspect-based mechanism, rather than a turn-on/turn-off approach as currently provided by the Assertion_Policy pragma.

No, it argues for a general facility, not some hack that only works for a particular pragma. The ghost code mechanism would handle this case perfectly, and it could do lots of other things as well.

The idea of "ghost code" is really a general ability to make and name configurations, for debugging, for proof support, and probably for things that we haven't considered (multihosting? multitargeting?). [I think the "ghost code" idea needs a more general name, since it really is a way to have safe configurations without introducing most of the errors that happen when they are managed with source-level stuff like macros.]

I'm supposed to be creating an issue for the "on hold" ghost code AI (soon), so perhaps we can drum up some interest beyond just me. ;-)

Getting back to the issue at hand. I'm against adding aspects that just help in very limited circumstances. If the configuration mechanism never gets off the ground, then we can revisit more targeted fixes, but I don't want to clutter the language with hacks if a more elegant general feature will handle the need.

                 Randy.

[sttaft]

On Wed, Feb 15, 2023 at 3:06 AM ARG-Editor @.***> wrote:

Tucker answers:

They use SPARK, so pre/postconditions are doing double duty -- they are used as part of formal proofs, but they are also used for run-time testing. However, there are some pre/postconditions which are only useful for SPARK -- they are too expensive for testing (e.g. because they use a universal quantifier), so they want to ignore those pre/postconditions for run-time checking. But there are other subprograms in the same package that they want to control more globally, so their contract checks are turned off in production, but turned on during testing. They intend to control that global mode distinction from the command line or some configuration-level pragma.

This is essentially the use case I was thinking of. And this is exactly the usage case for "ghost code".

If you think this is a good idea, you should include a link to the relevant AI. In fact, all assertion expressions are already considered to be "ghost code" by SPARK, so by itself that doesn't say anything. They also already have an aspect "Ghost" for indicating that a subprogram, assignment statement, object declaration, etc., is to be considered ghost code, and so can only be called from other ghost code or applied to a ghost variable.

Later you indicate you are referring to the idea that the ARG had where one could categorize ghost code more finely, with different notions of debugging code, checking code, performance analysis code, etc. That is not what is normally meant by the term "ghost code", so you should probably not use the term "ghost" here, but rather reference the draft AI or some other GitHub issue.

...

Getting back to the issue at hand. I'm against adding aspects that just help in very limited circumstances. If the configuration mechanism never gets off the ground, then we can revisit more targeted fixes, but I don't want to clutter the language with hacks if a more elegant general feature will handle the need.

We have generally tried to convert almost all pragmas to aspects, so it doesn't seem like a "hack" to convert Assertion_Policy into an aspect. It seems like a very natural generalization. I think the more general "ghost" idea we discussed is interesting, but I would suspect that for many folks, just being able to use Assertion_Policy as an aspect would be a cleaner solution. I also suspect the more general "ghost" idea may be controversial, and could in any case take years to finalize and get implemented. Adding support for Assertion_Policy as an aspect I suspect will be much simpler, and something that an implementation that already supports Assertion_Policy could do quickly.

Randy.

Take care, -Tuck

Message ID: @.*** com>

[ARG-Editor]

I'm not sure why you are repeating most of my points ("ghost code" is a lousy name, but it's the one we have, it will take effort to develop and might not succeed, I'll link the issue once I get it created - it's on my extensive to-do list, etc.).

In any case, it will be years before anything that we do here matters in any significant sense. Implementers can always invent aspects of their own, but nothing we do will be graven in stone until our next Ada document, and we haven't even started to think about that yet. So there is absolutely no rush to add halfway solutions to problems that should be superseded by much better solutions before anything gets finished.

The difficultly in using a solution to manage configurations that only allows two configurations is well known. Its silly to even waste time thinking about such solutions when we've already designed a more general solution that avoids most of the problems of the one-off solutions. This is an area where Ada can truly be improved, unlike a lot of the suggestions I've seen to date.

The one kind of pragma that we did not convert to aspects was confirguration pragmas, because they are intended to control many declarations at once. If we were going to do that, I think it should be in a general way, not just a single configuration pragma. (Assertion_Policy is a close relative of Suppress/Unsuppress; they should be aspects, too. And so on...) But I don't see the point of turning off some of the checks and leaving the subprograms that make up those checks in the code. So the "ghost code" mechanism (which is neither about "ghosts" or restricted to "code" -- we need a better name, but I don't have one) is an intergral part of this problem. A simple aspect is not enough.

                   Randy.

                            Randy.

[clairedross]

On Wed, Feb 15, 2023 at 3:37 PM S. Tucker Taft @.***> wrote:

If you think this is a good idea, you should include a link to the relevant AI. In fact, all assertion expressions are already considered to be "ghost code" by SPARK, so by itself that doesn't say anything. They also already have an aspect "Ghost" for indicating that a subprogram, assignment statement, object declaration, etc., is to be considered ghost code, and so can only be called from other ghost code or applied to a ghost variable.

I fully agree with Tuck here, please include a link, I would like to take a look to determine how much incompatibility this is going to cause...

Later you indicate you are referring to the idea that the ARG had where one could categorize ghost code more finely, with different notions of debugging code, checking code, performance analysis code, etc. That is not what is normally meant by the term "ghost code", so you should probably not use the term "ghost" here, but rather reference the draft AI or some other GitHub issue.

Indeed, this is not what ghost means. We already discussed with customer the possibility of providing several pre or post conditions with different "modes" attached. If it is close to what you are working one, then indeed, it looks relevant for this issue.

...

Getting back to the issue at hand. I'm against adding aspects that just help in very limited circumstances. If the configuration mechanism never gets off the ground, then we can revisit more targeted fixes, but I don't want to clutter the language with hacks if a more elegant general feature will handle the need.

We have generally tried to convert almost all pragmas to aspects, so it doesn't seem like a "hack" to convert Assertion_Policy into an aspect. It seems like a very natural generalization. I think the more general "ghost" idea we discussed is interesting, but I would suspect that for many folks, just being able to use Assertion_Policy as an aspect would be a cleaner solution. I also suspect the more general "ghost" idea may be controversial, and could in any case take years to finalize and get implemented. Adding support for Assertion_Policy as an aspect I suspect will be much simpler, and something that an implementation that already supports Assertion_Policy could do quickly.

Randy.

Take care, -Tuck

Message ID: @.*** com>

— Reply to this email directly, view it on GitHub https://github.com/Ada-Rapporteur-Group/User-Community-Input/issues/38#issuecomment-1431470317, or unsubscribe https://github.com/notifications/unsubscribe-auth/AB6NCMNALY24WR5EHCKGBILWXTSY5ANCNFSM6AAAAAAUYIE7JQ . You are receiving this because you are subscribed to this thread.Message ID: @.*** .com>

-- Claire Dross Senior Software Engineer, AdaCore

[sttaft]

Here is the original AI about "Ghost" which was largely reflecting exactly what SPARK supports:

http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0239-1.txt?rev=1.7

We discussed it at an ARG meting in October 2019, and evolved toward a more sophisticated approach, which is what Randy was alluding to:

http://www.ada-auth.org/ai-files/minutes/min-1910.html#AI239

However, no new version of the AI was produced incorporating these ideas, though Justin was working on one, I believe. In January 2020 we put further work on this on hold, in part due to implementation concerns.

[ARG-Editor]

Tucker wrote:

Here is the original AI about "Ghost" which was largely reflecting exactly what SPARK supports:

http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0239-1.txt?rev=1.7

The original version of that AI was like that, but the version you are pointing at goes well beyond that.

We discussed it at an ARG meting in October 2019, and evolved toward a more sophisticated approach, which is what Randy was alluding to:

http://www.ada-auth.org/ai-files/minutes/min-1910.html#AI239

However, no new version of the AI was produced incorporating these ideas, though Justin was working on one, I believe.

Those ideas were originally introduced in the June 2019 meeting (Warsaw), and Justin produced several updates including those ideas (1.3 during the meeting and 1.4 afterwards). But he certainly did not finish updating the AI, either.

... In January 2020 we put further work on this on hold, in part due to implementation concerns.

My recollection was that the concerns mainly revolved around wanting to be able to prototype these ideas before standardizing them, and having insufficient time to do that. (This AI was one of the original reasons for wanting to formally include prototyping activities in ARG planning.) We simply didn't have enough time to do so, which is why I didn't object too much to stopping work on this idea (it's important to get it right).

Anyway, this is one of the "hold" AIs that I need to resurrect based on the ARG vote in November (and clearly the main reason for stopping work, which was insufficient time, does not apply to future features). I plan to get to that next month. We can and should discuss it in an issue created for that purpose (and not clutter up this one).

                         Randy.

[sttaft]

I suppose at this point I would encourage AdaCore to support Assertion_Policy as an aspect, roughly as proposed above:

procedure Foo
   with Assertion_Policy => (Id1 => Ignore, Id2 => Check);

As Randy points out, implementors are allowed to add aspects. We can see whether users find that having Assertion_Policy as an aspect solves their problem.

[brgaeke]

Hi,

I'm writing in support of this proposal. In our use of Ada and SPARK we have run into a couple of scenarios where because

• the expression in the assertion tripped over some fault in the code generation, or
• the expression in the assertion turned out to be too expensive in space or time to evaluate, and
• we compile our code in both default-Assertion_Policy-Check (for debugging) and default-Assertion_Policy-Ignore (for production) configurations...

...it would have been very useful for us to be able to have Assertion_Policy supported as an aspect on subprograms. If such support had existed at the time we had these problems, it would have been trivially easy to change the Assertion_Policy for a given problematic subprogram or two, knowing that the setting would automatically revert back to its default for the given build configuration for the remainder of the package.

Thanks, -Brian Gaeke