Open karoliineh opened 3 months ago
On entire sv-benchmarks runs with 60s, this doesn't really make any difference to our score (after the second fixes). Some tasks (loop-lit/hh2012-ex1b) go from <1s to 60s TIMEOUT, embarrassingly many are from goblint-regression. Some tasks (list-simple/dll2n_remove_all) go from true to unknown, which is particularly odd. With the 60s time limit, we gain only 6 new true results.
While this PR makes the fixed loop unrolling work for the first time ever, the lack of positive impact suggests we need to rethink our loop unrolling because there are dubious things going on.
In SV-COMP no-overflow tasks there are cases similar to the following example:
where the loop has a fixed size of iterations from
i == 0
toi == 99
, which the autotuner is unable to detect because it only relies on finding the starting value through assignments.As the CIL representation of the if-statement
if (!(i==0 && j==0)) return 0;
is too complicated to extract the value from there, I opted for assuming that if the variable is not assigned to a constant value before the loop, its' value is 0.This revealed another bug, which makes me wonder if the autotuner even was ever able to find any fixed-size loops previously, as it checked for the condition:
using the loop statement itself, not its body, making it always think that there is a nested loop present that is also modifying the loop variable.
Also, loops with size 100 were deemed too big to unroll if there were more than 0 instructions (function calls or assignments) in the loop.