# Unification-based Pointer Analysis without Oversharing

## TL;DR

This paper introduces TeaDsa, a scalable and precise pointer analysis for LLVM that overcomes oversharing issues in existing analyses, improving verification of heap-manipulating programs.

## Contribution

We develop TeaDsa, a novel unification-based pointer analysis that eliminates oversharing, and enhance it with contextual information for better precision and speed.

## Key findings

- TeaDsa is ten times faster than SVF and SeaDsa.
- TeaDsa is more precise than SeaDsa and sometimes more precise than SVF.
- TeaDsa effectively detects unsafe memory accesses in large programs.

## Abstract

Pointer analysis is indispensable for effectively verifying heap-manipulating programs. Even though it has been studied extensively, there are no publicly available pointer analyses that are moderately precise while scalable to large real-world programs. In this paper, we show that existing context-sensitive unification-based pointer analyses suffer from the problem of oversharing -- propagating too many abstract objects across the analysis of different procedures, which prevents them from scaling to large programs. We present a new pointer analysis for LLVM, called TeaDsa, without such an oversharing. We show how to further improve precision and speed of TeaDsa with extra contextual information, such as flow-sensitivity at call- and return-sites, and type information about memory accesses. We evaluate TeaDsa on the verification problem of detecting unsafe memory accesses and compare it against two state-of-the-art pointer analyses: SVF and SeaDsa. We show that TeaDsa is one order of magnitude faster than either SVF or SeaDsa, strictly more precise than SeaDsa, and, surprisingly, sometimes more precise than SVF.