!standard 11.4.1(27/3)                                19-10-01   AI12-0239-1/03
!class Amendment 17-10-05
!status work item 17-10-05
!status received 17-10-03
!priority Low
!difficulty Medium
!subject Ghost Code

!summary

Support for ghost code and accompanying ghost policies are added.

!problem

Sometimes, the variables and functions that are present in a program are not
sufficient to specify intended properties. In such a case, it would be
desirable to have the possibility to insert in the program additional code
useful for specification and verification, specially identified so that it
can be discarded during compilation. So-called ghost code are these parts of
the code that are only meant for specification and verification, and have no
effect on the functional behavior of the program. The goal is to have more
assurance that a given instrumentation of a program for verification purposes
does not interfere with the program being instrumented, and of the removal of
instrumentation code in the final executable.

Additionally, fine-grained control over ghost code may be useful for
traceability and debugging.

!proposal

Static Semantics

1. Ada defines the Boolean-valued representation aspect Ghost as well as an
   Identifier-valued representation aspect Ghost_Policy which differentiates
   Ghost assertion policies. Ghost and Ghost_Policy are an aspect of all
   entities (e.g., subprograms, types, objects). An entity whose Ghost aspect
   is True is said to be a ghost entity; terms such as "ghost function" or
   "ghost variable" are defined analogously (e.g., a function whose Ghost
   aspect is True is said to be a ghost function). In addition, a subcomponent
   of a ghost object is a ghost object.

   Ghost policies are a class of assertion aspect and can only be specified
   within the Ghost_Assertion_Policy pragma as part of a list of Ghost_Ids with
   their associated Assertion_Policy. Ghost_Ids within an Ghost_Assertion_Policy
   pragma shall either be user-defined ghost policies or the default policy of
   Ghost. [This means that Ghost can be named in a Ghost_Assertion_Policy pragma.]

   When Ghost_Policy is not specified for a ghost entity its policy shall be
   Ghost.

   Ghost_Policy may appear on an entity without Ghost defined in which case
   it is assumed that Ghost shall be in effect for said entity (e.g. equivalent
   to with Ghost => True).

2. The Ghost aspect of an entity declared inside of a ghost entity
   (e.g., within the body of a ghost subprogram) is defined to be True.

   The Ghost aspect of an entity implicitly declared as part of the
   explicit declaration of a ghost entity (e.g., an implicitly declared
   subprogram associated with the declaration of a ghost type) is
   defined to be True. The Ghost aspect of a child of a ghost library
   unit is defined to be True.

3. A statement or pragma is said to be a "ghost statement" if

   * it occurs within a ghost subprogram or package; or

   * it is a call to a ghost procedure; or

   * it is an assignment statement whose target is a ghost variable; or

   * it is a pragma which encloses a name denoting a ghost entity or
     which specifies an aspect of a ghost entity.

4. If a Ghost assertion policy in effect at the point of a
   ghost statement or the declaration of a ghost entity is Ignore,
   then the elaboration of that construct (at run time) has no effect,
   other Ada rules notwithstanding. Similarly, the elaboration
   of the completion of a ghost entity has no effect if the Ghost
   assertion policy in effect at the point of the entity's
   initial declaration is Ignore.

   [A Ghost assertion policy of Ignore can be used to ensure that
   a compiler generates no code for ghost constructs.]

   Such a declaration is said to be a disabled ghost declaration;
   terms such as "disabled ghost type" and "disabled ghost subprogram"
   are defined analogously.

Legality Rules

5. The Ghost aspect may only be specified [explicitly] for the declaration
   of a subprogram, a generic subprogram, a type (including a partial view
   thereof), an object (or list of objects, in the case of an
   aspect_specification for an object_declaration having more than one
   defining_identifier), a package, or a generic package.

   The Ghost and Ghost_Policy aspect may be specified via either an
   aspect_specification or via a pragma. The representation pragma Ghost
   takes a single argument, a name denoting one or more entities whose Ghost
   aspect is then specified to be True. The representation pragma Ghost_Policy
   takes two arguments, a name denoting one or more Ghost entities or entities
   whose Ghost aspect is specified as true, and a ghost assertion policy
   identifier.

   [In particular, Ada does not currently include any form of
   ghost components of non-ghost record types, or ghost parameters of
   non-ghost subprograms.]

