c4-project / c4f

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

Emit atomic-fetches that compare against negated addends #238

Closed MattWindsor91 closed 3 years ago

MattWindsor91 commented 3 years ago

A variant of #237 concerns rewriting things like (C syntax, but this happens at the x86 level)

if (atomic_fetch_add(x, y) > -y) {
   // ...
}

into something like

if (lock(x -= -y) > -y) {
  // ...
}

(and similarly for atomic_fetch_sub(x, -y)) with the idea that the locked subtract sets up the same flags on x86 that we'd use for the comparison anyway. We don't seem to hit this optimisation yet, so it might be worth having comparison generators that trip it.

MattWindsor91 commented 3 years ago

I think this would become a new if action set, something like:

Probably a set of actions that look like this: