Skip to content

Cache field offset calculations using CIL#1974

Merged
sim642 merged 6 commits intomasterfrom
issue-1964
Apr 5, 2026
Merged

Cache field offset calculations using CIL#1974
sim642 merged 6 commits intomasterfrom
issue-1964

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Mar 31, 2026

Closes #1964.

TODO

  • Actually add caching.
  • Benchmark.

@sim642 sim642 added this to the v2.8.0 Clumsy Clurichaun milestone Mar 31, 2026
@sim642 sim642 self-assigned this Mar 31, 2026
@sim642 sim642 added cleanup Refactoring, clean-up feature performance Analysis time, memory usage analyze-that labels Mar 31, 2026
@sim642 sim642 marked this pull request as ready for review April 1, 2026 07:19
Copilot AI review requested due to automatic review settings April 1, 2026 07:19
Copy link
Copy Markdown
Contributor

Copilot AI left a comment

Choose a reason for hiding this comment

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

Pull request overview

This PR introduces memoization for CIL field offset computations to avoid repeated expensive Cil.bitsOffset calls, addressing #1964.

Changes:

  • Updated GobHashtbl.find_or_add_default_delayed to pass the key to the default thunk.
  • Added cached Cilfacade.fieldBitsOffsetOnly / fieldBytesOffsetOnly helpers and ensured the cache is cleared in Cilfacade.reset_lazy.
  • Switched multiple call sites to use the cached field offset helpers instead of recomputing offsets.

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 1 comment.

Show a summary per file
File Description
src/util/std/gobHashtbl.ml Changes find_or_add_default_delayed to provide the lookup key to the default function.
src/framework/xsltResultOutput.ml Adapts find_or_add_default_delayed call sites to the new default signature.
src/common/util/cilfacade.ml Adds field offset caching and resets it via reset_lazy.
src/cdomains/unionFind.ml Uses cached field bit offsets when mapping bit offsets back to struct fields.
src/cdomain/value/cdomains/offset.ml Uses cached field bit offsets in offset-to-index computation (incl. bitfield handling).
src/analyses/memOutOfBounds.ml Uses cached field byte offsets for field offset conversion.
src/analyses/base.ml Uses cached field byte offsets for container_of-style offset cancellation logic.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Comment thread src/common/util/cilfacade.ml
@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Apr 5, 2026

This speeds up rsync analysis by ~20% (on top of the CIL hasAttribute fix): goblint/bench@6e4ada7.
So I'll merge this and we'll see from knightly if any of it carries over to sv-benchmarks.

@sim642 sim642 merged commit 82ff50a into master Apr 5, 2026
14 of 16 checks passed
@sim642 sim642 deleted the issue-1964 branch April 5, 2026 09:10
@sim642
Copy link
Copy Markdown
Member Author

sim642 commented Apr 6, 2026

we'll see from knightly if any of it carries over to sv-benchmarks.

There's no impact on sv-benchmarks: #tum-nightly-svcomp > commit 82ff50a.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

analyze-that cleanup Refactoring, clean-up feature performance Analysis time, memory usage

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Cache field offset calculations using CIL

2 participants