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

Narrowing from widening thresholds #1502

Merged
merged 8 commits into from
Jun 11, 2024

Conversation

Red-Panda64
Copy link
Contributor

This PR allows narrowing of integer intervals when the bound being narrowed is a widening threshold. Beforehand, when an interval was widened to a threshold and the threshold fit (e.g. widen [0, 0] [0,1] = [0, 10] for an upper threshold 10), it could no longer be narrowed (even if []). This is because int intervals implement accelerated narrowing and will only narrow from from maximal upper or minimal lower bounds.
This PR will use the more precise bound, only when old bound is maximal/minimal or an upper/lower threshold. The narrowing must still terminate, since upper/lower bounds can only shrink/grow as often as there are thresholds.

Example:

int main() {
    int i;
    for(i = 0; i < 10 && i < 20; i += 3);
    __goblint_check(i <= 12);
}

The i < 20 condition is only in this example to be identified as an upper threshold.
Without this PR, the invariant cannot be shown when wideningThresholds are enabled: i is first widened to [0, 10], then [0, 20] at the loop head. Then, the narrowing iteration cannot reduce i to the more precise interval [0, 12]. With these changes, the more precise interval is inferred.

@sim642
Copy link
Member

sim642 commented Jun 4, 2024

Interval sets also use the widening thresholds, so it would make sense for them to also support this logic, if they already don't.

@sim642 sim642 changed the title Narrowing thresholds Narrowing from widening thresholds Jun 4, 2024
@Red-Panda64 Red-Panda64 force-pushed the narrowing-thresholds branch from f2b6ea8 to 2c9534e Compare June 4, 2024 18:32
@Red-Panda64 Red-Panda64 force-pushed the narrowing-thresholds branch from 2c9534e to d6456c8 Compare June 4, 2024 19:01
@Red-Panda64
Copy link
Contributor Author

Good point. I've made that adjustment. Also, I have fixed an oversight I made: before, the narrow operator did not have to explicitly check whether the new bound is more precise, because it would only change the bound if the previous value was maximal/minimal. Now it does have to check.

@michael-schwarz michael-schwarz self-requested a review June 4, 2024 19:24
src/cdomain/value/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomain/value/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomain/value/cdomains/intDomain.ml Outdated Show resolved Hide resolved
@Red-Panda64
Copy link
Contributor Author

I've also now added a unit test to make the modified narrow operator does indeed narrow from thresholds and does not permit growth. The test applies to intervals and interval sets, as well as upper and lower bounds.

@sim642 sim642 self-requested a review June 6, 2024 10:30
@michael-schwarz michael-schwarz merged commit bbf24be into goblint:master Jun 11, 2024
12 checks passed
@sim642 sim642 added this to the v2.4.0 milestone Jun 11, 2024
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 2, 2024
CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants