CVS difference for ais/ai-00209.txt

Differences between 1.1 and version 1.2
Log of other versions for file ais/ai-00209.txt

--- ais/ai-00209.txt	1998/10/01 19:03:10	1.1
+++ ais/ai-00209.txt	1999/02/08 23:00:59	1.2
@@ -1,16 +1,28 @@
-!standard H.3.1     (8)                             98-10-01  AI95-00209/00
-!class confirmation 98-10-01
+!standard H.3.1     (8)                             99-02-05  AI95-00209/01
+!class binding_interpretation 99-02-05
+!status work item 99-02-05
 !status received 98-10-01
 !priority Medium
 !difficulty Easy
 !subject pragma Reviewable; can objects become uninitialized?
 
-!summary 98-10-01
+!summary 99-02-05
 
+In H.3.1(8), the term "reference (to)" needs to be replaced by "usage
+(of the value of)".
 
+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. Formal IN and IN OUT parameters are always considered
+initialized.
+
+An implementation may, but need not, take advantage of aliasing analysis in
+determining whether or not an object is initialized.
+
 !question 98-10-01
 
-When pragma Reviewable is being used, can objects become uninitialized?
+When pragma Reviewable is being used, can objects become uninitialized? [No.]
 
 Consider the following example:
 
@@ -19,19 +31,80 @@
    B : Integer;
    C : Integer;
 begin
-   A := C;  -- C is unititialized
-   B := A;  -- Is A initialized???
+   A := C;  -- C is uninitialized
+   B := A;  -- Is A initialized??? [Yes.]
 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)?
+
+!recommendation 99-02-05
+
+(see summary)
+
+!wording 99-02-05
+
+H.3.1(8) should read: "For each usage of the value of a scalar object,
+an identification of the usage as either ....."
 
-!response 98-10-01
+!discussion 99-02-05
+
+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
+usages of the value of the object were meant to be diagnosed.
+
+If assignments of uninitialized values to objects were to
+"deinitialize" their target objects, the benefits of the diagnostics
+would be lessened, since they would no longer distinguish between
+truly uninitialized objects and those that were transitively
+affected.
+
+The main disadvantage arises, when an object remains "possibly
+uninitialized" only because the compiler is unable to prove the
+falsehood of the path predicate, on 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 need
+to 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 P then Y := X; end if;
+Of course, Y is well defined under all circumstances. However,
+the transitive infection model would make Y an uninitialized
+variable, 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) is diagnosed as "uninitialized" only
+because of the situation above.
+
+As a smaller issue, a transitive model would have to explain
+the difference between
+    A := C;
+and
+    A := C + 0;
+    A:= f(X); -- with f referencing C in its result computation
+Do the latter assignments also deinitialize if C is uninitialized ?
+
+We conclude that assignments by ininitialized objects should not
+deinitialize the target object.
+
+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. The effect on the diagnostics of uninitialized
+objects is conservatively correct, that is, all uninitialized objects
+will be recognized, but some objects initialized only by alias-effect
+will also be diagnosed as uninitialized.
 
 
-!appendix 98-10-01
+!appendix 99-02-08
 
 !topic pragma Reviewable; "known to be inititialized"
 !reference AARM95-H.3.1(8);6.0
@@ -70,6 +143,196 @@
 
 
 -- 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