TrustInSoft Analyzer Documentation¶

Analyzing the source code¶

Let’s have a look at the program example3.c, located in the /home/tis/1.42/C_Examples/TutorialExamples directory:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32

/* TrustInSoft Analyzer Tutorial - Example 3 */
#include <stdio.h>

#include <stdlib.h>
#include <stdio.h>
#include <stdint.h>
#include <inttypes.h>

int main(void)
{
    char *p, *q;
    uintptr_t pv, qv;
    {
        char a = 3;
        p = &a;
        pv = (uintptr_t)p;
    }
    {
        char b = 4;
        q = &b;
        qv = (uintptr_t)q;
    }
    printf("Roses are red,\nViolets are blue,\n");
    if (p == q)
        printf("This poem is lame,\nIt doesn't even rhyme.\n");
    else {
        printf("%p is different from %p\n", (void *)p, (void *)q);
        printf("%" PRIxPTR " is not the same as %" PRIxPTR "\n", pv, qv);
    }

    return 0;
}

This program prints out some text. The result should differ depending on the value of the expression p == q in line 24.

Start the value analysis with the following command:

$ tis-analyzer-gui -val -slevel 100 /home/tis/1.42/C_Examples/TutorialExamples/example3.c

and launch the GUI (as explained in the Getting Started section).

After selecting the Properties widget and the Only alarms button, you will notice that there is one alarm and some lines of dead code right after the alarm:

The assertion generated shows that the analyzer has found a dangling pointer (a pointer not pointing to a valid object):

/*@ assert Value: dangling_pointer: ¬\dangling(&p); */

Let’s use the analyzer to follow the variable p through the execution, and try to find the source of the problem:

The values of the variable p before and after the selected statement will be listed in the Values widget in the bottom panel. We can see that, after the initialization p = &a, the variable p holds the address of a as expected.

Selecting the expression p == q inside the if will show the value of p at this point in the program. Before the evaluation of the p == q expression p is shown as ESCAPINGADDR, meaning that it does not hold the address of a valid object anymore.

The reason is quite simple: p holds the address of the local variable a, whose lifetime is limited to the block in which the variable is defined:

{
    char a = 3;
    p = &a;
    pv = (uintptr_t) p;
}

The pointer p refers to the variable a outside of its lifetime, resulting in undefined behavior. As every execution path results in an undefined behavior, the analysis stops.

The problem: undefined behavior¶

When the behavior of a program is undefined, it means that anything can happen at execution time. Some programmers seem to think that, at least in some cases, this is not a big issue: they are certainly wrong. A program invoking undefined behavior is a time bomb.

A dangling pointer is an example of undefined behavior. Let’s illustrate its consequences on our example.

First we compile the program with gcc:

$ gcc -Wall -Wextra -Wpedantic /home/tis/1.42/C_Examples/TutorialExamples/example3.c -o example3

and notice that, despite all of our efforts, gcc does not issue any warnings.

Running the code will display the following text:

$./example3
Roses are red,
Violets are blue,
This poem is lame,
It doesn't even rhyme.

meaning that the condition p == q evaluated to true. This can happen if the variables a and b were allocated at the same address by the compiler (which is possible since they are never in scope at the same time).

Using different compilation options should not affect the behavior of the program, but compiling with a -O2 switch and running the program results in a different output:

$ gcc -Wall -Wextra -Wpedantic -O2 /home/tis/1.42/C_Examples/TutorialExamples/example3.c -o example3_opt

$./example3_opt
Roses are red,
Violets are blue,
0x7ffc9224f27e is different from 0x7ffc9224f27f
7ffc9224f27e is not the same as 7ffc9224f27f

This time the expression p == q evaluated to false because the variables a and b were allocated to different addresses. So changing the optimization level changed the behavior of our program.

In the aforementioned post you can see evidence of a third, very weird behavior, in which p == q evaluates to false, even though a and b are allocated to the same address.

The conclusion is clear, and we will state it as a general warning:

The solution: TrustInSoft Analyzer¶

We have already seen how TrustInSoft Analyzer is able to find dangling pointers and other weaknesses. We will continue the analysis and correct the code in order to guarantee that there are no problems left.

To avoid the dangling pointer problem, we will define a outside the block, so that its storage and address are guaranteed by the standard throughout the whole main function:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

//TrustInSoft Analyzer Tutorial - Example 3_1
#include <stdio.h>

#include <stdlib.h>
#include <stdio.h>
#include <stdint.h>
#include <inttypes.h>

int main(void)
{
    char *p, *q;
    uintptr_t pv, qv;
    char a = 3;
    {
        p = &a;
        pv = (uintptr_t)p;
    }
    {
        char b = 4;
        q = &b;
        qv = (uintptr_t)q;
    }
    printf("Roses are red,\nViolets are blue,\n");
    if (p == q)
        printf("This poem is lame,\nIt doesn't even rhyme.\n");
    else {
        printf("%p is different from %p\n", (void *)p, (void *)q);
        printf("%" PRIxPTR " is not the same as %" PRIxPTR "\n", pv, qv);
    }
}

and launch the value analysis again:

$ tis-analyzer-gui -val -slevel 100 /home/tis/1.42/C_Examples/TutorialExamples/example3_1.c

We notice that the dangling pointer alarm regarding p has been replaced by the same alarm about q. When evaluating the expression p == q the analyzer noticed a problem with the term p and stopped the analysis, so it did not get a chance to issue the alarm about q. Now that we corrected the first problem, the analyzer gets to the term q and raises the same kind of alarm.

Selecting the variables p and q in the Values widget tab and clicking on the p == q expression will show that, before evaluation, p holds the address of a whereas q has the value ESCAPINGADDR. This means that q is a dangling pointer, as it references the address of the out-of-scope variable b:

To correct the problem we will simply define b outside the block, as we did before with a:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

//TrustInSoft Analyzer Tutorial - Example 3_ok
#include <stdio.h>

#include <stdlib.h>
#include <stdio.h>
#include <stdint.h>
#include <inttypes.h>

int main(void)
{
    char *p, *q;
    uintptr_t pv, qv;
    char a = 3;
    char b = 4;
    {
        p = &a;
        pv = (uintptr_t)p;
    }
    {
        q = &b;
        qv = (uintptr_t)q;
    }
    printf("Roses are red,\nViolets are blue,\n");
    if (p == q)
        printf("This poem is lame,\nIt doesn't even rhyme.\n");
    else {
        printf("%p is different from %p\n", (void *)p, (void *)q);
        printf("%" PRIxPTR " is not the same as %" PRIxPTR "\n", pv, qv);
    }
}

and launch the analyzer one more time to verify that there are no other alarms:

$ tis-analyzer-gui -val -slevel 100 /home/tis/1.42/C_Examples/TutorialExamples/example3_ok.c

Notice that the

printf("This poem is lame,\nIt doesn\'t even rhyme.\n");

code is marked as dead. Indeed the variables a and b need to be allocated to different addresses, as they are in scope at the same time. As a consequence, the condition p == q evaluates always to false, so the first branch of the if statement will never be executed.

Congratulations! You have successfully corrected all the bugs in example3.c. The program is now guaranteed not to be subject to any of the weaknesses covered by TrustInSoft Analyzer.

Exploring the source code¶

Unlike our previous examples, the Skein implementation is composed of multiple files. All the files needed for this tutorial are located in the /home/tis/1.42/C_Examples/skein_verification directory.

Let’ start by listing all the files in the directory:

$ ls -l /home/tis/1.42/C_Examples/skein_verification

total 124
-rw-rw-r-- 1 tis tis   204 Oct  5 18:54 README
-rwxrwxr-x 1 tis tis  4984 Oct  5 18:54 SHA3api_ref.c
-rwxrwxr-x 1 tis tis  2001 Oct  5 18:54 SHA3api_ref.h
-rwxrwxr-x 1 tis tis  6141 Oct  5 18:54 brg_endian.h
-rwxrwxr-x 1 tis tis  6921 Oct  5 18:54 brg_types.h
-rw-rw-r-- 1 tis tis   524 Oct  5 18:54 main.c
-rwxrwxr-x 1 tis tis 34990 Oct  5 18:54 skein.c
-rwxrwxr-x 1 tis tis 16290 Oct  5 18:54 skein.h
-rwxrwxr-x 1 tis tis 18548 Oct  5 18:54 skein_block.c
-rwxrwxr-x 1 tis tis  7807 Oct  5 18:54 skein_debug.c
-rwxrwxr-x 1 tis tis  2646 Oct  5 18:54 skein_debug.h
-rwxrwxr-x 1 tis tis  1688 Oct  5 18:54 skein_port.h

The skein.h file is a good starting point to explore the API. We will focus our attention on the following lines of code:

typedef struct
    {
    size_t  hashBitLen;                      /* size of hash result, in bits */
    size_t  bCnt;                            /* current byte count in buffer b[] */
    u64b_t  T[SKEIN_MODIFIER_WORDS];         /* tweak words: T[0]=byte cnt, T[1]=flags */
    } Skein_Ctxt_Hdr_t;

typedef struct                               /*  256-bit Skein hash context structure */
    {
    Skein_Ctxt_Hdr_t h;                      /* common header context variables */
    u64b_t  X[SKEIN_256_STATE_WORDS];        /* chaining variables */
    u08b_t  b[SKEIN_256_BLOCK_BYTES];        /* partial block buffer (8-byte aligned) */
    } Skein_256_Ctxt_t;

typedef struct                               /*  512-bit Skein hash context structure */
    {
    Skein_Ctxt_Hdr_t h;                      /* common header context variables */
    u64b_t  X[SKEIN_512_STATE_WORDS];        /* chaining variables */
    u08b_t  b[SKEIN_512_BLOCK_BYTES];        /* partial block buffer (8-byte aligned) */
    } Skein_512_Ctxt_t;

typedef struct                               /* 1024-bit Skein hash context structure */
    {
    Skein_Ctxt_Hdr_t h;                      /* common header context variables */
    u64b_t  X[SKEIN1024_STATE_WORDS];        /* chaining variables */
    u08b_t  b[SKEIN1024_BLOCK_BYTES];        /* partial block buffer (8-byte aligned) */
    } Skein1024_Ctxt_t;

/*   Skein APIs for (incremental) "straight hashing" */
int  Skein_256_Init  (Skein_256_Ctxt_t *ctx, size_t hashBitLen);
int  Skein_512_Init  (Skein_512_Ctxt_t *ctx, size_t hashBitLen);
int  Skein1024_Init  (Skein1024_Ctxt_t *ctx, size_t hashBitLen);

int  Skein_256_Update(Skein_256_Ctxt_t *ctx, const u08b_t *msg, size_t msgByteCnt);
int  Skein_512_Update(Skein_512_Ctxt_t *ctx, const u08b_t *msg, size_t msgByteCnt);
int  Skein1024_Update(Skein1024_Ctxt_t *ctx, const u08b_t *msg, size_t msgByteCnt);

int  Skein_256_Final (Skein_256_Ctxt_t *ctx, u08b_t * hashVal);
int  Skein_512_Final (Skein_512_Ctxt_t *ctx, u08b_t * hashVal);
int  Skein1024_Final (Skein1024_Ctxt_t *ctx, u08b_t * hashVal);

It seems that, in order to hash a message, we’ll need to:

• declare a variable of type Skein_256_Ctxt_t;
• initialize it using the function Skein_256_Init;
• pass Skein_256_Update a representation of the string;
• call Skein_256_Final with the address of a buffer in order to write the hash value.

Writing a test driver¶

When confronted with the analysis of an application, the usual entry point for the analysis is its main function. Nonetheless, there are many contexts in which there will not be an obvious entry-point, for example when dealing with a library. In those cases, you will need to write a driver to test the code, or better, leverage existing tests in order to exercise the code.

As the Skein implementation includes no tests, we provide the file main.c as a test driver. It implements the steps outlined above in order to hash the message "People of Earth, your attention, please":

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23

/* Test driver for Skein hash function */
#include "skein.h"
#include "stdio.h"

#define HASHLEN (8)
u08b_t msg[80] = "People of Earth, your attention, please";

int main(void)
{
    u08b_t hash[HASHLEN];
    int i;

    Skein_256_Ctxt_t skein_context;

    Skein_256_Init(&skein_context, HASHLEN);
    Skein_256_Update(&skein_context, msg, 80);
    Skein_256_Final(&skein_context, hash);

    for (i = 0; i < HASHLEN; i++)
        printf("%d\n", hash[i]);

    return 0;
}

The driver also prints the contents of the hashed message in the for loop at the end of the file. Each of the printed values corresponds to the numerical value of the corresponding character in the hashed message.

We compile and run the code by executing the command:

$ gcc /home/tis/1.42/C_Examples/skein_verification/*.c && ./a.out

and get the following output:

215
78
61
246
0
0
0
0

A first value analysis¶

We will start by launching a simple value analysis with the following command:

$ tis-analyzer-gui -64 -val /home/tis/1.42/C_Examples/skein_verification/*.c

Next, we will launch the GUI by opening the link or pointing the browser to http://localhost:8080 (the port number may change if you have other analysis running at the same time).

Once you have opened the GUI, go to the Properties widget and click on the only alarms button:

In the Properties widget we can see that there are about 20 alarms.

As the analyzer is not precise enough, we will start by improving the precision of the analysis in order to reduce the number alarms. We will show how to do this in the next part of this tutorial.

Please click here to continue the tutorial.

Increasing the precision¶

A first step to improve the precision of the analysis is to activate the -slevel option. We will try to launch the analysis with an slevel value of 100 and see if there are any improvements:

$ tis-analyzer-gui -64 -val -slevel 100 /home/tis/1.42/C_Examples/skein_verification/*.c

We open the GUI again

and notice that there is only one alarm left, so all the other alarms were false alarms.

Investigating the alarms¶

With only one alarm left, we can investigate its cause to see if it is a true positive or not.

Notice that there is some dead code that cannot be reached by any execution. In particular, this function never terminates because the return statement cannot be reached.

This means that the execution never leaves the for loop in line 19:

    for (i = 0; i < HASHLEN; i++)
        printf("%d\n", hash[i]);

Clicking on the alarm in the Properties widget, we see that the alarm occurs indeed inside the loop. The annotation generated by the analyzer is:

/*@ assert Value: initialisation: \initialized(&hash[i]); */

meaning that we are trying to read a value that might not be properly initialized.

Let’s explore the values inside the hash array by going to the Values widget and clicking on the hash term in the Interactive Code Window.

By clicking on the values in the before column of the Values widget,

you will have a more readable output of the contents of the hash array:

[0] ∈ {215}
[1..7] ∈ UNINITIALIZED
This begins like: "�"

The analyzer is telling us that, before entering the loop, hash[0] contains the value 215 (which it tries to interpret as a character, which gives the This begins like: "�") and all the other items in the array are UNINITIALIZED.

Reading an uninitialized value is an undefined behavior, and that is exactly what the program is doing when trying to read past the first element of the array. The analysis stops here as all the execution paths lead to undefined behavior.

It seems that the alarm is indeed a true positive, so we cannot go further in the analysis without correcting the problem.

Finding and correcting the bug¶

As we have uninitialized values in the array, let’s have a look at the initialization function Skein_256_Init.

You can navigate to the definition of the function by right clicking on the function name:

This will update the Interactive Code Window with the code of the function:

After clicking on the hashBitLen variable, we can see in the Properties widget that its value is always 8.

This value corresponds to the value of the HASHLEN macro that is passed to Skein_256_Init function in line 15 of the original code:

    Skein_256_Init(&skein_context, HASHLEN);

Note that in the Interactive Code Window this macro has been expanded to 8.

So the length of the hash is expressed in bits, and we were inadvertently asking for an 8 bit hash. This explains why only the first element of the array was initialized.

As we wanted an 8 byte hash, we can correct the problem by multiplying the value by 8 in the call to Skein_256_Init, modifying line 15 of the main.c file to look like this:

    Skein_256_Init(&skein_context, 8 * HASHLEN);

After saving the changes we run TrustInSoft Analyzer again:

$ tis-analyzer-gui -64 -val -slevel 100 /home/tis/1.42/C_Examples/skein_verification/*.c

and open the GUI:

Congratulations! There are no more alarms, so our program is guaranteed to be free from all the kinds of bugs covered by TrustInSoft Analyzer.

The “real” hash value¶

We can see the value of the hash in the shell in which we executed TrustInSoft Analyzer:

Let’s compile and run the program again to check that the results are the same:

$ gcc /home/tis/1.42/C_Examples/skein_verification/*.c && ./a.out

We get the following output, which is indeed the same that we get on the analyzer

224
56
146
251
183
62
26
48

The next step¶

Our driver tested the Skein implementation on a single message of length 80. We could modify it by testing a number of different messages, and thus gain better coverage, as normal unit tests will do. But what if we could test it on all the messages of length 80?

This is certainly impossible to achieve by the execution of any compiled test, but it is in the scope of TrustInSoft Analyzer.

In the next part of this tutorial we will show you how to generalize the test to arbitrary messages of fixed length. This will give mathematical guarantees about the behavior of the implementation on any message of the fixed length.

Please click here to continue the tutorial.

The limits of software testing¶

Testing a program on a given set of test cases can allow you to identify some bugs, but it can not guarantee their absence. This is true even if you test your program on a huge amount of cases, because it is very unlikely that you will be able to cover them all.

Even in a simple example like ours (hashing a message of length 80), there are way too many test cases to consider (see the note below to get some detailed calculations).

Furthermore, even if your cases pass the test, this gives you no guarantee about future behavior: for example, if a test case results in an undefined behavior this might pass unnoticed in the test environment but trigger a bug in your client’s machine.

The power of abstract interpretation¶

The value analysis performed by TrustInSoft Analyzer uses abstract interpretation techniques in order to represent the values of the terms in the program. This allows for the representation of very large or even infinite sets of values in a way that makes sense to the analyzer. That is why we are going to be able to consider all the possible values for a given variable.

If the value analysis raises no alarms, this means that you have mathematical guarantees about the correctness of the program. These guarantees are not limited to one particular execution, but extend to any execution in a standard-compliant environment (which respects all the hypothesis made during the analysis).

Generalizing the analysis to arbitrary messages of fixed length¶

Our goal is to obtain a result that is valid for any given array of length 80. Let’s start by modifying the main.c program in order to tell the analyzer that each of the elements in the msg array can take any value between 0 and 255.

To accomplish this, it suffices to add a couple of lines to the main.c program

    for(i = 0; i < 80; i++)
        msg[i] = tis_interval(0, 255);

to make it look like this:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26

/* Test driver for Skein hash function */
#include "skein.h"
#include "stdio.h"

#define HASHLEN (8)
u08b_t msg[80];

int main(void)
{
    u08b_t hash[HASHLEN];
    int i;

    for(i = 0; i < 80; i++)
        msg[i] = tis_interval(0, 255);

    Skein_256_Ctxt_t skein_context;

    Skein_256_Init(&skein_context, 8 * HASHLEN);
    Skein_256_Update(&skein_context, msg, 80);
    Skein_256_Final(&skein_context, hash);

    for (i = 0; i < HASHLEN; i++)
        printf("%d\n", hash[i]);

    return 0;
}

We then launch the value analysis again

