Forcing GNAT to use 32-bit load/store instructions on ARM?

[daniel.dmk@googlemail.com]

Hello,

I've started using GNAT GPL for ARM (hosted on Windows) and I'm working on some code in SPARK 2014 to interface to memory-mapped registers to control registers on the STM32 F4 microcontroller, however I'm having trouble where GNAT is using byte loads/stores to the registers, instead of word load/stores (32-bit).

For a lot of registers on the STM32 it is necessary to always access the registers using 32-bit load/store instructions. Using half-word (16-bit) or byte (8-bit) accesses generates a CPU fault with these registers.

I'm representing the 32-bit register as a record as follows:

   type Bits_1 is mod 2**1 with Size => 1;

   type CR_Register is
      record
         RNGEN : Bits_1;
         IE    : Bits_1;
      end record;
   for CR_Register use
      record
         RNGEN at 0 range 2 .. 2; -- bits 0 .. 1 are reserved
         IE    at 0 range 3 .. 3;
         -- bits 4 .. 31 are reserved
      end record;
   for CR_Register'Size use 32;

I then define the register of type CR_Register at the peripheral's base address:

   CR : CR_Register
     with Size => 32,
       Volatile,
       Async_Readers, Async_Writers,
       Address => System'To_Address(Base_Address);

I'm using a record instead of a simple Unsigned_32 type so that:
1) I can hide access to the "reserved" parts of the register,
2) The code to modify the register is straightfoward.

For example, enabling the peripheral is done by setting the RNGEN bit to 1:

   CR.RNGEN := 1;

However, the GNAT compiler uses the ARM instruction ldrb to load the lower 8 bits of the register, modify the byte (or 16#40#), then use strb to write the lower 8-bits back to memory. This causes a fault since the register must be accessed using a 32-bit load/store instructions (the ldr and str instructions).

Does anyone know how I can force GNAT to generate the appropriate instructions?

Things I have tried:
1) Using the Atomic aspect on the record type and CR object had no effect on the code generated.
2) Using Pack.
3) Declaring the bits inside the register as: Bits_32 range 0 .. 1;

So far, I am able to get GNAT to use 32-bit load/stores only when I read the entire record into a temporary variable, as follows:

   declare
      Temp : CR_Register;
   begin
      Temp := CR;
      Temp.RNGEN := 1;
      CR := Temp;
   end;

However, this makes it more "clunky" to use in my opinion. I would prefer to be able to modify the bits directly, and have the compiler always use 32-bit load/store instructions.

Does anyone else have any ideas that I could try?

Thanks,
Dan