c4-project / c4f

The C4 Concurrent C Fuzzer
MIT License
13 stars 1 forks source link

Fuzzer action: loops with deadcode-inducing breaks #200

Closed MattWindsor91 closed 3 years ago

MattWindsor91 commented 4 years ago

Morriset's PLDI'13 paper has an example that begins thus:

g1 = 1;

for (int l = 0; (l != 4); l++) {
    if (g1) return NULL;
    // ...dead code
}

The idea here is that we have a loop that outwardly looks live, but a conditional right at the start of the loop that is always true ensures the loop statically always breaks out.

Adding this to FIR might be a little involved, as the fuzzer has no understanding of 'statements after this statement are dead'. We'd need to add a new FIR construct that either introduces a new literal block, ie

if (f1) return NULL;
{
  // dead code
}

or a sort-of 'metadata only flow block' that can't be introduced by the abstraction from C, disappears in the concretisation to C, and doesn't factor into any round-trip calculations. The latter might be nice if we can introduce it, because it'll immediately strengthen the fuzzer's ability to handle deadcode.

MattWindsor91 commented 3 years ago

I've added this in a slightly different way: