Initial proposal for ghost fields

[sttaft]

Looks very good. You might want to at least mention as an alternative the possibility of representing ghost fields using a mapping rather than directly in the enclosing record, thereby allowing the representation to stay the same without any need for padding, etc. Essentially one could establish a ghost mapping where all of the ghost fields would reside in a separate record, with the key being the 'Address of the non-ghost record, and the value being a record containing one or more ghost fields.

[Fabien-Chouteau]

Ghost fields having and impact on data layout made me cry a little :smiling_face_with_tear: I do understand the rational but it will be a no-go for some cases in low-level programing and also embedded where memory usage is key.

In cases where there are no representation clauses, will the compile be allowed to optimize the size of the record?

[yannickmoy]

@Fabien-Chouteau the issue is not only with representation clauses, but also attributes Size/Object_Size/Alignment. For the cases you mention, an extension could consist in giving a size of zero to the ghost component, which would thus be non-executable. As this brings new problems, I'd rather start with a solution that does not require it.

[yannickmoy]

@sttaft indeed, I had missed that earlier discussion between you and @swbaird from 2018! Thanks for pointing it out, I've taken it into account in the RFC. @Fabien-Chouteau I also mentioned null-size ghost components as possible future work.

[sttaft]

Since ghost components are not a standard Ada feature at this point, we could define their parameter passing semantics as we see fit. In the case of parameter passing, I would suggest that ghost components could always be passed by reference, so all that is happening on parameter passing is the addition of a mapping from the formal 'Address to the actual record of ghost fields. This should resolve the problem in case a ghost field requires pass by reference, while the non-ghost fields are normally passed by copy.

[yannickmoy]

@sttaft sorry I don't follow your suggestion. IIUC, you're suggesting that types with ghost components are considered as pass-by-reference types? I thought this was only an issue if we went for ghost components being stored in separate tables indexed by object addresses?

[QuentinOchem]

At this stage, forcing the layout to be the same for the ghost and non ghost will defeat their purpose, e.g.:

In order to guarantee that the program semantics are unaffected by the decision to activate or not ghost code, the compiler should use the same size and layout for record objects in both cases, using padding components instead of ghost components when ghost code is not activated.

The use cases that we have at this stage are for low level software, with constraints in terms of resources if not layout for final execution. There's no clear benefit in the current ghost fields semantics.

Generally speaking, ghost code has an impact on program resources - with ghost code active today, a program already takes more time and potentially more memory (e.g. stack). So saying that ghost field modify also resource consumption is not fundamentally at odds.

I would suggest alternatives approaches:

(1) ghost fields can never be compiled in the final executable. This adds constraints at compile time as it means we need some way to determine if a given assertion depends on ghost field, and thus can't be compiled (probably needs to be an error in that case)

(2) add a aspect "for Something'Ghost_Size use value;" which allows to specify a size for the ghost size if representation is needed. We can then just ignore ghost fields in the representation clause when ghost fields are not computed. If this attribute is not provided, then the size of the record will vary automatically depending on ghost code activation, as it would if you were to add or remove fields.

[sttaft]

Yannick wrote:

sorry I don't follow your suggestion. IIUC, you're suggesting that types with ghost components are considered as pass-by-reference types? I thought this was only an issue if we went for ghost components being stored in separate tables indexed by object addresses?

I was responding to Steve Baird's concern that adding ghost fields might change the parameter from being passed by copy to requiring pass by reference. I was suggesting that, if ghost fields are represented in a mapping from real_record'Address to a record containing any ghost fields of the record, these ghost fields can always be effectively passed by reference, even if the "real" fields are passed by copy. Because you now have a copy of the original real record, you would need to add to the ghost mapping a mapping from the copy'Address to the same record of ghost fields, so these two copies are effectively sharing the ghost fields record, since they conceptually represent the same object.

In short, even if the non-ghost record is passed by copy, its ghost fields could be passed by reference.

[yannickmoy]

@QuentinOchem I'd like to propose a third approach, which I mentioned in the RFC:

(3) have a way to specify that a ghost field has size 0, so that it takes no space, and as a result is not executable.

I prefer this approach over (1) because it still makes it possible to have executable ghost fields. I also prefer this approach over (2) which I don't understand, and leaves in any case the responsibility of "making it right" to the user, so you could end up proving some code and getting it to fail at runtime due to changes in type sizes.

[QuentinOchem]

@QuentinOchem I'd like to propose a third approach, which I mentioned in the RFC:

Right - I now realize that my proposals where actually already mapped in your alternatives:

