Range-based vector extension failure

[adpaco-aws]

While working on #184 I discovered that the code

fn main() {
    let mut v: Vec<u32> = Vec::new();
    v.extend(42..=42);
    assert!(v[0] == 42);
}

fails to verify with RMC. The cause of this failure is:

/home/ubuntu/rmc-rebase-3/library/core/src/slice/index.rs function _RNvXs0_NtNtCsbJgkeTxzpXM_4core5slice5indexjINtB5_10SliceIndexSmE5indexCs21hi0yVfW1J_10extend_min
[_RNvXs0_NtNtCsbJgkeTxzpXM_4core5slice5indexjINtB5_10SliceIndexSmE5indexCs21hi0yVfW1J_10extend_min.assertion.1] line 184 index out of bounds: the length is move _4 but the index is _3: FAILURE

And the corresponding C code for that function:

// _RNvXs0_NtNtCsbJgkeTxzpXM_4core5slice5indexjINtB5_10SliceIndexSmE5indexCs21hi0yVfW1J_10extend_min
// file /home/ubuntu/rmc-rebase-3/library/core/src/slice/index.rs line 182 column 5 function _RNvXs0_NtNtCsbJgkeTxzpXM_4core5slice5indexjINtB5_10SliceIndexSmE5indexCs21hi0yVfW1J_10extend_min
unsigned int * _RNvXs0_NtNtCsbJgkeTxzpXM_4core5slice5indexjINtB5_10SliceIndexSmE5indexCs21hi0yVfW1J_10extend_min(unsigned long int self, struct [u32] slice)
{
  unsigned int *var_0;
  unsigned long int var_3;
  unsigned long int var_4;
  _Bool var_5;

bb0:
  ;
  var_3 = self;
  var_4 = slice.len;
  var_5 = var_3 < var_4;
  if(var_5 == 0)
    /* index out of bounds: the length is move _4 but the index is _3 */
    assert(0);


bb1:
  ;
  var_0 = &slice.data[var_3];
  return var_0;
}

The trace shows that the length stored in var_4 is 0, which is why the assertion fails.

[adpaco-aws]

This example continues to be a problem since debugging can only be done looking at the C code generated (which cannot be compiled with gcc). The following example (the "push example") can be verified:

fn main() {
    let mut v: Vec<u32> = Vec::new();
    v.push(42);
    assert!(v[0] == 42);
}

But the extend example is a bit more complicated.

The main problem seems to be in how the vector is handled. For example, in the push example the push function is in charge of incrementing the vector:

struct Unit _RNvMs_NtCsjPaGuRiS19R_5alloc3vecINtB4_3VecmE4pushCs21hi0yVfW1J_10push_range(struct std::vec::Vec<u32> *self, unsigned int value)
{
[...]
bb8:
  ;
  self->len = self->len + 1;
  return VoidUnit;
/* resume instruction */
[...]
}

But this is not done in the same way in the case of the extend example, where the vector goes through a series of transformations before being extended (and functions from raw_vec.rs, spec_extend.rs are used for that).

[chinmaydd]

This issue is rooted in the way the length of a vector is set when the vector is extended with an iterator. Another example which reproduces this issue:

fn main() {
    let mut v: Vec<u32> = Vec::new();
    v.extend([42]);
    // FAILURE!
    assert!(v.len() == 1);
}

The spec_extend function (which is called by extend) uses the SetLenOnDrop struct which allows the compiler to get around a potential aliasing issue. SetLenOnDrop uses a local variable to track the length of the vector during the spec_extend function, which it assigns to the actual vector in its Drop implementation.

Currently, rmc codegens a Stmt::Skip for any DropGlue which causes the length of the original vector to be kept at 0. A potential remedy could be to codegen a call to the DropGlue function or add a special case for structs like SetLenOnDrop which have effect on soundness.

[adpaco-aws]

Good job on finding the root cause for this failure!!

I think that properly codegening DropGlue would be the sensible thing to do in this case.

[chinmaydd]

This issue has been fixed by #402 .