AdaCore Blog

SPARK, Beyond Normal Termination

SPARK, Beyond Normal Termination

by Claire Dross –

When teaching SPARK to my students, I generally explain the central position of contracts in formal verification in the following way: Contracts of subprograms summarize their behavior - preconditions constrain their inputs, while postconditions describe their effects. It is an easy way to see contracts, However, not returning normally, for example looping forever or raising exceptions, is definitely a significant effect of a subprogram. Modeling that effect would be beneficial because if it occurs in an unexpected way it might cause the entire program to derail. Release 24.0 of SPARK includes contracts that can be used to reason about subprograms which do not return normally.

Historically, SPARK has only been concerned with partial correctness, that is, verifying that a program is correct and abides by its contract, but not that it terminates. This choice is motivated by the fact that termination might be hard to verify - it typically requires users to provide decreasing metrics in loops and recursive subprograms - and might not be the focus of users. In the previous releases of SPARK, a tool-specific annotation, Always_Returns, allows users to request that the tool verifies the termination of their subprogram. In all subprograms, whether termination is requested or not, calls to No_Return procedures and statements raising exceptions are allowed, but only inside dead code - SPARK attempts to prove that the statements are never reached. Together, this allows a complete verification of subprograms which always return normally.

This partial solution is arguably appropriate for functions, which are restricted in SPARK to prevent side-effects. However, for procedures, this solution has reached its limits. First, it is rather ad-hoc: why silently allow an infinite loop in a subprogram whose termination has not been requested, but disallow a call to a No_Return procedure doing this exact same loop? Second, it is exceedingly constraining. Users want subprograms which sometimes terminate and sometimes don't, they want to be able to call No_Return procedures from them, and to regain termination in callers if they are only called in contexts in which they terminate. For exceptions it is the same story. Users want to verify their defensive coding leading to an exception being raised, and possibly also the handlers used to recover. Finally, treating all exceptions as errors makes annotating the Ada standard library more complicated, as it relies on exceptions to report issues. Some of these exceptions can be avoided using preconditions, but for others, that express properties which are not precisely modeled in SPARK, it is difficult and cumbersome for the user. As an example, using preconditions to protect against issues in the IO file system primitives is hardly feasible.

The upcoming release 24.0 of SPARK makes "abnormal termination" a first-class citizen. This feature is based on two new aspects: Exceptional_Cases and Always_Terminates. The aspect Exceptional_Cases allows users to list the exceptions that can be propagated by a procedure. For each propagated exception, a postcondition can be added that should hold whenever the corresponding exception is propagated by the procedure. Let us look at an example to illustrate its usage. Consider a procedure Parse_Natural which takes a string and returns the natural number encoded by the string. This procedure might fail for many reasons: an invalid input, an overflow in the computation... These failures cause exceptions to be raised:

Empty_Input    : exception;
Unexpected_Char: exception;
Overflow       : exception;

procedure Parse_Natural (S : String; Res : out Natural) is
begin
   if S'Length = 0 then
      raise Empty_Input;
   end if;
   Res := 0;

   for I in S'Range loop
      if S (I) not in '0' .. '9' then
         raise Unexpected_Char;
      elsif Res > Integer'Last / 10
        or else Res * 10 > Integer'Last -
          (Character'Pos (S (I)) - Character'Pos ('0'))
      then
         raise Overflow;
      end if;

      Res := Res * 10 + (Character'Pos (S (I)) - Character'Pos ('0'));
   end loop;
end Parse_Natural;

To specify my procedure, I define ghost functions to parse a sequence of digits. For them to be easier to use, I have chosen to avoid requiring preconditions and instead make them work on any string by parsing all unexpected characters as 0. I use big integers to avoid any overflows:

--  Ghost specification programs to read a number from a string

function Read_Digit (C : Character) return Big_Natural is
   (if C in '0' .. '9'
    then To_Big_Integer (Character'Pos (C) - Character'Pos ('0'))
    else 0)
with Ghost;

function Read_Number (S : String; Last : Integer) return Big_Natural is
   (if Last < S'First then 0
    else Read_Number (S, Last - 1) * 10 + Read_Digit (S (Last)))
with Ghost,
  Pre  => Last <= S'Last,
  Post => (for all I in S'Range =>
             (if I < Last then Read_Number (S, I) <= Read_Number'Result)),
  Subprogram_Variant => (Decreases => Last);

function Read_Number (S : String) return Big_Natural is
   (Read_Number (S, S'Last))
with Ghost,
  Post => (for all I in S'Range => Read_Number (S, I) <= Read_Number'Result);

Using these ghost functions, I can now encode the Parse_Value procedure and its possible error cases easily. The Exceptional_Cases aspect lists the 3 exceptions which might be propagated by Parse_Natural, and, for each of them, the situation in which they might be reached. Note that the fact that an exception will necessarily be propagated if an issue is encountered is ensured by the postcondition.

--  The procedure parsing a natural number

procedure Parse_Natural (S : String; Res : out Natural) with
  Post => S'Length > 0
    and then (for all I in S'Range => S (I) in '0' .. '9')
    and then To_Big_Integer (Res) = Read_Number (S),
  Exceptional_Cases =>
    (Empty_Input     => S'Length = 0,
     Unexpected_Char =>
       (for some I in S'Range => S (I) not in '0' .. '9'),
     Overflow        =>
       Read_Number (S) > To_Big_Integer (Integer'Last)));

Even if they are effectively postconditions, exceptional contracts are often used to constrain the cases where an exception can be raised, as I did for Parse_Natural. It is still possible to mention global outputs in these contracts, as well as output values of parameters as long as they are passed by reference. They allow users to specify the expected value of objects modified by the subprogram if an exception is propagated. This is interesting in particular because release 24.0 of SPARK also supports exception handlers. The SPARK proof tool will make sure that the exceptional postconditions are valid when an exception is propagated. Exceptional paths, going from the point where an exception is raised to the point where it is handled, are treated as normal paths by the tool. The behavior for exceptions which are not expected (handled or expected to be propagated) stays the same: the tool will make sure that they are never raised. As an example, consider the two functions To_Natural below. The first one contains a handler to catch the exceptions that might be propagated while parsing the string. The second does not have a handler, so SPARK will ensure that the call to Parse_Natural in its body never raises an exception.

function Valid_Natural (S : String) return Boolean is
  (S'Length > 0
   and then (for all I in S'Range => S (I) in '0' .. '9')
   and then Read_Number (S) <= To_Big_Integer (Natural'Last))
with Ghost;

type Natural_Option (Present : Boolean := False) is record
   case Present is
      when True  =>
         Val : Natural;
      when False =>
         null;
   end case;
end record;

function To_Natural (S : String) return Natural_Option with
  Post =>
    Valid_Natural (S) = To_Natural'Result.Present
    and then
      (if Valid_Natural (S) then To_Big_Integer (To_Natural'Result.Val) = Read_Number (S));

function To_Natural (S : String) return Natural_Option is
begin
   return Res : Natural_Option (True) do
      Parse_Natural (S, Res.Val);
   end return;
exception
   when others =>
      return (Present => False);
end To_Natural;

function To_Natural (S : String) return Natural with
  Pre  => Valid_Natural (S),
  Post => To_Big_Integer (To_Natural'Result) = Read_Number (S);

function To_Natural (S : String) return Natural is
begin
   return Res : Natural do
      Parse_Natural (S, Res);
   end return;
end To_Natural;

To avoid a blow-up of exceptional annotations on big call graphs, the keyword "others" can be used instead of an exception name in the aspect Exceptional_Cases to refer to any exception.

The second aspect introduced in SPARK 24 is used to specify cases where a subprogram loops forever or exits the subprogram in a non-standard way - a jump, or a call to OS_Exit for example. The Always_Terminates aspect allows users to supply a condition under which the subprogram needs to terminate normally or raise an exception. In most cases, the condition is simply True, for subprograms which always terminate, or False, for those which might not terminate. A condition of True can be omitted. In general, the subprogram shall terminate whenever its terminating condition evaluates to True on entry of the subprogram. The SPARK proof tool will ensure that this is the case. Let us look at some simple examples:

procedure Might_Loop_Forever with
  Always_Terminates => False;

procedure Might_Loop_Forever is
begin
   loop
      null;
   end loop;
end Might_Loop_Forever;

procedure Loops_Forever with
  No_Return,
  Exceptional_Cases => (others => False),
  Always_Terminates => False;

procedure Loops_Forever is
begin
   loop
      null;
   end loop;
end Loops_Forever;

procedure Loops_When_B (B : Boolean) with
  Post => not B,
  Always_Terminates => not B;

procedure Loops_When_B (B : Boolean) is
begin
   if B then
      Loops_Forever;
   end if;
end Loops_When_B;

procedure Terminates with
  Always_Terminates;
--  or Always_Terminates => True

procedure Terminates is
begin
   Loops_When_B (False);
end Terminates;

The annotation of Might_Loop_Forever states that it does not need to terminate. However it still might. To ensure that it actually doesn't, we must add either a postcondition of False or a No_Return Annotation, like for Loops_Forever. Note the Exceptional_Cases aspect on Loops_Forever. It is necessary because, unlike for regular subprograms, No_Return procedures can raise any exception by default. The procedure Loops_When_B is similar to Might_Loop_Forever but the combination of its Always_Terminates aspect and its postcondition describes precisely how it actually behaves. It makes it possible to call Loops_When_B inside Terminates which always returns normally.

Together, the Exceptional_Cases and Always_Terminates aspects allow for a precise handling of procedures which might not return normally. They make it possible to specify when abnormal termination is allowed and what happens in that case, so normal termination can be recovered in callers under the right conditions. As a last example, consider a procedure, Retry_Connect_Socket, that attempts to connect to a socket several times and raises an exception if the connection fails. The maximal number of attempts is given as a parameter. The special value 0 can be supplied to state that we should try indefinitely:

procedure Connect_Socket
  (Socket : aliased in out Socket_Type;
   Server : in out Sock_Addr_Type)
with
  Global => null,
  Pre  => not Is_Connected (Socket),
  Post => Is_Connected (Socket),
  Always_Terminates,
  Exceptional_Cases => (Socket_Error => not Is_Connected (Socket));
--  Make a connection to another socket which has the address of Server. Raise Socket_Error on error.

procedure Retry_Connect_Socket
  (Socket  : aliased in out Socket_Type;
   Server  : in out Sock_Addr_Type;
   Try_Num : Natural)
with
  Pre  => not Is_Connected (Socket),
  Post => Is_Connected (Socket),
  Always_Terminates => Try_Num /= 0,
  Exceptional_Cases =>
      (Socket_Error => Try_Num /= 0 and then not Is_Connected (Socket));


procedure Retry_Connect_Socket
  (Socket  : aliased in out Socket_Type;
   Server  : in out Sock_Addr_Type;
   Try_Num : Natural)
is
begin
   if Try_Num = 0 then
      loop
         pragma Loop_Invariant (not Is_Connected (Socket));
         begin
            Connect_Socket (Socket, Server);
            return;
         exception
            when Socket_Error =>
               null;
         end;
      end loop;
   else
      for K in 1 .. Try_Num - 1 loop
         pragma Loop_Invariant (not Is_Connected (Socket));
         begin
            Connect_Socket (Socket, Server);
            return;
         exception
            when Socket_Error =>
               null;
         end;
      end loop;
      Connect_Socket (Socket, Server);
   end if;
end Retry_Connect_Socket;

The expected behavior of Retry_Connect_Socket can be expressed easily in a contract using a combination of Always_Terminates and Exceptional_Cases. If it returns normally, then the socket is necessarily connected. It will necessarily terminate unless Try_Num is set to 0 (which means that there is no bound on the number of retries). The Socket_Error exception might be raised if a positive number of tries is specified. In this case, the socket is not connected. Note that the Socket parameters of Connect_Socket and Retry_Connect_Socket are marked as aliased. It is to ensure that it is passed by reference so it can be mentioned in the exceptional postcondition. The Retry_Connect_Socket procedure can be successfully verified by the SPARK proof tool.

This support will be available in the 24.0 release of SPARK Pro. Don't hesitate to try it out and tell us what you think!

Posted in #SPARK    

About Claire Dross

Claire Dross

Claire Dross has a PhD in deductive verification of programs using a satisfiability modulo theory solver with the Universite Paris-Sud. She also has an engineering degree from the Ecole Polytechnique and an engineering degree from the Ecole Nationale Superieure des Telecommunications. At AdaCore, she works full-time on the formal verification SPARK 2014 toolset.