Although WHOOP itself analyzes Boogie code, it seems that the Chauffeur component of their pipeline does some ad hoc rewriting of C code itself.
Moreover, c/pthread-driver-races in sv-benchmarks originate from WHOOP, although data races are checked by a value assertion. Unfortunately, sv-benchmarks only contains 2 out of 16 drivers mentioned in the paper and they're the smallest ones.
Nevertheless, the sv-benchmarks show a relatively thin main function harness to instantiate and invoke the driver hooks. This isn't mentioned anywhere, but the sv-benchmarks versions seem to have been generated using this fork: https://github.com/MontyCarter/chauffeur. So it might be good to get the other 14 drivers into pure C programs as well.
I tried to compile that in a LLVM 3.5 Docker container but got linking errors for a number of LLVM/Clang functions, so I couldn't get it to run. Maybe someone more familiar with LLVM knows how to fix the issue (@michael-schwarz?).
WHOOP is the tool presented by the article Fast and precise symbolic analysis of concurrency bugs in device drivers.
Although WHOOP itself analyzes Boogie code, it seems that the Chauffeur component of their pipeline does some ad hoc rewriting of C code itself. Moreover,
c/pthread-driver-racesin sv-benchmarks originate from WHOOP, although data races are checked by a value assertion. Unfortunately, sv-benchmarks only contains 2 out of 16 drivers mentioned in the paper and they're the smallest ones.Nevertheless, the sv-benchmarks show a relatively thin
mainfunction harness to instantiate and invoke the driver hooks. This isn't mentioned anywhere, but the sv-benchmarks versions seem to have been generated using this fork: https://github.com/MontyCarter/chauffeur. So it might be good to get the other 14 drivers into pure C programs as well.I tried to compile that in a LLVM 3.5 Docker container but got linking errors for a number of LLVM/Clang functions, so I couldn't get it to run. Maybe someone more familiar with LLVM knows how to fix the issue (@michael-schwarz?).