Version 1.5 of 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 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;
--
--
!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