Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript Benjamin Barslev Nielsen Aarhus University, Denmark barslev@cs.au.dk Anders Møller Aarhus University, Denmark amoeller@cs.au.dk Abstract In static analysis of modern JavaScript libraries, relational analysis at key locations is critical to provide sound and useful results. Prior work addresses this challenge by the use of various forms of trace partitioning and syntactic patterns, which is fragile and does not scale well, or by incorporating complex backwards analysis. In this paper, we propose a new lightweight variant of trace partitioning named value partitioning that refines individual abstract values instead of entire abstract states. We describe how this approach can effectively capture important relational properties involving dynamic property accesses, functions with free variables, and predicate functions. Furthermore, we extend an existing JavaScript analyzer with value partitioning and demonstrate experimentally that it is a simple, precise, and efficient alternative to the existing approaches for analyzing widely used JavaScript libraries. 2012 ACM Subject Classification Theory of computation → Program analysis Keywords and phrases JavaScript, dataflow analysis, abstract interpretation Digital Object Identifier 10.4230/LIPIcs.ECOOP.2020.16 Funding This work was supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No 647544). 1 Introduction JavaScript programs are challenging to analyze statically due to the dynamic nature of the language. One of the main obstacles is the presence of dynamic property access operations that allow objects to be manipulated using object property names that are dynamically computed strings. A typical pattern that has received much attention is correlated read/write pairs [25], a simple variant of which looks as follows: t = x[p]; ... y[p] = t; At run-time, this code copies a property whose name is the value of p from the x object to the y object. If the static analysis does not know precisely the string value of p, then the properties of x will be mixed together in y. Experience with analyzers such as WALA [25, 24, 28], SAFE [17, 22], JSAI [13], and TAJS [11, 2, 26] has shown that when analyzing real-world JavaScript code, including jQuery, Lodash, Underscore and other widely used libraries, such situations often cause an avalanche of spurious dataflow that makes the analysis results useless. If, for example, x is the object {m1: f1, m2: f2, ..., m10: f10} where f1, f2, . . . , f10 are functions, then any subsequent function call, for example y.m3(...), will be treated by the analysis as a call to any of the 10 functions. Several analysis techniques have been proposed to address this challenge. The techniques based on correlation tracking [25], static/dynamic determinacy [24, 2], and loop sensitivity [22] aim to increase precision by the use of context sensitivity or loop unrolling to ensure that © Benjamin Barslev Nielsen and Anders Møller; licensed under Creative Commons License CC-BY 34th European Conference on Object-Oriented Programming (ECOOP 2020). Editors: Robert Hirschfeld and Tobias Pape; Article No. 16; pp. 16:1–16:28 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany 16:2 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript the analysis has precise information about p in the example above. Although this approach works well in many cases, the aggressive use of context sensitivity or loop unrolling can be expensive on analysis time. Even more importantly, it falls short when p is not determinate (i.e., when its value is not fixed even when the call context is known). An important step forward is the approach used in the CompAbs analyzer, which is built on SAFE [16]: Even if p is imprecise, the loss of precision at the property write operation can be avoided by applying trace partitioning [23] at the property read operation, based on which properties exist on x. Intuitively, it is often not necessary to have precise information about p; instead we can refine the current abstract state into a collection of more precise partitions, one for each of the 10 properties of x (plus one extra for the case where p is none of those strings, but let us ignore that for now), and after the property write operation merge them again. (The same idea was used earlier in TAJS, but only at for-in loops, not at dynamic property reads [2].) This approach, however, also has drawbacks. Trace partitioning is expensive, so it must be used scarcely: in the example, the code between the dynamic property read and the dynamic property write is essentially analyzed 10 times. For this reason, CompAbs relies on a syntactic pre-analysis to recognize different kinds of correlated read/write pairs for guiding the creation and merging of partitions. Recent work [26] has shown that the syntactic pre-analysis approach of CompAbs is too fragile, for example, it is incapable of analyzing the Lodash library (see Section 2), and demand-driven value refinement has been proposed as an alternative. Instead of relying on context sensitivity, loop unrolling, or trace partitioning, that approach applies, during the analysis when encountering a dynamic property write operation with an imprecise property name, a separate backwards analysis to regain the relation between the property name and the value to be written. Although demand-driven value refinement has been shown to work quite well in practice, building a backwards analysis for the full JavaScript language and its standard library is a major endeavor, so developing simpler alternatives is desirable. Our approach builds upon the observation from CompAbs that sufficient precision can be obtained using trace partitioning based on the properties of the object being read. Our key insight is that we do not need to partition the entire abstract state as done by CompAbs: It suffices to only partition the abstract values for the property name p and the value being read x[p] in the above example. This means that instead of analyzing the code 10 times, we only analyze it once, but using partitioned abstract values that retain the correlation between p and x[p]. The partitioned abstract values are introduced at t = x[p] and used at y[p] = t by means of specialized transfer functions. We refer to this variant of trace partitioning as value partitioning. Since partitioning individual abstract values does not increase the analysis complexity as much as partitioning entire states, it becomes feasible to apply value partitioning more extensively, at every dynamic property read where the property name is imprecise, thereby obviating the need for the syntactic pre-analysis. In this paper we present a theoretical framework for value partitioning, together with three instantiations: property-name partitioning (which is the one used in the example above), free-variable partitioning (to improve precision for free variables of closures), and type partitioning (to improve precision for predicate functions). Additionally, we extend the static analyzer TAJS with all three kinds of value partitioning and demonstrate that the approach is effective for analyzing popular JavaScript libraries. Value partitioning is a lightweight alternative to the existing approaches to relational analysis for JavaScript: Compared to CompAbs-style trace partitioning it avoids many redundant computations caused by similarities between different partitions, and compared to demand-driven value refinement it avoids the need for creating a separate backwards analysis. B. B. Nielsen and A. Møller 16:3 1 function mixin(object, source) { 2 baseFor(source, function (func, methodName) { 3 if (!isFunction(func)) 4 return; 5 object[methodName] = func; 6 if (isFunction(object)) 7 object.prototype[methodName] = function() { 8 ... 9 func.apply(...); 10 } 11 }); 12 } 13 14 function baseFor(source, iteratee) { 15 Object.keys(source).forEach(function (key) { 16 iteratee(source[key], key); 17 }); 18 } 19 20 // usage of mixin during initialization 21 mixin(lodash, lodash); Figure 1 Motivating example based on code from the Lodash library. In summary our contributions are: Value partitioning: a general static analysis technique that is capable of reasoning about relations between abstract values. Three instantiations of value partitioning, which tackle different challenges in static analysis for JavaScript, each involving relational properties: property-name partitioning: relations between dynamically computed object property names and values; free-variable partitioning: relations between functions and their free variables; and type partitioning: relations between arguments and return values of predicate functions. Experimental results: We show that value partitioning makes TAJS more precise than CompAbs [16] for several real-world JavaScript libraries, including Lodash, which is the most widely used library. The resulting precision is comparable to (and in case of the Lodash4 benchmark group substantially higher than) that of demand-driven value refinement [26], without the need for a separate backwards analysis. 2 Motivating Example and Overview Figure 1 shows a small code example based on Lodash (version 4.17.10), which is the most depended-upon of all npm packages.1 Lines 1–12 define the function mixin, which copies all function properties from source to object. If object is a function, a new function (which 1 Lodash (https://lodash.com/) has more than 115 000 dependents in npm and more than 27 million weekly downloads as of May 2020. ECOOP 2020 16:4 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript on invocation calls the function to be copied) is also copied to object.prototype, such that instantiations of object (using the keyword new) also will have these functions. In line 21, which is executed during the initialization of Lodash, mixin is called with the library object as both arguments. The function mixin uses a helper function baseFor defined in lines 14– 18. It is called with source and a callback function defined in lines 2–11. The baseFor function then gets all the object property names from the source object using Object.keys, and the callback function is called (line 16) for each property name and corresponding property value. Line 3 checks whether func is a function. If so, the function is copied to object[methodName] in line 5. Note that func actually is the value source[methodName]. Line 6 checks whether object is also a function and if so, a new function is declared and written to object.prototype[methodName] in line 7. When invoked, that new function calls func using func.apply(...) in line 9. Such complex code is not unusual in modern JavaScript libraries. For a static analysis reasoning about the dataflow in this code, the correlation between methodName and func is critical. An analysis that loses track of this correlation will mix together all the properties of the library object lodash when analyzing the call mixin(lodash, lodash) in line 21. As a consequence, if the program being analyzed contains a call to, for example, lodash.map, that will be treated by the analysis as a call to any of Lodash’s more than 100 different functions, not only the actual map function, thereby triggering an avalanche of spurious dataflow. Existing approaches Existing JavaScript analyzers do not have precise information about the value of key in line 16, for various different reasons. (Most importantly, Object.keys produces an array of property names in unspecified order.) Previous work has suggested two approaches to analyze such code precisely even when key is imprecise. The CompAbs [16] approach uses trace partitioning guided by syntactic patterns. If trace partitioning is used at the dynamic property read operation in line 16, the abstract state is partitioned into a set of refined abstract states corresponding to the properties of the source object. This way the value of key is precise in each of those states, and the call in line 16 is analyzed separately for each of them. Trace partitioning, however, is expensive, so CompAbs limits the use of trace partitioning according to certain syntactic patterns. At this specific dynamic property operation, CompAbs chooses not to apply trace partitioning and fails to detect that the relation between methodName and func is important. The second approach is demand-driven value refinement [26], which can analyze the example code with sufficient precision to avoid mixing together the Lodash functions. With this approach, the analysis detects imprecision at the dynamic property write in line 5: methodName is an imprecise string and func can be many different functions. It then queries a backwards abstract interpreter asking for the possible value of methodName for each of the functions. The backwards analysis returns a precise property name for each function and thereby enables the dynamic property write operation to be modeled precisely. For the dynamic property write in line 7, the function defined in lines 7–10 is written to all properties of object.prototype, but the abstract value being written is augmented, such that the value of methodName remains precise. When reading func in line 9, the backwards analysis is queried to get the value of func relative to the value of methodName, thereby retrieving a precise value for func. This ensures the desired precision, but the approach requires a complicated backwards analysis. B. B. Nielsen and A. Møller 16:5 Value partitioning We will now informally explain how value partitioning can provide similar precision as demand-driven value refinement, but without the need for a backwards abstract interpreter. With traditional trace partitioning, as used by, for example, CompAbs, the analysis can track multiple abstract states for each program point, such that the different abstract states cover different assumptions about the execution paths that lead to that point. (Correlation tracking [25], determinacy-based analysis [24, 2], and loop sensitivity [22] can also be viewed as variations of trace partitioning.) The key idea behind value partitioning is that we can obtain a similar effect as trace partitioning by instead performing the partitioning at the level of individual abstract values. In principle, the resulting abstract domain is isomorphic to a traditional trace partitioning domain, but this approach provides more flexibility for using different kinds of partitioning for different parts of the abstract states. This general idea can be instantiated in multiple ways to track different kinds of relational properties. We next describe three instantiations that enable precise analysis of challenging JavaScript code, including the Lodash example. Property name partitioning One instantiation is property name partitioning, which performs partitioning at dynamic property reads, similar to the CompAbs technique, but on abstract values instead of abstract states. To illustrate this mechanism by example, consider the read operation in line 16 and the correlated write operation in line 5. Assume for simplicity that the source ob- ject has only two properties, {map: f1, trim: f2} where f1 and f2 are functions, and methodName is an abstract value that overapproximates all valid property names. When read- ing source[methodName], an analysis without value partitioning will read all the properties of source. When using value partitioning, we instead partition this value according to the prop- erty names of source, meaning that we obtain a value [t1 7→ f1, t2 7→ f2, t3 7→ undefined] where t1 , t2 , and t3 represent different partitions.2 Intuitively, t1 represents the execution traces where the property name being read is map, t2 similarly represents traces where the property name being read is trim, and t3 represents all other traces. We similarly write the partitioned value [t1 7→ "map", t2 7→ "trim", t3 7→ AnyString] to methodName.3 In this way, the resulting abstract state retains the correlation between the values of methodName and source[methodName]. Later the analysis reaches the write operation object[methodName] = func, with an abstract state where methodName is [t1 7→ "map", t2 7→ "trim", t3 7→ AnyString] and func is [t1 7→ f1, t2 7→ f2, t3 7→ undefined]. Since the property name and the value to be written have the same partitions, we can perform the dynamic property write separately for each partition, meaning that f1 is written to the map property, and analogously for the other two partitions, thereby avoiding mixing together the properties. Since the partitioning is performed at the value level, unlike traditional trace partitioning we do not need any extra call contexts to the callback function defined in line 2, so the overhead of value partitioning is negligible, even when the correlated read/write pairs span multiple functions. For this reason, we can apply property name partitioning at all dynamic property reads where the property name is imprecise, without the use of syntactic patterns. 2 In JavaScript, reading an absent property yields the special value undefined. 3 AnyString is an abstract value that represents any string. In practice we instead use a slightly more precise abstract value representing AnyString\{"map", "trim"}. ECOOP 2020 16:6 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript Free variable partitioning A second instantiation of value partitioning is for handling free variables more precisely. In the example, this is useful for func in line 9, which is a free variable in the function defined in lines 7–10. At that function definition, we partition both the resulting abstract function value ` and the abstract value of func according to the existing partitioning of func, intuitively to be able to distinguish functions created with different values of the free variable. This means that the function value being written at the dynamic property write in line 7 is [t1 7→ `t01 , t2 7→ `t02 , t3 7→ `t03 ] where `t01 represents the function created at a point where func is f1 (i.e., that point is at the end of a t1 trace), and similarly for the other partitions. At the same time, the value of func becomes [t1 7→ f1, t2 7→ f2, t3 7→ undefined, t01 7→ f1, t02 7→ f2, t03 7→ undefined] where the three new partitions t01 , t02 , and t03 denote the new partitioning we have made (one abstract value can thus have multiple partitionings simultaneously). Using the property name partitioning mechanism described above, at the dynamic property write in line 7, `t01 is written to the map property of object.prototype, and similarly for the other properties. We can exploit the free variable partitioning information when the function is later called. Assume the analysis encounters a call to the map method. The abstract value of lodash.prototype.map is then `t01 . We now use t01 as a context in ordinary context sensitive analysis of the function, so that when reaching func in line 9, it suffices to consider only the t01 partition of func, which yields the precise value f1, so again, we successfully avoided mixing together the properties. Type partitioning The above two uses of value partitioning are sufficient for analyzing the motivating example without critical precision losses, but we can make the analysis even more precise using a third variant. The function named isFunction used in the branch condition in line 6 is a typical example of a predicate function, i.e., a one-parameter function that returns a boolean, in this case testing whether the value passed in is a function. Assume the abstract value of the argument object is fun1|obj2, meaning that it represents either a function fun1 or a non-function object obj2. With a simple analysis, the abstract return value and hence the branch condition is Bool representing any boolean value, so the analysis does not know that object cannot be obj2 inside the branch. This causes the analysis to spuriously raise a type error when writing to object.prototype in line 7. Type partitioning avoids that imprecision as follows. Type partitioning is triggered at any call to a function with one argument, and partitions that argument according to its types. In this case, the value of object is partitioned into [a 7→ fun1, b 7→ obj2]. The result value from isFunction then becomes [a 7→ true, b 7→ false], which we can exploit using ordinary control sensitivity [10] (also called type refinement [14]) at the “true” branch such that object in line 7 will only be fun1 and not obj2. Overview In Section 3 we give a brief introduction to the analysis domain of TAJS. Section 4 explains the general value partitioning mechanism, and Section 5 details the three instantiations: property name partitioning, free variable partitioning, and type partitioning. Section 6 describes our experimental evaluation, and Section 7 discusses related work. B. B. Nielsen and A. Møller 16:7 r1 [r2 ] ← r3 : Writes r3 to the property named r2 of the object r1 r1 ← r2 [r3 ]: Reads the property named r3 of the object r2 to r1 r1 ← x: Reads the value of the variable x to r1 x ← r1 : Writes r1 to the variable x r1 ← c: Assigns the constant c to r1 r1 ← function(x){· · · }: Creates a closure for the function and stores it in r1 if(r1 ): Conditionally propagates dataflow (to model if and while) r1 ← r2 (r3 ): Calls the function r2 with argument r3 and stores the result in r1 r1 ← r2 ⊕ r3 : Computes the binary operation r2 ⊕ r3 and stores the result in r1 Figure 2 The main flow graph instructions in TAJS. X ∈ AnalysisLattice = L → State n ∈ N : Nodes σ ∈ State = (L → Obj) × Registers c ∈ C : Contexts o ∈ Obj = P → Value p ∈ P : Property names r ∈ Registers = R → Value ` ∈ L = N × C : Locations v ∈ Value = Prim × P(L) Figure 3 Simplified abstract domain. 3 Background: The TAJS Analyzer In this section we give a brief introduction to a heavily simplified version of the analysis domain and program representation used in TAJS [11, 2], which lays the foundation for our extensions in the following sections. TAJS is an open-source dataflow analysis tool for JavaScript built as a monotone frame- work [12]. A JavaScript program is represented as a control flow graph for each function, with nodes representing primitive instructions of the different kinds listed in Figure 2. Each instruction operates on registers, which can be thought of as special local variables. For simplicity, we ignore this and receiver objects at calls, and we assume all functions have only one parameter. As an example, the single JavaScript statement y[p] = x[p] is represented as six flow graph nodes as shown in Figure 4. The components of the abstract domain are summarized in Figure 3. A location is a pair of a node and a context. The contexts allow for context sensitivity (using the context-sensitivity strategy described by Andreasen and Møller [2]). The main abstract domain, AnalysisLattice, is a lattice that maps locations to abstract states, where each state contains abstract values of object properties and registers. Objects are modeled using context-sensitive allocation-site abstraction [6, 20], so abstract object addresses are simply locations.4 Functions are special kinds of objects. Abstract values are modeled using a product of a constant-propagation lattice [15] named Prim of primitive values (strings, numbers, etc.) and a powerset lattice of object addresses. The analysis is control sensitive by pruning infeasible dataflow at if nodes. This includes not only eliminating flow along unreachable branches, for example when a branch condition is definitely false [27], but also filtering abstract values based on the branch condition [10, 14]. 4 TAJS models absence/presence of object properties and uses two artificial properties DefaultNumeric and DefaultOther to model properties with unknown numeric/non-numeric names; we ignore that here. ECOOP 2020 16:8 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript n1 : r1 ← y n2 : r2 ← p n3 : r3 ← x n4 : r4 ← p n5 : r5 ← r3 [r4 ] n6 : r1 [r2 ] ← r5 Figure 4 Fragment of a control flow graph, for the single statement y[p] = x[p]. As an example, the JavaScript code if(z) is represented by two primitive instructions, r6 ← z and if(r6 ). In the “true” branch, not only r6 but also z must have the value true.5 To track the connection between r6 and z, a simple intraprocedural must-equals analysis is performed alongside the main dataflow analysis. We leverage this mechanism in Section 5, for example to obtain the information that r2 , r4 , and p must have the same value at the property read operation in Figure 4 (unless a property accessor changes p). To keep Figure 3 simple, we omit the must-equals information in the description of the State lattice. In the following sections, with a slight abuse of notation we let σ(r) denote the value of register r in state σ, and similarly, σ(x) denotes the value of variable x. Also, we use the notation σ(r) := . . . to describe the operation of writing a given value to register r and also to the variables and registers that are equal to r according to the must-equals information. If ` ∈ L is a location representing an object address, we sometimes write ` for the abstract value (⊥, {`}) ∈ Value. Similarly, for abstract values that represent primitive values only, we omit the location sets, for example, "foo" denotes the abstract value ("foo", ∅) ∈ Value. We omit many details of TAJS, including the definitions of the concretizations of the lattice elements, the definitions of the transfer functions for the different instructions, how values of variables are being stored in special activation objects, and how a call graph is built during the analysis. Analyzing full JavaScript also requires reasoning about prototypes, scope chains, implicit type conversions, exceptions, the standard library, property accessors (getters and setters), and much more. It suffices to know that the resulting abstract states soundly overapproximate the possible program behavior [7]. A trace is a concrete execution of the program expressed as a finite sequence of pairs (`, γ) where ` is a location and γ is a concrete state, starting at the program entry point with the initial call context in an empty state. The semantics of a program is defined as a set of traces. The collecting semantics is the program semantics projected onto the program locations: Given a location `, the collecting semantics for `, denoted J`K, is the set of states that appear at ` in the set of traces defined by the program semantics. The analysis result is thus a lattice element X ∈ AnalysisLattice such that J`K is a subset of the concretization of X(`) for all locations ` ∈ L. 5 In actual JavaScript, the value must be truthy, which also includes nonempty strings, nonzero numbers, and objects. B. B. Nielsen and A. Møller 16:9 t ∈ T : Partition tokens o ∈ Obj = P → PartitionedValue r ∈ Registers = R → PartitionedValue pv ∈ PartitionedValue = T ,→ Value Figure 5 Extension of the abstract domain for value partitioning. 4 Value Partitioning To prepare the analysis for value partitioning, we introduce a set T of partition tokens and replace occurrences of Value by PartitionedValue in the abstract domain, as shown in Figure 5. A partitioned value is a partial map from partition tokens to ordinary values. We use the notation [t1 7→ v1 , . . . , tk 7→ vk ] (or set-builder notation like [ti 7→ vi | i = 1, . . . , k]) to denote the partitioned value that maps ti to vi for each i = 1, . . . , k and is undefined for all other partition tokens. The partition tokens play a similar role as in trace partitioning [23], but at the level of abstract values. (We explain the differences between value partitioning and traditional trace partitioning in more detail in Section 7.) A partition token intuitively represents a set of execution traces. The special token any represents all traces, so the partitioned value [any 7→ v] has the same meaning as the ordinary value v in the original abstract domain. As an invariant, all partitioned values we use are defined for the token any.6 We extend partitioned values to be total functions pv : T → Value by defining pv(t) = pv(any) when t∈ / dom(pv).7 Assume X ∈ AnalysisLattice is the result of analyzing a given program, σ = X(`) is the abstract state at some location `, and [. . . , t 7→ v, . . . ] = σ(r) is the partitioned value of some register r. The meaning of such a partitioned value is that for any trace that ends at ` and is in the set of traces represented by t, the concrete value of r is in the concretization of the abstract value v. A covering 8 at a location ` is a set of partition tokens where the union of the sets of traces they represent is the set of all traces that lead to `. This means that if σ(x) = [. . . , t1 7→ v1 , ..., tk 7→ vk , . . . ] where σ = X(`) for some program variable x at location ` where {t1 , . . . , tk } is a covering, then for every concrete state in J`K, the value of x is in the concretization of at least one of the abstract values v1 , . . . , vk . For the initial abstract state at the program entry, all partitioned values use the trivial covering {any}. Now that we have generalized the abstract domain, it is easy to adjust all transfer functions for the different kinds of nodes to operate on partitioned values instead of ordinary values. As an example, the original transfer function for r1 ← r2 ⊕ r3 updates a given abstract state σ by σ(r1 ) := σ(r2 )⊕σ(r3 ) (where ⊕ applied to abstract values works as in constant propagation).9 6 When we define a partitioned value [ti 7→ vi | i = 1, . . . , k] without an any token, an any partition is implicitly created with value v1 t · · · t vk . 7 In trace partitioning terminology, this use of any corresponds to a simple pre-ordering of partition tokens. 8 For formal definitions of the notions of traces and coverings, see Rival and Mauborgne [23]. Basing our approach on partitions instead of coverings (a partition is a covering where all the trace sets are disjoint) could improve precision but would complicate the analysis without much practical benefit. 9 The actual TAJS analysis also models implicit type conversions. ECOOP 2020 16:10 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript T :: = any (Section 4) | valhN, R, Valuei (Section 5.1) | funhF, C, T i (Section 5.2) | typehN, R, Typesi (Section 5.3) Types :: = undefined | null | number | string | boolean | object | array | function | regexp Figure 6 Partition tokens used by property name partitioning, free variable partitioning, and type partitioning. When switching to the domain with partitioned values, we simply replace σ(r2 ) ⊕ σ(r3 ) by [t 7→ pv 2 (t) ⊕ pv 3 (t) | t ∈ dom(pv 2 ) ∪ dom(pv 3 ) where pv 2 = σ(r2 ) and pv 3 = σ(r3 )]. The other transfer functions and least-upper-bound are adapted similarly. A small example can illustrate how partitioning can make the analysis relational. Assume the binary operation is equality, r1 ← r2 == r3 , and that we have two partitions, t1 and t2 , where both registers r2 and r3 have the value 42 in partition t1 , and both have the value "foo" in partition t2 . With partitioning, the value of r1 becomes [t1 7→ true, t2 7→ true] (i.e., definitely true), whereas without partitioning, r2 and r3 both have the value 42|"foo", so the value of r1 becomes AnyBool (i.e., true or false). To get any advantage of the new abstract domain, we of course need to modify specific transfer functions to selectively introduce partition tokens and further exploit the extra information available regarding relational properties between values. We show how that can be accomplished in Section 5. Those mechanisms rely on some general operations for manipulating the partitions in partitioned values. Most importantly, we use an operation ] when introducing new coverings: pv 1 ] pv 2 where pv 1 , pv 2 ∈ PartitionedValue denotes the combined partitioned value. For each token that is only present in one of pv 1 or pv 2 , the new value will be the value for that token, and for each token shared by pv 1 and pv 2 , the new value will be the join of the two respective values. 5 Three Instantiations of Value Partitioning We now present three instantiations of the value partitioning framework. Each of them targets a category of relational properties that are relevant to analysis of JavaScript libraries. Each instantiation introduces a family of partition tokens, as shown in Figure 6, along with some modification of the analysis transfer functions. Each partition token represents a set of traces, as explained in the following. 5.1 Property Name Partitioning The first use of value partitioning is for improving precision at correlated object property read/write operations as in the motivating example. Partition tokens for property name partitioning We introduce a family of partition tokens, valhn, r, vi, where n ∈ N , r ∈ R, and v ∈ Value. Such a token represents the set of traces where at the last occurrence of n, the value of register r is v. In all valhn, r, vi tokens we use in property name partitioning, the node n B. B. Nielsen and A. Møller 16:11 σ(r3 ) ] [valhn, r3 , pi 7→ p | p ∈ propNames(σ(r2 ))] σ(r3 ) := ] [valhn, r3 , otheri 7→ AnyString] if σ(r3 )(any) = AnyString σ(r ) otherwise 3 [valhn, r3 , pi 7→ readProp(σ(r2 )(any), p) | p ∈ propNames(σ(r2 ))] σ(r1 ) := ] [valhn, r3 , otheri 7→ undefined] if σ(r3 )(any) = AnyString [any 7→ readProp(σ(r )(any), σ(r )(any))] otherwise 2 3 Figure 7 Introduction of partitioned values at a dynamic property read node n of the form r1 ← r2 [r3 ]. is a property read node (i.e., of the form r1 ← r2 [r3 ]), the register r is the one holding the property name in that instruction (i.e., r3 in r1 ← r2 [r3 ]), and the value v is a property name (i.e., an element of P ).10 As an example, assume the code from Figure 4 appears inside a loop, and consider the following two traces that both end at n6 : τa = · · · (n1 , γ1a )(n2 , γ2a )(n3 , γ3a )(n4 , γ4a )(n5 , γ5a )(n6 , γ6a ) and τb = · · · (n1 , γ1b )(n2 , γ2b )(n3 , γ3b )(n4 , γ4b )(n5 , γ5b )(n6 , γ6b ) where each “· · · ” is a trace prefix leading from the program entry point to this part of the code, γ1a , . . . , γ6b are concrete states, and τa is a prefix of τb . The last occurrence of n5 (which is the instruction r5 ← r3 [r4 ]) is emphasized in each of the traces. Also assume that the value of the register r4 is "foo" in γ5a and "bar" in γ5b . Note that r4 is the register holding the property name at the n5 instruction. In this situation, the token valhn5 , r4 , "foo"i represents τa but not τb . Dynamic property reads Figure 7 shows the modified transfer function for read-property nodes, r1 ← r2 [r3 ]. The function readProp(v1 , v2 ) looks up the abstract value of properties named v2 in the abstract objects pointed to by v1 in the current state σ.11 Property name partitioning is triggered if the property name is not precise (here modeled as AnyString), so in that case we partition the property name r3 with respect to the properties that appear in the abstract objects pointed to by r2 (expressed as propNames(σ(r2 ))), and perform the property read for each partition to obtain a partitioned value for r1 . We use the artificial abstract value other ∈ Value to represent all other properties; for that partition, the result value becomes undefined.12 If 10 In JavaScript, property names are either strings, which we model in the sub-lattice Prim, or symbols, which can be modeled as special heap locations. 11 Reading an object property is a nontrivial operation in JavaScript because of prototypes, getters, and implicit type conversions. Importantly, the value partitioning mechanism is orthogonal to such JavaScript technicalities. 12 In our implementation we use a more precise string lattice, which allows us to express more precisely that σ(r3 ) for the valhn, r3 , otheri partition is AnyString\propNames(σ(r2 )), i.e., any string except for the property names that are covered by other partitions. See also footnote 3. ECOOP 2020 16:12 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript for each t ∈ chooseCommonCovering(σ(r2), σ(r3 )): writeProp σ(r1 )(any), σ(r2 )(t), σ(r3 )(t) Figure 8 Exploiting partitioned values at a dynamic property write node, r1 [r2 ] ← r3 . the property name r3 is already precise (corresponding to the “otherwise” cases), there is no need to introduce new partitions, so in that case r3 is unmodified and the result value r1 is obtained directly using readProp and the any partition token. Recall that a valhn, r, pi token represents the set of traces where at the last occurrence of n, the value of register r is v. To respect this property we need to remove all existing valhn, _, _i tokens from the abstract state before applying the transfer function for dynamic property reads. (This is safe because every abstract value still has other coverings, in particular {any}.) Notice that for both r3 and r1 , the new partitions use the partition tokens valhn, r3 , pi where n is the read-property node. Evidently, the new partition tokens form a covering. Also, this new transfer function respects the interpretation of the newly added valhn, r, pi tokens, and due to the partitioning, the resulting abstract states maintain the relation between the involved object property names and values. Dynamic property writes Next, we modify the transfer function for dynamic property writes, r1 [r2 ] ← r3 , as shown in Figure 8, to take advantage of the partitionings introduced at dynamic property reads. The function writeProp(v1 , v2 , v3 ) writes v3 to the properties named v2 in the objects referred to by v1 .13 The function chooseCommonCovering finds a covering shared by the property name σ(r2 ) and the value to be written σ(r3 ). (An example is given below.) If multiple such coverings exist, a largest one (i.e., one with the largest number of partition tokens) is selected.14 Recall that the two values always share the {any} covering, which will be used if no other covering exist. When a covering has been chosen, the value is written to the appropriate object property for each partition, thereby exploiting the relational information. In case the {any} covering is chosen, the transfer function behaves as the original version without value partitioning. Example To better understand property name partitioning, we now explain the mechanism in more detail on the example given in Figure 4. Let us assume that σ(p) = [any 7→ AnyString], σ(x) = [any 7→ obj 2 ] and σ(y) = [any 7→ obj 1 ] where in state σ, obj 1 is the location of an empty abstract object and obj 2 is the location of an abstract object with two properties, {foo: 1, bar: 2}. This means when analyzing the read property node r5 ← r3 [r4 ] we have σ(r3 ) = [any 7→ obj 2 ] and σ(r4 ) = [any 7→ AnyString]. Since the property name r4 is 13 We omit the details of how the implementation of writeProp in TAJS handles strong/weak updates, setters, and implicit type conversions. Importantly, the value partitioning mechanism is orthogonal to such JavaScript technicalities. 14 Multiple coverings can arise if, for example, the same property name is used at two different property read operations. We choose the largest covering based on the heuristic that fine-grained coverings lead to higher precision than coarse-grained coverings. The most important consequence of this heuristic is that we avoid the {any} covering if others are available. In case of multiple largest ones, an arbitrary one is selected among them. B. B. Nielsen and A. Møller 16:13 pv ∈ PartitionedValue = T ,→ FPValue fv ∈ FPValue = FunctionPartitions × Value fp ∈ FunctionPartitions = P(T ) AnalysisLattice = C 0 × N → State c ∈ C 0 = FunctionPartitions × C Figure 9 Extensions of the abstract domain for free variable partitioning. imprecise, the first case in each definition in Figure 7 applies, meaning that value partitioning is triggered. Since propNames(σ(r2 )) = {"foo", "bar"}, we update r4 such that σ(r4 ) equals [valhn, r4 , "foo"i 7→ "foo", valhn, r4 , "bar"i 7→ "bar", valhn, r4 , otheri 7→ AnyString], where n is the read property node. Recall from Section 3 that the operation σ(r4 ) := . . . does not only modify r4 but also the must-equals variables and registers, meaning that this partitioned value is also written to r2 and p. The value being read gets the same partitions, such that σ(r5 ) becomes [valhn, r4 , "foo"i 7→ 1, valhn, r4 , "bar"i 7→ 2, valhn, r4 , otheri 7→ undefined]. When reaching the property write operation r1 [r2 ] ← r5 , the state σ contains σ(r2 ) = [valhn, r4 , "foo"i 7→ "foo", valhn, r4 , "bar"i 7→ "bar", valhn, r4 , otheri 7→ AnyString] and σ(r5 ) = [valhn, r4 , "foo"i 7→ 1, valhn, r4 , "bar"i 7→ 2, valhn, r4 , otheri 7→ undefined]. We now apply the transfer function from Figure 8. The two values σ(r2 ) and σ(r5 ) share two coverings: {any} and {valhn, r4 , "foo"i, valhn, r4 , "bar"i, valhn, r4 , otheri}. Since the second covering is largest, that one is picked by chooseCommonCovering(σ(r2 ), σ(r5 )). We therefore perform three writes corresponding to the abstract assignments obj 1["foo"]=1, obj 1["bar"]=2, and obj 1[AnyString]=undefined; notably, the properties foo and bar are not mixed together. 5.2 Free Variable Partitioning We now explain how to leverage value partitioning to gain precision for free variables, such as func in line 9 in the motivating example from Figure 1. Extending the abstract domain The first step is to extend the abstract domain as shown in Figure 9. The Value component in PartitionedValue is replaced by FPValue, which is a product of FunctionPartitions and Value. The component FunctionPartitions is a set of partition tokens, which we use for tracking which partitions the functions described in the Value component may have been declared in. (For instance, for the motivating example from Figure 1, the function declared in lines 7–10 was created in the partitions t01 , t02 , and t03 so the corresponding abstract values become15 ({t01 }, `), ({t02 }, `), and ({t03 }, `), where ` denotes the location for the created closure.) To preserve this information when analyzing calls to such functions, we also augment the set of contexts to include this information (replacing C by C 0 in AnalysisLattice). The FunctionPartitions set is empty for values and contexts that do not use free variable partitioning. 15 These three abstract values are denoted `t01 , `t02 , and `t03 , respectively, in the motivating example in Section 2. ECOOP 2020 16:14 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript pv(t) if t ∈ dom(pv) otherwise if t = funhf, c, t0 i ∧ ⊥ pv(t) = ∃c0 , t00 : c 6= c0 ∧ funhf, c0 , t00 i ∈ dom(pv) pv(any) otherwise Figure 10 Redefining how partitioned values are extended to total functions, exploiting free variable partitioning. Next, we introduce a new kind of partition tokens, and we then describe how elements of FunctionPartitions are created at function expressions and used at read variable nodes. Partition tokens for free variable partitioning We introduce a new kind of partition tokens, funhf, c, ti, where f is a function, c ∈ C 0 is a context, and t ∈ T is a partition token. A trace is represented by such a token if (1) the trace ends at a program location that belongs to a closure that was created when the trace up to that point was a t trace, and (2) that point in the trace is in function f in context c. (For instance, in the motivating example, a trace ending in line 9 where the currently executed closure was created in line 7 at the end of a t1 trace can be represented by funhf, c, t1 i, where f is the function at lines 2–11 and c is the context for the call to that function.) We only allow such partition tokens to appear in abstract values of variables that are declared in f . Intuitively, we use these partition tokens to obtain a form of heap specialization (also called heap cloning or context sensitive heap) [20] for the activation objects of f .16 An important property is that if the abstract value of a variable x declared in a function f contains partition token funhf, c0 , t00 i for some c0 , t00 but not funhf, c, t0 i for any c, t0 where c=6 c0 , then f has not been invoked with context c in any trace represented by funhf, c, t0 i. This means that it is safe to redefine how partitioned values are extended to total functions as shown in Figure 10. The only difference between the new and the original definition from Section 4 is the second case, where ⊥ is returned to indicate that the set of traces for the given partition is empty due to the above mentioned property being satisfied. Function definitions Assume the analysis reaches a function definition node, r1 ← function(· · · ){· · · }, while analyzing a function f in context c, and that the function being defined has free variables x1 , . . . , xn that are declared in f (i.e., as parameters or local variables). Note that f is the function containing the function definition node being analyzed, not the function being defined. Let ` denote the location of the newly created closure according to the original transfer function without free variable partitioning. We now partition both the resulting function value of register r1 and the values of x1 , . . . , xn as shown in Figure 11. First, we use a function chooseCovering that finds a largest covering, denoted LC , among the values of x1 , . . . , xn . (If multiple such coverings exist, an arbitrary one is selected among them, as before.) 16 Local variables and arguments are stored as properties on activation objects, which are created on each invocation. B. B. Nielsen and A. Møller 16:15 LC = chooseCovering(σ(x1 ), . . . , σ(xn )) ( σ(xi ) ] [funhf, c, ti 7→ σ(xi )(t) | t ∈ LC ] if LC ⊆ dom(σ(xi )) σ(xi ) := σ(xi ) otherwise ( [t 7→ ({funhf, c, ti} ∪ fp, `) | t ∈ LC ] if LC ⊆ dom(σ(xi )) for some xi σ(r1 ) := [any 7→ (∅, `)] otherwise Figure 11 Introduction of partitioned values at a function definition node r1 ← function(· · · ){· · · }. For each xi for i = 1, . . . , n, if the current value of xi contains the covering LC , we add funhf, c, ti 7→ σ(xi )(t) to the value of xi for each t ∈ LC . (This evidently respects the meaning of funhf, c, ti tokens informally described in the beginning of the section.) Otherwise, if the current value of xi does not contain LC , we leave xi unmodified. For the result register r1 , we augment the function location ` by the same partition tokens. If at least one free variable has been partitioned (i.e., LC ⊆ dom(σ(xi )) for some xi ), then for each of the partition tokens t ∈ LC , the value of r1 becomes the augmented value ({funhf, c, ti} ∪ fp, `) where fp is the set of function partitions in the current context c. By augmenting the value using the funhf, c, ti token, the information about the partitioning is available when ` is later invoked, which is explained below. (The function partitions fp of the current context describe how the current function was declared in an outer scope, so by inheriting those, the partitioning also works for multiple layers of nested functions.) Otherwise, if none of the free variables have been partitioned, register r1 is assigned the partitioned value [any 7→ (∅, `)], which is equivalent to the original transfer function without free variable partitioning. Function calls At a function call r1 ← r2 (r3 ) where σ(r2 ) is an augmented function value (fp, v) (i.e., fp is a set of partition tokens introduced at function definitions and v refers to the set of closures that may be invoked), we use fp to augment the context for each callee. (The set of augmented contexts C 0 contains the FunctionPartitions component exactly for this purpose.) Assume for simplicity that v refers to a single closure location so we only have one callee. By augmenting the context, when analyzing the body of the callee we retain the information about the partitions where the callee closure was created, which we can exploit when reading its free variables as explained next. Variable reads Figure 12 shows the updated transfer function for read variable nodes r1 ← x, where we read a variable x in a calling context with function partitions fp. The set of function partitions fp tells us which partitions the current closure may have been created in. For this reason, if the abstract value of x contains partition tokens that are also in fp, we can obtain a covering for x by considering only those partition tokens. If there is no such partition token, we just read the value of x as in the original transfer function. ECOOP 2020 16:16 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript ( F any 7→ {σ(x)(t) | t ∈ dom(σ(x)) ∩ fp} if dom(σ(x)) ∩ fp 6= ∅ σ(r1 ) := σ(x) otherwise Figure 12 Exploiting partitioned values at a read variable node, r1 ← x. 32 var o1 = {x: 1, y: 2}; 22 function f(v) { 33 var o2 = {}; 23 return function g() { 34 Object.keys(o1).forEach( 24 return v; 35 function h(p) { 25 } 36 var v = o1[p]; 26 } 37 o2[p] = function j() { 27 38 return v; 28 var foo = f("foo"); 39 } 29 var bar = f("bar"); 40 } 30 41 ); 31 assert(bar() != "foo"); 42 assert(o2.y() != 1); Figure 13 Free variable partitioning Figure 14 Free variable partitioning example with different contexts. example with partitioned argument. As an example, assume σ(x) = [funhf, c, ti 7→ 1, funhf, c0 , t0 i 7→ 2, . . . ] and fp = {funhf, c, ti}. The value of x tells us that x must be a local variable in function f which may have been called in contexts c and context c0 , and that x’s value is 1 or 2, respectively. Since fp = {funhf, c, ti}, we know that the current function is defined inside the lexical scope of f in context c, meaning that the value of x must be 1. Examples To better understand free variable partitioning, we provide two examples. The first example (Figure 13) shows how free variable partitioning can preserve precision when a function is called in multiple contexts, in a way that resembles traditional heap specialization [20]. The second example (Figure 14) shows how free variable partitioning can preserve the precision of free variables partitioned with property name partitioning. In Figure 13, lines 22–26 define a function f that returns a closure, which on invocation returns the argument passed to f. Lines 28 and 29 call f with the arguments "foo" and "bar" and store the returned closures in the variables foo and bar, respectively. Line 31 calls the closure stored in bar and asserts that the resulting value is not the string "foo". The two calls to f are analyzed in different contexts c and c0 (due to the context sensitivity mechanism mentioned in Section 3, as "foo" and "bar" are determinate values). For the invocation bar(), the resulting value is the value of the free variable v in the closure stored in bar. If not using heap specialization, the two concrete activation objects at the two calls to f would be modeled by a single abstract object, so the free variable v would have the imprecise abstract value AnyString. To reason precisely about the assertion in line 31, the analysis has to distinguish the value of v at the two calls. The baseline TAJS analyzer accomplishes this by the use of heap specialization [2], which provides two different abstract activation objects for the calls to f, so the two values "foo" and "bar" are kept separate. B. B. Nielsen and A. Møller 16:17 With free variable partitioning we obtain the same degree of precision as with heap specialization in this situation. Since v is a free variable in the closure created in line 23, we apply the top cases in the transfer functions shown in Figure 11 with LC = {any}. This means that v after the call to f("foo") will have the value [any 7→ "foo", funhf, c, anyi 7→ "foo"] and the value written to the foo variable is ({funhf, c, anyi}, `g ) where `g is the location of the closure created in line 23. For the call to f("bar"), the value for v will similarly be [any 7→ "bar", funhf, c0 , anyi 7→ "bar"] and the value written to bar is ({funhf, c0 , anyi}, `g ). Note the difference in the context part of the fun token (c at the "foo" call and c0 at the "bar" call), since the calls to f are in those two different contexts. The value of v then becomes [any 7→ AnyString, funhf, c, anyi 7→ "foo", funhf, c0 , anyi 7→ "bar"], so that the fun partitions preserve the precise values. Now when analyzing bar(), bar has the value ({funhf, c0 , anyi}, `g ), which means the calling context to the function g is augmented with the set of function partitions {funhf, c0 , anyi} as described above. When reading the free variable v in line 24, we use the first case in the transfer function defined in Figure 12, since dom(σ(x)) ∩ fp is {funhf, c0 , anyi}. This means that the resulting value from the variable read is the value [any 7→ "bar"], so we obtain the same precision as with heap specialization. This first example shows how the free variable partitioning mechanism works and how it relates to heap specialization, but it does not demonstrate any precision improvements compared to the existing TAJS analyzer, which does apply heap specialization. The second example, Figure 14, illustrates a simplified version of how free variable partitioning was used in the motivating example in combination with property name partitioning, which leads to a precision improvement of TAJS. Line 32 defines the object o1 with two properties, and line 33 defines o2 as an empty object. Lines 34–41 iterate over the properties of o1. For each property, it writes a function returning the value of o1[p] to the p property of o2. To prove that the assertion at line 42 always holds, it is critical that the values of v are not mixed together in the iterations. Using property name partitioning at line 36, the value of v becomes [valhn, r, "x"i 7→ 1, valhn, r, "y"i 7→ 2] and the value of p becomes [valhn, r, "x"i 7→ "x", valhn, r, "y"i 7→ "y"], where n is the read property node and r is the register storing the property name. (For clarity we ignore the other partition in this example.) When analyzing the closure creation at line 37, we use the top rules in Figure 11 with LC = {valhn, r, "x"i, valhn, r, "y"i}. This means that v is augmented with the additional partitions [funhh, c, valhn, r, "x"ii 7→ 1, funhh, c, valhn, r, "y"ii 7→ 2], and the value being written to o2[p] is [valhn, r, "x"i 7→ ({funhh, c, valhn, r, "x"ii}, `j ), valhn, r, "y"i 7→ ({funhh, c, valhn, r, "y"ii}, `j )]. Here, `j denotes the location of the closure created in line 37. At the dynamic property write, the property name and value to be written share the covering {valhn, r, "x"i, valhn, r, "y"i}, meaning that the write happens as described in Figure 8, so that o2.x becomes ({funhh, c, valhn, r, "x"ii}, `j ) and o2.y becomes ({funhh, c, valhn, r, "y"ii}, `j ). Now when o2.y is called in line 42, the call to j is augmented with the the set of function partitions {funhh, c, valhn, r, "y"ii}. Therefore when reading the value v in line 38, according to Figure 12 we only read the funhh, c, valhn, r, "y"ii partition. The result of reading v is then [any 7→ 2], so the analysis is precise enough to prove that the assertion at line 42 holds. 5.3 Type Partitioning Value partitioning can also be useful for partitioning values based on their types. Since JavaScript does not have function overloading, it is common to reflectively find the type of an argument, and based on the type run different pieces of code (as in line 3 in Figure 1). ECOOP 2020 16:18 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript σ(r3 ) ] [typehn, r3 , tyi 7→ filter(σ(r3 ), ty) | ty ∈ types(σ(r3 ))] σ(r3 ) := if |types(σ(r3 ))| > 1 σ(r ) otherwise 3 Figure 15 Addition to the transfer function for a call node with one argument, r1 ← r2 (r3 ). filter restricts a partitioned value to represent only values that match the given type, and types returns the possible types of the given partitioned value. This is often done through the use of predicate functions, which are one-parameter functions that return a boolean value. By partitioning the arguments at calls to predicate functions, the analysis becomes able to track the relations between the arguments and the return values, and thereby boost the control sensitivity mechanism (see Section 3) at branches that involve such calls. Since the analysis does not know in advance whether a function returns boolean values, we simply perform this partitioning at all function calls with one argument, without considering what values the function may return. Partition tokens for type partitioning We introduce type partitioning tokens of the form typehn, r, tyi, where n ∈ N is a call node r1 ← r2 (r3 ), r ∈ R is the argument register in n (in this case r3 ), and ty ∈ Types using the set of types shown in Figure 6. Such a token represents the set of traces where the type of r is ty at the last occurrence of n. For example, the traces that reach line 7 in Figure 1 are represented by the token typehn, r, functioni where n is the call to isFunction in line 6 and r is the argument register of that call node. Function calls Figure 15 shows an addition to the transfer function for call nodes, r1 ← r2 (r3 ), to partition the argument value before the call takes place. The first case applies if the argument σ(r3 ) abstractly represents values of multiple types (i.e., |types(σ(r3 ))| > 1, where types returns the set of all the types the given abstract value may have). In this case we introduce a partition typehn, r3 , tyi for each ty ∈ types(σ(r3 )), such that the value in that partition is filter(σ(r3 ), ty), where filter restricts σ(r3 ) to only represent values of type ty. Since all the possible types are represented, the new partitions together form a covering. Recall that a typehn, r, tyi token only represents information about the last occurrence of n in a given trace. To ensure this property we always remove all existing typehn, _, _i tokens from the abstract state immediately before applying the modified transfer function for call node n. Example As an example consider the code in Figure 16, and assume x has the abstract value fun1|obj2 (representing either the function fun1 or the object obj2). Without type partitioning, the result of analyzing the isObj(x) call is the abstract value AnyBool (representing true or false), so both branches are analyzed with x being fun1|obj2; however, in a concrete execution, fun1 will never flow to the “true” branch, and obj2 will never flow to the “false” branch. B. B. Nielsen and A. Møller 16:19 47 function isObj(arg) { 48 if (typeof arg == ’object’) 43 function isObj(arg) { 49 return true; 44 return typeof arg == ’object’; 50 else 45 } 51 return false; 46 if (isObj(x)) { ... } else { ... } 52 } 53 if (isObj(x)) { ... } else { ... } Figure 16 Type partitioning example. Figure 17 Type partitioning example with control dependent relations. By using type partitioning, we partition x before calling the predicate function. In this example let n be the call node and let r be its argument register. Then x be- comes [typehn, r, functioni 7→ fun1, typehn, r, objecti 7→ obj2]. Now when analyzing the body of isObj, the expression typeof arg == ’object’ evaluates to the partitioned value [typehn, r, functioni 7→ false, typehn, r, objecti 7→ true]. When reaching the if branch, control sensitivity ensures that only the object partition flows to the “true” branch (i.e., x’s value becomes [typehn, r, functioni 7→ ⊥, typehn, r, objecti 7→ obj2] in that branch), and only the function partition flows to the “false” branch (i.e., x’s value becomes [typehn, r, functioni 7→ fun1, typehn, r, objecti 7→ ⊥] in that branch). Control dependent relations Predicate functions are sometimes implemented with control dependent relations between the argument and the result, as in the example in Figure 17. The example is contrived but it is not uncommon in predicate functions that the result values appear as the literals true or false in branches. With the type partitioning mechanism described above, the returned values will not be partitioned in this situation, since the partitions in arg do not propagate to the values true and false. To mitigate this issue, we augment the abstract states as shown in Figure 18 to keep track of partitions that must be dead or may be live (represented by the two P(T ) components, respectively). A partition is dead if the set of traces it represents is empty, and it is live otherwise. (We only keep track of the live partitions in coverings where there are any dead partitions.) Since the branch condition typeof arg == ’object’ is analyzed with a partitioned value for arg, by control sensitivity we know that the only traces that can reach the “true” branch are those represented by the object partition, so we record that typehn, r, objecti is live and typehn, r, functioni is dead in that branch, and conversely in the other branch. To exploit this information, we also update the transfer function for constants, r1 ← c, as shown in Figure 19. Basically, it assigns ⊥ to all dead partitions and the constant c to all live partitions. If there are no dead partitions, it behaves as usual, where the constant is written to the any partition. When the analysis reaches true (line 49), we obtain the partitioned value [typehn, r, functioni 7→ ⊥, typehn, r, objecti 7→ true], and similarly when analyzing false (line 51) we get [typehn, r, functioni 7→ false, typehn, r, objecti 7→ ⊥]. The join of these two values is [typehn, r, functioni 7→ false, typehn, r, objecti 7→ true], which becomes the result of isObj(x). Due to the control sensitivity mechanism, only obj2 then flows to the “true” branch, and only fun1 flows to the “false” branch in line 53. ECOOP 2020 16:20 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript State 0 = State × P(T ) × P(T ) Figure 18 Abstract states updated to keep track of dead and live partitions. [t 7→ c | t ∈ livePartitions(σ)] ] [t 7→ ⊥ | t ∈ deadPartitions(σ)] σ(r1 ) := if deadPartitions(σ) 6= ∅ [any 7→ c] otherwise Figure 19 Updated transfer function for constant nodes, r1 ← c, for improved type partitioning. 6 Evaluation We have implemented the value partitioning framework (Section 4) and the three instantiations (Section 5) on top of TAJS v0.24. Implementing the general framework in TAJS required 900 lines of code, however most of this is boilerplate code for lifting operations on ordinary abstract values to also work on partitioned values. With the general framework in place, instantiations are easy to implement: property name partitioning (Section 5.1), free variable partitioning (Section 5.2), and type partitioning (Section 5.3) required only around 230, 250, and 60 lines of code, respectively. We disable TAJS’s for-in specialization technique, since it is subsumed by property name partitioning.17 We refer to our new analysis tool as TAJSValPar .18 Using this tool we evaluate our techniques by answering the following research questions: RQ1 How does TAJSValPar compare to existing state-of-the-art analyses for JavaScript? RQ2 What are the effects of the three different instantiations of value partitioning? All our experiments are conducted on an Ubuntu machine with a 2.6 GHz Intel Xeon E5-2697A CPU running a JVM with 10 GB RAM. 6.1 RQ1: Comparison with State-Of-The-Art Analyses We start by comparing TAJSValPar against the current state-of-the-art analyses for JavaScript: the baseline TAJS analyzer with static determinacy [2], TAJSVR [26] with demand-driven value refinement, and the CompAbs analyzer [16] based on the SAFE analyzer [17]. We use the same benchmarks as those used in the evaluation of TAJSVR , which is the most recent related work. Micro benchmarks We first evaluate TAJSValPar against a small collection of micro benchmarks that capture some of the main challenges that appear in analysis of modern JavaScript libraries and are used in previous work [16, 26]. The benchmarks all contain dynamic read/write pairs that 17 The motivation for introducing for-in specialization in [2] was to reason about correlated read/write pairs inside for-in loops. This relational information is now provided by property name partitioning. 18 TAJSValPar : TAJS with Value Partitioning B. B. Nielsen and A. Møller 16:21 Table 1 Micro-benchmarks that check how state-of-the-art analyses handle various dynamic read/write pairs that represent typical challenges in JavaScript library code. A 7 indicates that the analysis mixes together the properties of the object being manipulated, while a X indicates that it is sufficiently precise to keep them distinct. The CF, CG, AF, and AG benchmarks are drawn directly from [16], while M1, M2, and M3 are drawn directly from [26]. Benchmark TAJS CompAbs TAJSVR TAJSValPar CF X X X X CG X X X X AF 7 X X X AG 7 X X X M1 7 7 X X M2 7 7 X X M3 7 7 X X are variations of the pattern shown in the introduction and the motivating example. The results of the comparison are shown in Table 1. For these benchmarks, a test succeeds if it avoids mixing together properties in the dynamic read/write pairs. The first two examples, CF and CG, are loops where the static analyses have enough information to be able to unroll all the iterations and thereby analyze the read/write patterns with precise property names. For CF, property name partitioning in TAJSValPar gives the same degree of precision without loop unrolling. AF and AG are loops where the static analyses are incapable of obtaining a precise value for the property name used in the dynamic read/write pairs. TAJS fails to analyze these, but CompAbs detects the pattern syntactically and therefore applies trace partitioning to analyze the code precisely. TAJSVR also succeeds on these tests, because its backwards abstract interpreter is capable of providing the necessary relational information. In comparison, TAJSValPar can reason about the relational information on its own. Both TAJS and CompAbs fail on the last three tests (M1, M2, and M3). CompAbs fails on M1 and M3 because it does not apply partitioning due to the fragility of syntactic patterns, and it fails on M2 because the partitioning does not provide the necessary precision about free variables. Again, TAJSVR can analyze them all, since the backwards abstract interpreter is powerful enough to reason about all the cases, whereas TAJSValPar successfully preserves the relational properties by the use of value partitioning. These results demonstrate that for these benchmarks, TAJSValPar is capable of providing comparable precision to the demand-driven value refinement technique without the need for a complicated backwards analysis, and provides better precision than the other analyses. Library benchmarks The next set of benchmarks is taken from the evaluation of TAJSVR and consists of small test cases for popular real-world libraries. The libraries include the widely used functional utility library Underscore (which has more than 20 000 dependents in npm) v1.8.3 with 1 548 LoC and the most depended-upon package Lodash (more than 115 000 dependents). We analyze both Lodash3 (v3.0.0, 10 785 LoC) and Lodash4 (v4.17.10, 17 105 LoC), since their code bases are substantially different and therefore pose distinct challenges for static analysis. ECOOP 2020 16:22 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript Table 2 Analysis results for real-world benchmarks (from [26]). For each group of benchmarks and for each of the four analyzers, we show the number of tests that are analyzed successfully and (in parentheses) the average analysis time per successful test. Benchmark group TAJS CompAbs TAJSVR TAJSValPar Underscore (182 tests) 0 (-) 0 (-) 173 (2.9s) 173 (2.7s) Lodash3 (176 tests) 7 (2.4s) 0 (-) 172 (5.5s) 173 (5.3s) Lodash4 (306 tests) 0 (-) 0 (-) 266 (24.7s) 289 (26.3s) Prototype (6 tests) 0 (-) 2 (23.1s) 5 (97.7s) 5 (34.1s) Scriptaculous (1 tests) 0 (-) 1 (62.0s) 1 (236.9s) 1 (55.2s) jQuery (71 tests) 3 (16.0s) 0 (-) 3 (13.5s) 3 (20.4s) The other libraries, Prototype v1.7.2, Scriptaculous v1.9.0, and jQuery v1.10,19 are popular libraries for client-side web programming. The analysis results are shown in Table 2. We classify an analysis of a benchmark as successful if it terminates within 5 minutes and the analysis result to our knowledge is sound. In particular, an analysis run is considered a failure if the analysis result does not have dataflow to the ordinary exit of the program. (All the tests pass in normal execution, so an analysis result is obviously unsound if there is no dataflow to the ordinary exit.) To increase confidence in the soundness of the analysis results for TAJSValPar , we apply thorough soundness testing as described at the end of this section. Increasing the time budget does not help for these benchmarks: as reported previously for JavaScript analysis tools, critical precision losses tend to cause a proliferation of spurious dataflow that drastically increases analysis time and renders the analysis results useless [26, 11, 22, 16]. The results for TAJSValPar are comparable to those of TAJSVR , which outperforms the other analyzers. TAJSValPar succeeds in analyzing all the benchmarks that TAJSVR can handle, plus 24 more (one Lodash3 test and 23 Lodash4 tests). Note the substantial improvement for the Lodash4 tests: the number of Lodash4 tests that are not analyzed successfully is reduced from 40 to 17. None of the analyzers do well on the jQuery benchmarks; a preliminary manual study shows that the reasons are unrelated to relational analysis. The results are as expected, since property name partitioning and free variable partitioning are alternative techniques to provide the relational information that TAJSVR obtains from its demand-driven value refinement. Furthermore, value partitioning is triggered more often during the analysis, which means that the precision improvements are not limited to the few critical cases where value refinement is triggered. On top of this, type partitioning provides some additional precision beyond the capabilities of TAJSVR . Comparing the performance between TAJSValPar and TAJSVR , the most significant differences are for the Prototype and Scriptaculous benchmarks. TAJSValPar is around 3–4 times faster than TAJSVR , which is mainly because property name partitioning makes the for-in specialization technique in TAJS obsolete. For Underscore and Lodash3, TAJSValPar is slightly faster than TAJSVR . This is encouraging, because analyzing dynamic property writes as the one in line 7 in Figure 1 is more expensive in TAJSValPar than in TAJSVR . In TAJSVR such an operation is handled as a single imprecise write (since the precision is recovered on demand), whereas TAJSValPar performs the write for each property that is copied. To soundly handle setters, all the writes happen in different states that are 19 This is the version of jQuery used in [2]. Note that [16] used the older v1.4.4. B. B. Nielsen and A. Møller 16:23 subsequently joined together, which causes TAJSValPar to spend some extra time at such writes. Since the analysis time is nevertheless similar, we can conclude that value partitioning is cheaper for analyzing other parts of the libraries. For Lodash4 and jQuery, TAJSVR is slightly faster than TAJSValPar . For Lodash4, the main reason is the handling of dynamic property writes, and for the jQuery benchmarks, type partitioning adds little performance overhead as seen in Table 3. Precision Previous work [2, 22, 26] established that type analysis and call-graph construction are useful metrics for measuring the precision of an analysis for JavaScript, and therefore we use these metrics to evaluate the analysis precision of TAJSValPar . All locations are treated context-sensitively in these measurements, meaning that we count the same location once for each reachable context. We count the number of possible types for the resulting value in each variable or property read and find that in 99.19% of the reads, a single unique type is read, with the average number of types being 1.02. For measuring precision of the call-graph construction, we measure the number of call-sites with unique callees, and find this number to be 99.95% of all call-sites. These numbers show that when the analysis succeeds, it does so with very high precision. Soundness Formally proving soundness of the three variants of value partitioning is out of scope of this paper, however, we will informally justify that the general approach is sound. Since general trace partitioning is known to be sound, it suffices to argue that the precision gained by value partitioning is equivalent to that obtained through trace partitioning. The key reason why this holds for property name partitioning and type partitioning is that the partition tokens represent the last occurrence of some node, meaning that if two values share partitions, they represent information about the same execution traces. This means that we could (if ignoring performance) instead have applied traditional trace partitioning, with exactly the same partition tokens and at the same nodes, resulting in the same precision. (For further discussion about the connection between value partitioning and trace partitioning, see Section 7.) Similarly for free variable partitioning, since the partitions are only allowed on activation objects, the precision is never higher than what would be obtained using heap specialization (where each partition would be represented by a distinct abstract activation object), and therefore soundness follows from soundness of heap specialization. Furthermore, to increase confidence in the soundness of our implementation, all the TAJSValPar results have been thoroughly soundness tested [3]. This means that the analysis results overapproximate all the dataflow facts that have been observed during concrete executions of the analyzed benchmarks. For every variable and property read observed concretely, we have checked that the concrete value is in the concretization of the corresponding abstract value in the analysis results, and similarly for property writes and function calls. All our benchmarks except one pass in total more than 7.6 million soundness tests. The one benchmark that fails is a Lodash4 test, which uses ES6 iterators in combination with Arrays.from, which is not fully supported in the latest version of TAJS and is unrelated to the use of value partitioning. ECOOP 2020 16:24 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript Table 3 Analysis results for real-world benchmarks (from [26]) using different instantiations of value partitioning. “None” is without value partitioning, “P” is with property name partitioning, “P + FV” is with property name and free variable partitioning, and “F + PV + T” is with property name, free variable, and type partitioning. Benchmark group None P P + FV P + FV + T Underscore (182 tests) 0 (-) 149 (2.0s) 173 (2.5s) 173 (2.7s) Lodash3 (176 tests) 7 (2.4s) 167 (4.7s) 173 (5.1s) 173 (5.3s) Lodash4 (306 tests) 0 (-) 268 (16.8s) 274 (27.7s) 289 (26.3s) Prototype (6 tests) 0 (-) 0 (-) 5 (32.7s) 5 (34.1s) Scriptaculous (1 tests) 0 (-) 0 (-) 1 (53.1s) 1 (55.2s) jQuery (71 tests) 3 (16.0s) 3 (15.2s) 3 (16.5s) 3 (20.4s) 6.2 RQ2: Effects of the Three Instantiations We now investigate how much each of the three uses of value partitioning contributes to the results reported in the previous section. The results from running our analysis with only some instantiations enabled can be seen in Table 3. The column “P” is with only property name partitioning enabled; we see that it is sufficient for analyzing many of the Underscore and Lodash test cases, but not for any of the Prototype or Scriptaculous test cases. (Without property name partitioning but with the other two instantiations enabled, the analysis is not able to analyze more benchmarks than TAJS.) The column “P + FV” uses both property name partitioning and free variable partitioning. Also enabling free variable partitioning makes the analysis capable of analyzing many additional benchmarks: more Underscore and Lodash test cases, as well as some Prototype and Scriptaculous test cases. Compared to only property name partitioning, the analysis times are higher (for the reason discussed above regarding additional state joins). The last column “P + FV + T” is with all instantiations enabled and therefore contains the same numbers as shown in Table 2. We see that type partitioning enables the analysis of 15 additional Lodash4 tests, without significantly increasing the analysis time. We conclude that all three instantiations contribute to the results, where property name partitioning is the most important one, followed by free variable partitioning and then type partitioning. (TAJS already performs filtering at branches, as mentioned in Section 3; without that feature the effect of type partitioning would likely be larger.) 7 Related Work Trace partitioning Value partitioning can be viewed as a variant of trace partitioning [23] as explained in Sections 1, 2 and 4, but there are some important differences. Changing the original abstract domain in Section 4 to support traditional trace partitioning can be done by replacing L → State by L → T → State, so that an abstract state is maintained for each partition, at every location. Thus, different locations can partition the abstract states differently. Value partitioning instead has only one abstract state per location but partitions the individual abstract values, which adds an additional degree of flexibility: different parts of each abstract state can be partitioned differently. In particular, for the large parts of the states where we B. B. Nielsen and A. Møller 16:25 are not interested in relational information, we can use the {any} partitioning,20 while for the important registers and object properties, we can have nontrivial partitions. With traditional trace partitioning, the normal transfer functions are applied for each partition, which causes redundant computations because of the similarities between the different partitions21 ; with value partitioning, we only pay a price for partitioning at operations that involve abstract values with nontrivial partitions. This is the main reason for the low overhead of the technique. Another difference is that the partition tokens in traditional trace partitioning are actually lists of “directives” (the language of directives used by Rival and Mauborgne [23] is similar to our language of tokens in Figure 6), which can lead to a combinatorial explosion. By partitioning at the level of values and allowing multiple coverings in each partitioned value, we avoid the need to maintain such combinations. Relational analysis Traditional techniques for achieving relational analysis, as exemplified by the octagon abstract domain [19], focus on numeric relations, such as, linear inequalities. To reduce the cost of this approach, a syntactic pre-analysis called variable packing is typically used for partitioning the set of program variables, and one octagon is then used for each pack instead of tracking all possible combinations of inequalities. This kind of partitioning is reminiscent of value partitioning, but with the important difference that variable packing and octagons operate on sets of program variables whereas value partitioning works on individual abstract values. In our work with analysis of JavaScript libraries, we have not encountered a critical need for tracking numeric relations. The well-known analyzer Astrée [4] applies not only trace partitioning and octagons, but also a decision tree abstract domain that is used for tracking relations between booleans and numerical variables that affect control flow. That technique has some similarities with our type partitioning mechanism but relies on variable packing to avoid combinatorial explosions, whereas type partitioning uses the more lightweight value partitioning technique in combination with the existing control sensitivity mechanism of TAJS. The main purpose of value partitioning is to be able to reason about relations between different parts of the abstract state (i.e., program variables and registers) at the various program points. Some literature uses the term relational analysis with a slightly different meaning: to relate information across program points, typically relations between the entry and exits of functions [8, 5]. Static analysis for JavaScript Through the last decade, several static analyzers for JavaScript have been developed, including WALA [25, 24, 28], SAFE [17, 22], JSAI [13], and TAJS [11, 2, 26]. Although we focus on TAJS, the designs of SAFE and JSAI are reasonably similar, so we believe value partitioning could also be incorporated into those tools with little effort. As discussed in the introduction, much work has been put into improving precision of the analyses through different kinds of context sensitivity and elaborate abstract domains. The techniques include parameter sensitivity and heap context sensitivity [2], loop unrolling [22], 20 In our experiments, 99.4% of all abstract values have the trivial {any} partitioning. 21 This was shown experimentally in the work on TAJSVR [26, Section 7.1]. ECOOP 2020 16:26 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript and syntactic patterns for detecting correlated read/write pairs and guiding context sensi- tivity [25]. Other works have explored more expressive string abstractions to reason more precisely about property names in dynamic property accesses [18, 1, 21]. Our abstract domain extension for value partitioning has few assumptions about the underlying abstract domain, so most of these techniques can be combined with value partitioning. Despite such precision improvement techniques, imprecision is inevitable, and only a few techniques have been designed to handle dynamic property accesses with imprecise property names, most importantly, CompAbs-style trace partitioning [16] and demand-driven value refinement [26]. Previous work has shown that demand-driven value refinement enables analysis of many more challenging benchmarks than CompAbs-style trace partitioning (as also discussed in Section 6), and that the trace partitioning approach causes a large amount of redundant computation [26, Section 7.1]. The fundamental drawback of demand-driven value refinement is that it requires a separate backwards abstract interpreter for not only the entire JavaScript language but also the standard library. The backwards abstract interpreter of TAJSVR is not simply the dual of TAJS but works goal-directed and with its own abstract domain based on intuitionistic separation logic. In contrast, value partitioning directly leverages the existing forward analyzer and thereby supports both the JavaScript language and the standard library essentially for free, which makes this approach substantially easier to develop and maintain. Furthermore, value partitioning is more general (for example, it enables type partitioning), and the three instantiations we have presented lead to better precision (for the Lodash4 tests). The HOO (heap with open objects) abstract domain [9] is a relational abstraction that is designed to reason more precisely about abstract objects whose properties cannot be known statically. That approach is highly expressive but not scalable to real-world JavaScript libraries as those considered in Section 6. 8 Conclusion We have presented value partitioning, a static analysis technique for reasoning about relational properties. It is a lightweight alternative to traditional trace partitioning techniques that allows relational information to be incorporated into the abstract values instead of requiring separate abstract states for the partitions. We have proposed three instantiations of value partitioning in JavaScript analysis: property name partitioning, free variable partitioning, and type partitioning, which enable precise reasoning for dynamic read/write pairs, free variables, and predicate functions, respectively. The experimental results show that extending the TAJS analyzer with the three variants of value partitioning enables precise and efficient analysis of complex JavaScript libraries including Lodash and Underscore, thereby outperforming a state-of-the-art technique that relies on trace partitioning and without requiring a complicated backwards analysis. For the libraries considered in this study, property name partitioning has the largest effect among the proposed variants. An interesting direction for future research is to investigate whether some of the traditional context sensitivity strategies used in TAJS and other JavaScript analyzers can be reformulated as new value partitioning instantiations, to make analysis faster while retaining precision. B. B. Nielsen and A. Møller 16:27 References 1 Roberto Amadini, Alexander Jordan, Graeme Gange, François Gauthier, Peter Schachte, Harald Søndergaard, Peter J. Stuckey, and Chenyi Zhang. Combining string abstract domains for JavaScript analysis: An evaluation. In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, volume 10205 of Lecture Notes in Computer Science, pages 41–57, 2017. 2 Esben Andreasen and Anders Møller. Determinacy in static analysis for jQuery. In Proc. ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pages 17–31, 2014. 3 Esben Sparre Andreasen, Anders Møller, and Benjamin Barslev Nielsen. Systematic approaches for increasing soundness and precision of static analyzers. In Proceedings of the 6th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis, SOAP@PLDI 2017, Barcelona, Spain, June 18, 2017, pages 31–36, 2017. 4 Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. A static analyzer for large safety-critical software. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, San Diego, California, USA, June 9-11, 2003, pages 196–207. ACM, 2003. 5 Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. Compositional shape analysis by means of bi-abduction. J. ACM, 58(6):26:1–26:66, 2011. 6 David R. Chase, Mark N. Wegman, and F. Kenneth Zadeck. Analysis of pointers and structures. In Proceedings of the ACM SIGPLAN’90 Conference on Programming Language Design and Implementation (PLDI), White Plains, New York, USA, June 20-22, 1990, pages 296–310. ACM, 1990. 7 Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’77, pages 238–252, New York, NY, USA, 1977. ACM. 8 Patrick Cousot and Radhia Cousot. Modular static program analysis. In Compiler Construction, 11th International Conference, CC 2002, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings, volume 2304 of Lecture Notes in Computer Science, pages 159–178. Springer, 2002. 9 Arlen Cox, Bor-Yuh Evan Chang, and Xavier Rival. Automatic analysis of open objects in dynamic language programs. In Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, pages 134–150, 2014. 10 Arjun Guha, Claudiu Saftoiu, and Shriram Krishnamurthi. Typing local control and state using flow analysis. In Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, volume 6602 of Lecture Notes in Computer Science, pages 256–275. Springer, 2011. 11 Simon Holm Jensen, Anders Møller, and Peter Thiemann. Type analysis for JavaScript. In Proc. 16th International Static Analysis Symposium, pages 238–255, 2009. 12 John B. Kam and Jeffrey D. Ullman. Monotone data flow analysis frameworks. Acta Inf., 7(3):305–317, September 1977. 13 Vineeth Kashyap, Kyle Dewey, Ethan A. Kuefner, John Wagner, Kevin Gibbons, John Sarracino, Ben Wiedermann, and Ben Hardekopf. JSAI: a static analysis platform for JavaScript. In Proc. 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 121–132, 2014. ECOOP 2020 16:28 Value Partitioning: A Lightweight Approach to Relational Static Analysis for JavaScript 14 Vineeth Kashyap, John Sarracino, John Wagner, Ben Wiedermann, and Ben Hardekopf. Type refinement for static analysis of JavaScript. In DLS’13, Proceedings of the 9th Symposium on Dynamic Languages, part of SPLASH 2013, Indianapolis, IN, USA, October 26-31, 2013, pages 17–26. ACM, 2013. 15 Gary A. Kildall. A unified approach to global program optimization. In Conference Record of the ACM Symposium on Principles of Programming Languages, Boston, Massachusetts, USA, October 1973, pages 194–206. ACM Press, 1973. 16 Yoonseok Ko, Xavier Rival, and Sukyoung Ryu. Weakly sensitive analysis for JavaScript object-manipulating programs. Softw., Pract. Exper., 49(5):840–884, 2019. 17 Hongki Lee, Sooncheol Won, Joonho Jin, Junhee Cho, and Sukyoung Ryu. SAFE: formal specification and implementation of a scalable analysis framework for ECMAScript. In Proc. International Workshop on Foundations of Object Oriented Languages, 2012. 18 Magnus Madsen and Esben Andreasen. String analysis for dynamic field access. In Proc. 23rd International Conference on Compiler Construction, volume 8409 of Lecture Notes in Computer Science. Springer, 2014. 19 Antoine Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31–100, 2006. 20 Erik M. Nystrom, Hong-Seok Kim, and Wen-mei W. Hwu. Importance of heap specialization in pointer analysis. In Proceedings of the 2004 ACM SIGPLAN-SIGSOFT Workshop on Program Analysis For Software Tools and Engineering, PASTE’04, Washington, DC, USA, June 7-8, 2004, pages 43–48. ACM, 2004. 21 Changhee Park, Hyeonseung Im, and Sukyoung Ryu. Precise and scalable static analysis of jquery using a regular expression domain. In Proceedings of the 12th Symposium on Dynamic Languages, DLS 2016, pages 25–36, New York, NY, USA, 2016. ACM. 22 Changhee Park and Sukyoung Ryu. Scalable and precise static analysis of JavaScript applica- tions via loop-sensitivity. In Proc. 29th European Conference on Object-Oriented Programming, pages 735–756, 2015. 23 Xavier Rival and Laurent Mauborgne. The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst., 29(5), August 2007. 24 Max Schäfer, Manu Sridharan, Julian Dolby, and Frank Tip. Dynamic determinacy analysis. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, WA, USA, June 16-19, 2013, pages 165–174. ACM, 2013. 25 Manu Sridharan, Julian Dolby, Satish Chandra, Max Schäfer, and Frank Tip. Correlation tracking for points-to analysis of JavaScript. In Proc. 26th European Conference on Object- Oriented Programming, 2012. 26 Benno Stein, Benjamin Barslev Nielsen, Bor-Yuh Evan Chang, and Anders Møller. Static analysis with demand-driven value refinement. Proceedings of the ACM on Programming Languages (PACMPL), 3:140:1–140:29, 2019. 27 Mark N. Wegman and F. Kenneth Zadeck. Constant propagation with conditional branches. ACM Trans. Program. Lang. Syst., 13(2):181–210, 1991. 28 Shiyi Wei, Omer Tripp, Barbara G. Ryder, and Julian Dolby. Revamping JavaScript static analysis via localization and remediation of root causes of imprecision. In Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2016, Seattle, WA, USA, November 13-18, 2016, pages 487–498. ACM, 2016.
Authors Anders Møller Benjamin Barslev Nielsen
License CC-BY-3.0