An Incremental Slicing Method for Functional Programs
PRASANNA KUMAR K., IIT Bombay
AMITABHA SANYAL, IIT Bombay
AMEY KARKARE, IIT Kanpur

arXiv:1709.08016v1 [] 23 Sep 2017

Several applications of slicing require a program to be sliced with respect to more than one slicing criterion. Program specialization,
parallelization and cohesion measurement are examples of such applications. These applications can benefit from an incremental static
slicing method in which a significant extent of the computations for slicing with respect to one criterion could be reused for another.
In this paper, we consider the problem of incremental slicing of functional programs.
We first present a non-incremental version of the slicing algorithm which does a polyvariant analysis1 of functions. Since polyvariant
analyses tend to be costly, we compute a compact context-independent summary of each function and then use this summary at the
call sites of the function. The construction of the function summary is non-trivial and helps in the development of the incremental
version. The incremental method on the other hand consists of a one-time pre-computation step that uses the non-incremental version
to slice the program with respect to a fixed default slicing criterion and processes the results further to a canonical form. Presented
with an actual slicing criterion, the incremental step involves a low-cost computation that uses the results of the pre-computation to
obtain the slice.
We have implemented a prototype of the slicer for a pure subset of Scheme, with pairs and lists as the only algebraic data types.
Our experiments show that the incremental step of the slicer runs orders of magnitude faster than the non-incremental version. We
have also proved the correctness of our incremental algorithm with respect to the non-incremental version.
ACM Reference format:
Prasanna Kumar K., Amitabha Sanyal, and Amey Karkare. 2017. An Incremental Slicing Method for Functional Programs. 1, 1,
Article 1 (September 2017), 18 pages.
DOI: 10.1145/nnnnnnn.nnnnnnn

1

INTRODUCTION

Program slicing refers to the class of techniques that delete parts of a given program while preserving certain desired
behaviors, for example, memory, state or parts of output. These behaviors are called slicing criteria. Applications of
slicing include debugging (root-cause analysis), program specialization, parallelization and cohesion measurement.
However, in some of the above applications, a program has to be sliced more than once, each time with a different
slicing criterion. In such situations, the existing techniques [5, 8, 15, 18, 20, 23] are inefficient as they typically analyze
the program multiple times. Each round of analysis involves a fixed point computation on the program text or some
intermediate form of the program, typically SDG in the case of imperative languages. We thus require an incremental
1 In

a polyvariant analysis [21], the definition of a function in some form is re-analyzed multiple times with respect to different application contexts.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not
made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components
of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to
redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.
© 2017 ACM. Manuscript submitted to ACM

Manuscript submitted to ACM

1

2

Prasanna Kumar K., Amitabha Sanyal, and Amey Karkare
(define (lcc str lc cc)
(if (null? str)
(return (cons lc cc))
(if (eq? (car str) nl)
(return (lcc (cdr str)
(+ lc 1)
(+ cc 1)))
(return (lcc (cdr str)
π 1 :lc
π 2 :(+ cc 1))))))

(define (lcc str lc )
(if (null? str)
(return (cons lc ))
(if (eq? (car str) nl)
(return (lcc (cdr str)
(+ lc 1)
))
(return (lcc (cdr str)
π1 :lc
π2 : )))))

(define (lcc str  cc)
(if (null? str)
(return (cons  cc))
(if (eq? (car str) nl)
(return (lcc (cdr str)

(+ cc 1)))
(return (lcc (cdr str)
π1 : 
π 2 : (+ cc 1))))))

(define (main)
(return (lcc . . . 0 0))))
(a) Program to compute the number
of lines and characters in a string.

(define (main)
(return (lcc . . . 0 ))))
(b) Slice of program in (a) to compute
the number of lines only.

(define (main)
(return (lcc . . .  0))))
(c) Slice of program in (a) to compute
the number of characters only.

Fig. 1. A program in Scheme-like language and its slices. The parts that are sliced away are denoted by .

approach to slicing which can avoid repeated fixpoint computation by reusing some of the information obtained while
slicing the same program earlier with a different criterion.
The example from [15] shown in Figure 1b motivates the need for incremental slicing. It shows a simple program in
a Scheme-like language. It takes a string as input and returns a pair consisting of the number of characters and lines in
the string. Figure 1b shows the program when it is sliced with respect to the first component of the output pair, namely
the number of lines in the string (lc). All references to the count of characters (cc) and the expressions responsible for
computing cc only have been sliced away (denoted ). The same program can also be sliced to produce only the char
count and the resulting program is shown in Figure 1c.
The example illustrates several important aspects for an effective slicing procedure. We need the ability to specify a
rich set of slicing criteria to select different parts of a possibly complex output structure (first and second component of
the output pair in the example, or say, every even element in an output list). Also notice that to compute some part of
an output structure, all prefixes of the structure have to be computed. Thus, slicing criteria have to be prefix-closed.
Finally, it seems likely from the example, that certain parts of the program will be present in any slice, irrespective of
the specific slicing criterion2 . Thus, when multiple slices of the same program are required, a slicing procedure should
strive for efficiency by minimizing re-computations related to the common parts.
In this paper, we consider the problem of incremental slicing for functional programs. We restrict ourselves to tuples
and lists as the only algebraic data types. We represent our slicing criteria as regular grammars that represent sets of
prefix-closed strings of the selectors car and cdr. The slicing criterion represents the part of the output of the program
in which we are interested, and we view it as being a demand on the program. We first present a non-incremental
slicing method, which propagates the demand represented by the slicing criterion into the program. In this our method
resembles the projection function based methods of [8, 15]. However, unlike these methods, we do a context-sensitive
analysis of functions calls. This makes our method precise by avoiding analysis over infeasible interprocedural paths. To
avoid the inefficiency of analyzing a function once for each calling context, we create a compact context-independent
2 the

trivial null slicing criteria where the whole program is sliced away is an exception, but can be treated separately.

Manuscript submitted to ACM

An Incremental Slicing Method for Functional Programs

3

p ∈ Prog ::=d 1 . . . dn e main

— program

d ∈ Fdef ::=(define (f x 1 . . . x n ) e)

— function definition



 (if x e 1 e 2 )

e ∈ Expr ::= (let x ← s in e)

 (return x)


— conditional
— let binding
— return from function


k
nil




(cons
x
x
)
1
2


(cdr x)
s ∈ App ::= (car x)


(null?
x)
(+
x1 x2)


 (f x . . . x )
1
n


— constants
— constructor
— selectors
— tester/generic-arithmetic
— function application

Fig. 2. The syntax of our language

summary for each function. This summary is then used to step over function calls. As we shall see, it is this context
independent summary that also makes the incremental version possible in our approach.
The incremental version, has a one-time pre-computation step in which the program is sliced with respect to a default
criterion that is same for all programs. The result of this step is converted to a set of automata, one for each expression
in the program. This completes the pre-computation step. To decide whether a expression is in the slice for a given
slicing criterion, we simply intersect the slicing criterion with the automaton corresponding to the expression. If the
result is the empty set, the expression can be removed from the slice.
The main contributions of this paper are as follows:
(1) We propose a view of the slicing criterion in terms of a notion called demand (Section 3) and formulate the problem
of slicing as one of propagating the demand on the main expression to all the sub-expressions of the program. The
analysis for this is precise because it keeps the information at the calling context separate. However it attempts
to reduce the attendant inefficiency through the use of function summaries. The difficulty of creating function
summaries in a polyvariant analysis, especially when the domain of analysis is unbounded, has been pointed out in
[15].
(2) Our formulation (Section 4) allows us to derive an incremental version of slicing algorithm that factors out
computations common to all slicing criteria (Section 5) and re-uses these computations. To the best of our
knowledge, the incremental version of slicing in this form has not been attempted before.
(3) We have proven the correctness of the incremental slicing algorithm with respect to the non-incremental version
(Section 5.2).
(4) We have implemented a prototype slicer for a first-order version of Scheme (Section 7). We have also extended the
implementation to higher-order programs (Section 6) by converting such programs to first-order using firstification
techniques [9], slicing the firstified programs using our slicer, and then mapping the sliced program back to
the higher-order version. The implementation demonstrates the expected benefits of incremental slicing: the
incremental step is one to four orders of magnitude faster than the non-incremental version.
2

THE TARGET LANGUAGE—SYNTAX AND SEMANTICS

Figure 2 shows the syntax of our language. For ease of presentation, we restrict the language to Administrative Normal
Form (ANF) [4]. In this form, the arguments to functions can only be variables. To avoid dealing with scope-shadowing,
Manuscript submitted to ACM

4

Prasanna Kumar K., Amitabha Sanyal, and Amey Karkare

Premise

Transition

Rule Name

ρ, H, k
H, k
ρ(x) ∈ N
ρ(y) ∈ N
ρ, H, (+ x y)
H, ρ(x) + ρ(y)
H(ρ(x)) = (v 1 , v 2 )
ρ, H, (car x)
H, v 1
H(ρ(x)) = (v 1 , v 2 )
ρ, H, (cdr x)
H, v 2
` < dom(H) is a fresh location
ρ, H, (cons x y)
H[` 7→ (ρ(x), ρ(y))], `
ρ(x) ∈ N \ {0}
ρ, S, H, (if x e 1 e 2 ) −→ ρ, S, H, e 1
ρ(x) = 0
ρ, S, H, (if x e 1 e 2 ) −→ ρ, S, H, e 2
ρ(x) , nil
ρ, H, (null? x)
H, 0
ρ(x) = nil
ρ, H, (null? x)
H, 1
s is (f y1 . . . yn )
ρ, S, H, (let x ← s in e) −→ [~z 7→ ρ(~
y )], (ρ, x, e) • S, H, e f
f is (define (f z 1 . . . zn ) e f )
0
ρ, H, s
H ,v
ρ, S, H, (let x ← s in e) −→ ρ[x 7→ v], S, H 0, e
s is not (f y1 . . . yn )
ρ, (ρ 0, x 0, e 0 ) • S, H, (return x) −→ ρ 0 [x 0 7→ ρ(x)], S, H, e 0

const
prim
car
cdr
cons
if-true
if-false
null-true
null-false
let-fncall
let-nonfn
return

Fig. 3. The semantics of our language

we assume that all variables in a program are distinct. Neither of these two restrictions affect the expressibility of our
language. In fact, it is a simple matter to transform the pure subset of first order Scheme to our language, and map the
sliced program back to Scheme. To refer to an expression e, we may annotate it with a label π as π :e; however the label
is not part of the language. To keep the description simple, we shall assume that each program has its own unique set
of labels. In other words, a label identifies both the program point and the program that contains it.
A program in our language is a collection of function definitions followed by a main expression denoted as e main .
Applications (denoted by the syntactic category App) consist of functions or operators applied to variables. Expressions
(Expr) are either an if expression, a let expression that evaluates an application and binds the result to a variable, or a
return expression. The return keyword is used to mark the end of a function so as to initiate appropriate semantic
actions during execution. The distinction between expressions and applications will become important while specifying
the semantics of programs.
2.1

Semantics

We now present the operational semantics for our language. This is largely borrowed from [1, 7] and we include it here
for completeness. We start with the domains used by the semantics:
v:

Val

=

N + {nil} + Loc

– Values

ρ:

Env

=

Var → V al

– Environment

H:

Heap

=

Loc → (V al × V al + {empty}) – Heap

A value in our language is either a number, or the empty list denoted by nil, or a location in the heap. The heap
maps each location to a pair of values denoting a cons cell. Heap locations can also be empty. Finally, an environment
is a mapping from variables to values.
The dynamic aspects of the semantics, shown in Figure 3, are specified as a state transition system. The semantics of
applications s are given by the judgement form ρ, H, s
ρ 0, S 0, H 0, e 0 .

H 0, v, and those for expressions e by the form ρ, S, H, e →

Here S is a stack consisting of continuation frames of the form (ρ, x, e). The frame (ρ, x, e) signifies that if

Manuscript submitted to ACM

An Incremental Slicing Method for Functional Programs

5

the current function returns a value v, the next expression to be evaluated is e, and the environment for this evaluation
is ρ updated with the variable x bound to v. The start state is ({}ρ , [ ]S , {}H , e main ), where {}ρ is the empty environment,
[ ]S is the empty stack, and {}H is the empty heap. The program terminates successfully with result value ρ(x) on
reaching the halt state (ρ, [ ]S , H, (return x)). We use the notation ρ[x 7→ v] to denote the environment obtained by
updating ρ with the value for x as v. We also use [~
x 7→ v~ ] to denote an environment in which each x i has the value vi .
3

DEMAND

We now connect slicing with a notion called demand. A demand on an expression represents the set of paths that the
context of the expression may explore of the value of the expression. A demand is represented by a prefix-closed set of
strings over (0 + 1)∗ . Each string in the demand, called an access path, represents a traversal over the heap. 0 stands for
a single-step traversal over the heap by dereferencing the car field of a cons cell. Similarly, 1 denotes the dereferencing
of the cdr field of a cons cell.
As an example, a demand of {ϵ, 1, 10} on the expression (cons x y) means its context may need to visit the car
field of y in the heap (corresponding to the string 10 in the demand). The example also illustrates why demands are
prefix-closed—the car field of y cannot be visited without visiting first the cons cell resulting from the evaluation of
(cons x y) (represented by ϵ) and then the cell corresponding to y (represented by 1). The absence of 0 in the demand
also indicates that x is definitely not visited. Notice that to meet the demand {ϵ, 1, 10} on (cons x y), the access paths
{ϵ, 0} has to be visited starting from y. Thus we can think of (cons x y) as a demand transformer transforming the
demand {ϵ, 1, 10} to the demand {ϵ, 0} on y and the empty demand (represented by ∅) on x.
The slicing problem is now modeled as follows. Viewing the slicing criterion (also a set of strings over (0 + 1)∗ ) as a
demand3 on the main expression e main , we compute the demand on each expression in the program. If the demand on
a expression turns out to be ∅, the expression does not contribute to the demand on e main and can be removed from the
slice. Thus the solution of the slicing problem lies in computing a demand transformer that, given a demand on e main ,
computes a demand environment—a mapping of each expression (represented by its program point π ) to its demand.
We formulate this computation as an analysis called demand analysis.
We use σ to represent demands and α to represent access path. Given two access paths α 1 and α 2 , we use the
juxtaposition α 1 α 2 to denote their concatenation. We extend this notation to a concatenate a pair of demands and even
to the concatenation of a symbol with a demand: σ1 σ2 denotes the demand {α 1 α 2 | α 1 ∈ σ and α 2 ∈ σ2 } and 0σ is a
shorthand for {0α | α ∈ σ }.
3.1

Demand Analysis

Figure 4 shows the analysis. Given an application s and a demand σ , A returns a demand environment that maps
expressions of s to their demands. The third parameter to A, denoted DS, represents context-independent summaries
of the functions in the program, and will be explained shortly.
Consider the rule for the selector car. If the demand σ on (car x) is ∅, then no part of the value of (car x) is visited
and the demand on x is also ∅. However, if σ is non-empty, the context of (car x) has to first dereference the value of x
using the car field and then traverse the paths represented by σ . In this case, the demand on x is the set consisting of ϵ
(start at the root of x) and 0σ (dereference using car and then visit the paths in σ ). On the other hand, the rule for the

3 supplied

by a context that is external to the program
Manuscript submitted to ACM

6

Prasanna Kumar K., Amitabha Sanyal, and Amey Karkare

A(π:κ, σ , DS) = {π 7→ σ }, for constants including nil
A(π:(null? π1:x), σ , DS) = {π 1 7→ if σ , ∅ then {ϵ } else ∅, π 7→ σ }
A(π:(+ π1:x π2:y), σ , DS) = {π 1 7→ if σ , ∅ then {ϵ } else ∅, π 2 7→ if σ , ∅ then {ϵ } else ∅, π 7→ σ }
A(π:: (car π1: x), σ , DS) = {π1 7→ if σ , ∅ then {ϵ } ∪ 0σ else ∅, π 7→ σ }
A(π:: (cdr π1: x), σ , DS) = {π1 7→ if σ , ∅ then {ϵ } ∪ 1σ else ∅, π 7→ σ }
A(π:(cons π1:x π2:y), σ , DS) = {π1 7→ {α | 0α ∈ σ }, π2 7→ {α | 1α ∈ σ }, π 7→ σ }
n
Ø
A(π:(f π1:y1 · · · πn :yn ), σ , DS) =
{πi 7→ DSif (σ )} ∪ {π 7→ σ }
i=1

D(π:(return π1:x), σ , DS) = {π1 7→ σ , π 7→ σ }
D(π:(if π1:x e 1 e 2 ), σ , DS) = D(e 1 , σ , DS) ∪ D(e 2 , σ , DS) ∪ {π1 7→ if σ , ∅ then {ϵ } else ∅, π 7→ σ }
D(π:(let π 1:x ← s in e), σ , DS) = A(s, ∪ DE(π ), DS) ∪ {π 7→ σ }
π ∈Π

where DE = D(e, σ , DS), and Π represents all occurrences of x in e,
∀f , ∀i, ∀σ : D(e f , σ , DS) = DE, DSif =

Ð

π ∈Π

DE(π )

df1 . . . dfk `l DS

