Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented Jan 28, 2026

When CIL folds constant expressions, Goblint never sees the operations, and thus does not appear to perform all the necessary overflow checks. This used to be optional for our first SV-COMP no-overflow implementation in #149.

This reveals new things which probably should be evaluated speculatively.

TODO

@sim642 sim642 requested a review from karoliineh January 28, 2026 14:47
@sim642 sim642 added bug pr-dependency Depends or builds on another PR, which should be merged before explainability labels Jan 28, 2026
@sim642 sim642 force-pushed the checks-constFold-overflow branch from ca584ea to da7ab8c Compare January 28, 2026 19:01
@sim642
Copy link
Member Author

sim642 commented Feb 2, 2026

I was worried this might hurt performance, but sv-benchmarks level01 evaluation even suggests the opposite: OLS regression shows 5% speedup overall.
I don't know if this is due to disabling lowerConstants on the CIL side or not doing constFold in base, or both. I'll try to do an extra run to determine that.

The reason I was worried about performance is related to programs with many or large constant-foldable expressions. In theory, it might be cheaper to fold them directly, instead of using multiple of our int domains to reach the same constant result.
However, I now also see one way the performance could've improved: most expressions are not foldable, so constFold will just make an unnecessary copy on each evaluation (of each subexpression!).

@sim642
Copy link
Member Author

sim642 commented Feb 3, 2026

I don't know if this is due to disabling lowerConstants on the CIL side or not doing constFold in base, or both. I'll try to do an extra run to determine that.

Re-enabling lowerConstants again after this didn't have any impact, so I suppose the difference comes all from not constFold-ing repeatedly.

I think it'd make sense to have lowerConstants enabled to not re-evaluate enumerators on every use because that doesn't really happen at runtime. But it requires some cleanup in CIL to decouple lowerConstants from other unrelated uses (like conditional folding).

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

Labels

bug explainability pr-dependency Depends or builds on another PR, which should be merged before

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant