SPARK 20 Release Notes¶
We present here a few highlights of the new features in SPARK 20. You can access the complete list here.
Improved Support of Language Features¶
Support for Pointers Through Ownership¶
SPARK now supports pointers (a.k.a. values of access type) through the restrictions provided by ownership rules. These rules guarantee that, at any given point in the program, there is a unique name to refer to mutable data, which makes formal verification possible without requiring a huge annotation effort from users.
It makes it possible to implement in SPARK data structures that could only previously be implemented in Ada and made available to SPARK analysis through an interface (private types with an API):
data structures whose size evolves;
data structure containing indefinite elements, such as
String
;recursive data structures (lists, trees).
The detailed ownership rules are defined in SPARK 2014 Reference Manual. They revolve around the three key notions of move, borrow and observe, which correspond respectively to the notions of move, mutable borrow and borrow in the Rust programming language. A brief introduction to the SPARK ownership policy is provided in the SPARK User’s Guide. With respect to the rules presented in SPARK RM, the initial support in GNATprove does not yet attempt to verify absence of memory leaks.
See also the blog post on Using Pointers in SPARK.
Allow SPARK_Mode Off Inside Subprograms¶
Aspect or pragma SPARK_Mode
is now allowed with the value Off
inside a subprogram, on a local package or subprogram spec/body. It is
particularly useful for instantiating a generic whose body is marked
SPARK_Mode Off
inside a subprogram. Here is a simple example of use, on
which GNATprove proves the postcondition of SPARK procedure Wrapper
using the postcondition of the non-SPARK local procedure Update_X
(which cannot be in SPARK because it uses attribute Access
, which
remains outside of the SPARK subset even with the new support for pointers):
procedure Wrapper (X : aliased out Integer) with
SPARK_Mode,
Post => X = 42
is
procedure Update_X with
Global => (Output => X),
Post => X = 42;
procedure Update_X with
SPARK_Mode => Off
is
A : access Integer := X'Access;
begin
A.all := 421;
end Update_X;
begin
Update_X;
end Wrapper;
Program Specification¶
Support for Volatile Variables to Prevent Compiler Optimizations¶
SPARK now supports volatile variables whose aim is not to interact with the
physical world, but simply to prevent compiler optimizations. Such variables
are used for example to defend against fault injections by duplicating the
guards to access a critical section of the code. This is now possible in SPARK
when the volatile variable is marked with aspect or pragma No_Caching
.
Here is an example of use to defend against fault injection attacks:
Cond : Boolean with Volatile, No_Caching := Some_Computation;
if not Cond then
return;
end if;
if not Cond then
return;
end if;
if Cond then
-- here do some critical work
end if;
Contracts Added to Ada Standard Library¶
Multiple units of the Ada Standard Library were enhanced with contracts
specifying their effects (using Abstract_State
on packages and
Global
on subprograms) and their functionality (using Pre
and
Post
on subprograms):
An abstract state
File_System
is declared inAda.Text_IO
to represent interactions between the program and a file system. The API ofAda.Text_IO
and its child packages has been enhanced to indicate where the file system is read or written. As a result, GNATprove no longer raises warnings about missing global contracts when using subprograms fromAda.Text_IO
. AdditionallyStatus_Error
andMode_Error
are modelled in preconditions and postconditions, leading to corresponding Verification Conditions on user code calling the API.String manipulation units
Ada.Strings.Fixed
,Ada.Strings.Bounded
andAda.Strings.Unbounded
have been enhanced with preconditions and postconditions, leading to corresponding Verification Conditions on user code calling the API.Subprograms from unit
Ada.Task_Identification
have been enhanced with preconditions, leading to corresponding Verification Conditions on user code calling the API.
Tool Automation¶
Improved Floating-Point Support in Alt-Ergo Prover¶
The Alt-Ergo prover that is shipped with GNATprove has been updated. It now
includes improved support for reasoning about computations that involve
floating point numbers. This enhancement may result in fewer unproved checks. To
benefit from the enhancement, a level higher than 0 should be selected via the
--level
switch, or the alt-ergo prover should be selected explicitly by
including it in the provers provided via the --prover
switch.
For an example of properties that become provable with this enhanced support, see the blog post on Floating-Point Computations in SPARK.
Precise Proof of Initial_Condition Across Units¶
When the proof of the Initial_Condition
for a unit depends on the
Initial_Condition
of another with’ed unit being satisfied, GNATprove
can now use the condition of the with’ed unit in the proof provided the
elaboration of this other unit is “known to precede” (as defined in SPARK RM
7.7(2)) the elaboration of the current unit.
Better Support for Recursive Functions¶
GNATprove now assumes the postcondition of recursive functions annotated with
Terminating
in more cases. In particular, it now assumes it for
functions called from non-mutually recursive subprograms, and so, even when the
function is called from a contract, while still preserving soundness.
Parallel Analysis of Subprograms¶
Subprograms in the same unit are now analyzed in parallel. This can lead to
speedups especially in the case of few large units with many subprograms, or
when analyzing a single unit during development. For example, analysis at level
2 of the example SPARKSkein distributed with GNATprove takes 3 minutes 36
seconds with SPARK Pro 19 and only 2 minutes 33 seconds with SPARK Pro 20,
using 4 cores at 2.4 GHz of an Intel Xeon CPU running Linux 64 bits (average
over two runs), for a decrease of 30 % in running time. As another example,
analysis at level 2 of the largest file enclave.adb
of example Tokeneer
distributed with GNATprove takes 50 seconds with SPARK Pro 19 and
only 23 seconds with SPARK Pro 20, using 8 cores at 2.4 GHz of an Intel Xeon
CPU running Linux 64 bits (average over three runs), for a decrease of 54 % in
running time.
Tool Interaction¶
Better Messages From Flow Analysis¶
GNATprove now emits info messages “data dependencies proved” and “flow
dependencies proved” respectively for every Global
and Depends
contract that have been verified.
GNATprove now emits either a check on each access to a possibly uninitialized object, or a single info message on the object’s declaration when all accesses happen after the object has been initialized. Previously GNATprove could emit both info messages and checks, which was confusing, especially for arrays and objects accessed from different subprograms.
Summary Table Now Lists All Check Messages¶
Now all checks verified by GNATprove are accounted for in the summary
table printed at the top of the log file gnatprove.out
, whether the check
comes from flow analysis or from proof. New categories of checks have been
added:
“Data Dependencies” for
Global
contracts“Flow Dependencies” for
Depends
contracts“Termination” for subprogram termination
“Concurrency” for concurrency-related checks
Note that the categories “Run-time Checks” and “Termination” may contain checks from both flow analysis and proof. Here is an example of summary table generated for the Tokeneer example distributed with GNATprove:
-----------------------------------------------------------------------------------------------------------------------------
SPARK Analysis results Total Flow Interval CodePeer Provers Justified Unproved
-----------------------------------------------------------------------------------------------------------------------------
Data Dependencies 281 281 . . . . .
Flow Dependencies 228 228 . . . . .
Initialization 693 692 . . . 1 .
Non-Aliasing . . . . . . .
Run-time Checks 474 . . . 458 (CVC4 95%, Trivial 5%) 16 .
Assertions 45 . . . 45 (CVC4 82%, Trivial 18%) . .
Functional Contracts 304 . . . 302 (CVC4 82%, Trivial 18%) 2 .
LSP Verification . . . . . . .
Termination . . . . . . .
Concurrency . . . . . . .
-----------------------------------------------------------------------------------------------------------------------------
Total 2025 1201 (59%) . . 805 (40%) 19 (1%) .
Note the use of “Trivial” prover to denote checks proved by GNATprove without calling any automatic prover.
Dead Code Detected by Proof Warnings¶
The switch --proof-warnings
which was introduced in SPARK Pro 19 to detect
inconsistencies now triggers detection of dead code after branches in the
program (in if-statements, case-statements and loops) where previously only
dead code after loops was detected. Unreachable branches in all expressions are
also detected where previously this was restricted to expressions inside
assertions and contracts. For example, GNATprove now issues the following
messages:
dead.adb:6:18: warning: unreachable branch
dead.adb:8:12: warning: unreachable code
dead.adb:13:09: warning: unreachable code
when run with switch --proof-warnings
on the following code:
1procedure Dead (X : Integer; R : out Boolean) with SPARK_Mode is
2 Y : Natural := abs (X / 2);
3begin
4 if X < Y then
5 if X in 1 .. 100
6 and then Y > 42
7 then
8 R := True;
9 end if;
10 elsif X >= 0 then
11 R := True;
12 else
13 R := False;
14 end if;
15end Dead;
Decrease Occurrences of Spurious Counterexamples¶
Counterexamples displayed by GNATprove when a check is not proved are best efforts by the underlying provers, which may turn out to be spurious in some cases. This was often the case for counterexamples of “all zeroes”, where each variable gets a value of zero (or the equivalent enumeration value for enumerated types). These counterexamples are not presented to the user anymore.
Unproved Parts of Preconditions Identified¶
When the precondition of a call is unproved, GNATprove can now identify the part of the precondition which was not proved. This feature was already available for other assertion types, but not for preconditions. For example, GNATprove now issues the following messages:
context.adb:8:07: medium: precondition might fail, cannot prove X > 0
context.adb:9:07: medium: precondition might fail, cannot prove X > Y
context.adb:10:07: medium: precondition might fail, cannot prove Y < 100
when run on the following code:
1package Context
2 with SPARK_Mode
3is
4 procedure Do_Action (X, Y : Integer) with
5 Global => null,
6 Pre => X > 0 and then X > Y and then Y < 100;
7
8 procedure Call_Action;
9
10end Context;
1package body Context
2 with SPARK_Mode
3is
4 procedure Do_Action (X, Y : Integer) is null;
5
6 procedure Call_Action is
7 begin
8 Do_Action (-1, -2);
9 Do_Action (42, 99);
10 Do_Action (1000, 100);
11 end Call_Action;
12
13end Context;
Tool Usability¶
Automatic Target Configuration for GNAT Runtimes¶
If the runtime used for a project analyzed with GNATprove has a target
configuration file (this is the case for recent GNAT runtimes), GNATprove can
use this file automatically to configure the analysis for the target and
runtime. In that case, manual target configuration via the -gnateT
switch
is not necessary anymore. The project file needs to specify attributes
Target
and Runtime
, see the SPARK User’s Guide
for more details.
Better Warnings on Useless Code¶
GNATprove no longer emits warnings about statements having no effect for assignments to objects whose name contains one of the substrings DISCARD, DUMMY, IGNORE, JUNK, UNUSED in any casing. Similar warnings were already suppressed when compiling the code with GNAT; now they are also suppressed when analyzing the code with GNATprove.
GNATprove now emits warnings about ineffective statements in ghost subprograms. Previously such warnings were only emitted for non-ghost subprograms.
GNATprove Now Defines GPR_TOOL
Variable¶
The GPR_TOOL
variable is set by various AdaCore tools and can be used
to define tool-specific values of variables in the project file. GNATprove now
also sets this variable; it is set to the value “gnatprove”. See the SPARK
User’s Guide
for an example of use.
Ability to Specify File-Specific Switches¶
A subset of GNATprove switches can now be specified for specific files of a
project, typically to adjust the proof effort (prover timeout, steps and memory
limit). To this end, a new project file attribute Proof_Switches
has
been introduced. It can be used in this way:
package Prove is
for Proof_Switches ("Ada") use ("--report=all");
for Proof_Switches ("file.adb") use ("--timeout=10");
end Prove;
The existing Switches
attribute is now deprecated and
Proof_Switches
should be used instead. More information about these
attributes can be found in the SPARK User’s Guide.
New Switch --prover=all
¶
The existing switch --prover
of SPARK now accepts the special string
all
, which is equivalent to the provers cvc4, z3 and alt-ergo for SPARK
Pro, and equivalent to alt-ergo for SPARK Discovery.