Effective Analysis of C Programs by Rewriting Variability
Alexandru F. Iosif-Lazara , Jean Meloa , Aleksandar S. Dimovskia , Claus
Brabranda , and Andrzej Wąsowskia
a IT University of Copenhagen, Denmark
Abstract Context. Variability-intensive programs (program families) appear in many application areas and
for many reasons today. Different family members, called variants, are derived by switching statically configurable options (features) on and off, while reuse of the common code is maximized.
Inquiry. Verification of program families is challenging since the number of variants is exponential in the
number of features. Existing single-program analysis and verification tools cannot be applied directly to program families, and designing and implementing the corresponding variability-aware versions is tedious and
laborious.
Approach. In this work, we propose a range of variability-related transformations for translating program families into single programs by replacing compile-time variability with run-time variability (non-determinism).
The obtained transformed programs can be subsequently analyzed using the conventional off-the-shelf singleprogram analysis tools such as type checkers, symbolic executors, model checkers, and static analyzers.
Knowledge. Our variability-related transformations are outcome-preserving, which means that the relation
between the outcomes in the transformed single program and the union of outcomes of all variants derived
from the original program family is equality.
Grounding. We present our transformation rules and their correctness with respect to a minimal core imperative language IMP. Then, we discuss our experience of implementing and using the transformations for
efficient and effective analysis and verification of real-world C program families.
Importance. We report some interesting variability-related bugs that we discovered using various state-of-theart single-program C verification tools, such as Frama-C, Clang, LLBMC.
ACM CCS 2012

Software and its engineering → Software creation and management Software verification and validation;
Software notations and tools Formal language definitions;
Keywords Program Families, Variability-related Transformations, Verification, Static Analysis

The Art, Science, and Engineering of Programming
Submitted

September 1, 2016

Published

January 27, 2017

doi

10.22152/programming-journal.org/2017/1/1
© Alexandru F. Iosif-Lazar, Jean Melo, Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wąsowski
This work is licensed under a “CC BY 4.0” license.
In The Art, Science, and Engineering of Programming, vol. 1, no. 1, 2017, article 1; 25 pages.

Effective Analysis of C Programs by Rewriting Variability

1

Introduction

Many software systems today are variability intensive. They permit users to derive
a custom variant by choosing suitable configuration options (features) depending
on their requirements. There are different strategies for implementing variational
systems (program families) [11]. Still, many popular industrial program families
from system software (e.g. Linux kernel) and embedded software (e.g. cars, phones,
avionics) domains are implemented using annotative approaches such as conditional
compilation. For example, #ifdef annotations from the C-preprocessor are used to
specify under which conditions, parts of the code should be included or excluded
from a variant.
Due to the increasing popularity of program families, formal verification techniques
for proving their correctness are widely studied (see [35] for a survey). Analyzing
program families is challenging [29]. From only a few compile-time configuration
options, exponentially many variants can be derived. Thus, for large variabilityintensive software systems, any brute-force approach that derives and analyzes all
variants individually one by one using existing single-program analysis tools is very inefficient or even infeasible. Recently, many dedicated family-based (variability-aware)
analysis tools have been developed, which operate directly on program families. They
produce results for all variants at once in a single run by exploiting the similarities
between the variants. Examples of successful family-based analysis tools are applied to
syntax checking [25, 20], type checking [24, 8], static analysis [7, 6], model checking
[10, 14], etc. Although they are more efficient than the brute-force approach, still their
design and implementation for each particular analysis and language is tedious and
error prone. Often, these family-based tools are research prototypes implemented
from scratch. So it is very difficult to re-implement all optimization algorithms in them
that already exist for their single-program industrial-strength counterparts, which
have been under development for several decades.
Another approach for efficient variability-aware verification would be to replace
compile-time variability with run-time variability (or non-determinism) [37]. In
particular, in this work we consider a class of variability-related transformations that
transform a program family into a single program, whose outcomes are equal to the
union of all outcomes of individual variants. We call the corresponding transformations
outcome-preserving. Subsequently, existing single-program analysis tools (verification
oracles) that can handle non-determinism (run-time variability) can be used to analyze
the generated single program. Finally, the obtained results are interpreted back on
the individual variants. The overview of this approach is given in Figure 1. Instead of
using specialized variability-aware tools to analyze program families (which would
be tedious and labor intensive), our transformation-based approach allows us to use
the standard off-the-shelf single-program analysis tools to achieve the same goal.
Nevertheless, the limitation of our approach is that we may not obtain the most
precise conclusive results for all individual variants. Of course, this depends on the
particular analysis and tool that we use.
To demonstrate correctness of our transformation-based approach, we define the
transformations formally using IMP, a small imperative language. To model compile-

1-2

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski



analyzer

/ Single program
single-program



transform

analyzer

variability-aware

Variability-aware
program

results Single-program
Variability-aware interpret
o
results
results

Figure 1

The overview of our transformation-based approach for verification of program
families. The single-program analyzer can be any verification oracle for single
programs, such as: symbolic executor, type checker, static analyzer, model checker.

time variability, we extend IMP with an “#ifdef” construct for encoding multiple
variants, which we call IMP language. To encode run-time variability, we extend IMP
with an “or” construct for encoding non-determinism, which we call IMPor language.
We define transformations that translate any given IMP program into a corresponding
IMPor program. Furthermore, for each transformation we show the relation between
the semantics of the input and output programs.
Finally, we report on our experience with implementing and applying our transformations for a full-fledged language, C. The tool, called C Reconfigurator, uses
variability-aware parser SuperC [20] for parsing C code with preprocessor annotations, then applies our variability rewrites thus producing a single C program as
output. We evaluate our approach on real-world variability intensive C programs with
real bugs. We show how some known off-the-shelf single-program analysis tools can
be used for efficient and effective verification of such programs.
In summary, this work makes the following contributions:
A stand-alone variability-related transformation, which transforms a program family into a single program by replacing compile-time variability with non-determinism.
Correctness of the proposed transformation, which shows that the set of outcomes
of the transformed program is equal to the union of sets of outcomes of variants
from the input family.
A prototype tool, C Reconfigurator, which implements the above variabilityrelated transformation for the C language.
An evaluation of the effectiveness of our transformation-based approach for finding
real variability bugs in large variability intensive C software systems.

2

Motivating Example

We begin by showing how our variability transformations work on C program families.
Consider a preprocessor-based family of C programs shown in Figure 2 (left column),
which uses two (Boolean) features A and B . Our two features give rise to a family of
four variants defined by the set of configurations K = {A ∧ B, A ∧ ¬B, ¬A ∧ B, ¬A ∧ ¬B}.

1-3

Effective Analysis of C Programs by Rewriting Variability

int foo() {
int x:= 1;
#if (A) x:= x+1 #endif;
#if (B) x:= x-1 #endif;
return 2/x;

}
Figure 2

int A := r and() % 2;
int B := r and() % 2;
int foo() {
int x := 1;
if (A) x:= x+1;
if (B) x:= x-1;
return 2/x; }

Before (left column) and after (right column) our transformations

For each configuration a different variant (single program) can be generated by
appropriately resolving #if statements. For example, the variant for A ∧ B will have
both features A and B enabled (set to true), thus yielding the following body of f oo():
int x := 1; x := x+1; x := x-1; return 2/x . The variant for ¬A ∧ ¬B is: int x := 1; return 2/x .
In such program families, errors (also known as variability bugs [1]) can occur in some
variants (configurations) but not in others. In our example program family in Figure 2,
the variant ¬A ∧ B will crash at the return statement when we attempt to divide by
zero. On the other hand, the other variants do not contain the division-by-zero error
since the value of x at the return statement is: 1 for variants A ∧ B and ¬A ∧ ¬B , and 2
for A ∧ ¬B .
In Figure 2, we show a single program (right column) obtained by applying our
variability-related transformation on the family shown in the left column. All features
are first declared as ordinary global variables and non-deterministically initialized to 0
or 1, then all #if statements are transformed into ordinary if-s with the same conditions.
Thus, the division-by-zero error is present in this single program and corresponds to
a trace when A is initialized to 0 and B to 1. The set of outcomes of the transformed
program (Figure 2, right column) is equal to the union of outcomes of all individual
variants from the family (Figure 2, left column). Therefore, the division-by-zero error
is present in the transformed program.
In general, the transformed program that we obtain from the original program
family can be analyzed by various single-program verification tools, in order to find
variability errors or to confirm the absence of errors in the given program family.

