Using the Optimizer to Prove Safety Properties at Compile Time

Martin Uecker, 2026-05-22

Introduction

Previously, when I discussed maybe, I pointed out that the optimizer can be used to prove that there is no undefined behavior related to integer operations (or array bounds) left in some function. The idea is to use the undefined behavior sanitizer in trapping mode to instrument the code with run-time checks, and then verify that the optimizer eliminates the checks because they can not be triggered under given preconditions.

Unfortunately, it is not to practical to inspect the assembly code for larger programs. Here, I want to share a trick which works with GCC to transform those run-time checks into compile-time warnings or errors.

As an example, we consider a bug related to the rules for integer promotion which affected a crypto library as discussed here. The issue in the following code is that the unsigned eight-bit integer with all bits set gets promoted to an signed integer. If the integer type has 32 bits, shifting left by 24 bits shifts into the sign bit which has undefined behavior.

uint8_t start = -1;
printf("%x\n", start); // prints 0xff

uint64_t result = start << 24;
printf("%llx\n", result); // should print 00000000ff000000, but will print ffffffffff000000

result = (uint64_t)start << 24;
printf("%llx\n", result); // prints 00000000ff000000
	

We can use the shift sanitizer to detect this problem at run-time (Example on Godbolt). This is intended to help with finding bugs during testing and can be very effective whe used with fuzzing. Sanitizers can also be used to safely avoid the undefined behavior at run-time when used with trapping to terminate the program. Still, it would be much better (and sometimes this is a requirement) to make sure already during development that the code is statically safe and can never fail at run-time.

Amazingly, when using GCC prefixing the code with the declaration

[[gnu::warning("UNSAFE")]] void __builtin_trap();
	

achieves just this! For the example above, this then produces the following output (Example on Godbolt).

: In function 'main':
:15:29: warning: call to '__builtin_trap' declared with attribute warning: UNSAFE [-Wattribute-warning]
   15 |     uint64_t result = start << 24;
	

Why does this work? The sanitzer inserts calls to the built-in function __builtin_trap. For some reason, it is possible to add an explicit declatation to this function and an attribute can then be used to tell the compiler to emit a warning (or error) whenever a call to the function is not eliminated by an optimization.

The example for maybe modified to use this trick can be found here.

Unfortunately, this warning can not be controlled at a fine level and also does not provide too much information. Instrumented code is also sometimes still poorly optimized on GCC, which makes this less effective than it could be. Nevertheless, this can be quite useful already, and hopefully GCC's support for this technique will be improved in the future.

BTW: For those confused about C's conversion rules, it might be helpful to study some macros that implement the logic here for integer promotion and here for the usual arithmetic conversions, repectively.