SPARK 27 Release Notes¶

We present here a few highlights of the new features in SPARK 27. You can access the complete list here.

Language Extensions ¶

Support for functions with side-effects in more locations ¶

Generally, SPARK forbids side-effects in expressions. Functions that perform side effects (modify a global or a parameter, propagate an exception…) need to have the Side_Effects aspect and can only be used in specific places. SPARK now supports calls to functions with side-effects in more contexts. In addition to the left-hand side of assignments and the initial value of objects declared outside of a declare block, it is now possible to call functions with side-effects directly in:

the initialization of an extended return statement;
the expression of a return statement;
the condition of an if/elsif statement;
the selecting expression of a case statement;
the condition of an exit statement; and
the condition of a continue statement.

These extensions make using functions with side-effects much more natural in SPARK, reducing the burden to translate existing Ada to SPARK.

Precise global and parameter modes by proof ¶

In SPARK’s modular analysis, an in/out parameter of or global modified by a called subprogram is assumed to be completely and unconditionally modified by the call; developers are therefore required to state explicitly everything that is not modified and when, whenever greater precision is desired.

SPARK now provides the Modifies aspect, which allows developers to state when a parameter or global is modified and which parts, for composite types. For example:

type R is record
   F1, F2 : Boolean;
end record;
type RR is record
   G1, G2 : R;
end record;

procedure Write_G1_F1 (B : Boolean; X : in out RR) with
  Modifies => X.G1.F1 when B;

procedure Write_G1_F1 (B : Boolean; X : in out RR) is
begin
   if B then
      X.G1.F1 := False;
   end if;
end Write_G1_F1;

Referring to loop index in `for .. of` loops ¶

Ada provides array component iterators and container element iterators using the for .. of syntax, which yields cleaner loop bodies than for .. in without the need to capture the current element in a constant declaration inside the loop. However, since SPARK uses induction to prove loops, for .. of generally cannot be used as the loop index is typically required in the loop invariant for induction.

SPARK now offers a new attribute 'Loop_Index that allows the current loop iteration to be retrieved from array components or container elements. This allows induction to be performed while using for .. of.

For example, it will be possible to write:

for E of S loop
   if E = 0 then
     C := C + 1;
   end if;
   pragma Loop_Invariant (C <= E'Loop_Index - S'First + 1);
end loop;

where previously the loop would have required for .. in, instead, to establish the bound on C using induction.

Referring to values at labels ¶

SPARK developers can now use 'At to refer to the value of an object at a previous program point. Ada has provided ‘Old and ‘Loop_Entry, which allow the initial value of a subprogram parameter or the initial value of an object at the time a loop was entered to be referenced, respectively. Using ‘At, a developer can refer to the value of an object at a specific label, like this:

X := 1;
<<My_Label>>
X := 2;
pragma Assert ((X-1)'At (My_Label) = 0);

which is equivalent to

X := 1;
declare
   Compiler_Generated_Unique_Name : constant Integer := (X-1);
begin
   X := 2;
   pragma Assert (Compiler_Generated_Unique_Name = 0);
end;

Precise support for overlays ¶

Objects that share the same underlying memory region are referred to as overlays. SPARK now handles these objects precisely, in simple cases. As an example, we are able to prove the following code:

with Interfaces; use Interfaces;
procedure Test with SPARK_Mode is
   type Four_Small_Ints is record
      F, G, H, I : Unsigned_8;
   end record;
   for Four_Small_Ints use record
      F at 0 range 0 .. 7;
      G at 0 range 8 .. 15;
      H at 0 range 16 .. 23;
      I at 0 range 24 .. 31;
   end record;

   X : Unsigned_32 := 256;
   Y : Four_Small_Ints with Import, Address => X'Address;
begin
   pragma Assert (Y = (0, 1, 0, 0));
end;

This feature helps to enable zero-copy provable parsing of binary data into simple record types.

Refer to Discriminants of Unchecked Union Types ¶

The discriminants of unchecked union types are not actually stored in memory. As a result, it is not usually possible to access it. SPARK now allows references to the discriminants of unchecked union types when they occur in non-executable ghost code (i.e., ghost code with an assertion level that depends on Static):

type Int_Or_Float (Is_Int : Boolean := True) is record
  case Is_Int is
     when True =>
        My_Int : Integer;
     when False =>
        My_Float : Float;
  end case;
end record with Unchecked_Union;

procedure Increase_Int_Value
  (X : in out Int_Or_Float)
with
 Pre  => (Static => X.Is_Int and then
                    X.My_Int < Integer'Last),
 Post => (Static => X.Is_Int and then
                    X.My_Int = X.My_Int'Old + 1)
is
begin
  X.My_Int := X.My_Int + 1;
end Increase_Int_Value;

User Experience ¶

Proof manifests ¶

SPARK now offers proof manifests, an entirely new capability. Proof manifests are helpful in two situations:

to provide per-subprogram proof settings; and

to offer simpler, easier-to-use replay support for reproducing proofs in CI.

Proof manifests are TOML files that can be generated by calling gnatprove with --generate-manifest-dir and used by calling gnatprove with --proof-manifest-dir. Proof manifests offer hierarchical refinement: default settings placed on a unit can be overridden or augmented on a per-subprogram basis as needed.

Show if a proof comes from a cache ¶

SPARK now offers insight into whether a proved check was (re)proved by the solvers on the current run or served from a cache (local or file-based memcached). This can help explain situations in which SPARK results appear to be nondeterministic and can aid in debugging memcached-based CI deployments of SPARK. When gnatprove is run with --report=provers, in addition to reporting which prover proved a given check, gnatprove reports which cache, if any, provided the proof.

Feedback on why provers stopped working on unproved checks ¶

SPARK now provides information about why its provers stopped working on unproved checks.

Broadly speaking, provers stop working on checks for one of two reasons:

The provers reached configured resource limits. SPARK limits its provers with timeouts, step limits, and memory limits. If a prover stopped working because a given limit was reached, increasing that limit might result in a proved check.

The provers stopped working on the check even though resource limits were not reached. SPARK’s provers have internal heuristics that sometimes cause them to stop work early. This does not necessarily mean the check is proved false; it does mean that increasing timeout or step limit, for example, will not help.

SPARK now provides this information via new information appended to the check message:

[provers reached <limit> limit before completing the proof], where <limit> is one or more of time, step, and memory (e.g. [provers reached time and step limit before completing the proof]), or

[provers gave up before completing the proof]

In both cases, following the guidance in the section “How to Investigate Unproved Checks” of the SPARK User Guide remains our strong recommendation.

Provers are now staggered by default ¶

If users request multiprocessing (-j switch), GNATprove runs provers in parallel on the same checks in a “race”, then stops the remaining ones if one prover found a proof. While this leads to faster results, it can also lead to wasted work when most checks are proved by one fast prover, which is quite common. Now, the first prover is run first with a small head start; subsequent provers are then run shortly afterwards, if the first prover has not already found a proof.

SPARKlib Improvements ¶

Access-type conversions ¶

Access-type conversions, like overlays, can be used to reinterpret a value of a given type as a value of another type. This is especially useful for providing a typed reinterpretation of binary data with zero copies. While overlays provide an effective means to accomplish this within a subprogram, access-type conversions allow the resulting typed reinterpretation to be exported for use by the rest of the program.

SPARK now supports access-type conversions safely via the SPARKlib. The result of the conversion is a borrow or an observe, integrating fully into SPARK’s ownership model.

Tree-container library ¶

The SPARKlib now provides formal and functional generic trees. Like the other containers in the SPARKlib, developers can use these containers in their code and prove properties about the containers and the elements contained therein.

Linked Structures in Arrays ¶

The Higher-Order part of the SPARKlib now provides functions for reasoning about acyclic linked structures stored in an array. They work on arrays that store one or several linked structures using a Next function: for each cell in the array, the index of the next cell is returned by Next.

The Reachability package defines three functions over these structures, along with some lemmas that can be used to reason over them. The function Reachable_Set returns the functional set of all the indices in the array that can be reached from X by calling Next repeatedly. Finally, the function Model computes a functional sequence that stores the indices reachable from X in the reverse of the order in which they occur: the first element of the sequence is the last index of the structure, the one whose Next is No_Index, and the last element is X itself.