Version 1.6 of ai05s/ai05-0191-1.txt

Unformatted version of ai05s/ai05-0191-1.txt version 1.6
Other versions for file ai05s/ai05-0191-1.txt

!standard 13.3(9/1)          10-10-30 AI05-0191-1/04
!standard 13.3(73)
!class amendment 09-11-03
!status Amendment 2012 10-11-18
!status ARG Approved 7-0-3 10-10-30
!status work item 09-11-03
!status received 09-11-03
!priority Low
!difficulty Medium
!subject Aliasing predicates
!summary
Two attributes are defined for all objects to allow determination of partial or full aliasing with another object.
!problem
In writing preconditions, one often wants to preclude aliasing situations that would affect the outcome of a subprogram. Thus, predicates like
Are_Overlapping(A(I..K), A(J..L))
or Are_Same(A,B) would be desirable, where the first asserts that the two arguments overlap in memory, and the second asserts that the two arguments are in fact occupying the exact same memory location.
Yet, formulating these predicates in Ada is cumbersome and error prone.
It would be nice to provide these predicates as part of the language definition.
!proposal
(See wording.)
!wording
Change 13.3(9/1) as follows: The following representation attributes are defined: Address, Alignment, Size, Storage_Size, [and] Component_Size{, Is_Same, and Overlaps}.
Add after 13.3(73):
Static Semantics:
For a prefix X that denotes an object:
X'Is_Same
X'Is_Same denotes a function with the following specification:
function X'Is_Same(@i(A : any_type)) return Boolean;
The actual parameter shall be a name that denotes an object. The object denoted by the actual parameter can be of any type. This function evaluates the names of the objects involved and returns true if the representation of the object denoted by the actual parameter occupies exactly the same bits as the representation of the object denoted by X; it is false otherwise.
AARM Note: Is_Same means that, if the representation is contiguous, the objects sit at the same address and occupy the same length of memory.
Static Semantics:
For a prefix X that denotes an object:
X'Overlaps
X'Overlaps denotes a function with the following specification:
function X'Overlaps(@i(Arg: any_type))
return Boolean;
The actual parameter shall be a name that denotes an object. The object denoted by the actual parameter can be of any type. This function evaluates the names of the objects involved and returns true if the representation of the object denoted by the actual parameter shares at least one bit with the representation of the object denoted by X; it is false otherwise.
NOTES:
X'Is_Same(Y) implies X'Overlaps(Y).
X'Is_Same(Y) and X'Overlaps(Y) are not considered to be reads of X and Y.
!discussion
Casting such memory-related predicates into the semantic framework of Ada 2005 is surprisingly difficult.
Since these predicates are defined over the location of the arguments rather than their values, a definition that employs "normal" boolean functions with these objects as arguments cannot achieve the desired purpose. Passing parameters by value would have to be prohibited for such functions, which would call for language definition magic. In addition, fixing the type of the parameter(s) introduces restrictions on the generality of the functions.
For the same reason, the user cannot define an encapsulating function computing either predicate for types that allow for passing parameters by value. At best, he or she can pass addresses and representation lengths to a function that performs the necessary calculations and comparisons. This is a rather unsatisfactory situation, given that these aliasing predicates are conceptually straightforward.
Given some language magic to solve the parameter passing issue, one then needs to address the typing of the arguments. Type-safe full aliasing can arise for named entities of the same type or of derivation-related types, where one entity denotes a view of the other under a different type. The predicate then needs to accept arguments of equal types or of derivation-related types. Alternatively one could ask the user for a view conversion to the same type - the solved parameter passing issue makes sure that the view conversion is not seen as a value conversion. (It will be seen as a nuisance, though.)
However, this does not cover aliasing achieved by unchecked or unsafe programming, as is needed occasionally, e.g., in implementing heap management. To extend the predicates to cover this case as well, the Is_Same predicate needs to accommodate arguments of arbitrary, unrelated types. For the Overlaps predicate, an argument of any type needs to be accepted in any case (or, in a strictly type-safe variant, any subcomponent type). Again, this cannot be reasonably done without language magic. Generics are not a good answer, since the needed instantiations are gratuitous; they cannot check for anything and merely add text to the code.
Among several alternatives (rejected alternatives include a magic predefined package with predicate definitions or predefined predicates) a solution via predefined attributes of objects is selected:
O'Is_Same(X: <any type>) O'Overlaps(X: <any type>)
Is_Same returns true if the argument X occupies exactly the same memory space as O, it returns false otherwise.
Overlaps returns true if the argument X shares any part of the memory space with O, it returns false otherwise. Is_Same implies Overlaps.
It has been suggested to define Not_Same and Not_Overlaps instead, since most predicates will assert the absence of aliasing. While this is true, the extreme ugliness of "not Not_Overlaps" to assert partial aliasing speaks in favor of not using negatives as predefined boolean attributes.
It has been suggested that Is_Same could require the same type as the object whose attribute is queried to make the check more efficient. A simplification of the check would be possible only if the same constrained subtype were required. Also, the dissimilarity to Overlaps is a (small) argument against it; the major counter-argument is the exclusion of type-unsafe aliasing. A compiler can optimize the Is_Same attribute to a simple address equality when it recognizes the (sub)types of the objects to have equal length.
The attributes are styled along the existing attribute 'Val, even though the referential nature of the actual argument requires a deviation from the normal model of functions.
!example
procedure Exchange_Values(A, B: ref_type) Assert(not A'IsSame(B));
Assert(not A'Overlaps(B(i))); A(B(i)) := A(B(i)) + 1; -- intended to count in A the number of value occurrences in B -- part of a distribution sort
!ACATS test
An ACATS C test is needed for this feature.
!ASIS
Add two literals An_Is_Same_Attribute and An_Overlaps_Attribute to Attritbute_Kinds.
!appendix

From: Erhard Ploedereder
Sent: Sunday, June 14, 2009  2:40 AM

A frequent precondition is that parameter objects (and global objects) do not
overlap in memory. This precondition is a bit painful to write correctly with
current language means.

There should be some library-provided boolean function Is_Overlapping or Overlaps.

A broader question is whether there are other frequently required predicates
that could be standardized by the language. If so, the ARG should decide on the
method of provision, so that we do not end up with built-ins, attributes, libraries,
magic incantations, joyfully mixed.

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

From: Robert Dewar
Sent: Sunday, June 14, 2009  4:02 AM

This has to be an attribute to be useful, you don't want to have to instantiate
a generic for every possible type that might be involved in such a test, also
passing values is useless, and we can't expect to be able to use 'Access in
general, passing 'Size and 'Address is ugly, and anyway, won't work with all
parameter forms.

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

From: Randy Brukardt
Sent: Monday, October 25, 2010 11:59 PM

> Here is my rewrite of AI-191 (still on the 25th ;-)

You're lucky I tried to file the mail on AI-177 instead of going home at a
reasonable hour...

...
> Change 13.3 9/1 as follows: The following representation attributes
> are defined: Address, Alignment, Size, Storage_Size, [and]
> Component_Size{, External_Tag, Is_Same and Overlaps}.
>
> <<<<< Note old bug: the External_Tag needs to be added in any case.
> >>>>

This is not a bug: External_Tag is an operational, not representation,
attribute. Its header can be found at 13.3(73.1/1).

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

From: Erhard Ploedereder
Sent: Tuesday, October 26, 2010  1:10 AM

> This is not a bug: External_Tag is an operational, not representation, 
> attribute.

Oops. Then the new text needs to go a few paragraphs further up, I guess.

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

From: Robert Dewar
Sent: Saturday, October 30, 2010 4:46 PM

[He's referring to version /03, previously posted and not repeated here -
Editor.]

I really don't like the name Is_Same, seems much too generic, and sounds like it
is testing for identical entities or somesuch, I would use

Overlapping_Address_Range
Same_Address_Range

since this is what this is really about.

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

From: Tucker Taft
Sent: Saturday, October 30, 2010 5:35 PM

Address_Range is misleading.  "Range" in Ada implies contiguous, while we are
trying to accommodate discontiguous representations.

Something like "Occupies_Same_Bits" might be appropriate.  Or perhaps
X'Overlays(Y) when they shall all of their bits, and X'Overlaps(Y) when they
share at least one bit.

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

From: Robert Dewar
Sent: Saturday, October 30, 2010 5:37 PM

OK, I think worrying about non-contiguous representations is probably
unnecessary in practice, but I see what you mean. Yes, either of those would be
OK.

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

From: Erhard Ploedereder
Sent: Saturday, October 30, 2010 6:01 PM

I preferred some more abstract terms to be closer to the concept "Aliasing" that
to the concept "Representation". After all, I expect their use in Assertions and
Pre- and Postconditions.

Is_Same may be a bit bland. Fully_Aliased and Partially_Aliased was where I
started. I'd rather not have the bits creep into the name.

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

From: Bob Duff
Sent: Saturday, October 30, 2010 6:06 PM

> > Address_Range is misleading.  "Range" in Ada implies contiguous,
> > while we are trying to accommodate discontiguous representations.

More importantly, we want to accomodate packed bit-fields.

> > Something like "Occupies_Same_Bits" might be appropriate.  Or
> > perhaps X'Overlays(Y) when they shall all of their bits, and
> > X'Overlaps(Y) when they share at least one bit.

I like ..._Same_Bits.  Is_Same is really way too general of a name.

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

From: Robert Dewar
Sent: Saturday, October 30, 2010  6:32 PM

> More importantly, we want to accomodate packed bit-fields.

True, that does make sense ...

> I like ..._Same_Bits.  Is_Same is really way too general of a name.

So perhaps Same_Bits and Overlapping_Bits

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

From: Gary Dismukes
Sent: Saturday, October 30, 2010 9:40 PM

> Is_Same may be a bit bland. Fully_Aliased and Partially_Aliased was
> where I started. I'd rather not have the bits creep into the name.

How about something like Has_Same_Storage and Overlaps_Storage?
That would avoid mentioning bits.  Maybe still too low-level?

Tucker's suggestions of Overlays and Overlaps also seem OK, though it's too bad
they only differ in one character.

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

From: Robert Dewar
Sent: Sunday, November 7, 2010  8:43 AM

> How about something like Has_Same_Storage and Overlaps_Storage?
> That would avoid mentioning bits.  Maybe still too low-level?

This *is* a low level thing that cannot be explained easily in formal terms, so
it is fine to have low level names. I like these ones.

> Tucker's suggestions of Overlays and Overlaps also seem OK, though
> it's too bad they only differ in one character.

Seems too high level to me. The question is are we talking about some low level
check, or some high level semantic attribute with full "as-if" rules in place. I
think the former!

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

From: Tucker Taft
Sent: Sunday, November 7, 2010  9:01 AM

I also like "Has_Same_Storage" and "Overlaps_Storage."
Getting the word "storage" in there seems to remove some of the ambiguity,
without introducing the somewhat jarring word "bits" into the names.

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

From: Robert Dewar
Sent: Saturday, October 30, 2010 5:12 PM

> X'Is_Same(Y) and X'Overlaps(Y) are not considered to be reads of X and Y.

No, but in a case like

   X.A'Overlaps(Y.B)

if the records X and Y have dynamic components you may need to read all sorts of
bound information etc from the record to figure out the addresses of the two
fields???

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

From: Erhard Ploedereder
Sent: Saturday, October 30, 2010 5:56 PM

> No, but in a case like
>
>   X.A'Overlaps(Y.B)
>
>> if the records X and Y have dynamic components you may need to read
> all sorts of bound information etc from the record to figure out the
> addresses of the two fields???

Same is true for A(i)'Overlaps(C), but this still is logically no read of A(i).
The point was that these attributes work on uninitialized variables or on those
with invalid values. Hence also the "evaluates the name".

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


Questions? Ask the ACAA Technical Agent