$ tis-analyzer-gui -64 -val -slevel 100 /home/tis/1.42/C_Examples/skein_verification/*.c

and open the GUI:

There are no alarms in the GUI. This means that we have mathematical guarantees that the code is free from all the bugs covered by TrustInSoft Analyzer.

Congratulations! You have just proved that initializing, parsing, and hashing a message of length 80 by calling the three functions

    Skein_256_Init(&skein_context, 8 * HASHLEN);
    Skein_256_Update(&skein_context, msg, 80);
    Skein_256_Final(&skein_context, hash);

will cause no runtime errors, whatever the contents of the 80 char array msg.

A word on variation domains¶

We will end this part of the tutorial with a few words on the representation of values by the analyzer. At each program point, the analyzer determines a variation domain for each variable or expression. The value of the variable or expression is always guaranteed to be contained in the variation domain but, due to the possible loss of precision, these domains can be over-approximations.

If you go to the Values widget in the GUI and click on the msg variable in the Interactive Code Window (as shown below), you will be able to see how the analyzer represents integer values contained in the array msg of the program main.c:

The analyzer shows that, after the initialization loop, msg[0..79] ∈ [--..--]. This means that each of the values msg[0] to msg[79] can take an arbitrary value in the interval [--..--]. As pointed before, for an unsigned char [--..--] stands for any value that fits within the type, that is between 0 and 255.

This is exactly what was achieved by calling the function tis_interval(0, 255).

Analysis Overview¶

The main steps of an analysis are:

• First, to prepare the source code in order to make it understandable by the tool. This mainly consists of finding out which options are used to compile it (see Prepare the Sources). At the end of this step, the tool should be able to run the analysis without errors (see Check Preparation).
• Then, to define the perimeter to study (see Prepare the Analysis). This is a user choice depending on the part of the application that has to be verified. The goal of this step is to build the context in which the application will be analyzed.
• To run value analysis in order to detect alarms related to the software weaknesses listed in the CWE-subset. Value analysis can be tuned to increase the precision, either globally or locally, which helps in reducing the number of alarms (see Study the Alarms).
• Each remaining alarm must be examined to find out whether it is relevant or not (i.e. if it can actually happen or not). Some annotations can be added to help the analyzer in removing it if it appears to be a false alarm (see ACSL Properties).
• Finally, it is important to check all the annotations as they are used as hypotheses at the previous step. Some of them can be formally proven using the WP tool that involves theorem prover techniques (see Prove Annotations with WP). The others have to be carefully reviewed since all the results of the analysis rely on these hypotheses.

Here and there, extracting information, either to understand the results or to produce a report, is also useful. This can be done by combining options and scripts. How to do it is also explained in Get the Information.

Although the tool can be used purely from the command line interface, it also provides a GUI (see the TIS GUI Manual) that is very convenient for exploring the computed results.

Manual Preparation¶

clang -C -E -nostdinc -isystem TIS_KERNEL_SHARE/libc

$ tis-analyzer -I incl_dir f1.c f2.c f3.c

$ tis-analyzer -I incl_dir f1.c f2.c f3.ci

 int x = M;
 extern int y;

 int main(void) {
   return x + y;
 }

 int y = M;

$ clang -C -E -nostdinc -DM=1 -o h1.tis.ci h1.c
$ clang -C -E -nostdinc -DM=2 -o h2.tis.ci h2.c

$ tis-analyzer -val h1.tis.ci h2.tis.ci

...
[value] Values at end of function main:
    __retres ∈ {3}
...

-I$(tis-analyzer -print-share-path)/libc

 #include <tis-kernel/libc/xxx.h>

 // some more declarations and/or specification for <xxx.h>

tis-analyzer -metrics <..source and preprocessed files..> <..preprocessing options>

Automatic Preparation¶

This section describes how to automatically produce a compile_commands.json file that contains instructions on how to replay the compilation process independently of the build system.

sudo apt install bear

tis-analyzer -compilation-database path/to/compile_commands.json ...

tis-analyzer -compilation-database path/to/project ...

{
    "compilation_database":
    [
        "path/to/compile_commands.json"
    ],
    "files":
    [
        "path/to/file_1",
        "path/to/file_2",
        "path/to/file_N"
    ],
    "machdep": "gcc_x86_64",
    "main": "main",
    "val": true,
    "slevel-function":
    {
        "function_name": 10
    }
}

tis-analyzer -tis-config-load tis.config

Check Preparation¶

At this point, whatever method was chosen for the preparation step, you should, for instance, be able to execute:

tis-analyzer -metrics <... arguments...>

with the appropriate arguments, the analyzer should run with no errors. Using the command tis-analyzer-gui with the same arguments starts the GUI which lets you browse through the source code, but not see the analysis results yet, since nothing has been computed at the moment.

It is often useful to save the results of an analysis with:

tis-analyzer ... -save project.state > project.log

This command puts all the messages in the file project.log and saves the state of the project itself to the file project.state, so that it can be loaded later on. For instance, we can load it now in the GUI by executing:

tis-analyzer-gui -load project.state

In case the application includes some special features (assembler code, etc.) and/or requires to be studied for a specific hardware target and/or with specific compiler options, please refer to Dealing with Special Features.

Define the Perimeter¶

The study perimeter could be the whole program, or only some functions of a library, or a single use case scenario. Explaining how to decide which part of the source code should be studied is very difficult, since it depends a lot on the particular application, the amount of time available, and mostly on how one looks at the problem… Adopt an incremental approach: begin with a small study, in order to understand how to apply the tools in the given situation, and then enlarge the perimeter later on.

Prepare the Entry Point¶

In order to run a value analysis, an entry point to the program has to be provided. The body of the entry point function defines the studied perimeter. It is usually the main function which establishes the context verified by the analysis, but other functions can be used to this end as well.

• To analyze a library function, the entry point function should build values for the given library function’s input arguments, and then call the library function itself using the arguments prepared in this way (see Write an Entry Point).
• To analyze a scenario, preparation of input values may be needed as well, then followed by calling some functions in a sequence. This sequence of function calls defines the scenario.
• In some cases, the actual main function of an application can be used directly. However, if it takes options and arguments, it still has to be called from an entry point that builds values for them. The tis-mk-main utility can help in doing so (see tis-mk-main Manual). Be aware though, that if main is is a complex function that parses options and needs many string manipulations, it is probably a better idea to write a smaller entry point from scratch in order to define a more precise context of analysis.

It is important to mention here the difference between dynamic test execution and static value analysis. As the code is not executed in the latter, each of the built inputs provided to the analyzed function does not need to have a single value. It means that a function taking a single integer parameter x can, for instance, be analyzed for all the possible input values, or for all the values from a given set (e.g. 3 < x < 150). So when we mention “a value” here, we do not actually mean “a single concrete value”, but rather “a set of abstract values”.

#include <stdio.h>
#include <tis_builtin.h>

int compute (char * buf, size_t len, char * result);

int main (void) {
  char buf[100];
  tis_make_unknown (buf, 100);
  size_t len = tis_interval (0, 100);
  char x;
  char * result = tis_nondet_ptr (NULL, &x);
  int r = compute (buf, len, result);
}

#include<tis_builtin.h>
struct list {
    int data;
    struct list * next;
};
int main(){
    int *p0, *p1, *p2;
    struct list * p3;
    tis_init_type("int *", &p0, 1, 1, 1);
    tis_init_type("int *", &p1, 1, 10, 1);
    tis_init_type("int *", &p2, 1, 1, 0);
    tis_init_type("struct list *", &p3, 3, 1, 1);
    tis_dump_each();
}

p0 ∈ {{ &S_p0[0] }}
S_p0[0] ∈ [--..--]

p1 ∈ {{ &S_p1[0] }}
S_p1[0..9] ∈ [--..--]

p2 ∈ {{ NULL ; &S_p2[0] }}
S_p2[0] ∈ [--..--]

p3 ∈ {{ &S_p3[0] }}
S_p3[0].data ∈ [--..--]
    [0].next ∈ {{ &S_next_0_S_p3[0] }}
S_next_0_S_p3[0].data ∈ [--..--]
             [0].next ∈ {{ &S_next_0_S_next_0_S_p3[0] }}
S_next_0_S_next_0_S_p3[0].data ∈ [--..--]
                      [0].next ∈ {{ &S_next_0_S_next_0_S_next_0_S_p3[0] }}
S_next_0_S_next_0_S_next_0_S_p3[0].data ∈ [--..--]
                               [0].next ∈ {0}

more $(tis-analyzer -print-share-path)/tis_builtin.h

Check the External Functions¶

Now, when the main entry point is ready, it is time to run the value analysis for the first time using the -val option.

An important thing to check is the nature of external functions. More precisely, to look for this message in the log file:

$ grep Neither proj.log
[kernel] warning: Neither code nor specification for function ...

This message indicates that the given function is undefined. In order to progress with the value analysis, it MUST be defined by either:

• adding missing source files,
• or writing C stubs,
• or specifying it with ACSL properties.

The libc library functions should not appear in these messages since most of them are already specified in provided library files (see About Libraries).

char *mystrdup(char *s);

int main(void) {
  char c, *p;
  int x;
  p = mystrdup("abc");
  if (p)
    c = p[0];
  x = c - '0';
}

#include <string.h>
#include <stdlib.h>
#include <tis_builtin.h>

char *mystrdup(char *s) {
  size_t l = strlen(s);
  char *p = malloc(l+1);
  if (p) {
    tis_make_unknown(p, l);
    p[l] = 0;
  }
  return p;
}

$ tis-analyzer -val -slevel 10 main.c mystrdup.c

tests/val_examples/stub_main.c:13:[kernel] warning: accessing uninitialized left-value: assert \initialized(&c);
tests/val_examples/stub_main.c:13:[kernel] warning: completely indeterminate value in c.

Tune the Precision¶

Performing value analysis with no additional options (like in all the cases above) makes it run with a rather low precision. It should not take too long to get the results that indicate where the alarms were found. When using the GUI, the list of alarms can be selected using the Kind filter of the Properties panel, and a summary of the number of alarms can be found in the Dashboard panel.

The global precision can be changed using the -slevel n option. The greater n is, the more precise the analysis is (see About the Value Analysis for more details). These alarms which could be formally verified by increasing the precision in this way will disappear. Those which remain are the difficult part: they require further attention.

Value analysis takes longer and longer when the precision increases. Thus it can be profitable to fine tune the precision locally on certain functions in order to benefit from the higher precision level where it is advantageous (so that more alarms are formally verified) while keeping it lower where it matters less (so that the analysis runs faster).

For the same reason (fast analysis to find bugs earlier) it can also be useful to reduce (temporarily) the size of the arrays (when the source code is structured to allow this easily).

Using the command line option -tis one can examine the evolution of the analysis. More exactly, this option provides an interactive view of what the analyzer is doing and, for readability reasons, it should be always used in a large terminal. The insight into the progress of the analysis gained in this way helps greatly in choosing appropriate global and local precision levels:

• If it appears that huge amount of time is spent in a low level function f, its precision can be decreased using the -slevel-function f:n option with n smaller than the global precision.
• In the opposite case, if the global precision has to be kept low for performance issues, the local precision can be increased in some functions only.

The same information is shown when starting the value analysis from the GUI and the final analysis information can be found in the Dashboard panel.

Note that at this point the goal is not to study the alarms precisely, but rather to get a rough idea of the amount of work needed in order to be able to decide which part to study.

To Split or Not to Split¶

The experience suggests that if the size of the analyzed source code is large and / or if there are many alarms, it is usually worthwhile to split the study into smaller, more manageable sub-components. The idea here is to write a precise specification for every sub-component and then analyze each of them independently toward its particular specification. Afterwards, the main component can be studied using those specifications instead of using directly the sub-components’ source code.

It is quite easy to decide which part should be split if some main features are identifiable and clearly match a given function. Otherwise, a first overview of the number of alarms may help to isolate a part that seems difficult for the analyzer. However, as the separated function must be specified, it is much easier if it has a small and clear interface (in order study a function, it must be called in the intended context, and this context might be difficult to build if it corresponds to a large and complex data structure).

To split the analysis one must write:

• a main function for the main component,
• a main function and an ACSL specification for each of the API functions which is supposed to be studied independently.

Then, when performing the analysis for the main component, the -val-use-spec option should be used in order to provide the list of the API specified functions. For each of the functions from this list the value analysis will use the function’s ACSL specifications instead of the function’s body.

For instance, the commands below can be used to split the study into the main analysis with two sub-components corresponding to the f1 and f2 functions:

$ tis-analyzer -val $SRC main.c -val-use-spec f1,f2 \
                                -acsl-import f1.acsl,f2.acsl \
                                -save project.state
$ tis-analyzer -val $SRC main_f1.c -acsl-import f1.acsl -save project_f1.state
$ tis-analyzer -val $SRC main_f2.c -acsl-import f2.acsl -save project_f2.state

In the commands above:

• the files main.c, main_f1.c and main_f2.c should hold the entry points for the main component, and the f1 and f2 functions respectively;
• the files f1.acsl and f2.acsl should hold the ACSL specifications of the, respectively, f1 and f2 functions (see Write a Specification to learn how to write a specification).

Multi-Analysis¶

There is another case where studying an entry point may require several separate analyses: when there is a parameter in the program that has to be attributed a value (e.g. using a macro) and when it is difficult to give it an arbitrary value beforehand (e.g. it is a parameter defining the size of an array). In such situations it is better to write a loop in an external script to attribute different values to that parameter and run as many analyses as necessary.

The following script runs an analysis for every N being a multiple of 8 from 16 to 128:

#/bin/bash

for N in $(seq 16 8 128) ; do
  tis-analyzer -D N=$N -val $SRC main.c
done

Of course, it supposes that N is used somewhere in main.c.

Write a Specification¶

Writing a specification for a function is useful in two cases:

• When some splitting is done.

  A certain function can be studied independently, as a separate sub-component of the analysis. The function is verified toward a certain specification and then that specification can be used (instead of using directly the function’s body when analyzing function calls) in the main component’s verification (To Split or Not to Split).

• When using some unspecified external functions.

  If an external function, that is not part of the subset of the libc library functions provided with the tool (which are already specified), is used in the program, then it needs an explicit specification. The provided specification has to indicate at least which of the concerned data may be possibly modified by the function. Pre and postconditions are not mandatory in that case.

The specification is written in ACSL and is mainly composed of:

• preconditions (requires properties),
• modified data descriptions (left part of assigns properties),
• dependencies (\from part of assigns properties),
• postconditions (ensures properties).

The ACSL properties can be either inlined directly in the source files or written in separate files and loaded (as explained in ACSL Properties). An analysis will use the specification instead of the function’s body to process a function call when either the body is not provided or an appropriate -val-use-spec option has been set in the command line.

When analyzing a function call using the specification, the tool:

• first verifies that the pre-state satisfies the preconditions,
• then assumes that:
  • the post-state only differs from the pre-state for the specified modified data,
  • and that the post-state satisfies the postconditions.

requires r_x_pos: x > 0;

//@ assigns <left part> \from <right part>;

//@ assigns \result \from a, b, indirect:c;
int f (int a, int b, int c) { return c ? a : b; }

int t[10];
//@ requires 0 <= i < 10; assigns t[..] \from t[..], a, indirect:i;
void set_array_element (int i, int a) { t[i] = a; }

assigns B \from \nothing;
assigns \result \from B;

ensures \initialized(&B);

ensures (\result == 0 && \initialized(&B)) || (\result < 0);

Check the Coverage¶

Before going any further, it is often advantageous to check the code coverage in order to verify if all the dead code which exists in the application (i.e. the parts of code composed of the functions and branches that are not reachable by the analysis) is indeed intended. To learn how to do that, see Information about the Coverage.

Dead code can be spotted in the GUI by looking for statements with the red background. If some dead code seems strange, it can be explored and investigated using the value analysis results. Clicking on variables and expressions allows to inspect their computed values.

As long as the analysis did not degenerate, the code classified as dead by the tool is a conservative approximation of the actual dead code. It is guaranteed that, in the context defined by the input values, the concerned statements cannot be reached whatever happens. When relying on this guarantee, one should however keep in mind these two important assumptions it depends on: that it applies only if the analysis did not degenerate and that dead code is always considered in the context defined by the input values. This is because most of the time if some code has been marked as dead when it should not have been, the reason is actually that the context of analysis was defined too restrictively (i.e. it does not include all the input values that can happen in the real execution). Another common reason is that the analysis has simply stopped computing a given branch:

• either because the information was too imprecise to go further (in that case a degeneration warning message has been emitted),
• or because a fatal alarm has led to an invalid state (e.g. accessing the content of a pointer which is NULL for sure renders the state invalid).

Summary¶

At this point, one should have some analyses (one or several) which cover the intended parts of the code and end without any degeneration. The results most likely include alarms. The chapter Study the Alarms explains how to deal with the alarms and, before that, the chapter Get the Information explains how to extract more information from the analysis results.

In case if, due to applying some splitting, there are several analyses, there is no preferred order of the verifications. In any case however, modifying the existing specifications leads to invalidating the results obtained so far.

Generate the CSV Files¶

The tis-info plug-in can be used to generate CSV files. The main options allow us to extract the information concerning:

• functions: -info-csv-functions functions.csv
• variables: -info-csv-variables variables.csv
• properties: -info-csv-properties properties.csv
• statements: -info-csv-statements statements.csv

For instance, in order to get the information about functions from a previously saved project project.state, the command line would be:

tis-analyzer -load project.state -info-csv-functions functions.csv

As mentioned before, the kind of obtained information (i.e. either purely syntactic or also semantic) will depend on whether the saved project includes the value analysis results or not.

In the generated CSV files, the information about each element is printed on a single line (with comma separated fields). Hence, the files can be opened in a spreadsheet tool for easy selection of elements. Moreover, this format can be easily grepped (i.e. filtered using the grep utility), for instance, the following command returns all the information about the function funname:

grep funname functions.csv

In order to filter on a specified column, the awk tool is also very practical. For instance, the following command returns only the lines where the word valid appears in the fifth column:

awk -F, '! ($5~"valid") {print}' properties.cvs

Also, awk can be used to easily extract only some of the columns:

awk -F, '{print $4 $5}' properties.cvs

Information about the Functions¶

The generated file functions.csv provides information about the functions. It contains the list of both defined and declared functions appearing in the analyzed source code, including their locations, whether they are called or not, are they reachable in the analyzed context, etc. The most useful piece of information here concerns the coverage and it is detailed just below.

Information about the Coverage¶

grep -v TIS_KERNEL_SHARE

grep ", unreachable,"

grep -v ", unreachable," | grep -v "100.0%"

tis-aggregate coverage project.aggreg  >  coverage.csv

path_1/proj_1
path_2/proj_2
...
path_n/proj_n

Information about the Properties¶

The location and status of each property can be found in the properties.csv file. If the names given to the user annotations follow some naming conventions (see Naming the Annotations), it is quite easy to use grep to extract more precise information that file.

For instance, if the names of the annotations that should be proved by the WP plug-in all have a _wp suffix, it is easy to check if they are all verified with the following command:

grep "_wp," properties.csv | grep -v ", valid$"

Information about the Statements¶

The generated file statements.csv provides information about certain kinds of statements in the analyzed program.

For instance, it contains information about the function calls, in particular whether a specific call is direct or not. Moreover, if an indirect call has been encountered during the value analysis, it provides the list of all the possibly called functions. Extracting this information can be done with:

grep ", call," statements.csv | grep -v DIRECT

Some useful information concerning the condition values can also be found here. Especially, whether a condition happens to be always true or always false. This kind of situations is often also observable through the dead code, although not in all cases, since an if condition might be always true, but may have no else branch (which, obviously, would be dead if it existed).

Information about the Variables¶

The information about all the variables is available in the variables.csv generated file. The exception are the global variables which are not accessed or modified, since they are removed from the analysis results. This information can also be used, for instance, to easily find the location of the definition of a variable or to list all the static or volatile variables.

Understand and Sort the Alarms¶

The list of all the existing alarms is given in Value Analysis Alarms.

Most of the time understanding the meaning of alarms is relatively easy since the generated assertions, messages, and warnings tend to be quite clear. The matter that requires more effort is understanding whether a given alarm is relevant: can the problem that it indicates actually happen or not. If an alarm is false (which is in fact the most frequent case), the aim is to get rid of it: convince the tool that the corresponding problem cannot occur, so that the alarm stops being emitted. Finding out exactly where an alarm comes from is essential to this end.

False alarms are often a result of a too high level of approximation in the analysis. It is recommended to treat the alarms starting from the first one in order to detect an imprecision as soon as possible.

The list of the generated assertions can easily be extracted from the properties.csv file (see Information about the Properties). Then, for instance, these assertions can be counted in order to track the evolution of their total number during the working process. (Note, however, that this particular measure is not necessarily very pertinent, because the relation between problems and emitted alarms is not really one-to-one. Losing precision at one point of the analysis can lead to several alarms which have the same origin. Moreover, solving one problem may cause many unrelated new alarms, as several problems might have been hiding behind the solved one.)

The GUI is a good place to start studying the alarms by exploring the data values. As said before, the list of all the properties discovered during the analysis can be found in the Properties of the GUI, and there is a button which allows to select the alarms among all the properties. Start investigating with the first emitted alarm by sorting them by their emission rank.

About the Value Analysis¶

Understanding better how the value analysis works, and how to tune its options, helps greatly in dealing with the alarms.

Value analysis uses abstract interpretation techniques that propagate the information forward through the analyzed application’s control flow in order to compute states at each reachable program point. A state is an over-approximation of all the possible values that the variables can hold at a given program point. You can imagine a state as a mapping between the variables and sets of values (keep in mind though that in reality it is a little more complex than that). For instance, the sets of values of integer variables can be represented by integer intervals. For a detailed description of the representation of values, see Value Analysis Data Representation.

See Tune the Precision for explanations concerning tuning the precision level with the -slevel option. The precision level is related with the number of states that can be stored for each program point. The smaller this number is, the more coarse the approximation is, as more computed states are merged together.

Example:

  //@ assert 0 < x < 10;
  if (x < 5)
     y = 5;
  else
     y = 10;
L:

Computing a unique state at label L only gives that x ∈ [1..9] and y ∈ [5..10]. But if the slevel is larger, then two states can be stored at L giving exactly that either y == 5 when x ∈ [1..4] or y == 10 when x ∈ [5..9].

Notice that the assertion assert 0 < x < 10 above reduces the possible values for x. It is important to remember that this works in the same way for the assertions automatically generated from alarms. For instance, if a statement a = b / c; is reached with c ∈ [0..100], an alarm is emitted in form of an appropriate assertion:

/*@ assert Value: division_by_zero: c ≢ 0; */

Then, the analysis continues with context where c ∈ [1..100].

int x = f();
tis_variable_split (&x, sizeof(x), 10);

#include <tis_builtin.h>

int G;

void foo(int n)
{
    int x = G;
    /*@ assert x_pos: 1 <= x <= 10; */
}

int main(void)
{
    int n = tis_interval_split(-10, 10);
    G = n;
    if (n > 0)
        foo(n + 5);
    return 0;
}

Remove Alarms by Tuning the Analysis¶

Tuning the -slevel and -slevel-function options to control the precision of the analysis, using the information obtained from the -tis option’s output, has already been explained in Tune the Precision.

In the GUI, statements where the precision level (i.e. the slevel value) has been reached are indicated by a colored margin in source view windows (see Interactive Code Panel). Moreover, the reached value can be sorted in the statements window (Statements).

The analysis can also get imprecise for other reasons than reaching the defined precision level. Especially this is the case when the log trace include messages about garbled mix values. It is very likely that if such messages appear, the analysis will not produce any interesting results.

There are several other options that can be used to fine tune the value analysis.

Some of them work similarly to the -slevel option, i.e. they control the maximum number of states that can be kept separated. For instance:

• -val-split-return-function f:n: split the return states of function f according to \result == n and \result != n;

• -val-split-return auto: automatically split the states at the end of each function according to the function return code;

• -val-split-return-function f:full: keeps all the computed states at the end of function f in the callers;

• -val-slevel-merge-after-loop <f | @all> when set, the different execution paths that originate from the body of a loop are merged before entering the next execution.

  The default behavior is set to all functions (-val-slevel-merge-after-loop=@all). It can be removed for some functions (-val-slevel-merge-after-loop=@all,-f), and deactivated for all functions (-val-slevel-merge-after-loop=-@all), and activated for some (-val-slevel-merge-after-loop=-@all,+f).

• -wlevel n: do n loop iterations before widening.

Some other options can be used to control the precision of the representation of a value (rather than the number of states). For instance:

• -val-ilevel n: Sets the precision level for integer representation to n: each integer value is represented by a set of enumerated values up to n elements and above this number intervals (with congruence information) are used.
• -plevel n: Sets the precision level for array accesses to n: array accesses are precise as long as the interval for the index contains less than n values. See Tuning the precision for array accesses for more information about this option.

There are also options which allow to enable / disable certain alarms. Most of these options are enabled by default, and it is usually safer to leave it this way (unless you really know what you are doing).

Of course not all existing options have been enumerated here. The full list of the available options is given by -value-help.

#include <tis_builtin.h>

char c[20];
struct s { int m[50]; void *p; };
struct s t[60];

