CVS difference for ai05s/ai05-0289-1.txt
--- ai05s/ai05-0289-1.txt 2012/03/15 05:17:02 1.2
+++ ai05s/ai05-0289-1.txt 2012/05/11 04:52:49 1.3
@@ -851,7 +851,7 @@
****************************************************************
From: Randy Brukardt
-Sent: Monday, March 14, 2012 9:31 PM
+Sent: Wednesday, March 14, 2012 9:31 PM
The last bit of 7.3.2(21/3) says:
@@ -868,8 +868,21 @@
****************************************************************
+From: Erhard Ploedereder
+Sent: Thursday, March 15, 2012 5:26 AM
+
+> Invariant checks, any postcondition check, and any constraint {or
+> predicate} checks associated with by-copy in out or out parameters are
+> performed in an arbitrary order.
+
+Fix it, of course. (I am tempted to ask for "subtype predicate" in lieu of just
+"predicate", but I bow to uniformity if the "subtype" is consistently missing
+throughout the RM.)
+
+****************************************************************
+
From: Randy Brukardt
-Sent: Monday, March 14, 2012 10:20 PM
+Sent: Wednesday, March 14, 2012 10:20 PM
After sending the last message, I though of a slightly more important bug:
@@ -977,5 +990,493 @@
________ Recheck everything after a call as described above. (The
fewer holes the better.)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, March 14, 2012 10:27 PM
+
+And my vote in this straw poll:
+
+> So now I'm just 100% confused. There seem to be three possibilities;
+> please vote for one and explain if you want:
+>
+> __3/4th__ Leave 3.2.4(22/3) unmodified. (We're not going
+> to try to make Dynamic_Predicates "work"; it's
+> impossible.)
+>
+> __1/4th__ Recheck a by-reference parameter of any mode
+> after a call; don't check by-copy parameters.
+> (The by-copy parameter is unmodified, and if a
+> Dynamic_Predicate changes value by other reason, we're
+> not trying to keep it working. OTOH, it's possible to
+> modify an "in" parameter via the Rosen technique, so
+> rechecking makes sense.)
+>
+> ________ Recheck everything after a call as described above.
+> (The fewer holes the better.)
+
+I'm torn on this one. There is an argument that by-reference parameters should
+recheck; these could have their values changed and thus a recheck is a good
+idea. The constraints can't change by definition, but the predicate can. OTOH, a
+by-copy parameter can never change value and we don't recheck constraints on
+them unless they do change, so why treat predicates differently?
+
+But that seems pretty weird, so I lean toward saying that we already have it
+right. Thus the split vote above.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March 15, 2012 9:47 AM
+
+> After sending the last message, I though of a slightly more important bug:
+>
+> 3.2.4 also defines predicate checks on by-reference in out or out
+> parameters. Probably that sentence of 7.3.2(21/3) ought to include
+> them as well:
+>
+> Invariant checks, any postcondition check, and any constraint {or
+> predicate}
+> checks associated with [by-copy] in out or out parameters are performed
+> in an arbitrary order.
+>
+> But that set me to wondering: we changed the rules for invariants so
+> that they're checked for all parameters on the way out, regardless of mode.
+> Should we have done something similar for predicates as well?
+
+I would say "yes" for dynamic predicates, and "no" for static predicates.
+Dynamic predicates were specifically intended to handle cases involving
+indirection, etc., so it seems to make sense to check them at the same points we
+check type invariants. Static predicates don't need to be rechecked since they
+are specifically defined to behave more like range constraints.
+
+And because of indirection, by-copy vs. by-reference is irrelevant to the issue
+here.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March 15, 2012 5:39 PM
+
+> I would say "yes" for dynamic predicates, and "no" for static
+> predicates. Dynamic predicates were specifically intended to handle
+> cases involving indirection, etc., so it seems to make sense to check
+> them at the same points we check type invariants. Static predicates
+> don't need to be rechecked since they are specifically defined to
+> behave more like range constraints.
+>
+> And because of indirection, by-copy vs. by-reference is irrelevant to
+> the issue here.
+
+Fascinating. I gave three options, and you managed to invent a 4th. :-)
+
+I had rejected that possibility because it seemed very weird, especially as we
+allow static predicates on all types. So we still would need the current rule
+for static predicates and then a new rule for dynamic predicates. Beyond that,
+by-copy vs. by-reference does matter in the wording of the rule, at least,
+because for by-copy parameters (in out or out), the copy back does the check
+"naturally" (it falls out of the rules for subtype conversion). So we only need
+an extra check in other cases; and listing those makes the rule rather messy.
+
+Probably the best way to do that would be to implement a separate sentence after
+the existing one (but we have to be careful not to create two different
+predicates for a subtype):
+
+... After normal completion and leaving of a subprogram, for each in out or out
+parameter that is passed by reference, the predicate of the subtype of the
+actual is evaluated, and a check is made that the predicate is True. {Similarly,
+for every parameter of mode in, if the subtype of the actual has any dynamic
+predicates that apply, the predicate of the subtype of the actual is evaluated,
+and a check is made that the predicate is True.} ...
+
+AARM Ramification: For a parameter of mode in, if the subtype of the actual has
+only static predicates, no check is made after returning.
+
+Consider this choice #4.
+
+I'm unconvinced that this is a good idea. Besides the general clunkiness, it's
+not clear to me that this is the right split. A static predicate can be applied
+to a by-reference type, after all (although it would be hard for it to do much),
+so it's possible for it to occur on a type that uses the Rosen technique. OTOH,
+since it doesn't allow any components, I can't quite imagine how it could change
+(today). OT3H, it would make sense for these to allow access to bounds and
+discriminants of the type (not in Ada 2012, of course), and doing so would make
+this rule a bad choice. OT4H, we'd probably change it then.
+
+In any case, at this point, we have 1.75 votes for option #1 (do nothing), 0.25
+votes for option #2, and 1 vote for option #4. That doesn't give me enough
+guidance even to do nothing, so I hope that others will weight in on this topic.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Thursday, March 15, 2012 6:05 PM
+
+> ... After normal completion and leaving of a subprogram, for each in
+> out or out parameter that is passed by reference, the predicate of the
+> subtype of the actual is evaluated, and a check is made that the predicate is True.
+> {Similarly, for every parameter of mode in, if the subtype of the
+> actual has any dynamic predicates that apply, the predicate of the
+> subtype of the actual is evaluated, and a check is made that the predicate is True.} ...
+>
+> AARM Ramification: For a parameter of mode in, if the subtype of the
+> actual has only static predicates, no check is made after returning.
+>
+> Consider this choice #4.
+
+Sounds fine to me.
+
+> I'm unconvinced that this is a good idea. Besides the general
+> clunkiness, it's not clear to me that this is the right split. A
+> static predicate can be applied to a by-reference type, after all
+> (although it would be hard for it to do much), so it's possible for it
+> to occur on a type that uses the Rosen technique.
+
+I am not following you here. I thought an important property of a static
+predicate was that it involves the use of the predefined comparison, equality,
+or membership operations against static expressions (i.e. scalars or strings),
+so there are no indirections possible, and the specified places for checks are
+sufficient to ensure that the predicate remains true everywhere.
+
+> ... OTOH, since it doesn't allow any components, I can't quite imagine
+> how it could change (today). OT3H, it would make sense for these to
+> allow access to bounds and discriminants of the type (not in Ada 2012,
+> of course), and doing so would make this rule a bad choice. OT4H, we'd
+> probably change it then.
+
+It wouldn't be a "static predicate" if you started changing the rules in this
+way.
+
+> In any case, at this point, we have 1.75 votes for option #1 (do
+> nothing),
+> 0.25 votes for option #2, and 1 vote for option #4. That doesn't give
+> me enough guidance even to do nothing, so I hope that others will
+> weight in on this topic.
+
+Vote for option #4! Vote for option #4!
+The rest are junk.
+
+Never mind, that was my Super PAC talking... ;-)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, March 15, 2012 6:26 PM
+
+...
+> > I'm unconvinced that this is a good idea. Besides the general
+> > clunkiness, it's not clear to me that this is the right split. A
+> > static predicate can be applied to a by-reference type, after all
+> > (although it would be hard for it to do much), so it's possible for
+> > it to occur on a type that uses the Rosen technique.
+>
+> I am not following you here. I thought an important property of a
+> static predicate was that it involves the use of the predefined
+> comparison, equality, or membership operations against static
+> expressions (i.e. scalars or strings), so there are no indirections
+> possible, and the specified places for checks are sufficient to ensure
+> that the predicate remains true everywhere.
+
+I think you are right, but it mostly follows from general uselessness of static
+predicates on composite types and not from any well-defined principle. Indeed, I
+think I would have preferred that static predicates were only allowed on scalar
+types, in which case this discussion would not have come up.
+
+> > ... OTOH, since it doesn't allow any components, I can't quite
+> > imagine how it could change (today). OT3H, it would make sense for
+> > these to allow access to bounds and discriminants of the type (not
+> > in Ada 2012, of course), and doing so would make this rule a bad
+> > choice. OT4H, we'd probably change it then.
+>
+> It wouldn't be a "static predicate" if you started changing the rules
+> in this way.
+
+The bounds and non-mutable discriminants of a subtype can never change from an
+object after its creation. So it's hard to imagine how the predicate of the
+subtype of an object could change if it depended on those things. If we're going
+to allow static predicates on composite types, they might as well be useful.
+
+I suspect that mutable discriminants act pretty similarly to the stand-alone
+scalar objects for which static predicates are currently designed. So I think
+they too would not cause any problems -- but that would have to be verified (and
+surely not right now).
+
+My main point is that there are two possible views of static predicates: (1) a
+special gizmo to allow case statements/loops/etc.; and (2) a user-defined
+constraint that has similar properties to the built-in constraints.
+
+If (1), we should have restricted static predicates only to scalar (or maybe
+discrete) types. The gizmo only works there, and allowing more is just
+confusing. If (2), then why we don't allow bounds and discriminants (allowed in
+real constraints, after all) is not clear. The current rules are just weird
+because they don't really support either view quite right. (But this is an
+insufficient problem to worry about for Ada 2012 -- although if we don't
+restrict the use of static predicates now, then I presume we're leaning [sooner
+or later] to view (2), and thus some expansion of static predicates in the
+future should be expected.)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Thursday, March 15, 2012 9:40 PM
+
+One of the reasons I think that doing nothing is fine is that in practice I
+suspect we will have to revisit details like this anyway, no matter what we
+decide now. In particular, adding or subtracting predicate checks is something
+that will have very little impact and can certainly be done later.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Friday, March 16, 2012 4:47 AM
+
+> please
+> vote for one and explain if you want:
+>
+> ________ Leave 3.2.4(22/3) unmodified. (We're not going to
+> try to make Dynamic_Predicates "work"; it's impossible.)
+>
+> ________ Recheck a by-reference parameter of any mode after
+> a call; don't check by-copy parameters.
+> (The by-copy parameter is unmodified, and if a
+> Dynamic_Predicate changes value by other reason, we're not
+> trying to keep it working. OTOH, it's possible to
+> modify an "in" parameter via the Rosen technique, so
+> rechecking makes sense.)
+>
+> ________ Recheck everything after a call as described above.
+> (The fewer holes the better.)
+
+Abstain (not helpful to Randy), due to insufficiant understanding of the issues.
+
+Some thoughts though:
+IIUC, the problem is when an in out parameter is passed by reference, the actual
+has a dynamic predicate that the formal has not, and /something in the called
+subprogram changes the dynamic predicates in such a way that it does not hold
+any more/. I tend to think "what's the heck, the guy who does that gets what he
+deserves" (enforces my abstention).
+
+What happens in the case of null exclusion? i.e. if the actual excludes null,
+but not the formal? Hmmph, it's passed by copy, so there is no issue... Saved by
+the gong. I think that, had we had predicates in 2005, there would have been no
+null exclusion. We can argue if predicates should behave like constraints, but
+null exclusion should really behave the same as Static_Predicate => ptr /= null.
+
+> My main point is that there are two possible views of static
+> predicates: (1) a special gizmo to allow case statements/loops/etc.;
+> and (2) a user-defined constraint that has similar properties to the built-in
+> constraints.
+>
+> If (1), we should have restricted static predicates only to scalar (or maybe
+> discrete) types. The gizmo only works there, and allowing more is just
+> confusing. If (2), then why we don't allow bounds and discriminants
+> (allowed in real constraints, after all) is not clear. The current
+> rules are just weird because they don't really support either view
+> quite right. (But this is an insufficient problem to worry about for
+> Ada 2012 -- although if we don't restrict the use of static predicates
+> now, then I presume we're leaning [sooner or later] to view (2), and
+> thus some expansion of static predicates in the future should be
+> expected.)
+
+I support 2), with a growing feeling that dynamic predicates are really
+different from static predicates. In practice, I think there will be 3 uses of
+predicates:
+
+1) Static predicates (behave like constraints)
+2) Dynamic predicates that the user would have liked to be static, but that are
+ just too complicated. Don't expect the predicate to change during execution.
+ (behave like constraints)
+3) Sophisticated dynamic predicates (behave like assertions)
+
+The hard part of the discussion is due to the presence of 2)
+
+****************************************************************
+
+From: Jeff Cousins
+Sent: Friday, March 16, 2012 5:02 AM
+
+> I think you are right, but it mostly follows from general uselessness
+> of static predicates on composite types and not from any well-defined
+> principle. Indeed, I think I would have preferred that static predicates were
+> only allowed on scalar types, in which case this discussion would not have
+> come up.
+
+I don't think that many users are expecting predicates on composite types, and
+the one example in the rationale (actually a dynamic predicate) shows that it
+can have dodgy consequences.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Friday, March 16, 2012 11:47 AM
+
+I am abstaining, even though I am leaning towards the "Recheck everything" position. My reasons are
+
+- it is indeed very late to start fixing a complicated area
+
+- I feel deeply uncomfortable about a model that allows false
+ predicates to go unchecked at interface boundaries (which is
+ the case today even without "Ignore"). The term "as described
+ above" unfortunately makes the "Recheck everything" a rather
+ relative "everything", which I'd rather not discuss again at this
+ late stage. If it meant: "Check all predicates for all types and
+ parameter modes (and permit optimizing checks away even if the
+ predicates have side-effects)" then my vote is for "Recheck
+ Everything".
+
+****************************************************************
+
+From: Tullio Vardanega
+Sent: Friday, March 16, 2012 12:12 PM
+
+I abstain to the vote options as proposed.
+
+Other than that, I am leaning toward Erhard's "recheck everything"
+in the less extensive interpretation of "everything" that he suggests.
+
+****************************************************************
+
+From: Jeff Cousins
+Sent: Friday, March 16, 2012 12:54 PM
+
+I think I have to abstain too, though I'd support any of Randy's ideas to limit
+predicates to scalars.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, March 16, 2012 2:12 PM
+
+> [...]
+
+I vote for:
+
+ ___X____ Leave 3.2.4(22/3) unmodified.
+
+> ...(We're not going to try to
+> make Dynamic_Predicates "work"; it's impossible.)
+
+I take the above to be irrelevant editorializing. ;-) My vote neither agrees
+nor disagrees with it.
+
+The rationale for my vote is: (1) same as Robert, I don't see any reason for
+last-minute changes. (2) I'm concerned that the proposed wording changes make a
+difference between whether the compiler chose by-ref vs. by-copy. I don't know
+if that's true, but I don't want to study the issue (at the last minute!). If it
+is true, I'm definitely opposed -- opposed to having compiler choices affect
+whether certain parameters are checked.
+
+I will not carefully read the rest of this discussion (until we consider it
+again as an Ada 2012 AI).
+
+I'm puzzled by the two "abstain" votes I noticed. If you don't understand the
+issues, or don't want to think about them at this late date, I'd think you'd
+vote for "leave unmodified".
+
+****************************************************************
+
+From: Geert Bosch
+Sent: Friday, March 16, 2012 2:47 PM
+
+> ____X___ Leave 3.2.4(22/3) unmodified. (We're not going to
+> try to make Dynamic_Predicates "work"; it's impossible.)
+
+It's too late to consider anything else.
+
+****************************************************************
+
+From: Brad Moore
+Sent: Friday, March 16, 2012 3:20 PM
+
+> There seem to be three possibilities; please
+> vote for one and explain if you want:
+>
+> _____X___ Leave 3.2.4(22/3) unmodified. (We're not going to try
+> to make Dynamic_Predicates "work"; it's impossible.)
+>
+
+I agree with others that it it's too late to perfect this now. Fixing for Ada
+2020 is a better choice, as I think we will need some time to come up with a
+solution that will provide an acceptable level of confidence going forward.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, March 16, 2012 6:34 PM
+
+> I am abstaining, even though I am leaning towards the "Recheck
+> everything" position. My reasons are
+>
+> - it is indeed very late to start fixing a complicated area
+>
+> - I feel deeply uncomfortable about a model that allows false
+> predicates to go unchecked at interface boundaries (which is
+> the case today even without "Ignore"). The term "as described
+> above" unfortunately makes the "Recheck everything" a rather
+> relative "everything", which I'd rather not discuss again at this
+> late stage.
+
+I'm not sure that you understood my point with "as described above"; there was a
+specific wording proposal given in my original message, and I was referring to
+that specifically when I said "as described above".
+
+That wording explicitly excluded by-copy in out and out parameters from the
+extra check; that's simply because they are checked by the subtype conversion
+implicit in the copy-back. Having rules that mandate *two* checks for a single
+parameter at a single point would be completely insane.
+
+But the effect would be that every actual parameter would be rechecked after a
+call.
+
+(Note a problem with that wording: not all "in" parameters are even objects that
+can be checked after the call -- if they are just values, they have no subtype
+and trying to talk about it is dodgy.)
+
+> If it meant: "Check all predicates for all types and
+> parameter modes (and permit optimizing checks away even if the
+> predicates have side-effects)" then my vote is for "Recheck
+> Everything".
+
+Yes, that's the effect. The parenthetical remark is always true anyway, because
+we already have a rule to that effect (11.4.2(26/3)). Of course, it will rarely
+be the case that one could apply that rule to a dynamic predicate (just as for
+invariants), because the compiler would have to be able to prove that the value
+of the expression did not change on a re-evaluation. That's impossible in
+general; only dynamic predicates that don't contain any globals (including any
+dereferences to storage pools) and no functions whose implementation is unknown
+could possibly work, and those will be fairly rare.
+
+In any case, there is no model of dynamic predicates that will ever make them
+"safe", for any definition of "safe". The only question is how far to go?
+
+For static predicates, of course they can be optimized; and no permissions are
+needed to be able to do it (they can't have any side-effects or globals).
+
+Anyway, it looks like this should be an AI12, because its pretty obvious that
+there is neither consensus for a change nor any critical urgency. (Mandating
+additional checks would only be incompatible in programs that were already
+broken, so it is hard to get very concerned.)
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Saturday, March 17, 2012 9:26 PM
+
+> I'm puzzled by the two "abstain" votes I noticed.
+> If you don't understand the issues, or don't want to think about them
+> at this late date, I'd think you'd vote for "leave unmodified".
+
+Very easy. Voting to leave it unmodified would say that I "sort of agree" with
+the position, which I definitely do not (but the vote did not have a "none of
+the above" option).
+
+****************************************************************
+
+From: Bob Duff
+Sent: Sunday, March 18, 2012 8:08 AM
+
+OK, fair enough. My vote for "leave unmodified" means "leave unmodified for
+now". It doesn't mean I agree (not even "sort of") with what we've got.
****************************************************************
Questions? Ask the ACAA Technical Agent