2451 Numeric Pentagon Inference#2480
Open
schuler-henry wants to merge 38 commits into
Open
Conversation
Implemented closed pentagon domain as state domain of a closed-pentagon value domain that combines the interval value domain with a set domain representing the upper bounds.
Replaced the visitor call with a callback that resolves the interval for a node id to make the function mapper visitor independent to be reused in the pentagon semantics.
- Updated the condition semantics for intervals to allow other domains to use the existing semantics. Therefore, removed the explicit visitor and state domain and replaced it with generic state domain and getter/setter functions.
- Implemented same condition semantics as for interval domain - Added + expression semantics to pentagon
- Added || and && to interval/upper-bounds condition semantics - Added / and ^ to interval expression semantics
- Creating ClosedPentagonDomain copies its values. - Setting pentagon in ClosedPentagonDomain automatically applies reduction after setting the new value.
…tagon-inference-visitor # Conflicts: # src/abstract-interpretation/interval/condition-semantics.ts # src/abstract-interpretation/interval/eval.ts # src/abstract-interpretation/interval/expression-semantics.ts # src/abstract-interpretation/interval/numeric-interval-inference.ts # test/functionality/abstract-interpretation/interval/interval.ts
schuler-henry
added
the
abstract interpretation
EagleoutIce
approved these changes
May 15, 2026
| equal: true, leq: true, join: ClosedPentagonBottom, meet: ClosedPentagonBottom, concrete: [], abstract: ClosedPentagonBottom, widen: ClosedPentagonBottom | ||
| }); | ||
|
|
||
| // Compare {V ∈ [0, 10], V <= {V, W}} and {V ∈ [0, 10], V <= {W}} |
Member
There was a problem hiding this comment.
are self bounds not ignored automatically?
Collaborator
Author
There was a problem hiding this comment.
yes, they are
There was a problem hiding this comment.
Pull request overview
Concludes iteration 2 of the pentagon-domain abstract interpretation work: the closed pentagon domain is restructured as a state domain over a value-product (interval + upper-bounds) rather than a product of two state domains, and a new NumericPentagonInferenceVisitor is added with shared interval/upper-bounds condition semantics and extended expression semantics (divide, power, and/or). The interval inference visitor is refactored onto the same shared condition-semantics framework, and the previous interval-flavored pentagon/upper-bounds modules are moved/renamed under a new pentagon/ directory.
Changes:
- Replace
ClosedPentagonDomain(product-of-state-domains) with a new state-of-value-products design undersrc/abstract-interpretation/pentagon/, including a relocatedUpperBoundsValueDomainand supportingUpperBoundsDomainstate wrapper. - Add
NumericPentagonInferenceVisitorwith pentagon expression semantics (+,-, plus fall-through to interval semantics for*,/,^,length) and shared interval/upper-bounds condition semantics via a genericcreateConditionApplierinabsint-condition-semantics.ts. - Extend interval expression semantics with
/and^, refactorcondition-semantics.tsonto the shared mechanism, add comprehensive pentagon tests, and update the wiki documentation.
Reviewed changes
Copilot reviewed 26 out of 27 changed files in this pull request and generated 6 comments.
Show a summary per file
| File | Description |
|---|---|
| wiki/Abstract Interpretation.md | Regenerated docs reflecting the new pentagon module layout. |
| src/abstract-interpretation/absint-condition-semantics.ts | New shared condition-semantics framework with default !, (, &&, || handlers. |
| src/abstract-interpretation/absint-visitor.ts | Minor import cleanup; applyConditionSemantics now takes a non-undefined state. |
| src/abstract-interpretation/domains/state-abstract-domain.ts | Loosens generic bounds on top/bottom and overloads top(). |
| src/abstract-interpretation/interval/closed-pentagon-domain.ts | Removed (replaced by new pentagon module). |
| src/abstract-interpretation/interval/upper-bounds-domain.ts | Removed (replaced by new pentagon module). |
| src/abstract-interpretation/interval/condition-semantics.ts | Rewritten to use the shared condition-semantics framework via IntervalValueDomainAccess. |
| src/abstract-interpretation/interval/expression-semantics.ts | Adds /, ^; switches helpers to use a getInterval callback. |
| src/abstract-interpretation/interval/numeric-interval-inference.ts | Implements IntervalValueDomainAccess and uses new condition-semantics wrapper. |
| src/abstract-interpretation/interval/eval.ts | Adds pentagon visitor to instrumentation output. |
| src/abstract-interpretation/pentagon/closed-pentagon-domain.ts | New state-domain implementation of the closed pentagon with reduction. |
| src/abstract-interpretation/pentagon/closed-pentagon-value-domain.ts | New per-node value product (interval × upper-bounds). |
| src/abstract-interpretation/pentagon/expression-semantics.ts | Pentagon-aware +/- semantics that update upper-bounds; falls back to interval semantics otherwise. |
| src/abstract-interpretation/pentagon/numeric-pentagon-inference.ts | New visitor combining interval and upper-bounds inference. |
| src/abstract-interpretation/pentagon/upper-bounds/upper-bounds-value-domain.ts | Set-based per-node upper-bounds domain. |
| src/abstract-interpretation/pentagon/upper-bounds/upper-bounds-condition-semantics.ts | Upper-bounds-specific condition semantics. |
| src/util/numbers.ts | Adds getMax helper. |
| test/functionality/abstract-interpretation/interval/* | Test helper rename (Exact→Equal, SlicingCriterionExpected→IntervalSlicingCriterionExpected) and exported test-case lists for reuse. |
| test/functionality/abstract-interpretation/interval/thesis-example.test.ts | Adjusts 9@result expectation to bottom (over-approximation). |
| test/functionality/abstract-interpretation/interval/{closed-pentagon-domain,upper-bounds-domain}.test.ts | Removed (replaced by pentagon module tests). |
| test/functionality/abstract-interpretation/pentagon/pentagon.ts | New shared test helper for pentagon-domain expectations. |
| test/functionality/abstract-interpretation/pentagon/closed-pentagon-domain.test.ts | Tests for the new closed pentagon state domain. |
| test/functionality/abstract-interpretation/pentagon/inference.test.ts | Pentagon inference tests reusing interval test cases. |
| test/functionality/abstract-interpretation/pentagon/interim-presentation-example.test.ts | End-to-end pentagon example test. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
OliverGerstl
approved these changes
May 18, 2026
By adding the rhs to the end of the expression, we probably fix the instrumentation issue that causes scripts with nested assign a <- b <- c to fail to execute.
5 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Implemented the closed pentagon domain as state domain of a value product with the same expression/condition semantics as the interval inference implementation.
Added support for divide, power, and, and or semantics to both domains.
This concludes the changes for iteration 2.