I'll attempt to explain an approach I came up with to address simple context sensitivity in Demand CFA.

First some code to analyze.

fun do-something(f)
  f(5) + f(10)

fun main()
  do-something(fn(x) x + 2)
  do-something(fn(y) y + 1)

This is your typical example of call sensitivity. The purpose of call site sensitivity is to distinguish between multiple bindings of the same parameter, to allow for more precise analysis. In this case, we want to distinguish between the two bindings of f in do-something as well as the multiple bindings of x and y. In an exhaustive CFA we could choose to parameterize the analysis by the call site, but due to the dynamic nature of call sites and higher order functions we discover the different call sites as we do the analysis.

From a demand perspective, if I want to know the value of the expression f(5), first I need to figure out what values f can take on. Using demand CFA's caller relation we find both lambdas. Now we need to evaluate the body of the lambdas to figure out the value of the expression. The bodies references x and y. To find the value of x in a call site insensitive analysis we would typically find all bindings of x which would include 5 as well as 10. The result of the expression f(5) then would include the result for the expression f(10) as well. This seems nonsensical. The query clearly delineated a context we care about. We want to know the value of f(5) not f(10). However, full context sensitivity is often too expensive.

The idea I have is to keep track of bindings (as expressions / thunks) as we descend into a call, then when evaluating a reference to a parameter we know about in our bindings, we can directly evaluate that expression binding.

With the above example we still evaluate f to both lambdas, but when evaluating the bodies of the lambda we find that we already know the expression that x/y is bound to. Thus we have a selective context sensitivity - one where the evaluation preserves call / parameter binding relations, but only for calls we have made during the abstract evaluation. Note that the exhaustive formulation of CFA also preserves these relations between functions and parameters, at least until the second time the lambda is called, at which point the joining happens.

Question: How does this work in the presence of recursion

Okay lets consider what modifications might be needed in the presence of recursion / mutual recursion. Let's consider the following example.

fun map(l: list<int>, f: (int) -> int): list<int>
  match l
    Nil -> Nil
    Cons(x, xs) -> Cons(f(x), map(xs, f))

fun main()
  map([0, 1, 2, 3], fn(x) x + 1)

Hovering over f should result in just one closure. However, evaluating the expression f(x) should ideally result in just an abstract number (I know, not any more interesting than the type system). However, a more precise analysis could determine the range of numbers using an interval abstraction. However, let's take the general map statement in main: what do we have to do to make this particular sensitivity not diverge in the presence of recursion? When we evaluate the call to map, we bind the parameter l to the expression [0, 1, 2, 3] and f to the closure fn(x) x + 1. Then when evaluating the body, we meet the recursive call to map. If we keep binding the expressions an recurring, we could potentially diverge (I know, not in this case, but in the general case of non-inductive datatypes or recursion on numbers etc). Even on finite domains, unrolling recursion too much could result in long analysis times. So let us consider what we should bind to the parameters to prevent blowup. Let's consider widening the parameters by joining the abstract values of the parameters. This would result in the following bindings: f: eval(ref/f) join f, l: eval(xs) join l. Let's assume the abstraction of the ADT(abstract data type) for l ends up looking like: {Cons(0, Cons(1, Cons(2, Cons(3, Nil))))}. Then lets assume that xs is correctly abstracted to {Cons(1, Cons(2, Cons(3, Nil)))}. We have two paths forward, bind the concrete (unroll recursion), or widen. If we can determine that the size of the datatype is decreasing, and we have enough allotted time left, we could keep evaluation with precision. However, we can't know that ahead of time, (TODO: consider timeouts and other estimation or revisiting techniques). So let's widen. Let's consider some alternatives for joining l with xs:

Most precise (other than just putting into a set) {Cons(AbNum, Cons(AbNum, Cons(AbNum, {Cons(AbNum, Nil), Nil})))}

• This has the same issue as before, a long list could take a long time to evaluate (though this is still somewhat limited by the size of the syntax)
• Evaluating this one step results in another l: eval(xs) join l binding, which makes the abstraction larger in some ways (depending on how many alternates) {Cons(AbNum, {Cons(AbNum, {Cons(AbNum, Nil), Nil}), Nil})}. This is not tenable

So lets consider just widening to: {Cons(AbNum, self), Nil} where self just refers to the evaluation of the binding itself. With this approach on the second unwinding we find the evaluation already in the cache, and we can just return the value.

Two issues with this approach:

• Precisely defining the widening
• Defining the cache (so that it takes into account parameters properly)

My current naive approach (not handling recursion) keeps the parameters separate from the configuration in the cache. This has a few issues:

• Parameters are assumed to be only the bindings from the initial call (in a recursive call)
• A recursive call would cause an infinite loop
• I detect when I can use parameters by whether bind returns the directly enclosing lambda. (This is problematic since it doesn't check if I'm in a recursive context)

I need to adjust the memoization approach:

• Add a bottom value to the cache prior to evaluation (just on first visit?)
• Make sure this value has a cacheGeneration that will guarantee a single recursive evaluation

On the recursive call, the memoized results of the cache will determine that this is a recursive call (no actual results in the cache), and will join the parameters prior to evaluation. This means that I have to adjust my function that inserts the params to first check if the function I'm evaluating is in the cache. Also, I will have to migrate away from the syntactic check for parameter scope.

Okay now for formalizing the widening / joining of the abstract constructors. For two abstract values

• Functions are joined by making sets of lambdas (without bindings)
• Constructors are joined:
  • If they begin with the same constructor recur
  • Join all constructor parameters
    • If it is a recursive parameter (with same type variables etc)
    • If it is the same constructor, recur
    • If it is a different constructor, add the alternate to the top level set of constructors and set the parameter to a self value.
    • If it is not a recursive parameter, create a new join context, and join the parameters (self in a recursive constructor that isn't the primary constructor refers only to terminating the recursion on that parameter)
• Literals are joined by a simple lattice of Bottom/Precise/Top where joining two precise literals results in the literal if they are the same, otherwise top.
• Unknown externals etc are represented just by the resulting type
• Errors are just errors that accumulate -- TODO: consider what to do here

Weekend plans never work out for me. My priority is my family, so of course there really isn't much time for programming. The few times I can do some programming on the weekends are Friday and Saturday evening while Emily is working. Sometimes I'm busy reading a book, though I guess I did a little bit with a riverpod like framework for Koka. Not much though. Just trying to understand Riverpod's internals right now. Anyways, I got an email from Daan today about him releasing a new version of Koka today with fbip / fip keyword support. It sounds like he wants to do a Koka release with VSCode support in August, so we are going to talk next week about what should go into that release I think.

Thoughts below about Demand CFA for Algebraic Effects.

I just read Logic-flow analysis of higher-order programs by Matt Might.

Great paper, and had a lot of the ideas that were spinning around in my mind. Matt Might has done a ton of work in so many areas of control flow analysis that it boggles my mind.

The related work section at the end includes many references that I'd like to read to understand more in this area. However, I feel like egglog supersedes this work, with a lot of the same ideas but in a better framework for extending and experimenting with the ideas.

I watched a good video on Delimited Continuations from Alexis King last night. She explains them very well both semantically and with some examples. I'm glad to see that native support for them has been introduced to Haskell.

In figuring out what approach to take for my full program analysis for algebraic effects, I'm looking into a few things:

One is this paper Functional derivation of a virtual machine for delimited continuations, which I think was recommended to me by Kimball when I was first looking into algebraic effects, and first learning about control flow analyses. I'll probably also look into both the typed directed continuation passing style transformation that was originally implemented for Koka, as well as the more recent Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C.

As far as progress today on figuring out some benchmarks for how to improve Koka's performance, I've added some basic benchmarks, but there is still more research to go, to really show the difference. I wish there were more real-world example programs I could benchmark the changes on. I'm sure I'll be contributing to that due to my interest in Koka. I mostly spent time on the benchmarking scripts, but in doing so I also added / exposed a few methods for dealing with getting file information.

I'm looking into performance differences between integers and int32s in Koka.

I just read Better Together: Unifying Datalog and Equality Saturation.

A lot of good ideas in this paper. I'm interested in trying to use it for some of our analyses, or to implement a simple type system. However, like most logic languages I wonder how hard it is to for example read and parse a file, or if you need to parse a program in a more traditional language and then generate the egglog code for analyzing the program after the fact.

Anyways, the full version of the paper is on arxiv and includes an appendix with practical examples. The repo says that the python binding has a bit more documentation, but the link is bad. The rust crate has some docs but mostly for the api bindings and not the language itself. So I guess I'll be looking into the appendix of their extended paper if I want to learn more.

From the same conference (PLDI) I watched the presentation for this paper, as well as another talk from that section about Indexed Streams which was also interesting, but not really related.

In thinking about the defunctionalization paper from the prior post, I've come to the conclusion that polymorphism is a big problem for current control flow static analyses. Polymorphic functions introduce a lot of joining of abstract values. See Polymorphic splitting an effective polyvariant flow analysis

In reality the main thing that CFA is trying to address is where to values flow. In order to make the problem tractable, we need to abstract, and make adjustments to ensure termination. The main adjustment that is needed is to make recursion bounded. However, everything other adjustment seems to be a tradeoff between precision and theoretical complexity. The paradox of static analysis is that the more precise you can be the fewer spurious flow paths you explore, and the quicker the analysis in practice. However, the more precise you are the more complex the analysis is in theory. However, it seems to me that the theoretical complexity is more tied to the nature that with a constant m or k limit, you end up following more and more recursion. What if recursion was the only thing bounded by m or k? Essentially just have a parameter that controls the unrolling of recursive / mutually recursive functions. I wonder how precise such an analysis could be. I feel like Kimball has talked about some sort of analysis that uses regular expressions on traces to find or bound recursion. I'll have to see if I can find that paper, and see how it differs from my ideas.

Two thoughts about this:

• I wonder if I can augment my approach for Trace Preserving mCFA (unpublished) to account for these sorts of patterns
• I wonder if I can use the defunctionalization approach to do a set / union type system that handles polymorphism well

There is a lot of literature that I haven't read on this topic. I know I've seen at least one or two CFA papers about handling polymorphism specifically (such as let bound lambdas). Additionally, I have very little experience or background with set based type systems and defunctionalization. It would require a lot deeper dive into the literature to see what has already been done.

However, I think a union type inference (maybe augmented with both structural and nominal types) along with defunctionalization could get rid of a ton of spurious control flow for a CFA, and potentially be able to handle any untyped language. Using inference to type untyped languages seems like a hard problem, I wonder what the state of the art is. Here is one paper about Programming with union, intersection, and negation types which is probably a good introduction to set based type systems.

Additionally, I had some thoughts about how to proceed a full program analysis for algebraic effects and modern abstractions

• I'm thinking that it might be easiest (as far as just getting some results for the lab for a paper later this summer), to just use a small lambda calculus language based on scheme, with just a couple things added. (perform action ...args) for performing an effect, and (handle action (lambda (resume, ...args) handler) (lambda () body)) for the handling of the action. I'll focus on deep effect handlers, which reinstall the handler for the resumption. Additionally, I need to think more about threading state through, which is a common thing for languages with deep effect handlers to do, and makes it much easier to implement mutable state as an effect. Maybe something like: (handle action initial-state (lambda (state, resume, ...args) handler) (lambda (state) body)) with perform changing to (perform action ...args (lambda (result, state) body))
• I could also remove mutation from the language since I can just use the state effect
• Should I support user datatypes (currently in my prior analyses I just support linked lists and primitives), I think at the very least I should try supporting structural objects (which could all be represented the same way). Nominal objects could just be an extension of structural objects with a special tag field.

First blog post about readings of papers. This one is called Better Defunctionalization through Lambda Set Specialization.

The basic idea is to keep track of the lambdas that could flow to a particular location in the type system as a sort of set / effect type.

This allows for a large majority of call sites to reference first order functions, with just tags for which lambda is being called.

I've been looking into how to use the z3 theorem prover in Haskell lib. It turns out to be not very well documented, and my particular use case did not have any example programs available.

Specifically, for the abstract value representation for my analysis I want to be able to represent integer values as a unique identifier, along with some constraints that are found by learning about the control flow of the program. For example a binding for $x$ within an if statement's then branch where the condition is $x > 0$ should add the constraint that the abstract value that flows to that binding has a value greater than 0. This should be combined with finding other constants, such as using an integer to generating a list of a constant size or count down to a specific value. Finally we'd like to use Z3 to be able to prove that a value is within some concrete integer range. Using this information we can optimize the storage and arithmetic of these values statically, and omit a bunch of runtime checks that handle arbitrary precision integers.

Some thoughts on how to organize Demand CFA for Koka