In the previous post, we used analysis-scripts to prepare our analysis of Recommender. In this post, we will run EVA on the code and see how the iterative refinement of the analysis can be done. We assume the reader has performed all of the steps in the previous post, and is currently in the directory containing the GNUmakefile created previously.

Running the first EVA analysis

Running make main.eva will run the EVA plug-in in the console, and then output some metrics information. This is useful for scripts and experienced users. For now, running make main.eva.gui is more useful: it will run the analysis and then open the results in the GUI.

A *.{parse,eva}.gui target in analysis-scripts only run parsing/EVA if necessary; if it has already been run, and no source files or analysis parameters were modified, it will directly open the GUI.

In the GUI, in the Properties panel (you have to click Refresh after loading the GUI) if we inspect only Unknown/Invalid properties, we will notice 148 of them, several related to finiteness of floating-point values, as well as many related to variable initialization.

Note that the results of each analysis are stored in the main.eva directory, and also copied to a timestamped directory in the form main_YYYY-MM-DD_hh-mm-ss.eva. Thus main.eva always contains the latest analysis, while the timestamped copies are useful to retrieve past results and compare them, e.g. using meld's folder comparison view.

Iterating on EVA analyses

Let us use the Loop Analysis plug-in to obtain more precise results. Since analysis-scripts already created a Frama-C save file (extension .sav by default), we just need to load it and add -loop:

frama-c -load main.eva/framac.sav -loop > main.slevel

Open the main.slevel file with a text editor. It contains the output of the Loop Analysis plug-in: some informative text, and then a line that says:

[loop] Add this to your command line:

Followed by several command-line arguments related to the use of slevel. Let us erase everything up to and including the Add this ... line, and then include the file contents in the EVAFLAGS variable of our GNUmakefile:

EVAFLAGS    += $(shell cat main.slevel | tr '\\' ' ')

Note that we use the tr command-line utility to remove the backslashes from the output of Loop Analysis.

If we re-run make main.eva.gui, the dependencies managed by Make will re-run the analysis because its command-line changed, but not the parsing, since it was not impacted.

This time, we obtain 114 unknown/invalid properties.

Appeal to brute-force

Since this is a test case that runs very quickly, and because Loop Analysis' heuristics are not perfect, we can allow ourselves to try a somewhat aggressive -slevel. Let us remove the heuristics given by Loop Analysis, and instead use a global slevel of 500:

EVAFLAGS    += -slevel 500

The reason why we remove Loop Analysis' results is that, in some cases, it forces merging of states to avoid slowing down the analysis, and those settings take precedence over the global slevel.

The analysis will be much longer this time, but should still terminate in a few seconds. Given such a high slevel, we are lucky that it terminates at all. We will obtain 86 unknown/invalid properties this time.

Extra hypotheses for more precision

There are several options in EVA that allow a more precise analysis of less-than-ideal code that can be found in the wild. Most of them require knowing some details about the semantics of C, but others can be used more leniently, to help get a better idea of the code under analysis, before some serious analysis time is spent. One of them is -no-val-malloc-returns-null. This option is only useful when the code contains dynamic memory allocation, and what it does is to consider that memory allocation never fails.

By default, the memory allocation built-ins used by EVA suppose that memory allocation can fail, as stated in the standard (i.e. malloc can return NULL, for instance when there is not enough available memory). However, many code bases fail to test for such cases; which is admittedly a relatively rare situation, especially on a system that allows memory overcommitment. The -no-val-malloc-returns-null thus adds a new hypothesis to the underlying analysis ("... and considering that memory allocation never fails..."), in exchange for a more precise result.

In Recommender, we notice that there are some spots where malloc is tested for NULL (e.g. in src/learned_factors.c:47), but others where no such test is performed (e.g. in src/learned_factors.c:67). Thus adding this option should (hopefully) result in fewer alarms. Our EVAFLAGS line becomes:

EVAFLAGS    += -slevel 500 -no-val-malloc-returns-null

Indeed, running the analysis again results in only 56 unproved properties. However, it also reveals another issue.

Tracking red alarms

Opening in the GUI the result of the last iteration of the analysis, if we scroll through the main function, we see that the analysis has stopped (became red) before returning from the call to recommend_items. Jumping to its definition, we see a loop where j should go from 0 to 2 (the value contained in (estim_param->tset)->items_number)), but inspecting the value of j in the while condition shows {0; 1}. This means that the third iteration never took place, its trace cut short by some evaluation that resulted in a definitely invalid property.

There are several ways to proceed here:

• One can follow the "red path" in the GUI, jumping inside reachable functions in the GUI until the limit of the red path is found;

• Alternatively, in this case we have a warning (in the Messages tab) that says that all target addresses were invalid, which often indicates an issue with the evaluation of a state;

• Finally, one can prioritize alarms in the Properties tab, by checking only Invalid properties at first, before including Unknown ones.

In this case, all three would end up around the same source line (src/binary_heap.c:153), though this is not always true.

Spoiler alert: the Chlorine 17 release of Frama-C will include an extra panel, Red alarms, which will provide another way to get to properties that warrant extra attention when starting an analysis.

Note that, whenever the C code contains calls to assert(), Frama-C generates a call to __FC_assert whose precondition is requires \false. This leads to an Invalid alarm in the Properties panel, however this does not indicate that the source code necessarily has undefined behavior: it may be due to an imprecision in the assertion condition, which if possibly true, leads to the call being made, which will itself definitely indicate an error. But if the call may not happen, then the assertion should be treated like an Unknown alarm.

Spoiler alert: in Frama-C Chlorine (17), the behavior of assert will be changed to more closely match the usual approach: an Invalid alarm will only be generated when the assertion is definitely violated.

Back to the Invalid alarm: if we inspect the source code in question, we will see that the only valid index for the buffer bheap->buffer is 0, due to the ACSL assertion inserted by EVA:

/*@ assert Value: index_bound: bheap->filled_elements < 1; */
bheap->buffer[bheap->filled_elements] = value;

However, filled_elements is 1 in this call, which seems like an error. But why is it there? While it is impossible to know exactly the intent of the author of the code, by inspecting the definition of the buffer, we can obtain some clues. In the Information panel, if we inspect bheap, we see that:

Variable bheap has type `binary_heap_t *'.
It is a formal parameter.
It is referenced and its address is not taken.

And then if we click binary_heap_t itself, we obtain its type information:

Type information for `binary_heap_t':
(sizeof 16, defined at src/binary_heap.h:53)
 struct binary_heap {
    size_t max_size ;
    size_t filled_elements ;
    int (*value_comparer)(void const *, void const *) ;
    void *buffer[1] ;
 };

Finally, clicking the source line will take us to the definition in the binary_heap.h header, which contains some useful comments:

/*
 * binary_heap:  The heap is tree based data structure
 *
 * Members:
 *   max_size        The number of elements in the binary heap
 *   filled_elements The number of inserted elements so far
 *   buffer          The buffer is a dynamically allocated array
 *                   containing the heap's elements
 *
 */
typedef struct binary_heap
{
  size_t          max_size;
  size_t          filled_elements;
  bh_value_cmp    value_comparer;
  void*           buffer[1];
} binary_heap_t;

From the comment, it seems that the code is implementing the pattern of a flexible array member, where the last element of the binary_heap_t structure should be an incomplete array type. However, its current declaration corresponds to that of a fixed-size array, which according to the C standard cannot be accessed beyond its static bounds. We can fix this by using the proper flexible array member notation defined in the C99 standard.

Syntactic fixes

By replacing void* buffer[1]; with void* buffer[]; in src/binary_heap.h, we define a proper flexible array member. As a consequence, the code can access all elements of the dynamically-allocated array, as long as enough memory has been allocated for them.

You may notice that, after modifying the .h file and re-running make main.eva.gui, Make will not re-parse nor re-run the analysis, it will simply open the GUI again. This is because the .h file dependencies are not tracked by the Makefile rules: they were never included in the list of .c sources of main.parse (because such headers are directly included via preprocessor directives), so Make has no way to know about these implicit dependencies. You can remedy that by forcing Make to unconditionally make all targets, adding -B to the command line arguments.

After doing so, everything is recomputed, and we obtain … almost the same alarm.

This time, the alarm happens on the third iteration of the loop, instead of the second one: progress! … But not much. There is still a problem when accessing the last element of the array. To find out why, we can use the GUI again. However, this time the Invalid alarm is no longer present; the problem is more subtle. Still, the warning about all target addresses were invalid is still there. It points to this statement:

    /*@ assert
        Value: mem_access: \valid(&bheap->buffer[bheap->filled_elements]);
    */
    bheap->buffer[bheap->filled_elements] = value;

By inspecting bheap->filled_elements, we see its possible values were {1; 2} before the statement, but {1} afterwards. This indicates that index 2 is not valid for this memory access. But why? We can check the location being accessed, to see its validity.

If we inspect the values for bheap, we see, in the Values tab:

bheap -> {{ (binary_heap_t *)&__malloc_init_binary_heap_l42 }}

Then, if we left-click on __malloc_init_binary_heap_l42, the Information panel will display some extra lines about this value in particular, with a clickable link pointing to its syntactic information. Clicking on that link will display the type of the dynamically allocated block:

