Skip to content

Refactor loopUnrolling autotuner#1582

Merged
karoliineh merged 9 commits intomasterfrom
refactor-loopUnroll
Sep 30, 2024
Merged

Refactor loopUnrolling autotuner#1582
karoliineh merged 9 commits intomasterfrom
refactor-loopUnroll

Conversation

@karoliineh
Copy link
Copy Markdown
Member

@karoliineh karoliineh commented Sep 27, 2024

Refactor some code in loopUnrolling.ml, simplifies the following:

  • Use Log instead of printing to stderr
  • Improve debug messages and simplify their syntax
  • Make sure the goal (bound) of the loop is found from the exact same loop statement comparison expression where the var was found
  • Move functions defined in fixedLoopSize to top level to make function definitions' style consistent
  • Use let* option monad syntax from GobOption.Syntax in LoopUnrolling

@karoliineh karoliineh added the cleanup Refactoring, clean-up label Sep 27, 2024
@karoliineh karoliineh requested a review from sim642 September 27, 2024 19:24
@karoliineh karoliineh self-assigned this Sep 28, 2024
@sim642 sim642 added this to the SV-COMP 2025 milestone Sep 30, 2024
sim642
sim642 approved these changes Sep 30, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The conflict with master now needs resolving too.

@michael-schwarz michael-schwarz self-requested a review September 30, 2024 08:02
@karoliineh karoliineh merged commit 1f2bb69 into master Sep 30, 2024
@karoliineh karoliineh deleted the refactor-loopUnroll branch September 30, 2024 13:27
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 28, 2024
@sim642
[new release] goblint (2.5.0)
944a275 
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).
@sim642 sim642 mentioned this pull request Nov 28, 2024
Merged
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

@karoliineh karoliineh

Labels

cleanup Refactoring, clean-up

Projects

None yet

Milestone

SV-COMP 2025

Development

Successfully merging this pull request may close these issues.

3 participants

@karoliineh @sim642 @michael-schwarz