3

A Formal Model for Transformations

We now introduce the IMP language that we use to demonstrate our transformations
and their proofs of correctness. We describe two extensions of IMP: IMPor used to
represent run-time variability (non-determinism), and IMP used to represent compiletime variability.

1-4

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski
3.1 IMP

We use a simple imperative language, called IMP [32, 34], which represents a regular
general-purpose programming language, aimed at the development of single programs.
IMP is a well established minimal language, which is used only for presentational
purposes here.
IMP is an imperative language with two syntactic categories: expressions and
statements. Expressions include integer constants, variables, and binary operations.
Statements include a “do-nothing” statement skip , assignments, statement sequences,
conditional statements, while loops, and local variable declarations. Its abstract syntax
is summarized using the following grammar:
Syntax.

e ::= n | x | e0 ⊕ e1
s ::= skip | x := e |s0 ; s1 | if e then s0 else s1 | while e do s | var x:=e in s

In the above, n stands for an integer constant, x stands for a variable name, and ⊕
stands for any binary arithmetic operator. We denote by Stm and Exp the set of all
statements, s, and expressions, e, generated by the above grammar.
A state of a program is a store mapping variables to values (integer
numbers), Val = Z. We write Store = Var → Val to denote the set of all possible stores.
Expressions are computed in a given store, denoted by σ. A function E : Exp × Store →
Val defined below by induction on e, maps an expression and a store to a single value,
thereby formalizing evaluation of expressions.
Semantics.

E (n, σ) = n,

E (x , σ) = σ(x ),

E (e0 ⊕ e1 , σ) = E (e0 , σ) ⊕ E (e1 , σ)

Figure 3 presents the inference rules for a small-step operational semantics for IMP
[32, 34]. The notation σ[x 7→ n] denotes the state that maps x into n and all other
variables y into σ(y ). Following the convention popularized by C, we model Boolean
values as integers, with zero interpreted as false and everything else as true (see rules
If2 and Wh2, respectively, If1 and Wh1). Note that for variable declarations (see rules
Var1 or Var2) we need to restore the declared variable, x, to its earlier global value
assigned to x before the declaration, when the scope of declaration has completed.
That is why the statement s0 in intermediate configurations (rule Var1) is prefixed
with variable declarations whose initializations store the local values of x. We can
use the inference rules in Figure 3 to define the transition relation: 〈s, σ〉 → γ, where
γ is either of the form 〈s0 , σ0 〉 or of the form σ0 . If γ is of the form 〈s0 , σ0 〉 then the
execution of s is not completed and the complex statement s is rewritten into simpler
one s0 , possibly updating the store σ into σ0 (for instance, Seq1 or Seq2). If γ is of the
form σ0 then the execution of s from σ has terminated and the final state is σ0 (for
instance, Skip or Wh2).
A derivation sequence of s starting in store σ can be either a finite sequence 〈s, σ〉 →
〈s1 , σ1 〉 → . . . → σ0 (means: s is run in σ and terminates successfully transforming σ
to σ0 in the process), or an infinite sequence 〈s, σ〉 → 〈s1 , σ1 〉 → . . . (means: s diverges

1-5

Effective Analysis of C Programs by Rewriting Variability

Skip

Wh2

〈s0 , σ〉 → 〈s00 , σ0 〉

Sq1

〈skip , σ〉 → σ
〈x := e, σ〉 → σ[x 7→ n]
〈s0 ; s1 , σ〉→〈s00 ; s1 , σ0 〉
0
〈s0 , σ〉 → σ
E (e, σ) 6= 0
Sq2

If2

n = E (e, σ)

Asgn

〈s0 ; s1 , σ〉→〈s1 , σ0 〉
E (e, σ) = 0

〈if e then s0 else s1 , σ〉 → 〈s1 , σ〉
E (e, σ) = 0
〈while e do s, σ〉 → σ
Var2

Var1

If1

〈if e then s0 else s1 , σ〉 → 〈s0 , σ〉
E (e, σ) 6= 0

Wh1

〈while e do s, σ〉 → 〈s ; while e do s, σ〉
n = E (e, σ) 〈s, σ[x 7→ n]〉 → 〈s0 , σ0 〉

〈var x:=e in s, σ〉→〈var x:=σ0 (x) in s0 , σ0 [x 7→ σ(x)]〉
n = E (e, σ) 〈s, σ[x 7→ n]〉 → σ0
〈var x:=e in s, σ〉 → σ0 [x 7→ σ(x)]

Figure 3 Small-step operational semantics for IMP

when run in σ). We write [[s]]σ for the final store σ0 that can be derived from 〈s, σ〉
(if the derivation is finite), i.e. 〈s, σ〉 →∗ σ0 , otherwise if the derivation is infinite
[[s]]σ is undefined (empty). In general, we define:
S
[[s]] = σ∈StoreInit [[s]]σ
where StoreInit denotes the set of initial input stores on which s is executed.
3.2 IMPor

The language IMPor is obtained by extending IMP with a non-deterministic
choice operator ‘or’ which can non-deterministically choose to evaluate either of its
arguments.
Syntax

e

::=

... | e0 or e1

Since we have non-deterministic construct ‘or’, it is possible for an expression to evaluate to a set of different values in a given store. Therefore, now we
have E : Exp × Store → P (Val) defined as follows:
Semantics.

E (n, σ) = {n},
E (x , σ) = {σ(x )},
E (e0 or e1 , σ) = E (e0 , σ) ∪ E (e1 , σ)
E (e0 ⊕ e1 , σ) = {v0 ⊕ v1 | v0 ∈ E (e0 , σ), v1 ∈ E (e1 , σ)}

The small-step operational semantics rules for IMPor are those of IMP given in Figure 3,
but now they take into account the non-determinism of E (e, σ). For example, we have:
Wh1

n ∈ E (e, σ)

n 6= 0

〈while e do s, σ〉 → 〈s ; while e do s, σ〉

Wh2

0 ∈ E (e, σ)
〈while e do s, σ〉 → σ

For IMPor, we write [[s]]σ for the set of final stores σ0 that can be derived from 〈s, σ〉,
i.e. 〈s, σ〉 →∗ σ0 . Note that since IMPor is a non-deterministic
language [[s]]σ may
S
contain more than one final store. Finally, [[s]] = σ∈StoreInit [[s]]σ.
3.3 IMP

A finite set of Boolean variables F = {A1 , . . . , An } describes the set of available features
in the program family. Each feature may be enabled or disabled in a particular variant.

1-6

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski

A configuration k is a truth assignment or a valuation which gives a truth value to
each feature, i.e. k is a mapping from F to {true, false}. If a feature A ∈ F is enabled
for the configuration k then k(A) = true, otherwise k(A) = false. Any configuration
k can also be encoded as a conjunction of literals: k(A1 ) · A1 ∧ · · · ∧ k(An ) · An , where
true · A = A and false · A = ¬A. We write K for the set of all valid configurations
defined over F for a family. The set of valid configurations is typically described
by a feature model [23], but in this work we disregard syntactic representations of
the set K. Note that |K| ≤ 2|F| , since, in general, not every combination of features
yields a valid configuration. We define feature expressions, denoted FeatExp, as the
set of well-formed propositional logic formulas over F generated using the grammar:
φ ::= true | A ∈ F | ¬φ | φ1 ∧ φ2 | φ1 ∨ φ2 .
The programming language IMP is our two-stage extension of IMP (thus,
IMP does not contain the ‘or’ construct). Its abstract syntax includes the same expression and statement productions as IMP, but we add the new compile-time conditional statements for encoding multiple variants of a program. The new statements “#if (φ) s #endif” and “#if (φ) var x:=n in #endif s” contain a feature expression
φ ∈ FeatExp as a presence condition, such that only if φ is satisfied by a configuration
k ∈ K then the code between #if and #endif will be included in the variant for k.
Syntax.

