  A software analysis is a computer program that takes some representation of a
software product as input and produces some useful information about that
product as output. A software product line encompasses \emph{many} software
product variants, and thus existing analyses can be applied to each of the
product variations individually, but not to the entire product line as a whole.
Enumerating all product variants and analyzing them one by one is usually
intractable due to the combinatorial explosion of the number of product
variants with respect to product line features. Several software analyses
(e.g., type checkers, model checkers, data flow analyses) have been
redesigned/re-implemented to support variability. This usually requires a lot
of time and effort, and the variability-aware version of the analysis might
have new errors/bugs that do not exist in the original one.
  Given an analysis program written in a functional language based on PCF, in
this paper we present two approaches to transforming (lifting) it into a
semantically equivalent variability-aware analysis. A light-weight approach
(referred to as \emph{shallow lifting}) wraps the analysis program into a
variability-aware version, exploring all combinations of its input arguments.
Deep lifting, on the other hand, is a program rewriting mechanism where the
syntactic constructs of the input program are rewritten into their
variability-aware counterparts. Compositionally this results in an efficient
program semantically equivalent to the input program, modulo variability. We
present the correctness criteria for functional program lifting, together with
correctness proof sketches of our program transformations. We evaluate our
approach on a set of program analyses applied to the BusyBox C-language product
line.
