Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add termination analysis success messages for loop bounds #1580

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Add termination analysis success messages for loop bounds #1580

wants to merge 3 commits into from

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Sep 27, 2024

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 sim642 added cleanup Refactoring, clean-up feature usability sv-comp SV-COMP (analyses, results), witnesses labels Sep 27, 2024
@sim642 sim642 added this to the v2.5.0 milestone Sep 27, 2024
@sim642
Copy link
Member Author

sim642 commented Sep 27, 2024

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.

@sim642 sim642 mentioned this pull request Oct 29, 2024
Open
@jerhard
Copy link
Member

jerhard commented Oct 29, 2024 •
edited
Loading

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
Copy link
Contributor

hseidl commented Oct 29, 2024 via email

@sim642 sim642 modified the milestones: v2.5.0, v2.6.0 Nov 26, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
cleanup Refactoring, clean-up explainability feature sv-comp SV-COMP (analyses, results), witnesses usability
Projects
None yet
Milestone
v2.6.0
Development

Successfully merging this pull request may close these issues.

Success messages with bounds from termination analysis
3 participants
@sim642 @jerhard @hseidl