s ::= ... | #if (φ) s #endif | #if (φ) var x:=n in #endif s

Note that only statements and local variable declarations can be compile-time conditionally defined in IMP. However, in general “#if” constructs defined on arbitrary
language elements could be translated into constructs that respect the appropriate
syntactic structure of the language by code duplication [19]. Also note that the C
preprocessor uses the following keywords: #if, #ifdef, and #ifndef to start a conditional
construct; #elif and #else to create additional branches; and #endif to end a construct.
Any of such preprocessor conditional constructs can be desugared and represented
only by #if construct we use in this work, e.g. #ifdef (φ) s0 #else s1 #endif is translated
into #if (φ) s0 #endif ; #if (¬φ) s1 #endif.
The semantics of IMP has two stages: first, given a configuration k ∈ K
compute an IMP single program without #if-s; second, evaluate the obtained variant
using the standard IMP semantics. The first stage is a simple preprocessor specified
by the projection function πk mapping an IMP program family into an IMP single
program corresponding to the configuration k ∈ K. The projection πk copies all basic
statements of IMP that are also in IMP, and recursively pre-processes all sub-statements
of compound statements. For example, πk (skip) = skip and πk (s0 ;s1 ) = πk (s0 );πk (s1 ).
The interesting case is “#if (φ) s #endif” (resp., #if (φ) var x:=n in #endif s) statement,
Semantics.

1-7

Effective Analysis of C Programs by Rewriting Variability

