SPARK 20 Release Notes ====================== We present here a few highlights of the new features in SPARK 20. You can access the complete list `here `__. .. contents:: :local: 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 :code:`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 :code:`SPARK_Mode` is now allowed with the value :code:`Off` inside a subprogram, on a local package or subprogram spec/body. It is particularly useful for instantiating a generic whose body is marked :code:`SPARK_Mode Off` inside a subprogram. Here is a simple example of use, on which GNATprove proves the postcondition of SPARK procedure :code:`Wrapper` using the postcondition of the non-SPARK local procedure :code:`Update_X` (which cannot be in SPARK because it uses attribute :code:`Access`, which remains outside of the SPARK subset even with the new support for pointers): .. code-block:: ada 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 :code:`No_Caching`. Here is an example of use to defend against fault injection attacks: .. code-block:: ada 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 :code:`Abstract_State` on packages and :code:`Global` on subprograms) and their functionality (using :code:`Pre` and :code:`Post` on subprograms): * An abstract state :code:`File_System` is declared in :code:`Ada.Text_IO` to represent interactions between the program and a file system. The API of :code:`Ada.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 from :code:`Ada.Text_IO`. Additionally :code:`Status_Error` and :code:`Mode_Error` are modelled in preconditions and postconditions, leading to corresponding Verification Conditions on user code calling the API. * String manipulation units :code:`Ada.Strings.Fixed`, :code:`Ada.Strings.Bounded` and :code:`Ada.Strings.Unbounded` have been enhanced with preconditions and postconditions, leading to corresponding Verification Conditions on user code calling the API. * Subprograms from unit :code:`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 :code:`Initial_Condition` for a unit depends on the :code:`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 :code:`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 :code:`Global` and :code:`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 :code:`Global` contracts * "Flow Dependencies" for :code:`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: .. code-block:: ada :linenos: procedure Dead (X : Integer; R : out Boolean) with SPARK_Mode is Y : Natural := abs (X / 2); begin if X < Y then if X in 1 .. 100 and then Y > 42 then R := True; end if; elsif X >= 0 then R := True; else R := False; end if; end 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: .. code-block:: ada :linenos: package Context with SPARK_Mode is procedure Do_Action (X, Y : Integer) with Global => null, Pre => X > 0 and then X > Y and then Y < 100; procedure Call_Action; end Context; .. code-block:: ada :linenos: package body Context with SPARK_Mode is procedure Do_Action (X, Y : Integer) is null; procedure Call_Action is begin Do_Action (-1, -2); Do_Action (42, 99); Do_Action (1000, 100); end Call_Action; end 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 :code:`Target` and :code:`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 :code:`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 :code:`Proof_Switches` has been introduced. It can be used in this way: .. code-block:: ada package Prove is for Proof_Switches ("Ada") use ("--report=all"); for Proof_Switches ("file.adb") use ("--timeout=10"); end Prove; The existing :code:`Switches` attribute is now deprecated and :code:`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.