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:

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

That's better, but still fails to often.

f <- function (foo) {
    GLOBAL <- 1
    delayedCheck = quote(specWrapper(unquote(foo), unquote(highlySensitiveDoNotLeak)))
    assume(checkDoesNotAbort(delayedSpec))
    foo(highlySensitiveDoNotLeak)
}
f(function(x) if (GLOBAL != 1) leak(x))

Somehow we need the current analysis context as well, something like assume(checkDoesNotAbort(delayedSpec, analysisContextHere())).