{'fraction_non_alphanumeric': 0.04170599074198912, 'fraction_numerical': 0.0056626668464338685, 'mean_word_length': 4.738009283135637, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
So You Want to Analyze Scheme Programs With Datalog?

Static analysis approximates the results of a program by examining only its syntax. For example, control-flow analysis (CFA) determines which syntactic lambdas (for functional languages) or (for object-oriented) methods may be invoked at each call site within a program. Rich theoretical results exist studying control flow analysis for Scheme-like languages, but implementations are often complex and specialized. By contrast, object-oriented languages (Java in particular) enjoy high-precision control-flow analyses that scale to thousands (or more) of lines of code. State-of-the-art implementations (such as DOOP on Souffl\'e) structure the analysis using Horn-SAT (Datalog) to enable compilation of the analysis to efficient implementations such as high-performance relational algebra kernels. In this paper, we present an implementation of control-flow analysis for a significant subset of Scheme (including set!, call/cc, and primitive operations) using the Souffl\'e Datalog engine. We present an evaluation on a worst-case term demonstrating the polynomial complexity of our m-CFA and remark upon scalability results using Souffl\'e.


INTRODUCTION
Static analysis is a technique to explicate properties of a program's behavior via inspecting only the program's source code (without executing the program) [13]. There exist many frameworks for constructing program analyses, e.g., Cousot and Coust's abstract interpretation [5]. A static analysis is sound when it is strictly conservative in the sense that any true program behavior is reported (at least approximately) as a result of the analysis. Unfortunately-due to the halting problem-no terminating static analysis may be both sound and complete (all reported results represent true behavior). While static analyses may be constructed using arbitrary degrees of precision (e.g., via instrumentation-based polyvariance [7]) in principle, in practice balancing precision and complexity while retaining soundness requires significant engineering effort [2].
A central challenge in analyzing Scheme programs is control-flow analysis: for each callsite, which syntactic lambdas (in which contexts, for a context-sensitive analysis) may be invoked? This problem is simple in procedural languages (which include only direct control-flow), but challenging for higher-order languages, as data-flow and control-flow must be performed simultaneously. Shivers defined the -CFA family of increasingly-precise control-flow analyses for Scheme [16]. However, as Shivers notes, uniform -CFA quickly becomes intractable for the case > 0, even for reasonably-sized programs [15]. In fact, Van Horn and Mairson later showed that -CFA is EXPTIME-complete [18].
Compared to Scheme, significant engineering work has been expended into whole-program analysis for object-oriented languages, particularly Java [1,3,9,14]. This has culminated in stateof-the-art systems such as DOOP, whose analysis is written in Datalog for subsequent compilation to efficient relational algebra kernels implemented via C++ [3]. Systems such as DOOP scale to large (multi-thousand line) codebases even when context-sensitivity is considered. This would appear at odds with Van Horn and Mairson's result that -CFA is EXPTIME-complete. To resolve this paradox, Might et al. show that the degenerative closure structure of object-oriented languages (analogous to the difference between flat and linked closures), context-sensitive control-flow analyses of object-oriented languages is PTIME [11]. The authors also present -CFA, a technique to analyze arbitrary higher-order languages using flat closures to achieve polynomial complexity.
While the techniques for analyzing object-oriented languages using Datalog are well understood, we are aware of no existing presentation illustrating how Datalog may be used to implement the analysis of Scheme. We find this particularly surprising, as we believe the extreme efficiency of modern Datalog engines may prove a key enabling technology to tackle the inherent complexity of higher-order languages.
In this paper, we present a systematic approach for deriving a Datalog-based implementation of control-flow analysis for Scheme-like languages. Key to our approach is the formulation of the analysis via the abstracting abstract machines (AAM) methodology of Van Horn and Might [19]. We present how this formulation may be translated to Datalog, overcoming several key obstacles unique to Scheme. To evaluate our approach, we implemented an analysis of a significant subset of Scheme including multi-argument lambdas, conditional control-flow, builtins, and first-class continuations (call/cc). In section 3, we present a formalization of this language (noting how our choices anticipate a Datalog implementation) via the AAM approach, following in section 4 with its corresponding Datalog transliteration (we plan to the implementation of our analysis opensource). We validated (manually, via inspection) the correctness of our analysis and in section 5 present the results of a set of experiments benchmarking our implementation of -CFA for our subset of Scheme.

BACKGROUND AND RELATED WORK
In this section, we sketch several key background concepts that underlie our abstract semantics in Section 3 and subsequent Datalog implementation in Section 4.

Program Analysis and Abstract Interpretation
Kildall first introduced dataflow analysis (of flowchart-style programs in the style of Floyd [6]) to approximate static program behavior for the purpose of compile-time optimization [10]. A central idea of Kildall's work was using a lattice to impose an ordering on analysis results and ensure termination via the finiteness of said lattice. Cousot and Cousot later generalized Kildall's ideas to define the abstract interpretation of a program. Abstract interpretation allows relating an arbitrary pair of lattices, typically a concrete state space (Σ) and its abstraction (Σ), along with a pair, ( , ), of (adjunctive) mappings between them for abstraction ( ) and concretization ( ). Using this abstraction alongside a collecting semantics allows iterating a program analysis to some fixedpoint in an arbitrary lattice of abstract results. Assuming this lattice of results is of finite height, the collecting semantics (and therefore analysis) will necessarily terminate via Tarski's fixpoint theorem [17].
We elide a complete presentation of abstract interpretation; there exist several expository texts including those by Miné [12] and Nielsen and Nielsen [13].

Control Flow Analysis
Languages such as C do not include indirect control flow. Determining control flow (and also data flow) is simple for these languages, as control is syntactically-apparent. In scheme, it is more difficult to tell which values flow to a particular variable because of the pervasive use of higherorder functions.
Consider the following Scheme code: Deciding which branch of the if is taken depends on (at least) the values that flow to a and b. Similarly, to understand data flow, we also must know control flow: knowing which value flows to h requires reasoning about the if's control flow. The key is to compute both simultaneously. As the computation continues, data flow information is fed to create a control-flow graph (CFG) on-the-fly, and the new CFG is used to find new data-flow. This is a central idea in the original formulation of -CFA by Shivers [16], though presentations can also be found elsewhere [12,13].

Abstract Abstract Machines
Might and Van Horn presented the Abstracting Abstract Machines (AAM) approach to abstract interpretation for functional languages [19]. The key insight in their work is to redirect all sources of recursion in the analysis through a store which may be finitized by construction. Using this approach, an abstract semantics may be derived from an abstract machine specifying a concrete semantics. The AAM-based approach can compute any type of CFA, and encompasses a broad array of analysis precision including, e.g., object-sensitivity [7]. The machine described in this paper utilizes -CFA [11], a variant of -CFA that uses flat closures.

Datalog
Datalog is a bottom-up logic programming language largely based on Horn-SAT. We refer the reader to the exposition of Ceri et al. for a detailed description of Datalog [4]. Datalog programs consist of a set of Horn clauses of the form ( 0 , ...) ← ( 0 , ...) ∧ ... ∧ ( 0 , ...). To evaluate these programs, an extensional database (EDB) is provided as input specifying a set of initial facts. A Datalog engine then runs the rules to a fixed-point to produce an output database. The following example computes the cousin relation from the EDB relations of parent and sibling. cousin(a, c) :-parent(a, p), sibling(p, q), parent(c, q).
Relations can be recursive. Calculating ancestry is simple. The base case shows that a parent is trivially an ancestor, but a parent of an ancestor is also an ancestor: ancestor(p, a) :-parent(p, a). // If p already has some ancestor a, // the parent b of a is also an ancestor of p. ancestor(p, b) :-ancestor(p, a), parent(a, b).

Syntactic Classes
op ∈ Prim The set of primitives Many famous papers use a significant subset of scheme, perhaps too small for useful realworld analyses. Might et al. 's m-CFA paper uses a variant of the CPS lambda calculus with multiargument functions [11]. Shivers' original work on CFA utilized a CPS subset without conditionals or mutation, instead relying on primitives [16]. Van Horn et al. 's original Abstracting Abstract Machines adds mutation, conditionals, and first order continuations, but does not include multiargument lambdas, which is a crucial component of CFA [19]. Each of these leaves out important components which are required to build analyses on real languages.
In Figure 1, we separate complex from atomic expressions. We also include a variety of useful syntax such as mutation through set! expressions, let bindings, and the higher order control flow operator, call/cc. Conditional expressions and primitives are also highly important for writing meaningful examples. We support binary primitives, which are needed to analyze real scheme programs. Primitive ops include recursive data (i.e. lists), mathematical, and logical operations.
Our subset of scheme is capable of supporting many real world programs. Analyses will be more understandable and easier to implement due to these features. This syntax also clarifies contexts in a CFA and how they grow and shrink. With let and multi-argument lambdas, we can place multiple bindings in a single context. This will avoid states ascending to top, by decreasing the amount of contexts. Figure 2 presents a CESK* machine utilizing -CFA for value-analysis, [19] [11]. The states are partitioned into evaluation and application states, and the store is partitioned into a value-store and a continuation-store. There are a variety of continuations which give meaning to the program.
The state is partitioned into 2 types of sub-state. The control of an Eval state is syntax. When transitioning from an Eval state, the goal is to produce a value. For example, when an if expression is encountered, the resulting state is another Eval state with the guard expression as the control. The second type of state is an Apply, where the control is a value. These states will apply the control depending on the continuation. When an if expression's guard reaches an Apply state, a branch is selected based on the inspected value.
With abstracted abstract machines, both values and continuations are identified through the store with an address. However, they require different address types. Value addresses are determined by the polyvariance and analyses type we are conducting [7]. Continuations, however, are allocated in the Pushdown-For-Free style, which has its own allocator [8]. These stores are combined in the state, but are accessed separately and combined when clear in the semantics for brevity.
Environments in this machine are not a mapping, as shown in many AAM based approaches. Instead, environments are simply a function of context, and stand-in for time-stamps a la -CFA

∈Σ
Eval + Apply Semantic Classes for the Scheme m-CFA CESK* Machine [11]. Here, closures utilize flat-contexts, instead of the usual linked model. Instead of store-fetches beingˆ ( ( )), they are nowˆ ( , ). In -CFA, the current context is based on the top stack frames, as opposed to the latest call-sites.
There are a variety of continuation types to enumerate the various semantic features of the Scheme subset. When a set! expression is evaluated, a setk continuation is added to the store to identify what to accomplish after the inner expression is fully evaluated.
The Eval rules in Figure 3 govern how to break down complex expressions to form an atomic expression. Some rules are straightforward, such as E-If. After encountering an if expression, the guard is evaluated. A continuation is created to keep track of what to do when we know the value of the guard. Generally, an evaluation rule should focus on evaluating syntax, and not creating semantic objects such as contexts.
Although, other transition rules are trickier. The E-Let transitions to multiple states, one for each binding. For brevity, at least one binding is required, as a 0-binding let would have to transition directly to the body with a new context. Let is also complex since it creates the resulting context The E-Prim and E-Call rules are multi-stage rules. They each have multiple expressions that must be evaluated in a specific order. In a function call, the function is evaluated before the arguments, so there must be a special continuation frame for each juncture in the evaluation.
Atomic evaluation is defined in Figure 4. The function A produces values from atomic expressions. The rule E-AE will transition from an Eval state into an Apply state using A.
Apply rules, as shown in Figure 5 transition based on the value and the current continuation. These rules primarily govern contexts. Here, the context may be extended, bindings added to it, or it may be returned to a previous version.
Apply rules may be triggered at the same time. For example, if an address contains multiple value, then both A-If rules must be transitioned from. In Figure 6, both branches must be taken to soundly approximate this program when using a low sensitivity analysis such as 0-CFA. In the example, the inner let calls the same function twice, which, in the same context, binds the address to both #t and #f. Then, when is referenced, it contains both possibilities, so both branches will be taken.

Evaluation Rules
The A-Let rule will be ran once for every binding in a let expression. Because the addresses were calculated in the E-Let rule, not much work needs to be done in this rule. However, because every let continuation results in the same state, only one output state is generated for the body of the expression. Creating new contexts is only done when variables are bound. Creating scope like this is the trigger, and not simply evaluating an expression. Therefore, we only need to create a context in the case of E-Let, E-Call/cc, and E-Call. We only set the context in the Apply state, however, when we are evaluating the inner expression with the new bindings.

Helper Functionŝ
:  The value and continuation stores are necessarily responsible for an exponential growth of states in the state space. One method to maintain polynomial worst-case complexity when evaluating closures, is to separate the stores from the states, and to globalize the stores. After each state transition, the stores are combined and used for the next transitions. Figure 8 gives a collecting semantics which transforms a standard machine with an in-line store into a global store. The semantics utilize the injection functionÎ, along with the inline-store transition function .

DATALOG IMPLEMENTATION
Soufflé is used as the Datalog engine for its state-of-the-art runtime performance, parallelism, and language features. Algebraic Data Types (ADT) are utilized for contexts, value and continuation types to maintain brevity. This implementation can be replicated without ADTs but it will be much more verbose.
Implementing the above operational semantics as a Datalog program is generally a straightforward process. Many rules can be converted in a near 1:1 fashion. However, there are some unique relations that differ from the operational semantics. Still, the rules of the machine map closely to the implementation in Datalog. Figure 9 shows the similarity between the two.
stored_val(av, v) :-copy_ctx(from, to, e), freevar(fv, e), stored_val(av, v), av = $VAddress(fv, to). facts are generated by the heads of the clauses. As a result, more rules can be executed, extending the set of total facts. Figure 10 shows two interesting relations. These highlight a key difference between the operational semantics and the Datalog implementation. On the left is the equivalent to : peek_ctx. On the right is the implementation of copy. In Datalog, we compute a helper relation, peek_ctx, which computes a context as needed. The copy_ctx relation will signal a copy operation, from a source to a destination context. When a copy_ctx fact is added, it does not immediately do the copy, but it will trigger an inference rule for the stored_val relation.
See Appendix A for the full Datalog implementation.

EVALUATION
In this section we present an evaluation of our implementation of -CFA in Soufflé. To gain confidence in our implementation's correctness, we performed manual validation on a set of testcases.
To measure scalability and complexity in practice, we construct a family of terms that exhibit worst-case (polynomial) behavior. We used large terms in this family and ran experiments on a 28-core Linux server with 78GB of RAM.

Constructing worst-case terms for -CFA
In order to both evaluate the performance and verify the correctness of our implementation, we construct a family of terms that incur maximum-possible work in practice. Van Horn's dissertation details a construction of terms whose analysis require exponential work for -CFA [18]. Figure 11 shows an example for 1-CFA. The ultimate issue is that #t and #f will be conflated through the call to f, producing two runtime closures but four abstract closures; more bindings, or arguments to , may be added to add further complexity. We use Van Horn's technique to generate high-complexity terms for our -CFA implementation. The key trick to fool [k=1]-CFA from Van Horn's example is the application of the identity function inside the term. This identity function acts as padding, as [k=1]-CFA traces only the most recent call site. During concrete execution, the intermediate call to the identity function sits (on the stack) ((lambda (f) (let ((m (f #t)) (n (f #f))) m)) (lambda (z) ((lambda (x) x) (lambda (w) (w z z))))) (m1 (f 1)) (n0 (f 0))) m)) (lambda (z) ((lambda (x) (+ z (+ z ...))) (lambda (x) x))))  in front of the (separate) calls to f. In [k=1]-CFA, only the most recent callsite is remembered and thus #t and #f will flow to same address. However we cannot directly translatiterate this example into -CFA as we will not see the expected storage blowup. In -CFA, the context (the contour in -CFA) only grows in the state when values are bound to a variable. If padding is in function postion when (w) (w x) is evaluated, the context has not been extended yet. Using Van Horn's example with -CFA, the padding will be bypassed. In -CFA, the padding should be moved into argument position and -expand the precision losing term. This is shown in Figure  12. This modification forces conflation of the values after the padding label is appended into the context.

Results
We used our worst-case term construction to perform a variety of runs using Soufflé. Table 1 shows the results of our system on a set of two terms: one with 32 let bindings and one with 86 let bindings. We measure 0, 1, and 2-CFA using a variety of paddings (0, 1, and 2). By construction, we expect terms to explode when the amount of padding is too low as the analysis begins to conflate polynomially-greater callsites. For example, in 32/4, we see 0-CFA explode while 1 and 2-CFA are very fast. This is because both 1 and 2-CFA are fully-precise for the term. As expected, analyses of higher-complexity have longer runtimes. For example, looking at the timings for 2 padding, we can see that 2-CFA is roughly twice as slow as 0-CFA. We measured parallel performance using a variety of thread counts. Soufflé was built to support scalability and multithreading to speed up parallel execution on a single node. In our analysis, we believed there would be many potentially-parallelizable states. For exapmle, we evaluate different let clauses non-deterministically. We used Soufflé version 2.02, compiling from source with OpenMP support enabled. Our results were all compiled to C++ via Souffleé's -c flag. We verified CPU utilization (via htop) to ensure multithreading was enabled. However, as detailed in Table  2, our results demonstrated anti-scalability: instead of making the program run faster, the more cores used, the slower execution we observed, while also adding more memory overhead. GitHub issues from the Soufflé authors point to several potential reasons for poor scalability. For example, our implementation uses a large number of rules, and Soufflé does not parallelize across rules.

CONCLUSION
Datalog-based implementation of static analysis tools has enabled new frontiers in the scalability of analyses to object-oriented languages. However, we do not know of any presentations that extend these ideas to Scheme-like languages. This paper presented the key ideas necessary to implement analyses of Scheme-like languages using Datalog. We structure our analysis using the AAM-based approach to facilitate translation to Datalog's deductive rules, using the -CFA allocation strategy of Might et al. to mirror the flat closure structure naturally enabled by Datalog [11]. To our knowledge, this is the first presentation of a Datalog-based analysis for Scheme-like languages.