Prove Annotations with WP

WP refers both to a method to formally verify properties of the analyzed code and the name of the analyzer’s plug-in that implements this method. WP is a static analysis technique, like the value analysis, but involving theorem proving. For a short introduction describing how it works see Short Introduction to WP Computation.

The purpose of this chapter is mainly to explain in which cases WP can be used with a minimal amount of manual work required. This does not mean that it cannot be used in more complex situations, but then it requires more knowledge about the WP computation and/or competences in performing manual proofs using proof assistants such as Coq.

How to Run WP

The easiest way to run WP is to do it in the GUI by selecting the annotation to prove, right-clicking to open the pop-up menu, and choosing the Prove Property by WP option.

However, when the analysis evolves, it is usually more practical to run WP from the command line, save the project, and extract the status of the properties from the information file to just check that the results are still the same.

The command line to run WP and save the project looks like:

tis-analyzer -load project.state -wp-fct f1 -wp-prop f1_p1_wp, f1_p2_wp \
                           -then -wp-fct g,h -wp-prop f_pre_wp \
                           ...
                           -then -save project.wp.state

This command line:

  • opens a previously saved project project.state: it doesn’t need to include value analysis results, and even doesn’t have to include an entry point. All it needs is the body of the functions where the properties to verify are, and probably some specifications for the functions called from these functions.

  • tries to verify the properties named f1_p1_wp and f1_p2_wp in the f1 function,

  • then tries to verify the property f_pre in g and h.

    Notice that f_pre is supposed to be a precondition of f, and that it is checked in g and h which are supposed to be some of f callers;

  • saves the results in the project.wp.state project.

Notice that a _wp suffix is used in the names of the properties that are checked with WP. See Naming the Annotations to understand why naming conventions are useful.

This is an example of how to use WP, but the plug-in provides many other options if needed. Please use the -wp-help option to list them, and refer to the documentation for more details.

To know how to extract the status of the properties from the project.wp.state project, see Information about the Properties.

Short Introduction to WP Computation

Let us give very simple explanations about WP for the one that knows nothing about it, because it might be necessary to understand how it works in order to use it when suitable.

To verify that a property is true at a program point, the WP principle is to propagate it backward and to compute a formula that is such that, if it can be proved to be true, then it ensures that the initial property is true as well. The computed formula is then sent to some automatic prover(s). For instance, tis-analyzer comes with alt-ergo, but more provers can be added.

An example is easier to understand:

const int X = 10;

void f1(int x)
{
    int y = x + 1;
    int z = 2 * y;
L:  //@ assert y_val: y > X;
    ...
}

To ensure that y_val is true at L, WP computes that one have to prove that (x+1 > X) when entering the function. Notice that the z assignment has no effect since WP knows that it doesn’t modify y value. This can be automatically proved if a precondition gives:

//@ requires r_x_ge_X: x >= X;

This is because the final computed formula is:

x >= X ==> x+1 > X;

which is easily proved by any automatic prover.

It doesn’t work with the precondition:

//@ requires r_x_ge_15: x >= 15;

This is because WP only works on the function source code, which means that it has no information about the value of X. To solve this kind of problem, one can add:

//@ requires r_X_val: X == 10;

This precondition is easily validated by the value analysis and can be used by WP to finished the proof with r_x_ge_15.

In this simple case, the initial property and the computed formula are equivalent, but it is not always the case. WP just ensures that if the computed formula is true, then the property is true each time its program point is reached.

WP on Loops

To prove a loop invariant property, the WP computation is very similar, but decomposed into two goals:

  • establishment: the property must be true when reaching the loop. This is similar to an assert before the loop.
  • preservation: if the property is true at the beginning of an iteration, it is still true at the end.

Example:

//@ requires n < 100;
int main(int n)
{
    int i; int * p;
    for (i = 0, p = T; i < n; i++, p++) {
        *p = 3;
    }
    ...
}

The following property remove the alarm about the validity of the (*p) assignment in the loop:

//@ loop invariant li_1: p == T+i;

Moreover it can be proved by WP:

  • the establishment has to be proved before entering the loop, but after the initialization part. So the proof obligation is:

    T == T + 0
    
  • the preservation formula is similar to:

    p == T + i  ==>  p + 1 == T + (i + 1)
    

Both formula are trivially true.

WP for Indirect Memory Access

In the first example in Short Introduction to WP Computation, the z assignment has no effect on the WP computation since WP knows that it doesn’t modify y value. But it is different when pointers are involved. For instance:

void f(int * px, int x, int * py, int y)
{
    *px = x;
    *py = y;
    //@ assert a_px: *px == x;
    //@ assert a_py: *py == y;
    ...
}

WP is able to prove a_py, but not to prove a_px. The reason is that it doesn’t know whether the assignment to (*py) modifies (*px) value or not. The a_px can be proved only with the precondition:

//@ requires \separated (px, py);

It tells that there is no intersection between (*px) and (*py) locations in the memory.

In the context of adding annotations to remove alarms, except in very simple cases, it is not recommended to use WP when possibly overlapping pointers are involved since it may take some time to provide enough information.

WP for a Function Call

The other problem is when there are some function calls between the property and the statements that makes it true. Remember that WP only work on the source code of the property function, and on the specifications of the called functions.

extern int X;
void g (void);
void f(int x, int y)
{
    if (x > y && x > X) {
        g ();
        //@ assert ax1: x > y;
        //@ assert ax2: x > X;
        ...
    }
    ...
}

WP is able to prove ax1 since there is no way for g to modify either x or y, but ax2 cannot be proved since g may modify X.

There are two solutions to solve the problem:

  • add an assigns property for g to specify the modified data.

    For instance, ax2 is proved when adding:

    //@ assigns \nothing;
    

    This is not the preferred method since assigns are difficult to prove: it requires to know the modified data for each statement of g. The computed dependencies may help to justify the assigns property, but beware that this information is context dependent.

  • add a postcondition about the involved data. For instance:

    • specifying that X is not modified by g:

      //@ ensures X == \old (X);
      
    • or specifying that X decrease:

      //@ ensures X < \old (X);
      

Both solutions enable to prove ax2.

WP is Useful Even for Trivial Properties

The WP could seem useless if not used in complex cases, but it is not true: even when properties look trivial, it is useful to formally prove them, since it is so easy to make a mistake.

Let us look at an example:

//@ ensures e_res_ok: min <= \result <= max;
int bounds(int min, int x, int max)
{
    int res = x;
    if (x < min) res = min;
    if (x > max) res = max;
    return res;
}

The postcondition seems reasonably easy to justify, but WP is unable to prove it. WP computes a proof obligation equivalent to:

if (x > max)      then min <= max /\ max <= max
else if (x < min) then min <= min /\ min <= max
     else              min <= x   /\   x <= max

After simplifying the formula, it appears that the information (min <= max) is missing, so this postcondition cannot be proved without a precondition. It then has to be added and checked in every context where the function is called to ensure that the post-condition is verified.

WP Conclusion

The advice here is to use WP only in simple cases because complex cases needs expertise and require a lot of time. But we have seen that even for properties that look trivial, it is better to formally prove them, since it is so easy to make a mistake. Moreover, manual justification of trivial properties may look a little silly.

One must be especially careful when it seems that WP should be able to prove something, and doesn’t, since it may hide a problem somewhere. It is always better to understand if it is really a WP weakness, or something else.