[SMT-LIB] overflow checking for bit-vectors

[Viktor Kuncak]

Dear Clark

It's great to hear this update on bitvectors! I am also a fan of this
approach to define some specific value.

I have a question that relates to bitvectors. Apparently several solvers
including CVC4 and Z3 have conversions between mathematical integers and
bitvectors. From our initial experience with Leon (where we have both data
types soundly mapped), these are very useful. Is it true that they are not
in the standard? Is there a way to add them? I understand they are
connecting two theories, so there may be important framework issues, but we
seem to have canonical fixed models for both bitvectors and integers now,
so there is little doubt about the meaning of a mapping in most cases.

We should just define what is done when mathematical integer is too large
or too small. This is related to the present discussion. What does CVC4
specify in such case?

Best regards
  Viktor

On Thu, Oct 15, 2015 at 6:43 AM Clark Barrett <barrett at cs.nyu.edu> wrote:

> 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
> >
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>