Hash Consed Points To Sets - SVF-tools/SVF GitHub Wiki

SVF supports using hash consed points-to sets.

• Instead of representing each pointers' points-to sets explicitly, pointers' refer to a identifier which points to an explicit points-to sets. This allows pointers to share duplicate points-to sets. For example, instead of pt(p) = { a, b, c }, pt(q) = { a, b, c }, we'd have pt(p) = id, pt(q) = id, id = { a, b, c }.
• Operations are also memoised, meaning that performing the same operation twice will become a hash table lookup the second time. Some operations are preemptively memoised based on the results of other operations.
• Some operations are quickly disposed of (called property operations), for example, x U x immediately returns x without performing any real computations as we can simply compare identifiers to realise this.

Usage

The ptd determines whether to use explicitly represented points-to sets (mutable) or hash consed points-to sets (persistent). For example, wpa -fspta -ptd=persistent.

Effect

Andersen's and flow-sensitive analyses see a speed up. Andersen's sees the same memory usage (occasionally better, occasionally slight worse). Flow-sensitive analyses see improvement in memory usage.

Aside from the occasional small regression in Andersen's memory usage, there appears to be no downside.

Finally, garbage collection is not currently implemented (hence the lack of Andersen's memory usage improvement).

For more options to improve flow-sensitive analysis performance specifically, see the page on object clustering and the page on versioned staged flow-sensitive analysis.