FixedSizeBitVectors, QF_BV, overflows

[Pascal Fontaine]

Dear SMT users and developers,

There has been renewed requests to introduce within SMT-LIB some overflow predicates for bit vectors, i.e., predicates indicating if the result of an operation on bit vectors is not corresponding to the expected integer, because of the fixed bit width.  Impacted operations are: neg, add, sub, mul, div.

According to the initial request, we plan to introduce the following predicates:

bvnego

bvuaddo bvsaddo

bvusubo bvssubo

bvumulo bvsmulo

bvsdivo

with the same arguments as the corresponding operations, returning true if there is an overflow, and false if not.  We do not plan to distinguish whether the result is over or below the expected value.  We plan this evolution both for the 2.6 and the 3.0 versions of SMT-LIB.

We solicit comments on this by the end of January 2023.  If there are no objections by then, we will proceed in adding those functions in the relevant logics and theories.

Thanks for your feedback!

Happy holidays to All,

  Cesare, Clark, Pascal

[Florian Schanda]

On Thursday, 22 December 2022 10:56:48 CET Pascal Fontaine wrote:
> According to the initial request, we plan to introduce the following
> predicates:
>
> bvnego
> bvuaddo bvsaddo
> bvusubo bvssubo
> bvumulo bvsmulo
> bvsdivo
>
> with the same arguments as the corresponding operations, returning true
> if there is an overflow, and false if not.

I've asked for this a long time ago, so I am very glad it's finally here :)

The proposed predicates/naming sound reasonable.

There may be an extension to consider, an overflow predicate to test if a
float <-> bitvector conversion would not fit, but it's not as important.

> We do not plan to
> distinguish whether the result is over or below the expected value.

I do not think this would be necessary for the contexts where these predicates
are primarily useful (program verification).

> We
> plan this evolution both for the 2.6 and the 3.0 versions of SMT-LIB.
>
> We solicit comments on this by the end of January 2023. If there are no
> objections by then, we will proceed in adding those functions in the
> relevant logics and theories.

No objections, on the contrary. +1

Florian

[Levent Erkok]

Hi Cesare, Clark, Pascal:

These predicates are indeed very welcome. Unlike Florian, however, I think it'd also be good to add similar functionality to float conversion functions:

   ; from another floating point sort
   ((_ to_fp eb sb) RoundingMode (_ FloatingPoint mb nb) (_ FloatingPoint eb sb))

   ; from real
   ((_ to_fp eb sb) RoundingMode Real (_ FloatingPoint eb sb))

   ; from signed machine integer, represented as a 2's complement bit vector
   ((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))

   ; from unsigned machine integer, represented as bit vector
   ((_ to_fp_unsigned eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))

   ; to unsigned machine integer, represented as a bit vector
   ((_ fp.to_ubv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))

   ; to signed machine integer, represented as a 2's complement bit vector
   ((_ fp.to_sbv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))

   ; to real
   (fp.to_real (_ FloatingPoint eb sb) Real)

For naming: If a solver wants to provide individual overflow/underflow checking, maybe it's best to name these similar to bvsadd_out_of_range; then the names bvsaddo/bvsaddu can remain free for individual solver use to indicate overflow/underflow conditions.

Cheers,

-Levent.

 

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/6fb3655e-13cb-9518-0e7e-3e067ffef9d2%40uliege.be.

[Nyx Brain, Martin]

On Thu, 2022-12-22 at 09:35 -0800, Levent Erkok wrote:
>
> Hi Cesare, Clark, Pascal:
>
> These predicates are indeed very welcome. Unlike Florian, however, I
> think it'd also be good to add similar functionality to float
> conversion functions:

In principle, yes, this could be good. However some thought may be
required over semantics. Off the top of my head:

* Do you want to distinguish between early and late overflow? I.E.
before or after rounding. There has been some ambiguity over this in
the past.

