Re-evaluate defaults for `ana.malloc.unique_address_count` in SV-Comp

sim642 commented 1 year ago

This was changed to 5 in #1234, so I suppose we can consider it done for now?

michael-schwarz commented 1 year ago

This was only changed for MemSafety, one might want to re-evaluate it also for the other categories.

karoliineh commented 5 months ago

@sim642 made a run with --set ana.malloc.unique_address_count 1 on sv-benchmarks with no-overflow property. This gives 31 new correct results with a 60s timeout. However, it costs us a 14% slowdown as well.

So, for the best-case scenario, we should

[x] try to autotune it so that we only set ana.malloc.unique_address_count > 0 for programs with allocs that are not in loops and see if that helps with the loss in performance;
[ ] try out different values to see which is the best default for no-overflows;
[ ] inspect other categories in addition to MemSafety and no-overflows.

However, if we do not manage to do all that before SV-COMP 2025, we could at least enable it with 1 for no-overflows.

sim642 commented 1 month ago

However, if we do not manage to do all that before SV-COMP 2025, we could at least enable it with 1 for no-overflows.

This should be a fairly simple change to do now, so feel free to open a PR. I think I still have the 60s no-overflows run diff here: https://goblint.cs.ut.ee/results/191-no-overflow-pr-1511-before-alloc-1/table-generator-cmp.diff.html#/. We can postpone other additional improvements to SV-COMP 2026 then.

goblint / analyzer

Re-evaluate defaults for `ana.malloc.unique_address_count` in SV-Comp #1168