논□문

Bi-directional Demand-Driven Set-Based Analysis

Woongsik Choi and Kwangkeun Yi

Korea Advanced Institute of Science and Technology

Division of Computer Science

{wschoi, kwang}@ropas.kaist.ac.kr

Abstract

In this paper, we present a bi-directional demand-driven set-based analysis which solves only those constraints affecting program points one wants to analyze. To achieve this goal, we incorporate the notion of demands on set constraints and analyze programs in two directions: forward to know which values flow into a given point, and backward to know which program points that a given value flows into. We prove that for interested program points, our analysis gives exactly the same results as whole-program set-based analysis. As an experiment of our approach, we analyzed each program point separately using our demand-driven formulation. We report the efficiency of our analysis as percentage of constraints solved for each program point compared with the whole-program analysis.

1. Introduction

When analyzing programs, there are often situations that analysis of whole program is not needed. For example, one may need analysis results for only a subset of all functions in the program. For array bound check, only values for array index are needed. Another situation might be the semantic exhaustiveness check of pattern matchings in ML-like programs, where one may need only those values  flowing into pattern matchings.

With these motivations, we propose demand-driven formulation of set-based analysis. Set-based analysis [5,4,3] is a static analysis technique that estimates sets of values by regular tree grammars [4]. Such regular tree grammar's production rules are derived in a form of set-constraints. In set-based analysis, there's no solving order defined and due to higher order functions in functional languages, analysis results for a program point can't be determined until analysis for whole-program is finished. To overcome this aspect and make it demand-driven, we incorporate notion of demands to set-based analysis. Starting from initial demands of interested program points, we add new demands for related program points and solve a constraint only if we have demand for it. One can view demands as specifying solving order to set-based analysis.

To achieve demand-driven formulation in the presence of higher-order functions, we solve constraints in two directions. For a given program point, the result of set-based analysis is approximation of all values computed for the point. To acquire all such "forward" information of computation in demand-driven way, we sometimes need opposite "backward" information of all program points on which a given function can be called. Let's consider following higher-order program fragment.

let fun f x = case x of ...

fun g h = ... [eqn: e_{1}] ...

in ... f [eqn: e_{2}] ... g f ... end

For the (forward) demand of argument x, we have to collect function f's actual arguments, [eqn: e_{1}] and [eqn: e_{2}] by identifying all call sites of f. [eqn: e_{2}] might be easily identified syntactically, but as functions in higher-order programs are first-class objects, [eqn: e_{1}] can't be identified without analyzing all call sites the function f flows into. So, we add backward demand for f and solve this demand in backward direction identifying that f flows into the call site h [eqn: e_{1}].

1.1. Other Approaches for Demand Driven Analyses

Biswas formulated a demand-driven set-based analysis for the purpose of dead code elimination [2]. However, in his formulation, initial demand is restricted only to top-level expression and constraints for arbitrary program points can't be analyzed separately. He adds demand constraints to usual value constraints. His approach solves both value constraints and demand constraints simultaneously. Demand constraints are solved in such a way that if a program point is included in the demand, then it is not dead code. In this way, he solves constraints for only non-dead codes, and when solving is done, program points not in the demand set are identified as dead codes. Contrary to this use of demands to indicate non-dead codes, demands in our demand-driven formulation can be any program points of interest.

In Heintze and Tardieu's demand-driven formulation of pointer analysis for C-like languages[6], similar concept of separating forward flows and backward flows is used. In a language like C, pointer analysis is answering the query "what may a program variable p point to?". To solve indirect assignment in fully demand-driven way, they solve the backward query "what variables may point to p?". Our work can be seen as applying their strategies for demand-driven formulation to set-based analysis of higher-order languages.

Figure . Syntax

1.2. Paper Organization

The rest of this paper is organized as follows. In Section 2, we define a core ML language we will use to represent our work. In Section 3, we briefly summarize set-based analysis for the language. In Section 4, we modify the set-based analysis and formulate a demand-driven set-based analysis. In Section 5, we prove that our demand-driven formulation gives the same results for demanded program points. In Section 6, we report the experimental results for solving each program points separately and discuss about the results. In Section 7, we conclude the paper.

2. The Language

In this section, we introduce a simple language that we will describe our work with. It is an untyped core ML with data constructors and simplified pattern matching constructs.

Syntax of the language is shown in Figure 1. Here, [eqn: Var] is a finite set of program variables and  [eqn: Con] is a finite set of date constructors with predefined arities. [eqn: x,~ lambda x.e,~ e_1~ e_2], are components of core ML. [eqn: c(e_1 , CDOTS , e_n )] produces structured values with data constructor [eqn: c] of fixed arity [eqn: n].[eqn: case ( e_1 , c ( x_1 , CDOTS , x_n )~ RARROW ~ e_2 , y ~ RARROW ~ e_3 )] represents simplified pattern matching. Recursive functions are omitted for presentational simplicity because they are not affected by our demand-driven formulation.

We show dynamic semantics of the language in natural semantics form in Figure 2. The natural semantics establish the relation [eqn: E ~ ASSERT e ~ -> ~ v] saying that in environment [eqn: E], expression [eqn: e] evaluates to value [eqn: v]. Here, environment [eqn: E] is a finite mapping from program variables to values. The notation [eqn: E [ x ~ MAPSTO ~ v ]] denotes the environment which has the same mappings as [eqn: E] except for [eqn: x], which maps to [eqn: v]. We have two kinds of values, data constructed values and function closures. To enforce static scoping, we keep track of the environment in which a function is generated as a function closure.

Figure . Dynamic semantics

3. Set-Based Analysis [5]

Set-based analysis is a static analysis method, which approximates sets of values for each programs points by regular tree grammars [4], whose production rules are derived in a form of set constraints. By collapsing all environments appearing during evaluation into a single set environment, dependencies between different environments are ignored and runtime values of the program are approximated in finite time.

The method is separated into two phases. In first phase, initial set constraints are generated from the source program. This generation transforms the meaning of the program into set containment relationships with set expressions modeling approximation semantics. Also, every program point is named with set variables. So, after generation, the source program is not needed anymore. In second phase, we solve the generated constraints by adding simpler constraints explicitly representing flows of values. Analysis is done when there are no more constraints to add. The analysis result is explicit set containments for every set variable.

3.1. Set Constraints

We define set expressions and their meanings in Figure 3. We have three kinds of set expressions. First, variable set expressions denote program points. Two special set variables are used to handle flows generated by function applications. [eqn: dom ( lambda x . e )] denotes actual arguments flowing into [eqn: lambda x . e]'s formal argument. [eqn: ran ( lambda x . e )] denotes result values of function application. Second, abstractions and   constructed value expressions denote set of values, which we call atomic set expressions. Lastly, [eqn: apply] and [eqn: case] expression denote semantics of the language. Meaning of set expression is given by extending interpretation , which is a mapping from set variables to sets of values. Note that we don't have environments as function closure because single predefined set environment is used. Restrictions in the extension guarantees that  is sound approximation of the program.

Figure 3. Set expressions

Set constraints are of the form [eqn: SUPSETEQ ~ se] meaning that program point  contains the values denoted by [eqn: se].

Set constraints are generated from the source program by the rules in Figure 4. Environment  maps program variables to corresponding set variables. The relation [eqn: E ~ VDASH ~ e ~ TRIANGLER ~ (][eqn: ,C)]says that in environment [eqn: E], constraints [eqn: C] are generated with new set variable  denoting program point [eqn: e].

3.2. Set Constraint Solving

We present set constraint solving rules, E, in Figure 5. E simulates the data flows in programs by propagating set constraints. For example, for a function call site, rule E1 links the result of the site with body of functions flowing into the site and rule E2 links formal argument of those functions to actual argument of the site. Further simplifications are initiated by flowing values through links established.

Figure 4. Set constraint generation

Figure 5. Exhaustive solving (E)

We define analysis as the reflexive transitive closure [eqn: (C)] of E[eqn: (C)], a single step of adding constraints by applying E to [eqn: C]. The closure is the set of initial constraints [eqn: C] and all added constraints by repeatedly applying E. The main result of set-based analysis[3] showed that we get explicit representation of safe approximation of the program by collecting all constraints of the form [eqn: SUPSETEQ ~ ae] in [eqn: (C)].

4. Bi-directional Demand-Driven Set-Based Analysis

