From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: fac41,2c6139ce13be9980 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,3d3f20d31be1c33a X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,2c6139ce13be9980 X-Google-Attributes: gidf43e6,public From: bobduff@world.std.com (Robert A Duff) Subject: Re: Safety-critical development in Ada and Eiffel Date: 1997/07/19 Message-ID: X-Deja-AN: 257701153 References: Organization: The World Public Access UNIX, Brookline, MA Newsgroups: comp.software-eng,comp.lang.ada,comp.lang.eiffel Date: 1997-07-19T00:00:00+00:00 List-Id: In article , Jon S Anthony wrote: >In article bobduff@world.std.com (Robert A Duff) writes: > >> >> In article , >> >> jsa@alexandria.organon.com says... >> >> >> >> > type Require is boolean range True..True; >> >> >... >> >> > >> >> > Assert : Require := Complex_Precondition(X); >> >> This isn't quite right, because RM-11.6 allows the check to be >> eliminated. > >Bob, could you clarify this? Suppose Complex_Precondition(X) returns False. Normally, you would expect a range check on the assignment, and that would raise C_E. However, 11.6(5) says the implementation does *not* have to raise C_E, since *in the absence of raising it*, the result has no external effect. I'm presuming there are no further references to Assert. If Complex_Precondition has externally-visible side-effects, then they must happen. If it doesn't (and the compiler can prove it), then the entire call can also be eliminated. Another example: X: Integer := 999; Y: Integer range 1..10 := X; If there are no further references to Y (or there are, but they in turn have no external effect), C_E need not be raised. This is true whether or not there is a handler for C_E (or others) somewhere (which of course the compiler doesn't know, since it might be further up the call stack -- that is, the permission would be useless if the presence of a handler had something to do with it). Of course, in order to take advantage of the permission, the compiler has to prove the absence of external effect. If Y is a local variable, that's easy. I've heard some compiler writers say they would never consider taking advantage of 11.6, since it would confuse programmers. I've heard other compiler writers say that without 11.6, performance would stink. I also believe that compilers aren't super clever about taking advantage of 11.6 -- I believe that, because I've seen many ACVC tests that would fail if the compiler was smarter. Such ACVC tests are wrong, of course, but they only get fixed if compiler writers complain. (You can imagine why such tests exist -- they are checking that C_E is raised in all the zillion cases it should be, and it's easy to write a test where the *only* external effect of the C_E is in the exception handler. This isn't the kind of code that occurs a lot in *real* programs.) The basic idea is that you shouldn't write code that depends on getting C_E for a failed run-time check (which the "Assert: Require..." example does). You can, however, depend on the fact that if a given value is checked, you can't end up using a junk value in an externally visible way. E.g., in the above example, if we add a "Put(Y)", it cannot print out "999" -- it must raise C_E before that. In the "Assert: Require" example, if you print out the value of Assert, then the check will not be eliminated (but that kind of defeats the purpose of that little trick). Note that the permissions apply only to predefined checks. If you write an explicit "raise Constraint_Error;" or "raise My_Favorite_Error;", then the permission does not apply. >... I just had a look at 11.6 and I'm not >clear on how this works. For example given the above it would clearly >be the case that you would also have: ^^^^^ could? > >... >exception > when E : Constraint_Error => > Do_Something(....)... You *could* have such a handler, but normally you wouldn't -- you would just let the program crash, and use debugging tools (and/or your brain) to figure out why. After all, you wrote the assertion because you thought it was true. >in order to catch and do something in case the CE is raised. How >could the implementation know that this would not "have some effect on >the external interactions of the program"???? I think you're missing the phrase "in the absence of raising it" in the RM. >I know what you mean here, but a more accurate description would be >that an optimizer can change the behavior as long as that behavior is >not part of the defined semantics. Yeah, maybe. My point is just that the semantics (defined in the RM) defines a *set* of possible behaviors, and the compiler's job is to make sure that the actual behavior belongs to that set. If you recompile with optimization on, or if you simply run the same binary again, you might get a different behavior. >>... End users care about the *behavior*. > >Actually, if they really did care about behavior that was _not_ part >of the defined semantics, wouldn't that really be a case of an >"erroneous" or possibly "bounded error" program???? Not sure what you mean here. I'm talking about "end users" -- they don't normally care one whit what the programming language semantics are, nor even what programming language was used -- they just want the program to behave properly. And they often want the program to be written in such a way that it always gets the same answer for the same input. - Bob