(3) have a way to specify that a ghost field has size 0, so that it takes no space, and as a result is not executable.

I prefer this approach over (1) because it still makes it possible to have executable ghost fields.

I believe you're referring to:

An alternative would be to make ghost components never executable, which would require any ghost code referring to ghost components to be disabled. The benefit of that approach is that ghost components could be ignored when computing the type representation.

Which essentially the same as (1) (ie, you can't compile assertions referencing ghost fields).

I also prefer this approach over (2) which I don't understand, and leaves in any case the responsibility of "making it right" to the user, so you could end up proving some code and getting it to fail at runtime due to changes in type sizes.

I believe (2) is a variation on:

Another alternative would be to have executable ghost components, but change the type representation depending on whether ghost components are activated or not. The benefit of that approach is that no padding space is used when ghost components are deactivated. The big drawback is that computations that involve type representation values (like the type's size) are different when ghost components are activated or not.

My personal preference would definitely this one, although the consequence in terms of proof should be studied indeed. Do you have a simple example highlighting a piece of code that would prove but fail at run-time?

[yannickmoy]

@QuentinOchem see the following code, proved but which would fail at runtime with option (2):

procedure P is
   type T is record
      X : Integer;
      Y : Integer;  --  with Ghost;
   end record with Pack;
begin
   pragma Assert (T'Size = 64);
end P;

What's your rationale for not preferring (2)? For me, it's just like (3) but safer.

[QuentinOchem]

@QuentinOchem see the following code, proved but which would fail at runtime with option (2):

procedure P is
   type T is record
      X : Integer;
      Y : Integer;  --  with Ghost;
   end record with Pack;
begin
   pragma Assert (T'Size = 64);
end P;

One alternative to explore could be that in the context of ghost fields, T'Size isn't a value anymore from the SPARK perspective, but one or two. So the above would fail, but something like:

pragma Assert (T'Size <= 64);

Would work. This is limiting the use cases of 'Size for contracts in the presence of ghost fields, but that might be good enough.

What's your rationale for not preferring (2)? For me, it's just like (3) but safer.

I am anxious that people will still need to write executable contracts even in the presence of ghost fields. In some of the process documentation we're working on right now, we advise to compile with assertions enabled at e.g. integration time. As I understand (2), this would be impossible.

• Quentin

[yannickmoy]

I don't think we can safely "cheat" by pretending that T'Size is not what it is for the compiler. There are too many places where we could be bitten. What about type conversions which would only be safe when the ghost code is activated? What about places where the compiler frontend (common to GNAT and GNATprove) can deduce the static value of T'Size, etc?

For executing contracts, this will still be possible outside of the unit that uses ghost fields, or even selectively in these units by enabling/disabling Ghost assertion policy. Another option is for users to switch to ghost fields of size 0 for compiling without them, but activate them by removing that constraint. There is probably a review needed to guarantee that this is not invalidating the proof, but that seems more promising.

[clairedross]

Note that if we go for executable ghost fields, it is always possible to model non-executale ones by creating a private null record type in SPARK_Mode Off with a non-executable model function giving its value. The opposite is not true however.

[yannickmoy]

@clairedross good point! I was thinking that in that case you need to provide the full API for manipulating the ghost field, but in fact you can give just the model function like you said, which returns the true SPARK type that you'd like. The only drawback is that this makes the private part of the package SPARK_Mode => Off, but that's quite reasonable for now, and you can make this as small as you want. So that looks like a suitable compromise for now.

[clairedross]

You do need to give a ghost non-executable API to modify the field indeed, axiomatized with the model function. I don't see how we could do without?

On Mon, Feb 28, 2022 at 9:43 AM yannickmoy @.***> wrote:

@clairedross https://github.com/clairedross good point! I was thinking that in that case you need to provide the full API for manipulating the ghost field, but in fact you can give just the model function like you said, which returns the true SPARK type that you'd like. The only drawback is that this makes the private part of the package SPARK_Mode => Off, but that's quite reasonable for now, and you can make this as small as you want. So that looks like a suitable compromise for now.

— Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/pull/88#issuecomment-1054019538, or unsubscribe https://github.com/notifications/unsubscribe-auth/AB6NCMKAODVS7SHV3KKA3VDU5MYUZANCNFSM5PB62UKA . Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

You are receiving this because you were mentioned.Message ID: @.***>

-- Claire Dross Senior Software Engineer, AdaCore

[yannickmoy]

Yes, to modify it, but with the model function, it's almost as good as having the field itself.