`udiv_bitvec` does not check for a second operand of `0`

[aytey]

When targeting 32-bit Windows (I have not tried 64-bit Windows, sorry), I get an assertion error when running ./bin/test.exe udiv_bitvec.

To diagnose this failure, I modified test/testbv.c as follows (the print of bv1 and bv2 is superfluous, given the print of a1 and a2, but that shouldn't change anything):

-    assert (ares == bres);
+    if (ares != bres)
+    {
+        printf("***\n");
+        printf("bv1 = %" PRIu64 "\n", btor_bv_to_uint64(bv1));
+        printf("bv2 = %" PRIu64 "\n", btor_bv_to_uint64(bv2));
+        printf("a1 = %" PRIu64 "\n", a1);
+        printf("a2 = %" PRIu64 "\n", a2);
+        printf("ares = %" PRIu64 "\n", ares);
+        printf("bres = %" PRIu64 "\n", bres);
+        printf("***\n");
+    }
+    // assert (ares == bres);

and I get the following output:

***
bv1 = 4294978274
bv2 = 0
a1 = 4294978274
a2 = 0
ares = 4294967295
bres = 8589934591
***
***
bv1 = 12315
bv2 = 0
a1 = 12315
a2 = 0
ares = 4294967295
bres = 8589934591
***
***
bv1 = 19733
bv2 = 0
a1 = 19733
a2 = 0
ares = 4294967295
bres = 8589934591
***

So, of the 100000 tests that get run, we only see assertion failures when a2 is 0.

This particular test does this:

  binary_bitvec (udiv, btor_bv_udiv, BTOR_TEST_BITVEC_TESTS, 33);

where the last argument is the bit-width (33 in this case). Furthermore the function udiv looks like this:

udiv (uint64_t x, uint64_t y, uint32_t bw)
{
  if (y == 0) return UINT32_MAX % (uint64_t) pow (2, bw);
  return (x / y) % (uint64_t) pow (2, bw);
}

So, for udiv, if the second argument (== bv2) is 0, then it returns something based off of UINT32_MAX, while I imagine (and I haven't checked) that btor_bv_udiv is "width agnostic". Furthermore, all of the variables inside of the function binary_bitvec (the callee of udiv) are uint64_ts.

Interestingly, when I run this test (with these prints) on 32-bit Linux, then the lowest value I get for bv1/a1 is 48121 and the lowest for bv2/a2 is 96199 (i.e., I never seem to get 0 for bv2).

If I create a hand-written test on any Linux architecture (both 32-bit and 64-bit) that does something like this:

void udiv_zero_test(void)
{
  BtorBitVector *bv1, *bv2, *res;
  uint64_t a1, a2, ares, bres;
  uint32_t bit_width = 33;

  // 12315 and 0 come from the failing Windows tests
  bv1  = btor_bv_uint64_to_bv (g_mm, 12315, bit_width);
  bv2  = btor_bv_uint64_to_bv (g_mm, 0, bit_width);
  res  = btor_bv_udiv(g_mm, bv1, bv2);
  a1   = btor_bv_to_uint64 (bv1);
  a2   = btor_bv_to_uint64 (bv2);
  ares = udiv(a1, a2, bit_width);
  bres = btor_bv_to_uint64 (res);
  if (ares != bres)
  {
      printf("***\n");
      printf("bv1 = %" PRIu64 "\n", btor_bv_to_uint64(bv1));
      printf("bv2 = %" PRIu64 "\n", btor_bv_to_uint64(bv2));
      printf("a1 = %" PRIu64 "\n", a1);
      printf("a2 = %" PRIu64 "\n", a2);
      printf("ares = %" PRIu64 "\n", ares);
      printf("bres = %" PRIu64 "\n", bres);
      printf("***\n");
  }
  // assert (ares == bres);
  btor_bv_free (g_mm, res);
  btor_bv_free (g_mm, bv1);
  btor_bv_free (g_mm, bv2);
}

(rather than the call to random_bv) then I do see this failure (again, on any Linux architecture).

Importantly: if I change the function udiv to do its modulo calculation based up on UINT64_MAX then the tests no longer fail!

Some questions:

1. Is it correct that random_bv can return 0?
2. What does it mean that random_bv never returns 0 on Linux, but does on Windows (maybe rand() is just "less random" on Windows)?
3. Is there an issue that Boolector has no tests that explicitly check bv2 being 0?
4. Is it correct that udiv does its modulo calculations based off UINT32_MAX when working on 64-bit operands?

If you are happy, I would suggest that we:

1. Create a new bit-vector test-suite that does the same as udiv_bitvec, but where bv2 is always hard-coded to be 0 (maybe something like: udiv_bitvec_zero)
2. Modify the udiv function to base its calculations off of UINT64_MAX

I am more than happy to do this work.

[aniemetz]

@andrewvaughanj Good catch!

The issue here is indeed the udiv function in testbv.c, which obviously must use UINT64_MAX since the types are uint64_t. Good question why this came up with Windows, but not with Linux. In theory, rand() should return 0 on occasion, but very rarely so, probably. So yes, maybe it is less random on Windows?

I fixed the tests a bit differently than you suggested. Can you check if you still encounter problems with https://github.com/Boolector/boolector/commit/f689fbbfe820392d35e26be368f9d87d2dbdb037?

[aytey]

@aniemetz thanks for taking a look!

Everything now looks good to me (the important thing was the UINT32_MAX change):

Finished 1300 tests:
  Number of tests skipped: 19
  Number of tests succeeded: 1281
  Number of files successfully compared: 775/775

[aniemetz]

Great! Thanks for checking!