Make AE pointer comparisons conservative

[bjjwwang]

Summary

A points-to set records alternative targets for one runtime pointer, not targets held simultaneously. A known single target such as {a} identifies the pointer's exact target. A multi-target set such as {a, b} means that either target may be selected at runtime. Consequently, two equal multi-target sets do not by themselves prove that the two concrete pointers are equal.

This PR makes AE pointer comparison conservative and predicate-aware:

• normalize pointer operands into known address sets, {NULL}, or {BlackHole};
• produce definite eq/ne results only when known targets prove the outcome;
• keep overlapping multi-target sets, unresolved targets, and pointer ordering conservative;
• use the resulting Boolean interval directly for branch feasibility; and
• remove the duplicate pointer-comparison implementation that was unreachable behind the original address fast path.

Problem

AbstractInterpretation::updateStateOnCmp previously handled every comparison between two address values as if it were equality. As a result, icmp ne on the same known target evaluated to true, while icmp ne on disjoint targets evaluated to false. The predicate-aware address switch later in the function never ran because the earlier address branch had already consumed those operands.

The old logic also treated equality of two abstract address sets as concrete pointer equality. This is valid for {a} compared with {a}, but not for {a, b} compared with {a, b}: the two runtime pointers may independently select different targets. Similarly, BlackHole is a statically unresolved target and must not be compared as if it were one concrete address.

Finally, pointer-ordering cases compared abstract object IDs, whose numeric order does not represent runtime address order. isCmpBranchEdgeFeasible also bypassed pointer and null comparisons, preventing a sound comparison result from controlling branch reachability.

Formal semantics

Let N(i, v) normalize operand v, whose SVF variable ID is i, into an abstract address set:

$$ N(i,v) = \begin{cases} {\mathit{NULL}} & \text{if } i=\mathit{NullPtr} \text{ or } v=[0,0], \\ A_v & \text{if } v \text{ carries a known address set } A_v, \\ {\mathit{BlackHole}} & \text{otherwise.} \end{cases} $$

BlackHole is SVF's existing sentinel for a statically unresolved pointer target. For pointer comparison only, a set containing BlackHole is conservatively interpreted as the top of the address domain:

$$ \gamma_{\mathrm{cmp}}(A) = \begin{cases} \mathit{Addr} & \text{if } \mathit{BlackHole} \in A, \\ A & \text{otherwise.} \end{cases} $$

This scoped definition does not claim that every existing AddressValue operation implements BlackHole as an absorbing lattice-top element.

For equality, the possible concrete outcomes are:

$$ O_{eq}(A,B) = {,[a=b] \mid a \in \gamma_{\mathrm{cmp}}(A),, b \in \gamma_{\mathrm{cmp}}(B),}. $$

The Boolean outcomes are abstracted to an interval:

$$ \alpha_B(O)=[\min O,\max O], $$

where [1,1] is definitely true, [0,0] is definitely false, and [0,1] retains both outcomes.

Equivalently, the implementation uses:

hasUnknown(A, B) =
    BlackHole in A or BlackHole in B

mustEqual(A, B) =
    not hasUnknown(A, B)
    and |A| = 1
    and A = B

mayEqual(A, B) =
    hasUnknown(A, B)
    or (A intersect B is not empty)

abstract(A == B) = [mustEqual(A, B), mayEqual(A, B)]
abstract(A != B) = [not mayEqual(A, B), not mustEqual(A, B)]

This yields:

Left targets	Right targets	==	!=
{a}	{a}	[1,1]	[0,0]
{a}	{b}, where a != b	[0,0]	[1,1]
{a, b}	{c}, where the sets are disjoint	[0,0]	[1,1]
{a, b}	{a}	[0,1]	[0,1]
{a, b}	{a, b}	[0,1]	[0,1]
a set containing BlackHole	any set	[0,1]	[0,1]

NULL is a known distinguished target, so two null operands follow the same-known-target case.

Pointer-ordering predicates conservatively produce [0,1]. SVF object IDs identify abstract objects; their numeric order cannot justify pruning a concrete program path.

For a branch edge labelled by $b \in {0,1}$ and comparison result $R$:

$$ \mathit{feasible}(edge_b) \iff R \sqcap [b,b] \neq \bot. $$

Thus, an edge is removed only when every concrete pointer pair represented by the operands produces the opposite outcome. Branch feasibility does not need separate pointer or null cases.

Implementation

• normalizePointerAddresses gives null, known addresses, and unresolved operands one address-set representation.
• comparePointerValues implements the cases above as an explicit decision tree.
• updateStateOnCmp dispatches pointer operands to that helper and keeps the existing interval comparison for non-pointer operands.
• isCmpBranchEdgeFeasible consumes the stored comparison interval and remains conservative when no interval result is available.

Validation

• The ae target builds successfully with LLVM 21.1.8 and Z3 4.16.0.
• Focused pointer/null AE regressions: 28/28 passed across dense, semi-sparse, full-sparse, and no-main modes.
• Targeted tests verify definite results for the same and disjoint known targets.
• An overlapping-target test confirms that both feasible branches are retained.

[codecov]

Codecov Report

❌ Patch coverage is 83.92857% with 9 lines in your changes missing coverage. Please review.
✅ Project coverage is 68.01%. Comparing base (15224fc) to head (998aaec).
⚠️ Report is 1 commits behind head on master.

Files with missing lines	Patch %	Lines
svf/lib/AE/Svfexe/AbstractInterpretation.cpp	80.00%	9 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #1887      +/-   ##
==========================================
+ Coverage   67.89%   68.01%   +0.11%     
==========================================
  Files         261      261              
  Lines       26682    26653      -29     
  Branches     5109     5122      +13     
==========================================
+ Hits        18117    18127      +10     
+ Misses       8565     8526      -39     

Files with missing lines	Coverage Δ
svf/include/AE/Svfexe/AbstractInterpretation.h	100.00% <ø> (ø)
svf/lib/AE/Svfexe/AEDetector.cpp	85.60% <100.00%> (+0.11%)	⬆️
svf/lib/AE/Svfexe/AbsExtAPI.cpp	89.60% <100.00%> (+0.07%)	⬆️
svf/lib/AE/Svfexe/AbstractStateManager.cpp	76.47% <100.00%> (+0.96%)	⬆️
svf/lib/AE/Svfexe/AbstractInterpretation.cpp	88.29% <80.00%> (+5.97%)	⬆️

... and 1 file with indirect coverage changes

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.