Not null specifiable on an array type

[kevlar700]

Currently you can do

type Example_Array_Data is array (Positive range <>) of Integer;
type Example_Array (Length: Positive) is record
   Data : Example_Array_Data (1 .. Length);
end record;

Perhaps it is not worth the effort but it would be nice to be able to specify an array like so

type Example_Array is array (Positive range <>) of Integer not null;

The idea is that you could then be certain that a null check is not required after a function returns such a type?

[Richard-Wai]

If I understand correctly, I think you are referring to specifically the behavior of unconstrained array objects that have bounds with a "null range". I don't want to be too pedantic, but I think what you mean by "null check" is a regular contraint check, which would only apply if you actually tried to index into the array, tried to assign X'Last to a Positive variable, or tried to slide the null bounded array. Unless you do one of those things, there will never be a check that can fail with a null-bounded array. I cannot see a case where returning such an array would cause a check to fail unless you are sliding, in which case it is not necessarily specific to a null-bounded array.

The notion of null ranges are pretty fundamental to Ada, but the idea of a contract disallowing null ranges on an unconstrained array type seems potentially interesting. I'm not entirely convinced on its usefulness given that the concept of null ranges is always been part of Ada, and so iteration handles those conditions effortlessly. That being said, I think it might be better to put the "not null" near the index_subtype_defintion part of an unconstrained_array_definition.

Ergo: type Example_Array is array (Positive range <> not null) of Integer; or type Example_Array is array (Positive not null range <>) of Integer;

[joshua-c-fletcher]

Wouldn't this be the same as an aspect that specifies: type Example_Array is array (Positive range <>) or Integer with Dynamic_Predicate => Example_Array'First <= Example_Array'Last;

or

type Example_Array is array (Positive range <>) or Integer with Dynamic_Predicate => Example_Array'Length > 0;

[Richard-Wai]

@joshua-c-fletcher

I think the idea here is that you'd have a regular Ada constraint check added, whereas Dynamic_Predicate checking is part of the assertion framework, and is controlled by the Assertion_Polcicy, which may or my not be "Ignore" by default (implementation defined). It is also easier for the compiler to check the "null range" exclusion at compile-time where the opportunity arises.

However you are correct that this is something that can be checked through other means, and generally I think this is more evidence against the need for a new check, from my perspective. However I appreciate the general usefulness of being able to specify that a given object of an array type can never be empty. I worry that it won't be that simple in practice however. Array slicing in Ada is useful and common, and having null arrays seem to be an important part of that capability.

Edit: My comment originally read "Dynamic_Predicate checking is part of the assertion framework, and is off by default.". This is not strictly correct. The RM states that the Assertion_Policy, which controls if a Dynamic_Predicate is checked at run-time, if not defined, has a default that is "implementation defined". In the case of GNAT, the default is "Ignore", but that is not a property of the language, as my original wording would suggest.

[Jeff-Cousins]

Assuming I've understood the question, that (Dynamic_Predicate) is the route I'd take.JeffOn 27 Sept 2023 16:43, joshua-c-fletcher @.***> wrote: Wouldn't this be the same as an aspect that specifies: type Example_Array is array (Positive range <>) or Integer with Dynamic_Predicate => Example_Array'First <= Example_Array'Last; or type Example_Array is array (Positive range <>) or Integer with Dynamic_Predicate => Example_Array'Length > 0;

—Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you are subscribed to this thread.Message ID: @.***>

[kevlar700]

but I think what you mean by "null check" is a regular contraint check, which would only apply if you actually tried to index into the array,

hmm, perhaps this should have been part of this other issue.

https://github.com/Ada-Rapporteur-Group/User-Community-Input/issues/67

I use a light runtime where exception propagation is unsupported. Therefore I usually check a status as a null array access may end up causing the microchip to be restarted losing all memory (last chance handler) and in most instances I would prefer to drop that functionality than restart.

I have it on good authority from @SimonJWright that adding exception propagation to one never mind every microchip would unfortunately be time consuming.

Array slicing in Ada is useful and common, and having null arrays seem to be an important part of that capability.

The status may not be needed at all in some instances, if the function cannot return a null array. I find it offers nice readability to know that it cannot be empty too.

It is certainly true that null arrays can be useful at times.

[simonjwright]

I have it on good authority from @simonjwright that adding exception propagation to one never mind every microchip would unfortunately be time consuming.

I think I was quoting the late Robert Dewar’s remarks, "exceptions are a huge pain in the neck to implement, any language implementer would be happy to boot them out", so any authority that there might be is inherited.

A "light" runtime by definition has to leave a lot of Ada out; if you want tasking/exceptions etc you’ll need to choose a bigger microchip.

[kevlar700]

I think I was quoting the late Robert Dewar’s remarks, "exceptions are a huge pain in the neck to implement, any language implementer would be happy to boot them out", so any authority that there might be is inherited.

You mentioned something like they required a secondary stack and that it got quite hairy when you were getting it working for the runtimes that you had worked on.

A "light" runtime by definition has to leave a lot of Ada out; if you want tasking/exceptions etc you’ll need to choose a bigger microchip.

My micro is actually quite powerful. The bigger issue in my mind is that it would seem that requiring exceptions makes porting Ada to many microchips unlikely. Whilst I like exceptions, I would actually rather that Ada had never had them or such a complicated runtime.

In any case wouldn't you still need to consider whether you had to handle the exception. However, if the array can not be null then you could just access it without first checking the length? If the length can be 0 then shouldn't you provide a status to indicate that fact to the reader?

It isn't a big deal though. I just thought it would be neat.

[kevlar700]

I actually think this would be a big improvement for Ada without exception propagation where predicates are of no use in this case and contracts are of no use except for with Spark mode. Additionally not null would be generally more intuitive for any runtime.

The record type above is great for library use but problematic for a library user. Perhaps it is not worth the additional compiler complexity but array support of not null would be great for both library creators and library users in my opinion.

[ARG-Editor]

This idea seems rather confused. The expense/complication with returning of arrays is when you return an unconstrained array. In that case, the compiler is obligated to return the bounds along with the array, and usually to use some suboptimal way of managing the return memory (GNAT uses a secondary stack, Janus/Ada uses a managed heap allocation). Whether or not the array is null is mostly irrelevant to those costs.

Moreover, in general, the compiler cannot tell if an array to be returned is null. One needs to use a runtime check to do that. So if the goal is to eliminate exceptional conditions, declaring arrays to be non-null will not do that (at best, it would move any check into the subprogram, and that can be accomplished with a predicate or postcondition).

If you really need to avoid complication in functions that return arrays, you have to have functions that return statically constrained arrays. (For instance, that's all that's supported when interfacing to C.)

BTW, implementing exceptions in an Ada runtime isn't that hard. For Janus/Ada, the core runtime was about 4K on the old 16-bit 8086 processors. That included exceptions and heap management, and some very basic I/O. Back in the day, we had a number of customers using that for various embedded systems (most based on the 80186 chips). I realize that there are processors smaller than a 16-bit 8086, but they don't seem to really need the power of Ada (outside of the fun of proving that it can be done).

[kevlar700]

Thank you for reviewing this and for working on what is already an ambitious language.

Moreover, in general, the compiler cannot tell if an array to be returned is null. One needs to use a runtime check to do that. So if the goal is to eliminate exceptional conditions, declaring arrays to be non-null will not do that (at best, it would move any check into the subprogram, and that can be accomplished with a predicate or postcondition).

Which on a ZFP runtime would result in the last chance handler and the loss of almost all memory. The idea isn't in general. It would be a type definition accepted by a procedure and not returned. You can use SPARK to do this and more at compile time with pre conditions. However, I am currently completing making my whole code base SPARK compliant. However it has taken a bit of time to deal with all of the volatility of a microchip. Is using SPARK for this over kill?

If you really need to avoid complication in functions that return arrays, you have to have functions that return statically constrained arrays. (For instance, that's all that's supported when interfacing to C.)

I'm not interested in C and I actually use no secondary stack because it is a fixed size on light runtimes. Use of the heap in such an arbitrary way might actually be worse. You can still use unconstrained array types with procedures though and even declare them per loop iteration. I would have thought that their type definition could be not null and enforced by the compiler if say N (this loops array range) is of a positive type? I am likely missing a lot of complexity.

BTW, implementing exceptions in an Ada runtime isn't that hard. For Janus/Ada, the core runtime was about 4K on the old 16-bit 8086 processors. That included exceptions and heap management, and some very basic I/O. Back in the day, we had a number of customers using that for various embedded systems (most based on the 80186 chips). I realize that there are processors smaller than a 16-bit 8086, but they don't seem to really need the power of Ada (outside of the fun of proving that it can be done).

Okay. So can it be provided for all cortex-m chips. If not then how many hours should every user spend on how many chips to provide exception support. Then how much time on ensuring that the critical runtime code is correct? Will bugs be easy for the user to understand?

My personal opinion is that this could be reducing Adas adoption rate. It has cost me time and tried my perseverance to some degree. Thankfully, Ada offers so much that it has kept my resolve.

p.s. I think that consideration of ZFP runtimes is far more important than this feature request.

[Richard-Wai]

Okay. So can it be provided for all cortex-m chips. If not then how many hours should every user spend on how many chips to provide exception support. Then how much time on ensuring that the critical runtime code is correct? Will bugs be easy for the user to understand?

My personal opinion is that this could be reducing Adas adoption rate. It has cost me time and tried my perseverance to some degree. Thankfully, Ada offers so much that it has kept my resolve.

p.s. I think that consideration of ZFP runtimes is far more important than this feature request.

