[SMT-LIB] overflow checking for bit-vectors

[Christoph Wintersteiger]

Sounds like a good idea to me too. Z3 also has most of them, although perhaps not the most efficient encodings of them.

Cheers,
Christoph

Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | research.microsoft.com/people/cwinter


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Florian Schanda
Sent: 04 September 2015 09:21
To: smt-lib at cs.nyu.edu
Subject: [SMT-LIB] overflow checking for bit-vectors

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