AdaCore Blog

SPARK 2014 Flow Analysis

by Florian Schanda –

We have nearly finished implementing a central component of the SPARK 2014 analysis tools: the flow analysis engine; so this is a good time to introduce some of the analysis it will carry out. Broadly speaking it has two objectives.

  • Flow analysis detects dubious source constructs, for example the use of uninitialised variables or ineffective statements, and
  • it checks and enforces the correctness of the global and depends aspects.

Checking for dubious constructs

Perhaps the most important aspect of flow analysis is to check for some questionable constructs. One in particular affects the soundness of proof: the use of uninitialised variables. Lets assume we have a record with a few fields:

record R is
      X, Y, Z : Boolean;
   end record;

Then the following code will raise flow errors:

is
      Foo : R;
   begin
      Foo.X := False;
      Foo.Z := Is_Prime (17);

      Do_Stuff (Foo);  --  error: use of uninitialized component Foo.Y
   end

Another construct flow analysis will flag up is that of an ineffective assignment. Consider the following code where the first write to x is completely masked by the subsequent writes:

is
      x := 12;        --  ineffective assignment to x
      if y > 0 then
         x := y;
      else
         x := 0;
      end if;
   end

Checking contracts

SPARK 2014 introduces two kinds of contracts that state which variables are used by functions and procedures in the computation of their outputs. Flow analysis makes sure that code does not violate these contracts.

First up the global contract: this can be used to make use of global variables explicit. For example:

function Wibble (...) return Integer
     with Global => (Input => Some_State);  --  we read the global Some_State

Flow analysis will make sure that function Wibble will only read from and never updates Some_State, but also that it makes no use of any other global variables. Not only is this invaluable for documentation purposes (reading this spec is much more helpful than reading one without a global contract), it also makes the analysis of subprogram calling Wibble precise (as opposed to a worst-case assumption).

The other contract flow analysis checks is the depends aspect. This can be used to express constraints on data-flow and control-flow. For example:

procedure Do_Stuff (X : in out Integer;
                       Y :    out Integer)
     with Depends => (X => X,  --  Read as "X depends on X"
                      Y => X)  --  Read as "Y depends on X"
   is
   begin
      X := X - 1;      --  x depends on itself
      Y := 1;          --  y depends on nothing

      if X > 0 then    --  the early return will make any code
         return;       --    following have a control dependence
      end if;          --    on x

      Y := 0;          --  thus y here depends on x
   end Do_Stuff;

The depends contract can be useful as documentation, to express intent, or to verify that some data never flows into some variables:

procedure Do_Things (X, Y, Z : Integer)
     with Depends =>
       (Top_Secret_Stuff   => (Top_Secret_Stuff, Unclassified_Stuff, X, Y),
        Unclassified_Stuff => (Unclassified_Stuff, X, Z));

Here we can see that the top secret data is never used to compute the unclassified data, not even indirectly through control dependence.

As the "and from itself" dependency is quite common there is a shorthand notation for that too; the above can be rewritten as follows:

procedure Do_Things (X, Y, Z : Integer)
     with Depends =>
       (Top_Secret_Stuff   =>+ (Unclassified_Stuff, X, Y),
        Unclassified_Stuff =>+ (X, Z));

Posted in #Language    #SPARK   

About Florian Schanda