alire-project / GNAT-FSF-builds

Builds of the GNAT Ada compiler from FSF GCC releases
MIT License
32 stars 9 forks source link

msp430-elf toolchain #47

Closed JeremyGrosser closed 1 year ago

JeremyGrosser commented 1 year ago

Before this toolchain is useful to anyone, the msp430-elf target needs to be added to gprconfig_kb in order for gprbuild to find it. I did that in this commit, based on gprconfig_kb's master branch. GNAT-FSF-builds uses the 22.0.0 release of gprconfig_kb, so we'll either need to backport this patch or switch to a newer version.

I ported TI's blink demo to SPARK/Ada, using bare_runtime: https://github.com/JeremyGrosser/msp430test/blob/master/src/msp430test.adb

The main procedure passes gnatprove verification, but bare_runtime does not, so analysis of those units is skipped.

JeremyGrosser commented 1 year ago

I've generated linux64 binaries for this toolchain and setup a separate Alire index repo to point to them. Maybe it makes sense to just maintain these things separately to reduce @mosteo's workload. https://github.com/JeremyGrosser/alire-index-msp430

Fabien-Chouteau commented 1 year ago

Hi Jeremy thanks for the contribution. To be honest I won't have much time to look at this in the short term.

About the separate index, that's a good short term solution. But for the mid to long term it's better to have all the toolchain stuff built from the same place and available in the same index.

JeremyGrosser commented 1 year ago

Makes sense, thanks for taking a look!

JeremyGrosser commented 1 year ago

I tried porting bb-runtimes to this architecture, but I ran into some trouble with libgnat. It uses Unsigned to store the mantissa of IEEE Float. There's an assertion that checks that 'Machine_Mantissa <= Uns'Size, which fails. The implementation of Machine_Mantissa has a minimum of 24 bits, so this obviously won't work on a 16-bit machine.

Patching libgnat or removing Float support is a bit further than I want to go with this project, so I'm abandoning this PR. TI themselves have announced some upcoming chips with the MSP430 peripherals attached to a Cortex-M0+, so I think the days are numbered for this architecture anyway.

Fabien-Chouteau commented 1 year ago

If you can find a solutionbare_runtime for this problem in I am interested.