C standard library for CN

[yav]

The Problem

To verify and test things with CN we need a C standard library. Using the library that's pre-installed on the system is probably not a good plan, because:

• We may need to defined things in a way that is better suited for CN
• We need to provide specifications for the functions in the standard library, so we can prove/check stuff.

So we need a custom C standard library to use when CN is processing C files. For verification purposes, we only need the specifications of the functions in the library, however, to run executable specifications and tests we need actual implementations of the functions in the library, and we'd like to reuse the existing library rather than reimplementing the entire C standard library.

Proposed Solution

We'll define a library called cn_libc, which is essentially a wrapper around the C standard library defined on the system.
cn_libc consists of a collection of header (.h) and implementation (.c) files. The headers contain:

• opaque types (types whose implementation is not visible to the users)
• non-opaque types (e.g., structs with predefiend fields)
• function declarations

The functions in the .c implementation of cn_libc will start with a cn_ prefix, to avoid confusion with the corresponding function in the system's C standard library. Typically, they will be implemented by just calling the
relevant standard library function. For example, cn_stdio.c might contain a line like this:

FILE *cn_fopen(const char *restrict pathname, const char *restrict mode) { return fopen(pathename, mode); }

Of course, we'd like users of cn_libc to be able to use the normal names for functions (i.e., without the cn_ prefix). To achieve this, the headers of cn_libc would contain conditional renaming preprocessing directives as follows:

FILE *cn_fopen(const char *restrict pathname, const char *restrict mode);
#ifdef CN_USER_MODE
#define fopen cn_fopen
#endif

In this way, users can write fopen(...) or &fopen and the resulting code will be cn_fopen(...) or &cn_fopen.
This works because names from the C standard library are reserved, and users are not supposed to shadow them
(e.g., it is not ok to define a local variable called fopen).

For opaque types, such as FILE, the headers of cn_libc will provide a dummy definition, for example:

#ifdef CN_USER_MODE
typedef struct { int dummy; } FILE;
#endif

Since these are opaque, they can only be manipulated via pointers, so the definitions should not matter in the proofs. There is a potential problem that someone might write sizeof(FILE) and then you'd get different things when proving things vs. when testing things, but it is not quite clear on what that means anyway, as FILE is supposed to be opaque.

In the implementation (.c) files, we'll just omit these and use the declarations from the system library instead.

Non-opaque types are the trickiest, and for those we'd just have to copy the definition from the system library into CN's library, and we'll need to update CN's standard library if the system libraries ever change. Fortunately, I think this happens quite rarely for the C standard library.