Abstract

Many program analysis benefit from knowledge of aliasing or points-to information. Computing precise (FCPA, fully flow-sensitive and context-sensitive) and exhaustive (as against demand-driven) points-to information is known to be computationally expensive. Therefore many practical tools approximate the points-to information trading precision for efficiency. This often has an adverse impact on computationally intensive analyses such as model checking.

Previous approaches to FCPA (either top-down, or bottom-up using placeholders to explicate unknown locations or by using multiple call-specific summary flow functions) do not scale in practice. We adopt a traditional approach (constructing bottom-up procedure summaries) involving pointers but use a novel representation of procedure summaries: the generalized points-to graph (GPG); these leave unknown locations implicit.

By design, GPGs represent both memory (in terms of classical points-to facts) and memory transformers (in terms of generalized points-to facts). We perform FCPA by progressively reducing generalized points-to facts to classical points-to facts. GPGs distinguish between may and must pointer updates thereby facilitating strong updates within calling contexts. The number of nodes in the GPG for a procedure is linearly bounded by the number of variables and is independent of the number of statements in the procedure. Empirical measurements on SPEC benchmarks show that GPGs are indeed compact in spite of large procedure sizes and scale to programs of up to 158kLoC.