Many software systems are today variational. They can produce a potentially large variety of related programs (variants) by selecting suitable configuration options (features) at compile time. Specialized variability-aware (lifted, family-based) static analyses allow analyzing all variants of the family, simultaneously, in a single run without generating any of the variants explicitly. The elements of the lifted analysis domain represent tuples (i.e. disjunction of properties), which maintain one property from an existing single-program analysis domain per variant. Nevertheless, explicit property enumeration in tuples, one by one for all variants, immediately yields to combinatorial explosion given that the number of variants can grow exponentially with the number of features. Therefore, such lifted analyses may be too costly or even infeasible for families with a large number of variants.

In this work, we propose a more efficient lifted static analysis where sharing is explicitly possible between analysis elements corresponding to different variants. This is achieved by giving an symbolic representation of the lifted analysis domain, which can efficiently handle disjunctive properties in program families. The elements of the new lifted domain are binary decision diagrams where decision nodes are labeled with features, and the leaf nodes belong to an existing single-program analysis domain. We have developed such efficient lifted analysis which uses APRON and BDDAPRON libraries for implementing the new lifted analysis domain. The APRON library, used for the leaves, is a widely accepted API for numerical abstract domains (e.g. polyhedra, octagons, intervals), while the BDDAPRON is an extension of APRON which adds the power domain of Boolean formulae and any APRON domain. Through experiments applied to C program families, we show that our new BDD-based approach outperforms the old tuple-based approach for lifted analysis.