[SMT-LIB] overflow checking for bit-vectors

[Clark Barrett]

Hi Florian and all,

Thank you for this suggestion and I apologize for taking so long to
respond.  After some discussion, it seems like a fine idea to add these to
the SMT-LIB bit-vector logic.  We will proceed with a revised logic and
post to this list when it is ready.

-Clark

On Fri, Sep 4, 2015 at 1:20 AM, Florian Schanda <florian.schanda at altran.com>
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
> :)
>
> 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.
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>