search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Disable SV-COMP syntactic loop unrolling #1402

Closed sim642 closed 3 months ago

sim642 commented 3 months ago

This is cherry-picked from #1372 in preparation for it to get merged: https://github.com/goblint/analyzer/pull/1372#discussion_r1526572811.

I benchmarked the equivalent change at be3ee1d80: https://goblint.cs.ut.ee/results/158-rm-loop-unroll-after/table-generator-cmp.diff.html. This costs us ~100 tasks, mostly from nla-digbench-scaling/_unwindbound and product-lines/elevator_spec. The actual delta is that we lose ~130 true verdicts, but also gain ~30 true verdicts (from cases where unrolling causes excessive resource usage). The nightly BenchExec run will give a more up-to-date comparison, but I don't expect it to be different since nothing notable has been changed in SV-COMP analyses in this time.

To get this back, we'll have to finalize #1370 for SV-COMP 2025.

michael-schwarz commented 3 months ago

To get this back, we'll have to finalize https://github.com/goblint/analyzer/pull/1370 for SV-COMP 2025.

This is under the assumption that the same behavior can be achieved there, which is not a given, e.g., vis-a-vis automatic detection of widening points or the termination analysis.

sim642 commented 3 months ago

Closing since #1403 made it redundant for #1372.