c4-project / c4f

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

Use variables with equal KVs to satisfy reflexivity rules #236

Open MattWindsor91 opened 3 years ago

MattWindsor91 commented 3 years ago

If we have two variables x and y whose known value is the same, and we decide to construct a reflexivity rule (ie, x == f(x) -> true), we should be able to use y as f(x). As far as I remember, the fuzzer will only consider the known value of x or x itself here.

This has an actual purpose: when we generate cmpxchgs, the result of executing them will likely cause interesting known-value relationships between obj and expected, and we know of at least one LLVM optimisation that involves replacing comparisons between the old value of obj and expected with the output of the cmpxchg, so a judicious combination of good cmpxchg actions and this issue might provoke those better.

If it turns out the fuzzer already does this and I've forgotten about it, I'm going to look very silly.