tis-aggregate Manual

Introduction

The purpose of the tis-aggregate tool is to collect and aggregate several results generated by TrustInSoft Analyzer.

To know how to use TrustInSoft Analyzer, refer to TrustInSoft Analyzer Manual. The Basic usage section below assumes that you already know how to build tis-analyzer command lines to run analyses and get Value analysis results as explained in Prepare the Analysis.

The next Advanced usage section presents more tis-aggregate commands and options.

Basic usage

Let’s first give an example of using tis-aggregate to get the coverage from several value analysis results. As explained in the Check the Coverage section of the TrustInSoft Analyzer Manual, the coverage measures the percentage of the code that has been reached by the value analyses, and it helps to detect dead code.

Let’s consider a small application composed of two files:

File convert.c holding some library functions:
#include "convert.h"
int convert_atoi (char * arg, uint * p) {
  unsigned int x = 0;
  for (char* p = arg; *p != '\0'; p++) {
    char c = *p;
    if ('0' <= c && c <= '9')
      x = 10 * x + c - '0';
    else
      return 1;
  }
  *p = x;
  return 0;
}
static int nb_digit (uint x, uint base) {
  if (x == 0)
    return 1;
  else {
    int nb;
    for (nb = 0; x; x /= base) nb ++;
    return nb;
  }
}
char digit_name (int x) {
  return x < 10 ? '0' + x : 'a' + x - 10;
}
char * cv_to_base (uint x, uint base, char * buf) {
  if (2 <= base && base <= 16) {
    int nb = nb_digit (x, base);
    buf[nb--] = 0;
    while (nb >= 0) {
      int d = x%base;
      char c = d <= 9 ? '0' + d : digit_name (d);
      buf[nb--] = c;
      x /= base;
    }
  }
  else
    return NULL;
  return buf;
}
char * convert (char * str_x, char * str_base, char * buf) {
  unsigned int x, base;
  int err;
  err = convert_atoi (str_x, &x);
  if (err) return NULL;
  err = convert_atoi (str_base, &base);
  if (err) return NULL;
  return cv_to_base (x, base, buf);
}
File main.c holding the test entry point:

#include "convert.h"

int main (int argc, char * argv[]) {
  if (argc != 3) {
    printf ("Error: 2 arguments expects, got %d\n", argc);
    exit (EXIT_FAILURE);
  }

  char buf[100];
  char * x = argv[1];
    char * base = argv[2];
  char * p = convert (x, base, buf);

  if (p) {
    printf ("Result: convert %s in base %s = %s\n", x, base, p);
    return EXIT_SUCCESS;
  }
  else {
    printf ("Error: unable to convert %s in base %s\n", x, base);
    return EXIT_FAILURE;
  }
}

This application can for instance be analyzed with the following command line:

$ tis-analyzer -val -slevel 100 convert.c main.c -val-args ' 1234 10'

It gives results for the analysis of the application as if it were run with the two arguments 1234 and 10. Of course, it has to be run for other values to get more analysis results.

The Information about the Coverage section explains that the coverage is computed from csv files that are generated by tis-analyzer when using -info-csv-xxx options. The simplest way to generate those files is to just add the -info-csv-all option, and a name for the results, to the command line of each analysis.

For instance, the command line above becomes:

$ tis-analyzer -val -slevel 100 convert.c main.c -val-args ' 1234 10' \
  -info-csv-all results/test-1234-10

The argument of the option must be unique for each analysis since it is used as a base name to store the analysis result files. Those names are provided to tis-aggregate through what is called the INDEX file. Each line of this file holds the base name of one analysis results.

Before creating the index, let’s create another analysis with a different input:

$ tis-analyzer -val -slevel 100 convert.c main.c -val-args ' 1234 2' \
   -info-csv-all results/test-1234-2

So, the index file to create for these two analyses above would looks like:

Index file convert.aggreg.index
tests/tis-aggregate/test-1234-10
tests/tis-aggregate/test-1234-2

Now the coverage can be computed with:

$ tis-aggregate coverage convert.aggreg.index

It gives the following result:

Result of: tis-aggregate coverage convert.aggreg.index
File                                  Function        #reached  #statements  Ratio  Comment      
tests/tis-aggregate/main.c            __tis_globfini  2         2            100%   total        
tests/tis-aggregate/convert.c         convert         7         11           64%    partial      
tests/tis-aggregate/convert.c         convert_atoi    15        19           79%    partial      
tests/tis-aggregate/convert.c         cv_to_base      22        27           81%    partial      
tests/tis-aggregate/convert.c         digit_name      0         5            0%     not reached  
tests/tis-aggregate/main.c            main            10        15           67%    partial      
tests/tis-aggregate/convert.c         nb_digit        12        14           86%    partial      
TOTAL (functions)                                     6         7            86%                 
TOTAL (all statements)                                68        93           73%                 
TOTAL (stmts in reachable functions)                  68        88           77%                 

It shows the list of the functions with the number of reachable statements and the total number of statements.

The three last lines labelled TOTAL summarize the coverage:

  • functions: number of analyzed functions over the number of functions.
  • statements: number of reachable statements over the number of statements.
  • stmts in reachable functions: number of reachable statements over the number of statements in the reachable functions.

We can for instance see that the digit_name function is not reached. This is because it is only used for a base greater than 10. So let’s run other analyses (with other inputs) and add them into the index file to enhance the coverage:

Index file convert2.aggreg.index
tests/tis-aggregate/test-1234-10
tests/tis-aggregate/test-1234-2
tests/tis-aggregate/test-1234-16
tests/tis-aggregate/test-0-10
tests/tis-aggregate/test-a2b-10

The coverage becomes:

Result of: tis-aggregate coverage convert2.aggreg.index
File                                  Function        #reached  #statements  Ratio  Comment  
tests/tis-aggregate/main.c            __tis_globfini  2         2            100%   total    
tests/tis-aggregate/convert.c         convert         9         11           82%    partial  
tests/tis-aggregate/convert.c         convert_atoi    19        19           100%   total    
tests/tis-aggregate/convert.c         cv_to_base      23        27           85%    partial  
tests/tis-aggregate/convert.c         digit_name      4         5            80%    partial  
tests/tis-aggregate/main.c            main            13        15           87%    partial  
tests/tis-aggregate/convert.c         nb_digit        14        14           100%   total    
TOTAL (functions)                                     7         7            100%            
TOTAL (all statements)                                84        93           90%             
TOTAL (stmts in reachable functions)                  84        93           90%             

Notice that since the function coverage is now 100%, the statements coverage and the in perimeter one are the same.

Tis-aggregate coverage formats

To change the output format to csv (below) or html, the --format option can be used:

Result of: tis-aggregate coverage convert2.aggreg.index --format=csv
File,Function,#reached,#statements,Ratio,Comment
tests/tis-aggregate/main.c,__tis_globfini,2,2,100%,total
tests/tis-aggregate/convert.c,convert,9,11,82%,partial
tests/tis-aggregate/convert.c,convert_atoi,19,19,100%,total
tests/tis-aggregate/convert.c,cv_to_base,23,27,85%,partial
tests/tis-aggregate/convert.c,digit_name,4,5,80%,partial
tests/tis-aggregate/main.c,main,13,15,87%,partial
tests/tis-aggregate/convert.c,nb_digit,14,14,100%,total
TOTAL (functions),,7,7,100%,
TOTAL (all statements),,84,93,90%,
TOTAL (stmts in reachable functions),,84,93,90%,

The csv format may be useful to be opened in a spreadsheet tool for easy selection of elements.

When using --format=html, the coverage is represented with a decomposition based on the file paths. It makes it easier to browse the results. The presentation is interactive making it possible to fold/unfold the information. The default is to show only the summary of the coverage on the files and functions. It is also possible to see the detailed coverage of each statement by using the --html-stmts dir option provided the analysis was run before with:

$ tis-analyzer -aggreg-html-stmts dir [options]

It generates an HTML file for each function in the specified dir directory. So for instance, with these commands, the HTML detailed coverage is available from the results/html-cov/index.html file:

$ tis-analyzer -val -slevel 100 convert.c main.c -val-args ' 1234 10' \
   -info-csv-all results/test-1234-10 -aggreg-html-stmts results/html-cov
$ tis-aggregate coverage convert.aggreg.index \
                --format=html --html-stmt results/html-cov

The -aggreg-html-stmts option may be used several times: previously existing files are overwritten to make sure the more recent version is available. Notice that it is not mandatory to use -aggreg-html-stmts on each analysis, but the detailed coverage is then available only on the functions that have been translated, i.e. on those which have been seen in the analyses where -aggreg-html-stmts have been used.

Moreover, whatever the format is, the output file may be specified with the --output-file option (except when using --html-stmts dir where the output file is automatically dir/index.html).

To know more about the other features of the coverage command, read the Tis-aggregate coverage section below, or use:

$ tis-aggregate coverage --help

The tis-aggregate tool also provides other commands. The help command shows the available commands and the list of the options that are common to all of them:

$ tis-aggregate help

The following Advanced usage section presents some of them.

Advanced usage

Tis-aggregate coverage

The Basic usage section above already explained how to use the coverage command, but some more details are given below.

Dead statements

To better understand the coverage, the dead code (i.e. the unreachable statements) needs to be analyzed. The easiest way to do that is to use the GUI, where the dead statements are highlighted in red, but it can be difficult to make a synthesis of the dead code over several analyses. So tis-aggregate can be used to generate the list of the statements that are not reached by any analysis.

With the --statements option, the list of the statements is filtered to keep only the unreachable statements. A path/base_statements.dead.xxxxxx.csv file (where xxxxxx is a random string) is generated. It holds information about these statements that are never reached by any analysis.

On the example below, it gives for instance:

Result of: tis-aggregate coverage convert2.aggreg.index --statements
File                                  Function        #reached  #statements  Ratio  Comment  
tests/tis-aggregate/main.c            __tis_globfini  2         2            100%   total    
tests/tis-aggregate/convert.c         convert         9         11           82%    partial  
tests/tis-aggregate/convert.c         convert_atoi    19        19           100%   total    
tests/tis-aggregate/convert.c         cv_to_base      23        27           85%    partial  
tests/tis-aggregate/convert.c         digit_name      4         5            80%    partial  
tests/tis-aggregate/main.c            main            13        15           87%    partial  
tests/tis-aggregate/convert.c         nb_digit        14        14           100%   total    
TOTAL (functions)                                     7         7            100%            
TOTAL (all statements)                                84        93           90%             
TOTAL (stmts in reachable functions)                  84        93           90%             
File, Line, Function, Number
tests/tis-aggregate/convert.c, 28, digit_name, 2
tests/tis-aggregate/convert.c, 31, cv_to_base, 22
tests/tis-aggregate/convert.c, 42, cv_to_base, 23
tests/tis-aggregate/convert.c, 42, cv_to_base, 24
tests/tis-aggregate/convert.c, 42, cv_to_base, 25
tests/tis-aggregate/convert.c, 51, convert, 7
tests/tis-aggregate/convert.c, 51, convert, 8
tests/tis-aggregate/main.c, 26, main, 2
tests/tis-aggregate/main.c, 27, main, 3

Filters

Some options are provided to decide which functions should appear in the coverage results.

For instance, the coverage of the libc functions is usually not interesting to have, so the default is to ignore them, but they can be included when the --libc option is set.

The default behavior is to show the unreachable functions, but they can be skipped by setting the --skip-unreachable-fun option. It is especially useful when using the --libc option.

This is for instance the coverage computed on the first convert.aggreg.index index file shown above, without the unreachable functions:

Result of: tis-aggregate coverage convert.aggreg.index --skip-unreachable-fun
File                                  Function        #reached  #statements  Ratio  Comment  
tests/tis-aggregate/main.c            __tis_globfini  2         2            100%   total    
tests/tis-aggregate/convert.c         convert         7         11           64%    partial  
tests/tis-aggregate/convert.c         convert_atoi    15        19           79%    partial  
tests/tis-aggregate/convert.c         cv_to_base      22        27           81%    partial  
tests/tis-aggregate/main.c            main            10        15           67%    partial  
tests/tis-aggregate/convert.c         nb_digit        12        14           86%    partial  
TOTAL (functions)                                     6         6            100%            
TOTAL (all statements)                                68        88           77%             
TOTAL (stmts in reachable functions)                  68        88           77%             

Notice that the function coverage is now 100% since the unreachable functions are filtered out, but it might not always been the case when using the -val-use-spec option for instance.

The --skip-file and --skip-function options take a regular expression and specify the files or functions that should be skipped in the results. For example:

Result of: tis-aggregate coverage convert.aggreg.index --skip-function main
File                                  Function        #reached  #statements  Ratio  Comment      
tests/tis-aggregate/main.c            __tis_globfini  2         2            100%   total        
tests/tis-aggregate/convert.c         convert         7         11           64%    partial      
tests/tis-aggregate/convert.c         convert_atoi    15        19           79%    partial      
tests/tis-aggregate/convert.c         cv_to_base      22        27           81%    partial      
tests/tis-aggregate/convert.c         digit_name      0         5            0%     not reached  
tests/tis-aggregate/convert.c         nb_digit        12        14           86%    partial      
TOTAL (functions)                                     5         6            83%                 
TOTAL (all statements)                                58        78           74%                 
TOTAL (stmts in reachable functions)                  58        73           79%                 

The --skip-file option may be used to exclude all the functions that come from some files. For instance:

--skip-file '^lib'

Advice about the source code

Warning

Because the coverage rely on the statement number inside the function, it is relevant only for the functions that have exactly the same statements in all the analyses, which means that, if different preprocessing options are used, they must not change that function source code.

However, some analyses may hold only part of the source code: the statements of the functions that are not in some analyses results are considered as if they were present but dead.

Despite the warning above, if some functions really need a different code for some analyses, one should follow the advice presented below to nonetheless get usable coverage results.

Conditional statements

When adding a conditional statement, a #else part with the same number of statements should be added so that the other statements of the function keep the same number across the analyses. For instance:

#ifdef TEST_1
  tis_variable_split (&x, sizeof(x), 10);
# else
  ;
#endif
  <statement>
Two versions of the same function

It is sometimes the case when two versions of the same function are needed for some analyses. In this case, instead of redefining the function like this:

#ifdef CONFIG_1
int f (...) {
  <code 1>
}
#else
int f (...) {
  <code 2>
}
#endif

It is better to define two functions to make them visible in all the analyses. The conditional code is only used to call one or the other:

int f_config_1 (...) {
  <code 1>
}
int f_other_config (...) {
  <code 2>
}
int f (void) {
#ifdef CONFIG_1
  return f_config_1 (...);
#else
  return f_other_config (...);
#endif
}

Adding Justifications

Optionally, the --justif option can be used to provide a file with some justifications for partially covered functions.

Each line of this file must be formatted as:

function_name, number of justified dead statements, justification

The free text in justification can be anything, but cannot contain a newline nor a comma (in order to produce a well-formed CSV file).

This file is useful when doing the verification several times to check whether the number of unreachable statements has changed since the last time the results have been reviewed.

For instance, for the example presented above, the justification file may look like:

File convert.justif holding some dead code justification:
main, 2, no test with wrong number of arguments.
convert, 2, no test with invalid char in second input.
digit_name, 1, always called with `x>=10`.

And then the coverage result becomes:

Result of: tis-aggregate coverage convert.aggreg.index --justif convert.justif
File                                  Function        #reached  #statements  Ratio  #justified  Ratio  Comment                                     
tests/tis-aggregate/main.c            __tis_globfini  2         2            100%   0           100%   total                                       
tests/tis-aggregate/convert.c         convert         9         11           82%    2           100%   no test with invalid char in second input.  
tests/tis-aggregate/convert.c         convert_atoi    19        19           100%   0           100%   total                                       
tests/tis-aggregate/convert.c         cv_to_base      23        27           85%    0           85%    partial                                     
tests/tis-aggregate/convert.c         digit_name      4         5            80%    1           100%   always called with `x>=10`.                 
tests/tis-aggregate/main.c            main            13        15           87%    2           100%   no test with wrong number of arguments.     
tests/tis-aggregate/convert.c         nb_digit        14        14           100%   0           100%   total                                       
TOTAL (functions)                                     7         7            100%   0           100%                                               
TOTAL (all statements)                                84        93           90%    5           96%                                                
TOTAL (stmts in reachable functions)                  84        93           90%    5           96%                                                

Tis-aggregate property-status

Beside the Prepare the Analysis that shows how to run tis-analyzer commands to get Value analysis results, the ACSL Properties section shows how to add some properties in the code to solve some problems, and how some of them can be proven using the WP plugin that involves theorem prover techniques (see Prove Annotations with WP).

As pointed out by the Conclusion of the TrustInSoft Analyzer Manual, all the results obtained by the analyses rely on hypotheses, and the code annotations are a large part of them. The property-status command helps to detect the annotations that are not verified by computing the status of each property across several analyses. To get an ok status, a property has:

  • either to be valid (or dead) in every value analysis results,
  • or to be proved by WP,
  • or to be said to be manually reviewed (see About property reviews).

Index

We have seen in Basic usage that the index file holds the list of the base names of the analyses results. The property-status command also needs to know where the results come from. So an optional second column has to be added to specify the kind of analysis that gave the results. It can be value, wp or other. A missing kind is equivalent to other. The property-status command only consider the value and wp results. So the index file may look like:

path_1/proj_1
path_2/proj_2, value
path_2/proj_3, wp
...
path_n/proj_n

With the enhanced index file, the command may be run with:

$ tis-aggregate property-status appli.aggreg.index

To know more about the available property-status options, see the sections below or run:

$ tis-aggregate property-status --help

About property reviews

Some properties may be difficult to prove with the tools, so the user may prefer to justify them manually. The format of the file holding the intellectual review is not constrained, but it has to be a text file where the string [#justif-yyy:xxx] specifies that the property named xxx from the yyy function has been justified.

The file is provided to the tool with the --reviews option.

About property suffixes

Optionally, if the user follows the recommendations given in Naming the Annotations, i.e. takes care of adding a suffix to the property names, the --check-suffix option may be used to make the tool check if the computed status match the given suffix.

The default suffixes are:

  • _wp for properties that should be proved with WP (use the --wp-suffix to override it),
  • _val for properties that should be checked by the Value analysis (use the --val-suffix to override it),
  • _rv for properties that should be in the intellectual reviews (use the --review-suffix to override it),
  • the --ignore-suffix option can be used to specify a suffix to ignore, like _todo for instance.

Output

The default behavior of this command is to print the list of the properties that are not verified (according the criteria listed above). However, with the --all option, all the properties will be listed with information about their verification (and optionally information about the suffixes).

At the end of a study, it might be the case that some useless elements remain. For instance, if a property is valid in every analysis, it is useless to take some time proving it with WP. And if a property is valid in every analysis, or if it has been proved by WP, it is useless to keep a manual justification for it. When the --show-useless option is set, some warnings are generated for such useless elements and may help to clean the final results.

Tis-aggregate sql-export

As seen in the tis-info Manual, the .csv files generated when using the -info-csv-all option can be used to explore the results of an analysis. But if you are familiar with SQL, it might be easier to use it to make more elaborated requests over several .csv files.

The sql-export command generate a sqlite database:

$ tis-aggregate sql-export appli.aggreg.index name

The appli.aggreg.index file is the index file as usual, and name is one of the analysis of the index. This second argument is needed because the database is generated only for one analysis at the moment.

Use the --help option to have for more information about this command, and to see examples.