Pointer alignment verification

This blog post sums up what is the alignment constraint, its meaning for (common) hardware, how it has been derived at the C level and how Frama-C has been modified in version 32.0 (Germanium) to support the verification of this constraint and to support the keywords related to memory alignment.

In C, pointers are meant to store the address of objects in memory (or NULL), so that one can access these objects for reading or writing. An address is basically an integer value, and a simple way of thinking about such an operation during the execution is the following: the program reads the address (its integer value) and gets or sets the object starting from the memory cell whose number has this value (and subsequent memory cells if the object size is more than one). In practice, it is more complex than this, in particular when the program runs on top of an operating system, but it is not important for this blog post, so let us forget about that.

What is important is the fact that depending on what we load or store in memory, there exists a constraint on where we can do it: the alignment. This constraint originally comes from the hardware, but it has been derived at the level of the C programming language itself. If a program can perform a memory access that does not satisfy this constraint, it has an undefined behavior. Until version 32.0 (Germanium), this undefined behavior was not detected by Frama-C and some keywords related to the management of alignment were not supported.

If you already know about alignment in C, and only want to know what we have added in Frama-C, you can jump here.

Alignment in hardware

A CPU can only read words of a fixed size. A 32-bit processor can read a 4-byte word, a 64-bit processor can read 8-byte words. Furthermore, it can only do it at an address which is a multiple of the size of the word. This is a hardware constraint. If the program actually tries to read a smaller value that belongs to this word, it is OK: the CPU does the right shift and mask to get the actual value (note however, that when it is not aligned it might not be well optimized by the hardware), but if the value belongs to several words, the CPU would have to perform several loads to get the complete value. Depending on the architecture, either the CPU will do it, but it will be slower, or it is simply forbidden and causes an abort signal. Note that when the value is bigger than the word size, no instruction exists anyway for it, so the compiler will in fact have to transform the load into several loads (as a matter of fact, there are particular cases like SSE where the processor provides specific instructions that can load bigger values from the cache, but this post is already too technical).

A good way to make sure that it does not happen is to guarantee in the program that when the size of the value is smaller or equal to the word size, it must be aligned (at least) on its size (for example: char (1), short (2), int (4) on 32-bit architectures); and for a bigger value, that it is aligned at least on the size of the word, since several accesses are needed anyway (for example, on x86-32 bits, long long is aligned on 4 bytes, while it has size 8). Most types (we’re looking at you, long double) have a size that is a power of 2, and naturally, alignment follows the same trend, which gives the expected guarantees.

It is worth noting that when a value conforms to its given alignment, it also conforms to smaller alignments. If its address is a multiple of 4, it is also a multiple of 2. While the opposite is of course not true.

For any language implementation, the compiler thus must guarantee that the program will not perform any unaligned accesses and/or tell the users that when they do so, it is an error and the program has a bug …

Alignment in ISO C

C23 3.2

requirement that objects of a particular type be located on storage boundaries with addresses that are particular multiples of a byte address

Before entering into some details of the C standard, let us start with some good news: it is possible to write C code without caring at all about memory alignment from a safety point of view. If you never cast an integer or a pointer type to another pointer type and never use unions containing pointer types, the language rules prevent you from crafting an unaligned pointer (even if your pointers can have other problems, like being uninitialized).

This alignment constraint is precisely described in C23 6.2.8, whose paragraph 1 is quite clear:

Complete object types have alignment requirements which place restrictions on the addresses at which objects of that type may be allocated. An alignment is an implementation-defined integer value representing the number of bytes between successive addresses at which a given object can be allocated. […]

It is interesting to note that, because of this, even if we do not have to care about it directly, we can already observe the effect of the alignment constraint. Typically, in structures, to conform to this paragraph, the compiler needs to add padding bytes to guarantee that fields are correctly aligned according to the alignment of each type.

struct X {
  char c ;
  int  i ;
};

int main(void){
  struct X x = { 0, 0 };
  printf("sizeof(x): %lu\n", sizeof(x));
  printf("&x.c     : %p\n",  (void*) &x.c);
  printf("&x.i     : %p\n",  (void*) &x.i);
}

Example run:

sizeof(x): 8
&x.c     : 0x7ffc6aae91f0
&x.i     : 0x7ffc6aae91f4

We note that the size of the structure is 8 and not 5 (1 for char and 4 for int). The reason is that fields are not just put one after the other in memory, there is a gap between c and i to guarantee that i is correctly aligned for an int type in memory. And if we use the alignof operator to get the alignment constraint of int, we indeed get 4.

Now, we are in C. So, we want to be able to control alignment. The keyword _Alignas (alignas starting from C23) allows forcing the alignment of an object. For example, by writing:

_Alignas(long int) int x ;

We force the compiler to align x as if it were a long int. On x86-64, we could have also written:

_Alignas(8) int x ;

since the alignof(long int) is 8 and the standard allows providing a constant integer expression for the alignment. However, this alignment must be a valid alignment for int. That is: - a non-negative power of two (6.2.8 § 4), - stricter (= bigger - 6.2.8 § 5) than the alignment of the type (6.7.5 § 5), - lesser or equal to the maximum fundamental alignment (6.2.8 § 2), or - an allowed implementation-defined extended alignment (6.2.8 § 3).

The compiler detects violations of these rules (but beware, it will not check that the _Alignas specification is coherent across translation units and this may cause undefined behaviors). Thus, forcing the alignment of objects to a stricter alignment guarantees that it still conforms to the original one (if an object is aligned to 4, it is aligned to 8). Thus, taking the address of automatically allocated elements is always fine. Furthermore, the malloc function must return a pointer that has the maximum fundamental alignment allowed by the implementation so that it will always be correctly aligned for any type.

But in C, one can cast pointers.

C23 6.3.2.3 § 7

A pointer to an object type may be converted to a pointer to a different object type. If the resulting pointer is not correctly aligned for the referenced type, the behavior is undefined.

Thus, one may create unaligned pointers by conversion from another pointer type and this is an undefined behavior. We do not even need to dereference it, creating an unaligned pointer by pointer cast is already an undefined behavior.

int main(void){
  char c ;
  /* maybe undefined behavior depending on where c is, since on most
     implementations, alignof(char) is 1, while alignof(int) is 4.
  */
  int* p = (int*) &c ;
}

However, one can also create pointers from integers, but in this case, it is not immediately an undefined behavior if it is not aligned:

C23 6.3.2.3 § 5

An integer may be converted to any pointer type. Except as previously specified, the result is implementation-defined, might not be correctly aligned, might not point to an entity of the referenced type, and might produce an indeterminate representation when stored into an object.

This can be combined with the fact that converting a pointer to an integer type produces an implementation-defined value, as long as it can be represented:

C23 6.3.2.3 § 6

Any pointer type may be converted to an integer type. Except as previously specified, the result is implementation-defined. If the result cannot be represented in the integer type, the behavior is undefined. The result need not be in the range of values of any integer type.

Together, they allow us to transform the previous code as follows, where there is no undefined behavior:

int main(void){
  char c ;
  uintptr_t tmp = (uintptr_t) &c ;
  int* p = (int*) tmp ;
}

But anyway, trying to access this pointer if it is not aligned will still trigger an undefined behavior:

C23 6.5.3.2 § 4

The unary * operator denotes indirection. If the operand points to a function, the result is a function designator; if it points to an object, the result is an lvalue designating the object. If the operand has type “pointer to type”, the result has type “type”. If an invalid value has been assigned to the pointer, the behavior of the unary * operator is undefined ¹¹⁴⁾.

¹¹⁴⁾ […] Among the invalid values for dereferencing a pointer by the unary * operator are a null pointer, an address inappropriately aligned for the type of object pointed to, and the address of an object after the end of its lifetime.

Note that even if your hardware platform can safely (but slowly) perform unaligned accesses, it is an undefined behavior, and the compiler assumes that you do not have such accesses. It might optimize code with this assumption, which may introduce bugs. Pascal Cuoq already showed a few years ago an example where the compiler does such an optimization.

Thus, we would like to check that we never perform an unaligned memory access nor even create an unaligned pointer. It would be also interesting to check that the _Alignas specification is coherent across translation units.

Support in Frama-C

In version 32.0 Germanium, we extended the Frama-C kernel so that it can parse and correctly take into account C11+ alignment keywords. In particular, we now use the standard _Alignof/alignof keyword for platform-specific values detection, and not GCC’s __alignof__ operator anymore. This fixed a small bug related to the alignment of double on x86 32-bit machdeps. We also added support for the _Alignof/alignof keyword in ACSL and a new builtin predicate \aligned(p, n) that states p is aligned modulo n. The kernel is also able to detect incorrect alignas specifications, including inconsistent specifications across translation units.

A new alarm is available in Frama-C for unaligned pointers. It is enabled by default and controlled by the parameter -warn-unaligned-pointer. When a pointer type* is detected as unaligned, it generates an assertion:

//@ assert \aligned(ptr, alignof(type));

Which says “here, we should prove that ptr is aligned modulo alignof(type)”.

The Eva plug-in can now emit an alarm on potentially unaligned pointers. In our previous examples, Eva emits alarms on the created pointers. Note, however, that Eva (and other Frama-C plug-ins) are stricter than the ISO C; in particular, the example with the intermediate uintptr_t also produces an alarm, and can even produce invalid statuses for unaligned physical addresses (related to option -absolute-valid-range). A limitation is that Eva cannot learn from the value of the pointer, that is, reduce its post-state to a more precise one in which the pointer is always aligned. If you really need this kind of feature, contact us.

We applied Eva on the Open Source Case Studies repository with this new detection capability. It has generated a reasonable amount of new alarms. Most of them are related to the fact that the value of the incriminated pointer was imprecise anyway; a few additional true alarms have been found, but we have to further investigate to check whether they really have an impact. Overall, the cost of this new detection is barely noticeable.

Similarly, the RTE plug-in has been extended to generate assertions related to unaligned pointers. Like Eva, it can generate invalid statuses for physical addresses. A few optimizations are available to avoid generating alarms taking the address of automatic variables, provided that the address of the pointer itself is never taken by the program. We will come back to this further in this post.

The E-ACSL plug-in has been extended to correctly translate the \aligned predicate into C code. Combined with the RTE plug-in, it thus can detect unaligned pointers at runtime. For example, on our previous code sample:

$ e-acsl-gcc example.c --rte=all -O out && ./out.e-acsl
... compilation ...

example.c: In function 'main'
example.c:5: Error: Assertion failed:
    The failing predicate is:
    rte/pointer_alignment:
        \aligned(&c1,alignof(int)).
    With values at failure point:
    - rte: pointer_alignment: \aligned(&c1,alignof(int)): 0
    - &c1: 0x7ffdcead605d
    - alignof(int): 4

The WP plug-in does not support alignment verification. But why? Because the default memory model of WP is the Typed memory. It assumes that the program is well-typed. Thus, it assumes that you never cast pointers to other pointer types, nor unions. It thus does not make sense to verify this with this model. The experimental Bytes model would be the right place to add this feature, but it is a work in progress. We will certainly add this feature, but it is not the priority right now.

About the generation of alarms by Eva and RTE: since we forbid the creation of unaligned pointers, no matter if it is from a pointer or an integer, we could stop at this point. However, there is an undefined behavior that is currently not handled by Frama-C and even deliberately used by developers in existing projects which is breaking the strict-aliasing rule (note that it does not exist with this name in the ISO C standard). And when we do this, we can easily forge pointers that are unaligned without converting the pointer itself:

char c[sizeof(int) + 1];
int *tmp;
*((char **)&tmp) = c + 1;
int *p = tmp;

Thus, we still generate potential alarms when pointers are used for dereferencing, and not only for pointer conversions.

A few problems have been fixed with the GCC attributes __aligned__ and packed, but we still have some work on this topic; in particular, for corner cases like this one, where GCC developers are apparently not completely sure of what should be done (and other compilers have trouble following exactly what GCC does).

Acknowledgments

We thank the DGA (Direction Générale de l’Armement) and the AID (Agence de l’Innovation de Défense) for their support in implementing this feature.