C and interpreter test results do not match for this module.

[WilliamDue]

Note: sorry for the code snippet not being more concise, I was not able to shorten it anymore.

How to replicate the error

The following code results in the problem.

-- | file: error.fut
module type bitset = {
  type bitset[n]
  val nbs : i64
  val empty : (n : i64) -> bitset[(n - 1) / nbs + 1]
  val complement [n] : bitset[(n - 1) / nbs + 1] -> bitset[(n - 1) / nbs + 1]
  val size [n] : bitset[(n - 1) / nbs + 1] -> i64
}

module mk_bitset (I: integral) : bitset = {
  def nbs = i64.i32 I.num_bits
  type bitset [n] = [n]I.t
  def zero : I.t = I.i64 0
  
  def empty (n : i64) : bitset[(n - 1) / nbs + 1] =
    replicate ((n - 1) / nbs + 1) zero

  def set_front_bits_zero [n] (s : bitset[(n - 1) / nbs + 1]) : bitset[(n - 1) / nbs + 1] =
    let l = (n - 1) / nbs + 1
    let start = 1 + (n - 1) % nbs
    let to_keep = I.i64 (i64.not (i64.not 0 << start))
    in if l == 0
       then s
       else copy s with [l - 1] = s[l - 1] I.& to_keep
  
  def complement [n] (s : bitset[(n - 1) / nbs + 1]) : bitset[(n - 1) / nbs + 1] =
    map I.not s
    |> set_front_bits_zero
  
  def size [n] (s : bitset[(n - 1) / nbs + 1]) : i64 =
    map (i64.i32 <-< I.popc) s
    |> i64.sum
}

module bitset_u8 = mk_bitset u8
-- ==
-- entry: test_complement
-- input { 0u8 } output { 0i64 }
-- input { 1u8 } output { 1i64 }
-- input { 2u8 } output { 2i64 }
-- input { 8u8 } output { 8i64 }
entry test_complement (c : u8) : i64 =
  let c' = i64.u8 c
  let empty_set = bitset_u8.empty c'
  let full_set = bitset_u8.complement empty_set
  let result = bitset_u8.size full_set
  in result

The module creates an array with a given size which is used as a bitset. To compute the complement I not every element in the array and I remove the leading bits using set_front_bits_zero. The test creates a full bitset and asserts that it matches the capacity of the bitset.

When I test it using the c backend futhark test --no-terminal error.fut, I get the test result.

error.fut:
Compiling with --backend=c:
Running compiled program:
Running ./error:
Entry point: test_complement; dataset: #1 ("1u8"):
error.fut.test_complement.1.actual and error.fut.test_complement.1.expected do not match:
Value #0: expected 1, got 8
Entry point: test_complement; dataset: #2 ("2u8"):
error.fut.test_complement.2.actual and error.fut.test_complement.2.expected do not match:
Value #0: expected 2, got 8
0/1 passed.

While using the interpreter futhark test --no-terminal -i error.fut result in 1/1 passed..

I believe the problem arises at set_front_bits_zero, it ends up setting every bit 0 at the last index. Instead of only setting the bits that are not used to 0.

Version

Futhark 0.26.0 (prerelease - include info below when reporting bugs)
git: 0c5319357fc1a334117e817abc85fce1abbb8d0a

[athas]

This looks like a bug in the tracking of size parameters in a complex case. Here is a simpler program that still produces different results with the interpreter and compiler:

def empty (n : i64) : [(n - 1) / 8 + 1]u8 =
  replicate ((n - 1) / 8 + 1) 0

def get_n [n] (_s : [(n - 1) / 8 + 1]u8) =
  n

def complement [n] (s : [(n - 1) / 8 + 1]u8) =
  get_n s

entry test_complement (c' : i64) =
  complement (empty c')

Since the same type checker is used in both cases, the difference must lie in one of the frontend passes. It is the interpreter that produces the correct result.

[athas]

Yes, it is clear that monomorphisation cannot figure out which size argument to pass to get_n. For some reason it gets complement right.

[athas]

@catvayor Do you have time to take a look at this? You're the last one to touch this code I think. Something nonobvious is going wrong in dimMapping I think.