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.

Sign up for GitHub

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

Jump to bottom

Provide per-fundec context gas #1569

Closed
michael-schwarz opened this issue Sep 20, 2024 · 0 comments · Fixed by #1570
Closed

Provide per-fundec context gas #1569

michael-schwarz opened this issue Sep 20, 2024 · 0 comments · Fixed by #1570
Assignees
@michael-schwarz
Labels
feature in progress performance Analysis time, memory usage precision
Milestone
v2.5.0

Comments

@michael-schwarz
Copy link
Member

For the extended version of the rabbit hole paper, we want to experiment with providing a lower context gas that is instead tracked per fundec.

In this way, only calls to functions for which the gas has been exhausted are analyzed without context, but any function called from such functions will be analyzed context-sensitively again to limit the precision loss in cases where it is not required for termination.
@michael-schwarz michael-schwarz self-assigned this Sep 20, 2024
@michael-schwarz michael-schwarz added the performance Analysis time, memory usage label Sep 20, 2024
@michael-schwarz michael-schwarz mentioned this issue Sep 20, 2024
Merged
@sim642 sim642 added this to the v2.5.0 milestone Nov 18, 2024
sim642 added a commit to sim642/opam-repository that referenced this issue 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 issue Nov 28, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@michael-schwarz michael-schwarz

Labels
feature in progress performance Analysis time, memory usage precision
Projects
None yet
Milestone
v2.5.0
Development

Successfully merging a pull request may close this issue.

Context Gas per Function ⛽ goblint/analyzer
2 participants
@sim642 @michael-schwarz