Instrument traces benchmarks with assertions - Githubissues

goblint / bench

The benchmark suite

4 stars 5 forks source link

Instrument traces benchmarks with assertions #30

Closed sim642 closed 2 years ago

sim642 commented 2 years ago

This is currently on top of #28.

The assertions are added by the assert transformation using the following criteria:

only after locks,
only from apron analysis,
using cluster12 privatization,
no apron invariants are filtered out.

Then all the configurations are run on the instrumented benchmarks and assertion results counted. The results are currently available here: https://goblint.cs.ut.ee/simmo-results/goblint-bench_result-traces-rel-assert/. Notably:

Some benchmarks have zero (or close to it) assertions added since there's barely any locks.
Some fail to parse because assertions about globals are inserted before the globals are declared in the merged file.

Using https://github.com/goblint/analyzer/pull/768, we can reprove more invariants: https://goblint.cs.ut.ee/simmo-results/goblint-bench_result-traces-rel-assert3-no-pthread/.

sim642 commented 2 years ago

These aren't super useful, but I'm merging this such that #31 could be merged quickly.