Abstract Interpretation is
a very powerful technique to infer inductive invariants from
transition systems. We show how SeaHorn can be combined
with Crab-llvm, a tool that infers
invariants from LLVM bitcode based on abstract interpretation, to
strengthen the invariants inferred by `spacer`

, the PDR/IC3 back-end
solver. Consider the next example `crab1.c`

:

If we run the command:

You will notice that SeaHorn is unresponsive for a while. In fact, SeaHorn will never give you an answer!

To mitigate this, we can tell SeaHorn to call `crab-llvm`

and use all
the invariants inferred by `crab-llvm`

as *lemmas* in `spacer`

:

You should see that SeaHorn can now produce an answer. These are the
safe invariants produced by `spacer`

together with `crab-llvm`

:

In this example, `spacer`

could not find an inductive strengthening of
the property `x >= y`

. However, `crab-llvm`

can infer using classical
intervals the inductive invariant `y >= 0`

which is not enough to
prove the property but when in conjunction with `x >= y`

it suffices
to prove the program is safe.

Another example where `spacer`

can substantially benefit from abstract
interpretation is when universal quantifiers are needed to prove a
property. Consider the next example `crab2`

:

If the following command is executed:

then, SeaHorn proves the program is safe. Let us try now the following command:

In this case, we don’t get an answer in a reasonable amount of
time. The reason is that we are trying to prove that all elements in
the array are positive. This is tantamount to infer an universally
quantified invariant over all array cells. This is currently beyond
the capabilities of `spacer`

. However, `crab-llvm`

provides several
array domains that can easily infer invariants like the one we need
for our example.

We can instruct SeaHorn to call `crab-llvm`

with an array domain using
intervals to model array contents as follows:

However, note that we don’t get an answer yet. The reason is that even if `crab-llvm`

infers that all elements of the
array between `[0,n)`

is greater or equal than `0`

, `spacer`

does not
support lemmas with quantifiers. Therefore, it seems that our effort
of computing universally quantified invariants using `crab-llvm`

is
futile. The solution adopted in SeaHorn is to perform explicit
instantiation of the universally quantified invariants inferred by
`crab-llvm`

so that `spacer`

can digest them as quantifier-free
lemmas. To do that, for each read `v := a[i]`

of an array `a`

we
insert an assumption `assume (p(v))`

where `p`

is the property that
holds universally on each array element, and therefore it must hold on
the particular read element `a[i]`

. If we execute the command:

we can quickly get the following answer: