Now that SPARK has exceptional_cases is it possible to build the light runtimes for e.g. cortex-m0+ and cortex-m4 as GNAT provides but with just exception propagation support added (assuming that exception propagation is compatible with CPU clock speed changes for low power parts)?
AFAIK, the limitation of the light runtimes with exceptions is not that they could not be proven, but the fact that there needs to bee some code managing the information during an exception and that requires more than just a light runtime. However, I suppose that it will be easier than adding a tasking system 
Best,
Fer
1 Like
Exception propagation requires other runtime support such as a full heap allocator, but AFAIU it does not depend on tasking features so in theory you could set up a runtime that adds exception propagation without including tasking.
1 Like
I was hoping I could just replace the Ada.Exception package in the light runtime with one from embedded and maybe drop some features and add/replace some support like an allocator as needed but it doesn’t seem that straight forward with GNATs and bb-runtimes sources looking different and no idea how to build gnat_arm_elf. Seems like a rabbit hole.
Copilot reckons it wouldn’t be compatible with both the cortex-m0 and cortex-m4 either
“Cortex-M0/M0+ lacks the ARM exception unwinding instructions (ldmia/stmia patterns used in higher cores). The light runtime avoids this complexity.”
There’s no need to build gnat_arm_elf to build the runtime. You may be able to adapt bb-runtimes to gather the correct sources for what you want, but this isn’t entirely straightforward since you basically want to define your own source profile that is a mix of “light” and “embedded”, so that will be a bit more work than a usual port.
Depending on what you want to do, the simplest solution may be to just stick with the “embedded” profile if you want exception propagation, even if you don’t need tasking.
Copilot reckons it wouldn’t be compatible with both the cortex-m0 and cortex-m4 either
“Cortex-M0/M0+ lacks the ARM exception unwinding instructions (
ldmia/stmiapatterns used in higher cores). The light runtime avoids this complexity.”
Copilot is just plain wrong here. There are already runtimes that support exception propagation on Cortex-M0+ such as embedded_rp2040, and ldmia/stdmia are load/store instructions; they are not specific to exception unwinding nor are they related to the “light” runtime.
1 Like
I’m hoping for a runtime that runs on any cortex-m0+ and one that runs on any cortex-m4. I’m not actually bothered about stack unwinding as I could log next to the raise or handlers anyway but the ability of SPARK to track unhandled and the with Exception_Cases seems neat and would unify embedded and desktop code. The embedded profile would bring in clock speed dependent code but I want to keep the ability of dynamically changing the clock speed for low power devices like STM32U073 without affecting the runtime 
If I actually new how to build the light runtime bundled with GNAT then I might have a starting point. Is that done via bb-runtimes?
Ah I understand. So you basically want something like a light-cortex-m0p runtime, but which also supports exception propagation. This should be doable in theory, but as I mentioned above you’ll basically need something that’s a mixture of “light” and “embedded” (i.e. embedded without tasking), which hasn’t been done before.
I think we need to be careful to avoid getting confused between two steps here: generating the runtime source tree, and building (compiling) the runtime.
bb-runtimes generates the source tree by gathering a set of source files from various places (such as the gcc sources and target-specific sources stored in bb-runtimes), and pulls them together into one place, along with other required files such as a GPR file to compile the runtime. The top-level directory of a “light” runtime source tree contains things like:
gnatgnat_userldld_userada_object_pathada_source_pathruntime.xmlruntime_build.gprtarget_options.gpr
Compiling the runtime is then just a case of navigating to the generated source tree and using GPRbuild to compile everything. For a light runtime this would look something like:
gprbuild -P runtime_build.gpr -j0
While you could probably patch bb-runtimes to define your own profile which includes exception propagation, that will probably be fairly difficult for someone without much experience with the internals of bb-runtimes.
Another approach could be to take a generated runtime source tree for an existing “embedded” runtime, and strip out libgnarl (the library that implements tasking stuff in the runtime), leaving you with libgnat only (the library that implements the sequential stuff in the runtime). I’ve never tried this though, so I don’t know if there might still be some stuff in libgnat which references units in libgnarl that you may need to deal with.
1 Like
Exception handling doesn’t depends from any clocks, it should be doable to port it to light runtime, but it requires some amount of work.
You can use embedded runtime, it has exceptions support, and if code doesn’t use of any tasking constructs will not bring tasking support code into executable. However, it depends from the CPU clock (SysTick).
1 Like
I lost steam as I’m a little confused as to whether I actually want to replace my Status enum predicates with Exceptions. In regard to whether it matters that each status provides a compiler enforced case statement at each return vs the more global nature of exceptions . I guess exceptions being standardised wins out as well as not having to pass them (debatable) but I decided I have other priorities.
I guess if you aren’t using the code that uses the SysTick then the SysTick speed potentially changing may be irrelevant.
Yes, if application doesn’t use tasking constructs and Ada.Calandar/Ada.Real_Time (note, they are used by delay), it should work well.
1 Like