(demand-summary)

where (define (f z 1 . . . zn ) e f ) is one of df1 . . . dfk , 1 ≤ i ≤ n, and Π represents all occurrences
of zi in e f
Fig. 4. Demand Analysis

constructor cons works as follows: To traverse the path 0α (alternately 1α) starting from the root of (cons x y), one has
to traverse the path α starting from x (or y).
Since (null? x) only visits the root of x to examine the constructor, a non-null demand on (null? x) translates to the
demand ϵ on x. A similar reasoning also explains the rule for (+ x y). Since, both x and y evaluate to integers in a well
typed program, a non-null demand on (+ x y) translates to the demand ϵ on both x and y.
The rule for a function call uses a third parameter DS that represents the summaries of all functions in the program.
DS is a set of context-independent summaries, one for each (function, parameter) pair in the program. DSif represents

a transformation that describes how any demand σ on a call to f is transformed into the demand on its ith parameter.
DS is specified by the inference rule demand-summary. This rule gives a fixed-point property to be satisfied by DS,
namely, the demand transformation assumed for each function in the program should be the same as the demand
transformation calculated from the body of the function. Given DS, the rule for the function call is obvious. Notice that
the demand environment for each application s also includes the demand on s itself apart from its sub-expressions.
Operationally, the rule demand-summary is converted into a grammar (Section 4) that is parameterized with respect to
a placeholder terminal representing a symbolic demand. The language generated by this grammar is the least solution
satisfying the rule. The least solution corresponds to the most precise slice.
We finally discuss the rules for expressions given by D. The rules for return and if are obvious. The rule for
(let x ← s in e) first uses σ to calculate the demand environment DE of the let-body e. The demand on s is the union of
the demands on all occurrences of x in e. It is easy to see by examining the rules that the analysis results in demands
that are prefix-closed. More formally, let DEσ be the demand environment resulting from the analysis of a program for
a demand σ . Then, for an expression π:e in the program, DEσ (π ) is prefix closed.
Manuscript submitted to ACM

An Incremental Slicing Method for Functional Programs
4

7

COMPUTING CONTEXT-INDEPENDENT FUNCTION SUMMARIES

