Variability abstractions for lifted analyses

Family-based (lifted) static analysis for “highly configurable programs” (program families) is capable of analyzing all variants at once without generating any of them explicitly. It takes as input only the common code base, which encodes all variants of a program family, and produces precise analysis results corresponding to all variants. However, the computational cost of the lifted analysis still depends inherently on the number of variants, which is in the worst case exponential in the number of statically configurable options (features). For a large number of features, the lifted analysis may be too costly or even infeasible. In this work, we introduce variability abstractions defined as Galois connections, which simplify variability away from program families based on -s. Then, we use abstract interpretation as a formal method for the calculational-based derivation of abstracted lifted analyses, which are sound by construction.

Our approach for abstracting lifted analysis is orthogonal to the particular program analysis chosen as a client. While a single program analysis operates on program states and depends on language-specific constructs, the lifted analysis assumes that a single program analysis already exists and lifts its results to all variants of the analyzed program family. Variability abstractions aim to reduce this variability-specific component of the lifted analysis, which handles variability and -s. Furthermore, given the “orthogonality” of variability abstractions to the rest of the analysis (its language-specific component), we can implement abstractions as a preprocessor. In particular, given an abstraction we define a syntactic transformation, which translates any program family into an abstracted version of it, such that the analysis of the abstracted program family coincides with the corresponding abstracted analysis of the original program family. We have implemented the proposed approach, and we evaluate its practicality on three Java benchmarks. The evaluation shows that abstractions yield significant performance gains, especially for families with higher variability.