* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-11 21:36 ` Jesper Quorning
@ 2019-02-11 22:31 ` Anh Vo
2019-02-11 23:41 ` Randy Brukardt
2019-02-12 7:28 ` Mark Lorenzen
2 siblings, 0 replies; 19+ messages in thread
From: Anh Vo @ 2019-02-11 22:31 UTC (permalink / raw)
On Monday, February 11, 2019 at 1:36:56 PM UTC-8, Jesper Quorning wrote:
> søndag den 10. februar 2019 kl. 19.08.05 UTC+1 skrev Simon Wright:
> > Jesper Quorning <jesper.quorning@gmail.com> writes:
> >
> > Don't you already get a warning if a CE is going to be raised at
> > runtime?
>
> I would like a note from GCC when a there is an implicit (hidden) exception rise like array bunds checking.
> It would be a simple way of inspecting your quality of code. For instance if there is array bunds checks in a loop I may like to rewrite/design a part of the program.
GNAT gives warning about exception (mostly CE) to be raised for codes violating Ada run time language rules. These rules spread through out the Ada Language Reference Manual. Therefore, GNAT document may not reference all cases.
Anh Vo
^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-11 21:36 ` Jesper Quorning
2019-02-11 22:31 ` Anh Vo
@ 2019-02-11 23:41 ` Randy Brukardt
2019-02-12 7:05 ` Jesper Quorning
2019-02-12 8:19 ` Dmitry A. Kazakov
2019-02-12 7:28 ` Mark Lorenzen
2 siblings, 2 replies; 19+ messages in thread
From: Randy Brukardt @ 2019-02-11 23:41 UTC (permalink / raw)
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2576 bytes --]
"Jesper Quorning" <jesper.quorning@gmail.com> wrote in message
news:17375128-e016-4366-91ff-cd68f74689b3@googlegroups.com...
>søndag den 10. februar 2019 kl. 19.08.05 UTC+1 skrev Simon Wright:
>> Jesper Quorning <jesper.quorning@gmail.com> writes:
>>
>> Don't you already get a warning if a CE is going to be raised at
>> runtime?
>
>I would like a note from GCC when a there is an implicit (hidden) exception
>rise
>like array bunds checking. It would be a simple way of inspecting your
>quality of
>code. For instance if there is array bunds checks in a loop I may like to
>rewrite/design a part of the program.
This sounds like a great idea, in that many people (including me) have had
this one over the years. (The first time I remember hearing about it was at
the very first AdaTec (which later become SigAda) meeting that we went to -
circa 1984).
Anyway, this depends on what you mean by such a switch. A switch that simply
reported every place where the language semantics requires a
language-defined check wouldn't be useful, because the language requires a
check almost everywhere (for every subtype conversion, for instance,
including those that don't actually do anything).
A switch that only reports places that the compiler inserts checks is quite
expensive in practice to build, as it has to be associated with expensive
check elimination code to be useful. That can be especially difficult if the
check elimination code happens well after the code that handles warnings (as
in Janus/Ada).
I've been playing with such a switch in Janus/Ada lately (in a *very*
limited set of checks), and it just tends to prove that one's compiler isn't
as good at eliminating checks as one previously thought. :-) There are lots
of cases of checks being left that are "obviously" not needed, and all of
those provide noise in using such a switch for quality improvement. Having
such an obvious look is bad if only because it encourages spending effort on
check elimination (because of visibility) over other possible places to
spend effort. (This switch will be available in the current version of
Janus/Ada as soon as I get it released -- which will have to wait until my
Ada Standard work is done -- but I'm not planning on publicizing it as it
has too many false positives to be useful to most at this time.)
In the case of AdaCore, they have other tools for finding quality problems
in Ada code (like CodePeer), and they may very well want to put new effort
into those rather than into the compiler.
Randy.
^ permalink raw reply [flat|nested] 19+ messages in thread* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-11 23:41 ` Randy Brukardt
@ 2019-02-12 7:05 ` Jesper Quorning
2019-02-12 23:08 ` Randy Brukardt
2019-02-16 4:30 ` Brad Moore
2019-02-12 8:19 ` Dmitry A. Kazakov
1 sibling, 2 replies; 19+ messages in thread
From: Jesper Quorning @ 2019-02-12 7:05 UTC (permalink / raw)
tirsdag den 12. februar 2019 kl. 00.41.54 UTC+1 skrev Randy Brukardt:
> This sounds like a great idea, in that many people (including me) have had
> this one over the years. (The first time I remember hearing about it was at
> the very first AdaTec (which later become SigAda) meeting that we went to -
> circa 1984).
Ideas takes time to become reality.
> Anyway, this depends on what you mean by such a switch. A switch that simply
> reported every place where the language semantics requires a
> language-defined check wouldn't be useful, because the language requires a
> check almost everywhere (for every subtype conversion, for instance,
> including those that don't actually do anything).
1: subtype Index_Type is range 1 .. Integer'Last;
2: My_Array : array (Index_Type) of Boolean;
3: ...
4: My_Index : Integer := Get_Intege; -- Get integrer frome somewhere
5: ...
6: My_Array (My_Index) := True;
Should yield something like:
program.adb:6: (note) CONSTRAINT_ERRORE may be raise on array lower bound check
> A switch that only reports places that the compiler inserts checks is quite
> expensive in practice to build, as it has to be associated with expensive
> check elimination code to be useful. That can be especially difficult if the
> check elimination code happens well after the code that handles warnings (as
> in Janus/Ada).
It is just at note to the user of the compiler. Low optimisation mode gives more notes than high optimisation modes.
> I've been playing with such a switch in Janus/Ada lately (in a *very*
> limited set of checks), and it just tends to prove that one's compiler isn't
> as good at eliminating checks as one previously thought. :-) There are lots
> of cases of checks being left that are "obviously" not needed, and all of
> those provide noise in using such a switch for quality improvement. Having
> such an obvious look is bad if only because it encourages spending effort on
> check elimination (because of visibility) over other possible places to
> spend effort. (This switch will be available in the current version of
> Janus/Ada as soon as I get it released -- which will have to wait until my
> Ada Standard work is done -- but I'm not planning on publicizing it as it
> has too many false positives to be useful to most at this time.)
That this switch could lead to impoved compilers; I had not thougt of.
> In the case of AdaCore, they have other tools for finding quality problems
> in Ada code (like CodePeer), and they may very well want to put new effort
> into those rather than into the compiler.
You will reduce the need for other tools as the promary tool, GCC just reports as notes, what it is doing anyway.
Jesper.
^ permalink raw reply [flat|nested] 19+ messages in thread* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-12 7:05 ` Jesper Quorning
@ 2019-02-12 23:08 ` Randy Brukardt
2019-02-16 4:30 ` Brad Moore
1 sibling, 0 replies; 19+ messages in thread
From: Randy Brukardt @ 2019-02-12 23:08 UTC (permalink / raw)
"Jesper Quorning" <jesper.quorning@gmail.com> wrote in message
news:989ea6c7-b432-4214-beec-c0a50b76932c@googlegroups.com...
...
>> In the case of AdaCore, they have other tools for finding quality
>> problems
>> in Ada code (like CodePeer), and they may very well want to put new
>> effort
>> into those rather than into the compiler.
>
> You will reduce the need for other tools as the promary tool, GCC just
> reports
> as notes, what it is doing anyway.
That's the reason for doing it in Janus/Ada. I don't see a reasonable place
to put quality checks into normal workflow other than the compiler. In a
separate tool, it is too late (unless of course you run those tools
everytime you compile). The sort of problems found by quality warnings are
easily found by testing; the value is to save the time debugging "obvious"
errors. See the RRS blog entry on quality warnings:
http://www.rrsoftware.com/html/blog/quality.html for more on this topic.
Anyway, my point in mentioning that AdaCore has other tools for that purpose
is that AdaCore may have business reasons for not wanting to put more stuff
into the compiler. If you're giving away the compiler, then it might make
business sense to keep some of the capabilities in stuff that you are
charging for. (Let me say that I have no knowledge whatsoever on this topic,
it is just speculation on my part.)
I see from other messages that there is way to get the information you're
asking for, even if it isn't optimal. So it's also likely that AdaCore will
consider the need handled.
Randy.
^ permalink raw reply [flat|nested] 19+ messages in thread* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-12 7:05 ` Jesper Quorning
2019-02-12 23:08 ` Randy Brukardt
@ 2019-02-16 4:30 ` Brad Moore
2019-02-16 16:15 ` Jesper Quorning
1 sibling, 1 reply; 19+ messages in thread
From: Brad Moore @ 2019-02-16 4:30 UTC (permalink / raw)
One option would be to write the code you want checked in SPARK.
For example, from your example above, one could write....
package P with SPARK_Mode is
subtype Index_Type is Integer range 1 .. 100;
My_Array : array (Index_Type) of Boolean;
procedure Foo (Index : Integer);
end P;
package body P with SPARK_Mode is
procedure Foo (Index : Integer) is
begin
My_Array (Index) := True; -- SPARK detects exception may be raised here
end Foo;
end P;
The code compiles in Ada, but the SPARK prover complains....
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
p.adb:6:17: medium: array index check might fail (e.g. when Index = 0)
Brad
^ permalink raw reply [flat|nested] 19+ messages in thread* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-16 4:30 ` Brad Moore
@ 2019-02-16 16:15 ` Jesper Quorning
0 siblings, 0 replies; 19+ messages in thread
From: Jesper Quorning @ 2019-02-16 16:15 UTC (permalink / raw)
On Saturday, February 16, 2019 at 5:30:16 AM UTC+1, Brad Moore wrote:
> One option would be to write the code you want checked in SPARK.
I am not against exceptions as such. A note would be an easy way to inspect the quality for my writings. And easy to implement for the compiler writer (as far as I can see).
Jesper.
^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-11 23:41 ` Randy Brukardt
2019-02-12 7:05 ` Jesper Quorning
@ 2019-02-12 8:19 ` Dmitry A. Kazakov
2019-02-12 8:35 ` Jesper Quorning
1 sibling, 1 reply; 19+ messages in thread
From: Dmitry A. Kazakov @ 2019-02-12 8:19 UTC (permalink / raw)
On 2019-02-12 00:41, Randy Brukardt wrote:
> This sounds like a great idea, in that many people (including me) have had
> this one over the years.
What about exception contracts? That would resolve this and many other
issues. Bet there is no Constraint_Error (and conversely, there must be
one) and the compiler will have to check that.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-12 8:19 ` Dmitry A. Kazakov
@ 2019-02-12 8:35 ` Jesper Quorning
2019-02-12 9:20 ` Dmitry A. Kazakov
0 siblings, 1 reply; 19+ messages in thread
From: Jesper Quorning @ 2019-02-12 8:35 UTC (permalink / raw)
On Tuesday, February 12, 2019 at 9:19:11 AM UTC+1, Dmitry A. Kazakov wrote:
> What about exception contracts? That would resolve this and many other
> issues. Bet there is no Constraint_Error (and conversely, there must be
> one) and the compiler will have to check that.
This is for the experience engineer. Notes are for the novice.
Jesper.
^ permalink raw reply [flat|nested] 19+ messages in thread* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-12 8:35 ` Jesper Quorning
@ 2019-02-12 9:20 ` Dmitry A. Kazakov
2019-02-12 12:46 ` Jesper Quorning
0 siblings, 1 reply; 19+ messages in thread
From: Dmitry A. Kazakov @ 2019-02-12 9:20 UTC (permalink / raw)
On 2019-02-12 09:35, Jesper Quorning wrote:
> On Tuesday, February 12, 2019 at 9:19:11 AM UTC+1, Dmitry A. Kazakov wrote:
>
>> What about exception contracts? That would resolve this and many other
>> issues. Bet there is no Constraint_Error (and conversely, there must be
>> one) and the compiler will have to check that.
>
> This is for the experience engineer. Notes are for the novice.
Exactly the opposite. An experienced programmer could go without proper
contracts and manifested typing. It requires a lot of knowledge and
intuition to understand what is going on behind the scenes. Novices
cannot do that.
--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-12 9:20 ` Dmitry A. Kazakov
@ 2019-02-12 12:46 ` Jesper Quorning
0 siblings, 0 replies; 19+ messages in thread
From: Jesper Quorning @ 2019-02-12 12:46 UTC (permalink / raw)
On Tuesday, February 12, 2019 at 10:20:24 AM UTC+1, Dmitry A. Kazakov wrote:
> Exactly the opposite. An experienced programmer could go without proper
> contracts and manifested typing. It requires a lot of knowledge and
> intuition to understand what is going on behind the scenes. Novices
> cannot do that.
I would say it depends on how to learn Ada. Top down or bottom up. I did bottom up.
Jesper.
^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-11 21:36 ` Jesper Quorning
2019-02-11 22:31 ` Anh Vo
2019-02-11 23:41 ` Randy Brukardt
@ 2019-02-12 7:28 ` Mark Lorenzen
2019-02-12 8:34 ` Jesper Quorning
` (2 more replies)
2 siblings, 3 replies; 19+ messages in thread
From: Mark Lorenzen @ 2019-02-12 7:28 UTC (permalink / raw)
On Monday, February 11, 2019 at 10:36:56 PM UTC+1, Jesper Quorning wrote:
> I would like a note from GCC when a there is an implicit (hidden) exception rise like array bunds checking.
> It would be a simple way of inspecting your quality of code. For instance if there is array bunds checks in a loop I may like to rewrite/design a part of the program.
Do you have som example code at hand? If so, please try and compile it with pragma Restrictions (No_Exception_Propagation) is in effect and switch -gnatw.x (yes including the dot and x). I have used this to find all places in the code, where a run-time error could be raised. It is not an optimal solution due to the pragma and possible local exception handlers, but could give an idea of what GNAT is already capable of.
Mark L
^ permalink raw reply [flat|nested] 19+ messages in thread* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-12 7:28 ` Mark Lorenzen
@ 2019-02-12 8:34 ` Jesper Quorning
2019-02-12 22:31 ` Fedja Beader
2019-02-13 10:42 ` Simon Wright
2 siblings, 0 replies; 19+ messages in thread
From: Jesper Quorning @ 2019-02-12 8:34 UTC (permalink / raw)
On Tuesday, February 12, 2019 at 8:28:11 AM UTC+1, Mark Lorenzen wrote:
> Do you have som example code at hand? If so, please try and compile it with pragma Restrictions (No_Exception_Propagation) is in effect and switch -gnatw.x (yes including the dot and x). I have used this to find all places in the code, where a run-time error could be raised. It is not an optimal solution due to the pragma and possible local exception handlers, but could give an idea of what GNAT is already capable of.
I do not hate exceptions. I would like to improve the quality of my programming by getting notes where the compiler may rise an exception.
An now I also like to inspect the quality of the compiler. The vender may choose to hide the implicit expections caused by sub-optimal compiler quality.
Jesper.
^ permalink raw reply [flat|nested] 19+ messages in thread* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-12 7:28 ` Mark Lorenzen
2019-02-12 8:34 ` Jesper Quorning
@ 2019-02-12 22:31 ` Fedja Beader
2019-02-13 10:42 ` Simon Wright
2 siblings, 0 replies; 19+ messages in thread
From: Fedja Beader @ 2019-02-12 22:31 UTC (permalink / raw)
On Mon, 11 Feb 2019 23:28:09 -0800 (PST)
Mark Lorenzen <mark.lorenzen@gmail.com> wrote:
> pragma Restrictions (No_Exception_Propagation)
This pragma is default in embedded ZFP context and causes the
programmer to be overflowed with "... may call last_chance_handler"
warnings.
I have an Integer Put procedure where every other line results
in this warning being emitted. This happens even though I changed the
source code such that no call to last_chance_handler is present in the
resulting binary. This warning shouldn't be disabled entirely, as it is
very useful.
^ permalink raw reply [flat|nested] 19+ messages in thread
* Re: GNAT proposal: note on implicit exceptions insertion
2019-02-12 7:28 ` Mark Lorenzen
2019-02-12 8:34 ` Jesper Quorning
2019-02-12 22:31 ` Fedja Beader
@ 2019-02-13 10:42 ` Simon Wright
2 siblings, 0 replies; 19+ messages in thread
From: Simon Wright @ 2019-02-13 10:42 UTC (permalink / raw)
-gnatw.x (turn on warnings for non-local exception) is included in -gnatwa
It's turned off by -gnatw.X
^ permalink raw reply [flat|nested] 19+ messages in thread