c4-project / c4f

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

Exploit short circuiting in Boolean operators #226

Open MattWindsor91 opened 3 years ago

MattWindsor91 commented 3 years ago

The fuzzer's algebraic rules table captures rules such as x || true = true || x = true, which are useful for generating convoluted expressions with known final values. These are useful for making the compiler consider conditional atomic action evaluations, but one thing that we're missing is testing whether the compiler avoids evaluating side-effects of atomic actions altogether when those operators are short-circuited out.

For example, we could generate fun expressions such as:

int x = 4004;
if (x == 4004 || atomic_fetch_add(&y, 24) == 6) { foo; }

and, as far as I understand it, the short-circuiting semantics of || should kick in and cause y to be unmodified.

johnwickerson commented 3 years ago

Good idea!

MattWindsor91 commented 3 years ago

There's already some code that distinguishes between short-circuiting and non-short-circuiting operators: https://github.com/MattWindsor91/act/blob/1f41f7e7ddb7883cdae53613b35727f6b19f221f/lib/fir_gen/src/expr.ml#L446-L469 but it currently delegates to Bool_values.quickcheck_generator, which is always careful to generate side-effect-free Boolean expressions. Ideally, the short-circuiting version should delegate to a broader generator that can generate side-effects (either in how it generates Booleans, or how it generates integers that it feeds to relational operators), but I'd have to think about how to do so in a way that doesn't either duplicate code or make that generator module even less readable than it currently is...