[SMT-LIB] QF_BV and division by zero

[Levent Erkok]

Hi Clark,

I'm quite happy with an "interpreted" result, but I'm confused about the
result you picked. You said: " A circuit computes a value if zero is fed as
an input.  The value it computes is all 1's."

Can you provide some context around this? It seems overly broad, what
circuits are you referring to?

To add some more fuel to the argument, I'll point out that other tools in
the theorem proving community seem to prefer division by zero to be 0:

   - Isabelle defines: x / 0 = 0 AND x % 0 = x. (Page 168 of
http://isabelle.in.tum.de/doc/tutorial.pdf)

   - ACL2 agrees with Isabelle: (
http://www.cs.utexas.edu/users/moore/acl2/v6-2/UNARY-_slash_.html and
http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/RTL____Modulus
)

   - HOL defines x/0 = 0 as well. (
http://hol-theorem-prover.org/kananaskis-10-helpdocs/help/src-sml/htmlsigs/arithmeticTheory.html#DIVMOD_DEF-val).
(I couldn't quite tell the result for mod 0, perhaps an expert can opine.)

   - The Intel reference manual says #DE flag is raised and otherwise says
nothing about what the result should be:  (Volume 2A, page 3-407 of
http://www.intel.com/content/dam/www/public/us/en/documents/manuals/64-ia-32-architectures-software-developer-instruction-set-reference-manual-325383.pdf
)

In the x86 case (and from my personal experience), if an instruction raises
a pre-computation-flag (such as the #DE here), then the result is a don't
care; i.e., the architecture is free to populate the destination
register/location with any value. (i.e., Intel does *not* guarantee to keep
returning the same value in this case, whatever that might happen to be.)

Given this folklore, wouldn't it be better to align with the
Theorem-proving community where the consensus seems to be defining div-by-0
to be 0? I think one of the most important "customers" of the SMT
technology is actually other theorem-provers as they ship subgoals to SMT
solvers, so it would be beneficial to take into account how they interpret
division by zero in making this choice. For hardware folks, there's already
the flags/exceptions they have to deal with and the SMTLib standard has no
notion of such flags/exceptions anyhow, so picking a result of all 1's
seems to be inferior to leaving it uninterpreted.

-Levent.


On Wed, Oct 14, 2015 at 10:08 PM, Clark Barrett <barrett at cs.nyu.edu> wrote:

> Hi all,
>
> We've had many discussions about the semantics of division by zero in the
> bit-vector theory.  After the most recent discussion at the SMT workshop,
> it became clear that the arguments for fixing an interpretation seem to
> outweigh the arguments for the current semantics.  So, we are proposing to
> change the semantics of bit-vector division so that division by zero
> produces a vector of all 1's.  The rationale is:
>
> 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.
>
> A new version of bit-vectors with this proposed change will be available
> for comment soon.  In the meantime, feedback is welcome.
>
> -Clark
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>