AbstractDomains.jl

This Julia package allows you to run Julia programs with (possibly infinite) sets of values. These sets are called abstract domains, and computing with them is called abstract interpretation. Computing with sets of values is useful for static analysis and verification (e.g. to know for sure that some bug won't occur). But it is also useful for reasoning and inference.

Documentation can be found here

Domains

An abstract domain is used to represent a large or infinite set in a finite amount of space. For instance we can use intervals [a, b] to represent all the floating point numbers between a and b. AbstractDomains.jl then provides functions for computing with abstract values, for instance we can add or multiple two intervals.

Currently AbstractDomains.jl supports only two abstract domains: Interval and AbstractBool. For every primitive functions such as +, -, &, ifelse, defined on concrete values such as Float64 or Bool, there is a corresponding lifted method defined on its abstract counterpart: Interval and AbstractBool.

The meaning of these lifted functions is pointwise. That is, if we do C = f(A,B) where A and B are elements belonging to an abstract domain, then C should contain the result of applying f to all possible combinations of elements in A and B.

Example

If only using Intervals, AbstractDomains.jl is basically an interval arithmetic package, e.g.:

julia> A = Interval(0,1)
[0.0 1.0]

julia> B = Interval(1,2)
[1.0 2.0]

julia> C = A + B
[1.0 3.0]

C should be an interval which represents all the values if we took every value in the interval A. The following code represents what this means (note: it is not valid code):

# What C = A + B is doing (conceptually!)
c = Set(Float64)
for a in A
  for b in B
    push!(c, a + b)
  end
end

Functions involving intervals and normal values are also defined in AbstractDomains.jl:

julia> C * 3
[3.0 9.0]

Boolean Functions and AbstractBools

If we apply boolean functions (> >= < <= ifelse) to intervals, we don't get back a Bool, we get back an AbstractBool. For example:

julia> A = Interval(1,2)
[1.0 2.0]

julia> A > 0
{true}

julia> A > 3
{false}

This means that for all the elements in A (e.g., 1.0, 1.000001, 1.00002,...), all of them are greater than 0. Similarly none of A is greater than 3. But why has it returned these strange value {true} and {false} instead of true and false? The next example should help illustrate why:

julia> A = Interval(1,2)
[1.0 2.0]

julia> A > 1.5
{true,false}

The result {true,false} means that there are some values in A which are greater than 1.5 and some that are not greater than 1.5.

The values {true}, {false} and {true,false} fully represent the AbstractBool domain. These values are exported by AbstractDomains.jl as t, f and tf respectively, and primitive boolean operations are defined on them, e.g:

julia> t & t
{true}

julia> t & f
{false}

julia> tf & t
{true,false}

julia> tf & f
{false}

julia> tf | f
{true,false}

Some of these may require thinking about. But they are all consistent with the semantics of functions on abstract operations being defined pointwise, as described above.

Equality

Perhaps surprisingly, there are many meaningful definitions of equality. In AbstractDomains.jl equality == is, like the other functions we've seen before, defined pointwise. This can lead to some unexpected results if you're not careful, e.g.

julia> tf == tf
{true,false}

The answer is {true,false} because true == true is true, but false == true is false (to take just two of four possible combinations). Similarly:

julia> Interval(0,1) == Interval(0,1)
{true,false}

The answer is {true,false} because there are points in the first interval which equal to points in the second interval, but there are also points in the first interval which are not equal to point in the second interval.

Non-pointwise functions on abstract domains

If we really want to test the identity of abstract objects we would use `isequal, e.g.

julia> isequal(Interval(0,1), Interval(0,1))
true

julia> isequal(tf,f)
false

isequal is an example of a function on abstract values which is not defined pointwise. There are many useful others. Some of which we call domain functions:

julia> subsumes(Interval(0,1),Interval(0.4,0.5))
true

julia> isintersect(Interval(0,1),Interval(3,6))
false

julia> isintersect(t,f)
false

julia> isintersect(t,tf)
true

# ⊔ (\sqcup) is a lub
julia> Interval(0,1) ⊔ Interval(10,3)
[0.0 10.0]

Imprecision

Abstractions are sound but can be imprecise. Imprecision means that the result of a function application may contain values which are not possible in reality. E.g.:

julia> A = Interval(1,2)
[1.0 2.0]

julia> A / A
[0.5 2.0]

The precise answer should be [1.0, 1.0]. This imprecision comes because we do not recognise that the A in the denominator is the same A as in the numerator. That is, we have ignored the dependencies.

Imprecision is undesirable. We can take some comfort in knowing that we'll always be sound, which this example also demonstrates. Soundness means that the true answer [1.0, 1.0] must be a subset of the answer AbstractDomains.jl gives us. For instance, the following would never happen

julia> A = Interval(1,2)
[1.0 2.0]

# Unsound result: this can *NEVER* happen
julia> A / A
[2.0 3.0]