In this section, we develop a demand-driven set-based analysis by modifying Heintze's exhaustive set-based analysis presented in Section 3. Our demand-driven set-based analysis solves from arbitrary initial demands of interested program points, only those constraints affecting them and gives the same results as exhaustive set-based analysis for them.

4.1. Making it Demand-Driven

Let's consider the rule E1 of exhaustive solving E in Figure 5.

Here, we add the constraint that  contains [eqn: ran ( lambda x . e )]. We need this constraint if we want to know what values program point  evaluates to, i.e., if we have demand for . So, we need the following demand-driven rule with the notation [eqn: D(][eqn: )] meaning that we have demand for .

Next step is adding new demands to ensure that we solve all necessary constraints. Let's continue considering the case E1. We have to ensure that all premises in the original rule E1 are added in demand-driven solving. All constraints with [eqn: apply ( CDOTS )] are directly generated from the source program. So, the premise, [eqn: SUPSETEQ ~ apply (][eqn: ,][eqn: )] is guaranteed to be in demand-driven solving. However, the other premise, [eqn: SUPSETEQ ~ lambda x . e], can be added during solving process. We can guarantee that this premise is added in demand-driven solving with [eqn: D (][eqn: )], i.e., we need to know what values  evaluates to. So, we can write the following demand-add rule.

Note that from [eqn: D (][eqn: )], we can identify     [eqn: SUPSETEQ ~ apply (][eqn: ,][eqn: )] right away because it is a generated constraint.

Demand-add rules specify solving sequence. For example, the rule we have just defined specifies solving sequence as follows: To solve constraints for  which is a call site of     [eqn: SUPSETEQ ~ apply (][eqn: ,][eqn: )], we first find all functions  evaluates to.

Using similar approach, we can make all rules demand-driven and get associated demand-add rules except for the case E2 [eqn: dom ( lambda x . e )], which we will discuss next.

4.2. Demand for Formal Argument

Let's consider the rule E2.

We can make the rule itself demand driven as follows:

However, we can't get the associated demand-add rule as other cases. From [eqn: D ( dom ( lambda x . e ) )], we have only the clue that [eqn: lambda x . e] flows into some . Finding out all such  from [eqn: lambda x . e] is not trivial because   [eqn: SUPSETEQ ~ lambda x . e] might be a newly added constraint during solving.

Naive approach of following demand-add rule works, but it is not fully demand-driven in the sense that we solve all call sites regardless of initial demands:

In order to avoid this too loose demand-add rule, we need to consider solving constraints in the opposite direction. The information needed here is all call sites that [eqn: lambda x . e] flows into. So, we make it fully demand-driven by solving [eqn: lambda x . e] in the opposite backward direction. We specify solving directions with the notations [eqn: FD (][eqn: )] for ordinary forward solving of  and [eqn: BD ( se )] for the opposite backward solving of [eqn: se]. With these two solvings, demand-add rule for forward formal argument is stated as follows:

That is, we need to know where [eqn: lambda x . e] flows into (backward needness) if we need to know what values flow into formal argument [eqn: x] (forward needness).

4.3. Bi-directional Demand-Driven Solving

Our demand-driven solving rules consist of forward rules and backward rules interleaved. We solve some constraints in forward direction and some in backward direction. For the presentational simplicity, we include forward demand [eqn: FD (][eqn: )] and backward demand [eqn: BD ( ae )] or [eqn: BD (][eqn: )] as special kinds of set constraints.

Forward demand-driven solving, F, finds all constraints of the form [eqn: SUPSETEQ ~ se] if we have the forward demand, [eqn: FD (][eqn: )]. The solving rules and demand-add rules of forward solving are shown in Figure 6. Two rules are indexed with the same number for solving rule and corresponding demand-add rule.

Backward demand-driven solving, B, finds all constraints of the form [eqn: SUPSETEQ ~ se] if we have the backward demand, [eqn: BD ( se )]. We present solving rules and demand-add rules in Figure 7. We formulated these rules similar to the way we did for the forward solving. For example, B2 is derived from E2 by adding the premise [eqn: BD (][eqn: )] to ensure that we add [eqn: dom ( lambda x . e ) ~ SUPSETEQ ~] only if we have the backward needness for  as follows:

To guarantee that non-trivial premise        [eqn: SUPSETEQ ~ lambda x . e] is included in the backward solving, we devise following demand-add rule :

This rule specifies that to consider all program points that an actual argument of a call site flows into, we have to first find out all functions flowing into the call site. Other rules are derived according to similar ideas.

Figure 6. Forward demand-driven solving (F)

Demand-driven set-based analysis repeatedly applies rules F and B. Let [eqn: C'] be the union of the generated constraints and initial forward demands. We define FB[eqn: (C')] to be newly added constraints by applying F and B to [eqn: C'] once. Then, solving process is represented by the reflexive transitive closure, [eqn: (C')].

5. Equivalence

In this section, we prove that for the program points we want analyze, our demand-driven set-based analysis gives the same results as the original exhaustive analysis. We prove the equivalence by using similar strategy and notations Heintze used to prove equivalence of his demand-driven pointer analysis [6].

Figure 7. Backward demand-driven solving (B)

Equivalence guaranteed by our demand-driven formulation is restricted to top-level structure in case of constructed values. Suppose we have forward demand for  and constraint   [eqn: SUPSETEQ ~ c (][eqn: )] is in the solution. In this case, values for  are not guaranteed to be in the solution. This is not surprising since we only guarantees that all constraints of the form    [eqn: SUPSETEQ ~ se] are in the solution and we don't have constructed value set expression of the form [eqn: c ( ae )]. Solution of set-based analysis is a regular tree grammar specifying how to build values in the solution [4].

This is not severe restriction. First, one may actually need to know only top-level structure of values. In those situations, our method is more efficient than finding values for all components together. Second, if values for components are needed, those values can be solved by invoking the analysis again with demands for needed components. In reinvocations, constraints solved in previous invocations are saved and need not be solved again. So there's not much performance loss by solving constraints through successive steps for components.

Now, we prove the equivalence. Let's first define following assertions to represent result constraints of demand driven solving. Let [eqn: C] be generated constraints and [eqn: C'] be the union of generated constraints and initial forward demands.

this assertion states if [eqn: FD(X)] in    [eqn: (C')] then [eqn: X ~ SUPSETEQ ~ se ~ IN ~][eqn: (C')].

this assertion states if [eqn: FD(X)] in    [eqn: (C')] then [eqn: X ~ SUPSETEQ ~ se ~ IN ~][eqn: (C')].

Lemma 1 (Soundness). If  [eqn: SUPSETEQ ~ se ~ IN ~]

[eqn: (C')] then [eqn: SUPSETEQ ~ se ~ IN ~][eqn: (C)].

Proof: This is trivial since demand only restricts solving process. We start demand-driven solving with the same value constraints, and all solving rules in F and B are restricted version of the same rules in E each with an additional premise for demand.

Lemma 2 (Completeness).   If [eqn: SUPSETEQ ~ se ~ IN ~]

[eqn: (C)] then  and

Proof: We prove by induction on the proof tree of derivations of [eqn: SUPSETEQ ~ se ~ IN ~][eqn: (C)].

Base cases

Base cases of [eqn: SUPSETEQ ~ se ~ IN ~][eqn: (C)] are generated constraints . All these constraints are included in forward (backward) solving since [eqn: C' ~ SUPSETEQ ~ C].

Theorem 1 (Equivalence). For all [eqn: FD (][eqn: ) IN],

[eqn: C'], [eqn: SUPSETEQ ~ se ~ in ~][eqn: (C)] iff [eqn: SUPSETEQ ~ se ~ in ~][eqn: (C')].

Proof: It follows immediately from Lemma 1 and Lemma 2

6. Experimental Results and Discussion

We have implemented prototypes of both exhaustive analysis and demand-driven analysis over nML programming language system [7] to measure the performance of demand-driven analysis. We analyzed source code after pattern matching compilation based on decision tree model [1], which transforms ML's complex pattern matching to the restricted form of the core language. For other parts of full ML not represented in core language, we extended the core analysis with similar ideas in [5] except that we didn't analyze arithmetics.

We have experimented by solving each program point separately. For each program point, we start analysis from generated constraints from source program and with single forward demand for the point. As mentioned in Section 5, for the initial program point of interest, we solved for full structure of values by reinvocating the analysis for the components of structured values. We included significant libraries such as list libraries in the source program and analyzed them together.

Summary of experimental results are shown in Figure 8. First four programs are widely used benchmarks for ML. dsba is our analyzer itself. patcomp is a pattern match compiler for nML. evalcps is an interpreter and continuation passing style (cps) converter of simple functional language. Initial constraints are generated constraints from the program roughly indicating program size. We show maximum and average percentages of constraints added for demand-driven solving of a program point compared to exhaustive solving. Maximum percentage indicates the program point solving the largest number of constraints. We show average of all program points though it may not be much meaningful because of high variance.

More detailed results are shown in Figure 9. For each program, we give percentages of program points solving 0-5%,[eqn: CDOTS], 95-100% of constraints compared to exhaustive solving. We could see some interesting points with the results.

Figure 8. Experimental results (summary)

Figure 9. Experimental results (details)

Many program points solve 0-5%. This behavior is quite natural since many program points do simple computation. For example, in extreme, program points for constants solve 0\%.

Many program points solve near maximum percentages. In mono-variant analysis, all function calls are merged. So, if the result of a function call is needed, we have to analyze all other call sites of the function, which can be the cause of this behaviour. Also, we can think that mono-variance is causing clustering of program points with many 0's in Figure 9.

44%, 36.9% maximum percentages for fft and nucleic. What we observed from this behaviour is that demand-driven formulation reflects crude approximation done in base analysis and doesn't solve unnecessary constraints due to those approximation. fft and nucleic are intensive numerical applications. However, we didn't analyzed arithmetics. Analysis result for [eqn: e_1 + e_2] is [eqn: TOP], meaning all values are possible. So, values for [eqn: e_1] and [eqn: e_2] are not needed to get this [eqn: TOP] value. When we modified demand-driven formulation to enforce demand for [eqn: e_1] and [eqn: e_2], we got 61.4% maximum percentage for fft and 89.8% for nucleic. Also, fft uses arrays intensively. We analyzed arrays by collapsing all cells of an array into a single reference cell as Heintze did in [5]. Again, this approximation discards any need for array indexes other than needs for themselves. When we also enforced demands for array indexes in addition to arithmetic arguments, we got 80% maximum percentage.

7. Conclusion

We have developed a demand-driven approach for set-based analysis. By incorporating demands to the analysis, only those constraints related to interested program points are solved. To get fully demand-driven formulation, we solved some constraints in forward direction and some in backward direction. We have proved that our approach is equivalent to original exhaustive approach in the sense that for the initial demands, our approach gives exactly the same results. We have implemented prototypes of our analysis and experimental results show interesting aspects of demand-driven analysis.

References

[1] Marianne Baudinet and David MacQueen,  "Tree pattern matching for ML", unpublished paper, 1985.

[2] Sandip K. Biswas, "A demand-driven set-based analysis", Proceedings of ACM Symposium on Principles of Programming Languages, pages 372-385, 1997.

[3] Nevin Heintze, "Set-Based Program Analysis", PhD thesis, Carnegie Mellon University, October 1992.

[4] Nevin Heintze, "Set constraints in program analysis, Proceedings of International Symposium on Logic Programming, 1993.

[5] Nevin Heintze, "Set-based analysis of ML programs, Proceedings of the ACM Conference on Lisp and Functional Programming, pages 306-317, 1994.

[6] Nevin Heintze and Olivier Tardieu, "Demand driven pointer analysis", Proceedings of ACM Conference on Programming Language Design and Implementation, pages 24-34, 2001.

[7] nML programming language system, version 0.92a, Research On Program Analysis System, KAIST, March 2002, http://ropas.kaist.ac.kr/n.

Woongsik Choi

2002, M.S. Computer Science,  KAIST

2000, B.S. Computer Science,  KAIST

Kwangkeun Yi

1995 - now Associate Professor, KAIST

1993 - 1995 Member of Technical Staff, Software Principles Research Dept., Bell Labs., Murray Hill

1993, Ph.D. Computer Science, Univ. of Illinois at Urbana-Champaign

1990, M.S. Computer Science, Univ. of Illinois at Urbana-Champaign

1987, B.S. Computer Science & Statistics, Seoul National University