A slicing method used for, say, debugging needs to be as precise as possible to avoid false errors. We therefore choose
to analyze each function call separately with respect to its calling context. We now show how to obtain a contextindependent summary for each function definition from the rule demand-summary. Recall that this summary is a
function that transforms any demand on the result of a call to demands on the arguments. A convenient way of doing
this is to express how a symbolic demand is transformed by the body of a function. Summarizing the function in this
way has two benefits. It helps us to propagate a demand across several calls to a function without analyzing its body
each time. Even more importantly, it is the key to our incremental slicing method.
However, notice that the rules of demand analysis requires us to do operations that cannot be done on a symbolic
demand. The cons rule, for example is defined in terms of the set {α | 0α ∈ σ }. Clearly this requires us to know
the strings in σ . Similarly, the if rule requires to know whether σ is ∅. The way out is to treat these operations also
symbolically. For this we introduce three new symbols 0̄, 1̄ and 2, to capture the intended operations. If 0 represents
selection using car, 0̄ is intended to represent a use as the left argument of cons. Thus 0̄0 should reduce to the empty
string ϵ. Similarly 2 represents the symbolic transformation of any non-null demand to ϵ and null demand to itself.
These transformation are defined and also made deterministic through the simplification function S.
S({ϵ }) = {ϵ }
S(0σ ) = 0S(σ )
S(1σ ) = 1S(σ )
S(0̄σ ) = {α | 0α ∈ S(σ )}
S(1̄σ ) = {α | 1α ∈ S(σ )}
(
∅
if S(σ ) = ∅
S(2σ ) =
{ϵ } otherwise
S(σ1 ∪ σ2 ) = S(σ1 ) ∪ S(σ2 )
Notice that 0̄ strips the leading 0 from the string following it, as required by the rule for cons. Similarly, 2 examines the
string following it and replaces it by ∅ or {ϵ }; this is required by several rules. The A rules for cons and car in terms of
the new symbols are:
A(π: (cons π 1:x π2:y), σ , DS) = {π1 7→ 0̄σ , π2 7→ 1̄σ , π 7→ σ }
A(π: (car π1:x), σ , DS) = {π1 7→ 2σ ∪ 0σ , π 7→ σ }
and the D rule for if is:
D(π: (if π1:x e 1 e 2 ), σ , DS) = D(e 1 , σ , DS) ∪ D(e 2 , σ , DS) ∪
{π1 7→ if σ , ∅ then {ϵ } else ∅,
π 7→ σ }
The rules for cdr, + and null? are also modified similarly. Now the demand summaries can be obtained symbolically
with the new symbols as markers indicating the operations that should be performed string following it. When the final

Manuscript submitted to ACM

8

Prasanna Kumar K., Amitabha Sanyal, and Amey Karkare

demand environments are obtained with the given slicing criterion acting a concrete demand for the main expression
e main , the symbols 0̄, 1̄ and 2 are eliminated using the simplification function S.

4.1

Finding closed-forms for the summaries DS

Recall that DSif is a function that describes how the demand on a call to f translates to its ith argument. A straightfor-

ward translation of the demand-summary rule to obtain DSif is as follows: For a symbolic demand σ compute the the
demand environment in e f , the body of f . From this calculate the demand on the ith argument of f , say x. This is

the union of demands of all occurrences of x in the body of f . The demand on the ith argument is equated to DSif (σ ).
Since the body may contain other calls, the demand analysis within e f makes use of DS in turn. Thus our equations

may be recursive. On the whole, DS corresponds to a set of equations, one for each argument of each function. The
reader can verify that DS2lcc (σ ) in our running example is:
DS2lcc (σ )

=

0̄σ ∪ 2DS2lcc (σ )

As noted in [15], the main difficulty in obtaining a convenient function summary is to find a closed-form description
of DS2lcc (σ ) instead of the recursive specification. Our solution to the problem lies in the following observation: Since

we know that the demand rules always prefix symbols to the argument demand σ , we can write DSif (σ ) as DSif σ ,
where DSif is a set of strings over the alphabet {0, 1, 0̄, 1̄, 2}. The modified equations after doing this substitution will be,
DS2lcc σ

=

0̄σ ∪ 2DS2lcc σ

Thus, we have,

4.2

DS2lcc (σ )

=

DS2lcc σ

where DS2lcc

=

{0̄} ∪ 2DS2lcc

Computing the demand environment for the function bodies

The demand environment for a function body e f is calculated with respect to a concrete demand. To start with, we
consider the main expression e main as being the body of a function main, The demand on e main is the given slicing
criterion. Further, the concrete demand on a function f , denoted σf , is the union of the demands at all call-sites of
f . The demand environment of a function body e f is calculated using σf . If there is a call to д inside e f , the demand
summary DSд is used to propagate the demand across the call. Continuing with our example, the union of the demands
on the three calls to lcc is the slicing criterion. Therefore the demand on the expression at program point π 1 is given by
Dπ 1

=

DS2lcc

=

σlcc

=

DS2lcc σlcc
{0̄} ∪ 2DS2lcc

(1)

slicing criterion

At the end of this step, we shall have (i) A set of equations defining the demand summaries DSif for each argument of

each function, (ii) Equations specifying the demand Dπ at each program point π , and (iii) an equation for each concrete
demand σf on the body of each function f .
Manuscript submitted to ACM

An Incremental Slicing Method for Functional Programs
4.3

9

Converting analysis equations to grammars

Notice that the equations for DS2lcc are still recursive. However, Equation 1 can also be viewed as a grammar with

{0, 1, 1̄, 0̄, 2} as terminal symbols and DS2lcc , Dπ1 and σlcc as non-terminals. Thus finding the solution to the set of
equations generated by the demand analysis reduces to finding the language generated by the corresponding grammar.
The original equations can now be re-written as grammar rules as shown below:
Dπ1 → DS2lcc σlcc
DS2lcc → 0̄ | 2 DS2lcc

(2)

σlcc → slicing criteria
Thus the question whether the expression at π1 can be sliced for the slicing criterion σlcc is equivalent to asking whether
the language S(L(Dπ1 )) is empty. In fact, the simplification process S itself can be captured by adding the following set
of five unrestricted productions named unrestricted and adding the production Dπ0 1 → Dπ1 $ to the grammar generated
earlier.
0̄0 → ϵ

1̄1 → ϵ

2$ → ϵ

20 → 2

21 → 2
The set of five unrestricted productions shown are independent of the program being sliced and the slicing criterion.
The symbol $ marks the end of a sentence and is required to capture the 2 rule correctly.
We now generalize: Assume that π is the program point associated with an expression e. Given a slicing criterion σ ,
let G πσ denote the grammar (N , T , P πσ ∪ unrestricted ∪ {Dπ0 → Dπ $}, Dπ0 ). Here T is the set of terminals {0, 1, 0̄, 1̄, 2, $},

P πσ is the set of context-free productions defining Dπ , the demand on e (as illustrated by example 2). N contains the
non-terminals of P πσ and additionally includes the special non-terminal Dπ0 . As mentioned earlier, given a slicing
criterion σ , the question of whether the expression e can be sliced out of the containing program is equivalent to asking
whether the language L(G πσ ) is empty. We shall now show that this problem is undecidable.
Theorem 4.1. Given a program point π and slicing criterion σ , the problem whether L(G πσ ) is empty is undecidable.
Proof Outline. Recollect that the set of demands on an expression, as obtained by our analysis, is prefix closed. Since

the grammar always includes production {Dπ0 → Dπ $}, L(G πσ ) is non-empty if and only if it contains $ (i.e. empty
string followed by the $ symbol). We therefore have to show that the equivalent problem of whether $ belongs to L(G πσ )
is undecidable.
Given a Turing machine and a string α ∈ (0+1)∗ , the proof involves construction of a grammar G = (N ∪{S, S 0 },T , P ∪
unrestricted ∪ {S 0 → S$}, S 0 ) with the property that the Turing machine halts on α if and only if G accepts $. Notice
that P is a set of context-free productions over the terminal set T and may not necessarily be obtainable from demand
analysis of a program. However, G can be used to construct a program whose demand analysis results in a grammar G 0
that can used instead of G to replay the earlier proof. The details can be found in Lemmas B.2 and B.3 of [7].
We get around the problem of undecidability, we use the technique of Mohri-Nederhoff [10] to over-approximate P πσ

by a strongly regular grammar. The NFA corresponding to this automaton is denoted as M πσ . The simplification rules
can be applied on M πσ without any loss of precision. The details of the simplification process are in [6].

Manuscript submitted to ACM

10

Prasanna Kumar K., Amitabha Sanyal, and Amey Karkare
ǫ
0̄

0̄

0

2

0

2

(a)
0̄

1

2

1
2

(b)
0̄

0

2

(c)
Fig. 5. (a) & (b) show the simplification of the automaton M πσ1 for the slicing criteria σ = {ϵ, 0} and σ = {ϵ, 1} respectively. (c)
shows the canonical automaton A π1 and the corresponding completing automaton Aπ1

For our running example, the grammar after demand analysis is already regular, and thus remains unchanged
by Mohri-Nederhoff transformation. The automata in Figures 5(a) and 5(b) correspond to the two slicing criteria
σ

σlcc = {ϵ, 0} and σlcc = {ϵ, 1} and illustrate the simplification of corresponding Mohri-Nederhoff automata M π1lcc . It
can be seen that, when the slicing criterion is {ϵ, 1}, the language of Dπ1 is empty and hence e can be sliced away. A
drawback of the method outlined above is that with a change in the slicing criterion, the entire process of grammar
generation, Mohri-Nederhoff approximation and simplification has to be repeated. This is likely to be inefficient for
large programs.
5

INCREMENTAL SLICING

We now present an incremental algorithm which avoids the repetition of computation when the same program is sliced
with different criteria. This can be done by pre-computing the part of the slice computation that is independent of the
slicing criterion. The pre-computed part can then be used efficiently to slice the program for a given slicing criterion.
In general, the pre-computation consists of three steps: (i) computing the demand at each expression π : e for the
{ϵ }

fixed slicing criterion {ϵ } and applying the Mohri-Nederhoff procedure to yield the automaton M π , (ii) a step called
canonicalization which applies the simplification rules

{ϵ }
on M π

until the 0̄ and 1̄ symbols in the strings accepted by the

resulting automaton are only at the end, and, from this (iii) constructing an automaton called the completing automaton.
For the running example, the canonicalized and the completing automata are shown Figures 5(c). We explain these
steps now.
{ϵ }

As stated earlier, the automaton M π1 , after some simplifications, gives the first automaton (the canonicalized
automaton) shown in Figure 5(c), which we shall denote Aπ1 . It is clear that if Aπ1 is concatenated with a slicing
criterion that starts with the symbol 0, the result, after simplification, will be non-empty. We call a string that starts
with 0 as a completing string for Aπ1 . In this case, detecting a completing string was easy because all strings accepted
by Aπ1 end with 0̄. Now consider the second automaton in Figure 5(c), called the completing automaton, that recognizes
Manuscript submitted to ACM

An Incremental Slicing Method for Functional Programs

11

the language 0(0 + 1)∗ . This automaton recognizes all completing strings for Aπ1 and nothing else. Thus for an arbitrary
slicing criterion σ , it suffices to intersect σ with the completing automaton to decide whether the expression at π1 will
be in the slice. In fact, it is enough for the completing automaton to recognize just the language {0} instead of 0(0 + 1)∗ .
The reason is that any slicing criterion, say σ , is prefix closed, and therefore σ ∩ {0} is empty if and only if σ ∩ 0(0 + 1)∗
is empty. Our incremental algorithm generalizes this reasoning.
5.1

Completing Automaton and Slicing

For constructing the completing automaton for an expression e, we saw that it would be convenient to simplify the
{ϵ }

automaton Me

to an extent that all accepted strings, after simplification, have 0̄ and 1̄ symbols only at the end. We

now give a set of rules, denoted by C, that captures this simplification.
C({ϵ }) = {ϵ }
C(0σ ) = 0C(σ )
C(1σ ) = 1C(σ )
C(0̄σ ) = {0̄ | {ϵ } = C(σ )} ∪ {α | 0α ∈ C(σ )}
∪ {0̄1̄α | 1̄α ∈ C(σ )} ∪ {0̄0̄α | 0̄α ∈ C(σ )}
C(1̄σ ) = {1̄ | {ϵ } = C(σ )} ∪ {α | 1α ∈ C(σ )}
∪ {1̄1̄α | 1̄α ∈ C(σ )} ∪ {1̄0̄α | 0̄α ∈ C(σ )}
C(2σ ) = 2C(σ )
C(σ1 ∪ σ2 ) = C(σ1 ) ∪ C(σ2 )
C differs from S in that it accumulates continuous run of 0̄ and 1̄ at the end of a string. Notice that C, like S, simplifies
its input string from the right. Here is an example of C simplification:
C

C

120̄00201̄1̄10̄ → 120̄00201̄0̄ → 120201̄0̄
In contrast the simplification of the same string using S gives:
S

S

S

S

120̄00201̄1̄10̄ → 120̄00201̄1̄1∅ → 120̄00201̄0̄∅ → . . . → ∅
C satisfies two important properties:
Property 1. The result of C always has the form (0 + 1 + 2)∗ (0̄ + 1̄)∗ . Further, if σ ⊆ (0 + 1 + 2)∗ , then C(σ ) = σ .
Property 2. S subsumes C, i.e., S(C(σ1 )C(σ2 )) = S(σ1 σ2 ).
Note that while we have defined canonicalization over a language, the actual canonicalization takes place over
an automaton—specifically the automaton M π obtained after the Mohri-Nederhoff transformation. The function
createCompletingAutomaton in Algorithm 1 takes Aπ , the canonicalized Mohri-Nederhoff automaton for the slicing
criterion {ϵ }, as input, and constructs the completing automaton, denoted as Aπ .
Recollect that the strings recognized by Aπ are of the form (0 + 1 + 2)∗ (0̄ + 1̄)∗ . The algorithm first computes the set
of states reachable from the start state using only edges with labels {0, 1, 2}. This set is called the frontier set. It then
complements the automaton and drops all edges with {0, 1, 2} labels. Finally, all states in the frontier set are marked as
Manuscript submitted to ACM

12

Prasanna Kumar K., Amitabha Sanyal, and Amey Karkare

Function createCompletingAutomaton(A)
Data: The Canonicalized Automaton A = hQ, {0, 1, 0̄, 1̄, 2}, δ, q 0 , F i
Result: A, the completing automaton for A
F 0 ← {q fr | q fr ∈ Q, hasBarFreeTransition(q 0 , q fr , δ )}
/* ........Reverse the ‘‘bar’’ transitions: directions as well as labels ........
foreach (transition δ (q, 0̄) → q 0 ) do
add transition δ 0 (q 0, 0) → q
foreach (transition δ (q, 1̄) → q 0 ) do
add transition δ 0 (q 0, 1) → q
0
q 0 ← new state /* ................... start state of A ...................
foreach (state q ∈ F ) do
add transition δ 0 (q 00 , ϵ) → q
return Q ∪ {q 00 }, {0, 1}, δ 0, q 00 , F 0
Function inSlice(e, σ )
Data: expression e, slicing criteria σ
Result: Decides whether e should be retained in slice
return (L(Ae ) ∩ σ , ∅)

*/

*/

Algorithm 1: Functions to create the completing automaton and the slicing function.

final states. Since Aπ is independent of the slicing criteria, the completing automaton is also independent of the slicing
criteria and needs to be computed only once. It can be stored and re-used whenever the program needs to be sliced. To
decide whether π: e can be sliced out, the function inSlice described in Algorithm 1 just checks if the intersection of
the slicing criteria with L(Aπ ) is null.
5.2

Correctness of Incremental Slicing

We now show that the incremental algorithm to compute incremental slices is correct. Recall that we use the following
notations: (i) G πσ is the grammar generated by demand analysis (Figure 4) for an expression π : e in the program
{ϵ }
of interest, when the slicing criteria is σ , (ii) Aπ is the automaton corresponding to G π after Mohri-Nederhoff
transformation and canonicalization, and (iii) Aπ is the completing automaton for e. We first show that the result of the
demand analysis for an arbitrary slicing criterion σ can be decomposed as the concatenation of the demand analysis
obtained for the fixed slicing criterion {ϵ } and σ itself.
Lemma 5.1. For all expressions e and slicing criteria σ , L(G πσ ) = L(G π )σ .
{ϵ }

Proof. The proof is by induction on the structure of e. Observe that all the rules of the demand analysis (Figure 4)
add symbols only as prefixes to the incoming demand. Hence, the slicing criteria will always appear as a suffix of any
string that is produced by the grammar. Thus, any grammar L(G πσ ) can be decomposed as σ 0σ for some language σ 0 .
{ϵ }

Substituting {ϵ } for σ , we get G π

= σ 0 . Thus L(G πσ ) = L(G π )σ .
{ϵ }



Given a string s over (0̄ + 1̄)∗ , we use the notation s to stand for the reverse of s in which all occurrences of 0̄ are
replaced by 0 and 1̄ replaced by 1. Clearly, S({ss}) = {ϵ }.
We next prove the completeness and minimality of Aπ .
{s }

Lemma 5.2. {s | S(L(M π )) , ∅} = L(Aπ )(0 + 1)∗
Manuscript submitted to ACM

An Incremental Slicing Method for Functional Programs

13
{s }

{ϵ }

Proof. We first prove LHS ⊆ RHS. Let the string s ∈ S(L(M π )). Then by Lemma 5.1, s ∈ S(L(M π ){s}). By
{ϵ }
S(C(L(M π )){s}).

{ϵ }
Property 2, this also means that s ∈
Since strings in C(L(M π )) are of the form (0 + 1 + 2)∗ (0̄ + 1̄))∗
(Property 1), this means that there is a string p1p2 such that p1 ∈ (0 + 1 + 2)∗ and p2 ∈ (0̄ + 1̄)∗ , and S({p2 }{s}) ⊆ (0 + 1)∗ .

