AdaCore Blog

Formal Proof on Device Drivers with SPARK

Formal Proof on Device Drivers with SPARK

by Elsa Ferrara

Programming device drivers requires certain practices or operations. These include, for example, the multitude of volatile variables in the code. Volatiles are necessary to read from/to hardware registers for the device to function correctly and can be modified by the program's external environment.

On the other hand, SPARK imposes a number of restrictions on programs and also limits the use of certain practices permitted in Ada. The conventions imposed by SPARK are not all compatible with this type of code at first sight, so a “SPARKification” step is necessary in order to move on to SPARK-compatible code.

Here's a list of hurdles I encountered during my internship involving driver code and the rules authorized by SPARK. I also present ways of getting around these problems, as well as some best practices for having the most SPARK-compatible code in advance. This list is not exhaustive.

For your information, the examples given in this blog post are code snippets from the library I based my work on during my internship, made by Jeremy Grosser. For the sake of clarity, some parts of the code have been truncated to improve comprehension. You can find the same code after the modifications I've made here.

Volatile object

As mentioned in the introduction, volatile variables are very often present in drivers code, but SPARK imposes very restricted handling of them. Let's take a look at the code below as an example, where XOSC_Periph.CTRL.STABLE is a volatile variable.

procedure Enable_XOSC is
begin
   XOSC_Periph.CTRL.FREQ_RANGE := Val_1_15MHZ;
   XOSC_Periph.CTRL.ENABLE := ENABLE;
   while not XOSC_Periph.STATUS.STABLE loop
      null;
   end loop;
end Enable_XOSC;

This piece of code may seem correct, but it doesn't respect SPARK's rules. Indeed, if we look at SPARK reference manual, section 7.1.3 (10) tells us:

"Contrary to the general SPARK rule that expression evaluation cannot have side effects, a read of an effectively volatile object for reading is considered to have a side effect. To reconcile this discrepancy, a name denoting such an object shall only occur in a non-interfering context."

Even though the SPARK team is considering relaxing the restrictions to accept the original code as well, for the moment we have to deal with it.

We can see that this situation, in which the variable is volatile, does not correspond to a "non-interfering context". It is therefore necessary to transform the code so that it respects this rule. Let's consider this case authorized by the reference manual:

"A name occurs in a non-interfering context if it is: [...] the [right-hand side] expression of an assignment statement"

So, in order to bypass the restriction and allow this volatile variable to be used, we can assign its value to a temporary variable and reuse it later.

procedure Enable_XOSC is
   Tmp : Boolean;
begin
   XOSC_Periph.CTRL.FREQ_RANGE := Val_1_15MHZ;
   XOSC_Periph.CTRL.ENABLE := ENABLE;
   loop
      Tmp := XOSC_Periph.STATUS.STABLE;
      exit when Tmp;
   end loop;
end Enable_XOSC;

There is also a restriction on the declaration of volatiles, as shown in the following code.

function Transmit_Status
      (This : UART_Port)
      return UART_FIFO_Status
is
   Flags : constant UARTFR_Register := This.Periph.UARTFR;
begin
   if Flags.TXFE = False and Flags.TXFF = False then
      return Not_Full;
   elsif Flags.TXFE = False and Flags.TXFF = True then
      return Full;
   elsif Flags.BUSY then
      return Busy;
   elsif Flags.TXFE = True and Flags.TXFF = False then
      return Empty;
   else
      return Invalid;
   end if;
end Transmit_Status;

We cannot declare the variable Flags like that because it must be declared at a library level. This is what the reference manual explains in section 7.1.3 (3):

"The declaration of an effectively volatile stand-alone object or type shall be a library-level declaration. [In particular, it shall not be declared within a subprogram.]"

So it is needed to declare the object in the library and not in a program. In our case, this is not possible because it depends on the function parameter. To avoid this problem, we need to assign every possible Flags value to a variable so that we can reuse it later.

procedure Transmit_Status_Inner
        (Periph : UART_Peripheral;
        Result : out UART_FIFO_Status)
is
   Is_TXFE : constant Boolean := Periph.UARTFR.TXFE;
   Is_TXFF : constant Boolean := Periph.UARTFR.TXFF;
   Is_BUSY : constant Boolean := Periph.UARTFR.BUSY;
begin
   if not Is_TXFE and not Is_TXFF then
      Result := Not_Full;
   elsif not Is_TXFE and Is_TXFF then
      Result := Full;
   elsif Is_BUSY then
      Result := Busy;
   elsif Is_TXFE and not Is_TXFF then
      Result := Empty;
   else
      Result := Invalid;
   end if;
end Transmit_Status_Inner;

The last point about volatile is that the function doesn't support volatiles but if the variable is just an input variable, the function can be annotated with "Volatile_Function". Like in this example where CLOCKS_Periph is a volatile record.

function Enabled (CID : Clock_Id) return Boolean
is (CLOCKS_Periph.CLK (CID).CTRL.ENABLE)
  with Volatile_Function;

Use of global parameters

Another problem of becoming SPARK-compatible is the use of global parameters. As you may know (or not) functions and procedures are not the same, the distinction between the two is that a function returns a value, and a procedure does not. In SPARK, the difference is even stronger, as a function is not allowed to have side effects (no modification on the variables).

function Frequency
      (CID      : Countable_Clock_Id;
       Rounded  : Boolean := True;
       Accuracy : UInt4 := 15)
      return Hertz
is
   F : Hertz;
begin
[...]
   if CLOCKS_Periph.FC0_STATUS.DIED then
      return 0;
   else
      F := Hertz (CLOCKS_Periph.FC0_RESULT.KHZ) * 1_000;
      if Rounded then
         return F;
      else
         return F + ((Hertz (CLOCKS_Periph.FC0_RESULT.FRAC) * 3125) / 100);
      end if;
    end if;

This is an example of a simple function. At first it seems compatible with SPARK restriction but as CLOCKS_Periph is a global parameter it is not permitted for this subprogram to be a function due to the side effect I mentioned before. So we have to transform it into a procedure. In some cases it can be easy or not very disturbing but sometimes you will need the result of the function in preconditions for example so the adaptation is then more complicated.

The following snippet has the same functionality as the above code but implements it as a procedure while the return value is an out parameter.


procedure Frequency
     (CID      : Countable_Clock_Id;
      Result : out Hertz;
      Rounded  : Boolean := True;
      Accuracy : UInt4 := 15)
is
   F : Hertz;
   Tmp : Boolean;
   Tmp2 : HAL.UInt25;
   Tmp3 : HAL.UInt5;
begin
   [...]      
   Tmp := CLOCKS_Periph.FC0_STATUS.DIED;
   if Tmp then
      Result := 0;
   else
      Tmp2 := CLOCKS_Periph.FC0_RESULT.KHZ;
      F := Hertz (Tmp2) * 1_000;
      if Rounded then
         Result := F;
      else
         Tmp3 := CLOCKS_Periph.FC0_RESULT.FRAC;
         Result := F + ((Hertz (Tmp3) * 3125) / 100);
      end if;
   end if;
 end Frequency;

If you intend your code to be validated in SPARK, let's keep in mind that global variables can be problematic so try to limit the use of functions as much as possible.

Access to variables

Writing device drivers sometimes involves reading and having access to multiple instances of the same peripheral, in such cases it can be interesting to use pointers. Pointers are not a big problem because they are permitted in SPARK, but not when a variable is volatile and just like I said before volatiles are part and parcel of the device code.

We can take, for example, this function which calls PLL_SYS_Periph and PLL_USB_Periph instances of the PLL_Peripheral type by access.

procedure Configure_PLL
      (PLL    : PLL_Clock_Id;
       Config : PLL_Config)
is
   Periph : constant access PLL_Peripheral :=
      (if PLL = PLL_SYS then PLL_SYS_Periph'Access else PLL_USB_Periph'Access);
begin
   [...]