where the statement s (resp., the local variable declaration var x:=n in ) is included in
the resulting variant iff k |= φ ,1 otherwise it is removed. We have:
¨
πk (s) if k |= φ
πk (#if (φ) s #endif) =
skip
if k 6|= φ
¨
πk (var x:=n in s) if k |= φ
πk (#if (φ) var x:=n in #endif s) =
πk (s)
if k 6|= φ
Note that since any configuration k ∈ K has only one satisfying truth assignment
(values of all features are fixed in k), either k |= φ or k 6|= φ for any φ ∈ FeatExp.

4

Variability-related Transformations

Our aim is to transform an input IMP program family s with sets of features F and
configurations K into an output IMPor program s0 .
In a pre-transformation phase, we first convert each feature A ∈ F into the variable
A, which is non-deterministically initialized to 0 or 1 (meaning to false or true). Let
F = {A1 , . . . , An } be the set of available features in the family s, then we have the
following initialization fragment in the resulting pre-transformed program pre-t(s):
pre-t(s)= var A1 :=0 or 1 in . . . var An :=0 or 1 in s

Note that in the initialization we consider all possible combination of values for
features (in total 2|F| ). We will take into account the specific set of configurations K
(|K| ≤ 2|F| ) later on, in the transformation phase.
In the following, rewrite rules have the form:
ψ ` s

s0

meaning that: if the current program family being transformed matches any abstract
syntax tree (AST) node of the shape s nested under #if-s with the resulting presence
condition that implies ψ ∈ FeatExp (i.e. in context ψ) then replace s by s0 . Formally, if
we apply the rule ψ ` s s0 to a family:
. . . #if (φ1 ) . . . #if (φn ) . . . ; s; . . . #endif . . . #endif. . .

where φ1 ∧. . .∧φn =⇒ ψ, then we obtain the transformed program:
. . . #if (φ1 ) . . . #if (φn ) . . . ; s0 ; . . . #endif . . . #endif. . .

We write Rewr i t e(s, ψ ` s s0 ) for the final transformed program s0 obtained by
repeatedly applying the rule ψ ` s s0 on s and its transformed versions until we
reach a point where this rule can not be applied (a fixed point of the rule). Note

1

Here |= denotes the standard satisfaction relation of propositional logic.

1-8

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski

that rules of the form: true ` s s0 , are the most general and can be applied to any
statement s no matter whether s is a top-level statement not nested within some #if
or s is nested somewhere deep within #if-s. This is due to the fact that any “s” can be
written as: “#if (true) s #endif” in the earlier case when s is a top-level statement, and
φ =⇒ true for any φ ∈ Feat E x p in the latter case when s is nested within #if-s with
presence condition φ .
We start with three rules for eliminating configurable variable declarations. They
involve duplicating code and variable renaming. The most straightforward way to
handle renaming of variables in different contexts is by adding an environment δ
as a parameter to the statements being transformed. We define an environment
δ : Var × FeatExp → Var as a function mapping a given pair of a variable and a feature
expression to a variable name. We write δfe (x) ⊆ FeatExp for the set of all feature
expressions φ such that δ(x, φ) is defined, i.e. δfe (x) = {φ ∈ FeatExp | (x, φ) ∈ d om(δ)}.
We write (s, δ) to denote the result of simultaneously substituting δ(x, φ) for each
occurrence of any variable x in s in the context (presence condition) that implies φ .
This rule transforms a local variable conditionally
declared within a given context ψ ∈ FeatExp:
Conditional variable declaration.

ψ ` (#if (φ) var x:=n in #endif s, δ)

(1)

var xnew :=n in (s, δ[(x, φ) 7→ xnew ])

where xnew is a fresh variable name that does not occur as a free variable in s and
r ang e(δ).
The second rule handles the case when a local variable is
used within a context ψ ∈ Feat E x p. There are three cases to consider here.
Conditional variable use.

ψ ` (y:=e[x], δ)

(2.1)

(y:=e[δ(x, φ)], δ)

if there exists an unique φ ∈ δfe (x), such that ψ |= φ . Here e[x] means that the
variable x occurs free in the expression e. The second case is when there are several
φ1 , . . . φn ∈ δfe (x), such that sat(φ1 ∧ψ), . . . , sat(φn ∧ψ):
ψ ` (y:=e[x], δ)

(#if (φ1 ) y:=e[δ(x, φ1 )] #endif; . . . #if (φn ) y:=e[δ(x, φn )] #endif, δ)

(2.2)
Otherwise, meaning that for all φ ∈ δfe (x) it follows that unsat(φ∧ψ), we have:
ψ ` (y:=e[x], δ)

(2.3)

(y:=e[x], δ)

The third rule applies when a local variable is assigned
to within a context ψ ∈ FeatExp. There are three cases to consider here as well.
Conditional variable define.

ψ ` (x:=e, δ)

(3.1)

(δ(x, φ):=e), δ

when there exists an unique φ ∈ δfe (x), such that ψ|=φ .
ψ ` (x:=e, δ)

(#if (φ1 ) δ(x, φ1 ):=e #endif; . . . #if (φn ) δ(x, φn ):=e #endif), δ (3.2)

1-9

Effective Analysis of C Programs by Rewriting Variability

when there are φ1 , . . . φn ∈ δfe (x), such that sat(φ1 ∧ψ), . . . , sat(φn ∧ψ). Otherwise,
ψ ` (x:=e, δ)

(3.3)

(x:=e, δ)

After applying the above three rules, all local variable declarations that are conditionally defined (#if (φ) var x:=n in #endif s) are resolved. The transformed program
contains only #if-s where statements are conditionally defined.
The set of valid configurations K can be equated
to a propositional formula [4], say κ ∈ FeatExp, such that κ = ∨k∈K k. The last rule
simply replaces #if-s with ordinary if-s whose guards are strengthen with the feature
model κ, thus taking into account only valid configurations K of a family.
Conditional statement elimination.

ψ ` #if (φ) s #endif

if (φ∧κ) then s else skip

(4)

Note that we omit to write the environment δ in rules that do not use it explicitly (e.g.
rules (4), (5)). Let δ0 = [] be the empty environment. Let Rewr i t epreserve (pre-t(s), δ0 )
be the final transformed program s0 obtained from the pre-transformed program
pre-t(s) by applying the rules (1)–(3), and then the rule (4). The following result
shows that the set of final answers from terminating computations of s0 coincides with
the union of final answers from terminating computations of all variants from s.
S
Theorem 1. Let s0 = Rewr i t epreserve (pre-t(s), δ0 ). We have: [[s0 ]] = k∈K [[πk (s)]].
Proof. First, we show that Rewr i t epreserve (pre-t(s), δ0 ) terminates. This is due to the
fact the number of if-s in pre-t(s is finite, and by iteratively applying rules (1)–(3) we
eliminate all #if (φ) var x:=n in #endif s; whereas by applying rule (4) afterwards we
eliminate all #if (φ) s #endif. Subsequently, for each rule (1)–(3) and (4), the above
result can be proved by structural induction.
We now present an optimization rule, which is applied before the rules (1)–(4) for
eliminating if-s. The correctness of our transformation does not depend on it, but we
can use it for achieving faster convergence and smaller transformed programs. In our
implementation, we use many such optimization rules.
This rule collapses two sequentially composed #if-s with mutually
exclusive presence conditions φ0 and φ1 (i.e. φ0 ∧ φ1 ≡ false) that conditionally
enable the same statement s into one #if that conditionally enables s:
Guard inlining.

ψ ` #if (φ0 ) s #endif; #if (φ1 ) s #endif

#if (φ0 ∨ φ1 ) s #endif

(5)

Example 2. We present the transformation rules on a program family with F = {A, B}
and K = {A ∧ B, A ∧ ¬B, ¬A ∧ B, ¬A ∧ ¬B}.

#if (A) var x:=2 in #endif #if (¬A) var x:=5 in #endif #if (B) y:=x #endif, δ0

(1)
var x1 :=2 in #if (¬A) var x:=5 in #endif #if (B) y:=x #endif, [(x, A) 7→ x1 ]

(1)
var x1 :=2 in var x2 :=5 in #if (B) y:=x #endif, [(x, A) 7→ x1 , (x, ¬A) 7→ x2 ]
(2.2)
(4)

var x1 :=2 in var x2 :=5 in #if (B) #if (A) y:=x1 ; #endif#if (¬A) y:=x2 #endif #endif

var x1 :=2 in var x2 :=5 in if (B) then if (A) then y:=x1 else skip ;
if (¬A) then y:=x2 else skip ; else skip

1-10

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski

5

Implementation

We have developed a tool, called C Reconfigurator, which implements variabilityrelated transformations for the C language. All transformations are implemented using
Xtend 2 . The C Reconfigurator tool is available from: https://github.com/modelsteam/c-reconfigurator. It calls variability-aware parser SuperC [20] to parse code with
preprocessor annotations, which uses Binary Decision Diagrams (BDD’s) for encoding
feature expressions and for decisions during the parsing process. SuperC returns an
AST with variability, in which variability is reflected with choice nodes over feature
expressions. In particular, a choice node is a node with two children, such that the
left child of the choice node is included in the result of those configurations for which
the given feature expression is satisfied; otherwise the right child of the choice node
is included in the parsing result when the feature expression is not satisfied. We apply
our variability-related transformation rules as described in Section 4 on AST’s with
variability obtaining an ordinary AST, which is subsequently translated into a single
C program. Since IMP is a subset of C, all rewritings described in Section 4 transfer
directly to C. We now discuss how a selection of other interesting C constructs, which
are not present in IMP, are handled by our tool.
Variables declared with optional types are very common in C. For example, we have
x-bit integers on x-bit machines. We handle them in a similar way as configurable
variable declarations in rules (1)–(3). First, we rename and duplicate the variable
declaration, then at each point where the variable is used we transform the code such
that the used variable refers to the correct configuration name. For example,
#if (A) int #else float #endif x=0;
x = x+1;

will be transformed into:
int x1 = 0; float x2 = 0;
#if (A) x1 = x1 +1; #else x2 = x2 +1; #endif

Note that if optional local variables are initialized by non-constant expressions, then we
split their transformation into two parts: declaration which is performed by renaming
and duplication, followed by initialization where all optional variables refer to the
correct configuration.
Optional (configurable defined) functions are important since all statements in C
are inside some function. If conditionally defined code occurs in the function body,
then it will be transformed using the corresponding rules. For example,
int f (int x) {return #if (A) x++ #else 0 #endif; }

will be transformed into:
int f (int x) {return A? x++ : 0; }
2

http://www.eclipse.org/xtend/.

1-11

Effective Analysis of C Programs by Rewriting Variability

If the function signature is configurable, then we use renaming plus duplication
as in rules (1)–(3) for handling configurable variable declarations. For example, the
code:
int f (#if (A) int #else float #endif x) {. . .}

. . . f (5) . . .

will be transformed into:
int f1 (int x) {. . .}
int f2 (float x) {. . .}

. . . #if (A) f1 (5) #else f2 (5) #endif . . .

Arrays with optional size are also possible in real-world C programs. They usually
emerge via constant macros with conditional definitions. For example, the code
int a[#if (A) 10 #else 15 #endif ];
a[5] = 0;

will be transformed into:
int a1 [10]; int a2 [15];
#if (A) a1 [5] = 0; #else a2 [5] = 0; #endif

All other variability patterns that we met in our examples, such as configurable
fields in struct-s and pointers, are also handled similarly: first by using renaming and
duplication, then by modifying all references to the given pattern such that the use
always refers to the correct definition. Consider the following code with pointers:
int a = 10; int ∗ p = &a; #if (A) p = nul l; #endif (∗p)++

will be transformed into:
int a = 10; int ∗ p = &a; if (A) p = nul l; (∗p)++

Hence, we obtain a variability bug whenever the feature A is enabled.
We can see that most of the variability patterns are handled using renaming
plus duplication. In the worst case, this may cause exponential growth of the transformed program in the number of used features. However, in practice this does not
happen often (see Table 3 for some data from real files). Namely, variability patterns
usually depend on a few features, so only a few new definitions are used. Also we apply
several optimization rules, which eliminate all definitions that do not correspond to a
valid configuration. Finally, the evaluation results in Section 6 show that the analysis
time for such transformed programs is comparable to single programs. This is due to
the fact that transformed programs are not increased significantly and the analysis
tools we use (Frama-C, Clang, LLBMC) are very optimized and mature.
Remark.

1-12

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski

6

Evaluation

We evaluate our reconfiguration technique based on variability transformations and
single-program verification oracles on several real-world C case studies. The evaluation
aims to show that we can use state-of-the-art single-program verification tools to
verify realistic C program families using variability-related transformations. To do so,
we ask the following research questions:
How precise is our technique? (RQ1)
How efficient is the verification oracle to identify variability bugs after transforming
the code using our technique? (RQ2)
In particular, we want to reproduce the variability bugs reported in [1, 28] using various
verification oracles applied on transformed programs, which are obtained using our
tool. We use Frama-C [27], Clang [9] and LLBMC [30] as our verification oracles.
Frama-C is a framework for modular static (dataflow) analysis of C programs. The
Clang project includes the Clang compiler front-end and the Clang static analyzer for
several programming languages, including C. LLBMC (the low-level bounded model
checker) is a software model checking tool for finding bugs in C programs.
6.1 Subject Files and Experimental Setup

All transformations are applied using the C Reconfigurator tool as described in
Section 5. We investigate precision and performance in finding real variability bugs
extracted from three benchmarks: Linux, BusyBox and Libssh. In particular, we use
simplified bugs from the VDBb 3 database that are found in the Linux kernel files [1]
and in BusyBox. Abal et al. [1] created a simplified version of a program for each
bug they found by capturing the same essential behavior (and the same problem)
as in the original bug. Simplified bugs are independent of the kernel code and the
corresponding programs were derived systematically from the error trace. In addition,
we use real variability bugs from Libssh provided by Medeiros et al. [28].
Table 1 presents the characteristics of the subject files we analyzed in our empirical
study. We list: the file id, bug type, number of features (|F|), number of valid configurations (|K|), lines of code, the size in KB of the files before (with #ifdef-s) and after
(without #ifdef-s) our transformations, and commit hash (clickable) for each project.
This collection consists of a diverse set of bug types such as null pointer dereferences,
buffer overflow, and uninitialized variable. In total, we have 11 distinct kinds of bugs.
The number of features per file varies from one to seven. In addition, the number of
lines of code ranges from 12 to 165 for the simplified files (from VBDb), and from 1404
to 2959 for real files (from Libssh). After the transformation, the biggest increase in
size of almost 8 times can be observed for file id 7. This is due to the fact that this
file has seven different features and several variability patterns that depend on them.
In most of the other cases the size increase is not very big.

3

http://VBDb.itu.dk.

1-13

Effective Analysis of C Programs by Rewriting Variability

File
id

Bug type

VBDb Linux files
1
null pointer deref.
2
null pointer deref.
3
null pointer deref.
4
null pointer deref.
5
buffer overflow
6
buffer overflow
7
read out of bounds
8
uninitialized var.
9
uninitialized var.
10
uninitialized var.
11
uninitialized var.
12
uninitialized var.
13
undefined symbol
14
undefined symbol
15
undefined symbol
16
undefined symbol
17
undeclared identifier
18
undeclared identifier
19
wrong # of args
20
multiple funct. defs
21
dead code
22
incompatible type
23
assertion violation
24
assertion violation
25
assertion violation
VBDb BusyBox files
26
null pointer deref.
27
null pointer deref.
28
uninitialized var.
29
undefined symbol
30
undefined symbol
31
undeclared identifier
32
undeclared identifier
33
incompatible type
Real Libssh files
34
null pointer deref.
35
null pointer deref.
36
uninitialized var.

|F|

|K|

LOC

Size KB
before

after

Hash

5
3
4
3
1
1
7
2
1
1
2
2
4
2
2
2
3
2
1
2
1
2
2
2
2

24
6
8
6
2
2
63
4
2
2
4
4
14
4
4
4
8
4
2
4
2
4
4
4
4

165
112
55
34
58
33
69
54
54
53
38
26
25
20
20
19
37
20
12
21
19
27
79
75
41

2.9
1.9
0.9
0.5
1.0
0.6
1.1
0.8
1.0
0.8
0.9
0.3
0.4
0.3
0.3
0.3
0.6
0.3
0.2
0.3
0.2
0.4
1.5
1.1
0.6

4.3
2.5
1.0
0.6
1.2
0.7
8.4
1.0
1.1
1.0
1.2
0.5
0.6
0.5
0.5
0.5
1.0
0.4
0.4
0.8
0.3
0.7
1.8
1.2
0.7

76baeeb
f7ab9b4
ee3f34e
6252547
8c82962
60e233a
0f8f809
7acf6cd
bc8cec0
30e0532
1c17e4d
e39363a
7c6048b
2f02c15
6515e48
242f1a3
6651791
f48ec1d
e67bc51
e68bb91
809e660
d6c7e11
63878ac
657e964
0988c4c

1
2
2
1
2
1
1
3

2
4
4
2
4
2
2
8

28
24
28
42
27
35
19
46

0.4
0.4
0.4
0.8
0.4
0.5
0.3
0.9

0.7
0.6
0.7
0.9
0.6
0.8
0.4
1.5

199501f
1b487ea
b273d66
cf1f2ac
ebee301
5275b1e
b7ebc61
5cd6461

6
4
3

48
4
4

1404
1428
2959

34.8
44.1
72.4

32.6
31.9
77.6

0a4ea19
fadbe80
2a10019

Table 1 Characteristics of the benchmark files.

1-14

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski

Frama-C
id

buggy variantreconfigured all

y/n time

y/n time

time

VBDb Linux files
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø
Ø

218
220
215
218
218
213
218
241
224
216
234
216
239
237
224
213
216
210
210
213
239

Ø
Ø

x

Ø
Ø
Ø
Ø
Ø
Ø
inc
Ø
inc
Ø
Ø
Ø
Ø
Ø
Ø
Ø

x
x

235
225
236
224
227
227
225
250
230
224
224
227
248
244
248
222
230
224
224
228
240

5602
1394
1918
1379
488
463
14381
918
462
460
917
914
3194
905
906
910
3823
901
452
907
458

Clang/LLBMC
id

yes/no time yes/no time time
VBDb Linux files
22
23
24
25

Ø
Ø
Ø
Ø
Ø
Ø
Ø

230
224
237
230
231
220
216

Ø
Ø
inc
Ø
Ø
Ø
Ø

234
234
237
236
228
228
224

484
959
957
481
968
486
477

Ø
Ø
Ø
Ø

21
4
3
3

Ø
Ø
Ø
Ø

23
10
7
5

91
10
11
8

31

222

VBDb BusyBox files
33

Ø

27

Ø

(b) VBDb files using Clang (files 22 and

33) and LLBMC (files 23, 24, and 25).
Clang/LLBMC
id

buggy variantreconfigured all

yes/no time yes/no time time
34
35
36

VBDb BusyBox files
26
27
28
29
30
31
32

buggy variantreconfigured all

Ø
Ø
Ø

1526
1591
112

Ø
Ø
Ø

1702 17029
1804 5917
144 448

(c) Libssh files using Clang (file 36) and

LLBMC (files 34 and 35).

(a) VBDb files using Frama-C.
Table 2 Verification results for the benchmark files. Times in milliseconds (ms).

All experiments were executed on a Kubuntu VM (64bit, 4 CPUs), Intel® Core T M i73720QM CPU running at 2.6GHz with 12GB RAM memory. The performance numbers
reported constitute the median runtime of fifty independent executions.
6.2 Results

We now present the results of our empirical study and discuss the implications.
All experiment materials are available online at https://github.com/models-team/creconfigurator-test. Before we proceed, we stress that we only evaluate bugs that are
detectable by the verification tools on the erroneous variant code.

1-15

Effective Analysis of C Programs by Rewriting Variability

Table 2a shows the results of verifying our benchmark files which
contain known bugs by using Frama-C. The table has three main columns: buggy
variant, reconfigured, and all that depict the tool results on the buggy variant
code, on the reconfigured program family code, and on all valid variants from K
analyzed one by one (in a brute force fashion), respectively. Each checkmark (Ø)
means that the same bug was found in both the buggy variant and reconfigured
program by the verification tool. Otherwise, the result is either x —bug not found
in the reconfigured program, or inc—inconclusive which means that Frama-C was
able to detect a bug in the reconfigured program that is different from the bug in the
product variant. In the case of brute force approach (all), we consider the analyses
times of all valid variants regardless of whether they contain a bug or not.
In terms of precision, our C Reconfigurator tool transforms the family code by
preserving the erroneous traces from the buggy variant in most cases. For instance,
Frama-C could detect 22 (78%) bugs from the simplified benchmark files (28 in total)
after reconfiguring the files using our tool. Besides that, the C Reconfigurator
preserves a variety of bug types such as buffer overflow and uninitialized variable.
Still, for different types of bugs the success rate depends on the tool which may or
may not detect them. For example, our technique is able to transform a file containing
a memory leak error, but Frama-C does not have any analysis to identify it.
In three specific cases (cf. file ids 10, 12 and 28), Frama-C did not report the
original bug as an error, but it did detect that some variable might be uninitialized
in some conditions. This happens because Frama-C performs a may value analysis
for finding uninitialized variables. A may analysis describes information that may
possibly be true along one path to the given program point and, thus in our case,
computes a superset of all uninitialized variables in all variants. So the reported
variable may not match with the one in the buggy variant. We marked these three
cases as inc—inconclusive in the table. Still the verification oracle reports that there
might be an error in the reconfigured code.
In addition, the verification tool could not identify the required bug in the reconfigured file in three cases (cf. file ids 3, 20 and 21). For example, file 21 contains
dead code, which is a function (do_sect_fault()) that is never called when feature
ARM is enabled (see the code snippet in Fig. 4, left column). The C Reconfigurator
transforms the code by changing the #ifdef into ordinary if condition, making the
function available for the transformed single program (i.e., the function is not dead
any more), as shown in the code snippet in Fig. 4 (right column). The other two cases
are similar to this one in the sense that the C Reconfigurator makes feature code
explicit to the entire program family.
Generally speaking, if one variant does not use a variable/function, but another
does, then the reconfigured code will use the variable/function and the error will be
hidden (like in the example above). This happens due to the limitations of variability
encoding, especially because we cannot preprocess the reconfigured code to filter out
the irrelevant features for a particular variant. In a reconfigured code, all variants are
encoded as a single program (see Section 6.4 for more discussion).
We now consider the remaining simplified files. We use Clang and LLBMC to
analyze only the other types of bugs (incompatible type and assertion violation) that
Simplified files.

1-16

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski

int do_sect_fault(){
return 0;

int do_sect_fault(){
return 0;

}
int main(){
#ifndef ARM
do_sect_fault();
#endif
return 0;
}

}
int main(){
if (! ARM)
do_sect_fault();
return 0;

}

Figure 4 File 21 - Before (left) and after (right) our transformations

Frama-C cannot handle. We treat Clang/LLBMC as one verification oracle, since we
first need to compile and emit llvm code with Clang in order to analyze it using
LLBMC. So, we do not make difference in reporting whether the bug was found by
Clang during the compilation or afterwards by LLBMC.
Table 2b, similarly to Table 2a, shows the results of verifying both the buggy variant
and the reconfigured code using Clang and LLBMC. We also report the analysis
time of the brute force approach in the column all. As we can see, all bugs were
found by Clang/LLBMC in the reconfigured version. We can thus confirm that our C
Reconfigurator tool transforms the family code by preserving the erroneous traces
from the buggy variant. We are now ready to answer RQ1 on the precision of our
technique. Based on analyzing 33 simplified variability bugs from Linux and BusyBox,
we find that:
Answer RQ1 (precision). The C Reconfigurator enables single-program
verification tools such as Frama-C, Clang, and LLBMC to successfully detect
most of the simplified variability bugs on the reconfigured code, obtained
from the Linux and BusyBox benchmark files.
We now turn to evidence regarding research question RQ2 (performance). We evaluate
performance of the verification tools to identify the given variability bugs. Tables 2a
and 2b show time needed for the verification tools to analyze the buggy variant code
(buggy variant column) and the reconfigured program family code (reconfigured
column). We can see that the analysis times in both cases are similar although
reconfigured code is bigger in size. In fact, Frama-C takes less than half a second to
analyze each file regardless whether it is a variant or a reconfigured file. For instance,
Frama-C analyzes file 1 in 218 and 235 milliseconds on the variant code and on the
reconfigured program family code, respectively. Recall that file 1 contains a null pointer
dereference and has five features. If we apply the brute force approach (all column),
which analyzes all variants individually one by one, to this file using Frama-C it takes
5,602 ms, since the number of configurations is 24. In this way, we obtain significant
speed-up to verify the program family using our approach. We also obtain similar
results in terms of performance using Clang/LLBMC (see Tables 2b and 2c). In general,
the performance of analyzing a reconfigured code is similar to analyzing only one
variant, which gives us a speed-up proportional to the number of valid variants of a

1-17

Effective Analysis of C Programs by Rewriting Variability

program family. Overall, we answer the second research question (RQ2) by observing
that:
Answer RQ2 (performance). The C Reconfigurator speeds-up the familybased analysis via single-program verification tools, so that we can efficiently
detect simplified variability bugs on the reconfigured code, obtained from
the VBDb benchmark.
We now consider real files to confirm our previous observations with
respect to precision and performance. Table 2c presents the results of analyzing three
real files from the Libssh project using Clang and LLBMC. 4 These files contain two
types of bugs: null pointer dereference and uninitialized variable. Each file has at
least three distinct features.
We can see that our C Reconfigurator transforms the family code by preserving
the erroneous traces from the buggy variant even for complex and large files. In fact,
the verification tool (Clang/LLBMC) found the same bug (from the buggy variant
code) on the reconfigured code in all three cases. From this preliminary evidence,
we thus confirm that our technique enables single-program verification oracles to
successfully detect variability bugs on the reconfigured code, obtained from complex
and real files.
Regarding performance, we can still see the similarity in verifying a variant code
and a reconfigured one. For example, Clang/LLBMC took 1,5 sec to analyze file 34 in
the single variant version, whereas in the reconfigured version, the tool analyzed it
in 1,7 sec. We can also observe a speed-up of the family-based analysis using the C
Reconfigurator and single-program verification tools by a factor of the number of
valid variants compared to the brute force approach. We conclude that:
Summary. All single-program verification tools (Frama-C, Clang, LLBMC)
detect successfully and efficiently most of the variability bugs on the reconfigured code as well as on the single variant code.
Real files.

6.3 Threats to Validity

Verifying semantics preservation in a complex transformation is a
very hard problem [22, 2]. We manually verified the correctness of the C Reconfigurator on the simplified VBDb files by comparing the original and the reconfigured
files side-by-side, which leaves space for human error. For the larger real files we were
not able to determine if the C Reconfigurator preserved semantics for all variants
on the entire file due to the complex configuration space, but instead we focused on
the functions involved in producing/reproducing the bug. We mitigate this threat by
relying on the results of our evaluation which show the effectiveness of conventional
single-program analysis tools to identify the same bugs in the reconfigured code
version as in the buggy single varaints.
Internal validity.

4

We do not report results from Frama-C on the real files because Frama-C could not handle
them.

1-18

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski

From our preliminary evaluation, we show that our technique
transforms the program family code by preserving the erroneous traces from the
buggy variant. However, we acknowledge that our transformations were not tested
under the entirety of the C language, but only on the subset used in the VBDb and
Libssh files presented here. The C Reconfigurator though can be extended with
extra rules to deal with other cases that we did not face in our benchmark files. Worst
case exponential growth of transformed programs can happen, even though we have
not observed it in our subject files.
External validity.

6.4 Discussion

The main limitation of our transformation based approach is that we may not obtain
conclusive results for all individual variants, thus losing some precision. This is due to
the fact that our transformed program contains all possible paths that may occur in
any variant. However, the precision loss depends on the particular analysis we use.
Consider the case of model checking. Since (single-system) model checkers stop
once a single counter-example is found in the model, we can use our approach to find
a variability bug which occurs in some subset of valid variants but we will not be able
to report conclusive results (whether the given property is satisfied or not) for the
rest of the valid variants. To overcome this issue, we may repeat our technique on
the remaining variants for which no conclusive results were reported in the previous
iteration.
Consider the case of must dataflow analysis (e.g., available expressions, very busy
expressions). In this case, the result in a given program point contains only the
common results found on all execution paths to that point. Thus, the analysis result
for the transformed program will contain only the results that occur in all variants. For
example, for available expressions analysis we may obtain less available expressions
than there are in any single variant. The available expression analysis determines
which expressions must have already been computed, and not later modified, on all
paths to a program point [32]. This information can be used to avoid re-computation
of an expression. Consider the program family:
x := a + b; while (y > a + b) do { #ifdef (A) y := y − 1 #else a := a + 1 #endif }

The expression a + b is available at the guard of the while loop for variants satisfying
A, so it needs not be re-computed for them. However, in the transformed program we
have paths from all variants, so the expression a + b is modified by the assignment
a := a + 1 in a path coming from variants ¬A. Therefore, the analyzer will not report
this expression as available at the guard of the loop for the transformed program.
Consider the case of may dataflow analysis (e.g., reaching definitions, live variables,
uninitialized variables). In this case, the result in a given program point contains the
results found on at least one execution path to that point. Thus, the analysis result
for the transformed program will contain all results that occur in at least one variant.
For example, for live variables analysis, we may obtain more live variables than there
are in any single variant. The live variables analysis determines which variables may
be live at a program point, that is there is a path from the program point to a use of

1-19

Effective Analysis of C Programs by Rewriting Variability

the variable that does not redefine it [32]. This information can be used as a basis for
dead code elimination. If a variable is not live at the exit from an assignment to the
variable, then that assignment can be eliminated. Consider the program family:
x := 5; y := 1; #ifdef (A) x := 1 #else x := x + 1 #endif

The variable x is not live at the exit from the first assignment x := 5 for variants
satisfying A. Therefore, the assignment x := 5 is redundant for those variants. However,
x is live for ¬A variants, so it will be live after the first assignment for the transformed
program as well. Thus, we cannot eliminate this assignment in the transformed
program. This is also the reason why Frama-C does not identify the variability bug
for files 3, 20 and 21.

7

Related work

Recently, formal analysis and verification of program families have been a topic of
considerable research. The challenge is to develop efficient techniques that work at
the level of program families, rather than the level of single programs. There are two
main approaches to address this issue: (1) to develop dedicated variability-aware
(family-based) techniques and tools; (2) to use specific simulators and encodings
which transform program families into single programs that can be analyzed by
the standard single-program verification tools. The two approaches have different
strengths and weaknesses. The advantage of (1) is that precise (conclusive) results
are reported for every variant, but the disadvantage is that their implementation
can be tedious and labor intensive. On the other hand, the approaches based on (2)
re-use existing tools from single-program world, but some precision may be lost when
interpreting the obtained results.
Various lifted techniques have been
proposed which lift existing single-program verification techniques to work on the
level of program families. This includes lifted syntax checking [25, 20], lifted type
checking [24, 8], lifted static analysis [7, 6, 31], lifted model checking [10, 14], etc.
TypeChef [25] and SuperC [20] are variability-aware parsers, which can parse languages with preprocessor annotations. The results are ASTs with variability nodes. The
difference between these two approaches is that feature expressions are represented
as formulae in TypeChef, and as BDD’s in SuperC. TypeChef has also implemented
some variability-aware dataflow analyses. Several approaches have been proposed
for type checking program families directly. In particular, lifted type checking for
Featherweight Java was presented in [24], whereas variational lambda calculus was
studied in [8]. Lifted model checking for verifying variability intensive systems has
been introduced in [10]. SNIP, a specifically designed family-based model checker,
is implemented for efficient verification of temporal properties of such systems. The
input language to SNIP is fPromela, which represents a variability-aware extension
of the known Promela language for the (single-system) SPIN model checker [21].
fPromela uses an #ifdef-like statement for encoding multiple variants, which repSpecifically designed variability-aware techniques.

1-20

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski

resents a nondeterministic “if” statement guarded by features expressions that are
used to specify what system parts are included (resp., excluded) for which variants.
An approach for lifted software model checking using game semantics has been
introduced in [14]. It verifies safety of #ifdef-based second-order program families
containing undefined components, which are compactly represented using symbolic
game semantics models [13, 12]. Brabrand et al. [7] and Midtgaard et al. [31] show
how to lift any single-program dataflow analysis from the monotone framework to
work on the level of program families. The obtained lifted dataflow analyses are much
faster than ones based on the naive variant-by-variant approach that generates and
analyzes all variants one by one. Another efficient implementation of lifted analysis
formulated within the IFDS framework for inter-procedural distributive environments
has been proposed in SPLLIFT [6]. In order to speed-up the lifted verification techniques, variability abstractions have been introduced in [17, 18, 15, 16]. They tame the
exponential blowup caused by the large number of features and variants in a program
family. In this way, variability abstractions enable deliberate trading of precision for
speed in the context of lifted (monotone) data-flow analysis [17, 18] and lifted model
checking [15, 16].
Lifting by simulation. Variability encoding [37] and configuration lifting [33] are
based on generating a product-line simulator which simulates the behaviour of all
products in the product line. Then, an existing off-the-shelf single-program analyzer is
used to verify the generated product-line simulator, which represents a single program.
The work in [37] defines variability encoding on the top of TypeChef parser for C and
Java program families. They have applied the results of variability encoding to testing
[26], model checking [3], and deductive verification [36]. Compared to [37], our
approach has the following distinguished characteristics. C Reconfigurator is aimed
at transforming C program families and uses SuperC as a back-end tool. We show
transformation rules and their correctness with respect to a minimal C-like imperative
(state-based) language, whereas in [37] the rules and their correctness is shown
with respect to Featherweight Java. C is a language much wider used in industry for
variability than (Featherweight)Java. Also, we do not have to rely on object-oriented
encodings to make the variability-transformations work. We evaluate our approach
with several state-of-the-art single-program verification tools for finding real variability
bugs on real-world C programs (both on large and sanitized files). The academic
examples (e-mail, elevator, mine-pump) considered by Apel et al. [3] are considerably
smaller than those presented here; and they are focussed on verifying specific class of
bugs: undesired feature interactions (using CPAchecker [5]), whereas we consider
here various types of more severe bugs that occur in practice. In this way, the external
validity of our experiments is considerably broader. Yet another difference is that the
work in [3] considers product lines implemented using compositional approaches,
where all features are modeled as separate and composable units. In contrast, we
consider here annotative product lines based on #ifdef-s, which is a common way of
implementing variability in industry.

1-21

Effective Analysis of C Programs by Rewriting Variability

8

Conclusion

We have proposed variability-related transformations to translate program families
into single programs without variability. The transformed programs can then be effectively analyzed using various single-program analyzers. The evaluation confirms
that some interesting variability bugs can be found in real-world C programs in this
way. As a future work, we plan to extend our evaluation and consider more verification
oracles as well as different practical case studies. We derive several observations from
the attempt to verify, analyze, and find bugs in realistic C programs. We hope that
our technique will be useful for future builders of analysis tools.

References

[1] Iago Abal, Claus Brabrand, and Andrzej Wasowski. 42 variability bugs in the
linux kernel: a qualitative analysis. In ACM/IEEE International Conference on
Automated Software Engineering, ASE ’14, pages 421–432. ACM, 2014. URL: http:
//doi.acm.org/10.1145/2642937.2642990, doi:10.1145/2642937.2642990.
[2] Ahmad Salim Al-Sibahi, Aleksandar S. Dimovski, and Andrzej Wasowski. Symbolic execution of high-level transformations. In Proceedings of the 2016 ACM
SIGPLAN International Conference on Software Language Engineering, SLE 2016,
pages 207–220. ACM, 2016.
[3] Sven Apel, Alexander von Rhein, Philipp Wendler, Armin Größlinger, and Dirk
Beyer. Strategies for product-line verification: case studies and experiments. In
35th Intern. Conference on Software Engineering, ICSE ’13, pages 482–491, 2013.
[4] Don Batory. Feature models, grammars, and propositional formulas. In 9th
International Software Product Lines Conference, SPLC ’05, volume 3714 of LNCS,
pages 7–20. Springer-Verlag, 2005.
[5] Dirk Beyer and M. Erkan Keremoglu. Cpachecker: A tool for configurable software
verification. In Computer Aided Verification - 23rd International Conference,
CAV 2011. Proceedings, volume 6806 of LNCS, pages 184–190, 2011. URL: http:
//dx.doi.org/10.1007/978-3-642-22110-1_16, doi:10.1007/978-3-642-22110-1_16.
[6] Eric Bodden, Társis Tolêdo, Márcio Ribeiro, Claus Brabrand, Paulo Borba, and
Mira Mezini. Spllift : Statically analyzing software product lines in minutes
instead of years. In ACM SIGPLAN Conference on PLDI ’13, pages 355–364, 2013.
[7] Claus Brabrand, Márcio Ribeiro, Társis Tolêdo, Johnni Winther, and Paulo Borba.
Intraprocedural dataflow analysis for software product lines. Transactions on
Aspect-Oriented Software Development, 10:73–108, 2013.
[8] Sheng Chen, Martin Erwig, and Eric Walkingshaw. An error-tolerant type system
for variational lambda calculus. In ACM SIGPLAN International Conference on
Functional Programming, ICFP’12, pages 29–40, 2012. URL: http://doi.acm.org/10.
1145/2364527.2364535, doi:10.1145/2364527.2364535.
[9] Clang. Clang static analyzer. Clang: a C language family frontend for LLVM.
URL: http://clang-analyzer.llvm.org/.

1-22

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski

[10] Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel
Legay, and Jean-François Raskin. Featured transition systems: Foundations
for verifying variability-intensive systems and their application to LTL model
checking. IEEE Trans. Software Eng., 39(8):1069–1089, 2013. URL: http://doi.
ieeecomputersociety.org/10.1109/TSE.2012.86, doi:10.1109/TSE.2012.86.
[11] Paul Clements and Linda Northrop. Software Product Lines: Practices and Patterns.
Addison-Wesley, 2001.
[12] Aleksandar Dimovski and Ranko Lazic. Compositional software verification
based on game semantics and process algebra. STTT, 9(1):37–51, 2007. URL:
http://dx.doi.org/10.1007/s10009-006-0005-y, doi:10.1007/s10009-006-0005-y.
[13] Aleksandar S. Dimovski. Program verification using symbolic game semantics.
Theor. Comput. Sci., 560:364–379, 2014. URL: http://dx.doi.org/10.1016/j.tcs.2014.
01.016, doi:10.1016/j.tcs.2014.01.016.
[14] Aleksandar S. Dimovski. Symbolic game semantics for model checking program
families. In Model Checking Software - 23nd International Symposium, SPIN 2016,
Proceedings, volume 9641 of LNCS, pages 19–37. Springer, 2016.
[15] Aleksandar S. Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, and Andrzej
Wasowski. Family-based model checking without a family-based model checker.
In 22nd International SPIN Workshop on Model Checking of Software, SPIN ’15,
volume 9232 of LNCS, pages 282–299. Springer, 2015.
[16] Aleksandar S. Dimovski, Ahmad Salim Al-Sibahi, Claus Brabrand, and Andrzej
Wasowski. Efficient family-based model checking via variability abstractions.
STTT, 2016. doi:10.1007/s10009-016-0425-2.
[17] Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Variability
abstractions: Trading precision for speed in family-based analyses. In 29th
European Conference on Object-Oriented Programming, ECOOP ’15, volume 37 of
LIPIcs, pages 247–270. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
[18] Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Finding suitable
variability abstractions for family-based analysis. In FM 2016: Formal Methods 21st International Symposium, Proceedings, volume 9995 of LNCS, pages 217–234,
2016. URL: http://dx.doi.org/10.1007/978-3-319-48989-6_14, doi:10.1007/978-3-31948989-6_14.
[19] Alejandra Garrido and Ralph E. Johnson. Refactoring C with conditional compilation. In 18th IEEE International Conference on Automated Software Engineering
(ASE 2003), pages 323–326. IEEE Computer Society, 2003. URL: http://doi.
ieeecomputersociety.org/10.1109/ASE.2003.1240330, doi:10.1109/ASE.2003.1240330.
[20] Paul Gazzillo and Robert Grimm. Superc: parsing all of C by taming the
preprocessor. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’12, 2012, pages 323–334, 2012. URL: http:
//doi.acm.org/10.1145/2254064.2254103, doi:10.1145/2254064.2254103.
[21] Gerard J. Holzmann. The SPIN Model Checker - primer and reference manual.
Addison-Wesley, 2004.

1-23

Effective Analysis of C Programs by Rewriting Variability

[22] Alexandru F. Iosif-Lazar, Ahmad Salim Al-Sibahi, Aleksandar S. Dimovski,
Juha Erik Savolainen, Krzysztof Sierszecki, and Andrzej Wasowski. Experiences from designing and validating a software modernization transformation
(E). In 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, pages 597–607, 2015. URL: http://dx.doi.org/10.1109/ASE.2015.84,
doi:10.1109/ASE.2015.84.
[23] Kyo C. Kang, Sholom G. Cohen, James A. Hess, William E. Novak, and A. Spencer
Peterson. Feature-Oriented Domain Analysis (FODA) feasibility study. Technical
report, Carnegie-Mellon University Software Engineering Institute, November
1990.
[24] Christian Kästner, Sven Apel, Thomas Thüm, and Gunter Saake. Type checking
annotation-based product lines. ACM Trans. Softw. Eng. Methodol., 21(3):14, 2012.
[25] Christian Kästner, Paolo G. Giarrusso, Tillmann Rendel, Sebastian Erdweg, Klaus
Ostermann, and Thorsten Berger. Variability-aware parsing in the presence of
lexical macros and conditional compilation. In OOPSLA’11, pages 805–824. ACM,
2011.
[26] Christian Kästner, Alexander von Rhein, Sebastian Erdweg, Jonas Pusch, Sven
Apel, Tillmann Rendel, and Klaus Ostermann. Toward variability-aware testing.
In FOSD ’12, pages 1–8, 2012.
[27] Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris
Yakobowski. Frama-c: A software analysis perspective. Formal Asp. Comput.,
27(3):573–609, 2015. URL: http://dx.doi.org/10.1007/s00165-014-0326-7, doi:10.
1007/s00165-014-0326-7.
[28] Flávio Medeiros, Márcio Ribeiro, Rohit Gheyi, Christian Kästner, and Sven Apel.
An empirical study on configuration-related bugs. Submitted for publication at
IEEE TSE, 2016.
[29] Jean Melo, Claus Brabrand, and Andrzej Wasowski. How does the degree of
variability affect bug finding? In Proceedings of the 38th International Conference
on Software Engineering, ICSE ’16, pages 679–690, New York, NY, USA, 2016. ACM.
URL: http://doi.acm.org/10.1145/2884781.2884831, doi:10.1145/2884781.2884831.
[30] Florian Merz, Stephan Falke, and Carsten Sinz. LLBMC: bounded model checking
of C and C++ programs using a compiler IR. In Verified Software: Theories, Tools,
Experiments - 4th International Conference, VSTTE 2012, Proceedings, volume 7152
of LNCS, pages 146–161. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-64227705-4_12, doi:10.1007/978-3-642-27705-4_12.
[31] Jan Midtgaard, Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski.
Systematic derivation of correct variability-aware program analyses. Sci. Comput.
Program., 105:145–170, 2015. URL: http://dx.doi:10.1016/j.scico.2015.04.005, doi:
10.1016/j.scico.2014.10.002.
[32] Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Principles of Program
Analysis. Springer-Verlag, Secaucus, USA, 1999.
[33] H. Post and C. Sinz. Configuration lifting: Verification meets software configuration. In ASE’08, pages 347–350, LAquila, Italy, 2008. IEEE Computer Society.

1-24

A. F. Iosif-Lazar, J. Melo, A. S. Dimovski, C. Brabrand, A. Wasowski

[34] John C. Reynolds. Theories of Programming Languages. Cambridge University
Press, 1998.
[35] Thomas Thüm, Sven Apel, Christian Kästner, Ina Schaefer, and Gunter Saake. A
classification and survey of analysis strategies for software product lines. ACM
Comput. Surv., 47(1):6, 2014.
[36] Thomas Thüm, Ina Schaefer, Martin Hentschel, and Sven Apel. Family-based
deductive verification of software product lines. In Generative Programming and
Component Engineering, GPCE’12, pages 11–20. ACM, 2012. URL: http://doi.acm.
org/10.1145/2371401.2371404, doi:10.1145/2371401.2371404.
[37] Alexander von Rhein, Thomas Thüm, Ina Schaefer, Jörg Liebig, and Sven Apel.
Variability encoding: From compile-time to load-time variability. J. Log. Algebr.
Meth. Program., 85(1):125–145, 2016. URL: http://dx.doi.org/10.1016/j.jlamp.2015.
06.007, doi:10.1016/j.jlamp.2015.06.007.

1-25

