Skip to content

Narrowing from widening thresholds#1502

Merged
michael-schwarz merged 8 commits intogoblint:masterfrom
Red-Panda64:narrowing-thresholds
Jun 11, 2024
Merged

Narrowing from widening thresholds#1502
michael-schwarz merged 8 commits intogoblint:masterfrom
Red-Panda64:narrowing-thresholds

Conversation

@Red-Panda64
Copy link
Copy Markdown

@Red-Panda64 Red-Panda64 commented Jun 4, 2024

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 sim642 self-requested a review June 4, 2024 14:26
@sim642
Copy link
Copy Markdown
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
Copy Markdown
Author

Red-Panda64 commented Jun 4, 2024

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
sim642
sim642 reviewed Jun 5, 2024
View reviewed changes
@Red-Panda64
Copy link
Copy Markdown
Author

Red-Panda64 commented Jun 5, 2024

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 reviewed Jun 11, 2024
View reviewed changes
@michael-schwarz michael-schwarz merged commit bbf24be into goblint:master Jun 11, 2024
@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
@sim642
[new release] goblint (2.4.0)
38186e2 
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).
@sim642 sim642 mentioned this pull request Aug 2, 2024
Merged
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
@sim642 @avsm
[new release] goblint (2.4.0)
2afe816 
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

Reviewers

@sim642 sim642 sim642 approved these changes

@michael-schwarz michael-schwarz michael-schwarz approved these changes

Assignees

No one assigned

Labels

feature precision student-job

Projects

None yet

Milestone

v2.4.0

Development

Successfully merging this pull request may close these issues.

3 participants

@Red-Panda64 @sim642 @michael-schwarz