6. A Ghost aspect value of False shall not be explicitly specified
   except in a confirming aspect specification. [For example, a
   non-ghost declaration cannot occur within a ghost subprogram.]

   The value specified for a Ghost assertion policy in a
   Ghost_Assertion_Policy pragma shall be either Check or Ignore.
   [In other words, implementation-defined assertion policy values
   are not permitted.] The Ghost assertion policies in effect at any
   point of an Ada program shall be either Check or Ignore.

7.  A ghost primitive subprogram of a non-ghost type extension shall
    not override an inherited non-ghost primitive subprogram.
    A non-ghost primitive subprogram of a type extension shall
    not override an inherited ghost primitive subprogram.
    [A ghost subprogram may be a primitive subprogram of a non-ghost
    tagged type. A ghost type extension may have a non-ghost parent type or
    progenitor; primitive subprograms of such a type may override
    inherited (ghost or non-ghost) subprograms.]

8.  A Ghost pragma which applies to a declaration occurring
    in the visible part of a package shall not occur in the
    private part of that package.

    [This rule is to ensure that the ghostliness of a visible entity
    can be determined without having to look into the private part of
    the enclosing package.]

9. A ghost entity shall only be referenced:

   * from within an assertion expression; or

   * from within an aspect specification [(i.e., either an
     aspect_specification or an aspect-specifying pragma)]; or

   * within the declaration or completion of a ghost entity
     (e.g., from within the body of a ghost subprogram); or

   * within a ghost statement; or

   * within a with_clause or use_clause; or

   * within a renaming_declaration which either renames a ghost entity
     or occurs within a ghost subprogram or package.

10. A ghost entity shall not be referenced within an aspect
    specification [(including an aspect-specifying pragma)]
    which specifies an aspect of a non-ghost entity except in the
    following cases:

    * the reference occurs within an assertion expression which is
      not a predicate expression; or

    * the specified aspect is either Global or an implementation-defined
      aspect that authorizes ghost entities.
      [For example, the Global aspect of a non-ghost subprogram might
      refer to a ghost variable.]

   [Predicate expressions are excluded because predicates participate
   in membership tests; no Ghost_Assertion_Policy pragma has any effect on
   this participation. In the case of a Static_Predicate expression,
   there are also other reasons (e.g., case statements).]

11. An out or in out mode actual parameter in a call to a ghost
    subprogram shall be a ghost variable.

12. If the Ghost assertion policy in effect at the point of the
    declaration of a ghost entity is Ignore, then the Ghost assertion
    policy in effect at the point of any reference to that entity shall
    be Ignore.

    If the Ghost assertion policy in effect at the point of the
    declaration of a ghost variable is Check, then the Ghost assertion
    policy in effect at the point of any assignment to a part of that
    variable shall be Check.

    [This includes both assignment statements and passing a ghost
    variable as an out or in out mode actual parameter.]

13. A Ghost_Assertion_Policy pragma specifying Ghost assertion policies
    shall not occur within a ghost subprogram or package.
    If a ghost entity has a completion then the Ghost assertion policies
    in effect at the declaration and at the completion of the entity
    shall be the same. [This rule applies to subprograms, packages,
    types, and deferred constants.]

    The Ghost assertion policies in effect at the point of the
    declaration of an entity and at the point of an aspect specification
    which applies to that entity shall be the same.

14. The Ghost assertion policies in effect at the declaration of a
    primitive subprogram of a ghost tagged type and at
    the declaration of the ghost tagged type shall be the same.

15. If a tagged type is not a disabled ghost type, and if a
    primitive operation of the tagged type overrides an inherited
    operation, then the corresponding operation of the ancestor type
    shall be a disabled ghost subprogram if and only if the overriding
    subprogram is a disabled ghost subprogram.

16. If the Ghost assertion policy in effect at the point of
    a reference to a Ghost entity which occurs within an assertion
    expression is Ignore, then the assertion policy which governs the
    assertion expression (e.g., Pre for a precondition expression,
    Assert for the argument of an Assert pragma) shall [also] be Ignore.

17. A ghost type shall not have a task or protected part.
    A ghost object shall not be of a type which yields synchronized
    objects.
    A ghost object shall not have a volatile part.

!example

   function A_Ghost_Expr_Function (Lo, Hi : Natural) return Natural is
     (if Lo > Integer'Last - Hi then Lo else ((Lo + Hi) / 2))
     with Pre        => Lo <= Hi,
          Post       => A_Ghost_Expr_Function'Result in Lo .. Hi,
          Ghost;

   function A_Ghost_Function (Lo, Hi : Natural) return Natural
     with Pre        => Lo <= Hi,
          Post       => A_Ghost_Function'Result in Lo .. Hi,
          Ghost;

   -- The body of the function is declared elsewhere.

   function A_Nonexecutable_Ghost_Function (Lo, Hi : Natural)
     return Natural
     with Pre      => Lo <= Hi,
          Post     => A_Nonexecutable_Ghost_Function'Result in Lo .. Hi,
          Ghost,
          Import;

   -- The body of the function is not declared elsewhere.

Other examples of ghost code can be found in SPARK User's Guide:
http://docs.adacore.com/spark2014-docs/html/ug/en/source/specification_features.html#ghost-code

!discussion

Now, about modifying these rules for Ada.

#13 The second sentence could possibly be relaxed. For Ada, this
is more like advice about good practice rather than a requirement.

#15 is a rule about state abstractions (a SPARK construct) which
does not apply to Ada.

#19 could potentially be relaxed for Ada.

SPARK doesn't currently have access types (that should change soon),
so there are no rules about interactions between ghost objects and
access types. One approach: anything goes - no new rules needed.
This provides another way to get around #13 (we disable an
assignment to Some_Ptr.all and it turns out
that Some_Ptr refers at runtime to an enabled ghost object), but
maybe that's ok.

!ASIS

[Not sure. Perhaps a new aspect query would be needed. - Editor]

!ACATS test

ACATS B and C-Tests are needed to check that the new capabilities are supported.

!appendix

From: Steve Baird
Sent: Monday, October 2, 2017 11:57 PM

Opening a new AI to discuss adding "ghost code" to Ada. [This is version /01
of the AI - Editor.]

SPARK defines "ghost" code and it has proven to be extremely useful.  It seems
that this concept could be used in Ada as well to provide a powerful new
assertion mechanism. Ghost code
   - can include object, subprogram, and other declarations,
     as well as statements which reference these declarations;
   - is intended for use in assertions (e.g., the precondition
     or postcondition of a non-ghost subprogram might include
     a call to a ghost function);
   - can be enabled or disabled via assertion policy;
   - cannot (in SPARK) modify non-ghost state.

[The SPARK documentation can be found at
docs.adacore.com/spark2014-docs/html/lrm/subprograms.html#ghost-entities
but this AI is intended to be self-contained.]

SPARK enforces rules which have the consequence of ensuring that ghost code
cannot modify non-ghost state. The idea is that disabling ghost code should
not change the language-defined behavior of a program. In Ada, this might not
be enforced (in SPARK callers know statically what global variables are read
and written by a given procedure, so stricter rules are easier to check) and
instead some of these rules might only be recommended as good practice.
This would be much the same as the situation today with assertion expressions
that have significant side-effects; Ada does not prevent this but the practice
is not recommended. Nonetheless, program behavior is well-specified for all
combinations of assertion policy specifications.

The SPARK RM section section begins with the following introduction, some of
which might apply only in spirit in the case of Ada (if the rule that
ghost-code can't modify non-ghost state is not enforced in Ada):
   Ghost code is intended for making it easier to express assertions
   about a program. The essential property of ghost code is that it has
   no effect on the dynamic behavior of a valid Ada program. More
   specifically, if one were to take a valid Ada program and remove all
   ghost code from it (all declarations of ghost entities and all
   "innermost" statements, declarations, and pragmas which
   refer to those declarations, replacing removed statements with null
   statements when syntactically required), then the resulting program
   would still be a valid Ada program and its dynamic semantics should be
   unaffected by this transformation. [This transformation might affect
   the performance characteristics of the program (e.g., due to no longer
   evaluating provably true assertions), but that is not what we are
   talking about here. In rare cases, it might be necessary to make a
   small additional change after the removals (e.g.,
   adding an Elaborate_Body pragma) in order to avoid producing a
   library package that no longer needs a body (see Ada RM 7.2(4))].

For example, one might have an efficient-but-complex implementation of some
function, a simple-but-inefficient ghost implementation of the same function,
and an assertion that the two produce equal results.

****************************************************************

From: Steve Baird
Sent: Tuesday, October 3, 2017  9:49 AM

> If the Ghost assertion policy in effect at the point of the
> declaration of a ghost entity is Ignore, then the Ghost assertion
> policy in effect at the point of any reference to that entity shall be
> Ignore.

I forgot to mention the issue of enforcing rules such as the one cited above
in expanded instance bodies.

SPARK deals with this by simply enforcing such legality rules in expanded
instance bodies, but for Ada we would probably want to define post-compilation
checks.

****************************************************************

From: Randy Brukardt
Sent: Tuesday, October 3, 2017  2:16 PM

> Opening a new AI to discuss adding "ghost code" to Ada.

As always, I'm dubious that an all-or-nothing "ghost" mode is enough.
Janus/Ada's conditional compilation feature works like that, and it proved to
be inadequate for any real processes -- the only benefit it has is completely
removing conditionally compiled code including pragmas and declarations from
"production" tools. To use it in practice requires an extensive series of
boolean flags and (in some cases) menus in order to select what ought to be
checked. (Turning on everything is way too expensive in time and noise.)

Secondary thought: there doesn't seem to be a way to have ghost pragmas (like
pragma Suppress) that aren't directly associated with another ghost
declaration. We use Janus/Ada conditional compilation to set the suppression
state of each unit, so that the selection of production vs. testing code is
controlled by a single compilation flag.

Specifically:

    package body J2Code_Attributes is

        pragma Unsuppress (Access_Check);
        pragma Unsuppress (Index_Check);
        pragma Unsuppress (Length_Check);
        pragma Unsuppress (Overflow_Check);
        pragma Unsuppress (Range_Check);
        pragma Unsuppress (Elaboration_Check);
@       pragma Suppress (Access_Check);
@       pragma Suppress (Index_Check);
@       pragma Suppress (Length_Check);
@       pragma Suppress (Overflow_Check);
@       pragma Suppress (Range_Check);
@       pragma Suppress (Elaboration_Check);

        ...

The @ is compiled either as a space or a "--" depending on a compilation flag;
so one suppresses the listed checks IFF a "production" tool is being built as
opposed to a "testing" tool. This seems like an important capability that ought
to supported by ghost code.

****************************************************************

From: Tucker Taft
Sent: Tuesday, October 3, 2017 9:33 PM

Ghost code does not by itself typically take any time, but rather it is
callable from pre- and postconditions, type invariants, predicates, or assert
pragmas,  We already have fine-grained control over these other constructs, so
fine-grain control over ghost code is not particularly important from a time
efficiency point of view.  The reason you mark something as ghost is to be
sure that it is only called from these sorts of assertions, and you can be
certain that the code can be omitted from a "production" version if desired.
For systems being certified, it is often important to know that certain code
will *not* appear in the final executable, and ghost code is ideally suited
for that.

****************************************************************

From: Randy Brukardt
Sent: Thursday, October 5, 2017 11:55 PM

This seems to me to be too narrow of a view of the capability. The last
statement is the most accurate "...it is often important to know that
certain code will *not* appear in the final executable...". I totally agree
that this is very important, but that has nothing (directly) to do with
assertions. Certainly, a lot of such code is directly used by assertions. But
there is plenty of other such code: tracing code, instrumented storage pools,
debugging pragmas, and the like.

If we define the problem too narrowly, we'll end up with a solution that is
too narrow for a general purpose language like Ada. The proposed definition
makes sense for SPARK, which only cares about contracts; the general case
surely is broader than just that.

As I noted, Janus/Ada has a solution to this problem (going back to the very
early days). As it is lexical(!) in nature, it is too free-form to
standardize. But I'm going to have to replace it (since Ada 2020 has stolen
the @ it depends upon), and it would be good if its function could be replaced
by a standard feature.

I don't object to using the Assertion_Policy mechanism for ghost code, as it
probably isn't worth a separate mechanism. But it is silly to restrict ghost
code to assertions; it should be anything that isn't wanted in the production
system. And ideally, it would be possible to partition this into different
sets (as is also needed for assertions). And it ought to work on pragmas as
well as declarations and program units so that the configuration can be set
along with the rest of testing vs. production differences.

****************************************************************

From: Justin Squirek
Sent: Saturday, June 15, 2019  9:05 AM

[Version /02 of the AI was attached to this message - Editor.]

As one of my first serious AI assignments it shall be likely that I am
missing something or that other revisions be necessary : )

I will need to modify the semantics of Assertion_Policy, but I first wanted
to check the consensus of the group first.

The most relevant section is below:

!summary

Support for ghost code and accompanying ghost policies are added.

!problem

Sometimes, the variables and functions that are present in a program are not
sufficient to specify intended properties. In such a case, it would be
desirable to have the possibility to insert in the program additional code
useful for specification and verification, specially identified so that it
can be discarded during compilation. So-called ghost code are these parts of
the code that are only meant for specification and verification, and have no
effect on the functional behavior of the program. The goal is to have more
assurance that a given instrumentation of a program for verification purposes
does not interfere with the program being instrumented, and of the removal of
instrumentation code in the final executable.

Additionally, fine-grained control over ghost code may be useful for
traceability and debugging.

!proposal

Static Semantics

1. Ada defines the Boolean-valued representation aspect Ghost as well as an
    Identifier-valued representation aspect Ghost_Policy which differentiates
    Ghost assertion policies. Ghost and Ghost_Policy are an aspect of all
    entities (e.g., subprograms, types, objects). An entity whose Ghost aspect
    is True is said to be a ghost entity; terms such as "ghost function" or
    "ghost variable" are defined analogously (e.g., a function whose Ghost
    aspect is True is said to be a ghost function). In addition, a subcomponent
    of a ghost object is a ghost object.

    Ghost is an assertion aspect, and unique identifiers within an
    Assertion_Policy pragma shall be user-defined ghost policies.
    [This means that Ghost can be named in an Assertion_Policy pragma.]

    Ghost_Policy may appear on an entity without Ghost defined in which case
    it is assumed that Ghost shall be in effect for said entity (e.g.
    equivalent to with Ghost => True).

****************************************************************

From: Richard Wai
Sent: Sunday, June 16, 2019  12:18 AM

>     Ghost is an assertion aspect, and unique identifiers within an
>     Assertion_Policy pragma shall be user-defined ghost policies.
>     [This means that Ghost can be named in an Assertion_Policy pragma.]

I don't quite understand why " unique identifiers within an Assertion_Policy
pragma shall be user-defined ghost policies." I didn't see any other mention
of the idea of "user-defined ghost policies".

>     Ghost_Policy may appear on an entity without Ghost defined in which case
>     it is assumed that Ghost shall be in effect for said entity (e.g.
>     equivalent to with Ghost => True).

What is the purpose of Ghost_Policy, if we already have Ghost as a new
Assertion_Policy identifier? I also didn't see Ghost_Policy mentioned anywhere
else. So it looks like all it does is affect the Ghost aspect to also be true,
so it seems totally redundant.

****************************************************************

From: Justin Squirek
Sent: Sunday, June 16, 2019  5:27 AM

>>      Ghost is an assertion aspect, and unique identifiers within an
>>      Assertion_Policy pragma shall be user-defined ghost policies.
>>      [This means that Ghost can be named in an Assertion_Policy pragma.]
> I don't quite understand why " unique identifiers within an Assertion_Policy
> pragma shall be user-defined ghost policies." I didn't see any other mention
> of the idea of "user-defined ghost policies".

Yes, I agree, I need to go into more detail about what ghost policies are and
how they interact with the ghost aspect. In short the intention was to allow
categories of ghost so that they can be selectively turned on or off. Entities
marked simply with "Ghost" will be in the general policy of Ghost while
additional user-defined policies will act independently and will be indicated
with the new aspect Ghost_Policy.

>>      Ghost_Policy may appear on an entity without Ghost defined in which case
>>      it is assumed that Ghost shall be in effect for said entity (e.g.
>>      equivalent to with Ghost => True).
> What is the purpose of Ghost_Policy, if we already have Ghost as a new
Assertion_Policy identifier? I also didn't see Ghost_Policy mentioned anywhere
else. So it looks like all it does is affect the Ghost aspect to also be true,
so it seems totally redundant.

It would not be redundant since Ghost takes a boolean and thus could have some
sort of static expression which could lead to it being False.
Ghost_Policy takes an identifier and would lose this capability.

****************************************************************

From: Tucker Taft
Sent: Sunday, June 16, 2019  10:03 AM

Thanks Justin for a good start on this AI!  Has promise ...

****************************************************************

From: Justin Squirek
Sent: Tuesday, October 1, 2019  2:43 PM

Here is my homework for the upcoming meeting

[This was a copy of version /02 - Editor.]

****************************************************************

From: Justin Squirek
Sent: Tuesday, October 1, 2019  3:27 PM

I previously sent the wrong version. Please disregard that one and use this
one in its place.

[This is version /03 of the AI - Editor.]

****************************************************************

From: Tucker Taft
Sent: Tuesday, October 1, 2019  4:00 PM

Looks very good.  However, in an AI, we don't usually number the paragraphs of
a new section.  Was that intentional or a side effect of some formatting tool?
And the numbers are only on top-level paragraphs, which is definitely not our
usual formatting approach.

****************************************************************

From: Justin Squirek
Sent: Tuesday, October 1, 2019  4:17 PM

No, I was keeping in the style of the original AI. Which I guess was rougher
than I assumed. Please disregard extraneous formatting.

****************************************************************

From: Randy Brukardt
Sent: Tuesday, October 1, 2019  4:32 PM

I think Tucker is confusing !wording with !proposal. I agree that we usually
don't number paragraphs, but it was done here as there are so many separate
topics. And !proposal is free-form, so there's no reason to avoid numbering
if it makes it easier to refer to a particular topic. Presumably that would
be removed once it was replaced with actual wording.

****************************************************************

From: Randy Brukardt
Sent: Tuesday, October 1, 2019  6:46 PM

A couple of thoughts about this proposal:

(1) We haven't defined any new pragmas that apply to entities, as we think that
using aspects for such usages is  preferred. So I don't think we need or want
pragmas Ghost and Ghost_Policy. (GNAT can define such things if it wants.) We do
need the Ghost_Assertion_Policy pragma, as that is a more global thing.

(2) I didn't see anything where the text describes the use of user-defined ghost
"policies". They just sort of appear. I suspect that we need a different name
for these (they're not policies, they're sets of entities to which a policy
applies -- the policy is "Check" or "Ignore"). In particular, I find the
difference between "Ghost_Policy" and "Ghost_Assertion_Policy" confusing, for
this reason (the latter sets a policy, the former names the set to which a
policy applies - perhaps "Ghost_Set" is the appropriate name for the former, and
then we can use Ghost_Policy for the latter??)

****************************************************************