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.
