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 only work for 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 restrictive. For example it will fail for f(function()42) even though this argument is in a sense well behaved too.

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

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

(Note, that with foo == wellBehaved || doesNotAlter("x", foo)we have 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

If we think in terms of static analysis, then the above case represents itself roughly like this:

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]--->   1
                     \                                   /
                      `-->   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==⊥, ???]---’

where

specWrapper <- function(contextInterference) {
    *tmp* <- x
    contextInterference()
    if (x != *tmp*)
        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, it's too late.

But we can say, that a function satisfies a spec, if we can statically prove that the specWrapper does not abort. And, even though this is a static analysis, we can delay it and plug in the result dynamically:

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