Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] integer overflow

  • Subject: [Frama-c-discuss] integer overflow
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Thu, 11 Jun 2009 22:44:27 +0200
  • References: <4A315C7C.3030309@cs.utah.edu>
> > at run-time, assuming 2's complement arithmetic and proper
> > configuration of the characteristics of the target architecture.

>Third, overflow of signed arithmetic (for example, MAX_INT+1) is undefined. 
>  Due to C's semantics, the "correct superset of the values that can 
>actually be obtained at run-time" does not exist.  Rather, anything at all 
>can happen including terminating with a signal, continuing to execute with 
>a corrupt state, etc.  A C program should never continue to execute after 
>executing an operation with undefined behavior, and so it seems rather 
>important for Frama-C to give rigorous warnings in this case.

The value analysis does not try to assume only what is in the
C99 standard to get its results. When there are established practices
that rely on common compilers' behavior, we consider it fair game
to make the same assumptions that the programmer makes (with
reason). Especially because without these necessary hypotheses,
it may be impossible to conclude for C code that exists,
is being verified as is and works in practice.
We are not in the business of judging developers' styles and
asking them to change their habits. We try to provide tools
that can be used for verification and that do not require to
change the analyzed code when it works.

This was the mission statement (sorry for the soliloquy, but 
these things need to be said from time to time). Now,
naturally we are only doing our best and we can be misguided
in our interpretation of what is in
the "informal C standard"  and what isn't, especially
since we are not particularly experienced in embedded C
development ourselves. When in doubt, we certainly did try
to err on the side of being too lenient, so that no existing,
working embedded code would be rejected because of "style"
(it can be rejected because of the analyzer's imprecision
which is another story).

In addition to assuming 2's complement representation, we assume
that there is only one assembly instruction for, say, signed and
unsigned addition (with various flags all being computed so that you
can get those you were interested in, which C does not give you
access to anyway). And we assume that this instruction is always
used for signed addition.

>Optimizing C compilers including gcc routinely exploit the undefined nature 
>of signed overflow!

Rats! Do you have a reproducible example where the assembly does
not contain the addition at all?
This would not be the first time this tendency to aggressively exploit
undefinedness for optimization purposes causes us trouble. There is
a famous gcc optimization that makes it dangerous to do arithmetic
on invalid pointers, that we did not get around to model either yet.

>Anyway, I have some C functions for which I want to prove the absence of 
>the third kind of overflow, which results in undefined behavior.  Is there 
>a way to get Frama-C to help me do this?

I will try to make this possible soon, either in the form
of a patch published on this list
(hopefully you were compiling Frama-C from sources)
or as an experimental feature in the next release,
whose date it is forbidden to discuss on this list.

Pascal

PS: in fact, I have another rant:
why is it that these so-called "optimizations"
in gcc always seem only to optimize incorrect code?
Why not warn the developer, instead of generating
stupid code and  telling him/her "ha! ha! we got ya!"
when he notices and complains?
If the compiler replace a source code addition
by nothing in assembly, there is something wrong.
The compiler is not being smart,
it is being a wiseass.
Similarly, if it deems that a pointer comparison is
always true because the pointer is at one time invalid during
the chain of arithmetic operations that are applied to it,
why not warn instead of silently generating code that can only
be not what the developer wants?

I know, I know, generated code, macros,... I still think GCC's
user interface sucks.

-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: non disponible
Type: application/ms-tnef
Taille: 4755 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090611/4ad1c8df/attachment.bin