Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Tuesday, December 13 2016

Frama-C Silicon has been released!

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 contain1, however, so it will presented in more detail later.

1 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:

Show pointed values in the GUI

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.

Friday, April 8 2016

Small improvements to the Frama-C GUI

The Frama-C GUI received a few quality-of-life improvements that have not been announced during the Magnesium release. This post presents some of them, along with general GUI tips.

We focus on general-purpose UI improvements, while another post will discuss new Value-specific features, related to the new Values tab.

These UI features should be discoverable via menus or other signifiers in the UI, but we decided to keep them hidden until stabilization, to avoid breaking existing workflows in case we decided to remove them. They are still not 100% mature, but since we have been pleasantly using them for several months, we feel confident enough to disclose their existence.

The features mentioned here are:

Textual search

It is now possible to perform a textual search in most Frama-C panels using Ctrl+F. Here is the list of panels where this works:

  • List of globals (upper-left panel, which displays filenames and global definitions);
  • CIL code (central panel);
  • Original source code (upper-right panel);
  • Information tab (lower panel);
  • Console tab (lower panel).

When you press Ctrl+F, the currently focused panel will display a small search window (if it accepts textual search) like this one:

Text search panel

Notice that the window mentions in which panel the search will be performed. Also, the search is case-sensitive.

Click on Find to search for the string. You can type F3 to perform a "Repeat search", that is, advance to the next occurrence of the text without opening a new panel. If you reach the end of the text, this dialog will notify you:

Reaching the end of the text

Also, if the search text is not found, you'll be presented a different dialog:

Text not found dialog

Message/Property counters

The Messages and Properties tabs now display the total amount of items they contain. This summary is useful for a quick comparison between short analyses. The Messages tab always display the amount of items, while the Properties tab, because of its "lazy" nature (items are only updated after clicking the Refresh button), initially does not display anything, but after selecting the set of desired filters, the Refresh button will update the total count, as illustrated in the figures below (click on the orange circles to switch images).

  • Message/Property counters (1/6)
  • Message/Property counters (2/6)
  • Message/Property counters (3/6)
  • Message/Property counters (4/6)
  • Message/Property counters (5/6)
  • Message/Property counters (6/6)

Note that the font in the Refresh button becomes bold to indicate that an update is needed, and returns to normal afterwards.

Types in the Information tab

The Information tab has been modified to include some typing information about variables, as shown in the example below.

Type information

In the example, the user clicked on the res expression, which displays some information (rectangle 1) such as the current function, statement id (used internally), source code line (with a clickable link to focus it in the original source panel), the type of the variable (with a clickable link), and some extra details.

By clicking on the variable type, we obtain more information (rectangle 2):

  • sizeof;
  • Source code line where the type is defined (if it is not a predefined type), with a clickable link;
  • Expanded type information (in the case of composite types). If a field is defined via yet another composite type, a link to the type information of that type will also be displayed.

This is very useful when exploring new code bases.

Note that some information that was previously displayed in this tab (e.g. the results computed by the Value plug-in) has been moved to the Values tab, which will be described in a later post.

Property filters and filtersets

One common issue for new users is to properly set the filters in the Properties tab, to avoid displaying too much information. Advanced users also had some difficulties defining a precise set of filters that matched their needs.

To help both kinds of users, the Properties tab had two minor improvements: first, some filter categories were defined (Kind, Status, RTE-related), to allow folding/unfolding of sets of filters.

Second, a few recommended filter sets were defined, corresponding to the most often used filter combinations. A small "Filter" button (a pointing hand clicking on a square) has been added next to the Refresh button, as indicated in the screenshot below:

Filter properties button

The "Reset all filters to default" menu consists in:

  • Hiding properties with status Considered valid, Untried or Dead;

  • Hiding statuses that are useful only in some specific situations: this includes Behaviors, Axiomatic and Reachable.

These statuses are not included by default for two reasons: Axiomatic and Behaviors are redundant w.r.t. the contents of other filters, while Reachable properties such as the ones produced by Value may generate noise, e.g. dead code detected by Value may show up as "Reachable Invalid" status (i.e. "unreachable")¸ when its actual consolidated status is Valid but dead.

In most circumstances, these properties are not relevant for an analysis of potential alarms. Filtering them by default reduces noise, but it is still possible to select them when necessary.

A more restrictive view can be obtained by selecting the menu "Reset 'Status' filters to show only unproven/invalid". This further eliminates Valid and Valid under hypotheses, leaving only orange/red bullets, which are often the only ones we are interested in.

Note that the Current function filter is independent of these buttons.

(Approximate) mapping from original to CIL source

A much-requested functionality is the mapping from the original source (right panel) to the CIL code, to synchronize the views of both panels.

Before Magnesium, clicking on the original source code did not move the cursor on the CIL code. Now, an approximate mapping allows the user to click on the original source and have the CIL source scrolled to the approximate corresponding location, as in the example below, in which the user clicked on the macro IEEE_1180_1990_ABS.

Reverse mapping

Note that this feature is not 100% reliable because the mapping between both sources is not always invertible. For instance, consider syntactic unrolling of loops, or multiple expansion of macros. In some cases the mapping fails (no location is found) or moves the CIL code to a distant part; e.g. some parts of expressions, when clicked, scroll to the variable declaration instead. Also, static variables and macro definitions are particularly problematic. But overall, this feature is a net benefit, especially when trying to find a specific location in a large function. If you find unintuitive behaviors, do not hesitate to tell us; there may be some patterns which have not yet been considered.

Tip: In some cases, different parts of an expression give different results, so it may be worth trying a few nearby clicks.

Conclusion

Each modification to the Frama-C GUI in itself is a minor, almost imperceptible improvement, but together these features greatly contribute to our comfort and productivity when using the GUI. We hope you'll enjoy using them as well!