Thus s can be split into two strings s 1 and s 2 , such that S({p2 }{s 1 }) = {ϵ }. Therefore s 1 = p2 . From the construction of
Aπ we have p2 ∈ L(Aπ ) and s 2 ∈ (0 + 1)∗ . Thus, s ∈ L(Aπ )(0 + 1)∗ .
Conversely, for the proof of RHS ⊆ LHS, we assume that a string s ∈ L(Aπ )(0 + 1)∗ . From the construction of

Aπ we have strings p1 , p2 , s 0 such that p1p2 ∈ C(L(M πϵ )), p1 ∈ (0 + 1 + 2)∗ , p2 ∈ (0̄ + 1̄)∗ , s is p2s 0 and s 0 ∈ (0 + 1)∗ .
{s }
{ϵ }
{ϵ }
{s }
Thus, S(L(M π )) = S(L(M π {s})) = S(C(L(M π )){s}) = S({p1p2p2s 0 }) = {p1s 0 }. Thus, S(L(M π )) is non-empty
and s ∈ LHS.



We now prove our main result: Our slicing algorithm represented by inSlice (Algorithm 1) returns true if and only
if S(L(Aϵπ )σ ) is non-empty.
Theorem 5.3. S(L(M πσ )) , ∅ ↔ inSlice(e, σ )
Proof. We first prove the forward implication. Let s ∈ S(L(M πσ )). From Lemma 5.1, s ∈ S(L(M πϵ )σ ). From
Property 2, s ∈ S(C(L(M πϵ ))σ ). Thus, there are strings p1 , p2 such that p1 ∈ C(L(M πϵ )), p2 ∈ σ , s = S({p1p2 }). Further
p1 in turn can be decomposed as p3p4 such that p3 ∈ (0 + 1 + 2)∗ and p4 ∈ (0̄ + 1̄)∗ . We also have S({p4p2 }) ⊆ (0 + 1)∗ .
Thus p4 is a prefix of p2 .
From the construction of Aπ , we know p4 ∈ L(Aπ ). Further, p4 is a prefix of p2 and p2 ∈ σ , from the prefix closed
property of σ we have p4 ∈ σ . This implies Aπ ∩ σ , ∅ and thus inSlice(e, σ ) returns true.
Conversely, if inSlice(e, σ ) is true, then ∃s : s ∈ L(Aπ ) ∩ σ . In particular, s ∈ L(Aπ ). Thus, from Lemma 5.2 we have

S(L(M π )) , ∅. Further, since s ∈ σ we have S(L(M πσ )) , ∅.
{s }

6



EXTENSION TO HIGHER ORDER FUNCTIONS

We now describe how our method can also be used to slice higher order programs. This section has been included
mainly for completeness, and we do not make claims of novelty. We handle all forms of higher-order functions except
the cases of functions being returned as a result, and functions being stored in data structures—in our case lists. Even
with these limitations, one can write a number of useful and interesting higher-order programs in our language.
Consider the program in Figure 6(a). It contains a higher order function hof which applies its first argument f on its
second argument l. The function main creates a list lst1 and a function value g (through partial application) and uses
these in the two calls to hof. Finally, main returns the result of these calls in a pair. The program exhibits higher order
functions that take as actual arguments both manifest functions and partial applications.
For our first-order method to work on higher order functions, we borrow from a technique called firstification [9, 16].
Firstification transforms a higher-order program to a first-order program without altering its semantics. Our version of
firstification repeatedly (i) finds for each higher-order function the bindings of each of its functional parameters, (ii)
replaces the function by a specialized version for each of the bindings, and (iii) replaces each application of f by its
specialized version. These steps are repeated till we we are left with a program containing first order functions only.
In the example being considered, we first discover that f in foldr has a single binding to fun and the f of hof has
a binding to car. Specialization gives the functions foldr fun and hof car. We now see that f of hof has a second
binding to the partial application (foldr fun), This gives rise to a second specialization of hof called hof g.
Manuscript submitted to ACM

14

Prasanna Kumar K., Amitabha Sanyal, and Amey Karkare
(define (hof g l)
(return π f :(foldr fun 0 l)))

(define (hof f l)
(return π :(f l)))

(define (hof f l)
(return π :(f l)))

(define (hof car l)
(return πc :(car l)))
(define (foldr f id l)
(if(null? l)) (return id)
(return (f (car l)
(foldr f id (cdr l)))))

(define (foldr fun id l)
(if(null? l)) (return id)
(return (fun (car l)
(foldr fun id (cdr l)))))

(define (fun x y)
(return (+ y 1)))

(define (fun x y)
(return (+ y 1)))

(define (main)
(let lst1 ← (cons a (cons b nil)) in
(let g ← (foldr fun 0) in
(return (cons (hof car lst1)
(hof g lst1)))))

(define (main)
(let lst1 ← (cons a (cons b nil)) in
(let g ← (foldr fun 0) in
(return (cons (hof car lst1)
(hof g lst1))))))

(a) A program with higher order functions

(b) Program in (a) after specialization.

(define (main)
(let lst1 ← (cons a ) in
(let g ← ) in
(return (cons (hof car lst1)
))))
(c) Slice of the program in (a) with
slicing criterion {ϵ, 0}.

Fig. 6. An example higher order program

The program after firstification is shown in Figure 6(b). This program is subjected to demand analysis and the results
are reflected back into the higher-order program. Inside a higher order function that has been specialized, the demand
on an expression is an union of the demands on the specialized versions of the expression. Thus, the demand on π
is given by the union of the demands on πc and π f . Where the higher order function is applied, the demand on its
arguments is derived from the demand transformer of its specialized version. As an example, the demand on lst1 in
(hof car lst1) is obtained from the demand transformers of hof car. For the slicing criterion {ϵ, 0}, the the demand
on the second argument of (cons (hof car lst1) (hof g lst1)) is null and thus this argument and the binding of
g can both be sliced away. The slice for {ϵ, 0} is shown in Figure 6(c).
Note that our simple firstifier requires us to statically find all bindings of a functional parameter. This is not possible
if we allow functions to be returned as results or store functions in data-structures. As an example we can consider
a function f , that, depending on a calculated value n, returns a function д iterated n times (i.e. д ◦ д ◦ n .times
. . ◦ д). A
higher-order function receiving this value as a parameter would be cannot be specialized using the techniques described,
for example, in [9]. A similar thing can happen if we allow functions in lists.
7

EXPERIMENTS AND RESULTS

In this section, we present the results from our experiments on the implementations of both versions of slicing. In the
absence of the details of implementations of other slicing methods, we have compared the incremental step of our
method with the non-incremental version. Our experiments show that the incremental slicing algorithm gives benefits
even when the overhead of creating the completing automata is amortized over even a few slicing criteria.
Our benchmarks consists of first order programs derived from the nofib suite [11]. The higher order programs have
been handcrafted to bring out the issues related to higher order slicing. The program named parser includes most of
the higher order parser combinators required for parsing. fold corresponds to the example in Figure 6. Table 1 shows
Manuscript submitted to ACM

An Incremental Slicing Method for Functional Programs

15

Table 1. Statistics for incremental and non-incremental slicing

Program

treejoin
deriv
paraffins
nqueens
minmaxpos
nperm
linecharcount
studentinfo
knightstour
takl
lambda
parser
maptail
fold

Precomput
ation

6900.0
399.6
3252.8
395.4
27.9
943.1
11.7
1120.6
2926.5
71.6
4012.9
60088.2
22.1
21.4

#exprs
Slicing with {ϵ }
Slicing with {ϵ, 0}
in pro- NonInc
#expr NonInc
#expr
gram
inc
time
in slice inc
time
in slice
time
(ms)
time
(ms)
(ms)
(ms)
First-order Programs
581 6163.2
2.4
536
5577.2
2.8
538
389
268.0
1.6
241
311.2
1.6
249
1152 2287.3
5.2
1067
2529.2
5.1
1067
350
309.9
1.5
350
324.6
1.5
350
182
18.1
0.9
147
19.5
0.8
149
590
627.4
2.1
206
698.4
11.2
381
91
7.0
0.5
69
7.5
0.5
78
305
858.2
1.2
96
854.6
1.3
101
630 2188.1
2.8
436
2580.6
12.2
436
151
46.1
0.7
99
49.5
0.8
105
721 3089.0
2.7
26
3377.4
13.2
705
Higher-order Programs
820 46066.8
2.3
203 45599.0
2.3
209
96
5.5
0.5
51
15.4
0.6
67
114
13.3
0.4
17
14.4
0.5
76

Slicing with {ϵ, 1}
NonInc
#expr
inc
time
in slice
time
(ms)
(ms)
5861.4
333.2
2658.7
328.1
20.5
664.0
7.4
1043.3
2492.8
48.5
2719.8

4.6
2.3
5.1
1.6
0.9
11.8
0.5
7.5
7.4
0.7
5.3

538
266
1067
350
149
242
82
98
436
99
33

61929.2
17.4
16.9

4.1
0.6
0.6

209
56
33

the time required for slicing with different slicing criteria. For each benchmark, we first show, the pre-computation
time, i.e. the time required to construct the completing automata. We then consider three different slicing criteria, and
for each slicing criterion, present the times for non-incremental slicing and the incremental step. The results in Table 1
show that for all benchmarks, the time required to compute the completing automata is comparable to the time taken
for computing the slice non-incrementally. Since computing completing automata is a one time activity, incremental
slicing is very efficient even when a program is sliced only twice. As seen in Table 1, the time taken for the incremental
step is orders of magnitude faster than non-incremental slicing, thus confirming the benefits of reusing the completing
automata.
We also show the number of expressions in the original program and in the slice produced to demonstrate the
effectiveness of the slicing process itself. Here are some of the interesting cases. It can be seen that the slice for nqueens
for any slicing criterion includes the entire program. This is because finding out whether a solution exists for nqueens
requires the entire program to be executed. On the other hand, the program lambda is a λ-expression evaluator that
returns a tuple consisting of an atomic value and a list. The criterion {ϵ, 0} requires majority of the expressions in the
program to be present in the slice to compute the atomic value. On the other hand, the criterion {ϵ } or {ϵ, 1} do not
require any value to be computed and expressions which compute the constructor only are kept in the slice, hence our
algorithm is able to discard most of the expressions. This behavior can be clearly seen in the higher-order example
fold where a slicing criterion {ϵ, 0} selects an expression which only uses the first element of lst1, thus allowing our
slicing algorithm to discard most of the expressions that construct lst1. After examining the nature of the benchmark
programs, the slicing criteria and the slices, we conclude that slicing is most effective when the slicing criterion selects
parts of a bounded structure, such as a tuple, and the components of the tuple are produced by parts of the program
that are largely disjoint.
Manuscript submitted to ACM

16
8

Prasanna Kumar K., Amitabha Sanyal, and Amey Karkare
RELATED WORK

Program slicing has been an active area of research. However, most of the efforts in slicing have been for imperative
programs. The surveys [2, 19, 22] give good overviews of the variants of the slicing problem and their solution techniques.
The discussion in this section will be centered mainly around static and backward slicing of functional programs.
In the context of imperative programs, a slicing criterion is a pair consisting of a program point, and a set of
variables. The slicing problem is to determine those parts of the program that decide the values of the variables at
the program point [23]. A natural solution to the slicing problem is through the use of data and control dependences
between statements. Thus the program to be sliced is transformed into a graph called the program dependence graph
(PDG) [5, 13], in which nodes represent individual statements and edges represent dependences between them. The slice
consists of the nodes in the PDG that are reachable through a backward traversal starting from the node representing
the slicing criterion. Horwitz, Reps and Binkley [5] extend PDGs to handle interprocedural slicing. They show that a
naive extension could lead to imprecision in the computed slice due to the incorrect tracking of the calling context.
Their solution is to construct a context-independent summary of each function through a linkage grammar, and then
use this summary to step across function calls. The resulting graph is called a system dependence graph (SDG). Our
method generalizes SDGs to additionally keep track of the construction of algebraic data types (cons), selection of
components of data types (car and cdr) and their interaction, which may span across functions.
Silva, Tamarit and Tomás [20] adapt SDGs for functional languages, in particular Erlang. The adaptation is straightforward except that they handle dependences that arise out of pattern matching. Because of the use of SDGs, they can
manage calling contexts precisely. However, as pointed out by the authors themselves, when given the Erlang program:
{main() -> x = {1,2}, {y,z} = x, y}, their method produces the imprecise slice {main() -> x = {1,2}, {y,} = x, y} when
sliced on the variable y. Notice that the slice retains the constant 2, and this is because of inadequate handling of the
interaction between cons and cdr. For the equivalent program (let x← (cons 1 2) in (let y ← (car x) in y)) with the
slicing criterion ϵ, our method would correctly compute the demand on the constant 2 as 1̄(ϵ ∪ 0). This simplifies to the
demand ∅, and 2 would thus not be in the slice. Another issue is that while the paper mentions the need to handle
higher order functions, it does not provide details regarding how this is actually done. This would have been interesting
considering that the language considered allows lambda expressions.
The slicing technique that is closest to ours is due to Reps and Turnidge [15]. They use projection functions,
represented as certain kinds of tree grammars, as slicing criteria. This is the same as our use of prefix-closed regular
expressions. Given a program P and a projection function ψ , their goal is to produce a program which behaves like
ψ ◦ P. The analysis consists of propagating the projection function backwards to all subexpressions of the program.
After propagation, any expression with the projection function ⊥ (corresponding to our ∅ demand), are sliced out of the
program. Liu and Stoller [8] also use a method that is very similar to [15], but more extensive in scope.
These techniques differ from ours in two respects. These methods, unlike ours, do not derive context-independent
summaries of functions. This results in a loss of information due to merging of contexts and affects the precision of the
slice. Moreover, the computation of function summaries using symbolic demands enables the incremental version of
our slicing method. Consider, as an example, the program fragment π : (cons π 1 : x π2 :y) representing the body of a
function. Demand analysis with the symbolic demand σ gives the demand environment {π 7→ σ , π1 7→ 0̄σ , π2 7→ 1̄σ }.
Notice that the demands π1 and π 2 are in terms of the symbols 0̄ and 1̄. This is a result of our decision to work with
symbolic demands, and, as a consequence, also handle the constructor-selector interaction symbolically. If we now
slice with the default criterion ϵ and then canonicalize (instead of simplify), we are left with the demand environment
Manuscript submitted to ACM

An Incremental Slicing Method for Functional Programs

17

(define (mapsq l)
(if(null? l) (return l)
(return (cons (sq (car l))
(mapsq (cdr l)))))
Fig. 7. Example to illustrate the imprecision due to Mohri-Nederhoff approximation

{π 7→ ϵ, π1 7→ 0̄, π 2 7→ 1̄}. Notice that there is enough information in the demand environment to deduce, through the
construction of the completing automaton, that π 1 (π2 ) will be in the slice only if the slicing criterion includes 0(1).
Since the methods in [15] and [8] deal with demands in their concrete forms, it is difficult to see the incremental version
being replayed with their methods.
There are other less related approaches to slicing. A graph based approach has also been used by Rodrigues and
Barbosa [17] for component identification in Haskell programs. Given the intended use, the nodes of the graph
represents coarser structures such as modules, functions and data type definitions, and the edges represents relations
such as containment (e.g. a module containing a function definition). On a completely different note, Rodrigues and
Barbosa [18] use program calculation in the Bird-Meerteens formalism for obtaining a slice. Given a program P and a
projection function ψ , they calculate a program which is equivalent to ψ ◦ P. However the method is not automated.
Finally, dynamic slicing techniques have been explored for functional programs by Perera et al. [14], Ochoa et al. [12]
and Biswas [3].

9

CONCLUSIONS AND FUTURE WORK

We have presented a demand-based algorithm for incremental slicing of functional programs. The slicing criterion is a
prefix-closed regular language and represents parts of the output of the program that may be of interest to a user of our
slicing method. We view the slicing criterion as a demand, and the non-incremental version of the slicer does a demand
analysis to propagate this demand through the program. The slice consists of parts of the program with non-empty
demands after the propagation. A key idea in this analysis is the use of symbolic demands in demand analysis. Apart
form better handling of calling contexts that improves the precision of the analysis, this also helps in building the
incremental version.
The incremental version builds on the non-incremental version. A per program pre-computation step slices the
program with the default criterion ϵ. This step factors out the computation that is common to slicing with any criterion.
The result, reduced to a canonical form, can now be used to find the slice for a given criterion with minimal computation.
We have proven the correctness of the incremental algorithm with respect to the non-incremental version. And finally,
we have extended our approach to higher-order programs through firstification. Experiments with our implementation
confirm the benefits of incremental slicing.
There are however two areas of concern, one related to efficiency and the other to precision. To be useful, the slicer
should be able to slice large programs quickly. While our incremental slicer is fast enough, the pre-computation step is
slow, primarily because of the canonicalization step. In addition, the firstification process may create a large number of
specialized first-order programs. As an example, our experiments with functional parsers show that the higher-order
parser combinators such as or-parser and the and-parser are called often, and the arguments to these calls are in turns
calls to higher order functions, for instance the Kleene closure and the positive closure parsers.
Manuscript submitted to ACM

18

Prasanna Kumar K., Amitabha Sanyal, and Amey Karkare

The other concern is that while our polyvariant approach through computation of function summaries improves
precision, the resulting analysis leads to an undecidable problem. The workaround involves an approximation that
could lead to imprecision. As an example, consider the function mapsq shown in Figure 7. The reader can verify
that the function summary for mapsq would be given as: DS1mapsq (σ ) = DS1mapsq σ , where DS1mapsq is the language

ϵ | 1n 1̄n | 1n 020̄1̄n , for n ≥ 0. Now, given a slicing criterion σ = {ϵ, 1, 11, 110} standing for the path to the third
element of a list, it is easy to see that DS1mapsq (σ ) after simplification would give back σ itself, and this is the most

precise slice. However, due to Mohri-Nederhoff approximation DS1mapsq would be approximated by ϵ | 1n 1̄m | 1k 020̄1̄l ,
n, m, k, l ≥ 0. In this case, DS1mapsq would be (0 + 1)∗ , keeping all the elements of the input list l in the slice.
REFERENCES
[1] Rahul Asati, Amitabha Sanyal, Amey Karkare, and Alan Mycroft. Liveness-Based Garbage Collection. In Compiler Construction - 23rd International
Conference, CC 2014.
[2] David Binkley and Mark Harman. 2004. A survey of empirical results on program slicing. Advances in Computers 62 (2004).
[3] Sandip Kumar Biswas. 1997. Dynamic Slicing in Higher-order Programming Languages. Ph.D. Dissertation. University of Pennsylvania, Philadelphia,
PA, USA.
[4] Manuel M. T. Chakravarty, Gabriele Keller, and Patryk Zadarnowski. 2003. A Functional Perspective on SSA Optimisation Algorithms. In COCV,
2003.
[5] Susan Horwitz, Thomas W. Reps, and David Binkley. Interprocedural Slicing Using Dependence Graphs. In Proceedings of the ACM SIGPLAN’88
Conference on Programming Language Design and Implementation (PLDI) 1988.
[6] Amey Karkare, Uday Khedker, and Amitabha Sanyal. 2007. Liveness of Heap Data for Functional Programs. In Heap Analysis and Verification, HAV
2007.
[7] Prasanna Kumar, Amitabha Sanyal, and Amey Karkare. 2016. Liveness-based Garbage Collection for Lazy Languages. In Inrenational Symposium on
Memory Management (ISMM 2016).
[8] Yanhong A. Liu and Scott D. Stoller. 2003. Eliminating Dead Code on Recursive Data. Sci. Comput. Program. 47 (2003).
[9] Neil Mitchell and Colin Runciman. 2009. Losing Functions Without Gaining Data: Another Look at Defunctionalisation. In Proceedings of the 2nd
ACM SIGPLAN Symposium on Haskell.
[10] Mehryar Mohri and Mark-Jan Nederhof. 2000. Regular Approximation of Context-Free Grammars through Transformation. In Robustness in
Language and Speech Technology. Kluwer Academic Publishers.
[11] NoFib. 2017. Haskell Benchmark Suite. http://git.haskell.org/nofib.git. (Feb 2017). (Last accessed).
[12] Claudio Ochoa, Josep Silva, and Germán Vidal. 2008. Dynamic Slicing of Lazy Functional Programs Based on Redex Trails. Higher Order Symbol.
Comput. 21 (2008).
[13] Karl J. Ottenstein and Linda M. Ottenstein. 1984. The program dependence graph in a software development environment. ACM SIGPLAN Notices
19 (1984).
[14] Roly Perera, Umut A. Acar, James Cheney, and Paul Blain Levy. Functional programs that explain their work. In ACM SIGPLAN International
Conference on Functional Programming, ICFP 2012.
[15] Thomas W. Reps and Todd Turnidge. 1996. Program Specialization via Program Slicing. In Partial Evaluation, International Seminar, Dagstuhl Castle,
Germany.
[16] John C. Reynolds. 1998. Definitional Interpreters for Higher-Order Programming Languages. Higher-Order and Symbolic Computation 11, 4 (1998).
[17] Nuno F. Rodrigues and Lus S. Barbosa. 2006. Component Identification Through Program Slicing. Electronic Notes in Theoretical Computer Science
160 (2006).
[18] Nuno F. Rodrigues and Lus S. Barbosa. 2006. Program Slicing by Calculation. Journal of Universal Computer Science (2006).
[19] Josep Silva. 2012. A Vocabulary of Program Slicing-based Techniques. ACM Comput. Surv. (2012).
[20] Josep Silva, Salvador Tamarit, and César Tomás. 2012. System Dependence Graphs in Sequential Erlang. In Proceedings of the 15th International
Conference on Fundamental Approaches to Software Engineering (FASE’12).
[21] Scott F. Smith and Tiejun Wang. 2000. Polyvariant Flow Analysis with Constrained Types. In Proceedings of the 9th European Symposium on
Programming Languages and Systems (ESOP ’00).
[22] Frank Tip. 1995. A Survey of Program Slicing Techniques. Journal of Programming Languages 3 (1995).
[23] Mark Weiser. 1984. Program Slicing. IEEE Trans. Software Eng. 10 (1984).

Manuscript submitted to ACM

