SpeculativeAnalysis

Example

The idea with speculative analysis is to allow static analysis to be optimistic, where otherwise precision would be lost.

Let's consider an example:

f <- function(foo) {
  x <- 1
  foo()
  x
}

wellBehaved <- function() 1
illBehaved <- function() assign("x", 666, sys.frame())

f(wellBehaved)

We would like to constant propagate x <- 1. But, it's only correct in case foo being wellBehaved, not if it is illBehaved. To solve this issue we can place a guard:

f <- function(foo) {
  assume(contextInterefence == wellBehaved)
  foo()
  1
}

That works, but is overly conservative. For example it will fail for f(function()42) even though the function we pass is in a sense well behaved too.

What we want instead is a condition on foo, that is sufficient for our optimization to still be correct.

f <- function(foo) {
  assume(doesNotAlter("x", foo))
  foo()
  1
}

Let's call the sum of all conditions, such as doesNotAlter, the spec that foo needs to adhere to. Note, checking the spec is probably expensive. But, with (foo == wellBehaved || doesNotAlter("x", foo)) there exists a check that is both efficient and as weak as possible.

Specs

How do we derive a spec?

There are a number of properties that we want form it:

• It is a sufficient condition for our optimization to be correct
• We can verify it at runtime
• For practical reasons: Once we verified it, there is a quick check

From Static Analysis

If we think in terms of static analysis, then the above function f can be analyzed as follows:

x <- 1   ---[x=1]--->   foo()   ---[??]--->   x

Adding our hunch about foo being wellBehaved, while staying conservative, we get the following:

Conservative Analysis:

                      .-->   wellBehaved()   --[x=1]--.
                     /                                 \
x <- 1   ---[x==1]--|                                   |---[??]--->   x
                     \                                 /
                      `-->   foo()   ----------[??]---’

Obviously, the fact we need about x is lost at the merge between wellBehaved and foo. We can see this by looking at the difference between the results of an optimistic analysis and a conservative analysis. To get an optimistic analysis, we just replace foo with abort.

Optimistic Analysis
                      .-->   wellBehaved()   ---[x=1]--.
                     /                                  \
x <- 1   ---[x==1]--|                                    |---[x=1]--->   x
                     \                                  /
                      `-->   abort()   ---------[⊥]----’

To find a minimal spec, we need to back-propagate facts, that we used in optimizations. In this case we find that foo() needs to produce a state where x=1. We can wrap the call to foo in a spec that enforces this.

                     .->  wellBehaved()  ---------[x=1]------.
                    /                                         \
x <- 1   --[x==1]--|                                           |--[x=1, ??]-->   x
                    \                                         /
                     `-->  specWrapper(foo())  ---[x=1, ??]--’

Concretely, we could use the following spec:

specWrapper <- function(contextInterference) {
    contextInterference()
    if (x != 1)
        abort()
}

The problem with this is, that we can't actually execute such a specWrapper in general. To understand why, consider the following example:

specWrapper <- function(contextInterference, arg) {
    contextInterference(arg)
    if (sentANetworkPacket())
        abort()

specWrapper(foo, highlySensitiveDoNotLeak)

More realistically, in the case of a compiler, we might want to assert that a function does not print anything, does not alter the heap, and so on. All of those are effects, which, when detected retroactively, can't be undone.

On the other hand we can show, that a function satisfies a spec, by statically proving that the specWrapper does not abort. And, even though this is a static analysis, we can delay it and plug in the values dynamically.

Issues

Let's try to come up with an implementation strategy. Given a static analysis checkDoesNotAbort which tries to statically prove that a given expression cannot reach abort.

delayedCheck = quote(specWrapper(unquote(foo), unquote(highlySensitiveDoNotLeak)))
assume(checkDoesNotAbort(delayedSpec))
foo(highlySensitiveDoNotLeak)

That's better, but still fails to often. So far we just focus on the previously unknown piece foo, but disregard the context in which it is instantiated (i.e. f). Thus, we get a less precise result than we would have gotten, if we would have known foo statically. Consider:

f <- function (foo) {
    GLOBAL <- 1
    delayedCheck = quote(specWrapper(unquote(foo), unquote(doNotLeak)))
    assume(checkDoesNotAbort(delayedSpec))
    foo(doNotLeak)
    return 0
}

aFoo <- function(x) if (GLOBAL != 1) leak(x)
f(aFoo)

In this case the function foo does not leak the argument, but our analysis cannot know, without also considering the body of f. So, we also want to include some context.

Maybe a solution would be to partially evaluate f and then analyze the residual function. Conceptually, such a solution would behave along those lines:

f <- function (foo) {
    GLOBAL <- 1
    delayedCheck = quote(
        GLOBAL <- 1
        specWrapper(unquote(foo), unquote(doNotLeak))
        return(0))
    assume(checkDoesNotAbort(delayedCheck))
    foo(doNotLeak)
    return(0)
}

We probably do not want to keep a copy of the whole function for delayedCheck, but rather use the function itself. In any case, we need to argue why it should be possible to complete the original analysis on the optimized version of f.