Variable __malloc_init_binary_heap_l42 has type `char [23]'.

For dynamically allocated bases, EVA does not always have access to the original type intended for the allocated base, so it uses heuristics to restore that information. When such heuristics fail, it resorts to the "catch-all" char [].

"23" is a somewhat unusual size (not a multiple of the word size). Let us investigate where that number came from.

Using Studia

Right-clicking on __malloc_init_binary_heap_l42, in the Information tab, will display a context menu, the same one as if we had right-clicked some lvalue on the Cil code. We will use the Studia plug-in, in particular its Writes feature, to identify all points in the source code where this memory location was written prior to the statement indicated by the warning.

Studia will compute and highlight the statements in the code, and also add an extra column to the filetree display (upper left corner in the GUI), indicating all functions directly writing to the memory location (indicated by a 'tick' symbol in the Studia column) and the functions indirectly writing to it, that is, the callers of the former (indicated by an arrow symbol in the Studia column) as well as their own callers, recursively.

The functions writing to buffer are: balance_heap, init_binary_heap and insert_binary_heap. The first and the last write to fields in the buffer structure, but only init_binary_heap actually allocated the memory.

Well, I guess you could have directly inferred that from the variable name, which serves this exact purpose, but then I wouldn't have had an excuse to shamelessly plug Studia, one of the new features in Frama-C 16 Sulfur, would I?

Inside init_binary_heap lies our answer: the computation of the size of the bheap includes a -1, which is due to the fact that the non-flexible array member notation already had a byte allocated for the array, but our proper C99-compatible version no longer includes this byte. So the malloc'ed memory was 1 byte shorter, which led to the invalid memory access. So all we have to do is to fix the computation here (and take note of the fact that modifying other people's code without properly understanding it can lead to bugs).

At last … unable to progress

This time, we re-run the analysis (no need to use -B this time, since the .c file is tracked in the dependencies of our GNUmakefile), expecting to triumph over the syntactic distractions. However, we are greeted with a somewhat unpleasant surprise:

src/binary_heap.c:118:[value] warning: detected recursive call
    (balance_children <- balance_children :: src/binary_heap.c:135 <-
                         pop_binary_heap :: src/recommender.c:95 <-
                         recommend_items :: test/test.c:108 <-
                         main)
    Use -val-ignore-recursive-calls to ignore (beware this will make the analysis
    unsound)
[value] user error: Degeneration occurred:
    results are not correct for lines of code that can be reached from the degeneration point.

We should have seen it coming: binary heaps are fond of recursion. Our coverage did improve from the previous analysis (from about 75% to about 85%), but we now hit a harder obstacle. To deal with this, we'll have to stub the balance_children function, possibly over-approximating its behavior, or rewrite an equivalent, iterative version of the function. In either case, such transformations are out of the scope of this tutorial.

Conclusion and bonus features

In this tutorial, we showed how to use analysis-scripts, presenting most of its features in a quick usage scenario. There are still a few tricks up its sleeve which were not mentioned:

• flamegraph.txt: this file is computed by option -val-flamegraph, and it produces a Flamegraph of the analysis performed by EVA. This graph is useful when profiling larger case studies, to quickly visualize where the analysis is spending most of its time. This can indicate functions where less slevel or ACSL stubs might help.

• metrics.log: its output is displayed after running a .eva target. The coverage estimation is a quick indicator of progression in the analysis during the refining stage, i.e. sometimes when an analysis is made more precise, the number of alarms may actually increase, and the reason may be that the coverage has improved, so that more code is actually being analyzed, which might explain why now there are more alarms.

• alarms.csv: a CSV report with the same contents of the Properties panel in the GUI, obtained via the Report plug-in. Very useful for scripts.

• stats.txt: similar to the one present in the .parse directory; however, since parsing is usually very fast when compared to an EVA analysis, this version of the file is the one that is actually useful most of the time. In particular, if you want to compare the execution time of a new parameterization of the analysis, you just need to look at the user_time line. Very useful when you realize you forgot to type time make instead of make.

We hope this tutorial was useful to you and that the next Frama-C release will make things even easier! Don't forget to check some usage examples in open-source-case-studies, and please consider proposing your own case studies via Github issues.

Frama-C 15 (Phosphorus) has been released, and the OPAM package is already available! A MinGW-based OPAM package, distributed by fdopen's MinGW OPAM repository, is also available.

In this post, we briefly highlight two new features in this release. We also announce the release of a new Github repository, open-source-case-studies, which contains some snapshots of code bases ready to be analyzed with Frama-C/EVA.

Highlighted new features

E-ACSL in the default release

One notable change in this release is the direct integration of E-ACSL: instead of having to install OPAM packages frama-c and frama-c-e-acsl, you only need to install frama-c.

E-ACSL enables runtime verification in Frama-C, serving as an efficient tool for detecting undefined behavior and for debugging ACSL specifications. It can be used in a "stand-alone" mode (e.g. with assertions generated by the RTEgen plug-in), or in combination with EVA, in which case its instrumentation is more efficient: EVA only generates ACSL assertions for the properties that it cannot prove, thus greatly reducing E-ACSL's instrumentation.

Note that, due to the usage of jemalloc and some technical details, E-ACSL is disabled by default in Mac and Windows.

Better pretty-printing of #include directives

One of the drawbacks of the -print option of Frama-C was the fact that the code was entirely preprocessed, expanding a Hello world example to several hundreds of lines, due to the expansion of #include <stdio.h> and derived files.

There are now two options, -print-libc and -no-print-libc (the latter is enabled by default) which control the folding/unfolding of #include directives in pretty-printed code. More specifically, if your original code is:

#include <stdio.h>

int main() {
    printf("hello world!\n");
    return 0;
}

Then the result of -print will be:

/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
/*@ requires valid_read_string(format);
    assigns \result, __fc_stdout->__fc_FILE_data;
    assigns \result
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
    assigns __fc_stdout->__fc_FILE_data
      \from (indirect: __fc_stdout->__fc_FILE_id),
            __fc_stdout->__fc_FILE_data, (indirect: *(format + (0 ..)));
 */
int printf_va_1(char const *format);

int main(void)
{
  int __retres;
  printf_va_1("hello world!\n");
  __retres = 0;
  return __retres;
}

There are two interesting things to notice here:

1. Some #include directives are present at the beginning of the file. These directives correspond to all files from the Frama-C standard library whose identifiers were present in the (expanded) original code. For instance, errno.h is present because Frama-C's stdio.h includes it. As you can see, the mechanism does not guarantee a minimal number of includes, but it is much cleaner than having all files expanded;

2. The specification of printf_va_1 is visible. This is due to the fact that the Variadic plug-in (which is enabled by default on Frama-C 15 (Phosphorus)) generated this specification - it is not part of the standard Frama-C library. In fact, printf_va_1 is a specific instantiation of the variadic printf function. You can disable the automatic variadic translation with -variadic-no-translation, in which case -print will result in:

/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
#include "stddef.h"
#include "stdio.h"
int main(void)
{
  int __retres;
  printf("hello world!\n");
  __retres = 0;
  return __retres;
}

The Phosphorus release also includes, as usual, a series of bug fixes and minor improvements. Consult the Changelog for more details.

Open source case studies

A new Github repository on the Frama-C organization, open-source-case-studies, has been created to help users quickly run Frama-C (and EVA in particular) in more realistic code bases, which includes different sorts of open-source code; some of them are very small (a single file) while others contain significantly larger bases. Their usage is very simple: once you have installed Frama-C and put it in the PATH, enter one of the case study directories and run:

• make to parse and run EVA;

• make <target>.eva.gui to open the Frama-C GUI and view the results.

The target names vary on each case study, and can be obtained via make help. Note that this will show only the base target name, from which other targets are derived (e.g. <target>.parse, <target>.eva, <target>.eva.gui).

All case studies include a Makefile, which uses the files in fcscripts to generate targets and Makefile rules to allow running EVA quickly. Among the facilities provided by these scripts, we highlight:

• templates for Frama-C parametrization (i.e. variables CPPFLAGS, FCFLAGS and EVAFLAGS to delineate which options are related to preprocessing, parsing and running EVA), including helpful default parameters;

• automatic target dependencies on command line arguments: Frama-C reparses files only when they are modified, and re-runs EVA only when command line arguments change;

• saving of intermediate results in directories (for easy comparison via Meld), to run other plug-ins without having to re-run EVA (e.g. frama-c -load <target>.eva/framac.sav ...).

Note, however, that there are some caveats concerning this repository:

1. It is not representative of the scale of programs that Frama-C/EVA can handle; indeed, all large code bases where Frama-C/EVA is applied consist in industrial code that cannot be shared;

2. One of the main purposes of the repository (internally) is to serve for non-regression testing, which means that some analyses are not fully parametrized;

3. Some case studies include code that is not ideally dealt with by EVA, but may be useful for other plug-ins.

Those caveats aside, we hope this repository will give practical examples and help you to parametrize your own analyses. If you also have some interesting open source code bases on which to run EVA, you can submit them to us as a Github pull requests. This will make it easier to compare the behavior of future versions of Frama-C on such code, and to benefit from improvements in the analyzer.

On the previous post we've seen some recommendations about using Frama-C/EVA, and some tips about parsing. In this post, we will see how to run EVA, and how to quickly setup it for a more precise result.

We will reuse the save file produced at the end of the parsing, parsed.sav.

First run of EVA

The default parameters of EVA are intended for a fast analysis. In Frama-C 14 (Silicon), option -val-builtins-auto is recommended to enable the usage of built-in functions that improve the precision and sometimes the speed of the analysis¹.

¹ This option will be enabled by default in Frama-C 15 (Phosphorus).

The following command-line should result in a relatively quick first analysis:

frama-c -load parsed.sav -val-builtins-auto -val -save value.sav

Note that we save the result in another file. It can be reused as input for another analysis, or visualization in the GUI.

The analysis will likely output many alarms, some due to loss of precision, others due to an incorrect setup. Here are a few important alarms concerning an incorrect setup:

1. Missing code or specification

   file.c:42:[kernel] warning: Neither code nor specification for function foo, generating default assigns from the prototype
   

   There are two major causes for this warning: (1) the file containing the function definition was not given to Frama-C during parsing; or (2) the function has no source code and no ACSL specification was given.

   In the first case, the solution is to include the missing source file. Parsing will succeed even if only a declaration (function prototype) is present, but EVA requires more than that. It may be necessary to return to the parsing stage when this arrives.

   In the second case, you must supply an ACSL specification for the function, otherwise EVA will assume it has no effect, which may be unsound. To do it with minimal modifications to the original code, you can do the following:

   1. create a file, say stubs.h;
   2. copy the function prototype to be stubbed in stubs.h (adding the necessary #includes for the types used in the prototype);
   3. add an ACSL specification to this prototype;
   4. include stubs.h in the original source, either by adding #include "stubs.h", or using GCC's -include option (e.g. -cpp-extra-args="-includestubs.h", without spaces between -include and the file name).

2. Missing assigns clause, or missing \from

   When analyzing functions without source code, EVA imposes some constraints on the ACSL specification: they must contain assigns clauses, and these clauses must have \from dependencies. Otherwise, warnings such as the following may be generated:

   foo.c:1:[value] warning: no 'assigns \result \from ...' clause specified for function foo
   foo.c:3:[value] warning: no \from part for clause 'assigns *out;' of function foo
   foo.c:6:[kernel] warning: No code nor implicit assigns clause for function foo, generating default assigns from the prototype
   

   The following is an example of an incomplete specification:

   /*@ assigns *out; */
   void foo(int in, int *out);
   

   Even if it contains an \assigns clause for pointer out, it does not say where the result comes from. Adding \from in, for instance, makes the specification complete from the point of view of EVA.

   Note: EVA cannot verify the correctness of the specification in the absence of code, especially that of ensures clauses. If you provide an incorrect specification, the result may be unsound. For that reason, it is often useful to write a simplified (or abstract) implementation of the function and then run the analysis. If EVA has both the code and the specification, it is able to check ensures clauses and detect some kinds of errors.

Running EVA on monocypher

Running EVA on parsed.sav will start the value analysis on the main function defined in test.c. Due to the large number of small functions in Monocypher, EVA will output a huge amount of lines, whenever a new function is entered. Adding option -no-val-show-progress will omit messages emitted whenever entering a new function.

Also, the fact that this code contains lots of small functions with few or no side-effects is a very strong indicator that -memexec-all will be very helpful in the analysis.

Memexec, which is part of EVA, acts as a cache that allows reusing the result of function calls when their memory footprint is unchanged. It dramatically improves performance.

Combining both options, we obtain the following command-line:

frama-c -load parsed.sav -val -val-builtins-auto \
        -no-val-show-progress -memexec-all -save value.sav

The analysis will then start and emit several warnings (mainly due to imprecisions). It should finish in a few seconds, depending on your processor speed.

Improving EVA results

After running the value analysis, it is a good time to check what the result looks like, using the GUI:

frama-c-gui -load value.sav

In the screenshot below, we indicate some parts of the GUI that are useful when inspecting EVA results (besides the source view). We also indicate some parts that are never (or rarely) used with EVA.

Note that the Properties tab (between Console and Values) is not updated automatically: you need to click on the Refresh button before it outputs anything, and after changing filters.

Several tips concerning this panel were presented in a previous post about the GUI. If you follow them, you will be able to make the Properties panel show the total of Unknown (unproven) properties for the entire program, and only those. This number is often similar to the number of messages in the Messages panel.

In Monocypher, after setting the filters to show every Unknown property in the entire program, and clicking Refresh, we obtain over 900 unproven properties. Since the analysis was not tuned at all for precision (other than with -val-builtins-auto), this number is not particularly surprising.

A quick way to improve on results is to use the Loop analysis plug-in.

The Loop analysis plug-in performs a mostly syntactic analysis to estimate loop bounds in the program (using heuristics, without any soundness guarantees) and outputs a list of options to be added to the value analysis. Running EVA again with these options should improve the precision, although it may increase analysis time. Loop analysis' main objective is to speed up the repetitive task of finding loop bounds and providing them as semantic unrolling (-slevel) counters. The analysis may miss some loops, and the estimated bounds may be larger or smaller, but overall it minimizes the amount of manual work required.

Loop analysis does not depend on EVA, but if it has been run, the results may be more precise. In Monocypher, both commands below give an equivalent result (the difference is not significative in this context):

frama-c -load parsed.sav -loop
frama-c -load value.sav -loop

In both cases, Loop analysis' effect is simply to produce a text output that should be fed into EVA for a new analysis:

[loop] Add this to your command line:
       -val-slevel-merge-after-loop crypto_argon2i \
       -val-slevel-merge-after-loop crypto_blake2b_final \
       ...

You should, by now, use a shell script or a Makefile to run the Frama-C command line, adding all the -val-slevel-merge-after-loop and -slevel-function lines to your command.

Let us consider that the environment variable LOOPFLAGS contains the result of Loop analysis, and EVAFLAGS contains the flags mentioned previously (-no-val-show-progress, -val-builtins-auto and -memexec-all). Then the following command will re-run EVA with a more detailed (and, hopefully, precise) set of parameters:

frama-c -load parsed.sav $LOOPFLAGS -val $EVAFLAGS -save value2.sav

Opening this file on the GUI will indicate approximately 500 warnings, which is still substantial, but much better than before. Improvements to Loop analysis in the next release of Frama-C will allow this number to be reduced slightly.

The basic tutorial is over, but there are several paths to choose

From here on, there are several possibilities to reduce the imprecisions in the analysis:

• Inspect alarms and see if their functions contain loops that were not inferred by Loop analysis; if so, adding their bounds to -slevel-function can improve the precision of the analysis;

• Increase the precision using other parameters, such as -plevel;

• Stub libc functions to emulate/constrain inputs when relevant;

• Use EVA's abstract domains (e.g. -eva-equality-domain) to improve precision;

• Stop at the first few alarms (-val-stop-at-nth-alarm), to track more closely the sources of imprecision. However, when there are hundreds of alarms, this is more useful as a learning experience than as a practical solution.

Each solution is more appropriate in a specific situation. Here are a few tips for an intermediate-level user of EVA:

1. Functions that perform array initialization are often simple (a loop with a few assignments per iteration), so unrolling them completely should not slow down the analysis excessively. The Loop analysis plug-in usually works with them, but some pattern variations may throw it off. You may want to check the proposed values in such loops. Because initialization happens early in program execution, checking such loops may yield good results.

2. The plevel parameter is often used in response to messages such as:

   monocypher.c:491:[kernel] more than 200(255) elements to enumerate. Approximating.
   

   where the first number is the current plevel (by default, 200), and the second number is the amount that would be required to avoid the approximation. In this case, -plevel 255 would be reasonable, but if you had more than 200(67108864) elements, for instance, it would not be helpful to set the plevel to such a high value.

3. Stubbing is a good approach when dealing with functions that are closely system-dependent, specifically input functions that read from files, sockets, or from the command-line. Check the Frama-C builtins in __fc_builtin.h, they provide some useful primitives for abstracting away code with non-deterministic functions.

4. EVA's domains have specific trade-offs between precision and efficiency, and some have broader applicability than others. Future posts in this blog will describe some of these domains, but as a rule of thumb, two domains that are fairly low-cost and generally useful are -eva-equality-domain (for syntactic equalities) and -eva-gauges-domain (for some kinds of loops).

5. The Messages panel in the GUI is chronologically sorted, so it can help the user follow what the analysis did, to try and identify sources of imprecision. However, even in this case, there is still an advantage to using -val-stop-at-nth-alarm: because the execution stops abruptly, there are possibly less callstacks displayed in the GUI, and therefore it may be easier to see at a glance which parts of the code were actually executed, and the dependencies between values that lead to the alarm.

Non-terminating function?

The "beginner" tutorial ends here, but one thing that you may have noticed after running EVA, is the dreaded "non terminating function" message at the end of the analysis:

[value:final-states] Values at end of function main:
  NON TERMINATING FUNCTION

This indicates that, somewhere during the analysis, a completely invalid state was found, and EVA could not proceed. This usually indicates one of the following:

1. EVA's setup is incorrect: most likely, some function has missing or incorrect specifications, or some case that cannot be currently handled by EVA (e.g. recursive calls) was encountered.
2. A definitively undefined behavior is present in the code, which may or may not lead to an actual bug during execution. In either case, it should be taken care of.

We will see how to handle such situations in the next post, using the GUI and the Nonterm plug-in (-nonterm), in a tutorial destined for beginners and experienced users alike.

Frama-C 14 (Silicon) has just been released. In this post, we present a few additions that should help everyday usage of Value EVA.

Value is now EVA

The Value analysis plug-in has been renamed EVA, for Evolved Value Analysis. It has a new architecture that allows plugging abstract domains, among other features. It is a truly remarkable evolution which this post is too small to contain¹, however, so it will presented in more detail later.

¹ Facetious reference to Fermat's Last Theorem

Automatic built-in matching for libc functions

One of the new user-friendly features is the -val-builtins-auto option, which avoids having to memorize which built-in to use for each libc function that has one, namely malloc, free, and some floating-point and string-related functions (e.g. pow and strlen).

For instance, consider the following toy program, which simply allocates a buffer, copies a string into it, then allocates a buffer of the right size for the string, and stores it there.

// file.c
#include <stdio.h>
#include <stdlib.h>
#include "string.c" // include Frama-C's implementation of string.h

int main() {
  char *buf = malloc(256); // allocate a large buffer
  if (!buf) exit(1);
  char *msg = "silicon";
  strcpy(buf, msg);
  size_t n = strlen(buf);
  char *str = malloc(n + 1); // allocate a buffer with the exact size (plus '\0')
  if (!str) exit(1);
  strncpy(str, buf, n);
  str[n] = 0;
  size_t n2 = strlen(str);
  //@ assert n == n2;
  free(str);
  free(buf);
  return 0;
}

This program uses dynamic allocation and calls functions from string.h.

The following command-line is enough to obtain an interesting result:

frama-c file.c -val -val-builtins-auto -slevel 7

Without -val-builtins-auto one would need to use this overly long argument:

-val-builtin malloc:Frama_C_alloc_by_stack,free:Frama_C_free,strlen:Frama_C_strlen

For more details about Frama_C_alloc_by_stack, check the EVA manual, section 8.1.

The builtins for free and strlen were automatically chosen by EVA. Note however that strcpy and strncpy do not have builtins. In this case, we include "string.c" (which is actually in share/libc/string.c) to use the implementations available with Frama-C.

Analyzing a program using the implementations in share/libc/string.c is less efficient than using a built-in, but more precise than using only a specification. These implementations are designed to minimize the number of alarms when their inputs are imprecise. Also, because they are not optimized for execution, they are conceptually simpler than the actual libc implementations.

Using these functions. -slevel 7 ensures that their loops are fully unrolled in the example. Can you guess why 7 is the right value here?

Inspecting values in the GUI

Another improvement to usability comes in the form of a popup menu in the GUI. To see it, run the following command using the same file as previously:

frama-c-gui file.c -val -val-builtins-auto -slevel 7

On the Frama-C GUI, click on the str expression in the statement str = (char *)malloc(n + (size_t)1); (corresponding to line 11 in the original source code). Then open the Values tab, and you will see something similar to this:

In the Values tab on the bottom, right-clicking on the cell containing the NULL; &__malloc_main_l11[0] value will show a popup menu "Display values for ...". Clicking on it will add a new column displaying its contents.

Before Silicon, this information was already available, but as the result of a long and painful process. The new popup menu shows one entry per pointed variable in the chosen cell, so if there are several different values, there will be several popup menu entries.

malloc may fail

In the previous example, the values of str are those returned by the malloc builtin: NULL and a newly allocated base (__malloc_main_l11). This models the fact that there may not be enough memory, and malloc may fail. The code should definitely handle this case! But for the hurried evaluator, the use of option -no-val-malloc-returns-null can help focus on the other potential run-time errors (before coming back to the malloc-related ones).

Still ways to go

In this example, there are still some warnings, due to the specification of functions strcpy and strncpy, which use logical constructs not yet evaluated by EVA (but very useful for WP). They are not an issue in this example, since we used the actual implementation of these functions, and therefore do not need their specifications, but future work on EVA will help deal with these details and provide a more streamlined experience.

In our previous post, we left you in a cliffhanger: which \from is missing from our ACSL specification for safe_get_random_char? In this post, we explain the functional dependencies in our specification, how to test them, and then present the missing dependency.

Where do the \from come from?

Our complete specification for safe_get_random_char in the previous post includes several functional dependencies. Some of them are obvious, others not so much. For easier reference, here is the specification once again:

#include <stdlib.h>
typedef enum {OK, NULL_PTR, INVALID_LEN} status;

/*@
  assigns \result \from out, buf, n;
  assigns *out \from out, buf, buf[0 .. n-1], n;
  behavior null_ptr:
    assumes out == \null || buf == \null;
    assigns \result \from out, buf, n;
    ensures \result == NULL_PTR;
  behavior invalid_len:
    assumes out != \null && buf != \null;
    assumes n == 0;
    assigns \result \from out, buf, n;
    ensures \result == INVALID_LEN;
  behavior ok:
    assumes out != \null && buf != \null;
    assumes n > 0;
    requires \valid(out);
    requires \valid_read(&buf[0 .. n-1]);
    ensures \result == OK;
    ensures \initialized(out);
    ensures \subset(*out, buf[0 .. n-1]);
  complete behaviors;
  disjoint behaviors;
 */
status safe_get_random_char(char *out, char const *buf, unsigned n);

As a reminder, assigns a \from b1, b2, ... specifies that there are control and/or data dependencies from b1, b2, ... to a. Data dependencies are direct or indirect assignments (e.g. a = b1 or c = b1; a = c), and control dependencies are related to control-flow (e.g. if (b1 && b2) { a = 1; } else { a = 2; }). Value uses them for several purposes, such as:

• precision: to define the possible origins of pointers, otherwise imprecise values will degenerate into "modifies anything";
• efficiency: to avoid recomputing the state during a leaf function call, if the only difference is in the values of variables that no one depends on.

Value always requires that assigns clauses contain \from dependencies. Since \from are an overapproximation of the actual dependencies, in case of doubt the safe bet is to include more than the necessary. Too many \from, however, may lead to imprecise analyses.

One way to consider whether a given location should be part of a \from is to think in terms of variation: if the actual value of the location changed, would it possibly affect the assigned lvalue? If so, then there is a dependency.

Let us revisit our first get_random_char function, in particular its assigns clause:

//@ assigns \result \from buf[0 .. n-1], n;
char get_random_char(char const *buf, unsigned n);

If we change the value of any character between buf[0] and buf[n-1], this can have a direct impact on the result. Changing the value of n obviously also has an effect: there are more characters to choose from.

However, one thing that does not affect the result is the address of buf itself, that is, the contents of the buf pointer: if the buffer starts on address 0x42, or on address 0xfffe1415, the result of the function is the same, as long as the precondition is valid (i.e., the memory location is readable) and the contents of the buffer are the same.

But why, then, do we have buf (the pointer, not the pointed value) as part of the \from in safe_get_random_char (copied below)?

//@ assigns \result \from out, buf, n;
status safe_get_random_char(char *out, char const *buf, unsigned n);

Note that out is also present as a dependency, and for the same reason: the NULL pointer. In our specification, we included assumes clauses such as out == \null || buf == \null. We may expect, therefore, that our function will be able to distinguish whether any of these pointers is null, very likely via a test such as the following:

...
if (out == NULL || buf == NULL) { return INVALID_LEN; }
...

Such a test introduces control dependencies between out, buf and \result: if out is 0, the result is different than if out is nonzero (i.e. non-null). For that reason, out and buf must be included as dependencies. Conversely, note that the contents of the buffer itself do not affect \result.

When in doubt, try some code

A good way to check a specification is (when possible) to write an abstracted code of the function under test, then run Value (and sometimes From) and see if it matches the expectations.

For safe_get_random_char, a few lines of code suffice to obtain a roughly equivalent version of our specification:

#include "__fc_builtin.h"
#include <stdlib.h>
typedef enum { OK, NULL_PTR, INVALID_LEN } status;

status safe_get_random_char(char *out, char const *buf, unsigned n) {
  if (out == NULL || buf == NULL) return NULL_PTR;
  if (n == 0) return INVALID_LEN;
  *out = buf[Frama_C_interval(0,n-1)];
  return OK;
}

Note the usage of the built-in Frama_C_interval (included via __fc_builtin.h) to simulate a random value between 0 and n-1 (inclusive).

Now we need a main function to invoke our code. We will reuse the one we defined before, since its calls activate all branches in our code. Re-running Value, this time using the code plus the specification, will prove all pre- and post-conditions, except the one related to \subset(*out, buf[0 .. n-1]). This is just an imprecision in Value that may disappear in the future.

We can also try running the From plugin (frama-c -deps), without our specification, to see if the dependencies it infers are compatible with the ones we specified in our assigns clauses.

For function safe_get_random_char, From will infer the following dependencies related to \result and *out:

  ...
  a FROM Frama_C_entropy_source; out; buf; n; "abc" (and SELF)
  \result FROM out; buf; n
  ...

Frama_C_entropy_source comes from the usage of Frama_C_interval. For now, let us focus on the other variables:

• a is actually *out, and "abc" is actually buf[0 .. n-1]. The result of the From plugin is very concrete, so we have to abstract a few variable names.
• the SELF dependence related to *out simply means that the variable may not be assigned in the function (e.g. when an error is found). This information is not present in assigns clauses. In particular, for Value it could be useful to have a "must assign" clause, describing an underapproximation of assignments that are certain to happen in every execution. This is not present in ACSL, but it can often be compensated with the use of behaviors with refined assigns and ensures clauses, as we did.
• all dependencies, both for *out and \result, are the ones we had predicted before, except for Frama_C_entropy_source.

Variables such as Frama_C_entropy_source are often used to represent internal states of elements that are abstracted away in specifications. In this case, it can be seen as the internal state of the (pseudo-)random number generator that allows the result of our safe_get_random_char to be non-deterministic. Without it, we would have a function that could be assumed to return the same value every time that the same input parameters were given to it.

Thus, to really model a randomized result, we need to add such a variable to our specification. It is important not to forget to also assign to the variable itself, to represent the fact that its own internal state changed during the call. In our specification, it would be sufficient to add the following line to the global assigns clause:

  assigns Frama_C_entropy_source \from Frama_C_entropy_source;

With this final assigns clause, our specification is indeed complete. This concludes our tutorial on ACSL specifications oriented towards an analysis with Value!

A minor variant, an unexpected result

Let us consider a minor variant of our specification: what if we remove the postcondition ensures \subset(*out, buf[0 .. n-1])? We would expect Value to return [--..--], since *out is said to be assigned by the function, but we did not specify which values it may contain. However, this is what we obtain instead, after the call to safe_get_random_char(&c, msg, len_msg):

  c ∈
   {{ garbled mix of &{c; "abc"} (origin: Arithmetic {file.c:44}) }}

This undesirable garbled mix indicates that some pointer information leaked to the contents of the variable c, more precisely, that the address of c (out) itself could be contained in c. We know this is not the case, since in every reasonable implementation of safe_get_random_char, the address of out is never directly assigned to *out. However, until Frama-C Magnesium, there was no way to specify the distinction between dependencies that may impact the actual contents of an lvalue from dependencies which are only indirectly related to its value (e.g. control dependencies, such as testing whether out is NULL or not).

Because of that limitation, there were typically two ways to deal with that: omit dependencies (dangerous!) or accept the introduction of garbled mix. Frama-C Aluminium brought a new way to handle them that solves both issues. This will be the subject of the next post in this blog. Stay tuned!