CVS difference for ai05s/ai05-0274-1.txt
--- ai05s/ai05-0274-1.txt 2012/01/05 06:19:33 1.4
+++ ai05s/ai05-0274-1.txt 2012/02/14 03:34:35 1.5
@@ -1,9 +1,10 @@
-!standard 6.1.1(0) 11-12-22 AI05-0274-1/04
+!standard 6.1.1(0) 12-02-13 AI05-0274-1/05
!standard 11.4.2(1/2)
!standard 11.4.2(23/2)
!standard 11.4.2(25/2)
!class Amendment 11-11-11
!status Amendment 2012 11-11-12
+!status work item 11-12-27
!status ARG Approved 6-1-2 11-11-12
!status work item 11-11-11
!status received 11-11-11
@@ -110,6 +111,28 @@
normally with the affected assertion, but the assertion expression need not hold
if immediately reevaluated.
+[** Editor's note: There is some agreement that the above is too vague. After
+discussion with Tucker, the best I was able to come up with was:
+
+ It is a bounded error if within an assertion expression (directly or
+ indirectly) there is a function call F that alters the value of a variable
+ that is read (directly or indirectly) in some construct C that is part
+ of the assertion expression but is not part of F.
+
+But this is slightly too strong; it probably disallows a shared global logging
+facility if used in multiple function calls used in the same assertion
+expression. Also, the "that is read" is a bit clunky; but J-P objected
+[correctly] to talking about the name of the variable.
+
+Note that too strong of a rule probably is irrelevant to Ada implementations
+(which are unlikely to enforce this), but might matter to tools trying to
+prove the absence of exceptions (which means proving the absence of bounded
+errors).
+
+We should try to polish this some more, and probably consider if the next
+paragraph needs improvement as well. **]
+
+
It is a bounded error in an assertion expression associated with a call of or
return from a callable entity C to alter the value of any variable that could
alter the value of any other such assertion expression of the callable entry C.
@@ -191,7 +214,7 @@
Pragma Assert is used to assert the truth of a Boolean expression at any point
within a sequence of declarations or statements. Pragma Assertion_Policy is used
to control whether such assertions are to be ignored by the implementation, checked
-at run-time, or handled in some implementation-defined manner.
+at run-time, or handled in some implementation-defined manner.
@dby
Pragma Assert is used to assert the truth of a boolean expression at a point
within a sequence of declarations or statements.
@@ -237,7 +260,7 @@
!corrigendum 11.4.2(25/2)
@dinsa
-Implementations may define their own assertion policies.
+Implementations may define their own assertion policies.
@dinst
If the result of a function call in an assertion is not needed to determine the
value of the assertion expression, an implementation is permitted to omit the
@@ -861,19 +884,20 @@
Sent: Friday, December 23, 2011 3:24 AM
...
-> (2) We could just add a large AARM note explaining what we meant,
-> probably with an example. This probably would be good enough for
-> everyone other that Robert, who apparently refuses to read the AARM.
+> (2) We could just add a large AARM note explaining what we meant,
+> probably with an example. This probably would be good enough for
+> everyone other that Robert, who apparently refuses to read the AARM.
> :-) I'm not sure how best to write that note, however.
I stuck in the following AARM note:
-The rule above is intended to apply to all of the assertion expressions that are evaluated
-at the start of call (and similarly for the assertion expressions that are evaluated
-during the return from a call), but not other assertions actually given in the body, nor
-between the expressions given at the start and end. Specifically, a side effect in a
-function called from a precondition expression that changes the result of a postcondition
-expression of the same subprogram does not trigger this rule.
+The rule above is intended to apply to all of the assertion expressions that are
+evaluated at the start of call (and similarly for the assertion expressions that
+are evaluated during the return from a call), but not other assertions actually
+given in the body, nor between the expressions given at the start and end.
+Specifically, a side effect in a function called from a precondition expression
+that changes the result of a postcondition expression of the same subprogram
+does not trigger this rule.
I hope that's enough. Tell me if you disagree.
@@ -882,8 +906,349 @@
P.S. Merry Christmas!!
P.P.S. The call "SE(X)" in my rewritten proposal was a total accident, "X"
-was the parameter name in Steve's (illegal) example from the meeting, and I named the
-function SE as short for Side Effect. I didn't realize what it looked like until now.
-Very Merry Christmas!! ;-)
+was the parameter name in Steve's (illegal) example from the meeting, and I
+named the function SE as short for Side Effect. I didn't realize what it looked
+like until now. Very Merry Christmas!! ;-)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, December 27, 2011 8:18 PM
+
+Another thought on the "bounded error" AI:
+
+Steve voted against this AI, because "because he thinks this notion of 'affects'
+is too imprecise" (as recorded in the minutes). That's a weird statement,
+because the final wording doesn't include the word "affects" at all -- the final
+wording is "could alter". Still, let's ignore that and look at his actual
+concern (which I admit I didn't do during the meeting; my excuse was that I was
+too busy taking notes [at least that sounds plausible :-)]).
+
+Our intent with this rule is that compilers would not try to enforce it (that
+is, try to detect the error). However, it certainly is true that a complier
+*could* try to enforce it. Moreover, other tools (such as a SPARK-like prover)
+surely need to know whether this rule is violated (they are unlikely to allow
+bounded errors to persist in programs that they check). So it should be possible
+to determine, with knowledge of the entire program, whether or not the rule is
+violated.
+
+I was thinking about adding an AARM TBH note to clarify. But then I realized I
+don't really know what the rule is. Specifically, Steve gave an example that is
+questionable. But I don't think we ever clearly decided whether or not his
+example was a bounded error (that is, does it trigger the new rule). That's not
+going to work.
+
+Steve gave the following example:
+
+ Incb(X) and X > 0
+
+where Incb increments its parameter. In this case, the side-effect only "could
+alter" the result of the expression if the value of X = 0. So is the rule
+triggered or not?
+
+The problem with this example is that it is illegal by 6.4.1(6.18/3); the
+parameter to Incb has to be "in out" if X is to be modified (since an integer is
+a by-copy type), and that triggers the "Taft" order-of-evaluation checks. Since
+the arguments to "and" can be evaluated in either order, the expression is
+illegal on its face (and the reason is in large part the fact that the
+side-effect "could alter" the result -- what a tangled web we weave!). So there
+is no point in talking about it.
+
+But it is easy enough to write a similar example that is legal; just make the
+entity global and hidden. So let's write a more complete example:
+
+ Glob : Natural := 0;
+
+ function Incb (P : in Natural) return Boolean is
+ begin
+ Glob := Glob + P;
+ return P > 0;
+ end Incb;
+
+ procedure Bar (Param : in out Natural)
+ with Pre => Incb(Param) and Glob > 0;
+
+In this case, the expression value will only be altered if Glob = 0 and Param /=
+0 when Bar is called AND the function is called after evaluating "Glob > 0" (the
+language allows evaluating these operands in either order).
+
+Now, the rule in question is:
+
+"It is a bounded error in an assertion expression to alter the value of any
+variable that could alter the value of the assertion expression."
+
+Does this expression qualify? There seem to be at least four possible answers:
+
+(1) This expression does qualify. The only requirement is that there exist some
+set of values where the value would be altered. This seems to be the intent
+expressed by wording ("can alter"). However, taken literally, it could only
+apply to an expression that has parts that can be evaluated in an arbitrary
+order. That's because the value of the expression cannot change (even in the
+face of a side-effect) if the order is specified. For instance, if we change
+"and" to "and then" in the above expression, the value is always going to be the
+same.
+
+(2) This expression qualifies IFF Glob = 0 and Param /= 0. That is, the bounded
+error only occurs when the values actually cause the value to be altered. In
+this case, the normative wording should say "alters" rather than "can alter".
+This would be a rule that would be simple to verify if it applies, but it also
+would be extremely narrow (and also subject to the "and then" issue).
+
+Neither of these seems to be what was really intended. I've been ignoring the
+last sentence in this rule because it does nothing but describe the normal
+execution and a possible consequence. That consequence talks about the
+expression being immediately reevaluated; but note that that consequence can
+happen even for expressions that do not trigger either reading of the rule (that
+is, expressions using "and then" rather than "and").
+
+The problem with the rule as written is that it only talks about the altering
+the value of {the current evaluation of} the assertion expression. If we want to
+include some imaginary other evaluation of the expression, we had better say
+that explicitly. Indeed, Tucker had suggested that something about "immediate
+reevaluation" be part of the normative wording, that didn't happen for some
+reason. Imagining that it is part of the normative wording gives us two more
+answers:
+
+(3) This expression does qualify, and would even if "and" is replaced by "and
+then". The only requirement is that there exist some set of values where the
+value of a subsequent immediate evaluation would be altered. The normative
+wording should be what Tucker suggested during the meeting: "...that could alter
+the value of the expression on a immediate subsequent evaluation". Or perhaps:
+"...that could alter the value of the assertion expression, immediately or on a
+immediate subsequent evaluation". (I can imagine an expression where the value
+changes because of a side-effect, but an immediate re-evaluation would get the
+original answer - likely because the result type of Boolean has only two
+possible answers. Surely that should be covered.) This is a broad rule, covering
+the majority of possible side-effects (only the most benign would be allowed; a
+straight memo function surely would not be a bounded error, nor would saving
+values for logging, but I find it hard to imagine what else would not).
+
+(4) Same as above, but using "alters" rather than "can alter". That is, the
+bounded error only occurs if the value is in fact affected (directly or on an
+immediate subsequent evaluation). "and" or "and then" usually would not make a
+difference. This is a narrower rule, and it would make almost no sense for a
+compiler to try to detect it (which I thought was a goal) - it would have to do
+so at runtime (or is that run-time or run time ;-).
+
+I'm pretty sure we meant either (3) or (4), but it is not clear to me which is
+intended (nor do my meeting notes clarify anything). Note that either (3) or (4)
+requires changing the approved wording -- I agree with Steve that the current
+wording is too vague. And I don't think it reflects our intent (neither (1) nor
+(2) being our intent -- but I can't get that out of reading the rule).
+
+Beyond that, it's not clear whether we need a wording change for the second rule
+(the one about the multiple assertion expressions evaluated on entry or exit
+from a subprogram). It suffers from a similar problem, but there it is less
+likely that there would be a difference from an "immediate reevaluation", and
+far more likely that there would be a change in some other expression, so maybe
+fixing the first one is sufficient.
+
+Thoughts??
****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, December 27, 2011 9:07 PM
+
+Perhaps we should make the wording as similar as possible to the new rules
+restricting side-effect due to function [IN] OUT parameters, but make it fully
+general, rather than limiting it to statically recognizable situations.
+
+Our statically checkable rule is:
+
+If a construct C has two or more direct constituents that are names or
+expressions whose evaluation may occur in an arbitrary order, at least one of
+which contains a function call with an in out or out parameter, then the
+construct is legal only if:
+
+ For each name N that is passed as a parameter of mode in out or out to some inner
+ function call C2 (not including the construct C itself), there is no other name anywhere
+ within a direct constituent of the construct C other than the one containing C2, that is
+ known to refer to the same object.
+
+-----
+
+We could perhaps use this as a model, but use a much simpler,
+but non-statically-checkable rule. E.g.:
+
+ It is a bounded error if within an assertion expression (directly
+ or indirectly) there is a construct that updates an object whose
+ value possibly contributes to the value of the expression (directly or
+ indirectly).
+
+I'll admit it isn't very precise, but perhaps it is adequate.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, December 27, 2011 9:24 PM
+
+Isn't this too strong? It seems to ban memo functions because the memo value
+"possibly contributes to the value of the expression" (if it is used rather than
+recalculating the function value), and it is "updated" by the call to the memo
+function. The wording here doesn't say anything about the value that possibly
+contributes being different in some sense, and that seems necessary to allow
+memo functions (which clearly have a side-effect, but that effect does not
+change the result of the function).
+
+It does allow functions that log their calls (as that does not contribute to the
+result), but I don't think that is enough to satisfy everyone.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, December 27, 2011 9:58 PM
+
+How about something like:
+
+ It is a bounded error if within an assertion expression (directly or
+ indirectly) there is a construct that changes the value of an object whose
+ original value possibly contributes to the value of the expression (directly
+ or indirectly).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, December 27, 2011 10:44 PM
+
+Much better. The remaining question is what "possibly contributes" means. I
+think the intent is fairly clear (the value appears directly or indirectly
+somewhere else in the expression; it doesn't matter if that part is executed or
+not). [In the case of the rule having to do with multiple expressions, it
+appears in one of the other expressions; even easier.]
+
+But I can imagine Steve or Adam arguing about something like:
+
+ Pre => SE and then False and then Glob > 0
+
+where SE modifies Glob. One certainly can argue that Glob does not contribute in
+this expression. Of course, then one modifies False to a named constant and then
+to a static expression known to be False and then to a non-static expression
+that the compiler can prove to be False, and we've gone down the slippery slope
+to Hades.
+
+Maybe we should just talk about the variable directly. That's what the wording
+you were trying to copy did. How about:
+
+ It is a bounded error if within an assertion expression (directly or
+ indirectly) there is a construct C that alters the value of a variable whose
+ original value could be used (directly or indirectly) in some other
+ construct C2 that is part of the assertion expression but is not part of C.
+
+["could be used" doesn't sound much better to me]
+
+or maybe:
+
+ It is a bounded error if within an assertion expression (directly or
+ indirectly) there is a construct C1 that alters the value of a variable
+ whose original value possibly contributes (directly or indirectly) to the
+ value of some other construct C2 that is part of the assertion expression
+ but is not part of C1.
+
+[there's that phrase again. Still doesn't work.]
+
+or maybe even (copying even more of the other rule):
+
+ It is a bounded error if within an assertion expression (directly or
+ indirectly) there is a construct C1 that alters the value of a variable
+ whose name appears (directly or indirectly) in some other construct C2 that
+ is part of the assertion expression but is not part of C1.
+
+Humm. This latter version seems to reintroduce the memo-function problem,
+because even local variables are included:
+ Save_Memo1_Result : Natural;
+ Same_Memo1_Param : Natural;
+ function Memo1 (P : Natural) return Natural is
+ Temp : Natural;
+ begin
+ if Save_Memo1_Param = P then
+ return Save_Memo1_Result;
+ else
+ Temp := ...;
+ Save_Memo1_Param := P;
+ Save_Memo1_Result := Temp;
+ return Temp;
+ end if;
+ end Memo1;
+Here Temp would trigger the bounded error, even though it is obviously not
+relevant.
+
+Is it possible for a variable to be altered anywhere other than in a function
+(and still be part of an expression)? If not, perhaps we can consider the entire
+function as "the construct" and avoid this problem.
+
+ It is a bounded error if within an assertion expression (directly or
+ indirectly) there is a function call F that alters the value of a variable
+ whose name appears (directly or indirectly) in some construct C that is part
+ of the assertion expression but is not part of F.
+
+Now we're allowing local variables (because they can't be part of some other
+construct not in the function), and memo variables as well (because they should
+only appear in that one function).
+
+Still, I'm not that confortable with this. It seems to disallow a shared global
+logging facility - perhaps that isn't important enough to worry about.
+
+It's amazing that we know pretty much what we want the rule to be, but we can't
+seem to write it unambiguously enough to communicate that. Hope the above will
+inspire another try...
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Wednesday, December 28, 2011 2:31 AM
+
+> It is a bounded error if within an assertion expression (directly
+> or indirectly) there is a function call F that alters the value
+> of a variable whose
+> name appears (directly or indirectly) in some construct C that is
+> part of the assertion expression but is not part of F.
+
+"whose name appears" can't be right, or I'll call the renaming police...
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Wednesday, December 28, 2011 6:34 AM
+
+> Isn't this too strong? It seems to ban memo functions because the memo
+> value "possibly contributes to the value of the expression" (if it is
+> used rather than recalculating the function value), and it is
+> "updated" by the call to the memo function. The wording here doesn't
+> say anything about the value that possibly contributes being different
+> in some sense, and that seems necessary to allow memo functions (which
+> clearly have a side-effect, but that effect does not change the result of the function).
+>
+> It does allow functions that log their calls (as that does not
+> contribute to the result), but I don't think that is enough to satisfy
+> everyone.
+
+Well I wouldn't worry too much, if the rule ends up being over strenuous, no
+reasonable implementation will behave badly.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, December 28, 2011 12:04 AM
+
+I originally thought that as well, because no implementation is going to try too
+hard to enforce these rules. (Our purpose in adding them is more as a stern
+warning to people writing Ada code and to allow aggressive optimizations here.)
+
+But the situation is different for tools. If you have a tool that tries to prove
+exception absence (SPARK does this, and I would hope that there are or will be
+more general tools of this type), one prong of that is to prove the absence of
+any bounded errors. (As the occurrence of a bounded error can cause a
+Program_Error to be raised.) Such tools (unless they are strongly tied to a
+single implementation) will have to assume the worst (that is, that some
+implementation implements the rules literally and detects all such bounded
+errors). [Even in the case where no known implementation detects the bounded
+error, some future version could.] In which case, a rule which is too strenuous
+can be harmful (even if no implementation actually implements that part of the
+rule).
+
+So I would much rather have the rule be "just right", and if we have to err, it
+ought to be on the side of being a bit looser than ideal.
+
+****************************************************************
+
Questions? Ask the ACAA Technical Agent