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.

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

Improve loop bound detection for loop unrolling by handling casts in loop statements #1599

Merged
merged 2 commits into from
Oct 15, 2024

Conversation

karoliineh
Copy link
Member

Inspired by an unreach-call task num_conversion_1.c where we couldn't detect a bound for the following loop:

unsigned char c;
c = 0;
while (c < (unsigned char) 8) {
  ...
}

Unrolling the loop 8 times here helps us solve the task. In addition to the case in this program, where the loop statement is in the form CastE(TInt(int, ), Lval(Var(c, NoOffset))) < Const(Int(8,int,None)) I included all possible combinations of casting for both the left and right expressions in the loop comparison statement.

@karoliineh karoliineh added sv-comp SV-COMP (analyses, results), witnesses precision labels Oct 15, 2024
@karoliineh karoliineh added this to the SV-COMP 2025 milestone Oct 15, 2024
@karoliineh karoliineh requested a review from sim642 October 15, 2024 10:24
src/util/loopUnrolling.ml Outdated Show resolved Hide resolved
@karoliineh karoliineh requested a review from sim642 October 15, 2024 13:23
@sim642 sim642 merged commit d120e34 into master Oct 15, 2024
21 checks passed
@sim642 sim642 deleted the loopUnroll-casts-in-loopStatment branch October 15, 2024 17:47
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 28, 2024
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2025.

* Add 32bit vs 64bit architecture support (goblint/analyzer#54, goblint/analyzer#1574).
* Add per-function context gas analysis (goblint/analyzer#1569, goblint/analyzer#1570, goblint/analyzer#1598).
* Adapt automatic static loop unrolling (goblint/analyzer#1516, goblint/analyzer#1582, goblint/analyzer#1583, goblint/analyzer#1584, goblint/analyzer#1590, goblint/analyzer#1595, goblint/analyzer#1599).
* Adapt automatic configuration tuning (goblint/analyzer#1450, goblint/analyzer#1612, goblint/analyzer#1181, goblint/analyzer#1604).
* Simplify non-relational integer invariants in witnesses (goblint/analyzer#1517).
* Fix excessive hash collisions (goblint/analyzer#1594, goblint/analyzer#1602).
* Clean up various code (goblint/analyzer#1095, goblint/analyzer#1523, goblint/analyzer#1554, goblint/analyzer#1575, goblint/analyzer#1588, goblint/analyzer#1597, goblint/analyzer#1614).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
precision sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants