Frama-C news and ideas

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

Tag - conversions-and-promotions

Entries feed - Comments feed

Wednesday, October 9 2013

The overflow when converting from float to integer is undefined behavior

Integer overflows in C

A previous post on this blog was a reminder that in C, signed integer arithmetic overflow is undefined behavior. In contrast, the behavior of overflows in conversions from integer type to signed integer type is implementation-defined. The C99 standard allows for an implementation-defined signal to be raised, but in practice, the widespread compilation platforms provide two's complement behavior. And you can trust that they will continue to do so, because it's implementation-defined. Compiler makers cannot change their mind willy-nilly as if it was undefined behavior:

6.3.1.3 Signed and unsigned integers

1 When a value with integer type is converted to another integer type other than _Bool, if the value can be represented by the new type, it is unchanged.

2 Otherwise, if the new type is unsigned, the value is converted by repeatedly adding or subtracting one more than the maximum value that can be represented in the new type until the value is in the range of the new type.

3 Otherwise, the new type is signed and the value cannot be represented in it; either the result is implementation-defined or an implementation-defined signal is raised.

Floating-point overflows in C

The C standard does not mandate IEEE 754 floating-point arithmetic. Still, in practice, modern compilation platforms, if they provide floating-point features at all, provide either exactly IEEE 754 binary32 and binary64 formats and computations, or the same formats and a close approximation of the same computations.

IEEE 754 floating-point defines +inf and -inf values, so that any real number can be approximated in the target IEEE 754 format (albeit, when it ends up represented as an infinity, not precisely). This means that for C compilation platforms that implement IEEE 754 for floating-point, the condition “the value can be represented in the new type” is always true. There is no reason to worry of undefined behavior caused by overflow in either floating-point arithmetic or in the conversion of a double to a float.

Or indeed, in a constant. Consider GCC's warning here:

$ cat t.c
#include <stdio.h>

int main()
{
  double big = 0x1.0p5000;
  printf("%f\n", big);
}

$ gcc-172652/bin/gcc -std=c99 -Wall t.c && ./a.out 
t.c: In function ‘main’:
t.c:5:3: warning: floating constant exceeds range of ‘double’ [-Woverflow]
inf

The number 2^5000, represented in C as 0x1.0p5000, is totally in the range of double, which goes up to inf. Clang similarly warns that “magnitude of floating-point constant too large for type double”. A proper warning message would be that 2^5000 cannot be represented precisely, instead of implying that it cannot be represented at all.

Floating-point ↔ integer conversion overflows in C

But enough pedantry contests with compilers. The range of floating-point representations being what it is, we are left with only overflows in conversions from floating-point to integer to consider.


Suspense… (for the reader who did not pay attention to the title)


Overflows in conversions from floating-point to integer are undefined behavior. Clause 6.3.1.4 in the C99 standard make them so:

6.3.1.4 Real floating and integer

1 When a finite value of real floating type is converted to an integer type other than _Bool, the fractional part is discarded (i.e., the value is truncated toward zero). If the value of the integral part cannot be represented by the integer type, the behavior is undefined.

What can happen in practice when a C program invokes this particular flavor of undefined behavior? It is as bad as dereferencing an invalid address, mostly harmless like signed integer arithmetic overflow, or what? Let us find out.

The following program converts the double representation of 2^31, the smallest positive integer that does not fit a 32-bit int, to int.

int printf(const char *, ...);

int main()
{
  int i = 0x1.0p31;
  printf("%d\n", i);
}

Frama-C's value analysis warns about undefined behavior in this program:

$ frama-c -val t.c

warning: overflow in conversion of 0x1.0p31 (2147483648.) 
   from floating-point to integer.
   assert -2147483649 < 0x1.0p31 < 2147483648;

Fine-tuning the assertion -2147483649 < 0x1.0p31 < 2147483648 was a riot, by the way. Do you see why?

My aging (but still valiant) PowerPC-based Mac appears to think that saturation is the way to go: the variable i is set to INT_MAX:

$ gcc -std=c99 t.c && ./a.out 
2147483647

Dillon Pariente was first to draw our attention to overflow in floating-point-to-integer conversions, which caused CPU exceptions on the target CPU for the code he was analyzing. I understood that target CPU to also be a PowerPC, so I suspect the behavior must be configurable on that architecture.

Dillon Pariente's example was along the lines of float f = INT_MAX; int i = f; which is also hilarious if you are into that sort of humor.


In order to really show how weird things can get on Intel processors, I need to modify the test program a bit:

int printf(const char *, ...);

volatile double v = 0;

int main()
{
  int i1 = 0x1.0p31;
  int i2 = 0x1.0p31 + v;
  printf("%d %d\n", i1, i2);
}

The volatile type qualifier precludes optimization, but there is no hardware or thread to change the value of variable v. The two expressions 0x1.0p31 and 0x1.0p31 + v are both expressions of type double that evaluate to 2^31.

Still GCC and Clang, like a single compiler, think that these two expressions needn't result in the same value when converted to int:

$ gcc t.c && ./a.out 
2147483647 -2147483648
$ clang  t.c && ./a.out 
2147483647 -2147483648

The results are different because one conversion was evaluated statically to be placed in %esi (2147483647) whereas the other was evaluated at run-time in %edx with the cvttsd2si instruction:

$ clang -S -O t.c  && cat t.s
...
_main:                                  ## @main
...
	movsd	_v(%rip), %xmm0
	addsd	LCPI0_0(%rip), %xmm0
	cvttsd2si	%xmm0, %edx
	leaq	L_.str(%rip), %rdi
	movl	$2147483647, %esi       ## imm = 0x7FFFFFFF
	xorb	%al, %al
	callq	_printf
...
L_.str:                                 ## @.str
	.asciz	 "%d %d\n"

Only undefined behavior allows GCC and Clang to produce different values for i1 and i2 here: the values of these two variables are computed by applying the same conversion to the same original double number, and should be identical if the program was defined.


Generally speaking, cvttsd2si always produces -0x80000000 in cases of overflow. That is almost like saturation, except that floating-point numbers that are too positive are wrapped to INT_MIN. One may think of it as saturating to either -0x80000000 or 0x80000000, and in the latter case, wrapping around to -0x80000000 because of two's complement. I do not know whether this rationale bears any resemblance to the one Intel's engineers used to justify their choice.


So one might think that this is the end of the story: as long as the conversion is done at run-time on an Intel platform, the compiler uses the cvttsd2si instruction. Overflows, if overflows there are, “saturate to INT_MIN” as the convention is on this platform. This can be confirmed experimentally with the following program variant:

#include <stdio.h>
#include <stdlib.h>

int main(int c, char **v)
{
  int i = 0x1.0p31 + strtod(v[1], 0);
  printf("%d\n", i);
}

This new program takes a number from the command-line and adds it to 2^31, so that there is no opportunity for compile-time evaluation. We expect the conversion to saturate to INT_MIN, and it does:

$ gcc -std=c99 t.c && ./a.out 1234 && ./a.out 12345 && ./a.out 123456
-2147483648
-2147483648
-2147483648


Wait! It gets more amusing still. Let us change the program imperceptibly:

int main(int c, char **v)
{
  unsigned int i = 0x1.0p32 + strtod(v[1], 0);
  printf("%u\n", i);
}

The behavior of run-time overflow in the conversion from double to integer changes completely:

$ gcc -m64 -std=c99 t.c && ./a.out 1234 && ./a.out 123456 && ./a.out 12345678999 
1234
123456
3755744407

But conversion saturates again, at zero this time, for the same program, when targeting IA-32:

$ gcc -m32 -std=c99 t.c && ./a.out 1234 && ./a.out 123456 && ./a.out 12345678999
0
0
0

Do you have an explanation for this one? Leave a message in the comments section below. The fastest author of a complete explanation wins a static analyzer license.

Conclusion

In conclusion, the overflow in the conversion from floating-point to integer is rather on the nasty side of C's undefined behavior spectrum. It may appear to behave consistently if the compilation targets an architecture where the underlying assembly instruction(s) saturate. Saturation is the behavior that compilers GCC and Clang implement when they are able to evaluate the conversion at compile-time. In these conditions, a lucky programmer may not actually observe anything strange.

The idiosyncrasies of other architectures may lead to very different results for overflowing conversions depending on parameters outside the programmer's control (constant propagation, for instance, is more or less efficient depending on the optimization level and may be difficult to predict, as we already complained about when discussing Clang targeting the 387 FPU).


Acknowledgements: In addition to Dillon Pariente, I discussed this topic with Boris Yakobowski, John Regehr, Stephen Canon, and StackOverflow users tenos, Sander De Dycker and Mike Seymour prior to writing this blog post.

Saturday, August 24 2013

Function pointers in C

This post contains a complete list of everything a C program can do with a function pointer, for a rather reasonable definition of “do”. Examples of things not to do with a function pointer are also provided. That list, in contrast, is in no way exhaustive.

What a C program can do with a function pointer

Convert it to a different function pointer type

A function pointer can be converted to a different function pointer type. The C99 standard's clause 6.3.2.3:8 starts:

“A pointer to a function of one type may be converted to a pointer to a function of another type and back again; the result shall compare equal to the original pointer.”

Call the pointed function with the original type

Clause 6.3.2.3:8 continues:

“If a converted pointer is used to call a function whose type is not compatible with the pointed-to type, the behavior is undefined.”

Alright, so the above title is slightly sensationalistic: the pointed function can be called with a compatible type. After typedef int t;, the types t and int are compatible, and so are t (*)(t) and int (*)(int), the types of functions taking a t and returning a t and of functions taking an int and returning an int, respectively.

There is no third thing a C program can do with a function pointer

Seriously. The C99 standard has uintptr_t, a recommended integer type to convert data pointers to, but there is not even an equivalent integer type to store function pointers.

What a C program cannot do with a function pointer

Convert it to an ordinary pointer

Function pointers should not be converted to char * or void *, both of which are intended for pointers to data (“objects” in the vocabulary of the C standard). Historically, there has been plenty of reasons why pointers to functions and pointers to data might not have the same representation. With 64-bit architectures, the same reasons continue to apply nowadays.

Call the pointed function with an incompatible type

Even if you know that type float is 32-bit, the same as int on your platform, the following is undefined:

void f(int x);

int main(){
  void (*p)(float) = f;
  (*p)(3);
}

The line void (*p)(float) = f;, which defines a variable p of type “pointer to function that takes a float”, and initializes it with the conversion of f, is legal as per 6.3.2.3:8. However, the following statement, (*p)(3); is actually equivalent to (*p)((float)3);, because the type of p is used to decide how to convert the argument prior to the call, and it is undefined because p points to a function that requires an int as argument.


Even if you know that the types int and long are both 32-bit and virtually indistinguishable on your platform (you may be using an ILP32 or an IL32P64 platform), the types int and long are not compatible. Josh Haberman has written a nice essay on this precise topic.

Consider the program:

void f(int x);

int main(){
  void (*p)(long) = f;
  (*p)(3);
}

This time the statement is equivalent to (*p)((long)3);, and it is undefined, even if long and int are both 32-bit (substitute long and long long if you have a typical I32LP64 platform).


Lastly, the example that prompted this post was, in a bit of Open-Source code, the creation of a new execution thread. The example can be simplified into:

void apply(void (*f)(void*), void *arg)
{
  f(arg);
}

void fun(int *x){
  // work work
  *x = 1;
}

int data;

int main(){
  apply(fun, &data);
}

The undefined behavior is not visible: it takes place inside function apply(), which is a standard library function (it was pthread_create() in the original example). But it is there: the function apply() expects a pointer to function that takes a void* and applies it as such. The types int * and void * are not compatible, and neither are the types of functions that take these arguments.

Note that gcc -Wall warns about the conversion when passing fun to apply():

t.c:11: warning: passing argument 1 of ‘apply’ from incompatible pointer type

Fixing this warning with a cast to void (*)(void*) is a programmer mistake. The bug indicated by the warning is that there is a risk that fun() will be applied with the wrong type, and this warning is justified here, since fun() will be applied with the wrong type inside function apply(). If we “fix” the program this way:

$ tail -3 t.c
int main(){
  apply((void (*)(void*))fun, &data);
}
$ gcc -std=c99 -Wall t.c
$ 