void init(void) {
  for (int i = 0; i < 60; i++)
    {
      for (int j = 0; j < 50; j++)
        t[i].m[j] = (i + j) % 10;
      t[i].p = c + i % 20;
    }
}

int main(void) {
  init();
  int x = tis_interval(5, 45);
  int y = tis_interval(2, 56);
  t[y].m[x] = -1;

  x = tis_interval(5, 45);
  y = tis_interval(2, 56);
  int result = t[y].m[x];

  int *p = &t[y].m[x];
  int result2 = *p;
}

$ tis-analyzer -val -slevel-function init:10000 nestedarrays.c

  x ∈ [5..45]
  y ∈ [2..56]
  result ∈ {{ NULL + [-1..9] ; &c + [0..19] }}
  p ∈ {{ &t + [428..11604],0%4 }}
  result2 ∈ {{ NULL + [-1..9] ; &c + [0..19] }}

$ tis-analyzer -val -slevel-function init:10000 nestedarrays.c -plevel 3000

  x ∈ [5..45]
  y ∈ [2..56]
  result ∈ [-1..9]
  p ∈ {{ &t + [428..11604],0%4 }}
  result2 ∈ {{ NULL + [-1..9] ; &c + [0..19] }}

{{ &t + [428..11604],0%4 }}

Control the Analyzer¶

tis_show_each_iteration (i, t[i]);

[value] Called tis_show_each_iteration({0; 1; 2; 3; 4}, [0..10])

tis_print_subexps ("simple sums", x + y, y + z, z + x);

[value] Values of all the sub-expressions of simple sums (expr 1):
    int x + y ∈ {3}
    int x ∈ {1}
    int y ∈ {2}
[value] Values of all the sub-expressions of simple sums (expr 2):
    int y + z ∈ {5}
    int y ∈ {2}
    int z ∈ {3}
[value] Values of all the sub-expressions of simple sums (expr 3):
    int z + x ∈ {4}
    int x ∈ {1}
    int z ∈ {3}

tis_print_abstract_each(&i, &t);

[value] Called tis_print_abstract_each:
     i ∈ {0; 1; 2; 3; 4}
     t[0..4] ∈ [0..10]
      [5..99] ∈ UNINITIALIZED

$ tis-analyzer -val test.c -val-dump-destination all -val-dump-directory /tmp

test.c:11:[value] Dumping state in file '/tmp/state_0.txt'
test.c:11:[value] Dumping state in file '/tmp/state_0.json'

{
  "file": "test.c",
  "line": 11,
  "args": "([0..10])",
  "state": [
    {
      "base": "t",
      "values": [
        { "offset": "[0..4]", "value": "[0..10]" },
        { "offset": "[5..9]", "value": "UNINITIALIZED" }
      ]
    },
    { "base": "i", "values": [ { "value": "{0; 1; 2; 3; 4}" } ] }
  ]
}

$ kill -USR1 12345

$ tis-analyzer --timeout 5m -val ... -save project.state

 int x = 0; /* the memory location to watch */
 void *p = (void *)&x; /* its address */
 size_t s = sizeof(x); /* its size */
 int y[10];

 /* The analysis stops when x is not exact (i.e. not a singleton value). */
 int maximal_cardinal_allowed = 1;
 tis_watch_cardinal(p, s, maximal_cardinal_allowed, 0);

 /* The analysis stops the fourth time when x may be negative. */
 int forbidden_values = tis_interval(INT_MIN, -1);
 int exceptions = 3;
 tis_watch_value(p, s, forbidden_values, exceptions);

 /* The analysis stops when x may be an address. */
 tis_watch_address(p, s, 0);

/* The analysis stops when x may be a garbled mix value. */
 tis_watch_garbled(p, s, 0);

 p = y;

 /* The analysis starts to detect if an expression is evaluated to an
 imprecise pointer starting at base address &y. */
tis_detect_imprecise_pointer(p);

/* The analysis stops because the expression p+tis_interval_split(0,3)
is evaluated to an imprecise pointer &y + [0..3]. */
*(p+tis_interval(0,3)) = 3;

Remove Alarms by Adding Annotations¶

Tuning the precision using various analysis options, as previously explained, is one way of removing false alarms. Another way of guiding the analyzer is by adding assertions to the program. Other kinds of properties also can be introduced, but assertions are by far the most frequently used for this purpose.

If you do not know how to add ACSL properties to your project, first read ACSL Properties.

Of course, as the analysis results rely on the properties introduced in this way, they must be properly checked. The best approach is to verify such properties formally using, for instance, the WP plug-in (see Prove Annotations with WP) or other formal tools. When it is not possible, they should be verified manually.

Some examples are given below.

If source code modifications are needed, and the source code is in a git repository, the tis-modifications tool may be helpful to track them in order to check that they are correctly guarded. See tis-modifications Manual.

     int T[10];
     ...
L1:  if (0 <= x && x < y) {
       ...
L2:    if (y == 10) {
L3:      ... T[x] ...
         }
       ...
       }

at L3: assert ax: x < 10;

at L1: assert ay: y <= 10 || 10 < y;

int tmp = i + j;
if (tmp < 10) {
  ..
  //@ assert a_tmp: tmp == i + j;
  ... T[tmp] ...
  }

int T[100];

//@ requires 0 <= n < 50;
void main(int n)
{
    int i = 0;
    while (i <= n) {
        T[i] = 3;
        i++;
    }
    T[i] = i;
}

warning: accessing out of bounds index [1..127]. assert i < 100;

/*@ loop invariant i <= 50; */

Bounded Buffers¶

A very common situation is to have a pointer to an array, and an integer that gives the number of remaining bytes between this pointer and the end of the array. In the internal representation of the values, it is not possible to represent relations between these two variables.

Buffer problem: there is a relation between cur and len, but it cannot be represented.

A typical function to handle this buffer is:

void process (char * cur, size_t len) {
  char * p = cur;
  for (size_t i = 0 ; i < len ; i++, p++) {
    *p = ...
  }
}

The validity of the pointer p has to be checked to avoid an alarm on p access, but also to get precise results later on. It is especially important when the pointer points to an array that is part of a larger structure. For instance:

struct data {
  char buffer[BUFFER_LEN];
  unsigned current_index;
  unsigned state;
};

//@ requires 0 <= data->current_index < BUFFER_LEN;
int treatment (struct data * data, int n) {
  char * current = data->buffer + data->current_index;
  size_t length = BUFFER_LEN - data->current_index;
  if (n > length) n = length;
  process (current, n);
  ...
  }

If the analysis is not able to know that p does not go beyond the end of the buffer field, the value of the other fields current_index and state might be modified as well and might be too imprecise for the analysis to give interesting results later on.

So the process function needs a precondition to give the constraint on cur and len to ensure the validity of the pointer. This precondition could simply be:

//@ requires \valid (cur + 0 .. len-1);

Unfortunately, the Value analysis is not able to reduce the input states with this kind of annotation, but it can be translated into a more exploitable equation when one of the data is precise enough to reduce the other:

• if the data to reduce is the pointer:

//@ requires cur <= \base_addr (cur) + \block_length (cur) - len * sizeof (*cur);

• if the data to reduce is the length:

//@ requires length <= (\block_length (data) - \offset (data)) / sizeof (*data);

Notice that the ACSL functions \base_addr, \block_length and \offset only provide the expected information when cur is a pointer to an array allocated on its own. If the array is a field in a structure, \base_addr(cur) returns the base address of the structure.

Structure with a .buf field: ACSL functions are related to the allocated block, not the internal array.

Anyway in some cases, even if the analyzer computes the optimal information, cur and len both have an unknown value from intervals and the relation between the two variables has been lost. So the memory access to (*p) raises an alarm when we cannot check that adding the upper bound of both intervals is smaller than (buf + BUFFER_LEN). Moreover, if buf is in a structure as explained above, buf and BUFFER_LEN may be unknown in the function.

A trick can be to modify the original function by adding a parameter that gives a pointer in the object beyond which the function is not expected to access:

/*@ requires f_r_buf: val: cur <= bound;
    requires f_r_len: wp: len <= bound - cur;
*/
void process_bounded (char * cur, size_t len, char * bound) {
  char * p = cur;
  //@ loop invariant f_l_p: val: p <= bound;
  for (size_t i = 0 ; i < len ; i++, p++) {
    if (p >= bound) break;
    *p = ...
  }
}

In the previous example, the call to process would have to be changed to:

process_bounded (current, n, data->buffer + BUFFER_LEN);

As long as the preconditions are true, this modified function is equivalent to the original one. This first precondition is often checked by the Value analysis, when it is not, the value analysis reduces the range of cur. The value analysis can use the second precondition to reduce the length.

Two annotated functions with such bounds, tis_memset_bounded and tis_memcpy_bounded, are provided to be used instead of memset and memcpy when this problem occurs with these libc functions.

Inline ACSL Properties¶

One way to add ACSL annotations to a project is to write them directly in the source code in special comments:

• either standard C style comments: /*@ ... */,
• or one line C++ style comments: //@ ....

There are several kinds of properties and they all need to be placed in an appropriate place in the source code:

• Function specifications (described in Write a Specification) must be inserted either before the function itself or before the function’s declaration.
• Local properties (described in Remove Alarms by Adding Annotations):
  • assertions must be inserted at the program point where they apply,
  • loop properties must be inserted just before the loop they apply to.
• …

For more information about the ACSL language, please refer to the ACSL Documentation.

Import ACSL Properties¶

For many reasons it is usually preferable to avoid modifying the source code which is analyzed, as introducing changes to the application’s code can lead to difficulties in comparing it with the original version. For example, adding new properties alters the line numbering in a file, which makes it impossible to report problems with the original source line number.

The ACSLimporter plug-in makes it possible to write the ACSL properties into separate files and then import them for the analysis. The syntax of such files looks like this:

function <function-name>:
  contract:
    requires <pre-name-1>: <pre-definition-1>;
    assigns <assigns-definition-1>;
    ensures <post-name-1>: <post-definition-1>;

  at L1: assert <assert-name-1a>: <assert-definition-1a>;
  at L1: assert <assert-name-1b>: <assert-definition-1b>;
  at L2: assert <assert-name-2>: <assert-definition-2>;

  at loop 1:
    loop invariant <inv-name-1a>: <inv-definition-1a>;
    loop invariant <inv-name-1b>: <inv-definition-1b>;

Of course, the <...> parts should be substituted by specific names and definitions.

Depending on the organization of the project, it might be better to put all the properties in a single ACSL file or to split them throughout several files. If the properties concerning the same function appear in different files, the specifications are merged.

To load the property files, so that they are taken into account during the analysis, the -acsl-import <file.acsl> option has to be specified for each concerned ACSL file.

Naming the Annotations¶

Giving a unique name to each annotation permits referring to it easily later on. Moreover, it makes the result files a lot clearer and more readable: when mentioning a particular annotation they will use its name instead of the corresponding file name and line number.

Using standard naming conventions is highly recommended. Some tools require particular naming of assertions to properly check that everything have been verified at the end of the analysis.

The proposed naming conventions are:

• To choose a unique short prefix for annotations concerning each function (example: add_).
• To include a letter that indicates the kind of each property (e.g. first requires property for function add could be then named add_r1). (However, this not really necessary if the name is always used together with the corresponding keyword, like for example: requires add_r1, ensures add_e2, etc.)
• To use a suffix informing about the way each property is verified. For instance:
  • add_e2_val: if the property is found always valid by Value;
  • add_e2_wp: if the property is proved by WP;
  • add_e2_sc: if the property could have been removed as redundant by Scope (note: it could be necessary to keep this property anyway because it still might be useful for Value or WP computations);
  • add_e2_rv: if the property has been manually reviewed.

These naming conventions might seem to be quite cumbersome to use (especially the verification method suffix). However, as mentioned before, they make the automatic generation/verification possible, so they are highly recommended.

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.