GNAT proposal: note on implicit exceptions insertion

GNAT proposal: note on implicit exceptions insertion

[Jesper Quorning]

Hi Group

What is Your opinion on a switch for gnatmake that notes the programmer when a implicit excepton is inserted. I think it should work somewhat like -gnaty just making a note.

program.adb:99: (note) Implicit Constraint_Error infered


/Jesper

Re: GNAT proposal: note on implicit exceptions insertion

[Simon Wright]

Jesper Quorning <jesper.quorning@gmail.com> writes:

> What is Your opinion on a switch for gnatmake that notes the
> programmer when a implicit excepton is inserted. I think it should
> work somewhat like -gnaty just making a note.
>
> program.adb:99: (note) Implicit Constraint_Error infered

Don't you already get a warning if a CE is going to be raised at
runtime?

Re: GNAT proposal: note on implicit exceptions insertion

[Mark Lorenzen]

First of all the -gnaty switch is not a gnatmake switch but a gcc switch. Apart from that, I don't understand your proposal. What is an "implicit exception"?

Note that gnatmake is deprecated. The GNAT builder is now gprbuild.

Mark L

Re: GNAT proposal: note on implicit exceptions insertion

[Simon Wright]

Mark Lorenzen <mark.lorenzen@gmail.com> writes:

> Note that gnatmake is deprecated. The GNAT builder is now gprbuild.

Except that gnatmake is part of GCC, gprbuild isn't.

In GCC builds, gnatbind, gnatmake and gnatlink are built using
Makefiles, all the other tools are built using gnatmake.

gprbuild has the slight disadvantage (for someone who checks out quite a
lot of other people's code) that it needs a project file, and will only
use the default if there are no other project files in sight: and, if
there's more than one, you have to specify which one. gnatmake only uses
a project file if you tell it to.

Re: GNAT proposal: note on implicit exceptions insertion

[Jesper Quorning]

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.

Re: GNAT proposal: note on implicit exceptions insertion

[Anh Vo]

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

Re: GNAT proposal: note on implicit exceptions insertion

[Randy Brukardt]

[-- 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.

Re: GNAT proposal: note on implicit exceptions insertion

[Jesper Quorning]

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.

Re: GNAT proposal: note on implicit exceptions insertion

[Mark Lorenzen]

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

Re: GNAT proposal: note on implicit exceptions insertion

[Dmitry A. Kazakov]

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

Re: GNAT proposal: note on implicit exceptions insertion

[Jesper Quorning]

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.

Re: GNAT proposal: note on implicit exceptions insertion

[Jesper Quorning]

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.

Re: GNAT proposal: note on implicit exceptions insertion

[Dmitry A. Kazakov]

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

Re: GNAT proposal: note on implicit exceptions insertion

[Jesper Quorning]

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.

Re: GNAT proposal: note on implicit exceptions insertion

[Fedja Beader]

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.

Re: GNAT proposal: note on implicit exceptions insertion

[Randy Brukardt]

"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.

Re: GNAT proposal: note on implicit exceptions insertion

[Simon Wright]

-gnatw.x (turn on warnings for non-local exception) is included in -gnatwa
It's turned off by -gnatw.X

Re: GNAT proposal: note on implicit exceptions insertion

[Brad Moore]

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

Re: GNAT proposal: note on implicit exceptions insertion

[Jesper Quorning]

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.