[SMT-LIB] QF_BV and division by zero

[Levent Erkok]

Hi Clark,

I argued for a semantics of x / 0 = 0 AND x % 0 = x, for both signed and
unsigned bv/integer values In the following message:
http://www.cs.nyu.edu/pipermail/smt-lib/2015/000977.html

The crux of the argument is agreement with the theorem proving community,
as implemented by Isabelle, ACL2, and HOL (and possibly others). I maintain
the same point of view.

Cheers,

-Levent.

On Fri, Mar 31, 2017 at 11:07 PM, Clark Barrett <barrett at cs.stanford.edu>
wrote:

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