end Configure_PLL;

An error is raised by SPARK as both variables are volatile. To avoid this problem, we introduce an auxiliary function into the main function, with the variable initially pointed to by access as an additional argument.

Thus, we can call the inner function with the right parameters depending on the value wanted.

procedure Configure_PLL
     (PLL    : PLL_Clock_Id;
      Config : PLL_Config)
is
   procedure Inner_Config (Periph : in out PLL_Peripheral) is
   begin
      [...]
   end Inner_Config;
begin
   if PLL = PLL_SYS then
      Inner_Config (PLL_SYS_Periph);
   else
      Inner_Config (PLL_USB_Periph);
   end if;
end Configure_PLL;

Note that we used this trick for the SPI and UART ports to call the right peripherals. This was possible as there were only two ports for each protocol.

You can also see below how the port declarations were adapted to avoid using pointers. Instead of having the pointer, we give the correct variable depending on the port concerned.

SPI_0 : aliased RP.SPI.SPI_Port (0, RP2040_SVD.SPI.SPI0_Periph'Access);
SPI_1 : aliased RP.SPI.SPI_Port (1, RP2040_SVD.SPI.SPI1_Periph'Access);
-- new declaration   
SPI_0 : aliased RP.SPI.SPI_Port (0);
SPI_1 : aliased RP.SPI.SPI_Port (1);
procedure Enable_IRQ (This :        SPI_Port;
                         IRQ  :        SPI_IRQ_Flag)
is
   procedure Enable_IRQ_Inner (IRQ  :        SPI_IRQ_Flag;
                               Periph : in out SPI_Peripheral)
   is
   begin
      [...]
   end Enable_IRQ_Inner;
begin
   case This.Num is
      when 0 => Enable_IRQ_Inner (IRQ, SPI0_Periph);
      when 1 => Enable_IRQ_Inner (IRQ, SPI1_Periph);
   end case;
end Enable_IRQ;

This was possible as there were not a lot of ports, but we can see the limits here and how it can be difficult not to use access.

These restrictions also led us to modify a large part of the program by removing the HAL abstraction initially present. Indeed, interface accesses are not supported in SPARK at the moment. For the purposes of this internship, we have therefore chosen to remove this abstraction, which may be problematic in the context of a larger project where the code will be multiplied.

Address

The address clause is authorized under certain conditions but in the example below it is not permitted as the object is not fully initialized at declaration.

AUXSRC : CLK_CTRL_AUXSRC_Field
  with Volatile, Address => CLOCKS_Periph.CLK (GP).CTRL.AUXSRC'Address;

In this case to avoid having problems with SPARK, it is recommended to rename the variable as it corresponds to the same operation. The fewer clause addresses you use, the fewer problems you will encounter.

AUXSRC : CLK_CTRL_AUXSRC_Field renames CLOCKS_Periph.CLK (GP).CTRL.AUXSRC;

If renaming is not possible, it's best to avoid accessing the address of values when not required. If the address is mandatory, use SPARK_Mode => Off.

Numeric type and conversion

A basic recommendation is that the data type should be as precise as possible. Even if this has no direct impact, it greatly facilitates proof by SPARK. It's also easy to specify types in this kind of application, where data is often constrained by the environment or hardware.

It's also recommended to be careful with type conversions, as a wrong conversion can corrupt data integrity. For example, SPARK does not yet allow conversion between fixed-point and floating-point. The use of unchecked conversions must be limited, and the size of both types must be specified and equal.

Conclusion

So we've looked at a few tricks for adapting existing low-level code to SPARK and reconciling SPARK restrictions with the needs of driver code. While SPARK imposes certain restrictions on device driver programming, it presents an opportunity to create secure and reliable code. By embracing the challenges and following best practices, developers can achieve SPARK-compatible solutions that ensure robustness and improve the overall quality of their projects.

Posted in

About Elsa Ferrara

Elsa Ferrara

Elsa joined AdaCore in 2023 as an intern in the SPARK team as part of her engineering degree at ENSIIE.