Version 1.8 of ais/ai-00209.txt
!standard H.3.1 (8) 04-05-21 AI95-00209/04
!standard H.3.2 (9)
!class binding interpretation 99-02-05
!status Amendment 200Y 04-03-24
!status WG9 Approved 04-06-18
!status ARG Approved 9-0-0 04-03-05
!status work item 99-02-05
!status received 98-10-01
!priority Medium
!difficulty Easy
!qualifier Clarification
!subject pragma Reviewable; can objects become uninitialized?
!summary
In H.3.1(8), the term "reference (to)" needs to be replaced by "read (of)".
H.3.2(9) needs to be similarly changed.
For the purposes of Pragma Reviewable, objects are uninitialized if
they never were initialized or assigned to prior to use. All such
objects must be identified by an implementation in conformance with
H.3.1(8).
An implementation may identify additional objects as uninitialized if
the value of an uninitialized object is assigned to them.
An implementation may, but need not, take advantage of aliasing
analysis or knowledge of non-executable program paths in determining
whether or not an object is initialized.
!question
When pragma Reviewable is being used, can objects become uninitialized?
Consider the following example:
declare
A : Integer := 42;
B : Integer;
C : Integer;
begin
A := C; --
B := A; --
end;
The error in the program above is clearly the first statement.
Will it be correct to state at the usage of C, that C is "possibly
uninitialized" and at the subsequent usage of A, that A is "known to be
initialized" (initialized once, always initialized)?
!recommendation
(See summary.)
!wording
H.3.1(8) should read: "For each read of a scalar object, an identification
of the read as either ....."
The second sentence of H.3.2(9) should read: "Thus an inspection point has
the effect of an implicit read of each of its inspectable objects."
!discussion
First, the term "reference" in H.3.1(8) is incorrect as it also
includes the occurrence as the target of an assignment. Clearly, only
reads of the object were meant to be diagnosed. Similarly,
the NOTE H.3.2(9) is imprecise by its usage of the term "reference".
A definitive answer to the !question seems counter-productive. A model
that allows for a "deinitialization" caused by assigning the value of
an uninitialized object may, at times, be beneficial to a programmer
interested in knowing why an operation in the program causes a value
failure of the software. This benefit cannot be obtained, if we
restrict the model to a "once assigned, always initialized" model.
On the other hand, the deinitialization model will be a significant
nuisance during an overall examination of a program in search of any
use of truly uninitialized objects. Here, the "once assigned, always
initialized" model is preferable, since, after correction of any original
uninitialized usages, the consequential "deinitializations" will have
automatically disappeared.
The main disadvantage arises, when an object remains "possibly
uninitialized" only because the compiler is unable to prove the
falsehood of the path predicate, under which the object would be
uninitialized. A user (or verification system) will then have to
examine the code to establish that on all executable paths to the
usage point the object is indeed initialized. Once this is
established, clearly no other variable can be deinitialized by being
assigned the object's value. However, if the compiler diagnostics
assume transitive infection, then these other variables will
(continue to) be diagnosed as uninitialized, misleading the user.
Consider:
if P then X := 7; end if;
...
if Q then Y := X; else Y := 6; end if;
A := Y;
B := A + 1;
Assume further that Q implies P. Of course, Y is then well defined
under all circumstances. However, the transitive infection model would
make Y, and consequently A and B, uninitialized variables, since X is
"potentially uninitialized" at this point. The fact that X is
initialized depends on the branch predicates involved and is, in
general, undecidable. Surely users will not want to laboriously
determine that Y and whatever it transitively affects, i.e., the
variables A and B, are diagnosed as "uninitialized" only
because of such situations. The non-transitive model will correctly
identify the usage of X as "potentially uninitialized" and thus
identify the cause of a potential error, but leave Y, A, and B
undiagnosed, since the problem is clearly not at the point of their
usages.
Given the two presented usage scenarios of the diagnostics, we do
not want to favor one analysis model over the other. Rather, it is
best left to the negotiations between vendors supporting this annex
and their users, which of the models should be followed by the
implementation.
An object may be initialized through an aliasing effect. As aliasing
analysis is rather difficult and, in general, undecidable, albeit not
for scalar objects, Pragma Reviewable should not require the compiler
to perform such an analysis.
In summary, the diagnostics of uninitialized objects must be
conservatively correct, that is, all uninitialized objects will be
recognized, but some objects initialized only by alias-effects or
uninitialized only on non-executable paths, or assigned the value of
an uninitialized object may also be diagnosed as uninitialized.
!corrigendum H.3.1(8)
Replace the paragraph:
- For each reference to a scalar object, an identification of the
reference as either ``known to be initialized,'' or
``possibly uninitialized,'' independent of whether pragma Normalize_Scalars
applies;
by:
- For each read of a scalar object, an identification of
the read as either ``known to be initialized,'' or ``possibly uninitialized,''
independent of whether pragma Normalize_Scalars applies;
!corrigendum H.3.2(9)
Replace the paragraph:
7 The implementation is not allowed to perform ``dead store elimination'' on
the last assignment to a variable prior to a point where the variable is
inspectable. Thus an inspection point has the effect of an implicit reference
to each of its inspectable objects.
by:
7 The implementation is not allowed to perform ``dead store elimination'' on
the last assignment to a variable prior to a point where the variable is
inspectable. Thus an inspection point has the effect of an implicit read of
each of its inspectable objects.
!ACATS Test
An ACATS test could be constructed for this feature. However, the mechanism
for reporting results is implementation-defined, so it would not fit into the
normal B or C test classifications.
!appendix
!topic pragma Reviewable; "known to be inititialized"
!reference AARM95-H.3.1(8);6.0
!from Sven Soerensen 98-07-03
<<reference as: 1998-15867.a Sven H. Sorensen 1998-7-6>>
!discussion
AARM95-H.3.1(8):
For each reference to a scalar object, an identification
of the reference as either ``known to be initialized,''
or ``possibly uninitialized,'' independent of whether
pragma Normalize_Scalars applies;
My question is:
Can scalar objects _become_ unitialized?
Consider the following example:
declare
A : Integer := 42;
B : Integer;
C : Integer;
begin
A := C; -- C is unititialized
B := A; -- Is A initialized???
end;
The error in the program above is clearly the first statement.
Will it be correct to state at the reference to C, that C is "possibly
unititialized" and at the reference to A, that A is "known to be
initialized" (initialized once, always initialized)?
If scalar objects can become unititialized it is, as far as I
can see, necessary to make a global analysis in order to claim
that that an object is "known to be initialized".
-- Sven
****************************************************
From: Jean-Pierre Rosen
Sent: Sunday, February 07, 1999 8:57 AM
>For the purposes of Pragma Reviewable, objects are uninitialized, if
>they never were initialized or assigned to prior to use. Objects
>cannot become uninitialized by assigning the value of an uninitialized
>object to them.
I find this wording misleading, because of course objects DO become
unitialized in that case, although (proposed wording)
"implementations are not required to mark as uninitialized objects
that become uninitialized due to assignment of another uninitialized
object".
****************************************************
From: Erhard Ploedereder
Sent: Monday, February 08, 1999 5:33 AM
> If find this wording misleading, because of course objects DO become
> unitialized in that case, although (proposed wording) ...
If one takes that view, how would you want to treat
A := C + 0;
with C uninitialized ?
****************************************************
From: Robert A Duff
Sent: Monday, February 08, 1999 8:20 AM
I agree with J-P. Or perhaps add "uses of" before "uninitialized objects".
Erhard writes:
> If one takes that view, how would you want to treat
> A := C + 0;
> with C uninitialized ?
Pragma Reviewable should complain about the reference to C.
The point of the AI is that having complained once about an
uninitialized variable, we shouldn't require that further
uses of that same junk value get error messages. I just don't
like the *wording* of the AI, because it seems to imply that in:
> A := C; -- C is uninitialized
> B := A; -- Is A initialized??? [Yes.]
that the value of B is somehow OK -- it's not; the value of B is
possibly junk (assuming we actually got that far, because the bounded
error wasn't caught).
I agree with the conclusion of the AI, that only one message is needed
for the above example.
For that matter, I would go further, and say that only one message is
needed for this:
X := C; -- C is uninitialized
Y := C; -- It still is
An implementation should be allowed, but not required, to give an error
message on the second use of C.
By the way, note that this section of the RM is written in a rather
informal way. It uses the term "uninitialized", which is never
precisely defined. H.3.1(8.a) makes it clear that the intent is to
allow a great deal of freedom to the compiler -- the difference between
"known to be initialized" and "possibly uninitialized" is not nailed
down -- it depends on how smart the compiler is. And other requirements
for pragma Reviewable are also written in this same informal manner.
That's fine; let's not start inventing new (more precise) requirements
that were never intended to be there.
In general, when compiler writers ask questions about this (and some
other) features of the S & S annex, I think the ARG should normally
answer something like, "Go ask your users who want these features".
- Bob
****************************************************
From: Brian Wichmann
Sent: Monday, February 08, 1999 8:41 AM
Bob's got it right. pragma Reviewable is to aid those who have to
check the object code produced by the compiler because the consequences
of a undetected compiler bug are unacceptable. It has to be informal,
since it is unreasonable to tie down the analysis that the compiler
performs (which is likely to depend upon optimization).
Brian.
****************************************************
From: Robert Dewar
Sent: Monday, February 08, 1999 9:17 AM
Requirements that are not formalizable are junk and should not be in the RM,
or if they are there, can be ignored. Such requirements should at best appear
as implementation advice. I am afraid there is quite a bit of this kind of
junk in annex H!
****************************************************
From: Robert A Duff
Sent: Monday, February 08, 1999 10:50 AM
Perhaps, but we shouldn't try to change it now! If the ARG tries to
formalize all of Annex H, it will waste a lot of time, and cause a lot
of trouble for implementers. Better to let these things be worked out
between vendors and their customers (those customers who care about
safety, I mean).
- Bob
****************************************************
From: Robert Dewar
Sent: Monday, February 08, 1999 10:54 AM
No leave it as it is, and spend ZERO time trying to figure out what it
means if anything. The ARG has better things to do. Let the HRG spend
its time on this :-)
****************************************************
From: Robert A Duff
Sent: Monday, February 08, 1999 10:57 AM
In reference to H.3.1(8), Robert says:
> Yes, but that's a meaningless requirement, the compiler can simply say
> "all references to scalars are "possibly uninitialized"
> and that meets the (silly) requirement.
Sure, and the AARM annotation points out that a "lazy" compiler could do
just that.
On the other hand, a compiler can't say "all references are known to be
initialized".
Please remember why we're talking about the issue -- some compiler
vendor asked what they are supposed to do in certain specific cases. I
believe I advocated some time ago that the ARG tell the compiler vendor
"we don't know -- go ask your customers". But the ARG wanted to answer
the question. Fine. But please don't take this as an invitation to
rewrite the whole annex!
- Bob
****************************************************
From: Robert I. Eachus
Sent: Monday, February 08, 1999 11:17 AM
I totally agree. For example, an implementation might print out a (set
of) warning messages like:
foo.adb:23:14 Warning: Bar may be referenced before it is intialized.
to the standard error output, rather than interspersed in the source
listing. Is this non-conforming? Of course not! There is no requirement
for a source listing with pragma Reviewable. For example in ada-mode, I
would much prefer this approach. Should a compiler be dinged for providing
only one such message for each such variable instead of six hundred and
three?
****************************************************
From: Jean-Pierre Rosen
Sent: Monday, February 08, 1999 1:12 PM
>> If find this wording misleading, because of course objects DO become
>> unitialized in that case, although (proposed wording) ...
>
>If one takes that view, how would you want to treat
> A := C + 0;
>with C uninitialized ?
Right, I should have said "initialized with an uninitialized
*expression* (not variable). Well, maybe there is no such thing as an
uninitialized expression...
The point is to acknowledge that the compiler must identify variables
that are not assigned a value, not variables that are uninitialized for
more complex reasons.
****************************************************
Questions? Ask the ACAA Technical Agent