[SMT-LIB] QF_BV and division by zero

[Clark Barrett]

Hi everyone,

Yes, this should have been finalized last year and it's my fault it wasn't
- I'm very sorry :(
We have discussed this far too many times, but let's fix it finally.

There was broad consensus for using a vector of all 1's as the result of
bvudiv.  According to the message logs, Alberto, Daniel, Christoph, Armin,
and Bruno support this interpretation (correct me if I'm wrong).  A few
people also disagreed for various reasons, though they were mostly users
not developers and I believe their concerns can be addressed by using
define-fun to create a custom encoding that does what they want (see point
3 below).

To resurrect the old thread, here is the argument for going ahead with this
interpretation:

1. Bit-vectors are used to represent machine/circuit calculations.  A
circuit computes a value if zero is fed as an input.  The value it computes
is all 1's.

2. The current semantics were designed to help users find bugs, but they
still allow certain kinds of bugs to go masked.  For instance, the
semantics of first-order logic enforce that dividing the same number by 0
in two different places yields the same result.

3. Users have the freedom to encode bit-vector division however they like,
including using a unique uninterpreted function for every occurrence of
division.

The main reason to fix the interpretation is to make solver development for
QF_BV more clear and straightforward.

Trevor, you are arguing for a value of 0, but do you disagree that a vector
of 1's is the most natural result from a circuit?  What do others think
about his argument for 0?

I don't think we had consensus on what the result of bvurem should be when
the second operand is 0 (I could not find it in the message logs).  Could
those of you with a strong opinion weigh in?

Let's have one last round of discussion on this.  I promise this will be
the last time.

-Clark

On Wed, Mar 29, 2017 at 8:52 PM, Trevor Hansen <trev_abroad at yahoo.com>
wrote:

> It'd be great to have QF_BV division and remainder by zero resolved in
> time for this year's SMTCOMP.
> The relevant discussion from 2015 is in the thread here:
> http://www.cs.nyu.edu/pipermail/smt-lib/2015/000966.html
>
> Personally, I'd prefer division and remainder by zero to evaluate to zero.
> Because then the semantics of bvsdiv, bvsrem and bvsmod by zero are
> simpler.
> bvsdiv, bvsrem, and bvsmod are defined here: http://smtlib.cs.uiowa.
> edu/logics-all.shtml
>
> For example, bvsrem is:  (bvsrem s t) abbreviates
>       (let ((?msb_s ((_ extract |m-1| |m-1|) s))
>             (?msb_t ((_ extract |m-1| |m-1|) t)))
>         (ite (and (= ?msb_s #b0) (= ?msb_t #b0))
>              (bvurem s t)
>         (ite (and (= ?msb_s #b1) (= ?msb_t #b0))
>              (bvneg (bvurem (bvneg s) t))
>         (ite (and (= ?msb_s #b0) (= ?msb_t #b1))
>              (bvurem s (bvneg t)))
>              (bvneg (bvurem (bvneg s) (bvneg t))))))
> So if 's' is negative, whatever bvurem-by-zero evaluates to needs to be
> negated.  This means that if unsigned division/remainder evaluate to all
> ones, then (bvsdiv s 0),  (bvsrem s 0), (bvsmod s 0) all evaluate to
> all-ones if 's' is positive, and 1 if 's' is negative. This seems like an
> unnecessary complication.
> However, if (bvudiv s 0) and (bvurem s 0 ) evaluate to zero, then (bvsdiv
> s 0), (bvsrem s 0), (bvsmod s 0) also evaluate to zero. Levent Erkok
> commented that this how many theorem provers implement the semantics. So it
> seems simplest to me.
>
> Unless anyone has objections, I'll try to get a consensus from other QF_BV
> solver developers that division/remainder by zero evaluates to zero is the
> best way forward?
> Thanks,
> Trev.
>
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>