c4f: the C4 fuzzer

c4f (previously known as act) is a 'fuzzer' over C litmus tests of a format broadly compatible with that produced by memalloy and consumed by herdtools7. It takes initial litmus tests, and performs transformations to them that complicate their compilation while (hopefully!) preserving the soundness of the initial test's postcondition.

Other parts of the C4 project include:

• c4t, for running automated compiler tests using c4f;
• c4-scripts, for doing various tasks that c4f and c4t are too low-level to do comfortably;
• c4-corpora, a set of Memalloy-generated inputs that can be used with c4f.

Licence and Acknowledgements

• The overall c4f project, and all original code, is licenced under the MIT licence: see LICENSE.

• The C lexer and parser are based on those from herdtools7. We include these in c4f under the provisos of herd's CECILL-B licence: see LICENSE.herd. (This is not an official endorsement by the Herd team of this project.)

Included programs

c4f consists of two programs:

• c4f, the fuzzer itself, with commands to run the fuzzer, replay fuzzer traces, and bisect fuzzer traces;
• c4f-c, a toolset for interpreting C litmus tests and dumping them to executable C.

Each command has various subcommands, including the help command: for example, c4f help will tell you information about which subcommands the fuzzer has.

Building and running

NOTE: c4f uses Jane Street's core library, which only works properly on POSIX-style operating systems. If you're using Windows, consider using WSL, or Cygwin, etc.

There are two main ways to build and run c4f:

• run opam install . (or make install) to install it on your machine as a pinned OPAM package; then, if your OPAM switch is in PATH, just run the tools directly;
• run its commands as dune exec TOOLNAME -- ...; this will automatically build c4f for you when needed, but won't work well with c4f's scripts, and won't automatically install dependencies. (The -- is needed to stop dune from trying to parse the arguments itself.)

You can also manually build c4f using dune build, or make (which just calls the former).

Preparation

c4f optionally accepts a configuration file listing fuzzer parameters. If you're using c4t, it sets up the configuration itself; if not, check c4f.conf.example for an idea of what goes in such a file, and use -config PATH to supply one.

Basic usage

To test whether c4f is installed and working, you can try:

$ git clone https://github.com/c4-project/c4-corpora /path/to/corpora
$ c4f run /path/to/corpora/partialSC/small/test_8.litmus

(or dune exec c4f -- run, per above)

This should output some truly horrendous C to stdout. (You can experiment with the other test_X.litmus files in that directory, supply your own Litmus test, or add -o path.litmus to write to a file.)