The explicit cast to (void (*)(void*) silences the compiler, but the bug is still in the same place, in function apply().


Fortunately gcc -std=c99 -Wall is not the only static analyzer we can rely on. Frama-C's value analysis warns where the problem really is, in function apply(), and it warns for both the version with implicit conversion and the version with explicit cast:

$ frama-c -val t.c
…
[value] computing for function apply <- main.
        Called from t.c:14.
t.c:3:[value] warning: Function pointer and pointed function 'fun'  have incompatible types:
        void (void *) vs. void (int *x). assert(function type matches)

The correct way to use function apply() without changing it is to make a function with the correct type for it, and to pass that function to apply():

void stub(void *x){
  fun(x);  
}
…
  apply(stub, &data);

Note that in the above, x is implicitly converted when passed to function fun(), the same way that &data is implicitly converted to void* when passed to apply().

Conclusion

There is almost nothing you can do in C with a function pointer. The feature is still very useful and instills a bit of genericity in an otherwise decidedly low-level language.

Function pointers are not often used in the standard library, considering: qsort() is, with pthread_create(), another of the few functions that requires a function pointer. Like it, it is often misused: it has its own entry in the C FAQ.


Jens Gustedt provided advice in the writing of this post.

Thursday, July 11 2013

Arithmetic overflows in Fluorine

There is a C quiz in the middle of this post, lost in the middle of all the reminiscing.

A history of arithmetic overflows in Frama-C

From the very beginnings in 2005, until after the first Open Source release in 2008, Frama-C's value analysis was assuming that all arithmetic overflows produced two's complement results. This seemed the right thing to do at the time.

Then an option was introduced to emit alarms on undefined overflows. John Regehr suggested it after testing one of the Open Source versions. The option was turned off by default. If a value analysis user turned the option on, any undefined arithmetic overflow in the program would be detected and reported as a possible error, with the same gravity as dereferencing NULL or accessing an array out of its bounds.

Later, a helpful reminder was added to the value analysis' output: in the default behavior of not emitting alarms, an informative message was emitted instead—if such an overflow was detected—about two's complement being assumed.

There was one last change in the last release, Fluorine. Actually, two changes: the name of the option for emitting alarms on undefined overflows changed, and the default value changed. The setting is now to emit alarms by default, and can be changed to not emitting them, for instance if the target code is destined to be compiled with gcc -fno-strict-overflow -fwrapv, in which case all overflows happening during execution can be expected to produce two's complement results.


One aspect remains unchanged in the above evolution: the discussion only applies to undefined overflows.

The philosophy was always to analyze programs as they were written, and not to force any change of habit on software developers. The initial choice not to warn about overflows was because we knew there were so many of these—most of them intentional—that we would be deluging the user with what would feel like a flood of false positives.

The gradual shift towards more arithmetic overflow awareness is a consequence of the fact that in C, some arithmetic overflows are undefined behavior. Compilers display increasing sophistication when optimizing the defined behaviors to the detriment of the predictability of undefined ones. To make a long story short, the “overflows produce 2's complement results” heuristic was wrong for some programs as compiled by some optimizing compilers.

In keeping with the same philosophy, “overflows” that are defined according to the C99 standard have always been treated by the value analysis plug-in with the semantics mandated by the standard. Those overflows that the standard says must have “implementation-defined” results are treated with the semantics that the overwhelming majority of compilation platforms give them (and it remains possible to model other architectures as the need arises).

A quiz

Other static analyzers may also warn for arithmetic overflows, but the philosophy can be different. The philosophy may for instance be that any overflow, regardless of whether it is defined or implementation-defined according to the letter of the standard, might be unintentional and should be brought to the attention of the developer.

In the few examples below, the goal is to predict whether Frama-C's value analysis with its new default setting in Fluorine would emit an alarm for an overflow. For extra credit, a secondary goal is to predict whether another static analyzer that warns for all overflows would warn. We assume a 32-bit int and a 16-bit short, same as (almost) everybody has.

int a = 50000;
int b = 50000;
int r = a * b;
unsigned int a = 50000;
unsigned int b = 50000;
unsigned int r = a * b;
int a = 50000;
int b = 50000;
unsigned int r = a * b;
short a = 30000;
short b = 30000;
short r = a * b;
unsigned short a = 50000;
unsigned short b = 50000;
unsigned int r = a * b;

Answers

int a = 50000;
int b = 50000;
int r = a * b;

There is an overflow in this snippet (mathematically, 50000 * 50000 is 2500000000, which does not fit in an int). This overflow is undefined, so the value analysis warns about it.


unsigned int a = 50000;
unsigned int b = 50000;
unsigned int r = a * b;

The multiplication is an unsigned int multiplication, and when the mathematical result of unsigned operations is out of range, the C99 standard mandates that overflows wrap around. Technically, the C99 standard says “A computation involving unsigned operands can never overflow, …” (6.2.5:9) but we are using the word “overflow” with the same meaning as everyone outside the C standardization committee including Wikipedia editors.

To sum up, in the C99 standard, overflows in signed arithmetic are undefined and there are no overflows in unsigned arithmetic (meaning that unsigned overflows wrap around).


int a = 50000;
int b = 50000;
unsigned int r = a * b;

The multiplication is again a signed multiplication. It does not matter that the result is destined to an unsigned int variable because in C, types are inferred bottom-up. So the value analysis warns about an undefined overflow in the multiplication here.


short a = 30000;
short b = 30000;
short r = a * b;

There is no overflow here in the multiplication because the last line behaves as short r = (short) ((int) a * (int) b);. The justification for this behavior can be found in clause 6.3.1 of the C99 standard about conversions and promotions (the general idea is that arithmetic never operates on types smaller than int or unsigned int. Smaller types are implicitly promoted before arithmetic takes place). The product 900000000 does fit in the type int of the multiplication. But then there is a conversion when the int result is assigned to the short variable r. This conversion is implementation-defined, so the value analysis does not warn about it, but another static analyzer may choose to warn about this conversion.


unsigned short a = 50000;
unsigned short b = 50000;
unsigned int r = a * b;

Perhaps contrary to expectations, there is an undefined overflow in the multiplication a * b in this example. Right in the middle of the aforementioned 6.3.1 clause in the C99 standard, on the subject of the promotion of operands with smaller types than int, the following sentence can be found:

If an int can represent all values of the original type, the value is converted to an int; otherwise, it is converted to an unsigned int.

All values of a 16-bit unsigned short fit a 32-bit int, so the third line is interpreted as unsigned int r = (unsigned int) ((int) a * (int) b);.


Incidentally, things would be completely different in this last example if int and short were the same size, say if int was 16-bit. In this case the third line would be equivalent to unsigned int r = (unsigned int) a * (unsigned int) b; and would only contain an unsigned, innocuous overflow.

Wrapping up

In Fluorine, the option to activate or deactivate the emission of these undefined arithmetic overflow alarms is called -warn-signed-overflow (the opposite version for no alarms being -no-warn-signed-overflow). I felt that providing this piece of information earlier would have rendered the quiz too easy.

Although Frama-C's value analysis adheres to the semantics of C and only warns for undefined overflows, it is possible to use Frama-C to check for the other kinds of overflows by using another plug-in, Rte, to automatically annotate the target C program with ACSL assertions that express the conditions for overflows. Note that that post pre-dates the Fluorine release and is written in terms of the old options.

Thursday, April 25 2013

Sign extension

There is no “sign extension” in C. Please stop referring to “sign extension” in C programs.

In assembly, there is such a thing as “sign extension”

Sign-extend is an assembly instruction, say movsx %al, %ebx, to transfer the contents of a narrow register, say %al, to a wide register, say %ebx, copying the most significant bit of the narrow register all over the unoccupied bits of the wide register.

In C, there is no “sign extension”. Really.

In C, a short variable s contains -3 and the contents of that variable is transferred to another variable of type int, like so:

int i = s;

Variable i receives -3. That's it. That's “sign extension”.

It's an assignment and, in this particular case, a promotion. With other types it could have been a conversion. The target wide variable receives the value that was contained in the narrow variable. Why would this operation need a name, and such an ugly name as “sign extension” at that?

The name for “sign extension” in C is “getting the value”. Variable i receives the value of s. That's it. That is all there is.

Tuesday, February 26 2013

Portable modulo signed arithmetic operations

In a recent post, John Regehr reports on undefined behaviors in Coq! In Coq! Coq! Exclamation point!

Coq is a proof assistant. It looks over your shoulder and tells you what remains to be done while you are elaborating a mathematical proof. Coq has been used to check that the 4-color theorem really holds. It would be supremely ironic if an undefined behavior in a bit of C code in the OCaml implementation used to compile Coq caused it to accept as valid some incorrect proofs, for instance in the formally verified (in Coq) compiler CompCert.

Your mission, should you decide to accept it

Where are these undefined behaviors? They are in several places, but some of them are in the implementation of the bytecode arithmetic operations. In OCaml, basic operations such as addition and multiplication are specified as returning the mathematical result modulo 2^31, 2^32, 2^63 or 2^64, depending on the compilation platform and the integer type.

The problem here is not limited to OCaml. The Java Virtual Machine too specifies that arithmetic operations on its 32-bit integer type return results modulo 2^32. Someone wishing to implement a JVM in portable C would face the same issues.

In fact, this is just such a big issue that we should collectively try to work out a solution now.

A safer signed addition instruction

Let us assume a 32-bit platform. In this case, values of the unboxed OCaml type int range between -2^30 and 2^30-1 (31 bits of information). They are stored at run-time in the 31 most significant bits of a machine word, with the least significant bit set to one to distinguish it from a pointer. This representation is taken into account when applying arithmetic operations to machine words representing unboxed integers.

Here is an example, in file interp.c in the OCaml implementation. We are in the middle of the large switch that decodes bytecode instructions:

    Instruct(ADDINT):
      accu = (value)((intnat) accu + (intnat) *sp++ - 1); Next;

The - 1 in this expression compensates for the fact that the least significant bit is set in both operands, and we want it to be set in the result (and no carry to be propagated). But as written, there is an undefined overflow in the C implementation of the bytecode interpreter when the unboxed integers in accu and *sp total more than 2^30-1. In order to avoid a signed overflow here, the instruction ADDINT could be written:

      accu = (value)((uintnat) accu + (uintnat) *sp++ - 1U); Next;

This solution takes advantage of the fact that unlike signed addition, the behavior of unsigned addition when the result overflows the destination type is defined by the C standard. The solution above does make assumptions about the conversion from a signed to an unsigned type and vice versa, but these are implementation-defined (and we are only targeting implementations that define these conversions as 2's-complement).

No overhead is involved in this approach: a half-decent C compiler should generate the same instruction sequence for the new version as it already generates for the old version.

Multiplication

You may be vaguely worried about multiplication. For instance, you may remember that while, in a typical instruction set, there is only one addition instruction that works for both signed and unsigned operands, there are dedicated signed multiplication and unsigned multiplication instructions. These are IMUL and MUL in the x86 family of processors.

Fear not! The two multiplications are only because on x86 and many other processors, 32-bit multiplication returns a 64-bit result. If you want all 64 bits of the results to be what you expect, you need to choose the instruction that interprets the operands' highest bit correctly. But if on the other hand you only care for the lowest 32 bits of the result (that is, you only want a result modulo 2^32), then it does no matter that you use unsigned multiplication. Think of it as (x + k1 * 2^32) * (y + k2 * 2^32) for unknown k1 and k2.

And this is our case. Thus, in interp.c, the implementation for bytecode instruction MULINT could be changed from:

Instruct(MULINT):
  accu = Val_long(Long_val(accu) * Long_val(*sp++)); Next;

to:

Instruct(MULINT):
  accu = Val_long((intnat)((uintnat)Long_val(accu) * (uintnat)Long_val(*sp++))); Next;

Conclusion

As pointed out by John Regehr in the comments, the two fixes above are appropriate because the OCaml language definition specifies wrap-around behavior for its (signed) arithmetic operations. One should not assume that all the warnings emitted by IOC have a similar cause. Some may be deeper bugs requiring the logic to be fixed, instead of conversions to unsigned types that only ensure wrap-around behavior.

Issues of the nature discussed here should be in the bytecode version of the OCaml compiler only. By contrast, the native compiler should translate OCaml-level multiplication directly to assembly multiplication, bypassing the portable^Wwoefully underspecified assembly that is the C language.

Even programs generated by the native compiler interface with bits of OCaml runtime written in C, but this runtime is small.

So actually, there is not much cause for worry. If you are using a C compiler or a static analysis platform that involve OCaml code on a modern computer, they are probably already compiled with the native OCaml compiler.

Friday, March 2 2012

ptrdiff_t links for the week-end

Here are two links related to ptrdiff_t:


I was doubtful about the second one (I had no difficulties to accept the first one after the previous conversions-and-promotions-related posts on this blog). But type ptrdiff_t is for storing pointer differences, right? Why would a compilation platform (compiler and associated standard library including malloc()) make it just too small to hold all possible pointer differences? So I tested it, and StackOverflow user R.. is right:

#include <stddef.h>
#include <stdio.h>

main(){
  printf("%d\n", (int) sizeof(ptrdiff_t));
}

Compiling as a 32-bit program:

$ gcc -m32 t.c && ./a.out 
4

I am pretty sure I have allocated 2.2GB in a single malloc() call of a 32-bit process on this system. I was thankful for getting that much at the time, too. But 4 bytes are not enough to hold all signed differences between two pointers to char within a single 2.2GB chunk of memory:

#include <stdio.h>
#include <stdlib.h>

main(){
  char *p = malloc(2200000000U);
  if (!p) return 1;
  char *q = p + 2150000000U;
  printf("%td\n", q - p);
}

Please take a moment to predict the number printed by the above program yourself before looking down.




$ gcc -m32 t.c && ./a.out 
-2144967296

Tuesday, February 14 2012

Checking for overflows, revisited once

I do not have any solution I am 100% happy with to the overflow dilemma in the previous post. Here is one of the solutions that does not make me 100% happy.


The first (partial) solution is: program so that overflows correspond exactly to unwanted circumstances (and then it becomes meaningful to verify the absence of overflows. There are great automatic tools for that. Have you heard of them?)

“Program so that…” sounds abstract, but it may be as simple as using larger integer types that won't overflow for all intermediate computations:

  s = (int)((long long) u1 - (long long)u2);

Then the desired property (variable s contains the mathematical difference of u1 and u2) entirely rests on the final conversion from long long to int.


This solution doesn't apply in the common situation where the code is already written and gratuitous changes to it are prohibited. Also, you need to have an integer type large enough to contain all intermediate computations without overflows. In this example, unsigned int is 32-bit and long long is 64-bit, but the standard does not prevent unsigned int to be 64-bit and the same size as long long, in which case the conversion from unsigned int to long long could overflow. Rte would only insert additional assertions for the two intermediate conversions that we have added in the assignment. This wouldn't help; it would only make things worse.


“Won't the generated code be less efficient?”, you rightly ask. That all depends on the compiler. Optimizing compilers have no trouble at all optimizing the above assignment so that it uses only one 32-bit subtraction. On the Linux workstation on which I tried this, both clang -m32 -O0 and gcc -m32 -O0 did. It is amusing, because the code generated by both compilers with -O0 is ugly (gratuitously moving registers to memory and then to registers again) but, even with optimizations disabled, they still both get the fact that it is only necessary to compute the least significant 32 bits of the result.

With optimizations, both Clang and GCC generate clean code that naturally still uses a single 32-bit subtraction:

$ gcc -S -O2 -m32 t.c
$ cat t.s
...
f:
	pushl	%ebp
	movl	%esp, %ebp
	movl	8(%ebp), %eax
        subl	12(%ebp), %eax
	popl	%ebp
	ret

As an anecdote, when generating x86-64 code (and therefore having 64-bit subtraction available as a single instruction, with only the drawback of a slightly larger encoding), gcc -O0 keeps using 32-bit subtraction but clang -O0 uses 64-bit subtraction. This does not reveal anything about the compilers: it does not make sense to compare for efficiency the code they generate with optimization disabled.


That's all for this post.

Friday, February 10 2012

Checking for overflows operation by operation

My colleague Bernard Botella pointed out an interesting example in an offline discussion following the last quiz.

The setup

Consider the snippet:

int s;
unsigned u1, u2;
...
s = u1 - u2;

The programmer's intention with the assignment is to compute, in variable s of type int, the mathematical difference between the value of u1 and the value of u2. You would expect that, using automatic plug-ins in Frama-C, ey would be able to check that the initial values for u1 and u2 are in ranges for which this is always what happens.

In fact, this looks like a perfect assignment for Rte and the value analysis. Rte can generate assertions for the various conversions and the value analysis can check whether the conditions are satisfied, following the method outlined in a recent post.

This is, after all, exactly what static analyzers — and coding rules that forbid overflows — are for.

An obvious false positive

The overflow in the subtraction u1 - u2 looks like it can be justified away. After all, such a warning is emitted when u1==3 and u2==5, and s will still receive the expected value -2 after the implementation-defined conversion from the value of expression u1 - u2, that is, UINT_MAX - 1, to int.

The programmer may think “okay, I can see why I get this warning, it happens as soon as u2 is larger than u1, but this is defined and, in my case, innocuous. I only want to check that the mathematical difference fits in s. The check about the absence of overflow in the conversion to int is what I am really interested in.”


Say that the programmer is using the Rte plug-in to express the conditions for both the subtraction and the implicit conversion to int to be safe, pretty-printing an annotated program as a result:

$ frama-c -rte-unsigned-ov -rte t.c -print
...
void main(void)
{
  /*@ assert rte: (unsigned int)(u1-u2) ≤ 2147483647; */
  /*@ assert rte: u1-u2 ≥ 0; */
  s = (int)(u1 - u2);
  return;
}

Since the programmer has seen that the second assertion, about an overflow in the subtraction u1 - u2, is too restrictive, preventing use with u1==3 and u2==5, ey removes it. The programmer instead focuses on making sure that there is no overflow in the conversion to int of the difference, and feels confident if ey sees that there isn't any warning about that. It seems normal, right?

void main(void)
{
  /*@ assert rte: (unsigned int)(u1-u2) ≤ 2147483647; */
  s = (int)(u1 - u2);
  return;
}

But…

Consider the case where u1 is very small, u2 is very large, and the value analysis has been able to infer this information relatively precisely. We assume 0 ≤ u1 ≤ 10 and 3000000000 ≤ u2 ≤ 4000000000 for this example:

/*@ requires 0 <= u1 <= 10 ;
    requires 3000000000 <= u2 <= 4000000000 ; */
void main(void)
{
  /*@ assert rte: (unsigned int)(u1-u2) ≤ 2147483647; */
  s = (int)(u1 - u2);
  return;
}

In this case, the value analysis does not warn about the conversion to int ...

$ frama-c -val -lib-entry u.c
...
u.c:8:[value] Assertion got status valid.

... but the value in s is not the mathematical difference between u1 and u2.

Conclusion

The conclusion is that looking at overflows atomically is not a silver bullet. Granted, if all possible overflows in the program are verified to be impossible, then machine integers in the program observationally behave like mathematical integers. But the more common case is that some overflows do in fact happen in the program and are justified as benign by the programmer. The issue pointed out by Bernard Botella is that it is possible to justify an overflow, for which the rule seems too strict, by exhibiting input values for which the expected result is computed, and then to be surprised by the consequences.

Perhaps in another post, we can look at ways around this issue.

Friday, January 20 2012

A bit of explanation regarding the quiz in the last post

There are only positive constants in C, as per section 6.4.4 in the C99 standard:

integer-constant: 
        decimal-constant integer-suffixopt 
        octal-constant integer-suffixopt 
        hexadecimal-constant integer-suffixopt 
decimal-constant: 
        nonzero-digit 
        decimal-constant digit 
octal-constant: 
        0 
        octal-constant octal-digit 
hexadecimal-constant: 
        hexadecimal-prefix hexadecimal-digit 
        hexadecimal-constant hexadecimal-digit 
...

The minus sign is not part of the constant according to the grammar.


The expression -0x80000000 is parsed and typed as the application of the unary negation operator - to the constant 0x80000000. The table in section 6.4.4.1 of the standard shows that, when typing hexadecimal constants, unsigned types must be tried. The list of types to try to fit the hexadecimal constant in is, in order, int, unsigned int, long, unsigned long, long long, unsigned long long.

For many architectures, the first type in the list that fits 0x80000000 is unsigned int. Unary negation, when applied to an unsigned int, returns an unsigned int, so that -0x80000000 has type unsigned int and value 0x80000000.


Following the same reasoning as above, reading from the "Decimal Constant" column of the table in the C99 standard, the types to try are int, long, and long long. This might lead you to expect -2147483648 for the value of the expression -2147483648 compiled with GCC. Instead, when compiling this expression on a 32-bit architecture, GCC emits a warning, and the expression has the value 2147483648 instead. The warning is:

t.c:6: warning: this decimal constant is unsigned only in ISO C90

Indeed, there is a subtlety here for 32-bit architectures. GCC by default follows the C90 standard. It's not so much that the spirit of the table in section 6.4.4.1 in C99 changed between C90 and C99. The spirit remained the same, with unsigned types being tried for octal and hexadecimal constants, and mostly only signed types being tried for decimal constants. Here is the relevant snippet from the C90 standard:

The type of an integer constant is the first of the corresponding list in which its value can be represented. Unsuffixed decimal: int, long int, unsigned long int;

The difference really stems from the fact C90 did not have a long long type, and the list of types to try for a decimal constant ended in unsigned long, since that type contained values that did not fit in any other type. On a 32-bit architecture, where long and int are both 32-bit, 2147483648 fits neither int nor long, and so ends up being typed as an unsigned long. Note that on an architecture where long is 64-bit, then 2147483648 and -2147483648 are typed as long.


Finally, when GCC is told, with option -std=c99, to apply C99 rules on an architecture where long is 32-bit, then 2147483648 is typed as long long, so that the expression -2147483648 has type long long and value -2147483648.


This should explain the results obtained when compiling the three programs from last post with GCC on 32-bit and on 64-bit architectures.

Constants quiz

What does the following program print?

long long l;
#include <stdio.h>

int main()
{
  l = -0x80000000;
  printf("%lld\n", l);
}

$ gcc t.c && ./a.out 

And this one? (beware, trick question)

long long l;
#include <stdio.h>

int main()
{
  l = -2147483648;
  printf("%lld\n", l);
}

$ gcc t.c && ./a.out 

What, "it's too difficult!"? Okay, here is a hint in the form of a third question:

long long l;
#include <stdio.h>

int main()
{
  l = -2147483648;
  printf("%lld\n", l);
}

$ gcc -std=c99 t.c && ./a.out 

You are probably reading this on a computer on which the answers are "2147483648", "2147483648" and "-2147483648".

- page 1 of 2