* How do these connect with the type of float produced? Is producing a
subnormal / zero underflow? Can you overflow and not get infinity (for
example, in directed rounding modes)?

Cheers,
- Martin

--
UCU staff are currently in dispute with employers over pay, pensions
and working conditions. Part of the industrial action is 'action short
of a strike'. This may affect the speed at which you get responses to
e-mails and requests from some staff.

Details here: https://www.ucu.org.uk/article/12469/FAQs

[Tinelli, Cesare]

Levent,

Thanks for your suggestions. Martin raises very good points below. What is your take on them?

Best,

Cesare

> --
> You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/64dcd8008f741a47c59adc86d9b7fe42c912dd2b.camel%40city.ac.uk.

[Levent Erkok]

My motivation for overflow checking is to be able to model x86 instructions faithfully. For float-to-float conversions, I think a good example is to use CVTSD2SS instruction. (See Table D-16, Vol 1. D13 of Intel® 64 and IA-32 Architectures Software Developer’s Manual Combined Volumes: 1, 2A, 2B, 2C, 2D, 3A, 3B, 3C, 3D, and 4 You can see how CVTSD2SS is treated in the masked response cases with differing rounding-modes.)

Based on this, I think the specific answers are:

  * No need to distinguish early/late overflow; late is sufficient. That is, overflow is detected after rounding.

  * Since we’re considering after rounding, I think the overflow result will directly correspond to the conversion:

        * If you get overflow/underflow, then the result should be +/- infinity.

        * If the result is a subnormal, no overflow really exists. This is a precision loss, not overflow/underflow.

As I mentioned, the overriding goal is the ease of modeling of the conversion operators as found in x86/ARM etc. (Which I admit can be rather confusing themselves.) So, if anyone can come up with a notion of overflow that differs from the above but still allows simple modeling of what x86/ARM does, I think that should still be just fine as well.

-Levent.

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/AF1CDAA4-40C1-4D8B-8734-3E536D928DB6%40uiowa.edu.

[Andrew Jones]

Hi all,

Replying to the original email as the thread has somewhat diverged.

> We plan this evolution both for the 2.6 and the 3.0 versions of SMT-LIB.
>

How's this all looking? Is there a tentative "release date" for the
updated version?

I'm wondering if it makes sense for this to be a "2.7" release of
SMTLIB? This is to avoid solvers having to say "we support 2.6 but not
_that_ version of 2.6".

Maybe a better question for me to ask is: have there been previous
changes to SMTLIB 2.6 where *new* predicates have been added? If so, I
guess there's precedence for it being a 2.6 release. If not, I guess
following something like semver, this would require a new minor number
(i.e., 2.7).

Cheers,

Andrew

> --
> You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/6fb3655e-13cb-9518-0e7e-3e067ffef9d2%40uliege.be.

[erk...@gmail.com]

Hi Cesare, Clark, Pascal:

It's been almost a year you circulated the above email, but I just noticed a potential naming confusion: For negation and division, overflow only makes sense in the signed case. (Neither operation overflows for unsigned arguments.) But in the former case you called the predicate `bvnego`, while in the latter it's called `bvsdivo`. For consistency, wouldn't it be better to name them both `bvnego` and `bvdivo`, OR better yet `bvsnego` and `bvsdivo`? My vote would be for the latter pair.

Cheers,

-Levent.

[Clark Barrett]

Here's the rationale for the current naming scheme.

If there's an existing bv operator that can overflow in exactly one way, we just add "o" to the name of the operator.  This is the case for bvneg and bvsdiv.  If an operator can overflow in more than one way, then we add "u" or "s" to disambiguate it, which is why we have bvuaddo and bvsaddo, etc.

I do see your point, but on the other hand, we don't have a bvsneg operator, and bvneg can only overflow in one way, so in that sense, I think it's better to just stick with bvnego.

-Clark

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/503dc222-9d28-4841-8688-b3586d8520a1n%40googlegroups.com.

