c4f

Part of the C4 Project

What is c4f?

c4f mutates concurrent C test-cases, presented in the 'litmus test' format. It performs randomised changes to test-cases that refine the semantics of the test-case with respect to any observations over the original variables (for instance, the test's postcondition).

c4f aims to enhance test-cases by introducing things that complicate the compiler's analysis. These include:

c4f also contains some tools for replaying and bisecting fuzzing runs, and manipulating C litmus tests.

c4f is written in OCaml, and licenced predominantly under the MIT licence (some parts derive from Herdtools7, and are subject to the terms of its CECILL-B licence).

Features

Example

Suppose we have the following input litmus test (taken from c4-corpora):

C test_8

{ y = 0; x = 0; }

void
P0(atomic_int *y, atomic_int *x)
{
    int r0 = 0;
    r0 = atomic_load_explicit(x, memory_order_acquire);
    if (r0 == 1) { *y = 1; }
}

void
P1(atomic_int *y, atomic_int *x)
{ *y = 2; atomic_store_explicit(x, 1, memory_order_release); }

forall ((0:r0 == 0 /\ x == 1 /\ y == 2) \/ (0:r0 == 1 /\ x == 1 /\ y == 1))

c4f might 'fuzz' this test into the following:

C test_8

{ y = 0; x = 0; }

void
P0(atomic_int *x, atomic_int *y)
{
    int volatile r0 = 0;
    while (!(true || false) &&
    (0 <= 0 && 0 != -1390224 && 2147483647 != 2147483647))
    {
        if
        (((false ? 2147483647 : -1473764) ^ -131071 & (true ? 268435455 : 0))
        >=
        ((false ? 2147483647 : -1473764) ^ -131071 & (true ? 268435455 : 0)))
        {
            while ((true || !true && true && !true) <
            (true || !true && true && !true))
            {
                goto robust_bridge;
                while
                (((!(0 <
                        atomic_fetch_or_explicit(x, 0, memory_order_release))
                    ? 0 > atomic_fetch_or_explicit(y, 0, memory_order_relaxed)
                    ? r0 : 0 : atomic_load_explicit(x, memory_order_relaxed))
                    & r0)
                <= r0)
                {
                    r0--;
                    while (true ||
                    atomic_fetch_or_explicit(y, 0 | (false ? -5631 : 0),
                                                memory_order_seq_cst)
                    ==
                    atomic_fetch_sub_explicit(y, true ? -870673 & 0 : 0 !=
                                                2147483647 ? 0 : -19747598,
                                                memory_order_seq_cst)
                    &&
                    (atomic_fetch_sub_explicit(x, 0 - (false ? 0 : 0),
                                                memory_order_release)
                        !=
                        (false ? 0 :
                        atomic_load_explicit(x, memory_order_seq_cst))
                        || false))
                    { goto loud_vice; }
                    goto robust_bridge;
                }
            }
            goto phone;
            r0 = r0;
        } else { r0++; }
        goto loud_vice;
        for (; ; )
        {
            for (; ; )
            {
                do {  } while (!(true && true));
                while
                (atomic_fetch_xor_explicit(x, false ? 1 : 0 & 2147483647,
                                            memory_order_acq_rel)
                < (true ? 0 & 4 : 92 & 0)) { goto loud_vice; r0--; }
            }
            while (!false) {  }
        }
        r0++;
    }
    while ((false || false) && 0 > 0 && (true ? true : 0 > 0))
    {
        goto robust_bridge;
        while (!(0 == 0) || ((false ? false : false) || !true)) {  }
        goto loud_vice;
        for (; ; )
        {
            goto robust_bridge;
            for (; (false ? 32767 : true ? 0 : 0) + ((0 | 0) & 2147483647) ^
            (atomic_fetch_or_explicit(y, 0, memory_order_release) <= 0 &&
                true ? 2154366 ^
                atomic_fetch_add_explicit(x, 0 & 0, memory_order_relaxed) :
                atomic_load_explicit(x, memory_order_seq_cst) <
                atomic_fetch_sub_explicit(y, 0, memory_order_acquire) ? 0 : 0)
            & r0; )
            {
                goto loud_vice;
                if (false ? true : (5493101 != 0 && false) ==
                (5493101 != 0 && false))
                {
                    r0--;
                    phone: ;
                    while ((-2147483648 != 0 ? -2147483648 : 0) >
                    (-2147483648 != 0 ? -2147483648 : 0) &&
                    ((0 ^ -1) == (-2010 ^ 2147483647) ||
                        (10995223 == -178051316 ? 40281341 : 0) <=
                        (0 <= 0 ? 0 : 0) ||
                        ((-2147483648 | -1048576) == (0 ^ 0) || false)))
                    {  }
                } else
                {
                    for (; (2147483647 & 0 | 0 & 0 | (0 | 0) & -1) &
                    atomic_fetch_add_explicit(x, -1 & 0 ^ 0,
                                                memory_order_release);
                    ) { goto loud_vice; }
                }
                goto loud_vice;
            }
        }
        while (511 < 0 < (511 < 0) ? 0 != -67108864 || (true || false) || 11
        != 0 : true ? false : 0 != -7) { robust_bridge: ; }
    }
    loud_vice: ;
    r0 = atomic_load_explicit(x, memory_order_acquire);
    if (r0 == 1) { *y = 1; }
}

void
P1(atomic_int *x, atomic_int *y)
{
    if ((2147483647 ^ ((5 | -1) ^ (-365418550 ^ -1)) ^ (true ? 0 : -1)) <=
    (2147483647 ^ ((5 | -1) ^ (-365418550 ^ -1)) ^ (true ? 0 : -1)))
    {
        while (false && false && true ? (0 | 24827) != 0 : (0 | -8) !=
        (0 | -8)) {  }
        *y = 2;
        if (true && true && (true && true) ? 0 <= 0 : -8388607 ==
        (false ? 0 : 0)) { useless_house: ; } else
        {
            goto opulent_heap;
            for (; !true ? 0 : 0 + (true ? 0 : -1048576); )
            {
                while (true && true ? !true || true > true : 2147483647 ==
                (-2147483648 ^ 7328)) {  }
                while
                (!(false < false ? true && true : false ? 1 <= -12867131 :
                    true))
                {  }
                roost: ;
                goto opulent_heap;
            }
            goto roost;
            lane_2: ;
            for (; (false ? 1646789 : 18296147 & 0) !=
            atomic_load_explicit(y, memory_order_consume); )
            {
                goto fire_11;
                while (false)
                {
                    while
                    (!(false ||
                        !((0 <= 0 ?
                            atomic_fetch_add_explicit(x, 0,
                                                    memory_order_seq_cst)
                            : atomic_load_explicit(y, memory_order_consume))
                            < atomic_load_explicit(x, memory_order_relaxed))))
                    {
                        while ((true ? 0 : 0) + (true ? 0 : 0) <=
                        (-1 & (0 | 0)) ||
                        atomic_load_explicit(y, memory_order_relaxed) >
                        ((false ? -204 : 0) &
                            (false ?
                            atomic_load_explicit(x, memory_order_relaxed) :
                            atomic_load_explicit(y, memory_order_seq_cst))
                            |
                            atomic_fetch_sub_explicit(y, (true ? 0 : 0) ^ 0 & 0,
                                                    memory_order_acquire)))
                        {  }
                    }
                    while
                    ((0 != 0 ? 0 <= -1073741824 && false : false || false) &&
                    true) { opulent_heap: ; }
                    goto opulent_heap;
                }
            }
        }
        while (0 - 0 <= (0 + 0 | 2147483647) <
        (0 - 0 <= (0 + 0 | 2147483647))) {  }
        atomic_exchange_explicit(x, 1, memory_order_release);
        fire_11: ;
    } else { intern: ; }
}

forall ((0:r0 == 0 /\ x == 1 /\ y == 2) \/ (0:r0 == 1 /\ x == 1 /\ y == 1))