Safe Haskell | None |
---|---|

Language | Haskell2010 |

Author : Levent Erkok License : BSD3 Maintainer: erkokl@gmail.com Stability : experimental

Bounded fixed-point unrolling.

# Documentation

bfix :: (SymVal a, Uninterpreted (SBV a -> r)) => Int -> String -> ((SBV a -> r) -> SBV a -> r) -> SBV a -> r Source #

Bounded fixed-point operation. The call `bfix bnd nm f`

unrolls the recursion in `f`

at most
`bnd`

times, and uninterprets the function (with the name `nm`

) after the bound is reached.

This combinator is handy for dealing with recursive definitions that are not symbolically terminating and when the property we are interested in does not require an infinite unrolling, or when we are happy with a bounded proof. In particular, this operator can be used as a basis of software-bounded model checking algorithms built on top of SBV. The bound can be successively refined in a CEGAR like loop as necessary, by analyzing the counter-examples and rejecting them if they are false-negatives.

For instance, we can define the factorial function using the bounded fixed-point operator like this:

bfac :: SInteger -> SInteger bfac = bfix 10 "fac" fact where fact f n = ite (n .== 0) 1 (n * f (n-1))

This definition unrolls the recursion in factorial at most 10 times before uninterpreting the result. We can now prove:

`>>>`

Q.E.D.`prove $ \n -> n .>= 1 .&& n .<= 9 .=> bfac n .== n * bfac (n-1)`

And we would get a bogus counter-example if the proof of our property needs a larger bound:

`>>>`

Falsifiable. Counter-example: s0 = 10 :: Integer`prove $ \n -> n .== 10 .=> bfac n .== 3628800`

By design, if a function defined via `bfix`

is given a concrete argument, it will unroll
the recursion as much as necessary to complete the call (which can of course diverge). The bound
only applies if the given argument is symbolic. This fact can be used to observe concrete
values to see where the bounded-model-checking approach fails:

`>>>`

Falsifiable. Counter-example: bfac_10 = 3628800 :: Integer bfac_n = 7257600 :: Integer s0 = 10 :: Integer`prove $ \n -> n .== 10 .=> observe "bfac_n" (bfac n) .== observe "bfac_10" (bfac 10)`

Here, we see that the SMT solver must have decided to assign the value `2`

in the final call just
as it was reaching the base case, and thus got the final result incorrect. (Note
that `7257600 = 2 * 3628800`

.) A wrapper algorithm can then assert the actual value of
`bfac 10`

here as an extra constraint and can search for "deeper bugs."