[Pascal Fontaine]

Dear All,

thanks for the comments.  There has been some progress on this issue, and there is a proposal for modification of the SMT-LIB BV theory and logic.  The proposed theory and logic are in attachment, and a diff is given for convenience below.

Let me suggest that we continue the conversation here: https://github.com/SMT-LIB/SMT-LIB-2/issues/2 .  We (Cesare, Clark and I) try to better organize our workflows for the SMT-LIB, and this github space will help us keep track of issues and make progress faster.

Several people have made insightful remarks, notably about the names of the operators.  From several points of view, there are certainly possibilities for better names, but names do not matter that much, and in order to proceed, we need to make a decision at some point.  We will review the whole discussion while we are refactoring the 3.0 version of the theory (which will anyway require rethinking names).  For now (for the 2.6 version of the theory and logic), it seems that some implementers of BV decision procedures are quite attached to the names as suggested before.

Thanks and best,

  Pascal

Major changes to FixedSizeBitVectors.smt2:

103a105,107
>    o (_ bv0 m), with 0 < m, which takes a non-negative integer
>      n and returns the bitvector b: [0, m) → {0}
>
109a114,119
>    o bv2int, which takes a bitvector b: [0, m) → {0, 1}
>      with 0 < m, and returns an integer in the range [- 2^(m - 1), 2^(m - 1)),
>      and is defined as follows:
>
>        bv2int(b) := if b(m-1) = 0 then bv2nat(b) else bv2nat(b) - 2^m
>
182a193,206
>
>    We also define the following predicates
>
>    [[(bvnego s)]] := bv2int([[s]]) >= 2^(m - 1)
>
>    [[(bvuaddo s t)]] := (bv2nat([[s]]) + bv2nat([[t]])) >= 2^m
>
>    [[(bvsaddo s t)]] := (bv2int([[s]]) + bv2int([[t]])) >= 2^(m - 1) or
>                         (bv2int([[s]]) + bv2int([[t]])) < -2^(m - 1)
>
>    [[(bvumulo s t)]] := (bv2nat([[s]]) * bv2nat([[t]])) >= 2^m
>
>    [[(bvsmulo s t)]] := (bv2int([[s]]) * bv2int([[t]])) >= 2^(m - 1) or
>                         (bv2int([[s]]) * bv2int([[t]])) < -2^(m - 1)

Major changes to QF_BV.smt2:

77a79,88
>     (bvnego (_ BitVec m) Bool)
>       - overflow predicate for 2's complement unary minus
>     (bvuaddo (_ BitVec m) (_ BitVec m) Bool)
>       - overflow predicate for unsigned addition modulo 2^m
>     (bvsaddo (_ BitVec m) (_ BitVec m) Bool)
>       - overflow predicate for signed addition on m-bit 2's complement
>     (bvumulo (_ BitVec m) (_ BitVec m) Bool)
>       - overflow predicate for unsigned multiplication modulo 2^m
>     (bvsmulo (_ BitVec m) (_ BitVec m) Bool)
>       - overflow predicate for signed multiplication on m-bit 2's complement
104a116,121
>     (bvusubo (_ BitVec m) (_ BitVec m) Bool)
>       - overflow predicate for unsigned subtraction modulo 2^m
>     (bvssubo (_ BitVec m) (_ BitVec m) Bool)
>       - overflow predicate for signed 2's complement m-bit subtraction
>     (bvsdivo (_ BitVec m) (_ BitVec m) Bool)
>       - overflow predicate for 2's complement signed division
224a242,244
>     (bvusubo s t) stands for (bvult s t)
>     (bvssubo s t) abbreviates (or (bvsaddo s (bvneg t)) (and (bvnego t) (bvslt s (_ bv0 m))))
>     (bvsdivo s t) abbreviates (and (bvnego s) (= t (bvnot (_ bv0 m))))