test: disable demo.c semi-sparse widen-narrow (known limitation)#181
Open
bjjwwang wants to merge 1 commit intoSVF-tools:masterfrom
Open
test: disable demo.c semi-sparse widen-narrow (known limitation)#181bjjwwang wants to merge 1 commit intoSVF-tools:masterfrom
bjjwwang wants to merge 1 commit intoSVF-tools:masterfrom
Conversation
demo.c's recursive ArgValVar needs per-callsite storage which the semi-sparse model cannot represent (one def-site entry per ValVar, widening cannot be narrowed back). Dense mode handles this correctly. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Collaborator
|
Could we add more tests for loop and recursion handling |
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.
Why demo.c semi-sparse widen-narrow fails
Test code:
Dense derives result ∈ [10000, 10000]; sparse derives [10000, +∞] → assert not verified.
Root cause
In semi-sparse mode, an ArgValVar has exactly one def-site storage slot, but a recursive function needs multiple.
The parameter a of demo (ArgValVar Var23) has its def-site at demo's FunEntry (ICFGNode 1). Two CallPEs write to it:
main → demo(0) writes Var23 = 0
demo → demo(a+1) writes Var23 = a+1 (recursive)
Dense mode: every ICFGNode's trace holds its own ValVar copies. mergeStatesFromPredecessors(cycle_head) uses joinWith, which joins each predecessor's Var23. Widening sees the accumulated [0,1,2,...,+∞] growth; during narrowing, the a >= 10000 cmp branch refinement pulls the upper bound back to 10000.
Sparse mode:
joinWith skips ValVars (AbstractState.cpp:109)
ValVars live only at their def-site (here, FunEntry)
Each recursive iteration's CallPE writes Var23 = a+1 as a strong update, overwriting the previous iteration's value
prev_snapshot is the only place accumulation can live, but its Var23 eventually widens to [0, +∞]
During narrowing, the a >= 10000 cmp branch refinement can only tighten Var23 in a use-site's temporary state; it cannot write back to the def-site (sparse explicitly excludes ValVars from cycle_head joining)
Fundamental conflict:
Sparse's design assumption: "each ValVar has exactly one storage slot (at its def-site)"
Recursion's requirement: "the same ArgValVar simultaneously carries different values for different call contexts" (context-sensitive)
The two are incompatible: one slot cannot hold multiple live values, so they collapse into a single coarse interval. Once that interval widens to +∞, narrowing has no information source left to tighten it