Frama-C

Az alábbi levelet kaptam az imént:

Hello,

you seem to have initiated a discussion thread on http://hup.hu
where Frama-C was mentioned. We are not comfortable
posting this message to the forum, especially since automatic
translation do not make it easy for us to understand everything
that is said there, but if the text below seems to you
to be relevant to the discussion, please feel free to transmit it
to the forum.

Best regards,

Pascal Cuoq and the Frama-C development team

Dear HUP users,

The Frama-C development team has been guilty of a little bit of
kibozing ( http://en.wiktionary.org/wiki/kiboze ) and came across this
discussion thread. Although the development team does not have much in
terms of resources for reading it in its original language, it appears
that one of the topic discussed is that of the verification of
alignement of data.

This question has been asked before in the context of the CAT project
in which Frama-C's development was started. The short answer is "yes,
Frama-C may be able to verify that some addresses are always aligned
on a n-bytes boundary, if the compiler's choices for the layout of
data in memory follow some usual conventions". For instance, the
address of field i+1 in a struct should be determined by the compiler
computed by taking the address of field i, adding the size of field i
and rounding the result up to the required alignment for the
type of field i+1.
The involved parameters, such as types sizes and alignements, can be
autodetected by compiling a special program on the target platform.
Note that the requirement that the compiler has to allow
separate compilation and conform to the platform ABI is likely to
make these hypotheses reasonnable.

Frama-C is only able at this point to verify that an address is
aligned on a n-bytes boundary when this property results from both the
base address being aligned on a n-bytes boundary and the offset being
a multiple of n. For instance, it is able to conclude in this
example, because the base address of p+12 is an int array, and
therefore 4-bytes aligned:

int t[10];
char *p;
p = (char *) t;
* (int*) (p+12) = 42; /* p + 12 should really be aligned
                         on a 4-bytes boundary */

It definitely will be unable to conclude in the example below, because
the alignement property results from choosing an offset that compensates
the possible misalignement of the base address, and this kind of relation
between the alignment of the base address and the computed offset can
not be represented in the memory model used by Frama-C's value analysis.

char t[80];
char *p;
p = (t + 7) & ~7;
* (int*) p = 42; /* p absolutely needs to be aligned 
                    on a 4-bytes boundary */

Please find below a more complete example. In this example,
one would like to check that the pointer passed to function f
is always 4-bytes aligned.

____________________________________________

#ifdef USING_FRAMA_C_FOR_VERIFICATION
#include ".../share/builtin.h"

int Frama_C_is_base_aligned(void *, int); 
/* this should be in .../share/builtin.h but it is not as of version 20080502 */

void check_alignment(void *p, int n)
{
  int good_alignment = Frama_C_is_base_aligned(p, n) && Frama_C_offset(p) % n == 0;

  if (!good_alignment) Frama_C_show_each_alignment_warning(p,n);
}

#define CHECK_ALIGNMENT(P, N) check_alignment(P, N);

#else

#define CHECK_ALIGNMENT(P, N) 

#endif

int t[12]; 

char c[14]; 

struct S { int a; char b; } s[5]; 

int o1, o2, o3; 

int r1, r2, r3;

int b1, b2, b3;



struct S2 { int a; char b[10]; int c;} s2;

int os2a, os2b, os2c;

int o;


void f (char * p){
  CHECK_ALIGNMENT (p, 4)
  *(int*)p = 42;
}

void main(void) 
{ 

  int i; 

#ifdef USING_FRAMA_C_FOR_VERIFICATION
  i = Frama_C_interval(0, 10);
#else
  i = 5;
#endif

  o1 = Frama_C_offset(&t[i]); 
  r1 = o1 % 4 == 0;
  b1 = Frama_C_is_base_aligned(&t[i], 4);
  
  f(&t[i]);

  f(c + 3);

  o2 = Frama_C_offset(&c[i]); 

  r2 = o2 % 4 == 0;
  b2 = Frama_C_is_base_aligned(&c[i], 4);


  o3 = Frama_C_offset(&s[i].a); 

  r3 = o3 % 4 == 0;
  b3 = Frama_C_is_base_aligned(&s[i].a, 4);

  f(&s[i].a);

  os2a = Frama_C_offset(&s2.a);

  os2b = Frama_C_offset(&s2.b);

  f(&s2.b);
 
  os2c = Frama_C_offset(&s2.c);

  f(&s2.c);
}

_______________________

Use the command line (please replace ... by Frama-C's installation
path everywhere):

.../bin/viewer.opt -val .../share/builtin.c alignement_args_fonctions.c -cpp-command "gcc -C -E -I. -D USING_FRAMA_C_FOR_VERIFICATION"

You should be able to observe the values of variables o1, r1, b1, ...
and see if they correspond to your expectations. Besides, please
note the following lines in the analysis log:

[values] computing for function f <-main
[values] called from alignement_args_fonctions.c:66
[values] computing for function check_alignment <-f <-main
[values] called from alignement_args_fonctions.c:45
Argument of Frama_C_show_each_alignment_warning: {{ &c + {3; } ;}}
Argument of Frama_C_show_each_alignment_warning: {4; }

This part of the log mean that the analyzer is not able to guarantee
that the parameter for f is aligned when it is called from
line 66 in the example (the resolved address that poses a
problem, {{ &c + {3; } ;}}, is also printed, in case that helps
to track down the problem and attribute it to either a bug
in the source or a lack of precision in the analyzer).

Frama-C has been designed to be "correct", which means that there are
no problems in the program when it does not display any warnings.
This distinguishes it from other static analyzers which prefer to
display a warning only when they are quite sure that they have found
an actual problem, so as not to flood the user with too many warnings.
Frama-C typically display more false alarms than these (it displays a
warning as soon as it is not able to conclude that there is no
problem), but on the other hand, it also means that it can be used to
guarantee that there are no problems in a program, if you are so
inclined (it needs to be used properly, and some hypotheses have to
apply. Please see the documentation for more information. Oh, and it
still requires a lot of work).

--
trey @ gépház