In SPARK, data-flow analysis performs 2 steps: (1) verifying the user-defined data-flow contracts (e.g. Global / Depends) and (2) generating them when they are missing.

Accurate data-flow analysis is a necessary prerequisite for proof of absence of run-time-errors (AoRTE) checks.

SPARK 2005 only did the first step (assuming null global data in the absence of user-defined global contracts). The second step, generation, is useful for users that want to get the benefits of flow-analysis, including proven AoRTE, without bothering to annotate their code with contracts.

However, the global contracts that get generated may not meet expectations / requirements. For example, you may write to a variable that should only be read from. In this case, flow analysis and AoRTE proof could pass, but your code would not meet its requirements.

So there is a need to see what global contracts SPARK generates.

The generated global contracts were previously hidden from the user. They could be exposed with the switch --flow-show-gg, but then SPARK would output the generated global contracts to the console, which made them hard to utilise effectively.

In the integrated development environment, GNAT Studio, there is now a plugin that inserts the generated global contracts inline with the code.

The GNAT Studio contextual menu

Here, we have a screenshot of some Ada source code being edited in GNAT Studio. The code uses two globals, G1 and G2. Function Potato reads both. Function Kitty reads G1.

The user has right-clicked to select the new plugin, “Show generated Global contracts”.

Once the user clicks “Show generated Global contracts”, the generated global contracts get inserted into the editor window, so that the user can see what SPARK data-flow analysis detects as globals.

The user can then inspect the globals, and if they wish, copy-paste from this into their code, to add contracts. From this point, they can check whether the system fulfills global data-flow requirements.

We see this as a great learning tool for beginners to SPARK.

Tokeneer

Let’s test the plugin on the Tokeneer project - a codebase that makes extensive use of Globals. Tokeneer has been fully verified in SPARK, and has a comprehensive set of user-written Global contracts, so we need to hide these contracts from our plugin by adding the following directives to the file we want to test:

pragma Ignore_Pragma (Global);
pragma Ignore_Pragma (Refined_Global);
pragma Ignore_Pragma (Depends);
pragma Ignore_Pragma (Refined_Depends);

This will allow us to compare the user-written Global contracts with the ones displayed by our plugin.

The results:

File enclave.adb has a procedure named ValidateAdminToken:

We can see that the user-supplied Global contract (white background) closely matches the generated one (grey background). GNATprove has resolved Output => Status conservatively as In_Out => Enclave.Status. The plugin correctly summarises the effect on individual variables by the aggregated effect on the corresponding abstract state, when the variables belong to one.

We chose to prefix Global variable names with their full path, even when they are inside the current program unit. We decided to do this to disambiguate in such situations where we have two different variables sharing the same name, for example where we have Global variable X in package Outer, and Global variable X in package Inner, with Inner nested inside Outer:

Coming back to the Tokeneer code, we also ran the plugin on file keystore.adb, which has a function named GetBlock:

The plugin has correctly identified that there is no Global state. It’s useful to annotate this function with Global => null, so that we know it is not modifying any Global state.

We’d love to know how you use this feature and if you see any useful enhancements. One feature we could add is the ability to automatically insert a generated contract in the code if the user wishes so.