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

Fix and refactor syntactic loop unrolling #1369

Merged
merged 14 commits into from
Feb 26, 2024
Merged

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Feb 21, 2024

While working on fixing loop heads in YAML witnesses, I wanted to finally implement a cleaner fix to #1225 than #1248 by recording somewhere which statements came from loop unrolling.
To do this, I wanted to refactor things a bit and added cram tests to make sure I don't accidentally break anything. But I also discovered that continues are mishandled in loop unrolling from #563.

Changes

  1. Add cram tests for loop unrolling.
  2. Mark unrolled loop head labels as not originating from input code but transformations, like CIL does.
  3. Fix continue in loop unrolling. Due to (double) refs, there was undesirable sharing which caused all unrolled iterations to jump directly to the unrolled part, not to the next unrolled iteration as intended. Imperative programming is again dangerous.
  4. Add option dbg.justcil-printer to allow cram testing justcil output without clutter from line directives and builtin declarations.
  5. Remove excessive blocks from loop unrolling output.
  6. Remove goblint_array_domain attribute from non-array variables.

@sim642 sim642 added cleanup Refactoring, clean-up bug testing labels Feb 21, 2024
@sim642 sim642 self-assigned this Feb 21, 2024
@michael-schwarz
Copy link
Member

Nice catch! Do you think you can also craft an example where the better handling of continue means that an assertion that was previously failing now succeeds?

@sim642
Copy link
Member Author

sim642 commented Feb 21, 2024

There's now a test that fails on master.

@sim642 sim642 marked this pull request as ready for review February 21, 2024 14:30
@sim642 sim642 added this to the v2.4.0 milestone Feb 21, 2024
@michael-schwarz michael-schwarz self-requested a review February 21, 2024 16:24
@sim642 sim642 merged commit 0af40a3 into master Feb 26, 2024
19 checks passed
@sim642 sim642 deleted the loop-unrolling-refactor branch February 26, 2024 13:08
sim642 added a commit that referenced this pull request Feb 26, 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
Labels
bug cleanup Refactoring, clean-up testing
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants