-
Notifications
You must be signed in to change notification settings - Fork 42
Profiles and new platform support
If a program is strictly-conforming, then the basic C semantics with no extensions should be enough to interpret that program and detect undefined behavior. But the reality of how C is actually used means it is much more common for programs to depend on implementation-specific details of particular hardware or software platforms. Profiles are meant to allow the interpreter generated from the C semantics to analyze programs in the context of such platform-specific behavior.
Platform-specific extensions and behavior should optimally be confined to a profile. These behaviors can broadly be understood as behaviors originating from the compiler, the operating system, or the underlying hardware. We have broken them down into more specific categories below.
- Command-line interface/flags -- the specifics of the interface a particular compiler uses need to be supported for RV-Match to be able to replace that compiler in a build system.
- Preprocessor macros and extensions
- Implementation-specific choices
- Language extensions: pragmas, attributes
- Language extensions: built-in functions
- Language extensions: new syntax -- parser, semantics extensions
- Operating system interface and libraries
- Native execution/FFI support
The list of installed profiles can be queried with kcc -version. We currently support a few different profiles, all based on gcc and x86_64:
-
x86_64-linux-gcc-glibc-- the default profile intended to act as a drop-in replacement for gcc with-std=c11set. -
x86-gcc-limited-libc-- like thex86_64-linux-gcc-glibcprofile, except that it has limited support for the C standard library because it does not use the standard library implementation installed on the system. This is similar to the profile the open source semantics uses: https://github.com/kframework/c-semantics/tree/master/profiles/x86-gcc-limited-libc -
x86_64-linux-gcc-glibc-reverse-eval-order-- like the abovex86_64-linux-gcc-glibcprofile, except rules are evaluated in the reverse order, which can sometimes find errors due to non-determinately sequenced expressions. -
x86_64-linux-gcc-glibc-gnucandx86_64-linux-gcc-glibc-gnuc-reverse-eval-order-- these are profiles are both analogous to the similarly-named ones above, except they are meant to behave like gcc with-std=gnu11, which is the default behavior of gcc and might be required in certain cases. Functionally, these profiles provide the same GNUC language extensions as the ones above, the only difference is the value of feature-test macros.
In the past, we have also experimented with an 78k0r profile.
All of the above profiles are based on the behavior of gcc. Here we outline the extensions to the basic C semantics these profiles support in each of the categories mentioned above.
The command line interface to Match is provided by the kcc script, which is intended to be compatible with gcc. It supports many of gcc's most commonly-used flags. Supporting other another compiler's interface would generally require writing a similar wrapper script.
The current state of the command line interface supported by kcc can be seen with kcc --help. The actual command line parsing done by kcc happens here:
https://github.com/kframework/c-semantics/blob/master/scripts/RV_Kcc/Opts.pm
Extending kcc to support more flags would start by updating this file with the new flags.
Currently, kcc uses gcc as a C preprocessor. The default profile also unsets the __GNUC__ feature-test macro in order to discourage the use of GNU language extensions.
The preprocessor used by Match is set by the profile. E.g., this is the preprocessor used by the open source profile:
https://github.com/kframework/c-semantics/blob/master/profiles/x86-gcc-limited-libc/pp
The semantics