I think the ultimate experience of the run-time is more of an implementation detail than a language issue. It seems to be that Randy's point is that Ada itself is not overly onerous in its requirements, and that ZFP or small run-times are not only possible in Ada, it has been common. In modern times, full posix OS's for embedded applications are common and often open-source, which often can support full Ada quite easily (Linux, RTEMS, VxWorks, Greenhills, LynxOS, for example). At the end of the day though, this is not an Ada language issue, rather an implementation issue. That being said, GNAT can do most, if not all, of what you are looking for, even if it takes some work.

For example ZCX: GNAT uses the same GCC backend as C++, and so exception support in Ada is notionally available for most targets. However due to the way ZCX is implemented in GCC, some kind of "runtime" (libc) support is anticipated, but this can be provided by a light-weight embedded libc like newlib. If you have basic libc with malloc, GNAT already can give you essentially full Ada (besides tasking) on any target, nearly out of the box. If you don't want to/can't provide libc for the target, you can make very minor modifications to libgnat to implement a custom last-chance handler, so you don't necessarily need to "lose all memory". If you are slightly more ambitious, you can provide a few custom "libc" operations to provide full exception support on the barest of metal. Currently I'm writing a blog post about both of these strategies, but my time is pretty constrained lately, so that's not worth much. That being said, I have done it and it is trivial.

But again, at the end of the day this is not really a language problem, but an implementation problem, and I think you can argue even then it's really only a problem of documentation or direct support.

As for Ada adoption, keep in mind that most other "sexy" languages have large, well-funded non-profits behind them that try to take on user-experience issues like this. I suspect Ada will get there eventually. Unfortunately, Ada has a long history of proprietary implementations and commercial "support". But it is very clear that this area is improving and AdaCore has done a lot to move things in the right direction. The mere existence of GNAT is amazing achievement for Ada adoption.

Your frustrations are real and felt, and I think there are people working on improvements there.

[kevlar700]

Okay. So can it be provided for all cortex-m chips. If not then how many hours should every user spend on how many chips to provide exception support. Then how much time on ensuring that the critical runtime code is correct? Will bugs be easy for the user to understand? My personal opinion is that this could be reducing Adas adoption rate. It has cost me time and tried my perseverance to some degree. Thankfully, Ada offers so much that it has kept my resolve. p.s. I think that consideration of ZFP runtimes is far more important than this feature request.

I think the ultimate experience of the run-time is more of an implementation detail than a language issue. It seems to be that Randy's point is that Ada itself is not overly onerous in its requirements, and that ZFP or small run-times are not only possible in Ada, it has been common.

Common for Ada maybe, which is not common. There are a lot of runtime files to deal with. It is not a minor distraction to deal with it in confidence. Though a search for protected object support only showed up a few files. I feel like I could manage it but I am kind of against doing so because others that should be using Ada could not or would not do so. I certainly have other priorities, too.

In modern times, full posix OS's for embedded applications are common and often open-source, which often can support full Ada quite easily (Linux, RTEMS, VxWorks, Greenhills, LynxOS, for example). At the end of the day though, this is not an Ada language issue, rather an implementation issue. That being said, GNAT can do most, if not all, of what you are looking for, even if it takes some work.

All of which use C and have CVEs for things that Ada prevents like overflows.

necessarily need to "lose all memory". If you are slightly more ambitious, you can provide a few custom "libc" operations to provide full exception support on the barest of metal. Currently I'm writing a blog post about both of these strategies, but my time is pretty constrained lately, so that's not worth much. That being said, I have done it and it is trivial.

That would be an interesting read, one day. Keep your priorities in tact, of course. I guess this would not provide protected object support? I do not actually need protected object support but a lot of code uses them, aside from Spark code.

As far as I know the last chance handler cannot be returned from and the micro must be reset. I guess that you could store the ram to flash within it. I am not sure if that is more than you should really be doing in a last chance handler, hmm. However the state of the program would be lost, which can with a local non propagating handler, be preserved.

But again, at the end of the day this is not really a language problem, but an implementation problem, and I think you can argue even then it's really only a problem of documentation or direct support.

I'm not so sure that this isn't a language issue. Clocks aren't something that can necessarily apply across all micros especially in this low power age. Though perhaps it is too late. I guess the D.O.D. did not care about project setup costs much. Perhaps you are right in that it can be turned into a configuration step, to some degree. I guess simpler runtimes across the board would hamper e.g. amd64(x64) convenience. It seems that Rust may well be missing a number of language features on embedded systems, too... I think. So perhaps I am mistaken.

As for Ada adoption, keep in mind that most other "sexy" languages have large, well-funded non-profits behind them that try to take on user-experience issues like this. I suspect Ada will get there eventually. Unfortunately, Ada has a long history of proprietary implementations and commercial "support". But it is very clear that this area is improving and AdaCore has done a lot to move things in the right direction. The mere existence of GNAT is amazing achievement for Ada adoption.

I am very thankful for AdaCores work as well as all those involved in Adas illustrious past and future. Ada certainly deserves more funding.