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.