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
}

Note, that 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.

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

To find a minimal spec, we need to back-propagate facts about x, that we used in optimizations.

                     .->  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)
}

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:

defmacro F (check)
    function (foo) {
        GLOBAL <- 1
        check
        foo(highlySensitiveDoNotLeak)
    }

fWithSpec <- F(specWrapper(foo))

f <- F(assume(checkDoesNotAbort(quote(fWithSpec(unquote(foo))))))

Note that for this we need to make an additional correctness argument, since this optimized version of the function f is not the same as the source version. We partially analyze a source version f, then we optimize that function, we get f', and finally, we refine the original analysis, but using f' instead.