Partial soundness proofs for pragmatic static analyses

Question

I was reflecting on a comment by Rob Simmons on unsound static analyses:

An analysis that is neither sound nor complete is called pragmatic by Jaspan, as there aren't any theorems to be proved about such an analysis: they can be justified only by their utility in practice.

This is a pretty unsatisfying way to evaluate a static analysis; surely, we can make stronger claims than statistical correlations. Could we, perhaps, show that analyses are sound given some additional assumptions on the program?

Consider the classic example of determining if a variable in a C program is constant. A sound analysis requires a points-to analysis; an unsound analysis requires only a syntactic scan. It seems that it would be straightforward to prove the soundness of this analysis if we also assume that, at every assignment through a pointer, that pointer does not refer to the variable of interest. Such a proof should easily turn into an analysis that also outputs a finite list of assumptions made about specific program points to guarantee its soundness. Indeed, I already see comments on unsound analyses such as "This system is unsound because it assumes the inputs are unaliased," which suggests the theorem that the system is sound if the inputs are unaliased.

A search for "partial soundness" turns up a type theory paper, but no analysis papers. Systems such as CCured that generate dynamic checks upon the failure of the analysis seem related, but I've not seen them interpreted this way. Is there prior work along these lines?

Answer 1

Program analysis is an inherently applied field, so for many practitioners, the final word on the utility of an analysis is how it performs in practice.

The approach you are suggesting would make explicit situations in which the analysis is sound. However, isolating these situations requires the analyst to know about the semantics of the programming language, the semantics of the static analyzer and further identify the gaps between the two. In my experience, several people interested in designing a practical analysis find the overhead of studying semantics (and soundness) excessive, and people who focus on semantics and soundness tend not to investigate heuristics required to make the analysis work on large families of practical examples. This may explain the dearth of material.

That said, there are people who care about both practical utility and soundness, and even the specific problem you speak of (soundness with respect to points-to-analysis results). I think you will have more luck searching with the terms conditional soundness or relative soundness or parameterized soundness.

1. SAFECode: Enforcing Alias Analysis for Weakly Typed Languages, Dinakar Dhurjati, Sumant Kowshik, and Vikram Adve, PLDI 2006

2. Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors, Christopher L. Conway, Dennis Dams, Kedar S. Namjoshi, Clark Barrett, SAS 2008

3. A posteriori soundness for non-deterministic abstract interpretations, Matthew Might and Panagiotis Manolios, VMCAI 2009.

The first two papers are directly related to your question, and the third is just a slightly different approach to soundness, which may interest you in this context.

The soundness/utility trade-off is an active concern for the problem of call graph construction. In the presence of reflection and dynamic class loading, call graph construction is a non-trivial problem and it is difficult to achieve sound and useful results.

Papers citing Call graph construction in object-oriented languages as determined by Google Scholar.

A lot of those papers are not relevant for this discussion, but there are quite a few which contain relevant discussions, so I prefer to let you choose.