[SMT-LIB] overflow checking for bit-vectors

[Martin Brain]

On Fri, 2015-09-04 at 09:20 +0100, Florian Schanda wrote:
> Hi SMT-LIB,
> 
> I would like to propose an extension to bit-vectors. I have previously 
> discussed this at SMT'14 (indeed, some time ago now) and with Liana. It took 
> me some time to get around to writing the proposal; sorry!
> 
> The general idea is to have overflow-checking predicates, which can sometimes 
> be implemented more efficiently than the obvious way of doing it.
> 
> I propose to extend QF_BV as follows:
> 
>   Functions:
>  
>     (bvsaddo (_ BitVec m) (_ BitVec m) Bool)
>     (bvuaddo (_ BitVec m) (_ BitVec m) Bool)
>     (bvssubo (_ BitVec m) (_ BitVec m) Bool)
>     (bvusubo (_ BitVec m) (_ BitVec m) Bool)
>     (bvsmulo (_ BitVec m) (_ BitVec m) Bool)
>     (bvumulo (_ BitVec m) (_ BitVec m) Bool)
>     (bvsdivo (_ BitVec m) (_ BitVec m) Bool)
>       - signed and unsigned addition, subtraction, multiplication, and
>         unsigned division overflow checking
> 
>     (bvsnego (_ BitVec m) Bool)
>       - signed negation overflow checking
> 
> The signed overflow predicates checks if the given operation would yield a 
> value outside the range -2^(m-1) .. 2^(m-1) - 1, and the unsigned overflow 
> checks similar check if the result would be inside range 0 .. 2^m - 1.
> 
> The obvious way of doing this is to sign-extend both to a suitably sized bit-
> vector (m+1 for add, sub, div, neg and m*2 for mul), and then do the range 
> check; but it is possible to do it more efficiently [1]. It is always possible 
> to do this by hand, but I would trust solver developers much more than myself 
> :) Also, I think the predicates make the intent of the benchmark writer 
> clearer.
> 
> Thoughts, comments welcome. I am of course happy to provide/write some 
> overflow benchmarks from SPARK, if a solver developer implements the above :)

Sounds good and I suspect that CBMC would use them if standardised.

Aside from checking for overflows, these also have a use in generating
"nice" error traces and avoiding 'false' alarms caused by previous
errors.  For example finding a trace that triggers the n'th overflow
check without relying on the previous n-1 ones.

Cheers,
 - Martin