[SMT-LIB] overflow checking for bit-vectors

[Florian Schanda]

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 :)

Thanks,

- Florian

[1] Schulte, M. J., Gok, M., Balzola, P. I., & Brocato, R. W. (2000,
November). Combined unsigned and two's complement saturating multipliers.
In International Symposium on Optical Science and Technology (pp. 185-196).
International Society for Optics and Photonics.