Add termination analysis success messages for loop bounds

[sim642]

Closes #1577.

These are disabled by default, but can be enabled with dbg.termination-bounds.

Also cleans up the implementation of LoopTermination.special in general (pointless else (), too wide try scope, annoying half-indentation).

[sim642]

Although this doesn't really explain the case from #1577:

./goblint --conf conf/svcomp.json --set ana.specification ../sv-benchmarks/c/properties/termination.prp ../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c --html --enable dbg.termination-bounds

outputs (among other things)

[Success][Termination] Loop terminates: bounded by 0 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 1 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 2 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 3 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 4 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 5 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 6 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 7 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 8 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by 9 iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)
[Success][Termination] Loop terminates: bounded by (Not {0, 1}([0,32]),[10,2147483896],not {0} ([0,32]),ℤ) iteration(s) (../sv-benchmarks/c/termination-crafted-lit/KroeningSharyginaTsitovichWintersteiger-CAV2010-Fig1.c:17:9-17:16)

The maximum bound 2147483896 is one lower, but that's just because we activate congruence analysis we can rule out 2147483897 (which is is excluded because it is odd). And we don't go to top because we assume no overflows, so 2147483896 + 2 doesn't overflow to top. But if it were to be a loop incrementing by one, this could go up to 2147483897 and we consider it unbounded. So I'm a bit confused by the termination checking logic with this.

[jerhard]

Regarding our discussion at today's Gobcon, whether it suffices to exclude that the abstract value for the artificially introduced loop counter variable is top: As for an artificial loop counter i it is ensured that i is incremented by one in each iteration, if the loop is ounbounded, i will receive every possible value (even if any finite number of unrollings is performed). Thus, if our analysis is sound, i should have the top value for i (which is of unsigned type).

As a side note, the artificial loop counter should have an unsigned integer type, and thus should not be affected by the analyzer assuming that signed overflows do not happen.

[hseidl]

… but it should never wrap around, though :-)     HelmutAm 29.10.2024 um 14:59 schrieb Julian Erhard @.***>: Regarding our discussion at today's Gobcon, whether it suffices to exclude that the abstract value for the artificially introduced loop counter variable is top: As for an artificial loop counter i it is ensured that i is incremented by one in each iteration, if the loop is ounbounded, i will receive every possible value (even if any finite number of unrollings is performed). As a side note, the artificial loop counter should have an unsigned integer type, and thus should not be affected by the analyzer assuming that signed overflows do not happen.

—Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you are subscribed to this thread.Message ID: @.***>